OAI/Analysis/KadisonKastler/SmoothedNormalizerPaths.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact normalizers from approximate-normalizer smoothing paths

The path estimate produces algebra/commutant products independently at each smoothing scale. The UCP limit argument then recovers one exact normalizer without requiring the chosen products, or the polar paths, to converge.

  1. theorem OAI.KadisonKastler.exists_normalizer_of_infDist_lt line 29
  2. theorem OAI.KadisonKastler.exists_normalizer_of_smoothed_infDist line 41
  3. theorem OAI.KadisonKastler.uniform_typeIII_smoothed_normalizers line 69

    Source documentation

    Smoothing estimates give normalizers with constants chosen before the Hilbert space and the type III factor.

    theorem uniform_typeIII_smoothed_normalizers
    (hSpectral : PublishedVonNeumannSpectralCut.{u})
    (hCompare : PublishedTypeIIIProjectionComparison.{u})
    (hSakai : PublishedSimpleDerivationInner.{u})
    (hDistance : ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H], ∀ M : VonNeumannAlgebra H,
        PublishedBlockCommutantApproximation (Algebra M) H) :
    ∃ e0 K : ℝ, 0 < e0 ∧ 0 < K ∧
      ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
        [CompleteSpace H] [TopologicalSpace.SeparableSpace H],
      ∀ (M : VonNeumannAlgebra H), TypeIIIFactor M →
      ∀ W : unitary (H →L[ℂ] H),
…

    Mentions: OAI.KadisonKastler.PublishedBlockCommutantApproximation, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TypeIIIFactor