OAI/Analysis/KadisonKastler/TypeIIIDixmierConclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_scalar_average line 19

   Source documentation

   Spectral matrices and two successive self-adjoint averages handle every operator of the factor.

   theorem TypeIIIFactor.exists_scalar_average (hM : TypeIIIFactor M)
       (x : Algebra M) (ε : ℝ) (hε : 0 < ε) :
       ∃ (A : FiniteInnerAverage M) (z : ℂ),
         ‖A.apply x.val - z • (1 : H →L[ℂ] H)‖ < ε :=
   …

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

2. theorem OAI.KadisonKastler.publishedDixmierOfTypeIII line 26

   Source documentation

   Finite inner averages of a type III factor approximate scalars.

   theorem publishedDixmierOfTypeIII (hM : TypeIIIFactor M) : PublishedDixmierAveraging M := by
   …

   Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.PublishedDixmierAveraging