English
The coefficient of a substituted series is given by a finite sum of products of coefficients of f and the substituted monomials.
Русский
Коэффициент подстановки равен конечной сумме произведений коэффициентов из f и подстановленных мономов.
LaTeX
$$$\\operatorname{coeff}_{e}(\\operatorname{subst}(a,f)) = \\operatorname{finsum}\\!\\bigl( d \\mapsto \\operatorname{coeff}_{d} f \\cdot \\operatorname{coeff}_{e}(d.\\prod (a_s)^e) \\bigr)$$$
Lean4
theorem coeff_subst (ha : HasSubst a) (f : MvPowerSeries σ R) (e : τ →₀ ℕ) :
coeff e (subst a f) = finsum (fun d ↦ coeff d f • (coeff e (d.prod fun s e => (a s) ^ e))) :=
by
letI : UniformSpace R := ⊥
letI : UniformSpace S := ⊥
have := ((hasSum_aeval ha.hasEval f).map (coeff e) (continuous_coeff S e))
simp [← coe_substAlgHom ha, substAlgHom, ← this.tsum_eq, tsum_eq_finsum (coeff_subst_finite ha f e)]
