mathlib3 documentation

data.matrix.hadamard

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 #

Notation #

References #

Tags #

hadamard product, hadamard

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
@[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
theorem matrix.hadamard_comm {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B : matrix m n α) [comm_semigroup α] :
theorem matrix.hadamard_assoc {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [semigroup α] :
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
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
@[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
@[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
@[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
@[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
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)
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)
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
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 α) :