feat: the FTRL equality on arbitrary types, be-the-leader and the regret of follow-the-leader

LMLExplore/Bandits/StochasticMirrorDescent.lean

@@ -22,7 +22,7 @@ problem to online linear optimization with full information: they run mirror des
 estimates `Y t` of the losses, producing plays `a t`, and at round `t` sample the action `A t`
 from a distribution with mean `a t`. If the estimates are unbiased, the expected regret is the
 expected regret of the full-information algorithm on the estimated losses, so that the bounds of
-`LMLExplore.OnlineLearning.MirrorDescent` and `LMLExplore.OnlineLearning.FTRL` transfer in
+`LMLExplore.OnlineLearning.MirrorDescent` and `LMLExplore.OnlineLearning.FTRL.Basic` transfer in
 expectation [LS, Theorem 28.10].
 
 The probabilistic conditions are stated round by round, relative to a σ-algebra `m t` describing

LMLExplore/OnlineLearning/FTRL.lean → LMLExplore/OnlineLearning/FTRL/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import LMLExplore.Analysis.Convex.Bregman.Euclidean
 public import LMLExplore.Analysis.Convex.Bregman.StrongConvex
+public import LMLExplore.OnlineLearning.FTRL.Equality
 public import Mathlib.Analysis.Calculus.LocalExtr.Basic
 public import Mathlib.Topology.Order.Compact
 
@@ -33,17 +34,21 @@ potential measures the losses in the operator norm, the dual norm of the norm of
 norm of `E` chooses the pair of dual norms; for example `PiLp 1 (fun _ : α ↦ ℝ)` carries the `ℓ¹`
 norm, whose dual norm is the sup norm.
 
+The regret analysis of FTRL rests on the FTRL equality of
+`LMLExplore.OnlineLearning.FTRL.Equality`, which needs no structure at all
+[Ora, Lemma 7.1]. The bounds for linear losses on a normed space below are derived from it.
+
 ## Main definitions
 
 * `IsFTRLPlay K F η y t x`: `x` is a play of FTRL on `K` at round `t`, with potential `F`,
   learning rate `η` and losses `y`.
 
 ## Main statements
 
-* `sum_apply_sub_le_ftrl`: the **FTRL lemma** [Ora, Lemma 7.1], for regularizers that may change
-  over the rounds: the regret is at most `ψ n u - ψ 0 (a 0)` plus the sum of the stability terms
-  `y t (a t) - (m (t + 1) - m t)`, where `m t` is the value of the objective of round `t` at its
-  play.
+* `sum_apply_sub_le_ftrl`: the **FTRL lemma** for linear losses on a normed space, for
+  regularizers that may change over the rounds: the regret is at most `ψ n u - ψ 0 (a 0)` plus
+  the sum of the stability terms `y t (a t) - (m (t + 1) - m t)`, where `m t` is the value of the
+  objective of round `t` at its play.
 * `ftrl_regret_le_of_monotone`: for a convex `K` and regularizers `ψ t` nondecreasing in `t` on
   `K`, with derivatives `ψ' t` within `K` at the plays, the regret is at most
   `ψ n u - ψ 0 (a 0) + ∑ t < n, (y t (a t - a (t + 1)) - D_{ψ t}(a (t + 1), a t))`, with `D_ψ`
@@ -79,8 +84,10 @@ norm, whose dual norm is the sup norm.
 
 ## Implementation notes
 
-The FTRL lemma and its telescoping proof are adapted from the LMLPapers project (same author),
-where they are stated for gains on the probability simplex; here they hold for losses on any set.
+The FTRL lemma is adapted from the LMLPapers project (same author), where it is stated for gains
+on the probability simplex. Its telescoping proof, also adapted from there, now proves the FTRL
+equality for losses on any type, in `LMLExplore.OnlineLearning.FTRL.Equality`; this file states
+the case of linear losses on a subset `K` of a real normed space `E`.
 
 ## References
 
@@ -109,7 +116,8 @@ structure IsFTRLPlay (K : Set E) (F : E → ℝ) (η : ℝ) (y : ℕ → E →L[
   /-- The play minimizes the FTRL objective of round `t` over `K`. -/
   isMinOn : IsMinOn (fun b ↦ η * ∑ s ∈ range t, y s b + F b) K x
 
-/-- **FTRL lemma** [Ora, Lemma 7.1]. Let the point `a n` of round `n` do at least as well as `u`
+/-- **FTRL lemma for linear losses** [Ora, Lemma 7.1], the case of `regret_le_ftrl` for linear
+losses on a normed space. Let the point `a n` of round `n` do at least as well as `u`
 on the objective `b ↦ ∑ s < n, y s b + ψ n b`, for instance a minimizer of it over a set containing
 `u`. Then the regret against `u` after `n` rounds is at most `ψ n u - ψ 0 (a 0)` plus the sum over
 the rounds of the stability terms `y t (a t) - (m (t + 1) - m t)`, where
@@ -119,12 +127,10 @@ theorem sum_apply_sub_le_ftrl (ψ : ℕ → E → ℝ) (y : ℕ → E →L[ℝ]
     ∑ t ∈ range n, y t (a t - u) ≤ ψ n u - ψ 0 (a 0) + ∑ t ∈ range n, (y t (a t) -
       ((∑ s ∈ range (t + 1), y s (a (t + 1)) + ψ (t + 1) (a (t + 1))) -
         (∑ s ∈ range t, y s (a t) + ψ t (a t)))) := by
-  -- the values of the objectives at the plays telescope, and `a n` beats `u` at round `n`
-  have h_tele := sum_range_sub (fun t ↦ ∑ s ∈ range t, y s (a t) + ψ t (a t)) n
-  simp only [range_zero, sum_empty, zero_add] at h_tele
-  rw [sum_sub_distrib, h_tele]
-  simp only [map_sub, sum_sub_distrib]
-  linarith
+  have h := regret_le_ftrl ψ (fun t ↦ y t) a a (u := u) (by linarith)
+  rw [regret_eq_sum_apply_sub] at h
+  refine h.trans_eq (congrArg (_ + ·) (sum_congr rfl fun t _ ↦ ?_))
+  ring
 
 /-- Let `a` minimize over `K` the function `c ↦ L c + F c`, where `L` is a continuous linear
 functional and `F` has derivative `F'` within `K` at `a`. If the segment from `a` to `b` lies in

LMLExplore/OnlineLearning/FTRL/Equality.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import LMLExplore.OnlineLearning.Regret
+public import LMLExplore.Order.Filter.Extr
+
+/-!
+# The FTRL equality
+
+The regret analysis of follow the regularized leader (FTRL) rests on an equality that needs no
+structure at all: for regularizers and losses `ψ ℓ : ℕ → α → ℝ` on an arbitrary type `α`, with
+objectives `F t = ψ t + ∑ s < t, ℓ s`, and any points `x`, the regret of `x` is
+`ψ n u - ψ 0 (x 0)` plus the stability terms `F t (x t) - F (t + 1) (x (t + 1)) + ℓ t (x t)` plus
+`F n (x n) - F n u` [Ora, Lemma 7.1]. It holds for nonconvex losses, and the last term is
+nonpositive when `x n` minimizes `F n` over a set containing `u`. FTRL plays at round `t` a
+minimizer of `F t`. Adding a constant to the regularizer `ψ t` adds it to `F t`, which changes no
+play by `isMinOn_add_const_iff` [Ora, Remark 7.3], so the bounds may use `ψ t - c t` in place of
+`ψ t`, for instance with `c t` the minimum of `ψ t`.
+
+The bounds of FTRL for linear losses on a normed space, in
+`LMLExplore.OnlineLearning.FTRL.Basic`, are derived from this equality.
+
+## Main statements
+
+* `regret_eq_ftrl`: the **FTRL equality** [Ora, Lemma 7.1], on an arbitrary type and for arbitrary
+  losses, regularizers and points. The regret on the left may be that of other points than the
+  points of the stability terms [Ora, Remark 7.4].
+* `regret_le_ftrl`: the FTRL inequality, when the last point does at least as well as the
+  comparator on the last objective.
+* `sum_le_of_isMinOn_sum`: the **be-the-leader lemma** [Ora, Lemma 1.2]: the minimizers of the
+  cumulative losses including the current round have nonpositive regret.
+* `regret_le_sum_sub_of_isMinOn_sum`: the regret of follow-the-leader is at most
+  `∑ t < n, (ℓ t (x t) - ℓ t (x (t + 1)))`.
+
+## Implementation notes
+
+The telescoping proof of the FTRL equality is adapted from the LMLPapers project (same author),
+where the FTRL lemma is stated for gains on the probability simplex; here it holds for losses on
+any type.
+
+## References
+
+* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*,
+  arXiv:1912.13213v10, 2026.
+-/
+public section
+
+open Finset
+
+namespace LMLExplore.OnlineLearning
+
+variable {α : Type*}
+
+/-- **The FTRL equality** [Ora, Lemma 7.1 and Remark 7.4]. Let `ψ ℓ : ℕ → α → ℝ` be regularizers
+and losses on an arbitrary type `α`, let `F t = ψ t + ∑ s < t, ℓ s` be the objective of round `t`,
+and let `x z : ℕ → α` be any points. Then the regret of `z` against `u` after `n` rounds is
+`ψ n u - ψ 0 (x 0) + ∑ t < n, (F t (x t) - F (t + 1) (x (t + 1)) + ℓ t (z t))
+  + (F n (x n) - F n u)`.
+For `z = x` this is the regret of `x` [Ora, Lemma 7.1]. With `x t` the plays of FTRL, a minimizer
+of `F t`, and `z t` the plays of another algorithm, it expresses the regret of that algorithm
+through the FTRL plays [Ora, Remark 7.4]. No convexity and no minimality is needed. -/
+theorem regret_eq_ftrl (ψ ℓ : ℕ → α → ℝ) (x z : ℕ → α) (u : α) (n : ℕ) :
+    regret ℓ z u n = ψ n u - ψ 0 (x 0) +
+      ∑ t ∈ range n, ((ψ t (x t) + ∑ s ∈ range t, ℓ s (x t)) -
+        (ψ (t + 1) (x (t + 1)) + ∑ s ∈ range (t + 1), ℓ s (x (t + 1))) + ℓ t (z t)) +
+      ((ψ n (x n) + ∑ s ∈ range n, ℓ s (x n)) - (ψ n u + ∑ s ∈ range n, ℓ s u)) := by
+  -- the values of the objectives at the points telescope
+  have h_tele := sum_range_sub' (fun t ↦ ψ t (x t) + ∑ s ∈ range t, ℓ s (x t)) n
+  simp only [range_zero, sum_empty, add_zero] at h_tele
+  rw [regret_eq_sum_sub_sum, sum_add_distrib, h_tele]
+  ring
+
+/-- **The FTRL inequality** [Ora, Lemma 7.1]. Let `F t = ψ t + ∑ s < t, ℓ s` be the objective of
+round `t` and let `x n` do at least as well as `u` on `F n`, for instance a minimizer of `F n` over
+a set containing `u`. Then for any points `z`, the regret of `z` against `u` after `n` rounds is at
+most `ψ n u - ψ 0 (x 0) + ∑ t < n, (F t (x t) - F (t + 1) (x (t + 1)) + ℓ t (z t))`. -/
+theorem regret_le_ftrl (ψ ℓ : ℕ → α → ℝ) (x z : ℕ → α) {u : α} {n : ℕ}
+    (hx : ψ n (x n) + ∑ s ∈ range n, ℓ s (x n) ≤ ψ n u + ∑ s ∈ range n, ℓ s u) :
+    regret ℓ z u n ≤ ψ n u - ψ 0 (x 0) +
+      ∑ t ∈ range n, ((ψ t (x t) + ∑ s ∈ range t, ℓ s (x t)) -
+        (ψ (t + 1) (x (t + 1)) + ∑ s ∈ range (t + 1), ℓ s (x (t + 1))) + ℓ t (z t)) := by
+  rw [regret_eq_ftrl ψ ℓ x z u n]
+  linarith
+
+/-- **Be-the-leader** [Ora, Lemma 1.2, Remark 15.32]. If each `w t`, for `t < n`, lies in `V` and
+minimizes over `V` the cumulative loss `∑ s ≤ t, ℓ s` of the rounds up to and including `t`, then
+`∑ t < n, ℓ t (w t) ≤ ∑ t < n, ℓ t u` for every `u ∈ V`: the regret of the leaders that know the
+current loss is nonpositive. -/
+theorem sum_le_of_isMinOn_sum {V : Set α} (ℓ : ℕ → α → ℝ) (w : ℕ → α) {u : α} {n : ℕ}
+    (hw : ∀ t < n, w t ∈ V) (hmin : ∀ t < n, IsMinOn (fun a ↦ ∑ s ∈ range (t + 1), ℓ s a) V (w t))
+    (hu : u ∈ V) :
+    ∑ t ∈ range n, ℓ t (w t) ≤ ∑ t ∈ range n, ℓ t u := by
+  have hx : (0 : ℝ) + ∑ s ∈ range n, ℓ s (w (n - 1)) ≤ 0 + ∑ s ∈ range n, ℓ s u := by
+    rcases n with _ | n
+    · simp
+    simpa using isMinOn_iff.mp (hmin n n.lt_succ_self) u hu
+  -- the FTRL inequality with no regularizer, the follow-the-leader points `w (t - 1)` in the
+  -- stability terms and the be-the-leader points `w t` in the regret
+  have h := regret_le_ftrl (fun _ _ ↦ 0) ℓ (fun t ↦ w (t - 1)) w hx
+  -- each round compares the leader `w (t - 1)` of the first `t` rounds with `w t` on these rounds
+  have h_round : ∀ t ∈ range n, (0 + ∑ s ∈ range t, ℓ s (w (t - 1))) -
+      (0 + ∑ s ∈ range (t + 1), ℓ s (w (t + 1 - 1))) + ℓ t (w t) ≤ 0 := by
+    intro t ht
+    have ht := mem_range.mp ht
+    rw [Nat.add_sub_cancel, sum_range_succ]
+    rcases t with _ | t
+    · simp
+    have h_le := isMinOn_iff.mp (hmin t (by omega)) (w (t + 1)) (hw (t + 1) ht)
+    simp only [Nat.add_sub_cancel] at h_le ⊢
+    linarith
+  rw [regret_eq_sum_sub_sum] at h
+  linarith [sum_nonpos h_round]
+
+/-- **The regret of follow-the-leader** [Ora, Lemma 1.2 and the proof of Theorem 1.3]. If each
+`x (t + 1)`, for `t < n`, lies in `V` and minimizes over `V` the cumulative loss
+`∑ s ≤ t, ℓ s`, then the regret of `x` against every `u ∈ V` after `n` rounds is at most
+`∑ t < n, (ℓ t (x t) - ℓ t (x (t + 1)))`. The first point `x 0` is arbitrary. -/
+theorem regret_le_sum_sub_of_isMinOn_sum {V : Set α} (ℓ : ℕ → α → ℝ) (x : ℕ → α) {u : α}
+    {n : ℕ} (hx : ∀ t < n, x (t + 1) ∈ V)
+    (hmin : ∀ t < n, IsMinOn (fun a ↦ ∑ s ∈ range (t + 1), ℓ s a) V (x (t + 1))) (hu : u ∈ V) :
+    regret ℓ x u n ≤ ∑ t ∈ range n, (ℓ t (x t) - ℓ t (x (t + 1))) := by
+  have h := sum_le_of_isMinOn_sum ℓ (fun t ↦ x (t + 1)) hx hmin hu
+  rw [regret_eq_sum_sub_sum, sum_sub_distrib]
+  linarith
+
+end LMLExplore.OnlineLearning

LMLExplore/OnlineLearning/LocalNorm.lean

@@ -12,7 +12,7 @@ public import LMLExplore.OnlineLearning.MirrorDescent
 # Local-norm regret bounds through the unconstrained step
 
 The regret bounds of follow the regularized leader and of mirror descent with a potential `F`
-(`LMLExplore.OnlineLearning.FTRL`, `LMLExplore.OnlineLearning.MirrorDescent`) are sums of
+(`LMLExplore.OnlineLearning.FTRL.Basic`, `LMLExplore.OnlineLearning.MirrorDescent`) are sums of
 stability terms `y (a - b) - D_F(b, a) / η`, where `a` is the play of a round, `y` its loss, `η`
 its learning rate and `b` the next play (or the comparator). Strong convexity bounds such a term
 by `η / (2 m) * ‖y‖ ^ 2`, which is useless for losses with a large dual norm, such as the

LMLExplore/OnlineLearning/MirrorDescent.lean

@@ -5,16 +5,16 @@ Authors: Rémy Degenne
 -/
 module
 
-public import LMLExplore.OnlineLearning.FTRL
+public import LMLExplore.OnlineLearning.FTRL.Basic
 public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
 
 /-!
 # Mirror descent
 
 Online linear optimization on a set `K` of a real normed space `E`, with losses
-`y t : E →L[ℝ] ℝ` in the dual of `E`, as in `LMLExplore.OnlineLearning.FTRL`. **Mirror descent**
-with potential `F` and learning rate `η` starts at a minimizer `a 0` of `F` over `K` [LS, (28.1)]
-and, after the loss `y t` of round `t`, plays a minimizer over `K` of
+`y t : E →L[ℝ] ℝ` in the dual of `E`, as in `LMLExplore.OnlineLearning.FTRL.Basic`.
+**Mirror descent** with potential `F` and learning rate `η` starts at a minimizer `a 0` of `F`
+over `K` [LS, (28.1)] and, after the loss `y t` of round `t`, plays a minimizer over `K` of
 `b ↦ η y t b + D_F(b, a t)` [LS, (28.2)], where `D_F(b, a) = F b - F a - F'(b - a)` is the
 Bregman divergence of `F` for a derivative `F'` of `F` at `a`. Where FTRL regularizes the
 cumulative loss, mirror descent only uses the last loss and the last play. The learning rate may

LMLExplore/OnlineLearning/Simplex.lean

@@ -9,7 +9,7 @@ public import LMLExplore.Analysis.Convex.NegEntropy
 public import LMLExplore.Analysis.Normed.Lp.PiLp
 public import LMLExplore.Analysis.Real.Sqrt
 public import LMLExplore.OnlineLearning.ExponentialWeights
-public import LMLExplore.OnlineLearning.FTRL
+public import LMLExplore.OnlineLearning.FTRL.Basic
 
 /-!
 # Online linear optimization on the probability simplex

LMLExplore/OnlineLearning/UnitBallPotential.lean

@@ -5,7 +5,7 @@ Authors: Rémy Degenne
 -/
 module
 
-public import LMLExplore.OnlineLearning.FTRL
+public import LMLExplore.OnlineLearning.FTRL.Basic
 public import Mathlib.Analysis.SpecialFunctions.Log.Deriv
 public import Mathlib.Analysis.SpecialFunctions.Sqrt
 

LMLExplore/Order/Filter/Extr.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Mathlib.Order.Filter.Extr
+
+/-!
+# Minima are invariant under adding a constant
+
+Adding a constant to a function into an ordered additive structure with cancellation changes none
+of its minimum points, with respect to a filter or on a set.
+
+## Main statements
+
+* `isMinFilter_add_const_iff`: `fun b ↦ f b + c` has a minimum at `a` with respect to `l` iff `f`
+  does.
+* `isMinOn_add_const_iff`: `fun b ↦ f b + c` has a minimum at `a` on `s` iff `f` does.
+-/
+
+public section
+
+variable {α β : Type*} [Add β] [Preorder β] [AddRightMono β] [AddRightReflectLE β]
+  {f : α → β} {l : Filter α} {s : Set α} {a : α}
+
+/-- Adding a constant to a function changes none of its minimum points with respect to a
+filter. -/
+theorem isMinFilter_add_const_iff (c : β) :
+    IsMinFilter (fun b ↦ f b + c) l a ↔ IsMinFilter f l a := by
+  simp only [IsMinFilter, add_le_add_iff_right]
+
+/-- Adding a constant to a function changes none of its minimum points on a set. -/
+theorem isMinOn_add_const_iff (c : β) : IsMinOn (fun b ↦ f b + c) s a ↔ IsMinOn f s a :=
+  isMinFilter_add_const_iff c