OAI/Analysis/KadisonKastler/ControlledPowerDrift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.controlled_word_error_identity line 19

   Source documentation

   Cancelling the test unitary separates the positive word error into its word commutator and the controlled lift commutator.

   theorem controlled_word_error_identity
       (T : K →L[ℂ] K) (Q s U : unitary (K →L[ℂ] K)) (ξ : K) :
       T (((Q : K →L[ℂ] K) * s * U) ξ) -
         ((Q : K →L[ℂ] K) * s * U) ((star (U : K →L[ℂ] K)) (T ((U : K →L[ℂ] K) ξ))) =
       (T * (Q : K →L[ℂ] K) - Q * T) ((s : K →L[ℂ] K) ((U : K →L[ℂ] K) ξ)) +
         (Q : K →L[ℂ] K) ((T * (s : K →L[ℂ] K) - s * T) ((U : K →L[ℂ] K) ξ)) := by
   …

2. theorem OAI.KadisonKastler.controlled_word_error_rms_le line 36

   Source documentation

   The controlled lift adds at most 2δ to the word's root mean square.

   theorem controlled_word_error_rms_le
       (T : K →L[ℂ] K) (Q : Ω → unitary (K →L[ℂ] K))
       (s U : unitary (K →L[ℂ] K)) (ξ : K) {δ : ℝ} (hδ : 0 ≤ δ)
       (hs : ‖T * (s : K →L[ℂ] K) - s * T‖ ≤ 2 * δ) :
       finiteRMS (fun θ => T (((Q θ : K →L[ℂ] K) * s * U) ξ) -
         ((Q θ : K →L[ℂ] K) * s * U)
           ((star (U : K →L[ℂ] K)) (T ((U : K →L[ℂ] K) ξ)))) ≤
       finiteRMS (fun θ => (T * (Q θ : K →L[ℂ] K) - Q θ * T)
         ((s : K →L[ℂ] K) ((U : K →L[ℂ] K) ξ))) + 2 * δ * ‖ξ‖ := by
   …

   Mentions: OAI.KadisonKastler.finiteRMS

3. theorem OAI.KadisonKastler.eventually_controlled_word_error line 59

   Source documentation

   The 68δ positive-word limit and the controlled lift give 70δ.

   theorem eventually_controlled_word_error
       (l : Filter J) (T : K →L[ℂ] K)
       (Q : J → Ω → unitary (K →L[ℂ] K))
       (s : J → unitary (K →L[ℂ] K)) (U : unitary (K →L[ℂ] K))
       (ξ : K) {δ : ℝ} (hδ : 0 ≤ δ)
       (hs : ∀ j, ‖T * (s j : K →L[ℂ] K) - s j * T‖ ≤ 2 * δ)
       (hword : ∀ ε > 0, ∀ᶠ j in l,
         finiteRMS (fun θ => (T * (Q j θ : K →L[ℂ] K) - Q j θ * T)
           ((s j : K →L[ℂ] K) ((U : K →L[ℂ] K) ξ))) ≤ 68 * δ * ‖ξ‖ + ε) :
       ∀ ε > 0, ∀ᶠ j in l,
         finiteRMS (fun θ => T (((Q j θ : K →L[ℂ] K) * s j * U) ξ) -
           ((Q j θ : K →L[ℂ] K) * s j * U)
   …

   Mentions: OAI.KadisonKastler.finiteRMS