English
For HasEval a and any f ∈ MvPowerSeries σ R, the evaluation aeval ha f is given by a convergent sum over multi-indices d: HasSum (d ↦ coeff d f · d.prod (a s)^e) (MvPowerSeries.aeval ha f).
Русский
Для HasEval a и любого f ∈ MvPowerSeries σ R отображение aeval ha f задаётся сходимым суммированием по многоиндексам d: HasSum (d ↦ coeff d f · ∏_s (a_s)^{d(s)}) (MvPowerSeries.aeval ha f).
LaTeX
$$$HasSum\left( d : σ \to_0 \mathbb{N} \to \mathbb{R}, \; (coeff\ d\ f) \cdot \big(d.prod (\lambda s e, (a\ s)^{e})\big) \right) \; (MvPowerSeries.aeval ha f)$$$
Lean4
theorem aeval_eq_sum (ha : HasEval a) (f : MvPowerSeries σ R) :
MvPowerSeries.aeval ha f = tsum (fun (d : σ →₀ ℕ) ↦ (coeff d f) • (d.prod fun s e => (a s) ^ e)) :=
(hasSum_aeval ha f).tsum_eq.symm
