Online Learning Criteria

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

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 = OnlineLearner.mistakes.go L c L.init seq 0

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

Equations

• OnlineLearner.mistakes.go L c state [] count = count
• OnlineLearner.mistakes.go L c state (x :: xs) count = OnlineLearner.mistakes.go L c (L.update state x (c x)) xs (if L.predict state x ≠ c x then count + 1 else count)

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

• L.cumulativeLoss loss seq = OnlineLearner.cumulativeLoss.go L loss L.init seq 0

noncomputable def OnlineLearner.cumulativeLoss.go {X : Type u} {Y : Type v} (L : OnlineLearner X Y) (loss : LossFunction Y) (state : L.State) (remaining : List (X × Y)) (acc : ℝ) : ℝ

Equations

• OnlineLearner.cumulativeLoss.go L loss state [] acc = acc
• OnlineLearner.cumulativeLoss.go L loss state ((x, y) :: rest) acc = OnlineLearner.cumulativeLoss.go L loss (L.update state x y) rest (acc + loss (L.predict state x) y)

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