dotProduct_vecMul_hadamard — Mathlib

English

For A,B, and vectors v∈α^m, w∈α^n, the bilinear form v^T (A ⊙ B) w equals tr(diag(v) A (B diag(w))^T).

Русский

Для матриц A,B и векторов v∈α^m, w∈α^n выполняется равенство v^T (A ⊙ B) w = tr(diag(v) A (B diag(w))^T).

LaTeX

$$$v^T (A \odot B) w = \operatorname{tr}(\operatorname{diag}(v) A (B \operatorname{diag}(w))^T)$$$

Lean4

theorem dotProduct_vecMul_hadamard [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
    v ᵥ* (A ⊙ B) ⬝ᵥ w = trace (diagonal v * A * (B * diagonal w)ᵀ) :=
  by
  rw [← sum_hadamard_eq, Finset.sum_comm]
  simp [dotProduct, vecMul, Finset.sum_mul, mul_assoc]

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