Monotonicity of rangefinder error in semidefinite order

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.MT2020CorRrfMonotone

open Matrix

variable {𝕜 : Type*} [RCLike 𝕜]

/-- Moore–Penrose conditions: `G` is the pseudoinverse `M^†` of `M`. -/
def IsMoorePenroseInverse {r s : ℕ} (M : Matrix (Fin r) (Fin s) 𝕜)
    (G : Matrix (Fin s) (Fin r) 𝕜) : Prop :=
  M * G * M = M ∧ G * M * G = G ∧ (M * G)ᴴ = M * G ∧ (G * M)ᴴ = G * M

/-- The Moore–Penrose pseudoinverse `M^†`, selected by its defining conditions
(it exists and is unique, so the selection is the pseudoinverse). -/
noncomputable def pinv {r s : ℕ} (M : Matrix (Fin r) (Fin s) 𝕜) :
    Matrix (Fin s) (Fin r) 𝕜 :=
  Classical.epsilon (IsMoorePenroseInverse M)

/-- The Nyström approximation `A⟨X⟩ := (AX)(X^* A X)^† (AX)^*` (eqn:nys-def). -/
noncomputable def nystrom {n ℓ : ℕ} (A : Matrix (Fin n) (Fin n) 𝕜)
    (X : Matrix (Fin n) (Fin ℓ) 𝕜) : Matrix (Fin n) (Fin n) 𝕜 :=
  (A * X) * pinv (Xᴴ * A * X) * (A * X)ᴴ

/-- The Schur complement `A / X := A - A⟨X⟩` (eqn:schur-complement). -/
noncomputable def schurComplement {n ℓ : ℕ} (A : Matrix (Fin n) (Fin n) 𝕜)
    (X : Matrix (Fin n) (Fin ℓ) 𝕜) : Matrix (Fin n) (Fin n) 𝕜 :=
  A - nystrom A X

/-- The rangefinder approximation error `E(B, X) := (I - P_Y) B` with `Y = BX`. -/
noncomputable def rangefinderError {m n ℓ : ℕ} (B : Matrix (Fin m) (Fin n) 𝕜)
    (X : Matrix (Fin n) (Fin ℓ) 𝕜) : Matrix (Fin m) (Fin n) 𝕜 :=
  (1 - orthogonalProjector (B * X)) * B

/-- The squared error `|E|^2 := E^* E` (a psd matrix, not a scalar). -/
noncomputable def sqAbs {m n : ℕ} (E : Matrix (Fin m) (Fin n) 𝕜) :
    Matrix (Fin n) (Fin n) 𝕜 :=
  Eᴴ * E

/-- The semidefinite (Loewner) order `M ≼ N`: `N - M` is positive semidefinite. -/
def PsdLE {n : ℕ} (M N : Matrix (Fin n) (Fin n) 𝕜) : Prop :=
  (N - M).PosSemidef

/-- mt2020 cor:rrf-monotone: if `B^* B ≼ C^* C`, then for each fixed test matrix `X`,
`|E(B,X)|^2 = (B^*B)/X ≼ (C^*C)/X = |E(C,X)|^2`. -/
theorem rrf_monotone {m p n ℓ : ℕ}
    (B : Matrix (Fin m) (Fin n) 𝕜) (C : Matrix (Fin p) (Fin n) 𝕜)
    (hBC : PsdLE (Bᴴ * B) (Cᴴ * C))
    (X : Matrix (Fin n) (Fin ℓ) 𝕜) :
    sqAbs (rangefinderError B X) = schurComplement (Bᴴ * B) X ∧
    PsdLE (schurComplement (Bᴴ * B) X) (schurComplement (Cᴴ * C) X) ∧
    schurComplement (Cᴴ * C) X = sqAbs (rangefinderError C X) := by
  sorry

end RNLAPhaseB.MT2020CorRrfMonotone