Hadamard mixing of the leading right singular subspace

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

/-- The unnormalized (Sylvester) Hadamard matrix `H̃_n` of order `n = 2^p`,
written in closed form: entry `(i,j)` is `(-1)^{# of bit positions b < p where
both i and j have bit b set}`. This is the same matrix produced by the Sylvester
recursion `H̃_{2n} = [[H̃_n, H̃_n], [H̃_n, -H̃_n]]`, `H̃_1 = [1]`. -/
noncomputable def sylvesterHadamard (p : ℕ) : Matrix (Fin (2 ^ p)) (Fin (2 ^ p)) ℝ :=
  fun i j => (-1 : ℝ) ^
    ((Finset.range p).filter
      (fun b => i.val.testBit b = true ∧ j.val.testBit b = true)).card

/-- The normalized Hadamard transform `H_n = (1/√n) H̃_n`, with `n = 2^p`. -/
noncomputable def normalizedHadamard (p : ℕ) : Matrix (Fin (2 ^ p)) (Fin (2 ^ p)) ℝ :=
  (1 / Real.sqrt (((2 ^ p : ℕ) : ℝ))) • sylvesterHadamard p

/-- The law of a random sign: `+1` with probability `1/2` and `-1` with probability `1/2`. -/
noncomputable def rademacherMeasure : Measure ℝ :=
  (2⁻¹ : ℝ≥0∞) • (Measure.dirac (1 : ℝ) + Measure.dirac (-1 : ℝ))

/-- The random diagonal of `D` in the Randomized Hadamard Transform: each `D_ii`
is `+1` with probability `1/2` and `-1` with probability `1/2`, and the diagonal
entries are mutually independent. -/
structure RandomSignDiagonal {Ω : Type*} [MeasurableSpace Ω] {n : ℕ}
    (P : Measure Ω) (d : Ω → Fin n → ℝ) : Prop where
  entry_hasLaw : ∀ i, ProbabilityTheory.HasLaw (fun ω => d ω i) rademacherMeasure P
  entries_iIndep : ProbabilityTheory.iIndepFun (fun i ω => d ω i) P

/-- Lemma (lem:HUnew). Let `V_k` be an `n × k` matrix with orthonormal columns
(`n = 2^p`), and let `H D` be the `n × n` Randomized Hadamard Transform. Then with
probability at least `.95`, `‖(H D V_k)_{i*}‖₂² ≤ 2 k ln(40 n k) / n` for all
`i = 1, …, n`. -/
theorem lem_HUnew {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (p k : ℕ) (V : Matrix (Fin (2 ^ p)) (Fin k) ℝ) (hV : OrthonormalColumns V)
    (d : Ω → Fin (2 ^ p) → ℝ) (hd : RandomSignDiagonal P d) :
    (19 / 20 : ℝ≥0∞) ≤
      P {ω | ∀ i : Fin (2 ^ p),
        l2Norm ((normalizedHadamard p * Matrix.diagonal (d ω) * V) i) ^ 2 ≤
          2 * (k : ℝ) * Real.log (40 * ((2 ^ p : ℕ) : ℝ) * (k : ℝ)) / ((2 ^ p : ℕ) : ℝ)} := by
  sorry

end RNLAPhaseB.DM2017.HUnew