Truncated Teichmüller expansion of a Witt vector

Let $p$ be a prime, let $B$ be a commutative ring, let $w$ be a Witt vector in $W(B) =$ WittVector p B, and let $N$ be a natural number. The assertion is that there exists a Witt vector $w' \in W(B)$ with

where the sum is over $n$ in Finset.range N, $w_n$ denotes the $n$-th Witt coefficient w.coeff n, $[\,a\,]$ denotes the Teichmüller element WittVector.teichmuller p a of $W(B)$, and $V^{n}$ means the $n$-fold iterate of the underlying function of the Verschiebung additive map WittVector.verschiebung : WittVector p B →+ WittVector p B. Both the addition and the finite sum are those of the Witt vector ring $W(B)$. No hypothesis beyond commutativity of $B$ is imposed: in particular $B$ need not be of characteristic $p$, nor torsion-free, nor $p$-adically complete, and the statement is purely existential, giving no formula for $w'$ (the witness produced is the $N$-fold shift of $w$).

This is the truncated Teichmüller (digit) expansion of a Witt vector, the basic device for writing an element of $W(B)$ as a finite sum of Verschiebungs of Teichmüller representatives modulo the image of $V^{N}$. It is used in the work on formal $\mathcal{O}_D$-modules in the Cerednik–Drinfeld part of the development, where endomorphisms are analysed through their effect on such expansions.