Deterministic spectral error of a 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.MT2020RRFDeterministic

/-- Leading index embedding `Fin k → Fin n` (first `k` columns). -/
def leadingIdx {k n : ℕ} (hk : k ≤ n) : Fin k → Fin n := Fin.castLE hk

/-- Trailing index embedding `Fin (n - k) → Fin n` (remaining `n - k` columns). -/
def trailingIdx {k n : ℕ} (hk : k ≤ n) : Fin (n - k) → Fin n :=
  fun j => ⟨k + j.val, by have := j.isLt; omega⟩

/-- A matrix has full row rank when its coordinate linear map is surjective
(its rows are linearly independent / its rank equals its number of rows). -/
def FullRowRank {𝕜 : Type*} [CommSemiring 𝕜] {m p : Type*} [Fintype p] [DecidableEq p]
    (M : Matrix m p 𝕜) : Prop :=
  Function.Surjective (Matrix.toLin' M)

/-- `A'` is the Moore–Penrose pseudoinverse `A^†` of `A`. -/
def IsMoorePenroseInverse {𝕜 : Type*} [RCLike 𝕜] {m p : Type*} [Fintype m] [Fintype p]
    (A : Matrix m p 𝕜) (A' : Matrix p m 𝕜) : Prop :=
  A * A' * A = A ∧ A' * A * A' = A' ∧ (A * A')ᴴ = A * A' ∧ (A' * A)ᴴ = A' * A

/-- The singular value `σ_{k+1}` (1-based) read from the diagonal `σ` of the SVD,
zero-padded when `k + 1 > n` (then `Σ₂` is empty). -/
def singularValueNext {n : ℕ} (σ : Fin n → ℝ) (k : ℕ) : ℝ :=
  if h : k < n then σ ⟨k, h⟩ else 0

/-- mt2020 thm:rrf-deterministic (master error bound, spectral norm).
Setting (m = n after zero extension): `B = U diag(σ) Vᴴ` with `U, V` square unitary,
`σ` nonnegative and weakly decreasing. For `k ≤ ℓ`, `V₁` = first `k` columns of `V`,
`V₂` = remaining `n - k` columns, `Σ₂ = diag(σ_{k+1}, …, σ_n)`, `X₁ = V₁ᴴ X`,
`X₂ = V₂ᴴ X`, and `X₁` is assumed to have full row rank. With `Y = B X`,
`‖(I - P_Y) B‖ ≤ σ_{k+1} + ‖Σ₂ X₂ X₁^†‖` in the spectral norm. -/
theorem rrf_deterministic {𝕜 : Type*} [RCLike 𝕜] {n ℓ : ℕ}
    (B : Matrix (Fin n) (Fin n) 𝕜) (X : Matrix (Fin n) (Fin ℓ) 𝕜)
    (U V : Matrix (Fin n) (Fin n) 𝕜) (σ : Fin n → ℝ)
    (hU : Uᴴ * U = 1 ∧ U * Uᴴ = 1) (hV : Vᴴ * V = 1 ∧ V * Vᴴ = 1)
    (hσ_nonneg : ∀ i, 0 ≤ σ i) (hσ_anti : Antitone σ)
    (hSVD : B = U * Matrix.diagonal (fun i => ((σ i : ℝ) : 𝕜)) * Vᴴ)
    (k : ℕ) (hkℓ : k ≤ ℓ) (hkn : k ≤ n)
    (hX1 : FullRowRank ((V.submatrix id (leadingIdx hkn))ᴴ * X))
    (X1pinv : Matrix (Fin ℓ) (Fin k) 𝕜)
    (hpinv : IsMoorePenroseInverse ((V.submatrix id (leadingIdx hkn))ᴴ * X) X1pinv) :
    ‖(1 - orthogonalProjector (B * X)) * B‖ ≤
      singularValueNext σ k +
        ‖Matrix.diagonal (fun j => ((σ (trailingIdx hkn j) : ℝ) : 𝕜)) *
            ((V.submatrix id (trailingIdx hkn))ᴴ * X) * X1pinv‖ := by
  sorry

end RNLAPhaseB.MT2020RRFDeterministic