English
For any f ∈ C(ℤ_p,E) the Mahler series has sum equal to mahlerSeries f under the appropriate conditions (norms, ultrametric), i.e., the series converges to f.
Русский
Для любого f ∈ C(ℤ_p,E) ряд Маhler имеет предел, равный f (при заданных условиях норм и ультраметричности).
LaTeX
$$$$ \\text{hasSum}_{mahler}(f) \\Rightarrow \\text{sum of } mahlerTerm(Δ^n f(0),n) = f. $$$$
Lean4
/-- The coefficients of a Mahler series can be recovered from the sum by taking forward differences at
`0`.
-/
theorem fwdDiff_mahlerSeries (ha : Tendsto a atTop (𝓝 0)) (n) : Δ_[1]^[n] (mahlerSeries a) (0 : ℤ_[p]) = a n :=
calc
Δ_[1]^[n] (mahlerSeries a)
0
-- throw away terms after the nth
_ = Δ_[1]^[n] (fun k ↦ ∑ j ∈ range (n + 1), k.choose j • (a j)) 0 :=
by
simp only [fwdDiff_iter_eq_sum_shift, zero_add]
refine Finset.sum_congr rfl fun j hj ↦ ?_
rw [nsmul_one, nsmul_one, mahlerSeries_apply_nat ha (Nat.lt_succ.mp <| Finset.mem_range.mp hj), Nat.cast_id]
-- bring `Δ_[1]` inside sum
_ = ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k ↦ k.choose j • (a j)) 0 :=
by
simp only [fwdDiff_iter_eq_sum_shift, smul_sum]
rw [sum_comm]
-- bring `Δ_[1]` inside scalar-mult
_ = ∑ j ∈ range (n + 1), (Δ_[1]^[n] (fun k ↦ k.choose j : ℕ → ℤ) 0) • (a j) := by
simp only [fwdDiff_iter_eq_sum_shift, zero_add, sum_smul, smul_assoc, natCast_zsmul]
-- finish using `fwdDiff_iter_choose_zero`
_ = a n := by
simp only [fwdDiff_iter_choose_zero, ite_smul, one_smul, zero_smul, sum_ite_eq, Finset.mem_range,
lt_add_iff_pos_right, zero_lt_one, ↓reduceIte]
