The exponential series of $m \log_p x$ converges to $x^m$ on the ball $\|x - 1\| \le \|p\|^2$

Let $p$ be a prime and let $K$ be a complete ultrametric field of characteristic zero with $\|p\| < 1$. Let $x \in K$ with $\|x - 1\| \le \|p\|^2$ and let $m \ge 0$ be an integer. Then the exponential series of $m \log_p x$ converges and

Proof idea. Write $y = \log_p x$; then $\|y\| = \|x - 1\| \le \|p\|^2$. Since $\|k!\| \ge \|p\|^{k-1}$ for $k \ge 1$, the terms $y^k / k!$ have norm at most $\|p\|^{k+1}$, so the series $E(y)$ converges, and $\|E(y) - 1\| \le \|p\|^2$. The Cauchy product gives $E(y_1 + y_2) = E(y_1) E(y_2)$. From $E(y)^{p^n} = E(p^n y)$ and the estimate $\|E(t) - 1 - t\| \le \|t\|^2 / \|p\|$ it follows that $(E(y)^{p^n} - 1)/p^n \to y$, so $\log_p E(y) = y$. Then $\log_p E(\log_p x) = \log_p x$ and the injectivity of $\log_p$ on the ball gives $E(\log_p x) = x$. The case of general $m$ follows from $\log_p (x^m) = m \log_p x$.

Use. For $x$ in the ball, the function $z \mapsto x^z$ on the integers is the restriction of the power series $\sum_k (\log_p x)^k z^k / k!$. This makes the auxiliary function of Baker's method a restricted power series, to which the $p$-adic Schwarz lemma (IsUltrametricDist.norm_tsum_mul_pow_le_of_hasseDeriv_eq_zero) applies. It is a tool for NumberField.Brumer.extrapolation_step.

Formalization Note. $\log_p$ is PadicLog.log (p := p) of Definitions.Def_PadicLog, defined by Iwasawa's limit $\lim_n (x^{p^n} - 1)/p^n$ and not by a power series; the platform has no $p$-adic exponential. The statement is a HasSum. The norm of $K$ is not normalized; only $\|p\| < 1$ is used. Relevant platform lemmas: PadicLog.norm_log, PadicLog.log_pow, PadicLog.log_injOn, PadicLog.tendsto_logSeq.