Hadamard product of matrices

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

Tags

hadamard product, hadamard

def Matrix.hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} [Mul α] (A : Matrix m n α) (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

• Matrix.hadamard A B = Matrix.of fun (i : m) (j : n) => A i j * B i j

@[simp]

theorem Matrix.hadamard_apply {α : Type u_1} {m : Type u_4} {n : Type u_5} [Mul α] (A : Matrix m n α) (B : Matrix m n α) (i : m) (j : n) : Matrix.hadamard A B i j = A i j * B i j

def Matrix.«term_⊙_» : Lean.TrailingParserDescr

Equations

• Matrix.«term_⊙_» = Lean.ParserDescr.trailingNode `Matrix.term_⊙_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊙ ") (Lean.ParserDescr.cat `term 101))

theorem Matrix.hadamard_comm {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) [CommSemigroup α] : Matrix.hadamard A B = Matrix.hadamard B A

theorem Matrix.hadamard_assoc {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [Semigroup α] : Matrix.hadamard (Matrix.hadamard A B) C = Matrix.hadamard A (Matrix.hadamard B C)

theorem Matrix.hadamard_add {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [Distrib α] : Matrix.hadamard A (B + C) = Matrix.hadamard A B + Matrix.hadamard A C

theorem Matrix.add_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [Distrib α] : Matrix.hadamard (B + C) A = Matrix.hadamard B A + Matrix.hadamard C A

@[simp]

theorem Matrix.smul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [IsScalarTower R α α] (k : R) : Matrix.hadamard (k • A) B = k • Matrix.hadamard A B

@[simp]

theorem Matrix.hadamard_smul {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [SMulCommClass R α α] (k : R) : Matrix.hadamard A (k • B) = k • Matrix.hadamard A B

@[simp]

theorem Matrix.hadamard_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) [MulZeroClass α] : Matrix.hadamard A 0 = 0

@[simp]

theorem Matrix.zero_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) [MulZeroClass α] : Matrix.hadamard 0 A = 0

theorem Matrix.hadamard_one {α : Type u_1} {n : Type u_5} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) : Matrix.hadamard M 1 = Matrix.diagonal fun (i : n) => M i i

theorem Matrix.one_hadamard {α : Type u_1} {n : Type u_5} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) : Matrix.hadamard 1 M = Matrix.diagonal fun (i : n) => M i i

theorem Matrix.diagonal_hadamard_diagonal {α : Type u_1} {n : Type u_5} [DecidableEq n] [MulZeroClass α] (v : n → α) (w : n → α) : Matrix.hadamard (Matrix.diagonal v) (Matrix.diagonal w) = Matrix.diagonal (v * w)

theorem Matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] : (Finset.sum Finset.univ fun (i : m) => Finset.sum Finset.univ fun (j : n) => Matrix.hadamard A B i j) = Matrix.trace (A * Matrix.transpose B)

theorem Matrix.dotProduct_vecMul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) : Matrix.dotProduct (Matrix.vecMul v (Matrix.hadamard A B)) w = Matrix.trace (Matrix.diagonal v * A * Matrix.transpose (B * Matrix.diagonal w))