# Documentation

Mathlib.Data.Matrix.ColumnRowPartitioned

# 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) :
Matrix (m₁ 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]

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) :
Matrix m (n₁ 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₂)]

Instances For
def Matrix.toColumns₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
Matrix m n₁ R

Given a column partitioned matrix extract the first column

Instances For
def Matrix.toColumns₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
Matrix m n₂ R

Given a column partitioned matrix extract the second column

Instances For
def Matrix.toRows₁ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) :
Matrix m₁ n R

Given a row partitioned matrix extract the first row

Instances For
def Matrix.toRows₂ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) :
Matrix m₂ n R

Given a row partitioned matrix extract the second row

Instances For
@[simp]
theorem Matrix.fromRows_apply_inl {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) (i : m₁) (j : n) :
Matrix.fromRows A₁ A₂ () j = A₁ i j
@[simp]
theorem Matrix.fromRows_apply_inr {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) (i : m₂) (j : n) :
Matrix.fromRows A₁ A₂ () j = A₂ i j
@[simp]
theorem Matrix.fromColumns_apply_inl {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) (i : m) (j : n₁) :
Matrix.fromColumns A₁ A₂ i () = A₁ i j
@[simp]
theorem Matrix.fromColumns_apply_inr {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) (i : m) (j : n₂) :
Matrix.fromColumns A₁ A₂ i () = A₂ i j
@[simp]
theorem Matrix.toRows₁_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) (i : m₁) (j : n) :
= A () j
@[simp]
theorem Matrix.toRows₂_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) (i : m₂) (j : n) :
= A () j
@[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) :
@[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) :
@[simp]
theorem Matrix.toColumns₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) (i : m) (j : n₁) :
= A i ()
@[simp]
theorem Matrix.toColumns₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) (i : m) (j : n₂) :
= A i ()
@[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) :
= 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) :
= A₂
@[simp]
theorem Matrix.fromColumns_toColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
@[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) :
= 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.fromColumns_ext_iff {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) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
= A₁ = B₁ A₂ = B₂
theorem Matrix.fromRows_ext_iff {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) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :
Matrix.fromRows A₁ A₂ = Matrix.fromRows B₁ B₂ A₁ = B₁ A₂ = B₂
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) :
=
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) :
@[simp]
theorem Matrix.fromRows_mul {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [] [] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
Matrix.fromRows A₁ A₂ * B = Matrix.fromRows (A₁ * B) (A₂ * B)
@[simp]
theorem Matrix.mul_fromColumns {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [] [] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
A * = Matrix.fromColumns (A * B₁) (A * B₂)
@[simp]
theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [] :
= 0
@[simp]
theorem Matrix.fromColumns_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [] :
= 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} [] [] (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.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₂] [] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
* 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₂] [] (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.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₂] [] (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₂] [] [] [] [] (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.fromRows B₁ B₂ = 1 Matrix.fromRows B₁ B₂ * = 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} [] [] [] (p : nProp) [] (A₁ : Matrix n { i // p i } R) (A₂ : Matrix n { i // ¬p i } R) (B₁ : Matrix { i // p i } n R) (B₂ : Matrix { i // ¬p i } n R) :
* Matrix.fromRows B₁ B₂ = 1 Matrix.fromRows B₁ B₂ * = 1
theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :