Weighted group algebra of a uniform pro-p group (source code)

= Weighted group algebra of a uniform pro-p group
{title2=$v(\sum_\alpha c_\alpha b^\alpha)=\inf_\alpha(v_p(c_\alpha)+s|\alpha|)$}

Choose ordered minimal <topological generators> $a_1,\ldots,a_d$ of a <uniform pro-p group> for odd $p$, put $b_i=a_i-1$, and choose $1/(p-1)<s<1$. Ordered monomials $b^\alpha=b_1^{\alpha_1}\cdots b_d^{\alpha_d}$ give power-series coordinates in the integral <completed group algebra>. The displayed <Non-Archimedean absolute value> filtration gives a complete normed $\mathbb Q_p$-algebra after completion of the rational <group algebra>. The power relation raises valuation by one, and interchanging $b_i,b_j$ adds terms of valuation at least $1+s>2s$, so multiplication does not decrease total valuation. The <p-adic logarithm> and <p-adic exponential> are inverse on the relevant small balls. In particular $\log G$ is a faithful realization of the <Lie algebra of a uniform pro-p group>, useful for verifying its intrinsic limit operations and the <Baker--Campbell--Hausdorff formula> without assuming the correspondence in advance.