Game-Theoretic Infrastructure for Online Learning

Definitions and interface lemmas for the online learning game:

• LTree: depth-indexed complete Littlestone trees
• LTree.isShattered: path-wise shattering
• LittlestoneDim: Littlestone dimension as WithBot (WithTop ℕ)
• OnlineLearner.mistakesFrom: mistake counting from arbitrary state
• adversary_core: core adversary lemma
• versionSpace, SOA: Standard Optimal Algorithm and its interface
• Version-space infrastructure lemmas

Characterization theorems live in FLT_Proofs.Theorem.Online.

inductive LTree (X : Type) : ℕ → Type

A complete binary Littlestone tree of depth n.

• leaf {X : Type} : LTree X 0
• branch {X : Type} {n : ℕ} : X → LTree X n → LTree X n → LTree X (n + 1)

def LTree.isShattered {X : Type} {n : ℕ} (C : ConceptClass X Bool) : LTree X n → Prop

Path-wise shattering for complete trees. Path B: leaf case requires C.Nonempty (NA₁₀).

Equations

• One or more equations did not get rendered due to their size.
• LTree.isShattered C LTree.leaf = Set.Nonempty C

theorem LTree.nonempty_of_isShattered {X : Type} {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n) (hT : isShattered C T) : Set.Nonempty C

Helper: shattering implies the concept class is nonempty.

theorem LTree.isShattered_mono {X : Type} {n : ℕ} (T : LTree X n) {C C' : ConceptClass X Bool} (h : C ⊆ C') : isShattered C T → isShattered C' T

Shattering is upward-monotone in the concept class.

noncomputable def LittlestoneDim (X : Type) (C : ConceptClass X Bool) : WithBot (WithTop ℕ)

Littlestone dimension: the maximum depth of a complete shattered tree. Path B: returns WithBot (WithTop ℕ) so Ldim(∅) = ⊥ (NA₁₀).

Equations

• LittlestoneDim X C = ⨆ (n : ℕ), ⨆ (_ : ∃ (T : LTree X n), LTree.isShattered C T), ↑↑n

theorem adversary_core {X : Type} (L : OnlineLearner X Bool) (s : L.State) {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n) (hT : LTree.isShattered C T) (hne : Set.Nonempty C) : ∃ (seq : List X), ∃ c ∈ C, L.mistakesFrom s c seq = n

Core adversary lemma.

theorem mistakesFrom_init_eq {X : Type} (L : OnlineLearner X Bool) (c : X → Bool) (seq : List X) : L.mistakesFrom L.init c seq = L.mistakes c seq

Relate mistakesFrom to the original mistakes function.

def versionSpace {X : Type} (C : ConceptClass X Bool) (history : List (X × Bool)) : ConceptClass X Bool

Version space after observing a history.

Equations

• versionSpace C history = {c : Concept X Bool | c ∈ C ∧ ∀ p ∈ history, c p.1 = p.2}

noncomputable def SOA (X : Type) (C : ConceptClass X Bool) : OnlineLearner X Bool

The Standard Optimal Algorithm (SOA).

Equations

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

theorem SOA_predict_eq (X : Type) (C : ConceptClass X Bool) (history : List (X × Bool)) (x : X) : (SOA X C).predict history x = if LittlestoneDim X {c : Concept X Bool | c ∈ versionSpace C history ∧ c x = true} ≥ LittlestoneDim X {c : Concept X Bool | c ∈ versionSpace C history ∧ c x = false} then true else false

SOA prediction: picks the label whose version space side has higher Ldim. NOT @[simp]: proofs should explicitly opt-in to see SOA internals (Inv-stability).

theorem SOA_update_eq (X : Type) (C : ConceptClass X Bool) (history : List (X × Bool)) (x : X) (y : Bool) : (SOA X C).update history x y = history ++ [(x, y)]

SOA state update: append observation to history. NOT @[simp]: explicit use preserves abstraction barrier.

theorem SOA_init_eq (X : Type) (C : ConceptClass X Bool) : (SOA X C).init = []

SOA init state is empty history.

theorem SOA_mistakesFrom_cons (X : Type) (C : ConceptClass X Bool) (history : List (X × Bool)) (c : X → Bool) (x : X) (xs : List X) : (SOA X C).mistakesFrom history c (x :: xs) = (if (SOA X C).predict history x ≠ c x then 1 else 0) + (SOA X C).mistakesFrom (history ++ [(x, c x)]) c xs

SOA mistakesFrom cons: unfold one step using the interface.

theorem versionSpace_subset {X : Type} {C : ConceptClass X Bool} {history : List (X × Bool)} : versionSpace C history ⊆ C

Version space subset.

theorem target_in_versionSpace {X : Type} {C : ConceptClass X Bool} {c : X → Bool} (hcC : c ∈ C) {history : List (X × Bool)} (hcons : ∀ p ∈ history, c p.1 = p.2) : c ∈ versionSpace C history

Target stays in version space.

theorem versionSpace_append {X : Type} {C : ConceptClass X Bool} {history : List (X × Bool)} {x : X} {y : Bool} : versionSpace C (history ++ [(x, y)]) ⊆ versionSpace C history

Extending history restricts the version space.

theorem ldim_versionSpace_le {X : Type} {C : ConceptClass X Bool} {history : List (X × Bool)} : LittlestoneDim X (versionSpace C history) ≤ LittlestoneDim X C

Ldim of version space ≤ Ldim of C.