Logarithm tangent bound (source code)

= Logarithm tangent bound
{title2=$\log u\leq u-1\quad(u>0)$}

For the natural <logarithm>, define $F(u)=u-1-\log u$. Its <derivative> is $1-1/u$, negative below one and positive above one. Thus its global minimum is $F(1)=0$, proving the bound, with equality only at one. Equivalently $\log(1+x)\leq x$ for $x>-1$; this also follows from <concavity> and the tangent line at one.