English
The inner product of a finite linear combination with the corresponding vector equals the conjugate of the coefficient: ⟪∑ i∈s l_i v_i, v_i⟫ = conj(l_i).
Русский
Скалярное произведение конечной линейной комбинации с соответствующим вектором равно сопряженному коэффициенту: ⟪∑ i∈s l_i v_i, v_i⟫ = conj(l_i).
LaTeX
$$$\langle \sum_{i \in s} l_i v_i, v_i \rangle = \overline{l_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_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) :
⟪∑ i ∈ s, l i • v i, v i⟫ = conj (l i) := by
classical
simp only [sum_inner, inner_smul_left, orthonormal_iff_ite.mp hv, hi, mul_boole, Finset.sum_ite_eq', if_true]
