The pseudoinverse of a covariance matrix

Matrix.covariancePseudoInverse inverts the nonzero eigenvalues of a real positive-semidefinite matrix and vanishes on its kernel. Invalid covariance matrices give zero. This is the inverse needed to condition a Gaussian vector on an observed block with singular covariance.

The construction uses Mathlib's finite-spectrum continuous functional calculus. Its Euclidean operator is the existing LinearMap.moorePenroseInverse, so uniqueness follows from the four Penrose equations rather than a choice of eigenbasis.

References

• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51 (1955), 406–413.
• T. W. Anderson, An Introduction to Multivariate Statistical Analysis, 3rd ed., Wiley (2003).

noncomputable def Matrix.covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : Matrix ι ι ℝ

Invert the nonzero eigenvalues of a positive-semidefinite covariance matrix, sending zero eigenvalues to zero. For a matrix that is not positive semidefinite, return zero.

theorem Matrix.covariancePseudoInverse_of_posSemidef {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : C.covariancePseudoInverse = cfc (fun (x : ℝ) => x⁻¹) C

The positive-semidefinite branch of the covariance pseudoinverse.

@[simp]

theorem Matrix.covariancePseudoInverse_of_not_posSemidef {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : ¬C.PosSemidef) : C.covariancePseudoInverse = 0

An invalid covariance has zero pseudoinverse.

@[simp]

theorem Matrix.covariancePseudoInverse_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] : covariancePseudoInverse 0 = 0

The pseudoinverse of zero is zero, also in dimension zero.

theorem Matrix.posSemidef_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : C.covariancePseudoInverse.PosSemidef

Every covariance pseudoinverse is positive semidefinite, including the invalid branch.

theorem Matrix.commute_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : Commute C C.covariancePseudoInverse

A covariance matrix commutes with its pseudoinverse.

theorem Matrix.mul_covariancePseudoInverse_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : C * C.covariancePseudoInverse * C = C

The first Penrose equation for a positive-semidefinite matrix.

theorem Matrix.covariancePseudoInverse_mul_self_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : C.covariancePseudoInverse * C * C.covariancePseudoInverse = C.covariancePseudoInverse

The second Penrose equation holds for every matrix, including invalid covariances.

theorem Matrix.isHermitian_mul_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : (C * C.covariancePseudoInverse).IsHermitian

The product of a covariance and its pseudoinverse is symmetric.

theorem Matrix.isHermitian_covariancePseudoInverse_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Matrix ι ι ℝ) : (C.covariancePseudoInverse * C).IsHermitian

The product of a covariance pseudoinverse and its covariance is symmetric.

theorem Matrix.isMoorePenroseInverse_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : (toEuclideanLin C).IsMoorePenroseInverse (toEuclideanLin C.covariancePseudoInverse)

The functional-calculus construction satisfies all four Moore–Penrose equations.

theorem Matrix.eq_covariancePseudoInverse_of_penrose {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C D : Matrix ι ι ℝ} (hC : C.PosSemidef) (h₁ : C * D * C = C) (h₂ : D * C * D = D) (h₃ : (C * D).IsHermitian) (h₄ : (D * C).IsHermitian) : D = C.covariancePseudoInverse

The four matrix Penrose equations characterize the covariance pseudoinverse.

theorem Matrix.toEuclideanLin_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : toEuclideanLin C.covariancePseudoInverse = (toEuclideanLin C).moorePenroseInverse

The covariance construction agrees with the existing Moore–Penrose inverse of the Euclidean operator.

theorem Matrix.covariancePseudoInverse_of_posDef {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosDef) : C.covariancePseudoInverse = C⁻¹

At positive-definite covariance, the pseudoinverse is the ordinary inverse.

theorem Matrix.covariancePseudoInverse_eq_inv_of_unique {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Unique ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : C.covariancePseudoInverse = C⁻¹

On one coordinate, the pseudoinverse of a valid covariance agrees with the totalized ordinary inverse, including zero variance.

@[simp]

theorem Matrix.covariancePseudoInverse_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : C.covariancePseudoInverse.covariancePseudoInverse = C

Inverting the covariance pseudoinverse recovers every valid covariance.

theorem Matrix.toEuclideanLin_mul_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : toEuclideanLin (C * C.covariancePseudoInverse) = ↑(toEuclideanLin C).range.starProjection

Multiplication by a covariance and its pseudoinverse is the orthogonal projection onto its Euclidean range. Submodule.starProjection is the ambient inclusion composed with Submodule.orthogonalProjectionOnto.

theorem Matrix.toEuclideanLin_covariancePseudoInverse_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : toEuclideanLin (C.covariancePseudoInverse * C) = ↑(toEuclideanLin C).range.starProjection

Multiplication by a covariance pseudoinverse and its covariance is the orthogonal projection onto the covariance's Euclidean range.

theorem Matrix.tendsto_inv_sq_add_smul_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {C : Matrix ι ι ℝ} (hC : C.PosSemidef) : Filter.Tendsto (fun (ε : ℝ) => (C ^ 2 + ε • 1)⁻¹ * C) (nhdsWithin 0 (Set.Ioi 0)) (nhds C.covariancePseudoInverse)

The covariance pseudoinverse is the limit of (C² + ε I)⁻¹ C as positive ε tends to zero. The limit includes zero covariance and empty coordinate types.

theorem Matrix.measurable_covariancePseudoInverse {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Measurable covariancePseudoInverse

The totalized covariance pseudoinverse is Borel measurable in all matrix entries.