feat: online subgradient descent on unbounded sets and on strongly convex losses

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

LMLExplore/OnlineLearning/FTRL/Quadratic.lean

@@ -179,24 +179,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
 

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**