OAI/Analysis/KadisonKastler/BilateralRandomWalk.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Independent forward and reflected backward random walks

  1. abbrev OAI.KadisonKastler.BilateralWalkPath line 15
  2. def OAI.KadisonKastler.bilateralWalkLaw line 17
  3. instance OAI.KadisonKastler.(instance at line 20) line 20
  4. def OAI.KadisonKastler.bilateralFuture line 24
  5. def OAI.KadisonKastler.bilateralPast line 26
  6. def OAI.KadisonKastler.bilateralReflectedPast line 28
  7. theorem OAI.KadisonKastler.bilateralFuture_measurable line 31
  8. theorem OAI.KadisonKastler.bilateralPast_measurable line 35
  9. theorem OAI.KadisonKastler.bilateralReflectedPast_measurable line 38
  10. theorem OAI.KadisonKastler.bilateralFuture_law line 42
  11. theorem OAI.KadisonKastler.bilateralPast_law line 46
  12. theorem OAI.KadisonKastler.bilateralReflectedPast_law line 54
  13. theorem OAI.KadisonKastler.bilateral_halves_independent line 65
  14. theorem OAI.KadisonKastler.bilateral_reflected_halves_independent line 94