English
The quadratic version of map_finsupp_sum: for a quadratic map Q, a finitely supported function f, and g, Q on the finsupp sum equals the finsupp sum of Q composed with g plus a cross-term sum of polarizations.
Русский
Квадратичная версия map_finsupp_sum: для Q, функции f с конечной поддержкой и g, Q на сумме над f равна сумме Q(g) плюс сумма попарных поляризаций.
LaTeX
$$$ Q (f.sum g) = f.sum (\\lambda i r . Q (g i r)) + \\sum p \\in f.support.sym2 with \\neg p.IsDiag, polarSym2 Q (p.map (\\lambda i . g i (f i))) $$$
Lean4
/-- The quadratic version of `_root_.map_finsupp_sum`. -/
theorem map_finsuppSum (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M) :
Q (f.sum g) =
f.sum (fun i r ↦ Q (g i r)) + ∑ p ∈ f.support.sym2 with ¬p.IsDiag, polarSym2 Q (p.map fun i ↦ g i (f i)) :=
Q.map_sum _ _
