English
There is a HasSum representation of eval₂ as a weighted sum over multi-indices, with coefficients given by φ of coeffs of f and products of a(s) powers.
Русский
Существуют представления вида HasSum для eval₂ как взвешенная сумма по мультииндексам: коэффициенты — φ(coeff d f), а — произведения a(s)^{e_s}.
LaTeX
$$$$\operatorname{HasSum}\Bigl(d:\,\sigma \to\_{0} \mathbb{N}\Bigr) \mapsto \phi(\operatorname{coeff}_{d} f) \cdot \Bigl(d.\prod_{s} (a(s))^{e_s}\Bigr)$$$$
Lean4
theorem hasSum_eval₂ (hφ : Continuous φ) (ha : HasEval a) (f : MvPowerSeries σ R) :
HasSum (fun (d : σ →₀ ℕ) ↦ φ (coeff d f) * (d.prod fun s e => (a s) ^ e)) (MvPowerSeries.eval₂ φ a f) :=
by
rw [← coe_eval₂Hom hφ ha, eval₂Hom_eq_extend hφ ha]
convert (hasSum_of_monomials_self f).map (eval₂Hom hφ ha) (?_) with d
· simp only [Function.comp_apply, coe_eval₂Hom, ← MvPolynomial.coe_monomial, eval₂_coe, eval₂_monomial]
· rw [coe_eval₂Hom]; exact continuous_eval₂ hφ ha
