OAI/Analysis/KadisonKastler/ModularProductTest.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The centered separating test for the bicentralizer criterion

These are the exact product-state moments used in Marrakchi, arXiv:1811.10253v2, proof of Theorem D. The test has expectation one. The approximate-eigenstate selection needed after this computation is separate.

  1. theorem OAI.KadisonKastler.ModularConjugationData.rightAction_vectorState line 26
  2. theorem OAI.KadisonKastler.vectorState_square_value line 37
  3. theorem OAI.KadisonKastler.vectorState_star_value line 44
  4. def OAI.KadisonKastler.modularCenteredTest line 50
  5. theorem OAI.KadisonKastler.modularCenteredTest_selfAdjoint line 54
  6. theorem OAI.KadisonKastler.modularCenteredTest_product_value line 58