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]