2×2 block matrices and the Schur complement #
This file proves properties of 2×2 block matrices [A B; C D]
that relate to the Schur complement
D - C*A⁻¹*B
.
Some of the results here generalize to 2×2 matrices in a category, rather than just a ring. A few
results in this direction can be found in the file CateogryTheory.Preadditive.Biproducts
,
especially the declarations CategoryTheory.Biprod.gaussian
and CategoryTheory.Biprod.isoElim
.
Compare with Matrix.invertibleOfFromBlocks₁₁Invertible
.
Main results #
Matrix.det_fromBlocks₁₁
,Matrix.det_fromBlocks₂₂
: determinant of a block matrix in terms of the Schur complement.Matrix.invOf_fromBlocks_zero₂₁_eq
,Matrix.invOf_fromBlocks_zero₁₂_eq
: the inverse of a block triangular matrix.Matrix.isUnit_fromBlocks_zero₂₁
,Matrix.isUnit_fromBlocks_zero₁₂
: invertibility of a block triangular matrix.Matrix.det_one_add_mul_comm
: the Weinstein–Aronszajn identity.Matrix.PosSemidef.fromBlocks₁₁
andMatrix.PosSemidef.fromBlocks₂₂
: If a matrixA
is positive definite, then[A B; Bᴴ D]
is positive semidefinite if and only ifD - Bᴴ A⁻¹ B
is positive semidefinite.
LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement.
LDU decomposition of a block matrix with an invertible bottom-right corner, using the Schur complement.
Block triangular matrices #
An upper-block-triangular matrix is invertible if its diagonal is.
Equations
- A.fromBlocksZero₂₁Invertible B D = (Matrix.fromBlocks A B 0 D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟A) (-(⅟A * B * ⅟D)) 0 ⅟D) ⋯
Instances For
A lower-block-triangular matrix is invertible if its diagonal is.
Equations
- A.fromBlocksZero₁₂Invertible C D = (Matrix.fromBlocks A 0 C D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟A) 0 (-(⅟D * C * ⅟A)) ⅟D) ⋯
Instances For
Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).
Equations
- A.invertibleOfFromBlocksZero₂₁Invertible B D = (A.invertibleOfLeftInverse (⅟(Matrix.fromBlocks A B 0 D)).toBlocks₁₁ ⋯, D.invertibleOfRightInverse (⅟(Matrix.fromBlocks A B 0 D)).toBlocks₂₂ ⋯)
Instances For
Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).
Equations
- A.invertibleOfFromBlocksZero₁₂Invertible C D = (A.invertibleOfRightInverse (⅟(Matrix.fromBlocks A 0 C D)).toBlocks₁₁ ⋯, D.invertibleOfLeftInverse (⅟(Matrix.fromBlocks A 0 C D)).toBlocks₂₂ ⋯)
Instances For
invertibleOfFromBlocksZero₂₁Invertible
and Matrix.fromBlocksZero₂₁Invertible
form
an equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
invertibleOfFromBlocksZero₁₂Invertible
and Matrix.fromBlocksZero₁₂Invertible
form
an equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An upper block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of Matrix.fromBlocksZero₂₁InvertibleEquiv
.
A lower block-triangular matrix is invertible iff both elements of its diagonal are.
This is a propositional form of Matrix.fromBlocksZero₁₂InvertibleEquiv
forms an iff
.
An expression for the inverse of an upper block-triangular matrix, when either both elements of diagonal are invertible, or both are not.
An expression for the inverse of a lower block-triangular matrix, when either both elements of diagonal are invertible, or both are not.
2×2 block matrices #
General 2×2 block matrices #
A block matrix is invertible if the bottom right corner and the corresponding schur complement is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A block matrix is invertible if the top left corner and the corresponding schur complement is.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.
Equations
Instances For
If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.
Equations
- A.invertibleOfFromBlocks₁₁Invertible B C D = D.invertibleOfFromBlocks₂₂Invertible C B A
Instances For
Matrix.invertibleOfFromBlocks₂₂Invertible
and Matrix.fromBlocks₂₂Invertible
as an
equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matrix.invertibleOfFromBlocks₁₁Invertible
and Matrix.fromBlocks₁₁Invertible
as an
equivalence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.
If the top-right element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.
Lemmas about Matrix.det
#
Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.
Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.
The Weinstein–Aronszajn identity. Note the 1
on the LHS is of shape m×m, while the 1
on
the RHS is of shape n×n.
A special case of the Matrix determinant lemma for when A = I
.
The Matrix determinant lemma
TODO: show the more general version without hA : IsUnit A.det
as
(A + col u * row v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u
.
A generalization of the Matrix determinant lemma
Lemmas about ℝ
and ℂ
and other StarOrderedRing
s #
Equations
- Matrix.«term_⊕ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_⊕ᵥ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ᵥ ") (Lean.ParserDescr.cat `term 66))