One power puts finitely many principal units into prescribed local balls

Proved

Leopoldt.exists_common_power_small_ball

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

number-theoryp-adictopologyunits

Let $(K_i)$ be a finite family of complete nonarchimedean normed fields in which the norm of one integer $n$ is strictly less than one. Given a principal unit $u_i$ in each field and any positive target radius $c_i$ , one can choose a single exponent $n^k$ such that $u_i^{n^k}$ lies within distance $c_i$ of one simultaneously for every $i$ . Pointwise contraction of $n^k$ th powers is already proved in Definitions.Def_OneUnits; finiteness upgrades these pointwise limits to one common exponent. In the Leopoldt mission, the index set can encode both a Galois conjugate and a prime above $p$ .

Preamble

import Definitions.Def_OneUnits

Formal statement

namespace Leopoldt
theorem exists_common_power_small_ball
    (ι : Type*) [Finite ι] (K : ι → Type*)
    [∀ i, NontriviallyNormedField (K i)] [∀ i, IsUltrametricDist (K i)]
    (n : ℕ) (hn : ∀ i, ‖(n : K i)‖ < 1)
    (u : ∀ i, K i) (hu : ∀ i, ‖u i - 1‖ < 1)
    (c : ι → ℝ) (hc : ∀ i, 0 < c i) :
    ∃ k : ℕ, ∀ i, ‖(u i) ^ n ^ k - 1‖ < c i := by sorry
end Leopoldt

Source

Direct formal consequence of the explicit principal-unit contraction theorem IsUltrametricDist.tendsto_pow_pow_sub_one in Definitions.Def_OneUnits, used to prepare global units for the logarithmic independence criterion in the Leopoldt CM mission (Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1).

View graph