From 279e1f9e911d82d042071cd98e8e6d31909d2de5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 09:51:10 +0100 Subject: [PATCH 1/3] feat: online subgradient descent on unbounded sets and on strongly convex losses Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/MirrorDescent.lean | 55 ++- .../OnlineLearning/SubgradientDescent.lean | 312 ++++++++++++++++-- 2 files changed, 329 insertions(+), 38 deletions(-) diff --git a/LMLExplore/OnlineLearning/MirrorDescent.lean b/LMLExplore/OnlineLearning/MirrorDescent.lean index abcf1300..e14ba9cd 100644 --- a/LMLExplore/OnlineLearning/MirrorDescent.lean +++ b/LMLExplore/OnlineLearning/MirrorDescent.lean @@ -63,8 +63,11 @@ of losses, in particular for losses chosen adaptively from the past plays. `d 0 / η 0 + ∑ t < n - 1, (1 / η (t + 1) - 1 / η t) * d (t + 1) - d n / η (n - 1) + ∑ t < n, (y t (a t - a (t + 1)) - D_F(a (t + 1), a t) / η t)`. Every regret bound below is derived from it. -* `mirrorDescent_regret_le_of_antitone`: with nonincreasing learning rates `η t` and divergences - `D_F(u, a t) ≤ D`, the regret is at most +* `sum_apply_sub_le_mirrorDescent_of_antitone`: with nonincreasing learning rates `η t` and + divergences `D_F(u, a t) ≤ D` for `t < n`, the regret is at most + `(D - D_F(u, a n)) / η (n - 1) + ∑ t < n, (y t (a t - a (t + 1)) - D_F(a (t + 1), a t) / η t)`, + for any initial play and any potential. +* `mirrorDescent_regret_le_of_antitone`: for a convex potential, the regret is at most `D / η (n - 1) + ∑ t < n, (y t (a t - a (t + 1)) - D_F(a (t + 1), a t) / η t)`. * `mirrorDescent_regret_le_of_strongConvexOn_of_antitone`: [Ora, Theorem 6.11], its form `D / η (n - 1) + ∑ t < n, η t / (2 m) * ‖y t‖ ^ 2` for an `m`-strongly convex potential. @@ -417,6 +420,37 @@ section Antitone variable {η : ℕ → ℝ} +/-- **Regret of mirror descent with nonincreasing learning rates, keeping the last divergence.** +Let `K` be convex and let the learning rates `η t > 0` be nonincreasing. Let each `a (t + 1)`, for +`t < n`, be a mirror descent step on `K` from `a t` with derivative `F' t` and learning rate `η t`, +for the loss `y t`, where `F` has derivative `F' (t + 1)` within `K` at `a (t + 1)`. If `n > 0` +and `D` bounds the Bregman divergences `d t = D_F(u, a t)` for `t < n`, then for every `u ∈ K`, +`∑ t < n, y t (a t - u) + ≤ (D - d n) / η (n - 1) + ∑ t < n, (y t (a t - a (t + 1)) - D_F(a (t + 1), a t) / η t)`. +Neither the convexity of `F` nor `a 0 ∈ K` is needed. -/ +theorem sum_apply_sub_le_mirrorDescent_of_antitone (hK : Convex ℝ K) (hη : ∀ t, 0 < η t) + (hη_anti : Antitone η) (y : ℕ → E →L[ℝ] ℝ) (a : ℕ → E) (F' : ℕ → E →L[ℝ] ℝ) + (ha : ∀ t < n, IsMirrorDescentStep K F (η t) (y t) (a t) (F' t) (a (t + 1))) + (hF' : ∀ t < n, HasFDerivWithinAt F (F' (t + 1)) K (a (t + 1))) (hn : 0 < n) {D : ℝ} + (hDu : ∀ t < n, bregDiv F u (a t) (F' t) ≤ D) (hu : u ∈ K) : + ∑ t ∈ range n, y t (a t - u) ≤ (D - bregDiv F u (a n) (F' n)) / η (n - 1) + + ∑ t ∈ range n, (y t (a t - a (t + 1)) - bregDiv F (a (t + 1)) (a t) (F' t) / η t) := by + have h := sum_apply_sub_le_mirrorDescent hK (fun t _ ↦ hη t) y a F' ha hF' hu + -- with nonincreasing rates, the coefficients `1 / η (t + 1) - 1 / η t` are nonnegative, and the + -- divergences they weigh are at most `D` + have h_sum : ∑ t ∈ range (n - 1), ((η (t + 1))⁻¹ - (η t)⁻¹) * bregDiv F u (a (t + 1)) (F' (t + 1)) + ≤ D * ((η (n - 1))⁻¹ - (η 0)⁻¹) := by + rw [← sum_range_sub (fun t ↦ (η t)⁻¹), mul_sum] + refine sum_le_sum fun t ht ↦ ?_ + rw [mul_comm D] + exact mul_le_mul_of_nonneg_left (hDu (t + 1) (by have := mem_range.mp ht; omega)) + (sub_nonneg.mpr (inv_anti₀ (hη (t + 1)) (hη_anti t.le_succ))) + have h_init : bregDiv F u (a 0) (F' 0) / η 0 ≤ D / η 0 := + div_le_div_of_nonneg_right (hDu 0 hn) (hη 0).le + have h_eq : D / η 0 + D * ((η (n - 1))⁻¹ - (η 0)⁻¹) = D / η (n - 1) := by ring + rw [sub_div] + linarith + /-- **Regret of mirror descent with nonincreasing learning rates**, before the use of strong convexity [Ora, Theorem 6.11]. Let `F` be convex on `K` and let the learning rates `η t > 0` be nonincreasing. Let `a 0 ∈ K` and let each `a (t + 1)`, for `t < n`, be a mirror descent step on @@ -435,24 +469,13 @@ theorem mirrorDescent_regret_le_of_antitone (hF : ConvexOn ℝ K F) (hη : ∀ t ∑ t ∈ range n, (y t (a t - a (t + 1)) - bregDiv F (a (t + 1)) (a t) (F' t) / η t) := by rcases n.eq_zero_or_pos with rfl | hn · simpa using div_nonneg hD (hη _).le - have h := sum_apply_sub_le_mirrorDescent hF.1 (fun t _ ↦ hη t) y a F' ha - (fun t ht ↦ hF' (t + 1) ht) hu + have h := sum_apply_sub_le_mirrorDescent_of_antitone hF.1 hη hη_anti y a F' ha + (fun t ht ↦ hF' (t + 1) ht) hn hDu hu -- the last divergence `D_F(u, a n)` is nonnegative by convexity have h_last : 0 ≤ bregDiv F u (a n) (F' n) / η (n - 1) := div_nonneg ((hF' n le_rfl).hasSubgradientWithinAt hF (mem_of_isMirrorDescentStep ha0K ha n le_rfl) u hu) (hη _).le - -- with nonincreasing rates, the coefficients `1 / η (t + 1) - 1 / η t` are nonnegative, and the - -- divergences they weigh are at most `D` - have h_sum : ∑ t ∈ range (n - 1), ((η (t + 1))⁻¹ - (η t)⁻¹) * bregDiv F u (a (t + 1)) (F' (t + 1)) - ≤ D * ((η (n - 1))⁻¹ - (η 0)⁻¹) := by - rw [← sum_range_sub (fun t ↦ (η t)⁻¹), mul_sum] - refine sum_le_sum fun t ht ↦ ?_ - rw [mul_comm D] - exact mul_le_mul_of_nonneg_left (hDu (t + 1) (by have := mem_range.mp ht; omega)) - (sub_nonneg.mpr (inv_anti₀ (hη (t + 1)) (hη_anti t.le_succ))) - have h_init : bregDiv F u (a 0) (F' 0) / η 0 ≤ D / η 0 := - div_le_div_of_nonneg_right (hDu 0 hn) (hη 0).le - have h_eq : D / η 0 + D * ((η (n - 1))⁻¹ - (η 0)⁻¹) = D / η (n - 1) := by ring + rw [sub_div] at h linarith /-- **Regret of mirror descent with nonincreasing learning rates and a strongly convex potential** diff --git a/LMLExplore/OnlineLearning/SubgradientDescent.lean b/LMLExplore/OnlineLearning/SubgradientDescent.lean index 9c5a6cbf..89e06935 100644 --- a/LMLExplore/OnlineLearning/SubgradientDescent.lean +++ b/LMLExplore/OnlineLearning/SubgradientDescent.lean @@ -6,7 +6,9 @@ Authors: LMLExplore contributors module public import LMLExplore.Analysis.Real.Sqrt +public import LMLExplore.NumberTheory.Harmonic.Bounds public import LMLExplore.OnlineLearning.MirrorDescent +public import LMLExplore.OnlineLearning.Regret /-! # Online convex optimization and projected online subgradient descent @@ -20,10 +22,22 @@ plays therefore apply to convex losses, run on the linearized losses. On a real inner product space, mirror descent with the potential `‖b‖ ^ 2 / 2` is **projected online subgradient descent** [Zin03; Ora, Section 2.2]: the next play is the point of `K` nearest -to the gradient step `a t - η t • g t`. With a nonincreasing learning rate, its regret on a set of -diameter at most `D`, for subgradients of norm at most `G`, is at most -`D ^ 2 / (2 η (n - 1)) + ∑ t < n, η t / 2 * ‖g t‖ ^ 2`, and the anytime learning rate -`η t = D / (G √(t + 1))` gives the bound `3 / 2 * D * G * √n` for every horizon `n`. +to the gradient step `a t - η t • g t`. Each such step satisfies +`⟪g t, a t - u⟫ ≤ (‖u - a t‖ ^ 2 - ‖u - a (t + 1)‖ ^ 2) / (2 η t) + η t / 2 * ‖g t‖ ^ 2` +[Ora, Lemma 2.12], so that: + +* with a constant learning rate `η`, the regret against `u` is at most + `(‖u - a 0‖ ^ 2 - ‖u - a n‖ ^ 2) / (2 η) + η / 2 * ∑ t < n, ‖g t‖ ^ 2`, on any convex set, bounded + or not [Ora, Theorem 2.13]; +* with nonincreasing learning rates and plays at distance at most `D` from `u`, it is at most + `(D ^ 2 - ‖u - a n‖ ^ 2) / (2 η (n - 1)) + ∑ t < n, η t / 2 * ‖g t‖ ^ 2`, and the anytime + learning rate `η t = D / (G √(t + 1))` gives the bound `3 / 2 * D * G * √n` on a set of + diameter `D`, for subgradients of norm at most `G`; +* for losses `f t` that are `μ t`-strongly convex, the learning rates `η t = 1 / ∑ s ≤ t, μ s` + give the bound `∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)` [HAK07; Ora, Theorem 4.7], hence + `L ^ 2 / (2 μ) * (1 + log n)` for `μ t = μ` and `‖g t‖ ≤ L` [Ora, Corollary 4.8]. On the + guessing game of the squared losses `(a - y t) ^ 2` on `[0, 1]`, this is `1 + log n` + [Ora, Example 4.11]. ## Main statements @@ -31,13 +45,26 @@ diameter at most `D`, for subgradients of norm at most `G`, is at most at the plays is at most the regret of the linearized losses. * `isMirrorDescentStep_norm_sq_div_two_iff`: the mirror descent steps for the potential `‖b‖ ^ 2 / 2` and the loss `⟪g, ·⟫` from `a` are the points of `K` nearest to `a - η • g`. -* `onlineSubgradientDescent_regret_le`: the regret of projected online subgradient descent with - nonincreasing learning rates. +* `inner_sub_le_of_isMinOn_norm_sub`: [Ora, Lemmas 2.12 and 2.31] one step of projected online + subgradient descent. +* `onlineSubgradientDescent_regret_le_norm_sub_sq_div`: [Ora, Theorem 2.13] the regret with a + constant learning rate, with no bound on the diameter. +* `onlineSubgradientDescent_regret_le_of_antitone`: [Ora, Theorem 2.13] the regret with + nonincreasing learning rates, keeping the last distance `‖u - a n‖`. +* `onlineSubgradientDescent_regret_le`: its form on a set of diameter at most `D`. * `onlineSubgradientDescent_regret_le_sqrt`: with `η t = D / (G √(t + 1))`, the regret is at most `3 / 2 * D * G * √n`. +* `onlineSubgradientDescent_regret_le_sum_norm_sq_div`: [Ora, Theorem 4.7] the regret on losses + that are strongly convex at the plays, and `onlineSubgradientDescent_regret_le_of_strongConvexOn` + its form for strongly convex losses. +* `onlineSubgradientDescent_regret_le_mul_one_add_log`: [Ora, Corollary 4.8] logarithmic regret + for `μ`-strongly convex losses with bounded subgradients. +* `onlineSubgradientDescent_regret_sq_sub_le_one_add_log`: [Ora, Example 4.11] the guessing game. ## References +* [HAK07] E. Hazan, A. Agarwal and S. Kale, *Logarithmic regret algorithms for online convex + optimization*, Machine Learning 69 (2007). * [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, arXiv:1912.13213v10, 2026. * [Zin03] M. Zinkevich, *Online convex programming and generalized infinitesimal gradient ascent*, @@ -91,6 +118,92 @@ theorem isMirrorDescentStep_norm_sq_div_two_iff {η : ℝ} {g a x : E} : refine and_congr_right fun _ ↦ forall₂_congr fun c _ ↦ ?_ rw [div_le_div_iff_of_pos_right two_pos, sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] +/-- **One step of projected online subgradient descent** [Ora, Lemmas 2.12 and 2.31]. Let `K` be +convex, let `η > 0`, and let `x ∈ K` be a point of `K` nearest to the gradient step `a - η • g`. +Then for every `u ∈ K`, +`⟪g, a - u⟫ ≤ (‖u - a‖ ^ 2 - ‖u - x‖ ^ 2) / (2 η) + η / 2 * ‖g‖ ^ 2`. +The point `a` need not lie in `K`. -/ +theorem inner_sub_le_of_isMinOn_norm_sub (hK : Convex ℝ K) {η : ℝ} (hη : 0 < η) {g a x : E} + (hx : x ∈ K) (hmin : IsMinOn (fun b ↦ ‖b - (a - η • g)‖) K x) (hu : u ∈ K) : + ⟪g, a - u⟫ ≤ (‖u - a‖ ^ 2 - ‖u - x‖ ^ 2) / (2 * η) + η / 2 * ‖g‖ ^ 2 := by + -- the one-step inequality of mirror descent with the potential `‖b‖ ^ 2 / 2` + have h := (isMirrorDescentStep_norm_sq_div_two_iff.mpr ⟨hx, hmin⟩).apply_sub_le hK hη + (hasFDerivAt_norm_sq_div_two x).hasFDerivWithinAt hu + -- its stability term + have h_stab := apply_sub_sub_div_le_of_mul_norm_sq_le one_pos hη (innerSL ℝ g) + (le_of_eq (by ring) : 1 / 2 * ‖x - a‖ ^ 2 ≤ ‖x - a‖ ^ 2 / 2) + simp only [bregDiv_norm_sq_div_two, innerSL_apply_apply, innerSL_apply_norm] at h h_stab + have h_eq : (‖u - a‖ ^ 2 / 2 - ‖u - x‖ ^ 2 / 2 - ‖x - a‖ ^ 2 / 2) / η = + (‖u - a‖ ^ 2 - ‖u - x‖ ^ 2) / (2 * η) - ‖x - a‖ ^ 2 / 2 / η := by + field_simp + have h_eq' : η / (2 * 1) * ‖g‖ ^ 2 = η / 2 * ‖g‖ ^ 2 := by rw [mul_one] + linarith + +/-- **Regret of projected online subgradient descent with a constant learning rate** +[Ora, Theorem 2.13, second bound]. Let `K` be convex and `η > 0`. Let `g t` be a subgradient of +the loss `f t` within `K` at `a t`, and let `a (t + 1)` be a point of `K` nearest to +`a t - η • g t`, for `t < n`. Then for every `u ∈ K`, +`regret f a u n ≤ (‖u - a 0‖ ^ 2 - ‖u - a n‖ ^ 2) / (2 η) + η / 2 * ∑ t < n, ‖g t‖ ^ 2`. +No bound on the diameter of `K` is needed, so this applies on unbounded sets. -/ +theorem onlineSubgradientDescent_regret_le_norm_sub_sq_div (hK : Convex ℝ K) {η : ℝ} + (hη : 0 < η) (f : ℕ → E → ℝ) (g a : ℕ → E) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ IsMinOn (fun b ↦ ‖b - (a t - η • g t)‖) K (a (t + 1))) + (hu : u ∈ K) : + regret f a u n ≤ + (‖u - a 0‖ ^ 2 - ‖u - a n‖ ^ 2) / (2 * η) + η / 2 * ∑ t ∈ range n, ‖g t‖ ^ 2 := by + rw [regret_def] + refine (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ a hg hu).trans ?_ + -- each round is bounded by its one-step inequality, and the distances to `u` telescope + have h_step (t : ℕ) (ht : t ∈ range n) : innerSL ℝ (g t) (a t - u) ≤ + (‖u - a t‖ ^ 2 - ‖u - a (t + 1)‖ ^ 2) / (2 * η) + η / 2 * ‖g t‖ ^ 2 := by + have ht' := mem_range.mp ht + simpa using inner_sub_le_of_isMinOn_norm_sub hK hη (ha t ht').1 (ha t ht').2 hu + refine (sum_le_sum h_step).trans_eq ?_ + rw [sum_add_distrib, ← sum_div, sum_range_sub' (fun t ↦ ‖u - a t‖ ^ 2), mul_sum] + +/-- **Regret of projected online subgradient descent with nonincreasing learning rates** +[Ora, Theorem 2.13, first bound]. Let `K` be convex and let the learning rates `η t > 0` be +nonincreasing. Let `g t` be a subgradient of the loss `f t` within `K` at `a t`, and let +`a (t + 1)` be a point of `K` nearest to `a t - η t • g t`, for `t < n`. If `n > 0` and +`‖u - a t‖ ≤ D` for `t < n`, then for `u ∈ K`, +`regret f a u n ≤ (D ^ 2 - ‖u - a n‖ ^ 2) / (2 η (n - 1)) + ∑ t < n, η t / 2 * ‖g t‖ ^ 2`. +Only the distances from the plays to `u` are bounded, not the diameter of `K`; the bound keeps +the term `- ‖u - a n‖ ^ 2 / (2 η (n - 1))`. -/ +theorem onlineSubgradientDescent_regret_le_of_antitone (hK : Convex ℝ K) {η : ℕ → ℝ} + (hη : ∀ t, 0 < η t) (hη_anti : Antitone η) (f : ℕ → E → ℝ) (g a : ℕ → E) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ IsMinOn (fun b ↦ ‖b - (a t - η t • g t)‖) K (a (t + 1))) + (hn : 0 < n) {D : ℝ} (hD : ∀ t < n, ‖u - a t‖ ≤ D) (hu : u ∈ K) : + regret f a u n ≤ + (D ^ 2 - ‖u - a n‖ ^ 2) / (2 * η (n - 1)) + ∑ t ∈ range n, η t / 2 * ‖g t‖ ^ 2 := by + have ha' (t : ℕ) (ht : t < n) := isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) + -- the Bregman divergences to `u` are `‖u - a t‖ ^ 2 / 2 ≤ D ^ 2 / 2` + have hDu (t : ℕ) (ht : t < n) : + bregDiv (fun b : E ↦ ‖b‖ ^ 2 / 2) u (a t) (innerSL ℝ (a t)) ≤ D ^ 2 / 2 := by + rw [bregDiv_norm_sq_div_two] + gcongr + exact hD t ht + have h := sum_apply_sub_le_mirrorDescent_of_antitone hK hη hη_anti (fun t ↦ innerSL ℝ (g t)) a + (fun t ↦ innerSL ℝ (a t)) ha' (fun t _ ↦ (hasFDerivAt_norm_sq_div_two _).hasFDerivWithinAt) + hn hDu hu + -- the stability term of round `t` is at most `η t / 2 * ‖g t‖ ^ 2` + have h_stab : ∑ t ∈ range n, (innerSL ℝ (g t) (a t - a (t + 1)) - + bregDiv (fun b : E ↦ ‖b‖ ^ 2 / 2) (a (t + 1)) (a t) (innerSL ℝ (a t)) / η t) ≤ + ∑ t ∈ range n, η t / 2 * ‖g t‖ ^ 2 := by + refine sum_le_sum fun t _ ↦ ?_ + have := apply_sub_sub_div_le_of_mul_norm_sq_le one_pos (hη t) (innerSL ℝ (g t)) + (le_of_eq (by ring) : 1 / 2 * ‖a (t + 1) - a t‖ ^ 2 ≤ ‖a (t + 1) - a t‖ ^ 2 / 2) + rw [bregDiv_norm_sq_div_two] + simpa [innerSL_apply_norm] using this + rw [bregDiv_norm_sq_div_two] at h + have h_eq : (D ^ 2 / 2 - ‖u - a n‖ ^ 2 / 2) / η (n - 1) = + (D ^ 2 - ‖u - a n‖ ^ 2) / (2 * η (n - 1)) := by + field_simp + rw [regret_def] + refine (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ a hg hu).trans ?_ + linarith + /-- **Regret of projected online subgradient descent** [Ora, Section 2.2]. Let `K` be convex with `‖x - y‖ ≤ D` for `x, y ∈ K`, and let the learning rates `η t > 0` be nonincreasing. Let `g t` be a subgradient of the loss `f t` within `K` at `a t`, for `t < n`, let `a 0 ∈ K`, and let each @@ -105,22 +218,18 @@ theorem onlineSubgradientDescent_regret_le (hK : Convex ℝ K) {η : ℕ → ℝ (hu : u ∈ K) : ∑ t ∈ range n, (f t (a t) - f t u) ≤ D ^ 2 / (2 * η (n - 1)) + ∑ t ∈ range n, η t / 2 * ‖g t‖ ^ 2 := by - have ha' (t : ℕ) (ht : t < n) := isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) - have h_mem := mem_of_isMirrorDescentStep ha0 ha' - have hD : 0 ≤ D := (norm_nonneg _).trans (hKD u hu u hu) - -- the Bregman divergences to `u` are at most `D ^ 2 / 2` - have hDu (t : ℕ) (ht : t < n) : - bregDiv (fun b : E ↦ ‖b‖ ^ 2 / 2) u (a t) (innerSL ℝ (a t)) ≤ D ^ 2 / 2 := by - rw [bregDiv_norm_sq_div_two] - gcongr - exact hKD u hu (a t) (h_mem t ht.le) - have h := mirrorDescent_regret_le_of_strongConvexOn_of_antitone - (strongConvexOn_norm_sq_div_two hK) one_pos hη hη_anti (fun t ↦ innerSL ℝ (g t)) a - (fun t ↦ innerSL ℝ (a t)) ha0 ha' - (fun t _ ↦ (hasFDerivAt_norm_sq_div_two (a t)).hasFDerivWithinAt) (by positivity) hDu hu - simp only [innerSL_apply_norm, mul_one] at h - rw [div_div] at h - exact (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ a hg hu).trans h + rcases n.eq_zero_or_pos with rfl | hn + · simpa using div_nonneg (sq_nonneg D) (mul_pos two_pos (hη _)).le + have h_mem := mem_of_isMirrorDescentStep ha0 fun t ht ↦ + isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) + have h := onlineSubgradientDescent_regret_le_of_antitone hK hη hη_anti f g a hg ha hn + (fun t ht ↦ hKD u hu (a t) (h_mem t ht.le)) hu + -- the last distance `‖u - a n‖` only decreases the bound + have h_last : 0 ≤ ‖u - a n‖ ^ 2 / (2 * η (n - 1)) := by + have := hη (n - 1) + positivity + rw [regret_def, sub_div] at h + linarith /-- **Projected online subgradient descent with an anytime learning rate** [Ora, Section 2.2]. Let `K` be convex with `‖x - y‖ ≤ D` for `x, y ∈ K`, and let `g t` be a subgradient of the loss @@ -186,6 +295,165 @@ theorem onlineSubgradientDescent_regret_le_sqrt (hK : Convex ℝ K) {D G : ℝ} have := mul_le_mul_of_nonneg_left h_sum h_DG linarith +/-- **Regret of projected online subgradient descent on strongly convex losses** +[Ora, Theorem 4.7]. Let `K` be convex, and let the moduli `μ t` have positive partial sums +`0 < ∑ s ≤ t, μ s`, for `t < n`. Let each loss `f t` lie above the paraboloid +`f t (a t) + ⟪g t, · - a t⟫ + μ t / 2 * ‖· - a t‖ ^ 2` on `K` (strong convexity at the plays), and +let `a (t + 1)` be a point of `K` nearest to `a t - η t • g t` for the learning rate +`η t = 1 / ∑ s ≤ t, μ s`, for `t < n`. Then for every `u ∈ K`, +`regret f a u n ≤ ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)`. +The moduli `μ t` need not be nonnegative, and `a 0` need not lie in `K`. -/ +theorem onlineSubgradientDescent_regret_le_sum_norm_sq_div (hK : Convex ℝ K) (f : ℕ → E → ℝ) + (g a : ℕ → E) {μ : ℕ → ℝ} (hμ : ∀ t < n, 0 < ∑ s ∈ range (t + 1), μ s) + (hf : ∀ t < n, ∀ v ∈ K, f t (a t) + ⟪g t, v - a t⟫ + μ t / 2 * ‖v - a t‖ ^ 2 ≤ f t v) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ + IsMinOn (fun b ↦ ‖b - (a t - (∑ s ∈ range (t + 1), μ s)⁻¹ • g t)‖) K (a (t + 1))) + (hu : u ∈ K) : + regret f a u n ≤ ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), μ s) := by + set S : ℕ → ℝ := fun t ↦ ∑ s ∈ range t, μ s with hS_def + have hS (t : ℕ) : S (t + 1) = S t + μ t := sum_range_succ μ t + -- the potential `S t / 2 * ‖u - a t‖ ^ 2` decreases by the regret of round `t`, up to the + -- stability term `‖g t‖ ^ 2 / (2 S (t + 1))` + have h_step (t : ℕ) (ht : t ∈ range n) : f t (a t) - f t u ≤ + (S t / 2 * ‖u - a t‖ ^ 2 - S (t + 1) / 2 * ‖u - a (t + 1)‖ ^ 2) + + ‖g t‖ ^ 2 / (2 * S (t + 1)) := by + have ht' := mem_range.mp ht + have hpos : 0 < S (t + 1) := hμ t ht' + have h_one := inner_sub_le_of_isMinOn_norm_sub hK (inv_pos.mpr hpos) (ha t ht').1 + (ha t ht').2 hu + have h_f := hf t ht' u hu + have h_inner : ⟪g t, u - a t⟫ = -⟪g t, a t - u⟫ := by rw [← inner_neg_right, neg_sub] + have h_eq₁ : (‖u - a t‖ ^ 2 - ‖u - a (t + 1)‖ ^ 2) / (2 * (S (t + 1))⁻¹) = + S (t + 1) / 2 * ‖u - a t‖ ^ 2 - S (t + 1) / 2 * ‖u - a (t + 1)‖ ^ 2 := by + field_simp + have h_eq₂ : (S (t + 1))⁻¹ / 2 * ‖g t‖ ^ 2 = ‖g t‖ ^ 2 / (2 * S (t + 1)) := by + field_simp + have h_eq₃ : S (t + 1) / 2 * ‖u - a t‖ ^ 2 = + S t / 2 * ‖u - a t‖ ^ 2 + μ t / 2 * ‖u - a t‖ ^ 2 := by + rw [hS] + ring + linarith + rw [regret_def] + refine (sum_le_sum h_step).trans ?_ + rw [sum_add_distrib, sum_range_sub' (fun t ↦ S t / 2 * ‖u - a t‖ ^ 2)] + -- the final potential `S n / 2 * ‖u - a n‖ ^ 2` is nonnegative + have h_last : 0 ≤ S n / 2 * ‖u - a n‖ ^ 2 := by + rcases n with _ | m + · simp [hS_def] + · have := hμ m m.lt_succ_self + positivity + simp only [hS_def, sum_range_zero, zero_div, zero_mul, zero_sub] at h_last ⊢ + linarith + +/-- **Regret of projected online subgradient descent on strongly convex losses** +[Ora, Theorem 4.7]. Let `K` be convex, let the loss `f t` be `μ t`-strongly convex on `K`, with +positive partial sums `0 < ∑ s ≤ t, μ s`, and let `g t` be a subgradient of `f t` within `K` at +`a t`, for `t < n`. Let `a 0 ∈ K`, and let `a (t + 1)` be a point of `K` nearest to +`a t - η t • g t` for the learning rate `η t = 1 / ∑ s ≤ t, μ s`, for `t < n`. Then for every +`u ∈ K`, `regret f a u n ≤ ∑ t < n, ‖g t‖ ^ 2 / (2 ∑ s ≤ t, μ s)`. -/ +theorem onlineSubgradientDescent_regret_le_of_strongConvexOn (hK : Convex ℝ K) (f : ℕ → E → ℝ) + (g a : ℕ → E) {μ : ℕ → ℝ} (hμ : ∀ t < n, 0 < ∑ s ∈ range (t + 1), μ s) + (hf : ∀ t < n, StrongConvexOn K (μ t) (f t)) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) (ha0 : a 0 ∈ K) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ + IsMinOn (fun b ↦ ‖b - (a t - (∑ s ∈ range (t + 1), μ s)⁻¹ • g t)‖) K (a (t + 1))) + (hu : u ∈ K) : + regret f a u n ≤ ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), μ s) := by + have h_mem : ∀ t < n, a t ∈ K + | 0, _ => ha0 + | t + 1, ht => (ha t (Nat.lt_of_succ_lt ht)).1 + refine onlineSubgradientDescent_regret_le_sum_norm_sq_div hK f g a hμ (fun t ht v hv ↦ ?_) ha hu + simpa using (hf t ht).add_add_le_of_hasSubgradientWithinAt (h_mem t ht) hv (hg t ht) + +/-- **Logarithmic regret of projected online subgradient descent on strongly convex losses** +[Ora, Corollary 4.8]. Let `K` be convex and `μ > 0`. Let the loss `f t` be `μ`-strongly convex +on `K`, and let `g t` be a subgradient of `f t` within `K` at `a t` with `‖g t‖ ≤ L`, for `t < n`. +Let `a 0 ∈ K`, and let `a (t + 1)` be a point of `K` nearest to `a t - η t • g t` for the learning +rate `η t = 1 / ((t + 1) μ)`, for `t < n`. Then for every `u ∈ K`, +`regret f a u n ≤ L ^ 2 / (2 μ) * (1 + log n)`. -/ +theorem onlineSubgradientDescent_regret_le_mul_one_add_log (hK : Convex ℝ K) (f : ℕ → E → ℝ) + (g a : ℕ → E) {μ L : ℝ} (hμ : 0 < μ) (hf : ∀ t < n, StrongConvexOn K μ (f t)) + (hg : ∀ t < n, HasSubgradientWithinAt (f t) (innerSL ℝ (g t)) K (a t)) + (hgL : ∀ t < n, ‖g t‖ ≤ L) (ha0 : a 0 ∈ K) + (ha : ∀ t < n, a (t + 1) ∈ K ∧ + IsMinOn (fun b ↦ ‖b - (a t - (((t : ℝ) + 1) * μ)⁻¹ • g t)‖) K (a (t + 1))) + (hu : u ∈ K) : + regret f a u n ≤ L ^ 2 / (2 * μ) * (1 + Real.log n) := by + have h_sum (t : ℕ) : ∑ s ∈ range (t + 1), μ = ((t : ℝ) + 1) * μ := by simp + have h := onlineSubgradientDescent_regret_le_of_strongConvexOn hK f g a (μ := fun _ ↦ μ) + (fun t _ ↦ by rw [h_sum]; positivity) hf hg ha0 (fun t ht ↦ by rw [h_sum]; exact ha t ht) hu + simp only [h_sum] at h + refine h.trans ?_ + -- each stability term is at most `L ^ 2 / (2 μ) * (t + 1)⁻¹` + have h_term : ∀ t ∈ range n, ‖g t‖ ^ 2 / (2 * (((t : ℝ) + 1) * μ)) ≤ + L ^ 2 / (2 * μ) * ((t : ℝ) + 1)⁻¹ := by + intro t ht + have h_sq : ‖g t‖ ^ 2 ≤ L ^ 2 := by + gcongr + exact hgL t (mem_range.mp ht) + calc ‖g t‖ ^ 2 / (2 * (((t : ℝ) + 1) * μ)) ≤ L ^ 2 / (2 * (((t : ℝ) + 1) * μ)) := by gcongr + _ = L ^ 2 / (2 * μ) * ((t : ℝ) + 1)⁻¹ := by field_simp + refine (sum_le_sum h_term).trans ?_ + rw [← mul_sum] + exact mul_le_mul_of_nonneg_left (Real.sum_range_inv_add_one_le n) (by positivity) + +/-- **Online subgradient descent on the guessing game** [Ora, Example 4.11]. Let the outcomes +`y t` lie in `[0, 1]`, and let the plays start at `x 0 ∈ [0, 1]` and follow +`x (t + 1) = x t - (x t - y t) / (t + 1)` for `t < n`: this is projected online subgradient descent +on `[0, 1]` for the `2`-strongly convex squared losses `(a - y t) ^ 2`, with gradient +`2 (x t - y t)` and learning rate `1 / (2 (t + 1))`, whose steps stay in `[0, 1]`. Then the +regret of the squared losses against every `u ∈ [0, 1]` is at most `1 + log n`. -/ +theorem onlineSubgradientDescent_regret_sq_sub_le_one_add_log (x y : ℕ → ℝ) {u : ℝ} {n : ℕ} + (hy : ∀ t < n, y t ∈ Set.Icc 0 1) (hx0 : x 0 ∈ Set.Icc 0 1) + (hx : ∀ t < n, x (t + 1) = x t - (x t - y t) / (t + 1)) (hu : u ∈ Set.Icc 0 1) : + regret (fun t a ↦ (a - y t) ^ 2) x u n ≤ 1 + Real.log n := by + -- the plays are convex combinations of the previous play and outcome, so they stay in `[0, 1]` + have h_mem (t : ℕ) : t ≤ n → x t ∈ Set.Icc 0 1 := by + induction t with + | zero => exact fun _ ↦ hx0 + | succ t ih => + intro ht + have ⟨h0, h1⟩ := ih (Nat.le_of_succ_le ht) + have ⟨hy0, hy1⟩ := hy t ht + have h_eq : x (t + 1) = (t * x t + y t) / (t + 1) := by + rw [hx t ht] + field_simp + ring + rw [h_eq] + constructor + · positivity + · rw [div_le_one (by positivity)] + nlinarith + -- the squared losses are `2`-strongly convex, with derivative `2 (x t - y t)` at `x t` + have hf (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) + (innerSL ℝ (2 * (x t - y t))) (Set.Icc 0 1) (x t) := by + refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ + simp only [innerSL_apply_apply, Real.inner_apply] + nlinarith [sq_nonneg (a - x t)] + have hgL (t : ℕ) (ht : t < n) : ‖2 * (x t - y t)‖ ≤ 2 := by + have ⟨h0, h1⟩ := h_mem t ht.le + have ⟨hy0, hy1⟩ := hy t ht + rw [Real.norm_eq_abs, abs_le] + constructor <;> linarith + -- the gradient steps are the plays, so they are their own nearest points in `[0, 1]` + have ha (t : ℕ) (ht : t < n) : x (t + 1) ∈ Set.Icc 0 1 ∧ IsMinOn + (fun b ↦ ‖b - (x t - (((t : ℝ) + 1) * 2)⁻¹ • (2 * (x t - y t)))‖) (Set.Icc 0 1) + (x (t + 1)) := by + refine ⟨h_mem (t + 1) ht, isMinOn_iff.mpr fun b _ ↦ ?_⟩ + have h_step : x t - (((t : ℝ) + 1) * 2)⁻¹ • (2 * (x t - y t)) = x (t + 1) := by + rw [hx t ht, smul_eq_mul] + field_simp + rw [h_step, sub_self, norm_zero] + exact norm_nonneg _ + have h := onlineSubgradientDescent_regret_le_mul_one_add_log (convex_Icc (0 : ℝ) 1) _ + (fun t ↦ 2 * (x t - y t)) x two_pos hf hg hgL hx0 ha hu + norm_num at h + exact h + end InnerProductSpace end LMLExplore.OnlineLearning From d273b47021484e76652f7343e13d79eabfc99b9a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 11:25:52 +0100 Subject: [PATCH 2/3] refactor: factor the subgradient descent stability bound and the squared-loss facts Add inner_sub_sub_norm_sq_div_le, the stability term of one projected subgradient step, and use it in inner_sub_le_of_isMinOn_norm_sub and onlineSubgradientDescent_regret_le_of_antitone. Factor strongConvexOn_sq_sub and hasSubgradientWithinAt_sq_sub in FTRL/Quadratic.lean and use them in both guessing-game theorems. Use mem_of_isMirrorDescentStep for the plays' membership in the strongly convex bound. Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/FTRL/Quadratic.lean | 36 +++++++++------ .../OnlineLearning/SubgradientDescent.lean | 46 +++++++++---------- 2 files changed, 46 insertions(+), 36 deletions(-) diff --git a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean index 99747a66..a17abd39 100644 --- a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean +++ b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean @@ -42,6 +42,8 @@ bound `4 + 4 log n` of [Ora, Theorem 1.3]. `⟪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)]. +* `strongConvexOn_sq_sub`, `hasSubgradientWithinAt_sq_sub`: the squared loss `(a - y) ^ 2` is + `2`-strongly convex, with subgradient `2 (x - y)` at `x`. * `regret_sq_sub_le_one_add_log`: [Ora, Example 7.26] the regret of follow-the-leader on the guessing game. @@ -168,6 +170,21 @@ theorem isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff {ι : Type*} (t : Fins refine forall₂_congr fun b _ ↦ ?_ rw [mul_le_mul_iff_of_pos_left (half_pos hμ), sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] +/-- The squared loss `(a - y) ^ 2` is `2`-strongly convex on every convex set of `ℝ`. -/ +theorem strongConvexOn_sq_sub {s : Set ℝ} (hs : Convex ℝ s) (y : ℝ) : + StrongConvexOn s 2 fun a ↦ (a - y) ^ 2 := by + convert strongConvexOn_div_two_mul_norm_sub_sq hs 2 y using 2 with a + rw [Real.norm_eq_abs, sq_abs] + ring + +/-- The derivative `2 (x - y)` of the squared loss `(a - y) ^ 2` at `x` is a subgradient of it +within every set of `ℝ`. -/ +theorem hasSubgradientWithinAt_sq_sub (s : Set ℝ) (x y : ℝ) : + HasSubgradientWithinAt (fun a ↦ (a - y) ^ 2) (innerSL ℝ (2 * (x - y))) s x := by + refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ + simp only [innerSL_apply_apply, Real.inner_apply] + nlinarith [sq_nonneg (a - x)] + /-- **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 @@ -179,24 +196,17 @@ theorem regret_sq_sub_le_one_add_log (x y : ℕ → ℝ) {u : ℝ} {n : ℕ} (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 + have h := regret_le_ftl_of_strongConvexOn (fun t a ↦ (a - y t) ^ 2) x _ + (fun t _ ↦ strongConvexOn_sq_sub (convex_Icc 0 1) (y t)) + (fun t _ ↦ by simp only [sum_const, card_range, nsmul_eq_mul]; positivity) hx hmin + (fun t _ ↦ hasSubgradientWithinAt_sq_sub _ (x t) (y t)) 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] + simp only [innerSL_apply_norm, 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 diff --git a/LMLExplore/OnlineLearning/SubgradientDescent.lean b/LMLExplore/OnlineLearning/SubgradientDescent.lean index 89e06935..54cfc205 100644 --- a/LMLExplore/OnlineLearning/SubgradientDescent.lean +++ b/LMLExplore/OnlineLearning/SubgradientDescent.lean @@ -7,6 +7,7 @@ module public import LMLExplore.Analysis.Real.Sqrt public import LMLExplore.NumberTheory.Harmonic.Bounds +public import LMLExplore.OnlineLearning.FTRL.Quadratic public import LMLExplore.OnlineLearning.MirrorDescent public import LMLExplore.OnlineLearning.Regret @@ -45,6 +46,8 @@ to the gradient step `a t - η t • g t`. Each such step satisfies at the plays is at most the regret of the linearized losses. * `isMirrorDescentStep_norm_sq_div_two_iff`: the mirror descent steps for the potential `‖b‖ ^ 2 / 2` and the loss `⟪g, ·⟫` from `a` are the points of `K` nearest to `a - η • g`. +* `inner_sub_sub_norm_sq_div_le`: the stability term of one step of projected online + subgradient descent. * `inner_sub_le_of_isMinOn_norm_sub`: [Ora, Lemmas 2.12 and 2.31] one step of projected online subgradient descent. * `onlineSubgradientDescent_regret_le_norm_sub_sq_div`: [Ora, Theorem 2.13] the regret with a @@ -118,6 +121,16 @@ theorem isMirrorDescentStep_norm_sq_div_two_iff {η : ℝ} {g a x : E} : refine and_congr_right fun _ ↦ forall₂_congr fun c _ ↦ ?_ rw [div_le_div_iff_of_pos_right two_pos, sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] +/-- **Stability of one step of projected online subgradient descent.** For `η > 0`, +`⟪g, a - b⟫ - ‖b - a‖ ^ 2 / 2 / η ≤ η / 2 * ‖g‖ ^ 2`: the linear gain of a step from `a` to `b` +minus its Bregman divergence for the potential `‖·‖ ^ 2 / 2`, divided by `η`, is at most +`η / 2 * ‖g‖ ^ 2`. -/ +theorem inner_sub_sub_norm_sq_div_le {η : ℝ} (hη : 0 < η) (g a b : E) : + ⟪g, a - b⟫ - ‖b - a‖ ^ 2 / 2 / η ≤ η / 2 * ‖g‖ ^ 2 := by + have h := apply_sub_sub_div_le_of_mul_norm_sq_le one_pos hη (innerSL ℝ g) + (one_div_mul_eq_div 2 (‖b - a‖ ^ 2)).le + rwa [mul_one, innerSL_apply_norm, innerSL_apply_apply] at h + /-- **One step of projected online subgradient descent** [Ora, Lemmas 2.12 and 2.31]. Let `K` be convex, let `η > 0`, and let `x ∈ K` be a point of `K` nearest to the gradient step `a - η • g`. Then for every `u ∈ K`, @@ -130,13 +143,11 @@ theorem inner_sub_le_of_isMinOn_norm_sub (hK : Convex ℝ K) {η : ℝ} (hη : 0 have h := (isMirrorDescentStep_norm_sq_div_two_iff.mpr ⟨hx, hmin⟩).apply_sub_le hK hη (hasFDerivAt_norm_sq_div_two x).hasFDerivWithinAt hu -- its stability term - have h_stab := apply_sub_sub_div_le_of_mul_norm_sq_le one_pos hη (innerSL ℝ g) - (le_of_eq (by ring) : 1 / 2 * ‖x - a‖ ^ 2 ≤ ‖x - a‖ ^ 2 / 2) - simp only [bregDiv_norm_sq_div_two, innerSL_apply_apply, innerSL_apply_norm] at h h_stab + have h_stab := inner_sub_sub_norm_sq_div_le hη g a x + simp only [bregDiv_norm_sq_div_two, innerSL_apply_apply] at h have h_eq : (‖u - a‖ ^ 2 / 2 - ‖u - x‖ ^ 2 / 2 - ‖x - a‖ ^ 2 / 2) / η = (‖u - a‖ ^ 2 - ‖u - x‖ ^ 2) / (2 * η) - ‖x - a‖ ^ 2 / 2 / η := by field_simp - have h_eq' : η / (2 * 1) * ‖g‖ ^ 2 = η / 2 * ‖g‖ ^ 2 := by rw [mul_one] linarith /-- **Regret of projected online subgradient descent with a constant learning rate** @@ -192,10 +203,8 @@ theorem onlineSubgradientDescent_regret_le_of_antitone (hK : Convex ℝ K) {η : bregDiv (fun b : E ↦ ‖b‖ ^ 2 / 2) (a (t + 1)) (a t) (innerSL ℝ (a t)) / η t) ≤ ∑ t ∈ range n, η t / 2 * ‖g t‖ ^ 2 := by refine sum_le_sum fun t _ ↦ ?_ - have := apply_sub_sub_div_le_of_mul_norm_sq_le one_pos (hη t) (innerSL ℝ (g t)) - (le_of_eq (by ring) : 1 / 2 * ‖a (t + 1) - a t‖ ^ 2 ≤ ‖a (t + 1) - a t‖ ^ 2 / 2) - rw [bregDiv_norm_sq_div_two] - simpa [innerSL_apply_norm] using this + rw [bregDiv_norm_sq_div_two, innerSL_apply_apply] + exact inner_sub_sub_norm_sq_div_le (hη t) (g t) (a t) (a (t + 1)) rw [bregDiv_norm_sq_div_two] at h have h_eq : (D ^ 2 / 2 - ‖u - a n‖ ^ 2 / 2) / η (n - 1) = (D ^ 2 - ‖u - a n‖ ^ 2) / (2 * η (n - 1)) := by @@ -359,11 +368,10 @@ theorem onlineSubgradientDescent_regret_le_of_strongConvexOn (hK : Convex ℝ K) IsMinOn (fun b ↦ ‖b - (a t - (∑ s ∈ range (t + 1), μ s)⁻¹ • g t)‖) K (a (t + 1))) (hu : u ∈ K) : regret f a u n ≤ ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * ∑ s ∈ range (t + 1), μ s) := by - have h_mem : ∀ t < n, a t ∈ K - | 0, _ => ha0 - | t + 1, ht => (ha t (Nat.lt_of_succ_lt ht)).1 + have h_mem := mem_of_isMirrorDescentStep ha0 fun t ht ↦ + isMirrorDescentStep_norm_sq_div_two_iff.mpr (ha t ht) refine onlineSubgradientDescent_regret_le_sum_norm_sq_div hK f g a hμ (fun t ht v hv ↦ ?_) ha hu - simpa using (hf t ht).add_add_le_of_hasSubgradientWithinAt (h_mem t ht) hv (hg t ht) + simpa using (hf t ht).add_add_le_of_hasSubgradientWithinAt (h_mem t ht.le) hv (hg t ht) /-- **Logarithmic regret of projected online subgradient descent on strongly convex losses** [Ora, Corollary 4.8]. Let `K` be convex and `μ > 0`. Let the loss `f t` be `μ`-strongly convex @@ -424,16 +432,7 @@ theorem onlineSubgradientDescent_regret_sq_sub_le_one_add_log (x y : ℕ → ℝ · positivity · rw [div_le_one (by positivity)] nlinarith - -- the squared losses are `2`-strongly convex, with derivative `2 (x t - y t)` at `x t` - have hf (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) - (innerSL ℝ (2 * (x t - y t))) (Set.Icc 0 1) (x t) := by - refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ - simp only [innerSL_apply_apply, Real.inner_apply] - nlinarith [sq_nonneg (a - x t)] + -- the gradients `2 (x t - y t)` of the squared losses are bounded by `2` have hgL (t : ℕ) (ht : t < n) : ‖2 * (x t - y t)‖ ≤ 2 := by have ⟨h0, h1⟩ := h_mem t ht.le have ⟨hy0, hy1⟩ := hy t ht @@ -450,7 +449,8 @@ theorem onlineSubgradientDescent_regret_sq_sub_le_one_add_log (x y : ℕ → ℝ rw [h_step, sub_self, norm_zero] exact norm_nonneg _ have h := onlineSubgradientDescent_regret_le_mul_one_add_log (convex_Icc (0 : ℝ) 1) _ - (fun t ↦ 2 * (x t - y t)) x two_pos hf hg hgL hx0 ha hu + (fun t ↦ 2 * (x t - y t)) x two_pos (fun t _ ↦ strongConvexOn_sq_sub (convex_Icc 0 1) (y t)) + (fun t _ ↦ hasSubgradientWithinAt_sq_sub _ (x t) (y t)) hgL hx0 ha hu norm_num at h exact h From 6e2f87303f6472d6bb086c42eb8f483fd92dbcef Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 12:33:36 +0100 Subject: [PATCH 3/3] refactor: move the squared-loss lemmas next to the Euclidean potential strongConvexOn_sq_sub and hasSubgradientWithinAt_sq_sub move from FTRL/Quadratic.lean to Analysis/Convex/Bregman/Euclidean.lean, so that SubgradientDescent.lean no longer imports follow-the-leader material. Co-Authored-By: Claude Code --- .../Analysis/Convex/Bregman/Euclidean.lean | 18 ++++++++++++++++++ LMLExplore/OnlineLearning/FTRL/Quadratic.lean | 17 ----------------- .../OnlineLearning/SubgradientDescent.lean | 2 +- 3 files changed, 19 insertions(+), 18 deletions(-) diff --git a/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean b/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean index cdc19463..680bda0b 100644 --- a/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean +++ b/LMLExplore/Analysis/Convex/Bregman/Euclidean.lean @@ -6,6 +6,7 @@ Authors: LMLExplore contributors module public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic public import Mathlib.Analysis.InnerProductSpace.Calculus public import TauCeti.Analysis.Convex.Strong @@ -24,6 +25,8 @@ With this potential, mirror descent is projected gradient descent. * `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`). +* `LMLExplore.strongConvexOn_sq_sub`, `LMLExplore.hasSubgradientWithinAt_sq_sub`: on `ℝ`, the + squared loss `(a - y) ^ 2` is `2`-strongly convex, with subgradient `2 (x - y)` at `x`. -/ public section @@ -72,4 +75,19 @@ theorem strongConvexOn_norm_sq_div_two (hK : Convex ℝ K) : rw [sub_zero] ring +/-- The squared loss `(a - y) ^ 2` is `2`-strongly convex on every convex set of `ℝ`. -/ +theorem strongConvexOn_sq_sub {s : Set ℝ} (hs : Convex ℝ s) (y : ℝ) : + StrongConvexOn s 2 fun a ↦ (a - y) ^ 2 := by + convert strongConvexOn_div_two_mul_norm_sub_sq hs 2 y using 2 with a + rw [Real.norm_eq_abs, sq_abs] + ring + +/-- The derivative `2 (x - y)` of the squared loss `(a - y) ^ 2` at `x` is a subgradient of it +within every set of `ℝ`. -/ +theorem hasSubgradientWithinAt_sq_sub (s : Set ℝ) (x y : ℝ) : + HasSubgradientWithinAt (fun a ↦ (a - y) ^ 2) (innerSL ℝ (2 * (x - y))) s x := by + refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ + simp only [innerSL_apply_apply, Real.inner_apply] + nlinarith [sq_nonneg (a - x)] + end LMLExplore diff --git a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean index a17abd39..cfd9707c 100644 --- a/LMLExplore/OnlineLearning/FTRL/Quadratic.lean +++ b/LMLExplore/OnlineLearning/FTRL/Quadratic.lean @@ -42,8 +42,6 @@ bound `4 + 4 log n` of [Ora, Theorem 1.3]. `⟪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)]. -* `strongConvexOn_sq_sub`, `hasSubgradientWithinAt_sq_sub`: the squared loss `(a - y) ^ 2` is - `2`-strongly convex, with subgradient `2 (x - y)` at `x`. * `regret_sq_sub_le_one_add_log`: [Ora, Example 7.26] the regret of follow-the-leader on the guessing game. @@ -170,21 +168,6 @@ theorem isMinOn_sum_inner_add_div_two_mul_norm_sub_sq_iff {ι : Type*} (t : Fins refine forall₂_congr fun b _ ↦ ?_ rw [mul_le_mul_iff_of_pos_left (half_pos hμ), sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] -/-- The squared loss `(a - y) ^ 2` is `2`-strongly convex on every convex set of `ℝ`. -/ -theorem strongConvexOn_sq_sub {s : Set ℝ} (hs : Convex ℝ s) (y : ℝ) : - StrongConvexOn s 2 fun a ↦ (a - y) ^ 2 := by - convert strongConvexOn_div_two_mul_norm_sub_sq hs 2 y using 2 with a - rw [Real.norm_eq_abs, sq_abs] - ring - -/-- The derivative `2 (x - y)` of the squared loss `(a - y) ^ 2` at `x` is a subgradient of it -within every set of `ℝ`. -/ -theorem hasSubgradientWithinAt_sq_sub (s : Set ℝ) (x y : ℝ) : - HasSubgradientWithinAt (fun a ↦ (a - y) ^ 2) (innerSL ℝ (2 * (x - y))) s x := by - refine hasSubgradientWithinAt_iff_le.mpr fun a _ ↦ ?_ - simp only [innerSL_apply_apply, Real.inner_apply] - nlinarith [sq_nonneg (a - x)] - /-- **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 diff --git a/LMLExplore/OnlineLearning/SubgradientDescent.lean b/LMLExplore/OnlineLearning/SubgradientDescent.lean index 54cfc205..039d35b7 100644 --- a/LMLExplore/OnlineLearning/SubgradientDescent.lean +++ b/LMLExplore/OnlineLearning/SubgradientDescent.lean @@ -5,9 +5,9 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.Analysis.Convex.Bregman.Euclidean public import LMLExplore.Analysis.Real.Sqrt public import LMLExplore.NumberTheory.Harmonic.Bounds -public import LMLExplore.OnlineLearning.FTRL.Quadratic public import LMLExplore.OnlineLearning.MirrorDescent public import LMLExplore.OnlineLearning.Regret