hasSum_of_monomials_self — Mathlib

English

A power series is the sum, in the sense of summable families, of its monomial terms.

Русский

Степенной ряд является суммой своих мономов (путём суммирования по индексу).

LaTeX

$$$f = \sum_{d=0}^{\infty} \mathrm{monomial}_d(\mathrm{coeff}_d f)$$$

Lean4

/-- A power series is the sum (in the sense of summable families) of its monomials -/
theorem hasSum_of_monomials_self (f : PowerSeries R) : HasSum (fun d : ℕ => monomial d (coeff d f)) f :=
  by
  rw [← (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.hasSum_iff]
  convert MvPowerSeries.WithPiTopology.hasSum_of_monomials_self f
  simp only [LinearEquiv.coe_toEquiv, comp_apply, monomial, coeff, Finsupp.LinearEquiv.finsuppUnique_apply,
    PUnit.default_eq_unit]
  congr
  all_goals { ext; simp
  }

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