Rangefinder error as a Schur complement

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

open MeasureTheory
open scoped Matrix
open scoped Matrix.Norms.L2Operator
open scoped BigOperators
open scoped ENNReal
open scoped ComplexOrder

namespace RNLAPhaseB.MT2020.PropRrfSchur

/-- `W` is the Moore–Penrose pseudoinverse `M^†` of the matrix `M`: the four
Penrose conditions. The pseudoinverse is unique, so a binder constrained by
these equations denotes the source's `M^†`. -/
structure IsMoorePenroseInverse {𝕜 : Type*} [RCLike 𝕜] {p q : Type*}
    [Fintype p] [Fintype q] (M : Matrix p q 𝕜) (W : Matrix q p 𝕜) : Prop where
  mul_mul_self : M * W * M = M
  self_mul_mul : W * M * W = W
  mul_selfAdjoint : (M * W)ᴴ = M * W
  selfAdjoint_mul : (W * M)ᴴ = W * M

/-- The Nyström approximation (eqn:nys-def)
`A⟨X⟩ := (A X) (X^* A X)^† (A X)^*`, where `W` is the pseudoinverse
`(X^* A X)^†` (constrained separately by `IsMoorePenroseInverse`). -/
def nystromApprox {𝕜 : Type*} [RCLike 𝕜] {n k : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) (X : Matrix (Fin n) (Fin k) 𝕜)
    (W : Matrix (Fin k) (Fin k) 𝕜) : Matrix (Fin n) (Fin n) 𝕜 :=
  (A * X) * W * (A * X)ᴴ

/-- The Schur complement (eqn:schur-complement) `A / X := A - A⟨X⟩`, with `W`
standing for `(X^* A X)^†`. -/
def schurComplement {𝕜 : Type*} [RCLike 𝕜] {n k : ℕ}
    (A : Matrix (Fin n) (Fin n) 𝕜) (X : Matrix (Fin n) (Fin k) 𝕜)
    (W : Matrix (Fin k) (Fin k) 𝕜) : Matrix (Fin n) (Fin n) 𝕜 :=
  A - nystromApprox A X W

/-- The approximation error `E(B, X) := (I - P_Y) B` with `Y = B X` and `P_Y`
the orthogonal projector onto the range of `Y`. -/
noncomputable def approxError {𝕜 : Type*} [RCLike 𝕜] {m n ℓ : ℕ}
    (B : Matrix (Fin m) (Fin n) 𝕜) (X : Matrix (Fin n) (Fin ℓ) 𝕜) :
    Matrix (Fin m) (Fin n) 𝕜 :=
  (1 - orthogonalProjector (B * X)) * B

/-- mt2020 Proposition (prop:rrf-schur). For an arbitrary test matrix
`X ∈ F^{n×ℓ}` (F = ℝ or ℂ, realized as `RCLike 𝕜`), with `Y = B X` and
`E = (I - P_Y) B`, the squared error `|E|^2 := E^* E` equals the Schur
complement `(B^* B) / X`, i.e. `B^*B - (B^*B X)(X^* B^*B X)^† (B^*B X)^*`;
and `|E|^2` is a psd matrix. The pseudoinverse is represented by any matrix
satisfying the Penrose conditions (it is unique). -/
theorem prop_rrf_schur {𝕜 : Type*} [RCLike 𝕜] {m n ℓ : ℕ}
    (B : Matrix (Fin m) (Fin n) 𝕜) (X : Matrix (Fin n) (Fin ℓ) 𝕜)
    (W : Matrix (Fin ℓ) (Fin ℓ) 𝕜)
    (hW : IsMoorePenroseInverse (Xᴴ * (Bᴴ * B) * X) W) :
    (approxError B X)ᴴ * approxError B X = schurComplement (Bᴴ * B) X W ∧
      ((approxError B X)ᴴ * approxError B X).PosSemidef := by
  sorry

end RNLAPhaseB.MT2020.PropRrfSchur