Block matrices and their determinant #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a predicate matrix.block_triangular saying a matrix
is block triangular, and proves the value of the determinant for various
matrices built out of blocks.
Main definitions #
matrix.block_triangularexpresses that aobyomatrix is block triangular, if the rows and columns are ordered according to some orderb : o → α
Main results #
matrix.det_of_block_triangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocksmatrix.det_of_upper_triangularandmatrix.det_of_lower_triangular: the determinant of a triangular matrix is the product of the entries along the diagonal
Tags #
matrix, diagonal, det, block triangular
@[protected, simp]
theorem
matrix.block_triangular.submatrix
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[has_lt α]
{f : n → m}
(h : M.block_triangular b) :
(M.submatrix f f).block_triangular (b ∘ f)
theorem
matrix.block_triangular_reindex_iff
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
[has_lt α]
{b : n → α}
{e : m ≃ n} :
(⇑(matrix.reindex e e) M).block_triangular b ↔ M.block_triangular (b ∘ ⇑e)
@[simp]
theorem
matrix.block_triangular_zero
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{b : m → α}
[has_lt α] :
0.block_triangular b
@[protected]
theorem
matrix.block_triangular.neg
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[has_lt α]
(hM : M.block_triangular b) :
(-M).block_triangular b
theorem
matrix.block_triangular.add
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M N : matrix m m R}
{b : m → α}
[has_lt α]
(hM : M.block_triangular b)
(hN : N.block_triangular b) :
(M + N).block_triangular b
theorem
matrix.block_triangular.sub
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M N : matrix m m R}
{b : m → α}
[has_lt α]
(hM : M.block_triangular b)
(hN : N.block_triangular b) :
(M - N).block_triangular b
theorem
matrix.block_triangular_diagonal
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{b : m → α}
[preorder α]
[decidable_eq m]
(d : m → R) :
theorem
matrix.block_triangular_block_diagonal'
{α : Type u_1}
{m' : α → Type u_6}
{R : Type v}
[comm_ring R]
[preorder α]
[decidable_eq α]
(d : Π (i : α), matrix (m' i) (m' i) R) :
theorem
matrix.block_triangular_block_diagonal
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
[preorder α]
[decidable_eq α]
(d : α → matrix m m R) :
theorem
matrix.block_triangular.mul
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{b : m → α}
[linear_order α]
[fintype m]
{M N : matrix m m R}
(hM : M.block_triangular b)
(hN : N.block_triangular b) :
(M * N).block_triangular b
theorem
matrix.upper_two_block_triangular
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[comm_ring R]
[preorder α]
(A : matrix m m R)
(B : matrix m n R)
(D : matrix n n R)
{a b : α}
(hab : a < b) :
(matrix.from_blocks A B 0 D).block_triangular (sum.elim (λ (i : m), a) (λ (j : n), b))
Determinant #
theorem
matrix.equiv_block_det
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
(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
@[simp]
theorem
matrix.det_to_square_block_id
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
(M : matrix m m R)
(i : m) :
(M.to_square_block id i).det = M i i
theorem
matrix.det_to_block
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
(M : matrix m m R)
(p : m → Prop)
[decidable_pred p] :
theorem
matrix.two_block_triangular_det
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
(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.two_block_triangular_det'
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
(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
@[protected]
theorem
matrix.block_triangular.det
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[decidable_eq α]
[linear_order α]
(hM : M.block_triangular b) :
M.det = (finset.image b finset.univ).prod (λ (a : α), (M.to_square_block b a).det)
theorem
matrix.block_triangular.det_fintype
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[decidable_eq α]
[fintype α]
[linear_order α]
(h : M.block_triangular b) :
M.det = finset.univ.prod (λ (k : α), (M.to_square_block b k).det)
theorem
matrix.det_of_upper_triangular
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
[decidable_eq m]
[fintype m]
[linear_order m]
(h : M.block_triangular id) :
M.det = finset.univ.prod (λ (i : m), M i i)
theorem
matrix.det_of_lower_triangular
{m : Type u_3}
{R : Type v}
[comm_ring R]
[decidable_eq m]
[fintype m]
[linear_order m]
(M : matrix m m R)
(h : M.block_triangular ⇑order_dual.to_dual) :
M.det = finset.univ.prod (λ (i : m), M i i)
Invertible #
theorem
matrix.block_triangular.to_block_inverse_mul_to_block_eq_one
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[linear_order α]
[invertible M]
(hM : M.block_triangular b)
(k : α) :
theorem
matrix.block_triangular.inv_to_block
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[linear_order α]
[invertible M]
(hM : M.block_triangular b)
(k : α) :
The inverse of an upper-left subblock of a block-triangular matrix M is the upper-left
subblock of M⁻¹.
def
matrix.block_triangular.invertible_to_block
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[linear_order α]
[invertible M]
(hM : M.block_triangular b)
(k : α) :
invertible (M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k))
An upper-left subblock of an invertible block-triangular matrix is invertible.
Equations
- hM.invertible_to_block k = (M.to_block (λ (i : m), b i < k) (λ (i : m), b i < k)).invertible_of_left_inverse ((⅟ M).to_block (λ (i : m), b i < k) (λ (i : m), b i < k)) _
theorem
matrix.to_block_inverse_eq_zero
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[linear_order α]
[invertible M]
(hM : M.block_triangular b)
(k : α) :
A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step
towards block_triangular.inv_to_block below.
theorem
matrix.block_triangular_inv_of_block_triangular
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[comm_ring R]
{M : matrix m m R}
{b : m → α}
[decidable_eq m]
[fintype m]
[linear_order α]
[invertible M]
(hM : M.block_triangular b) :
The inverse of a block-triangular matrix is block-triangular.