Documentation

Mathlib.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

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
  • A.hadamard B = Matrix.of fun (i : m) (j : n) => A i j * B i j
Instances For
    @[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) :
    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 : Matrix m n α) (B : Matrix m n α) [CommSemigroup α] :
    A.hadamard B = B.hadamard 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 α] :
    (A.hadamard B).hadamard C = A.hadamard (B.hadamard 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 α] :
    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 : Matrix m n α) (B : Matrix m n α) (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 : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [IsScalarTower 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 : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [SMulCommClass 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 α) [MulZeroClass α] :
    A.hadamard 0 = 0
    @[simp]
    theorem Matrix.zero_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) [MulZeroClass α] :
    theorem Matrix.hadamard_one {α : Type u_1} {n : Type u_5} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
    M.hadamard 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α) :
    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 α] :
    i : m, j : n, A.hadamard B i j = (A * B.transpose).trace
    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 (A.hadamard B)) w = (Matrix.diagonal v * A * (B * Matrix.diagonal w).transpose).trace