mathlib documentation

linear_algebra.matrix.block

Block matrices and their determinant #

This file defines a predicate matrix.block_triangular_matrix saying a matrix is block triangular, and proves the value of the determinant for various matrices built out of blocks.

Main definitions #

Main results #

Tags #

matrix, diagonal, det, block triangular

theorem matrix.det_to_block {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (p : m → Prop) [decidable_pred p] :
M.det = ((M.to_block p p).from_blocks (M.to_block p (λ (j : m), ¬p j)) (M.to_block (λ (j : m), ¬p j) p) (M.to_block (λ (j : m), ¬p j) (λ (j : m), ¬p j))).det
theorem matrix.det_to_square_block {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (k : fin n) :
(M.to_square_block b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem matrix.det_to_square_block' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (k : ) :
(M.to_square_block' b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem matrix.two_block_triangular_det {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (p : m → Prop) [decidable_pred p] (h : ∀ (i : m), ¬p i∀ (j : m), p jM i j = 0) :
M.det = ((M.to_square_block_prop p).det) * (M.to_square_block_prop (λ (i : m), ¬p i)).det
theorem matrix.equiv_block_det {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {p q : m → Prop} [decidable_pred p] [decidable_pred q] (e : ∀ (x : m), q x p x) :
theorem matrix.to_square_block_det'' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (k : fin n) :
(M.to_square_block b k).det = (M.to_square_block' (λ (i : m), (b i)) k).det
def matrix.block_triangular_matrix' {R : Type v} [comm_ring R] {o : Type u_1} (M : matrix o o R) {n : } (b : o → fin n) :
Prop

Let b map rows and columns of a square matrix M to n blocks. Then block_triangular_matrix' M n b says the matrix is block triangular.

Equations
theorem matrix.upper_two_block_triangular' {R : Type v} [comm_ring R] {m : Type u_1} {n : Type u_2} (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix' (sum.elim (λ (i : m), 0) (λ (j : n), 1))
def matrix.block_triangular_matrix {R : Type v} [comm_ring R] {o : Type u_1} (M : matrix o o R) (b : o → ) :
Prop

Let b map rows and columns of a square matrix M to blocks indexed by s. Then block_triangular_matrix M n b says the matrix is block triangular.

Equations
theorem matrix.upper_two_block_triangular {R : Type v} [comm_ring R] {m : Type u_1} {n : Type u_2} (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix (sum.elim (λ (i : m), 0) (λ (j : n), 1))
theorem matrix.det_of_block_triangular_matrix {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (h : M.block_triangular_matrix b) (n : ) (hn : ∀ (i : m), b i < n) :
M.det = ∏ (k : ) in finset.range n, (M.to_square_block' b k).det
theorem matrix.det_of_block_triangular_matrix'' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) (b : m → ) (h : M.block_triangular_matrix b) :
theorem matrix.det_of_block_triangular_matrix' {m : Type u_1} [decidable_eq m] [fintype m] {R : Type v} [comm_ring R] (M : matrix m m R) {n : } (b : m → fin n) (h : M.block_triangular_matrix' b) :
M.det = ∏ (k : fin n), (M.to_square_block b k).det
theorem matrix.det_of_upper_triangular {R : Type v} [comm_ring R] {n : } (M : matrix (fin n) (fin n) R) (h : ∀ (i j : fin n), j < iM i j = 0) :
M.det = ∏ (i : fin n), M i i
theorem matrix.det_of_lower_triangular {R : Type v} [comm_ring R] {n : } (M : matrix (fin n) (fin n) R) (h : ∀ (i j : fin n), i < jM i j = 0) :
M.det = ∏ (i : fin n), M i i