Inverting a function: proof of $W(x) = \ln\frac{x}{\ln\frac{x}{\ddots}}$

Context : This reference contains your continued fraction expansions of Lambert's $W$ function. It is valid in the complex domain under the condition $|W(w)|>1$ ; one finds there another one, with $\exp$ instead of $\log$, valid for $|W(w)|<1$ (see below). See also the answer by Robert Israel there.

In the following, I will restrict my attention to real values of variable $w$.

Let us first rewrite your formula under the following form for real positive values of $w$ :

A) If $w>e : a_{n+1}=\ln(\frac{w}{\ a_{n}})$ with for example $a_0=2$ has a limit $L=W(w)$.

knowing that you have to switch to another function in the other case :

B) If $w<e : b_{n+1}=\exp(\frac{w}{\ b_{n}})$ with for example $b_0=2$ has a limit $L$ s.t. $W(w)=\dfrac{w}{L}$.

Special case :

If $w=e$,... $W(w)=1$.

(the resp. convergences of $a_n$ and $b_n$ are very slow when $w$ is close to $e$)

Fig. 1 : This picture features two different things : 1) The principal branch of Lambert function $W$, which is defined as the inverse of function $y=xe^{x}$ on the region where the latter is increasing ; 2) an example of "cobweb convergence" (in case A)) to a limit $L=W(w)$ of iterative sequence $u_{n+1}=f(u_n)$ where $f(x)=\ln(w/x)=ln(x)-ln(w)$ (in the case $w=4$ and $u_0=2$).

Remarks :

1. This cobweb convergence is convincing graphically ; but we must "guarantee" that it exists. This is due to the fact that $f'(L)=-1/L=-1/W(w) \approx -0.8$ with absolute value $<1$ warranting cobweb convergence, a classical consequence of Mean Value Theorem). But it remains, using MVT, to prove convergence in a rigorous way using a narrow enough interval around the limit.

2. Connection of the continued fraction (under the restriction that the notations make sense... as @fedja has remarked) with Lambert function : $$W(x)=\ln\dfrac{x}{W(x)} \iff \exp(W(x)) = \dfrac{x}{W(x)}$$

(by taking $\exp$ on both sides), itself equivalent to the definition of (the principal branch of) Lambert $W$ function. $$W(x)\exp(W(x))=x.$$

3. Good numerical methods about Lambert function can be found here.

A simple proof by recursive definition: $$ f(x)=\ln\cfrac{x}{\ln\cfrac{x}{\ln\cfrac{x}{\ddots}}}\\ f(x)=\ln\frac{x}{f(x)}\\ e^{f(x)}=\frac{x}{f(x)}\\ f(x)e^{f(x)}=x\\ f(x)=W(x) $$