diff --git a/LMLExplore/Analysis/Calculus/MeanValue.lean b/LMLExplore/Analysis/Calculus/MeanValue.lean new file mode 100644 index 00000000..3701f70c --- /dev/null +++ b/LMLExplore/Analysis/Calculus/MeanValue.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Analysis.Calculus.Deriv.MeanValue + +/-! +# Comparing values of a function through the sign of its derivative + +Mathlib's `monotoneOn_of_hasDerivWithinAt_nonneg` and `antitoneOn_of_hasDerivWithinAt_nonpos` +turn the sign of a derivative on an interval into monotonicity. This file packages the two-sided +form used to prove that a point is a maximum: if the derivative of `f` is nonnegative to the left +of `x₀` and nonpositive to its right, then `f x ≤ f x₀` for every `x`. + +## Main statements + +* `LMLExplore.apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos`: if `f` has derivative `f' y` at + each `y` between `x` and `x₀`, with `f' ≥ 0` on `(x, x₀)` and `f' ≤ 0` on `(x₀, x)`, then + `f x ≤ f x₀`. +-/ + +public section + +namespace LMLExplore + +/-- If `f` is differentiable on the segment between `x` and `x₀`, with a nonnegative derivative +between `x` and `x₀` when `x < x₀` and a nonpositive one when `x > x₀`, then `f x ≤ f x₀`. -/ +theorem apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos {f f' : ℝ → ℝ} {x x₀ : ℝ} + (hd : ∀ y ∈ Set.uIcc x x₀, HasDerivAt f (f' y) y) + (hneg : ∀ y ∈ Set.Ioo x x₀, 0 ≤ f' y) (hpos : ∀ y ∈ Set.Ioo x₀ x, f' y ≤ 0) : + f x ≤ f x₀ := by + have hcont : ContinuousOn f (Set.uIcc x x₀) := + fun y hy ↦ (hd y hy).continuousAt.continuousWithinAt + rcases le_total x x₀ with h0 | h0 + · rw [Set.uIcc_of_le h0] at hd hcont + refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc x x₀) hcont + (fun y hy ↦ (hd y (interior_subset hy)).hasDerivWithinAt) ?_ + ⟨le_rfl, h0⟩ ⟨h0, le_rfl⟩ h0 + rw [interior_Icc] + exact hneg + · rw [Set.uIcc_of_ge h0] at hd hcont + refine antitoneOn_of_hasDerivWithinAt_nonpos (convex_Icc x₀ x) hcont + (fun y hy ↦ (hd y (interior_subset hy)).hasDerivWithinAt) ?_ + ⟨le_rfl, h0⟩ ⟨h0, le_rfl⟩ h0 + rw [interior_Icc] + exact hpos + +end LMLExplore diff --git a/LMLExplore/Analysis/Real/Sqrt.lean b/LMLExplore/Analysis/Real/Sqrt.lean index 9216ddea..41d0ba71 100644 --- a/LMLExplore/Analysis/Real/Sqrt.lean +++ b/LMLExplore/Analysis/Real/Sqrt.lean @@ -11,6 +11,7 @@ public import Mathlib.Analysis.Calculus.Deriv.Inv public import Mathlib.Analysis.Calculus.Deriv.Mul public import Mathlib.Analysis.Real.Sqrt public import Mathlib.Analysis.SpecialFunctions.Sqrt +import TauCeti.Analysis.SpecialFunctions.Sqrt /-! # Square roots of quotients, increments of the square root and sums of inverse square roots @@ -38,6 +39,10 @@ public import Mathlib.Analysis.SpecialFunctions.Sqrt * `Real.le_add_sqrt_of_sq_le`: the root of a quadratic inequality, `x² ≤ b x + c` with `b, c ≥ 0` forces `x ≤ b + √c`. It solves for `√τ` inequalities of the form `τ ≤ b √τ + c`, as in the self-bounding inequality `Real.le_of_le_sqrt_mul_add`. +* `Real.le_div_two_add_add_sqrt_of_sub_sqrt_le`, `Real.le_add_add_sqrt_of_sub_sqrt_le`: an + implicit bound solved [Ora, Lemma 4.29]. For `a ≥ 0`, `x - √(a x + b) ≤ c` forces + `x ≤ a / 2 + c + √(a² / 4 + b + a c) ≤ a + c + √(b + a c)`. It turns regret bounds in which the + losses of the algorithm appear on both sides, as the `L⋆` bounds, into explicit ones. * `Real.sum_range_inv_sqrt_add_one_le`: `∑_{j < n} 1 / √(j + 1) ≤ 2 √n`. * `Real.sum_range_inv_sqrt_max_one_le`: `∑_{j < n} 1 / √(max 1 j) ≤ 2 √n + 1`, the same sum with the index clipped at `1`. @@ -48,6 +53,7 @@ public import Mathlib.Analysis.SpecialFunctions.Sqrt ## References +* [Ora] F. Orabona, *A Modern Introduction to Online Learning*, arXiv:1912.13213v10. * [JOA10] T. Jaksch, R. Ortner and P. Auer, *Near-optimal regret bounds for reinforcement learning*, Journal of Machine Learning Research 11 (2010). -/ @@ -162,6 +168,31 @@ theorem le_add_sqrt_of_sq_le {x b c : ℝ} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : x nlinarith [mul_pos (show 0 < x - √c by linarith) (show 0 < x - b - √c by linarith), mul_nonneg hs0 (show 0 ≤ 2 * x - b - 2 * √c by linarith)] +/-- **An implicit bound solved** [Ora, Lemma 4.29]: for `a ≥ 0`, `x - √(a x + b) ≤ c` forces +`x ≤ a / 2 + c + √(a² / 4 + b + a c)`. + +It makes explicit the regret bounds that contain the losses of the algorithm on both sides, as the +`L⋆` bounds for self-bounded losses. Unlike [Ora], it needs no sign condition on `x`, `b` or +`c`. -/ +theorem le_div_two_add_add_sqrt_of_sub_sqrt_le {x a b c : ℝ} (ha : 0 ≤ a) + (h : x - √(a * x + b) ≤ c) : x ≤ a / 2 + c + √(a ^ 2 / 4 + b + a * c) := by + rcases le_or_gt x c with hxc | hxc + · linarith [sqrt_nonneg (a ^ 2 / 4 + b + a * c)] + -- for `x > c`, `(x - c)² ≤ a (x - c) + (a c + b)`, so `x - c` is at most the larger root + have hsq : (x - c) ^ 2 ≤ a * x + b := (le_sqrt' (by linarith)).1 (by linarith) + have := le_sqrt_of_sq_le (show (x - c - a / 2) ^ 2 ≤ a ^ 2 / 4 + b + a * c by nlinarith) + linarith + +/-- **An implicit bound solved** [Ora, Lemma 4.29], in its simpler form: for `a ≥ 0`, +`x - √(a x + b) ≤ c` forces `x ≤ a + c + √(b + a c)`. -/ +theorem le_add_add_sqrt_of_sub_sqrt_le {x a b c : ℝ} (ha : 0 ≤ a) (h : x - √(a * x + b) ≤ c) : + x ≤ a + c + √(b + a * c) := by + have h2 : √(a ^ 2 / 4) = a / 2 := by + rw [show a ^ 2 / 4 = (a / 2) ^ 2 by ring, sqrt_sq (by positivity)] + have := sqrt_add_le_add_sqrt (a ^ 2 / 4) (b + a * c) + rw [← add_assoc] at this + linarith [le_div_two_add_add_sqrt_of_sub_sqrt_le ha h] + /-- `∑_{j < n} 1 / √(j + 1) ≤ 2 √n`. -/ theorem sum_range_inv_sqrt_add_one_le (n : ℕ) : ∑ j ∈ Finset.range n, (√((j : ℝ) + 1))⁻¹ ≤ 2 * √n := by diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean index 9222cd96..1d6fcd1d 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Log.Basic public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import LMLExplore.Analysis.Calculus.MeanValue import Mathlib.Analysis.Complex.ExponentialBounds import Mathlib.Analysis.SpecialFunctions.Log.Deriv @@ -16,6 +17,9 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv ## Main statements * `Real.min_one_le_two_mul_log_one_add`: `min 1 u ≤ 2 log (1 + u)` for `u ≥ 0`. +* `Real.sub_sq_le_log_one_add`, `Real.log_one_add_le_sub_sq_div_four`: the quadratic bounds + `x - x² ≤ log (1 + x)` for `x ≥ -1 / 2` and `log (1 + x) ≤ x - x² / 4` for `-1 < x ≤ 1`, which + linearize logarithmic losses and log-wealths in online learning [Ora, Example 7.39, §13.7]. * `Real.monotoneOn_log_one_add_mul_log_sq`: `x ↦ log (1 + x log² x)` is monotone on `[1, ∞)`. * `Real.log_natCast_le_log_natCast`: `log` is monotone on natural numbers. * `Real.one_le_log_natCast_of_three_le`: `1 ≤ log n` for a natural number `n ≥ 3`. @@ -68,6 +72,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv * [GK16] A. Garivier and E. Kaufmann, *Optimal best arm identification with fixed confidence*, COLT 2016, proof of Theorem 14. * [LS] T. Lattimore and Cs. Szepesvári, *Bandit Algorithms*, Cambridge University Press, 2020. +* [Ora] F. Orabona, *A Modern Introduction to Online Learning*, arXiv:1912.13213v10. * [MDJKLV21] P. Ménard, O. D. Domingues, A. Jonsson, E. Kaufmann, E. Leurent and M. Valko, *Fast active learning for pure exploration in reinforcement learning*, ICML 2021, Lemma 9. * [EV26] A. Essakine and C. Vernade, *Tight sample complexity bounds for entropic best policy @@ -93,6 +98,68 @@ theorem min_one_le_two_mul_log_one_add {u : ℝ} (hu : 0 ≤ u) : min 1 u ≤ 2 · nlinarith [mul_le_mul_of_nonneg_right (min_le_left 1 u) hpos.le] linarith [le_log_one_add_of_nonneg hu] +/-- The derivative of `y ↦ log (1 + y) + p y` at `y > -1`, for `p` with derivative `q` at `y`. -/ +private lemma hasDerivAt_log_one_add_add {p : ℝ → ℝ} {q y : ℝ} (hp : HasDerivAt p q y) + (hy : -1 < y) : HasDerivAt (fun z ↦ log (1 + z) + p z) ((1 + y)⁻¹ + q) y := by + have h := ((hasDerivAt_id y).const_add 1).log (by simp; linarith) + exact (h.add hp).congr_deriv (by simp [one_div]) + +/-- **A quadratic lower bound on `log (1 + x)`**: `x - x² ≤ log (1 + x)` for `x ≥ -1 / 2`. + +It bounds below the log-wealth `log (1 + β c)` of a bettor who stakes a fraction `|β| ≤ 1 / 2` +of their wealth on a coin `c ∈ [-1, 1]`, as in [Ora, §13.7], which states it for `|x| ≤ 1 / 2`. -/ +theorem sub_sq_le_log_one_add {x : ℝ} (hx : -1 / 2 ≤ x) : x - x ^ 2 ≤ log (1 + x) := by + rcases le_or_gt 0 x with h0 | h0 + · -- `x - x² ≤ 2 x / (x + 2) ≤ log (1 + x)` + refine le_trans ?_ (le_log_one_add_of_nonneg h0) + rw [le_div_iff₀ (by linarith)] + nlinarith [mul_nonneg h0 (sq_nonneg x)] + -- `y ↦ log (1 + y) - y + y²` decreases on `[-1 / 2, 0]`, its derivative `y (1 + 2 y) / (1 + y)` + -- being nonpositive there + have h := LMLExplore.apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos + (f := fun z ↦ -(log (1 + z) + (z ^ 2 - z))) + (f' := fun y ↦ -((1 + y)⁻¹ + (2 * y - 1))) (x := x) (x₀ := 0) + (fun y hy ↦ (hasDerivAt_log_one_add_add (p := fun z ↦ z ^ 2 - z) + (((hasDerivAt_pow 2 y).sub (hasDerivAt_id y)).congr_deriv (by simp)) + (by rw [Set.uIcc_of_le h0.le] at hy; linarith [hy.1])).neg) + (fun y hy ↦ by + have h1 : 0 < 1 + y := by linarith [hy.1] + rw [show -((1 + y)⁻¹ + (2 * y - 1)) = -(y * (1 + 2 * y)) / (1 + y) by field_simp; ring] + exact div_nonneg (by nlinarith [hy.1, hy.2]) h1.le) + (fun y hy ↦ absurd (hy.1.trans hy.2) h0.not_gt) + simp only [add_zero, log_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + sub_self, neg_zero, neg_add_rev, neg_sub] at h + linarith + +/-- **A quadratic upper bound on `log (1 + x)`**: `log (1 + x) ≤ x - x² / 4` for `-1 < x ≤ 1`. + +It turns exp-concavity into the quadratic lower bound on the losses that the Online Newton Step +uses [Ora, Example 7.39]. -/ +theorem log_one_add_le_sub_sq_div_four {x : ℝ} (hx₁ : -1 < x) (hx₂ : x ≤ 1) : + log (1 + x) ≤ x - x ^ 2 / 4 := by + -- `y ↦ log (1 + y) + y² / 4 - y` has derivative `-y (1 - y) / (2 (1 + y))`: it increases on + -- `(-1, 0]` and decreases on `[0, 1]`, so it is at most its value `0` at `0` + have hd' : ∀ y : ℝ, -1 < y → (1 + y)⁻¹ + (y / 2 - 1) = -(y * (1 - y)) / (2 * (1 + y)) := + fun y hy ↦ by + have : 1 + y ≠ 0 := by linarith + field_simp + ring + have h := LMLExplore.apply_le_apply_of_hasDerivAt_of_nonneg_of_nonpos + (f := fun z ↦ log (1 + z) + (z ^ 2 / 4 - z)) + (f' := fun y ↦ (1 + y)⁻¹ + (y / 2 - 1)) (x := x) (x₀ := 0) + (fun y hy ↦ hasDerivAt_log_one_add_add (p := fun z ↦ z ^ 2 / 4 - z) + ((((hasDerivAt_pow 2 y).div_const 4).sub (hasDerivAt_id y)).congr_deriv (by simp; ring)) + (by rcases Set.mem_uIcc.1 hy with hy | hy <;> linarith [hy.1, hy.2])) + (fun y hy ↦ by + rw [hd' y (hx₁.trans hy.1)] + exact div_nonneg (by nlinarith [hy.1, hy.2]) (by linarith [hx₁.trans hy.1])) + (fun y hy ↦ by + rw [hd' y (by linarith [hy.1])] + exact div_nonpos_of_nonpos_of_nonneg (by nlinarith [hy.1, hy.2]) (by linarith [hy.1])) + simp only [add_zero, log_one, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + zero_div, sub_self] at h + linarith + /-- The function `x ↦ log (1 + x log² x)` is monotone on `[1, ∞)`. It is the logarithm of the exploration function `f(x) = 1 + x log² x` of the asymptotically optimal UCB and KL-UCB algorithms. -/ diff --git a/LMLExplore/Analysis/SumIntegralComparisons.lean b/LMLExplore/Analysis/SumIntegralComparisons.lean new file mode 100644 index 00000000..0fcc1922 --- /dev/null +++ b/LMLExplore/Analysis/SumIntegralComparisons.lean @@ -0,0 +1,130 @@ +/- +Copyright (c) 2026 LMLExplore contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: LMLExplore contributors +-/ +module + +public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic + +/-! +# Weighted sums of an antitone function and its integral + +Mathlib's `AntitoneOn.sum_le_integral` compares the values of an antitone function at the +integers with its integral. Its weighted form compares the values at the partial sums of a +nonnegative sequence: for `f` antitone on `(c, c + ∑_{t < n} a t]` and integrable on +`[c, c + ∑_{t < n} a t]`, and `a t ≥ 0`, +`∑_{t < n} a t f (c + ∑_{s ≤ t} a s) ≤ ∫_c^{c + ∑_{t < n} a t} f`. + +Adaptive learning rates of online learning are of the form `η_t ∝ f (∑_{s ≤ t} a s)`, where +`a s` is the squared norm of the subgradient of round `s` (as in AdaGrad), and the regret bounds +sum the terms `a t f (∑_{s ≤ t} a s)`. The two instances below are the ones these bounds use. + +## Main statements + +* `AntitoneOn.sum_mul_le_integral_of_integrableOn`: the weighted comparison [Ora, Lemma 4.13]. +* `Real.sum_div_sqrt_le_two_mul_sqrt`: `∑_{t < n} a t / √(∑_{s ≤ t} a s) ≤ 2 √(∑_{t < n} a t)` + for `a t ≥ 0`, the case `f x = 1 / √x`. +* `Real.sum_div_add_le_log_div`: `∑_{t < n} a t / (c + ∑_{s ≤ t} a s) ≤ log ((c + ∑_t a t) / c)` + for `a t ≥ 0` and `c > 0`, the case `f x = 1 / x`. + +In the first, a term whose denominator vanishes has `a t = 0`, and Lean's convention `x / 0 = 0` +omits it, as [Ora] does. + +## References + +* [Ora] F. Orabona, *A Modern Introduction to Online Learning*, arXiv:1912.13213v10, Lemma 4.13. +-/ + +public section + +open Finset MeasureTheory Set intervalIntegral + +variable {f : ℝ → ℝ} {c : ℝ} {a : ℕ → ℝ} {n : ℕ} + +/-- **Weighted sums of an antitone function** [Ora, Lemma 4.13]. Let `a t ≥ 0` for `t < n`, and +let `f` be antitone on `(c, c + ∑_{t < n} a t]` and integrable on `[c, c + ∑_{t < n} a t]`. Then +`∑_{t < n} a t f (c + ∑_{s ≤ t} a s) ≤ ∫_c^{c + ∑_{t < n} a t} f`. + +The sign of `f` and its value at `c` play no role. With `a t = 1` it is Mathlib's +`AntitoneOn.sum_le_integral_of_integrableOn`. -/ +theorem AntitoneOn.sum_mul_le_integral_of_integrableOn + (hf : AntitoneOn f (Ioc c (c + ∑ t ∈ range n, a t))) + (hfi : IntegrableOn f (Icc c (c + ∑ t ∈ range n, a t))) (ha : ∀ t < n, 0 ≤ a t) : + ∑ t ∈ range n, a t * f (c + ∑ s ∈ range (t + 1), a s) ≤ + ∫ x in c..c + ∑ t ∈ range n, a t, f x := by + set S : ℕ → ℝ := fun t ↦ c + ∑ s ∈ range t, a s with hS + -- each term is at most the integral of `f` over `[S t, S (t + 1)]`, an interval of length + -- `a t` on which `f` is at least its value at the right endpoint + -- the partial sums `S t` increase from `S 0 = c` to `S n` on `[0, n]` + have hmono : ∀ {k l}, k ≤ l → l ≤ n → S k ≤ S l := fun hkl hl ↦ + add_le_add le_rfl (sum_le_sum_of_subset_of_nonneg (range_subset_range.2 hkl) + fun t ht _ ↦ ha t ((mem_range.1 ht).trans_le hl)) + have hc : ∀ {t}, t ≤ n → c ≤ S t := fun ht ↦ by simpa [hS] using hmono (Nat.zero_le _) ht + have hint : ∀ t < n, IntervalIntegrable f volume (S t) (S (t + 1)) := fun t ht ↦ + (intervalIntegrable_iff_integrableOn_Icc_of_le (hmono t.le_succ ht)).2 + (hfi.mono_set (Set.Icc_subset_Icc (hc ht.le) (hmono ht le_rfl))) + calc ∑ t ∈ range n, a t * f (S (t + 1)) + = ∑ t ∈ range n, ∫ _ in S t..S (t + 1), f (S (t + 1)) := by + refine sum_congr rfl fun t _ ↦ ?_ + simp [hS, sum_range_succ] + _ ≤ ∑ t ∈ range n, ∫ x in S t..S (t + 1), f x := by + refine sum_le_sum fun t ht ↦ ?_ + have ht : t < n := mem_range.1 ht + refine integral_mono_on_of_le_Ioo (hmono t.le_succ ht) intervalIntegrable_const + (hint t ht) fun x hx ↦ ?_ + have h0 : c ≤ S t := hc ht.le + have hn : S (t + 1) ≤ S n := hmono ht le_rfl + exact hf ⟨h0.trans_lt hx.1, hx.2.le.trans hn⟩ ⟨h0.trans_lt (hx.1.trans hx.2), hn⟩ + hx.2.le + _ = ∫ x in c..c + ∑ t ∈ range n, a t, f x := by + rw [sum_integral_adjacent_intervals hint] + simp [hS] + +namespace Real + +/-- **The square-root sum** [Ora, Lemma 4.13]: for `a t ≥ 0`, +`∑_{t < n} a t / √(∑_{s ≤ t} a s) ≤ 2 √(∑_{t < n} a t)`. + +A term whose denominator vanishes is `0` (then `a t = 0`). It is the sum of the stability terms +of online subgradient descent with the adaptive rates `η_t ∝ 1 / √(∑_{s ≤ t} ‖g_s‖²)`. -/ +theorem sum_div_sqrt_le_two_mul_sqrt (ha : ∀ t < n, 0 ≤ a t) : + ∑ t ∈ range n, a t / √(∑ s ∈ range (t + 1), a s) ≤ 2 * √(∑ t ∈ range n, a t) := by + set A := ∑ t ∈ range n, a t + have hA : 0 ≤ A := sum_nonneg fun t ht ↦ ha t (mem_range.1 ht) + -- `1 / √x = x ^ (-1 / 2)` on `[0, A]`, including at `0`, where both sides are `0` + have heq : EqOn (fun x : ℝ ↦ (√x)⁻¹) (fun x ↦ x ^ (-1 / 2 : ℝ)) (uIcc 0 A) := fun x hx ↦ by + rw [uIcc_of_le hA] at hx + simp only [sqrt_eq_rpow, neg_div, rpow_neg hx.1, one_div] + have hint : IntervalIntegrable (fun x : ℝ ↦ (√x)⁻¹) volume 0 A := + (intervalIntegral.intervalIntegrable_rpow' (r := -1 / 2) (by norm_num)).congr + (heq.symm.mono uIoc_subset_uIcc) + have hanti : AntitoneOn (fun x : ℝ ↦ (√x)⁻¹) (Ioc 0 (0 + A)) := fun x hx y _ hxy ↦ + inv_anti₀ (sqrt_pos.2 hx.1) (sqrt_le_sqrt hxy) + have h := hanti.sum_mul_le_integral_of_integrableOn + (by simpa using (intervalIntegrable_iff_integrableOn_Icc_of_le hA).1 hint) ha + rw [zero_add, integral_congr heq, integral_rpow (Or.inl (by norm_num))] at h + simp_rw [zero_add, ← div_eq_mul_inv] at h + refine h.trans_eq ?_ + rw [show (-1 / 2 : ℝ) + 1 = 1 / 2 by norm_num, zero_rpow (by norm_num), sqrt_eq_rpow] + ring + +/-- **The logarithmic sum** [Ora, Lemma 4.13]: for `a t ≥ 0` and `c > 0`, +`∑_{t < n} a t / (c + ∑_{s ≤ t} a s) ≤ log ((c + ∑_{t < n} a t) / c)`. + +It is the sum of the stability terms of online learning with the rates +`η_t ∝ 1 / (c + ∑_{s ≤ t} a s)`, as for strongly convex and exp-concave losses. -/ +theorem sum_div_add_le_log_div (hc : 0 < c) (ha : ∀ t < n, 0 ≤ a t) : + ∑ t ∈ range n, a t / (c + ∑ s ∈ range (t + 1), a s) ≤ + log ((c + ∑ t ∈ range n, a t) / c) := by + set A := ∑ t ∈ range n, a t + have hA : 0 ≤ A := sum_nonneg fun t ht ↦ ha t (mem_range.1 ht) + have hanti : AntitoneOn (fun x : ℝ ↦ x⁻¹) (Ioc c (c + A)) := fun x hx y _ hxy ↦ + inv_anti₀ (hc.trans hx.1) hxy + have hcont : ContinuousOn (fun x : ℝ ↦ x⁻¹) (Icc c (c + A)) := + continuousOn_inv₀.mono fun x hx ↦ (hc.trans_le hx.1).ne' + have h := hanti.sum_mul_le_integral_of_integrableOn hcont.integrableOn_Icc ha + simp_rw [← div_eq_mul_inv] at h + exact h.trans_eq (integral_inv_of_pos hc (by linarith)) + +end Real