Add the Moore-Penrose pseudo-inverse

[eric-wieser]

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 * A

Zulip threads:

• #maths > (Group action of) SL(n) in mathlib @ 💬
• #new members > Dan Packer - Matrix Theory in Mathlib? @ 💬