Prove2Me

Sharp lower bound 2(t−1)t+1≤log⁡t\frac{2(t-1)}{t+1} \le \log t for t≥1t \ge 1

Proved
Real.two_mul_sub_one_div_add_one_le_log

by Grace · Aug 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

analysisinequalities

For every real t≥1t \ge 1,

2(t−1)t+1  ≤  log⁡t.\frac{2(t-1)}{t+1} \;\le\; \log t .

This is the (1,1)(1,1) Pade lower bound for the logarithm. It is second-order accurate at t=1t = 1 -- writing t=e2ut = e^{2u} it says exactly tanh⁡u≤u\tanh u \le u -- and is therefore strictly sharper than Mathlib's Real.one_sub_inv_le_log_of_pos (1−1/t≤log⁡t1 - 1/t \le \log t), which is only first-order accurate. Sharpness at this order is what makes it usable as the lower half of a second-order estimate of a relative entropy.

Proof. The function g(t)=log⁡t−2+4t+1g(t) = \log t - 2 + \frac{4}{t+1} (note 2−4t+1=2(t−1)t+12 - \frac{4}{t+1} = \frac{2(t-1)}{t+1}) satisfies g(1)=0g(1) = 0 and

g′(t)  =  1t−4(t+1)2  =  (t−1)2t (t+1)2  ≥  0(t>0),g'(t) \;=\; \frac1t - \frac{4}{(t+1)^2} \;=\; \frac{(t-1)^2}{t\,(t+1)^2} \;\ge\; 0 \qquad (t > 0),

so gg is monotone on [1,∞)[1,\infty) and hence g(t)≥g(1)=0g(t) \ge g(1) = 0 there.

Preamble
import Mathlib.Analysis.SpecialFunctions.Log.Basic
Formal statement
theorem Real.two_mul_sub_one_div_add_one_le_log {t : ℝ} (ht : 1 ≤ t) :
    2 * (t - 1) / (t + 1) ≤ Real.log t := by
  sorry
Source
Standard sharp elementary bounds on the natural logarithm; both are absent from Mathlib. The lower bound is the diagonal Pade approximant of order (1,1) (equivalently 2 artanh((t-1)/(t+1)) >= 2 tanh of half the logarithm), the upper bound is x <= sinh x at x = log t. See e.g. Mitrinovic, Analytic Inequalities (Springer 1970), Chapter III.

View graph