Documentation

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

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.

    Instances For
      source
      theorem Matrix.hadamard_comm {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [CommMagma α] :
      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_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] (M : Matrix n n α) (w : n → α) :
      M.hadamard (diagonal w) = diagonal (M.diag * w)
      source
      theorem Matrix.diagonal_hadamard {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] (M : Matrix n n α) (w : n → α) :
      (diagonal w).hadamard M = diagonal (w * M.diag)
      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.diagonal_hadamard_eq_diagonal_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] {A : Matrix n n α} {d e : n → α} :
      (diagonal d).hadamard A = diagonal e ↔ d * A.diag = e
      source
      theorem Matrix.hadamard_diagonal_eq_diagonal_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] {A : Matrix n n α} {d e : n → α} :
      A.hadamard (diagonal d) = diagonal e ↔ A.diag * d = e
      source
      theorem Matrix.hadamard_one {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
      M.hadamard 1 = diagonal M.diag
      source
      theorem Matrix.one_hadamard {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
      hadamard 1 M = diagonal M.diag
      source
      theorem Matrix.one_hadamard_eq_diagonal_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} {d : n → α} :
      hadamard 1 A = diagonal d ↔ A.diag = d
      source
      theorem Matrix.hadamard_one_eq_diagonal_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} {d : n → α} :
      A.hadamard 1 = diagonal d ↔ A.diag = d
      source
      theorem Matrix.one_hadamard_eq_zero_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} :
      hadamard 1 A = 0 ↔ A.diag = 0
      source
      theorem Matrix.hadamard_one_eq_zero_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} :
      A.hadamard 1 = 0 ↔ A.diag = 0
      source
      theorem Matrix.one_hadamard_eq_one_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} :
      hadamard 1 A = 1 ↔ A.diag = 1
      source
      theorem Matrix.hadamard_one_eq_one_iff {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] {A : Matrix n n α} :
      A.hadamard 1 = 1 ↔ A.diag = 1
      source
      @[simp]
      theorem Matrix.hadamard_of_one {α : Type u_1} {m : Type u_2} {n : Type u_3} [MulOneClass α] (A : Matrix m n α) :
      A.hadamard (of 1) = A
      source
      @[simp]
      theorem Matrix.of_one_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} [MulOneClass α] (A : Matrix m n α) :
      (of 1).hadamard A = A
      source
      theorem Matrix.hadamard_self_eq_self_iff {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] {A : Matrix m n α} :
      A.hadamard A = A ↔ ∀ (i : m) (j : n), IsIdempotentElem (A i j)
      source
      theorem Matrix.submatrix_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_5} {o : Type u_6} [Mul α] (A B : Matrix m n α) (e : l → m) (f : o → n) :
      (A.hadamard B).submatrix e f = (A.submatrix e f).hadamard (B.submatrix e f)
      source
      theorem Matrix.transpose_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] (A B : Matrix m n α) :
      (A.hadamard B).transpose = A.transpose.hadamard B.transpose
      source
      theorem Matrix.conjTranspose_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] [StarMul α] (A B : Matrix m n α) :
      (A.hadamard B).conjTranspose = B.conjTranspose.hadamard A.conjTranspose
      source
      theorem Matrix.single_hadamard_single_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] (i : m) (j : n) (a b : α) :
      (single i j a).hadamard (single i j b) = single i j (a * b)
      source
      theorem Matrix.single_hadamard_single_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 : α) :
      (single ia ja a).hadamard (single ib jb b) = 0
      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] [NonUnitalSemiring α] :
      ∑ 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] [NonUnitalSemiring α] [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
      vecMul v (A.hadamard B) ⬝ᵥ w = (diagonal v * A * (B * diagonal w).transpose).trace