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]