English
In an orthonormal family, the inner product with a left-hand linear combination yields the conjugate coefficient: ⟪linearCombination 𝕜 v l, v_i⟫ = conj(l_i).
Русский
Для ортонормированного набора скалярное произведение с левой линейной комбинацией дает сопряженный коэффициент: ⟪linearCombination 𝕜 v l, v_i⟫ = conj(l_i).
LaTeX
$$$\langle \operatorname{linearCombination} 𝕜 v l, 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_right_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) :
⟪v i, ∑ i ∈ s, l i • v i⟫ = l i := by classical simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]
