Add the Moore-Penrose pseudo-inverse #24787
Description
Note that the naive definition of
import Mathlib
variable {m n R : Type*} [CommRing R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n]
noncomputable def pinv (A : Matrix m n R) : Matrix n m R :=
(Aᵀ * A)⁻¹ * Aᵀonly works when FIntype.card m >= Fintype.card n, and even then only when rank A = Fintype.card n.
Some possible references for a generalized definition:
- The generalized Moore-Penrose inverse, Mar 1992
- The Moore-Penrose inverse over a commutative ring, Dec 1992
A quick attempt at the second one seems to start with:
def IsMoorePenroseInverse {α β γ δ} [HMul α β γ] [HMul β α δ] [HMul γ α α] [HMul δ β β] [Star γ] [Star δ]
(A : α) (As : β) :=
A * As * A = A ∧ As * A * As = As ∧ star (A * As) = A * As ∧ star (As * A) = As * AZulip threads: