Gaussian power-rangefinder moment bound

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.MT2020CorRRFPowerGauss

open RNLAPhaseB

/-- Moore–Penrose conditions: `X = A^†` (unique solution). -/
def IsMoorePenroseInverse {k l : ℕ} (A : Matrix (Fin k) (Fin l) ℝ)
    (X : Matrix (Fin l) (Fin k) ℝ) : Prop :=
  A * X * A = A ∧ X * A * X = X ∧ (A * X)ᵀ = A * X ∧ (X * A)ᵀ = X * A

/-- Singular values of `B` in weakly decreasing order: square roots of the eigenvalues
of `Bᵀ B`, which has `n` of them. -/
noncomputable def singularValues {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ) : List ℝ :=
  (List.ofFn fun i : Fin n =>
      Real.sqrt ((Matrix.isHermitian_conjTranspose_mul_self B).eigenvalues i)).mergeSort
    (fun a b => decide (b ≤ a))

/-- 1-based `σ_j(B)`, zero-padded; used only for `j ≥ 1`. -/
noncomputable def singularValue {m n : ℕ} (B : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  (singularValues B).getD (j - 1) 0

/-- MT2020 cor:rrf-power-gauss, under the conditions of thm:rrf-gauss.

* `B ∈ ℝ^{m×n}` and `k < ℓ - 1`.
* `Z = ‖Γ^†‖`, where `Γ ∈ ℝ^{k×ℓ}` is standard normal.
* The test matrix `Ω` is standard normal and `m×ℓ`, as in alg:power-rangefinder.
* `Y = (BB^*)^q Ω`.

The norm is the spectral norm. The exponent `1/(2q)` is read with `q ≥ 1`. -/
theorem cor_rrf_power_gauss
    {Ω Θ : Type*} [MeasurableSpace Ω] [MeasurableSpace Θ]
    (P : Measure Ω) (Q : Measure Θ)
    (m n l k q : ℕ) (B : Matrix (Fin m) (Fin n) ℝ)
    (Om : Ω → Matrix (Fin m) (Fin l) ℝ) (hOm : StandardGaussianTestMatrix P Om)
    (hk : k < l - 1) (hq : 1 ≤ q)
    (Γ : Θ → Matrix (Fin k) (Fin l) ℝ) (hΓ : StandardGaussianTestMatrix Q Γ)
    (Γpinv : Θ → Matrix (Fin l) (Fin k) ℝ)
    (hpinv : ∀ θ, IsMoorePenroseInverse (Γ θ) (Γpinv θ)) :
    let Y : Ω → Matrix (Fin m) (Fin l) ℝ := fun ω => (B * Bᵀ) ^ q * Om ω
    let err : Ω → ℝ := fun ω => ‖(1 - orthogonalProjector (Y ω)) * B‖
    let EZ : ℝ := ∫ θ, ‖Γpinv θ‖ ∂Q
    let σ : ℕ → ℝ := singularValue B
    (∫ ω, err ω ∂P) ≤ (∫ ω, err ω ^ (2 * q) ∂P) ^ (1 / (2 * (q : ℝ))) ∧
    (∫ ω, err ω ^ (2 * q) ∂P) ^ (1 / (2 * (q : ℝ))) ≤
      ((1 + Real.sqrt ((k : ℝ) / ((l : ℝ) - k - 1))) * σ (k + 1) ^ (2 * q)
        + EZ * Real.sqrt (∑ j ∈ Finset.Ioc k n, σ j ^ (4 * q))) ^ (1 / (2 * (q : ℝ))) := by
  sorry

end RNLAPhaseB.MT2020CorRRFPowerGauss