diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index ef058a9c..4c9ec112 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,6 +1,7 @@ module -- shake: keep-all --deprecated_module: ignore public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.MVT public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule @@ -50,6 +51,37 @@ public import LeanMachineLearning.Online.Bandit.BayesRegret public import LeanMachineLearning.Online.Bandit.Regret public import LeanMachineLearning.Online.Bandit.RewardByCountMeasure public import LeanMachineLearning.Online.Bandit.SumRewards +public import LeanMachineLearning.Online.OnlineConvexOptimization.Algorithms.COMD.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.Algorithms.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.Algorithms.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Boundary +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Formula +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Optimality +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.RegretBound +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Domain +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Stability +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Boundary +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Formula +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Optimality +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.RegretBound +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Boundary +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Optimality +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Pathlength +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.RegretBound +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Stability +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.Boundary +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.Optimality +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.RegretBound +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.RegretDecomposition public import LeanMachineLearning.SequentialLearning.ActionIndicator public import LeanMachineLearning.SequentialLearning.Algorithm public import LeanMachineLearning.SequentialLearning.AlgorithmDensity diff --git a/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/MVT.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/MVT.lean new file mode 100644 index 00000000..e54b4c85 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/MVT.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.Calculus.Deriv.MeanValue +public import Mathlib.Analysis.Calculus.Deriv.AffineMap +public import Mathlib.Analysis.Calculus.Deriv.Pow +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic + +/-! +# Second-Order Mean Value Theorem for Bregman Divergences + +This file provides the second-order Mean Value Theorem (Lagrange remainder form) +for generalized Bregman divergences `D_[f](x, y, J)`: + +* `exists_repeated_rolle`: Repeated Rolle's Theorem for an `n`-th order sequence of derivatives. +* `bregDiv_mvt`: If `f` is twice differentiable along + `segment ℝ x y`, then there exists `z ∈ segment ℝ x y` such that + `D_[f](x, y, f' y) = 1/2 * f'' z (x - y) (x - y)`. +-/ + +@[expose] public section + +/-- NOTE: This lemma is a general 1D calculus result and should probably go +to `Mathlib.Analysis.Calculus.Deriv.MeanValue`. -/ +lemma exists_repeated_rolle (n : ℕ) {g : Fin (n + 2) → (ℝ → ℝ)} {b : ℝ} (hb : 0 < b) + (hg_diff : ∀ k : Fin (n + 1), ∀ t ∈ Set.Icc 0 b, HasDerivAt (g k.castSucc) (g k.succ t) t) + (hg_zero : ∀ k : Fin (n + 1), g k.castSucc 0 = 0) + (hgb : g 0 b = 0) : + ∃ c ∈ Set.Ioo 0 b, g (Fin.last (n + 1)) c = 0 := by + obtain ⟨c1, hc1, hc1_eq⟩ := exists_hasDerivAt_eq_zero hb + (fun t ht ↦ (hg_diff 0 t ht).continuousAt.continuousWithinAt) + ((hg_zero 0).trans hgb.symm) + (fun t ht ↦ hg_diff 0 t (Set.Ioo_subset_Icc_self ht)) + cases n with + | zero => exact ⟨c1, hc1, hc1_eq⟩ + | succ n => + obtain ⟨c, hc, hc_eq⟩ := exists_repeated_rolle n (g := fun k ↦ g k.succ) hc1.1 + (fun k t ht ↦ hg_diff k.succ t ⟨ht.1, ht.2.trans (le_of_lt hc1.2)⟩) + (fun k ↦ hg_zero k.succ) hc1_eq + exact ⟨c, ⟨hc.1, hc.2.trans hc1.2⟩, hc_eq⟩ + +open scoped Bregman + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +theorem bregDiv_mvt + {f : E → ℝ} {f' : E → (E →L[ℝ] ℝ)} {f'' : E → (E →L[ℝ] (E →L[ℝ] ℝ))} + (x y : E) + (hf' : ∀ z ∈ segment ℝ x y, HasFDerivAt f (f' z) z) + (hf'' : ∀ z ∈ segment ℝ x y, HasFDerivAt f' (f'' z) z) : + ∃ z ∈ segment ℝ x y, + D_[f](x, y, f' y) = (1/2 : ℝ) * (f'' z (x - y)) (x - y) := by + have hp {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) : AffineMap.lineMap y x t ∈ segment ℝ x y := by + rw [segment_symm]; exact lineMap_mem_segment (𝕜 := ℝ) y x ht + let D := D_[f](x, y, f' y) + let g (k : Fin 3) (t : ℝ) : ℝ := match k with + | 0 => f (AffineMap.lineMap y x t) - f y - t * f' y (x - y) - t^2 * D + | 1 => f' (AffineMap.lineMap y x t) (x - y) - f' y (x - y) - 2 * t * D + | 2 => f'' (AffineMap.lineMap y x t) (x - y) (x - y) - 2 * D + obtain ⟨c, hc, hc_eq⟩ := exists_repeated_rolle 1 (g := g) zero_lt_one + (by intro k t ht + fin_cases k + · exact (by ring : f' (AffineMap.lineMap y x t) (x - y) - 1 * f' y (x - y) - + 2 * t ^ (2 - 1) * D = g 1 t) ▸ + ((((hf' _ (hp ht)).comp_hasDerivAt t AffineMap.hasDerivAt_lineMap).sub_const + (f y)).sub + ((hasDerivAt_id t).mul_const (f' y (x - y))) |>.sub + ((hasDerivAt_pow 2 t).mul_const D)) + · exact (by ring : f'' (AffineMap.lineMap y x t) (x - y) (x - y) - 2 * 1 * D = g 2 t) ▸ + (((ContinuousLinearMap.apply ℝ ℝ (x - y)).hasFDerivAt.comp_hasDerivAt t + ((hf'' _ (hp ht)).comp_hasDerivAt t AffineMap.hasDerivAt_lineMap)).sub_const + (f' y (x - y)) |>.sub + ((hasDerivAt_id t |>.const_mul 2).mul_const D))) + (by intro k; fin_cases k <;> simp [g]) + (by simp [g, D, bregDiv]) + exact ⟨AffineMap.lineMap y x c, hp (Set.Ioo_subset_Icc_self hc), + by linarith [show g 2 c = 0 from hc_eq]⟩ diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD/RegretDecomposition.lean new file mode 100644 index 00000000..e17e2c44 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD/RegretDecomposition.lean @@ -0,0 +1,132 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.Normed.Module.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic + +/-! +# Master Regret Decomposition for Centered Online Mirror Descent (COMD) + +This file establishes the exact multi-round algebraic regret decomposition for Centered +Online Mirror Descent (COMD) following Lemma A.1.1 (Strong Centered Mirror Descent Lemma) +from Andrew Jacobsen's thesis, *Adapting to Non-Stationarity in Online Learning*. + +## Main definitions +* `boundary` +* `linearization` +* `pathlength` +* `stability` +* `optimality` +* `centering` +* `adjustment` +* `shift` + +## Main results +* `regret_decomposition_eq`: The master multi-round algebraic regret equality holding + for all $T \ge 0$. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace OnlineConvexOptimization.COMD + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-! ### Auxiliary Term Definitions -/ + +section AuxTerms + +variable (η : ℝ) +variable (ψ φ : ℕ → E → ℝ) +variable (gψ gφ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u w w_tilde : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- Boundary term comprising initial and final Bregman divergences anchored at $\tilde{w}_1$: +$$D_{\psi_{T+1}}(u_T,\tilde w_1,g\psi_{T+1}(\tilde w_1)) + - D_{\psi_{T+1}}(u_T,\tilde w_{T+1},g\psi_{T+1}(\tilde w_{T+1})).$$ -/ +def boundary (T : ℕ) : ℝ := + D_[ψ (T + 1)](u T, w_tilde 1, gψ (T + 1) (w_tilde 1)) + - D_[ψ (T + 1)](u T, w_tilde (T + 1), gψ (T + 1) (w_tilde (T + 1))) + +/-- Linearization slack from replacing $l_t$ with $g_t$: $-D_{l_t}(u_t, w_{t+1}, g_t)$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u t, w (t + 1), g t) + +/-- Regret budget for varying comparator: +$$(g\psi_t(\tilde w_t) - g\psi_t(\tilde w_1))(u_{t-1} - u_t).$$ -/ +def pathlength (t : ℕ) : ℝ := + (gψ t (w_tilde t) - gψ t (w_tilde 1)) (u (t - 1) - u t) + +/-- One-round stability penalty balancing the movement of the loss `l_t` between +the anchor `w̃_t` and iterate `w_{t+1}` against the divergence regularizer step: +$$\eta\,(l_t(\tilde w_t) - l_t(w_{t+1})) + - D_{\psi_t}(w_{t+1}, \tilde w_t, g\psi_t(\tilde w_t)).$$ -/ +def stability (t : ℕ) : ℝ := + η * (l t (w_tilde t) - l t (w (t + 1))) - D_[ψ t](w (t + 1), w_tilde t, gψ t (w_tilde t)) + +/-- Encodes the update implicitly via first-order optimality conditions: +$$(\eta\,g_t + g\varphi_t(w_{t+1}) + g\psi_{t+1}(w_{t+1}) - g\psi_t(\tilde w_t) + - g\psi_{t+1}(\tilde w_1) + g\psi_t(\tilde w_1))(u_t - w_{t+1}).$$ +$\text{optimality}(t) \le 0$ when $w_{t+1}$ satisfies first-order optimality +anchored at $\tilde{w}_1$. -/ +def optimality (t : ℕ) : ℝ := + ((η : ℝ) • g t + gφ t (w (t + 1)) + gψ (t + 1) (w (t + 1)) - gψ t (w_tilde t) + - gψ (t + 1) (w_tilde 1) + gψ t (w_tilde 1)) (u t - w (t + 1)) + +/-- Surplus contribution induced by the centering potential `φ_t`: +$$\varphi_t(u_t) - \varphi_t(w_{t+1}) - D_{\varphi_t}(u_t, w_{t+1}, g\varphi_t(w_{t+1})).$$ +Zero when no centering is used (`φ_t = 0`). -/ +def centering (t : ℕ) : ℝ := + φ t (u t) - φ t (w (t + 1)) - D_[φ t](u t, w (t + 1), gφ t (w (t + 1))) + +/-- Divergence drift capturing arbitrary post-processing or state adjustments +from iterate `w_{t+1}` to anchor `w̃_{t+1}`: +$$D_{\psi_{t+1}}(u_t,\tilde w_{t+1},g\psi_{t+1}(\tilde w_{t+1})) + - D_{\psi_{t+1}}(u_t,w_{t+1},g\psi_{t+1}(w_{t+1})).$$ +Vanishes for unadjusted or projection-free +updates (`w̃_{t+1} = w_{t+1}`), and yields small controllable penalties for schemes +like Fixed Share. -/ +def adjustment (t : ℕ) : ℝ := + D_[ψ (t+1)](u t, w_tilde (t + 1), gψ (t+1) (w_tilde (t + 1))) + - D_[ψ (t+1)](u t, w (t + 1), gψ (t+1) (w (t + 1))) + +/-- Regularizer shift evaluated on iterate $w_{t+1}$ anchored at initial state $\tilde{w}_1$: +$$D_{\psi_{t+1} - \psi_t}(w_{t+1}, \tilde w_1, g\psi_{t+1}(\tilde w_1) - g\psi_t(\tilde w_1)).$$ -/ +def shift (t : ℕ) : ℝ := + D_[ψ (t + 1) - ψ t](w (t + 1), w_tilde 1, gψ (t + 1) (w_tilde 1) - gψ t (w_tilde 1)) + +/-! ### Strong Centered Regret Decomposition (Jacobsen) -/ + +/-- Master Centered Online Mirror Descent Regret Decomposition Identity +(Andrew Jacobsen, *Adapting to Non-Stationarity in Online Learning*, Lemma A.1.1). -/ +theorem regret_decomposition_eq (T : ℕ) : + η * (∑ t ∈ Ico 1 (T + 1), (l t (w_tilde t) - l t (u t))) = + boundary ψ gψ u w_tilde T + + (∑ t ∈ Ico 1 (T + 1), adjustment ψ gψ u w w_tilde t) + + (∑ t ∈ Ico 1 (T + 1), pathlength gψ u w_tilde t) + + (∑ t ∈ Ico 1 (T + 1), stability η ψ gψ w w_tilde l t) + - (∑ t ∈ Ico 1 (T + 1), shift ψ gψ w w_tilde t) + - (∑ t ∈ Ico 1 (T + 1), optimality η gψ gφ u w w_tilde g t) + + (∑ t ∈ Ico 1 (T + 1), centering φ gφ u w t) + + η * (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) := by + induction T with + | zero => simp [boundary] + | succ T ih => + simp_rw [Finset.sum_Ico_succ_top (by omega : 1 ≤ T + 1), mul_add, ih] + dsimp [boundary, optimality, adjustment, pathlength, stability, centering, + shift, linearization, bregDiv] + simp only [map_sub, add_apply, sub_apply, smul_apply, smul_eq_mul] + ring + +end AuxTerms + +end OnlineConvexOptimization.COMD diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD2/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD2/RegretDecomposition.lean new file mode 100644 index 00000000..f8225aad --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/COMD2/RegretDecomposition.lean @@ -0,0 +1,134 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.Normed.Module.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic + +/-! +# Master Regret Decomposition for Centered Online Mirror Descent (COMD2) + +This file establishes the exact multi-round algebraic regret decomposition for Centered +Online Mirror Descent (version 2) with pure potential shifts and direct regularizer updates, +as a variation of Lemma A.1.1 (Strong Centered Mirror Descent Lemma) from Andrew Jacobsen's thesis, +*Adapting to Non-Stationarity in Online Learning*. + +The regret decomposition holds for any sequence of comparators `u_t` and any sequence +of centering potentials `φ_t`. Specializations (e.g. static regret `u_t = u`, or uncentered +settings `φ_t = 0`) are derived as corollaries in separate modules. + +## Main definitions +* `boundary` +* `linearization` +* `pathlength` +* `stability` +* `optimality` +* `centering` +* `adjustment` +* `shift` + +## Main results +* `regret_decomposition_eq`: The master multi-round algebraic regret equality holding + for all $T \ge 0$. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace OnlineConvexOptimization.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +/-! ### Auxiliary Term Definitions -/ + +section AuxTerms + +variable (η : ℝ) +variable (ψ φ : ℕ → E → ℝ) +variable (gψ gφ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u w w_tilde : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- Boundary term comprising initial and final Bregman divergences anchored at $\tilde{w}_1$: +$$D_{\psi_1}(u_0,\tilde w_1,g\psi_1(\tilde w_1)) + - D_{\psi_{T+1}}(u_T,\tilde w_{T+1},g\psi_{T+1}(\tilde w_{T+1})) + + \psi_{T+1}(u_T) - \psi_1(u_0).$$ -/ +def boundary (T : ℕ) : ℝ := + D_[ψ 1](u 0, w_tilde 1, gψ 1 (w_tilde 1)) + - D_[ψ (T + 1)](u T, w_tilde (T + 1), gψ (T + 1) (w_tilde (T + 1))) + + ψ (T + 1) (u T) - ψ 1 (u 0) + +/-- Linearization slack from replacing $l_t$ with $g_t$: $-D_{l_t}(u_t, w_{t+1}, g_t)$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u t, w (t + 1), g t) + +/-- Regret budget for varying comparator: +$$(g\psi_t(\tilde w_t))(u_{t-1} - u_t).$$ -/ +def pathlength (t : ℕ) : ℝ := + gψ t (w_tilde t) (u (t - 1) - u t) + +/-- One-round stability penalty balancing the movement of the loss `l_t` between +the anchor `w̃_t` and iterate `w_{t+1}` against the divergence regularizer step: +$$\eta\,(l_t(\tilde w_t) - l_t(w_{t+1})) + - D_{\psi_t}(w_{t+1}, \tilde w_t, g\psi_t(\tilde w_t)).$$ -/ +def stability (t : ℕ) : ℝ := + η * (l t (w_tilde t) - l t (w (t + 1))) - D_[ψ t](w (t + 1), w_tilde t, gψ t (w_tilde t)) + +/-- Encodes the update implicitly via first-order optimality conditions: +$$(\eta\,g_t + g\varphi_t(w_{t+1}) + g\psi_{t+1}(w_{t+1}) - g\psi_t(\tilde w_t))(u_t - w_{t+1}).$$ +$\text{optimality}(t) \le 0$ when $w_{t+1}$ satisfies first-order optimality. -/ +def optimality (t : ℕ) : ℝ := + ((η : ℝ) • g t + gφ t (w (t + 1)) + gψ (t + 1) (w (t + 1)) - gψ t (w_tilde t)) (u t - w (t + 1)) + +/-- Surplus contribution induced by the centering potential `φ_t`: +$$\varphi_t(u_t) - \varphi_t(w_{t+1}) - D_{\varphi_t}(u_t, w_{t+1}, g\varphi_t(w_{t+1})).$$ +Zero when no centering is used (`φ_t = 0`). -/ +def centering (t : ℕ) : ℝ := + φ t (u t) - φ t (w (t + 1)) - D_[φ t](u t, w (t + 1), gφ t (w (t + 1))) + +/-- Divergence drift capturing arbitrary post-processing or state adjustments +from iterate `w_{t+1}` to anchor `w̃_{t+1}`: +$$D_{\psi_{t+1}}(u_t,\tilde w_{t+1},g\psi_{t+1}(\tilde w_{t+1})) + - D_{\psi_{t+1}}(u_t,w_{t+1},g\psi_{t+1}(w_{t+1})).$$ +Vanishes for unadjusted or projection-free +updates (`w̃_{t+1} = w_{t+1}`), and yields small controllable penalties for schemes +like Fixed Share. -/ +def adjustment (t : ℕ) : ℝ := + D_[ψ (t+1)](u t, w_tilde (t + 1), gψ (t+1) (w_tilde (t + 1))) + - D_[ψ (t+1)](u t, w (t + 1), gψ (t+1) (w (t + 1))) + +/-- Regularizer shift evaluated on iterate $w_{t+1}$: +$$-(\psi_{t+1} - \psi_t)(w_{t+1}).$$ -/ +def shift (t : ℕ) : ℝ := + - (ψ (t + 1) - ψ t) (w (t + 1)) + +/-- Master Centered Online Mirror Descent (version 2) Regret Decomposition Identity +(variation of Andrew Jacobsen, *Adapting to Non-Stationarity in Online Learning*, Lemma A.1.1). -/ +theorem regret_decomposition_eq (T : ℕ) : + η * (∑ t ∈ Ico 1 (T + 1), (l t (w_tilde t) - l t (u t))) = + boundary ψ gψ u w_tilde T + + (∑ t ∈ Ico 1 (T + 1), adjustment ψ gψ u w w_tilde t) + + (∑ t ∈ Ico 1 (T + 1), pathlength gψ u w_tilde t) + + (∑ t ∈ Ico 1 (T + 1), stability η ψ gψ w w_tilde l t) + + (∑ t ∈ Ico 1 (T + 1), shift ψ w t) + - (∑ t ∈ Ico 1 (T + 1), optimality η gψ gφ u w w_tilde g t) + + (∑ t ∈ Ico 1 (T + 1), centering φ gφ u w t) + + η * (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) := by + induction T with + | zero => simp [boundary] + | succ T ih => + simp_rw [Finset.sum_Ico_succ_top (by omega : 1 ≤ T + 1), mul_add, ih] + dsimp [boundary, optimality, adjustment, shift, pathlength, + stability, centering, linearization, bregDiv] + simp only [map_sub, add_apply, sub_apply, smul_apply, smul_eq_mul] + ring + +end AuxTerms + +end OnlineConvexOptimization.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/FTRL/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/FTRL/RegretDecomposition.lean new file mode 100644 index 00000000..2a3a41b1 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/Algorithms/FTRL/RegretDecomposition.lean @@ -0,0 +1,93 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Algebra.BigOperators.Group.Finset.Defs +public import Mathlib.Basic.Real.Basic +public import Mathlib.Order.Interval.Finset.Nat +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Topology.Algebra.InfiniteSum.Order + +/-! +# Master Regret Decomposition for Follow-the-Regularized-Leader (FTRL) + +This file establishes the exact multi-round algebraic regret decomposition for +Follow-the-Regularized-Leader (FTRL), corresponding to Lemma 7.1 in Francesco Orabona's +*A Modern Introduction to Online Learning* (v10). Writing +$F_t(x) = \psi_t(x) + \sum_{i=1}^{t-1} \ell_i(x)$ and +$x_t \in \arg\min_{x \in V} F_t(x)$, the regret satisfies, for all $u$, +$$\sum_{t=1}^T (\ell_t(x_t) - \ell_t(u)) + = \psi_{T+1}(u) - \min_{x \in V} \psi_1(x) + + \sum_{t=1}^T (F_t(x_t) - F_{t+1}(x_{t+1}) + \ell_t(x_t)) + + F_{T+1}(x_{T+1}) - F_{T+1}(u).$$ + +## Main definitions +* `Fobj` +* `boundary` +* `stability` +* `terminalOptimality` + +## Main results +* `regret_decomposition_eq`: The master algebraic regret equality holding for all $T \ge 0$. +-/ + +open scoped BigOperators +open Finset + +@[expose] public section + +namespace OnlineConvexOptimization.FTRL + +variable {E : Type*} + +section Terms + +variable (ψ : ℕ → E → ℝ) +variable (u : E) +variable (w : ℕ → E) +variable (l : ℕ → E → ℝ) + +/-- +Cumulative objective (Orabona's $F_t$): $F_t(x) = \psi_t(x) + \sum_{i=1}^{t-1} \ell_i(x)$. +-/ +def Fobj (t : ℕ) (y : E) : ℝ := + ψ t y + ∑ i ∈ Ico 1 t, l i y + +/-- Boundary term: $\psi_{T+1}(u) - \min_{x \in V} \psi_1(x) = \psi_{T+1}(u) - F_1(x_1)$. -/ +def boundary (T : ℕ) : ℝ := + ψ (T + 1) u - Fobj ψ l 1 (w 1) + +/-- One-round stability penalty $F_t(x_t) - F_{t+1}(x_{t+1}) + \ell_t(x_t)$, +measuring the advance of $F_t + \ell_t$ between $x_t$ and $x_{t+1}$. -/ +def stability (t : ℕ) : ℝ := + Fobj ψ l t (w t) - Fobj ψ l (t + 1) (w (t + 1)) + l t (w t) + +/-- Terminal optimality deficit $F_{T+1}(x_{T+1}) - F_{T+1}(u)$ of $x_{T+1}$ relative to $u$. -/ +def terminalOptimality (T : ℕ) : ℝ := + Fobj ψ l (T + 1) (w (T + 1)) - Fobj ψ l (T + 1) u + +/-- Master Algebraic Regret Decomposition Identity for FTRL (Orabona, Lemma 7.1): +$$\sum_{t=1}^T (\ell_t(x_t) - \ell_t(u)) + = \psi_{T+1}(u) - \min_{x \in V} \psi_1(x) + + \sum_{t=1}^T (F_t(x_t) - F_{t+1}(x_{t+1}) + \ell_t(x_t)) + + F_{T+1}(x_{T+1}) - F_{T+1}(u).$$ -/ +theorem regret_decomposition_eq (T : ℕ) : + (∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u)) = + boundary ψ u w l T + + (∑ t ∈ Ico 1 (T + 1), stability ψ w l t) + + terminalOptimality ψ u w l T := by + induction T with + | zero => + simp [boundary, terminalOptimality, Fobj] + | succ T ih => + simp_rw [sum_Ico_succ_top (by omega : 1 ≤ T + 1), ih] + dsimp [boundary, terminalOptimality, stability, Fobj] + simp_rw [sum_Ico_succ_top (by omega : 1 ≤ T + 1)] + ring + +end Terms + +end OnlineConvexOptimization.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Boundary.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Boundary.lean new file mode 100644 index 00000000..e43ab6fe --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Boundary.lean @@ -0,0 +1,64 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv + +/-! +# Boundary Term Bound for Learning with Expert Advice (LEA) + +This file bounds the boundary term +$$\mathrm{boundary}(\psi, \nabla\psi, u, w, T) = + D_{\psi_1}(u, w_1) - D_{\psi_{T+1}}(u, w_{T+1}) + \psi_{T+1}(u) - \psi_1(u)$$ +for LEA under shifted unnormalized negative entropy regularizers $\psi^{\mathrm{shift}}_t$ +when the initial iterate $w_1$ is chosen as the uniform distribution on the standard simplex +$\Delta^{d-1}$: +$$w_1 = \left( \frac{1}{d}, \dots, \frac{1}{d} \right) \in \Delta^{d-1}.$$ + +## Main results + +* `boundary_shifted_le_log_card`: When $\alpha_1 \ge 0, \alpha_{T+1} \ge 0$, + the multi-round boundary term satisfies: + $$\mathrm{boundary}(\psi^{\mathrm{shift}}_\alpha, \nabla\psi_\alpha, u, w, T) + \le \alpha_1 \ln d + (\psi^{\mathrm{shift}}_{\alpha(T+1)}(u) - + \psi^{\mathrm{shift}}_{\alpha 1}(u)).$$ +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.COMD2 + +variable {d : ℕ} + +/-- Boundary term bound for LEA with uniform initialization $w_1 = (1/d, \dots, 1/d)$ and +sequence of shifted regularizers $\psi^{\mathrm{shift}}_t = \text{unnormEntropyShifted}(\alpha_t)$ +with $\alpha_1 \ge 0$ and $\alpha_{T+1} \ge 0$: +$$\mathrm{boundary}(\psi^{\mathrm{shift}}_\alpha, \nabla\psi_\alpha, u, w, T) + \le \alpha_1 \ln d + (\psi^{\mathrm{shift}}_{\alpha(T+1)}(u) - + \psi^{\mathrm{shift}}_{\alpha 1}(u)).$$ -/ +theorem boundary_shifted_le_log_card (α : ℕ → ℝ) (hα1 : 0 ≤ α 1) (T : ℕ) + (hαT : 0 ≤ α (T + 1)) (hd : 0 < d) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex) + (w : ℕ → EuclideanSpace ℝ (Fin d)) + (hw1 : w 1 = uniformSimplex d) + (hwT : w (T + 1) ∈ stdSimplex (d := d)) + (hwT_pos : ∀ i, 0 < w (T + 1) i) : + boundary (fun t ↦ unnormEntropyShifted (α t)) (fun t ↦ unnormEntropyFDeriv (α t)) u w T ≤ + α 1 * Real.log d + (unnormEntropyShifted (α (T + 1)) u - unnormEntropyShifted (α 1) u) := by + dsimp [boundary] + simp only [bregDiv_unnormEntropyShifted, hw1] + have h_breg_end := + (hasFDerivAt_unnormEntropy (α (T + 1)) (w (T + 1)) hwT_pos).hasSubgradientWithinAt + (convexOn_unnormEntropy_stdSimplex (α (T + 1)) hαT) hwT u hu + have h_init := bregDiv_unnormEntropy_uniformSimplex_le (α 1) hα1 hd u hu + linarith + +end Online.OCO.LEA.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Formula.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Formula.lean new file mode 100644 index 00000000..b4842f4e --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Formula.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Optimality +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# Update Formula for Online Mirror Descent in LEA + +This file defines the explicit closed-form update for Entropic Online Mirror Descent (OMD) +in Learning with Expert Advice (LEA) with time-varying regularizer weights +$\alpha_t, \alpha_{t+1} > 0$: + +$$w_{t+1, i} = \frac{w_{t, i}^{\alpha_t / \alpha_{t+1}} \exp(-g_{t, i}/\alpha_{t+1})} + {\sum_{j=1}^d w_{t, j}^{\alpha_t / \alpha_{t+1}} \exp(-g_{t, j}/\alpha_{t+1})}.$$ + +(When $\alpha_t = \alpha_{t+1} = \frac{1}{\eta}$ is constant, this reduces to the standard +multiplicative Exponential Weights / Hedge step $w_{t+1, i} \propto w_{t, i} e^{-\eta g_{t, i}}$.) + +## Main definitions + +* `omdExpWeightStep`: The one-step update function mapping $w_t \in \Delta^{d-1}$ + to $w_{t+1} \in \Delta^{d-1}$. +* `omdExpWeights`: The full recursive sequence of iterates for Entropic OMD. + +## Main results + +* `omdExpWeightStep_pos`: Positivity $0 < (w_{t+1})_i$ for all $i$. +* `omdExpWeightStep_mem_stdSimplex`: Membership $w_{t+1} \in \Delta^{d-1}$. +* `omdExpWeights_pos`: Coordinate positivity for all rounds $t \ge 1$. +* `omdExpWeights_mem_stdSimplex`: Simplex membership for all rounds $t \ge 1$. +* `omdExpWeights_isMinOn`: Exact minimizer property of the step. +* `omdExpWeights_optimality_nonneg`: Non-negativity of per-round optimality. +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.COMD2 + +variable {d : ℕ} + +/-- Coordinate-wise unnormalized weight for the exponential update: +$$w_i^{\alpha / \alpha'} \exp(-g_i / \alpha')$$ -/ +noncomputable def omdExpWeightUnnorm (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : ℝ := + (w i) ^ (α / α') * Real.exp (-(g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α') + +lemma omdExpWeightUnnorm_pos (α α' : ℝ) {w : EuclideanSpace ℝ (Fin d)} + (hw_pos : ∀ i, 0 < w i) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + 0 < omdExpWeightUnnorm α α' w g i := by + dsimp [omdExpWeightUnnorm] + exact mul_pos (Real.rpow_pos_of_pos (hw_pos i) _) (Real.exp_pos _) + +lemma sum_omdExpWeightUnnorm_pos (hd : 0 < d) (α α' : ℝ) {w : EuclideanSpace ℝ (Fin d)} + (hw_pos : ∀ i, 0 < w i) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + 0 < ∑ i, omdExpWeightUnnorm α α' w g i := by + have : (univ : Finset (Fin d)).Nonempty := + Finset.univ_nonempty_iff.mpr (Fin.pos_iff_nonempty.mp hd) + exact sum_pos (fun i _ ↦ omdExpWeightUnnorm_pos α α' hw_pos g i) this + +lemma sum_omdExpWeightUnnorm_ne_zero (hd : 0 < d) (α α' : ℝ) {w : EuclideanSpace ℝ (Fin d)} + (hw_pos : ∀ i, 0 < w i) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + ∑ i, omdExpWeightUnnorm α α' w g i ≠ 0 := + (sum_omdExpWeightUnnorm_pos hd α α' hw_pos g).ne' + +/-- The one-step update for Entropic Online Mirror Descent: +$$w_{t+1, i} = \frac{w_{t, i}^{\alpha_t / \alpha_{t+1}} \exp(-g_{t, i} / \alpha_{t+1})} + {\sum_j w_{t, j}^{\alpha_t / \alpha_{t+1}} \exp(-g_{t, j} / \alpha_{t+1})}.$$ -/ +noncomputable def omdExpWeightStep (_hd : 0 < d) (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : EuclideanSpace ℝ (Fin d) := + WithLp.toLp 2 (fun i ↦ omdExpWeightUnnorm α α' w g i / ∑ j, omdExpWeightUnnorm α α' w g j) + +lemma omdExpWeightStep_apply (hd : 0 < d) (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + omdExpWeightStep hd α α' w g i = + omdExpWeightUnnorm α α' w g i / ∑ j, omdExpWeightUnnorm α α' w g j := + rfl + +/-- Positivity of coordinates after an Entropic OMD step. -/ +lemma omdExpWeightStep_pos (hd : 0 < d) (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (hw_pos : ∀ i, 0 < w i) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + 0 < omdExpWeightStep hd α α' w g i := by + rw [omdExpWeightStep_apply] + exact div_pos (omdExpWeightUnnorm_pos α α' hw_pos g i) + (sum_omdExpWeightUnnorm_pos hd α α' hw_pos g) + +/-- The Entropic OMD update always stays within the standard simplex $\Delta^{d-1}$. -/ +theorem omdExpWeightStep_mem_stdSimplex (hd : 0 < d) (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (hw_pos : ∀ i, 0 < w i) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + omdExpWeightStep hd α α' w g ∈ stdSimplex (d := d) := by + rw [mem_stdSimplex_iff] + refine ⟨fun i ↦ (omdExpWeightStep_pos hd α α' w hw_pos g i).le, ?_⟩ + simp_rw [omdExpWeightStep_apply] + rw [← sum_div, div_self (sum_omdExpWeightUnnorm_ne_zero hd α α' hw_pos g)] + +/-- Logarithm of coordinates for the Exponential Weights update. -/ +lemma log_omdExpWeightStep_apply (hd : 0 < d) (α α' : ℝ) (_hα' : 0 < α') + (w : EuclideanSpace ℝ (Fin d)) (hw_pos : ∀ i, 0 < w i) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + Real.log (omdExpWeightStep hd α α' w g i) = + (α / α') * Real.log (w i) - (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α' + - Real.log (∑ j, omdExpWeightUnnorm α α' w g j) := by + rw [omdExpWeightStep_apply, Real.log_div (omdExpWeightUnnorm_pos α α' hw_pos g i).ne' + (sum_omdExpWeightUnnorm_pos hd α α' hw_pos g).ne'] + dsimp [omdExpWeightUnnorm] + rw [Real.log_mul (Real.rpow_pos_of_pos (hw_pos i) _).ne' (Real.exp_pos _).ne', + Real.log_rpow (hw_pos i), Real.log_exp] + ring + +/-- The objective function for the mirror descent step: +$$x \mapsto g(x) + \psi_{\alpha'}(x) - \nabla\psi_\alpha(w)(x).$$ -/ +noncomputable def mirrorStepObj (α α' : ℝ) (w : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ := + g x + unnormEntropy α' x - (unnormEntropyFDeriv α w) x + +/-- Linear coordinate expansion of the subgradient and Fréchet derivative on $\mathbb{R}^d$. -/ +lemma mirrorStepObj_diff_eq (hd : 0 < d) (α α' : ℝ) (hα' : 0 < α') + (w : EuclideanSpace ℝ (Fin d)) (hw_pos : ∀ i, 0 < w i) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (x : EuclideanSpace ℝ (Fin d)) (hx : x ∈ stdSimplex) : + (g + unnormEntropyFDeriv α' (omdExpWeightStep hd α α' w g) - unnormEntropyFDeriv α w) + (x - omdExpWeightStep hd α α' w g) = 0 := by + let w_next := omdExpWeightStep hd α α' w g + have hw_next_mem := omdExpWeightStep_mem_stdSimplex hd α α' w hw_pos g + rw [mem_stdSimplex_iff] at hx hw_next_mem + have h_basis (y : EuclideanSpace ℝ (Fin d)) : + g y = ∑ i, y i * g (EuclideanSpace.basisFun (Fin d) ℝ i) := by + have hy : y = ∑ i, y i • EuclideanSpace.basisFun (Fin d) ℝ i := by + ext i; simp [EuclideanSpace.basisFun_apply, Pi.single_apply] + conv_lhs => rw [hy] + rw [map_sum] + refine sum_congr rfl fun i _ ↦ by rw [map_smul, smul_eq_mul] + simp only [sub_apply, add_apply, unnormEntropyFDeriv_apply] + have h_w_next_i (i : Fin d) : + g (EuclideanSpace.basisFun (Fin d) ℝ i) + α' * Real.log (w_next i) - α * Real.log (w i) = + - α' * Real.log (∑ j, omdExpWeightUnnorm α α' w g j) := by + have hlog := log_omdExpWeightStep_apply hd α α' hα' w hw_pos g i + dsimp [w_next] + rw [hlog] + have hα'_ne : α' ≠ 0 := hα'.ne' + field_simp + ring + have h_comb : (g (x - w_next) + α' * ∑ i, (x - w_next) i * Real.log (w_next i) + - α * ∑ i, (x - w_next) i * Real.log (w i)) = + ∑ i, (x i - w_next i) * + (g (EuclideanSpace.basisFun (Fin d) ℝ i) + α' * Real.log (w_next i) + - α * Real.log (w i)) := by + rw [h_basis (x - w_next)] + simp only [PiLp.sub_apply, mul_sum, ← sum_add_distrib, ← sum_sub_distrib] + congr 1 with i + ring + rw [h_comb] + simp_rw [h_w_next_i] + rw [← sum_mul, sum_sub_distrib, hx.2, hw_next_mem.2, sub_self, zero_mul] + +/-- The Exponential Weights update is an exact constrained minimizer (`IsMinOn`) +of the linearized mirror descent step objective on the standard simplex $\Delta^{d-1}$. -/ +theorem isMinOn_omdExpWeightStep (hd : 0 < d) (α α' : ℝ) (hα' : 0 < α') + (w : EuclideanSpace ℝ (Fin d)) (hw_pos : ∀ i, 0 < w i) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + IsMinOn (fun x ↦ g x + unnormEntropy α' x - (unnormEntropyFDeriv α w) x) + (stdSimplex (d := d)) (omdExpWeightStep hd α α' w g) := by + let w_next := omdExpWeightStep hd α α' w g + have hw_next_pos := omdExpWeightStep_pos hd α α' w hw_pos g + have hw_next_mem := omdExpWeightStep_mem_stdSimplex hd α α' w hw_pos g + have h_diff : HasFDerivAt (unnormEntropy α') (unnormEntropyFDeriv α' w_next) w_next := + hasFDerivAt_unnormEntropy α' w_next hw_next_pos + have h_conv : ConvexOn ℝ (stdSimplex (d := d)) (unnormEntropy α') := + convexOn_unnormEntropy_stdSimplex α' hα'.le + let lin : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ := g - unnormEntropyFDeriv α w + have h_obj_conv : ConvexOn ℝ (stdSimplex (d := d)) (unnormEntropy α' + ⇑lin) := + h_conv.add (lin.toLinearMap.convexOn h_conv.1) + have h_obj_diff : HasFDerivAt (unnormEntropy α' + ⇑lin) + (unnormEntropyFDeriv α' w_next + lin) w_next := + h_diff.add lin.hasFDerivAt + intro x hx + have h_zero : (unnormEntropyFDeriv α' w_next + lin) (x - w_next) = 0 := by + dsimp [lin] + have := mirrorStepObj_diff_eq hd α α' hα' w hw_pos g x hx + have h_reorder : (unnormEntropyFDeriv α' w_next + (g - unnormEntropyFDeriv α w)) (x - w_next) = + (g + unnormEntropyFDeriv α' w_next - unnormEntropyFDeriv α w) (x - w_next) := by + simp only [add_apply, sub_apply] + ring + rwa [h_reorder] + have h_subg_base := (hasSubgradientWithinAt_iff_le.mp + (h_obj_diff.hasSubgradientWithinAt h_obj_conv hw_next_mem)) x hx + dsimp [bregDiv] at h_subg_base + rw [h_zero, add_zero] at h_subg_base + dsimp [lin] at h_subg_base ⊢ + simp only [sub_apply] at h_subg_base ⊢ + linarith + +/-! ### Whole Trajectory Sequence Construction and Properties -/ + +/-- Recursive trajectory of iterates generated by the Exponential Weights update, starting from +$w_1 = \mathrm{uniformSimplex}(d)$ at $t = 1$. -/ +noncomputable def omdExpWeights (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) : ℕ → EuclideanSpace ℝ (Fin d) + | 0 => uniformSimplex d + | 1 => uniformSimplex d + | t + 2 => omdExpWeightStep hd (α (t + 1)) (α (t + 2)) (omdExpWeights hd α g (t + 1)) (g (t + 1)) + +@[simp] +lemma omdExpWeights_one (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) : + omdExpWeights hd α g 1 = uniformSimplex d := + rfl + +lemma omdExpWeights_succ_succ (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) : + omdExpWeights hd α g (t + 2) = + omdExpWeightStep hd (α (t + 1)) (α (t + 2)) (omdExpWeights hd α g (t + 1)) (g (t + 1)) := + rfl + +/-- Every iterate $w_t$ produced by `omdExpWeights` is strictly positive in all coordinates for +$t \ge 1$. -/ +theorem omdExpWeights_pos (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) : + ∀ t ≥ 1, ∀ i, 0 < omdExpWeights hd α g t i := by + intro t ht + obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := Nat.exists_eq_add_of_le' ht + clear ht + induction n with + | zero => + intro i + rw [omdExpWeights_one] + exact uniformSimplex_pos hd i + | succ n ih => + intro i + rw [omdExpWeights_succ_succ] + exact omdExpWeightStep_pos hd (α (n + 1)) (α (n + 2)) (omdExpWeights hd α g (n + 1)) + (fun j ↦ ih j) (g (n + 1)) i + +/-- Every iterate $w_t$ produced by `omdExpWeights` lies in the standard simplex $\Delta^{d-1}$ for +$t \ge 1$. -/ +theorem omdExpWeights_mem_stdSimplex (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) : + ∀ t ≥ 1, omdExpWeights hd α g t ∈ stdSimplex (d := d) := by + intro t ht + obtain ⟨n, rfl⟩ : ∃ n, t = n + 1 := Nat.exists_eq_add_of_le' ht + clear ht + induction n with + | zero => + rw [omdExpWeights_one] + exact mem_stdSimplex_uniformSimplex hd + | succ n _ => + rw [omdExpWeights_succ_succ] + have h_pos : ∀ j, 0 < omdExpWeights hd α g (n + 1) j := by + have : 1 ≤ n + 1 := by omega + exact omdExpWeights_pos hd α g (n + 1) this + exact omdExpWeightStep_mem_stdSimplex hd (α (n + 1)) (α (n + 2)) + (omdExpWeights hd α g (n + 1)) h_pos (g (n + 1)) + +/-- The iterates generated by `omdExpWeights` satisfy the `IsMinOn` condition at each +round $t \ge 1$. -/ +theorem omdExpWeights_isMinOn (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) (ht : 1 ≤ t) + (hα'_pos : 0 < α (t + 1)) : + IsMinOn (fun x ↦ g t x + unnormEntropy (α (t + 1)) x - + (unnormEntropyFDeriv (α t) (omdExpWeights hd α g t)) x) + (stdSimplex (d := d)) (omdExpWeights hd α g (t + 1)) := by + obtain ⟨k, rfl⟩ : ∃ k, t = k + 1 := Nat.exists_eq_add_of_le' ht + rw [omdExpWeights_succ_succ] + have h_pos := omdExpWeights_pos hd α g (k + 1) (by omega) + exact isMinOn_omdExpWeightStep hd (α (k + 1)) (α (k + 1 + 1)) hα'_pos + (omdExpWeights hd α g (k + 1)) h_pos (g (k + 1)) + +/-- Per-round optimality deficit is non-negative for the concrete `omdExpWeights` trajectory +at any comparator $u \in \Delta^{d-1}$ when $\alpha_{t+1} > 0$. -/ +theorem omdExpWeights_optimality_nonneg (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) (ht : 1 ≤ t) (hα'_pos : 0 < α (t + 1)) + {u : EuclideanSpace ℝ (Fin d)} (hu : u ∈ stdSimplex) : + 0 ≤ optimality (fun s ↦ unnormEntropyFDeriv (α s)) u (omdExpWeights hd α g) g t := by + have hw_succ_pos := omdExpWeights_pos hd α g (t + 1) (by omega) + have hw_succ := omdExpWeights_mem_stdSimplex hd α g (t + 1) (by omega) + have h_diff := hasFDerivAt_unnormEntropy (α (t + 1)) (omdExpWeights hd α g (t + 1)) hw_succ_pos + have h_conv := convexOn_unnormEntropy_stdSimplex (d := d) (α (t + 1)) hα'_pos.le + have h_min := omdExpWeights_isMinOn hd α g t ht hα'_pos + exact optimality_nonneg_of_isMinOn (ψ := fun s ↦ unnormEntropy (α s)) + (gψ := fun s ↦ unnormEntropyFDeriv (α s)) + t h_diff h_conv hw_succ hu h_min + +/-- Cumulative first-order optimality deficit is non-negative for the concrete `omdExpWeights` +trajectory at any comparator $u \in \Delta^{d-1}$. -/ +theorem omdExpWeights_sum_optimality_nonneg (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 1), 0 < α (t + 1)) + {u : EuclideanSpace ℝ (Fin d)} (hu : u ∈ stdSimplex) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), + optimality (fun s ↦ unnormEntropyFDeriv (α s)) u (omdExpWeights hd α g) g t := + sum_nonneg fun t ht ↦ + omdExpWeights_optimality_nonneg hd α g t (mem_Ico.mp ht).1 (hα_pos t ht) hu + +end Online.OCO.LEA.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Optimality.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Optimality.lean new file mode 100644 index 00000000..fc7e7d9a --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/Optimality.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.RegretDecomposition +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# First-Order Optimality Bounds for Online Mirror Descent (LEA Specialization) + +This file proves that the first-order optimality deficit: +$$\mathrm{optimality}_t = (\eta g_t + \nabla \psi_{t+1}(w_{t+1}) - + \nabla \psi_t(w_t))(u - w_{t+1})$$ +is **non-negative** (i.e. $0 \le \mathrm{optimality}_t$) whenever $w_{t+1}$ minimizes the +linearized mirror descent step: +$$x \mapsto \eta g_t(x) + \psi_{t+1}(x) - \nabla \psi_t(w_t)(x)$$ +over a convex domain $s \subseteq E$, $\psi_{t+1}$ is convex and differentiable at $w_{t+1}$, +and the comparator $u \in s$. + +## Main results +* `optimality_nonneg_of_isMinOn`: $0 \le \mathrm{optimality}_t$ + whenever $w_{t+1}$ is a constrained minimizer on $s$ and $u \in s$. +-/ + +open scoped BigOperators Bregman Topology +open Filter Finset + +@[expose] public section + +namespace Online.OCO.LEA.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Optimality + +variable {ψ : ℕ → E → ℝ} +variable {gψ : ℕ → E → (E →L[ℝ] ℝ)} +variable {u : E} +variable {w : ℕ → E} +variable {g : ℕ → (E →L[ℝ] ℝ)} +variable {s : Set E} + +/-- First-order optimality deficit is non-negative when $w_{t+1}$ minimizes the mirror +descent step objective over $s$, $\psi_{t+1}$ is convex with Fréchet derivative +$g\psi_{t+1}(w_{t+1})$, and $u \in s$. -/ +lemma optimality_nonneg_of_isMinOn (t : ℕ) + (hψ_diff : HasFDerivAt (ψ (t + 1)) (gψ (t + 1) (w (t + 1))) (w (t + 1))) + (hψ_conv : ConvexOn ℝ s (ψ (t + 1))) + (hw : w (t + 1) ∈ s) + (hu : u ∈ s) + (h_min : IsMinOn (fun x ↦ (g t) x + ψ (t + 1) x - (gψ t (w t)) x) s (w (t + 1))) : + 0 ≤ optimality gψ u w g t := by + let lin : E →L[ℝ] ℝ := g t - gψ t (w t) + have h_conv : ConvexOn ℝ s (ψ (t + 1) + ⇑lin) := + hψ_conv.add (lin.toLinearMap.convexOn hψ_conv.1) + have h_min' : IsMinOn ((ψ (t + 1) + ⇑lin) + fun _ : E ↦ (0 : ℝ)) s (w (t + 1)) := by + intro x hx + have := h_min hx + dsimp [lin] at this ⊢ + simp only [add_zero, sub_apply] at this ⊢ + linarith + have h_subg := ((hψ_diff.add lin.hasFDerivAt).hasSubgradientWithinAt_add_iff + (g := 0) h_conv (convexOn_const 0 h_conv.1) hw).mp + (hasSubgradientWithinAt_zero_iff_isMinOn.mpr h_min') u hu + dsimp [bregDiv, optimality, lin] at h_subg ⊢ + simp only [sub_self, zero_sub, neg_apply, neg_neg, add_apply, sub_apply] at h_subg ⊢ + linarith + +/-- Cumulative first-order optimality deficit is non-negative when each $w_{t+1}$ is a +constrained minimizer of the mirror descent step objective over $s$. -/ +lemma sum_optimality_nonneg_of_isMinOn (T : ℕ) + (hψ_diff : ∀ t ∈ Ico 1 (T + 1), HasFDerivAt (ψ (t + 1)) (gψ (t + 1) (w (t + 1))) (w (t + 1))) + (hψ_conv : ∀ t ∈ Ico 1 (T + 1), ConvexOn ℝ s (ψ (t + 1))) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hu : u ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 1), + IsMinOn (fun x ↦ (g t) x + ψ (t + 1) x - (gψ t (w t)) x) s (w (t + 1))) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), optimality gψ u w g t := by + refine sum_nonneg fun t ht ↦ ?_ + have ht2 : t + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico] at ht ⊢; omega + exact optimality_nonneg_of_isMinOn t (hψ_diff t ht) (hψ_conv t ht) (hw_mem (t + 1) ht2) hu + (hw_min t ht) + +end Optimality + +end Online.OCO.LEA.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretBound.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretBound.lean new file mode 100644 index 00000000..63a93547 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretBound.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Formula +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Stability +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic +import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.COMD2.Boundary + +/-! +# Regret Bound for Online Mirror Descent in Learning with Expert Advice (LEA) + +This file proves the multi-round regret bound for Learning with Expert Advice (LEA) using +Online Mirror Descent (OMD) with time-varying unnormalized negative entropy regularization +and non-negative loss subgradients $g_t \ge 0$. + +## Main results + +* `regret_bound`: The cumulative regret bound for the Exponential Weights + (Hedge / Entropic OMD) trajectory `omdExpWeights hd α g`. +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.COMD2 + +variable {d : ℕ} + +/-- Cumulative regret upper bound for Exponential Weights (Hedge / Entropic OMD) with non-negative +losses $g_t \ge 0$, where the stability term is bounded directly with $w_t$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u)) \le \alpha_1 \ln d + (\psi_{\alpha(T+1)}(u) - \psi_{\alpha 1}(u)) + + \sum_{t=1}^T \frac{1}{2\alpha_t} \sum_{i=1}^d w_{t, i} (g_t)_i^2.$$ -/ +theorem regret_bound (α : ℕ → ℝ) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 2), 0 < α t) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (hd : 0 < d) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) + (w : ℕ → EuclideanSpace ℝ (Fin d)) + (hw_def : w = omdExpWeights hd α g) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex) + (l : ℕ → EuclideanSpace ℝ (Fin d) → ℝ) + (hg : ∀ t ∈ Ico 1 (T + 1), HasSubgradientWithinAt (l t) (g t) stdSimplex (w t)) + (hg_nonneg : ∀ t ∈ Ico 1 (T + 1), + ∀ i, 0 ≤ g t (EuclideanSpace.basisFun (Fin d) ℝ i)) : + ∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u) ≤ + α 1 * Real.log d + (unnormEntropyShifted (α (T + 1)) u - unnormEntropyShifted (α 1) u) + + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * + ∑ i, (w t i) * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + subst hw_def + have hw1 : omdExpWeights hd α g 1 = uniformSimplex d := omdExpWeights_one hd α g + have hw : ∀ t ∈ Ico 1 (T + 2), omdExpWeights hd α g t ∈ stdSimplex (d := d) := fun t ht ↦ + omdExpWeights_mem_stdSimplex hd α g t (mem_Ico.mp ht).1 + have hw_pos : ∀ t ∈ Ico 1 (T + 2), ∀ i, 0 < omdExpWeights hd α g t i := fun t ht ↦ + omdExpWeights_pos hd α g t (mem_Ico.mp ht).1 + have h_decomp := regret_decomposition_eq (fun s ↦ unnormEntropyShifted (α s)) + (fun s ↦ unnormEntropyFDeriv (α s)) u (omdExpWeights hd α g) g l T + have h_bound := boundary_shifted_le_log_card α (hα_pos 1 (by simp)).le T + (hα_pos (T + 1) (by simp)).le hd u hu (omdExpWeights hd α g) hw1 + (hw (T + 1) (by simp)) (hw_pos (T + 1) (by simp)) + have h_opt_sum := omdExpWeights_sum_optimality_nonneg hd α g T + (fun t ht ↦ hα_pos (t + 1) (by rw [mem_Ico] at ht ⊢; omega)) hu + have h_lin_sum : ∑ t ∈ Ico 1 (T + 1), linearization u (omdExpWeights hd α g) g l t ≤ 0 := + sum_nonpos fun t ht ↦ by dsimp [linearization]; linarith [hg t ht u hu] + have h_stab := sum_stability_le_dual_norm_wt (w := omdExpWeights hd α g) (g := g) α T + (fun t ht ↦ hα_pos t (by rw [mem_Ico] at ht ⊢; omega)) hw_pos hg_nonneg + have h_shift_le := sum_shift_unnormEntropyShifted_nonpos hd α (omdExpWeights hd α g) T h_mono hw + linarith + +end Online.OCO.LEA.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretDecomposition.lean new file mode 100644 index 00000000..c3e73bf7 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/COMD2/RegretDecomposition.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.RegretTerms + +/-! +# Static Regret Decomposition for Online Mirror Descent (LEA Specialization) + +This file defines the direct, algebraic regret decomposition for Online Mirror Descent +tailored to the Learning with Expert Advice (LEA) setting: +* **Static comparator**: $u_t = u$ for all rounds $t$. +* **No centering**: $\varphi_t = 0$. +* **No state adjustment**: $\tilde{w}_t = w_t$. + +Under these conditions, the regret is governed by the boundary divergence & potential drift, +and four per-round regret terms: +1. `boundary`: Initial divergence minus final divergence plus regularizer drift at $u$. +2. `stability`: Movement of the loss balanced against regularizer divergence (from `LEA.Common`). +3. `shift`: Cross-round regularizer potential drift on iterates $w_t$ (from `LEA.Common`). +4. `optimality`: First-order optimality deficit of the update step. +5. `linearization`: Loss linearization error via subgradients. + +## Main definitions +* `boundary` +* `linearization` +* `optimality` + +## Main results +* `regret_decomposition_eq`: The algebraic multi-round regret equality. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Terms + +variable (ψ : ℕ → E → ℝ) +variable (gψ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u : E) +variable (w : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- Boundary term comprising initial and final Bregman divergences and regularizer drift at $u$. -/ +def boundary (T : ℕ) : ℝ := + D_[ψ 1](u, w 1, gψ 1 (w 1)) + - D_[ψ (T + 1)](u, w (T + 1), gψ (T + 1) (w (T + 1))) + + ψ (T + 1) u - ψ 1 u + +/-- Error incurred by linearizing the loss with subgradient `g_t` at $w_t$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u, w t, g t) + +/-- Encodes the update implicitly via first-order optimality conditions: +$\text{optimality}(t) \le 0$ when $w_{t+1}$ satisfies first-order optimality. -/ +def optimality (t : ℕ) : ℝ := + (g t + gψ (t + 1) (w (t + 1)) - gψ t (w t)) (u - w (t + 1)) + +/-- Exact multi-round algebraic regret decomposition for static, uncentered, unadjusted OMD. -/ +theorem regret_decomposition_eq (T : ℕ) : + (∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u)) = + boundary ψ gψ u w T + + (∑ t ∈ Ico 1 (T + 1), LEA.stability ψ gψ w g t) + + (∑ t ∈ Ico 1 (T + 1), LEA.shift ψ w t) + - (∑ t ∈ Ico 1 (T + 1), optimality gψ u w g t) + + (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) := by + induction T with + | zero => + simp [boundary] + | succ T ih => + simp_rw [Finset.sum_Ico_succ_top (by omega : 1 ≤ T + 1), ih] + dsimp [boundary, optimality, LEA.shift, LEA.stability, linearization, bregDiv] + simp only [map_sub, add_apply, sub_apply] + ring + +end Terms + +end Online.OCO.LEA.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Domain.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Domain.lean new file mode 100644 index 00000000..9aadf91b --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Domain.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.PiL2 + +/-! +# Standard Simplex Domain for Online Convex Optimization + +This file defines the standard simplex `stdSimplex` directly as a convex subset of +`EuclideanSpace ℝ (Fin d)` and provides basic properties of the uniform distribution. + +## Main definitions + +* `stdSimplex`: The standard simplex $\Delta^{d-1} \subset \mathbb{R}^d$ + defined as $\{x \in \mathbb{R}^d \mid (\forall i, 0 \le x_i) \wedge \sum_i x_i = 1\}$. +* `uniformSimplex`: The uniform distribution $w_1 = (1/d, \dots, 1/d)$. + +## Main results + +* `convex_stdSimplex`: Convexity of `stdSimplex`. +* `mem_stdSimplex_uniformSimplex`: Membership $w_1 \in \Delta^{d-1}$. +-/ + +open scoped BigOperators +open Finset + +@[expose] public section + +namespace Online.OCO.LEA + +variable {d : ℕ} + +/-- The standard simplex $\Delta^{d-1} \subset \mathbb{R}^d$ in `EuclideanSpace ℝ (Fin d)`: +$$\Delta^{d-1} = \left\{ x \in \mathbb{R}^d \;\middle|\; \forall i, 0 \le x_i +\;\text{and}\; \sum_{i=1}^d x_i = 1 \right\}$$ -/ +def stdSimplex : Set (EuclideanSpace ℝ (Fin d)) := + { x : EuclideanSpace ℝ (Fin d) | (∀ i, 0 ≤ x i) ∧ ∑ i, x i = 1 } + +lemma mem_stdSimplex_iff (x : EuclideanSpace ℝ (Fin d)) : + x ∈ stdSimplex ↔ (∀ i, 0 ≤ x i) ∧ ∑ i, x i = 1 := + Iff.rfl + +/-- The standard simplex is a convex set in `EuclideanSpace ℝ (Fin d)`. -/ +theorem convex_stdSimplex : Convex ℝ (stdSimplex (d := d)) := by + intro x hx y hy a b ha hb hab + refine ⟨fun i ↦ add_nonneg (mul_nonneg ha (hx.1 i)) (mul_nonneg hb (hy.1 i)), ?_⟩ + simp only [PiLp.add_apply, PiLp.smul_apply, smul_eq_mul, sum_add_distrib, + ← mul_sum, hx.2, hy.2, mul_one, hab] + +/-- The uniform distribution vector on `EuclideanSpace ℝ (Fin d)`: +$$w_1 = \left( \frac{1}{d}, \dots, \frac{1}{d} \right)$$ -/ +noncomputable def uniformSimplex (d : ℕ) : EuclideanSpace ℝ (Fin d) := + WithLp.toLp 2 (fun _ ↦ (1 : ℝ) / d) + +@[simp] +lemma uniformSimplex_apply (i : Fin d) : uniformSimplex d i = (1 : ℝ) / d := + rfl + +lemma uniformSimplex_pos (hd : 0 < d) (i : Fin d) : 0 < uniformSimplex d i := + div_pos zero_lt_one (Nat.cast_pos.mpr hd) + +/-- The uniform distribution lies in the standard simplex `stdSimplex`. -/ +theorem mem_stdSimplex_uniformSimplex (hd : 0 < d) : uniformSimplex d ∈ stdSimplex (d := d) := by + refine ⟨fun i ↦ (uniformSimplex_pos hd i).le, ?_⟩ + simp [Nat.cast_ne_zero.mpr hd.ne'] + +end Online.OCO.LEA diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/RegretTerms.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/RegretTerms.lean new file mode 100644 index 00000000..961f480e --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/RegretTerms.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.Normed.Module.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic + +/-! +# Common Regret Terms for Learning with Expert Advice (LEA) + +This file collects the per-round regret terms shared across the LEA algorithms: +the stability tradeoff and the regularizer potential shift. + +## Main definitions + +* `stability`: One-round stability tradeoff between loss reduction and divergence. +* `shift`: Regularizer potential shift across rounds. +-/ + +open scoped Bregman + +@[expose] public section + +namespace Online.OCO.LEA + +variable {E : Type*} + +/-- Stability tradeoff between loss reduction and regularizer distance: +$$(g_t)(w_t - w_{t+1}) - D_{\psi_t}(w_{t+1}, w_t, g\psi_t(w_t)).$$ -/ +def stability [NormedAddCommGroup E] [NormedSpace ℝ E] + (ψ : ℕ → E → ℝ) (gψ : ℕ → E → (E →L[ℝ] ℝ)) (w : ℕ → E) (g : ℕ → (E →L[ℝ] ℝ)) (t : ℕ) : ℝ := + (g t) (w t - w (t + 1)) - D_[ψ t](w (t + 1), w t, gψ t (w t)) + +/-- Potential shift accounting for changes in regularizers across rounds: +$$- (\psi_{t+1} - \psi_t)(w_{t+1}).$$ -/ +def shift (ψ : ℕ → E → ℝ) (w : ℕ → E) (t : ℕ) : ℝ := + - (ψ (t + 1) - ψ t) (w (t + 1)) + +end Online.OCO.LEA diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Regularizer.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Regularizer.lean new file mode 100644 index 00000000..82b124a4 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Regularizer.lean @@ -0,0 +1,273 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Domain +public import Mathlib.Analysis.Calculus.Deriv.Basic +import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.MVT +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog + +/-! +# Scaled Unnormalized Negative Entropy Regularizer for LEA + +This file defines the scaled unnormalized negative entropy regularizer +$$\psi_\alpha(x) = \alpha \sum_{i=1}^d (x_i \ln x_i - x_i),$$ +its Fréchet derivative $\nabla\psi_\alpha(x)$, its Hessian second-derivative bilinear map, +and proves: +1. `hasFDerivAt_unnormEntropy`: Formula for the Fréchet derivative + $\nabla\psi_\alpha(x) = \alpha (\ln x_i)_i$. +2. `hasFDerivAt_unnormEntropyFDeriv`: Formula for the Hessian bilinear form. +3. `bregDiv_unnormEntropy_mvt`: Second-order Taylor/MVT remainder for the Bregman divergence. +4. `convexOn_unnormEntropy_stdSimplex`: Convexity of `unnormEntropy α` on the standard simplex + `stdSimplex` for $\alpha \ge 0$. + +## Main definitions +* `unnormEntropy` +* `unnormEntropyFDeriv` +* `unnormEntropyHessian` +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA + +variable {d : ℕ} + +/-! ### Definitions -/ + +/-- The scaled unnormalized negative entropy regularizer with scale $\alpha \in \mathbb{R}$: +$$\psi_\alpha(x) = \alpha \sum_{i=1}^d (x_i \ln x_i - x_i)$$ -/ +noncomputable def unnormEntropy (α : ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ := + α * ∑ i, (x i * Real.log (x i) - x i) + +/-- Coordinate projection on `EuclideanSpace ℝ (Fin d)` as a continuous linear map. -/ +noncomputable abbrev eucProj (i : Fin d) : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ := + EuclideanSpace.proj (𝕜 := ℝ) (ι := Fin d) i + +lemma hasDerivAt_mul_log_sub {x : ℝ} (hx : x ≠ 0) : + HasDerivAt (fun t ↦ t * Real.log t - t) (Real.log x) x := by + have := (Real.hasDerivAt_mul_log hx).sub (hasDerivAt_id x) + ring_nf at this + exact this + +/-- The Fréchet derivative of scaled unnormalized negative entropy at $x \in \mathbb{R}^d_{>0}$: +$$v \mapsto \alpha \sum_{i=1}^d v_i \ln x_i$$ -/ +noncomputable def unnormEntropyFDeriv (α : ℝ) (x : EuclideanSpace ℝ (Fin d)) : + EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ := + α • (∑ i, (Real.log (x i)) • eucProj i) + +@[simp] +lemma unnormEntropyFDeriv_apply (α : ℝ) (x v : EuclideanSpace ℝ (Fin d)) : + unnormEntropyFDeriv α x v = α * ∑ i, v i * Real.log (x i) := by + simp [unnormEntropyFDeriv, mul_comm] + +/-- The Hessian (second Fréchet derivative) of scaled unnormalized negative entropy at +$x \in \mathbb{R}^d_{>0}$: +$$(v, w) \mapsto \alpha \sum_{i=1}^d \frac{v_i w_i}{x_i}$$ -/ +noncomputable def unnormEntropyHessian (α : ℝ) (x : EuclideanSpace ℝ (Fin d)) : + EuclideanSpace ℝ (Fin d) →L[ℝ] (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) := + α • (∑ i, (x i)⁻¹ • ContinuousLinearMap.smulRight (eucProj i) (eucProj i)) + +@[simp] +lemma unnormEntropyHessian_apply (α : ℝ) (x v w : EuclideanSpace ℝ (Fin d)) : + unnormEntropyHessian α x v w = α * ∑ i, (v i * w i) / x i := by + simp [unnormEntropyHessian, div_eq_inv_mul, mul_sum] + +/-- The Bregman divergence of unnormalized negative entropy decomposes coordinate-wise: +$$D_{\psi_\alpha}(x, y) = \alpha \sum_{i=1}^d (x_i \ln(x_i / y_i) - x_i + y_i).$$ -/ +lemma bregDiv_unnormEntropy_apply (α : ℝ) (x y : EuclideanSpace ℝ (Fin d)) + (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) : + D_[unnormEntropy α](x, y, unnormEntropyFDeriv α y) = + α * ∑ i, (x i * Real.log (x i / y i) - x i + y i) := by + dsimp [bregDiv, unnormEntropy] + rw [unnormEntropyFDeriv_apply, mul_sum, mul_sum, mul_sum, mul_sum] + simp_rw [← sum_sub_distrib, Real.log_div (hx _).ne' (hy _).ne'] + refine sum_congr rfl fun i _ ↦ by dsimp; ring + +/-! ### Fréchet Derivatives -/ + +/-- Fréchet derivative of scaled unnormalized negative entropy at any $y \in \mathbb{R}^d_{>0}$. -/ +theorem hasFDerivAt_unnormEntropy (α : ℝ) (y : EuclideanSpace ℝ (Fin d)) (hy : ∀ i, 0 < y i) : + HasFDerivAt (unnormEntropy α) (unnormEntropyFDeriv α y) y := by + have h := HasFDerivAt.sum (u := (univ : Finset (Fin d))) + (fun i _ ↦ (hasDerivAt_mul_log_sub (hy i).ne').comp_hasFDerivAt y (eucProj i).hasFDerivAt) + have h_scaled := h.const_smul α + have h_eq_fun : (α • (∑ i : Fin d, (fun t ↦ t * Real.log t - t) ∘ ⇑(eucProj i))) = + unnormEntropy α := by + ext x; simp [unnormEntropy, smul_eq_mul] + have h_eq_deriv : α • (∑ i : Fin d, (Real.log (y i)) • eucProj i) = + unnormEntropyFDeriv α y := rfl + rw [h_eq_deriv] at h_scaled + rwa [h_eq_fun] at h_scaled + +/-- Second Fréchet derivative (Hessian) of scaled unnormalized negative entropy at +$y \in \mathbb{R}^d_{>0}$. -/ +theorem hasFDerivAt_unnormEntropyFDeriv (α : ℝ) (y : EuclideanSpace ℝ (Fin d)) (hy : ∀ i, 0 < y i) : + HasFDerivAt (unnormEntropyFDeriv α) (unnormEntropyHessian α y) y := by + have h (i : Fin d) : HasFDerivAt (fun x ↦ (Real.log (x i)) • eucProj i) + ((y i)⁻¹ • ContinuousLinearMap.smulRight (eucProj i) (eucProj i)) y := by + have hlog : HasFDerivAt (fun x ↦ Real.log (x i)) ((y i)⁻¹ • eucProj i) y := by + change HasFDerivAt (Real.log ∘ fun x ↦ x i) ((y i)⁻¹ • eucProj i) y + exact (Real.hasDerivAt_log (hy i).ne').comp_hasFDerivAt y (eucProj i).hasFDerivAt + have h_smul := hlog.smul_const (eucProj i) + have h_clm : ((y i)⁻¹ • eucProj i).smulRight (eucProj i) = + (y i)⁻¹ • ContinuousLinearMap.smulRight (eucProj i) (eucProj i) := by + ext v w; simp [ContinuousLinearMap.smulRight_apply, smul_eq_mul, mul_assoc] + rwa [h_clm] at h_smul + have h_sum := (HasFDerivAt.sum (u := univ) (fun i _ ↦ h i)).const_smul α + have h_eq_fun : + (α • (∑ i : Fin d, fun x : EuclideanSpace ℝ (Fin d) ↦ (Real.log (x i)) • eucProj i)) = + unnormEntropyFDeriv α := by + ext x; simp [unnormEntropyFDeriv] + have h_eq_deriv : α • (∑ i, (y i)⁻¹ • ContinuousLinearMap.smulRight (eucProj i) (eucProj i)) = + unnormEntropyHessian α y := rfl + rw [h_eq_deriv] at h_sum + rwa [h_eq_fun] at h_sum + +/-! ### Second-Order Taylor Remainder (MVT) for Bregman Divergence -/ + +theorem bregDiv_unnormEntropy_mvt (α : ℝ) (x y : EuclideanSpace ℝ (Fin d)) + (h_pos : ∀ z ∈ segment ℝ x y, ∀ i, 0 < (z : EuclideanSpace ℝ (Fin d)) i) : + ∃ z ∈ segment ℝ x y, + D_[unnormEntropy α](x, y, unnormEntropyFDeriv α y) = (α / 2) * ∑ i, (x i - y i)^2 / z i := by + obtain ⟨z, hz, hz_eq⟩ := bregDiv_mvt x y + (fun z hz ↦ hasFDerivAt_unnormEntropy α z (h_pos z hz)) + (fun z hz ↦ hasFDerivAt_unnormEntropyFDeriv α z (h_pos z hz)) + exact ⟨z, hz, by rw [hz_eq, unnormEntropyHessian_apply]; simp_rw [PiLp.sub_apply, sq]; ring⟩ + +/-! ### Convexity of Regularizer -/ + +/-- Convexity of scaled unnormalized negative entropy on the non-negative orthant +$\{x \mid \forall i, 0 \le x_i\}$ for $\alpha \ge 0$. -/ +theorem convexOn_unnormEntropy_nonneg (α : ℝ) (hα : 0 ≤ α) : + ConvexOn ℝ {x : EuclideanSpace ℝ (Fin d) | ∀ i, 0 ≤ x i} (unnormEntropy α) := by + refine ⟨fun x hx y hy a b ha hb _ i ↦ add_nonneg (mul_nonneg ha (hx i)) (mul_nonneg hb (hy i)), + fun x hx y hy a b ha hb hab ↦ ?_⟩ + dsimp [unnormEntropy] + have h_base : ∑ i, ((a * x i + b * y i) * Real.log (a * x i + b * y i) - (a * x i + b * y i)) ≤ + a * ∑ i, (x i * Real.log (x i) - x i) + b * ∑ i, (y i * Real.log (y i) - y i) := by + rw [mul_sum, mul_sum, ← sum_add_distrib] + exact sum_le_sum fun i _ ↦ by + have := Real.convexOn_mul_log.2 (hx i) (hy i) ha hb hab + dsimp at this; linarith + have := mul_le_mul_of_nonneg_left h_base hα + linarith + +/-- Convexity of scaled unnormalized negative entropy on the standard simplex `stdSimplex` +for $\alpha \ge 0$. -/ +theorem convexOn_unnormEntropy_stdSimplex (α : ℝ) (hα : 0 ≤ α) : + ConvexOn ℝ (stdSimplex (d := d)) (unnormEntropy α) := + (convexOn_unnormEntropy_nonneg α hα).subset (fun _ hx ↦ (mem_stdSimplex_iff _).mp hx |>.1) + convex_stdSimplex + +/-- Non-negativity of unnormalized negative entropy Bregman divergence for $\alpha \ge 0$: +$$D_{\psi_\alpha}(x, y) \ge 0 \quad \text{for } x, y > 0.$$ -/ +lemma bregDiv_unnormEntropy_nonneg (α : ℝ) (hα : 0 ≤ α) (x y : EuclideanSpace ℝ (Fin d)) + (hx : ∀ i, 0 < x i) (hy : ∀ i, 0 < y i) : + 0 ≤ D_[unnormEntropy α](x, y, unnormEntropyFDeriv α y) := + (hasFDerivAt_unnormEntropy α y hy).hasSubgradientWithinAt + (convexOn_unnormEntropy_nonneg α hα) (fun i ↦ (hy i).le) x (fun i ↦ (hx i).le) + +/-! ### Shifted Regularizer -/ + +/-- Shifted unnormalized negative entropy regularizer with offset $\alpha (\ln d + 1)$: +$$\psi^{\mathrm{shift}}_\alpha(x) = \psi_\alpha(x) + \alpha (\ln d + 1)$$ -/ +noncomputable def unnormEntropyShifted (α : ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ := + unnormEntropy α x + α * (Real.log d + 1) + +lemma unnormEntropyShifted_smul (α : ℝ) (x : EuclideanSpace ℝ (Fin d)) : + unnormEntropyShifted α x = α • unnormEntropyShifted 1 x := by + dsimp [unnormEntropyShifted, unnormEntropy]; ring + +@[simp] +lemma bregDiv_unnormEntropyShifted (α : ℝ) (x y : EuclideanSpace ℝ (Fin d)) : + D_[unnormEntropyShifted α](x, y, unnormEntropyFDeriv α y) = + D_[unnormEntropy α](x, y, unnormEntropyFDeriv α y) := by + dsimp [bregDiv, unnormEntropyShifted]; ring + +/-- The Bregman divergence $D_{\psi_\alpha}(u, w_1)$ from the uniform distribution $w_1$ to any +comparator $u \in \Delta^{d-1}$ is exactly $\alpha (\ln d + \sum_{i=1}^d u_i \ln u_i)$. -/ +theorem bregDiv_unnormEntropy_uniformSimplex (α : ℝ) (hd : 0 < d) (u : EuclideanSpace ℝ (Fin d)) + (hu : u ∈ stdSimplex (d := d)) : + D_[unnormEntropy α](u, uniformSimplex d, unnormEntropyFDeriv α (uniformSimplex d)) = + α * (Real.log d + ∑ i, u i * Real.log (u i)) := by + have hu_sum := (mem_stdSimplex_iff u).mp hu |>.2 + have hw_sum : ∑ i, uniformSimplex d i = 1 := (mem_stdSimplex_uniformSimplex hd).2 + have hlog (i : Fin d) : Real.log (uniformSimplex d i) = -Real.log d := by + simp [uniformSimplex_apply, one_div, Real.log_inv] + rw [bregDiv, unnormEntropy, unnormEntropy, unnormEntropyFDeriv_apply] + simp_rw [sum_sub_distrib, hlog, PiLp.sub_apply, ← sum_mul, sum_sub_distrib, hw_sum, hu_sum] + ring + +/-- For any comparator $u \in \Delta^{d-1}$, the entropy sum $\sum_{i=1}^d u_i \ln u_i \le 0$. -/ +lemma sum_mul_log_nonpos_of_mem_stdSimplex {u : EuclideanSpace ℝ (Fin d)} + (hu : u ∈ stdSimplex (d := d)) : + ∑ i, u i * Real.log (u i) ≤ 0 := by + rw [mem_stdSimplex_iff] at hu + refine sum_nonpos fun i _ ↦ ?_ + by_cases h0 : u i = 0 + · simp [h0] + · have h_le1 : u i ≤ 1 := by + have : u i ≤ ∑ j, u j := single_le_sum (fun j _ ↦ hu.1 j) (Finset.mem_univ i) + rwa [hu.2] at this + have hlog_nonpos : Real.log (u i) ≤ 0 := Real.log_nonpos (hu.1 i) h_le1 + exact mul_nonpos_of_nonneg_of_nonpos (hu.1 i) hlog_nonpos + +/-- For any comparator $u \in \Delta^{d-1}$ and $\alpha \ge 0$, the Bregman divergence from the +uniform distribution is upper-bounded by $\alpha \ln d$: +$$D_{\psi_\alpha}(u, w_1) \le \alpha \ln d.$$ -/ +theorem bregDiv_unnormEntropy_uniformSimplex_le (α : ℝ) (hα : 0 ≤ α) (hd : 0 < d) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex (d := d)) : + D_[unnormEntropy α](u, uniformSimplex d, unnormEntropyFDeriv α (uniformSimplex d)) ≤ + α * Real.log d := by + rw [bregDiv_unnormEntropy_uniformSimplex α hd u hu] + have h_nonpos := sum_mul_log_nonpos_of_mem_stdSimplex hu + nlinarith + +/-- The shifted unnormalized negative entropy evaluates to zero at the uniform distribution +$w_1 = (1/d, \dots, 1/d)$. -/ +lemma unnormEntropyShifted_uniformSimplex (hd : 0 < d) (α : ℝ) : + unnormEntropyShifted α (uniformSimplex d) = 0 := by + rw [unnormEntropyShifted, unnormEntropy] + have hlog : ∀ i : Fin d, Real.log (uniformSimplex d i) = -Real.log d := by + intro i; simp [uniformSimplex_apply, one_div, Real.log_inv] + have hw_sum : ∑ i, uniformSimplex d i = 1 := (mem_stdSimplex_uniformSimplex hd).2 + simp_rw [sum_sub_distrib, hlog, ← sum_mul, hw_sum, one_mul] + ring + +/-- For any comparator $u \in \Delta^{d-1}$ and $\alpha \ge 0$, the shifted unnormalized negative +entropy is upper-bounded by $\alpha \ln d$: +$$\psi^{\mathrm{shift}}_\alpha(u) \le \alpha \ln d.$$ -/ +theorem unnormEntropyShifted_le_log_card (α : ℝ) (hα : 0 ≤ α) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex (d := d)) : + unnormEntropyShifted α u ≤ α * Real.log d := by + dsimp [unnormEntropyShifted, unnormEntropy] + have hu_sum : ∑ i, (u i * Real.log (u i) - u i) = (∑ i, u i * Real.log (u i)) - 1 := by + rw [sum_sub_distrib, (mem_stdSimplex_iff u).mp hu |>.2] + have h_nonpos := sum_mul_log_nonpos_of_mem_stdSimplex hu + rw [hu_sum] + nlinarith + +/-- Base shifted regularizer $\psi^{\mathrm{shift}}_1(x) \ge 0$ on the standard simplex +$\Delta^{d-1}$ when $d > 0$. -/ +theorem unnormEntropyShifted_nonneg_of_mem_stdSimplex (hd : 0 < d) (x : EuclideanSpace ℝ (Fin d)) + (hx : x ∈ stdSimplex (d := d)) : + 0 ≤ unnormEntropyShifted 1 x := by + have hw_pos : ∀ i, 0 < uniformSimplex d i := uniformSimplex_pos hd + have hw_mem : uniformSimplex d ∈ stdSimplex (d := d) := mem_stdSimplex_uniformSimplex hd + have h_sub := (hasFDerivAt_unnormEntropy 1 (uniformSimplex d) hw_pos).hasSubgradientWithinAt + (convexOn_unnormEntropy_stdSimplex 1 (by norm_num)) hw_mem x hx + rw [bregDiv_unnormEntropy_uniformSimplex 1 hd x hx, one_mul] at h_sub + have h_sum : ∑ i, (x i * Real.log (x i) - x i) = (∑ i, x i * Real.log (x i)) - 1 := by + rw [sum_sub_distrib, (mem_stdSimplex_iff x).mp hx |>.2] + dsimp [unnormEntropyShifted, unnormEntropy]; rw [h_sum]; linarith + +end Online.OCO.LEA diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Shift.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Shift.lean new file mode 100644 index 00000000..7ab260a0 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Shift.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer + +/-! +# Shift Term Bound for LEA Regularizers + +This file bounds the regularizer potential shift term: +$$\mathrm{shift}(t) = -(\psi_{t+1} - \psi_t)(w_{t+1})$$ +when the time-dependent regularizers are scaled versions $\psi_t = \alpha_t \psi_0$ of a base +regularizer $\psi_0$. + +With a non-negative regularizer $\psi_0 \ge 0$ and decreasing step sizes $\eta_t$ +(i.e., non-decreasing regularization weights $\alpha_t \le \alpha_{t+1}$ where +$\alpha_t \propto 1/\eta_t$), the shift terms are non-positive ($\mathrm{shift}(t) \le 0$), +contributing non-positively to regret. + +## Main definitions + +* `shift`: Potential shift $-(\psi_{t+1} - \psi_t)(w_{t+1})$. + +## Main results + +* `shift_nonpos_of_nondecreasing`: + $\alpha_t \le \alpha_{t+1}$ and $\psi_0(w_{t+1}) \ge 0 \implies \mathrm{shift}(t) \le 0$. +* `sum_shift_nonpos_of_nondecreasing`: + $\sum_{t=1}^T \mathrm{shift}(t) \le 0$ under non-decreasing weights and non-negative regularizer. +* `sum_shift_unnormEntropyShifted_nonpos`: + Cumulative shift with shifted unnormalized negative entropy regularizers + $\psi^{\mathrm{shift}}_t = \text{unnormEntropyShifted}(\alpha_t)$ is unconditionally non-positive + for iterates on the simplex. +-/ + +open scoped BigOperators +open Finset + +@[expose] public section + +namespace Online.OCO.LEA + +variable {E : Type*} + +/-- If the regularizer weight sequence is non-decreasing ($\alpha_t \le \alpha_{t+1}$) +(i.e., decreasing step sizes $\eta_t = 1/\alpha_t$) +and the base regularizer is non-negative ($\psi_0(x) \ge 0$), +then the shift term is non-positive ($\mathrm{shift}(t) \le 0$). -/ +theorem shift_nonpos_of_nondecreasing (α : ℕ → ℝ) (ψ₀ : E → ℝ) (w : ℕ → E) (t : ℕ) + (h_mono : α t ≤ α (t + 1)) (h_pos : 0 ≤ ψ₀ (w (t + 1))) : + shift (fun s ↦ α s • ψ₀) w t ≤ 0 := by + dsimp [shift] + nlinarith + +/-- Cumulative shift is non-positive when the regularizer weights are non-decreasing +(decreasing step size schedule) and $\psi_0 \ge 0$. -/ +theorem sum_shift_nonpos_of_nondecreasing (α : ℕ → ℝ) (ψ₀ : E → ℝ) (w : ℕ → E) (T : ℕ) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (h_pos : ∀ t ∈ Ico 1 (T + 1), 0 ≤ ψ₀ (w (t + 1))) : + ∑ t ∈ Ico 1 (T + 1), shift (fun s ↦ α s • ψ₀) w t ≤ 0 := + sum_nonpos fun t ht ↦ shift_nonpos_of_nondecreasing α ψ₀ w t (h_mono t ht) (h_pos t ht) + +/-- For shifted regularizers $\psi^{\mathrm{shift}}(t) = \text{unnormEntropyShifted}(\alpha_t)$ +with non-decreasing weights $\alpha_t \le \alpha_{t+1}$ and iterates on the standard simplex +`stdSimplex`, cumulative shift is non-positive. -/ +theorem sum_shift_unnormEntropyShifted_nonpos {d : ℕ} (hd : 0 < d) (α : ℕ → ℝ) + (w : ℕ → EuclideanSpace ℝ (Fin d)) (T : ℕ) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (hw : ∀ t ∈ Ico 1 (T + 2), w t ∈ stdSimplex (d := d)) : + ∑ t ∈ Ico 1 (T + 1), shift (fun s ↦ unnormEntropyShifted (α s)) w t ≤ 0 := by + have h_eq : (fun s ↦ unnormEntropyShifted (α s)) = + fun s ↦ α s • (unnormEntropyShifted 1 : EuclideanSpace ℝ (Fin d) → ℝ) := by + ext s x; exact unnormEntropyShifted_smul (α s) x + rw [h_eq] + refine sum_shift_nonpos_of_nondecreasing α (unnormEntropyShifted 1) w T h_mono fun t ht ↦ ?_ + have hw_succ : w (t + 1) ∈ stdSimplex (d := d) := hw (t + 1) (by rw [mem_Ico] at ht ⊢; omega) + exact unnormEntropyShifted_nonneg_of_mem_stdSimplex hd (w (t + 1)) hw_succ + +end Online.OCO.LEA diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Stability.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Stability.lean new file mode 100644 index 00000000..3b63fbfc --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/Common/Stability.lean @@ -0,0 +1,323 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer + +/-! +# Stability Bound for Learning with Expert Advice (LEA) + +This file proves the local-norm stability bound for Learning with Expert Advice (LEA) +following Orabona (Lemma 7.15 / Lemma 6.32) using the coordinate-wise Fenchel-Young inequality, +the Mean Value Theorem for Bregman divergence, and the unconstrained Exponential Gradient candidate +maximizer to bound the stability term directly using the iterate $w_t$: +$$\sum_{t=1}^T \mathrm{stability}_t \le + \sum_{t=1}^T \frac{1}{2\alpha_t} \sum_{i=1}^d w_{t, i} (g_t)_i^2.$$ + +## Main definitions +* `stability`: One-round stability tradeoff between loss reduction and divergence. +* `expGradCandidate`: Unconstrained exponential gradient candidate maximizer. + +## Main results +* `dual_local_norm_eta_le`: Coordinate-weighted duality bound with step size $\eta$. +* `stability_le_dual_norm`: One-round stability term bound via MVT at + intermediate point $z$. +* `stability_le_dual_norm_wt`: One-round stability bound with iterate $w_t$ + (Orabona Lemma 7.15 / Lemma 6.32). +* `sum_stability_le_dual_norm_wt`: Cumulative stability bound with $w_t$. +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA + +variable {d : ℕ} + +/-! ### Scalar and Coordinate Duality (Fenchel-Young / Local Norms Replacement) + +Mathlib currently does not provide general local norms $\|v\|_{\nabla^2\psi(z)}$ or their duals +$\|g\|_{\nabla^2\psi(z)^{-1}}^*$. For the unnormalized negative entropy regularizer, the Hessian +is diagonal with entries $(\nabla^2\psi(z))_{ii} = 1 / z_i$. + +The lemma `dual_local_norm_eta_le` is the concrete, coordinate-wise replacement: it directly proves +the Fenchel-Young duality bound: +$$\langle \eta g, v \rangle - \frac{1}{2} \|v\|_z^2 \le \frac{\eta^2}{2} \|g\|_{z, *}^2,$$ +where $\|v\|_z^2 = \sum_i v_i^2 / z_i$ and $\|g\|_{z, *}^2 = \sum_i z_i g_i^2$. -/ + +/-- Scaled coordinate-wise duality inequality with learning rate $\eta$: +$$\eta \sum_{i=1}^d v_i g_i - \frac{1}{2} \sum_{i=1}^d \frac{v_i^2}{z_i} + \le \frac{\eta^2}{2} \sum_{i=1}^d z_i g_i^2.$$ + +This serves as the concrete coordinate replacement for the local-norm Fenchel-Young inequality +$\langle \eta g, v \rangle - \frac{1}{2} \|v\|_z^2 \le \frac{\eta^2}{2} (\|g\|_z^*)^2$. -/ +lemma dual_local_norm_eta_le (η : ℝ) (v : EuclideanSpace ℝ (Fin d)) (g : Fin d → ℝ) + (z : EuclideanSpace ℝ (Fin d)) (hz : ∀ i, 0 < z i) : + η * (∑ i, v i * g i) - (1 / 2 : ℝ) * (∑ i, (v i) ^ 2 / z i) ≤ + (η ^ 2 / 2) * ∑ i, z i * (g i) ^ 2 := by + calc η * (∑ i, v i * g i) - (1 / 2 : ℝ) * (∑ i, (v i) ^ 2 / z i) + _ = ∑ i, (v i * (η * g i) - (1 / 2 : ℝ) * ((v i) ^ 2 / z i)) := by + rw [mul_sum, mul_sum, ← sum_sub_distrib]; congr 1 with i; ring + _ ≤ ∑ i, (1 / 2 : ℝ) * (z i * (η * g i) ^ 2) := sum_le_sum fun i _ ↦ by + have h_sq := div_nonneg (sq_nonneg (v i - z i * (η * g i))) (hz i).le + have : (v i - z i * (η * g i))^2 / z i = + (v i)^2 / z i - 2 * (v i * (η * g i)) + z i * (η * g i)^2 := by + field_simp [(hz i).ne']; ring + linarith + _ = (η ^ 2 / 2) * ∑ i, z i * (g i) ^ 2 := by + rw [mul_sum]; congr 1 with i; ring + +/-- One-round stability bound for Learning with Expert Advice via the Mean Value Theorem (MVT): +when $w_{t+1} \in \text{stdSimplex}$, and iterates $w_{t+1}, w_t$ have strictly positive +coordinates, the round-$t$ stability term with regularizer scale $\alpha_t > 0$ +`stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t` +is upper bounded by $\frac{1}{2 \alpha_t} \sum_{i=1}^d z_i (g_t)_i^2$ +for some intermediate point $z \in [w_{t+1}, w_t]$. -/ +theorem stability_le_dual_norm (w : ℕ → EuclideanSpace ℝ (Fin d)) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (α : ℕ → ℝ) (t : ℕ) (hα_pos : 0 < α t) + (hw_next_pos : ∀ i, 0 < w (t + 1) i) + (hw_t_pos : ∀ i, 0 < w t i) : + ∃ z ∈ segment ℝ (w (t + 1)) (w t), + stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t ≤ + (1 / (2 * α t)) * ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + have h_pos : ∀ z ∈ segment ℝ (w (t + 1)) (w t), ∀ i, 0 < (z : EuclideanSpace ℝ (Fin d)) i := by + rintro z ⟨a, b, ha, hb, hab, rfl⟩ i + dsimp + obtain rfl | ha_pos := eq_or_lt_of_le ha + · have : b = 1 := by linarith + simp [this, hw_t_pos i] + · linarith [mul_pos ha_pos (hw_next_pos i), mul_nonneg hb (hw_t_pos i).le] + obtain ⟨z, hz_seg, hz_breg⟩ := bregDiv_unnormEntropy_mvt (α t) (w (t + 1)) (w t) h_pos + refine ⟨z, hz_seg, ?_⟩ + dsimp [stability] + rw [bregDiv_unnormEntropyShifted, hz_breg] + have h_decomp : g t (w t - w (t + 1)) = + ∑ i, (w t i - w (t + 1) i) * g t (EuclideanSpace.basisFun (Fin d) ℝ i) := by + have : w t - w (t + 1) = + ∑ i, (w t i - w (t + 1) i) • EuclideanSpace.basisFun (Fin d) ℝ i := by + ext i; simp [EuclideanSpace.basisFun_apply, Pi.single_apply] + rw [this, map_sum] + refine sum_congr rfl fun i _ ↦ by rw [map_smul, smul_eq_mul] + simp_rw [show ∀ i, (w (t + 1) i - w t i)^2 = (w t i - w (t + 1) i)^2 from + fun i ↦ by rw [← neg_sub (w t i) (w (t + 1) i), neg_sq]] + have h_dual := dual_local_norm_eta_le (1 / α t) (w t - w (t + 1)) + (fun i ↦ g t (EuclideanSpace.basisFun (Fin d) ℝ i)) z (h_pos z hz_seg) + have h_pi (i : Fin d) : (w t - w (t + 1)) i = w t i - w (t + 1) i := rfl + simp_rw [h_pi] at h_dual + have h_mult := mul_le_mul_of_nonneg_left h_dual hα_pos.le + have h_rw : α t * ((1 / α t) * ∑ i, (w t i - w (t + 1) i) * + g t (EuclideanSpace.basisFun (Fin d) ℝ i) - (1 / 2 : ℝ) * + ∑ i, (w t i - w (t + 1) i) ^ 2 / z i) = + (∑ i, (w t i - w (t + 1) i) * g t (EuclideanSpace.basisFun (Fin d) ℝ i)) - + (α t / 2) * ∑ i, (w t i - w (t + 1) i) ^ 2 / z i := by + rw [mul_sub, ← mul_assoc, mul_one_div_cancel hα_pos.ne', one_mul]; ring + have h_rw_rhs : α t * (((1 / α t) ^ 2 / 2) * ∑ i, z i * + (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2) = + (1 / (2 * α t)) * ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + calc α t * (((1 / α t) ^ 2 / 2) * ∑ i, z i * + (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2) + _ = (α t * (1 / (α t ^ 2 * 2))) * ∑ i, z i * + (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by ring + _ = (1 / (2 * α t)) * ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + congr 1; field_simp [hα_pos.ne'] + linarith [h_decomp, h_mult, h_rw, h_rw_rhs] + +/-! ### Stability Bound via Candidate Maximizer (Orabona Lemma 7.15 / Lemma 6.32) -/ + +/-- Stability bound for $w_{t+1} \in s$ derived via a candidate maximizer +$\tilde{w}_{t+1} \in s$: bounds the stability term by the local norm at an +intermediate point $\tilde{z} \in [\tilde{w}_{t+1}, w_t]$ via `stability_le_dual_norm`. -/ +theorem stability_le_dual_norm_of_isMaxOn (w : ℕ → EuclideanSpace ℝ (Fin d)) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (α : ℕ → ℝ) (t : ℕ) (hα_pos : 0 < α t) + (s : Set (EuclideanSpace ℝ (Fin d))) + (hw_next : w (t + 1) ∈ s) + (w_tilde_next : EuclideanSpace ℝ (Fin d)) + (hw_tilde_pos : ∀ i, 0 < w_tilde_next i) + (hw_t_pos : ∀ i, 0 < w t i) + (h_max : IsMaxOn (fun x ↦ (g t) (w t - x) - + D_[unnormEntropyShifted (α t)](x, w t, unnormEntropyFDeriv (α t) (w t))) s + w_tilde_next) : + ∃ z ∈ segment ℝ w_tilde_next (w t), + stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t ≤ + (1 / (2 * α t)) * ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + let w_cand : ℕ → EuclideanSpace ℝ (Fin d) := fun k ↦ + if k = t + 1 then w_tilde_next else w k + have h_cand_next : w_cand (t + 1) = w_tilde_next := ite_eq_left rfl + have h_cand_t : w_cand t = w t := ite_eq_right (show t ≠ t + 1 by omega) + obtain ⟨z, hz_seg, hz_le⟩ := stability_le_dual_norm w_cand g α t hα_pos + (by rw [h_cand_next]; exact hw_tilde_pos) (by rw [h_cand_t]; exact hw_t_pos) + rw [h_cand_next, h_cand_t] at hz_seg + dsimp [stability] at hz_le + rw [h_cand_next, h_cand_t] at hz_le + refine ⟨z, hz_seg, ?_⟩ + have h_le_max : stability (fun s ↦ unnormEntropyShifted (α s)) + (fun s ↦ unnormEntropyFDeriv (α s)) w g t ≤ + (g t) (w t - w_tilde_next) - + D_[unnormEntropyShifted (α t)](w_tilde_next, w t, unnormEntropyFDeriv (α t) (w t)) := by + dsimp [stability] + exact h_max hw_next + linarith + +/-! ### Unconstrained Exponential Gradient Candidate Maximizer -/ + +/-- The unconstrained candidate minimizer $\tilde{w}_{t+1}$ in coordinate form: +$$\tilde{w}_{t+1, i} = w_{t, i} \exp\left(-\frac{\langle g_t, e_i \rangle}{\alpha}\right)$$ -/ +noncomputable def expGradCandidate (α : ℝ) (wt : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : EuclideanSpace ℝ (Fin d) := + WithLp.toLp 2 (fun i ↦ wt i * Real.exp (- (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α)) + +@[simp] +lemma expGradCandidate_apply (α : ℝ) (wt : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + expGradCandidate α wt g i = wt i * Real.exp (- (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α) := + rfl + +lemma expGradCandidate_pos (α : ℝ) (wt : EuclideanSpace ℝ (Fin d)) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (hwt_pos : ∀ i, 0 < wt i) (i : Fin d) : + 0 < expGradCandidate α wt g i := + mul_pos (hwt_pos i) (Real.exp_pos _) + +/-- When $g_i \ge 0$ and $\alpha > 0$, candidate coordinates are bounded above by $w_{t, i}$. -/ +lemma expGradCandidate_le_wt (α : ℝ) (hα_pos : 0 < α) + (wt : EuclideanSpace ℝ (Fin d)) (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) + (hg_nonneg : ∀ i, 0 ≤ g (EuclideanSpace.basisFun (Fin d) ℝ i)) + (hwt_nonneg : ∀ i, 0 ≤ wt i) (i : Fin d) : + expGradCandidate α wt g i ≤ wt i := by + dsimp [expGradCandidate] + have h_div_nonpos : - (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α ≤ 0 := by + rw [neg_div, neg_nonpos] + exact div_nonneg (hg_nonneg i) hα_pos.le + have h_exp_le_one : Real.exp (- (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α) ≤ 1 := by + simpa using Real.exp_le_exp_of_le h_div_nonpos + calc wt i * Real.exp (- (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α) + _ ≤ wt i * 1 := mul_le_mul_of_nonneg_left h_exp_le_one (hwt_nonneg i) + _ = wt i := mul_one (wt i) + +/-- Any point on the segment $[\tilde{w}, w]$ is coordinate-wise bounded above by $w$ +when $\tilde{w} \le w$. -/ +lemma segment_le_of_le (w_tilde w_t : EuclideanSpace ℝ (Fin d)) + (h_le : ∀ i, w_tilde i ≤ w_t i) + (z : EuclideanSpace ℝ (Fin d)) (hz : z ∈ segment ℝ w_tilde w_t) (i : Fin d) : + z i ≤ w_t i := by + rcases hz with ⟨a, b, ha, hb, hab, rfl⟩ + dsimp + calc a * w_tilde i + b * w_t i + _ ≤ a * w_t i + b * w_t i := by + linarith [mul_le_mul_of_nonneg_left (h_le i) ha] + _ = (a + b) * w_t i := by ring + _ = w_t i := by rw [hab, one_mul] + +/-- `expGradCandidate` is the global maximizer on the positive orthant +$\mathcal{X} = \{x \in \mathbb{R}^d \mid \forall i, 0 < x_i\}$ of the unconstrained OMD objective +$x \mapsto \langle g_t, w_t - x \rangle - D_{\psi_{\alpha_t}}(x, w_t)$. -/ +theorem isMaxOn_expGradCandidate (α : ℝ) (hα_pos : 0 < α) + (wt : EuclideanSpace ℝ (Fin d)) (hwt_pos : ∀ i, 0 < wt i) + (g : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + IsMaxOn (fun x ↦ g (wt - x) - + D_[unnormEntropyShifted α](x, wt, unnormEntropyFDeriv α wt)) + {x : EuclideanSpace ℝ (Fin d) | ∀ i, 0 < x i} (expGradCandidate α wt g) := by + set w_cand := expGradCandidate α wt g + have hw_cand_pos : ∀ i, 0 < w_cand i := expGradCandidate_pos α wt g hwt_pos + intro x hx + dsimp + rw [bregDiv_unnormEntropyShifted, bregDiv_unnormEntropyShifted] + have h_diff_grad : (unnormEntropyFDeriv α wt - unnormEntropyFDeriv α w_cand) = g := by + ext v + simp only [unnormEntropyFDeriv_apply, sub_apply] + have h_log_ratio (i : Fin d) : Real.log (wt i) - Real.log (w_cand i) = + (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α := by + have h_cand_i : w_cand i = + wt i * Real.exp (- (g (EuclideanSpace.basisFun (Fin d) ℝ i)) / α) := rfl + rw [h_cand_i, Real.log_mul (hwt_pos i).ne' (Real.exp_pos _).ne', Real.log_exp] + ring + have h_g_sum : g v = ∑ i, v i * g (EuclideanSpace.basisFun (Fin d) ℝ i) := by + have : v = ∑ i, v i • EuclideanSpace.basisFun (Fin d) ℝ i := by + ext i; simp [EuclideanSpace.basisFun_apply, Pi.single_apply] + conv_lhs => rw [this] + rw [map_sum] + refine sum_congr rfl fun i _ ↦ by rw [map_smul, smul_eq_mul] + have h_rw_sum : α * ∑ i, v i * (Real.log (wt i) - Real.log (w_cand i)) = + ∑ i, v i * g (EuclideanSpace.basisFun (Fin d) ℝ i) := by + rw [mul_sum] + refine sum_congr rfl fun i _ ↦ by + rw [h_log_ratio i] + have hα_ne : α ≠ 0 := hα_pos.ne' + rw [mul_left_comm, mul_div_cancel₀ _ hα_ne] + rw [← mul_sub, ← sum_sub_distrib] + have h_dist : (∑ i, (v i * Real.log (wt i) - v i * Real.log (w_cand i))) = + ∑ i, v i * (Real.log (wt i) - Real.log (w_cand i)) := + sum_congr rfl fun i _ ↦ by ring + rw [h_dist, h_rw_sum, ← h_g_sum] + have h_three := bregDiv_three_point (f := unnormEntropy α) (z := x) (x := w_cand) (y := wt) + (J_x := unnormEntropyFDeriv α w_cand) (J_y := unnormEntropyFDeriv α wt) + have h_grad_eval : (unnormEntropyFDeriv α wt - unnormEntropyFDeriv α w_cand) (x - w_cand) = + g (x - w_cand) := by rw [h_diff_grad] + rw [h_grad_eval] at h_three + have h_lin : g (wt - w_cand) - g (wt - x) = g (x - w_cand) := by + have : wt - w_cand - (wt - x) = x - w_cand := by ext; simp + rw [← map_sub, this] + have h_nonneg := bregDiv_unnormEntropy_nonneg α hα_pos.le x w_cand hx hw_cand_pos + linarith [h_three, h_lin, h_nonneg] + +/-- Stability bound for strictly positive iterates $w_t, w_{t+1} > 0$ when losses +are non-negative $g_t \ge 0$: bounds the stability term directly with $w_t$ instead of +the intermediate point $z$. -/ +theorem stability_le_dual_norm_wt (w : ℕ → EuclideanSpace ℝ (Fin d)) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (α : ℕ → ℝ) (t : ℕ) (hα_pos : 0 < α t) + (hw_next_pos : ∀ i, 0 < w (t + 1) i) + (hw_t_pos : ∀ i, 0 < w t i) + (hg_nonneg : ∀ i, 0 ≤ g t (EuclideanSpace.basisFun (Fin d) ℝ i)) : + stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t ≤ + (1 / (2 * α t)) * ∑ i, w t i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + have h_max := isMaxOn_expGradCandidate (α t) hα_pos (w t) hw_t_pos (g t) + have hw_next_mem : w (t + 1) ∈ {x : EuclideanSpace ℝ (Fin d) | ∀ i, 0 < x i} := hw_next_pos + obtain ⟨z, hz_seg, hz_le⟩ := stability_le_dual_norm_of_isMaxOn w g α t hα_pos + {x | ∀ i, 0 < x i} hw_next_mem (expGradCandidate (α t) (w t) (g t)) + (expGradCandidate_pos (α t) (w t) (g t) hw_t_pos) hw_t_pos h_max + have hz_le_wt (i : Fin d) : z i ≤ w t i := by + refine segment_le_of_le (expGradCandidate (α t) (w t) (g t)) (w t) ?_ z hz_seg i + intro j + exact expGradCandidate_le_wt (α t) hα_pos (w t) (g t) hg_nonneg (fun k ↦ (hw_t_pos k).le) j + have h_sum_le : ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 ≤ + ∑ i, w t i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + refine sum_le_sum fun i _ ↦ ?_ + exact mul_le_mul_of_nonneg_right (hz_le_wt i) (sq_nonneg _) + have h_factor_pos : 0 ≤ 1 / (2 * α t) := by + refine div_nonneg zero_le_one (mul_nonneg (by norm_num) hα_pos.le) + calc stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t + _ ≤ (1 / (2 * α t)) * ∑ i, z i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := hz_le + _ ≤ (1 / (2 * α t)) * ∑ i, w t i * + (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := + mul_le_mul_of_nonneg_left h_sum_le h_factor_pos + +/-- Multi-round cumulative stability bound for strictly positive iterates $w_t, w_{t+1} > 0$ +when losses are non-negative $g_t \ge 0$: +$$\sum_{t=1}^T \mathrm{stability}_t \le + \sum_{t=1}^T \frac{1}{2\alpha_t} \sum_{i=1}^d w_{t, i} (g_t)_i^2.$$ -/ +theorem sum_stability_le_dual_norm_wt (w : ℕ → EuclideanSpace ℝ (Fin d)) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (α : ℕ → ℝ) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 1), 0 < α t) + (hw_pos : ∀ t ∈ Ico 1 (T + 2), ∀ i, 0 < w t i) + (hg_nonneg : ∀ t ∈ Ico 1 (T + 1), + ∀ i, 0 ≤ g t (EuclideanSpace.basisFun (Fin d) ℝ i)) : + ∑ t ∈ Ico 1 (T + 1), + stability (fun s ↦ unnormEntropyShifted (α s)) (fun s ↦ unnormEntropyFDeriv (α s)) w g t ≤ + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * + ∑ i, w t i * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + refine sum_le_sum fun t ht ↦ ?_ + have hw_next_pos : ∀ i, 0 < w (t + 1) i := by + rw [mem_Ico] at ht + exact hw_pos (t + 1) (by rw [mem_Ico]; omega) + have hw_t_pos : ∀ i, 0 < w t i := by + rw [mem_Ico] at ht + exact hw_pos t (by rw [mem_Ico]; omega) + exact stability_le_dual_norm_wt w g α t (hα_pos t ht) + hw_next_pos hw_t_pos (hg_nonneg t ht) + +end Online.OCO.LEA diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Boundary.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Boundary.lean new file mode 100644 index 00000000..4ab55c54 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Boundary.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer + +/-! +# Boundary Term Bound for Follow-the-Regularized-Leader (FTRL) + +This file bounds the boundary term +$$\mathrm{boundary}(\psi, u, w, T) = \psi_{T+1}(u) - \psi_1(w_1)$$ +for FTRL with shifted unnormalized negative entropy regularizers $\psi^{\mathrm{shift}}_t$. + +## Main results + +* `boundary_shifted_le_log_card`: Boundary term bound: + $$\mathrm{boundary}(\psi^{\mathrm{shift}}_\alpha, u, w, T) \le + \alpha_1 \ln d + (\psi^{\mathrm{shift}}_{\alpha(T+1)}(u) - + \psi^{\mathrm{shift}}_{\alpha 1}(u)).$$ +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.FTRL + +variable {d : ℕ} + +/-- Boundary term bound for FTRL with uniform initialization $w_1 = (1/d, \dots, 1/d)$ and +sequence of shifted regularizers $\psi^{\mathrm{shift}}_t = \text{unnormEntropyShifted}(\alpha_t)$: +$$\mathrm{boundary}(\psi^{\mathrm{shift}}_\alpha, u, w, T) + = \psi^{\mathrm{shift}}_{\alpha(T+1)}(u) - \psi^{\mathrm{shift}}_{\alpha 1}(w_1) + \le \alpha_1 \ln d + (\psi^{\mathrm{shift}}_{\alpha(T+1)}(u) - + \psi^{\mathrm{shift}}_{\alpha 1}(u)).$$ -/ +theorem boundary_shifted_le_log_card (α : ℕ → ℝ) (hα1 : 0 ≤ α 1) (T : ℕ) + (hd : 0 < d) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex (d := d)) + (w : ℕ → EuclideanSpace ℝ (Fin d)) + (hw1 : w 1 = uniformSimplex d) : + boundary (fun t ↦ unnormEntropyShifted (α t)) u w T ≤ + α 1 * Real.log d + (unnormEntropyShifted (α (T + 1)) u - unnormEntropyShifted (α 1) u) := by + dsimp [boundary] + rw [hw1, unnormEntropyShifted_uniformSimplex hd, sub_zero] + have hu_le := unnormEntropyShifted_le_log_card (α 1) hα1 u hu + linarith + +end Online.OCO.LEA.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Formula.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Formula.lean new file mode 100644 index 00000000..386fddfb --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Formula.lean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Regularizer +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Optimality +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# Exponential Weights Update Formula for Follow-the-Regularized-Leader (FTRL) + +This file defines the explicit closed-form Exponential Weights update for FTRL with cumulative +linearized losses and unnormalized negative entropy regularizer with scale $\alpha_t > 0$: + +$$w_{t, i} = \frac{\exp\left(- \frac{1}{\alpha_t} \sum_{k=1}^{t-1} g_{k, i}\right)} + {\sum_{j=1}^d \exp\left(- \frac{1}{\alpha_t} \sum_{k=1}^{t-1} g_{k, j}\right)}.$$ + +## Main definitions +* `expWeight`: The standard exponential weight predictor. +* `expWeights`: The full sequence of Exponential Weights (FTRL) iterates. + +## Main results +* `expWeight_pos`: Strict positivity in each coordinate. +* `expWeight_mem_stdSimplex`: Membership $w_t \in \Delta^{d-1}$. +* `expWeight_isMinOn`: Minimizer property of $w_t$ + for $F_t$ on $\Delta^{d-1}$. +* `expWeights_optimality_nonneg`: Non-negativity of per-round optimality. +* `expWeights_terminalOptimality_nonpos`: Non-positivity of terminal + optimality. +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.FTRL + +variable {d : ℕ} + +/-- Coordinate-wise unnormalized weight for FTRL with cumulative linear losses: +$$\exp\left(- \frac{1}{\alpha} \sum_{k=1}^{t-1} g_{k, i}\right)$$ -/ +noncomputable def expWeightUnnorm (α : ℝ) (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) + (i : Fin d) : ℝ := + Real.exp (- (g_cum (EuclideanSpace.basisFun (Fin d) ℝ i)) / α) + +lemma expWeightUnnorm_pos (α : ℝ) (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + 0 < expWeightUnnorm α g_cum i := by + dsimp [expWeightUnnorm] + exact Real.exp_pos _ + +lemma sum_expWeightUnnorm_pos (hd : 0 < d) (α : ℝ) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + 0 < ∑ i, expWeightUnnorm α g_cum i := by + have : (univ : Finset (Fin d)).Nonempty := + Finset.univ_nonempty_iff.mpr (Fin.pos_iff_nonempty.mp hd) + exact sum_pos (fun i _ ↦ expWeightUnnorm_pos α g_cum i) this + +/-- The normalized exponential weights vector: +$$w_i = \frac{\exp\left(- \frac{1}{\alpha} g_{\mathrm{cum}, i}\right)} + {\sum_j \exp\left(- \frac{1}{\alpha} g_{\mathrm{cum}, j}\right)}$$ -/ +noncomputable def expWeight (_hd : 0 < d) (α : ℝ) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : EuclideanSpace ℝ (Fin d) := + WithLp.toLp 2 (fun i ↦ expWeightUnnorm α g_cum i / ∑ j, expWeightUnnorm α g_cum j) + +lemma expWeight_apply (hd : 0 < d) (α : ℝ) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + expWeight hd α g_cum i = + expWeightUnnorm α g_cum i / ∑ j, expWeightUnnorm α g_cum j := + rfl + +lemma expWeight_pos (hd : 0 < d) (α : ℝ) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + 0 < expWeight hd α g_cum i := by + rw [expWeight_apply] + exact div_pos (expWeightUnnorm_pos α g_cum i) + (sum_expWeightUnnorm_pos hd α g_cum) + +lemma expWeight_mem_stdSimplex (hd : 0 < d) (α : ℝ) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + expWeight hd α g_cum ∈ stdSimplex (d := d) := by + rw [mem_stdSimplex_iff] + refine ⟨fun i ↦ (expWeight_pos hd α g_cum i).le, ?_⟩ + simp_rw [expWeight_apply, ← sum_div] + exact div_self (sum_expWeightUnnorm_pos hd α g_cum).ne' + +lemma expWeight_log_apply (hd : 0 < d) (α : ℝ) (_hα : 0 < α) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) (i : Fin d) : + Real.log (expWeight hd α g_cum i) = + - (g_cum (EuclideanSpace.basisFun (Fin d) ℝ i)) / α - + Real.log (∑ j, expWeightUnnorm α g_cum j) := by + rw [expWeight_apply, Real.log_div (expWeightUnnorm_pos α g_cum i).ne' + (sum_expWeightUnnorm_pos hd α g_cum).ne'] + dsimp [expWeightUnnorm] + rw [Real.log_exp] + +/-- The gradient of the objective $F(x) = \psi_\alpha(x) + g_{\mathrm{cum}}(x)$ at +$w = \mathrm{expWeight}(hd, \alpha, g_{\mathrm{cum}})$ applied to any difference +$(x - w)$ in the affine tangent space of $\Delta^{d-1}$ vanishes identically. -/ +lemma ftrl_obj_diff_eq (hd : 0 < d) (α : ℝ) (hα : 0 < α) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) + (x : EuclideanSpace ℝ (Fin d)) (hx : x ∈ stdSimplex (d := d)) : + (g_cum + unnormEntropyFDeriv α (expWeight hd α g_cum)) + (x - expWeight hd α g_cum) = 0 := by + let w := expWeight hd α g_cum + have hw_mem := expWeight_mem_stdSimplex hd α g_cum + rw [mem_stdSimplex_iff] at hx hw_mem + have h_basis (y : EuclideanSpace ℝ (Fin d)) : + g_cum y = ∑ i, y i * g_cum (EuclideanSpace.basisFun (Fin d) ℝ i) := by + have hy : y = ∑ i, y i • EuclideanSpace.basisFun (Fin d) ℝ i := by + ext i; simp [EuclideanSpace.basisFun_apply, Pi.single_apply] + conv_lhs => rw [hy] + rw [map_sum] + refine sum_congr rfl fun i _ ↦ by rw [map_smul, smul_eq_mul] + simp only [add_apply, unnormEntropyFDeriv_apply] + have h_w_i (i : Fin d) : + g_cum (EuclideanSpace.basisFun (Fin d) ℝ i) + α * Real.log (w i) = + - α * Real.log (∑ j, expWeightUnnorm α g_cum j) := by + have hlog := expWeight_log_apply hd α hα g_cum i + dsimp [w] + rw [hlog] + have hα_ne : α ≠ 0 := hα.ne' + field_simp + ring + have h_comb : (g_cum (x - w) + α * ∑ i, (x - w) i * Real.log (w i)) = + ∑ i, (x i - w i) * + (g_cum (EuclideanSpace.basisFun (Fin d) ℝ i) + α * Real.log (w i)) := by + rw [h_basis (x - w)] + simp only [PiLp.sub_apply, mul_sum, ← sum_add_distrib] + congr 1 with i + ring + rw [h_comb] + simp_rw [h_w_i] + rw [← sum_mul, sum_sub_distrib, hx.2, hw_mem.2, sub_self, zero_mul] + +/-- The vector $w = \mathrm{expWeight}(hd, \alpha, g_{\mathrm{cum}})$ minimizes the +FTRL objective $F(x) = \psi_\alpha(x) + g_{\mathrm{cum}}(x)$ over the standard simplex. -/ +lemma isMinOn_expWeight (hd : 0 < d) (α : ℝ) (hα : 0 < α) + (g_cum : EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ) : + IsMinOn (fun x ↦ unnormEntropy α x + g_cum x) (stdSimplex (d := d)) + (expWeight hd α g_cum) := by + set w := expWeight hd α g_cum + have hw_mem := expWeight_mem_stdSimplex hd α g_cum + have hw_pos : ∀ i, 0 < w i := expWeight_pos hd α g_cum + have h_diff : HasFDerivAt (unnormEntropy α) (unnormEntropyFDeriv α w) w := + hasFDerivAt_unnormEntropy α w hw_pos + have h_conv : ConvexOn ℝ (stdSimplex (d := d)) (unnormEntropy α) := + convexOn_unnormEntropy_stdSimplex α hα.le + have h_obj_conv : ConvexOn ℝ (stdSimplex (d := d)) (unnormEntropy α + ⇑g_cum) := + h_conv.add (g_cum.toLinearMap.convexOn h_conv.1) + have h_obj_diff : HasFDerivAt (unnormEntropy α + ⇑g_cum) + (unnormEntropyFDeriv α w + g_cum) w := + h_diff.add g_cum.hasFDerivAt + intro x hx + have h_zero : (unnormEntropyFDeriv α w + g_cum) (x - w) = 0 := by + have := ftrl_obj_diff_eq hd α hα g_cum x hx + have h_comm : (unnormEntropyFDeriv α w + g_cum) (x - w) = + (g_cum + unnormEntropyFDeriv α w) (x - w) := by + simp only [add_apply] + ring + rwa [h_comm] + have h_subg_base := (hasSubgradientWithinAt_iff_le.mp + (h_obj_diff.hasSubgradientWithinAt h_obj_conv hw_mem)) x hx + dsimp [bregDiv] at h_subg_base + rw [h_zero, add_zero] at h_subg_base + exact h_subg_base + +/-- Full trajectory of Exponential Weights (FTRL) iterates at each round $t \ge 1$: +$$w_t = \mathrm{expWeights}\left(hd, \alpha_t, \sum_{i=1}^{t-1} g_i\right).$$ -/ +noncomputable def expWeights (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) : EuclideanSpace ℝ (Fin d) := + expWeight hd (α t) (∑ i ∈ Ico 1 t, g i) + +lemma expWeights_pos (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) (i : Fin d) : + 0 < expWeights hd α g t i := + expWeight_pos hd (α t) (∑ i ∈ Ico 1 t, g i) i + +@[simp] +lemma expWeights_one (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) : + expWeights hd α g 1 = uniformSimplex d := by + ext i + rw [expWeights, expWeight_apply] + have h_sum_zero : (∑ i ∈ Ico 1 1, g i) = 0 := by simp + dsimp [expWeightUnnorm] + simp only [h_sum_zero, zero_apply, neg_zero, zero_div, Real.exp_zero, + sum_const, card_univ, Fintype.card_fin, nsmul_eq_mul, mul_one, + one_div] + +lemma expWeights_mem_stdSimplex (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) : + expWeights hd α g t ∈ stdSimplex (d := d) := + expWeight_mem_stdSimplex hd (α t) (∑ i ∈ Ico 1 t, g i) + +/-- The iterates generated by `expWeights` satisfy the `IsMinOn` condition +at each round $t \ge 1$. -/ +theorem expWeights_isMinOn (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) (hα_pos : 0 < α t) : + IsMinOn (FObj (fun t x ↦ unnormEntropy (α t) x) g t) + (stdSimplex (d := d)) (expWeights hd α g t) := by + have := isMinOn_expWeight hd (α t) hα_pos (∑ i ∈ Ico 1 t, g i) + have h_eq : (fun x ↦ unnormEntropy (α t) x + (∑ i ∈ Ico 1 t, g i) x) = + FObj (fun t x ↦ unnormEntropy (α t) x) g t := by + ext x + dsimp [FObj] + rw [_root_.sum_apply] + rwa [h_eq] at this + +/-- The iterates generated by `expWeights` satisfy the terminal `IsMinOn` condition +at horizon $T$. -/ +theorem expWeights_terminal_isMinOn (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (T : ℕ) (hα_pos : 0 < α (T + 1)) : + IsMinOn (FObj (fun t x ↦ unnormEntropy (α t) x) g (T + 1)) + (stdSimplex (d := d)) (expWeights hd α g (T + 1)) := by + have := isMinOn_expWeight hd (α (T + 1)) hα_pos (∑ i ∈ Ico 1 (T + 1), g i) + have h_eq : (fun x ↦ unnormEntropy (α (T + 1)) x + (∑ i ∈ Ico 1 (T + 1), g i) x) = + FObj (fun t x ↦ unnormEntropy (α t) x) g (T + 1) := by + ext x + dsimp [FObj] + rw [_root_.sum_apply] + rwa [h_eq] at this + +/-- Per-round first-order optimality deficit is non-negative for the concrete `expWeights` +trajectory. -/ +theorem expWeights_optimality_nonneg (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (t : ℕ) (hα_pos : 0 < α t) : + 0 ≤ optimality (fun t x ↦ unnormEntropyFDeriv (α t) x) (expWeights hd α g) g t := by + have hw_pos : ∀ i, 0 < expWeights hd α g t i := expWeights_pos hd α g t + have h_diff := hasFDerivAt_unnormEntropy (α t) (expWeights hd α g t) hw_pos + have h_conv := convexOn_unnormEntropy_stdSimplex (d := d) (α t) hα_pos.le + have hwt := expWeights_mem_stdSimplex hd α g t + have hwt1 := expWeights_mem_stdSimplex hd α g (t + 1) + have h_min := expWeights_isMinOn hd α g t hα_pos + exact optimality_nonneg_of_isMinOn (ψ := fun t x ↦ unnormEntropy (α t) x) + t h_diff h_conv hwt hwt1 h_min + +/-- Cumulative first-order optimality deficit is non-negative for the concrete `expWeights` +trajectory. -/ +theorem expWeights_sum_optimality_nonneg (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 1), 0 < α t) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), + optimality (fun t x ↦ unnormEntropyFDeriv (α t) x) (expWeights hd α g) g t := + sum_nonneg fun t ht ↦ expWeights_optimality_nonneg hd α g t (hα_pos t ht) + +/-- Terminal optimality deficit is non-positive for the concrete `expWeights` trajectory +at any comparator $u \in \Delta^{d-1}$. -/ +theorem expWeights_terminalOptimality_nonpos (hd : 0 < d) (α : ℕ → ℝ) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) (T : ℕ) (hα_pos : 0 < α (T + 1)) + {u : EuclideanSpace ℝ (Fin d)} (hu : u ∈ stdSimplex (d := d)) : + terminalOptimality (fun t x ↦ unnormEntropy (α t) x) u + (expWeights hd α g) g T ≤ 0 := by + have h_min := expWeights_terminal_isMinOn hd α g T hα_pos + exact terminalOptimality_nonpos_of_isMinOn (ψ := fun t x ↦ unnormEntropy (α t) x) + T hu h_min + +end Online.OCO.LEA.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Optimality.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Optimality.lean new file mode 100644 index 00000000..f73f824a --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/Optimality.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.RegretDecomposition +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# Optimality Bounds for Follow-the-Regularized-Leader (FTRL) + +This file handles the optimality terms in the FTRL regret decomposition: +1. **Per-round first-order optimality**: + $$\mathrm{optimality}_t = \left(g\psi_t(w_t) + \sum_{i=1}^{t-1} g_i\right)(w_{t+1} - w_t) \ge 0$$ + whenever $w_t$ minimizes $F_t(y) = \psi_t(y) + \sum_{i=1}^{t-1} g_i(y)$ over convex domain $s$, + and $w_{t+1} \in s$. +2. **Terminal optimality**: + $$\mathrm{terminalOptimality}_T = F_{T+1}(w_{T+1}) - F_{T+1}(u) \le 0$$ + whenever $w_{T+1}$ minimizes $F_{T+1}$ over $s$, and comparator $u \in s$. + +Because $\mathrm{optimality}_t$ enters with a minus sign and $\mathrm{terminalOptimality}_T$ +enters with a plus sign in `regret_decomposition_eq`: +$$- \sum_{t=1}^T \mathrm{optimality}_t \le 0$$ +and +$$\mathrm{terminalOptimality}_T \le 0,$$ +these bounds establish that both terms can be upper-bounded by $0$ in the regret bound. + +## Main results +* `optimality_nonneg_of_isMinOn`: $0 \le \mathrm{optimality}_t$. +* `terminalOptimality_nonpos_of_isMinOn`: $\mathrm{terminalOptimality}_T \le 0$. +-/ + +open scoped BigOperators Bregman Topology +open Filter Finset + +@[expose] public section + +namespace Online.OCO.LEA.FTRL + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Optimality + +variable {ψ : ℕ → E → ℝ} +variable {gψ : ℕ → E → (E →L[ℝ] ℝ)} +variable {u : E} +variable {w : ℕ → E} +variable {g : ℕ → (E →L[ℝ] ℝ)} +variable {s : Set E} + +/-- Per-round first-order optimality deficit is non-negative when $w_t$ minimizes +the cumulative objective $F_t$ over $s$, $\psi_t$ is convex with Fréchet derivative +$g\psi_t(w_t)$, and $w_{t+1} \in s$. -/ +lemma optimality_nonneg_of_isMinOn (t : ℕ) + (hψ_diff : HasFDerivAt (ψ t) (gψ t (w t)) (w t)) + (hψ_conv : ConvexOn ℝ s (ψ t)) + (hwt : w t ∈ s) + (hwt1 : w (t + 1) ∈ s) + (h_min : IsMinOn (FObj ψ g t) s (w t)) : + 0 ≤ optimality gψ w g t := by + let lin : E →L[ℝ] ℝ := ∑ i ∈ Ico 1 t, g i + have h_conv : ConvexOn ℝ s (ψ t + ⇑lin) := + hψ_conv.add (lin.toLinearMap.convexOn hψ_conv.1) + have h_min' : IsMinOn ((ψ t + ⇑lin) + fun _ : E ↦ (0 : ℝ)) s (w t) := by + intro x hx + simpa [FObj, lin, add_zero] using h_min hx + have h_subg := ((hψ_diff.add lin.hasFDerivAt).hasSubgradientWithinAt_add_iff + (g := 0) h_conv (convexOn_const 0 h_conv.1) hwt).mp + (hasSubgradientWithinAt_zero_iff_isMinOn.mpr h_min') (w (t + 1)) hwt1 + dsimp [bregDiv, optimality, lin] at h_subg ⊢ + simpa using h_subg + +/-- Cumulative first-order optimality deficit is non-negative when each $w_t$ minimizes +the cumulative objective $F_t$ over $s$. -/ +lemma sum_optimality_nonneg_of_isMinOn (T : ℕ) + (hψ_diff : ∀ t ∈ Ico 1 (T + 1), HasFDerivAt (ψ t) (gψ t (w t)) (w t)) + (hψ_conv : ∀ t ∈ Ico 1 (T + 1), ConvexOn ℝ s (ψ t)) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 1), IsMinOn (FObj ψ g t) s (w t)) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), optimality gψ w g t := by + refine sum_nonneg fun t ht ↦ ?_ + have ht1 : t ∈ Ico 1 (T + 2) := Ico_subset_Ico_right (by omega) ht + have ht2 : t + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico] at ht ⊢; omega + exact optimality_nonneg_of_isMinOn t (hψ_diff t ht) (hψ_conv t ht) + (hw_mem t ht1) (hw_mem (t + 1) ht2) (hw_min t ht) + +/-- Terminal optimality deficit is non-positive when $w_{T+1}$ minimizes +the terminal cumulative objective $F_{T+1}$ over $s$ and $u \in s$. -/ +lemma terminalOptimality_nonpos_of_isMinOn (T : ℕ) + (hu : u ∈ s) + (h_min : IsMinOn (FObj ψ g (T + 1)) s (w (T + 1))) : + terminalOptimality ψ u w g T ≤ 0 := by + dsimp [terminalOptimality] + have h_le : FObj ψ g (T + 1) (w (T + 1)) ≤ FObj ψ g (T + 1) u := h_min hu + linarith + +end Optimality + +end Online.OCO.LEA.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretBound.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretBound.lean new file mode 100644 index 00000000..3572a8e6 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretBound.lean @@ -0,0 +1,84 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Formula +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.Stability +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic +import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.FTRL.Boundary + +/-! +# Regret Bound for Follow-the-Regularized-Leader (FTRL) in LEA + +This file proves the multi-round regret bound for Learning with Expert Advice (LEA) using +Follow-the-Regularized-Leader (FTRL) with time-varying unnormalized negative entropy regularization +and non-negative loss subgradients $g_t \ge 0$. + +## Main results + +* `regret_bound`: The cumulative regret bound for the FTRL Exponential + Weights trajectory `expWeights hd α g`. +-/ + +open scoped BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.FTRL + +variable {d : ℕ} + +/-- Cumulative regret upper bound for FTRL Exponential Weights with non-negative losses +$g_t \ge 0$, where the stability term is bounded directly with $w_t$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u)) \le \alpha_1 \ln d + (\psi_{\alpha(T+1)}(u) - \psi_{\alpha 1}(u)) + + \sum_{t=1}^T \frac{1}{2\alpha_t} \sum_{i=1}^d w_{t, i} (g_t)_i^2.$$ -/ +theorem regret_bound (α : ℕ → ℝ) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 2), 0 < α t) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (hd : 0 < d) + (g : ℕ → (EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ)) + (w : ℕ → EuclideanSpace ℝ (Fin d)) + (hw_def : w = expWeights hd α g) + (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ stdSimplex (d := d)) + (l : ℕ → EuclideanSpace ℝ (Fin d) → ℝ) + (hg : ∀ t ∈ Ico 1 (T + 1), + HasSubgradientWithinAt (l t) (g t) (stdSimplex (d := d)) (w t)) + (hg_nonneg : ∀ t ∈ Ico 1 (T + 1), + ∀ i, 0 ≤ g t (EuclideanSpace.basisFun (Fin d) ℝ i)) : + ∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u) ≤ + α 1 * Real.log d + (unnormEntropyShifted (α (T + 1)) u - unnormEntropyShifted (α 1) u) + + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * + ∑ i, (w t i) * (g t (EuclideanSpace.basisFun (Fin d) ℝ i)) ^ 2 := by + subst hw_def + have hw1 : expWeights hd α g 1 = uniformSimplex d := expWeights_one hd α g + have hw : ∀ t ∈ Ico 1 (T + 2), expWeights hd α g t ∈ stdSimplex (d := d) := fun t _ ↦ + expWeights_mem_stdSimplex hd α g t + have hw_pos : ∀ t ∈ Ico 1 (T + 2), ∀ i, 0 < expWeights hd α g t i := fun t _ i ↦ + expWeights_pos hd α g t i + have h_term_opt : + terminalOptimality (fun s ↦ unnormEntropy (α s)) u (expWeights hd α g) g T ≤ 0 := + expWeights_terminalOptimality_nonpos hd α g T (hα_pos (T + 1) (by simp)) hu + have h_decomp := regret_decomposition_eq (fun s ↦ unnormEntropyShifted (α s)) + (fun s ↦ unnormEntropyFDeriv (α s)) u (expWeights hd α g) g l T + have h_bound := boundary_shifted_le_log_card α (hα_pos 1 (by simp)).le T hd u hu + (expWeights hd α g) hw1 + have h_opt_sum := expWeights_sum_optimality_nonneg hd α g T + (fun t ht ↦ hα_pos t (by rw [mem_Ico] at ht ⊢; omega)) + have h_lin_sum : ∑ t ∈ Ico 1 (T + 1), linearization u (expWeights hd α g) g l t ≤ 0 := + sum_nonpos fun t ht ↦ by dsimp [linearization]; linarith [hg t ht u hu] + have h_stab := sum_stability_le_dual_norm_wt (w := expWeights hd α g) (g := g) α T + (fun t ht ↦ hα_pos t (by rw [mem_Ico] at ht ⊢; omega)) hw_pos hg_nonneg + have h_shift_le := sum_shift_unnormEntropyShifted_nonpos hd α (expWeights hd α g) T h_mono hw + have h_term_shift : + terminalOptimality (fun s ↦ unnormEntropyShifted (α s)) u (expWeights hd α g) g T = + terminalOptimality (fun s ↦ unnormEntropy (α s)) u (expWeights hd α g) g T := by + dsimp [terminalOptimality, FObj, unnormEntropyShifted]; ring + rw [h_term_shift] at h_decomp + linarith + +end Online.OCO.LEA.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretDecomposition.lean new file mode 100644 index 00000000..3a9822ef --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/LEA/FTRL/RegretDecomposition.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.LEA.Common.RegretTerms + +/-! +# Static Regret Decomposition for Follow-the-Regularized-Leader (FTRL) + +This file defines the exact multi-round algebraic regret decomposition for +Follow-the-Regularized-Leader (FTRL) in the Learning with Expert Advice (LEA) setting, +where the predictor optimizes the cumulative linearized objective +$$F_t(y) = \psi_t(y) + \sum_{i=1}^{t-1} g_i(y).$$ + +## Main definitions +* `FObj` +* `boundary` +* `linearization` +* `optimality` +* `terminalOptimality` + +## Main results +* `regret_decomposition_eq`: The algebraic multi-round regret equality for FTRL. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace Online.OCO.LEA.FTRL + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Terms + +variable (ψ : ℕ → E → ℝ) +variable (gψ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u : E) +variable (w : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- +The cumulative linearized objective function $F_t(y) = \psi_t(y) + \sum_{i=1}^{t-1} g_i(y)$. +-/ +def FObj (t : ℕ) (y : E) : ℝ := + ψ t y + ∑ i ∈ Ico 1 t, g i y + +/-- Boundary regularizer term: $\psi_{T+1}(u) - \psi_1(w_1)$. -/ +def boundary (T : ℕ) : ℝ := + ψ (T + 1) u - ψ 1 (w 1) + +/-- Error incurred by linearizing the loss with subgradient `g_t` at $w_t$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u, w t, g t) + +/-- First-order optimality deficit of iterate $w_t$ under the cumulative objective $F_t$. -/ +def optimality (t : ℕ) : ℝ := + (gψ t (w t) + ∑ i ∈ Ico 1 t, g i) (w (t + 1) - w t) + +/-- Terminal optimality deficit of $w_{T+1}$ under full objective $F_{T+1}$ relative to $u$. -/ +def terminalOptimality (T : ℕ) : ℝ := + FObj ψ g (T + 1) (w (T + 1)) - FObj ψ g (T + 1) u + +/-- Exact multi-round algebraic regret decomposition for FTRL with cumulative linearized losses. -/ +theorem regret_decomposition_eq (T : ℕ) : + (∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u)) = + boundary ψ u w T + + (∑ t ∈ Ico 1 (T + 1), LEA.shift ψ w t) + + (∑ t ∈ Ico 1 (T + 1), LEA.stability ψ gψ w g t) + + (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) + - (∑ t ∈ Ico 1 (T + 1), optimality gψ w g t) + + terminalOptimality ψ u w g T := by + induction T with + | zero => + simp [boundary, terminalOptimality, FObj] + | succ T ih => + simp_rw [sum_Ico_succ_top (by omega : 1 ≤ T + 1), ih] + dsimp [boundary, terminalOptimality, LEA.shift, LEA.stability, linearization, optimality, + bregDiv, FObj] + simp only [map_sub, add_apply, _root_.sum_apply] + simp_rw [sum_sub_distrib, sum_Ico_succ_top (by omega : 1 ≤ T + 1)] + ring + +end Terms + +end Online.OCO.LEA.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Boundary.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Boundary.lean new file mode 100644 index 00000000..1b63c580 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Boundary.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer + +/-! +# Boundary Term Bound for Euclidean OMD / Projected OGD + +This file bounds the dynamic boundary term: +$$\mathrm{boundary}(\psi_\alpha, \nabla\psi_\alpha, u, w, T) = + D_{\psi_1}(u_0, w_1) - D_{\psi_{T+1}}(u_T, w_{T+1}) + \psi_{T+1}(u_T) - \psi_1(u_0)$$ +for $\psi_t(w) = \frac{\alpha_t}{2} \|w\|^2$. + +When initialized at $w_1 = 0$ and $\alpha_{T+1} \ge 0$: +$$\mathrm{boundary}(\psi_\alpha, \nabla\psi_\alpha, u, w, T) \le \frac{\alpha_{T+1}}{2} \|u_T\|^2.$$ + +## Main results +* `boundary_eucSq_le`: Upper bound on the boundary term for dynamic comparators. +-/ + +open scoped RealInnerProductSpace BigOperators + +@[expose] public section + +namespace Online.OCO.OGD.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Boundary term bound for Euclidean quadratic regularizer in OMD / Projected OGD: +$$\mathrm{boundary}(\psi_\alpha, \nabla\psi_\alpha, u, w, T) \le \frac{\alpha_{T+1}}{2} \|u_T\|^2$$ +when $w_1 = 0$ and $\alpha_{T+1} \ge 0$. -/ +theorem boundary_eucSq_le (α : ℕ → ℝ) (T : ℕ) (hα : 0 ≤ α (T + 1)) + (u : ℕ → E) (w : ℕ → E) (hw1 : w 1 = 0) : + boundary (fun s ↦ eucSq (α s)) (fun s ↦ eucSqFDeriv (α s)) u w T ≤ + (α (T + 1) / 2) * ‖u T‖^2 := by + dsimp [boundary, eucSq] + rw [bregDiv_eucSq_eq, bregDiv_eucSq_eq, hw1, sub_zero] + have h_div_nonneg : 0 ≤ (α (T + 1) / 2) * ‖u T - w (T + 1)‖^2 := by + have : 0 ≤ α (T + 1) / 2 := by linarith + positivity + linarith + +end Online.OCO.OGD.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Optimality.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Optimality.lean new file mode 100644 index 00000000..843e60f8 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Optimality.lean @@ -0,0 +1,94 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.RegretDecomposition +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# Optimality Bounds for Euclidean OMD / Projected OGD + +This file proves that the first-order optimality deficit: +$$\mathrm{optimality}_t = (g_t + \nabla\psi_{t+1}(w_{t+1}) - \nabla\psi_t(w_t))(u - w_{t+1})$$ +is **non-negative** ($0 \le \mathrm{optimality}_t$) whenever $w_{t+1}$ minimizes the +linearized mirror descent step: +$$x \mapsto (g_t)(x) + \psi_{t+1}(x) - (\nabla\psi_t(w_t))(x)$$ +over an arbitrary convex set $s \subseteq E$, $\psi_{t+1}$ is convex and differentiable at +$w_{t+1}$, and comparator $u \in s$. + +Because this term appears with a minus sign in `regret_decomposition_eq`: +$$- \sum_t \mathrm{optimality}_t \le 0,$$ +non-negativity directly establishes that the optimality term can be discarded or upper-bounded +by $0$. + +## Main results +* `optimality_nonneg_of_isMinOn`: $0 \le \mathrm{optimality}_t$. +-/ + +open scoped BigOperators Bregman Topology +open Filter Finset + +@[expose] public section + +namespace Online.OCO.OGD.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Optimality + +variable {ψ : ℕ → E → ℝ} +variable {gψ : ℕ → E → (E →L[ℝ] ℝ)} +variable {u : ℕ → E} +variable {w : ℕ → E} +variable {g : ℕ → (E →L[ℝ] ℝ)} +variable {s : Set E} + +/-- First-order optimality deficit is non-negative when $w_{t+1}$ minimizes the mirror +descent step objective over $s$, $\psi_{t+1}$ is convex with Fréchet derivative +$g\psi_{t+1}(w_{t+1})$, and $u_t \in s$. -/ +lemma optimality_nonneg_of_isMinOn (t : ℕ) + (hψ_diff : HasFDerivAt (ψ (t + 1)) (gψ (t + 1) (w (t + 1))) (w (t + 1))) + (hψ_conv : ConvexOn ℝ s (ψ (t + 1))) + (hw : w (t + 1) ∈ s) + (hu : u t ∈ s) + (h_min : IsMinOn (fun x ↦ (g t) x + ψ (t + 1) x - (gψ t (w t)) x) s (w (t + 1))) : + 0 ≤ optimality gψ u w g t := by + let lin : E →L[ℝ] ℝ := g t - gψ t (w t) + have h_conv : ConvexOn ℝ s (ψ (t + 1) + ⇑lin) := + hψ_conv.add (lin.toLinearMap.convexOn hψ_conv.1) + have h_min' : IsMinOn ((ψ (t + 1) + ⇑lin) + fun _ : E ↦ (0 : ℝ)) s (w (t + 1)) := by + intro x hx + have := h_min hx + dsimp [lin] at this ⊢ + simp only [add_zero, sub_apply] at this ⊢ + linarith + have h_subg := ((hψ_diff.add lin.hasFDerivAt).hasSubgradientWithinAt_add_iff + (g := 0) h_conv (convexOn_const 0 h_conv.1) hw).mp + (hasSubgradientWithinAt_zero_iff_isMinOn.mpr h_min') (u t) hu + dsimp [bregDiv, optimality, lin] at h_subg ⊢ + simp only [sub_self, zero_sub, neg_apply, neg_neg, add_apply, sub_apply] at h_subg ⊢ + linarith + +/-- Cumulative first-order optimality deficit is non-negative when each $w_{t+1}$ minimizes +the mirror descent step objective over $s$. -/ +lemma sum_optimality_nonneg_of_isMinOn (T : ℕ) + (hψ_diff : ∀ t ∈ Ico 1 (T + 1), HasFDerivAt (ψ (t + 1)) (gψ (t + 1) (w (t + 1))) (w (t + 1))) + (hψ_conv : ∀ t ∈ Ico 1 (T + 1), ConvexOn ℝ s (ψ (t + 1))) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hu : ∀ t ∈ Ico 1 (T + 1), u t ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 1), + IsMinOn (fun x ↦ (g t) x + ψ (t + 1) x - (gψ t (w t)) x) s (w (t + 1))) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), optimality gψ u w g t := by + refine sum_nonneg fun t ht ↦ ?_ + have ht2 : t + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico] at ht ⊢; omega + exact optimality_nonneg_of_isMinOn t (hψ_diff t ht) (hψ_conv t ht) (hw_mem (t + 1) ht2) (hu t ht) + (hw_min t ht) + +end Optimality + +end Online.OCO.OGD.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Pathlength.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Pathlength.lean new file mode 100644 index 00000000..88f7c6c4 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/Pathlength.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer + +/-! +# Pathlength Term Bound for OMD Dynamic Regret + +This file bounds the dynamic comparator pathlength term: +$$\mathrm{pathlength}_t = (g\psi_t(w_t))(u_{t-1} - u_t)$$ +for Euclidean quadratic regularizers $\psi_t(w) = \frac{\alpha_t}{2} \|w\|^2$, where +$\nabla\psi_t(w_t) = \alpha_t \langle w_t, \cdot \rangle$. + +By Cauchy-Schwarz: +$$\mathrm{pathlength}_t \le \alpha_t \|w_t\| \|u_{t-1} - u_t\|.$$ + +## Main results +* `pathlength_eucSq_le`: Upper bound on one-round pathlength via Cauchy-Schwarz. +* `sum_pathlength_eucSq_le`: Cumulative pathlength bound over rounds $t \in [1, T]$. +-/ + +open scoped RealInnerProductSpace BigOperators +open Finset + +set_option linter.style.longLine false + +@[expose] public section + +namespace Online.OCO.OGD.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- One-round pathlength upper bound for Euclidean quadratic regularizer via Cauchy-Schwarz: +$$\mathrm{pathlength}_t \le \alpha_t \|w_t\| \|u_{t-1} - u_t\|.$$ -/ +theorem pathlength_eucSq_le (α : ℕ → ℝ) (t : ℕ) (hα_nonneg : 0 ≤ α t) + (u : ℕ → E) (w : ℕ → E) : + pathlength (fun s ↦ eucSqFDeriv (α s)) u w t ≤ + α t * ‖w t‖ * ‖u (t - 1) - u t‖ := by + dsimp [pathlength] + rw [eucSqFDeriv_apply] + nlinarith [real_inner_le_norm (w t) (u (t - 1) - u t)] + +/-- Cumulative pathlength upper bound for Euclidean quadratic regularizer with bounded iterates $\|w_t\| \le R$: +$$\sum_{t=1}^T \mathrm{pathlength}_t \le R \sum_{t=1}^T \alpha_t \|u_{t-1} - u_t\|.$$ -/ +theorem sum_pathlength_eucSq_le (α : ℕ → ℝ) (T : ℕ) + (hα_nonneg : ∀ t ∈ Ico 1 (T + 1), 0 ≤ α t) + (u : ℕ → E) (w : ℕ → E) (R : ℝ) (hw_norm : ∀ t ∈ Ico 1 (T + 1), ‖w t‖ ≤ R) : + ∑ t ∈ Ico 1 (T + 1), pathlength (fun s ↦ eucSqFDeriv (α s)) u w t ≤ + R * ∑ t ∈ Ico 1 (T + 1), α t * ‖u (t - 1) - u t‖ := by + rw [mul_sum] + refine sum_le_sum fun t ht ↦ ?_ + have h1 := pathlength_eucSq_le α t (hα_nonneg t ht) u w + have h2 : α t * ‖w t‖ * ‖u (t - 1) - u t‖ ≤ R * (α t * ‖u (t - 1) - u t‖) := by + have := mul_le_mul_of_nonneg_right (hw_norm t ht) + (mul_nonneg (hα_nonneg t ht) (norm_nonneg (u (t - 1) - u t))) + linarith + exact h1.trans h2 + +end Online.OCO.OGD.COMD2 + diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretBound.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretBound.lean new file mode 100644 index 00000000..9e2e7257 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretBound.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Stability +import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Boundary +import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Optimality +import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.COMD2.Pathlength + +/-! +# Regret Bound for Online Mirror Descent (OMD / Projected OGD) + +This file proves the multi-round cumulative dynamic regret bound for Online Mirror Descent +(OMD / Projected OGD) on an arbitrary convex set $s \subseteq E$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u_t)) \le + \frac{\alpha_{T+1}}{2} \|u_T\|^2 + R_w \sum_{t=1}^T \alpha_t \|u_{t-1} - u_t\| + + \sum_{t=1}^T \frac{1}{2\alpha_t} \|g_t\|^2.$$ + +## Main results +* `regret_bound`: The cumulative dynamic regret bound for OMD on an arbitrary convex set $s$. +-/ + +open scoped RealInnerProductSpace BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.OGD.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Cumulative dynamic regret upper bound for Euclidean OMD / Projected OGD on convex set $s$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u_t)) \le + \frac{\alpha_{T+1}}{2} \|u_T\|^2 + R_w \sum_{t=1}^T \alpha_t \|u_{t-1} - u_t\| + + \sum_{t=1}^T \frac{1}{2\alpha_t} \|g_t\|^2.$$ -/ +theorem regret_bound (T : ℕ) + (α : ℕ → ℝ) (hα_pos : ∀ t ∈ Ico 1 (T + 2), 0 < α t) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (s : Set E) (hs : Convex ℝ s) + (l : ℕ → E → ℝ) + (g : ℕ → (E →L[ℝ] ℝ)) + (w : ℕ → E) (hw1 : w 1 = 0) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 1), + IsMinOn (fun x ↦ (g t) x + (α (t + 1) / 2) * ‖x‖ ^ 2 - α t * ⟪w t, x⟫) s (w (t + 1))) + (hg : ∀ t ∈ Ico 1 (T + 1), HasSubgradientWithinAt (l t) (g t) s (w t)) + (u : ℕ → E) (hu : ∀ t ∈ Ico 1 (T + 1), u t ∈ s) + (R_w : ℝ) (hw_norm : ∀ t ∈ Ico 1 (T + 1), ‖w t‖ ≤ R_w) : + ∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t (u t)) ≤ + (α (T + 1) / 2) * ‖u T‖^2 + + R_w * (∑ t ∈ Ico 1 (T + 1), α t * ‖u (t - 1) - u t‖) + + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * ‖g t‖^2 := by + have hT1 : T + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico]; omega + have h_bound := boundary_eucSq_le α T (hα_pos (T + 1) hT1).le u w hw1 + have h_shift := OGD.sum_shift_eucSq_nonpos α w T h_mono + have h_stab := OGD.sum_stability_le_norm_sq α T + (fun t ht ↦ hα_pos t (Ico_subset_Ico_right (by omega) ht)) w g + have h_path := sum_pathlength_eucSq_le α T + (fun t ht ↦ (hα_pos t (Ico_subset_Ico_right (by omega) ht)).le) u w R_w hw_norm + have h_lin : ∑ t ∈ Ico 1 (T + 1), linearization u w g l t ≤ 0 := + sum_nonpos fun t ht ↦ by dsimp [linearization]; linarith [hg t ht (u t) (hu t ht)] + have h_opt := sum_optimality_nonneg_of_isMinOn + (ψ := fun k ↦ eucSq (α k)) (gψ := fun k ↦ eucSqFDeriv (α k)) T + (fun t _ ↦ hasFDerivAt_eucSq (α (t + 1)) (w (t + 1))) + (fun t ht ↦ convexOn_eucSq (α (t + 1)) + (hα_pos (t + 1) (by rw [mem_Ico] at ht ⊢; omega)).le s hs) + hw_mem hu hw_min + linarith [regret_decomposition_eq (fun k ↦ eucSq (E := E) (α k)) + (fun k ↦ eucSqFDeriv (α k)) u w g l T] + +end Online.OCO.OGD.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretDecomposition.lean new file mode 100644 index 00000000..7b4842f0 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/COMD2/RegretDecomposition.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.RegretTerms + +/-! +# Dynamic Regret Decomposition for Online Mirror Descent (OMD / Projected OGD) + +This file defines the exact multi-round algebraic dynamic regret decomposition for +Online Mirror Descent (OMD) / Projected OGD on a real normed space $E$ +with time-varying regularizers $\psi_t$. + +## Main definitions +* `boundary` +* `pathlength` +* `linearization` +* `optimality` + +## Main results +* `regret_decomposition_eq`: The dynamic algebraic multi-round regret equality for OMD. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace Online.OCO.OGD.COMD2 + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Terms + +variable (ψ : ℕ → E → ℝ) +variable (gψ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u : ℕ → E) +variable (w : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- Boundary term comprising initial and final Bregman divergences and regularizer drift at $u$. -/ +def boundary (T : ℕ) : ℝ := + D_[ψ 1](u 0, w 1, gψ 1 (w 1)) + - D_[ψ (T + 1)](u T, w (T + 1), gψ (T + 1) (w (T + 1))) + + ψ (T + 1) (u T) - ψ 1 (u 0) + +/-- Linear coupling penalty measuring the variation in the comparator sequence $u_t$: +$$(g\psi_t(w_t))(u_{t-1} - u_t).$$ -/ +def pathlength (t : ℕ) : ℝ := + (gψ t (w t)) (u (t - 1) - u t) + +/-- Error incurred by linearizing the loss with subgradient `g_t` at $w_t$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u t, w t, g t) + +/-- First-order optimality deficit of the update step: +$$(g_t + \nabla\psi_{t+1}(w_{t+1}) - \nabla\psi_t(w_t))(u_t - w_{t+1}).$$ -/ +def optimality (t : ℕ) : ℝ := + (g t + gψ (t + 1) (w (t + 1)) - gψ t (w t)) (u t - w (t + 1)) + +/-- Exact multi-round algebraic dynamic regret decomposition for OMD / Projected OGD. -/ +theorem regret_decomposition_eq (T : ℕ) : + (∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t (u t))) = + boundary ψ gψ u w T + + (∑ t ∈ Ico 1 (T + 1), pathlength gψ u w t) + + (∑ t ∈ Ico 1 (T + 1), OGD.stability ψ gψ w g t) + + (∑ t ∈ Ico 1 (T + 1), OGD.shift ψ w t) + - (∑ t ∈ Ico 1 (T + 1), optimality gψ u w g t) + + (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) := by + induction T with + | zero => + simp [boundary] + | succ T ih => + simp_rw [Finset.sum_Ico_succ_top (by omega : 1 ≤ T + 1), ih] + dsimp [boundary, pathlength, optimality, OGD.shift, OGD.stability, linearization, bregDiv] + simp only [map_sub, add_apply, sub_apply] + ring + +end Terms + +end Online.OCO.OGD.COMD2 diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/RegretTerms.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/RegretTerms.lean new file mode 100644 index 00000000..82afaf06 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/RegretTerms.lean @@ -0,0 +1,42 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.Normed.Module.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic + +/-! +# Common Regret Terms for Online Gradient Descent (OGD / OMD / FTRL) + +This file collects the per-round regret terms shared across the OGD algorithms: +the stability tradeoff and the regularizer potential shift. + +## Main definitions + +* `stability`: One-round stability tradeoff between loss reduction and divergence. +* `shift`: Regularizer potential shift across rounds. +-/ + +open scoped Bregman + +@[expose] public section + +namespace Online.OCO.OGD + +variable {E : Type*} + +/-- Stability tradeoff between loss reduction and regularizer distance: +$$(g_t)(w_t - w_{t+1}) - D_{\psi_t}(w_{t+1}, w_t, \nabla\psi_t(w_t)).$$ -/ +def stability [NormedAddCommGroup E] [NormedSpace ℝ E] + (ψ : ℕ → E → ℝ) (gψ : ℕ → E → (E →L[ℝ] ℝ)) (w : ℕ → E) (g : ℕ → (E →L[ℝ] ℝ)) (t : ℕ) : ℝ := + (g t) (w t - w (t + 1)) - D_[ψ t](w (t + 1), w t, gψ t (w t)) + +/-- Potential shift accounting for changes in regularizers across rounds: +$$- (\psi_{t+1} - \psi_t)(w_{t+1}).$$ -/ +def shift (ψ : ℕ → E → ℝ) (w : ℕ → E) (t : ℕ) : ℝ := + - (ψ (t + 1) - ψ t) (w (t + 1)) + +end Online.OCO.OGD diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Regularizer.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Regularizer.lean new file mode 100644 index 00000000..44e5fee9 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Regularizer.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.LinearMap +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import Mathlib.Analysis.InnerProductSpace.Calculus + +/-! +# Euclidean Regularizer and Divergences for Online Gradient Descent (OGD) + +This file defines the scaled Euclidean regularizer $\psi_\alpha(w) = \frac{\alpha}{2} \|w\|^2$ +on a real inner product space $E$, its Fréchet derivative +$\nabla\psi_\alpha(w) = \alpha \langle w, \cdot \rangle$, +its Bregman divergence $D_{\psi_\alpha}(x, y) = \frac{\alpha}{2} \|x - y\|^2$, and convexity. + +## Main definitions + +* `eucSq`: The scaled squared Euclidean regularizer $\psi_\alpha(w) = \frac{\alpha}{2} \|w\|^2$. +* `eucSqFDeriv`: Fréchet derivative map $\alpha \langle w, \cdot \rangle$. + +## Main results + +* `bregDiv_eucSq_eq`: $D_{\psi_\alpha}(x, y) = \frac{\alpha}{2} \|x - y\|^2$. +* `bregDiv_eucSq_nonneg`: Non-negativity of Euclidean Bregman divergence for $\alpha \ge 0$. +* `hasFDerivAt_eucSq`: Fréchet differentiability of `eucSq`. +* `differentiable_eucSq`: Differentiability of `eucSq`. +* `convexOn_eucSq`: Convexity of `eucSq` for $\alpha \ge 0$. +* `hasSubgradientWithinAt_eucSq`: Subgradient property of `eucSqFDeriv`. +-/ + +open scoped RealInnerProductSpace Bregman + +@[expose] public section + +namespace Online.OCO.OGD + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- The scaled Euclidean quadratic regularizer $\psi_\alpha(w) = \frac{\alpha}{2} \|w\|^2$. -/ +noncomputable def eucSq (α : ℝ) (w : E) : ℝ := + (α / 2) * ‖w‖^2 + +/-- Gradient of `eucSq α w` as a continuous linear functional $\alpha \cdot \mathrm{innerSL}(w)$. -/ +noncomputable def eucSqFDeriv (α : ℝ) (w : E) : E →L[ℝ] ℝ := + α • innerSL ℝ w + +@[simp] +lemma eucSqFDeriv_apply (α : ℝ) (w v : E) : eucSqFDeriv α w v = α * ⟪w, v⟫ := by + simp [eucSqFDeriv, innerSL_apply_apply] + +/-- Bregman divergence of $\psi_\alpha(w) = \frac{\alpha}{2} \|w\|^2$ +is $\frac{\alpha}{2} \|x - y\|^2$. -/ +@[simp] +theorem bregDiv_eucSq_eq (α : ℝ) (x y : E) : + D_[eucSq α](x, y, eucSqFDeriv α y) = (α / 2) * ‖x - y‖^2 := by + dsimp [bregDiv, eucSq] + rw [eucSqFDeriv_apply, norm_sub_sq_real, sq, + inner_sub_right, real_inner_self_eq_norm_mul_norm, real_inner_comm x y] + ring + +/-- Non-negativity of Euclidean Bregman divergence for $\alpha \ge 0$. -/ +lemma bregDiv_eucSq_nonneg (α : ℝ) (hα : 0 ≤ α) (x y : E) : + 0 ≤ D_[eucSq α](x, y, eucSqFDeriv α y) := by + rw [bregDiv_eucSq_eq] + positivity + +/-- Fréchet derivative of `eucSq α` at any point $w \in E$. -/ +theorem hasFDerivAt_eucSq (α : ℝ) (w : E) : + HasFDerivAt (eucSq α) (eucSqFDeriv α w) w := by + have := (hasStrictFDerivAt_norm_sq (F := E) w).hasFDerivAt.const_smul (α / 2) + convert this using 1 + · ext x; simp [eucSq, smul_eq_mul] + · ext v; simp [eucSqFDeriv]; ring + +/-- Differentiability of `eucSq α` on the entire space $E$. -/ +theorem differentiable_eucSq (α : ℝ) : Differentiable ℝ (eucSq (E := E) α) := + fun w ↦ (hasFDerivAt_eucSq α w).differentiableAt + +/-- Convexity of `eucSq α` on any convex set $s \subseteq E$ when $\alpha \ge 0$. -/ +theorem convexOn_eucSq (α : ℝ) (hα : 0 ≤ α) (s : Set E) (hs : Convex ℝ s) : + ConvexOn ℝ s (eucSq α) := by + refine ⟨hs, fun x _ y _ a b _ _ hab ↦ ?_⟩ + dsimp [eucSq] + have h_id : ⟪a • x + b • y, a • x + b • y⟫ = + a * ⟪x, x⟫ + b * ⟪y, y⟫ - a * b * ⟪x - y, x - y⟫ := by + have ha : a * a = a - a * b := by nlinarith + have hb : b * b = b - a * b := by nlinarith + rw [inner_add_left, inner_add_right, inner_add_right, + inner_sub_left, inner_sub_right, inner_sub_right] + simp only [inner_smul_left, inner_smul_right, conj_trivial, real_inner_comm y x] + linear_combination ⟪x, x⟫ * ha + ⟪y, y⟫ * hb + simp only [sq, ← real_inner_self_eq_norm_mul_norm] + rw [h_id] + have : 0 ≤ (α / 2) * (a * b * ⟪x - y, x - y⟫) := by + have : 0 ≤ ⟪x - y, x - y⟫ := real_inner_self_nonneg + positivity + linarith + +/-- Subgradient property of `eucSqFDeriv α w` on any set $s \subseteq E$ when $\alpha \ge 0$. -/ +theorem hasSubgradientWithinAt_eucSq (α : ℝ) (hα : 0 ≤ α) (s : Set E) (w : E) : + HasSubgradientWithinAt (eucSq α) (eucSqFDeriv α w) s w := by + intro y _ + rw [bregDiv_eucSq_eq] + positivity + +end Online.OCO.OGD diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Shift.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Shift.lean new file mode 100644 index 00000000..20059a08 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Shift.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer + +/-! +# Shift Term Bound for OGD Regularizers + +This file bounds the regularizer potential shift term: +$$\mathrm{shift}(t) = -(\psi_{t+1} - \psi_t)(w_{t+1})$$ +when $\psi_t = \text{eucSq}(\alpha_t)$ with non-decreasing weights $\alpha_t \le \alpha_{t+1}$. + +## Main definitions +* `shift`: Potential shift $-(\psi_{t+1} - \psi_t)(w_{t+1})$. + +## Main results +* `shift_nonpos_of_nondecreasing`: $\alpha_t \le \alpha_{t+1} \implies \mathrm{shift}(t) \le 0$. +* `sum_shift_nonpos_of_nondecreasing`: Cumulative shift is non-positive. +-/ + +open scoped BigOperators +open Finset + +@[expose] public section + +namespace Online.OCO.OGD + +variable {E : Type*} [NormedAddCommGroup E] + +/-- Shift term for `eucSq` is non-positive under non-decreasing regularization weights. -/ +theorem shift_eucSq_nonpos (α : ℕ → ℝ) (w : ℕ → E) (t : ℕ) + (h_mono : α t ≤ α (t + 1)) : + shift (fun s ↦ eucSq (α s)) w t ≤ 0 := by + dsimp [shift, eucSq] + have h_diff : 0 ≤ α (t + 1) - α t := sub_nonneg.mpr h_mono + have : 0 ≤ ((α (t + 1) - α t) / 2) * ‖w (t + 1)‖^2 := by positivity + linarith + +/-- Cumulative shift for `eucSq` is non-positive under non-decreasing regularization weights. -/ +theorem sum_shift_eucSq_nonpos (α : ℕ → ℝ) (w : ℕ → E) (T : ℕ) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) : + ∑ t ∈ Ico 1 (T + 1), shift (fun s ↦ eucSq (α s)) w t ≤ 0 := + sum_nonpos fun t ht ↦ shift_eucSq_nonpos α w t (h_mono t ht) + +end Online.OCO.OGD diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Stability.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Stability.lean new file mode 100644 index 00000000..b8e7de12 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/Common/Stability.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.RegretTerms +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer + +/-! +# Stability Bound for Online Gradient Descent (OGD / OMD / FTRL) + +This file bounds the stability term: +$$\mathrm{stability}_t = (g_t)(w_t - w_{t+1}) - D_{\psi_t}(w_{t+1}, w_t)$$ +for Euclidean quadratic regularizer $\psi_t(w) = \frac{\alpha_t}{2} \|w\|^2$. + +By Cauchy-Schwarz / Hölder's inequality on inner product spaces: +$$(g_t)(w_t - w_{t+1}) - \frac{\alpha_t}{2} \|w_{t+1} - w_t\|^2 \le \frac{1}{2\alpha_t} \|g_t\|^2.$$ + +## Main definitions +* `stability`: One-round stability tradeoff between loss reduction and regularizer divergence. + +## Main results +* `stability_le_norm_sq`: One-round stability upper bound via Cauchy-Schwarz / Hölder. +* `sum_stability_le_norm_sq`: Cumulative multi-round stability upper bound. +-/ + +open scoped RealInnerProductSpace BigOperators Bregman +open Finset + + +@[expose] public section + +namespace Online.OCO.OGD + +variable {E : Type*} [NormedAddCommGroup E] + +variable [InnerProductSpace ℝ E] + +/-- One-round stability bound for Euclidean quadratic regularization via Cauchy-Schwarz / Hölder: +$$(g_t)(w_t - w_{t+1}) - \frac{\alpha_t}{2} \|w_{t+1} - w_t\|^2 \le +\frac{1}{2\alpha_t} \|g_t\|^2.$$ -/ +theorem stability_le_norm_sq (α : ℕ → ℝ) (t : ℕ) (hα_pos : 0 < α t) + (w : ℕ → E) (g : ℕ → (E →L[ℝ] ℝ)) : + stability (fun s ↦ eucSq (α s)) (fun s ↦ eucSqFDeriv (α s)) w g t ≤ + (1 / (2 * α t)) * ‖g t‖^2 := by + dsimp [stability] + rw [bregDiv_eucSq_eq] + have h_dual : (g t) (w t - w (t + 1)) ≤ ‖g t‖ * ‖w (t + 1) - w t‖ := by + rw [norm_sub_rev (w (t + 1))] + exact le_trans (le_abs_self _) ((g t).le_opNorm _) + have h_scale : + (2 * α t) * ((g t) (w t - w (t + 1)) - (α t / 2) * ‖w (t + 1) - w t‖^2) ≤ ‖g t‖^2 := by + have h_sq : 0 ≤ (α t * ‖w (t + 1) - w t‖ - ‖g t‖)^2 := sq_nonneg _ + have h_expand : + 2 * α t * (‖g t‖ * ‖w (t + 1) - w t‖) - 2 * α t * ((α t / 2) * ‖w (t + 1) - w t‖^2) = + ‖g t‖^2 - (α t * ‖w (t + 1) - w t‖ - ‖g t‖)^2 := by ring + nlinarith + have h_div := mul_le_mul_of_nonneg_left h_scale (show 0 ≤ 1 / (2 * α t) by positivity) + have h_cancel : + (1 / (2 * α t)) * ((2 * α t) * ((g t) (w t - w (t + 1)) - (α t / 2) * ‖w (t + 1) - w t‖^2)) = + (g t) (w t - w (t + 1)) - (α t / 2) * ‖w (t + 1) - w t‖^2 := by + field_simp [hα_pos.ne'] + rwa [h_cancel] at h_div + +/-- Cumulative multi-round stability bound for Euclidean quadratic regularization: +$$\sum_{t=1}^T \mathrm{stability}_t \le \sum_{t=1}^T \frac{1}{2\alpha_t} \|g_t\|^2.$$ -/ +theorem sum_stability_le_norm_sq (α : ℕ → ℝ) (T : ℕ) + (hα_pos : ∀ t ∈ Ico 1 (T + 1), 0 < α t) + (w : ℕ → E) (g : ℕ → (E →L[ℝ] ℝ)) : + (∑ t ∈ Ico 1 (T + 1), + stability (fun s ↦ eucSq (α s)) (fun s ↦ eucSqFDeriv (α s)) w g t) ≤ + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * ‖g t‖^2 := + sum_le_sum fun t ht ↦ stability_le_norm_sq α t (hα_pos t ht) w g + +end Online.OCO.OGD diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Boundary.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Boundary.lean new file mode 100644 index 00000000..e316348c --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Boundary.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer + +/-! +# Boundary Term Bound for Euclidean FTRL / Lazy OGD + +This file bounds the boundary term: +$$\mathrm{boundary}(\psi, u, w, T) = \psi_{T+1}(u) - \psi_1(w_1)$$ +for $\psi_t(w) = \frac{\alpha_t}{2} \|w\|^2$. + +When initialized at $w_1 = 0$ (or $\|w_1\| \ge 0$), and $\|u\| \le R$: +$$\mathrm{boundary}(\psi_\alpha, u, w, T) \le \frac{\alpha_{T+1}}{2} R^2.$$ + +## Main results +* `boundary_eucSq_le`: Upper bound on the boundary term. +-/ + +open scoped RealInnerProductSpace BigOperators + +@[expose] public section + +namespace Online.OCO.OGD.FTRL + +variable {E : Type*} [NormedAddCommGroup E] + +/-- Exact boundary term formula for Euclidean quadratic regularization initialized at $w_1 = 0$: +$$\mathrm{boundary}(\psi_\alpha, u, w, T) = \frac{\alpha_{T+1}}{2} \|u\|^2.$$ -/ +theorem boundary_eucSq_eq (α : ℕ → ℝ) (T : ℕ) + (u : E) (w : ℕ → E) (hw1 : w 1 = 0) : + boundary (fun s ↦ eucSq (α s)) u w T = (α (T + 1) / 2) * ‖u‖^2 := by + dsimp [boundary, eucSq] + rw [hw1, norm_zero, zero_pow two_ne_zero, mul_zero, sub_zero] + +/-- Boundary term bound for Euclidean quadratic regularization: +$$\mathrm{boundary}(\psi_\alpha, u, w, T) \le \frac{\alpha_{T+1}}{2} R^2$$ +when $\|u\| \le R$, $w_1 = 0$, and $\alpha_{T+1} \ge 0$. -/ +theorem boundary_eucSq_le (α : ℕ → ℝ) (T : ℕ) (hα : 0 ≤ α (T + 1)) (R : ℝ) + (u : E) (hu_norm : ‖u‖ ≤ R) + (w : ℕ → E) (hw1 : w 1 = 0) : + boundary (fun s ↦ eucSq (α s)) u w T ≤ (α (T + 1) / 2) * R^2 := by + rw [boundary_eucSq_eq α T u w hw1] + have h_scale : 0 ≤ α (T + 1) / 2 := by linarith + have h_sq : ‖u‖^2 ≤ R^2 := by nlinarith [norm_nonneg u] + nlinarith + +end Online.OCO.OGD.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Optimality.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Optimality.lean new file mode 100644 index 00000000..6a844e9d --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/Optimality.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.RegretDecomposition +public import Mathlib.Analysis.Calculus.FDeriv.Defs +import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv +import Mathlib.Analysis.Calculus.FDeriv.Add + +/-! +# Optimality Bounds for Euclidean FTRL / Lazy OGD + +This file proves the non-negativity of per-round optimality and non-positivity of terminal +optimality for Follow-the-Regularized-Leader (FTRL / Lazy OGD) on an arbitrary convex set +$s \subseteq E$. + +## Main results +* `optimality_nonneg_of_isMinOn`: $0 \le \mathrm{optimality}_t$. +* `terminalOptimality_nonpos_of_isMinOn`: $\mathrm{terminalOptimality}_T \le 0$. +-/ + +open scoped BigOperators Bregman Topology +open Filter Finset + +@[expose] public section + +namespace Online.OCO.OGD.FTRL + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Optimality + +variable {ψ : ℕ → E → ℝ} +variable {gψ : ℕ → E → (E →L[ℝ] ℝ)} +variable {u : E} +variable {w : ℕ → E} +variable {g : ℕ → (E →L[ℝ] ℝ)} +variable {s : Set E} + +/-- Per-round first-order optimality deficit is non-negative when $w_t$ minimizes +the cumulative objective $F_t$ over $s$, $\psi_t$ is convex with Fréchet derivative +$g\psi_t(w_t)$, and $w_{t+1} \in s$. -/ +lemma optimality_nonneg_of_isMinOn (t : ℕ) + (hψ_diff : HasFDerivAt (ψ t) (gψ t (w t)) (w t)) + (hψ_conv : ConvexOn ℝ s (ψ t)) + (hwt : w t ∈ s) + (hwt1 : w (t + 1) ∈ s) + (h_min : IsMinOn (FObj ψ g t) s (w t)) : + 0 ≤ optimality gψ w g t := by + let lin : E →L[ℝ] ℝ := ∑ i ∈ Ico 1 t, g i + have h_conv : ConvexOn ℝ s (ψ t + ⇑lin) := + hψ_conv.add (lin.toLinearMap.convexOn hψ_conv.1) + have h_min' : IsMinOn ((ψ t + ⇑lin) + fun _ : E ↦ (0 : ℝ)) s (w t) := by + intro x hx + simpa [FObj, lin, add_zero] using h_min hx + have h_subg := ((hψ_diff.add lin.hasFDerivAt).hasSubgradientWithinAt_add_iff + (g := 0) h_conv (convexOn_const 0 h_conv.1) hwt).mp + (hasSubgradientWithinAt_zero_iff_isMinOn.mpr h_min') (w (t + 1)) hwt1 + dsimp [bregDiv, optimality, lin] at h_subg ⊢ + simpa using h_subg + +/-- Cumulative first-order optimality deficit is non-negative when each $w_t$ minimizes +the cumulative objective $F_t$ over $s$. -/ +lemma sum_optimality_nonneg_of_isMinOn (T : ℕ) + (hψ_diff : ∀ t ∈ Ico 1 (T + 1), HasFDerivAt (ψ t) (gψ t (w t)) (w t)) + (hψ_conv : ∀ t ∈ Ico 1 (T + 1), ConvexOn ℝ s (ψ t)) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 1), IsMinOn (FObj ψ g t) s (w t)) : + 0 ≤ ∑ t ∈ Ico 1 (T + 1), optimality gψ w g t := by + refine sum_nonneg fun t ht ↦ ?_ + have ht1 : t ∈ Ico 1 (T + 2) := Ico_subset_Ico_right (by omega) ht + have ht2 : t + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico] at ht ⊢; omega + exact optimality_nonneg_of_isMinOn t (hψ_diff t ht) (hψ_conv t ht) + (hw_mem t ht1) (hw_mem (t + 1) ht2) (hw_min t ht) + +/-- Terminal optimality deficit is non-positive when $w_{T+1}$ minimizes +the terminal cumulative objective $F_{T+1}$ over $s$ and $u \in s$. -/ +lemma terminalOptimality_nonpos_of_isMinOn (T : ℕ) + (hu : u ∈ s) + (h_min : IsMinOn (FObj ψ g (T + 1)) s (w (T + 1))) : + terminalOptimality ψ u w g T ≤ 0 := by + dsimp [terminalOptimality] + have h_le : FObj ψ g (T + 1) (w (T + 1)) ≤ FObj ψ g (T + 1) u := h_min hu + linarith + +end Optimality + +end Online.OCO.OGD.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretBound.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretBound.lean new file mode 100644 index 00000000..8461a532 --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretBound.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.RegretDecomposition +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Regularizer +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Shift +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.Stability +import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.Boundary +import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.FTRL.Optimality + +/-! +# Regret Bound for Follow-the-Regularized-Leader (FTRL / Lazy OGD) + +This file proves the multi-round cumulative regret bound for Follow-the-Regularized-Leader +(FTRL / Lazy OGD) on an arbitrary convex set $s \subseteq E$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u)) \le + \frac{\alpha_{T+1}}{2} \|u\|^2 + \sum_{t=1}^T \frac{1}{2\alpha_t} \|g_t\|^2.$$ + +## Main results +* `regret_bound`: The cumulative regret bound for FTRL on an arbitrary convex set $s$. +-/ + +open scoped RealInnerProductSpace BigOperators Bregman Topology +open Finset + +@[expose] public section + +namespace Online.OCO.OGD.FTRL + +variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + +/-- Cumulative regret upper bound for Euclidean FTRL / Lazy OGD on a convex set $s \subseteq E$: +$$\sum_{t=1}^T (l_t(w_t) - l_t(u)) \le + \frac{\alpha_{T+1}}{2} \|u\|^2 + \sum_{t=1}^T \frac{1}{2\alpha_t} \|g_t\|^2.$$ -/ +theorem regret_bound (T : ℕ) + (α : ℕ → ℝ) (hα_pos : ∀ t ∈ Ico 1 (T + 2), 0 < α t) + (h_mono : ∀ t ∈ Ico 1 (T + 1), α t ≤ α (t + 1)) + (s : Set E) (hs : Convex ℝ s) + (l : ℕ → E → ℝ) + (g : ℕ → (E →L[ℝ] ℝ)) + (w : ℕ → E) (hw1 : w 1 = 0) + (hw_mem : ∀ t ∈ Ico 1 (T + 2), w t ∈ s) + (hw_min : ∀ t ∈ Ico 1 (T + 2), + IsMinOn (fun x ↦ (α t / 2) * ‖x‖ ^ 2 + ∑ i ∈ Ico 1 t, g i x) s (w t)) + (hg : ∀ t ∈ Ico 1 (T + 1), HasSubgradientWithinAt (l t) (g t) s (w t)) + (u : E) (hu : u ∈ s) : + ∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u) ≤ + (α (T + 1) / 2) * ‖u‖^2 + + ∑ t ∈ Ico 1 (T + 1), (1 / (2 * α t)) * ‖g t‖^2 := by + have hT1 : T + 1 ∈ Ico 1 (T + 2) := by rw [mem_Ico]; omega + have h_bound := boundary_eucSq_eq α T u w hw1 + have h_shift := OGD.sum_shift_eucSq_nonpos α w T h_mono + have h_stab := OGD.sum_stability_le_norm_sq α T + (fun t ht ↦ hα_pos t (Ico_subset_Ico_right (by omega) ht)) w g + have h_lin : ∑ t ∈ Ico 1 (T + 1), linearization u w g l t ≤ 0 := + sum_nonpos fun t ht ↦ by dsimp [linearization]; linarith [hg t ht u hu] + have h_opt := sum_optimality_nonneg_of_isMinOn (ψ := fun k ↦ eucSq (α k)) T + (fun t _ ↦ hasFDerivAt_eucSq (α t) (w t)) + (fun t ht ↦ convexOn_eucSq (α t) (hα_pos t (Ico_subset_Ico_right (by omega) ht)).le s hs) + hw_mem (fun t ht ↦ hw_min t (Ico_subset_Ico_right (by omega) ht)) + have h_term := terminalOptimality_nonpos_of_isMinOn (ψ := fun k ↦ eucSq (α k)) + T hu (hw_min (T + 1) hT1) + linarith [regret_decomposition_eq (fun k ↦ eucSq (E := E) (α k)) + (fun k ↦ eucSqFDeriv (α k)) u w g l T] + +end Online.OCO.OGD.FTRL diff --git a/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretDecomposition.lean b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretDecomposition.lean new file mode 100644 index 00000000..a3b73d7e --- /dev/null +++ b/LeanMachineLearning/Online/OnlineConvexOptimization/OGD/FTRL/RegretDecomposition.lean @@ -0,0 +1,88 @@ +/- +Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Isidoor Pinillo Esquivel +-/ +module + +public import LeanMachineLearning.Online.OnlineConvexOptimization.OGD.Common.RegretTerms + +/-! +# Static Regret Decomposition for Follow-the-Regularized-Leader (FTRL / Lazy OGD) + +This file defines the exact multi-round algebraic regret decomposition for +Follow-the-Regularized-Leader (FTRL) in the Euclidean OGD setting with cumulative objective: +$$F_t(y) = \psi_t(y) + \sum_{i=1}^{t-1} g_i(y).$$ + +## Main definitions +* `FObj` +* `boundary` +* `linearization` +* `optimality` +* `terminalOptimality` + +## Main results +* `regret_decomposition_eq`: The algebraic multi-round regret equality for FTRL. +-/ + +open scoped BigOperators Bregman +open Finset + +@[expose] public section + +namespace Online.OCO.OGD.FTRL + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] + +section Terms + +variable (ψ : ℕ → E → ℝ) +variable (gψ : ℕ → E → (E →L[ℝ] ℝ)) +variable (u : E) +variable (w : ℕ → E) +variable (g : ℕ → (E →L[ℝ] ℝ)) +variable (l : ℕ → E → ℝ) + +/-- The cumulative linearized objective function $F_t(y) = \psi_t(y) + \sum_{i=1}^{t-1} g_i(y)$. -/ +def FObj (t : ℕ) (y : E) : ℝ := + ψ t y + ∑ i ∈ Ico 1 t, g i y + +/-- Boundary regularizer term: $\psi_{T+1}(u) - \psi_1(w_1)$. -/ +def boundary (T : ℕ) : ℝ := + ψ (T + 1) u - ψ 1 (w 1) + +/-- Error incurred by linearizing the loss with subgradient `g_t` at $w_t$. -/ +def linearization (t : ℕ) : ℝ := + - D_[l t](u, w t, g t) + +/-- First-order optimality deficit of iterate $w_t$ under the cumulative objective $F_t$. -/ +def optimality (t : ℕ) : ℝ := + (gψ t (w t) + ∑ i ∈ Ico 1 t, g i) (w (t + 1) - w t) + +/-- Terminal optimality deficit of $w_{T+1}$ under full objective $F_{T+1}$ relative to $u$. -/ +def terminalOptimality (T : ℕ) : ℝ := + FObj ψ g (T + 1) (w (T + 1)) - FObj ψ g (T + 1) u + +/-- Exact multi-round algebraic regret decomposition for Euclidean FTRL / Lazy OGD. -/ +theorem regret_decomposition_eq (T : ℕ) : + (∑ t ∈ Ico 1 (T + 1), (l t (w t) - l t u)) = + boundary ψ u w T + + (∑ t ∈ Ico 1 (T + 1), OGD.shift ψ w t) + + (∑ t ∈ Ico 1 (T + 1), OGD.stability ψ gψ w g t) + + (∑ t ∈ Ico 1 (T + 1), linearization u w g l t) + - (∑ t ∈ Ico 1 (T + 1), optimality gψ w g t) + + terminalOptimality ψ u w g T := by + induction T with + | zero => + simp [boundary, terminalOptimality, FObj] + | succ T ih => + simp_rw [sum_Ico_succ_top (by omega : 1 ≤ T + 1), ih] + dsimp [boundary, terminalOptimality, OGD.shift, OGD.stability, linearization, optimality, + bregDiv, FObj] + simp only [map_sub, add_apply, _root_.sum_apply] + simp_rw [sum_sub_distrib, sum_Ico_succ_top (by omega : 1 ≤ T + 1)] + ring + +end Terms + +end Online.OCO.OGD.FTRL