From 7554365b203be74419e6f50c694df5374ae720eb Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 06:47:18 +0100 Subject: [PATCH 1/3] feat: the telescoping of the mix losses of exponential weights, stated once Move `mixLoss`, `hedgePotential` and their lemmas from AdaHedge to `OnlineLearning/ExponentialWeights.lean`, prove the telescoping of the mix losses of exponential weights with nonincreasing learning rates, and derive the anytime regret bounds of exponential weights from it. AdaHedge's telescoping uses the same step lemma. Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/AdaHedge.lean | 159 +------- .../OnlineLearning/ExponentialWeights.lean | 373 +++++++++++++++++- .../OnlineLearning/ExponentiatedGradient.lean | 6 +- LMLExplore/OnlineLearning/Simplex.lean | 218 ++-------- 4 files changed, 401 insertions(+), 355 deletions(-) diff --git a/LMLExplore/OnlineLearning/AdaHedge.lean b/LMLExplore/OnlineLearning/AdaHedge.lean index 4e2ce293..29d9e955 100644 --- a/LMLExplore/OnlineLearning/AdaHedge.lean +++ b/LMLExplore/OnlineLearning/AdaHedge.lean @@ -7,7 +7,6 @@ module public import LMLExplore.OnlineLearning.ExponentialWeights public import LMLExplore.Probability.Moments.SubGaussian.Simplex -public import Mathlib.Analysis.MeanInequalitiesPow /-! # AdaHedge @@ -23,8 +22,9 @@ round, the learning rate is infinite and AdaHedge follows the leader: it plays t distribution on the experts of minimal cumulative loss, with mix loss the smallest loss of these experts. -The analysis rests on two facts. The mix losses telescope: for a fixed learning rate `η`, the mix -loss of the exponential weights is the increment of the potential +The analysis rests on two facts. The mix losses telescope, as for exponential weights with any +nonincreasing learning rates (`LMLExplore.OnlineLearning.ExponentialWeights`): for a fixed learning +rate `η`, the mix loss of the exponential weights is the increment of the potential `Φ_η(L) = -(1/η) log ((1/K) ∑ a, exp (-η L a))` (`mixLoss_softmax`), which is at most `L a + log K / η` and nonincreasing in `η` (`hedgePotential_le_of_le`). Since the learning rates of AdaHedge decrease, the total mix loss is at most `min_a L_n a + Δ_n`, so that the regret is at most @@ -37,9 +37,6 @@ pure exploration games of [DKM19, Lemma 3]. ## Main definitions -* `LMLExplore.OnlineLearning.mixLoss η w ℓ`: the mix loss `-(1/η) log ∑ a, w a exp (-η ℓ a)`. -* `LMLExplore.OnlineLearning.hedgePotential η L`: the potential - `-(1/η) log ((1/K) ∑ a, exp (-η L a))` of exponential weights. * `LMLExplore.OnlineLearning.leaders L`, `LMLExplore.OnlineLearning.ftlWeights L`: the experts of minimal cumulative loss and the uniform distribution on them (follow the leader). * `LMLExplore.OnlineLearning.adaHedgeGap y t`: the cumulative mixability gap `Δ_t` of AdaHedge @@ -48,10 +45,8 @@ pure exploration games of [DKM19, Lemma 3]. ## Main statements -* `mixLoss_le_sum_mul`, `sum_mul_le_mixLoss_add`: `⟨w, ℓ⟩ - η (hi - lo) ^ 2 / 8 ≤ m ≤ ⟨w, ℓ⟩`. -* `hedgePotential_eq_mixLoss`: the potential is the mix loss of the uniform weights. -* `mixLoss_softmax`: the mix loss of exponential weights is the increment of the potential. -* `hedgePotential_le_of_le`: the potential is nonincreasing in the learning rate. +* `sum_mul_le_mixLoss_add`: `⟨w, ℓ⟩ - η (hi - lo) ^ 2 / 8 ≤ mixLoss η w ℓ` for losses in + `[lo, hi]`. * `adaHedge_mem_simplex`: AdaHedge plays probability vectors. * `adaHedge_regret_le_two_mul_adaHedgeGap`: the regret of AdaHedge is at most `2 Δ_n`. * `adaHedgeGap_le`: `Δ_n ≤ B + √((∑ t < n, b t ^ 2) log K) / 2` for loss ranges `b t ≤ B`. @@ -77,143 +72,17 @@ namespace LMLExplore.OnlineLearning variable {α : Type*} [Fintype α] -/-! ### The mix loss and the potential of exponential weights -/ - -/-- Multiplying an inequality by `-η⁻¹` for `0 < η`: `-η⁻¹ X ≤ c ↔ -η c ≤ X`. -/ -private lemma neg_inv_mul_le_iff {η : ℝ} (hη : 0 < η) {X c : ℝ} : - -η⁻¹ * X ≤ c ↔ -η * c ≤ X := by - rw [neg_mul, neg_le, inv_mul_eq_div, le_div_iff₀ hη, neg_mul, mul_comm, neg_mul] - -/-- Multiplying an inequality by `-η⁻¹` for `0 < η`: `c ≤ -η⁻¹ X ↔ X ≤ -η c`. -/ -private lemma le_neg_inv_mul_iff {η : ℝ} (hη : 0 < η) {X c : ℝ} : - c ≤ -η⁻¹ * X ↔ X ≤ -η * c := by - rw [neg_mul, le_neg, inv_mul_eq_div, div_le_iff₀ hη, neg_mul, mul_comm, neg_mul] - -/-- The **mix loss** `-(1/η) log ∑ a, w a exp (-η ℓ a)` of the loss vector `ℓ` under the weights -`w`, at the learning rate `η`. -/ -noncomputable def mixLoss (η : ℝ) (w ℓ : α → ℝ) : ℝ := - -η⁻¹ * log (∑ a, w a * exp (-η * ℓ a)) - -lemma mixLoss_def (η : ℝ) (w ℓ : α → ℝ) : - mixLoss η w ℓ = -η⁻¹ * log (∑ a, w a * exp (-η * ℓ a)) := (rfl) - -/-- The mix loss is at most the loss `⟨w, ℓ⟩` of the weights, by Jensen's inequality. -/ -lemma mixLoss_le_sum_mul {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) (ℓ : α → ℝ) : - mixLoss η w ℓ ≤ ∑ a, w a * ℓ a := by - have hw' := mem_simplex_iff.1 hw - have h := convexOn_exp.map_sum_le (t := univ) (w := w) (p := fun a ↦ -η * ℓ a) - (fun a _ ↦ hw'.1 a) hw'.2 (fun _ _ ↦ Set.mem_univ _) - simp only [smul_eq_mul] at h - have hsum : ∑ a, w a * (-η * ℓ a) = -η * ∑ a, w a * ℓ a := by - rw [Finset.mul_sum] - exact Finset.sum_congr rfl fun a _ ↦ by ring - rw [hsum] at h - rw [mixLoss_def, neg_inv_mul_le_iff hη, ← log_exp (-η * ∑ a, w a * ℓ a)] - exact log_le_log (exp_pos _) h +/-! ### The mix loss of bounded losses -/ /-- The mix loss is at least `⟨w, ℓ⟩ - η (hi - lo) ^ 2 / 8` for losses in `[lo, hi]`, by Hoeffding's lemma. -/ lemma sum_mul_le_mixLoss_add {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) {ℓ : α → ℝ} {lo hi : ℝ} (hℓ : ∀ a, ℓ a ∈ Set.Icc lo hi) : ∑ a, w a * ℓ a ≤ mixLoss η w ℓ + η * (hi - lo) ^ 2 / 8 := by - rw [← sub_le_iff_le_add, mixLoss_def, le_neg_inv_mul_iff hη] + rw [← sub_le_iff_le_add, mixLoss_def, ← inv_neg, ← div_eq_inv_mul, + le_div_iff_of_neg (neg_lt_zero.2 hη)] exact (log_sum_mul_exp_le hw hℓ (-η)).trans_eq (by ring) -/-- The mix loss of losses at least `lo` is at least `lo`. -/ -lemma le_mixLoss {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) {ℓ : α → ℝ} {lo : ℝ} - (hℓ : ∀ a, lo ≤ ℓ a) : - lo ≤ mixLoss η w ℓ := by - have hw' := mem_simplex_iff.1 hw - have hle : ∑ a, w a * exp (-η * ℓ a) ≤ exp (-η * lo) := by - calc ∑ a, w a * exp (-η * ℓ a) ≤ ∑ a, w a * exp (-η * lo) := - Finset.sum_le_sum fun a _ ↦ mul_le_mul_of_nonneg_left - (exp_le_exp.2 (by nlinarith [hℓ a])) (hw'.1 a) - _ = exp (-η * lo) := by rw [← Finset.sum_mul, hw'.2, one_mul] - have hpos := sum_mul_pos_of_mem_simplex hw fun a ↦ exp_pos (-η * ℓ a) - rw [mixLoss_def, le_neg_inv_mul_iff hη, ← log_exp (-η * lo)] - exact log_le_log hpos hle - -/-- The potential `-(1/η) log ((1/K) ∑ a, exp (-η L a))` of exponential weights with learning rate -`η` at the cumulative loss vector `L`, with `K` the cardinality of `α`. -/ -noncomputable def hedgePotential (η : ℝ) (L : α → ℝ) : ℝ := - -η⁻¹ * log ((∑ a, exp (-η * L a)) / Fintype.card α) - -lemma hedgePotential_def (η : ℝ) (L : α → ℝ) : - hedgePotential η L = -η⁻¹ * log ((∑ a, exp (-η * L a)) / Fintype.card α) := (rfl) - -/-- The potential is the mix loss of the cumulative losses under the uniform weights. -/ -lemma hedgePotential_eq_mixLoss (η : ℝ) (L : α → ℝ) : - hedgePotential η L = mixLoss η (fun _ ↦ (Fintype.card α : ℝ)⁻¹) L := by - simp_rw [hedgePotential_def, mixLoss_def, Finset.sum_div, div_eq_inv_mul] - -/-- The mix loss of the exponential weights `softmax (-(η • L))` is the increment -`Φ_η(L + ℓ) - Φ_η(L)` of the potential. -/ -lemma mixLoss_softmax [Nonempty α] (η : ℝ) (L ℓ : α → ℝ) : - mixLoss η (softmax (-(η • L))) ℓ = hedgePotential η (L + ℓ) - hedgePotential η L := by - have hZ : 0 < ∑ a, exp (-η * L a) := Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty - have hZ' : 0 < ∑ a, exp (-η * (L + ℓ) a) := Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty - have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos - have hsum : ∑ a, softmax (-(η • L)) a * exp (-η * ℓ a) = - (∑ a, exp (-η * (L + ℓ) a)) / ∑ a, exp (-η * L a) := by - rw [Finset.sum_div] - refine Finset.sum_congr rfl fun a _ ↦ ?_ - simp only [softmax_apply, Pi.neg_apply, Pi.smul_apply, smul_eq_mul, Pi.add_apply, mul_add, - neg_mul, exp_add] - ring - rw [mixLoss_def, hsum, hedgePotential_def, hedgePotential_def, log_div hZ'.ne' hZ.ne', - log_div hZ'.ne' hK.ne', log_div hZ.ne' hK.ne'] - ring - -/-- The potential is at most `L a + log K / η` for every expert `a`. -/ -lemma hedgePotential_le {η : ℝ} (hη : 0 < η) (L : α → ℝ) (a : α) : - hedgePotential η L ≤ L a + log (Fintype.card α) / η := by - have : Nonempty α := ⟨a⟩ - have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos - have hle : exp (-η * L a) ≤ ∑ b, exp (-η * L b) := - Finset.single_le_sum (f := fun b ↦ exp (-η * L b)) (fun b _ ↦ (exp_pos _).le) (mem_univ a) - have hlog : -η * L a - log (Fintype.card α) ≤ log ((∑ b, exp (-η * L b)) / Fintype.card α) := by - rw [log_div (Finset.sum_pos (fun b _ ↦ exp_pos _) univ_nonempty).ne' hK.ne', - ← log_exp (-η * L a)] - exact sub_le_sub_right (log_le_log (exp_pos _) hle) _ - rw [hedgePotential_def, neg_inv_mul_le_iff hη] - refine le_of_eq_of_le ?_ hlog - field_simp - ring - -/-- The potential is at least every lower bound of the cumulative losses. -/ -lemma le_hedgePotential [Nonempty α] {η : ℝ} (hη : 0 < η) {L : α → ℝ} {x : ℝ} - (hL : ∀ a, x ≤ L a) : - x ≤ hedgePotential η L := - hedgePotential_eq_mixLoss η L ▸ le_mixLoss (uniform_mem_simplex α) hη hL - -/-- The potential is nonincreasing in the learning rate: for `0 < η' ≤ η`, -`Φ_η(L) ≤ Φ_η'(L)`. This is the power mean inequality. -/ -lemma hedgePotential_le_of_le [Nonempty α] {η η' : ℝ} (hη' : 0 < η') (hη : η' ≤ η) - (L : α → ℝ) : - hedgePotential η L ≤ hedgePotential η' L := by - have hη0 : 0 < η := hη'.trans_le hη - have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos - set p := η / η' with hp - have hp1 : 1 ≤ p := by rw [hp, le_div_iff₀ hη', one_mul]; exact hη - -- the power mean inequality for the weights `1/K` and the values `exp (-η' L a)` - have hmean := Real.rpow_arith_mean_le_arith_mean_rpow univ (fun _ ↦ (Fintype.card α : ℝ)⁻¹) - (fun a ↦ exp (-η' * L a)) (fun _ _ ↦ inv_nonneg.2 hK.le) - (by simp [Finset.card_univ, hK.ne']) (fun _ _ ↦ (exp_pos _).le) hp1 - have hpow (a : α) : exp (-η' * L a) ^ p = exp (-η * L a) := by - rw [← exp_mul, hp] - congr 1 - field_simp - simp only [hpow, ← Finset.mul_sum] at hmean - have hpos' : 0 < (Fintype.card α : ℝ)⁻¹ * ∑ a, exp (-η' * L a) := - mul_pos (inv_pos.2 hK) (Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty) - have hlog := log_le_log (rpow_pos_of_pos hpos' p) hmean - rw [log_rpow hpos'] at hlog - rw [hedgePotential_def, hedgePotential_def, div_eq_inv_mul, div_eq_inv_mul, - neg_inv_mul_le_iff hη0] - refine le_of_eq_of_le ?_ hlog - rw [hp] - field_simp - /-! ### Follow the leader -/ section Leaders @@ -521,7 +390,6 @@ private lemma sum_adaHedgeMixLoss_le (y : ℕ → α → ℝ) (n : ℕ) : set L := ∑ s ∈ range n, y s set S := ∑ t ∈ range n, adaHedgeMixLoss (adaHedgeGap y t) (∑ s ∈ range t, y s) (y t) have hmono : Δ ≤ adaHedgeGap y (n + 1) := monotone_adaHedgeGap y n.le_succ - have hLsucc : ∑ t ∈ range (n + 1), y t = L + y n := sum_range_succ _ _ simp only [Finset.sum_range_succ] by_cases hΔ : Δ = 0 · -- infinite learning rate, all experts tied: the mix loss is the smallest loss @@ -541,17 +409,12 @@ private lemma sum_adaHedgeMixLoss_le (y : ℕ → α → ℝ) (n : ℕ) : have hΔpos : 0 < Δ := lt_of_le_of_ne h0 (Ne.symm hΔ) have hpos : 0 < adaHedgeGap y (n + 1) := hΔpos.trans_le hmono have hlogK := log_card_pos_of_div_pos h0 hΔ (hη hΔ) - have hm : adaHedgeMixLoss Δ L (y n) = - hedgePotential (log (Fintype.card α) / Δ) (L + y n) - - hedgePotential (log (Fintype.card α) / Δ) L := by - rw [adaHedgeMixLoss_of_ne_zero hΔ, adaHedgeWeights_of_ne_zero hΔ, mixLoss_softmax] refine ⟨fun h ↦ absurd h hpos.ne', fun _ ↦ ?_⟩ have hrate : log (Fintype.card α) / adaHedgeGap y (n + 1) ≤ log (Fintype.card α) / Δ := div_le_div_of_nonneg_left hlogK.le hΔpos hmono - have := hedgePotential_le_of_le (div_pos hlogK hpos) hrate (L + y n) - have := ih.2 hΔ - rw [hm] - linarith + have hstep := add_mixLoss_softmax_le_hedgePotential (hη hΔ) le_rfl (ih.2 hΔ) (y n) + rw [adaHedgeMixLoss_of_ne_zero hΔ, adaHedgeWeights_of_ne_zero hΔ] + exact hstep.trans (hedgePotential_le_of_le (div_pos hlogK hpos) hrate (L + y n)) /-- **Regret of AdaHedge** in terms of its cumulative mixability gap: against every expert `a`, `∑ t < n, (⟨w_t, y t⟩ - y t a) ≤ 2 Δ_n`. -/ diff --git a/LMLExplore/OnlineLearning/ExponentialWeights.lean b/LMLExplore/OnlineLearning/ExponentialWeights.lean index 705184eb..c0232529 100644 --- a/LMLExplore/OnlineLearning/ExponentialWeights.lean +++ b/LMLExplore/OnlineLearning/ExponentialWeights.lean @@ -9,6 +9,7 @@ public import LMLExplore.Analysis.Convex.Simplex public import LMLExplore.Analysis.SpecialFunctions.Exp public import Mathlib.Algebra.BigOperators.Field public import Mathlib.MeasureTheory.Function.SpecialFunctions.Basic +import Mathlib.Analysis.MeanInequalitiesPow import TauCeti.Analysis.SpecialFunctions.Exp.QuadraticBound /-! @@ -22,20 +23,36 @@ cumulative loss. For rewards `r t = 1 - y t` (more generally `r t = c t - y t` w `c t`), the softmax of `η` times the cumulative rewards is the same vector, since adding a constant to every coordinate of `v` does not change `softmax v`. -For nonnegative losses, the regret of exponential weights against every coordinate `a` satisfies -the local-norm bound -`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η + η / 2 * ∑ t < n, ⟨p t, (y t) ^ 2⟩`, -with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The second-order terms are -averages under the played weights, rather than squared sup norms of the losses: this is what -makes the bound useful for the unbounded but nonnegative importance-weighted loss estimates of -Exp3 [LS, Section 11.3]. This bound and its form for nonincreasing learning rates -(`softmax_regret_le`, `softmax_regret_le_of_antitone`) are proved in -`LMLExplore.OnlineLearning.Simplex`, through follow the regularized leader with the negative -entropy. +The analysis of exponential weights rests on the *mix loss* +`mixLoss η w ℓ = -(1/η) log ∑ a, w a exp (-η ℓ a)` of a loss vector `ℓ` under weights `w`, and on +the potential `hedgePotential η L = -(1/η) log ((1/k) ∑ a, exp (-η L a))` of a cumulative loss +vector `L`, with `k` the cardinality of `α`. The mix loss of the weights `softmax (-(η • L))` is the +increment of the potential from `L` to `L + ℓ`, and the potential is nonincreasing in `η`, so for +nonincreasing learning rates `η t` the mix losses of the weights +`p t = softmax (-(η t • ∑ s < t, y s))` telescope: their sum is at most the potential at the last +learning rate, which is at most the cumulative loss of every coordinate plus `log k / η (n - 1)` +[dRvEGK14, Section 2]. The regret is therefore at most `log k / η (n - 1)` plus the sum of the +*mixability gaps* `⟨p t, y t⟩ - mixLoss (η t) (p t) (y t)`, with `⟨p, y⟩ = ∑ b, p b * y b`. Since +`log x ≤ x - 1`, the mixability gap is at most `(∑ b, p b * (exp (-(η * y b)) - 1 + η * y b)) / η`. + +For nonnegative losses this gives the local-norm bound +`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η (n - 1) + ∑ t < n, η t / 2 * ⟨p t, (y t) ^ 2⟩` +against every coordinate `a`. The second-order terms are averages under the played weights, rather +than squared sup norms of the losses: this is what makes the bound useful for the unbounded but +nonnegative importance-weighted loss estimates of Exp3 [LS, Section 11.3]. For losses that may be +negative but satisfy `η t * y t a ≥ -1`, such as the loss estimates of adversarial linear bandits, +`exp (-x) ≤ 1 - x + x ^ 2` for `x ≥ -1` gives the same bound with `η t * ⟨p t, (y t) ^ 2⟩` in place +of `η t / 2 * ⟨p t, (y t) ^ 2⟩` [LS, proof of Theorem 27.1]. The same mix losses and potential give +the regret bound of AdaHedge (`LMLExplore.OnlineLearning.AdaHedge`), and the mixability gap is the +stability term of follow the regularized leader with the negative entropy +(`LMLExplore.OnlineLearning.Simplex`). ## Main definitions * `LMLExplore.OnlineLearning.softmax v`: the softmax (exponential weights) of `v`. +* `LMLExplore.OnlineLearning.mixLoss η w ℓ`: the mix loss `-(1/η) log ∑ a, w a exp (-η ℓ a)`. +* `LMLExplore.OnlineLearning.hedgePotential η L`: the potential + `-(1/η) log ((1/k) ∑ a, exp (-η L a))` of exponential weights. ## Main statements @@ -50,6 +67,24 @@ entropy. `η ≥ 0`, `∑ b, p b * (exp (-(η * y b)) - 1 + η * y b) ≤ η ^ 2 / 2 * ∑ b, p b * y b ^ 2`. * `sum_mul_exp_neg_sub_one_add_le_of_neg_one_le`: for nonnegative weights `p` and a loss `y` with `η * y b ≥ -1`, `∑ b, p b * (exp (-(η * y b)) - 1 + η * y b) ≤ η ^ 2 * ∑ b, p b * y b ^ 2`. +* `mixLoss_le_sum_mul`, `le_mixLoss`: the mix loss lies between the smallest loss and `⟨w, ℓ⟩`. +* `mixLoss_softmax`: the mix loss of exponential weights is the increment of the potential. +* `hedgePotential_le_of_le`: the potential is nonincreasing in the learning rate. +* `hedgePotential_le_sum_mul`: the potential is at most `⟨u, L⟩ + log k / η` for every probability + vector `u`. +* `sum_mul_sub_mixLoss_le`: the mixability gap is at most + `(∑ b, p b * (exp (-(η * y b)) - 1 + η * y b)) / η`. +* `add_mixLoss_softmax_le_hedgePotential`: one step of the telescoping of the mix losses. +* `sum_mixLoss_softmax_le_of_antitone`: with nonincreasing learning rates, the total mix loss of + exponential weights is at most the potential at the last learning rate. +* `softmax_regret_le_sum_sub_mixLoss_of_antitone`: the regret of exponential weights with + nonincreasing learning rates is at most `log k / η (n - 1)` plus the sum of the mixability gaps. +* `softmax_regret_le_sum_exp_of_antitone`: the same bound through the stability terms + `(∑ b, p b * (exp (-(η * y b)) - 1 + η * y b)) / η`. +* `softmax_regret_le_of_antitone`: the local-norm regret bound for nonnegative losses, and + `softmax_regret_le` its case of a constant learning rate. +* `softmax_regret_le_of_antitone_of_neg_one_le`, `softmax_regret_le_of_neg_one_le`: the local-norm + bound `∑ t < n, η t * ⟨p t, (y t) ^ 2⟩` for losses with `η t * y t a ≥ -1`. ## Implementation notes @@ -59,6 +94,10 @@ formalization of [SSKM26] in the paper project `RemyDegenne/Schlisselberg2026Hid ## References +* [BCB12] S. Bubeck and N. Cesa-Bianchi, *Regret analysis of stochastic and nonstochastic + multi-armed bandit problems*, Foundations and Trends in Machine Learning 5(1), 2012. +* [dRvEGK14] S. de Rooij, T. van Erven, P. D. Grünwald and W. M. Koolen, *Follow the leader if you + can, hedge if you must*, JMLR 15 (2014), Section 2. * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020. * [Ora] F. Orabona, *Online learning: a modern introduction using convex optimization*, arXiv:1912.13213v10, 2026. @@ -162,4 +201,318 @@ theorem sum_mul_exp_neg_sub_one_add_le_of_neg_one_le {p y : α → ℝ} (hp : _ ≤ p b * (η ^ 2 * y b ^ 2) := mul_le_mul_of_nonneg_left (by nlinarith) (hp b) _ = η ^ 2 * (p b * y b ^ 2) := by ring +/-! ### The mix loss and the potential of exponential weights -/ + +/-- Multiplying an inequality by `-η⁻¹` for `0 < η`: `-η⁻¹ X ≤ c ↔ -η c ≤ X`. -/ +private lemma neg_inv_mul_le_iff {η : ℝ} (hη : 0 < η) {X c : ℝ} : + -η⁻¹ * X ≤ c ↔ -η * c ≤ X := by + rw [neg_mul, neg_le, inv_mul_eq_div, le_div_iff₀ hη, neg_mul, mul_comm, neg_mul] + +/-- Multiplying an inequality by `-η⁻¹` for `0 < η`: `c ≤ -η⁻¹ X ↔ X ≤ -η c`. -/ +private lemma le_neg_inv_mul_iff {η : ℝ} (hη : 0 < η) {X c : ℝ} : + c ≤ -η⁻¹ * X ↔ X ≤ -η * c := by + rw [neg_mul, le_neg, inv_mul_eq_div, div_le_iff₀ hη, neg_mul, mul_comm, neg_mul] + +/-- The **mix loss** `-(1/η) log ∑ a, w a exp (-η ℓ a)` of the loss vector `ℓ` under the weights +`w`, at the learning rate `η`. -/ +noncomputable def mixLoss (η : ℝ) (w ℓ : α → ℝ) : ℝ := + -η⁻¹ * log (∑ a, w a * exp (-η * ℓ a)) + +lemma mixLoss_def (η : ℝ) (w ℓ : α → ℝ) : + mixLoss η w ℓ = -η⁻¹ * log (∑ a, w a * exp (-η * ℓ a)) := (rfl) + +/-- The mix loss `-(1/η) log ∑ a, w a exp (-(η ℓ a))`, with the exponent in `simp` normal form. -/ +lemma mixLoss_eq_neg_log_div (η : ℝ) (w ℓ : α → ℝ) : + mixLoss η w ℓ = -(log (∑ a, w a * exp (-(η * ℓ a))) / η) := by + simp_rw [mixLoss_def, neg_mul] + ring + +/-- The mix loss is at most the loss `⟨w, ℓ⟩` of the weights, by Jensen's inequality. -/ +lemma mixLoss_le_sum_mul {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) (ℓ : α → ℝ) : + mixLoss η w ℓ ≤ ∑ a, w a * ℓ a := by + have hw' := mem_simplex_iff.1 hw + have h := convexOn_exp.map_sum_le (t := univ) (w := w) (p := fun a ↦ -η * ℓ a) + (fun a _ ↦ hw'.1 a) hw'.2 (fun _ _ ↦ Set.mem_univ _) + simp only [smul_eq_mul] at h + have hsum : ∑ a, w a * (-η * ℓ a) = -η * ∑ a, w a * ℓ a := by + rw [Finset.mul_sum] + exact Finset.sum_congr rfl fun a _ ↦ by ring + rw [hsum] at h + rw [mixLoss_def, neg_inv_mul_le_iff hη, ← log_exp (-η * ∑ a, w a * ℓ a)] + exact log_le_log (exp_pos _) h + +/-- The mix loss of losses at least `lo` is at least `lo`. -/ +lemma le_mixLoss {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) {ℓ : α → ℝ} {lo : ℝ} + (hℓ : ∀ a, lo ≤ ℓ a) : + lo ≤ mixLoss η w ℓ := by + have hw' := mem_simplex_iff.1 hw + have hle : ∑ a, w a * exp (-η * ℓ a) ≤ exp (-η * lo) := by + calc ∑ a, w a * exp (-η * ℓ a) ≤ ∑ a, w a * exp (-η * lo) := + Finset.sum_le_sum fun a _ ↦ mul_le_mul_of_nonneg_left + (exp_le_exp.2 (by nlinarith [hℓ a])) (hw'.1 a) + _ = exp (-η * lo) := by rw [← Finset.sum_mul, hw'.2, one_mul] + have hpos := sum_mul_pos_of_mem_simplex hw fun a ↦ exp_pos (-η * ℓ a) + rw [mixLoss_def, le_neg_inv_mul_iff hη, ← log_exp (-η * lo)] + exact log_le_log hpos hle + +/-- The potential `-(1/η) log ((1/K) ∑ a, exp (-η L a))` of exponential weights with learning rate +`η` at the cumulative loss vector `L`, with `K` the cardinality of `α`. -/ +noncomputable def hedgePotential (η : ℝ) (L : α → ℝ) : ℝ := + -η⁻¹ * log ((∑ a, exp (-η * L a)) / Fintype.card α) + +lemma hedgePotential_def (η : ℝ) (L : α → ℝ) : + hedgePotential η L = -η⁻¹ * log ((∑ a, exp (-η * L a)) / Fintype.card α) := (rfl) + +/-- The potential is the mix loss of the cumulative losses under the uniform weights. -/ +lemma hedgePotential_eq_mixLoss (η : ℝ) (L : α → ℝ) : + hedgePotential η L = mixLoss η (fun _ ↦ (Fintype.card α : ℝ)⁻¹) L := by + simp_rw [hedgePotential_def, mixLoss_def, Finset.sum_div, div_eq_inv_mul] + +/-- The mix loss of the exponential weights `softmax (-(η • L))` is the increment +`Φ_η(L + ℓ) - Φ_η(L)` of the potential. -/ +lemma mixLoss_softmax [Nonempty α] (η : ℝ) (L ℓ : α → ℝ) : + mixLoss η (softmax (-(η • L))) ℓ = hedgePotential η (L + ℓ) - hedgePotential η L := by + have hZ : 0 < ∑ a, exp (-η * L a) := Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty + have hZ' : 0 < ∑ a, exp (-η * (L + ℓ) a) := Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty + have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos + have hsum : ∑ a, softmax (-(η • L)) a * exp (-η * ℓ a) = + (∑ a, exp (-η * (L + ℓ) a)) / ∑ a, exp (-η * L a) := by + rw [Finset.sum_div] + refine Finset.sum_congr rfl fun a _ ↦ ?_ + simp only [softmax_apply, Pi.neg_apply, Pi.smul_apply, smul_eq_mul, Pi.add_apply, mul_add, + neg_mul, exp_add] + ring + rw [mixLoss_def, hsum, hedgePotential_def, hedgePotential_def, log_div hZ'.ne' hZ.ne', + log_div hZ'.ne' hK.ne', log_div hZ.ne' hK.ne'] + ring + +/-- The potential is at most `L a + log K / η` for every expert `a`. -/ +lemma hedgePotential_le {η : ℝ} (hη : 0 < η) (L : α → ℝ) (a : α) : + hedgePotential η L ≤ L a + log (Fintype.card α) / η := by + have : Nonempty α := ⟨a⟩ + have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos + have hle : exp (-η * L a) ≤ ∑ b, exp (-η * L b) := + Finset.single_le_sum (f := fun b ↦ exp (-η * L b)) (fun b _ ↦ (exp_pos _).le) (mem_univ a) + have hlog : -η * L a - log (Fintype.card α) ≤ log ((∑ b, exp (-η * L b)) / Fintype.card α) := by + rw [log_div (Finset.sum_pos (fun b _ ↦ exp_pos _) univ_nonempty).ne' hK.ne', + ← log_exp (-η * L a)] + exact sub_le_sub_right (log_le_log (exp_pos _) hle) _ + rw [hedgePotential_def, neg_inv_mul_le_iff hη] + refine le_of_eq_of_le ?_ hlog + field_simp + ring + +/-- The potential is at least every lower bound of the cumulative losses. -/ +lemma le_hedgePotential [Nonempty α] {η : ℝ} (hη : 0 < η) {L : α → ℝ} {x : ℝ} + (hL : ∀ a, x ≤ L a) : + x ≤ hedgePotential η L := + hedgePotential_eq_mixLoss η L ▸ le_mixLoss (uniform_mem_simplex α) hη hL + +/-- The potential is nonincreasing in the learning rate: for `0 < η' ≤ η`, +`Φ_η(L) ≤ Φ_η'(L)`. This is the power mean inequality. -/ +lemma hedgePotential_le_of_le [Nonempty α] {η η' : ℝ} (hη' : 0 < η') (hη : η' ≤ η) + (L : α → ℝ) : + hedgePotential η L ≤ hedgePotential η' L := by + have hη0 : 0 < η := hη'.trans_le hη + have hK : (0 : ℝ) < Fintype.card α := by exact_mod_cast Fintype.card_pos + set p := η / η' with hp + have hp1 : 1 ≤ p := by rw [hp, le_div_iff₀ hη', one_mul]; exact hη + -- the power mean inequality for the weights `1/K` and the values `exp (-η' L a)` + have hmean := Real.rpow_arith_mean_le_arith_mean_rpow univ (fun _ ↦ (Fintype.card α : ℝ)⁻¹) + (fun a ↦ exp (-η' * L a)) (fun _ _ ↦ inv_nonneg.2 hK.le) + (by simp [Finset.card_univ, hK.ne']) (fun _ _ ↦ (exp_pos _).le) hp1 + have hpow (a : α) : exp (-η' * L a) ^ p = exp (-η * L a) := by + rw [← exp_mul, hp] + congr 1 + field_simp + simp only [hpow, ← Finset.mul_sum] at hmean + have hpos' : 0 < (Fintype.card α : ℝ)⁻¹ * ∑ a, exp (-η' * L a) := + mul_pos (inv_pos.2 hK) (Finset.sum_pos (fun a _ ↦ exp_pos _) univ_nonempty) + have hlog := log_le_log (rpow_pos_of_pos hpos' p) hmean + rw [log_rpow hpos'] at hlog + rw [hedgePotential_def, hedgePotential_def, div_eq_inv_mul, div_eq_inv_mul, + neg_inv_mul_le_iff hη0] + refine le_of_eq_of_le ?_ hlog + rw [hp] + field_simp + +/-- The potential of the zero cumulative loss vector is zero. -/ +@[simp] +lemma hedgePotential_zero_right (η : ℝ) : hedgePotential η (0 : α → ℝ) = 0 := by + rcases isEmpty_or_nonempty α with _ | _ <;> simp [hedgePotential_def] + +/-- The potential is at most `⟨u, L⟩ + log K / η` for every probability vector `u`, with `K` the +cardinality of `α`. -/ +lemma hedgePotential_le_sum_mul {η : ℝ} (hη : 0 < η) (L : α → ℝ) {u : α → ℝ} + (hu : u ∈ simplex α) : + hedgePotential η L ≤ ∑ a, u a * L a + log (Fintype.card α) / η := by + have := nonempty_of_mem_simplex hu + obtain ⟨hu0, hu1⟩ := mem_simplex_iff.1 hu + obtain ⟨a, ha⟩ := Finite.exists_min L + have h_min : L a ≤ ∑ b, u b * L b := + calc L a = ∑ b, u b * L a := by rw [← sum_mul, hu1, one_mul] + _ ≤ ∑ b, u b * L b := sum_le_sum fun b _ ↦ mul_le_mul_of_nonneg_left (ha b) (hu0 b) + linarith [hedgePotential_le hη L a] + +/-- **The mixability gap is at most the exponential stability term.** For a probability vector +`w`, a loss `ℓ` and a learning rate `η > 0`, the mixability gap `⟨w, ℓ⟩ - mixLoss η w ℓ` is at +most `(∑ a, w a * (exp (-(η * ℓ a)) - 1 + η * ℓ a)) / η`, since `log x ≤ x - 1`. -/ +lemma sum_mul_sub_mixLoss_le {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) + (ℓ : α → ℝ) : + ∑ a, w a * ℓ a - mixLoss η w ℓ ≤ (∑ a, w a * (exp (-(η * ℓ a)) - 1 + η * ℓ a)) / η := by + have hw1 := (mem_simplex_iff.1 hw).2 + have hZ : 0 < ∑ a, w a * exp (-(η * ℓ a)) := sum_mul_pos_of_mem_simplex hw fun a ↦ exp_pos _ + have h_log := log_le_sub_one_of_pos hZ + have h_expand : ∑ a, w a * (exp (-(η * ℓ a)) - 1 + η * ℓ a) = + ∑ a, w a * exp (-(η * ℓ a)) - 1 + η * ∑ a, w a * ℓ a := by + simp_rw [mul_add, mul_sub, mul_one, sum_add_distrib, sum_sub_distrib, hw1, mul_sum] + congr 1 + exact sum_congr rfl fun a _ ↦ by ring + rw [h_expand, mixLoss_eq_neg_log_div, sub_neg_eq_add, add_div, + mul_div_cancel_left₀ _ hη.ne', add_comm (∑ a, w a * ℓ a)] + gcongr + +/-! ### Regret of exponential weights -/ + +/-- **One step of the telescoping of the mix losses.** If `S` is at most the potential of `L` at a +learning rate `η'`, then adding the mix loss of the exponential weights `softmax (-(η • L))` at a +smaller learning rate `0 < η ≤ η'` keeps `S` below the potential of `L + ℓ` at `η`. -/ +lemma add_mixLoss_softmax_le_hedgePotential [Nonempty α] {η η' : ℝ} (hη : 0 < η) (hηη' : η ≤ η') + {S : ℝ} {L : α → ℝ} (hS : S ≤ hedgePotential η' L) (ℓ : α → ℝ) : + S + mixLoss η (softmax (-(η • L))) ℓ ≤ hedgePotential η (L + ℓ) := by + rw [mixLoss_softmax] + linarith [hedgePotential_le_of_le hη hηη' L] + +/-- **The mix losses of exponential weights telescope** [dRvEGK14, Section 2]. For losses `y t` +and nonincreasing learning rates `η t > 0`, the mix losses of the weights +`p t = softmax (-(η t • ∑ s < t, y s))` satisfy +`∑ t < n, mixLoss (η t) (p t) (y t) ≤ hedgePotential (η (n - 1)) (∑ t < n, y t)`: each mix loss is +an increment of the potential at the current learning rate, and the potential grows when the +learning rate decreases (`add_mixLoss_softmax_le_hedgePotential`). -/ +theorem sum_mixLoss_softmax_le_of_antitone [Nonempty α] {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) + (hη_anti : Antitone η) (y : ℕ → α → ℝ) (n : ℕ) : + ∑ t ∈ range n, mixLoss (η t) (softmax (-(η t • ∑ s ∈ range t, y s))) (y t) ≤ + hedgePotential (η (n - 1)) (∑ t ∈ range n, y t) := by + induction n with + | zero => simp + | succ n ih => + rw [sum_range_succ, sum_range_succ, Nat.add_sub_cancel] + exact add_mixLoss_softmax_le_hedgePotential (hη n) (hη_anti (Nat.sub_le n 1)) ih (y n) + +/-- **Regret of exponential weights with nonincreasing learning rates**, through the mixability +gaps [dRvEGK14, Section 2; Ora, Section 7.5]. For losses `y t` and nonincreasing learning rates +`η t > 0`, the weights `p t = softmax (-(η t • ∑ s < t, y s))` satisfy, against every point `u` of +the simplex, +`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + + ∑ t < n, (⟨p t, y t⟩ - mixLoss (η t) (p t) (y t))`, +with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The mixability gap +`⟨p, y⟩ - mixLoss η p y = ⟨p, y⟩ + log (∑ b, p b * exp (-(η * y b))) / η` is also the stability +term of follow the regularized leader with the negative entropy at `p`. -/ +theorem softmax_regret_le_sum_sub_mixLoss_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) + (hη_anti : Antitone η) (y : ℕ → α → ℝ) (n : ℕ) {u : α → ℝ} (hu : u ∈ simplex α) : + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ + log (Fintype.card α) / η (n - 1) + + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - + mixLoss (η t) (softmax (-(η t • ∑ s ∈ range t, y s))) (y t)) := by + have := nonempty_of_mem_simplex hu + have h_tel := sum_mixLoss_softmax_le_of_antitone hη hη_anti y n + have h_pot := hedgePotential_le_sum_mul (hη (n - 1)) (∑ t ∈ range n, y t) hu + have h_u : ∑ b, u b * (∑ t ∈ range n, y t) b = ∑ t ∈ range n, ∑ b, u b * y t b := by + simp_rw [Finset.sum_apply, mul_sum] + exact sum_comm + rw [sum_sub_distrib, sum_sub_distrib] + linarith + +/-- **Regret of exponential weights with nonincreasing learning rates**, through the exponential +stability terms [Ora, Section 7.5; BCB12, proof of Theorem 3.1]. For losses `y t` and nonincreasing +learning rates `η t > 0`, the weights `p t = softmax (-(η t • ∑ s < t, y s))` satisfy, against +every point `u` of the simplex, +`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + + ∑ t < n, (∑ b, p t b * (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t`, +with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. No sign condition on the losses is +needed; the local-norm bounds `softmax_regret_le_of_antitone` (nonnegative losses) and +`softmax_regret_le_of_antitone_of_neg_one_le` (losses with `η t * y t b ≥ -1`) bound the +stability terms. -/ +theorem softmax_regret_le_sum_exp_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) + (hη_anti : Antitone η) (y : ℕ → α → ℝ) (n : ℕ) {u : α → ℝ} (hu : u ∈ simplex α) : + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ + log (Fintype.card α) / η (n - 1) + + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * + (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t := by + have := nonempty_of_mem_simplex hu + exact (softmax_regret_le_sum_sub_mixLoss_of_antitone hη hη_anti y n hu).trans <| + add_le_add le_rfl <| sum_le_sum fun t _ ↦ + sum_mul_sub_mixLoss_le (softmax_mem_simplex _) (hη t) (y t) + + +/-- **Regret of exponential weights with nonincreasing learning rates** [Ora, Section 7.5; +BCB12, proof of Theorem 3.1]. For losses `y t` that are nonnegative at the rounds `t < n` and +nonincreasing learning rates `η t > 0`, the weights `p t = softmax (-(η t • ∑ s < t, y s))` +satisfy, against every point `u` of the simplex, +`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, η t / 2 * ⟨p t, (y t) ^ 2⟩`, +with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. -/ +theorem softmax_regret_le_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) (hη_anti : Antitone η) + {y : ℕ → α → ℝ} {n : ℕ} (hy : ∀ t < n, ∀ b, 0 ≤ y t b) {u : α → ℝ} (hu : u ∈ simplex α) : + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ + log (Fintype.card α) / η (n - 1) + + ∑ t ∈ range n, η t / 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by + refine (softmax_regret_le_sum_exp_of_antitone hη hη_anti y n hu).trans + (add_le_add le_rfl (sum_le_sum fun t ht ↦ ?_)) + rw [div_le_iff₀ (hη t)] + calc _ ≤ η t ^ 2 / 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := + sum_mul_exp_neg_sub_one_add_le (softmax_nonneg _) (hy t (mem_range.1 ht)) (hη t).le + _ = _ := by ring + +/-- **Regret of exponential weights with nonincreasing learning rates, for losses bounded +below** [LS, proof of Theorem 27.1]. For losses `y t` with +`η t * y t b ≥ -1` at the rounds `t < n` and nonincreasing learning rates `η t > 0`, the weights +`p t = softmax (-(η t • ∑ s < t, y s))` satisfy, against every point `u` of the simplex, +`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, η t * ⟨p t, (y t) ^ 2⟩`, +with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The losses may be negative, as +the loss estimates of adversarial linear bandits are. -/ +theorem softmax_regret_le_of_antitone_of_neg_one_le {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) + (hη_anti : Antitone η) {y : ℕ → α → ℝ} {n : ℕ} (hy : ∀ t < n, ∀ b, -1 ≤ η t * y t b) + {u : α → ℝ} (hu : u ∈ simplex α) : + ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ + log (Fintype.card α) / η (n - 1) + + ∑ t ∈ range n, η t * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by + refine (softmax_regret_le_sum_exp_of_antitone hη hη_anti y n hu).trans + (add_le_add le_rfl (sum_le_sum fun t ht ↦ ?_)) + rw [div_le_iff₀ (hη t)] + calc _ ≤ η t ^ 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := + sum_mul_exp_neg_sub_one_add_le_of_neg_one_le (softmax_nonneg _) (hy t (mem_range.1 ht)) + _ = _ := by ring + +/-- **Regret of exponential weights** with local norms. For losses `y t` that are nonnegative at +the rounds `t < n` and a learning rate `η > 0`, the weights `p t = softmax (-(η • ∑ s < t, y s))` +satisfy, against every coordinate `a`, +`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η + η / 2 * ∑ t < n, ⟨p t, (y t) ^ 2⟩`, +with `k` the cardinality of `α`. This is the case of a constant learning rate and a vertex of the +simplex in `softmax_regret_le_of_antitone`. -/ +theorem softmax_regret_le {η : ℝ} (hη : 0 < η) {y : ℕ → α → ℝ} {n : ℕ} + (hy : ∀ t < n, ∀ b, 0 ≤ y t b) (a : α) : + ∑ t ∈ range n, (∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b - y t a) ≤ + log (Fintype.card α) / η + + η / 2 * ∑ t ∈ range n, ∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by + classical + have h := softmax_regret_le_of_antitone (η := fun _ ↦ η) (fun _ ↦ hη) antitone_const hy + (single_mem_simplex a) + simpa [Pi.single_apply, mul_sum] using h + +/-- **Regret of exponential weights for losses bounded below** [LS, proof of Theorem 27.1]. For +losses `y t` with `η * y t b ≥ -1` at the rounds `t < n` and a learning rate `η > 0`, the weights +`p t = softmax (-(η • ∑ s < t, y s))` satisfy, against every coordinate `a`, +`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η + η * ∑ t < n, ⟨p t, (y t) ^ 2⟩`, +with `k` the cardinality of `α`. This is the case of a constant learning rate and a vertex of the +simplex in `softmax_regret_le_of_antitone_of_neg_one_le`. -/ +theorem softmax_regret_le_of_neg_one_le {η : ℝ} (hη : 0 < η) {y : ℕ → α → ℝ} {n : ℕ} + (hy : ∀ t < n, ∀ b, -1 ≤ η * y t b) (a : α) : + ∑ t ∈ range n, (∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b - y t a) ≤ + log (Fintype.card α) / η + + η * ∑ t ∈ range n, ∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by + classical + have h := softmax_regret_le_of_antitone_of_neg_one_le (η := fun _ ↦ η) (fun _ ↦ hη) + antitone_const hy (single_mem_simplex a) + simpa [Pi.single_apply, mul_sum] using h + end LMLExplore.OnlineLearning diff --git a/LMLExplore/OnlineLearning/ExponentiatedGradient.lean b/LMLExplore/OnlineLearning/ExponentiatedGradient.lean index 66591429..769cbc5c 100644 --- a/LMLExplore/OnlineLearning/ExponentiatedGradient.lean +++ b/LMLExplore/OnlineLearning/ExponentiatedGradient.lean @@ -26,9 +26,9 @@ minimum value of the objective is `-log ∑ a, w a * exp (-(η * ℓ a))`. In pa in the interior of the simplex, the steps do not change when a constant is added to the loss, and from the uniform point with a constant learning rate the exact trajectory is the sequence of exponential weights `softmax (-(η • ∑ s < t, ℓ s))`, to which the regret bounds of -`LMLExplore.OnlineLearning.Simplex` apply (for instance `softmax_regret_le`). The analysis of -mirror descent with the negative entropy and approximate steps [SSKM26, Section 5.3, Appendix D] -uses the step in this form, with the minimum value of its objective. +`LMLExplore.OnlineLearning.ExponentialWeights` apply (for instance `softmax_regret_le`). The +analysis of mirror descent with the negative entropy and approximate steps [SSKM26, Section 5.3, +Appendix D] uses the step in this form, with the minimum value of its objective. ## Main statements diff --git a/LMLExplore/OnlineLearning/Simplex.lean b/LMLExplore/OnlineLearning/Simplex.lean index 82deca9e..b8d7d0e0 100644 --- a/LMLExplore/OnlineLearning/Simplex.lean +++ b/LMLExplore/OnlineLearning/Simplex.lean @@ -30,17 +30,13 @@ point of the simplex, `R_n ≤ log k / η + η / 2 ∑ t < n, ‖y t‖ ^ 2` wit For nonnegative losses, the stability terms of exponential weights are bounded by local norms [Ora, Section 7.5; BCB12, proof of Theorem 3.1]. At a probability vector `p` with positive coordinates, the stability term `q ↦ ⟨p - q, y⟩ - D(q, p) / η`, with `D` the relative entropy -(the Bregman divergence of the negative entropy on the simplex), has maximum -`⟨p, y⟩ + log (∑ a, p a * exp (-(η * y a))) / η` over the simplex, by the Gibbs variational -principle. Since `log x ≤ x - 1` and `exp (-x) ≤ 1 - x + x ^ 2 / 2` for `x ≥ 0`, it is at most -`η / 2 * ⟨p, y ^ 2⟩`. With FTRL for nonincreasing learning rates `η t`, the weights -`p t = softmax (-(η t • ∑ s < t, y s))` then satisfy, against every point `u` of the simplex, -`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, η t / 2 * ⟨p t, (y t) ^ 2⟩`. -Its case of a constant learning rate and a vertex `u` is the bound `softmax_regret_le` used by -Exp3, Exp3-IX and Exp4. For losses that may be negative but satisfy `η t * y t a ≥ -1`, such as -the loss estimates of adversarial linear bandits, `exp (-x) ≤ 1 - x + x ^ 2` for `x ≥ -1` gives the -same bound with `η t * ⟨p t, (y t) ^ 2⟩` in place of `η t / 2 * ⟨p t, (y t) ^ 2⟩` -[LS, proof of Theorem 27.1]. +(the Bregman divergence of the negative entropy on the simplex), has maximum the mixability gap +`⟨p, y⟩ - mixLoss η p y = ⟨p, y⟩ + log (∑ a, p a * exp (-(η * y a))) / η` over the simplex, by +the Gibbs variational principle. Since `log x ≤ x - 1` and `exp (-x) ≤ 1 - x + x ^ 2 / 2` for +`x ≥ 0`, it is at most `η / 2 * ⟨p, y ^ 2⟩`. The regret bounds of exponential weights with +nonincreasing learning rates that these stability terms give (`softmax_regret_le_of_antitone` and +its relatives) are proved in `LMLExplore.OnlineLearning.ExponentialWeights` from the telescoping of +the mix losses, which needs no convex analysis. ## Main statements @@ -53,20 +49,11 @@ same bound with `η t * ⟨p t, (y t) ^ 2⟩` in place of `η t / 2 * ⟨p t, (y * `softmax_regret_le_sqrt`: the same bound for exponential weights stated on `α → ℝ`, for losses in `[-1, 1]`. * `isGreatest_sum_sub_mul_sub_sum_mul_log_div_div`: the maximum over the simplex of the stability - term of exponential weights at `p`. + term of exponential weights at `p` is the mixability gap. * `sum_sub_mul_sub_sum_mul_log_div_div_le`: the stability term is at most `(∑ a, p a * (exp (-(η * y a)) - 1 + η * y a)) / η`. * `sum_sub_mul_sub_sum_mul_log_div_div_le_mul_sum_mul_sq`: for a nonnegative loss `y`, the stability term is at most `η / 2 * ∑ a, p a * y a ^ 2`. -* `softmax_regret_le_sum_exp_of_antitone`: the regret bound of exponential weights with - nonincreasing learning rates through the stability terms - `(∑ a, p a * (exp (-(η * y a)) - 1 + η * y a)) / η`, for every loss. -* `softmax_regret_le_of_antitone`: the local-norm regret bound of exponential weights with - nonincreasing learning rates, for nonnegative losses. -* `softmax_regret_le`: its case of a constant learning rate, against every coordinate. -* `softmax_regret_le_of_antitone_of_neg_one_le`, `softmax_regret_le_of_neg_one_le`: the local-norm - bound `∑ t < n, η t * ⟨p t, (y t) ^ 2⟩` for losses with `η t * y t a ≥ -1`, which may be - negative. ## References @@ -259,18 +246,20 @@ private lemma sum_sub_mul_sub_sum_mul_log_div_div_eq (p q y : α → ℝ) {η : field_simp ring -/-- **The stability term of exponential weights** [Ora, Section 7.5]. For a probability vector `p` -with positive coordinates, a loss `y` and a learning rate `η > 0`, the stability term of FTRL with -the negative entropy at `p`, `q ↦ ∑ a, (p a - q a) * y a - D(q, p) / η` with -`D(q, p) = ∑ a, q a * log (q a / p a)` the relative entropy, has maximum -`∑ a, p a * y a + log (∑ a, p a * exp (-(η * y a))) / η` over the simplex. This is the Gibbs -variational principle for the vector `-(η • y)`. -/ +/-- **The stability term of exponential weights is the mixability gap** [Ora, Section 7.5]. For a +probability vector `p` with positive coordinates, a loss `y` and a learning rate `η > 0`, the +stability term of FTRL with the negative entropy at `p`, +`q ↦ ∑ a, (p a - q a) * y a - D(q, p) / η` with `D(q, p) = ∑ a, q a * log (q a / p a)` the +relative entropy, has maximum the mixability gap +`∑ a, p a * y a - mixLoss η p y = ∑ a, p a * y a + log (∑ a, p a * exp (-(η * y a))) / η` over +the simplex. This is the Gibbs variational principle for the vector `-(η • y)`. -/ theorem isGreatest_sum_sub_mul_sub_sum_mul_log_div_div {p : α → ℝ} (hp : p ∈ simplex α) (hp0 : ∀ a, 0 < p a) (y : α → ℝ) {η : ℝ} (hη : 0 < η) : IsGreatest ((fun q ↦ ∑ a, (p a - q a) * y a - (∑ a, q a * log (q a / p a)) / η) '' simplex α) - (∑ a, p a * y a + log (∑ a, p a * exp (-(η * y a))) / η) := by + (∑ a, p a * y a - mixLoss η p y) := by obtain ⟨⟨q, hq, hq_eq⟩, h_le⟩ := isGreatest_sum_mul_sub_sum_mul_log_div hp hp0 fun a ↦ -(η * y a) + rw [mixLoss_eq_neg_log_div, sub_neg_eq_add] refine ⟨⟨q, hq, ?_⟩, ?_⟩ · simp only at hq_eq ⊢ rw [sum_sub_mul_sub_sum_mul_log_div_div_eq p q y hη.ne', hq_eq] @@ -289,20 +278,14 @@ theorem sum_sub_mul_sub_sum_mul_log_div_div_le {p q : α → ℝ} (hp : p ∈ si (hq : q ∈ simplex α) (hqp : ∀ a, p a = 0 → q a = 0) (y : α → ℝ) {η : ℝ} (hη : 0 < η) : ∑ a, (p a - q a) * y a - (∑ a, q a * log (q a / p a)) / η ≤ (∑ a, p a * (exp (-(η * y a)) - 1 + η * y a)) / η := by - have hp1 := (mem_simplex_iff.1 hp).2 - have hZ : 0 < ∑ a, p a * exp (-(η * y a)) := - sum_mul_pos_of_mem_simplex hp fun a ↦ exp_pos (-(η * y a)) - -- the Gibbs variational principle and `log Z ≤ Z - 1` + -- the Gibbs variational principle bounds the stability term by the mixability gap have h_gibbs := sum_mul_sub_sum_mul_log_div_le_log_sum_mul_exp hp hq hqp fun a ↦ -(η * y a) - have h_log := log_le_sub_one_of_pos hZ - have h_expand : ∑ a, p a * (exp (-(η * y a)) - 1 + η * y a) = - ∑ a, p a * exp (-(η * y a)) - 1 + η * ∑ a, p a * y a := by - simp_rw [mul_add, mul_sub, mul_one, sum_add_distrib, sum_sub_distrib, hp1, mul_sum] - congr 1 - exact sum_congr rfl fun a _ ↦ by ring - rw [sum_sub_mul_sub_sum_mul_log_div_div_eq p q y hη.ne', h_expand, add_div, - mul_div_cancel_left₀ _ hη.ne', add_comm (∑ a, p a * y a)] - exact add_le_add (div_le_div_of_nonneg_right (h_gibbs.trans h_log) hη.le) le_rfl + have h_gap : ∑ a, (p a - q a) * y a - (∑ a, q a * log (q a / p a)) / η ≤ + ∑ a, p a * y a - mixLoss η p y := by + rw [sum_sub_mul_sub_sum_mul_log_div_div_eq p q y hη.ne', mixLoss_eq_neg_log_div, + sub_neg_eq_add] + exact add_le_add le_rfl (div_le_div_of_nonneg_right h_gibbs hη.le) + exact h_gap.trans (sum_mul_sub_mixLoss_le hp hη y) /-- **Local-norm stability of exponential weights** [Ora, Section 7.5; BCB12, proof of Theorem 3.1]. For probability vectors `p` and `q` with `q a = 0` whenever `p a = 0`, a nonnegative @@ -321,157 +304,4 @@ theorem sum_sub_mul_sub_sum_mul_log_div_div_le_mul_sum_mul_sq {p q : α → ℝ} _ ≤ (η ^ 2 / 2 * ∑ a, p a * y a ^ 2) / η := div_le_div_of_nonneg_right h_sq hη.le _ = _ := h_div -/-- **Regret of exponential weights with nonincreasing learning rates**, through the exponential -stability terms [Ora, Section 7.5; BCB12, proof of Theorem 3.1]. For losses `y t` and nonincreasing -learning rates `η t > 0`, the weights `p t = softmax (-(η t • ∑ s < t, y s))` satisfy, against -every point `u` of the simplex, -`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) - + ∑ t < n, (∑ b, p t b * (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t`, -with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The weights are the plays of FTRL -on the simplex with the negative entropy and the rates `η t`. No sign condition on the losses is -needed; the local-norm bounds `softmax_regret_le_of_antitone` (nonnegative losses) and -`softmax_regret_le_of_antitone_of_neg_one_le` (losses with `η t * y t b ≥ -1`) bound the -stability terms. -/ -theorem softmax_regret_le_sum_exp_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) - (hη_anti : Antitone η) (y : ℕ → α → ℝ) (n : ℕ) {u : α → ℝ} (hu : u ∈ simplex α) : - ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ - log (Fintype.card α) / η (n - 1) + - ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * - (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t := by - classical - have := nonempty_of_mem_simplex hu - have h_log : 0 ≤ log (Fintype.card α) := log_natCast_nonneg _ - set p : ℕ → α → ℝ := fun t ↦ softmax (-(η t • ∑ s ∈ range t, y s)) with hp_def - have hp_mem (t : ℕ) : p t ∈ simplex α := softmax_mem_simplex _ - have hp_pos (t : ℕ) (c : α) : 0 < p t c := softmax_pos _ c - -- the stability terms `(∑ b, p t b * (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t` - set B : ℕ → ℝ := fun t ↦ (∑ b, p t b * (exp (-(η t * y t b)) - 1 + η t * y t b)) / η t - with hB_def - rcases n with _ | m - · simpa using div_nonneg h_log (hη 0).le - -- the losses as linear functionals on `PiLp 1 (fun _ : α ↦ ℝ)` - set Y : ℕ → PiLp 1 (fun _ : α ↦ ℝ) →L[ℝ] ℝ := - fun t ↦ ∑ b, y t b • PiLp.proj (𝕜 := ℝ) 1 (fun _ : α ↦ ℝ) b - have hY_apply (t : ℕ) (x : PiLp 1 fun _ : α ↦ ℝ) : Y t x = ∑ b, y t b * x b := by - simp [Y] - have hY_single (t : ℕ) : (fun c ↦ Y t (PiLp.single 1 c 1)) = y t := - funext fun c ↦ by simp [Y, PiLp.single_apply] - -- the exponential weights are the plays of FTRL with the negative entropy - set a : ℕ → PiLp 1 (fun _ : α ↦ ℝ) := fun t ↦ toLp 1 (p t) - have ha (t : ℕ) : - IsFTRLPlay (ofLp ⁻¹' simplex α) (fun x ↦ negEntropy (ofLp x)) (η t) Y t (a t) := by - rw [isFTRLPlay_negEntropy_iff, ofLp_toLp] - simp_rw [hY_single, hp_def] - have hF' (t : ℕ) : HasFDerivWithinAt (fun x : PiLp 1 (fun _ : α ↦ ℝ) ↦ negEntropy (ofLp x)) - (∑ c, log (a t c) • PiLp.proj (𝕜 := ℝ) 1 (fun _ : α ↦ ℝ) c) (ofLp ⁻¹' simplex α) (a t) := - (hasFDerivAt_negEntropy fun c ↦ (hp_pos t c).ne').hasFDerivWithinAt - have h := ftrl_regret_succ_le_of_antitone (n := m) strongConvexOn_negEntropy.1 hη hη_anti Y a - (fun t _ ↦ ha t) _ (fun t _ ↦ hF' t) (u := toLp 1 u) (by simpa using hu) - -- each stability term is at most `B t` - have h_stab (t : ℕ) (q : PiLp 1 fun _ : α ↦ ℝ) (hq : ofLp q ∈ simplex α) : - Y t (a t - q) - bregDiv (fun x : PiLp 1 (fun _ : α ↦ ℝ) ↦ negEntropy (ofLp x)) q (a t) - (∑ c, log (a t c) • PiLp.proj (𝕜 := ℝ) 1 (fun _ : α ↦ ℝ) c) / η t ≤ B t := by - rw [bregDiv_negEntropy hq (by simpa [a] using hp_mem t) - fun c hc ↦ absurd hc (hp_pos t c).ne', hY_apply] - have h_eq : ∑ b, y t b * (a t - q) b = ∑ b, (p t b - ofLp q b) * y t b := - sum_congr rfl fun b _ ↦ by simp [a, mul_comm] - simp only [a] at h_eq ⊢ - rw [h_eq] - exact sum_sub_mul_sub_sum_mul_log_div_div_le (hp_mem t) hq - (fun c hc ↦ absurd hc (hp_pos t c).ne') (y t) (hη t) - -- the range of the negative entropy on the simplex is at most `log k` - have h_range : (negEntropy (ofLp (toLp 1 u)) - negEntropy (ofLp (a 0))) / η m ≤ - log (Fintype.card α) / η m := by - refine div_le_div_of_nonneg_right ?_ (hη m).le - rw [ofLp_toLp] - linarith [negEntropy_le_neg_one hu, neg_log_card_sub_one_le_negEntropy (hp_mem 0)] - have h_sum : ∑ t ∈ range m, (Y t (a t - a (t + 1)) - - bregDiv (fun x : PiLp 1 (fun _ : α ↦ ℝ) ↦ negEntropy (ofLp x)) (a (t + 1)) (a t) - (∑ c, log (a t c) • PiLp.proj (𝕜 := ℝ) 1 (fun _ : α ↦ ℝ) c) / η t) ≤ - ∑ t ∈ range m, B t := - sum_le_sum fun t _ ↦ h_stab t _ (by simpa [a] using hp_mem (t + 1)) - have h_last := h_stab m (toLp 1 u) (by simpa using hu) - have h_lhs : ∑ t ∈ range (m + 1), Y t (a t - toLp 1 u) = - ∑ t ∈ range (m + 1), (∑ b, p t b * y t b - ∑ b, u b * y t b) := - sum_congr rfl fun t _ ↦ by - rw [hY_apply, ← sum_sub_distrib] - exact sum_congr rfl fun b _ ↦ by simp [a]; ring - have h_goal : ∑ t ∈ range (m + 1), (∑ b, p t b * y t b - ∑ b, u b * y t b) ≤ - log (Fintype.card α) / η m + ∑ t ∈ range (m + 1), B t := by - rw [← h_lhs, sum_range_succ B m] - linarith - rw [Nat.add_sub_cancel] - simpa only [hp_def, hB_def] using h_goal - -/-- **Regret of exponential weights with nonincreasing learning rates** [Ora, Section 7.5; -BCB12, proof of Theorem 3.1]. For losses `y t` that are nonnegative at the rounds `t < n` and -nonincreasing learning rates `η t > 0`, the weights `p t = softmax (-(η t • ∑ s < t, y s))` -satisfy, against every point `u` of the simplex, -`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, η t / 2 * ⟨p t, (y t) ^ 2⟩`, -with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The weights are the plays of FTRL -on the simplex with the negative entropy and the rates `η t`. -/ -theorem softmax_regret_le_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) (hη_anti : Antitone η) - {y : ℕ → α → ℝ} {n : ℕ} (hy : ∀ t < n, ∀ b, 0 ≤ y t b) {u : α → ℝ} (hu : u ∈ simplex α) : - ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ - log (Fintype.card α) / η (n - 1) + - ∑ t ∈ range n, η t / 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by - refine (softmax_regret_le_sum_exp_of_antitone hη hη_anti y n hu).trans - (add_le_add le_rfl (sum_le_sum fun t ht ↦ ?_)) - rw [div_le_iff₀ (hη t)] - calc _ ≤ η t ^ 2 / 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := - sum_mul_exp_neg_sub_one_add_le (softmax_nonneg _) (hy t (mem_range.1 ht)) (hη t).le - _ = _ := by ring - -/-- **Regret of exponential weights with nonincreasing learning rates, for losses bounded -below** [LS, proof of Theorem 27.1]. For losses `y t` with -`η t * y t b ≥ -1` at the rounds `t < n` and nonincreasing learning rates `η t > 0`, the weights -`p t = softmax (-(η t • ∑ s < t, y s))` satisfy, against every point `u` of the simplex, -`∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, η t * ⟨p t, (y t) ^ 2⟩`, -with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The losses may be negative, as -the loss estimates of adversarial linear bandits are. -/ -theorem softmax_regret_le_of_antitone_of_neg_one_le {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) - (hη_anti : Antitone η) {y : ℕ → α → ℝ} {n : ℕ} (hy : ∀ t < n, ∀ b, -1 ≤ η t * y t b) - {u : α → ℝ} (hu : u ∈ simplex α) : - ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ - log (Fintype.card α) / η (n - 1) + - ∑ t ∈ range n, η t * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by - refine (softmax_regret_le_sum_exp_of_antitone hη hη_anti y n hu).trans - (add_le_add le_rfl (sum_le_sum fun t ht ↦ ?_)) - rw [div_le_iff₀ (hη t)] - calc _ ≤ η t ^ 2 * ∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b ^ 2 := - sum_mul_exp_neg_sub_one_add_le_of_neg_one_le (softmax_nonneg _) (hy t (mem_range.1 ht)) - _ = _ := by ring - -/-- **Regret of exponential weights** with local norms. For losses `y t` that are nonnegative at -the rounds `t < n` and a learning rate `η > 0`, the weights `p t = softmax (-(η • ∑ s < t, y s))` -satisfy, against every coordinate `a`, -`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η + η / 2 * ∑ t < n, ⟨p t, (y t) ^ 2⟩`, -with `k` the cardinality of `α`. This is the case of a constant learning rate and a vertex of the -simplex in `softmax_regret_le_of_antitone`. -/ -theorem softmax_regret_le {η : ℝ} (hη : 0 < η) {y : ℕ → α → ℝ} {n : ℕ} - (hy : ∀ t < n, ∀ b, 0 ≤ y t b) (a : α) : - ∑ t ∈ range n, (∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b - y t a) ≤ - log (Fintype.card α) / η + - η / 2 * ∑ t ∈ range n, ∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by - classical - have h := softmax_regret_le_of_antitone (η := fun _ ↦ η) (fun _ ↦ hη) antitone_const hy - (single_mem_simplex a) - simpa [Pi.single_apply, mul_sum] using h - -/-- **Regret of exponential weights for losses bounded below** [LS, proof of Theorem 27.1]. For -losses `y t` with `η * y t b ≥ -1` at the rounds `t < n` and a learning rate `η > 0`, the weights -`p t = softmax (-(η • ∑ s < t, y s))` satisfy, against every coordinate `a`, -`∑ t < n, (⟨p t, y t⟩ - y t a) ≤ log k / η + η * ∑ t < n, ⟨p t, (y t) ^ 2⟩`, -with `k` the cardinality of `α`. This is the case of a constant learning rate and a vertex of the -simplex in `softmax_regret_le_of_antitone_of_neg_one_le`. -/ -theorem softmax_regret_le_of_neg_one_le {η : ℝ} (hη : 0 < η) {y : ℕ → α → ℝ} {n : ℕ} - (hy : ∀ t < n, ∀ b, -1 ≤ η * y t b) (a : α) : - ∑ t ∈ range n, (∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b - y t a) ≤ - log (Fintype.card α) / η + - η * ∑ t ∈ range n, ∑ b, softmax (-(η • ∑ s ∈ range t, y s)) b * y t b ^ 2 := by - classical - have h := softmax_regret_le_of_antitone_of_neg_one_le (η := fun _ ↦ η) (fun _ ↦ hη) - antitone_const hy (single_mem_simplex a) - simpa [Pi.single_apply, mul_sum] using h - end LMLExplore.OnlineLearning From 72dbf994c267cf397785cc78f6e1d5e484f0413c Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 07:09:19 +0100 Subject: [PATCH 2/3] doc: describe the mixability gap as the maximum of the FTRL stability term Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/ExponentialWeights.lean | 12 +++++++----- LMLExplore/OnlineLearning/Simplex.lean | 5 +++-- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/LMLExplore/OnlineLearning/ExponentialWeights.lean b/LMLExplore/OnlineLearning/ExponentialWeights.lean index c0232529..87004ba6 100644 --- a/LMLExplore/OnlineLearning/ExponentialWeights.lean +++ b/LMLExplore/OnlineLearning/ExponentialWeights.lean @@ -43,9 +43,10 @@ nonnegative importance-weighted loss estimates of Exp3 [LS, Section 11.3]. For l negative but satisfy `η t * y t a ≥ -1`, such as the loss estimates of adversarial linear bandits, `exp (-x) ≤ 1 - x + x ^ 2` for `x ≥ -1` gives the same bound with `η t * ⟨p t, (y t) ^ 2⟩` in place of `η t / 2 * ⟨p t, (y t) ^ 2⟩` [LS, proof of Theorem 27.1]. The same mix losses and potential give -the regret bound of AdaHedge (`LMLExplore.OnlineLearning.AdaHedge`), and the mixability gap is the -stability term of follow the regularized leader with the negative entropy -(`LMLExplore.OnlineLearning.Simplex`). +the regret bound of AdaHedge (`LMLExplore.OnlineLearning.AdaHedge`), and the mixability gap at `p` +is the maximum over the simplex of the stability term of follow the regularized leader with the +negative entropy at `p`, by the Gibbs variational principle +(`isGreatest_sum_sub_mul_sub_sum_mul_log_div_div` in `LMLExplore.OnlineLearning.Simplex`). ## Main definitions @@ -406,8 +407,9 @@ the simplex, `∑ t < n, (⟨p t, y t⟩ - ⟨u, y t⟩) ≤ log k / η (n - 1) + ∑ t < n, (⟨p t, y t⟩ - mixLoss (η t) (p t) (y t))`, with `k` the cardinality of `α` and `⟨p, y⟩ = ∑ b, p b * y b`. The mixability gap -`⟨p, y⟩ - mixLoss η p y = ⟨p, y⟩ + log (∑ b, p b * exp (-(η * y b))) / η` is also the stability -term of follow the regularized leader with the negative entropy at `p`. -/ +`⟨p, y⟩ - mixLoss η p y = ⟨p, y⟩ + log (∑ b, p b * exp (-(η * y b))) / η` is also the maximum +over the simplex of the stability term of follow the regularized leader with the negative entropy +at `p`, by the Gibbs variational principle (`isGreatest_sum_sub_mul_sub_sum_mul_log_div_div`). -/ theorem softmax_regret_le_sum_sub_mixLoss_of_antitone {η : ℕ → ℝ} (hη : ∀ t, 0 < η t) (hη_anti : Antitone η) (y : ℕ → α → ℝ) (n : ℕ) {u : α → ℝ} (hu : u ∈ simplex α) : ∑ t ∈ range n, (∑ b, softmax (-(η t • ∑ s ∈ range t, y s)) b * y t b - ∑ b, u b * y t b) ≤ diff --git a/LMLExplore/OnlineLearning/Simplex.lean b/LMLExplore/OnlineLearning/Simplex.lean index b8d7d0e0..3245f7e9 100644 --- a/LMLExplore/OnlineLearning/Simplex.lean +++ b/LMLExplore/OnlineLearning/Simplex.lean @@ -36,7 +36,7 @@ the Gibbs variational principle. Since `log x ≤ x - 1` and `exp (-x) ≤ 1 - x `x ≥ 0`, it is at most `η / 2 * ⟨p, y ^ 2⟩`. The regret bounds of exponential weights with nonincreasing learning rates that these stability terms give (`softmax_regret_le_of_antitone` and its relatives) are proved in `LMLExplore.OnlineLearning.ExponentialWeights` from the telescoping of -the mix losses, which needs no convex analysis. +the mix losses, which needs neither FTRL nor Bregman divergences. ## Main statements @@ -246,7 +246,8 @@ private lemma sum_sub_mul_sub_sum_mul_log_div_div_eq (p q y : α → ℝ) {η : field_simp ring -/-- **The stability term of exponential weights is the mixability gap** [Ora, Section 7.5]. For a +/-- **The maximum of the stability term of exponential weights is the mixability gap** +[Ora, Section 7.5]. For a probability vector `p` with positive coordinates, a loss `y` and a learning rate `η > 0`, the stability term of FTRL with the negative entropy at `p`, `q ↦ ∑ a, (p a - q a) * y a - D(q, p) / η` with `D(q, p) = ∑ a, q a * log (q a / p a)` the From 43b6899c52ca81713d8667285a03b102d0d66c04 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 14 Nov 2026 07:58:47 +0100 Subject: [PATCH 3/3] refactor: state the mix loss inequalities as iff lemmas, used by AdaHedge Co-Authored-By: Claude Code --- LMLExplore/OnlineLearning/AdaHedge.lean | 3 +-- LMLExplore/OnlineLearning/ExponentialWeights.lean | 14 ++++++++++++-- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/LMLExplore/OnlineLearning/AdaHedge.lean b/LMLExplore/OnlineLearning/AdaHedge.lean index 29d9e955..f3b5130e 100644 --- a/LMLExplore/OnlineLearning/AdaHedge.lean +++ b/LMLExplore/OnlineLearning/AdaHedge.lean @@ -79,8 +79,7 @@ lemma. -/ lemma sum_mul_le_mixLoss_add {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) {ℓ : α → ℝ} {lo hi : ℝ} (hℓ : ∀ a, ℓ a ∈ Set.Icc lo hi) : ∑ a, w a * ℓ a ≤ mixLoss η w ℓ + η * (hi - lo) ^ 2 / 8 := by - rw [← sub_le_iff_le_add, mixLoss_def, ← inv_neg, ← div_eq_inv_mul, - le_div_iff_of_neg (neg_lt_zero.2 hη)] + rw [← sub_le_iff_le_add, le_mixLoss_iff hη] exact (log_sum_mul_exp_le hw hℓ (-η)).trans_eq (by ring) /-! ### Follow the leader -/ diff --git a/LMLExplore/OnlineLearning/ExponentialWeights.lean b/LMLExplore/OnlineLearning/ExponentialWeights.lean index 87004ba6..24a9ef0c 100644 --- a/LMLExplore/OnlineLearning/ExponentialWeights.lean +++ b/LMLExplore/OnlineLearning/ExponentialWeights.lean @@ -228,6 +228,16 @@ lemma mixLoss_eq_neg_log_div (η : ℝ) (w ℓ : α → ℝ) : simp_rw [mixLoss_def, neg_mul] ring +/-- For `0 < η`, the mix loss is at most `c` iff `-η c ≤ log ∑ a, w a exp (-η ℓ a)`. -/ +lemma mixLoss_le_iff {η : ℝ} (hη : 0 < η) {w ℓ : α → ℝ} {c : ℝ} : + mixLoss η w ℓ ≤ c ↔ -η * c ≤ log (∑ a, w a * exp (-η * ℓ a)) := by + rw [mixLoss_def, neg_inv_mul_le_iff hη] + +/-- For `0 < η`, the mix loss is at least `c` iff `log ∑ a, w a exp (-η ℓ a) ≤ -η c`. -/ +lemma le_mixLoss_iff {η : ℝ} (hη : 0 < η) {w ℓ : α → ℝ} {c : ℝ} : + c ≤ mixLoss η w ℓ ↔ log (∑ a, w a * exp (-η * ℓ a)) ≤ -η * c := by + rw [mixLoss_def, le_neg_inv_mul_iff hη] + /-- The mix loss is at most the loss `⟨w, ℓ⟩` of the weights, by Jensen's inequality. -/ lemma mixLoss_le_sum_mul {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < η) (ℓ : α → ℝ) : mixLoss η w ℓ ≤ ∑ a, w a * ℓ a := by @@ -239,7 +249,7 @@ lemma mixLoss_le_sum_mul {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (h rw [Finset.mul_sum] exact Finset.sum_congr rfl fun a _ ↦ by ring rw [hsum] at h - rw [mixLoss_def, neg_inv_mul_le_iff hη, ← log_exp (-η * ∑ a, w a * ℓ a)] + rw [mixLoss_le_iff hη, ← log_exp (-η * ∑ a, w a * ℓ a)] exact log_le_log (exp_pos _) h /-- The mix loss of losses at least `lo` is at least `lo`. -/ @@ -253,7 +263,7 @@ lemma le_mixLoss {w : α → ℝ} (hw : w ∈ simplex α) {η : ℝ} (hη : 0 < (exp_le_exp.2 (by nlinarith [hℓ a])) (hw'.1 a) _ = exp (-η * lo) := by rw [← Finset.sum_mul, hw'.2, one_mul] have hpos := sum_mul_pos_of_mem_simplex hw fun a ↦ exp_pos (-η * ℓ a) - rw [mixLoss_def, le_neg_inv_mul_iff hη, ← log_exp (-η * lo)] + rw [le_mixLoss_iff hη, ← log_exp (-η * lo)] exact log_le_log hpos hle /-- The potential `-(1/η) log ((1/K) ∑ a, exp (-η L a))` of exponential weights with learning rate