Unsolved Challenge: Natural logarithm and Exponent

[anemone]

Prove $e^{-x}\le \ln(e^x-x-\ln x)$ for $x>0$.

 

[Opalg]

Partial answer

Spoiler

Let $ x = x_0\approx 0.5671432$ be the point at which $e^{-x} = x$ (in terms of the Lambert function, $x_0 = W_0(1)$). Then $\ln x_0 = -x_0$, and so $\ln(e^{x_0} - x_0 - \ln x_0) = \ln(e^{x_0}) = x_0 = e^{-x_0}$. Thus at the point $x_0$ the two functions $e^{-x}$ and $\ln(e^x - x - \ln x)$ are equal.

Now let $f(x) = \ln(e^x - x - \ln x)$. Then $$f'(x) = \frac{e^x - 1 - \frac1x}{e^x - x - \ln x} = \frac{-1 + \bigl(e^x - \frac1x\bigr)}{e^x - (x+\ln x)}.$$ When $x = x_0$, both of the expressions in parentheses in that last fraction vanish. Therefore $f'(x_0) = \dfrac{-1}{e^{x_0}} = -e^{-x_0}$, which is the same as the derivative of $e^{-x}$ at $x_0$.

When $x>x_0$, $e^x - \frac1x$ and $x + \ln x$ are both positive. So in the expression for $f'(x)$ the numerator is greater than $-1$ and the denominator is less than $e^x$, and so $f'(x) > -e^{-x}$. Conversely, when $x<x_0$, $e^x - \frac1x$ and $x + \ln x$ are both negative and so $f'(x) < -e^{-x}$. It follows that $x_0$ is a local minimum for the function $f(x) - e^{-x}$. Therefore $\ln(e^x - x - \ln x) \geqslant e^{-x}$ in the neighbourhood of $x_0$.

Once you get away from the neighbourhood of $x_0$ it ought to be relatively easy to see that $\ln(e^x - x - \ln x)$ is greater than $e^{-x}$, but I don't have the patience or energy to pursue that part of the problem.