Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

Online learning is strictly stronger than PAC learning.

Declonline_strictly_stronger_pac

(∀ (X : Type) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableConceptClass X C],
    OnlineLearnable X Bool C → PACLearnable X C) ∧
  ∃ X x C, PACLearnable X C ∧ ¬OnlineLearnable X Bool C

TopicOnline learning

ThesisStepDefinition

Declonline_strictly_stronger_pacDeclaration kindtheorem

(∀ (X : Type) [inst : MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableConceptClass X C],
    OnlineLearnable X Bool C → PACLearnable X C) ∧
  ∃ X x C, PACLearnable X C ∧ ¬OnlineLearnable X Bool C

ConceptClass MeasurableConceptClass OnlineLearnable PACLearnable

Uses

online_imp_pac
pac_not_implies_online

Declpac_not_implies_onlineDeclaration kindtheorem
```
∃ X x C, PACLearnable X C ∧ ¬OnlineLearnable X Bool C
```
ConceptClass EmpiricalError FLT.Concept LittlestoneDim OnlineLearnable PACLearnable WellBehavedVC thresholdClass zeroOneLoss
Uses
Used by
- online_strictly_stronger_pac
Declvcdim_threshold_finiteDeclaration kindtheorem
VCDim of threshold class on ℕ is finite (≤ 1).
```
VCDim ℕ thresholdClass✝ < ⊤
```
Shatters VCDim thresholdClass
Uses
- threshold_not_shatter_pair
Used by
- pac_not_implies_online
Declthreshold_not_shatter_pairDeclaration kindtheorem
No 2-element subset of ℕ is shattered by the threshold class. Key: the labeling (smaller → false, larger → true) is impossible by monotonicity.
```
∀ {S : Finset ℕ}, 2 ≤ S.card → ¬Shatters ℕ thresholdClass✝ S
```
ConceptClass FLT.Concept Shatters thresholdClass
Used by
- vcdim_threshold_finite
Declldim_threshold_topDeclaration kindtheorem
LittlestoneDim of threshold class = ⊤.
```
LittlestoneDim ℕ thresholdClass✝ = ⊤
```
FLT.Concept LTree LTree.isShattered LittlestoneDim thresholdClass
Uses
- threshold_shattered_all_depths
Used by
- pac_not_implies_online
Declthreshold_shattered_all_depthsDeclaration kindtheorem
```
∀ (d : ℕ), ∃ T, LTree.isShattered thresholdClass✝ T
```
FLT.Concept LTree LTree.isShattered thresholdClass thresholdTree
Uses
- thresholdTree_shattered
Used by
- ldim_threshold_top
DeclthresholdTree_shatteredDeclaration kindtheorem
The threshold tree is shattered by any concept class containing all thresholds with indices in [lo, lo + 2^d - 1].
```
∀ (lo d : ℕ) (C : ConceptClass ℕ Bool),
  (∀ (n : ℕ), lo ≤ n → n < lo + 2 ^ d → (fun x => decide (x ≤ n)) ∈ C) → LTree.isShattered C (thresholdTree✝ lo d)
```
ConceptClass FLT.Concept LTree LTree.isShattered thresholdTree
Used by
- threshold_shattered_all_depths
Declforward_directionDeclaration kindtheorem
Forward direction: OnlineLearnable → LittlestoneDim < ⊤
```
∀ (X : Type) (C : ConceptClass X Bool), OnlineLearnable X Bool C → LittlestoneDim X C < ⊤
```
ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim MistakeBounded OnlineLearnable OnlineLearner OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakesFrom
Uses
Used by
- pac_not_implies_online
DeclmistakesFrom_init_eqDeclaration kindtheorem
Relate mistakesFrom to the original mistakes function.
```
∀ {X : Type} (L : OnlineLearner X Bool) (c : X → Bool) (seq : List X), L.mistakesFrom L.init c seq = L.mistakes c seq
```
OnlineLearner OnlineLearner.State OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakes.go OnlineLearner.mistakesFrom OnlineLearner.predict OnlineLearner.update
Used by
- forward_direction
Decladversary_coreDeclaration kindtheorem
Core adversary lemma.
```
∀ {X : Type} (L : OnlineLearner X Bool) (s : L.State) {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n),
  LTree.isShattered C T → Set.Nonempty C → ∃ seq, ∃ c ∈ C, L.mistakesFrom s c seq = n
```
ConceptClass FLT.Concept LTree LTree.isShattered OnlineLearner OnlineLearner.State OnlineLearner.mistakesFrom OnlineLearner.predict OnlineLearner.update
Used by
- forward_direction
DeclLTree.nonempty_of_isShatteredDeclaration kindtheorem
Helper: shattering implies the concept class is nonempty.
```
∀ {X : Type} {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n), LTree.isShattered C T → Set.Nonempty C
```
ConceptClass FLT.Concept LTree LTree.isShattered
Used by
- forward_direction
Declonline_imp_pacDeclaration kindtheorem
Online learnable → PAC learnable. Γ₄₈: requires LittlestoneDim → VCDim bridge or online-to-batch conversion.
```
∀ (X : Type u) [inst : MeasurableSpace X] (C : ConceptClass X Bool),
  OnlineLearnable X Bool C → ∀ [MeasurableConceptClass X C], PACLearnable X C
```
ConceptClass FLT.Concept MeasurableConceptClass MistakeBounded OnlineLearnable PACLearnable VCDim WellBehavedVC
Uses
Used by
- online_strictly_stronger_pac
Declvcdim_le_of_mistake_boundedDeclaration kindtheorem
Mistake-bounded learner → VCDim ≤ M (universe-polymorphic).
```
∀ {X : Type u} {C : ConceptClass X Bool} {M : ℕ}, MistakeBounded X Bool C M → VCDim X C ≤ ↑M
```
ConceptClass FLT.Concept MistakeBounded OnlineLearner OnlineLearner.init OnlineLearner.mistakes Shatters VCDim mistakesFromU
Uses
- adversary_from_shatters
- mistakesFromU_init_eq
Used by
- online_imp_pac
DeclmistakesFromU_init_eqDeclaration kindtheorem
Relate mistakesFromU to the original mistakes function.
```
∀ {X : Type u} (L : OnlineLearner X Bool) (c : X → Bool) (seq : List X),
  mistakesFromU✝ L L.init c seq = L.mistakes c seq
```
OnlineLearner OnlineLearner.State OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakes.go OnlineLearner.predict OnlineLearner.update mistakesFromU
Used by
- vcdim_le_of_mistake_bounded
Decladversary_from_shattersDeclaration kindtheorem
Adversary argument directly from shattering (universe-polymorphic). Given a shattered set S and any online learner L starting from state s, there exists a sequence and target concept where L makes |S| mistakes.
```
∀ {X : Type u} (L : OnlineLearner X Bool) (s : L.State) {C : ConceptClass X Bool} {S : Finset X},
  Shatters X C S → ∃ seq, ∃ c ∈ C, mistakesFromU✝ L s c seq = S.card
```
ConceptClass FLT.Concept OnlineLearner OnlineLearner.State OnlineLearner.predict OnlineLearner.update Shatters mistakesFromU
Uses
- shatters_restrict
Used by
- vcdim_le_of_mistake_bounded
Declshatters_restrictDeclaration kindtheorem
Restricted shattering: if C shatters S and we restrict to {c ∈ C | c x = b}, then S \ {x} is shattered by the restricted class (when x ∈ S).
```
∀ {X : Type u} {C : ConceptClass X Bool} {S : Finset X},
  Shatters X C S → ∀ {x : X}, x ∈ S → ∀ (b : Bool), Shatters X {c | c ∈ C ∧ c x = b} (S.erase x)
```
ConceptClass FLT.Concept Shatters
Used by
- adversary_from_shatters
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 C
```
BatchLearner BatchLearner.learn ConceptClass FLT.Concept PACLearnable VCDim WellBehavedVC
Uses
- uc_imp_pac
- vcdim_finite_imp_uc'
Used by
- online_imp_pac
- pac_not_implies_online
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 C
```
ConceptClass EmpiricalError FLT.Concept GrowthFunction HasUniformConvergence HypothesisSpace TrueErrorReal VCDim WellBehavedVC zeroOneLoss
Uses
Used by
- vcdim_finite_imp_pac_via_uc'
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
```
ConceptClass FLT.Concept GrowthFunction Shatters VCDim
Used by
- vcdim_finite_imp_uc'

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_bound with growth_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 δ

ConceptClass EmpiricalError FLT.Concept GrowthFunction TrueErrorReal zeroOneLoss

Uses

growth_exp_le_delta
symmetrization_uc_bound

Used by

vcdim_finite_imp_uc'

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_step to 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)))
```
ConceptClass EmpiricalError FLT.Concept GrowthFunction TrueErrorReal zeroOneLoss
Uses
Used by
- uc_bad_event_le_delta_proved

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_step for the opposite direction. Uses hoeffding_one_sided_upper instead of hoeffding_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}

ConceptClass EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss

Uses

hoeffding_one_sided_upper

Used by

symmetrization_uc_bound

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_pi to 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_sided with t = ε/2.
- The hm_large hypothesis 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.
- EmpiricalError is 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}
```
ConceptClass EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss
Uses
- hoeffding_one_sided
Used by
- symmetrization_uc_bound
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ε²/8
4. 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)
- SplitMeasure and ValidSplit (defined above)
- Measure.pi permutation invariance (to be proved or imported)
- Hoeffding for sampling without replacement
- GrowthFunction on 2m points + sauer_shelah_exp_bound from 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)))
```
ConceptClass EmpiricalError FLT.Concept GrowthFunction zeroOneLoss
Uses
- exchangeability_chain_bound
Used by
- symmetrization_uc_bound

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)))

ConceptClass EmpiricalError FLT.Concept GrowthFunction SignVector boolToSign zeroOneLoss

Uses

finite_exchangeability_bound
rademacher_mgf_bound
restriction_pattern_count
zeroOneLoss.congr_simp

Used by

double_sample_pattern_bound

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_3

zeroOneLoss

Used by

exchangeability_chain_bound

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 n
```
ConceptClass FLT.Concept GrowthFunction
Used by
- exchangeability_chain_bound

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))

SignVector boolToSign

Uses

cosh_le_exp_sq_half

Used by

exchangeability_chain_bound

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
- rademacher_mgf_bound

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 ≤ B

Used by

exchangeability_chain_bound

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

ConceptClass GrowthFunction

Uses

growth_function_le_two_pow
pow_mul_exp_neg_le_factorial_div
sum_choose_le_exp_pow

Used by

uc_bad_event_le_delta_proved

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
```
Used by
- growth_exp_le_delta
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 / t
```
Used by
- growth_exp_le_delta
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 ^ n
```
ConceptClass FLT.Concept GrowthFunction
Used by
- growth_exp_le_delta

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))

EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss

Used by

symmetrization_step_lower
vcdim_finite_imp_uc'

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_half infrastructure 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.pi independence structure.
- Needs: Measure.pi integral 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 : ℝ)
- EmpiricalError returns ℝ, TrueErrorReal returns ℝ, good — no ENNReal gap
- The measure value is ENNReal, the bound exp(-2mt²) is ℝ≥0∞ via ENNReal.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))
```
EmpiricalError FLT.Concept TrueErrorReal zeroOneLoss
Used by
- symmetrization_step
- vcdim_finite_imp_uc'
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
```
BatchLearner BatchLearner.learn ConceptClass EmpiricalError FLT.Concept HasUniformConvergence HypothesisSpace IsConsistentWith PACLearnable TrueError TrueErrorReal zeroOneLoss
Uses
- BatchLearner.output_in_H
Used by
- vcdim_finite_imp_pac_via_uc'
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.hypotheses
```
BatchLearner BatchLearner.hypotheses BatchLearner.learn FLT.Concept HypothesisSpace
Used by
- uc_imp_pac
DeclMeasurableConceptClass.hmeas_CDeclaration kindtheorem
```
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C],
  ∀ c ∈ C, Measurable c
```
ConceptClass FLT.Concept MeasurableConceptClass
Uses
- MeasurableConceptClass.mem_measurable
Used by
- online_imp_pac
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
```
ConceptClass FLT.Concept MeasurableConceptClass
Used by
- MeasurableConceptClass.hmeas_C
DeclMeasurableConceptClass.hc_measDeclaration kindtheorem
```
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C]
  (c : Concept X Bool), Measurable c
```
ConceptClass FLT.Concept MeasurableConceptClass
Uses
- MeasurableConceptClass.all_measurable
Used by
- online_imp_pac
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
```
ConceptClass FLT.Concept MeasurableConceptClass
Used by
- MeasurableConceptClass.hc_meas
DeclMeasurableConceptClass.hWBDeclaration kindtheorem
```
∀ {X : Type u} [inst : MeasurableSpace X] (C : ConceptClass X Bool) [h : MeasurableConceptClass X C], WellBehavedVC X C
```
ConceptClass MeasurableConceptClass WellBehavedVC
Uses
- MeasurableConceptClass.wellBehaved
Used by
- online_imp_pac
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 C
```
ConceptClass MeasurableConceptClass WellBehavedVC
Used by
- MeasurableConceptClass.hWB
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

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 → ℝ

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)
```
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)
```

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

DefinitionLTreeinductive
A complete binary Littlestone tree of depth n.
```
Type → ℕ → Type
```
DefinitionLTree.isShattereddef
Path-wise shattering for complete trees. Path B: leaf case requires C.Nonempty (NA₁₀).
```
{X : Type} → {n : ℕ} → ConceptClass X Bool → LTree X n → Prop
```
DefinitionLittlestoneDimdef
Littlestone dimension: the maximum depth of a complete shattered tree. Path B: returns WithBot (WithTop ℕ) so Ldim(∅) = ⊥ (NA₁₀).
```
(X : Type) → ConceptClass X Bool → WithBot (WithTop ℕ)
```
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
```
DefinitionMistakeBoundeddef
Mistake-bounded learning: the learner makes at most M mistakes on ANY sequence. No distribution assumption. Characterized by Littlestone dimension.
```
(X : Type u) → (Y : Type v) → [DecidableEq Y] → ConceptClass X Y → ℕ → Prop
```
DefinitionOnlineLearnabledef
Online learnable: there exists a finite mistake bound.
```
(X : Type u) → (Y : Type v) → [DecidableEq Y] → ConceptClass X Y → Prop
```
DefinitionOnlineLearnerstructure
An online learner: receives instances one at a time, makes predictions sequentially.
```
Type u → Type v → Type (max (max 1 u) v)
```

DefinitionOnlineLearner.Statedef

Internal state type

{X : Type u} → {Y : Type v} → OnlineLearner X Y → Type

DefinitionOnlineLearner.initdef

Initial state

{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State

DefinitionOnlineLearner.mistakesdef

Helper: run an online learner on a sequence, counting mistakes.

{X : Type u} → {Y : Type v} → [DecidableEq Y] → OnlineLearner X Y → Concept X Y → List X → ℕ

DefinitionOnlineLearner.mistakes.godef

{X : Type u} → {Y : Type v} → [DecidableEq Y] → (L : OnlineLearner X Y) → Concept X Y → L.State → List X → ℕ → ℕ

DefinitionOnlineLearner.mistakesFromdef

Count mistakes starting from state s.

{X : Type} → (L : OnlineLearner X Bool) → L.State → (X → Bool) → List X → ℕ

DefinitionOnlineLearner.predictdef
Predict: given current state and new instance, output a prediction
```
{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State → X → Y
```
DefinitionOnlineLearner.updatedef
Update: given current state, instance, and revealed true label, update state
```
{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State → X → Y → self.State
```
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
```
DefinitionShattersdefYaël Dillies
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
```
DefinitionboolToSigndef
Convert Bool labels to ±1 reals. true ↦ 1, false ↦ -1.
```
Bool → ℝ
```
DefinitionmistakesFromUdef
Count mistakes starting from state s (universe-polymorphic version).
```
{X : Type u} → (L : OnlineLearner X Bool) → L.State → (X → Bool) → List X → ℕ
```
DefinitionthresholdClassdef
Threshold concept class on ℕ: { (· ≤ n) | n : ℕ }. VCDim = 1 (PAC-learnable), LittlestoneDim = ∞ (not online-learnable).
```
ConceptClass ℕ Bool
```
DefinitionthresholdTreedef
Build a shattered Littlestone tree of depth d for the threshold class restricted to thresholds in interval [lo, lo + 2^d - 1]. The concept class parameter C should contain all thresholds (· ≤ n) for lo ≤ n ≤ lo + 2^d - 1. We show the tree is shattered by C when C ⊇ these thresholds.
```
ℕ → (d : ℕ) → LTree ℕ d
```
DefinitionzeroOneLossdef
The 0-1 loss for classification.
```
(Y : Type v) → [DecidableEq Y] → LossFunction Y
```

DOIMTH.R-2026-6028

Cite

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: 5835f1632641
Verified: 2026-09-24T00:00:00Z