Squared norm of a finite sum in a real inner product space

Expanding ‖∑ i ∈ s, f i‖ ^ 2 = ⟪∑ i ∈ s, f i, ∑ j ∈ s, f j⟫ separates the diagonal terms ∑ i ∈ s, ‖f i‖ ^ 2 from the off-diagonal inner products ∑ p ∈ s.offDiag, ⟪f p.1, f p.2⟫ (norm_sum_sq_real).

Main results

• norm_sum_sq_real: the squared norm of a finite sum, expanded over the diagonal and the ordered pairs of distinct indices.

theorem norm_sum_sq_real {V : Type u_1} {ι : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (s : Finset ι) (f : ι → V) : ‖∑ i ∈ s, f i‖ ^ 2 = ∑ i ∈ s, ‖f i‖ ^ 2 + ∑ p ∈ s.offDiag, inner ℝ (f p.1) (f p.2)

The squared norm of a finite sum is the sum of the squared norms plus the inner products over the ordered pairs of distinct indices.