English
For any orthonormal v, and finsupp l1, l2, the inner product of the left linearCombination with the left vector equals the sum with coefficients of l2, weighted by the star of l1's coefficient.
Русский
Для ортонормированного v и линейной комбинации по Finsupp, скалярное произведение левой линейной комбинации и левой вектор равняется сумме коэффициентов, умноженных на сопряжение первого коэффициента.
LaTeX
$$$\langle \operatorname{linearCombination} 𝕜 v l_1, v_i \rangle = \overline{l_1(i)}$$$
Lean4
/-- The inner product of two linear combinations of a set of orthonormal vectors, expressed as
a sum over the first `Finsupp`. -/
theorem inner_finsupp_eq_sum_left {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
⟪linearCombination 𝕜 v l₁, linearCombination 𝕜 v l₂⟫ = l₁.sum fun i y => conj y * l₂ i := by
simp only [l₁.linearCombination_apply _, Finsupp.sum_inner, hv.inner_right_finsupp, smul_eq_mul]
