OAI/Analysis/KadisonKastler/BilateralBlockWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Three separated increment blocks in the double-ergodicity proof.

  1. def OAI.KadisonKastler.bilateralLeftWord line 15
  2. def OAI.KadisonKastler.bilateralMiddleWord line 16
  3. def OAI.KadisonKastler.bilateralRightWord line 17
  4. theorem OAI.KadisonKastler.bilateralLeftWord_measurable line 20
  5. theorem OAI.KadisonKastler.bilateralMiddleWord_measurable line 23
  6. theorem OAI.KadisonKastler.bilateralRightWord_measurable line 26
  7. theorem OAI.KadisonKastler.bilateral_block_word_factorization line 30
  8. theorem OAI.KadisonKastler.bilateralIncrementProduct_shift_coordinate_measurable line 39
  9. def OAI.KadisonKastler.bilateralSymmetricWindow line 50
  10. theorem OAI.KadisonKastler.exists_symmetricWindow_L2_approximation line 54