OAI/Analysis/KadisonKastler/ExpectedFromBicentralizer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The expected subfactor from the ambient state properties

The relative algebras require no additional homogeneity or bicentralizer assumptions: both properties transfer through the constructed spatial matrix-corner isomorphism.

  1. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_bicentralizer line 26