Lemmas for concrete matrices Matrix (Fin m) (Fin n) α

This file contains alternative definitions of common operators on matrices that expand definitionally to the expected expression when evaluated on !![] notation.

This allows "proof by reflection", where we prove A = !![A 0 0, A 0 1; A 1 0, A 1 1] by defining Matrix.etaExpand A to be equal to the RHS definitionally, and then prove that A = eta_expand A.

The definitions in this file should normally not be used directly; the intent is for the corresponding *_eq lemmas to be used in a place where they are definitionally unfolded.

Main definitions

• Matrix.transposeᵣ
• Matrix.dotProductᵣ
• Matrix.mulᵣ
• Matrix.mulVecᵣ
• Matrix.vecMulᵣ
• Matrix.etaExpand

def Matrix.Forall {α : Type u_1} {m : ℕ} {n : ℕ} : (Matrix (Fin m) (Fin n) α → Prop) → Prop

∀ with better defeq for ∀ x : Matrix (Fin m) (Fin n) α, P x.

Equations

• Matrix.Forall x = x (↑Matrix.of ![])
• Matrix.Forall x = FinVec.Forall fun r => Matrix.Forall fun A => x (↑Matrix.of (Matrix.vecCons r A))

theorem Matrix.forall_iff {α : Type u_1} {m : ℕ} {n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop) : Matrix.Forall P ↔ (x : Matrix (Fin m) (Fin n) α) → P x

This can be use to prove

example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
  (∀ x, P x) ↔ ∀ a b c d e f, P !![a, b, c; d, e, f] :=
(forall_iff _).symm

def Matrix.Exists {α : Type u_1} {m : ℕ} {n : ℕ} : (Matrix (Fin m) (Fin n) α → Prop) → Prop

∃ with better defeq for ∃ x : Matrix (Fin m) (Fin n) α, P x.

Equations

• Matrix.Exists x = x (↑Matrix.of ![])
• Matrix.Exists x = FinVec.Exists fun r => Matrix.Exists fun A => x (↑Matrix.of (Matrix.vecCons r A))

theorem Matrix.exists_iff {α : Type u_1} {m : ℕ} {n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop) : Matrix.Exists P ↔ ∃ x, P x

This can be use to prove

example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
  (∃ x, P x) ↔ ∃ a b c d e f, P !![a, b, c; d, e, f] :=
(exists_iff _).symm

def Matrix.transposeᵣ {α : Type u_1} {m : ℕ} {n : ℕ} : Matrix (Fin m) (Fin n) α → Matrix (Fin n) (Fin m) α

Matrix.transpose with better defeq for Fin

Equations

• Matrix.transposeᵣ x_4 = ↑Matrix.of ![]
• Matrix.transposeᵣ A = ↑Matrix.of (Matrix.vecCons (FinVec.map (fun v => v 0) A) (Matrix.transposeᵣ (Matrix.submatrix A id Fin.succ)))

@[simp]

theorem Matrix.transposeᵣ_eq {α : Type u_1} {m : ℕ} {n : ℕ} (A : Matrix (Fin m) (Fin n) α) : Matrix.transposeᵣ A = Matrix.transpose A

This can be used to prove

example (a b c d : α) : transpose !![a, b; c, d] = !![a, c; b, d] := (transposeᵣ_eq _).symm

def Matrix.dotProductᵣ {α : Type u_1} [Mul α] [Add α] [Zero α] {m : ℕ} (a : Fin m → α) (b : Fin m → α) : α

Matrix.dotProduct with better defeq for Fin

@[simp]

theorem Matrix.dotProductᵣ_eq {α : Type u_1} [Mul α] [AddCommMonoid α] {m : ℕ} (a : Fin m → α) (b : Fin m → α) : Matrix.dotProductᵣ a b = Matrix.dotProduct a b

This can be used to prove

example (a b c d : α) [Mul α] [AddCommMonoid α] :
  dot_product ![a, b] ![c, d] = a * c + b * d :=
(dot_productᵣ_eq _ _).symm

def Matrix.mulᵣ {l : ℕ} {m : ℕ} {n : ℕ} {α : Type u_1} [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) : Matrix (Fin l) (Fin n) α

Matrix.mul with better defeq for Fin

@[simp]

theorem Matrix.mulᵣ_eq {l : ℕ} {m : ℕ} {n : ℕ} {α : Type u_1} [Mul α] [AddCommMonoid α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) : Matrix.mulᵣ A B = A * B

This can be used to prove

example [AddCommMonoid α] [Mul α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] * !![b₁₁, b₁₂;
                    b₂₁, b₂₂] =
  !![a₁₁*b₁₁ + a₁₂*b₂₁, a₁₁*b₁₂ + a₁₂*b₂₂;
     a₂₁*b₁₁ + a₂₂*b₂₁, a₂₁*b₁₂ + a₂₂*b₂₂] :=
(mulᵣ_eq _ _).symm

def Matrix.mulVecᵣ {l : ℕ} {m : ℕ} {α : Type u_1} [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) : Fin l → α

Matrix.mulVec with better defeq for Fin

@[simp]

theorem Matrix.mulVecᵣ_eq {l : ℕ} {m : ℕ} {α : Type u_1} [NonUnitalNonAssocSemiring α] (A : Matrix (Fin l) (Fin m) α) (v : Fin m → α) : Matrix.mulVecᵣ A v = Matrix.mulVec A v

This can be used to prove

example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂].mulVec ![b₁, b₂] = ![a₁₁*b₁ + a₁₂*b₂, a₂₁*b₁ + a₂₂*b₂] :=
(mulVecᵣ_eq _ _).symm

def Matrix.vecMulᵣ {l : ℕ} {m : ℕ} {α : Type u_1} [Mul α] [Add α] [Zero α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α) : Fin m → α

Matrix.vecMul with better defeq for Fin

@[simp]

theorem Matrix.vecMulᵣ_eq {l : ℕ} {m : ℕ} {α : Type u_1} [NonUnitalNonAssocSemiring α] (v : Fin l → α) (A : Matrix (Fin l) (Fin m) α) : Matrix.vecMulᵣ v A = Matrix.vecMul v A

This can be used to prove

example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
  vecMul ![b₁, b₂] !![a₁₁, a₁₂;
                       a₂₁, a₂₂] = ![b₁*a₁₁ + b₂*a₂₁, b₁*a₁₂ + b₂*a₂₂] :=
(vecMulᵣ_eq _ _).symm

def Matrix.etaExpand {α : Type u_1} {m : ℕ} {n : ℕ} (A : Matrix (Fin m) (Fin n) α) : Matrix (Fin m) (Fin n) α

Expand A to !![A 0 0, ...; ..., A m n]

theorem Matrix.etaExpand_eq {α : Type u_1} {m : ℕ} {n : ℕ} (A : Matrix (Fin m) (Fin n) α) : Matrix.etaExpand A = A

This can be used to prove

example (A : Matrix (Fin 2) (Fin 2) α) :
  A = !![A 0 0, A 0 1;
         A 1 0, A 1 1] :=
(etaExpand_eq _).symm