# mathlibdocumentation

data.matrix.block

# Block Matrices #

## Main definitions #

• matrix.from_blocks: build a block matrix out of 4 blocks
• matrix.to_blocks₁₁, matrix.to_blocks₁₂, matrix.to_blocks₂₁, matrix.to_blocks₂₂: extract each of the four blocks from matrix.from_blocks.
• matrix.block_diagonal: block diagonal of equally sized blocks
• matrix.block_diagonal': block diagonal of unequally sized blocks
def matrix.from_blocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
matrix (n o) (l m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Equations
@[simp]
theorem matrix.from_blocks_apply₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) (i : n) (j : l) :
A.from_blocks B C D (sum.inl i) (sum.inl j) = A i j
@[simp]
theorem matrix.from_blocks_apply₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) (i : n) (j : m) :
A.from_blocks B C D (sum.inl i) (sum.inr j) = B i j
@[simp]
theorem matrix.from_blocks_apply₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) (i : o) (j : l) :
A.from_blocks B C D (sum.inr i) (sum.inl j) = C i j
@[simp]
theorem matrix.from_blocks_apply₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) (i : o) (j : m) :
A.from_blocks B C D (sum.inr i) (sum.inr j) = D i j
def matrix.to_blocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : matrix (n o) (l m) α) :
l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.

Equations
def matrix.to_blocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : matrix (n o) (l m) α) :
m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.

Equations
def matrix.to_blocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : matrix (n o) (l m) α) :
l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.

Equations
def matrix.to_blocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : matrix (n o) (l m) α) :
m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.

Equations
theorem matrix.from_blocks_to_blocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : matrix (n o) (l m) α) :
@[simp]
theorem matrix.to_blocks_from_blocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
@[simp]
theorem matrix.to_blocks_from_blocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
@[simp]
theorem matrix.to_blocks_from_blocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
@[simp]
theorem matrix.to_blocks_from_blocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
theorem matrix.from_blocks_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} {β : Type u_10} (A : l α) (B : m α) (C : l α) (D : m α) (f : α → β) :
(A.from_blocks B C D).map f = (A.map f).from_blocks (B.map f) (C.map f) (D.map f)
theorem matrix.from_blocks_transpose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (A : l α) (B : m α) (C : l α) (D : m α) :
(A.from_blocks B C D) = B D
theorem matrix.from_blocks_conj_transpose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [has_star α] (A : l α) (B : m α) (C : l α) (D : m α) :
(A.from_blocks B C D) = B D
def matrix.is_two_block_diagonal {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [has_zero α] (A : matrix (n o) (l m) α) :
Prop

A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish

Equations
def matrix.to_block {m : Type u_2} {n : Type u_3} {α : Type u_9} (M : n α) (p : m → Prop) (q : n → Prop) :
matrix {a // p a} {a // q a} α

Let p pick out certain rows and q pick out certain columns of a matrix M. Then to_block M p q is the corresponding block matrix.

Equations
@[simp]
theorem matrix.to_block_apply {m : Type u_2} {n : Type u_3} {α : Type u_9} (M : n α) (p : m → Prop) (q : n → Prop) (i : {a // p a}) (j : {a // q a}) :
M.to_block p q i j = M i j
def matrix.to_square_block {m : Type u_2} {α : Type u_9} (M : m α) {n : } (b : m → fin n) (k : fin n) :
matrix {a // b a = k} {a // b a = k} α

Let b map rows and columns of a square matrix M to blocks. Then to_square_block M b k is the block k matrix.

Equations
@[simp]
theorem matrix.to_square_block_def {m : Type u_2} {α : Type u_9} (M : m α) {n : } (b : m → fin n) (k : fin n) :
k = λ (i j : {a // b a = k}), M i j
def matrix.to_square_block' {m : Type u_2} {α : Type u_9} (M : m α) (b : m → ) (k : ) :
matrix {a // b a = k} {a // b a = k} α

Alternate version with b : m → nat. Let b map rows and columns of a square matrix M to blocks. Then to_square_block' M b k is the block k matrix.

Equations
@[simp]
theorem matrix.to_square_block_def' {m : Type u_2} {α : Type u_9} (M : m α) (b : m → ) (k : ) :
k = λ (i j : {a // b a = k}), M i j
def matrix.to_square_block_prop {m : Type u_2} {α : Type u_9} (M : m α) (p : m → Prop) :
matrix {a // p a} {a // p a} α

Let p pick out certain rows and columns of a square matrix M. Then to_square_block_prop M p is the corresponding block matrix.

Equations
@[simp]
theorem matrix.to_square_block_prop_def {m : Type u_2} {α : Type u_9} (M : m α) (p : m → Prop) :
= λ (i j : {a // p a}), M i j
theorem matrix.from_blocks_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [semiring α] (x : α) (A : l α) (B : m α) (C : l α) (D : m α) :
x A.from_blocks B C D = (x A).from_blocks (x B) (x C) (x D)
theorem matrix.from_blocks_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [semiring α] (A : l α) (B : m α) (C : l α) (D : m α) (A' : l α) (B' : m α) (C' : l α) (D' : m α) :
A.from_blocks B C D + A'.from_blocks B' C' D' = (A + A').from_blocks (B + B') (C + C') (D + D')
theorem matrix.from_blocks_multiply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [semiring α] {p : Type u_5} {q : Type u_6} [fintype l] [fintype m] (A : l α) (B : m α) (C : l α) (D : m α) (A' : p α) (B' : q α) (C' : p α) (D' : q α) :
A.from_blocks B C D A'.from_blocks B' C' D' = (A A' + B C').from_blocks (A B' + B D') (C A' + D C') (C B' + D D')
@[simp]
theorem matrix.from_blocks_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_9} [semiring α] [decidable_eq l] [decidable_eq m] (d₁ : l → α) (d₂ : m → α) :
0 0 (matrix.diagonal d₂) = matrix.diagonal (sum.elim d₁ d₂)
@[simp]
theorem matrix.from_blocks_one {l : Type u_1} {m : Type u_2} {α : Type u_9} [semiring α] [decidable_eq l] [decidable_eq m] :
1.from_blocks 0 0 1 = 1
def matrix.block_diagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [has_zero α] :
matrix (m × o) (n × o) α

matrix.block_diagonal M turns a homogenously-indexed collection of matrices M : o → matrix m n α' into a m × o-by-n × o block matrix which has the entries of M along the diagonal and zero elsewhere.

See also matrix.block_diagonal' if the matrices may not have the same size everywhere.

Equations
• (i, k) (j, k') = ite (k = k') (M k i j) 0
theorem matrix.block_diagonal_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [has_zero α] (ik : m × o) (jk : n × o) :
jk = ite (ik.snd = jk.snd) (M ik.snd ik.fst jk.fst) 0
@[simp]
theorem matrix.block_diagonal_apply_eq {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [has_zero α] (i : m) (j : n) (k : o) :
(i, k) (j, k) = M k i j
theorem matrix.block_diagonal_apply_ne {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [has_zero α] (i : m) (j : n) {k k' : o} (h : k k') :
(i, k) (j, k') = 0
theorem matrix.block_diagonal_map {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} {β : Type u_10} (M : o → n α) [decidable_eq o] [has_zero α] [has_zero β] (f : α → β) (hf : f 0 = 0) :
f = matrix.block_diagonal (λ (k : o), (M k).map f)
@[simp]
theorem matrix.block_diagonal_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [has_zero α] :
= matrix.block_diagonal (λ (k : o), (M k))
@[simp]
theorem matrix.block_diagonal_conj_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} [decidable_eq o] {α : Type u_1} [semiring α] [star_ring α] (M : o → n α) :
= matrix.block_diagonal (λ (k : o), (M k))
@[simp]
theorem matrix.block_diagonal_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [decidable_eq o] [has_zero α] :
@[simp]
theorem matrix.block_diagonal_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_9} [decidable_eq o] [has_zero α] [decidable_eq m] (d : o → m → α) :
matrix.block_diagonal (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : m × o), d ik.snd ik.fst)
@[simp]
theorem matrix.block_diagonal_one {m : Type u_2} {o : Type u_4} {α : Type u_9} [decidable_eq o] [has_zero α] [decidable_eq m] [has_one α] :
@[simp]
theorem matrix.block_diagonal_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M N : o → n α) [decidable_eq o] [add_monoid α] :
@[simp]
theorem matrix.block_diagonal_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] [add_group α] :
@[simp]
theorem matrix.block_diagonal_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M N : o → n α) [decidable_eq o] [add_group α] :
@[simp]
theorem matrix.block_diagonal_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] {p : Type u_1} [fintype n] [fintype o] [semiring α] (N : o → p α) :
matrix.block_diagonal (λ (k : o), M k N k) =
@[simp]
theorem matrix.block_diagonal_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} (M : o → n α) [decidable_eq o] {R : Type u_1} [semiring R] [ α] (x : R) :
def matrix.block_diagonal' {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] :
matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α

matrix.block_diagonal' M turns M : Π i, matrix (m i) (n i) α into a Σ i, m i-by-Σ i, n i block matrix which has the entries of M along the diagonal and zero elsewhere.

This is the dependently-typed version of matrix.block_diagonal.

Equations
theorem matrix.block_diagonal'_eq_block_diagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [decidable_eq o] [has_zero α] (M : o → n α) {k k' : o} (i : m) (j : n) :
(i, k) (j, k') = k, i⟩ k', j⟩
theorem matrix.block_diagonal'_minor_eq_block_diagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_9} [decidable_eq o] [has_zero α] (M : o → n α) :
theorem matrix.block_diagonal'_apply {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] (ik : Σ (i : o), m' i) (jk : Σ (i : o), n' i) :
jk = dite (ik.fst = jk.fst) (λ (h : ik.fst = jk.fst), M ik.fst ik.snd (cast _ jk.snd)) (λ (h : ¬ik.fst = jk.fst), 0)
@[simp]
theorem matrix.block_diagonal'_apply_eq {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] (k : o) (i : m' k) (j : n' k) :
k, i⟩ k, j⟩ = M k i j
theorem matrix.block_diagonal'_apply_ne {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] {k k' : o} (i : m' k) (j : n' k') (h : k k') :
k, i⟩ k', j⟩ = 0
theorem matrix.block_diagonal'_map {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} {β : Type u_10} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] [has_zero β] (f : α → β) (hf : f 0 = 0) :
= matrix.block_diagonal' (λ (k : o), (M k).map f)
@[simp]
theorem matrix.block_diagonal'_transpose {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [has_zero α] :
= matrix.block_diagonal' (λ (k : o), (M k))
@[simp]
theorem matrix.block_diagonal'_conj_transpose {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} [decidable_eq o] {α : Type u_1} [semiring α] [star_ring α] (M : Π (i : o), matrix (m' i) (n' i) α) :
= matrix.block_diagonal' (λ (k : o), (M k))
@[simp]
theorem matrix.block_diagonal'_zero {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} [decidable_eq o] [has_zero α] :
@[simp]
theorem matrix.block_diagonal'_diagonal {o : Type u_4} {m' : o → Type u_5} {α : Type u_9} [decidable_eq o] [has_zero α] [Π (i : o), decidable_eq (m' i)] (d : Π (i : o), m' i → α) :
matrix.block_diagonal' (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : Σ (i : o), m' i), d ik.fst ik.snd)
@[simp]
theorem matrix.block_diagonal'_one {o : Type u_4} {m' : o → Type u_5} {α : Type u_9} [decidable_eq o] [has_zero α] [Π (i : o), decidable_eq (m' i)] [has_one α] :
@[simp]
theorem matrix.block_diagonal'_add {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M N : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [add_monoid α] :
@[simp]
theorem matrix.block_diagonal'_neg {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [add_group α] :
@[simp]
theorem matrix.block_diagonal'_sub {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M N : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] [add_group α] :
@[simp]
theorem matrix.block_diagonal'_mul {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] {p : o → Type u_1} [semiring α] [Π (i : o), fintype (n' i)] [fintype o] (N : Π (i : o), matrix (n' i) (p i) α) :
matrix.block_diagonal' (λ (k : o), M k N k) =
@[simp]
theorem matrix.block_diagonal'_smul {o : Type u_4} {m' : o → Type u_5} {n' : o → Type u_6} {α : Type u_9} (M : Π (i : o), matrix (m' i) (n' i) α) [decidable_eq o] {R : Type u_1} [semiring R] [ α] (x : R) :