OAI/Analysis/KadisonKastler/FrequencyNormalizer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact normalizers from the constructed frequency smoothing

All constants precede the Hilbert space and algebra. The previously proved polar-path theorem is applied to the actual Poisson operators at positive heights tending to zero.

  1. theorem OAI.KadisonKastler.uniform_typeIII_normalizer_from_frequency_smoothing line 29
  2. theorem OAI.KadisonKastler.uniform_typeIII_normalizer_from_frequency_defects line 125

    Source documentation

    The analytic approximation and exact-normalizer construction applied straight to the two concrete frequency-cut defects.

    theorem uniform_typeIII_normalizer_from_frequency_defects
    (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)
    (hHardy : PublishedHardyMultiplierEvaluation.{u})
    (hNest : PublishedRealNestDistance.{u})
    (hRealSpectral : PublishedRealSpectralCommutant.{u})
    (hDiagonal : PublishedRealDiagonalDecomposition.{u}) :
    ∃ δ0 K : ℝ, 0 < δ0 ∧ 0 < K ∧
…

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