Expected error of a Gaussian rangefinder

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.MT2020RrfGauss

/-- The four Moore–Penrose conditions: `X` is the pseudoinverse of the real matrix `A`. -/
def IsMoorePenroseInverse {k ℓ : ℕ} (A : Matrix (Fin k) (Fin ℓ) ℝ)
    (X : Matrix (Fin ℓ) (Fin k) ℝ) : Prop :=
  A * X * A = A ∧ X * A * X = X ∧ (A * X)ᵀ = A * X ∧ (X * A)ᵀ = X * A

/-- The Moore–Penrose pseudoinverse `A^†`: a matrix satisfying the Moore–Penrose
conditions. Such a matrix exists and is unique, so this is the pseudoinverse. The
`else` branch is never reached mathematically. -/
noncomputable def pinv {k ℓ : ℕ} (A : Matrix (Fin k) (Fin ℓ) ℝ) :
    Matrix (Fin ℓ) (Fin k) ℝ := by
  classical
  exact if h : ∃ X, IsMoorePenroseInverse A X then Classical.choose h else 0

/-- The singular values of `B`, in weakly decreasing order: the square roots of the
eigenvalues (with multiplicity) of `Bᵀ B`, i.e. of the real roots of its
characteristic polynomial (which splits, `Bᵀ B` being symmetric psd). -/
noncomputable def singularValues {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ) : List ℝ :=
  ((((Bᵀ * B).charpoly.roots).sort (· ≤ ·)).reverse).map Real.sqrt

/-- The singular value `σ_j` of `B` (1-based index `j`), zero-padded beyond the list. -/
noncomputable def singularValue {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  (singularValues B).getD (j - 1) 0

/-- The tail sum `∑_{j > k} σ_j^2` of squared singular values of `B`. -/
noncomputable def singularTailSq {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ) (k : ℕ) : ℝ :=
  (((singularValues B).drop k).map (fun s => s ^ 2)).sum

/-- mt2020 thm:rrf-gauss. `B ∈ ℝ^{m×n}`, `Ω` a (real) standard normal `n×ℓ` test
matrix, `Y = BΩ`, `k < ℓ - 1`, `Z = ‖Γ^†‖` with `Γ ∈ ℝ^{k×ℓ}` standard normal. Then
`E‖(I - P_Y)B‖ ≤ (1 + √(k/(ℓ-k-1))) σ_{k+1} + (E Z)(∑_{j>k} σ_j²)^{1/2}`,
with `‖·‖` the spectral norm. -/
theorem rrf_gauss {S : Type*} [MeasurableSpace S] (P : Measure S)
    {m n ℓ k : ℕ} (B : Matrix (Fin m) (Fin n) ℝ)
    (G : S → Matrix (Fin n) (Fin ℓ) ℝ) (hG : StandardGaussianTestMatrix P G)
    (Gam : S → Matrix (Fin k) (Fin ℓ) ℝ) (hGam : StandardGaussianTestMatrix P Gam)
    (hk : k < ℓ - 1) :
    ∫ ω, ‖(1 - orthogonalProjector (B * G ω)) * B‖ ∂P ≤
      (1 + Real.sqrt ((k : ℝ) / ((ℓ : ℝ) - k - 1))) * singularValue B (k + 1) +
        (∫ ω, ‖pinv (Gam ω)‖ ∂P) * Real.sqrt (singularTailSq B k) := by
  sorry

end RNLAPhaseB.MT2020RrfGauss