OAI/Analysis/KadisonKastler/SmoothedNormalizerLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.operatorConjugation_weak_tendsto line 25

   Source documentation

   Strong convergence of the adjoints already gives weak convergence of the conjugated operators. No norm convergence of the smoothing is used.

   theorem operatorConjugation_weak_tendsto {l : Filter ι}
       (Q : ι → (H →L[ℂ] H)) (W : H →L[ℂ] H)
       (hstar : ∀ x, Tendsto (fun i => star (Q i) x) l (𝓝 (star W x)))
       (a : H →L[ℂ] H) (x y : H) :
       Tendsto (fun i => inner ℂ y (operatorConjugationLinear (Q i) a x)) l
         (𝓝 (inner ℂ y (operatorConjugationLinear W a x))) := by
   …

   Mentions: OAI.KadisonKastler.operatorConjugationLinear

2. theorem OAI.KadisonKastler.exists_normalizer_of_smoothed_approximation line 45

   Source documentation

   A uniformly bounded strong-star approximation to a unitary, uniformly close to exact normalizers, yields an actual normalizer with a universal linear displacement estimate. This is the UCP limit step in Section 7.

   theorem exists_normalizer_of_smoothed_approximation
       (P : VonNeumannAlgebra H) (W : unitary (H →L[ℂ] H))
       (hCorrection : PublishedMultiplicationCorrection (unitaryConjugateAlgebra W P))
       (hCommutant : PublishedBlockCommutantApproximation
         (Algebra (unitaryConjugateAlgebra W P)) H)
       (ω : Ultrafilter ι) (V : ι → unitary (H →L[ℂ] H))
       (hV : ∀ i, Conjugates (V i) P P) (Q : ι → H →L[ℂ] H)
       (hstar : ∀ x, Tendsto (fun i => star (Q i) x) (ω : Filter ι)
         (𝓝 (star (W : H →L[ℂ] H) x)))
       {C d g : ℝ} (hC : 0 ≤ C) (hd : 0 ≤ d)
       (hQ : ∀ i, ‖Q i‖ ≤ C) (hVQ : ∀ i, ‖(V i : H →L[ℂ] H) - Q i‖ ≤ d)
       (hsmall : (1 + C) * d < 1 / 1000) (hge : g + (1 + C) * d < 1)
   …

   Mentions: OAI.KadisonKastler.PublishedMultiplicationCorrection, OAI.KadisonKastler.unitaryConjugateAlgebra, OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.Conjugates