OAI/Analysis/KadisonKastler/TypeIIICommutantSpatialSplit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Spatial splitting when the commutant is a separably acting type III factor

This is the type III commutant step of Sakai's spatial innerness proof. Compact minimization, finite unitary averages and spectral projection comparison supply every part of the argument.

  1. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_typeIII_commutant_of_projection_countability line 22
  2. theorem OAI.KadisonKastler.exists_selfAdjoint_split_of_typeIII_commutant line 77