OAI/Analysis/KadisonKastler/CenteredTestCentralVectors.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Moving the detected centered test to approximate central vectors

The remote coisometries shift either side of the modular eigenvalue one. Their existence is supplied by the constructed spatial matrix product.

  1. theorem OAI.KadisonKastler.real_lt_of_close line 25
  2. theorem OAI.KadisonKastler.centeredTest_approximate_central_vectors line 32