Hadamard product of matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main definition #

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

Notation #

⊙: the Hadamard product matrix.hadamard;

References #

https://en.wikipedia.org/wiki/hadamard_product_(matrices)

Tags #

hadamard product, hadamard

source

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.hadamard B = ⇑matrix.of (λ (i : m) (j : n), A i j * B i j)

source

@[simp]

theorem matrix.hadamard_apply {α : Type u_1} {m : Type u_4} {n : Type u_5} [has_mul α] (A B : matrix m n α) (i : m) (j : n) :

A.hadamard 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.hadamard B = B.hadamard 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.hadamard B).hadamard C = A.hadamard (B.hadamard 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.hadamard (B + C) = A.hadamard B + A.hadamard 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).hadamard A = B.hadamard A + C.hadamard 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_smul R α] [is_scalar_tower R α α] (k : R) :

(k • A).hadamard B = k • A.hadamard 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_smul R α] [smul_comm_class R α α] (k : R) :

A.hadamard (k • B) = k • A.hadamard 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.hadamard 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.hadamard 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.hadamard 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.hadamard 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).hadamard (matrix.diagonal w) = matrix.diagonal (v * w)

source

theorem matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B : matrix m n α) [fintype m] [fintype n] [semiring α] :

finset.univ.sum (λ (i : m), finset.univ.sum (λ (j : n), A.hadamard B i j)) = (A.mul B.transpose).trace

source

theorem matrix.dot_product_vec_mul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B : matrix m n α) [fintype m] [fintype n] [semiring α] [decidable_eq m] [decidable_eq n] (v : m → α) (w : n → α) :

matrix.dot_product (matrix.vec_mul v (A.hadamard B)) w = (((matrix.diagonal v).mul A).mul (B.mul (matrix.diagonal w)).transpose).trace