Mathesis

Dhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z

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.

Decloptimal_mistake_bound_eq_ldim

∀ (X : Type) (C : ConceptClass X Bool), Set.Nonempty C → ↑(OptimalMistakeBound X C) = LittlestoneDim X C

TopicOnline learning

ThesisStepHypothesisDefinition

Decloptimal_mistake_bound_eq_ldimDeclaration kindtheorem
```
∀ (X : Type) (C : ConceptClass X Bool), Set.Nonempty C → ↑(OptimalMistakeBound X C) = LittlestoneDim X C
```
ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim MistakeBounded OnlineLearnable OnlineLearner OnlineLearner.State OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakesFrom OptimalMistakeBound SOA versionSpace
Uses
Declbackward_directionDeclaration kindtheorem
Backward direction: LittlestoneDim < ⊤ → OnlineLearnable.
```
∀ (X : Type) (C : ConceptClass X Bool), LittlestoneDim X C < ⊤ → OnlineLearnable X Bool C
```
ConceptClass FLT.Concept LittlestoneDim MistakeBounded OnlineLearnable OnlineLearner OnlineLearner.State OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakesFrom SOA versionSpace
Uses
Used by
- optimal_mistake_bound_eq_ldim
Declsoa_mistakes_boundedDeclaration kindtheorem
SOA mistakes from a given state are bounded by the Ldim of the version space. This is the core M-Potential argument.
```
∀ {X : Type} {C : ConceptClass X Bool},
  ∀ c ∈ C,
    ∀ (history : List (X × Bool)),
      (∀ p ∈ history, c p.1 = p.2) →
        ∀ (d : ℕ),
          LittlestoneDim X (versionSpace C history) ≤ ↑↑d →
            LittlestoneDim X (versionSpace C history) < ⊤ → ∀ (seq : List X), (SOA X C).mistakesFrom history c seq ≤ d
```
ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim OnlineLearner.mistakesFrom OnlineLearner.predict SOA versionSpace
Uses
Used by
- backward_direction
- optimal_mistake_bound_eq_ldim

DeclversionSpace_appendDeclaration kindtheorem

Extending history restricts the version space.

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

ConceptClass FLT.Concept versionSpace

Used by

soa_mistakes_bounded

Decltarget_in_versionSpaceDeclaration kindtheorem

Target stays in version space.

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

ConceptClass FLT.Concept versionSpace

Used by

soa_mistakes_bounded

Declldim_strict_decrease_on_mistakeDeclaration kindtheorem
On an SOA mistake, the Ldim of the version space strictly decreases.
```
∀ {X : Type} {C : ConceptClass X Bool} {history : List (X × Bool)} {x : X} {c : X → Bool},
  c ∈ versionSpace C history →
    (SOA X C).predict history x ≠ c x →
      LittlestoneDim X (versionSpace C history) < ⊤ →
        LittlestoneDim X (versionSpace C (history ++ [(x, c x)])) < LittlestoneDim X (versionSpace C history)
```
ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim OnlineLearner.predict SOA versionSpace
Uses
Used by
- soa_mistakes_bounded

Declsoa_predict_specDeclaration kindtheorem

SOA predicts the label whose side has higher Ldim.

∀ {X : Type} (C : ConceptClass X Bool) (history : List (X × Bool)) (x : X),
  have V := versionSpace C history;
  have b := (SOA X C).predict history x;
  LittlestoneDim X {c | c ∈ V ∧ c x = b} ≥ LittlestoneDim X {c | c ∈ V ∧ c x = !b}

ConceptClass FLT.Concept LittlestoneDim OnlineLearner.predict SOA versionSpace

Used by

ldim_strict_decrease_on_mistake

Declldim_zero_all_agreeDeclaration kindtheorem
When Ldim(V) = 0 (↑↑0), all concepts in V agree on every point. Key lemma for M-VersionSpaceCollapse.
```
∀ {X : Type} {V : ConceptClass X Bool},
  LittlestoneDim X V = ↑0 → Set.Nonempty V → ∀ (x : X) (c₁ c₂ : X → Bool), c₁ ∈ V → c₂ ∈ V → c₁ x = c₂ x
```
ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim
Used by
- ldim_strict_decrease_on_mistake

Declldim_branch_lower_boundDeclaration kindtheorem

Build a tree of depth k+1 from shattered subtrees on both sides. Parametrized over b : Bool so we don't need to case-split in the caller.

∀ {X : Type} {V : ConceptClass X Bool} {x : X} {k : ℕ} {b : Bool},
  (∃ Tb, LTree.isShattered {c | c ∈ V ∧ c x = b} Tb) →
    (∃ Tnb, LTree.isShattered {c | c ∈ V ∧ c x = !b} Tnb) →
      (∃ c ∈ V, c x = b) → (∃ c ∈ V, c x = !b) → LittlestoneDim X V ≥ ↑↑(k + 1)

ConceptClass FLT.Concept LTree LTree.isShattered LittlestoneDim

Used by

ldim_strict_decrease_on_mistake

Declexists_shattered_of_ldim_geDeclaration kindtheorem
From Ldim ≥ d, extract a shattered tree of depth exactly d.
```
∀ {X : Type} {C : ConceptClass X Bool} {d : ℕ}, LittlestoneDim X C ≥ ↑↑d → ∃ T, LTree.isShattered C T
```
ConceptClass FLT.Concept LTree LTree.isShattered LTree.truncate LittlestoneDim
Uses
- LTree.isShattered_truncate
- LTree.nonempty_of_isShattered
Used by
- ldim_strict_decrease_on_mistake
DeclLTree.isShattered_truncateDeclaration kindtheorem
A truncated tree is shattered if the original is.
```
∀ {X : Type} {C : ConceptClass X Bool} {m : ℕ} (T : LTree X m),
  LTree.isShattered C T → ∀ {n : ℕ} (h : n ≤ m), LTree.isShattered C (LTree.truncate h T)
```
ConceptClass FLT.Concept LTree LTree.isShattered LTree.truncate
Uses
- LTree.nonempty_of_isShattered
Used by
- exists_shattered_of_ldim_ge
DeclWithBot_WithTop_lt_succ_leDeclaration kindtheorem
In WithBot (WithTop ℕ), a < ↑↑(n+1) → a ≤ ↑↑n. Reusable lattice fact.
```
∀ {a : WithBot (WithTop ℕ)} {n : ℕ}, a < ↑↑(n + 1) → a ≤ ↑↑n
```
Used by
- soa_mistakes_bounded

DeclSOA_mistakesFrom_consDeclaration kindtheorem

SOA mistakesFrom cons: unfold one step using the interface.

∀ (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

ConceptClass OnlineLearner.mistakesFrom OnlineLearner.predict SOA

Used by

soa_mistakes_bounded

DeclLTree.isShattered_monoDeclaration kindtheorem
Shattering is upward-monotone in the concept class.
```
∀ {X : Type} {n : ℕ} (T : LTree X n) {C C' : ConceptClass X Bool},
  C ⊆ C' → LTree.isShattered C T → LTree.isShattered C' T
```
ConceptClass FLT.Concept LTree LTree.isShattered
Used by
- ldim_strict_decrease_on_mistake
- soa_mistakes_bounded
Decladversary_lower_boundDeclaration kindtheorem
Adversary lower bound (M-InfSup reusable primitive): If a tree of depth n is shattered by C, then any mistake-bounded learner must allow at least n mistakes. This is the "inf ≥ sup" half of minimax.
```
∀ {X : Type} {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n),
  LTree.isShattered C T → ∀ {M : ℕ}, MistakeBounded X Bool C M → n ≤ M
```
ConceptClass FLT.Concept LTree LTree.isShattered MistakeBounded OnlineLearner OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakesFrom
Uses
Used by
- optimal_mistake_bound_eq_ldim
DeclmistakesFrom_init_eqDeclaration kindtheorem
Relate mistakesFrom to the original mistakes function.
```
∀ {X : Type} (L : OnlineLearner X Bool) (c : X → Bool) (seq : List X), L.mistakesFrom L.init c seq = L.mistakes c seq
```
OnlineLearner OnlineLearner.State OnlineLearner.init OnlineLearner.mistakes OnlineLearner.mistakes.go OnlineLearner.mistakesFrom OnlineLearner.predict OnlineLearner.update
Used by
Decladversary_coreDeclaration kindtheorem
Core adversary lemma.
```
∀ {X : Type} (L : OnlineLearner X Bool) (s : L.State) {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n),
  LTree.isShattered C T → Set.Nonempty C → ∃ seq, ∃ c ∈ C, L.mistakesFrom s c seq = n
```
ConceptClass FLT.Concept LTree LTree.isShattered OnlineLearner OnlineLearner.State OnlineLearner.mistakesFrom OnlineLearner.predict OnlineLearner.update
Used by
- adversary_lower_bound
DeclLTree.nonempty_of_isShatteredDeclaration kindtheorem
Helper: shattering implies the concept class is nonempty.
```
∀ {X : Type} {C : ConceptClass X Bool} {n : ℕ} (T : LTree X n), LTree.isShattered C T → Set.Nonempty C
```
ConceptClass FLT.Concept LTree LTree.isShattered
Used by
DeclSOA_init_eqDeclaration kindtheorem
SOA init state is empty history.
```
∀ (X : Type) (C : ConceptClass X Bool), (SOA X C).init = []
```
ConceptClass OnlineLearner.State OnlineLearner.init SOA
Used by
- backward_direction
- optimal_mistake_bound_eq_ldim
Hypothesishne
```
Set.Nonempty C
```
DefinitionConceptClassdef
A concept class is a set of concepts. Used by every paradigm, complexity measure, and criterion.
Primary definition: Set of functions. Used for PAC/agnostic PAC where concept classes are sets over which VC dimension, Rademacher complexity, covering numbers, etc. are measured. Alternative definitions below for contexts requiring decidability, enumerability, or measurability.
```
Type u → Type v → Type (max v u)
```
DefinitionFLT.Conceptdef
A concept is a function from domain to label. This is the atomic unit that concept classes collect and learners try to approximate.
```
Type u → Type v → Type (max u v)
```
DefinitionLTreeinductive
A complete binary Littlestone tree of depth n.
```
Type → ℕ → Type
```
DefinitionLTree.isShattereddef
Path-wise shattering for complete trees. Path B: leaf case requires C.Nonempty (NA₁₀).
```
{X : Type} → {n : ℕ} → ConceptClass X Bool → LTree X n → Prop
```
DefinitionLTree.truncatedef
Truncate a complete tree to a smaller depth.
```
{X : Type} → {n m : ℕ} → n ≤ m → LTree X m → LTree X n
```
DefinitionLittlestoneDimdef
Littlestone dimension: the maximum depth of a complete shattered tree. Path B: returns WithBot (WithTop ℕ) so Ldim(∅) = ⊥ (NA₁₀).
```
(X : Type) → ConceptClass X Bool → WithBot (WithTop ℕ)
```
DefinitionMistakeBoundeddef
Mistake-bounded learning: the learner makes at most M mistakes on ANY sequence. No distribution assumption. Characterized by Littlestone dimension.
```
(X : Type u) → (Y : Type v) → [DecidableEq Y] → ConceptClass X Y → ℕ → Prop
```
DefinitionOnlineLearnabledef
Online learnable: there exists a finite mistake bound.
```
(X : Type u) → (Y : Type v) → [DecidableEq Y] → ConceptClass X Y → Prop
```
DefinitionOnlineLearnerstructure
An online learner: receives instances one at a time, makes predictions sequentially.
```
Type u → Type v → Type (max (max 1 u) v)
```

DefinitionOnlineLearner.Statedef

Internal state type

{X : Type u} → {Y : Type v} → OnlineLearner X Y → Type

DefinitionOnlineLearner.initdef

Initial state

{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State

DefinitionOnlineLearner.mistakesdef

Helper: run an online learner on a sequence, counting mistakes.

{X : Type u} → {Y : Type v} → [DecidableEq Y] → OnlineLearner X Y → Concept X Y → List X → ℕ

DefinitionOnlineLearner.mistakes.godef

{X : Type u} → {Y : Type v} → [DecidableEq Y] → (L : OnlineLearner X Y) → Concept X Y → L.State → List X → ℕ → ℕ

DefinitionOnlineLearner.mistakesFromdef

Count mistakes starting from state s.

{X : Type} → (L : OnlineLearner X Bool) → L.State → (X → Bool) → List X → ℕ

DefinitionOnlineLearner.predictdef
Predict: given current state and new instance, output a prediction
```
{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State → X → Y
```
DefinitionOnlineLearner.updatedef
Update: given current state, instance, and revealed true label, update state
```
{X : Type u} → {Y : Type v} → (self : OnlineLearner X Y) → self.State → X → Y → self.State
```
DefinitionOptimalMistakeBounddef
Mistake bound: minimum worst-case mistakes for online learning of C.
```
(X : Type u) → ConceptClass X Bool → WithTop ℕ
```

DefinitionSOAdef

The Standard Optimal Algorithm (SOA).

(X : Type) → ConceptClass X Bool → OnlineLearner X Bool

DefinitionversionSpacedef

Version space after observing a history.

{X : Type} → ConceptClass X Bool → List (X × Bool) → ConceptClass X Bool

DOIMTH.R-2026-6011

Cite

Verification

Replay: accepted
Axioms: Classical.choiceQuot.soundpropext
Statement identity: not-applicable
Substrate: Lean 4 kernel v4.31.0
Dictionary pin: design-lab@5802df4 · initial
Frozen export: 5fe03070080b
Verified: 2026-09-24T00:00:00Z