Littlestone Dimension (Online Paradigm)

The online-learning analog of VC dimension. Characterizes mistake-bounded learnability.

inductive MistakeTree (X : Type u) : Type u

A mistake tree (Littlestone tree): a complete binary tree where each internal node is labeled with an instance x.

• leaf {X : Type u} : MistakeTree X
• branch {X : Type u} : X → MistakeTree X → MistakeTree X → MistakeTree X

def MistakeTree.depth {X : Type u} : MistakeTree X → ℕ

Depth of a mistake tree.

Equations

• MistakeTree.leaf.depth = 0
• (MistakeTree.branch a l r).depth = 1 + max l.depth r.depth

def MistakeTree.isShattered (X : Type u) (C : ConceptClass X Bool) : MistakeTree X → Prop

A mistake tree is shattered by C if every root-to-leaf path is realized by some concept in C.

Note: This branch-wise definition does NOT restrict the concept class at recursive calls. It allows different witness concepts at each tree level without requiring path consistency. Counterexample: C = {const_true, const_false} gives LittlestoneDim = ⊤ under this definition, but C is online-learnable with M = 1.

The correct definition (used in Theorem/Online.lean) restricts C at each branch: | .branch x l r => (∃ c ∈ C, c x = true) ∧ (∃ c ∈ C, c x = false) ∧ isShattered X {c ∈ C | c x = true} l ∧ isShattered X {c ∈ C | c x = false} r

The characterization theorem uses the corrected version.

Equations

• MistakeTree.isShattered X C MistakeTree.leaf = True
• MistakeTree.isShattered X C (MistakeTree.branch a l r) = ((∃ c ∈ C, c a = true ∧ MistakeTree.isShattered X C l) ∧ ∃ c ∈ C, c a = false ∧ MistakeTree.isShattered X C r)

noncomputable def BranchWiseLittlestoneDim (X : Type u) (C : ConceptClass X Bool) : WithTop ℕ

Littlestone dimension (branch-wise variant): see Theorem/Online.lean for the corrected path-consistent version used in the characterization theorem.

Equations

• BranchWiseLittlestoneDim X C = ⨆ (T : MistakeTree X), ⨆ (_ : MistakeTree.isShattered X C T), ↑T.depth

def MistakeTree.fromList {X : Type u} : List X → MistakeTree X

Build a complete binary tree from a list of instances.

Equations

• MistakeTree.fromList [] = MistakeTree.leaf
• MistakeTree.fromList (x_1 :: xs) = MistakeTree.branch x_1 (MistakeTree.fromList xs) (MistakeTree.fromList xs)

theorem MistakeTree.fromList_depth {X : Type u} (l : List X) : (fromList l).depth = l.length

The depth of a mistake tree built from a list of length n equals n. The basic well-formedness property of the fromList constructor: depth tracks list length exactly, so the Littlestone dimension can be read off from a built tree.

theorem Shatters.subset {X : Type u} {C : ConceptClass X Bool} {S T : Finset X} (hS : Shatters X C S) (hTS : T ⊆ S) : Shatters X C T

If C shatters a Finset S (every labeling realized), restricting to a subset still shatters.

theorem MistakeTree.fromList_shattered {X : Type u} [DecidableEq X] {C : ConceptClass X Bool} (l : List X) (hl : l.Nodup) (hS : Shatters X C l.toFinset) : isShattered X C (fromList l)

A shattered tree can be built from any list of elements from a shattered Finset.

theorem BranchWiseLittlestoneDim_ge_VCDim (X : Type u) [DecidableEq X] (C : ConceptClass X Bool) : VCDim X C ≤ BranchWiseLittlestoneDim X C

Ldim (branch-wise) upper bounds VCdim: Ldim(C) ≥ VCdim(C) for all C. Uses the branch-wise definition. See Theorem/Online.lean for the corrected version.