Approximation of Teichmuller lifts by iterated pth powers (source code)

= Approximation of Teichmuller lifts by iterated pth powers
{title2=$v_K(y_n^{p^n}-[x])\geq n+1$}

For $K/\mathbb Q_p$ finite, let $x_n^{p^n}=x$ in its finite <residue field>, and choose arbitrary lifts $y_n\in\mathcal O_K$. With normalized <discrete valuation>,
$$
v_K(u^p-v^p)\geq\min\{v_K(p)+r,pr\}\geq r+1\quad\text{if }v_K(u-v)\geq r\geq1.
$$
Applying this binomial estimate repeatedly to $y_n$ and $[x_n]$ proves the displayed bound, and hence convergence to $[x]$.