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).