Tail error from pseudoinverse perturbation

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017.SampleLem40pfn2

/-- Number of common one-bits of `i` and `j` among the `q` binary digits. -/
def hadamardBitInner (q : ℕ) (i j : Fin (2 ^ q)) : ℕ :=
  ((Finset.range q).filter
    (fun b => i.val.testBit b = true ∧ j.val.testBit b = true)).card

/-- Normalized (Sylvester) Hadamard matrix of size `n = 2^q`:
`H i j = n^{-1/2} (-1)^{⟨bits i, bits j⟩}`. -/
noncomputable def normalizedHadamard (q : ℕ) : Matrix (Fin (2 ^ q)) (Fin (2 ^ q)) ℝ :=
  fun i j => (Real.sqrt ((2 : ℝ) ^ q))⁻¹ * (-1 : ℝ) ^ (hadamardBitInner q i j)

/-- Sampling-and-rescaling matrix `S ∈ ℝ^{n×c}`: column `t` is `√(n/c) e_{idx t}`. -/
noncomputable def samplingMatrix {n c : ℕ} (idx : Fin c → Fin n) :
    Matrix (Fin n) (Fin c) ℝ :=
  fun i t => if idx t = i then Real.sqrt ((n : ℝ) / (c : ℝ)) else 0

/-- Squared Frobenius norm. -/
def frobSq {a b : ℕ} (M : Matrix (Fin a) (Fin b) ℝ) : ℝ :=
  ∑ i, ∑ j, (M i j) ^ 2

/-- `Y` is the Moore–Penrose pseudoinverse of `X`. -/
def IsMoorePenroseInverse {k c : ℕ} (X : Matrix (Fin k) (Fin c) ℝ)
    (Y : Matrix (Fin c) (Fin k) ℝ) : Prop :=
  X * Y * X = X ∧ Y * X * Y = Y ∧ (X * Y)ᵀ = X * Y ∧ (Y * X)ᵀ = Y * X

/-- Full SVD `A = U Σ Vᵀ`, `U`,`V` orthogonal, `Σ` rectangular diagonal with
nonnegative nonincreasing diagonal. -/
structure IsSVD {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (U : Matrix (Fin m) (Fin m) ℝ)
    (Sig : Matrix (Fin m) (Fin n) ℝ) (V : Matrix (Fin n) (Fin n) ℝ) : Prop where
  U_orth : Uᵀ * U = 1
  V_orth : Vᵀ * V = 1
  diag : ∀ i j, i.val ≠ j.val → Sig i j = 0
  nonneg : ∀ i j, i.val = j.val → 0 ≤ Sig i j
  antitone : ∀ i j i' j', i.val = j.val → i'.val = j'.val → i.val ≤ i'.val →
    Sig i' j' ≤ Sig i j
  factor : A = U * Sig * Vᵀ

/-- `A_k = U_k Σ_k V_kᵀ` (eqn:svdnotation). -/
noncomputable def truncatedSVD {m n k : ℕ} (U : Matrix (Fin m) (Fin m) ℝ)
    (Sig : Matrix (Fin m) (Fin n) ℝ) (V : Matrix (Fin n) (Fin n) ℝ)
    (hkm : k ≤ m) (hkn : k ≤ n) : Matrix (Fin m) (Fin n) ℝ :=
  U.submatrix id (Fin.castLE hkm) * Sig.submatrix (Fin.castLE hkm) (Fin.castLE hkn) *
    (V.submatrix id (Fin.castLE hkn))ᵀ

/-- Law of the diagonal of `D`: i.i.d. entries equal to `±1` with probability `1/2` each. -/
structure RademacherDiagonalLaw {Ω : Type*} [MeasurableSpace Ω] {n : ℕ}
    (P : Measure Ω) (d : Ω → Fin n → ℝ) : Prop where
  meas : ∀ i, Measurable (fun ω => d ω i)
  values : ∀ ω i, d ω i = 1 ∨ d ω i = -1
  plus : ∀ i, P {ω | d ω i = 1} = 1 / 2
  minus : ∀ i, P {ω | d ω i = -1} = 1 / 2
  indep : ProbabilityTheory.iIndepFun (fun i ω => d ω i) P

/-- Law of the sampled indices: `c` i.i.d. uniform draws from `{1,…,n}`, with replacement. -/
structure UniformWithReplacementLaw {Ω : Type*} [MeasurableSpace Ω] {n c : ℕ}
    (P : Measure Ω) (idx : Ω → Fin c → Fin n) : Prop where
  meas : ∀ t, Measurable (fun ω => idx ω t)
  uniform : ∀ t j, P {ω | idx ω t = j} = ((n : ℝ≥0∞))⁻¹
  indep : ProbabilityTheory.iIndepFun (fun t ω => idx ω t) P

/-- Eqn. (eqn:lem:HU_eqn2new): `‖(H D V_k)_{i*}‖₂² ≤ 2k ln(40nk)/n` for all `i`. -/
def HUEqn2New {n k : ℕ} (H D : Matrix (Fin n) (Fin n) ℝ) (Vk : Matrix (Fin n) (Fin k) ℝ) :
    Prop :=
  ∀ i, l2Norm (fun j => (H * D * Vk) i j) ^ 2 ≤
    2 * (k : ℝ) * Real.log (40 * (n : ℝ) * (k : ℝ)) / (n : ℝ)

/-- Eqn. (eqn:ppdd2). -/
def Ppdd2 (k n c : ℕ) (ε : ℝ) : Prop :=
  (c : ℝ) ≥ 192 * (k : ℝ) * Real.log (40 * (n : ℝ) * (k : ℝ)) / ε ^ 2 *
    Real.log (192 * Real.sqrt 20 * (k : ℝ) * Real.log (40 * (n : ℝ) * (k : ℝ)) / ε ^ 2)

/-- dm2017 Lemma lem:sample_lem40pfn2. `A = UΣVᵀ`, `V_k` = first `k` columns of `V`,
`A_{k,⊥} = A − U_kΣ_kV_kᵀ`, `n = 2^q`, `H` normalized Hadamard, `D = diag(d)`,
`S = samplingMatrix idx` as in RandLowRank; `Xp ω = (V_kᵀ D H S)^†`. The lemma is
conditioned on Eqn. (eqn:lem:HU_eqn2new) (event `F`); the conditional probability
`P(E | F) ≥ .9` is written as `0.9 · P F ≤ P (F ∩ E)`. `ε ∈ (0,1/2]` is inherited from
thm:relerrLowRank, whose proof this lemma belongs to. -/
theorem sample_lem40pfn2
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (m q k c : ℕ) (hkm : k ≤ m) (hkn : k ≤ 2 ^ q)
    (A : Matrix (Fin m) (Fin (2 ^ q)) ℝ) (U : Matrix (Fin m) (Fin m) ℝ)
    (Sig : Matrix (Fin m) (Fin (2 ^ q)) ℝ) (V : Matrix (Fin (2 ^ q)) (Fin (2 ^ q)) ℝ)
    (hSVD : IsSVD A U Sig V)
    (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε ≤ 1 / 2)
    (d : Ω → Fin (2 ^ q) → ℝ) (hd : RademacherDiagonalLaw P d)
    (idx : Ω → Fin c → Fin (2 ^ q)) (hidx : UniformWithReplacementLaw P idx)
    (hindep : ProbabilityTheory.IndepFun d idx P)
    (Xp : Ω → Matrix (Fin c) (Fin k) ℝ)
    (hXp : ∀ ω, IsMoorePenroseInverse
      ((V.submatrix id (Fin.castLE hkn))ᵀ * Matrix.diagonal (d ω) * normalizedHadamard q *
        samplingMatrix (idx ω)) (Xp ω))
    (hc : Ppdd2 k (2 ^ q) c ε) :
    let H := normalizedHadamard q
    let Vk := V.submatrix id (Fin.castLE hkn)
    let Aperp := A - truncatedSVD U Sig V hkm hkn
    let X := fun ω => Vkᵀ * Matrix.diagonal (d ω) * H * samplingMatrix (idx ω)
    let F := {ω | HUEqn2New H (Matrix.diagonal (d ω)) Vk}
    let E := {ω | 2 * frobSq (Aperp * Matrix.diagonal (d ω) * H * samplingMatrix (idx ω) *
        (Xp ω - (X ω)ᵀ)) ≤ 80 * ε ^ 2 * frobSq Aperp}
    (9 / 10 : ℝ≥0∞) * P F ≤ P (F ∩ E) := by
  sorry

end RNLAPhaseB.DM2017.SampleLem40pfn2