$1/y -\log y = x $, asymptotically

Question

I'm interested in the asymptotic expansion for $x \rightarrow +\infty$ of the solution to

$$ \frac{1}{y} - \log y = x $$

Is the leading term simply $y \sim 1/x$? How to show that rigorously? How to estimate the remainder?

This is what I tried: I thought of solving the equation iteratively, neglecting the second term in the first approximation, then plugging the solution back into it. This gives increasingly good approximations $y_0$, $y_1$, $\ldots$ such as

$$ \frac{1}{y_0} = x $$

$$ y_1 = \frac{1}{ x - \log x}$$

Is this method justified? Are these approximations really increasingly good? Do they form an asymptotic series in a strict sense?

An answer to any of these questions would be welcome.

Answer 1

Given that $1/y$ grows much faster than $\ln y$ as $y$ approaches zero, the term $y=1/x $ dominants. The asymptotic solution can then be written as

$$y = \frac{1}{x}(1+\Delta)\tag{1}$$

where $\Delta$ is the next-order correction term. Plug (1) into $$ \frac{1}{y} - \log y = x $$

to get

$$\frac{x}{1+\Delta} -\ln\frac 1x -\ln(1+\Delta)=x$$

Then, $\Delta$ is approximated as

$$\Delta \approx -\frac 1x \ln \frac 1x$$

Therefore, the asymptotic solution is

$$ y = \frac 1x \left( 1-\frac 1x \ln \frac 1x \right)$$

Answer 2

Let $z=\frac 1y$ to face $$z+\log(z)=x \implies z e^z=e^x\implies z=W(e^x)\implies y=\frac 1{W(e^x)}$$ where appears Lambert function.

Using the asymptotics of $W(t)$ given in the linked Wikipedia page for large values of $t$

$$z=x-\log(x)+\cdots\implies y \sim \frac 1 {x-\log(x)}\sim \frac 1 x \left(1+\frac{\log(x)} x\right)$$