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ᵣ
• 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 : Fin x✝¹ → α) => Matrix.Forall fun (A : Matrix (Fin n) (Fin x✝¹) α) => 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 used 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 : Fin x✝¹ → α) => Matrix.Exists fun (A : Matrix (Fin n) (Fin x✝¹) α) => 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 : Matrix (Fin m) (Fin n) α), P x

This can be used 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

• x_4.transposeᵣ = Matrix.of ![]
• A.transposeᵣ = Matrix.of (Matrix.vecCons (FinVec.map (fun (v : Fin (n + 1) → α) => v 0) A) (A.submatrix id Fin.succ).transposeᵣ)

@[simp]

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

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 b : Fin m → α) : α

dotProduct with better defeq for Fin

Equations

• Matrix.dotProductᵣ a b = FinVec.sum (FinVec.seq (FinVec.map (fun (x1 x2 : α) => x1 * x2) a) b)

@[simp]

theorem Matrix.dotProductᵣ_eq {α : Type u_1} [Mul α] [AddCommMonoid α] {m : ℕ} (a b : Fin m → α) : Matrix.dotProductᵣ a b = 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

Equations

• A.mulᵣ B = Matrix.of (FinVec.map (fun (v₁ : Fin m → α) => FinVec.map (fun (v₂ : Fin m → α) => Matrix.dotProductᵣ v₁ v₂) B.transpose) A)

@[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) α) : A.mulᵣ 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

Equations

• A.mulVecᵣ v = FinVec.map (fun (a : Fin m → α) => Matrix.dotProductᵣ a v) A

@[simp]

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

This can be used to prove

example [NonUnitalNonAssocSemiring α] (a₁₁ a₁₂ a₂₁ a₂₂ b₁ b₂ : α) :
  !![a₁₁, a₁₂;
     a₂₁, a₂₂] *ᵥ ![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

Equations

• Matrix.vecMulᵣ v A = FinVec.map (fun (a : Fin l → α) => Matrix.dotProductᵣ v a) A.transpose

@[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₂ : α) :
  ![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]

Equations

• A.etaExpand = Matrix.of (FinVec.etaExpand fun (i : Fin m) => FinVec.etaExpand fun (j : Fin n) => A i j)

theorem Matrix.etaExpand_eq {α : Type u_1} {m n : ℕ} (A : Matrix (Fin m) (Fin n) α) : A.etaExpand = 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