Online Learning Criteria

Mistake-bounded learning, online learnability, and regret bounds. Characterized by Littlestone dimension.

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

Count mistakes from an arbitrary online-learner state.

Equations

• L.mistakesFrom state c [] = 0
• L.mistakesFrom state c (x_1 :: xs) = (if L.predict state x_1 ≠ c x_1 then 1 else 0) + L.mistakesFrom (L.update state x_1 (c x_1)) c xs

noncomputable def OnlineLearner.mistakes {X : Type u} {Y : Type v} [DecidableEq Y] (L : OnlineLearner X Y) (c : Concept X Y) (seq : List X) : ℕ

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

Equations

• L.mistakes c seq = L.mistakesFrom L.init c seq

def MistakeBounded (X : Type u) (Y : Type v) [DecidableEq Y] (C : ConceptClass X Y) (M : ℕ) : Prop

Mistake-bounded learning: the learner makes at most M mistakes on ANY sequence. No distribution assumption. Characterized by Littlestone dimension.

Equations

• MistakeBounded X Y C M = ∃ (L : OnlineLearner X Y), ∀ c ∈ C, ∀ (seq : List X), L.mistakes c seq ≤ M

def OnlineLearnable (X : Type u) (Y : Type v) [DecidableEq Y] (C : ConceptClass X Y) : Prop

Online learnable: there exists a finite mistake bound.

Equations

• OnlineLearnable X Y C = ∃ (M : ℕ), MistakeBounded X Y C M

noncomputable def OnlineLearner.cumulativeLoss {X : Type u} {Y : Type v} (L : OnlineLearner X Y) (loss : LossFunction Y) (seq : List (X × Y)) : ℝ

Helper: cumulative loss of an online learner on a sequence.

Equations

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

noncomputable def fixedHypothesisLoss {X : Type u} {Y : Type v} (h : Concept X Y) (loss : LossFunction Y) (seq : List (X × Y)) : ℝ

Helper: cumulative loss of a fixed hypothesis on a sequence.

Equations

• fixedHypothesisLoss h loss seq = List.foldl (fun (acc : ℝ) (p : X × Y) => acc + loss (h p.1) p.2) 0 seq

def RegretBounded (X : Type u) (Y : Type v) (H : HypothesisSpace X Y) (loss : LossFunction Y) (bound : ℕ → ℝ) : Prop

Regret-bounded learning: the learner's cumulative loss is close to the best hypothesis in hindsight. No distributional assumptions.

Equations

• RegretBounded X Y H loss bound = ∃ (L : OnlineLearner X Y), ∀ (seq : List (X × Y)), ∀ h ∈ H, L.cumulativeLoss loss seq - fixedHypothesisLoss h loss seq ≤ bound seq.length