Fundamental theorem of statistical learning (5-way equivalence, BP₅).
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool)
[MeasurableConceptClass X C],
(PACLearnable X C ↔ VCDim X C < ⊤) ∧
(VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k) ∧
(VCDim X C < ⊤ ↔
∀ ε > 0,
∃ m₀,
∀ (D : MeasureTheory.Measure X),
MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) ∧
(PACLearnable X C →
∃ L mf,
(∀ (ε δ : ℝ),
0 < ε →
0 < δ →
∀ (D : MeasureTheory.Measure X),
MeasureTheory.IsProbabilityMeasure D →
∀ c ∈ C,
(MeasureTheory.Measure.pi fun x => D)
{xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥
ENNReal.ofReal (1 - δ)) ∧
(∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ) ∧
∀ (d : ℕ),
VCDim X C = ↑d →
∀ (ε δ : ℝ),
0 < ε →
ε ≤ 1 / 4 →
0 < δ →
δ ≤ 1 →
δ ≤ 1 / 7 →
1 ≤ d → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ ∧ ⌈(↑d - 1) / 2⌉₊ ≤ mf ε δ) ∧
(VCDim X C < ⊤ ↔ ∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i)- Declfundamental_theoremDeclaration kindtheorem
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C], (PACLearnable X C ↔ VCDim X C < ⊤) ∧ (VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k) ∧ (VCDim X C < ⊤ ↔ ∀ ε > 0, ∃ m₀, ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) ∧ (PACLearnable X C → ∃ L mf, (∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥ ENNReal.ofReal (1 - δ)) ∧ (∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ) ∧ ∀ (d : ℕ), VCDim X C = ↑d → ∀ (ε δ : ℝ), 0 < ε → ε ≤ 1 / 4 → 0 < δ → δ ≤ 1 → δ ≤ 1 / 7 → 1 ≤ d → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ ∧ ⌈(↑d - 1) / 2⌉₊ ≤ mf ε δ) ∧ (VCDim X C < ⊤ ↔ ∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i) - Declvc_characterizationDeclaration kindtheorem
VC characterization: C is PAC-learnable iff VCDim(C) < ∞.
PROOF DECOMPOSITION: This theorem factors through the two directions above: ← : vcdim_finite_imp_uc + uc_imp_pac (in Generalization.lean) → : pac_imp_vcdim_finite (contrapositive via double-sample)
HC at this joint: The ← direction crosses from combinatorics (VCDim, GrowthFunction) to measure theory (Measure.pi, TrueError). The → direction crosses from measure theory back to combinatorics. Both crossings have HC > 0.
UK₈: The ↔ hides an ASYMMETRY: the ← proof is constructive (produces ERM), while the → proof is non-constructive (produces hard distribution).
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C], PACLearnable X C ↔ VCDim X C < ⊤
Used by
- Declvcdim_finite_imp_pacDeclaration kindtheorem
Direction ←: finite VCDim implies PAC learnability.
PROOF ROUTE (via new infrastructure in Generalization.lean): Step 1: VCDim < ∞ → HasUniformConvergence (vcdim_finite_imp_uc) Sub-step 1a: Sauer-Shelah gives GrowthFunction bound Sub-step 1b: Symmetrization reduces UC to growth function counting Sub-step 1c: Concentration inequality closes the bound Step 2: HasUniformConvergence → PACLearnable (uc_imp_pac) Sub-step 2a: Construct ERM learner Sub-step 2b: ERM is consistent in realizable case Sub-step 2c: Consistent + UC → low TrueError
KU₁₈: C.Nonempty is needed for ERM but not stated as hypothesis. If C = ∅, then PACLearnable is vacuously true (∀ c ∈ C, ... is vacuous). But ERM needs a fallback hypothesis from C. Is this a genuine gap or does the empty case work out vacuously?
Counterdefinition (COUNTER-4): If the ERM approach fails for computational reasons (ERM is noncomputable, and we need a computable learner for computational learning theory), swap to the compression-based proof: VCDim < ∞ → finite compression scheme (Moran-Yehudayoff 2016) → compression scheme learner is PAC. Swap condition: When proving COMPUTATIONAL PAC learnability (polynomial time).
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool), VCDim X C < ⊤ → ∀ [MeasurableConceptClass X C], PACLearnable X C
BatchLearnerBatchLearner.learnConceptClassFLT.ConceptMeasurableConceptClassPACLearnableVCDimWellBehavedVCUses
Used by
- Declpac_sample_complexity_sandwichDeclaration kindtheorem
Quantitative sample-complexity sandwich attached to any PAC witness. Packages: (1) PAC guarantee, (2) SampleComplexity ≤ mf, (3) NFL/VC lower bound on both SampleComplexity and mf.
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C], PACLearnable X C → ∃ L mf, (∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥ ENNReal.ofReal (1 - δ)) ∧ (∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ) ∧ ∀ (d : ℕ), VCDim X C = ↑d → ∀ (ε δ : ℝ), 0 < ε → ε ≤ 1 / 4 → 0 < δ → δ ≤ 1 → δ ≤ 1 / 7 → 1 ≤ d → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ ∧ ⌈(↑d - 1) / 2⌉₊ ≤ mf ε δBatchLearnerBatchLearner.learnConceptClassFLT.ConceptMeasurableConceptClassPACLearnableSampleComplexityVCDimWellBehavedVCUses
Used by
- Declsample_complexity_upper_of_pac_witnessDeclaration kindtheorem
Any PAC witness (L, mf) gives an upper bound on SampleComplexity: the infimum is at most the witness sample size.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) (L : BatchLearner X Bool) (mf : ℝ → ℝ → ℕ), (∀ (ε δ : ℝ), 0 < ε → 0 < δ → ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥ ENNReal.ofReal (1 - δ)) → ∀ (ε δ : ℝ), 0 < ε → 0 < δ → SampleComplexity X C ε δ ≤ mf ε δ - Declsample_complexity_lower_boundDeclaration kindtheorem
Sample complexity lower bound: ⌈(d-1)/2⌉ ≤ SampleComplexity.
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (d : ℕ), VCDim X C = ↑d → ∀ (ε δ : ℝ), 0 < ε → ε ≤ 1 / 4 → 0 < δ → δ ≤ 1 → δ ≤ 1 / 7 → 1 ≤ d → (∀ h ∈ C, Measurable h) → (∀ (c : Concept X Bool), Measurable c) → WellBehavedVC X C → ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ - Declpac_lower_bound_memberDeclaration kindtheorem
PAC lower bound membership: if m achieves PAC for C with VCDim = d, then m ≥ ⌈(d-1)/(64ε)⌉. This is the core adversarial counting argument factored for PAC.lean assembly. Note: the tight constant is (d-1)/(2ε) (EHKV 1989); see EHKV.lean.
Proof route (double-averaging on shattered set): 1. VCDim = d → ∃ shattered S with |S| = d 2. D = uniform on S (probability measure, each point has weight 1/d) 3. m < ⌈(d-1)/(64ε)⌉ → 2m < d → NFL counting applies 4. Double-averaging over 2^d labelings: E_f[E_xs[error]] ≥ (d-m)/(2d) > 1/4 5. Reversed Markov: ∃ c₀ ∈ C with Pr[error ≤ 1/8] ≤ 6/7 6. For ε ≤ 1/8: Pr[error ≤ ε] ≤ 6/7 = 1 - 1/7, contradicting PAC
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (d : ℕ), VCDim X C = ↑d → ∀ (ε δ : ℝ), 0 < ε → ε ≤ 1 / 4 → 0 < δ → δ ≤ 1 → δ ≤ 1 / 7 → 1 ≤ d → ∀ m ∈ {m | ∃ L, ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ c ∈ C, (MeasureTheory.Measure.pi fun x => D) {xs | D {x | L.learn (fun i => (xs i, c (xs i))) x ≠ c x} ≤ ENNReal.ofReal ε} ≥ ENNReal.ofReal (1 - δ)}, ⌈(↑d - 1) / 2⌉₊ ≤ m - Declgrowth_bounded_imp_vcdim_finiteDeclaration kindtheorem
Growth function polynomially bounded → VCDim < ⊤. Reverse direction: if GrowthFunction m ≤ ∑_{i≤d} C(m,i) for all m ≥ d, then VCDim ≤ d (otherwise GrowthFunction = 2^m for m = VCDim > d).
∀ (X : Type u) (C : ConceptClass X Bool), (∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i) → VCDim X C < ⊤
Used by
- Declfundamental_vc_compressionDeclaration kindtheorem
Fundamental theorem: finite VC dim ↔ finite compression scheme with side information. Moran-Yehudayoff 2016 (arXiv:1503.06960). Sorry-free via Compression.lean. Γ₇₃ RESOLVED: CompressionSchemeWithInfo parameterized by concept class C. The no-side-info version (Littlestone-Warmuth conjecture) remains open.
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k
Used by
- Declfundamental_vc_compression_with_infoDeclaration kindtheorem
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ ↔ ∃ k cs, CompressionSchemeWithInfo.size cs = k
Used by
- Declvcdim_finite_imp_compression_with_infoDeclaration kindtheorem
The forward direction of the Moran-Yehudayoff theorem: finite VC dimension implies existence of a compression scheme with finite side information.
The construction: 1. Build a proper finite-support learner L from VC + Sauer-Shelah 2. For sample S: extract c, Y = pointSupport S, HY = hypothesis envelope 3. Apply approximate minimax on the agreement game → distribution p on HY 4. Apply VC ε-approximation on agreement tests → T representative hypotheses 5. Kernel = union of witness subsets for T hypotheses 6. Side info = incidence: which hypothesis's witness contains each kernel point 7. Reconstruct by majority vote over T hypotheses
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ → ∃ k cs, CompressionSchemeWithInfo.size cs = k
- Declvcdim_finite_imp_proper_finite_support_learnerDeclaration kindtheorem
Finite VC dimension implies existence of a proper finite-support learner. The construction uses ERM + finite_support_vc_approx on the disagreement family.
∀ (X : Type u) (C : ConceptClass X Bool), Set.Nonempty C → VCDim X C < ⊤ → ∃ _L, True
ConceptClassFLT.ConceptFinitePMFFinset.boolVCDimProperFiniteSupportLearnerVCDimboolTestExpectationdisagreementFamilyempiricalPMFlabeledSampleOfFinsetsupportErrorUses
- DeclsupportError_eq_boolTestExpectationDeclaration kindtheorem
supportError expressed in terms of boolTestExpectation of a disagreement test.
∀ {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool), supportError Y q h c = boolTestExpectation q fun y => decide (h ↑y ≠ c ↑y) - DecldisagreementFamily_boolVCDim_leDeclaration kindtheorem
VC dimension of the disagreement family is bounded by VCDim(C). Restriction to Y and xor with c do not increase shattering dimension.
∀ {X : Type u} [inst : DecidableEq X] (C : ConceptClass X Bool) (c : X → Bool) (Y : Finset X) {d : ℕ}, VCDim X C ≤ ↑d → (disagreementFamily✝ C c Y).boolVCDim ≤ d - Declmoran_yehudayoff_forward_constructionDeclaration kindtheorem
The Moran-Yehudayoff forward construction. Uses
finalizeIncidenceSchemeto package the majority-vote scheme with universe-correct Info type.The agent must provide:
compressCore,blockHyp,rowHyp,hsmall,hsub,hagree,hmajor. These are the MY wiring.∀ (X : Type u) (C : ConceptClass X Bool), Set.Nonempty C → ∀ (L : ProperFiniteSupportLearner X C), VCDim X C < ⊤ → ∀ (_K : ℕ), ∃ k cs, CompressionSchemeWithInfo.size cs = kCompressionSchemeWithInfo.sizeCompressionSchemeWithInfo0ConceptClassFLT.ConceptFinitePMFFinitePMF.probFinset.boolVCDimIncidenceInfoProperFiniteSupportLearnerProperFiniteSupportLearner.learnProperFiniteSupportLearner.sampleBoundVCDimagreeTestagreeTestsboolGamePayoffboolTestExpectationboundedSubsamplesdecodeWitnessLabeldecodeWitnessXCoordsempiricalPMFencodeWitnessInfohypothesisEnvelopelabeledSampleOfFinsetpointSupportuniformPMFUses
- Declroundtrip_blockHyp_eq_repDeclaration kindtheorem
Generic roundtrip theorem for the
hroundsorry.If:
encodeWitnessInfois used incompressCore,decodeWitnessXCoordsanddecodeWitnessLabelare used inblockHyp, and- the kernel contains the witness pairs with the correct labels,
then the decoded block hypothesis is exactly the representative hypothesis.
∀ {X : Type u} [inst : DecidableEq X] (learn : {m : ℕ} → (Fin m → X × Bool) → X → Bool) (kernel : Finset (X × Bool)) (c : X → Bool) (K : ℕ) (W : Finset X) (h : X → Bool), kernel.card ≤ K → (∀ x ∈ W, (x, c x) ∈ kernel) → (∀ p ∈ kernel, p.2 = c p.1) → learn (labeledSampleOfFinset c W) = h → ∀ (x : X), have info := encodeWitnessInfo kernel c K W; have blockXCoords := decodeWitnessXCoords kernel info; have blockLabel := decodeWitnessLabel kernel; learn (labeledSampleOfFinset blockLabel blockXCoords) x = h xUses
- DecllabeledSampleOfFinset_eq_of_eq_on_supportDeclaration kindtheorem
If two label functions agree on all points of
Z, then the labeled samples they induce onZ.equivFinare equal.∀ {X : Type u} [DecidableEq X] {ℓ₁ ℓ₂ : X → Bool} {Z : Finset X}, (∀ x ∈ Z, ℓ₁ x = ℓ₂ x) → labeledSampleOfFinset ℓ₁ Z = labeledSampleOfFinset ℓ₂ ZUsed by
- DecldecodeWitnessXCoords_encode_eqDeclaration kindtheorem
If every
(x, c x)withx ∈ Wlies inkernel, andkernel.card ≤ K, then decoding the encoded witness positions gives back exactlyW.∀ {X : Type u} [inst : DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) {K : ℕ} (W : Finset X), kernel.card ≤ K → (∀ x ∈ W, (x, c x) ∈ kernel) → decodeWitnessXCoords kernel (encodeWitnessInfo kernel c K W) = WUsed by
- DecldecodeWitnessLabel_eq_on_encodedDeclaration kindtheorem
On the encoded witness support, the decoded label function agrees with the true label function
c, provided every pair in the kernel has the correct second coordinate.∀ {X : Type u} [inst : DecidableEq X] (kernel : Finset (X × Bool)) (c : X → Bool) (W : Finset X), (∀ x ∈ W, (x, c x) ∈ kernel) → (∀ p ∈ kernel, p.2 = c p.1) → ∀ x ∈ W, decodeWitnessLabel kernel x = c xUsed by
- Declmwu_approx_minimaxDeclaration kindtheorem
Genuine approximate minimax via MWU regret extraction. If every column mixture admits a pure row with expected payoff ≥ v, then there is a row mixture with payoff ≥ v - ε against every column.
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [Nonempty R] [Nonempty C] [DecidableEq R] [DecidableEq C] (M : R → C → Bool) (v ε : ℝ), 0 < ε → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → ∃ p, ∀ (c : C), v - ε ≤ boolGamePayoff M p cFinitePMFFinitePMF.probMWUConfig.potentialMWUConfig.weightsboolGamePayoffempiricalPMFmwuConfigmwuHitCountmwuRowsuniformPMFUses
- Declweight_le_potentialDeclaration kindtheorem
A single weight is bounded by the potential.
∀ {C : Type u_1} [inst : Fintype C] (cfg : MWUConfig C) (c : C), cfg.weights c ≤ cfg.potentialUsed by
- Declmwu_weight_eq_pow_hitCountDeclaration kindtheorem
Exact individual-weight tracking: the weight of column
cafterTrounds is(1-η)to the number of rounds in whichcwas hit.∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (T : ℕ) (c : C), (mwuConfig M η hη1 v hrow T).weights c = (1 - η) ^ mwuHitCount✝ M η hη1 v hrow T cFinitePMFFinitePMF.probMWUConfigMWUConfig.toPMFMWUConfig.weightsmwuConfigmwuHitCountmwuRunmwuUpdateWeightsUsed by
- DeclMWUConfig.mk.congr_simpDeclaration kindtheorem
∀ {C : Type u_1} [inst : Fintype C] (weights weights_1 : C → ℝ) (e_weights : weights = weights_1) (weights_pos : ∀ (c : C), 0 < weights c), { weights := weights, weights_pos := weights_pos } = { weights := weights_1, weights_pos := ⋯ }Used by
- Declmwu_potential_T_boundDeclaration kindtheorem
Potential bound after T steps: Φ_T ≤ |C| · (1 - ηv)^T.
This is the core MWU guarantee. Combined with individual weight lower bounds (w_T(c) = (1-η)^{losses(c)}), it yields the regret bound.
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool) (η : ℝ), 0 ≤ η → ∀ (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (T : ℕ), (mwuConfig M η hη1 v hrow T).potential ≤ ↑(Fintype.card C) * (1 - η * v) ^ TUsed by
- Declpotential_one_step_boundDeclaration kindtheorem
Potential bound after one step: Φ' ≤ Φ · (1 - η·v).
∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [inst_1 : Nonempty C] (M : R → C → Bool) (η : ℝ), 0 ≤ η → ∀ (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (cfg : MWUConfig C), (mwuUpdateWeights M η hη1 cfg ⋯.choose).potential ≤ cfg.potential * (1 - η * v)Used by
- Declbest_response_payoff_weightsDeclaration kindtheorem
Best response payoff ≥ v · Φ in terms of weights.
∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [inst_1 : Nonempty C] (M : R → C → Bool) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (cfg : MWUConfig C), v * cfg.potential ≤ ∑ c, cfg.weights c * if M ⋯.choose c = true then 1 else 0Used by
- DeclMWUConfig.potential_posDeclaration kindtheorem
∀ {C : Type u_1} [inst : Fintype C] [Nonempty C] (cfg : MWUConfig C), 0 < cfg.potentialUsed by
- DeclMWUConfig.weights_posDeclaration kindtheorem
∀ {C : Type u_1} [inst : Fintype C] (self : MWUConfig C) (c : C), 0 < self.weights c - DeclmwuUpdateWeights.congr_simpDeclaration kindtheorem
∀ {C : Type u_1} [inst : Fintype C] {R : Type u_2} (M M_1 : R → C → Bool), M = M_1 → ∀ (η η_1 : ℝ) (e_η : η = η_1) (hη1 : η < 1) (cfg cfg_1 : MWUConfig C), cfg = cfg_1 → ∀ (r r_1 : R), r = r_1 → mwuUpdateWeights M η hη1 cfg r = mwuUpdateWeights M_1 η_1 ⋯ cfg_1 r_1Used by
- DeclmwuInit_potentialDeclaration kindtheorem
∀ (C : Type u_1) [inst : Fintype C], (mwuInit C).potential = ↑(Fintype.card C)
Used by
- Declminimax_value_le_oneDeclaration kindtheorem
The minimax value of a Boolean game is at most 1.
∀ {R : Type u_1} {C : Type u_2} [Fintype R] [inst : Fintype C] [Nonempty C] (M : R → C → Bool) (v : ℝ), (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → v ≤ 1 - DeclhitRate_from_potentialDeclaration kindtheorem
Arithmetic core: from the potential bound and sufficiently small η / large T, deduce a per-column hit-rate lower bound. Uses Real.log — exactly 4 Mathlib lemmas.
∀ {N H T : ℕ} {η v ε : ℝ}, 0 < ↑N → 0 < η → η < 1 → v ≤ 1 → 0 < T → (1 - η) ^ H ≤ ↑N * (1 - η * v) ^ T → η ≤ ε / 4 → Real.log ↑N / (η * ↑T) ≤ ε / 4 → v - ε ≤ ↑H / ↑TUsed by
- DeclboolGamePayoff_nonnegDeclaration kindtheorem
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] (M : R → C → Bool) (p : FinitePMF R) (c : C), 0 ≤ boolGamePayoff M p cUsed by
- DeclboolGamePayoff_empirical_eq_hitCountDeclaration kindtheorem
Empirical payoff of the MWU row sequence equals the normalized hit count.
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] [inst_3 : DecidableEq R] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) {T : ℕ} (hT : 0 < T) (c : C), boolGamePayoff M (empiricalPMF hT (mwuRows M η hη1 v hrow T)) c = ↑(mwuHitCount✝ M η hη1 v hrow T c) / ↑TUsed by
- DeclmwuHitCount_eq_sum_indicatorDeclaration kindtheorem
The recursive hit counter agrees with the sum of Boolean indicators over the emitted row sequence.
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : Fintype C] [inst_2 : Nonempty C] (M : R → C → Bool) (η : ℝ) (hη1 : η < 1) (v : ℝ) (hrow : ∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) (T : ℕ) (c : C), ↑(mwuHitCount✝ M η hη1 v hrow T c) = ∑ t, if M (mwuRows M η hη1 v hrow T t) c = true then 1 else 0 - DeclboolGamePayoff_empirical_eq_avgDeclaration kindtheorem
Specialized empirical-payoff identity for ApproxMinimax (avoids cyclic import with FiniteVCApprox).
∀ {R : Type u_1} {C : Type u_2} [inst : Fintype R] [inst_1 : DecidableEq R] {T : ℕ} (hT : 0 < T) (rs : Fin T → R) (M : R → C → Bool) (c : C), boolGamePayoff M (empiricalPMF hT rs) c = (∑ t, if M (rs t) c = true then 1 else 0) / ↑T - DeclhypothesisEnvelope_subDeclaration kindtheorem
Every hypothesis in the envelope is in C.
∀ {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C) (c : X → Bool) (Y : Finset X), ∀ h ∈ hypothesisEnvelope L c Y, h ∈ C - DeclProperFiniteSupportLearner.output_memDeclaration kindtheorem
∀ {X : Type u} {C : ConceptClass X Bool} (self : ProperFiniteSupportLearner X C) {m : ℕ} (S : Fin m → X × Bool), self.learn S ∈ CUsed by
- Declgood_on_support_gives_row_responseDeclaration kindtheorem
For each C-realizable sample, the proper learner provides a row-response for the minimax game on the hypothesis envelope.
∀ {X : Type u} {C : ConceptClass X Bool} (L : ProperFiniteSupportLearner X C), ∀ c ∈ C, ∀ (Y : Finset X) [Nonempty ↥Y] (HY : Finset (X → Bool)), HY = hypothesisEnvelope L c Y → ∀ (q : FinitePMF ↥Y), ∃ h, 2 / 3 ≤ ∑ y, q.prob y * if decide (↑h ↑y = c ↑y) = true then 1 else 0 - DeclsupportAgreement_eq_one_sub_supportErrorDeclaration kindtheorem
Weighted agreement = 1 - supportError.
∀ {X : Type u} (Y : Finset X) (q : FinitePMF ↥Y) (h c : X → Bool), (∑ y, q.prob y * if h ↑y = c ↑y then 1 else 0) = 1 - supportError Y q h c - DeclProperFiniteSupportLearner.good_on_supportDeclaration kindtheorem
∀ {X : Type u} {C : ConceptClass X Bool} (self : ProperFiniteSupportLearner X C), ∀ c ∈ C, ∀ (Y : Finset X) (q : FinitePMF ↥Y), ∃ Z ⊆ Y, Z.card ≤ self.sampleBound ∧ supportError Y q (self.learn (labeledSampleOfFinset c Z)) c ≤ 1 / 3 - Declfinite_support_vc_approxDeclaration kindtheorem
Finite-support distributions uniformly approximate any distribution on a VC class. For a class of VC dimension at most
dand anyε > 0, there existsT = T(d, ε)such that every finitely supported distributionμis withinε(uniformly over the class) of some empirical distribution onTpoints. A density-style reduction that lets the approximate minimax / MWU machinery, which lives in finite support, apply to general distributions.∀ (d : ℕ) (ε : ℝ), 0 < ε → ∃ T, ∃ (hT : 0 < T), ∀ {H : Type u_1} [inst : Fintype H] [inst_1 : DecidableEq H] (A : Finset (H → Bool)), A.boolVCDim ≤ d → ∀ (μ : FinitePMF H), ∃ hs, ∀ a ∈ A, |boolTestExpectation μ a - boolTestExpectation (empiricalPMF hT hs) a| ≤ εConceptClassEmpiricalErrorFLT.ConceptFinitePMFFinitePMF.probFinitePMF.toPMFFinset.boolVCDimGrowthFunctionShattersTrueErrorRealVCDimboolFamilyToFinsetFamilyboolTestExpectationempiricalPMFextendBoolliftClasszeroOneLossUses
- DecltrueErrorReal_extend_falseDeclaration kindtheorem
∀ {H : Type u_1} [inst : Fintype H] [DecidableEq H] [inst_2 : MeasurableSpace H] [MeasurableSingletonClass H] (μ : FinitePMF H) (a : H → Bool), TrueErrorReal (H ⊕ ℕ) (extendBool✝ a) (fun x => false) (PMF.map Sum.inl (FinitePMF.toPMF✝ μ)).toMeasure = boolTestExpectation μ aUsed by
- DeclboolTestExpectation_nonnegDeclaration kindtheorem
A convex combination of values in
{0, 1}is nonnegative.∀ {H : Type u_1} [inst : Fintype H] (μ : FinitePMF H) (f : H → Bool), 0 ≤ boolTestExpectation μ fUsed by
- DeclboolTestExpectation_le_oneDeclaration kindtheorem
A convex combination of values in
{0, 1}is at most1.∀ {H : Type u_1} [inst : Fintype H] (μ : FinitePMF H) (f : H → Bool), boolTestExpectation μ f ≤ 1Used by
- DeclFinitePMF.prob_nonnegDeclaration kindtheorem
∀ {H : Type u_1} [inst : Fintype H] (self : FinitePMF H) (h : H), 0 ≤ self.prob h - DeclFinitePMF.prob_sum_oneDeclaration kindtheorem
∀ {H : Type u_1} [inst : Fintype H] (self : FinitePMF H), ∑ h, self.prob h = 1 - DeclfinalizeIncidenceSchemeDeclaration kindtheorem
Final existential wrapper: closes the theorem in the exact form expected.
∀ {X : Type u} {C : ConceptClass X Bool} (T K : ℕ) (compressCore : {m : ℕ} → (Fin m → X × Bool) → Finset (X × Bool) × IncidenceInfo T K) (blockHyp : Finset (X × Bool) → IncidenceInfo T K → Fin T → X → Bool) (rowHyp : {m : ℕ} → (S : Fin m → X × Bool) → (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → Fin T → X → Bool), 0 < T → (∀ {m : ℕ} (S : Fin m → X × Bool), (compressCore S).1.card ≤ K) → (∀ {m : ℕ} (S : Fin m → X × Bool), ↑(compressCore S).1 ⊆ Set.range S) → (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m) (t : Fin T), blockHyp (compressCore S).1 (compressCore S).2 t (S i).1 = rowHyp S hreal t (S i).1) → (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m), (∑ t, if rowHyp S hreal t (S i).1 = (S i).2 then 1 else 0) / ↑T > 1 / 2) → ∃ k cs, CompressionSchemeWithInfo.size cs = k - DeclencodeWitnessInfo.congr_simpDeclaration kindtheorem
∀ {X : Type u} {inst : DecidableEq X} [inst_1 : DecidableEq X] (kernel kernel_1 : Finset (X × Bool)), kernel = kernel_1 → ∀ (c c_1 : X → Bool), c = c_1 → ∀ (K : ℕ) (W W_1 : Finset X), W = W_1 → encodeWitnessInfo kernel c K W = encodeWitnessInfo kernel_1 c_1 K W_1 - DeclboolTestExpectation_empirical_eq_avgDeclaration kindtheorem
Bridges the
FinitePMFview and the sample-average view: the expectation of aBool-valued test under the empirical PMF of a sample equals the sample average(1/T) ∑_t f (s_t). This lets the MWU updates and the approximation transfer principle live in the same distributional framework.∀ {H : Type u_1} [inst : Fintype H] [inst_1 : DecidableEq H] {T : ℕ} (hT : 0 < T) (hs : Fin T → H) (f : H → Bool), boolTestExpectation (empiricalPMF hT hs) f = (∑ t, if f (hs t) = true then 1 else 0) / ↑T - DeclboolGamePayoff_eq_boolTestExpectationDeclaration kindtheorem
Identifies the game-theoretic payoff (a row distribution against a fixed column in the Bool game) with the corresponding test expectation. The translation that lets the MWU regret bound be applied directly to the compression problem.
∀ {R : Type u_1} [inst : Fintype R] [DecidableEq R] {C : Type u_2} (M : R → C → Bool) (p : FinitePMF R) (c : C), boolGamePayoff M p c = boolTestExpectation p fun r => M r c - DeclagreeTests_boolVCDim_leDeclaration kindtheorem
VC dimension of the agreement-test family is bounded by
2^(d+1) - 1, wheredbounds the VC dimension of the concept classC. Uses Assouad's coding argument directly: if a shattered setTin↥HYhas|T| ≥ 2^(d+1), embed bitstrings intoT, extractd+1distinct points fromYvia shattering, and show these points are shattered byC(using the XOR trick whereb(j) = decide(g(x_j) = c(x_j))absorbs the agree/disagree flip).∀ {X : Type u} [DecidableEq X] (C : ConceptClass X Bool) (c : X → Bool) (Y : Finset X) (HY : Finset (X → Bool)), (∀ h ∈ HY, h ∈ C) → ∀ {d : ℕ}, VCDim X C ≤ ↑d → (agreeTests c Y HY).boolVCDim ≤ 2 ^ (d + 1) - 1 - Declcompression_with_info_imp_vcdim_finiteDeclaration kindtheorem
Compression with side info implies finite VC dimension. Proof by pigeonhole: compress is injective on C-realizable labelings (by correctness), but compressed outputs form a bounded set.
∀ (X : Type u) (C : ConceptClass X Bool), (∃ k cs, cs.size = k) → VCDim X C < ⊤
CompressionSchemeWithInfoCompressionSchemeWithInfo.InfoCompressionSchemeWithInfo.compressCompressionSchemeWithInfo.info_finiteCompressionSchemeWithInfo.kernelSizeCompressionSchemeWithInfo.sizeConceptClassFLT.ConceptShattersVCDimUses
- Declshatters_subset_compressionDeclaration kindtheorem
∀ {X : Type u} {C : ConceptClass X Bool} {S T : Finset X}, T ⊆ S → Shatters X C S → Shatters X C T - Declexp_beats_poly_compressionDeclaration kindtheorem
Exponential beats polynomial for the compression pigeonhole argument.
∀ (s : ℕ), (s + 1) ^ 2 * (4 * (s + 1) ^ 2) ^ s < 2 ^ (2 * (s + 1) * (s + 1))
- Declsucc_le_two_pow_compressionDeclaration kindtheorem
∀ (k : ℕ), k + 1 ≤ 2 ^ k
Used by
- Declcompress_with_info_injective_on_labelingsDeclaration kindtheorem
Pigeonhole core: if two C-realizable samples over the same points with different labelings produce the same (kernel, info) pair, correctness forces the labelings to agree.
∀ {X : Type u} {n : ℕ} {C : ConceptClass X Bool} (cs : CompressionSchemeWithInfo X Bool C) (pts : Fin n → X), Function.Injective pts → ∀ (f g : Fin n → Bool), (∃ c ∈ C, ∀ (i : Fin n), c (pts i) = f i) → (∃ c ∈ C, ∀ (i : Fin n), c (pts i) = g i) → ((cs.compress fun i => (pts i, f i)) = cs.compress fun i => (pts i, g i)) → f = g - DeclCompressionSchemeWithInfo.correctDeclaration kindtheorem
Correctness: reconstructed hypothesis agrees with every sample point, when the sample is C-realizable
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y), (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → ∀ (i : Fin m), self.reconstruct (self.compress S).1 (self.compress S).2 (S i).1 = (S i).2 - DeclCompressionSchemeWithInfo.compress_subDeclaration kindtheorem
Compressed set is a subset of the sample
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y), ↑(self.compress S).1 ⊆ Set.range S - DeclCompressionSchemeWithInfo.compress_smallDeclaration kindtheorem
Compressed set is small
∀ {X : Type u} {Y : Type v} {C : ConceptClass X Y} (self : CompressionSchemeWithInfo X Y C) {m : ℕ} (S : Fin m → X × Y), (self.compress S).1.card ≤ self.kernelSize - Declfundamental_rademacherDeclaration kindtheorem
Fundamental theorem: Rademacher complexity characterization. BP₅: two asymmetric directions crossing different paradigm joints. Uses uniform vanishing (∃ m₀ ∀ D), which is the textbook-standard form.
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C], PACLearnable X C ↔ ∀ ε > 0, ∃ m₀, ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < εConceptClassFLT.ConceptMeasurableConceptClassPACLearnableRademacherComplexityShattersVCDimWellBehavedVCUses
Used by
- Declvcdim_finite_imp_rademacher_vanishingDeclaration kindtheorem
VCDim finite → Rademacher vanishes uniformly. The bound m₀ depends only on d and ε, NOT on D.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool), VCDim X C < ⊤ → ∀ ε > 0, ∃ m₀, ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < εUses
Used by
- Declvcdim_zero_rademacher_le_inv_sqrtDeclaration kindtheorem
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X), VCDim X C = ↑0 → ∀ (m : ℕ), 0 < m → ∀ [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun x => D)], RademacherComplexity X C D m ≤ 1 / √↑m - Declvcdim_zero_concepts_agreeDeclaration kindtheorem
When VCDim = 0, Rademacher complexity is bounded by 1/√m.
VCDim = 0 means no singleton is shattered, so the concept class acts as a single effective labeling. EmpRad ≤ 1/√m by Khintchine's inequality / Jensen. This avoids the d > 0 hypothesis of
vcdim_bounds_rademacher_quantitative.∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C = ↑0 → ∀ (h₁ h₂ : Concept X Bool), h₁ ∈ C → h₂ ∈ C → ∀ (x : X), h₁ x = h₂ x
- Declvcdim_bounds_rademacher_quantitativeDeclaration kindtheorem
VC dimension upper bounds Rademacher complexity: Rad ≤ √(2d·log(em/d)/m).
The proof decomposes into: (1) Pointwise: EmpRad(xs) ≤ B for all xs [Massart + Sauer-Shelah] (2) Integral: Rad = ∫ EmpRad ≤ ∫ B = B [probability measure]
Step (2) is proved. Step (1) for B ≥ 1 follows from EmpRad ≤ 1. Step (1) for B < 1 requires Massart finite lemma + Sauer-Shelah growth bound.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ), 0 < m → ∀ (d : ℕ), VCDim X C = ↑d → 0 < d → d ≤ m → ∀ [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun x => D)], RademacherComplexity X C D m ≤ √(2 * ↑d * Real.log (Real.exp 1 * ↑m / ↑d) / ↑m)ConceptClassEmpiricalRademacherComplexityFLT.ConceptRademacherComplexityShattersSignVectorVCDimboolToSignrademacherCorrelationUses
- Declncard_restrictions_le_sum_choose_setDeclaration kindtheorem
For a Set-based concept class C with VCDim X C = d, the number of distinct restrictions of C to any finite set S is bounded by ∑_{i≤d} C(|S|, i).
This bridges from our Set-based VCDim to Mathlib's Finset.vcDim on the restriction to S, using the fact that ↥S is Fintype for any Finset S.
∀ {X : Type u} (C : ConceptClass X Bool) (S : Finset X) (d : ℕ), VCDim X C = ↑d → {f | ∃ c ∈ C, ∀ (x : ↥S), c ↑x = f x}.ncard ≤ ∑ i ∈ Finset.range (d + 1), S.card.choose i - Declfinite_massart_lemmaDeclaration kindtheorem
Massart finite lemma: E_σ[max_{j ≤ N} Z_j] ≤ σ√(2 log N).
∀ {m : ℕ}, 0 < m → ∀ {N : ℕ} (hN : 0 < N) (Z : Fin N → SignVector m → ℝ) (σ_param : ℝ), 0 < σ_param → (∀ (j : Fin N) (t : ℝ), 0 ≤ t → 1 / ↑(Fintype.card (SignVector m)) * ∑ sv, Real.exp (t * Z j sv) ≤ Real.exp (t ^ 2 * σ_param ^ 2 / 2)) → (1 / ↑(Fintype.card (SignVector m)) * ∑ sv, Finset.univ.sup' ⋯ fun j => Z j sv) ≤ σ_param * √(2 * Real.log ↑N) - Declexp_mul_sup'_le_sumDeclaration kindtheorem
Soft-max bound: exp(t · Finset.sup') ≤ Σ exp(t · f_i).
∀ {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (hs : s.Nonempty) (f : ι → ℝ) (t : ℝ), 0 ≤ t → Real.exp (t * s.sup' hs f) ≤ ∑ i ∈ s, Real.exp (t * f i)Used by
- DeclrademacherComplexity_le_oneDeclaration kindtheorem
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool) (D : MeasureTheory.Measure X) (m : ℕ), 0 < m → ∀ [MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi fun x => D)], RademacherComplexity X C D m ≤ 1
- Declanalytical_log_sqrt_boundDeclaration kindtheorem
Analytical lemma: for d > 0, m ≥ ⌈32(d+1)/ε⁴⌉+1, ε ∈ (0,1], we have 2d·log(em/d)/m < ε².
Uses
Real.log_le_rpow_divwith exponent 1/2: log(x) ≤ x^(1/2)/(1/2) = 2√x. Then 2d·log(em/d)/m ≤ 2d·2√(em/d)/(m) ≤ ε².∀ (d m : ℕ) (ε : ℝ), 0 < ε → ε ≤ 1 → 0 < d → d ≤ m → ⌈32 * (↑d + 1) / ε ^ 4⌉₊ + 1 ≤ m → 2 * ↑d * Real.log (Real.exp 1 * ↑m / ↑d) / ↑m < ε ^ 2 - Declvcdim_finite_imp_pac_via_uc'Declaration kindtheorem
VCDim < ⊤ → PACLearnable via UC route.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool), VCDim X C < ⊤ → (∀ h ∈ C, Measurable h) → (∀ (c : Concept X Bool), Measurable c) → WellBehavedVC X C → PACLearnable X CUsed by
- Declvcdim_finite_imp_uc'Declaration kindtheorem
Finite VCDim implies uniform convergence. Proof: VCDim < ∞ → UC.
- Finite X: direct Hoeffding per-hypothesis + finite union bound.
- Infinite X: Sauer-Shelah → symmetrization + growth function → UC.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool), VCDim X C < ⊤ → (∀ h ∈ C, Measurable h) → (∀ (c : Concept X Bool), Measurable c) → WellBehavedVC X C → HasUniformConvergence X CConceptClassEmpiricalErrorFLT.ConceptGrowthFunctionHasUniformConvergenceHypothesisSpaceTrueErrorRealVCDimWellBehavedVCzeroOneLossUses
- Declvcdim_finite_imp_growth_boundedDeclaration kindtheorem
VCDim < ⊤ → growth function polynomially bounded by partial binomial sum. Forward direction of fundamental_theorem conjunct 5. Uses Sauer-Shelah: GrowthFunction(m) ≤ ∑_{i≤d} C(m,i) where d = VCDim.
∀ (X : Type u) (C : ConceptClass X Bool), VCDim X C < ⊤ → ∃ d, ∀ (m : ℕ), d ≤ m → GrowthFunction X C m ≤ ∑ i ∈ Finset.range (d + 1), m.choose i
- Decluc_bad_event_le_delta_provedDeclaration kindtheorem
UC bad-event bound: for m ≥ m₀(v,ε,δ), the probability of the bad event (∃ h with |TrueErr-EmpErr| ≥ ε) is at most δ. Composes
symmetrization_uc_boundwithgrowth_exp_le_delta.∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε δ : ℝ), 0 < ε → 0 < δ → δ < 1 → ∀ (v : ℕ), 0 < v → (∀ (n : ℕ), v ≤ n → GrowthFunction X C n ≤ ∑ i ∈ Finset.range (v + 1), n.choose i) → (16 * Real.exp 1 * (↑v + 1) / ε ^ 2) ^ (v + 1) / δ ≤ ↑m → MeasureTheory.NullMeasurableSet {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) → (MeasureTheory.Measure.pi fun x => D) {xs | ∃ h ∈ C, |TrueErrorReal X h c D - EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool)| ≥ ε} ≤ ENNReal.ofReal δUsed by
- Declsymmetrization_uc_boundDeclaration kindtheorem
The symmetrization uniform convergence bound: two-sided version. P[∃h∈C: |TrueErr-EmpErr| ≥ ε] ≤ 4·GF(C,2m)·exp(-mε²/8).
Proof strategy (4 steps):
1. Decompose absolute value: |TrueErr - EmpErr| ≥ ε ↔ (TrueErr - EmpErr ≥ ε) ∨ (EmpErr - TrueErr ≥ ε)
have abs_decomp : ∀ (a b : ℝ), |a - b| ≥ ε ↔ a - b ≥ ε ∨ b - a ≥ ε := by intro a b; constructor · intro h; by_cases h' : a - b ≥ ε · exact Or.inl h' · exact Or.inr (by linarith [abs_sub_comm a b, le_abs_self (a - b)]) · intro h; cases h with | inl h => exact le_trans (le_of_eq (abs_of_nonneg (by linarith))) (by linarith) | inr h => exact le_trans (le_of_eq (abs_of_nonpos (by linarith) ▸ ...)) ...2. Upper tail: P[∃h∈C: TrueErr-EmpErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)
- Direct application of
symmetrization_step+double_sample_pattern_bound.
3. Lower tail: P[∃h∈C: EmpErr-TrueErr ≥ ε] ≤ 2·GF(C,2m)·exp(-mε²/8)
- Apply the symmetric argument: swap roles of S and S' in the double sample.
- Equivalently, apply
symmetrization_stepto the event EmpErr-TrueErr ≥ ε and bound the double-sample event {EmpErr_S - EmpErr_{S'} ≥ ε/2}. - The bound is symmetric because D^m ⊗ D^m is symmetric under swapping factors.
have swap_symmetry : DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S) - EmpErr(S') ≥ ε/2} = DoubleSampleMeasure D m {p | ∃ h ∈ C, EmpErr(S') - EmpErr(S) ≥ ε/2} := Measure.prod_swap ...
4. Union bound: P[|gap| ≥ ε] ≤ P[gap ≥ ε] + P[gap ≤ -ε] ≤ 2·GF·exp(...) + 2·GF·exp(...) = 4·GF(C,2m)·exp(-mε²/8)
-- Uses: MeasureTheory.measure_union_le for the union of two events -- CAST: 2 * X + 2 * X = 4 * X in ENNReal (need ENNReal.add_mul or similar)References: SSBD Theorem 6.7, Kakade-Tewari Lecture 19
∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε : ℝ), 0 < ε → 2 * Real.log 2 ≤ ↑m * ε ^ 2 → MeasureTheory.NullMeasurableSet {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) → (MeasureTheory.Measure.pi fun x => D) {xs | ∃ h ∈ C, |TrueErrorReal X h c D - EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool)| ≥ ε} ≤ ENNReal.ofReal (4 * ↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8))) - Direct application of
- Declsymmetrization_step_lowerDeclaration kindtheorem
Symmetrization step for the lower tail: P[∃h: EmpErr-TrueErr ≥ ε] ≤ 2·P_{double}[∃h: EmpErr_S-EmpErr_{S'} ≥ ε/2].
Mirror of
symmetrization_stepfor the opposite direction. Useshoeffding_one_sided_upperinstead ofhoeffding_one_sided.∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε : ℝ), 0 < ε → 2 * Real.log 2 ≤ ↑m * ε ^ 2 → (MeasureTheory.Measure.pi fun x => D) {xs | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) - TrueErrorReal X h c D ≥ ε} ≤ 2 * ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) ≥ ε / 2}Used by
- Declsymmetrization_stepDeclaration kindtheorem
Symmetrization: the probability of a large gap TrueErr-EmpErr is at most twice the probability of a large gap EmpErr'-EmpErr on the double sample.
Proof strategy (6 steps):
1. Witness selection: For S in the bad event, ∃h* ∈ C with TrueErr(h) - EmpErr_S(h) ≥ ε.
-- In the bad event set, extract h* by classical choice have h_witness : ∀ xs ∈ bad_event, ∃ h* ∈ C, TrueErrorReal X h* c D - EmpiricalError X Bool h* (sample xs) (zeroOneLoss Bool) ≥ ε2. Ghost sample mean: E_{S'}[EmpErr_{S'}(h)] = TrueErr(h) ≥ EmpErr_S(h*) + ε.
- Uses:
MeasureTheory.integral_pito compute E[EmpErr] over product measure. - KEY LEMMA: For fixed h, E_{D^m}[EmpiricalError(h,S)] = TrueErrorReal(h,c,D). This is because EmpErr = (1/m)∑ indicator(x_i), and E[indicator(x_i)] = TrueErrorReal.
have expected_emp_err : ∀ h* : Concept X Bool, ∫ xs, EmpiricalError X Bool h* (sample xs) (zeroOneLoss Bool) ∂(Measure.pi (fun _ : Fin m => D)) = TrueErrorReal X h* c D := by ...
3. Hoeffding on ghost sample: P_{S'}[EmpErr_{S'}(h) < TrueErr(h) - ε/2] ≤ exp(-mε²/2).
- Apply
hoeffding_one_sidedwith t = ε/2. - The
hm_largehypothesis ensures exp(-mε²/2) < 1/2: 2·ln2 ≤ mε² ⟹ mε²/2 ≥ ln2 ⟹ exp(-mε²/2) ≤ 1/2.have hoeffding_ghost : ∀ h* ∈ C, Measure.pi (fun _ : Fin m => D) {xs' | EmpiricalError X Bool h* (sample xs') (zeroOneLoss Bool) < TrueErrorReal X h* c D - ε/2} ≤ ENNReal.ofReal (Real.exp (-m * (ε/2)^2 * 2)) := by intro h* _; exact hoeffding_one_sided D h* c m hm (ε/2) (by linarith) (by ...) (by ...)
4. Complementary probability: P_{S'}[EmpErr_{S'}(h) - EmpErr_S(h) ≥ ε/2] ≥ 1/2.
- From step 2: TrueErr(h) ≥ EmpErr_S(h) + ε
- From step 3: P[EmpErr_{S'} ≥ TrueErr - ε/2] ≥ 1/2
- Chain: EmpErr_{S'} ≥ TrueErr - ε/2 ≥ EmpErr_S + ε - ε/2 = EmpErr_S + ε/2
5. Conditional to unconditional: The witness h* from step 1 also witnesses the double-sample event ∃h∈C: EmpErr'-EmpErr ≥ ε/2. So: P_{S'}[double event | S bad] ≥ 1/2.
have conditional_bound : ∀ xs ∈ bad_event, Measure.pi (fun _ : Fin m => D) {xs' | ∃ h ∈ C, EmpiricalError ... xs' - EmpiricalError ... xs ≥ ε/2} ≥ ENNReal.ofReal (1/2) := by ...6. Fubini integration: By Measure.prod_apply and Fubini: P_{S,S'}[double event] = ∫_S P_{S'}[double event | S] ≥ (1/2) · P_S[bad event] ⟹ P_S[bad event] ≤ 2 · P_{S,S'}[double event].
-- Uses: MeasureTheory.Measure.prod_apply or lintegral_prod -- MEASURABILITY: the double-sample event is measurable as a finite union -- of sets of the form {(xs,xs') | EmpErr'(h) - EmpErr(h) ≥ ε/2} for h ∈ C. -- Since C may be infinite, measurability requires care: the sup over h -- must be shown to be measurable. For finite restriction patterns (≤ 2^m -- on Fin m → Bool), this is a finite union.MEASURABILITY CONCERNS:
{xs | ∃ h ∈ C, ...}is NOT obviously measurable for infinite C. Strategy: decompose via restriction patterns. On any fixed xs, the set of labelings {(h(xs 0), ..., h(xs(m-1))) | h ∈ C} has at most GF(C,m) ≤ 2^m elements. So the ∃h event is a finite union of measurable sets.EmpiricalErroris a finite sum of measurable functions, hence measurable.- The product σ-algebra on (Fin m → X) × (Fin m → X) is generated by cylinder sets, and our events are in this σ-algebra.
References: SSBD Lemma 4.5, Kakade-Tewari Lecture 19 Lemma 1
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε : ℝ), 0 < ε → 2 * Real.log 2 ≤ ↑m * ε ^ 2 → (MeasureTheory.Measure.pi fun x => D) {xs | ∃ h ∈ C, TrueErrorReal X h c D - EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≥ ε} ≤ 2 * ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2}Used by
- Uses:
- Decldouble_sample_pattern_boundDeclaration kindtheorem
On the double sample, the probability that any hypothesis has EmpErr' - EmpErr ≥ ε/2 is bounded by GF(C,2m) · exp(-mε²/8).
Proof strategy (Approach A — standard exchangeability, 5 steps):
1. EXCHANGEABILITY: Under D^m ⊗ D^m, the 2m draws z₁,...,z_{2m} are iid from D. The joint distribution is invariant under permutations of {1,...,2m}.
Key lemma: P_{D^m⊗D^m}[event(S,S')] = E_z[P_{split}[event | z]] where z = merged sample and the split is uniformly random among all C(2m,m) ways to partition z into two groups of m.
-- Measure.pi permutation invariance have pi_perm_invariant : ∀ (σ : Equiv.Perm (Fin (2*m))), (Measure.pi (fun _ : Fin (2*m) => D)).map (fun z i => z (σ i)) = Measure.pi (fun _ : Fin (2*m) => D) := by ... -- Consequence: the event probability equals the split-averaged probability have exchangeability : DoubleSampleMeasure D m {p | ∃ h ∈ C, gap(p) ≥ ε/2} = ∫ z, SplitMeasure m {vs | ∃ h ∈ C, gap(split z vs) ≥ ε/2} ∂(Measure.pi (fun _ : Fin (2*m) => D)) := by ...2. CONDITIONING: For fixed merged sample z of 2m points:
- C restricts to at most GF(C,2m) distinct labeling patterns on z (deterministic).
- For each pattern p, define: diff(p, split) = EmpErr_{S'}(p) - EmpErr_S(p) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i where a_i = 1[pattern(z_i) ≠ c(z_i)] ∈ {0,1}.
-- Number of distinct patterns have num_patterns : ∀ (z : MergedSample X m), Set.ncard {p : Fin (2*m) → Bool | ∃ h ∈ C, ∀ i, p i = (h (z i) ≠ c (z i))} ≤ GrowthFunction X C (2*m) := by ...3. PER-PATTERN HOEFFDING ON SPLITS: For fixed z and fixed pattern p: Under uniformly random split (S,S') of z into two groups of m: diff(p, split) = (1/m) ∑_{i∈S'} a_i - (1/m) ∑_{i∈S} a_i
This is a function of the random partition. By Hoeffding's inequality for sampling without replacement (Serfling 1974): P_split[diff ≥ ε/2] ≤ exp(-mε²/8)
Alternative derivation: Hoeffding without replacement from Hoeffding with replacement (iid signs) via coupling. The without-replacement bound is actually TIGHTER (variance reduction), but the with-replacement bound suffices.
-- Per-pattern concentration have per_pattern_bound : ∀ (z : MergedSample X m) (a : Fin (2*m) → ℝ) (ha : ∀ i, a i ∈ Set.Icc 0 1), SplitMeasure m {vs | (1/m) * ∑ i ∈ second_group vs, a i - (1/m) * ∑ i ∈ first_group vs, a i ≥ ε/2} ≤ ENNReal.ofReal (Real.exp (-(m : ℝ) * (ε/2)^2 / 2)) := by ... -- Note: m*(ε/2)^2/2 = mε²/84. UNION BOUND: P_split[∃ pattern: diff ≥ ε/2 | z] ≤ (number of patterns) · max_pattern P_split[diff ≥ ε/2] ≤ GF(C,2m) · exp(-mε²/8)
have union_bound : ∀ (z : MergedSample X m), SplitMeasure m {vs | ∃ h ∈ C, gap(split z vs, h) ≥ ε/2} ≤ ENNReal.ofReal (GrowthFunction X C (2*m) * Real.exp (-(m : ℝ) * ε^2 / 8)) := by ...5. INTEGRATE: P_{D^m⊗D^m}[event] = E_z[P_split[event|z]] (by step 1) ≤ E_z[GF(C,2m) · exp(-mε²/8)] (by step 4, pointwise) = GF(C,2m) · exp(-mε²/8) (bound is independent of z)
-- The bound is a constant, so integrating gives the same constant -- (using IsProbabilityMeasure for the 2m-fold product)Infrastructure needed:
Fin.sumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n)(available in Mathlib)mergeSamples/splitMergedSample(defined above)SplitMeasureandValidSplit(defined above)Measure.pipermutation invariance (to be proved or imported)- Hoeffding for sampling without replacement
GrowthFunctionon 2m points +sauer_shelah_exp_boundfrom Rademacher.lean
MEASURABILITY CONCERNS:
- The merged sample z ↦ P_split[event|z] must be measurable as a function of z. Since the event is a finite union over patterns, and each pattern's indicator is a measurable function of z (finite evaluation), this follows.
GrowthFunction X C (2*m)is a natural number (deterministic), no measurability issue.
References: SSBD Theorem 6.7, Hoeffding (1963), Serfling (1974)
∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε : ℝ), 0 < ε → MeasureTheory.NullMeasurableSet {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) → ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ≤ ENNReal.ofReal (↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)))Used by
- Declexchangeability_chain_boundDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] [Infinite X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (C : ConceptClass X Bool) (c : Concept X Bool), (∀ h ∈ C, Measurable h) → Measurable c → ∀ (m : ℕ), 0 < m → ∀ (ε : ℝ), 0 < ε → ε ≤ 2 → Set.Nonempty C → MeasureTheory.NullMeasurableSet {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ((MeasureTheory.Measure.pi fun x => D).prod (MeasureTheory.Measure.pi fun x => D)) → have μ := MeasureTheory.Measure.pi fun x => D; (μ.prod μ) {p | ∃ h ∈ C, EmpiricalError X Bool h (fun i => (p.2 i, c (p.2 i))) (zeroOneLoss Bool) - EmpiricalError X Bool h (fun i => (p.1 i, c (p.1 i))) (zeroOneLoss Bool) ≥ ε / 2} ≤ ENNReal.ofReal (↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)))Used by
- DeclzeroOneLoss.congr_simpDeclaration kindtheorem
∀ (Y : Type v) {inst : DecidableEq Y} [inst_1 : DecidableEq Y] (a a_1 : Y), a = a_1 → ∀ (a_2 a_3 : Y), a_2 = a_3 → zeroOneLoss Y a a_2 = zeroOneLoss Y a_1 a_3Used by
- Declrestriction_pattern_countDeclaration kindtheorem
The number of distinct restriction patterns of C on any n points is at most GF(C,n). For z : Fin n → X, define patterns(z) = {p : Fin n → Bool | ∃ h ∈ C, ∀ i, p i = (h(z i) ≠ c(z i))}. Then patterns(z).ncard ≤ GrowthFunction X C n by definition of GrowthFunction.
∀ {X : Type u} [MeasurableSpace X] [Infinite X] (C : ConceptClass X Bool) (c : Concept X Bool) (n : ℕ) (z : Fin n → X), {p | ∃ h ∈ C, ∀ (i : Fin n), p i = decide (h (z i) ≠ c (z i))}.ncard ≤ GrowthFunction X C nUsed by
- Declrademacher_mgf_boundDeclaration kindtheorem
Rademacher MGF bound.
∀ {m : ℕ}, 0 < m → ∀ (a : Fin m → ℝ) (c : ℝ), 0 ≤ c → (∀ (i : Fin m), |a i| ≤ c) → ∀ (t : ℝ), 0 ≤ t → 1 / ↑(Fintype.card (SignVector m)) * ∑ σ, Real.exp (t * (1 / ↑m * ∑ i, a i * boolToSign (σ i))) ≤ Real.exp (t ^ 2 * c ^ 2 / (2 * ↑m)) - Declcosh_le_exp_sq_halfDeclaration kindtheorem
cosh(x) ≤ exp(x²/2). Standard sub-Gaussian bound.
∀ (x : ℝ), Real.cosh x ≤ Real.exp (x ^ 2 / 2)
Used by
- Declfinite_exchangeability_boundDeclaration kindtheorem
Generic finite exchangeability bound. Given a measure-preserving family of transformations on a probability space, a NullMeasurableSet S, and a pointwise bound on the sum of preimage indicators, conclude ν(S) ≤ B.
∀ {Ω : Type u_1} {G : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : Fintype G] [Nonempty G] {ν : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure ν] (T : G → Ω → Ω) (S : Set Ω), (∀ (g : G), MeasureTheory.MeasurePreserving (T g) ν ν) → MeasureTheory.NullMeasurableSet S ν → ∀ (B : ENNReal), (∀ (z : Ω), ∑ g, (T g ⁻¹' S).indicator 1 z ≤ B * ↑(Fintype.card G)) → ν S ≤ BUsed by
- Declgrowth_exp_le_deltaDeclaration kindtheorem
∀ {X : Type u} [MeasurableSpace X] (C : ConceptClass X Bool) (v : ℕ), 0 < v → ∀ (m : ℕ), 0 < m → ∀ (ε δ : ℝ), 0 < ε → 0 < δ → δ < 1 → (∀ (n : ℕ), v ≤ n → GrowthFunction X C n ≤ ∑ i ∈ Finset.range (v + 1), n.choose i) → (16 * Real.exp 1 * (↑v + 1) / ε ^ 2) ^ (v + 1) / δ ≤ ↑m → 4 * ↑(GrowthFunction X C (2 * m)) * Real.exp (-(↑m * ε ^ 2 / 8)) ≤ δ ∧ 2 * Real.log 2 ≤ ↑m * ε ^ 2 - Declsum_choose_le_exp_powDeclaration kindtheorem
Pure combinatorial inequality: ∑_{i=0}^d C(m,i) ≤ (em/d)^d for d ≤ m, d ≥ 1.
∀ (d m : ℕ), 0 < d → d ≤ m → ∑ i ∈ Finset.range (d + 1), ↑(m.choose i) ≤ (Real.exp 1 * ↑m / ↑d) ^ d
- Declpow_mul_exp_neg_le_factorial_divDeclaration kindtheorem
Key arithmetic lemma for PAC bound: for t > 0, t^d * exp(-t) ≤ (d+1)!/t. Follows from exp(t) ≥ t^(d+1)/(d+1)! (partial sum of Taylor series).
∀ {d : ℕ} {t : ℝ}, 0 < t → t ^ d * Real.exp (-t) ≤ ↑(d + 1).factorial / tUsed by
- Declgrowth_function_le_two_powDeclaration kindtheorem
Trivial bound: GrowthFunction ≤ 2^n for all concept classes. Each restriction to an n-element set yields a function in S → Bool, and there are at most 2^n such functions.
∀ {X : Type u} (C : ConceptClass X Bool) (n : ℕ), GrowthFunction X C n ≤ 2 ^ nUsed by
- Declhoeffding_one_sided_upperDeclaration kindtheorem
Upper-tail Hoeffding: for iid Bernoulli(p) draws, the empirical average overshoots the mean by ≥ t with probability ≤ exp(-2mt²).
This is the mirror of
hoeffding_one_sided(which bounds the lower tail). The proof uses the same sub-Gaussian machinery with Z_i = indicator(x_i) - p (instead of p - indicator(x_i)).∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (h c : Concept X Bool) (m : ℕ), 0 < m → ∀ (t : ℝ), 0 < t → t ≤ 1 → MeasurableSet {x | h x ≠ c x} → (MeasureTheory.Measure.pi fun x => D) {xs | EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≥ TrueErrorReal X h c D + t} ≤ ENNReal.ofReal (Real.exp (-2 * ↑m * t ^ 2)) - Declhoeffding_one_sidedDeclaration kindtheorem
One-sided Hoeffding: for iid Bernoulli(p) draws, the empirical average undershoots the mean by ≥ t with probability ≤ exp(-2mt²).
Proof strategy (3 steps):
1. MGF bound (Hoeffding's lemma): For X ∈ [0,1] with E[X] = p, E[exp(s(X-p))] ≤ exp(s²/8).
- Adapt from
cosh_le_exp_sq_halfinfrastructure in Rademacher.lean. - Key: convexity of exp on [0,1] gives E[exp(sX)] ≤ p·exp(s) + (1-p)·exp(0), then the s²/8 bound follows from ln(1 + x) ≤ x and Taylor expansion.
have mgf_bound : ∀ (s : ℝ), ∫ x, Real.exp (s * (indicator x - p)) ∂D ≤ Real.exp (s^2 / 8) := by ...
2. Product independence: E[exp(s·∑(X_i-p))] = ∏ E[exp(s(X_i-p))] ≤ exp(ms²/8).
- Uses
MeasureTheory.Measure.piindependence structure. - Needs:
Measure.piintegral factorization for product of functions. - MEASURABILITY:
fun xs => Real.exp (s * ∑ i, f (xs i))is measurable (composition of measurable functions).have product_bound : ∀ (s : ℝ), ∫ xs, Real.exp (s * ∑ i, (indicator (xs i) - p)) ∂Measure.pi (fun _ => D) ≤ Real.exp (m * s^2 / 8) := by ...
3. Exponential Markov + optimize: P[∑(X_i-p) ≤ -mt] = P[exp(-s·∑(X_i-p)) ≥ exp(smt)] ≤ exp(-smt + ms²/8). Optimize over s: set s = 4t to get ≤ exp(-2mt²).
- Uses Markov's inequality in ENNReal form.
- CAST ISSUE: Markov gives ENNReal bound, need to convert exp(-2mt²) between ENNReal.ofReal and the measure value.
have markov_step : ∀ (s : ℝ) (hs : 0 < s), Measure.pi (fun _ => D) {xs | ∑ i, (indicator (xs i) - p) ≤ -(m : ℝ) * t} ≤ ENNReal.ofReal (Real.exp (-(s * m * t) + m * s^2 / 8)) := by ... have optimize : Real.exp (-(4*t * m * t) + m * (4*t)^2 / 8) = Real.exp (-2 * m * t^2) := by ring_nf
CAST ISSUES to watch:
m : ℕneeds cast toℝin the exponent:(m : ℝ)EmpiricalErrorreturnsℝ,TrueErrorRealreturnsℝ, good — no ENNReal gap- The measure value is
ENNReal, the boundexp(-2mt²)isℝ≥0∞viaENNReal.ofReal
References: SSBD Lemma B.3, Hoeffding (1963)
∀ {X : Type u} [inst : MeasurableSpace X] (D : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure D] (h c : Concept X Bool) (m : ℕ), 0 < m → ∀ (t : ℝ), 0 < t → t ≤ 1 → MeasurableSet {x | h x ≠ c x} → (MeasureTheory.Measure.pi fun x => D) {xs | EmpiricalError X Bool h (fun i => (xs i, c (xs i))) (zeroOneLoss Bool) ≤ TrueErrorReal X h c D - t} ≤ ENNReal.ofReal (Real.exp (-2 * ↑m * t ^ 2)) - Adapt from
- Decluc_imp_pacDeclaration kindtheorem
Uniform convergence implies PAC learnability via ERM. The ERM learner (which exists by ermLearn) achieves PAC learning when uniform convergence holds. This is the second half of vcdim_finite_imp_pac.
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool), Set.Nonempty C → HasUniformConvergence X C → PACLearnable X C
- DeclBatchLearner.output_in_HDeclaration kindtheorem
Output is in the hypothesis space
∀ {X : Type u} {Y : Type v} (self : BatchLearner X Y) {m : ℕ} (S : Fin m → X × Y), self.learn S ∈ self.hypothesesUsed by
- Declrademacher_lower_bound_on_shatteredDeclaration kindtheorem
Adversarial Rademacher lower bound on shattered sets. For |T| >= 4m^2 + 1, exists D with Rad_m(C,D) >= 1/2.
Proof: D = uniform on T. Product measure = uniform on T^m. On injective samples from T (shattered): EmpRad = 1 (by empRad_eq_one_of_injective_in_shattered). EmpRad ≥ 0 everywhere (by empRad_nonneg). Birthday bound: P[injective m draws from n ≥ 4m²+1 points] ≥ 1 - m(m-1)/(2n) ≥ 7/8 ≥ 1/2. So ∫ EmpRad ≥ P[injective] · 1 + P[¬injective] · 0 ≥ 1/2.
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (T : Finset X), Shatters X C T → ∀ (m : ℕ), 0 < m → 4 * m ^ 2 + 1 ≤ T.card → ∃ D, MeasureTheory.IsProbabilityMeasure D ∧ 1 / 2 ≤ RademacherComplexity X C D mUses
Used by
- DeclempiricalRademacherComplexity_le_oneDeclaration kindtheorem
∀ (X : Type u) (C : ConceptClass X Bool) {m : ℕ}, 0 < m → ∀ (xs : Fin m → X), EmpiricalRademacherComplexity X C xs ≤ 1 - DeclempRad_nonnegDeclaration kindtheorem
∀ {X : Type u} (C : ConceptClass X Bool) {m : ℕ}, m ≠ 0 → ∀ (xs : Fin m → X), 0 ≤ EmpiricalRademacherComplexity X C xs - Declsum_boolToSign_cancelDeclaration kindtheorem
Rademacher cancellation: Σ_σ boolToSign(σ i) * f(σ) = 0 when f doesn't depend on coordinate i. Proof: the bit-flip involution at coordinate i pairs each σ with flipAt i σ, negating boolToSign(σ i) while preserving f.
∀ {m : ℕ} (i : Fin m) (f : SignVector m → ℝ), (∀ (σ σ' : SignVector m), (∀ (k : Fin m), k ≠ i → σ k = σ' k) → f σ = f σ') → ∑ σ, boolToSign (σ i) * f σ = 0 - DeclflipAt_otherDeclaration kindtheorem
∀ {m : ℕ} (i : Fin m) (σ : SignVector m) (k : Fin m), k ≠ i → flipAt✝ i σ k = σ kUsed by
- DeclflipAt_involutiveDeclaration kindtheorem
∀ {m : ℕ} (i : Fin m), Function.Involutive (flipAt✝ i)Used by
- DeclflipAt_boolToSignDeclaration kindtheorem
∀ {m : ℕ} (i : Fin m) (σ : SignVector m), boolToSign (flipAt✝ i σ i) = -boolToSign (σ i)Used by
- DeclempRad_eq_one_of_injective_in_shatteredDeclaration kindtheorem
Key combinatorial lemma: injective samples from a shattered set have EmpRad = 1.
∀ {X : Type u} [DecidableEq X] (C : ConceptClass X Bool) {m : ℕ}, 0 < m → ∀ (T : Finset X), Shatters X C T → ∀ (xs : Fin m → X), Function.Injective xs → (∀ (i : Fin m), xs i ∈ T) → EmpiricalRademacherComplexity X C xs = 1 - Declshatters_subsetDeclaration kindtheorem
Subset of a shattered set is shattered.
∀ {X : Type u} (C : ConceptClass X Bool) (T S : Finset X), S ⊆ T → Shatters X C T → Shatters X C S - DeclempRad_eq_one_of_all_labelingsDeclaration kindtheorem
On samples where every labeling is realizable, EmpRad = 1.
For each sign vector σ, the hypothesis provides h ∈ C with h(xs i) = σ i, giving corr(h,σ,xs) = 1. Since |corr| ≤ 1, the sSup is exactly 1. Averaging over all σ gives EmpRad = (1/2^m)·2^m·1 = 1.
This is the combinatorial core of the NFL Rademacher lower bound: when xs are distinct points from a shattered set, every labeling is realized, so this lemma applies.
∀ {X : Type u} (C : ConceptClass X Bool) {m : ℕ}, 0 < m → ∀ (xs : Fin m → X), (∀ (σ : SignVector m), ∃ h ∈ C, ∀ (i : Fin m), h (xs i) = σ i) → EmpiricalRademacherComplexity X C xs = 1 - DeclrademacherCorrelation_abs_le_oneDeclaration kindtheorem
∀ {X : Type u} {m : ℕ}, 0 < m → ∀ (h : Concept X Bool) (σ : SignVector m) (xs : Fin m → X), |rademacherCorrelation h σ xs| ≤ 1 - DeclboolToSign_mul_abs_le_oneDeclaration kindtheorem
∀ (b₁ b₂ : Bool), |boolToSign b₁ * boolToSign b₂| ≤ 1
- DeclboolToSign_abs_le_oneDeclaration kindtheorem
∀ (b : Bool), |boolToSign b| ≤ 1
Used by
- DeclboolToSign_abs_eq_oneDeclaration kindtheorem
∀ (b : Bool), |boolToSign b| = 1
- Declcorr_eq_one_of_agreeDeclaration kindtheorem
When h agrees with σ on all sample points, correlation is exactly 1.
∀ {X : Type u} {m : ℕ}, 0 < m → ∀ (h : Concept X Bool) (σ : SignVector m) (xs : Fin m → X), (∀ (i : Fin m), h (xs i) = σ i) → rademacherCorrelation h σ xs = 1 - Declpac_imp_vcdim_finiteDeclaration kindtheorem
Direction →: PAC learnability implies finite VCDim.
PROOF ROUTE (via double-sample infrastructure in Generalization.lean): Step 1: Contrapositive — assume VCDim = ∞ Step 2: For m = mf(ε,δ), extract S with |S| = 2m shattered by C (uses WithTop.eq_top_iff_forall_ge, same as vcdim_univ_infinite) Step 3: Construct D = uniform on S (Finset.uniformMeasure?) KU₁₉: Mathlib's uniform measure on a finite set — does
MeasureTheory.Measure.count/Finset.cardgive IsProbabilityMeasure? Step 4: Double-sample trick via GhostSample + symmetrization Step 5: Counting argument on restricted labelingsHC at this joint: Step 3 requires constructing a specific probability measure from a combinatorial object (the shattered set). This is a P₁→P₂ crossing. UK₉: The construction of the hard distribution is the only non-constructive step. Can it be made constructive? (Related to derandomization in learning.)
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool), PACLearnable X C → VCDim X C < ⊤
- Declvcdim_infinite_not_pacDeclaration kindtheorem
If VCDim = ⊤, then C is not PAC learnable. Proof: for any learner L with sample function mf, pick ε = 1/4, δ = 1/4. Let m = mf(1/4, 1/4). Since VCDim = ⊤, ∃ shattered set S with |S| ≥ 2m. Put D = uniform on S. For random labeling, any m-sample learner has expected error ≥ 1/4 on unseen points. This is the core of pac_imp_vcdim_finite (contrapositive direction).
∀ (X : Type u) [inst : MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool), VCDim X C = ⊤ → ¬PACLearnable X C
Used by
- DecluniformMeasure_isProbabilityDeclaration kindtheorem
The uniform measure is a probability measure when X is nonempty and finite.
∀ (X : Type u) [inst : MeasurableSpace X] [inst_1 : Fintype X] [MeasurableSingletonClass X] (hne : Nonempty X), 0 < Fintype.card X → MeasureTheory.IsProbabilityMeasure (uniformMeasure X hne)
- Declnfl_counting_coreDeclaration kindtheorem
NFL counting core: for a shattered set T with |T| > 2m, there exists a labeling f₀ : ↥T → Bool and its shattering witness c₀ ∈ C such that the number of samples xs : Fin m → ↥T where the learner achieves low error (≤ |T|/4) is at most half the total number of samples. Proof: double-counting + pigeonhole using per_sample_labeling_bound.
∀ {X : Type u} {C : ConceptClass X Bool} {T : Finset X}, Shatters X C T → ∀ {m : ℕ}, 2 * m < T.card → ∀ (L : BatchLearner X Bool), ∃ f₀, ∃ c₀ ∈ C, (∀ (t : ↥T), c₀ ↑t = f₀ t) ∧ 2 * {xs | {t | c₀ ↑t ≠ L.learn (fun i => (↑(xs i), c₀ ↑(xs i))) ↑t}.card * 4 ≤ T.card}.card ≤ Fintype.card (Fin m → ↥T) - Declper_sample_labeling_boundDeclaration kindtheorem
Per-sample labeling bound: for any fixed xs : Fin m → α on a Fintype α with 2m < |α|, and any function output : (α → Bool) → (α → Bool) that only depends on the restriction of f to {xs i}, at most half the labelings f : α → Bool have error(f, output(f)) * 4 ≤ |α|.
Proof: pair each f with flip_unseen(f). The pair has complementary disagreements on unseen points, and |unseen| > |α|/2, so at most one can have low error.
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (m : ℕ), 2 * m < Fintype.card α → ∀ (xs : Fin m → α) (output : (α → Bool) → α → Bool), (∀ (f f' : α → Bool), (∀ (i : Fin m), f (xs i) = f' (xs i)) → output f = output f') → 2 * {f | {t | f t ≠ output f t}.card * 4 ≤ Fintype.card α}.card ≤ Fintype.card (α → Bool)Used by
- DeclMeasurableConceptClass.hmeas_CDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C], ∀ c ∈ C, Measurable c - DeclMeasurableConceptClass.mem_measurableDeclaration kindtheorem
Every concept in C is measurable
∀ {X : Type u} {inst : MeasurableSpace X} {C : ConceptClass X Bool} [self : MeasurableConceptClass X C], ∀ h ∈ C, Measurable h - DeclMeasurableConceptClass.hc_measDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C] (c : Concept X Bool), Measurable c - DeclMeasurableConceptClass.all_measurableDeclaration kindtheorem
All concepts X → Bool are measurable (for disagreement sets)
∀ {X : Type u} {inst : MeasurableSpace X} (C : ConceptClass X Bool) [self : MeasurableConceptClass X C] (c : Concept X Bool), Measurable c - DeclMeasurableConceptClass.hWBDeclaration kindtheorem
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C], WellBehavedVC X C - DeclMeasurableConceptClass.wellBehavedDeclaration kindtheorem
Uniform convergence bad event is NullMeasurableSet
∀ {X : Type u} {inst : MeasurableSpace X} {C : ConceptClass X Bool} [self : MeasurableConceptClass X C], WellBehavedVC X CUsed by
- DefinitionBatchLearnerstructure
A batch learner (PAC paradigm): takes a finite sample, returns a hypothesis.
Type u → Type v → Type (max u v)
- DefinitionBatchLearner.hypothesesdef
The learner's hypothesis space
{X : Type u} → {Y : Type v} → BatchLearner X Y → HypothesisSpace X Y - DefinitionBatchLearner.learndef
The learning algorithm: given a sample, produce a hypothesis
{X : Type u} → {Y : Type v} → BatchLearner X Y → {m : ℕ} → (Fin m → X × Y) → Concept X Y - DefinitionCompressionSchemeWithInfostructure
A labeled compression scheme with finite side information. This is the object proved to exist by Moran-Yehudayoff (2016, arXiv:1503.06960).
The current
CompressionSchemeis strictly stronger: it requires reconstruction from the compressed Finset alone (no side information). SeeOpen_NoInfoCompressionStrengtheningfor that conjecture.(X : Type u) → (Y : Type v) → ConceptClass X Y → Type (max (max u (u_1 + 1)) v)
- DefinitionCompressionSchemeWithInfo.Infodef
The side information type
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → Type u_1 - DefinitionCompressionSchemeWithInfo.compressdef
Compression: extract ≤ kernelSize labeled examples + side information
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → (self : CompressionSchemeWithInfo X Y C) → {m : ℕ} → (Fin m → X × Y) → Finset (X × Y) × self.Info - DefinitionCompressionSchemeWithInfo.info_finitedef
Side information is finite
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → (self : CompressionSchemeWithInfo X Y C) → Fintype self.Info - DefinitionCompressionSchemeWithInfo.kernelSizedef
Kernel size bound
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → ℕ - DefinitionCompressionSchemeWithInfo.reconstructdef
Reconstruction: produce hypothesis from compressed subset AND side information
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → (self : CompressionSchemeWithInfo X Y C) → Finset (X × Y) → self.Info → X → Y - DefinitionCompressionSchemeWithInfo.sizedef
Total size of a compression scheme with side information: kernel size + number of side information states. (The paper uses k + log₂(|I|+1); we use the simpler k + |I| which is an upper bound and avoids importing Real.log.)
{X : Type u} → {Y : Type v} → {C : ConceptClass X Y} → CompressionSchemeWithInfo X Y C → ℕ - DefinitionCompressionSchemeWithInfo0def
Fix the hidden
Infouniverse parameter ofCompressionSchemeWithInfoto0. This resolves the universe elaboration obstruction:Fin T → Finset (Fin K)isType 0, whileCompressionSchemeWithInfo X Bool CwithX : Type uinfersInfo : Type u. Pinning to.{u, 0, 0}allowsType 0Info directly.(X : Type u) → (Y : Type) → ConceptClass X Y → Type (max (max u 1) 0)
- DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
Type u → Type v → Type (max v u)
- DefinitionEmpiricalErrordef
Empirical error: average loss on a finite sample.
(X : Type u) → (Y : Type v) → Concept X Y → {m : ℕ} → (Fin m → X × Y) → LossFunction Y → ℝ - DefinitionEmpiricalRademacherComplexitydef
(X : Type u) → ConceptClass X Bool → {m : ℕ} → (Fin m → X) → ℝ - DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
Type u → Type v → Type (max u v)
- DefinitionFinitePMFstructure
A probability mass function over a finite type. Named FinitePMF to avoid conflict with Mathlib's PMF.
(H : Type u_1) → [Fintype H] → Type u_1
- DefinitionFinitePMF.probdef
{H : Type u_1} → [inst : Fintype H] → FinitePMF H → H → ℝ - DefinitionFinitePMF.toPMFdef
{H : Type u_1} → [inst : Fintype H] → FinitePMF H → PMF H - DefinitionFinset.boolVCDimdef
VC dimension of a finite
Bool-valued family, computed via the set-system imageboolFamilyToFinsetFamilyand Mathlib'sFinset.vcDim. Declarednoncomputablebecause the underlyingvcDimis.{H : Type u_1} → [Fintype H] → [DecidableEq H] → Finset (H → Bool) → ℕ - DefinitionGrowthFunctiondef
Growth function (shattering coefficient): π_C(m) = max_{|S|=m} |{c|_S : c ∈ C}|. For each m-element set S, counts the number of distinct restrictions of C to S, then takes the supremum over all such S.
(X : Type u) → ConceptClass X Bool → ℕ → ℕ
- DefinitionHasUniformConvergencedef
Uniform convergence of empirical error to true error over a hypothesis class. This is the property that makes finite VCDim → PAC learnability work. BP₅ connects here: this is ONE of the five characterizations.
M-DefinitionRepair (Γ₃₅ → Γ₄₁): The m₀ must be INDEPENDENT of D and c. That's what "uniform" means — convergence is uniform over all distributions and all target concepts. The original definition had m₀ depending on D and c, making uc_imp_pac unprovable (PACLearnable's mf must be independent of D, c). Repaired: ∃ m₀ is now BEFORE ∀ D, ∀ c. This STRENGTHENS the definition (A5-valid: adds content, doesn't simplify).
(X : Type u) → [MeasurableSpace X] → HypothesisSpace X Bool → Prop
- DefinitionHypothesisSpacedef
A hypothesis space is a set of candidate concepts that the learner searches over. When H = C (the realizable case), every concept in the target class is available. When H ⊂ C or H ⊃ C, we are in the improper/agnostic regime.
Structurally identical to ConceptClass but semantically distinct: ConceptClass is the ground truth collection; HypothesisSpace is what the learner has access to.
Type u → Type v → Type (max v u)
- DefinitionIncidenceInfodef
Concrete side information for the MY construction: each of the
Trecovered blocks is represented by the set of kernel positions it uses.ℕ → ℕ → Type
- DefinitionIsConsistentWithdef
A hypothesis h is consistent with labeled sample S.
(X : Type u) → (Y : Type v) → [DecidableEq Y] → Concept X Y → {m : ℕ} → (Fin m → X × Y) → Prop - DefinitionMWUConfigstructure
MWU config: weight vector with positivity proof.
(C : Type u_1) → [Fintype C] → Type u_1
- DefinitionMWUConfig.potentialdef
Potential = sum of weights.
{C : Type u_1} → [inst : Fintype C] → MWUConfig C → ℝ - DefinitionMWUConfig.toPMFdef
Normalize config to PMF.
{C : Type u_1} → [inst : Fintype C] → [Nonempty C] → MWUConfig C → FinitePMF C - DefinitionMWUConfig.weightsdef
{C : Type u_1} → [inst : Fintype C] → MWUConfig C → C → ℝ - DefinitionMeasurableConceptClassstructure
A concept class with the measure-theoretic regularity needed for PAC theory.
Bundles three conditions: 1. Every concept in C is measurable 2. All concepts are measurable (needed for disagreement set measurability) 3. The UC bad event satisfies NullMeasurableSet (WellBehavedVC)
Condition 3 is the deep one: for uncountable C, the existential {∃ h ∈ C, |TrueErr - EmpErr| ≥ ε} is NOT MeasurableSet in general. WellBehavedVC asserts it is NullMeasurableSet, which suffices for integration (lintegral_indicator_one₀).
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionPACLearnabledef
PAC (Probably Approximately Correct) learning. The central definition of computational learning theory.
Sample space: Fin m → X with i.i.d. product measure D^m. Labels: derived deterministically from target concept c (realizable case). Error: D-probability of disagreement between learner output and c.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionProperFiniteSupportLearnerstructure
A proper finite-support learner for a concept class C. This structure captures the existence of a bounded-support ERM with error at most 1/3 for any C-realizable finite distribution. CORRECTED: good_on_support returns Finset X (not Fin k → X).
(X : Type u) → ConceptClass X Bool → Type u
- DefinitionProperFiniteSupportLearner.learndef
{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → {m : ℕ} → (Fin m → X × Bool) → X → Bool - DefinitionProperFiniteSupportLearner.sampleBounddef
{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → ℕ - DefinitionRademacherComplexitydef
(X : Type u) → [inst : MeasurableSpace X] → ConceptClass X Bool → MeasureTheory.Measure X → ℕ → ℝ
- DefinitionSampleComplexitydef
Sample complexity of PAC learning: the minimum number of samples needed to achieve (ε,δ)-PAC learning. m_C(ε,δ) = sInf{m | ∃ L, ∀ D prob, ∀ c ∈ C, D^m{S : error(L(S)) ≤ ε} ≥ 1-δ}.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → ℝ → ℝ → ℕ
A set S ⊆ X is shattered by concept class C if every labeling of S is realized by some concept in C.
(X : Type u) → ConceptClass X Bool → Finset X → Prop
- DefinitionSignVectordef
ℕ → Type
- DefinitionTrueErrordef
True error (0-1 loss, realizable case): D-probability of disagreement. This is what PACLearnable's success event measures.
(X : Type u) → [inst : MeasurableSpace X] → Concept X Bool → Concept X Bool → MeasureTheory.Measure X → ENNReal
- DefinitionTrueErrorRealdef
True error in ℝ: for use in bounds involving subtraction/absolute value. COUNTER-1 of TrueError. The toReal bridge loses information when the measure is ⊤.
(X : Type u) → [inst : MeasurableSpace X] → Concept X Bool → Concept X Bool → MeasureTheory.Measure X → ℝ
- DefinitionVCDimdef
VC dimension of a concept class: the size of the largest shattered set. Returns ℕ∞ = WithTop ℕ.
(X : Type u) → ConceptClass X Bool → WithTop ℕ
- DefinitionWellBehavedVCdef
A concept class is well-behaved if the ghost gap event is null-measurable. This is the minimal regularity assumption for the symmetrization proof.
(X : Type u) → [MeasurableSpace X] → ConceptClass X Bool → Prop
- DefinitionagreeTestdef
Per-point agreement test: for a fixed point x ∈ Y and concept c, maps hypothesis h to whether h(x) = c(x).
{X : Type u} → (X → Bool) → X → (HY : Finset (X → Bool)) → ↥HY → Bool - DefinitionagreeTestsdef
The family of agreement tests over all points in Y.
{X : Type u} → (X → Bool) → Finset X → (HY : Finset (X → Bool)) → Finset (↥HY → Bool) - DefinitionboolFamilyToFinsetFamilydef
Maps a finite family of
Bool-valued functions to its image as a family of accepting sets. The set-system view is what Mathlib'sFinset.ShattersandFinset.vcDimconsume, so this is the entry point from the function-class view to the combinatorial VC machinery.{H : Type u_1} → [Fintype H] → [DecidableEq H] → Finset (H → Bool) → Finset (Finset H) - DefinitionboolGamePayoffdef
Expected payoff of distribution p against column c in a Boolean game.
{R : Type u_1} → {C : Type u_2} → [inst : Fintype R] → (R → C → Bool) → FinitePMF R → C → ℝ - DefinitionboolTestExpectationdef
Expected value of a
Bool-valued test under a finite distribution, via the indicator embeddingif f h then 1 else 0. The central quantity of the finite-VC approximation layer: a TV bound on distributions translates to a uniform bound on test expectations viaexpectation_approx_of_tv.{H : Type u_1} → [inst : Fintype H] → FinitePMF H → (H → Bool) → ℝ - DefinitionboolToSigndef
Convert Bool labels to ±1 reals. true ↦ 1, false ↦ -1.
Bool → ℝ
- DefinitionboundedSubsamplesdef
Bounded subsamples: all subsets of Y with cardinality ≤ s.
{X : Type u} → Finset X → ℕ → Finset (Finset X) - DefinitiondecodeWitnessLabeldef
Decode labels from the kernel. This is exactly the current MY reconstruction convention in your file.
{X : Type u} → [DecidableEq X] → Finset (X × Bool) → X → Bool - DefinitiondecodeWitnessXCoordsdef
Decode the X-coordinates of a block from kernel positions. This matches the current
blockHypshape.{X : Type u} → Finset (X × Bool) → {K : ℕ} → Finset (Fin K) → Finset X - DefinitiondisagreementFamilydef
The disagreement family: for each h ∈ C, the test y ↦ decide(h(y) ≠ c(y)) restricted to Y. Used for the VC approximation step in the proper learner proof.
{X : Type u} → ConceptClass X Bool → (X → Bool) → (Y : Finset X) → Finset (↥Y → Bool) - DefinitionempiricalPMFdef
Build FinitePMF from empirical frequencies of a finite sequence.
{α : Type u_1} → [inst : Fintype α] → [DecidableEq α] → {T : ℕ} → 0 < T → (Fin T → α) → FinitePMF α - DefinitionencodeWitnessInfodef
Encode a witness set
Was the set of kernel positions of the pairs(x, c x). The boundkernel.card ≤ Kis fed into the encoding through theifbranch, so the result has the same shape as the currentcompressCorecode.{X : Type u} → [DecidableEq X] → Finset (X × Bool) → (X → Bool) → (K : ℕ) → Finset X → Finset (Fin K) - DefinitionextendBooldef
{H : Type u_1} → (H → Bool) → H ⊕ ℕ → Bool - DefinitionflipAtdef
Bit-flip at coordinate i: σ ↦ σ' where σ'(i) = !σ(i), σ'(k) = σ(k) for k ≠ i.
{m : ℕ} → Fin m → SignVector m → SignVector m - DefinitionhypothesisEnvelopedef
The hypothesis envelope: the finite set of all possible learner outputs on bounded subsamples of Y, labeled by concept c.
{X : Type u} → {C : ConceptClass X Bool} → ProperFiniteSupportLearner X C → (X → Bool) → Finset X → Finset (X → Bool) - DefinitionlabeledSampleOfFinsetdef
Build a labeled sample from a Finset of points and a concept.
{X : Type u} → (X → Bool) → (Z : Finset X) → Fin Z.card → X × Bool - DefinitionliftClassdef
{H : Type u_1} → Finset (H → Bool) → ConceptClass (H ⊕ ℕ) Bool - DefinitionmkIncidenceSchemeOfMajoritydef
The actual final closure helper. Packages the majority-vote construction. If decoded hypotheses agree with reference hypotheses on sample points, and majority of reference hypotheses agree with each label, then majority-vote reconstruction is correct.
{X : Type u} → {C : ConceptClass X Bool} → (T K : ℕ) → (compressCore : {m : ℕ} → (Fin m → X × Bool) → Finset (X × Bool) × IncidenceInfo T K) → (blockHyp : Finset (X × Bool) → IncidenceInfo T K → Fin T → X → Bool) → (rowHyp : {m : ℕ} → (S : Fin m → X × Bool) → (∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) → Fin T → X → Bool) → 0 < T → (∀ {m : ℕ} (S : Fin m → X × Bool), (compressCore S).1.card ≤ K) → (∀ {m : ℕ} (S : Fin m → X × Bool), ↑(compressCore S).1 ⊆ Set.range S) → (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m) (t : Fin T), blockHyp (compressCore S).1 (compressCore S).2 t (S i).1 = rowHyp S hreal t (S i).1) → (∀ {m : ℕ} (S : Fin m → X × Bool) (hreal : ∃ c ∈ C, ∀ (i : Fin m), c (S i).1 = (S i).2) (i : Fin m), (∑ t, if rowHyp S hreal t (S i).1 = (S i).2 then 1 else 0) / ↑T > 1 / 2) → CompressionSchemeWithInfo0 X Bool C - DefinitionmwuConfigdef
The MWU config after T steps.
{R : Type u_1} → {C : Type u_2} → [Fintype R] → [inst : Fintype C] → [Nonempty C] → (M : R → C → Bool) → (η : ℝ) → η < 1 → (v : ℝ) → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → ℕ → MWUConfig C - DefinitionmwuHitCountdef
Count how many rounds hit a fixed column, aligned to the recursion of
mwuRun.{R : Type u_1} → {C : Type u_2} → [Fintype R] → [inst : Fintype C] → [Nonempty C] → (M : R → C → Bool) → (η : ℝ) → η < 1 → (v : ℝ) → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → ℕ → C → ℕ - DefinitionmwuInitdef
Initial config: all weights = 1.
(C : Type u_1) → [inst : Fintype C] → MWUConfig C
- DefinitionmwuRowsdef
The MWU row sequence after T steps.
{R : Type u_1} → {C : Type u_2} → [Fintype R] → [inst : Fintype C] → [Nonempty C] → (M : R → C → Bool) → (η : ℝ) → η < 1 → (v : ℝ) → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → (T : ℕ) → Fin T → R - DefinitionmwuRundef
MWU run: iterate T steps, returning final config and row sequence.
{R : Type u_1} → {C : Type u_2} → [Fintype R] → [inst : Fintype C] → [Nonempty C] → (M : R → C → Bool) → (η : ℝ) → η < 1 → (v : ℝ) → (∀ (q : FinitePMF C), ∃ r, v ≤ ∑ c, q.prob c * if M r c = true then 1 else 0) → (T : ℕ) → MWUConfig C × (Fin T → R) - DefinitionmwuUpdateWeightsdef
One MWU update step on weights.
{C : Type u_1} → [inst : Fintype C] → {R : Type u_2} → (R → C → Bool) → (η : ℝ) → η < 1 → MWUConfig C → R → MWUConfig C - DefinitionpointSupportdef
Extract the domain points from a labeled sample.
{X : Type u} → {m : ℕ} → (Fin m → X × Bool) → Finset X - DefinitionrademacherCorrelationdef
{X : Type u} → {m : ℕ} → Concept X Bool → SignVector m → (Fin m → X) → ℝ - DefinitionsupportErrordef
Weighted error of hypothesis h vs concept c over a FinitePMF on Y.
{X : Type u} → (Y : Finset X) → FinitePMF ↥Y → (X → Bool) → (X → Bool) → ℝ - DefinitionuniformMeasuredef
Uniform probability measure on a Fintype: (1/|X|) · count. This gives each point probability 1/|X|. Requires |X| > 0 (nonempty).
(X : Type u) → [inst : MeasurableSpace X] → [Fintype X] → Nonempty X → MeasureTheory.Measure X
- DefinitionuniformPMFdef
Uniform PMF over a nonempty Fintype.
(C : Type u_1) → [inst : Fintype C] → [Nonempty C] → FinitePMF C
- DefinitionzeroOneLossdef
The 0-1 loss for classification.
(Y : Type v) → [DecidableEq Y] → LossFunction Y
Verification
- Replay
- accepted
- Axioms
- Classical.choiceQuot.soundpropext
- Statement identity
- not-applicable
- Substrate
- Lean 4 kernel v4.31.0
- Dictionary pin
- design-lab@5802df4 · initial
- Frozen export
- 1595fb15a896
- Verified
- 2026-09-24T00:00:00Z