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

source
def Matrix.hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] (A B : Matrix m n α) :
Matrix m n α

Matrix.hadamard (denoted as ⊙ within the Matrix namespace) defines the Hadamard product, which is the pointwise product of two matrices of the same size.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.hadamard_apply {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] (A B : Matrix m n α) (i : m) (j : n) :
    A.hadamard B i j = A i j * B i j
    source
    def Matrix.«term_⊙_» :
    Lean.TrailingParserDescr

    Matrix.hadamard (denoted as ⊙ within the Matrix namespace) defines the Hadamard product, which is the pointwise product of two matrices of the same size.

    Equations
    Instances For
      source
      theorem Matrix.hadamard_comm {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [CommSemigroup α] :
      A.hadamard B = B.hadamard A
      source
      theorem Matrix.hadamard_assoc {α : Type u_1} {m : Type u_2} {n : Type u_3} (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_2} {n : Type u_3} (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_2} {n : Type u_3} (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_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [Mul α] [SMul R α] [IsScalarTower R α α] (k : R) :
      (k • A).hadamard B = k • A.hadamard B
      source
      @[simp]
      theorem Matrix.hadamard_smul {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [Mul α] [SMul R α] [SMulCommClass R α α] (k : R) :
      A.hadamard (k • B) = k • A.hadamard B
      source
      @[simp]
      theorem Matrix.hadamard_zero {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [MulZeroClass α] :
      A.hadamard 0 = 0
      source
      @[simp]
      theorem Matrix.zero_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [MulZeroClass α] :
      hadamard 0 A = 0
      source
      theorem Matrix.hadamard_one {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
      M.hadamard 1 = diagonal fun (i : n) => M i i
      source
      theorem Matrix.one_hadamard {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
      hadamard 1 M = diagonal fun (i : n) => M i i
      source
      theorem Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] (i : m) (j : n) (a b : α) :
      (stdBasisMatrix i j a).hadamard (stdBasisMatrix i j b) = stdBasisMatrix i j (a * b)
      source
      theorem Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_of_ne {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] {ia : m} {ja : n} {ib : m} {jb : n} (h : ¬(ia = ib ∧ ja = jb)) (a b : α) :
      (stdBasisMatrix ia ja a).hadamard (stdBasisMatrix ib jb b) = 0
      source
      theorem Matrix.diagonal_hadamard_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] (v w : n → α) :
      (diagonal v).hadamard (diagonal w) = diagonal (v * w)
      source
      theorem Matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] :
      ∑ i : m, ∑ j : n, A.hadamard B i j = (A * B.transpose).trace
      source
      theorem Matrix.dotProduct_vecMul_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
      vecMul v (A.hadamard B) ⬝ᵥ w = (diagonal v * A * (B * diagonal w).transpose).trace