mathlib documentation

data.matrix.hadamard

Hadamard product of matrices #

This file defines the Hadamard product matrix.hadamard and contains basic properties about them.

Main definition #

Notation #

References #

Tags #

hadamard product, hadamard

source
@[simp]
def matrix.hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} [has_mul α] (A B : matrix m n α) :
matrix m n α

matrix.hadamard defines the Hadamard product, which is the pointwise product of two matrices of the same size.

Equations
  • (A ⊙ B) i j = (A i j) * B i j
source
theorem matrix.hadamard_comm {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B : matrix m n α) [comm_semigroup α] :
A ⊙ B = B ⊙ A
source
theorem matrix.hadamard_assoc {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [semigroup α] :
A ⊙ B ⊙ C = A ⊙ (B ⊙ C)
source
theorem matrix.hadamard_add {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [distrib α] :
A ⊙ (B + C) = A ⊙ B + A ⊙ C
source
theorem matrix.add_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [distrib α] :
(B + C) ⊙ A = B ⊙ A + C ⊙ A
source
@[simp]
theorem matrix.smul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A B : matrix m n α) [has_mul α] [has_scalar R α] [is_scalar_tower R α α] (k : R) :
(k • A) ⊙ B = k • A ⊙ B
source
@[simp]
theorem matrix.hadamard_smul {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A B : matrix m n α) [has_mul α] [has_scalar R α] [smul_comm_class R α α] (k : R) :
A ⊙ (k • B) = k • A ⊙ B
source
@[simp]
theorem matrix.hadamard_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : matrix m n α) [mul_zero_class α] :
A ⊙ 0 = 0
source
@[simp]
theorem matrix.zero_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : matrix m n α) [mul_zero_class α] :
0 ⊙ A = 0
source
theorem matrix.hadamard_one {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_one_class α] (M : matrix n n α) :
M ⊙ 1 = matrix.diagonal (λ (i : n), M i i)
source
theorem matrix.one_hadamard {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_one_class α] (M : matrix n n α) :
1 ⊙ M = matrix.diagonal (λ (i : n), M i i)
source
theorem matrix.diagonal_hadamard_diagonal {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_class α] (v w : n → α) :
matrix.diagonal v ⊙ matrix.diagonal w = matrix.diagonal (v * w)
source
theorem matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_4} {n : Type u_5} (R : Type u_6) (A B : matrix m n α) [fintype m] [fintype n] [semiring α] [semiring R] [module R α] :
∑ (i : m) (j : n), (A ⊙ B) i j = ⇑(matrix.trace m R α) (A ⬝ Bᵀ)
source
theorem matrix.dot_product_vec_mul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (R : Type u_6) (A B : matrix m n α) [fintype m] [fintype n] [semiring α] [semiring R] [module R α] [decidable_eq m] [decidable_eq n] (v : m → α) (w : n → α) :
matrix.vec_mul v (A ⊙ B) ⬝ᵥ w = ⇑(matrix.trace m R α) (matrix.diagonal v ⬝ A ⬝ (B ⬝ matrix.diagonal w)ᵀ)