feat: weighted sums of antitone functions, an implicit square-root bound, and quadratic bounds on log (1 + x)

LMLExplore/Analysis/Calculus/MeanValue.lean

@@ -0,0 +1,53 @@
+/-
+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` is continuous on the
+  segment between `x` and `x₀` and has derivative `f' y` at each `y` strictly between them, with
+  `f' ≥ 0` on `(x, x₀)` and `f' ≤ 0` on `(x₀, x)`, then `f x ≤ f x₀`.
+-/
+
+public section
+
+namespace LMLExplore
+
+/-- If `f` is continuous on the segment between `x` and `x₀` and differentiable in its interior,
+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₀ : ℝ}
+    (hcont : ContinuousOn f (Set.uIcc x x₀))
+    (hd : ∀ y ∈ Set.Ioo (min x x₀) (max 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
+  rcases le_total x x₀ with h0 | h0
+  · rw [Set.uIcc_of_le h0] at hcont
+    rw [min_eq_left h0, max_eq_right h0] at hd
+    refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc x x₀) hcont
+      (fun y hy ↦ (hd y (by rwa [interior_Icc] at hy)).hasDerivWithinAt) ?_
+      ⟨le_rfl, h0⟩ ⟨h0, le_rfl⟩ h0
+    rw [interior_Icc]
+    exact hneg
+  · rw [Set.uIcc_of_ge h0] at hcont
+    rw [min_eq_right h0, max_eq_left h0] at hd
+    refine antitoneOn_of_hasDerivWithinAt_nonpos (convex_Icc x₀ x) hcont
+      (fun y hy ↦ (hd y (by rwa [interior_Icc] at hy)).hasDerivWithinAt) ?_
+      ⟨le_rfl, h0⟩ ⟨h0, le_rfl⟩ h0
+    rw [interior_Icc]
+    exact hpos
+
+end LMLExplore

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

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,76 @@ 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 hd : ∀ y ∈ Set.uIcc x 0, HasDerivAt (fun z ↦ -(log (1 + z) + (z ^ 2 - z)))
+      (-((1 + y)⁻¹ + (2 * y - 1))) y := 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
+  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 ↦ (hd y hy).continuousAt.continuousWithinAt)
+    (fun y hy ↦ hd y (Set.uIoo_subset_uIcc_self hy))
+    (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 hd : ∀ y ∈ Set.uIcc x 0, HasDerivAt (fun z ↦ log (1 + z) + (z ^ 2 / 4 - z))
+      ((1 + y)⁻¹ + (y / 2 - 1)) y := 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])
+  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 ↦ (hd y hy).continuousAt.continuousWithinAt)
+    (fun y hy ↦ hd y (Set.uIoo_subset_uIcc_self hy))
+    (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. -/

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