OAI/Analysis/KadisonKastler/PhaseRowDrift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.normalized_phase_mean_square_le line 20

   Source documentation

   The normalized orthogonal phase sum preserves a uniform bound on its terms in mean square, independently of the number of terms.

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

   Mentions: OAI.KadisonKastler.finitePhaseSum

2. theorem OAI.KadisonKastler.phase_basis_row_drift_le line 36

   Source documentation

   The subsequent choice of a basis row also preserves that uniform mean-square bound.

   theorem phase_basis_row_drift_le {n : ℕ} (χ : 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, ‖v i‖ ≤ C) :
       finiteRMS (fun ta : Ω × Fin n => (Real.sqrt (n : ℝ)) •
         ((Real.sqrt (Fintype.card I : ℝ))⁻¹ • finitePhaseSum χ v ta.1) ta.2) ≤ C := by
   …

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

3. theorem OAI.KadisonKastler.eventually_phase_basis_row_drift_le line 54

   Source documentation

   Finitely many eventual power-drift estimates pass to the row drift with no loss depending on the number of powers or the matrix size.

   theorem eventually_phase_basis_row_drift_le {n : ℕ} (l : Filter J)
       (χ : I → Ω → ℂ)
       (hχ : ∀ i j, (𝔼 t, star (χ i t) * χ j t) = if i = j then 1 else 0)
       (v : J → I → Generator.FiniteHilbert (Fin n) H)
       {C : ℝ} (hC : 0 ≤ C)
       (hv : ∀ i, ∀ ε > 0, ∀ᶠ j in l, ‖v j i‖ ≤ C + ε) :
       ∀ ε > 0, ∀ᶠ j in l,
         finiteRMS (fun ta : Ω × Fin n => (Real.sqrt (n : ℝ)) •
           ((Real.sqrt (Fintype.card I : ℝ))⁻¹ • finitePhaseSum χ (v j) ta.1) ta.2) ≤ C + ε := by
   …

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