Separation Theorems

These prove that the paradigms are genuinely different — the criteria do NOT imply each other.

theorem online_imp_pac (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) (hol : OnlineLearnable X Bool C) [MeasurableConceptClass X C] : PACLearnable X C

Online learnable → PAC learnable. Γ₄₈: requires LittlestoneDim → VCDim bridge or online-to-batch conversion.

def LearnEvalMeasurable {X : Type u} [MeasurableSpace X] (L : BatchLearner X Bool) : Prop

Joint measurability of a batch learner's evaluation map.

Equations

• LearnEvalMeasurable L = ∀ (m : ℕ), Measurable fun (p : (Fin m → X × Bool) × X) => L.learn p.1 p.2

theorem universal_imp_pac (X : Type u) [MeasurableSpace X] (C : ConceptClass X Bool) [MeasurableHypotheses X C] (hL_meas : ∀ (L : BatchLearner X Bool), LearnEvalMeasurable L) (hul : UniversalLearnable X C) : PACLearnable X C

Universal learnable → PAC learnable. Proof sketch: UniversalLearnable gives learner L with rate → 0 and Pr[error ≤ rate(m)] ≥ 2/3. Two components:

1. Event containment: rate(m) < ε ⟹ {error ≤ rate(m)} ⊆ {error ≤ ε} (monotonicity).
2. Confidence boosting: 2/3 → 1-δ via median-of-means (Γ₆₇, sorry'd in boost_two_thirds_to_pac). Routes through boost_two_thirds_to_pac which encapsulates the Chernoff-based boosting.

theorem pac_not_implies_online : ∃ (X : Type) (x : MeasurableSpace X) (C : ConceptClass X Bool), PACLearnable X C ∧ ¬OnlineLearnable X Bool C

theorem ex_not_implies_pac : ∃ (X : Type) (_ : Countable X) (x : MeasurableSpace X) (C : ConceptClass X Bool), EXLearnable X C ∧ ¬PACLearnable X C

EX does not imply PAC. Witness: X = ℕ, C = all indicator functions of finite subsets of ℕ. EX-learnable: learner outputs "true on everything seen so far" — converges on any text. Not PAC-learnable: VCDim = ⊤ (every finite set is shattered).

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

Online learning is strictly stronger than PAC learning.

theorem ex_strictly_stronger_finite (X : Type u) (C : ConceptClass X Bool) : FiniteLearnable X C → EXLearnable X C

EX learning is strictly stronger than finite learning.

theorem online_pac_gold_separation : (∃ (X : Type) (x : MeasurableSpace X) (C : ConceptClass X Bool), PACLearnable X C ∧ ¬OnlineLearnable X Bool C) ∧ ∃ (X : Type) (_ : Countable X) (x : MeasurableSpace X) (C : ConceptClass X Bool), EXLearnable X C ∧ ¬PACLearnable X C

Online-PAC-Gold three-way separation. Pl-REPAIR: first conjunct had [Fintype X] which made it false. Fixed to match pac_not_implies_online repair.