English
For any f ∈ C(ℤ_p,E), mahlerEquiv E f equals the sequence of forward differences Δ^n f(0).
Русский
Для любого f ∈ C(ℤ_p,E), mahlerEquiv E f совпадает с последовательностью forward-разностей Δ^n f(0).
LaTeX
$$$$ mahlerEquiv E f = (Δ^{n} f(0))_{n\\in \\mathbb{N}}. $$$$
Lean4
/-- The isometric equivalence from `C(ℤ_[p], E)` to the space of sequences in `E` tending to `0` given
by Mahler's theorem, for `E` a nonarchimedean `ℚ_[p]`-Banach space.
-/
noncomputable def mahlerEquiv : C(ℤ_[p], E) ≃ₗᵢ[ℤ_[p]] C₀(ℕ, E)
where
toFun f := ⟨⟨(Δ_[1]^[·] f 0), continuous_of_discreteTopology⟩, cocompact_eq_atTop (α := ℕ) ▸ fwdDiff_tendsto_zero f⟩
invFun a := mahlerSeries a
map_add' f
g := by
ext x
simp only [ContinuousMap.coe_add, fwdDiff_iter_add, Pi.add_apply, ZeroAtInftyContinuousMap.coe_mk,
ZeroAtInftyContinuousMap.coe_add]
map_smul' r
f := by
ext n
simp only [ContinuousMap.coe_smul, RingHom.id_apply, ZeroAtInftyContinuousMap.coe_mk,
ZeroAtInftyContinuousMap.coe_smul, Pi.smul_apply, fwdDiff_iter_const_smul]
left_inv f := (hasSum_mahler f).tsum_eq
right_inv a := ZeroAtInftyContinuousMap.ext <| fwdDiff_mahlerSeries (cocompact_eq_atTop (α := ℕ) ▸ zero_at_infty a)
norm_map'
f := by
simp only [LinearEquiv.coe_mk, ← ZeroAtInftyContinuousMap.norm_toBCF_eq_norm]
apply le_antisymm
· exact BoundedContinuousFunction.norm_le_of_nonempty.mpr (fun n ↦ norm_fwdDiff_iter_apply_le 1 f 0 n)
· rw [← (hasSum_mahler f).tsum_eq]
refine (norm_tsum_le _).trans (ciSup_le fun n ↦ ?_)
refine le_trans (le_of_eq ?_) (BoundedContinuousFunction.norm_coe_le_norm _ n)
simp [(hasSum_mahler f).tsum_eq]
