star_dotProduct_gram_mulVec — Mathlib

English

For v = (v_i) and x,y ∈ 𝕜^n, the identity holds: x* ⬝ᵥ (gram 𝕜 v) *ᵥ y = ⟪∑ i x_i v_i, ∑ i y_i v_i⟫_𝕜.

Русский

Для v = (v_i) и векторов x,y ∈ 𝕜^n имеем: x^* (gram 𝕜 v) y = ⟪∑ i x_i v_i, ∑ i y_i v_i⟫_𝕜.

LaTeX

$$$ \overline{x}^{\top} (\text{gram } 𝕜 v) y = \left\langle \sum_i x_i v_i, \sum_j y_j v_j \right\rangle_{𝕜} $$$

Lean4

theorem star_dotProduct_gram_mulVec (v : n → E) (x y : n → 𝕜) :
    star x ⬝ᵥ (gram 𝕜 v) *ᵥ y = ⟪∑ i, x i • v i, ∑ i, y i • v i⟫_𝕜 :=
  by
  trans ∑ i, ∑ j, conj (x i) * y j * ⟪v i, v j⟫_𝕜
  ·
    simp_rw [dotProduct, mul_assoc, ← Finset.mul_sum, mulVec, dotProduct, mul_comm, ← star_def, gram_apply,
      Pi.star_apply]
  · simp_rw [sum_inner, inner_sum, inner_smul_left, inner_smul_right, mul_assoc]

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