Schur complements and rank-one inverse updates

Generalized Schur complements of positive-semidefinite block matrices are positive semidefinite. The inverse used in the complement need only be Hermitian and satisfy P * D * P = P; in particular the result applies to a singular block's pseudoinverse.

For a square matrix A and an index i, write B for the principal submatrix of A on the indices other than i. When B is invertible, the reciprocal of the diagonal entry (A⁻¹) i i is the scalar Schur complement A i i - aᵢ ⬝ᵥ B⁻¹ *ᵥ aⁱ of B in A, where aᵢ and aⁱ are the i-th row and column of A with the entry A i i removed. This holds also when A is singular, both sides then being zero, and when i is the only index, B then being empty.

For an invertible matrix A, the Sherman–Morrison formula expresses the inverse of A + vecMulVec u v in terms of A⁻¹. The scalar 1 + v ⬝ᵥ (A⁻¹ *ᵥ u) is a unit exactly when the perturbed matrix is invertible. These results specialize Mathlib's Matrix.det_add_replicateCol_mul_replicateRow and Matrix.add_mul_mul_inv_eq_sub to a single column and row, over any commutative ring; the scalar inverse is Ring.inverse.

Main results

• Matrix.PosSemidef.schur_complement₂₂ and Matrix.PosSemidef.schur_complement₁₁: positivity of generalized Schur complements, without invertibility of the pivot block.
• Matrix.inv_inv_apply_self_eq_sub: the reciprocal of (A⁻¹) i i is the scalar Schur complement of the complementary principal block, whenever that block is invertible.
• Matrix.PosDef.inv_inv_apply_self_eq_sub: the same identity for positive-definite matrices, whose principal blocks are always invertible.
• Matrix.isUnit_add_vecMulVec_iff: a rank-one update is invertible exactly when its Sherman–Morrison denominator is a unit.
• Matrix.inv_add_vecMulVec: the Sherman–Morrison inverse formula over a commutative ring.

References

• R. A. Horn, C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press, 2013, §0.7.4 (the Sherman–Morrison–Woodbury formula).

theorem Matrix.PosSemidef.schur_complement₂₂ {m : Type u_1} {n : Type u_2} {R : Type u_3} [Ring R] [PartialOrder R] [StarRing R] [Finite m] [Fintype n] {A : Matrix m m R} {B : Matrix m n R} {D P : Matrix n n R} (h : (fromBlocks A B B.conjTranspose D).PosSemidef) (hP : P.IsHermitian) (hPDP : P * D * P = P) : (A - B * P * B.conjTranspose).PosSemidef

A generalized Schur complement of the bottom-right block of a positive-semidefinite matrix is positive semidefinite. Only the Hermitian property and the second generalized-inverse equation are needed, so the block may be singular.

theorem Matrix.PosSemidef.schur_complement₁₁ {m : Type u_1} {n : Type u_2} {R : Type u_3} [Ring R] [PartialOrder R] [StarRing R] [Fintype m] [Finite n] {A P : Matrix m m R} {B : Matrix m n R} {D : Matrix n n R} (h : (fromBlocks A B B.conjTranspose D).PosSemidef) (hP : P.IsHermitian) (hPAP : P * A * P = P) : (D - B.conjTranspose * P * B).PosSemidef

A generalized Schur complement of the top-left block of a positive-semidefinite matrix is positive semidefinite, including when that block is singular.

theorem Matrix.isUnit_add_vecMulVec_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n R) (hA : IsUnit A) (u v : n → R) : IsUnit (A + vecMulVec u v) ↔ IsUnit (1 + v ⬝ᵥ A⁻¹.mulVec u)

A rank-one perturbation of an invertible matrix is invertible exactly when its Sherman–Morrison denominator is a unit.

theorem Matrix.inv_add_vecMulVec {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (A : Matrix n n R) (hA : IsUnit A) (u v : n → R) (hd : IsUnit (1 + v ⬝ᵥ A⁻¹.mulVec u)) : (A + vecMulVec u v)⁻¹ = A⁻¹ - Ring.inverse (1 + v ⬝ᵥ A⁻¹.mulVec u) • vecMulVec (A⁻¹.mulVec u) (vecMul v A⁻¹)

Sherman–Morrison formula over a commutative ring. The rank-one correction is the outer product of the updated column and row, divided by the scalar denominator.

theorem Matrix.inv_inv_apply_self_eq_sub {n : Type u_1} {K : Type u_2} [Fintype n] [DecidableEq n] [Field K] (A : Matrix n n K) (i : n) (hB : IsUnit (A.submatrix Subtype.val Subtype.val).det) : (A⁻¹ i i)⁻¹ = A i i - (fun (a : { a : n // a ≠ i }) => A i ↑a) ⬝ᵥ (A.submatrix Subtype.val Subtype.val)⁻¹.mulVec fun (b : { a : n // a ≠ i }) => A (↑b) i

The reciprocal of a diagonal entry (A⁻¹) i i of the inverse of a square matrix is the scalar Schur complement of the principal block of A away from i, provided that block is invertible. Both sides vanish when A is singular.

theorem Matrix.PosDef.inv_inv_apply_self_eq_sub {n : Type u_1} [Fintype n] [DecidableEq n] {A : Matrix n n ℝ} (hA : A.PosDef) (i : n) : (A⁻¹ i i)⁻¹ = A i i - (fun (a : { a : n // a ≠ i }) => A i ↑a) ⬝ᵥ (A.submatrix Subtype.val Subtype.val)⁻¹.mulVec fun (b : { a : n // a ≠ i }) => A (↑b) i

The reciprocal of a diagonal entry (A⁻¹) i i of the inverse of a positive-definite real matrix is the scalar Schur complement of the principal block of A away from i.