When $x\to\infty$, $\liminf w'(x) \geq w'(x_2) - y'(x_2) > 0$, which contradicts the boundedness of $w$.

This lemma is used to prove a bound on the Laguerre functions.

\[lemm:estimeLaguerre\] For all $m, n \in {\mathbb{N}}$ and $s {\mathrel{\mathop:} = }\sqrt{m+n+1}$, for all $z \geq 0$, $$l_{m,n}(z) \leq \frac1\pi\left\{ \begin{array}{ll}
                                 1 &{\rm \ if \ } 0 \leq z \leq s \\
                                 e^{-(z-s)^2} &{\rm \ if \ } z \geq s.
                                       \end{array} 
                               \right. 
        \label{eq:estimeLaguerre}$$

When $z \leq s$, the result follows from the uniform bound on Wigner functions obtained by applying the Cauchy-Schwarz inequality to (\[eq:1\]).

When $z \geq s$, $L_{n}^\alpha(2z^2)$ doesn’t vanish and keeps the same sign as $L_{n}^\alpha(2s^2)$. Now, as it can be seen from [@Szego:1959uq 5.1.2], the function $w(z) {\mathrel{\mathop:} = }\sqrt{z}{l_{m,n}(z)}$ satisfies the differential equation $w''=(4(z^2-s^2)+\frac{\alpha^2-1/4}{z^2})z$. On the other hand, $y(z) {\mathrel{\mathop:} = }\sqrt{s} {l_{m,n}(s)} e^{-(z-s)^2}$ satisfies $y'' =
    (4(z-s)^2-2) y$. When $z \geq s$, $$4(z-s)^2-2 < 4(z^2-s^2) + \frac{\alpha^2-1/4}{z^2}$$ from which we conclude with Lemma \[lemm:ineqdiff\] that $w(z)
    \leq y(z)$.

Finally, a lemma to bound the tail of a series.

\[lemm:magicjohnson\] If $\nu > 0$ and $C > 0$, there exists a $z_{0}$ such that $z \geq
    z_{0}$ implies $$\sum_{m+n \geq z} e^{-C (m+n)^{\nu}} \leq \frac{2 