OAI/Analysis/KadisonKastler/ExpectedFromCentralLine.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The expected subfactor from a nonfaithful central line

The support corner and its conjugate support restore a cyclic separating vector on the original representation. Thus the central line need not itself consist of separating vectors before the corner transfer.

  1. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_supported_central_line line 25