feat: the self-bounding inequality [MDJKLV21, Lemma 13] with the corrected constant

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,19 @@ 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`.
+
+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
+  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

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`, 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,61 @@ 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`.
+
+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
+  · 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)²`, 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
+    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) :

LMLExplore/Analysis/SpecialFunctions/Log/SelfBounding.lean

@@ -0,0 +1,204 @@
+/-
+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.
+
+## 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,
+  *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
+
+/-- `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`. -/
+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τ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_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, 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)`. -/
+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 := 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.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
+
+/-- `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