OAI/Analysis/KadisonKastler/ProductCentralizerDiffuse.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Diffuseness of the fixed product-state centralizer

Scalar center and small nonzero projections exclude minimal projections. This supplies the trace cuts used to assemble state-scaling isometries.

  1. theorem OAI.KadisonKastler.algebraProjection_trace_mono line 21
  2. theorem OAI.KadisonKastler.factor_no_minimal_of_small_projections line 29
  3. theorem OAI.KadisonKastler.diffuse_of_no_minimal line 45
  4. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_centralizer_scalarCenter line 68
  5. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_centralizer_diffuse line 74