Bound for function involving Lambert W Given that $W(x)$ is the Lambert W function, how can one prove that 
$$(2+W(x))e^{-W(x)}\leq 2 \frac{\log^2 x}{x}, \quad x\geq e^2$$
Is it possible to generalize this and find a function $f(x)$ such that 
$$
4\left(1+W(\sqrt{x}/2)\right)^2e^{-2W(\sqrt{x}/2)}\leq f(x)
$$
 A: Since $ W(x)\,e^{W(x)}=x $ the first inequality is equivalent to:
$$\forall x\geq e^2,\quad W(x)( W(x)+2) \leq 2\log^2 x \tag{1} $$
or to:
$$\forall x\geq e^2,\quad W(x) \leq -1+\sqrt{1+2\log^2 x}\tag{2} $$
or to:
$$\forall x\geq e^2,\quad x\leq \left(-1+\sqrt{1+2\log^2 x}\right)\exp\left(-1+\sqrt{1+2\log^2 x}\right)\tag{3} $$
that follows from:
$$ \forall x\geq e^2,\quad x\leq \frac{2}{e}\,\exp\left(\sqrt{1+2\log^2 x}\right) \tag{4}$$
that follows from:
$$ \forall x\geq e^2, \sqrt{1+2\log^2 x}\geq \sqrt{2}\log x.\tag{5} $$
In general, $W(x)$ can be well-approximated by using Newton's method for solving $y e^y=x$, by taking $y_0=\log x$, for instance. By using a fixed-point iteration, instead, we get:
$$ W(x)\approx \log x-\log\left(\log x-\log\log x\right).\tag{6}$$
A: About the first question, here it is proved that, for $x>e
 $,$$\log\left(x\right)-\log\left(\log\left(x\right)\right)<W\left(x\right)<\log\left(x\right)-\frac{1}{2}\log\left(\log\left(x\right)\right)
 $$ so we have $$\left(2+W\left(x\right)\right)e^{-W\left(x\right)}=2e^{-W\left(x\right)}+xe^{-2W\left(x\right)}\leq\frac{2\log\left(x\right)}{x}+\frac{\log^{2}\left(x\right)}{x}.
 $$About the second question, we have $$ 4\left(1+W\left(\sqrt{x}/2\right)\right)^{2}e^{-2W\left(\sqrt{x}/2\right)}=4\left(e^{-W\left(\sqrt{x}/2\right)}+\frac{\sqrt{x}}{2}e^{-2W\left(\sqrt{x}/2\right)}\right)^{2}
 $$and so, if $x>4e^{2}
 $, $$\leq4\left(\frac{2\log\left(\sqrt{x}/2\right)}{\sqrt{x}}+\frac{2\log^{2}\left(\sqrt{x}/2\right)}{\sqrt{x}}\right)^{2}.
 $$
