OAI/Analysis/KadisonKastler/NondominatedVectorWitness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Two-vector witnesses when the test state is not dominated

A small positive cut of a projection of large relative state weight is equivalent to its complement in the type III factor. The resulting partial isometry has large test displacement and small reference displacement.

  1. theorem OAI.KadisonKastler.exists_nondominated_two_vector_witness line 23