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 #
matrix.block_triangular_matrixexpresses that aobyomatrix is block triangular, if the rows and columns are ordered according to some orderb : o → ℕ
Main results #
det_of_block_triangular_matrix: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocksdet_of_upper_triangularanddet_of_lower_triangular: the determinant of a triangular matrix is the product of the entries along the diagonal
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] :
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 j → M 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) :
(M.to_square_block_prop p).det = (M.to_square_block_prop q).det
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
- M.block_triangular_matrix' b = ∀ (i j : o), b j < b i → M i j = 0
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
- M.block_triangular_matrix b = ∀ (i j : o), b j < b i → M i j = 0
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) :
M.det = ∏ (k : ℕ) in finset.image b finset.univ, (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)
{n : ℕ}
(b : m → fin n)
(h : M.block_triangular_matrix' b) :
M.det = ∏ (k : fin n), (M.to_square_block b k).det