English
Let Q be a quadratic map from M to N over a commutative ring R, and let {f_i} be a finite family in M indexed by a finite set s. Then Q evaluated at the sum of the f_i equals the sum of Q(f_i) plus the sum, over all unordered pairs {i,j} from s, of the polarization of Q applied to (f_i, f_j).
Русский
Пусть Q — квадратичное отображение из M в N над коммутативным кольцом R, и пусть имеется конечная семейство элементов {f_i} в M, индексированная множеством s. Тогда Q(∑_{i∈s} f_i) равняется ∑_{i∈s} Q(f_i) плюс сумма по всем неупорядоченным парам {i,j} из s поляризованной формы polarSym2(Q)(f_i, f_j).
LaTeX
$$$ Q\\left(\\sum_{i\\in s} f_i\\right) = \\sum_{i\\in s} Q(f_i) \\, + \\, \\sum_{\\{i,j\\} \\subseteq s} polarSym2(Q)(f_i, f_j) $$$
Lean4
protected theorem map_sum {ι} [DecidableEq ι] (Q : QuadraticMap R M N) (s : Finset ι) (f : ι → M) :
Q (∑ i ∈ s, f i) = ∑ i ∈ s, Q (f i) + ∑ ij ∈ s.sym2 with ¬ij.IsDiag, polarSym2 Q (ij.map f) := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha
ih =>
simp_rw [Finset.sum_cons, QuadraticMap.map_add, ih, add_assoc, Finset.sym2_cons, Finset.sum_filter,
Finset.sum_disjUnion, Finset.sum_map, Finset.sum_cons, Sym2.mkEmbedding_apply, Sym2.isDiag_iff_proj_eq, not_true,
if_false, zero_add, Sym2.map_pair_eq, polarSym2_sym2Mk, ← polarBilin_apply_apply, _root_.map_sum,
polarBilin_apply_apply]
congr 2
rw [add_comm]
congr! with i hi
rw [if_pos (ne_of_mem_of_not_mem hi ha).symm]
