Hadamard mixing of an orthonormal basis

import RNLAPhaseB.B3Base
import RNLAPhaseB.Complexity

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

namespace RNLAPhaseB.DM2017LemHU

/-- The unnormalized (Sylvester) Hadamard matrix `H̃_n` of order `n = 2^k`, given by
the closed form of the recursion `H̃_1 = [1]`, `H̃_{2n} = [[H̃_n, H̃_n], [H̃_n, -H̃_n]]`:
with 0-based indices, the `(i, j)` entry is `(-1)^{⟨bits(i), bits(j)⟩}`. -/
noncomputable def unnormalizedHadamard (k : ℕ) : Matrix (Fin (2 ^ k)) (Fin (2 ^ k)) ℝ :=
  fun i j => (-1 : ℝ) ^
    ((Finset.range k).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^k`. -/
noncomputable def normalizedHadamard (k : ℕ) : Matrix (Fin (2 ^ k)) (Fin (2 ^ k)) ℝ :=
  (1 / Real.sqrt ((2 : ℝ) ^ k)) • unnormalizedHadamard k

/-- The random diagonal of the Randomized Hadamard Transform: each diagonal entry
`D_ii` is `+1` with probability `1/2` and `-1` with probability `1/2`, the entries
being independent. -/
structure RademacherDiagonalSigns {Ω : Type*} [MeasurableSpace Ω] {n : ℕ}
    (P : Measure Ω) (s : Ω → Fin n → ℝ) : Prop where
  measurable : ∀ i, Measurable (fun ω => s ω i)
  prob_plus : ∀ i, P {ω | s ω i = 1} = 1 / 2
  prob_minus : ∀ i, P {ω | s ω i = -1} = 1 / 2
  indep : ProbabilityTheory.iIndepFun (fun i ω => s ω i) P

/-- Lemma (dm2017, lem:HU). Let `U` be an `n × d` orthogonal matrix (orthonormal
columns) and `HD` the `n × n` Randomized Hadamard Transform (`n = 2^k`). Then with
probability at least `.95`, `‖(HDU)_{i*}‖_2^2 ≤ 2 d ln(40 n d) / n` for all `i`. -/
theorem lem_HU {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (k d : ℕ) (U : Matrix (Fin (2 ^ k)) (Fin d) ℝ) (hU : Uᵀ * U = 1)
    (s : Ω → Fin (2 ^ k) → ℝ) (hs : RademacherDiagonalSigns P s) :
    (95 / 100 : ℝ≥0∞) ≤ P {ω | ∀ i : Fin (2 ^ k),
      (l2Norm (fun j => (normalizedHadamard k * Matrix.diagonal (s ω) * U) i j)) ^ 2 ≤
        2 * (d : ℝ) * Real.log (40 * ((2 : ℝ) ^ k) * (d : ℝ)) / ((2 : ℝ) ^ k)} := by
  sorry

end RNLAPhaseB.DM2017LemHU