RandomizedRMS.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Elementary norm bounds for finite random vectors

theorem OAI.KadisonKastler.finiteRMS_eq_norm line 19
Source documentation
Finite root mean square is the normalized direct-sum norm.
```
theorem finiteRMS_eq_norm (v : Ω → H) :
    finiteRMS v = (Real.sqrt (Fintype.card Ω : ℝ))⁻¹ * ‖WithLp.toLp 2 v‖ := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.finiteRMS_add_le line 28
Source documentation
Minkowski's inequality for the finite random vectors in the row construction.
```
theorem finiteRMS_add_le (v w : Ω → H) :
    finiteRMS (fun i => v i + w i) ≤ finiteRMS v + finiteRMS w := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.finiteRMS_le_const line 36
Source documentation
A pointwise norm bound gives the same root mean square bound.
```
theorem finiteRMS_le_const [Nonempty Ω] (v : Ω → H) {C : ℝ}
    (hC : 0 ≤ C) (hv : ∀ i, ‖v i‖ ≤ C) : finiteRMS v ≤ C := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.finiteRMS_mono line 47
Source documentation
Pointwise norm domination passes through finite root mean squares.
```
theorem finiteRMS_mono (v w : Ω → H) (hv : ∀ i, ‖v i‖ ≤ ‖w i‖) :
    finiteRMS v ≤ finiteRMS w := by
…
```
Mentions: OAI.KadisonKastler.finiteRMS
theorem OAI.KadisonKastler.finiteRMS_sq line 54
Source documentation
Squaring finite root mean square recovers its average of squares.
```
theorem finiteRMS_sq (v : Ω → H) :
    (finiteRMS v) ^ 2 = 𝔼 i, ‖v i‖ ^ 2 :=
…
```
Mentions: OAI.KadisonKastler.finiteRMS

theorem OAI.KadisonKastler.phase_basis_double_rms_le line 62

Source documentation

Orthogonal scalar phases and a uniform basis row preserve bounds that already hold in root mean square over an independent random choice.

theorem phase_basis_double_rms_le {n : ℕ} [Nonempty Θ]
    (χ : I → Ω → ℂ)
    (hχ : ∀ i j, (𝔼 t, star (χ i t) * χ j t) = if i = j then 1 else 0)
    (v : I → Θ → Generator.FiniteHilbert (Fin n) H)
    {C : ℝ} (hC : 0 ≤ C) (hv : ∀ i, finiteRMS (v i) ≤ C) :
    finiteRMS (fun ta : (Θ × Ω) × Fin n => (Real.sqrt (n : ℝ)) •
      ((Real.sqrt (Fintype.card I : ℝ))⁻¹ •
        finitePhaseSum χ (fun i => v i ta.1.1) ta.1.2) ta.2) ≤ C := by
…

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