OAI/Analysis/KadisonKastler/FiniteFactorDixmier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Dixmier averaging for every represented finite factor

  1. theorem OAI.KadisonKastler.publishedDixmierOfFiniteTypeI line 21

    Source documentation

    Finiteness in a type I factor forces its minimal cyclic representation to have a finite orthonormal basis.

    theorem publishedDixmierOfFiniteTypeI (hM : IsTypeIFactor M)
    (hfinite : FiniteProjectionIn M 1) : PublishedDixmierAveraging M := by
…

    Mentions: OAI.KadisonKastler.IsTypeIFactor, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.PublishedDixmierAveraging

  2. theorem OAI.KadisonKastler.publishedDixmierOfFiniteFactor line 52

    Source documentation

    Dixmier averaging on finite factors is independent of their represented Hilbert-space multiplicity.

    theorem publishedDixmierOfFiniteFactor (hM : ScalarCenter M)
    (hfinite : FiniteProjectionIn M 1) : PublishedDixmierAveraging M := by
…

    Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.FiniteProjectionIn, OAI.KadisonKastler.PublishedDixmierAveraging