Relative solution error for sketched least squares

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017LemSuffCond2

open Matrix

/-- `Ad` is the Moore–Penrose generalized inverse `A^†` of `A` (the four Penrose equations). -/
def IsMoorePenroseInverse {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ)
    (Ad : Matrix (Fin d) (Fin n) ℝ) : Prop :=
  A * Ad * A = A ∧ Ad * A * Ad = Ad ∧ (A * Ad)ᵀ = A * Ad ∧ (Ad * A)ᵀ = Ad * A

/-- Thin SVD `A = U_A Σ_A V_Aᵀ`: `U_A ∈ ℝ^{n×d}` has orthonormal columns (the top `d` left
singular vectors), `V_A` is orthogonal, and `Σ_A = diag(σ)` with nonnegative,
nonincreasing singular values. -/
def IsThinSVD {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) (U : Matrix (Fin n) (Fin d) ℝ)
    (σ : Fin d → ℝ) (V : Matrix (Fin d) (Fin d) ℝ) : Prop :=
  OrthonormalColumns U ∧ Vᵀ * V = 1 ∧ Antitone σ ∧ (∀ i, 0 ≤ σ i) ∧
    A = U * diagonal σ * Vᵀ

/-- `σ_max(A) = ‖A‖₂` (spectral norm). -/
noncomputable def sigmaMax {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) : ℝ := ‖A‖

/-- `σ_min(A)`: the smallest (d-th) singular value, `min_{‖y‖₂ = 1} ‖A y‖₂`. -/
noncomputable def sigmaMin {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) : ℝ :=
  sInf ((fun y : Fin d → ℝ => l2Norm (A *ᵥ y)) '' {y | l2Norm y = 1})

/-- The condition number `κ(A) = σ_max(A) / σ_min(A)`. -/
noncomputable def condNumber {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) : ℝ :=
  sigmaMax A / sigmaMin A

/-- `𝒵 = min_x ‖A x − b‖₂`, the optimal residual of the least squares problem. -/
noncomputable def lsResidual {n d : ℕ} (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ) : ℝ :=
  ⨅ x : Fin d → ℝ, l2Norm (A *ᵥ x - b)

/-- `b^⊥ = U_A^⊥ U_A^⊥ᵀ b = b − U_A U_Aᵀ b`, the part of `b` outside the column space of `A`. -/
noncomputable def bPerp {n d : ℕ} (U : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ) : Fin n → ℝ :=
  b - U *ᵥ (Uᵀ *ᵥ b)

/-- Condition (eqn:lemma1_ass1): `σ_i²(X U_A) ≥ 1/√2` for all `i = 1, …, d`, stated
equivalently as `‖X U_A y‖₂² ≥ (1/√2)‖y‖₂²` for all `y ∈ ℝ^d`. -/
def LemmaOneCondition1 {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ) : Prop :=
  ∀ y : Fin d → ℝ, (1 / Real.sqrt 2) * l2Norm y ^ 2 ≤ l2Norm ((X * U) *ᵥ y) ^ 2

/-- Condition (eqn:lemma1_ass2): `‖U_Aᵀ Xᵀ X b^⊥‖₂² ≤ ε 𝒵² / 2`, for a generic matrix `X`.

Symbol identification (restricted context, statement interpretation only): the source's
RandLeastSquares discussion (book.md:1048) instantiates the preconditioning matrix as
`X = Sᵀ H D`. Lemma lem:sample_lem40pf states that it establishes Condition
(eqn:lemma1_ass2) for this algorithm, and its displayed inequality is
`‖(SᵀHD U_A)ᵀ SᵀHD b^⊥‖₂² ≤ ε 𝒵²/2`. Writing `X` for `SᵀHD` gives
`‖(X U_A)ᵀ X b^⊥‖₂² = ‖U_Aᵀ Xᵀ X b^⊥‖₂² ≤ ε 𝒵²/2`. This identification only reads off
the form of the condition. No property of `S`, `H`, `D` or the algorithm is assumed here:
Lemma lem:suff_cond applies to any `X` (book.md:1061). -/
def LemmaOneCondition2 {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (U : Matrix (Fin n) (Fin d) ℝ) (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ)
    (ε : ℝ) : Prop :=
  l2Norm (Uᵀ *ᵥ (Xᵀ *ᵥ (X *ᵥ bPerp U b))) ^ 2 ≤ ε * lsResidual A b ^ 2 / 2

/-- `x̃_opt` solves the sketched problem (eqn:orig_ls_prob_Xrotated) `min_x ‖X(A x − b)‖₂`. -/
def IsSketchedLSSolution {r n d : ℕ} (X : Matrix (Fin r) (Fin n) ℝ)
    (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ) (xt : Fin d → ℝ) : Prop :=
  ∀ x : Fin d → ℝ, l2Norm (X *ᵥ (A *ᵥ xt - b)) ≤ l2Norm (X *ᵥ (A *ᵥ x - b))

/-- dm2017 Lemma lem:suff_cond2 (in the setting of Lemma lem:suff_cond): if
`‖U_A U_Aᵀ b‖₂ ≥ γ ‖b‖₂` for some `γ ∈ (0,1]`, then
`‖x_opt − x̃_opt‖₂ ≤ √ε (κ(A) √(γ⁻² − 1)) ‖x_opt‖₂`, with `x_opt = A^† b`.
The hypotheses of Lemma lem:suff_cond are expanded: the overconstrained problem
(`d ≤ n`, full column rank), `U_A` from the thin SVD, Conditions (eqn:lemma1_ass1) and
(eqn:lemma1_ass2) on `X` for some `ε ∈ (0,1)`, and `x̃_opt` solving the `X`-rotated problem. -/
theorem lem_suff_cond2 {n d r : ℕ}
    (A : Matrix (Fin n) (Fin d) ℝ) (b : Fin n → ℝ)
    (hnd : d ≤ n) (hA : FullColumnRank A)
    (U : Matrix (Fin n) (Fin d) ℝ) (σ : Fin d → ℝ) (V : Matrix (Fin d) (Fin d) ℝ)
    (hsvd : IsThinSVD A U σ V)
    (Ad : Matrix (Fin d) (Fin n) ℝ) (hAd : IsMoorePenroseInverse A Ad)
    (X : Matrix (Fin r) (Fin n) ℝ) (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1)
    (h1 : LemmaOneCondition1 X U) (h2 : LemmaOneCondition2 X U A b ε)
    (xt : Fin d → ℝ) (hxt : IsSketchedLSSolution X A b xt)
    (γ : ℝ) (hγ0 : 0 < γ) (hγ1 : γ ≤ 1)
    (hγb : γ * l2Norm b ≤ l2Norm (U *ᵥ (Uᵀ *ᵥ b))) :
    l2Norm (Ad *ᵥ b - xt) ≤
      Real.sqrt ε * (condNumber A * Real.sqrt ((γ ^ 2)⁻¹ - 1)) * l2Norm (Ad *ᵥ b) := by
  sorry

end RNLAPhaseB.DM2017LemSuffCond2