diff --git a/LMLExplore/OnlineLearning/AdaHedge.lean b/LMLExplore/OnlineLearning/AdaHedge.lean index 4e2ce293..f3b5130e 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,16 @@ 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, le_mixLoss_iff 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 +389,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 +408,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..24a9ef0c 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,37 @@ 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 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 * `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 +68,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 +95,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 +202,329 @@ 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 + +/-- 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 + 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_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 [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 +`η` 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 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) ≤ + 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..3245f7e9 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 neither FTRL nor Bregman divergences. ## 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,21 @@ 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 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 +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 +279,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 +305,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