Theorem 8.2, p. 144 — Perceptron mistake bound against every hinge power

Proved

ModernOnlineLearning.Classification.theorem_8_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

machine-learningmistake-boundonline-classificationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-bookp2o-v1perceptron

Let $(z_t,y_t)_{t=1}^T$ be any sequence with $z_t\in\mathbb R^d$ , $y_t\in\{-1,1\}$ , and $\|z_t\|_2\le R$ . Run Algorithm 8.2 and write $M$ for its number of mistakes, counting zero-score predictions as mistakes. For every $u\in\mathbb R^d$ and every real $q\ge1$ , put $L_q(u)=\sum_{t=1}^T\max(1-y_t\langle z_t,u\rangle,0)^q$ . Then

M-L_q(u)\le \frac{q^2R^2\|u\|_2^2}{2} +qR\|u\|_2\sqrt{\frac{q^2R^2\|u\|_2^2}{4}+L_q(u)}.

The bound compares the Perceptron's mistakes simultaneously with the hinge-power loss of every fixed linear competitor.

Formalization Note Rounds are indexed from $1$ . The auxiliary feature set $X\subseteq\mathbb R^d$ is omitted because the theorem quantifies over the sequence itself and uses only its norm bound. The implicit $R\ge0$ is explicit; $R=0$ and $T=0$ are included. The square-root argument is nonnegative since hinge-power losses are nonnegative for $q\ge1$ .

Preamble

import Mathlib
import Definitions.Def_ModernOnlineLearning_Classification_Perceptron

Formal statement

namespace ModernOnlineLearning.Classification

/-- Orabona, Theorem 8.2, p. 144: the Perceptron mistake bound for every
competitor and every real hinge power `q ≥ 1`. -/
theorem theorem_8_2 {d : ℕ} (T : ℕ) (z : ℕ → ModernOnlineLearning.Adaptive.Vec d) (y : ℕ → ℝ)
    (hy : ∀ t ∈ Finset.Icc 1 T, y t = -1 ∨ y t = 1)
    (R : ℝ) (hR : 0 ≤ R)
    (hz : ∀ t ∈ Finset.Icc 1 T, ‖z t‖ ≤ R)
    (u : ModernOnlineLearning.Adaptive.Vec d) (q : ℝ) (hq : 1 ≤ q) :
    mistakes z y T - cumulativeHinge z y T u q ≤
      q ^ 2 * R ^ 2 * ‖u‖ ^ 2 / 2 +
        q * R * ‖u‖ * Real.sqrt
          (q ^ 2 * R ^ 2 * ‖u‖ ^ 2 / 4 + cumulativeHinge z y T u q) := by sorry

end ModernOnlineLearning.Classification

Source

Orabona, arXiv:1912.13213v10, Theorem 8.2, p. 144; Algorithm 8.2 and hinge-power loss, p. 143

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph