English
The inner product of two sums over the same index set equals the index-wise sum of products of coefficients.
Русский
Скалярное произведение двух сумм по одному и тому же индексу равно по индексу сумма произведений коэффициентов.
LaTeX
$$$\langle \sum_{i\in s} l_1(i) v_i, \sum_{i\in s} l_2(i) v_i \rangle = \sum_{i\in s} \overline{l_1(i)} \cdot l_2(i)$$$
Lean4
/-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
a sum. -/
protected theorem inner_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι → 𝕜) (s : Finset ι) :
⟪∑ i ∈ s, l₁ i • v i, ∑ i ∈ s, l₂ i • v i⟫ = ∑ i ∈ s, conj (l₁ i) * l₂ i :=
by
simp_rw [sum_inner, inner_smul_left]
refine Finset.sum_congr rfl fun i hi => ?_
rw [hv.inner_right_sum l₂ hi]
