hasSum_mahlerSeries — Mathlib

English

If a_n → 0, then the Mahler terms converge and the series has sum mahlerSeries(a).

Русский

Если a_n → 0, то члены серии Маhler сходятся и ряд имеет предел mahlerSeries(a).

LaTeX

$$$$ \\text{If } a_n \\to 0, \\text{ then } \\sum_{n=0}^{\\infty} mahlerTerm(a(n), n) \\text{ converges to } mahlerSeries(a). $$$$

Lean4

/-- A Mahler series whose coefficients tend to 0 is convergent. -/
theorem hasSum_mahlerSeries (ha : Tendsto a atTop (𝓝 0)) :
    HasSum (fun n ↦ mahlerTerm (a n) n) (mahlerSeries a : C(ℤ_[p], E)) :=
  by
  refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum
  rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢
  simpa only [norm_mahlerTerm, Nat.cofinite_eq_atTop] using ha

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