English
For a finite family {f_i} indexed by s, the polarization relation can be written as Q(∑ f_i) equals the cross-polarization term minus the sum of the individual Q(f_i).
Русский
Для конечной семейства {f_i}, индексированного по s, поляризационная формула записывается как Q(∑ f_i) равно кросс-поляризационному члену минус сумма отдельных Q(f_i).
LaTeX
$$$ Q\\left(\\sum_{i\\in s} f_i\\right) = \\sum_{\\{i,j\\} \\subseteq s} polarSym2(Q)(f_i, f_j) - \\sum_{i\\in s} Q(f_i) $$$
Lean4
protected theorem map_sum' {ι} (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) :
Q (∑ i ∈ s, f i) = ∑ ij ∈ s.sym2, polarSym2 Q (ij.map f) - ∑ i ∈ s, Q (f i) := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha
ih =>
simp_rw [Finset.sum_cons, QuadraticMap.map_add Q, ih, add_assoc, Finset.sym2_cons, Finset.sum_disjUnion,
Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply, Sym2.map_pair_eq, polarSym2_sym2Mk, ←
polarBilin_apply_apply, _root_.map_sum, polarBilin_apply_apply, polar_self]
abel_nf
