OAI/Analysis/KadisonKastler/PublishedCentralDecomposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The published common central decomposition input

Blackadar, Operator Algebras (Springer, 2006), III.1.6.2--4 and III.5.1.10--14: central decomposition on separable Hilbert space, simultaneous decomposition of norm-separable C-star subalgebras, and reconstruction of bounded measurable fields. The common C-star algebra is required to commute with the common center so that it is decomposable. The dimension strata are trivialized over standard Borel spaces with finite measures.

Only this structural input is retained. In particular, the proposition below contains no distance estimate, implementer or stability conclusion.

  1. structure OAI.KadisonKastler.MeasuredHilbertStratum line 30
  2. abbrev OAI.KadisonKastler.MeasuredHilbertStratum.space line 49
  3. def OAI.KadisonKastler.ScalarCenter line 51
  4. structure OAI.KadisonKastler.CentralPairDecomposition line 57
  5. def OAI.KadisonKastler.PublishedCentralPairDecomposition line 82

    Source documentation

    The central case of the cited decomposition and reconstruction results, for one pair and one chosen norm-separable common C-star algebra.

    def PublishedCentralPairDecomposition : Prop :=
…