/- Copyright (c) 2026 Terence Tao. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Terence Tao -/ import Mathlib.Analysis.SpecialFunctions.Log.Deriv import Mathlib.Analysis.SpecialFunctions.Sqrt import Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp import Mathlib.Analysis.Calculus.MeanValue /-! # `log (sinh h / h) ≤ √(h² + 9) - 3` This is the sharp estimate behind the simplified polar inequality `β(1) ≤ α/(3+α)` of the blog post: applied at `u = αβ(1)/2`, `h = α(2-β(1))/2`, it is exactly what turns `1 ≤ ∫₀¹ exp(α(-1 + (2-β(1))t)) dt = e^{-u} sinh h / h` into `β(1) ≤ α/(3+α)`. The constant `3` cannot be improved: at `B = α/(3+α)` the slack in the integral inequality is `-α⁵/540 + α⁶/648`, so the bound is tight to three orders at `α = 0`. ## The proof Differentiating, it suffices to prove `coth h - 1/h ≤ h/√(h²+9)`, which after clearing denominators is `G(h) := h⁴ sinh²h - (h²+9) (h cosh h - sinh h)² ≥ 0`. The informal write-up gets this from the Taylor expansion `G(h) = Σ_{k≥4} 2^{2k-3} (2k-1) (2k-6)² / (2k)! · h^{2k}`, all of whose coefficients are nonnegative. Formalizing an infinite series with nonnegative coefficients is unpleasant, and unnecessary. Setting `Φ(y) := e^{2y} P₁(y) - e^y P₂(y) - P₃(y)`, `P₁ = y³-10y²+36y-36`, `P₂ = y⁴+16y²-72`, `P₃ = y³+10y²+36y+36`, one has the algebraic identity `Φ(2h) = 16 e^{2h} G(h)`, so `G ≥ 0` iff `Φ ≥ 0` on `[0,∞)`. And `Φ` is *closed* under differentiation in the family `Sf u v w y = e^{2y} u(y) - e^y v(y) - w(y)`, `u` cubic, `v` quartic, `w` cubic, under `u ↦ 2u + u'`, `v ↦ v + v'`, `w ↦ w'`. Eight steps of that recurrence reach `Φ⁽⁸⁾(y) = 256 e^{2y} (y³+2y²-2y+10) - e^y (y⁴+32y³+352y²+1600y+2504)`, and `Φ⁽ʲ⁾(0) = 0` for `j ≤ 7`. So it is enough to prove `Φ⁽⁸⁾ ≥ 0` and integrate eight times. For `Φ⁽⁸⁾`, divide by `e^y` and use just three terms of the exponential series: what is left is `56 + 448 * y + 928 * y ^ 2 + 480 * y ^ 3 + 511 * y ^ 4 + 128 * y ^ 5`, every coefficient of which is positive. No certificate, no series manipulation — one `ring` identity and eight applications of "vanishes at `0` and has nonnegative derivative". ## Main statements * `Sendov.sinh_sq_le`: `(h²+9)(h cosh h - sinh h)² ≤ h⁴ sinh²h`; * `Sendov.log_sinh_div_le`: the displayed inequality; * `Sendov.sinh_le_mul_exp`: the form actually used, `sinh h ≤ h exp (√(h²+9) - 3)`. -/ namespace Sendov open Real Set Filter /-- `f` vanishes at `0` and has nonnegative derivative on `[0,∞)`, hence is nonnegative there. -/ private lemma nonneg_of_deriv {f g : ℝ → ℝ} (hd : ∀ z, HasDerivAt f (g z) z) (h0 : f 0 = 0) (hg : ∀ z, 0 ≤ z → 0 ≤ g z) {y : ℝ} (hy : 0 ≤ y) : 0 ≤ f y := by have hmono : MonotoneOn f (Ici 0) := by refine monotoneOn_of_deriv_nonneg (convex_Ici 0) (fun z _ => (hd z).continuousAt.continuousWithinAt) (fun z hz => (hd z).differentiableAt.differentiableWithinAt) (fun z hz => ?_) rw [(hd z).deriv] rw [interior_Ici] at hz exact hg z (le_of_lt hz) simpa [h0] using hmono (mem_Ici.2 le_rfl) (mem_Ici.2 hy) hy /-- `1 + y + y²/2 ≤ exp y` for `y ≥ 0`: three terms of the exponential series. -/ private lemma quad_le_exp {y : ℝ} (hy : 0 ≤ y) : 1 + y + y ^ 2 / 2 ≤ exp y := by suffices 0 ≤ exp y - 1 - y - y ^ 2 / 2 by linarith refine nonneg_of_deriv (f := fun t => exp t - 1 - t - t ^ 2 / 2) (g := fun t => exp t - 1 - t) (fun t => ?_) (by norm_num) (fun t ht => ?_) hy · exact ((((hasDerivAt_exp t).sub_const 1).sub (hasDerivAt_id' t)).sub ((hasDerivAt_pow 2 t).div_const 2)).congr_deriv (by norm_num) · linarith [add_one_le_exp t] /-- The family closed under differentiation: `e^{2y} u(y) - e^y v(y) - w(y)` with `u`, `w` cubic and `v` quartic. -/ private noncomputable def Sf (u₃ u₂ u₁ u₀ v₄ v₃ v₂ v₁ v₀ w₃ w₂ w₁ w₀ y : ℝ) : ℝ := exp (2 * y) * (u₃ * y ^ 3 + u₂ * y ^ 2 + u₁ * y + u₀) - exp y * (v₄ * y ^ 4 + v₃ * y ^ 3 + v₂ * y ^ 2 + v₁ * y + v₀) - (w₃ * y ^ 3 + w₂ * y ^ 2 + w₁ * y + w₀) private lemma hasDerivAt_Sf (u₃ u₂ u₁ u₀ v₄ v₃ v₂ v₁ v₀ w₃ w₂ w₁ w₀ y : ℝ) : HasDerivAt (fun t : ℝ => Sf u₃ u₂ u₁ u₀ v₄ v₃ v₂ v₁ v₀ w₃ w₂ w₁ w₀ t) (Sf (2 * u₃) (2 * u₂ + 3 * u₃) (2 * u₁ + 2 * u₂) (2 * u₀ + u₁) v₄ (v₃ + 4 * v₄) (v₂ + 3 * v₃) (v₁ + 2 * v₂) (v₀ + v₁) 0 (3 * w₃) (2 * w₂) w₁ y) y := by simp only [Sf] have he2 : HasDerivAt (fun t : ℝ => exp (2 * t)) (exp (2 * y) * 2) y := ((hasDerivAt_id' y).const_mul (2 : ℝ)).exp.congr_deriv (by ring) have he1 : HasDerivAt (fun t : ℝ => exp t) (exp y) y := hasDerivAt_exp y have hu : HasDerivAt (fun t : ℝ => u₃ * t ^ 3 + u₂ * t ^ 2 + u₁ * t + u₀) (3 * u₃ * y ^ 2 + 2 * u₂ * y + u₁) y := by have h := ((((hasDerivAt_pow 3 y).const_mul u₃).add ((hasDerivAt_pow 2 y).const_mul u₂)).add ((hasDerivAt_id' y).const_mul u₁)).add_const u₀ refine h.congr_deriv ?_ norm_num ring have hv : HasDerivAt (fun t : ℝ => v₄ * t ^ 4 + v₃ * t ^ 3 + v₂ * t ^ 2 + v₁ * t + v₀) (4 * v₄ * y ^ 3 + 3 * v₃ * y ^ 2 + 2 * v₂ * y + v₁) y := by have h := (((((hasDerivAt_pow 4 y).const_mul v₄).add ((hasDerivAt_pow 3 y).const_mul v₃)).add ((hasDerivAt_pow 2 y).const_mul v₂)).add ((hasDerivAt_id' y).const_mul v₁)).add_const v₀ refine h.congr_deriv ?_ norm_num ring have hw : HasDerivAt (fun t : ℝ => w₃ * t ^ 3 + w₂ * t ^ 2 + w₁ * t + w₀) (3 * w₃ * y ^ 2 + 2 * w₂ * y + w₁) y := by have h := ((((hasDerivAt_pow 3 y).const_mul w₃).add ((hasDerivAt_pow 2 y).const_mul w₂)).add ((hasDerivAt_id' y).const_mul w₁)).add_const w₀ refine h.congr_deriv ?_ norm_num ring exact (((he2.mul hu).sub (he1.mul hv)).sub hw).congr_deriv (by ring) /-- The base of the induction, `Φ⁽⁸⁾ ≥ 0`. Three terms of the exponential series leave a polynomial with every coefficient positive. -/ private lemma step8 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 256 512 (-512) 2560 1 32 352 1600 2504 0 0 0 0 y := by have : (1 + y + y ^ 2 / 2) * (256 * y ^ 3 + 512 * y ^ 2 - 512 * y + 2560) ≤ exp y * (256 * y ^ 3 + 512 * y ^ 2 - 512 * y + 2560) := by grw [quad_le_exp hy] nlinarith [sq_nonneg (y - 1), pow_nonneg hy 3, sq_nonneg y] have : (0 : ℝ) ≤ 56 + 448 * y + 928 * y ^ 2 + 480 * y ^ 3 + 511 * y ^ 4 + 128 * y ^ 5 := by nlinarith [pow_nonneg hy 5, pow_nonneg hy 4, pow_nonneg hy 3, sq_nonneg y, hy] have h3 : (0 : ℝ) ≤ exp y * (256 * y ^ 3 + 512 * y ^ 2 - 512 * y + 2560) - (2504 + 1600 * y + 352 * y ^ 2 + 32 * y ^ 3 + 1 * y ^ 4) := by nlinarith calc _ ≤ _ := mul_nonneg (exp_pos y).le h3 _ = _ := by simp only [Sf, two_mul, exp_add] ring private lemma step7 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 128 64 (-320) 1440 1 28 268 1064 1440 0 0 0 0 y := by refine nonneg_of_deriv (g := Sf 256 512 (-512) 2560 1 32 352 1600 2504 0 0 0 0) (fun z => ?_) ?_ step8 hy · exact (hasDerivAt_Sf 128 64 (-320) 1440 1 28 268 1064 1440 0 0 0 0 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step6 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 64 (-64) (-96) 768 1 24 196 672 768 0 0 0 0 y := by refine nonneg_of_deriv (g := Sf 128 64 (-320) 1440 1 28 268 1064 1440 0 0 0 0) (fun z => ?_) ?_ step7 hy · exact (hasDerivAt_Sf 64 (-64) (-96) 768 1 24 196 672 768 0 0 0 0 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step5 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 32 (-80) 32 368 1 20 136 400 368 0 0 0 0 y := by refine nonneg_of_deriv (g := Sf 64 (-64) (-96) 768 1 24 196 672 768 0 0 0 0) (fun z => ?_) ?_ step6 hy · exact (hasDerivAt_Sf 32 (-80) 32 368 1 20 136 400 368 0 0 0 0 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step4 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 16 (-64) 80 144 1 16 88 224 144 0 0 0 0 y := by refine nonneg_of_deriv (g := Sf 32 (-80) 32 368 1 20 136 400 368 0 0 0 0) (fun z => ?_) ?_ step5 hy · exact (hasDerivAt_Sf 16 (-64) 80 144 1 16 88 224 144 0 0 0 0 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step3 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 8 (-44) 84 30 1 12 52 120 24 0 0 0 6 y := by refine nonneg_of_deriv (g := Sf 16 (-64) 80 144 1 16 88 224 144 0 0 0 0) (fun z => ?_) ?_ step4 hy · exact (hasDerivAt_Sf 8 (-44) 84 30 1 12 52 120 24 0 0 0 6 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step2 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 4 (-28) 70 (-20) 1 8 28 64 (-40) 0 0 6 20 y := by refine nonneg_of_deriv (g := Sf 8 (-44) 84 30 1 12 52 120 24 0 0 0 6) (fun z => ?_) ?_ step3 hy · exact (hasDerivAt_Sf 4 (-28) 70 (-20) 1 8 28 64 (-40) 0 0 6 20 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step1 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 2 (-17) 52 (-36) 1 4 16 32 (-72) 0 3 20 36 y := by refine nonneg_of_deriv (g := Sf 4 (-28) 70 (-20) 1 8 28 64 (-40) 0 0 6 20) (fun z => ?_) ?_ step2 hy · exact (hasDerivAt_Sf 2 (-17) 52 (-36) 1 4 16 32 (-72) 0 3 20 36 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num private lemma step0 (y : ℝ) (hy : 0 ≤ y) : 0 ≤ Sf 1 (-10) 36 (-36) 1 0 16 0 (-72) 1 10 36 36 y := by refine nonneg_of_deriv (g := Sf 2 (-17) 52 (-36) 1 4 16 32 (-72) 0 3 20 36) (fun z => ?_) ?_ step1 hy · exact (hasDerivAt_Sf 1 (-10) 36 (-36) 1 0 16 0 (-72) 1 10 36 36 z).congr_deriv (by grind [Sf]) · simp only [Sf] norm_num /-- The algebraic bridge: `Φ(2h) = 16 e^{2h} G(h)`. -/ private lemma Sf_eq (h : ℝ) : Sf 1 (-10) 36 (-36) 1 0 16 0 (-72) 1 10 36 36 (2 * h) = 16 * exp h ^ 2 * (h ^ 4 * sinh h ^ 2 - (h ^ 2 + 9) * (h * cosh h - sinh h) ^ 2) := by have : exp h ≠ 0 := (exp_pos h).ne' have e4 : exp (2 * (2 * h)) = exp h ^ 4 := by simp [←exp_nat_mul]; ring have e2 : exp (2 * h) = exp h ^ 2 := by simp [←exp_nat_mul] simp only [Sf, sinh_eq, cosh_eq, e4, e2, exp_neg] field_simp ring /-- **The key inequality.** Equivalent to `coth h - 1/h ≤ h/√(h²+9)`. -/ theorem sinh_sq_le {h : ℝ} (hh : 0 ≤ h) : (h ^ 2 + 9) * (h * cosh h - sinh h) ^ 2 ≤ h ^ 4 * sinh h ^ 2 := by have h0 := step0 (2 * h) (by linarith) rw [Sf_eq] at h0 have : (0 : ℝ) < 16 * exp h ^ 2 := by positivity nlinarith /-- `sinh h ≤ h cosh h` for `h ≥ 0`; equivalently `h cosh h - sinh h ≥ 0`, which is what makes the square root below legitimate. -/ private lemma sinh_le_mul_cosh {h : ℝ} (hh : 0 ≤ h) : sinh h ≤ h * cosh h := by have : 0 ≤ h * cosh h - sinh h := by refine nonneg_of_deriv (f := fun t => t * cosh t - sinh t) (g := fun t => t * sinh t) (fun t => ?_) (by simp) (fun t ht => mul_nonneg ht (sinh_nonneg_iff.2 ht)) hh exact (((hasDerivAt_id' t).mul (hasDerivAt_cosh t)).sub (hasDerivAt_sinh t)).congr_deriv (by ring) linarith /-- `√(h²+9) (h cosh h - sinh h) ≤ h² sinh h`: the square root of `Sendov.sinh_sq_le`, which is the derivative inequality `coth h - 1/h ≤ h/√(h²+9)` cleared of denominators. -/ theorem sqrt_mul_sub_le {h : ℝ} (hh : 0 ≤ h) : sqrt (h ^ 2 + 9) * (h * cosh h - sinh h) ≤ h ^ 2 * sinh h := by have : (0 : ℝ) ≤ h ^ 2 * sinh h := mul_nonneg (sq_nonneg h) (sinh_nonneg_iff.2 hh) have : (0 : ℝ) ≤ sqrt (h ^ 2 + 9) * (h * cosh h - sinh h) := mul_nonneg (sqrt_nonneg _) (by linarith [sinh_le_mul_cosh hh]) have : (sqrt (h ^ 2 + 9) * (h * cosh h - sinh h)) ^ 2 ≤ (h ^ 2 * sinh h) ^ 2 := by convert sinh_sq_le hh · rw [mul_pow, sq_sqrt (by positivity)] · ring nlinarith /-- **The sharp bound.** This is `(lsh)` of the blog post. -/ theorem log_sinh_div_le {h : ℝ} (hh : 0 < h) : log (sinh h / h) ≤ sqrt (h ^ 2 + 9) - 3 := by set ψ : ℝ → ℝ := fun z => sqrt (z ^ 2 + 9) - 3 - (log (sinh z) - log z) with hψdef -- `ψ` has nonnegative derivative on `(0,∞)` have hderiv : ∀ z : ℝ, 0 < z → HasDerivAt ψ (z / sqrt (z ^ 2 + 9) - (cosh z / sinh z - 1 / z)) z := by intro z hz have hsinh : sinh z ≠ 0 := ne_of_gt (sinh_pos_iff.2 hz) apply HasDerivAt.sub · have h := (((hasDerivAt_pow 2 z).add_const 9).sqrt (ne_of_gt (by positivity))).sub_const 3 refine h.congr_deriv ?_ field_simp ring · exact (((hasDerivAt_sinh z).log hsinh).sub ((hasDerivAt_id' z).log (ne_of_gt hz))).congr_deriv (by field_simp) have hmono : MonotoneOn ψ (Ioi 0) := by refine monotoneOn_of_deriv_nonneg (convex_Ioi 0) (fun z hz => (hderiv z hz).continuousAt.continuousWithinAt) (fun z hz => (hderiv z (by rwa [interior_Ioi] at hz)).differentiableAt.differentiableWithinAt) (fun z hz => ?_) rw [interior_Ioi, mem_Ioi] at hz rw [(hderiv z hz).deriv, sub_nonneg, div_sub_div _ _ (ne_of_gt (sinh_pos_iff.2 hz)) (ne_of_gt hz), div_le_div_iff₀ (by positivity) (by positivity)] nlinarith [sqrt_mul_sub_le (le_of_lt hz)] -- `ψ → 0` as `z → 0⁺` have hslope : Tendsto (fun z => sinh z / z) (nhdsWithin 0 {(0 : ℝ)}ᶜ) (nhds 1) := by simpa [slope_fun_def, div_eq_inv_mul, hasDerivAt_iff_tendsto_slope] using hasDerivAt_sinh 0 have hlog : Tendsto ψ (nhdsWithin 0 (Ioi 0)) (nhds 0) := by have hsub : nhdsWithin (0 : ℝ) (Ioi 0) ≤ nhdsWithin 0 {(0 : ℝ)}ᶜ := nhdsWithin_mono _ (fun z hz => ne_of_gt hz) have h1 : Tendsto (fun z => log (sinh z / z)) (nhdsWithin 0 (Ioi 0)) (nhds 0) := by simpa [Function.comp_def] using (continuousAt_log one_ne_zero).tendsto.comp (hslope.mono_left hsub) have h2 : Tendsto (fun z : ℝ => sqrt (z ^ 2 + 9) - 3) (nhdsWithin 0 (Ioi 0)) (nhds 0) := by have h9 : sqrt (9 : ℝ) = 3 := by rw [show (9 : ℝ) = 3 ^ 2 by norm_num, sqrt_sq (by norm_num : (0:ℝ) ≤ 3)] have hc : ContinuousAt (fun z => sqrt (z ^ 2 + 9) - 3) 0 := by fun_prop simpa [ContinuousWithinAt, h9] using hc.continuousWithinAt (s := Ioi (0 : ℝ)) have heq : ∀ᶠ z : ℝ in nhdsWithin 0 (Ioi 0), ψ z = (sqrt (z ^ 2 + 9) - 3) - log (sinh z / z) := by filter_upwards [self_mem_nhdsWithin] with z hz rw [hψdef, log_div (ne_of_gt (sinh_pos_iff.2 hz)) (ne_of_gt hz)] simpa [tendsto_congr' heq] using h2.sub h1 -- combine have hev : ∀ᶠ z : ℝ in nhdsWithin 0 (Ioi 0), ψ z ≤ ψ h := by have hmem : Ioo (0 : ℝ) h ∈ nhdsWithin (0 : ℝ) (Ioi 0) := mem_nhdsGT_iff_exists_Ioo_subset.2 (Exists.intro h (And.intro (mem_Ioi.2 hh) subset_rfl)) filter_upwards [hmem] with z hz exact hmono (mem_Ioi.2 hz.1) (mem_Ioi.2 hh) (le_of_lt hz.2) have h0 : (0 : ℝ) ≤ ψ h := le_of_tendsto hlog hev have : (0 : ℝ) < sinh h / h := div_pos (sinh_pos_iff.2 hh) hh rw [hψdef] at h0 rw [log_div (ne_of_gt (sinh_pos_iff.2 hh)) (ne_of_gt hh)] linarith /-- The form in which the estimate is used: `sinh h ≤ h exp (√(h²+9) - 3)`. -/ theorem sinh_le_mul_exp {h : ℝ} (hh : 0 ≤ h) : sinh h ≤ h * exp (sqrt (h ^ 2 + 9) - 3) := by rcases eq_or_lt_of_le hh with rfl | hpos · simp · have hd : (0 : ℝ) < sinh h / h := div_pos (sinh_pos_iff.2 hpos) hpos grw [← (log_le_iff_le_exp hd).1 (log_sinh_div_le hpos)] field_simp simp end Sendov