From 8823def0986d84227e0c06f4763cb46bcdf23f51 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 15 Nov 2026 13:12:37 +0100 Subject: [PATCH] feat: AdaGrad on a box, its regret bound and coordinatewise scale-freeness Add the online learners `OnlineLearner.adaGradIcc` (adaptive projected online subgradient descent on an interval) and `OnlineLearner.adaGrad` (their coordinatewise product on a box), with their run lemmas, scale-freeness, and the regret bound of [Ora, Theorem 4.32] for linear and convex losses. Add `Set.isMinOn_abs_sub_projIcc`: the projection onto a closed interval is a nearest point. Co-Authored-By: Claude Code --- .../Algebra/Order/Interval/Set/ProjIcc.lean | 46 ++++ LMLExplore/OnlineLearning/AdaptiveRate.lean | 227 +++++++++++++++++- 2 files changed, 272 insertions(+), 1 deletion(-) create mode 100644 LMLExplore/Algebra/Order/Interval/Set/ProjIcc.lean diff --git a/LMLExplore/Algebra/Order/Interval/Set/ProjIcc.lean b/LMLExplore/Algebra/Order/Interval/Set/ProjIcc.lean new file mode 100644 index 00000000..a5b7d896 --- /dev/null +++ b/LMLExplore/Algebra/Order/Interval/Set/ProjIcc.lean @@ -0,0 +1,46 @@ +/- +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 Mathlib.Algebra.Order.Group.Abs +public import Mathlib.Order.Filter.Extr +public import Mathlib.Order.Interval.Set.ProjIcc + +/-! +# The projection onto a closed interval is a nearest point + +In a linearly ordered additive group, `Set.projIcc a b h x` is a point of `[a, b]` nearest to `x` +for the distance `|y - x|`: it minimizes `y ↦ |y - x|` over `[a, b]`. This is the projection step +of projected online subgradient descent on an interval of `ℝ`, and coordinatewise on a box. + +## Main statements + +* `Set.isMinOn_abs_sub_projIcc`: `projIcc a b h x` minimizes `y ↦ |y - x|` over `Icc a b`. +-/ + +public section + +namespace Set + +variable {α : Type*} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a b : α} + +/-- **The projection onto a closed interval is a nearest point**: `projIcc a b h x` minimizes the +distance `y ↦ |y - x|` to `x` over `[a, b]`. -/ +theorem isMinOn_abs_sub_projIcc (h : a ≤ b) (x : α) : + IsMinOn (fun y ↦ |y - x|) (Icc a b) (projIcc a b h x : α) := by + refine isMinOn_iff.mpr fun y hy ↦ ?_ + rcases le_total x a with hxa | hax + · rw [projIcc_of_le_left h hxa, abs_of_nonneg (sub_nonneg.mpr hxa), + abs_of_nonneg (sub_nonneg.mpr (hxa.trans hy.1))] + exact sub_le_sub_right hy.1 x + rcases le_total b x with hbx | hxb + · rw [projIcc_of_right_le h hbx, abs_of_nonpos (sub_nonpos.mpr hbx), + abs_of_nonpos (sub_nonpos.mpr (hy.2.trans hbx))] + exact neg_le_neg (sub_le_sub_right hy.2 x) + · rw [projIcc_of_mem h ⟨hax, hxb⟩, sub_self, abs_zero] + exact abs_nonneg _ + +end Set diff --git a/LMLExplore/OnlineLearning/AdaptiveRate.lean b/LMLExplore/OnlineLearning/AdaptiveRate.lean index 06211d30..223585c9 100644 --- a/LMLExplore/OnlineLearning/AdaptiveRate.lean +++ b/LMLExplore/OnlineLearning/AdaptiveRate.lean @@ -5,13 +5,15 @@ Authors: LMLExplore contributors -/ module +public import LMLExplore.Algebra.Order.Interval.Set.ProjIcc public import LMLExplore.Analysis.Convex.Smooth public import LMLExplore.Analysis.SumIntegralComparisons +public import LMLExplore.OnlineLearning.Learner.Operations public import LMLExplore.OnlineLearning.SubgradientDescent import TauCeti.Analysis.Real.Sqrt /-! -# Adaptive learning rates and `L⋆` bounds +# Adaptive learning rates, `L⋆` bounds and AdaGrad The regret bound of mirror descent with nonincreasing learning rates `η t` and an `m`-strongly convex potential `F` is `B / η (n - 1) + ∑ t < n, η t / (2 m) * ‖y t‖ ^ 2`, where `B` bounds the @@ -34,6 +36,25 @@ controlled by the losses, `‖g t‖ ^ 2 ≤ 2 s f t (a t)`, as for nonnegative comparator `u`: it is at most `4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)` [Ora, Theorem 4.30]. This **`L⋆` bound** is constant when the comparator has zero cumulative loss. +**AdaGrad** [DHS11], [Ora, Section 4.2.4] adapts one learning rate per coordinate. On a box +`∏ a, [l a, r a]` of `α → ℝ`, it runs in each coordinate `a` the adaptive projected online +subgradient descent on the interval `[l a, r a]`, of diameter `D a = r a - l a`, with the learning +rate `D a / √(2 ∑ s ≤ t, g s a ^ 2)` computed from that coordinate of the subgradients alone. It +is the coordinatewise product (`OnlineLearner.pi`) of the one-dimensional learners +`OnlineLearner.adaGradIcc`, so its linear regret is the sum of the regrets of the coordinates, and +the one-dimensional case of [Ora, Theorem 4.14] gives the regret bound +`√2 ∑ a, D a √(∑ t < n, g t a ^ 2)` [Ora, Theorem 4.32]. Since `|g t a| ≤ ‖g t‖`, this is at most +`√2 (∑ a, D a) √(∑ t < n, ‖g t‖ ^ 2)`, for the sup norm of `α → ℝ`. Since each coordinate divides +its step by the root of the sum of its own squared subgradients, the plays of AdaGrad are unchanged +when each coordinate of every subgradient is multiplied by a positive constant of that coordinate. + +## Main definitions + +* `LMLExplore.OnlineLearning.OnlineLearner.adaGradIcc l r h x₀`: AdaGrad on the interval `[l, r]`, + that is, projected online subgradient descent on `[l, r]` with adaptive learning rates. +* `LMLExplore.OnlineLearning.OnlineLearner.adaGrad l r h x₀`: AdaGrad on the box + `∏ a, [l a, r a]` [Ora, Algorithm 4.1]. + ## Main statements * `mirrorDescent_regret_le_two_mul_sqrt`: mirror descent with an `m`-strongly convex potential and @@ -45,9 +66,18 @@ comparator `u`: it is at most `4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)` [Ora, Th `4 s D ^ 2 + 2 D √(s ∑ t < n, f t u)` for losses with `‖g t‖ ^ 2 ≤ 2 s f t (a t)`. * `onlineSubgradientDescent_regret_le_of_selfBoundedOn`: its form for nonnegative `s`-self-bounded losses. +* `OnlineLearner.hasRegretBound_adaGradIcc`: AdaGrad on an interval `[l, r]` has regret at most + `(r - l) √(2 ∑ t < n, g t ^ 2)` for linear losses. +* `OnlineLearner.hasRegretBound_adaGrad`, `OnlineLearner.regret_run_adaGrad_le`: + [Ora, Theorem 4.32] AdaGrad on a box has regret at most `√2 ∑ a, D a √(∑ t < n, g t a ^ 2)`, + for linear and for convex losses. +* `OnlineLearner.run_adaGrad_mul`: AdaGrad is coordinatewise scale-free (see + [Ora, Definition 4.33]). ## References +* [DHS11] J. Duchi, E. Hazan and Y. Singer, *Adaptive subgradient methods for online learning and + stochastic optimization*, JMLR 12, 2011. * [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, arXiv:1912.13213v10, 2026. -/ @@ -296,4 +326,199 @@ theorem onlineSubgradientDescent_regret_le_of_selfBoundedOn (hK : Convex ℝ K) end InnerProductSpace +section AdaGrad + +open Set + +/-- The play of round `t` of `OnlineLearner.adaGradIcc l r h x₀` from the feedback `g` of the +rounds `s < t`, by recursion on `t`. -/ +private noncomputable def adaGradIccPlay (l r : ℝ) (h : l ≤ r) (x₀ : ℝ) : + (t : ℕ) → (Fin t → ℝ) → ℝ + | 0, _ => projIcc l r h x₀ + | t + 1, g => projIcc l r h (adaGradIccPlay l r h x₀ t (fun s ↦ g s.castSucc) - + (r - l) / √(2 * ∑ s, g s ^ 2) * g (Fin.last t)) + +namespace OnlineLearner + +variable {C : Type*} + +section Interval + +variable {l r : ℝ} {h : l ≤ r} {x₀ : ℝ} + +/-- **AdaGrad on an interval** `[l, r]`: projected online subgradient descent on `[l, r]` with the +adaptive learning rates of [Ora, Theorem 4.14], for the diameter `r - l`. Its feedback at round +`t` is the derivative `g t` of a linear loss `x ↦ g t * x`, or a subgradient of a convex loss at +the play. It plays first the projection of `x₀` onto `[l, r]`, then +`x (t + 1) = projIcc l r h (x t - (r - l) / √(2 ∑ s ≤ t, g s ^ 2) * g t)` +(`run_adaGradIcc_succ`). While the feedback observed so far vanishes, the learning rate is `0` +with Lean's division, and the learner stays at its play. It ignores the contexts. -/ +noncomputable def adaGradIcc (l r : ℝ) (h : l ≤ r) (x₀ : ℝ) : OnlineLearner C ℝ ℝ where + play t hist _ := adaGradIccPlay l r h x₀ t fun s ↦ (hist s).2 + +/-- The first play of AdaGrad on `[l, r]` is the projection of `x₀` onto `[l, r]`. -/ +@[simp] +lemma run_adaGradIcc_zero (c : ℕ → C) (g : ℕ → ℝ) : + (adaGradIcc l r h x₀).run c g 0 = projIcc l r h x₀ := by + simp only [run_def, adaGradIcc, adaGradIccPlay] + +/-- The update of AdaGrad on `[l, r]`: the projection onto `[l, r]` of the subgradient step from +the current play, with the learning rate `(r - l) / √(2 ∑ s ≤ t, g s ^ 2)`. -/ +lemma run_adaGradIcc_succ (c : ℕ → C) (g : ℕ → ℝ) (t : ℕ) : + (adaGradIcc l r h x₀).run c g (t + 1) = projIcc l r h ((adaGradIcc l r h x₀).run c g t - + (r - l) / √(2 * ∑ s ∈ range (t + 1), g s ^ 2) * g t) := by + rw [run_def, run_def] + simp only [adaGradIcc, adaGradIccPlay, Fin.val_castSucc, Fin.val_last, + Fin.sum_univ_eq_sum_range (fun s ↦ g s ^ 2)] + +/-- The plays of AdaGrad on `[l, r]` lie in `[l, r]`. -/ +lemma run_adaGradIcc_mem (c : ℕ → C) (g : ℕ → ℝ) (t : ℕ) : + (adaGradIcc l r h x₀).run c g t ∈ Icc l r := by + rcases t with _ | t + · rw [run_adaGradIcc_zero] + exact Subtype.mem _ + · rw [run_adaGradIcc_succ] + exact Subtype.mem _ + +/-- **AdaGrad on an interval is scale-free**: its plays are unchanged when every feedback is +multiplied by the same positive constant. -/ +theorem run_adaGradIcc_const_mul {k : ℝ} (hk : 0 < k) (c : ℕ → C) (g : ℕ → ℝ) : + (adaGradIcc l r h x₀).run c (fun t ↦ k * g t) = (adaGradIcc l r h x₀).run c g := by + funext t + induction t with + | zero => rw [run_adaGradIcc_zero, run_adaGradIcc_zero] + | succ t ih => + rw [run_adaGradIcc_succ, run_adaGradIcc_succ, ih] + -- the learning rate is divided by `k`, and the feedback multiplied by `k` + have h_sum : 2 * ∑ s ∈ range (t + 1), (k * g s) ^ 2 = + k ^ 2 * (2 * ∑ s ∈ range (t + 1), g s ^ 2) := by + simp only [mul_pow, ← mul_sum] + ring + rw [h_sum, Real.sqrt_sq_mul, abs_of_pos hk] + rcases eq_or_ne (√(2 * ∑ s ∈ range (t + 1), g s ^ 2)) 0 with h0 | h0 + · simp [h0] + · congr 3 + field_simp + +/-- **Regret guarantee of AdaGrad on an interval** [Ora, Theorem 4.14]. For linear losses +`x ↦ g t * x` on `ℝ`, the regret of AdaGrad on `[l, r]` after `n` rounds against every `u ∈ [l, r]` +is at most `(r - l) √(2 ∑ t < n, g t ^ 2)`. The learning rates need neither the horizon nor a bound +on the feedback. -/ +theorem hasRegretBound_adaGradIcc : + (adaGradIcc (C := C) l r h x₀).HasRegretBound (fun g x ↦ g * x) (fun _ _ ↦ True) (Icc l r) + (fun n _ g _ ↦ (r - l) * √(2 * ∑ t ∈ range n, g t ^ 2)) := by + refine hasRegretBound_iff.mpr fun c g n _ u hu ↦ ?_ + have h_mem := run_adaGradIcc_mem (l := l) (r := r) (h := h) (x₀ := x₀) c g + -- the step is a projected subgradient step on `[l, r]` for the losses `⟪g t, ·⟫ = g t * ·` + have h_step (t : ℕ) (_ : t < n) : (adaGradIcc l r h x₀).run c g (t + 1) ∈ Icc l r ∧ + IsMinOn (fun b ↦ ‖b - ((adaGradIcc l r h x₀).run c g t - + ((r - l) / √(2 * ∑ s ∈ range (t + 1), ‖g s‖ ^ 2)) • g t)‖) (Icc l r) + ((adaGradIcc l r h x₀).run c g (t + 1)) := by + simp only [Real.norm_eq_abs, sq_abs, smul_eq_mul] + rw [run_adaGradIcc_succ] + exact ⟨Subtype.mem _, isMinOn_abs_sub_projIcc h _⟩ + have h_dist (t : ℕ) (_ : t < n) : ‖u - (adaGradIcc l r h x₀).run c g t‖ ≤ r - l := by + rw [Real.norm_eq_abs, abs_sub_le_iff] + constructor <;> linarith [hu.1, hu.2, (h_mem t).1, (h_mem t).2] + have h_bound := onlineSubgradientDescent_regret_le_mul_sqrt_sum (convex_Icc l r) + (fun t ↦ innerSL ℝ (g t)) g _ (fun t _ ↦ hasSubgradientWithinAt_linear _) (h_mem 0) h_step + h_dist hu + simp only [Real.norm_eq_abs, sq_abs] at h_bound + convert h_bound using 1 + simp only [regret_def, innerSL_apply_apply, Real.inner_apply] + +end Interval + +section Box + +variable {α : Type*} {l r : α → ℝ} {h : l ≤ r} {x₀ : α → ℝ} + +/-- **AdaGrad** on the box `∏ a, [l a, r a]` of `α → ℝ` [Ora, Algorithm 4.1]: the coordinatewise +product (`OnlineLearner.pi`) of the learners AdaGrad on the intervals `[l a, r a]`. Its feedback at +round `t` is a vector `g t : α → ℝ`, the gradient of a linear loss `x ↦ ∑ a, g t a * x a` or a +subgradient of a convex loss at the play. Each coordinate `a` runs projected online subgradient +descent on `[l a, r a]` with its own adaptive learning rate +`(r a - l a) / √(2 ∑ s ≤ t, g s a ^ 2)` (`run_adaGrad_succ`), from the projection of `x₀` onto the +box. It ignores the contexts. -/ +noncomputable def adaGrad (l r : α → ℝ) (h : l ≤ r) (x₀ : α → ℝ) : + OnlineLearner C (α → ℝ) (α → ℝ) := + pi (G := fun _ ↦ ℝ) (X := fun _ ↦ ℝ) fun a ↦ adaGradIcc (l a) (r a) (h a) (x₀ a) + +/-- The coordinates of the plays of AdaGrad are the plays of AdaGrad on the intervals +`[l a, r a]` against the coordinates of the feedback. -/ +lemma run_adaGrad (c : ℕ → C) (g : ℕ → α → ℝ) (t : ℕ) (a : α) : + (adaGrad l r h x₀).run c g t a = (adaGradIcc (l a) (r a) (h a) (x₀ a)).run c (g · a) t := + run_pi (G := fun _ ↦ ℝ) (X := fun _ ↦ ℝ) _ c g t a + +/-- The first play of AdaGrad is the projection of `x₀` onto the box. -/ +@[simp] +lemma run_adaGrad_zero (c : ℕ → C) (g : ℕ → α → ℝ) (a : α) : + (adaGrad l r h x₀).run c g 0 a = projIcc (l a) (r a) (h a) (x₀ a) := by + rw [run_adaGrad, run_adaGradIcc_zero] + +/-- The update of AdaGrad [Ora, Algorithm 4.1]: each coordinate takes a projected subgradient step +on `[l a, r a]`, with the learning rate `(r a - l a) / √(2 ∑ s ≤ t, g s a ^ 2)` of that +coordinate. -/ +lemma run_adaGrad_succ (c : ℕ → C) (g : ℕ → α → ℝ) (t : ℕ) (a : α) : + (adaGrad l r h x₀).run c g (t + 1) a = projIcc (l a) (r a) (h a) + ((adaGrad l r h x₀).run c g t a - + (r a - l a) / √(2 * ∑ s ∈ range (t + 1), g s a ^ 2) * g t a) := by + rw [run_adaGrad, run_adaGrad, run_adaGradIcc_succ] + +/-- The plays of AdaGrad lie in the box `∏ a, [l a, r a]`. -/ +lemma run_adaGrad_mem (c : ℕ → C) (g : ℕ → α → ℝ) (t : ℕ) : + (adaGrad l r h x₀).run c g t ∈ univ.pi fun a ↦ Icc (l a) (r a) := fun a _ ↦ by + rw [run_adaGrad] + exact run_adaGradIcc_mem c _ t + +/-- **AdaGrad is coordinatewise scale-free** (see [Ora, Definition 4.33]): its plays are unchanged +when each coordinate of every feedback is multiplied by a positive constant of that coordinate. -/ +theorem run_adaGrad_mul {k : α → ℝ} (hk : ∀ a, 0 < k a) (c : ℕ → C) (g : ℕ → α → ℝ) : + (adaGrad l r h x₀).run c (fun t ↦ k * g t) = (adaGrad l r h x₀).run c g := by + funext t a + rw [run_adaGrad, run_adaGrad] + exact congrFun (run_adaGradIcc_const_mul (hk a) c fun s ↦ g s a) t + +variable [Fintype α] + +/-- **Regret guarantee of AdaGrad** [Ora, Theorem 4.32]. For linear losses +`x ↦ ∑ a, g t a * x a` on `α → ℝ`, the regret of AdaGrad after `n` rounds against every `u` in the +box `∏ a, [l a, r a]` is at most `√2 ∑ a, (r a - l a) √(∑ t < n, g t a ^ 2)`: the sum over the +coordinates of the regret bounds of AdaGrad on the intervals. -/ +theorem hasRegretBound_adaGrad : + (adaGrad (C := C) l r h x₀).HasRegretBound (fun g x ↦ ∑ a, g a * x a) (fun _ _ ↦ True) + (univ.pi fun a ↦ Icc (l a) (r a)) + (fun n _ g _ ↦ √2 * ∑ a, (r a - l a) * √(∑ t ∈ range n, g t a ^ 2)) := by + refine (HasRegretBound.pi (G := fun _ ↦ ℝ) (X := fun _ ↦ ℝ) + fun a ↦ hasRegretBound_adaGradIcc).mono (fun _ _ _ _ ↦ trivial) subset_rfl + fun n c g u _ _ ↦ le_of_eq ?_ + rw [mul_sum] + refine sum_congr rfl fun a _ ↦ ?_ + rw [Real.sqrt_mul zero_le_two] + ring + +/-- **AdaGrad on convex losses** [Ora, Theorem 4.32]. Let `g t` be a subgradient of the loss `f t` +within the box `∏ a, [l a, r a]` at the play of round `t` of AdaGrad, for `t < n`: the linear map +`x ↦ ∑ a, g t a * x a`. Then for every `u` in the box, the regret of AdaGrad after `n` rounds is at +most `√2 ∑ a, (r a - l a) √(∑ t < n, g t a ^ 2)`. The feedback `g` may be chosen adaptively, as for +the closed-loop runs (`OnlineLearner.closedLoopFeedback`). -/ +theorem regret_run_adaGrad_le (f : ℕ → (α → ℝ) → ℝ) (c : ℕ → C) (g : ℕ → α → ℝ) {n : ℕ} + (hg : ∀ t < n, HasSubgradientWithinAt (f t) + (∑ a, g t a • ContinuousLinearMap.proj a : (α → ℝ) →L[ℝ] ℝ) + (univ.pi fun a ↦ Icc (l a) (r a)) ((adaGrad l r h x₀).run c g t)) + {u : α → ℝ} (hu : u ∈ univ.pi fun a ↦ Icc (l a) (r a)) : + regret f ((adaGrad l r h x₀).run c g) u n ≤ + √2 * ∑ a, (r a - l a) * √(∑ t ∈ range n, g t a ^ 2) := by + rw [regret_def] + refine (sum_sub_le_sum_apply_sub_of_hasSubgradientWithinAt f _ _ hg hu).trans ?_ + refine le_of_eq_of_le ?_ ((hasRegretBound_adaGrad (h := h) (x₀ := x₀)).regret_le (c := c) + (g := g) (fun _ _ ↦ trivial) hu) + simp [regret_def, mul_sub, sum_sub_distrib] + +end Box + +end OnlineLearner + +end AdaGrad + end LMLExplore.OnlineLearning