feat: optimistic FTRL, and the stability of minimizers under linear perturbations

LMLExplore/Analysis/Convex/Coercive.lean

@@ -5,6 +5,7 @@ Authors: LMLExplore contributors
 -/
 module
 
+public import LMLExplore.Analysis.Normed.Operator.Basic
 public import Mathlib.Analysis.Convex.Continuous
 public import Mathlib.Analysis.Normed.Module.HahnBanach
 public import TauCeti.Analysis.Convex.Conjugate
@@ -67,7 +68,7 @@ theorem fenchelConjugate_le_of_norm_sub_le
   refine fenchelConjugate_le _ fun x ↦ EReal.coe_sub_le_comm.2 ?_
   have hvx : v x - u x ≤ r * ‖x‖ := by
     rw [← sub_apply]
-    exact (le_abs_self _).trans ((v - u).le_opNorm x |>.trans (by gcongr))
+    exact (v - u).apply_le_opNorm_mul_norm x |>.trans (by gcongr)
   rw [LinearMap.flip_apply, topDualPairing_apply, ← EReal.coe_sub]
   exact (EReal.coe_le_coe_iff.2 (by linarith)).trans (hf x)
 

LMLExplore/Analysis/Convex/Conjugate.lean

@@ -7,6 +7,7 @@ module
 
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
 public import LMLExplore.Analysis.Convex.Bregman.StrictConvex
+public import LMLExplore.Analysis.Normed.Operator.Basic
 public import Mathlib.Analysis.Normed.Operator.Bilinear
 public import TauCeti.Analysis.Convex.EffectiveDomain
 public import TauCeti.Analysis.Convex.Subdifferential
@@ -229,7 +230,7 @@ private lemma exists_pos_apply_sub_sub_bregDiv_le (hF : ConvexOn ℝ D F)
   obtain ⟨c, hc, hgrow⟩ := hFs.exists_pos_mul_norm_le_bregDiv hF hx hu hρ hsphere
   refine ⟨c, hc, fun h hh z hz ↦ ?_⟩
   have hφz : 0 ≤ bregDiv F z x u := hu z hz
-  have hhz : h (z - x) ≤ ‖h‖ * ‖z - x‖ := (le_abs_self _).trans (h.le_opNorm _)
+  have hhz : h (z - x) ≤ ‖h‖ * ‖z - x‖ := h.apply_le_opNorm_mul_norm _
   rcases le_or_gt ‖z - x‖ ρ with hzx | hzx
   · -- Near `x`, the tilt is at most `‖h‖ ρ ≤ ε ‖h‖`.
     have : ‖h‖ * ‖z - x‖ ≤ ε * ‖h‖ := by

LMLExplore/Analysis/Convex/Strong.lean

@@ -7,6 +7,7 @@ module
 
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
 public import LMLExplore.Analysis.Convex.Bregman.Taylor
+public import LMLExplore.Analysis.Normed.Operator.Basic
 public import Mathlib.Analysis.Convex.Strong
 public import Mathlib.Analysis.Normed.Module.FiniteDimension
 public import Mathlib.Topology.Semicontinuity.Basic
@@ -28,9 +29,10 @@ sense at every point of `s`, including its boundary [Ora, Lemma 4.2, Theorems 4.
   strong monotonicity `m * ‖x - y‖ ^ 2 ≤ (g_x - g_y) (x - y)` of the subgradients;
 * a function whose second derivative satisfies `m * ‖y - x‖ ^ 2 ≤ f'' z (y - x) (y - x)` at the
   points `z` of each segment `[x, y]` of a convex set is `m`-strongly convex there;
-* an `m`-strongly convex function grows quadratically away from a minimizer, and, for `m > 0` in
-  finite dimension, a lower semicontinuous `m`-strongly convex function on a nonempty closed set
-  has exactly one minimizer there.
+* an `m`-strongly convex function grows quadratically away from a minimizer, so that, for
+  `m > 0`, minimizers of its perturbations by continuous linear maps `θ₁` and `θ₂` are at distance
+  at most `‖θ₁ - θ₂‖ / m`, and, for `m > 0` in finite dimension, a lower semicontinuous
+  `m`-strongly convex function on a nonempty closed set has exactly one minimizer there.
 
 The last statement is what makes the plays of follow the regularized leader and mirror descent
 with a strongly convex potential exist on closed sets that need not be bounded.
@@ -56,6 +58,9 @@ with a strongly convex potential exist on closed sets that need not be bounded.
 * `Convex.strongConvexOn_of_hasFDerivWithinAt2_mul_norm_sub_sq_le`: [Ora, Theorem 4.3] the
   second-order criterion along segments.
 * `StrongConvexOn.add_mul_norm_sub_sq_le_of_isMinOn`: quadratic growth away from a minimizer.
+* `StrongConvexOn.mul_norm_sub_le_norm_sub_of_isMinOn_add`: [Ora, Lemma 7.49] the minimizers
+  `x, y` of the linear perturbations `f + θ₁` and `f + θ₂` of an `m`-strongly convex `f` satisfy
+  `m * ‖x - y‖ ≤ ‖θ₁ - θ₂‖`.
 * `StrongConvexOn.exists_forall_lt_of_lowerSemicontinuousWithinAt`: for `m > 0`, `f` exceeds its
   value at a point of lower semicontinuity on the points of `s` far enough from it.
 * `StrongConvexOn.exists_isMinOn`, `StrongConvexOn.existsUnique_isMinOn`: [Ora, Theorem 6.9]
@@ -75,7 +80,7 @@ with a strongly convex potential exist on closed sets that need not be bounded.
 * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020,
   Corollary 28.8.
 * [Ora] F. Orabona, *Online Learning: A Modern Introduction Using Convex Optimization*,
-  arXiv:1912.13213v10, Lemma 4.2, Theorems 4.3, 4.6 and 6.9.
+  arXiv:1912.13213v10, Lemmas 4.2 and 7.49, Theorems 4.3, 4.6 and 6.9.
 -/
 
 public section
@@ -109,6 +114,12 @@ theorem add_convexOn (hf : StrongConvexOn s m f) (hg : ConvexOn ℝ s g) :
     StrongConvexOn s m (f + g) := by
   simpa using hf.add (strongConvexOn_zero.2 hg)
 
+/-- The sum of an `m`-strongly convex function on `s` and a continuous linear map is
+`m`-strongly convex on `s`. -/
+theorem add_continuousLinearMap (hf : StrongConvexOn s m f) (L : E →L[ℝ] ℝ) :
+    StrongConvexOn s m fun a ↦ f a + L a :=
+  hf.add_convexOn (L.toLinearMap.convexOn hf.1)
+
 /-- A nonnegative multiple `c • f` of an `m`-strongly convex function on `s` is
 `(c * m)`-strongly convex on `s`. -/
 theorem smul {c : ℝ} (hc : 0 ≤ c) (hf : StrongConvexOn s m f) :
@@ -175,6 +186,29 @@ theorem add_mul_norm_sub_sq_le_of_isMinOn (hf : StrongConvexOn s m f) (hx : x 
   simpa using hf.add_add_le_of_hasSubgradientWithinAt hx hy
     (hasSubgradientWithinAt_zero_iff_isMinOn.2 hmin)
 
+/-- **Stability of the minimizers under linear perturbations** [Ora, Lemma 7.49]. If `f` is
+`m`-strongly convex on `s`, and `x, y ∈ s` minimize on `s` the perturbations `f + θ₁` and
+`f + θ₂` of `f` by continuous linear maps, then `m * ‖x - y‖ ≤ ‖θ₁ - θ₂‖`, where `‖θ₁ - θ₂‖` is
+the dual norm. For `m > 0`, the minimizers are thus `1 / m`-Lipschitz in the perturbation:
+`‖x - y‖ ≤ ‖θ₁ - θ₂‖ / m`. -/
+theorem mul_norm_sub_le_norm_sub_of_isMinOn_add (hf : StrongConvexOn s m f) (hx : x ∈ s)
+    (hy : y ∈ s) {θ₁ θ₂ : E →L[ℝ] ℝ} (hx_min : IsMinOn (fun a ↦ f a + θ₁ a) s x)
+    (hy_min : IsMinOn (fun a ↦ f a + θ₂ a) s y) :
+    m * ‖x - y‖ ≤ ‖θ₁ - θ₂‖ := by
+  have h₁ := (hf.add_continuousLinearMap θ₁).add_mul_norm_sub_sq_le_of_isMinOn hx hx_min hy
+  have h₂ := (hf.add_continuousLinearMap θ₂).add_mul_norm_sub_sq_le_of_isMinOn hy hy_min hx
+  -- adding the quadratic growths at the two minimizers, `m ‖x - y‖² ≤ (θ₁ - θ₂) (y - x)`
+  have h_op : (θ₁ - θ₂) (y - x) ≤ ‖θ₁ - θ₂‖ * ‖x - y‖ := by
+    rw [norm_sub_rev x y]
+    exact (θ₁ - θ₂).apply_le_opNorm_mul_norm _
+  simp only [sub_apply, map_sub] at h_op
+  rw [norm_sub_rev y x] at h₁
+  have h_sq : m * ‖x - y‖ * ‖x - y‖ ≤ ‖θ₁ - θ₂‖ * ‖x - y‖ := by nlinarith
+  rcases (norm_nonneg (x - y)).eq_or_lt with h0 | hpos
+  · rw [← h0, mul_zero]
+    exact norm_nonneg _
+  · exact le_of_mul_le_mul_right h_sq hpos
+
 end StrongConvexOn
 
 namespace Convex
@@ -370,7 +404,7 @@ theorem exists_isMinOn_add_continuousLinearMap [FiniteDimensional ℝ E]
     (hf : StrongConvexOn s m f) (hm : 0 < m) (hs : IsClosed s) (hs_ne : s.Nonempty)
     (hf_lsc : LowerSemicontinuousOn f s) (L : E →L[ℝ] ℝ) :
     ∃ x ∈ s, IsMinOn (f + ⇑L) s x :=
-  (hf.add_convexOn (by simpa using L.toLinearMap.convexOn hf.1)).exists_isMinOn hm hs hs_ne
+  (hf.add_continuousLinearMap L).exists_isMinOn hm hs hs_ne
     (hf_lsc.add (L.continuous.lowerSemicontinuous.lowerSemicontinuousOn s))
 
 /-- **Existence and uniqueness of the minimizer of a strongly convex function** [Ora,
@@ -397,7 +431,7 @@ lemma apply_sub_sub_div_le_of_mul_norm_sq_le {m η D : ℝ} (hm : 0 < m) (hη :
     y (a - b) - D / η ≤ η / (2 * m) * ‖y‖ ^ 2 := by
   have h_apply : y (a - b) ≤ ‖b - a‖ * ‖y‖ := by
     rw [norm_sub_rev, mul_comm]
-    exact (Real.le_norm_self _).trans (y.le_opNorm _)
+    exact y.apply_le_opNorm_mul_norm _
   -- `x z - m x² / (2 η) ≤ η z² / (2 m)`, a square completion
   set x := ‖b - a‖
   set z := ‖y‖

LMLExplore/Analysis/Normed/Operator/Basic.lean

@@ -0,0 +1,33 @@
+/-
+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.Analysis.Normed.Operator.Basic
+
+/-!
+# Real continuous linear functionals and the operator norm
+
+A real continuous linear functional `f` satisfies `f x ≤ ‖f‖ * ‖x‖`, the form of the operator
+norm bound `ContinuousLinearMap.le_opNorm` that pairs a loss or a dual vector with a
+displacement in online learning and convex analysis.
+
+## Main statements
+
+* `ContinuousLinearMap.apply_le_opNorm_mul_norm`: `f x ≤ ‖f‖ * ‖x‖` for `f : E →L[ℝ] ℝ`.
+-/
+
+public section
+
+namespace ContinuousLinearMap
+
+variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E]
+
+/-- A real continuous linear functional is bounded above by its operator norm times the norm of
+its argument: `f x ≤ ‖f‖ * ‖x‖`. -/
+theorem apply_le_opNorm_mul_norm (f : E →L[ℝ] ℝ) (x : E) : f x ≤ ‖f‖ * ‖x‖ :=
+  (Real.le_norm_self _).trans (f.le_opNorm x)
+
+end ContinuousLinearMap

LMLExplore/Bandits/UnitBallFTRL.lean

@@ -6,6 +6,7 @@ Authors: LMLExplore contributors
 module
 
 public import LMLExplore.Analysis.InnerProductSpace.Dual
+public import LMLExplore.Analysis.Normed.Operator.Basic
 public import LMLExplore.Bandits.StochasticMirrorDescent
 public import LMLExplore.MeasureTheory.Function.ConditionalExpectation.FiniteValued
 public import LMLExplore.OnlineLearning.UnitBallPotential
@@ -407,7 +408,7 @@ private lemma integral_sum_apply_smul_sub_le (hr1 : r ≤ 1) (hu : ‖u‖ ≤ 1
                 (integrable_const _) ?_
               filter_upwards [hy1 t (mem_range.1 ht)] with ω hω
               calc y t ω (r • u - u) ≤ ‖y t ω‖ * ‖r • u - u‖ :=
-                    (le_abs_self _).trans ((y t ω).le_opNorm (r • u - u))
+                    (y t ω).apply_le_opNorm_mul_norm _
                 _ ≤ 1 * (1 - r) := mul_le_mul hω h_norm (norm_nonneg _) zero_le_one
                 _ = 1 - r := one_mul _
           _ = 1 - r := by simp