OAI/Analysis/KadisonKastler/ModularGraphAction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.modularComparisonField_continuous line 18
2. theorem OAI.KadisonKastler.modularComparisonField_star_continuous line 36
3. theorem OAI.KadisonKastler.uniform_common_action_of_rescaled_graphs line 51

   Source documentation

   The graph estimate now supplies both frequency defects. The uniform tolerance and linear conjugacy constant precede all representation data.

   theorem uniform_common_action_of_rescaled_graphs
       (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})
       {B : ℝ} (hB : 0 ≤ B) :
   …

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