The projection onto the row space of a matrix #
When A * Aᴴ is invertible, Aᴴ * (A * Aᴴ)⁻¹ is the Moore–Penrose pseudoinverse of A, and
Aᴴ * (A * Aᴴ)⁻¹ * A is a star projection that fixes A from the right. Over ℝ and ℂ it is
the orthogonal projection onto the row space of A.
[UPSTREAM] candidate.
theorem
Matrix.mul_conjTranspose_mul_inv_mul
{m : Type u_1}
{n : Type u_2}
{α : Type u_3}
[Fintype m]
[Fintype n]
[DecidableEq m]
[CommRing α]
[StarRing α]
{A : Matrix m n α}
(h : IsUnit (A * A.conjTranspose).det)
:
A * (A.conjTranspose * (A * A.conjTranspose)⁻¹ * A) = A
theorem
Matrix.isStarProjection_conjTranspose_mul_inv_mul
{m : Type u_1}
{n : Type u_2}
{α : Type u_3}
[Fintype m]
[Fintype n]
[DecidableEq m]
[CommRing α]
[StarRing α]
{A : Matrix m n α}
(h : IsUnit (A * A.conjTranspose).det)
:
IsStarProjection (A.conjTranspose * (A * A.conjTranspose)⁻¹ * A)