Generalization Results (redirected to primed versions)

Theorems moved from Generalization.lean and Rademacher.lean. Each call has been redirected from the orphaned sorry'd version (e.g. vcdim_finite_imp_uc) to the primed version (e.g. vcdim_finite_imp_uc') in Symmetrization.lean.

Main results

• uc_does_not_imply_online : UC ⊬ online learnability (paradigm separation)
• consistent_learner_pac : consistency + finite VCDim → PAC
• sample_complexity_lower_bound : PAC lower bound via VCDim
• rademacher_vanishing_imp_pac : uniform Rademacher vanishing → PAC

theorem uc_does_not_imply_online (X : Type u) [MeasurableSpace X] [Infinite X] (hmeas_C_all : ∀ (C : ConceptClass X Bool), ∀ h ∈ C, Measurable h) (hc_meas_all : ∀ (c : Concept X Bool), Measurable c) (hWB_all : ∀ (C : ConceptClass X Bool), WellBehavedVC X C) : ¬∀ (C : ConceptClass X Bool), HasUniformConvergence X C → ∃ (M : ℕ), MistakeBounded X Bool C M

PAC uniform convergence does NOT imply online learnability. There exist concept classes with finite VCDim (hence PAC learnable) but infinite Littlestone dimension (hence not online learnable with finite mistake bound). Witness: threshold class C_φ on X via embedding φ : ℕ ↪ X. VCDim(C_φ) ≤ 1 (monotonicity prevents 2-shattering). LittlestoneDim(C_φ) = ∞ (adversary binary search forces d mistakes for any d).

theorem uc_does_not_imply_online' (X : Type u) [MeasurableSpace X] [Infinite X] [UniversallyMeasurableSpace X] : ¬∀ (C : ConceptClass X Bool), HasUniformConvergence X C → ∃ (M : ℕ), MistakeBounded X Bool C M

Typeclass version of uc_does_not_imply_online. Uses UniversallyMeasurableSpace to avoid threading ∀-quantified measurability.

theorem consistent_learner_pac (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (hvcdim : VCDim X C < ⊤) (hmeas_C : ∀ h ∈ C, Measurable h) (hc_meas : ∀ (c : Concept X Bool), Measurable c) (hWB : WellBehavedVC X C) (L : BatchLearner X Bool) (_hcons : ∀ {m : ℕ} (S : Fin m → X × Bool) (i : Fin m), L.learn S (S i).1 = (S i).2) : PACLearnable X C

Consistent learners are PAC learners when VCDim < ⊤.

theorem consistent_learner_pac' (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableConceptClass X C] (hvcdim : VCDim X C < ⊤) (L : BatchLearner X Bool) (hcons : ∀ {m : ℕ} (S : Fin m → X × Bool) (i : Fin m), L.learn S (S i).1 = (S i).2) : PACLearnable X C

Typeclass version of consistent_learner_pac.

theorem sample_complexity_lower_bound (X : Type u) [MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (d : ℕ) (hd : VCDim X C = ↑d) (ε δ : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1 / 4) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hδ2 : δ ≤ 1 / 7) (hd_pos : 1 ≤ d) (hmeas_C : ∀ h ∈ C, Measurable h) (hc_meas : ∀ (c : Concept X Bool), Measurable c) (hWB : WellBehavedVC X C) : ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ

Sample complexity lower bound: ⌈(d-1)/2⌉ ≤ SampleComplexity.

theorem sample_complexity_lower_bound' (X : Type u) [MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C] (d : ℕ) (hd : VCDim X C = ↑d) (ε δ : ℝ) (hε : 0 < ε) (hε1 : ε ≤ 1 / 4) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hδ2 : δ ≤ 1 / 7) (hd_pos : 1 ≤ d) : ⌈(↑d - 1) / 2⌉₊ ≤ SampleComplexity X C ε δ

Typeclass version of sample_complexity_lower_bound.

theorem rademacher_vanishing_imp_pac (X : Type u) [MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) (hmeas_C : ∀ h ∈ C, Measurable h) (hc_meas : ∀ (c : Concept X Bool), Measurable c) (hWB : WellBehavedVC X C) (hrad : ∀ ε > 0, ∃ (m₀ : ℕ), ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) : PACLearnable X C

Rademacher vanishing → PAC learnability (← direction of fundamental_rademacher). Uses uniform vanishing (∃ m₀ ∀ D), the textbook-standard form.

theorem rademacher_vanishing_imp_pac' (X : Type u) [MeasurableSpace X] [MeasurableSingletonClass X] (C : ConceptClass X Bool) [MeasurableConceptClass X C] (hrad : ∀ ε > 0, ∃ (m₀ : ℕ), ∀ (D : MeasureTheory.Measure X), MeasureTheory.IsProbabilityMeasure D → ∀ m ≥ m₀, RademacherComplexity X C D m < ε) : PACLearnable X C

Typeclass version of rademacher_vanishing_imp_pac.