OAI/Analysis/KadisonKastler/SmallVectorSubprojection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Small positive vector-state cuts in type III algebras

Restricting to the vector support makes every nonzero subprojection have positive weight. Repeated proper splitting then makes that weight small.

  1. theorem OAI.KadisonKastler.vector_projection_sub_weight line 22
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_half_vector_subprojection line 37
  3. theorem OAI.KadisonKastler.TypeIIIFactor.exists_geometric_vector_subprojection line 53
  4. theorem OAI.KadisonKastler.TypeIIIFactor.exists_small_positive_vector_subprojection line 68