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
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6011 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6011
Cite
Verification
- Library
- FLT_Proofs.Theorem.Online
- Statement digest
- 3beeca7ea2fe
- First verified
- 2026-09-24T00:00:00Z