eval₂_eq_tsum — Mathlib

English

For continuous φ and evaluable a, the series sum equals evaluation: HasSum (d ↦ φ(coeff d f) a^d) (f.eval₂ φ a).

Русский

Для непрерывного φ и оценивания a сумма ряда даёт значение f при eval₂ φ a.

LaTeX

$$$\text{HasSum} (\lambda d, φ(\text{coeff } d f) \cdot a^{d}) \ (f.eval_2 φ a)$$$

Lean4

theorem eval₂_eq_tsum (hφ : Continuous φ) (ha : HasEval a) (f : PowerSeries R) :
    PowerSeries.eval₂ φ a f = ∑' d : ℕ, φ (coeff d f) * a ^ d :=
  (hasSum_eval₂ hφ ha f).tsum_eq.symm

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