English
Let Q be a quadratic map between R-modules M and N, and let g be a family of vectors g(i) in M indexed by ι with coefficients l(i) in R having finite support. Then the value of Q on the linear combination ∑ i l(i) g(i) is equal to the quadratic contribution coming from the squares of the coefficients, plus a correction term coming from pairwise interactions given by the polar form. More precisely, Q(∑ i l(i) g(i)) equals ∑ i l(i)^2 Q(g(i)) plus the sum over unordered pairs {i,j} with i ≠ j of l(i)l(j) times the polarSym2 of Q evaluated at (g(i), g(j)).
Русский
Пусть Q — квадратичное отображение между R-модулями M и N, а g: ι → M — семейство векторов с индексами i, коэффициенты l(i) ∈ R имеют конечную опору. Тогда значение Q на линейной combinations ∑ i l(i) g(i) равно квадратичному вкладу от квадратов коэффициентов плюс поправке, получаемой из попарных взаимодействий через полярную форму. Точнее, Q(∑ i l(i) g(i)) = ∑ i l(i)^2 Q(g(i)) + ∑ {i,j} (i ≠ j) l(i)l(j) polarSym2(Q)(g(i), g(j)).
LaTeX
$$$ Q\\Bigl(\\sum_i l_i\,g(i)\\Bigr) = \\sum_i l_i^2\,Q(g(i)) \\\\ + \\\\ \\sum_{\\{i,j\\}\\subseteq \\mathrm{supp}(l), i \\neq j} (l_i\,l_j)\, polarSym2(Q)(g(i), g(j)). $$$
Lean4
/-- The quadratic version of `Finsupp.apply_linearCombination`. -/
theorem apply_linearCombination (Q : QuadraticMap R M N) {g : ι → M} (l : ι →₀ R) :
Q (linearCombination R g l) =
linearCombination R (Q ∘ g) (l * l) +
∑ p ∈ l.support.sym2 with ¬p.IsDiag, (p.map l).mul • polarSym2 Q (p.map g) :=
by
simp_rw [linearCombination_apply, map_finsuppSum, Q.map_smul, mul_smul]
rw [(l * l).sum_of_support_subset support_mul_subset_left _ <| by simp]
simp [Finsupp.sum, ← polarSym2_map_smul, mul_smul]
