The Moore–Penrose inverse

For linear maps A : E → F and B : F → E between inner product spaces, B is a Moore–Penrose inverse of A when the four Penrose conditions hold:

A B A = A     B A B = B     A B is symmetric     B A is symmetric

Here symmetric means LinearMap.IsSymmetric, that is ⟪A B x, y⟫ = ⟪x, A B y⟫ for all x and y, which makes sense without assuming that adjoints exist. When the spaces are finite-dimensional, the last two conditions are the usual Penrose equations (A B)† = A B and (B A)† = B A. The symmetric idempotents A B and B A are the orthogonal projections onto the ranges of A and of B. This file records the relation as the predicate LinearMap.IsMoorePenroseInverse, shows that it determines B uniquely, that it is symmetric in A and B, and that it is compatible with adjoints. For maps between finite-dimensional spaces, LinearMap.moorePenroseInverse A is the singular-system construction

A⁺ y = ∑ᵢ σᵢ⁻² ⟪A vᵢ, y⟫ vᵢ = ∑ᵢ σᵢ⁻¹ ⟪uᵢ, y⟫ vᵢ,

where (vᵢ) = A.rightSingularBasis is the ordered orthonormal eigenbasis of A† A, σᵢ are the singular values of A, and uᵢ = σᵢ⁻¹ A vᵢ = A.leftSingularVector i are the left singular vectors. In words, A⁺ inverts each nonzero singular value and sends the zero ones to zero. Every Moore–Penrose inverse of A equals A⁺.

The relation reduces to familiar one-sided inverses in the injective, surjective, and invertible cases: A⁺ A = 1 for injective A, A A⁺ = 1 for surjective A, and A⁺ = A⁻¹ for a linear equivalence.

Main definitions

• LinearMap.IsMoorePenroseInverse A B: the four Penrose conditions.
• LinearMap.moorePenroseInverse A: the Moore–Penrose inverse of a map between finite-dimensional inner product spaces, built from its singular system.

Main statements

• LinearMap.IsMoorePenroseInverse.unique: Moore–Penrose inverses are unique. This holds in arbitrary inner product spaces.
• LinearMap.isMoorePenroseInverse_adjoint_iff: B is a Moore–Penrose inverse of A if and only if B† is one of A†.
• LinearMap.isMoorePenroseInverse_moorePenroseInverse: the singular-system construction satisfies the Penrose equations.
• LinearMap.isMoorePenroseInverse_iff_eq_moorePenroseInverse: the Penrose equations characterize A⁺.

References

• R. Penrose, A generalized inverse for matrices, Proc. Cambridge Philos. Soc. 51 (1955), 406–413.
• A. Ben-Israel, T. N. E. Greville, Generalized Inverses: Theory and Applications, 2nd ed., CMS Books in Mathematics, Springer (2003), Chapter 1.

structure LinearMap.IsMoorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) : Prop

IsMoorePenroseInverse A B states that B is a Moore–Penrose inverse of A: the four Penrose conditions hold, namely A B A = A, B A B = B, and the compositions A B and B A are symmetric in the sense of LinearMap.IsSymmetric. In finite dimension the last two conditions are the adjoint equations (A B)† = A B and (B A)† = B A.

• comp_comp_self : A ∘ₗ B ∘ₗ A = A

  B is a generalized inverse of A.

• comp_comp_self' : B ∘ₗ A ∘ₗ B = B

  A is a generalized inverse of B.

• isSymmetric_comp : (A ∘ₗ B).IsSymmetric

  The idempotent A B onto the range of A is symmetric.

• isSymmetric_comp' : (B ∘ₗ A).IsSymmetric

  The idempotent B A onto the range of B is symmetric.

theorem LinearMap.IsMoorePenroseInverse.apply_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (h : A.IsMoorePenroseInverse B) (x : E) : A (B (A x)) = A x

Pointwise form of A B A = A.

theorem LinearMap.IsMoorePenroseInverse.apply_apply_apply' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (h : A.IsMoorePenroseInverse B) (y : F) : B (A (B y)) = B y

Pointwise form of B A B = B.

theorem LinearMap.IsMoorePenroseInverse.symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (h : A.IsMoorePenroseInverse B) : B.IsMoorePenroseInverse A

The Moore–Penrose relation is symmetric: if B is a Moore–Penrose inverse of A, then A is a Moore–Penrose inverse of B.

theorem LinearMap.IsMoorePenroseInverse.comp_eq_id_of_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (h : A.IsMoorePenroseInverse B) (hA : Function.Injective ⇑A) : B ∘ₗ A = id

If A is injective, a Moore–Penrose inverse of A is a left inverse.

theorem LinearMap.IsMoorePenroseInverse.comp_eq_id_of_surjective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (h : A.IsMoorePenroseInverse B) (hA : Function.Surjective ⇑A) : A ∘ₗ B = id

If A is surjective, a Moore–Penrose inverse of A is a right inverse.

theorem LinearMap.IsMoorePenroseInverse.of_comp_eq_id {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} (hBA : B ∘ₗ A = id) (hAB : A ∘ₗ B = id) : A.IsMoorePenroseInverse B

A two-sided inverse is a Moore–Penrose inverse.

theorem LinearMap.isMoorePenroseInverse_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} : A.IsMoorePenroseInverse B ↔ B.IsMoorePenroseInverse A

The Moore–Penrose relation is symmetric in its two arguments.

@[simp]

theorem LinearMap.isMoorePenroseInverse_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] : IsMoorePenroseInverse 0 0

The zero map is its own Moore–Penrose inverse.

@[simp]

theorem LinearEquiv.isMoorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [SeminormedAddCommGroup F] [InnerProductSpace 𝕜 F] (e : E ≃ₗ[𝕜] F) : (↑e).IsMoorePenroseInverse ↑e.symm

A linear equivalence and its inverse are Moore–Penrose inverses of each other.

theorem LinearMap.IsMoorePenroseInverse.unique {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B C : F →ₗ[𝕜] E} (hB : A.IsMoorePenroseInverse B) (hC : A.IsMoorePenroseInverse C) : B = C

Uniqueness of the Moore–Penrose inverse. A linear map between inner product spaces has at most one Moore–Penrose inverse.

theorem LinearMap.IsMoorePenroseInverse.adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (h : A.IsMoorePenroseInverse B) : (adjoint A).IsMoorePenroseInverse (adjoint B)

The Moore–Penrose relation is compatible with adjoints: if B is a Moore–Penrose inverse of A, then B† is a Moore–Penrose inverse of A†.

theorem LinearMap.isMoorePenroseInverse_adjoint_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {A : E →ₗ[𝕜] F} {B : F →ₗ[𝕜] E} : (adjoint A).IsMoorePenroseInverse (adjoint B) ↔ A.IsMoorePenroseInverse B

B is a Moore–Penrose inverse of A if and only if B† is a Moore–Penrose inverse of A†.

The singular-system construction

noncomputable def LinearMap.moorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : F →ₗ[𝕜] E

The Moore–Penrose inverse of a linear map A between finite-dimensional inner product spaces: A⁺ y = ∑ᵢ σᵢ⁻² ⟪A vᵢ, y⟫ vᵢ, where (vᵢ) is the right singular basis of A (the ordered orthonormal eigenbasis of A† A) and σᵢ are the singular values of A. Indices with σᵢ = 0 contribute nothing.

theorem LinearMap.moorePenroseInverse_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (y : F) : A.moorePenroseInverse y = ∑ i : Fin (Module.finrank 𝕜 E), (↑(A.singularValues ↑i ^ 2))⁻¹ • inner 𝕜 (A (A.rightSingularBasis i)) y • A.rightSingularBasis i

The singular expansion of A⁺ y.

@[simp]

theorem LinearMap.isMoorePenroseInverse_moorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.IsMoorePenroseInverse A.moorePenroseInverse

The singular-system construction A⁺ is a Moore–Penrose inverse of A.

theorem LinearMap.isMoorePenroseInverse_iff_eq_moorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) {B : F →ₗ[𝕜] E} : A.IsMoorePenroseInverse B ↔ B = A.moorePenroseInverse

Characterization of the Moore–Penrose inverse. A map satisfies the four Penrose equations for A if and only if it is A⁺.

theorem LinearMap.moorePenroseInverse_comp_of_injective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (hA : Function.Injective ⇑A) : A.moorePenroseInverse ∘ₗ A = id

The Moore–Penrose inverse of an injective map is a left inverse.

theorem LinearMap.comp_moorePenroseInverse_of_surjective {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (hA : Function.Surjective ⇑A) : A ∘ₗ A.moorePenroseInverse = id

The Moore–Penrose inverse of a surjective map is a right inverse.

@[simp]

theorem LinearEquiv.moorePenroseInverse_eq_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (e : E ≃ₗ[𝕜] F) : (↑e).moorePenroseInverse = ↑e.symm

The Moore–Penrose inverse of a linear equivalence is its inverse.

@[simp]

theorem LinearMap.moorePenroseInverse_moorePenroseInverse {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : A.moorePenroseInverse.moorePenroseInverse = A

The Moore–Penrose inverse is involutive: (A⁺)⁺ = A.

@[simp]

theorem LinearMap.moorePenroseInverse_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) : (adjoint A).moorePenroseInverse = adjoint A.moorePenroseInverse

The Moore–Penrose inverse commutes with adjoints: (A†)⁺ = (A⁺)†.

@[simp]

theorem LinearMap.moorePenroseInverse_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : moorePenroseInverse 0 = 0

The Moore–Penrose inverse of the zero map is zero.

theorem Matrix.isMoorePenroseInverse_toEuclideanLin_of_penrose {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [RCLike 𝕜] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] {C : Matrix m n 𝕜} {D : Matrix n m 𝕜} (h₁ : C * D * C = C) (h₂ : D * C * D = D) (h₃ : (C * D).IsHermitian) (h₄ : (D * C).IsHermitian) : (toEuclideanLin C).IsMoorePenroseInverse (toEuclideanLin D)

The four matrix Penrose equations imply the Moore–Penrose relation between the corresponding Euclidean linear maps.