mahlerSeries_apply — Mathlib

English

If ha: Tendsto a atTop to 0, and m ≤ n, then mahlerSeries a evaluated at m equals the finite sum ∑_{i=0}^{n} (m choose i) a_i.

Русский

Если ha: a_n → 0 и m ≤ n, то mahlerSeries(a)(m) равен конечной сумме ∑_{i=0}^{n} (m choose i) a_i.

LaTeX

$$$$ mahlerSeries(a)(m) = \\sum_{i=0}^{n} {m \\choose i} a_i \\quad (m \\le n). $$$$

Lean4

/-- Evaluation of a Mahler series is just the pointwise sum. -/
theorem mahlerSeries_apply (ha : Tendsto a atTop (𝓝 0)) (x : ℤ_[p]) : mahlerSeries a x = ∑' n, mahler n x • a n := by
  simp only [mahlerSeries, ← ContinuousMap.tsum_apply (hasSum_mahlerSeries ha).summable, mahlerTerm_apply]

Похожие утверждения