diff --git a/LMLExplore/Analysis/Convex/Coercive.lean b/LMLExplore/Analysis/Convex/Coercive.lean index 76749da7..d258f0b2 100644 --- a/LMLExplore/Analysis/Convex/Coercive.lean +++ b/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) diff --git a/LMLExplore/Analysis/Convex/Conjugate.lean b/LMLExplore/Analysis/Convex/Conjugate.lean index 2683673c..094ff43a 100644 --- a/LMLExplore/Analysis/Convex/Conjugate.lean +++ b/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 diff --git a/LMLExplore/Analysis/Convex/Strong.lean b/LMLExplore/Analysis/Convex/Strong.lean index f23a7bcd..f26e947b 100644 --- a/LMLExplore/Analysis/Convex/Strong.lean +++ b/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‖ diff --git a/LMLExplore/Analysis/Normed/Operator/Basic.lean b/LMLExplore/Analysis/Normed/Operator/Basic.lean new file mode 100644 index 00000000..78bd71f9 --- /dev/null +++ b/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 diff --git a/LMLExplore/Bandits/UnitBallFTRL.lean b/LMLExplore/Bandits/UnitBallFTRL.lean index 98492cd6..072913d8 100644 --- a/LMLExplore/Bandits/UnitBallFTRL.lean +++ b/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 diff --git a/LMLExplore/OnlineLearning/FTRL/Optimistic.lean b/LMLExplore/OnlineLearning/FTRL/Optimistic.lean new file mode 100644 index 00000000..16e2870d --- /dev/null +++ b/LMLExplore/OnlineLearning/FTRL/Optimistic.lean @@ -0,0 +1,288 @@ +/- +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 LMLExplore.OnlineLearning.FTRL.Stability + +/-! +# Optimistic follow the regularized leader + +Optimistic follow the regularized leader (optimistic FTRL) [Ora, Algorithm 7.8] predicts, before +each round `t`, a hint loss `p t : E → ℝ` for the loss `ℓ t` to come, and plays a minimizer +`x t` over a set `V` of a real normed space `E` of the objective `F t + p t`, where +`F t = ψ t + ∑ s < t, ℓ s` is the objective of FTRL with regularizers `ψ t`. Nothing is assumed on +how the hints are chosen: they may depend arbitrarily on the past, and `p t = 0` is FTRL. When the +hints predict the losses well, the regret is smaller than that of FTRL; when they predict them +badly, the worst-case bound of FTRL is essentially kept. + +* For a subgradient `ĝ t` within `V` of the prediction error `ℓ t - p t` at `x t`, and objectives + `F t + ℓ t` that are `λ t`-strongly convex on `V`, the regret against every comparator `u` is at + most [Ora, Theorem 7.47] + `ψ (n - 1) u - ψ 0 (x 0) + ∑ t < n, (ĝ t (x t - x (t + 1)) - λ t / 2 * ‖x t - x (t + 1)‖ ^ 2) + + ∑ t < n - 1, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1)))`, + where the last point `x n` is a leader of the objective `ψ (n - 1) + ∑ s < n, ℓ s` without hint, + hence at most the same with `‖ĝ t‖ ^ 2 / (2 λ t)` in place of the stability terms, a bound that + needs no last point. The losses and the hints need not be convex: only `F t + ℓ t` is strongly + convex. +* For linear losses `g t` and linear hints `p t`, regularizers `ψ t` that are `λ t`-strongly convex + and nondecreasing in `t` on `V`, and any auxiliary linear hints `q t`, the regret is at most + [Ora, Theorem 7.48] + `ψ (n - 1) u - min ψ 0 + ∑ t < n, (‖g t - q t‖ ^ 2 / (2 λ t) + ‖g t‖ * ‖p t - q t‖ / λ t)`. + With `q = p` this is implied by the previous bound for these losses; with `q = g` the first term + vanishes, which is what delayed feedback needs [Ora, Section 7.13]. The proof compares the + plays with those of the auxiliary hints, through the stability of the minimizers of a strongly + convex function under linear perturbations, + `StrongConvexOn.mul_norm_sub_le_norm_sub_of_isMinOn_add` [Ora, Lemma 7.49]. + +## Main statements + +* `optimistic_ftrl_stability_le_of_strongConvexOn`: the stability bound of one round of + optimistic FTRL. +* `regret_le_optimistic_ftrl_of_strongConvexOn`: [Ora, Theorem 7.47, first inequality] the + regret of optimistic FTRL through its stability terms. +* `regret_le_optimistic_ftrl_norm_sq_div_of_strongConvexOn`: [Ora, Theorem 7.47, second + inequality] the regret of optimistic FTRL through the dual norms of the subgradients of the + prediction errors. +* `sum_apply_sub_le_optimistic_ftrl`: [Ora, Theorem 7.48] the improved bound for linear losses and + linear hints, for auxiliary hints whose plays are given. +* `sum_apply_sub_le_optimistic_ftrl_of_isClosed`: [Ora, Theorem 7.48] the same bound for all + auxiliary hints, in finite dimension, on a closed set and for lower semicontinuous + regularizers, where the auxiliary plays exist. + +## Implementation notes + +[Ora] proves Theorem 7.47 by viewing optimistic FTRL as FTRL with the regularizers +`ψ t + p t`, sets the hint of round `n` (book round `T + 1`) to the hint of round `n - 1`, and +telescopes the hints. That last hint is set at the wrong round: the bound holds with no hint at +round `n`, the last point `x n` being a leader of `ψ (n - 1) + ∑ s < n, ℓ s`. The proof here does +not telescope the hints. It applies the FTRL equality `regret_le_ftrl` to the regularizers +`ψ (min t (n - 1))`, which repeat the last one, and bounds each stability term +`F t (x t) - F (t + 1) (x (t + 1)) + ℓ t (x t)` through the strong convexity of `F t + ℓ t`: since +`x t` minimizes `F t + p t` over `V`, a subgradient of `ℓ t - p t` within `V` at `x t` is one of +`F t + ℓ t`. + +## References + +* [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, + arXiv:1912.13213v10, 2026, Algorithm 7.8, Theorems 7.47 and 7.48, Lemma 7.49. +-/ +public section + +open Finset + +namespace LMLExplore.OnlineLearning + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} + +/-- **Stability of optimistic FTRL** [Ora, proof of Theorem 7.47]. Let `x t ∈ V` minimize over `V` +the objective `F t + p` of optimistic FTRL with hint `p`, where `F t = ψ t + ∑ s < t, ℓ s`, let `g` +be a subgradient of the prediction error `ℓ t - p` within `V` at `x t`, and let `F t + ℓ t` be +`lam`-strongly convex on `V`. Then for every `z ∈ V`, +`F t (x t) - F (t + 1) z + ℓ t (x t) ≤ g (x t - z) - lam / 2 * ‖x t - z‖ ^ 2 + ψ t z - ψ (t + 1) z`. +This is `ftrl_stability_le_of_strongConvexOn` for the regularizers `ψ s + p` and the loss +`ℓ t - p` at round `t`, which leave the objective `F (t + 1)` unchanged. -/ +theorem optimistic_ftrl_stability_le_of_strongConvexOn {ψ ℓ : ℕ → E → ℝ} {p : E → ℝ} + {x : ℕ → E} {t : ℕ} {z : E} {g : E →L[ℝ] ℝ} {lam : ℝ} + (hmin : IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, ℓ s a + p a) V (x t)) + (hg : HasSubgradientWithinAt (fun a ↦ ℓ t a - p a) g V (x t)) + (hΦ : StrongConvexOn V lam fun a ↦ ψ t a + ∑ s ∈ range (t + 1), ℓ s a) (hx : x t ∈ V) + (hz : z ∈ V) : + (ψ t (x t) + ∑ s ∈ range t, ℓ s (x t)) - (ψ (t + 1) z + ∑ s ∈ range (t + 1), ℓ s z) + + ℓ t (x t) ≤ + g (x t - z) - lam / 2 * ‖x t - z‖ ^ 2 + ψ t z - ψ (t + 1) z := by + -- FTRL with the regularizers `ψ s + p` and the loss `ℓ t - p` at round `t` + set ℓ' := Function.update ℓ t fun a ↦ ℓ t a - p a + have hℓ't : ℓ' t = fun a ↦ ℓ t a - p a := Function.update_self _ _ _ + have hℓ' (a : E) : ∑ s ∈ range t, ℓ' s a = ∑ s ∈ range t, ℓ s a := + sum_congr rfl fun s hs ↦ congrFun (Function.update_of_ne (mem_range.mp hs).ne _ _) a + have h := ftrl_stability_le_of_strongConvexOn (ψ := fun s a ↦ ψ s a + p a) (ℓ := ℓ') + (lam := lam) (by simpa only [hℓ', add_right_comm] using hmin) (by rwa [hℓ't]) + (by convert hΦ using 2 with a; simp only [sum_range_succ, hℓ', hℓ't]; ring) hx hz + simp only [sum_range_succ, hℓ', hℓ't] at h ⊢ + linarith + +/-- **The regret of optimistic FTRL** [Ora, Algorithm 7.8, Theorem 7.47, first inequality]. Let +`x t ∈ V`, for `t ≤ n`. For `t < n`, let `x t` minimize over `V` the objective `F t + p t` of +optimistic FTRL, where `F t = ψ t + ∑ s < t, ℓ s` and `p t` is the hint of round `t`, let `g t` be +a subgradient within `V` of the prediction error `ℓ t - p t` at `x t`, and let `F t + ℓ t` be +`lam t`-strongly convex on `V`. If the last point does at least as well as `u` on the objective +`ψ (n - 1) + ∑ s < n, ℓ s` without hint (for instance if `x n` minimizes it over a set containing +`u`), then +`regret ℓ x u n ≤ ψ (n - 1) u - ψ 0 (x 0) + + ∑ t < n, (g t (x t - x (t + 1)) - lam t / 2 * ‖x t - x (t + 1)‖ ^ 2) + + ∑ t < n - 1, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1)))`. +Neither the losses nor the hints need to be convex or differentiable, the regularizers need not +be monotone in `t`, and the moduli `lam t` may be of any sign. -/ +theorem regret_le_optimistic_ftrl_of_strongConvexOn (ψ ℓ p : ℕ → E → ℝ) (x : ℕ → E) + (g : ℕ → E →L[ℝ] ℝ) {lam : ℕ → ℝ} {u : E} {n : ℕ} + (hΦ : ∀ t < n, StrongConvexOn V (lam t) fun a ↦ ψ t a + ∑ s ∈ range (t + 1), ℓ s a) + (hx : ∀ t ≤ n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, ℓ s a + p t a) V (x t)) + (hg : ∀ t < n, HasSubgradientWithinAt (fun a ↦ ℓ t a - p t a) (g t) V (x t)) + (hxn : ψ (n - 1) (x n) + ∑ s ∈ range n, ℓ s (x n) ≤ ψ (n - 1) u + ∑ s ∈ range n, ℓ s u) : + regret ℓ x u n ≤ ψ (n - 1) u - ψ 0 (x 0) + + ∑ t ∈ range n, (g t (x t - x (t + 1)) - lam t / 2 * ‖x t - x (t + 1)‖ ^ 2) + + ∑ t ∈ range (n - 1), (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1))) := by + rcases n with _ | n + · simp only [zero_tsub, range_zero, sum_empty, add_zero, regret_zero] at hxn ⊢ + linarith + -- the FTRL equality for the regularizers `ψ (min t n)`, which repeat the last one + have h := regret_le_ftrl (fun t ↦ ψ (min t n)) ℓ x x (u := u) (n := n + 1) + (by simpa using hxn) + have hψ (t : ℕ) (ht : t ≤ n) : ψ (min t n) = ψ t := by rw [min_eq_left ht] + -- the stability term of round `t`, compared with the next point `x (t + 1)` + have h_round : ∀ t ∈ range (n + 1), + (ψ (min t n) (x t) + ∑ s ∈ range t, ℓ s (x t)) - + (ψ (min (t + 1) n) (x (t + 1)) + ∑ s ∈ range (t + 1), ℓ s (x (t + 1))) + ℓ t (x t) ≤ + (g t (x t - x (t + 1)) - lam t / 2 * ‖x t - x (t + 1)‖ ^ 2) + + (ψ (min t n) (x (t + 1)) - ψ (min (t + 1) n) (x (t + 1))) := by + intro t ht + have ht := mem_range.mp ht + have h := optimistic_ftrl_stability_le_of_strongConvexOn (ψ := fun t ↦ ψ (min t n)) + (by simpa only [hψ t (by omega)] using hmin t ht) (hg t ht) + (by simpa only [hψ t (by omega)] using hΦ t ht) (hx t (by omega)) (hx (t + 1) ht) + linarith + -- the increment of the repeated last regularizer vanishes + have h_inc : ∑ t ∈ range (n + 1), (ψ (min t n) (x (t + 1)) - ψ (min (t + 1) n) (x (t + 1))) = + ∑ t ∈ range n, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1))) := by + rw [sum_range_succ, min_self, min_eq_right n.le_succ, sub_self, add_zero] + exact sum_congr rfl fun t ht ↦ by + rw [hψ t (mem_range.mp ht).le, hψ (t + 1) (mem_range.mp ht)] + have h_sum := (sum_le_sum h_round).trans_eq sum_add_distrib + rw [h_inc] at h_sum + rw [min_eq_right n.le_succ, Nat.zero_min] at h + rw [Nat.add_sub_cancel] + linarith + +/-- **The regret of optimistic FTRL** [Ora, Theorem 7.47, second inequality]. Let `n > 0` and, +for `t < n`, let `x t ∈ V` minimize over `V` the objective `F t + p t` of optimistic FTRL, where +`F t = ψ t + ∑ s < t, ℓ s` and `p t` is the hint of round `t`, let `g t` be a subgradient within +`V` of the prediction error `ℓ t - p t` at `x t`, and let `F t + ℓ t` be `lam t`-strongly convex +on `V`, with `lam t > 0`. Then for every `u ∈ V`, +`regret ℓ x u n ≤ ψ (n - 1) u - ψ 0 (x 0) + ∑ t < n, ‖g t‖ ^ 2 / (2 lam t) + + ∑ t < n - 1, (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1)))`, +where `‖g t‖` is the dual norm. When the hint `p t` is the loss `ℓ t` up to an additive constant, +`g t = 0` is a subgradient and the round costs nothing; with no hint, `g t` is a subgradient of +`ℓ t` and this is the bound of FTRL for convex losses, with the last regularizer repeated. -/ +theorem regret_le_optimistic_ftrl_norm_sq_div_of_strongConvexOn (ψ ℓ p : ℕ → E → ℝ) + (x : ℕ → E) (g : ℕ → E →L[ℝ] ℝ) {lam : ℕ → ℝ} {u : E} {n : ℕ} (hn : 0 < n) + (hlam : ∀ t < n, 0 < lam t) + (hΦ : ∀ t < n, StrongConvexOn V (lam t) fun a ↦ ψ t a + ∑ s ∈ range (t + 1), ℓ s a) + (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, ℓ s a + p t a) V (x t)) + (hg : ∀ t < n, HasSubgradientWithinAt (fun a ↦ ℓ t a - p t a) (g t) V (x t)) (hu : u ∈ V) : + regret ℓ x u n ≤ ψ (n - 1) u - ψ 0 (x 0) + ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * lam t) + + ∑ t ∈ range (n - 1), (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1))) := by + -- the first inequality, with the comparator itself as the last point + set y := Function.update x n u with hy + have hyx (t : ℕ) (ht : t < n) : y t = x t := Function.update_of_ne ht.ne _ _ + have h := regret_le_optimistic_ftrl_of_strongConvexOn ψ ℓ p y g (V := V) (u := u) hΦ + (fun t ht ↦ by + rcases ht.lt_or_eq with ht | rfl + · exact hyx t ht ▸ hx t ht + · simpa [hy] using hu) + (fun t ht ↦ hyx t ht ▸ hmin t ht) (fun t ht ↦ hyx t ht ▸ hg t ht) (by simp [hy]) + rw [regret_congr hyx, hyx 0 hn] at h + have h_inc : ∑ t ∈ range (n - 1), (ψ t (y (t + 1)) - ψ (t + 1) (y (t + 1))) = + ∑ t ∈ range (n - 1), (ψ t (x (t + 1)) - ψ (t + 1) (x (t + 1))) := + sum_congr rfl fun t ht ↦ by rw [hyx (t + 1) (by have := mem_range.mp ht; omega)] + have h_stab : ∑ t ∈ range n, (g t (y t - y (t + 1)) - lam t / 2 * ‖y t - y (t + 1)‖ ^ 2) ≤ + ∑ t ∈ range n, ‖g t‖ ^ 2 / (2 * lam t) := + sum_le_sum fun t ht ↦ apply_sub_sub_mul_norm_sq_le (hlam t (mem_range.mp ht)) _ _ _ + linarith + +/-- **The improved regret of optimistic FTRL for linear losses** [Ora, Theorem 7.48], with given +auxiliary plays. Let the losses `g t` and the hints `p t` be linear, and the regularizers `ψ t` be +`lam t`-strongly convex on `V`, with `lam t > 0`, and nondecreasing in `t` on `V`, with +`c ≤ ψ 0` on `V`. For `t < n`, let `x t ∈ V` minimize over `V` the objective +`ψ t + ∑ s < t, g s + p t` of optimistic FTRL, and let `y t ∈ V` minimize over `V` the objective +`ψ t + ∑ s < t, g s + q t` with auxiliary linear hints `q t`. Then for every `u ∈ V`, +`∑ t < n, g t (x t - u) + ≤ ψ (n - 1) u - c + ∑ t < n, (‖g t - q t‖ ^ 2 / (2 lam t) + ‖g t‖ * ‖p t - q t‖ / lam t)`, +where the norms of `g t`, `p t` and `q t` are dual norms. The auxiliary plays enter only the proof; +`sum_apply_sub_le_optimistic_ftrl_of_isClosed` proves their existence in finite dimension. -/ +theorem sum_apply_sub_le_optimistic_ftrl (ψ : ℕ → E → ℝ) (g p q : ℕ → E →L[ℝ] ℝ) (x y : ℕ → E) + {lam : ℕ → ℝ} {c : ℝ} {u : E} {n : ℕ} (hlam : ∀ t < n, 0 < lam t) + (hψ : ∀ t < n, StrongConvexOn V (lam t) (ψ t)) + (hψ_mono : ∀ t, t + 1 < n → ∀ a ∈ V, ψ t a ≤ ψ (t + 1) a) (hc : ∀ a ∈ V, c ≤ ψ 0 a) + (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, g s a + p t a) V (x t)) + (hy : ∀ t < n, y t ∈ V) + (hymin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, g s a + q t a) V (y t)) + (hu : u ∈ V) : + ∑ t ∈ range n, g t (x t - u) ≤ ψ (n - 1) u - c + + ∑ t ∈ range n, (‖g t - q t‖ ^ 2 / (2 * lam t) + ‖g t‖ * ‖p t - q t‖ / lam t) := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simpa using hc u hu + -- the regret of the auxiliary plays, by the second inequality of Theorem 7.47 + have h_aux := regret_le_optimistic_ftrl_norm_sq_div_of_strongConvexOn ψ (fun t ↦ g t) + (fun t ↦ q t) y (fun t ↦ g t - q t) hn hlam + (fun t ht ↦ by simpa using (hψ t ht).add_continuousLinearMap (∑ s ∈ range (t + 1), g s)) + hy hymin + (fun t _ ↦ hasSubgradientWithinAt_linear (g t - q t)) hu + have h_inc : ∑ t ∈ range (n - 1), (ψ t (y (t + 1)) - ψ (t + 1) (y (t + 1))) ≤ 0 := + sum_nonpos fun t ht ↦ by + have ht := mem_range.mp ht + linarith [hψ_mono t (by omega) _ (hy (t + 1) (by omega))] + have hy0 := hc _ (hy 0 hn) + -- the plays and the auxiliary plays are close by the stability of linear perturbations + have h_close : ∀ t ∈ range n, g t (x t - y t) ≤ ‖g t‖ * ‖p t - q t‖ / lam t := by + intro t ht + have ht := mem_range.mp ht + have h := ((hψ t ht).add_continuousLinearMap (∑ s ∈ range t, g s) + ).mul_norm_sub_le_norm_sub_of_isMinOn_add (hx t ht) (hy t ht) (θ₁ := p t) (θ₂ := q t) + (by simpa using hmin t ht) (by simpa using hymin t ht) + rw [mul_div_assoc] + calc g t (x t - y t) ≤ ‖g t‖ * ‖x t - y t‖ := (g t).apply_le_opNorm_mul_norm _ + _ ≤ ‖g t‖ * (‖p t - q t‖ / lam t) := by + gcongr + rw [le_div_iff₀ (hlam t ht), mul_comm] + exact h + have h_split : ∑ t ∈ range n, g t (x t - u) = + regret (fun t ↦ g t) y u n + ∑ t ∈ range n, g t (x t - y t) := by + rw [regret_def, ← sum_add_distrib] + exact sum_congr rfl fun t _ ↦ by simp only [map_sub]; ring + rw [h_split, sum_add_distrib] + linarith [sum_le_sum h_close] + +/-- **The improved regret of optimistic FTRL for linear losses** [Ora, Theorem 7.48]. In finite +dimension, let `V` be closed, let the losses `g t` and the hints `p t` be linear, and let the +regularizers `ψ t` be lower semicontinuous and `lam t`-strongly convex on `V`, with `lam t > 0`, +and nondecreasing in `t` on `V`, with `c ≤ ψ 0` on `V`. For `t < n`, let `x t ∈ V` minimize over +`V` the objective `ψ t + ∑ s < t, g s + p t` of optimistic FTRL. Then for every `u ∈ V` and all +linear maps `q t`, +`∑ t < n, g t (x t - u) + ≤ ψ (n - 1) u - c + ∑ t < n, (‖g t - q t‖ ^ 2 / (2 lam t) + ‖g t‖ * ‖p t - q t‖ / lam t)`, +where the norms of `g t`, `p t` and `q t` are dual norms. With `q = p` this is a weakening, for +linear losses and nondecreasing regularizers, of the bound of +`regret_le_optimistic_ftrl_norm_sq_div_of_strongConvexOn`; with `q = g` the bound is +`ψ (n - 1) u - c + ∑ t < n, ‖g t‖ * ‖p t - g t‖ / lam t`. -/ +theorem sum_apply_sub_le_optimistic_ftrl_of_isClosed [FiniteDimensional ℝ E] (hV : IsClosed V) + (ψ : ℕ → E → ℝ) (g p q : ℕ → E →L[ℝ] ℝ) (x : ℕ → E) {lam : ℕ → ℝ} {c : ℝ} {u : E} {n : ℕ} + (hlam : ∀ t < n, 0 < lam t) (hψ : ∀ t < n, StrongConvexOn V (lam t) (ψ t)) + (hψ_lsc : ∀ t < n, LowerSemicontinuousOn (ψ t) V) + (hψ_mono : ∀ t, t + 1 < n → ∀ a ∈ V, ψ t a ≤ ψ (t + 1) a) (hc : ∀ a ∈ V, c ≤ ψ 0 a) + (hx : ∀ t < n, x t ∈ V) + (hmin : ∀ t < n, IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, g s a + p t a) V (x t)) + (hu : u ∈ V) : + ∑ t ∈ range n, g t (x t - u) ≤ ψ (n - 1) u - c + + ∑ t ∈ range n, (‖g t - q t‖ ^ 2 / (2 * lam t) + ‖g t‖ * ‖p t - q t‖ / lam t) := by + -- the auxiliary plays exist, as minimizers of strongly convex lower semicontinuous functions + have h_ex (t : ℕ) : ∃ y, t < n → y ∈ V ∧ + IsMinOn (fun a ↦ ψ t a + ∑ s ∈ range t, g s a + q t a) V y := by + by_cases ht : t < n + · obtain ⟨y, hy, hymin⟩ := (hψ t ht).exists_isMinOn_add_continuousLinearMap (hlam t ht) hV + ⟨u, hu⟩ (hψ_lsc t ht) (∑ s ∈ range t, g s + q t) + refine ⟨y, fun _ ↦ ⟨hy, ?_⟩⟩ + convert hymin using 1 + ext a + simp [add_assoc] + · exact ⟨0, fun h ↦ absurd h ht⟩ + choose y hy using h_ex + exact sum_apply_sub_le_optimistic_ftrl ψ g p q x y hlam hψ hψ_mono hc hx hmin + (fun t ht ↦ (hy t ht).1) (fun t ht ↦ (hy t ht).2) hu + +end LMLExplore.OnlineLearning