English
Let p be a prime and R a normed ring equipped with a compatible Z_p-algebra structure. For any r in R such that r^n → 0 as n → ∞, there exists a unique continuous additive character χ: Z_p → R with χ(1) = 1 + r, and χ is given by the Mahler series mahlerSeries(r^·).
Русский
Пусть p — простое число и R — нормированное кольцо с совместной структурой над Z_p. Для любого r ∈ R такой что r^n → 0 при n → ∞ существует единственный непрерывный аддитивный символ χ: Z_p → R с χ(1) = 1 + r, причём χ задаётся через ряд Махлера mahlerSeries(r^·).
LaTeX
$$$$\exists! \chi \in \mathrm{AddChar}(\mathbb{Z}_p,R)\;\text{с непрерывностью},\; \chi(1)=1+r\;\text{и}\; \chi=\operatorname{mahlerSeries}(r^{\cdot}).$$$$
Lean4
/-- The unique continuous additive character of `ℤ_[p]` mapping `1` to `1 + r`. -/
noncomputable def addChar_of_value_at_one (r : R) (hr : Tendsto (r ^ ·) atTop (𝓝 0)) : AddChar ℤ_[p] R
where
toFun := mahlerSeries (r ^ ·)
map_zero_eq_one' := by
rw [← Nat.cast_zero, mahlerSeries_apply_nat hr le_rfl, zero_add, Finset.sum_range_one, Nat.choose_self, pow_zero,
one_smul]
map_add_eq_mul' a
b := by
let F : C(ℤ_[p], R) := mahlerSeries (r ^ ·)
change F (a + b) = F a * F b
have hF (n : ℕ) : F n = (r + 1) ^ n :=
by
rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]
refine Finset.sum_congr rfl fun i hi ↦ ?_
rw [one_pow, mul_one, nsmul_eq_mul, Nat.cast_comm]
refine
congr_fun
((denseRange_natCast.prodMap denseRange_natCast).equalizer ((map_continuous F).comp continuous_add)
(continuous_mul.comp (map_continuous <| F.prodMap F)) (funext fun ⟨m, n⟩ ↦ ?_))
(a, b)
simp [← Nat.cast_add, hF, ContinuousMap.prodMap_apply, pow_add]
