Block Matrices from Rows and Columns #
This file provides the basic definitions of matrices composed from columns and rows.
The concatenation of two matrices with the same row indices can be expressed as
A = fromColumns A₁ A₂ the concatenation of two matrices with the same column indices
can be expressed as B = fromRows B₁ B₂.
We then provide a few lemmas that deal with the products of these with each other and with block matrices
Tags #
column matrices, row matrices, column row block matrices
def
Matrix.fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
:
Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]
Equations
- Matrix.fromRows A₁ A₂ = Matrix.of (Sum.elim A₁ A₂)
Instances For
def
Matrix.fromColumns
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
(B₁ : Matrix m n₁ R)
(B₂ : Matrix m n₂ R)
:
Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]
Equations
- Matrix.fromColumns B₁ B₂ = Matrix.of fun (i : m) => Sum.elim (B₁ i) (B₂ i)
Instances For
@[simp]
theorem
Matrix.toRows₁_fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
:
Matrix.toRows₁ (Matrix.fromRows A₁ A₂) = A₁
@[simp]
theorem
Matrix.toRows₂_fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
:
Matrix.toRows₂ (Matrix.fromRows A₁ A₂) = A₂
@[simp]
theorem
Matrix.toColumns₁_fromColumns
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
(A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R)
:
Matrix.toColumns₁ (Matrix.fromColumns A₁ A₂) = A₁
@[simp]
theorem
Matrix.toColumns₂_fromColumns
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
(A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R)
:
Matrix.toColumns₂ (Matrix.fromColumns A₁ A₂) = A₂
@[simp]
theorem
Matrix.fromRows_toRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
(A : Matrix (m₁ ⊕ m₂) n R)
:
Matrix.fromRows (Matrix.toRows₁ A) (Matrix.toRows₂ A) = A
theorem
Matrix.fromRows_inj
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
:
Function.Injective2 Matrix.fromRows
theorem
Matrix.fromColumns_inj
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
:
Function.Injective2 Matrix.fromColumns
theorem
Matrix.transpose_fromColumns
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
(A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R)
:
Matrix.transpose (Matrix.fromColumns A₁ A₂) = Matrix.fromRows (Matrix.transpose A₁) (Matrix.transpose A₂)
theorem
Matrix.transpose_fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
:
Matrix.transpose (Matrix.fromRows A₁ A₂) = Matrix.fromColumns (Matrix.transpose A₁) (Matrix.transpose A₂)
@[simp]
theorem
Matrix.fromRows_mulVec
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
[Fintype n]
[Semiring R]
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
(v : n → R)
:
Matrix.mulVec (Matrix.fromRows A₁ A₂) v = Sum.elim (Matrix.mulVec A₁ v) (Matrix.mulVec A₂ v)
@[simp]
theorem
Matrix.vecMul_fromColumns
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype m]
[Semiring R]
(B₁ : Matrix m n₁ R)
(B₂ : Matrix m n₂ R)
(v : m → R)
:
Matrix.vecMul v (Matrix.fromColumns B₁ B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)
@[simp]
theorem
Matrix.sum_elim_vecMul_fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
[Fintype m₁]
[Fintype m₂]
[Semiring R]
(B₁ : Matrix m₁ n R)
(B₂ : Matrix m₂ n R)
(v₁ : m₁ → R)
(v₂ : m₂ → R)
:
Matrix.vecMul (Sum.elim v₁ v₂) (Matrix.fromRows B₁ B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
@[simp]
theorem
Matrix.fromColumns_mulVec_sum_elim
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype n₁]
[Fintype n₂]
[Semiring R]
(A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R)
(v₁ : n₁ → R)
(v₂ : n₂ → R)
:
Matrix.mulVec (Matrix.fromColumns A₁ A₂) (Sum.elim v₁ v₂) = Matrix.mulVec A₁ v₁ + Matrix.mulVec A₂ v₂
@[simp]
theorem
Matrix.fromRows_zero
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
[Semiring R]
:
Matrix.fromRows 0 0 = 0
@[simp]
theorem
Matrix.fromColumns_zero
{R : Type u_1}
{m : Type u_2}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Semiring R]
:
Matrix.fromColumns 0 0 = 0
@[simp]
theorem
Matrix.fromColumns_fromRows_eq_fromBlocks
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n₁ : Type u_6}
{n₂ : Type u_7}
(B₁₁ : Matrix m₁ n₁ R)
(B₁₂ : Matrix m₁ n₂ R)
(B₂₁ : Matrix m₂ n₁ R)
(B₂₂ : Matrix m₂ n₂ R)
:
Matrix.fromColumns (Matrix.fromRows B₁₁ B₂₁) (Matrix.fromRows B₁₂ B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
@[simp]
theorem
Matrix.fromRows_fromColumn_eq_fromBlocks
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n₁ : Type u_6}
{n₂ : Type u_7}
(B₁₁ : Matrix m₁ n₁ R)
(B₁₂ : Matrix m₁ n₂ R)
(B₂₁ : Matrix m₂ n₁ R)
(B₂₂ : Matrix m₂ n₂ R)
:
Matrix.fromRows (Matrix.fromColumns B₁₁ B₁₂) (Matrix.fromColumns B₂₁ B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
theorem
Matrix.fromRows_mul_fromColumns
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype n]
[Semiring R]
(A₁ : Matrix m₁ n R)
(A₂ : Matrix m₂ n R)
(B₁ : Matrix n n₁ R)
(B₂ : Matrix n n₂ R)
:
Matrix.fromRows A₁ A₂ * Matrix.fromColumns B₁ B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
A row partitioned matrix multiplied by a column partioned matrix gives a 2 by 2 block matrix
theorem
Matrix.fromColumns_mul_fromRows
{R : Type u_1}
{m : Type u_2}
{n : Type u_5}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype n₁]
[Fintype n₂]
[Semiring R]
(A₁ : Matrix m n₁ R)
(A₂ : Matrix m n₂ R)
(B₁ : Matrix n₁ n R)
(B₂ : Matrix n₂ n R)
:
Matrix.fromColumns A₁ A₂ * Matrix.fromRows B₁ B₂ = A₁ * B₁ + A₂ * B₂
A column partitioned matrix mulitplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices
theorem
Matrix.fromColumns_mul_fromBlocks
{R : Type u_1}
{m : Type u_2}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype m₁]
[Fintype m₂]
[Semiring R]
(A₁ : Matrix m m₁ R)
(A₂ : Matrix m m₂ R)
(B₁₁ : Matrix m₁ n₁ R)
(B₁₂ : Matrix m₁ n₂ R)
(B₂₁ : Matrix m₂ n₁ R)
(B₂₂ : Matrix m₂ n₂ R)
:
Matrix.fromColumns A₁ A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = Matrix.fromColumns (A₁ * B₁₁ + A₂ * B₂₁) (A₁ * B₁₂ + A₂ * B₂₂)
A column partitioned matrix multipiled by a block matrix results in a column partioned matrix
theorem
Matrix.fromBlocks_mul_fromRows
{R : Type u_1}
{m₁ : Type u_3}
{m₂ : Type u_4}
{n : Type u_5}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype n₁]
[Fintype n₂]
[Semiring R]
(A₁ : Matrix n₁ n R)
(A₂ : Matrix n₂ n R)
(B₁₁ : Matrix m₁ n₁ R)
(B₁₂ : Matrix m₁ n₂ R)
(B₂₁ : Matrix m₂ n₁ R)
(B₂₂ : Matrix m₂ n₂ R)
:
Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * Matrix.fromRows A₁ A₂ = Matrix.fromRows (B₁₁ * A₁ + B₁₂ * A₂) (B₂₁ * A₁ + B₂₂ * A₂)
A block matrix mulitplied by a row partitioned matrix gives a row partitioned matrix
theorem
Matrix.fromColumns_mul_fromRows_eq_one_comm
{R : Type u_1}
{n : Type u_5}
{n₁ : Type u_6}
{n₂ : Type u_7}
[Fintype n]
[Fintype n₁]
[Fintype n₂]
[DecidableEq n]
[DecidableEq n₁]
[DecidableEq n₂]
[CommRing R]
(e : n ≃ n₁ ⊕ n₂)
(A₁ : Matrix n n₁ R)
(A₂ : Matrix n n₂ R)
(B₁ : Matrix n₁ n R)
(B₂ : Matrix n₂ n R)
:
Matrix.fromColumns A₁ A₂ * Matrix.fromRows B₁ B₂ = 1 ↔ Matrix.fromRows B₁ B₂ * Matrix.fromColumns A₁ A₂ = 1
Multiplication of a matrix by its inverse is commutative.
This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.
The condition e : n ≃ n₁ ⊕ n₂ states that fromColumns A₁ A₂ and fromRows B₁ B₂ are "square".
theorem
Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm
{R : Type u_1}
{n : Type u_5}
[Fintype n]
[DecidableEq n]
[CommRing R]
(p : n → Prop)
[DecidablePred p]
(A₁ : Matrix n { i : n // p i } R)
(A₂ : Matrix n { i : n // ¬p i } R)
(B₁ : Matrix { i : n // p i } n R)
(B₂ : Matrix { i : n // ¬p i } n R)
:
Matrix.fromColumns A₁ A₂ * Matrix.fromRows B₁ B₂ = 1 ↔ Matrix.fromRows B₁ B₂ * Matrix.fromColumns A₁ A₂ = 1