English
The inner product of two finite linear combinations of an orthonormal family equals the sum of products of coefficients: ⟪∑ l1_i v_i, ∑ l2_i v_i⟫ = ∑ conj(l1_i) l2_i.
Русский
Скалярное произведение двух конечных линейных комбинаций ортонормированного набора равно сумме произведений коэффициентов: ⟪∑ l1_i v_i, ∑ l2_i v_i⟫ = ∑ conj(l1_i) l2_i.
LaTeX
$$$\Big\langle \sum_{i} l_1(i) v_i, \sum_{i} l_2(i) v_i \Big
angle = \sum_{i} \overline{l_1(i)} \cdot l_2(i)$$$
Lean4
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector. -/
theorem inner_left_fintype [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) :
⟪∑ i : ι, l i • v i, v i⟫ = conj (l i) :=
hv.inner_left_sum l (Finset.mem_univ _)
