Documentation

Mathlib.LinearAlgebra.Matrix.SchurComplement

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 #

theorem Matrix.fromBlocks_eq_of_invertible₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α) [Invertible A] :
Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 0 (C * A) 1 * Matrix.fromBlocks A 0 0 (D - C * A * B) * Matrix.fromBlocks 1 (A * B) 0 1

LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement.

theorem Matrix.fromBlocks_eq_of_invertible₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
Matrix.fromBlocks A B C D = Matrix.fromBlocks 1 (B * D) 0 1 * Matrix.fromBlocks (A - B * D * C) 0 0 D * Matrix.fromBlocks 1 0 (D * C) 1

LDU decomposition of a block matrix with an invertible bottom-right corner, using the Schur complement.

Block triangular matrices #

def Matrix.fromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] :

An upper-block-triangular matrix is invertible if its diagonal is.

Equations
Instances For
    def Matrix.fromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] :

    A lower-block-triangular matrix is invertible if its diagonal is.

    Equations
    Instances For
      theorem Matrix.invOf_fromBlocks_zero₂₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (Matrix.fromBlocks A B 0 D)] :
      theorem Matrix.invOf_fromBlocks_zero₁₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (Matrix.fromBlocks A 0 C D)] :
      def Matrix.invertibleOfFromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible (Matrix.fromBlocks A B 0 D)] :

      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
        def Matrix.invertibleOfFromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible (Matrix.fromBlocks A 0 C D)] :

        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
          def Matrix.fromBlocksZero₂₁InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) :

          invertibleOfFromBlocksZero₂₁Invertible and Matrix.fromBlocksZero₂₁Invertible form an equivalence.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Matrix.fromBlocksZero₁₂InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) :

            invertibleOfFromBlocksZero₁₂Invertible and Matrix.fromBlocksZero₁₂Invertible form an equivalence.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Matrix.isUnit_fromBlocks_zero₂₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α} :

              An upper block-triangular matrix is invertible iff both elements of its diagonal are.

              This is a propositional form of Matrix.fromBlocksZero₂₁InvertibleEquiv.

              @[simp]
              theorem Matrix.isUnit_fromBlocks_zero₁₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} :

              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.

              theorem Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) (hAD : IsUnit A IsUnit D) :

              An expression for the inverse of an upper block-triangular matrix, when either both elements of diagonal are invertible, or both are not.

              theorem Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) (hAD : IsUnit A IsUnit D) :

              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 #

              def Matrix.fromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * D * C)] :

              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
                def Matrix.fromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * A * B)] :

                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
                  theorem Matrix.invOf_fromBlocks₂₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * D * C)] [Invertible (Matrix.fromBlocks A B C D)] :
                  (Matrix.fromBlocks A B C D) = Matrix.fromBlocks ((A - B * D * C)) (-((A - B * D * C) * B * D)) (-(D * C * (A - B * D * C))) (D + D * C * (A - B * D * C) * B * D)
                  theorem Matrix.invOf_fromBlocks₁₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * A * B)] [Invertible (Matrix.fromBlocks A B C D)] :
                  (Matrix.fromBlocks A B C D) = Matrix.fromBlocks (A + A * B * (D - C * A * B) * C * A) (-(A * B * (D - C * A * B))) (-((D - C * A * B) * C * A)) (D - C * A * B)
                  def Matrix.invertibleOfFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (Matrix.fromBlocks A B C D)] :
                  Invertible (A - B * D * C)

                  If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Matrix.invertibleOfFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (Matrix.fromBlocks A B C D)] :
                    Invertible (D - C * A * B)

                    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
                      def Matrix.invertibleEquivFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :

                      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
                        def Matrix.invertibleEquivFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] :

                        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
                          theorem Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible D] :
                          IsUnit (Matrix.fromBlocks A B C D) IsUnit (A - B * D * C)

                          If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding schur complement is.

                          theorem Matrix.isUnit_fromBlocks_iff_of_invertible₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible A] :
                          IsUnit (Matrix.fromBlocks A B C D) IsUnit (D - C * A * B)

                          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 #

                          theorem Matrix.det_fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] :
                          (Matrix.fromBlocks A B C D).det = A.det * (D - C * A * B).det

                          Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.

                          @[simp]
                          theorem Matrix.det_fromBlocks_one₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) :
                          (Matrix.fromBlocks 1 B C D).det = (D - C * B).det
                          theorem Matrix.det_fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
                          (Matrix.fromBlocks A B C D).det = D.det * (A - B * D * C).det

                          Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.

                          @[simp]
                          theorem Matrix.det_fromBlocks_one₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) :
                          (Matrix.fromBlocks A B C 1).det = (A - B * C).det
                          theorem Matrix.det_one_add_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
                          (1 + A * B).det = (1 + B * A).det

                          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.

                          theorem Matrix.det_mul_add_one_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
                          (A * B + 1).det = (B * A + 1).det

                          Alternate statement of the Weinstein–Aronszajn identity

                          theorem Matrix.det_one_sub_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
                          (1 - A * B).det = (1 - B * A).det
                          theorem Matrix.det_one_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] (u : mα) (v : mα) :
                          (1 + Matrix.col ι u * Matrix.row ι v).det = 1 + Matrix.dotProduct v u

                          A special case of the Matrix determinant lemma for when A = I.

                          theorem Matrix.det_add_col_mul_row {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] {A : Matrix m m α} (hA : IsUnit A.det) (u : mα) (v : mα) :
                          (A + Matrix.col ι u * Matrix.row ι v).det = A.det * (1 + Matrix.row ι v * A⁻¹ * Matrix.col ι u).det

                          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.

                          theorem Matrix.det_add_mul {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α) (hA : IsUnit A.det) :
                          (A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

                          A generalization of the Matrix determinant lemma

                          Lemmas about and and other StarOrderedRings #

                          theorem Matrix.schur_complement_eq₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (x : m𝕜) (y : n𝕜) [Invertible A] (hA : A.IsHermitian) :
                          Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star (x + (A⁻¹ * B).mulVec y)) A) (x + (A⁻¹ * B).mulVec y) + Matrix.dotProduct (Matrix.vecMul (star y) (D - B.conjTranspose * A⁻¹ * B)) y
                          theorem Matrix.schur_complement_eq₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (x : m𝕜) (y : n𝕜) [Invertible D] (hD : D.IsHermitian) :
                          Matrix.dotProduct (Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D)) (Sum.elim x y) = Matrix.dotProduct (Matrix.vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D) ((D⁻¹ * B.conjTranspose).mulVec x + y) + Matrix.dotProduct (Matrix.vecMul (star x) (A - B * D⁻¹ * B.conjTranspose)) x
                          theorem Matrix.IsHermitian.fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [Fintype m] [DecidableEq m] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : A.IsHermitian) :
                          (Matrix.fromBlocks A B B.conjTranspose D).IsHermitian (D - B.conjTranspose * A⁻¹ * B).IsHermitian
                          theorem Matrix.IsHermitian.fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [StarRing 𝕜] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : D.IsHermitian) :
                          (Matrix.fromBlocks A B B.conjTranspose D).IsHermitian (A - B * D⁻¹ * B.conjTranspose).IsHermitian
                          theorem Matrix.PosSemidef.fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [Fintype m] [DecidableEq m] [Fintype n] {A : Matrix m m 𝕜} (B : Matrix m n 𝕜) (D : Matrix n n 𝕜) (hA : A.PosDef) [Invertible A] :
                          (Matrix.fromBlocks A B B.conjTranspose D).PosSemidef (D - B.conjTranspose * A⁻¹ * B).PosSemidef
                          theorem Matrix.PosSemidef.fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {𝕜 : Type u_5} [CommRing 𝕜] [PartialOrder 𝕜] [StarRing 𝕜] [StarOrderedRing 𝕜] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix m m 𝕜) (B : Matrix m n 𝕜) {D : Matrix n n 𝕜} (hD : D.PosDef) [Invertible D] :
                          (Matrix.fromBlocks A B B.conjTranspose D).PosSemidef (A - B * D⁻¹ * B.conjTranspose).PosSemidef