hasSum_aeval — Mathlib

English

Let ha be HasEval a and f a power series in R. Then the series sum over d of coeff d f times a^d converges to f.aeval ha; i.e., HasSum (coeff d f • a^d) (f.aeval ha).

Русский

Пусть ha = HasEval a и f — степенной ряд над R. Тогда ряд сумма по d из coeff d f умноженного на a^d сходится к f.aeval ha; то есть HasSum (coeff d f • a^d) (f.aeval ha).

LaTeX

$$$ \text{HasSum}(\lambda d, \mathrm{coeff}_d f \cdot a^d) \; (f.\mathrm{aeval}\ ha) $$$

Lean4

theorem hasSum_aeval (ha : HasEval a) (f : PowerSeries R) : HasSum (fun d ↦ coeff d f • a ^ d) (f.aeval ha) :=
  by
  simp_rw [coe_aeval, ← algebraMap_smul (R := R) S, smul_eq_mul]
  exact hasSum_eval₂ (continuous_algebraMap R S) ha f

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