Iwasawa's limit defining the $p$ -adic logarithm converges on all principal units

Proved

PadicLog.tendsto_logSeq_of_norm_sub_one_lt_one

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

leopoldtnumber-theoryp-adic

Let $K$ be a complete non-archimedean field of characteristic $0$ whose residue characteristic is $p$ , i.e. $\|p\|<1$ . For every principal unit $x\in K$ , that is every $x$ with $\|x-1\|<1$ , the sequence

\frac{x^{p^n}-1}{p^n}\qquad(n=0,1,2,\dots)

converges in $K$ , and its limit is the $p$ -adic logarithm $\log_p x$ .

Thus the limit-form logarithm is well defined on the whole group $U^{(1)}=1+\mathfrak m$ of principal units, not only on the small ball $\|x-1\|\le\|p\|^2$ where its basic properties were first established; this is the starting point for using $\log_p$ on all local and semilocal principal units.

Formalization Note Here $K$ is any complete, nontrivially normed, ultrametric field of characteristic zero with $\|p\|<1$ (e.g. a finite extension of $\mathbb{Q}_p$ , or a completion $K_{\mathfrak p}$ of a number field at $\mathfrak p\mid p$ ). PadicLog.log is the platform definition from Definitions.Def_PadicLog: $\log x=\lim_{n}(x^{p^n}-1)/p^n$ (a limUnder), previously only studied on the ball $\|x-1\|\le\|p\|^2$ ; PadicLog.logSeq x n $=(x^{p^n}-1)/p^n$ .

Preamble

import Definitions.Def_PadicLog

Formal statement

namespace PadicLog

theorem tendsto_logSeq_of_norm_sub_one_lt_one {p : ℕ} [Fact p.Prime] {K : Type*}
    [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    [Fact (‖((p : ℕ) : K)‖ < 1)] [CharZero K] {x : K} (hx : ‖x - 1‖ < 1) :
    Filter.Tendsto (logSeq (p := p) x) Filter.atTop (nhds (log (p := p) x)) := by sorry

end PadicLog

Source

Washington, Introduction to Cyclotomic Fields (2nd ed., GTM 83), §5.1, Proposition 5.4 (the p-adic logarithm log_p on 1+pO extended to units; log_p(xy)=log_p x+log_p y; log_p x=0 iff x is a root of unity times a power of p) and Neukirch, Algebraic Number Theory, Ch. II, Prop. (5.4)–(5.5) (the logarithm on principal units U^(1), log x = lim (x^{p^n}-1)/p^n style extension). Iwasawa's limit form: Iwasawa, Lectures on p-adic L-functions, §2.

View graph

Iwasawa's limit defining the ppp-adic logarithm converges on all principal units

Iwasawa's limit defining the $p$ -adic logarithm converges on all principal units