Spectral accuracy of leverage-based row sampling

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.Theorem7Correct

/-- The sampling-probability conditions of Eqn. (eqn:appopt4):
`∑_k p_k = 1` and `p_k ≥ β ‖U_{k*}‖₂² / d` for all `k = 1, …, n`. -/
def SamplingProbabilitiesCondition {n d : ℕ} (U : Matrix (Fin n) (Fin d) ℝ)
    (β : ℝ) (p : Fin n → ℝ) : Prop :=
  (∑ k, p k = 1) ∧ ∀ k, β * (l2Norm (U k)) ^ 2 / (d : ℝ) ≤ p k

/-- The index draws of RandMatrixMultiply: for `t = 1, …, c`, `i_t ∈ {1,…,n}` is picked
with `Pr[i_t = k] = p_k`, independently and with replacement. -/
def RandMatrixMultiplyIndexSampling {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {n c : ℕ} (p : Fin n → ℝ) (idx : Ω → Fin c → Fin n) : Prop :=
  (∀ t, Measurable (fun ω => idx ω t)) ∧
  (∀ t k, P {ω | idx ω t = k} = ENNReal.ofReal (p k)) ∧
  ProbabilityTheory.iIndepFun (fun t ω => idx ω t) P

/-- The matrix `R ∈ ℝ^{c×d}` returned by RandMatrixMultiply with `A = Uᵀ`, `B = U`:
`R_{t*} = (1 / sqrt(c p_{i_t})) U_{i_t *}`. -/
noncomputable def randMatrixMultiplyR {n d c : ℕ} (U : Matrix (Fin n) (Fin d) ℝ)
    (p : Fin n → ℝ) (i : Fin c → Fin n) : Matrix (Fin c) (Fin d) ℝ :=
  fun t j => (1 / Real.sqrt ((c : ℝ) * p (i t))) * U (i t) j

/-- dm2017 thm:theorem7correct. `U ∈ ℝ^{n×d}` with `UᵀU = I_d`; `R` is built by
RandMatrixMultiply (inputs `A = Uᵀ`, `B = U`, integer `1 ≤ c ≤ n`, `p_k ≥ 0`) with
probabilities satisfying Eqn. (eqn:appopt4) for some `β ∈ (0,1]`; `ε ∈ (0,1)`;
`c ≥ (96d/(βε²)) ln(96d/(βε²√δ))`. Then with probability at least `1-δ`,
`‖UᵀU − RᵀR‖₂ = ‖I_d − RᵀR‖₂ ≤ ε` (spectral norm). The informal `n ≫ d` is not a
precise hypothesis and is not encoded; `δ > 0` is the domain of `ln(·/√δ)`. -/
theorem theorem7correct {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] {n d c : ℕ}
    (U : Matrix (Fin n) (Fin d) ℝ) (hU : Uᵀ * U = 1)
    (p : Fin n → ℝ) (hp_nonneg : ∀ k, 0 ≤ p k)
    (β : ℝ) (hβ0 : 0 < β) (hβ1 : β ≤ 1)
    (hp : SamplingProbabilitiesCondition U β p)
    (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1)
    (δ : ℝ) (hδ : 0 < δ)
    (hc1 : 1 ≤ c) (hcn : c ≤ n)
    (hc : 96 * (d : ℝ) / (β * ε ^ 2) *
        Real.log (96 * (d : ℝ) / (β * ε ^ 2 * Real.sqrt δ)) ≤ (c : ℝ))
    (idx : Ω → Fin c → Fin n)
    (hidx : RandMatrixMultiplyIndexSampling P p idx) :
    ENNReal.ofReal (1 - δ) ≤
      P {ω |
        ‖Uᵀ * U - (randMatrixMultiplyR U p (idx ω))ᵀ * randMatrixMultiplyR U p (idx ω)‖ =
          ‖(1 : Matrix (Fin d) (Fin d) ℝ) -
            (randMatrixMultiplyR U p (idx ω))ᵀ * randMatrixMultiplyR U p (idx ω)‖ ∧
        ‖(1 : Matrix (Fin d) (Fin d) ℝ) -
            (randMatrixMultiplyR U p (idx ω))ᵀ * randMatrixMultiplyR U p (idx ω)‖ ≤ ε} := by
  sorry

end RNLAPhaseB.DM2017.Theorem7Correct