Coleman interpolation theorem for cyclotomic local units (source code)

= Coleman interpolation theorem for cyclotomic local units
{c}
{title2=$f_u(\zeta_n-1)=u_n,\quad Nf_u=f_u$}

For odd $p$ and a <norm-compatible sequence of local units> in $\mathbb Q_p(\mu_{p^{n+1}})$, there is a unique $f_u\in\mathbb Z_p[[T]]^\times$ interpolating all its entries, and the <Coleman norm operator> fixes it. To construct it, choose integral unit polynomials $F_j$ interpolating entry $u_j$, and take a convergent subsequence of $N^jF_{2j}$ in the compact $(p,T)$-adic unit space. The congruence $NF\equiv F\pmod p$ and <Coleman norm contraction> show that its evaluation at any fixed level tends to the desired entry. Uniqueness follows from the <Weierstrass preparation theorem>: a nonzero integral power series has only finitely many zeros in the open unit disk. The norm relation on evaluations then proves norm fixation. Principal units correspond to $f_u(0)\equiv1\pmod p$.