Error after truncating a projected approximation

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.HMT2011Truncation

/-- The `j`-th largest entry, counted with multiplicity, of a finite real family `lam`.
It is the supremum of the thresholds `t` for which at least `j` indices satisfy `t ≤ lam i`.
For `1 ≤ j ≤ n` this is the `j`-th largest value. For `j > n` the set is empty, so the
value is `0` (the usual zero padding). -/
noncomputable def kthLargest {n : ℕ} (lam : Fin n → ℝ) (j : ℕ) : ℝ := by
  classical
  exact sSup {t : ℝ | j ≤ (Finset.univ.filter (fun i => t ≤ lam i)).card}

/-- The `j`-th singular value `σ_j` of a real matrix `A` (1-based index). It is the square
root of the `j`-th largest eigenvalue of the positive semidefinite matrix `Aᴴ A`, and it is
zero-padded beyond the number of columns. It is derived from `A`; it is not a free sequence. -/
noncomputable def singularValue {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (j : ℕ) : ℝ :=
  Real.sqrt (kthLargest (Matrix.isHermitian_conjTranspose_mul_self A).eigenvalues j)

/-- `Ahat` is a best rank-`k` approximation of `M` with respect to the spectral norm:
`rank Ahat ≤ k`, and `Ahat` minimizes `‖M - B‖` (the spectral/ℓ₂-operator norm) over all
`B` with `rank B ≤ k`. -/
def IsBestRankApproxSpectral {m n : ℕ} (k : ℕ) (M Ahat : Matrix (Fin m) (Fin n) ℝ) : Prop :=
  Ahat.rank ≤ k ∧ ∀ B : Matrix (Fin m) (Fin n) ℝ, B.rank ≤ k → ‖M - Ahat‖ ≤ ‖M - B‖

/-- HMT 2011, Theorem (thm:truncation). Let `A` be an `m × n` matrix with singular values
`σ_1 ≥ σ_2 ≥ …`, and let `Z` be an `m × ℓ` matrix with `ℓ ≥ k`. Suppose `Ahat` is a best
rank-`k` approximation of `P_Z A` with respect to the spectral norm. Then
`‖A - Ahat‖ ≤ σ_{k+1} + ‖(I - P_Z) A‖`. -/
theorem truncation_error_bound {m n ℓ : ℕ} (k : ℕ) (hk : k ≤ ℓ)
    (A : Matrix (Fin m) (Fin n) ℝ) (Z : Matrix (Fin m) (Fin ℓ) ℝ)
    (Ahat : Matrix (Fin m) (Fin n) ℝ)
    (hAhat : IsBestRankApproxSpectral k (orthogonalProjector Z * A) Ahat) :
    ‖A - Ahat‖ ≤ singularValue A (k + 1) + ‖(1 - orthogonalProjector Z) * A‖ := by
  sorry

end RNLAPhaseB.HMT2011Truncation