RandomizedRows.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The mean-square normalization of the randomized rows

theorem OAI.KadisonKastler.normalized_phase_mean_square line 19

Source documentation

Normalizing a finite orthogonal phase sum removes its number of terms from the mean square.

theorem normalized_phase_mean_square (χ : I → Ω → ℂ)
    (hχ : ∀ i j, (𝔼 t, star (χ i t) * χ j t) = if i = j then 1 else 0)
    (v : I → H) (x : H) (hv : ∀ i, ‖v i‖ = ‖x‖) :
    (𝔼 t, ‖(Real.sqrt (Fintype.card I : ℝ))⁻¹ • finitePhaseSum χ v t‖ ^ 2) = ‖x‖ ^ 2 := by
…

Mentions: OAI.KadisonKastler.finitePhaseSum

theorem OAI.KadisonKastler.basis_row_mean_square line 35
Source documentation
Averaging a uniformly chosen basis row, with the factor sqrt n, preserves the Hilbert direct-sum norm exactly.
```
theorem basis_row_mean_square (x : Generator.FiniteHilbert (Fin n) H) :
    (𝔼 a : Fin n, ‖(Real.sqrt (n : ℝ)) • x a‖ ^ 2) = ‖x‖ ^ 2 := by
…
```
Mentions: OAI.Generator.FiniteHilbert

theorem OAI.KadisonKastler.phase_basis_row_mean_square line 46

Source documentation

Independent choice of a phase and a basis row produces a row family of mean-square norm exactly that of the original vector.

theorem phase_basis_row_mean_square (χ : I → Ω → ℂ)
    (hχ : ∀ i j, (𝔼 t, star (χ i t) * χ j t) = if i = j then 1 else 0)
    (v : I → Generator.FiniteHilbert (Fin n) H)
    (x : Generator.FiniteHilbert (Fin n) H) (hv : ∀ i, ‖v i‖ = ‖x‖) :
    (𝔼 ta : Ω × Fin n,
      ‖(Real.sqrt (n : ℝ)) •
        ((Real.sqrt (Fintype.card I : ℝ))⁻¹ • finitePhaseSum χ v ta.1) ta.2‖ ^ 2) = ‖x‖ ^ 2 := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.finitePhaseSum