English
For k,n ∈ ℕ, mahler k (n) = binomial(n,k).
Русский
Для k,n ∈ ℕ верно mahler(k,n) = {n \\choose k}.
LaTeX
$$$$ mahler(k,n) = {n \\choose k}, \\quad k,n \\in \\mathbb{N}. $$$$
Lean4
/-- The value of a Mahler series at a natural number `n` is given by the finite sum of the first `m`
terms, for any `n ≤ m`.
-/
theorem mahlerSeries_apply_nat (ha : Tendsto a atTop (𝓝 0)) {m n : ℕ} (hmn : m ≤ n) :
mahlerSeries a (m : ℤ_[p]) = ∑ i ∈ range (n + 1), m.choose i • a i :=
by
have h_van (i) : m.choose (i + (n + 1)) = 0 := Nat.choose_eq_zero_of_lt (by cutsat)
have aux : Summable fun i ↦ m.choose (i + (n + 1)) • a (i + (n + 1)) := by
simpa only [h_van, zero_smul] using summable_zero
simp only [mahlerSeries_apply ha, mahler_natCast_eq, Nat.cast_smul_eq_nsmul, add_zero,
← aux.sum_add_tsum_nat_add' (f := fun i ↦ m.choose i • a i), h_van, zero_smul, tsum_zero]
