Online Learning Characterization Theorems

Characterization proofs for online learnability via the Littlestone dimension. Game-theoretic infrastructure (LTree, isShattered, LittlestoneDim, SOA, versionSpace) lives in FLT_Proofs.Complexity.GameInfra.

Main results:

• forward_direction: OnlineLearnable → LittlestoneDim < ⊤
• backward_direction: LittlestoneDim < ⊤ → OnlineLearnable
• littlestone_characterization: equivalence of the above
• optimal_mistake_bound_eq_ldim: OptimalMistakeBound = LittlestoneDim (for nonempty C)

theorem forward_direction (X : Type) (C : ConceptClass X Bool) : OnlineLearnable X Bool C → LittlestoneDim X C < ⊤

Forward direction: OnlineLearnable → LittlestoneDim < ⊤

def LTree.truncate {X : Type} {n m : ℕ} (h : n ≤ m) : LTree X m → LTree X n

Truncate a complete tree to a smaller depth.

Equations

• One or more equations did not get rendered due to their size.

theorem LTree.isShattered_truncate {X : Type} {C : ConceptClass X Bool} {m : ℕ} (T : LTree X m) (hT : isShattered C T) {n : ℕ} (h : n ≤ m) : isShattered C (truncate h T)

A truncated tree is shattered if the original is.

theorem backward_direction (X : Type) (C : ConceptClass X Bool) : LittlestoneDim X C < ⊤ → OnlineLearnable X Bool C

Backward direction: LittlestoneDim < ⊤ → OnlineLearnable.

theorem littlestone_characterization (X : Type) (C : ConceptClass X Bool) : OnlineLearnable X Bool C ↔ LittlestoneDim X C < ⊤

Littlestone characterization: C is online-learnable iff LittlestoneDim(C) < ∞.

theorem optimal_mistake_bound_eq_ldim (X : Type) (C : ConceptClass X Bool) (hne : Set.Nonempty C) : ↑(OptimalMistakeBound X C) = LittlestoneDim X C

The optimal mistake bound equals the Littlestone dimension (for nonempty C). Path B: OptimalMistakeBound : WithTop ℕ, LittlestoneDim : WithBot (WithTop ℕ). For nonempty C, LittlestoneDim ≥ 0, so the coercion ↑(OptimalMistakeBound) works.