eval₂_eq_tsum — Mathlib

English

The evaluation of f equals the infinite sum over multi-indices of the same HasSum expression.

Русский

Оценка f равна бесконечной сумме по мультииндиксам того же выражения HasSum.

LaTeX

$$$$\operatorname{eval}_{\phi}^{a}(f) = \sum^{\prime}_{d: \sigma \to_{0} \mathbb{N}} \phi(\operatorname{coeff}_{d} f) \cdot \Bigl(d.\prod_{s} (a(s))^{e_s}\Bigr).$$$$

Lean4

theorem eval₂_eq_tsum (hφ : Continuous φ) (ha : HasEval a) (f : MvPowerSeries σ R) :
    MvPowerSeries.eval₂ φ a f = ∑' (d : σ →₀ ℕ), φ (coeff d f) * (d.prod fun s e => (a s) ^ e) :=
  (hasSum_eval₂ hφ ha f).tsum_eq.symm

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