From 13df3d63d6711457bf6b198c7ce46a5972db2f76 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 03:50:16 +0100 Subject: [PATCH 1/2] feat: FTRL-Proximal, and follow-the-leader on strongly convex and quadratized losses Sum the proximal stability lemma [Ora, Lemma 7.7] through the FTRL equality, and derive from it the regret of FTRL-Proximal [Ora, Example 7.9], of follow-the-leader on strongly convex losses [Ora, Corollary 7.25] and on quadratized losses [Ora, Algorithm 7.5], the closed form (7.9) of the latter's plays, and the 1 + log n regret of follow-the-leader on the guessing game [Ora, Example 7.26]. Co-Authored-By: Claude Code --- .../Analysis/Convex/Bregman/Euclidean.lean | 21 +- LMLExplore/Analysis/Convex/Strong.lean | 15 ++ LMLExplore/OnlineLearning/FTRL/Quadratic.lean | 214 ++++++++++++++++++ LMLExplore/OnlineLearning/FTRL/Stability.lean | 68 +++++- LMLExplore/OnlineLearning/Regret.lean | 6 + 5 files changed, 319 insertions(+), 5 deletions(-) create mode 100644 LMLExplore/OnlineLearning/FTRL/Quadratic.lean diff --git a/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean b/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean index f5943374..cdc19463 100644 --- a/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean +++ b/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean @@ -21,8 +21,9 @@ With this potential, mirror descent is projected gradient descent. * `LMLExplore.hasFDerivAt_norm_sq_div_two`: the derivative of `‖b‖ ^ 2 / 2` at `x` is `⟪x, ·⟫`. * `LMLExplore.bregDiv_norm_sq_div_two`: the Bregman divergence of `‖b‖ ^ 2 / 2` is `D(x, y) = ‖x - y‖ ^ 2 / 2`. -* `LMLExplore.strongConvexOn_norm_sq_div_two`: `‖b‖ ^ 2 / 2` is `1`-strongly convex on every - convex set. +* `LMLExplore.strongConvexOn_div_two_mul_norm_sub_sq`: `m / 2 * ‖b - c‖ ^ 2` is `m`-strongly + convex on every convex set; in particular `‖b‖ ^ 2 / 2` is `1`-strongly convex + (`LMLExplore.strongConvexOn_norm_sq_div_two`). -/ public section @@ -52,11 +53,23 @@ theorem bregDiv_norm_sq_div_two (x y : E) : rw [real_inner_comm] ring +/-- `m / 2 * ‖b - c‖ ^ 2` is `m`-strongly convex on every convex set, for every real `m` and every +center `c`. -/ +theorem strongConvexOn_div_two_mul_norm_sub_sq (hK : Convex ℝ K) (m : ℝ) (c : E) : + StrongConvexOn K m fun b : E ↦ m / 2 * ‖b - c‖ ^ 2 := by + refine strongConvexOn_iff_convex.mpr ?_ + -- `m / 2 * ‖b - c‖ ^ 2 - m / 2 * ‖b‖ ^ 2 = m / 2 * ‖c‖ ^ 2 - m * ⟪c, b⟫` is affine in `b` + convert (convexOn_const (m / 2 * ‖c‖ ^ 2) hK).add + (((-m) • innerSL ℝ c).toLinearMap.convexOn hK) using 1 + ext b + simp [norm_sub_sq_real, real_inner_comm b c] + ring + /-- `‖b‖ ^ 2 / 2` is `1`-strongly convex on every convex set. -/ theorem strongConvexOn_norm_sq_div_two (hK : Convex ℝ K) : StrongConvexOn K 1 fun b : E ↦ ‖b‖ ^ 2 / 2 := by - refine strongConvexOn_iff_convex.mpr ?_ - convert convexOn_const (0 : ℝ) hK using 2 with b + convert strongConvexOn_div_two_mul_norm_sub_sq hK 1 0 using 2 with b + rw [sub_zero] ring end LMLExplore diff --git a/LMLExplore/Analysis/Convex/Strong.lean b/LMLExplore/Analysis/Convex/Strong.lean index 8cefded0..f23a7bcd 100644 --- a/LMLExplore/Analysis/Convex/Strong.lean +++ b/LMLExplore/Analysis/Convex/Strong.lean @@ -39,6 +39,8 @@ with a strongly convex potential exist on closed sets that need not be bounded. * `StrongConvexOn.add`: [Ora, Theorem 4.6] the sum of an `m`-strongly convex and an `n`-strongly convex function is `(m + n)`-strongly convex. +* `StrongConvexOn.fun_sum`: a finite sum of `m i`-strongly convex functions is + `(∑ i, m i)`-strongly convex. * `UniformConvexOn.smul`, `StrongConvexOn.smul`: a nonnegative multiple `c • f` of a uniformly convex function with modulus `φ` is uniformly convex with modulus `c • φ`; of an `m`-strongly convex function, it is `(c * m)`-strongly convex. @@ -114,6 +116,19 @@ theorem smul {c : ℝ} (hc : 0 ≤ c) (hf : StrongConvexOn s m f) : (UniformConvexOn.smul hc hf).mono fun r ↦ le_of_eq (by simp only [Pi.smul_apply, smul_eq_mul]; ring) +/-- **Finite sums of strongly convex functions.** If each `f i`, for `i ∈ t`, is +`m i`-strongly convex on the convex set `s`, then `∑ i ∈ t, f i` is `(∑ i ∈ t, m i)`-strongly +convex on `s`. The moduli need not be nonnegative. -/ +theorem fun_sum {ι : Type*} {t : Finset ι} {m : ι → ℝ} {f : ι → E → ℝ} (hs : Convex ℝ s) + (hf : ∀ i ∈ t, StrongConvexOn s (m i) (f i)) : + StrongConvexOn s (∑ i ∈ t, m i) fun x ↦ ∑ i ∈ t, f i x := by + classical + induction t using Finset.induction_on with + | empty => simpa using strongConvexOn_zero.2 (convexOn_const 0 hs) + | insert i t hi ih => + simp only [Finset.sum_insert hi] + exact (hf i (Finset.mem_insert_self i t)).add (ih fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)) + /-- **The subgradient inequality of a strongly convex function** [Ora, Lemma 4.2]. If `f` is `m`-strongly convex on `s` and `g` is a subgradient of `f` within `s` at `x ∈ s`, then `f` lies above the paraboloid `f x + g (y - x) + m / 2 * ‖y - x‖ ^ 2` on `s`. The modulus `m` may diff --git a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean new file mode 100644 index 00000000..02d0faca --- /dev/null +++ b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean @@ -0,0 +1,214 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import LMLExplore.Analysis.Convex.Bregman.Euclidean +public import LMLExplore.NumberTheory.Harmonic.Bounds +public import LMLExplore.OnlineLearning.FTRL.Stability + +/-! +# FTRL-Proximal and follow-the-leader on quadratized losses + +On a real inner product space `E`, two algorithms of follow the regularized leader (FTRL) add to +their objectives quadratic terms `c / 2 * ‖a - x s‖ ^ 2` centered at their own past plays `x s`. + +* **FTRL-Proximal** [Ora, Example 7.9] plays at round `t` a minimizer over a set `V` of + `∑ s < t, (σ s / 2 * ‖a - x s‖ ^ 2 + ℓ s a)`, with weights `σ s ≥ 0` that may be chosen after + the loss of round `s`. Its regularizer `ψ t = ∑ s < t, σ s / 2 * ‖· - x s‖ ^ 2` is proximal: the + play `x t` minimizes the increment `ψ (t + 1) - ψ t = σ t / 2 * ‖· - x t‖ ^ 2`. For convex + losses with subgradients `g t` at the plays, its regret against every `u ∈ V` is at most + `∑ t < n, σ t / 2 * ‖u - x t‖ ^ 2 + ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, σ s)`. +* **Follow-the-leader on the quadratized losses** + `q t a = g t a + μ t / 2 * ‖a - x t‖ ^ 2` [Ora, Algorithm 7.5, (7.9)] has, for losses + that lie above these quadratics at the plays (strong convexity at the plays), the bound + `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` of follow-the-leader on strongly convex losses, while + each of its plays is a projection onto `V` of an explicit point: for `g s = ⟪v s, ·⟫`, the + minimizers over `V` of `∑ s < t, q s` are the points of `V` nearest to + `(∑ s < t, μ s)⁻¹ • ∑ s < t, (μ s • x s - v s)`. + +Follow-the-leader on the squared losses `(a - y t) ^ 2` of the guessing game on `[0, 1]`, which +are `2`-strongly convex, has regret at most `1 + log n` [Ora, Example 7.26], an improvement on the +bound `4 + 4 log n` of [Ora, Theorem 1.3]. + +## Main statements + +* `regret_le_ftrl_proximal`: [Ora, Example 7.9] the regret of FTRL-Proximal for convex losses. +* `regret_le_ftl_quadratized`: [Ora, Corollary 7.25, Algorithm 7.5] the regret of + follow-the-leader on the quadratized losses. +* `isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff`: the minimizers of a sum of quadratics + `⟪v i, ·⟫ + μ i / 2 * ‖· - x i‖ ^ 2` with positive total weight are the nearest points to an + explicit center; in particular the plays of follow-the-leader on the quadratized losses + [Ora, (7.9)]. +* `regret_sq_sub_le_one_add_log`: [Ora, Example 7.26] the regret of follow-the-leader on the + guessing game. + +## References + +* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, + arXiv:1912.13213v10, 2026, Theorem 1.3, Example 7.9, Corollary 7.25, Algorithm 7.5, (7.9), + Example 7.26. +-/ +public section + +open Finset +open scoped RealInnerProductSpace + +namespace LMLExplore.OnlineLearning + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {V : Set E} + +/-- **The regret of FTRL-Proximal** [Ora, Example 7.9]. Let the losses `ℓ t` be convex on `V`, and +let the weights `σ t ≥ 0` have positive partial sums `0 < ∑ s ≤ t, σ s`, for `t < n`. Let +`x t ∈ V` minimize over `V` the objective `∑ s < t, (σ s / 2 * ‖a - x s‖ ^ 2 + ℓ s a)`, so that +`x 0` is any point of `V`, and let `g t` be a subgradient of `ℓ t` within `V` at `x t`, for +`t < n`. Then for every `u ∈ V`, +`regret ℓ x u n ≤ ∑ t < n, σ t / 2 * ‖u - x t‖ ^ 2 + ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, σ s)`, +where `‖g t‖` is the dual norm. The weight `σ t` may depend on the losses up to round `t`. -/ +theorem regret_le_ftrl_proximal (ℓ : ℕ → E → ℝ) (x : ℕ → E) (g : ℕ → E →L[ℝ] ℝ) {σ : ℕ → ℝ} + {u : E} {n : ℕ} (hσ : ∀ t < n, 0 ≤ σ t) (hσ_sum : ∀ t < n, 0 < ∑ s ∈ range (t + 1), σ s) + (hℓ : ∀ t < n, ConvexOn ℝ V (ℓ t)) (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, + IsMinOn (fun a ↦ ∑ s ∈ range t, σ s / 2 * ‖a - x s‖ ^ 2 + ∑ s ∈ range t, ℓ s a) V (x t)) + (hg : ∀ t < n, HasSubgradientWithinAt (ℓ t) (g t) V (x t)) (hu : u ∈ V) : + regret ℓ x u n ≤ ∑ t ∈ range n, σ t / 2 * ‖u - x t‖ ^ 2 + + ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), σ s) := by + -- the proximal regularizers, and the plays up to round `n - 1` followed by the comparator + set ψ : ℕ → E → ℝ := fun t a ↦ ∑ s ∈ range t, σ s / 2 * ‖a - x s‖ ^ 2 with hψ_def + set x' : ℕ → E := fun t ↦ if t < n then x t else u with hx'_def + have hx'_lt (t : ℕ) (ht : t < n) : x' t = x t := by simp [x', ht] + have hx' (t : ℕ) (ht : t ≤ n) : x' t ∈ V := by + rcases ht.lt_or_eq with ht | rfl + · exact (hx'_lt t ht).symm ▸ hx t ht + · simpa [x'] using hu + -- `x t` minimizes the increment `ψ (t + 1) - ψ t = σ t / 2 * ‖· - x t‖ ^ 2` + have hprox (t : ℕ) (ht : t < n) : IsMinOn (fun a ↦ ψ (t + 1) a - ψ t a) V (x' t) := by + refine isMinOn_iff.mpr fun a _ ↦ ?_ + have := hσ t ht + simp only [hψ_def, sum_range_succ, add_sub_cancel_left, hx'_lt t ht, sub_self, norm_zero, + zero_pow two_ne_zero, mul_zero] + positivity + -- the objectives `F (t + 1)` are `∑ s ≤ t, σ s`-strongly convex + have hF (t : ℕ) (ht : t < n) : StrongConvexOn V (∑ s ∈ range (t + 1), σ s) + fun a ↦ ψ (t + 1) a + ∑ s ∈ range (t + 1), ℓ s a := by + have hV := (hℓ t ht).1 + have h := StrongConvexOn.fun_sum (t := range (t + 1)) (m := σ) + (f := fun s a ↦ σ s / 2 * ‖a - x s‖ ^ 2 + ℓ s a) hV fun s hs ↦ + (strongConvexOn_div_two_mul_norm_sub_sq hV (σ s) (x s)).add_convexOn + (hℓ s ((mem_range.mp hs).trans_le ht)) + simpa only [sum_add_distrib] using h + have h := regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn ψ ℓ x' g (u := u) hσ_sum hF hx' + (fun t ht ↦ by simpa [hx'_lt t ht] using hmin t ht) hprox + (fun t ht ↦ (hx'_lt t ht).symm ▸ hg t ht) (by simp [x']) + -- the increments of the regularizers vanish at the plays + have h_inc : ∑ t ∈ range n, (ψ t (x' t) - ψ (t + 1) (x' t)) = 0 := + sum_eq_zero fun t ht ↦ by simp [hψ_def, sum_range_succ, hx'_lt t (mem_range.mp ht)] + have h_pen : ψ n u = ∑ t ∈ range n, σ t / 2 * ‖u - x t‖ ^ 2 := rfl + rw [h_inc, add_zero, h_pen, regret_congr hx'_lt] at h + simpa [hψ_def] using h + +/-- **Follow-the-leader on quadratized losses** [Ora, Corollary 7.25, Algorithm 7.5]. Let the +weights `μ t ≥ 0` have positive partial sums `0 < ∑ s ≤ t, μ s`, and let each loss `ℓ t` lie +above the quadratic `ℓ t (x t) + g t (· - x t) + μ t / 2 * ‖· - x t‖ ^ 2` on `V` (for instance +if `ℓ t` is `μ t`-strongly convex on `V` and `g t` is a subgradient within `V` at `x t`), for +`t < n`. Let `x t ∈ V` minimize over `V` the cumulative quadratized loss +`∑ s < t, (g s a + μ s / 2 * ‖a - x s‖ ^ 2)`, so that `x 0` is any point of `V`. Then for every +`u ∈ V`, `regret ℓ x u n ≤ ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)`, where `‖g t‖` is the dual +norm. This is the bound of follow-the-leader on the losses `ℓ t` +(`regret_le_ftl_of_strongConvexOn`), with plays that are projections of explicit points +(`isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff`). -/ +theorem regret_le_ftl_quadratized (hV : Convex ℝ V) (ℓ : ℕ → E → ℝ) (x : ℕ → E) + (g : ℕ → E →L[ℝ] ℝ) {μ : ℕ → ℝ} {u : E} {n : ℕ} (hμ : ∀ t < n, 0 ≤ μ t) + (hμ_sum : ∀ t < n, 0 < ∑ s ∈ range (t + 1), μ s) + (hℓ : ∀ t < n, ∀ a ∈ V, ℓ t (x t) + g t (a - x t) + μ t / 2 * ‖a - x t‖ ^ 2 ≤ ℓ t a) + (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ∑ s ∈ range t, (g s a + μ s / 2 * ‖a - x s‖ ^ 2)) V (x t)) + (hu : u ∈ V) : + regret ℓ x u n ≤ ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), μ s) := by + -- the quadratized losses + set ℓ' : ℕ → E → ℝ := fun t a ↦ g t a + μ t / 2 * ‖a - x t‖ ^ 2 with hℓ'_def + -- `g t` is a subgradient of the `μ t`-strongly convex `ℓ' t` at `x t` + have hg (t : ℕ) (ht : t < n) : HasSubgradientWithinAt (ℓ' t) (g t) V (x t) := by + refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ + simp only [hℓ'_def, sub_self, norm_zero, map_sub] + have := hμ t ht + nlinarith [sq_nonneg ‖a - x t‖] + have hℓ' (t : ℕ) (_ : t < n) : StrongConvexOn V (μ t) (ℓ' t) := by + convert (strongConvexOn_div_two_mul_norm_sub_sq hV (μ t) (x t)).add_convexOn + ((g t).toLinearMap.convexOn hV) using 1 + ext a + simp [hℓ'_def, add_comm] + have h := regret_le_ftl_of_strongConvexOn ℓ' x g hℓ' hμ_sum hx hmin hg hu + -- the regret of the losses is at most that of the quadratized losses + refine le_trans ?_ h + simp only [regret_def] + refine sum_le_sum fun t ht ↦ ?_ + have h_le := hℓ t (mem_range.mp ht) u hu + simp only [hℓ'_def, sub_self, norm_zero, map_sub] at h_le ⊢ + nlinarith + +/-- **The minimizers of a sum of quadratics** [Ora, (7.9)]. For weights `μ i` with positive +sum `M = ∑ i ∈ t, μ i`, centers `x i` and linear terms `⟪v i, ·⟫`, the minimizers over any set `V` +of `∑ i ∈ t, (⟪v i, a⟫ + μ i / 2 * ‖a - x i‖ ^ 2)` are its points nearest to +`M⁻¹ • ∑ i ∈ t, (μ i • x i - v i)`. The individual weights may be negative. With +`g s = ⟪v s, ·⟫`, the plays of follow-the-leader on the quadratized losses of +`regret_le_ftl_quadratized` are thus the projections onto `V` of +`(∑ s < t, μ s)⁻¹ • ∑ s < t, (μ s • x s - v s)`. -/ +theorem isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff {ι : Type*} (t : Finset ι) + (v x : ι → E) {μ : ι → ℝ} (hμ : 0 < ∑ i ∈ t, μ i) (V : Set E) (a : E) : + IsMinOn (fun b ↦ ∑ i ∈ t, (⟪v i, b⟫ + μ i / 2 * ‖b - x i‖ ^ 2)) V a ↔ + IsMinOn (fun b ↦ ‖b - (∑ i ∈ t, μ i)⁻¹ • ∑ i ∈ t, (μ i • x i - v i)‖) V a := by + set M := ∑ i ∈ t, μ i with hM + set c := M⁻¹ • ∑ i ∈ t, (μ i • x i - v i) with hc + -- completing the square: the objective is `M / 2 * ‖b - c‖ ^ 2` plus a constant + have h_sq (b : E) : ∑ i ∈ t, (⟪v i, b⟫ + μ i / 2 * ‖b - x i‖ ^ 2) = + M / 2 * ‖b - c‖ ^ 2 + (∑ i ∈ t, μ i / 2 * ‖x i‖ ^ 2 - M / 2 * ‖c‖ ^ 2) := by + have h_inner : M * ⟪b, c⟫ = ∑ i ∈ t, (μ i * ⟪b, x i⟫ - ⟪v i, b⟫) := by + rw [hc, inner_smul_right, ← mul_assoc, mul_inv_cancel₀ hμ.ne', one_mul, inner_sum] + exact sum_congr rfl fun i _ ↦ by + rw [inner_sub_right, inner_smul_right, real_inner_comm (v i) b] + have h_lin : ∑ i ∈ t, μ i / 2 * (2 * ⟪b, x i⟫) = ∑ i ∈ t, μ i * ⟪b, x i⟫ := + sum_congr rfl fun i _ ↦ by ring + rw [sum_sub_distrib] at h_inner + simp only [norm_sub_sq_real, mul_add, mul_sub, sum_add_distrib, sum_sub_distrib, ← sum_mul, + ← sum_div, ← hM] + linear_combination (-1 : ℝ) * h_lin + h_inner + simp only [isMinOn_iff, h_sq, add_le_add_iff_right] + refine forall₂_congr fun b _ ↦ ?_ + rw [mul_le_mul_iff_of_pos_left (half_pos hμ), sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] + +/-- **Follow-the-leader on the guessing game** [Ora, Example 7.26]. Let the outcomes `y t` and the +plays `x t` lie in `[0, 1]`, and let `x t` minimize over `[0, 1]` the cumulative squared loss +`∑ s < t, (a - y s) ^ 2` of the previous rounds, so that `x 0` is any point of `[0, 1]`, for +`t < n`. Then the regret of the squared losses against every `u ∈ [0, 1]` is at most `1 + log n`. +This improves the bound `4 + 4 log n` of [Ora, Theorem 1.3]. -/ +theorem regret_sq_sub_le_one_add_log (x y : ℕ → ℝ) {u : ℝ} {n : ℕ} + (hy : ∀ t < n, y t ∈ Set.Icc 0 1) (hx : ∀ t < n, x t ∈ Set.Icc 0 1) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ∑ s ∈ range t, (a - y s) ^ 2) (Set.Icc 0 1) (x t)) + (hu : u ∈ Set.Icc 0 1) : + regret (fun t a ↦ (a - y t) ^ 2) x u n ≤ 1 + Real.log n := by + -- the squared losses are `2`-strongly convex, with derivative `2 (x t - y t)` at `x t` + have hℓ (t : ℕ) (_ : t < n) : StrongConvexOn (Set.Icc (0 : ℝ) 1) 2 fun a ↦ (a - y t) ^ 2 := by + convert strongConvexOn_div_two_mul_norm_sub_sq (convex_Icc (0 : ℝ) 1) 2 (y t) using 2 with a + rw [Real.norm_eq_abs, sq_abs] + ring + have hg (t : ℕ) (_ : t < n) : HasSubgradientWithinAt (fun a ↦ (a - y t) ^ 2) + (ContinuousLinearMap.toSpanSingleton ℝ (2 * (x t - y t))) (Set.Icc 0 1) (x t) := by + refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ + simp only [ContinuousLinearMap.toSpanSingleton_apply, smul_eq_mul] + nlinarith [sq_nonneg (a - x t)] + have h := regret_le_ftl_of_strongConvexOn (fun t a ↦ (a - y t) ^ 2) x _ hℓ + (fun t _ ↦ by simp only [sum_const, card_range, nsmul_eq_mul]; positivity) hx hmin hg hu + refine h.trans ((sum_le_sum fun t ht ↦ ?_).trans (Real.sum_range_inv_add_one_le n)) + -- each stability term is `(x t - y t) ^ 2 / (t + 1) ≤ 1 / (t + 1)` + have ht := mem_range.mp ht + have h_sq : (x t - y t) ^ 2 ≤ 1 := by + nlinarith [(hx t ht).1, (hx t ht).2, (hy t ht).1, (hy t ht).2] + simp only [ContinuousLinearMap.norm_toSpanSingleton, Real.norm_eq_abs, sum_const, card_range, + nsmul_eq_mul, Nat.cast_add, Nat.cast_one] + rw [sq_abs, inv_eq_one_div, div_le_div_iff₀ (by positivity) (by positivity)] + nlinarith + +end LMLExplore.OnlineLearning diff --git a/LMLExplore/OnlineLearning/FTRL/Stability.lean b/LMLExplore/OnlineLearning/FTRL/Stability.lean index 3bbbaf2b..557c3a7e 100644 --- a/LMLExplore/OnlineLearning/FTRL/Stability.lean +++ b/LMLExplore/OnlineLearning/FTRL/Stability.lean @@ -40,6 +40,9 @@ subgradient of `ℓ t` within `V` at `x t` and `F t + ℓ t` is `λ t`-strongly minimizes `F n` over `V`), `regret ≤ ψ n u - ψ 0 (x 0) + ∑ t < n, ‖g t‖ ^ 2 / (2 λ t) + ∑ t < n, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1)))`. +With proximal regularizers the increments are evaluated at `x t` instead, and with no regularizer, +follow-the-leader on losses whose partial sums `∑ s ≤ t, ℓ s` are strongly convex has regret at +most `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` [Ora, Corollary 7.25]. ## Main statements @@ -56,11 +59,15 @@ minimizes `F n` over `V`), * `regret_le_ftrl_of_strongConvexOn_div`: [Ora, Corollary 7.6] its case of the regularizers `F / η t`, for an `m`-strongly convex `F`, convex losses and arbitrary positive learning rates, keeping the increments `(1 / η t - 1 / η (t + 1)) * F (x (t + 1))` of the regularizers. +* `regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn`: [Ora, Lemmas 7.1 and 7.7] the regret of FTRL + with proximal regularizers. +* `regret_le_ftl_of_strongConvexOn`: [Ora, Corollary 7.25] the regret of follow-the-leader on + strongly convex losses. ## References * [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, - arXiv:1912.13213v10, 2026, Lemmas 7.5 and 7.7, Corollary 7.6. + arXiv:1912.13213v10, 2026, Lemmas 7.5 and 7.7, Corollaries 7.6 and 7.25. -/ public section @@ -250,6 +257,65 @@ theorem regret_le_ftrl_of_strongConvexOn_div {F : E → ℝ} {m : ℝ} (hF : Str (1 / η t - 1 / η (t + 1)) * F (x (t + 1)) := fun _ _ ↦ by ring rwa [sum_congr rfl h_stab, sum_congr rfl h_inc] at h +/-- **The regret of FTRL with proximal regularizers** [Ora, Lemmas 7.1 and 7.7]. Let `x t ∈ V`, +for `t ≤ n`, and let `x t`, for `t < n`, minimize over `V` both the objective +`F t = ψ t + ∑ s < t, ℓ s` and the increment `ψ (t + 1) - ψ t` of the regularizers. Let `g t` be +a subgradient of `ℓ t` within `V` at `x t` and let `F (t + 1)` be `lam t`-strongly convex on `V`, +with `lam t > 0`, for `t < n`. If the last point does at least as well as the comparator `u` on +the last objective, `F n (x n) ≤ F n u`, then +`regret ℓ x u n ≤ ψ n u - ψ 0 (x 0) + ∑ t < n, ‖g t‖ ^ 2 / (2 lam t) + + ∑ t < n, (ψ t (x t) - ψ (t + 1) (x t))`, +where `‖g t‖` is the dual norm. Only the objectives `F (t + 1)` must be strongly convex, and the +regularizer increments are evaluated at the plays `x t` themselves. -/ +theorem regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn (ψ ℓ : ℕ → E → ℝ) (x : ℕ → E) + (g : ℕ → E →L[ℝ] ℝ) {lam : ℕ → ℝ} {u : E} {n : ℕ} (hlam : ∀ t < n, 0 < lam t) + (hF : ∀ t < n, StrongConvexOn V (lam t) fun a ↦ ψ (t + 1) a + ∑ s ∈ range (t + 1), ℓ s a) + (hx : ∀ t ≤ n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, ℓ s a) V (x t)) + (hprox : ∀ t < n, IsMinOn (fun a ↦ ψ (t + 1) a - ψ t a) V (x t)) + (hg : ∀ t < n, HasSubgradientWithinAt (ℓ t) (g t) V (x t)) + (hxn : ψ n (x n) + ∑ s ∈ range n, ℓ s (x n) ≤ ψ n u + ∑ s ∈ range n, ℓ s u) : + regret ℓ x u n ≤ ψ n u - ψ 0 (x 0) + ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * lam t) + + ∑ t ∈ range n, (ψ t (x t) - ψ (t + 1) (x t)) := by + refine (regret_le_ftrl ψ ℓ x x hxn).trans ?_ + rw [add_assoc, ← sum_add_distrib] + -- bound each stability term, with the comparison point `x (t + 1)` + refine add_le_add le_rfl (sum_le_sum fun t ht ↦ ?_) + have ht := mem_range.mp ht + have h := ftrl_stability_le_norm_sq_div_of_isMinOn_sub_of_strongConvexOn (hlam t ht) (hmin t ht) + (hprox t ht) (hg t ht) (hF t ht) (hx t ht.le) (hx (t + 1) ht) + linarith + +/-- **Follow-the-leader on strongly convex losses** [Ora, Corollary 7.25]. Let each loss `ℓ t` be +`μ t`-strongly convex on `V`, with positive partial sums `0 < ∑ s ≤ t, μ s`, for `t < n`. Let +`x t ∈ V` minimize over `V` the cumulative loss `∑ s < t, ℓ s` of the previous rounds, so that +`x 0` is any point of `V`, and let `g t` be a subgradient of `ℓ t` within `V` at `x t`, for +`t < n`. Then for every `u ∈ V`, +`regret ℓ x u n ≤ ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)`, +where `‖g t‖` is the dual norm. The moduli `μ t` themselves may be negative. -/ +theorem regret_le_ftl_of_strongConvexOn (ℓ : ℕ → E → ℝ) (x : ℕ → E) (g : ℕ → E →L[ℝ] ℝ) + {μ : ℕ → ℝ} {u : E} {n : ℕ} (hℓ : ∀ t < n, StrongConvexOn V (μ t) (ℓ t)) + (hμ : ∀ t < n, 0 < ∑ s ∈ range (t + 1), μ s) (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ∑ s ∈ range t, ℓ s a) V (x t)) + (hg : ∀ t < n, HasSubgradientWithinAt (ℓ t) (g t) V (x t)) (hu : u ∈ V) : + regret ℓ x u n ≤ ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), μ s) := by + -- the plays up to round `n - 1`, then the comparator + set x' : ℕ → E := fun t ↦ if t < n then x t else u with hx'_def + have hx'_lt (t : ℕ) (ht : t < n) : x' t = x t := by simp [x', ht] + have hx' (t : ℕ) (ht : t ≤ n) : x' t ∈ V := by + rcases ht.lt_or_eq with ht | rfl + · exact (hx'_lt t ht).symm ▸ hx t ht + · simpa [x'] using hu + -- the cumulative losses up to round `t` are `∑ s ≤ t, μ s`-strongly convex + have hF (t : ℕ) (ht : t < n) : + StrongConvexOn V (∑ s ∈ range (t + 1), μ s) fun a ↦ 0 + ∑ s ∈ range (t + 1), ℓ s a := by + simpa using StrongConvexOn.fun_sum (hℓ t ht).1 fun s hs ↦ + hℓ s ((mem_range.mp hs).trans_le ht) + have h := regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn (fun _ _ ↦ 0) ℓ x' g (u := u) hμ hF + hx' (fun t ht ↦ by simpa [hx'_lt t ht] using hmin t ht) (fun t _ ↦ isMinOn_const) + (fun t ht ↦ (hx'_lt t ht).symm ▸ hg t ht) (by simp [x']) + simpa [regret_congr hx'_lt] using h + end NormedSpace section InnerProductSpace diff --git a/LMLExplore/OnlineLearning/Regret.lean b/LMLExplore/OnlineLearning/Regret.lean index 63ed9e70..08076a7a 100644 --- a/LMLExplore/OnlineLearning/Regret.lean +++ b/LMLExplore/OnlineLearning/Regret.lean @@ -106,6 +106,12 @@ lemma regret_succ (ℓ : ℕ → α → ℝ) (x : ℕ → α) (u : α) (n : ℕ) regret ℓ x u (n + 1) = regret ℓ x u n + (ℓ n (x n) - ℓ n u) := by rw [regret_def, regret_def, sum_range_succ] +/-- The regret after `n` rounds depends only on the plays of the first `n` rounds. -/ +lemma regret_congr {y : ℕ → α} (h : ∀ t < n, x t = y t) : + regret ℓ x u n = regret ℓ y u n := by + simp only [regret_def] + exact sum_congr rfl fun t ht ↦ by rw [h t (mem_range.mp ht)] + /-- The regret against a comparator is the difference of the cumulative losses. -/ lemma regret_eq_sum_sub_sum (ℓ : ℕ → α → ℝ) (x : ℕ → α) (u : α) (n : ℕ) : regret ℓ x u n = ∑ t ∈ range n, ℓ t (x t) - ∑ t ∈ range n, ℓ t u := by From 78c1a709c3cd896e148c93ac9c8d3b8850d7db4d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 04:09:21 +0100 Subject: [PATCH 2/2] refactor: derive FTRL-Proximal from follow-the-leader on strongly convex losses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Prove regret_le_ftrl_proximal from regret_le_ftl_of_strongConvexOn applied to the losses σ t / 2 * ‖· - x t‖ ^ 2 + ℓ t, removing the duplicated padding of the plays. Fix the Stability module docstring's statement of the follow-the-leader bound and its references. Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/FTRL/Quadratic.lean | 55 ++++++++----------- LMLExplore/OnlineLearning/FTRL/Stability.lean | 7 ++- 2 files changed, 26 insertions(+), 36 deletions(-) diff --git a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean index 02d0faca..99747a66 100644 --- a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean +++ b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean @@ -66,7 +66,9 @@ let the weights `σ t ≥ 0` have positive partial sums `0 < ∑ s ≤ t, σ s`, `x 0` is any point of `V`, and let `g t` be a subgradient of `ℓ t` within `V` at `x t`, for `t < n`. Then for every `u ∈ V`, `regret ℓ x u n ≤ ∑ t < n, σ t / 2 * ‖u - x t‖ ^ 2 + ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, σ s)`, -where `‖g t‖` is the dual norm. The weight `σ t` may depend on the losses up to round `t`. -/ +where `‖g t‖` is the dual norm. The weight `σ t` may depend on the losses up to round `t`. +FTRL-Proximal is follow-the-leader on the `σ t`-strongly convex losses +`σ t / 2 * ‖· - x t‖ ^ 2 + ℓ t`, and the bound follows from `regret_le_ftl_of_strongConvexOn`. -/ theorem regret_le_ftrl_proximal (ℓ : ℕ → E → ℝ) (x : ℕ → E) (g : ℕ → E →L[ℝ] ℝ) {σ : ℕ → ℝ} {u : E} {n : ℕ} (hσ : ∀ t < n, 0 ≤ σ t) (hσ_sum : ∀ t < n, 0 < ∑ s ∈ range (t + 1), σ s) (hℓ : ∀ t < n, ConvexOn ℝ V (ℓ t)) (hx : ∀ t < n, x t ∈ V) @@ -75,39 +77,26 @@ theorem regret_le_ftrl_proximal (ℓ : ℕ → E → ℝ) (x : ℕ → E) (g : (hg : ∀ t < n, HasSubgradientWithinAt (ℓ t) (g t) V (x t)) (hu : u ∈ V) : regret ℓ x u n ≤ ∑ t ∈ range n, σ t / 2 * ‖u - x t‖ ^ 2 + ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), σ s) := by - -- the proximal regularizers, and the plays up to round `n - 1` followed by the comparator - set ψ : ℕ → E → ℝ := fun t a ↦ ∑ s ∈ range t, σ s / 2 * ‖a - x s‖ ^ 2 with hψ_def - set x' : ℕ → E := fun t ↦ if t < n then x t else u with hx'_def - have hx'_lt (t : ℕ) (ht : t < n) : x' t = x t := by simp [x', ht] - have hx' (t : ℕ) (ht : t ≤ n) : x' t ∈ V := by - rcases ht.lt_or_eq with ht | rfl - · exact (hx'_lt t ht).symm ▸ hx t ht - · simpa [x'] using hu - -- `x t` minimizes the increment `ψ (t + 1) - ψ t = σ t / 2 * ‖· - x t‖ ^ 2` - have hprox (t : ℕ) (ht : t < n) : IsMinOn (fun a ↦ ψ (t + 1) a - ψ t a) V (x' t) := by - refine isMinOn_iff.mpr fun a _ ↦ ?_ + -- FTRL-Proximal is follow-the-leader on the `σ t`-strongly convex losses + -- `ℓ' t = σ t / 2 * ‖· - x t‖ ^ 2 + ℓ t` + set ℓ' : ℕ → E → ℝ := fun t a ↦ σ t / 2 * ‖a - x t‖ ^ 2 + ℓ t a with hℓ'_def + have hℓ' (t : ℕ) (ht : t < n) : StrongConvexOn V (σ t) (ℓ' t) := + (strongConvexOn_div_two_mul_norm_sub_sq (hℓ t ht).1 (σ t) (x t)).add_convexOn (hℓ t ht) + -- `g t` is a subgradient of `ℓ' t` at `x t`, where the quadratic is nonnegative and vanishes + have hg' (t : ℕ) (ht : t < n) : HasSubgradientWithinAt (ℓ' t) (g t) V (x t) := by + refine hasSubgradientWithinAt_iff_le.mpr fun a ha ↦ ?_ + have h := hasSubgradientWithinAt_iff_le.mp (hg t ht) a ha have := hσ t ht - simp only [hψ_def, sum_range_succ, add_sub_cancel_left, hx'_lt t ht, sub_self, norm_zero, - zero_pow two_ne_zero, mul_zero] - positivity - -- the objectives `F (t + 1)` are `∑ s ≤ t, σ s`-strongly convex - have hF (t : ℕ) (ht : t < n) : StrongConvexOn V (∑ s ∈ range (t + 1), σ s) - fun a ↦ ψ (t + 1) a + ∑ s ∈ range (t + 1), ℓ s a := by - have hV := (hℓ t ht).1 - have h := StrongConvexOn.fun_sum (t := range (t + 1)) (m := σ) - (f := fun s a ↦ σ s / 2 * ‖a - x s‖ ^ 2 + ℓ s a) hV fun s hs ↦ - (strongConvexOn_div_two_mul_norm_sub_sq hV (σ s) (x s)).add_convexOn - (hℓ s ((mem_range.mp hs).trans_le ht)) - simpa only [sum_add_distrib] using h - have h := regret_le_ftrl_of_isMinOn_sub_of_strongConvexOn ψ ℓ x' g (u := u) hσ_sum hF hx' - (fun t ht ↦ by simpa [hx'_lt t ht] using hmin t ht) hprox - (fun t ht ↦ (hx'_lt t ht).symm ▸ hg t ht) (by simp [x']) - -- the increments of the regularizers vanish at the plays - have h_inc : ∑ t ∈ range n, (ψ t (x' t) - ψ (t + 1) (x' t)) = 0 := - sum_eq_zero fun t ht ↦ by simp [hψ_def, sum_range_succ, hx'_lt t (mem_range.mp ht)] - have h_pen : ψ n u = ∑ t ∈ range n, σ t / 2 * ‖u - x t‖ ^ 2 := rfl - rw [h_inc, add_zero, h_pen, regret_congr hx'_lt] at h - simpa [hψ_def] using h + simp only [hℓ'_def, sub_self, norm_zero, zero_pow two_ne_zero, mul_zero, zero_add] + nlinarith [sq_nonneg ‖a - x t‖] + have h := regret_le_ftl_of_strongConvexOn ℓ' x g hℓ' hσ_sum hx + (fun t ht ↦ by simpa only [hℓ'_def, sum_add_distrib] using hmin t ht) hg' hu + -- the regret of `ℓ'` is that of `ℓ` minus the quadratic terms at the comparator + have h_reg : regret ℓ' x u n = regret ℓ x u n - ∑ t ∈ range n, σ t / 2 * ‖u - x t‖ ^ 2 := by + simp only [regret_def, hℓ'_def, sub_self, norm_zero, zero_pow two_ne_zero, mul_zero, + zero_add, ← sum_sub_distrib] + exact sum_congr rfl fun _ _ ↦ by ring + linarith /-- **Follow-the-leader on quadratized losses** [Ora, Corollary 7.25, Algorithm 7.5]. Let the weights `μ t ≥ 0` have positive partial sums `0 < ∑ s ≤ t, μ s`, and let each loss `ℓ t` lie diff --git a/LMLExplore/OnlineLearning/FTRL/Stability.lean b/LMLExplore/OnlineLearning/FTRL/Stability.lean index 557c3a7e..8abbbb01 100644 --- a/LMLExplore/OnlineLearning/FTRL/Stability.lean +++ b/LMLExplore/OnlineLearning/FTRL/Stability.lean @@ -41,8 +41,9 @@ minimizes `F n` over `V`), `regret ≤ ψ n u - ψ 0 (x 0) + ∑ t < n, ‖g t‖ ^ 2 / (2 λ t) + ∑ t < n, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1)))`. With proximal regularizers the increments are evaluated at `x t` instead, and with no regularizer, -follow-the-leader on losses whose partial sums `∑ s ≤ t, ℓ s` are strongly convex has regret at -most `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` [Ora, Corollary 7.25]. +follow-the-leader on `μ t`-strongly convex losses `ℓ t` whose moduli have positive partial sums +`0 < ∑ s ≤ t, μ s` has regret at most `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` +[Ora, Corollary 7.25]. ## Main statements @@ -67,7 +68,7 @@ most `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` [Ora, Corollary 7.25]. ## References * [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, - arXiv:1912.13213v10, 2026, Lemmas 7.5 and 7.7, Corollaries 7.6 and 7.25. + arXiv:1912.13213v10, 2026, Lemmas 7.1, 7.5 and 7.7, Corollaries 7.6 and 7.25. -/ public section