Expected Frobenius norm after column 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.FNormExp

/-- Squared Frobenius norm `‖M‖_F^2 = ∑_{i,j} M_{ij}^2` of a real matrix. It is written
explicitly so that the scoped L2-operator norm opened in the header is not used. -/
def frobeniusNormSq {m n : ℕ} (M : Matrix (Fin m) (Fin n) ℝ) : ℝ :=
  ∑ i, ∑ j, (M i j) ^ 2

/-- The sampling-and-rescaling matrix `S ∈ ℝ^{n×c}` of RandLowRank (alg:alg_randlowrank,
steps 2-3). In trial `t` the index `idx t` is selected, and column `t` of `S` is
`sqrt(n/c) e_{idx t}`, where `e_i` is the `i`-th canonical vector of `ℝ^n`. -/
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

/-- The law of the sampled indices in RandLowRank step 3: `c` i.i.d. trials, drawn with
replacement, each selecting uniformly at random an integer in `{1,…,n}`. In Lean the
integers are `Fin n`, which is 0-based. -/
structure RandLowRankSampledIndices {Ω : Type*} [MeasurableSpace Ω] {n c : ℕ} [NeZero n]
    (P : Measure Ω) (idx : Ω → Fin c → Fin n) : Prop where
  isProbabilityMeasure : IsProbabilityMeasure P
  uniform : ∀ t : Fin c,
    ProbabilityTheory.HasLaw (fun ω => idx ω t) (PMF.uniformOfFintype (Fin n)).toMeasure P
  indep : ProbabilityTheory.iIndepFun (fun (t : Fin c) (ω : Ω) => idx ω t) P

/-- dm2017 lem:FNormExp. Let `S ∈ ℝ^{n×c}` be constructed as in RandLowRank.
The number of columns `c` is set by Eqn. (cval5):
`c ≥ c₀ (k ln n / ε²)(ln(k/ε²) + ln ln n)`,
where the rank parameter is `k`, the error parameter is `ε ∈ (0,1/2)`, and `c₀` is the
source's fixed constant. Then for every `X ∈ ℝ^{m×n}` we have
`E ‖XS‖_F² = ‖X‖_F²`, and with probability at least `0.95` we have
`‖XS‖_F² ≤ 20 ‖X‖_F²`. -/
theorem lem_FNormExp {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (m n c k : ℕ) [NeZero n] (ε c₀ : ℝ) (hε : 0 < ε ∧ ε < 1 / 2)
    (hc_pos : 0 < c)
    (hc : c₀ * ((k : ℝ) * Real.log n / ε ^ 2) *
        (Real.log ((k : ℝ) / ε ^ 2) + Real.log (Real.log n)) ≤ (c : ℝ))
    (idx : Ω → Fin c → Fin n) (hidx : RandLowRankSampledIndices P idx)
    (X : Matrix (Fin m) (Fin n) ℝ) :
    (∫ ω, frobeniusNormSq (X * samplingMatrix (idx ω)) ∂P) = frobeniusNormSq X ∧
    (19 / 20 : ℝ≥0∞) ≤
      P {ω | frobeniusNormSq (X * samplingMatrix (idx ω)) ≤ 20 * frobeniusNormSq X} := by
  sorry

end RNLAPhaseB.DM2017.FNormExp