inner_finsupp_eq_sum_right — Mathlib

English

Similarly, the inner product of two linear combinations equals the sum with conjugate coefficients from l1 and l2.

Русский

Аналогично, скалярное произведение двух линейных комбинаций равно сумме с сопряженными коэффициентами из l1 и l2.

LaTeX

$$$\langle \operatorname{linearCombination} 𝕜 v l_1, \operatorname{linearCombination} 𝕜 v l_2 \rangle = \sum_i \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 over the second `Finsupp`. -/
theorem inner_finsupp_eq_sum_right {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) :
    ⟪linearCombination 𝕜 v l₁, linearCombination 𝕜 v l₂⟫ = l₂.sum fun i y => conj (l₁ i) * y := by
  simp only [l₂.linearCombination_apply _, Finsupp.inner_sum, hv.inner_left_finsupp, mul_comm, smul_eq_mul]

Похожие утверждения