From feedb0de5112ff1af6ebb6dca04efc1dcd66d1e0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 10:59:55 +0100 Subject: [PATCH 1/2] feat: the self-bounding inequality [MDJKLV21, Lemma 13] with the corrected constant MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Solve `τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)`, `L = log (α τ)`, for `τ`: `Real.le_of_le_sqrt_mul_add` (constant `C₁ = (8/5) log (11 α² (A + E) (C + √D)²)`) and `Real.le_of_le_sqrt_mul_add'` (`(C + D)²`, for `D ≥ 1`), with the root of a quadratic inequality `Real.le_add_sqrt_of_sq_le` and the logarithm bounds `Real.log_le_rpow_div_exp_one_mul`, `Real.log_le_of_le_mul_sq_log`. Co-Authored-By: Claude Code --- LMLExplore/Analysis/Real/Sqrt.lean | 13 ++ .../Analysis/SpecialFunctions/Log/Basic.lean | 51 +++++ .../SpecialFunctions/Log/SelfBounding.lean | 196 ++++++++++++++++++ 3 files changed, 260 insertions(+) create mode 100644 LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean diff --git a/LMLExplore/Analysis/Real/Sqrt.lean b/LMLExplore/Analysis/Real/Sqrt.lean index 1875a272..2c43d5b7 100644 --- a/LMLExplore/Analysis/Real/Sqrt.lean +++ b/LMLExplore/Analysis/Real/Sqrt.lean @@ -26,6 +26,9 @@ public import Mathlib.Analysis.Real.Sqrt `√n`, as for the exploration rates of C-tracking. * `Real.tendsto_one_add_sqrt_div_atTop`: `(1 + √x) / x → 0` as `x → ∞`, so that a tracking error of order `1 + √n` after `n` rounds, as for C-tracking, is `o(n)`. +* `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.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`. @@ -114,6 +117,16 @@ theorem tendsto_one_add_sqrt_div_atTop : Tendsto (fun x : ℝ ↦ (1 + √x) / x filter_upwards with x rw [add_div, sqrt_div_self', one_div, Function.comp_apply, one_div] +/-- The root of a quadratic inequality: `x² ≤ b x + c` with `b, c ≥ 0` forces `x ≤ b + √c`. -/ +theorem le_add_sqrt_of_sq_le {x b c : ℝ} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : x ^ 2 ≤ b * x + c) : + x ≤ b + √c := by + by_contra! hlt + have hs := sq_sqrt hc + have hs0 := sqrt_nonneg c + -- `(x - √c) (x - b - √c) > 0` and `√c (2 x - b - 2 √c) ≥ 0` add up to `x² - b x > c` + 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)] + /-- `∑_{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 cb9dd3ea..68602a2f 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean @@ -20,6 +20,11 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv * `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`. * `Real.log_div_rpow_le_exp_neg_one`: `log x / x ^ p ≤ 1 / e` for `x ≥ 1` and `p ≥ 1`. +* `Real.log_le_rpow_div_exp_one_mul`: `log y ≤ y ^ γ / (e γ)` for `y ≥ 0` and `γ > 0`, Mathlib's + `Real.log_le_rpow_div` sharpened by the factor `e`. +* `Real.log_le_of_le_mul_sq_log`: if `1 ≤ y ≤ M log² y` with `M > 0`, then + `log y ≤ (8 / 5) log (4 M)`. It bounds the logarithm in the self-bounding inequality + `Real.le_of_le_sqrt_mul_add`. * `Real.monotone_log_two_mul_mul_add_one`: `n ↦ log (2 n (n + 1))` is monotone on `ℕ`. * `Real.tendsto_log_one_add_mul_log_sq_div_log_atTop`: `log (1 + x log² x) / log x → 1` as `x → ∞`. @@ -154,6 +159,52 @@ theorem log_div_rpow_le_exp_neg_one {x p : ℝ} (hx : 1 ≤ x) (hp : 1 ≤ p) : (by simpa using rpow_le_rpow_of_exponent_le hx hp) _ ≤ exp (-1) := h_log +/-- `log y ≤ y ^ γ / (e γ)` for `y ≥ 0` and `γ > 0`: Mathlib's `Real.log_le_rpow_div` sharpened by +the factor `e`. -/ +theorem log_le_rpow_div_exp_one_mul {y γ : ℝ} (hy : 0 ≤ y) (hγ : 0 < γ) : + log y ≤ y ^ γ / (exp 1 * γ) := by + rcases hy.eq_or_lt with rfl | hy + · rw [log_zero, zero_rpow hγ.ne', zero_div] + have hz : 0 < y ^ γ := rpow_pos_of_pos hy γ + -- `log (y ^ γ / e) ≤ y ^ γ / e - 1`, and `log (y ^ γ / e) = γ log y - 1` + have h := log_le_sub_one_of_pos (show 0 < y ^ γ / exp 1 by positivity) + rw [log_div hz.ne' (exp_pos 1).ne', log_exp, log_rpow hy, sub_le_sub_iff_right] at h + rw [le_div_iff₀ (exp_pos 1)] at h + rw [le_div_iff₀ (by positivity)] + linarith + +/-- If `1 ≤ y ≤ M (log y)²` with `M > 0`, then `log y ≤ (8 / 5) log (4 M)`. -/ +theorem log_le_of_le_mul_sq_log {y M : ℝ} (hy : 1 ≤ y) (hM : 0 < M) (h : y ≤ M * log y ^ 2) : + log y ≤ 8 / 5 * log (4 * M) := by + have hy0 : 0 < y := by linarith + have hlog : 0 ≤ log y := log_nonneg hy + have he : 2.7 < exp 1 := lt_trans (by norm_num) exp_one_gt_d9 + -- `log y ≤ 16 / (3 e) y ^ (3 / 16)`, hence `log² y ≤ 4 y ^ (3 / 8)` + have h1 : log y ≤ 16 / (3 * exp 1) * y ^ (3 / 16 : ℝ) := by + calc log y ≤ y ^ (3 / 16 : ℝ) / (exp 1 * (3 / 16)) := + log_le_rpow_div_exp_one_mul hy0.le (by norm_num) + _ = 16 / (3 * exp 1) * y ^ (3 / 16 : ℝ) := by field_simp + have h2 : log y ^ 2 ≤ 4 * y ^ (3 / 8 : ℝ) := by + calc log y ^ 2 ≤ (16 / (3 * exp 1) * y ^ (3 / 16 : ℝ)) ^ 2 := pow_le_pow_left₀ hlog h1 2 + _ = (16 / (3 * exp 1)) ^ 2 * y ^ (3 / 8 : ℝ) := by + rw [mul_pow, sq (y ^ (3 / 16 : ℝ)), ← rpow_add hy0]; norm_num + _ ≤ 4 * y ^ (3 / 8 : ℝ) := by + gcongr + rw [div_pow, div_le_iff₀ (by positivity)] + nlinarith + -- so `y = y ^ (5 / 8) y ^ (3 / 8) ≤ 4 M y ^ (3 / 8)`, that is `y ^ (5 / 8) ≤ 4 M` + have h3 : y ^ (5 / 8 : ℝ) ≤ 4 * M := by + have hy38 : 0 < y ^ (3 / 8 : ℝ) := rpow_pos_of_pos hy0 _ + refine le_of_mul_le_mul_right ?_ hy38 + rw [← rpow_add hy0, show (5 / 8 : ℝ) + 3 / 8 = 1 by norm_num, rpow_one] + calc y ≤ M * log y ^ 2 := h + _ ≤ M * (4 * y ^ (3 / 8 : ℝ)) := by gcongr + _ = 4 * M * y ^ (3 / 8 : ℝ) := by ring + have h5 : 5 / 8 * log y ≤ log (4 * M) := by + rw [← log_rpow hy0] + exact log_le_log (rpow_pos_of_pos hy0 _) h3 + linarith + /-- If `g n / log n → D` as `n → ∞` and `D < c`, then eventually `g n < c log n`. -/ theorem eventually_lt_mul_log_of_tendsto_div_log {g : ℕ → ℝ} {D c : ℝ} (hg : Tendsto (fun n : ℕ ↦ g n / log n) atTop (𝓝 D)) (hc : D < c) : diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean b/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean new file mode 100644 index 00000000..d7f36d90 --- /dev/null +++ b/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean @@ -0,0 +1,196 @@ +/- +Copyright (c) 2026 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +module + +public import LMLExplore.Analysis.Real.Sqrt +public import LMLExplore.Analysis.SpecialFunctions.Log.Basic +import Mathlib.Analysis.Complex.ExponentialBounds + +/-! +# The self-bounding inequality + +Sample complexity analyses of exploration algorithms bound the number of rounds `τ` by an +implicit inequality in which `τ` appears on both sides, under a square root and inside +logarithms: with `L = log (α τ)`, +`τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)`. +This file solves it for `τ`, for `α ≥ e`, `A, B, C, D ≥ 0` and `B ≤ E`. Write +`K = C² (A + B) + (D + 2 √D C) (A + E)`. + +## Main statements + +* `Real.le_mul_sq_of_le_sqrt_mul_add`: the same hypothesis with any `L ≥ 1` in place of + `log (α τ)` gives `τ ≤ K L²`. +* `Real.log_le_of_le_sqrt_mul_add`: if `τ > 1`, then `L ≤ (8 / 5) log (4 α K)`. +* `Real.le_mul_sq_log_add_one_of_le_sqrt_mul_add`: `τ ≤ K ((8 / 5) log M)² + 1` for every + `M ≥ 4 α K`. +* `Real.le_of_le_sqrt_mul_add`: **the self-bounding inequality** [MDJKLV21, Lemma 13], + `τ ≤ C² (A + B) C₁² + (D + 2 √D C) (A + E) C₁² + 1` with + `C₁ = (8 / 5) log (11 α² (A + E) (C + √D)²)`. +* `Real.le_of_le_sqrt_mul_add'`: the same bound with `C₁ = (8 / 5) log (11 α² (A + E) (C + D)²)`, + for `D ≥ 1`. + +[MDJKLV21, Lemma 13] and [EV26, Lemma 29] state the bound with +`C₁ = (8 / 5) log (11 α² (A + E) (C + D))` and assume `A, B, C, D > 0` and `B ≥ 1`. That constant +is too small: `α = e`, `B = E = 1`, `C = 1000`, `A = D = 10⁻⁶` and `τ = 4 · 10⁸` satisfy the +hypothesis but not the conclusion. The factor `C + D` must be squared, which is +`Real.le_of_le_sqrt_mul_add'`; the positivity assumptions and `B ≥ 1` are not needed. + +## References + +* [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, + arXiv:2007.13442, Lemma 13. +* [EV26] A. Essakine and C. Vernade, *Tight sample complexity bounds for entropic best policy + identification*, COLT 2026, arXiv:2605.13717, Lemma 29. +-/ + +public section + +namespace Real + +variable {A B C D E α τ : ℝ} + +/-- The quadratic part of the self-bounding inequality: if `L ≥ 1` and +`τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)` with `A, B, C, D ≥ 0` and `B ≤ E`, then `τ ≤ K L²` for +`K = C² (A + B) + (D + 2 √D C) (A + E)`. -/ +theorem le_mul_sq_of_le_sqrt_mul_add {L : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) + (hE : B ≤ E) (hL : 1 ≤ L) + (h : τ ≤ C * √(τ * (A * L + B * L ^ 2)) + D * (A * L + E * L ^ 2)) : + τ ≤ (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) * L ^ 2 := by + have hL0 : 0 ≤ L := by linarith + have hAB : 0 ≤ A + B := by linarith + have hAE : 0 ≤ A + E := by linarith + rcases lt_or_ge τ 0 with hτ | hτ + · have : 0 ≤ (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) * L ^ 2 := by positivity + linarith + -- `A L ≤ A L²` since `L ≥ 1` + have hAL : A * L ≤ A * L ^ 2 := mul_le_mul_of_nonneg_left (by nlinarith) hA + -- the quadratic inequality `τ ≤ C L √(A + B) √τ + D (A + E) L²` in `√τ` + have hτ' : τ ≤ C * L * √(A + B) * √τ + D * (A + E) * L ^ 2 := by + calc τ ≤ C * √(τ * (A * L + B * L ^ 2)) + D * (A * L + E * L ^ 2) := h + _ ≤ C * √(τ * ((A + B) * L ^ 2)) + D * ((A + E) * L ^ 2) := by gcongr <;> linarith + _ = C * L * √(A + B) * √τ + D * (A + E) * L ^ 2 := by + rw [show τ * ((A + B) * L ^ 2) = L ^ 2 * ((A + B) * τ) by ring, + sqrt_mul (by positivity), sqrt_sq hL0, sqrt_mul hAB] + ring + -- its solution `√τ ≤ C L √(A + B) + √D √(A + E) L` + have hx : √τ ≤ C * L * √(A + B) + √D * √(A + E) * L := by + have := le_add_sqrt_of_sq_le (x := √τ) (b := C * L * √(A + B)) (c := D * (A + E) * L ^ 2) + (by positivity) (mul_nonneg (mul_nonneg hD hAE) (sq_nonneg L)) + (by rw [sq_sqrt hτ]; linarith) + rwa [sqrt_mul (mul_nonneg hD hAE), sqrt_mul hD, sqrt_sq hL0] at this + have hae : √(A + B) * √(A + E) ≤ A + E := by + calc √(A + B) * √(A + E) ≤ √(A + E) * √(A + E) := by gcongr + _ = A + E := mul_self_sqrt hAE + calc τ = √τ ^ 2 := (sq_sqrt hτ).symm + _ ≤ (C * L * √(A + B) + √D * √(A + E) * L) ^ 2 := by gcongr + _ = L ^ 2 * (C ^ 2 * (A + B) + D * (A + E)) + + 2 * C * √D * L ^ 2 * (√(A + B) * √(A + E)) := by + linear_combination (C ^ 2 * L ^ 2) * sq_sqrt hAB + (L ^ 2 * √D ^ 2) * sq_sqrt hAE + + (L ^ 2 * (A + E)) * sq_sqrt hD + _ ≤ L ^ 2 * (C ^ 2 * (A + B) + D * (A + E)) + 2 * C * √D * L ^ 2 * (A + E) := by gcongr + _ = (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) * L ^ 2 := by ring + +/-- The logarithm in the self-bounding inequality: `log (α τ) ≤ (8 / 5) log (4 α K)` with +`K = C² (A + B) + (D + 2 √D C) (A + E)`, for `α ≥ e` and `τ > 1`. -/ +theorem log_le_of_le_sqrt_mul_add (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) + (hE : B ≤ E) (hα : exp 1 ≤ α) (hτ : 1 < τ) + (h : τ ≤ C * √(τ * (A * log (α * τ) + B * log (α * τ) ^ 2)) + + D * (A * log (α * τ) + E * log (α * τ) ^ 2)) : + log (α * τ) ≤ 8 / 5 * log (4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E))) := by + set K := C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E) + have hα0 : 0 < α := (exp_pos 1).trans_le hα + have hατ : exp 1 ≤ α * τ := hα.trans (le_mul_of_one_le_right hα0.le hτ.le) + have hτK := le_mul_sq_of_le_sqrt_mul_add hA hB hC hD hE + ((le_log_iff_exp_le (mul_pos hα0 (by linarith))).2 hατ) h + have hK0 : 0 < K := by + by_contra! hK + nlinarith [sq_nonneg (log (α * τ))] + rw [mul_assoc] + refine log_le_of_le_mul_sq_log ((one_le_exp zero_le_one).trans hατ) (by positivity) ?_ + calc α * τ ≤ α * (K * log (α * τ) ^ 2) := by gcongr + _ = α * K * log (α * τ) ^ 2 := by ring + +/-- The self-bounding inequality, sharp form: if `τ` satisfies +`τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)` with `L = log (α τ)`, `α ≥ e`, `A, B, C, D ≥ 0` and +`B ≤ E`, then `τ ≤ K ((8 / 5) log M)² + 1` for every `M ≥ 4 α K`, where +`K = C² (A + B) + (D + 2 √D C) (A + E)`. -/ +theorem le_mul_sq_log_add_one_of_le_sqrt_mul_add (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) + (hD : 0 ≤ D) (hE : B ≤ E) (hα : exp 1 ≤ α) + (h : τ ≤ C * √(τ * (A * log (α * τ) + B * log (α * τ) ^ 2)) + + D * (A * log (α * τ) + E * log (α * τ) ^ 2)) + {M : ℝ} (hM : 4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) ≤ M) : + τ ≤ (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) * (8 / 5 * log M) ^ 2 + 1 := by + set K := C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E) + have hK : 0 ≤ K := by have := hB.trans hE; positivity + rcases le_or_gt τ 1 with h1 | h1 + · nlinarith [sq_nonneg (8 / 5 * log M)] + have hα0 : 0 < α := (exp_pos 1).trans_le hα + have hL1 : 1 ≤ log (α * τ) := + (le_log_iff_exp_le (mul_pos hα0 (by linarith))).2 + (hα.trans (le_mul_of_one_le_right hα0.le h1.le)) + have hτK := le_mul_sq_of_le_sqrt_mul_add hA hB hC hD hE hL1 h + have hK0 : 0 < K := by + by_contra! hK + nlinarith [sq_nonneg (log (α * τ))] + have hL : log (α * τ) ≤ 8 / 5 * log M := + (log_le_of_le_sqrt_mul_add hA hB hC hD hE hα h1 h).trans (by gcongr) + calc τ ≤ K * log (α * τ) ^ 2 := hτK + _ ≤ K * (8 / 5 * log M) ^ 2 := by gcongr + _ ≤ K * (8 / 5 * log M) ^ 2 + 1 := by linarith + +/-- `4 α K ≤ 11 α² (A + E) (C + √D)²` for `K = C² (A + B) + (D + 2 √D C) (A + E)` and `α ≥ e`. -/ +private lemma four_mul_mul_le_mul_sq_add_sqrt (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) + (hD : 0 ≤ D) (hE : B ≤ E) (hα : exp 1 ≤ α) : + 4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) + ≤ 11 * α ^ 2 * (A + E) * (C + √D) ^ 2 := by + have hE0 : 0 ≤ E := hB.trans hE + have he : 2.7 < exp 1 := lt_trans (by norm_num) exp_one_gt_d9 + -- `K ≤ (A + E) (C + √D)²` since `B ≤ E`, and `4 α ≤ 11 α²` since `α ≥ e` + have hK : C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E) ≤ (A + E) * (C + √D) ^ 2 := by + nlinarith [mul_le_mul_of_nonneg_left hE (sq_nonneg C), sq_sqrt hD] + have h4 : 4 * α ≤ 11 * α ^ 2 := by nlinarith + calc 4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) + ≤ 11 * α ^ 2 * ((A + E) * (C + √D) ^ 2) := by + gcongr + _ = 11 * α ^ 2 * (A + E) * (C + √D) ^ 2 := by ring + +/-- **The self-bounding inequality** [MDJKLV21, Lemma 13], with the corrected constant: if `τ` +satisfies `τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)` with `L = log (α τ)`, `α ≥ e`, +`A, B, C, D ≥ 0` and `B ≤ E`, then `τ ≤ C² (A + B) C₁² + (D + 2 √D C) (A + E) C₁² + 1` with +`C₁ = (8 / 5) log (11 α² (A + E) (C + √D)²)`. -/ +theorem le_of_le_sqrt_mul_add (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) (hE : B ≤ E) + (hα : exp 1 ≤ α) + (h : τ ≤ C * √(τ * (A * log (α * τ) + B * log (α * τ) ^ 2)) + + D * (A * log (α * τ) + E * log (α * τ) ^ 2)) : + τ ≤ C ^ 2 * (A + B) * (8 / 5 * log (11 * α ^ 2 * (A + E) * (C + √D) ^ 2)) ^ 2 + + (D + 2 * √D * C) * (A + E) * (8 / 5 * log (11 * α ^ 2 * (A + E) * (C + √D) ^ 2)) ^ 2 + + 1 := by + have := le_mul_sq_log_add_one_of_le_sqrt_mul_add hA hB hC hD hE hα h + (four_mul_mul_le_mul_sq_add_sqrt hA hB hC hD hE hα) + linarith + +/-- **The self-bounding inequality** [MDJKLV21, Lemma 13] for `D ≥ 1`, with the constant +`C₁ = (8 / 5) log (11 α² (A + E) (C + D)²)`: if `τ` satisfies +`τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)` with `L = log (α τ)`, `α ≥ e`, `A, B, C ≥ 0` and +`B ≤ E`, then `τ ≤ C² (A + B) C₁² + (D + 2 √D C) (A + E) C₁² + 1`. -/ +theorem le_of_le_sqrt_mul_add' (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 1 ≤ D) (hE : B ≤ E) + (hα : exp 1 ≤ α) + (h : τ ≤ C * √(τ * (A * log (α * τ) + B * log (α * τ) ^ 2)) + + D * (A * log (α * τ) + E * log (α * τ) ^ 2)) : + τ ≤ C ^ 2 * (A + B) * (8 / 5 * log (11 * α ^ 2 * (A + E) * (C + D) ^ 2)) ^ 2 + + (D + 2 * √D * C) * (A + E) * (8 / 5 * log (11 * α ^ 2 * (A + E) * (C + D) ^ 2)) ^ 2 + + 1 := by + have hD0 : 0 ≤ D := zero_le_one.trans hD + have hE0 : 0 ≤ E := hB.trans hE + have hsqrt : √D ≤ D := (sqrt_le_left hD0).2 (by nlinarith) + have hM : 4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) + ≤ 11 * α ^ 2 * (A + E) * (C + D) ^ 2 := + (four_mul_mul_le_mul_sq_add_sqrt hA hB hC hD0 hE hα).trans (by gcongr) + have := le_mul_sq_log_add_one_of_le_sqrt_mul_add hA hB hC hD0 hE hα h hM + linarith + +end Real From f7f8e8444dfe24306b4b524eb287a14b82d94942 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 12 Nov 2026 12:25:09 +0100 Subject: [PATCH 2/2] fix: address review of the self-bounding inequality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Credit the Essakine2026Tight formalization in the changed files, drop the redundant hypothesis 0 < M of Real.log_le_of_le_mul_sq_log, weaken 1 < τ to 1 ≤ τ in Real.log_le_of_le_sqrt_mul_add, factor the shared 1 ≤ log (α τ) step into a private helper, and say "general form" instead of "sharp form". Co-Authored-By: Claude Code --- LMLExplore/Analysis/Real/Sqrt.lean | 5 ++- .../Analysis/SpecialFunctions/Log/Basic.lean | 17 +++++++-- .../SpecialFunctions/Log/SelfBounding.lean | 38 +++++++++++-------- 3 files changed, 40 insertions(+), 20 deletions(-) diff --git a/LMLExplore/Analysis/Real/Sqrt.lean b/LMLExplore/Analysis/Real/Sqrt.lean index 2c43d5b7..d59ae81c 100644 --- a/LMLExplore/Analysis/Real/Sqrt.lean +++ b/LMLExplore/Analysis/Real/Sqrt.lean @@ -117,7 +117,10 @@ theorem tendsto_one_add_sqrt_div_atTop : Tendsto (fun x : ℝ ↦ (1 + √x) / x filter_upwards with x rw [add_div, sqrt_div_self', one_div, Function.comp_apply, one_div] -/-- The root of a quadratic inequality: `x² ≤ b x + c` with `b, c ≥ 0` forces `x ≤ b + √c`. -/ +/-- The root of a quadratic inequality: `x² ≤ b x + c` with `b, c ≥ 0` forces `x ≤ b + √c`. + +Adapted from the formalization in the paper project RemyDegenne/Essakine2026Tight (same author), +file `ForLMLExplore/Analysis/Real/Sqrt.lean`. -/ theorem le_add_sqrt_of_sq_le {x b c : ℝ} (hb : 0 ≤ b) (hc : 0 ≤ c) (h : x ^ 2 ≤ b * x + c) : x ≤ b + √c := by by_contra! hlt diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean index 68602a2f..9bc47be7 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean @@ -22,7 +22,7 @@ import Mathlib.Analysis.SpecialFunctions.Log.Deriv * `Real.log_div_rpow_le_exp_neg_one`: `log x / x ^ p ≤ 1 / e` for `x ≥ 1` and `p ≥ 1`. * `Real.log_le_rpow_div_exp_one_mul`: `log y ≤ y ^ γ / (e γ)` for `y ≥ 0` and `γ > 0`, Mathlib's `Real.log_le_rpow_div` sharpened by the factor `e`. -* `Real.log_le_of_le_mul_sq_log`: if `1 ≤ y ≤ M log² y` with `M > 0`, then +* `Real.log_le_of_le_mul_sq_log`: if `1 ≤ y ≤ M log² y`, then `log y ≤ (8 / 5) log (4 M)`. It bounds the logarithm in the self-bounding inequality `Real.le_of_le_sqrt_mul_add`. * `Real.monotone_log_two_mul_mul_add_one`: `n ↦ log (2 n (n + 1))` is monotone on `ℕ`. @@ -160,7 +160,10 @@ theorem log_div_rpow_le_exp_neg_one {x p : ℝ} (hx : 1 ≤ x) (hp : 1 ≤ p) : _ ≤ exp (-1) := h_log /-- `log y ≤ y ^ γ / (e γ)` for `y ≥ 0` and `γ > 0`: Mathlib's `Real.log_le_rpow_div` sharpened by -the factor `e`. -/ +the factor `e`. + +Adapted from the formalization in the paper project RemyDegenne/Essakine2026Tight (same author), +file `ForLMLExplore/Analysis/SpecialFunctions/Pow/Real.lean`. -/ theorem log_le_rpow_div_exp_one_mul {y γ : ℝ} (hy : 0 ≤ y) (hγ : 0 < γ) : log y ≤ y ^ γ / (exp 1 * γ) := by rcases hy.eq_or_lt with rfl | hy @@ -173,11 +176,17 @@ theorem log_le_rpow_div_exp_one_mul {y γ : ℝ} (hy : 0 ≤ y) (hγ : 0 < γ) : rw [le_div_iff₀ (by positivity)] linarith -/-- If `1 ≤ y ≤ M (log y)²` with `M > 0`, then `log y ≤ (8 / 5) log (4 M)`. -/ -theorem log_le_of_le_mul_sq_log {y M : ℝ} (hy : 1 ≤ y) (hM : 0 < M) (h : y ≤ M * log y ^ 2) : +/-- If `1 ≤ y ≤ M (log y)²`, then `log y ≤ (8 / 5) log (4 M)`. + +Adapted from the formalization in the paper project RemyDegenne/Essakine2026Tight (same author), +file `ForLMLExplore/Analysis/SpecialFunctions/Pow/Real.lean`, where `M > 0` is assumed. -/ +theorem log_le_of_le_mul_sq_log {y M : ℝ} (hy : 1 ≤ y) (h : y ≤ M * log y ^ 2) : log y ≤ 8 / 5 * log (4 * M) := by have hy0 : 0 < y := by linarith have hlog : 0 ≤ log y := log_nonneg hy + have hM : 0 < M := by + by_contra! hM + nlinarith [mul_nonneg (neg_nonneg.2 hM) (sq_nonneg (log y))] have he : 2.7 < exp 1 := lt_trans (by norm_num) exp_one_gt_d9 -- `log y ≤ 16 / (3 e) y ^ (3 / 16)`, hence `log² y ≤ 4 y ^ (3 / 8)` have h1 : log y ≤ 16 / (3 * exp 1) * y ^ (3 / 16 : ℝ) := by diff --git a/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean b/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean index d7f36d90..70b42b2c 100644 --- a/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean +++ b/LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean @@ -23,7 +23,7 @@ This file solves it for `τ`, for `α ≥ e`, `A, B, C, D ≥ 0` and `B ≤ E`. * `Real.le_mul_sq_of_le_sqrt_mul_add`: the same hypothesis with any `L ≥ 1` in place of `log (α τ)` gives `τ ≤ K L²`. -* `Real.log_le_of_le_sqrt_mul_add`: if `τ > 1`, then `L ≤ (8 / 5) log (4 α K)`. +* `Real.log_le_of_le_sqrt_mul_add`: if `τ ≥ 1`, then `L ≤ (8 / 5) log (4 α K)`. * `Real.le_mul_sq_log_add_one_of_le_sqrt_mul_add`: `τ ≤ K ((8 / 5) log M)² + 1` for every `M ≥ 4 α K`. * `Real.le_of_le_sqrt_mul_add`: **the self-bounding inequality** [MDJKLV21, Lemma 13], @@ -38,6 +38,14 @@ is too small: `α = e`, `B = E = 1`, `C = 1000`, `A = D = 10⁻⁶` and `τ = 4 hypothesis but not the conclusion. The factor `C + D` must be squared, which is `Real.le_of_le_sqrt_mul_add'`; the positivity assumptions and `B ≥ 1` are not needed. +## Implementation notes + +The statements and proofs are adapted from the formalization in the paper project +RemyDegenne/Essakine2026Tight (same author), file +`ForLMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean`. Here the quadratic part +`Real.le_mul_sq_of_le_sqrt_mul_add` holds for any `L ≥ 1` rather than only `L = log (α τ)`, and +the final bounds do not assume `τ ≥ 0`. + ## References * [MDJKLV21] P. Ménard, O. D. Domingues, A. Jonsson, E. Kaufmann, E. Leurent and M. Valko, @@ -94,27 +102,29 @@ theorem le_mul_sq_of_le_sqrt_mul_add {L : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hC _ ≤ L ^ 2 * (C ^ 2 * (A + B) + D * (A + E)) + 2 * C * √D * L ^ 2 * (A + E) := by gcongr _ = (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E)) * L ^ 2 := by ring +/-- `1 ≤ log (α τ)` for `α ≥ e` and `τ ≥ 1`. -/ +private lemma one_le_log_mul (hα : exp 1 ≤ α) (hτ : 1 ≤ τ) : 1 ≤ log (α * τ) := by + have hα0 : 0 < α := (exp_pos 1).trans_le hα + exact (le_log_iff_exp_le (mul_pos hα0 (by linarith))).2 + (hα.trans (le_mul_of_one_le_right hα0.le hτ)) + /-- The logarithm in the self-bounding inequality: `log (α τ) ≤ (8 / 5) log (4 α K)` with -`K = C² (A + B) + (D + 2 √D C) (A + E)`, for `α ≥ e` and `τ > 1`. -/ +`K = C² (A + B) + (D + 2 √D C) (A + E)`, for `α ≥ e` and `τ ≥ 1`. -/ theorem log_le_of_le_sqrt_mul_add (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) (hD : 0 ≤ D) - (hE : B ≤ E) (hα : exp 1 ≤ α) (hτ : 1 < τ) + (hE : B ≤ E) (hα : exp 1 ≤ α) (hτ : 1 ≤ τ) (h : τ ≤ C * √(τ * (A * log (α * τ) + B * log (α * τ) ^ 2)) + D * (A * log (α * τ) + E * log (α * τ) ^ 2)) : log (α * τ) ≤ 8 / 5 * log (4 * α * (C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E))) := by set K := C ^ 2 * (A + B) + (D + 2 * √D * C) * (A + E) have hα0 : 0 < α := (exp_pos 1).trans_le hα - have hατ : exp 1 ≤ α * τ := hα.trans (le_mul_of_one_le_right hα0.le hτ.le) - have hτK := le_mul_sq_of_le_sqrt_mul_add hA hB hC hD hE - ((le_log_iff_exp_le (mul_pos hα0 (by linarith))).2 hατ) h - have hK0 : 0 < K := by - by_contra! hK - nlinarith [sq_nonneg (log (α * τ))] + have hτK := le_mul_sq_of_le_sqrt_mul_add hA hB hC hD hE (one_le_log_mul hα hτ) h rw [mul_assoc] - refine log_le_of_le_mul_sq_log ((one_le_exp zero_le_one).trans hατ) (by positivity) ?_ + refine log_le_of_le_mul_sq_log (one_le_mul_of_one_le_of_one_le + ((one_le_exp zero_le_one).trans hα) hτ) ?_ calc α * τ ≤ α * (K * log (α * τ) ^ 2) := by gcongr _ = α * K * log (α * τ) ^ 2 := by ring -/-- The self-bounding inequality, sharp form: if `τ` satisfies +/-- The self-bounding inequality, general form: if `τ` satisfies `τ ≤ C √(τ (A L + B L²)) + D (A L + E L²)` with `L = log (α τ)`, `α ≥ e`, `A, B, C, D ≥ 0` and `B ≤ E`, then `τ ≤ K ((8 / 5) log M)² + 1` for every `M ≥ 4 α K`, where `K = C² (A + B) + (D + 2 √D C) (A + E)`. -/ @@ -129,15 +139,13 @@ theorem le_mul_sq_log_add_one_of_le_sqrt_mul_add (hA : 0 ≤ A) (hB : 0 ≤ B) ( rcases le_or_gt τ 1 with h1 | h1 · nlinarith [sq_nonneg (8 / 5 * log M)] have hα0 : 0 < α := (exp_pos 1).trans_le hα - have hL1 : 1 ≤ log (α * τ) := - (le_log_iff_exp_le (mul_pos hα0 (by linarith))).2 - (hα.trans (le_mul_of_one_le_right hα0.le h1.le)) + have hL1 := one_le_log_mul hα h1.le have hτK := le_mul_sq_of_le_sqrt_mul_add hA hB hC hD hE hL1 h have hK0 : 0 < K := by by_contra! hK nlinarith [sq_nonneg (log (α * τ))] have hL : log (α * τ) ≤ 8 / 5 * log M := - (log_le_of_le_sqrt_mul_add hA hB hC hD hE hα h1 h).trans (by gcongr) + (log_le_of_le_sqrt_mul_add hA hB hC hD hE hα h1.le h).trans (by gcongr) calc τ ≤ K * log (α * τ) ^ 2 := hτK _ ≤ K * (8 / 5 * log M) ^ 2 := by gcongr _ ≤ K * (8 / 5 * log M) ^ 2 + 1 := by linarith