Deterministic low-rank sampling inequality

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017MainLemmaGeneral

/-- Squared Frobenius norm `‖M‖_F^2 = ∑_{i,j} M_{ij}^2` of a real matrix. -/
def frobeniusNormSq {p q : ℕ} (M : Matrix (Fin p) (Fin q) ℝ) : ℝ :=
  ∑ i, ∑ j, M i j ^ 2

/-- `X` is the Moore–Penrose pseudoinverse `M^†` of the real matrix `M`
(the four Penrose conditions; over ℝ self-adjoint means symmetric). -/
def IsMoorePenroseInverse {p q : ℕ} (M : Matrix (Fin p) (Fin q) ℝ)
    (X : Matrix (Fin q) (Fin p) ℝ) : Prop :=
  M * X * M = M ∧ X * M * X = X ∧ (M * X)ᵀ = M * X ∧ (X * M)ᵀ = X * M

/-- A thin SVD `A = U Σ Vᵀ` of `A` with `ρ` nonzero singular values: `U`, `V` have
orthonormal columns and the singular values `σ` are positive and sorted in
nonincreasing order (so column `i` of `U`/`V` is the `i`-th left/right singular vector). -/
structure IsThinSVD {m n ρ : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
    (U : Matrix (Fin m) (Fin ρ) ℝ) (σ : Fin ρ → ℝ) (V : Matrix (Fin n) (Fin ρ) ℝ) :
    Prop where
  U_orthonormal : Uᵀ * U = 1
  V_orthonormal : Vᵀ * V = 1
  sigma_pos : ∀ i, 0 < σ i
  sigma_antitone : Antitone σ
  factorization : A = U * Matrix.diagonal σ * Vᵀ

/-- The first `k` columns of a matrix with `ρ` columns (`U_k`, `V_k`). -/
def leadingCols {p ρ k : ℕ} (hk : k ≤ ρ) (M : Matrix (Fin p) (Fin ρ) ℝ) :
    Matrix (Fin p) (Fin k) ℝ :=
  M.submatrix id (Fin.castLE hk)

/-- `A_k = U_k Σ_k V_kᵀ`, built from the top `k` singular triplets of the SVD. -/
def rankKPart {m n ρ k : ℕ} (hk : k ≤ ρ)
    (U : Matrix (Fin m) (Fin ρ) ℝ) (σ : Fin ρ → ℝ) (V : Matrix (Fin n) (Fin ρ) ℝ) :
    Matrix (Fin m) (Fin n) ℝ :=
  leadingCols hk U * Matrix.diagonal (fun i => σ (Fin.castLE hk i)) * (leadingCols hk V)ᵀ

/-- dm2017 Lemma `lem:mainlemma_general`: for `A ∈ ℝ^{m×n}` with SVD notation
`A_k = U_k Σ_k V_kᵀ`, and any `Z ∈ ℝ^{n×c}` (`c ≥ k`) with `rank(V_kᵀ Z) = k`,
`‖A_k − (AZ)(AZ)^† A_k‖_F^2 ≤ ‖(A − A_k) Z (V_kᵀ Z)^†‖_F^2`.
The pseudoinverses are given as matrices satisfying the Penrose conditions
(which determine them uniquely). -/
theorem mainlemma_general {m n c k ρ : ℕ}
    (A : Matrix (Fin m) (Fin n) ℝ)
    (U : Matrix (Fin m) (Fin ρ) ℝ) (σ : Fin ρ → ℝ) (V : Matrix (Fin n) (Fin ρ) ℝ)
    (hsvd : IsThinSVD A U σ V) (hk : k ≤ ρ)
    (Z : Matrix (Fin n) (Fin c) ℝ) (hck : k ≤ c)
    (hrank : ((leadingCols hk V)ᵀ * Z).rank = k)
    (AZpinv : Matrix (Fin c) (Fin m) ℝ) (hAZ : IsMoorePenroseInverse (A * Z) AZpinv)
    (VZpinv : Matrix (Fin c) (Fin k) ℝ)
    (hVZ : IsMoorePenroseInverse ((leadingCols hk V)ᵀ * Z) VZpinv) :
    frobeniusNormSq (rankKPart hk U σ V - (A * Z) * AZpinv * rankKPart hk U σ V)
      ≤ frobeniusNormSq ((A - rankKPart hk U σ V) * Z * VZpinv) := by
  sorry

end RNLAPhaseB.DM2017MainLemmaGeneral