English
There is an isometric equivalence between the space of continuous functions C(ℤ_p,E) and the space of sequences C_0(ℕ,E), given by f ↦ (Δ^n f(0))_n.
Русский
Существует изометрическое эквивалентное отображение между пространством непрерывных функций и последовательностей: f ↦ (Δ^n f(0))_n.
LaTeX
$$$$ mahlerEquiv: C(\\mathbb{Z}_p,E) \\cong_{\\text{iso}} C_0(\\mathbb{N},E). $$$$
Lean4
/-- **Mahler's theorem**: for any continuous function `f` from `ℤ_[p]` to a `p`-adic Banach space, the
Mahler series with coefficients `n ↦ Δ_[1]^[n] f 0` converges to the original function `f`.
-/
theorem hasSum_mahler (f : C(ℤ_[p], E)) : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] f 0) n) f := by
-- First show `∑' n, mahlerTerm f n` converges to *something*.
have : HasSum (fun n ↦ mahlerTerm (Δ_[1]^[n] f 0) n) (mahlerSeries (Δ_[1]^[·] f 0) : C(ℤ_[p], E)) :=
hasSum_mahlerSeries
(fwdDiff_tendsto_zero f)
-- Now show that the sum of the Mahler terms must equal `f` on a dense set, so it is actually `f`.
convert this using 1
refine
ContinuousMap.coe_injective (denseRange_natCast.equalizer (map_continuous f) (map_continuous _) (funext fun n ↦ ?_))
simpa [mahlerSeries_apply_nat (fwdDiff_tendsto_zero f) le_rfl] using shift_eq_sum_fwdDiff_iter 1 f n 0
