NormalizerLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Recovering a normalizer from weak limits of conjugations

The smoothing argument supplies exact normalizers close to moving linear maps. Only the latter maps need to converge. A weak limit of the actual conjugations is UCP and has range in the original algebra; the complete error bound then gives a nearby exact normalizer.

theorem OAI.KadisonKastler.complete_bound_of_two_weak_limits line 36

Source documentation

A complete bound survives when both compared maps vary and converge only on individual weak operator coefficients.

theorem complete_bound_of_two_weak_limits
    (F R : ι → A →ₗ[ℂ] (H →L[ℂ] H)) (S ρ : A →ₗ[ℂ] (H →L[ℂ] H))
    (hF : ∀ a x y, Tendsto (fun i => inner ℂ y (F i a x)) l
      (𝓝 (inner ℂ y (S a x))))
    (hR : ∀ a x y, Tendsto (fun i => inner ℂ y (R i a x)) l
      (𝓝 (inner ℂ y (ρ a x))))
    {e : ℝ} (he : 0 ≤ e) (hclose : ∀ i, CompletelyBoundedBy (F i - R i) e) :
    CompletelyBoundedBy (S - ρ) e := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.exists_normalizer_of_weak_comparison line 58

Source documentation

The modular smoothing limit step. The comparison maps may be neither positive nor multiplicative. The exact conjugations supply positivity and range membership, while the comparison maps supply the limit representation.

theorem exists_normalizer_of_weak_comparison
    (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)
    (R : ι → Algebra P →ₗ[ℂ] (H →L[ℂ] H))
    (hR : ∀ a x y, Tendsto (fun i => inner ℂ y (R i a x)) (ω : Filter ι)
      (𝓝 (inner ℂ y (unitaryConj W a x))))
    {e g : ℝ} (he : 0 ≤ e) (hesmall : e < 1 / 1000)
    (hge : g + e < 1) (hgap : kkDistance (unitaryConjugateAlgebra W P) P < g)
…

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