Sharp upper bound $\log t \le \tfrac12\left(t - \tfrac1t\right)$ for $t \ge 1$

Proved

Real.log_le_sub_inv_div_two

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

analysisinequalities

For every real $t \ge 1$ ,

\log t \;\le\; \frac{1}{2}\left(t - \frac{1}{t}\right).

The right-hand side is the average of Mathlib's two first-order bounds $\log t \le t - 1$ and $\log t \ge 1 - 1/t$ , and unlike either of them it is second-order accurate at $t = 1$ ; it is exactly the statement $x \le \sinh x$ for $x \ge 0$ .

Proof. Put $x = \log t \ge 0$ . Then $\sinh x = \tfrac12(e^x - e^{-x}) = \tfrac12\bigl(t - t^{-1}\bigr)$ , and $x \le \sinh x$ for $x \ge 0$ .

Preamble

import Mathlib.Analysis.SpecialFunctions.Log.Basic

Formal statement

theorem Real.log_le_sub_inv_div_two {t : ℝ} (ht : 1 ≤ t) :
    Real.log t ≤ (t - 1 / t) / 2 := 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

Sharp upper bound log⁡t≤12(t−1t)\log t \le \tfrac12\left(t - \tfrac1t\right)logt≤21​(t−t1​) for t≥1t \ge 1t≥1

Sharp upper bound $\log t \le \tfrac12\left(t - \tfrac1t\right)$ for $t \ge 1$