Rational lower bound for the natural logarithm (source code)

= Rational lower bound for the natural logarithm
{title2=$\ln(1+t)>2t/(2+t)\quad(t>0)$}

For $t>0$, the <natural logarithm> satisfies
$$
\boxed{\ln(1+t)>\frac{2t}{2+t}.}
$$
To prove it, put $h(t)=\ln(1+t)-2t/(2+t)$. Then $h(0)=0$ and the <derivative> is $h'(t)=t^2/[(1+t)(2+t)^2]>0$. More precisely,
$$
h(t)=\int_0^t\frac{s^2}{(1+s)(2+s)^2}\,ds.
$$
This positive <integral> controls errors in symmetric approximations to the <logarithm>. After writing $x=1+t$, the bound is $\ln x>2(x-1)/(x+1)$ for $x>1$; the inequality reverses for $0<x<1$ by replacing $x$ with $1/x$.