OAI/Analysis/KadisonKastler/RandomWalkPathAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The nonsingular action on rooted random-walk paths

The root is separated from the sequence of increments. Left translation changes only the root, and commutes with advancing the random walk.

  1. abbrev OAI.KadisonKastler.RandomWalkPath line 21
  2. def OAI.KadisonKastler.randomWalkPathLaw line 23
  3. instance OAI.KadisonKastler.randomWalkPathLaw_probability line 26
  4. def OAI.KadisonKastler.randomWalkPathAction line 30
  5. theorem OAI.KadisonKastler.randomWalkPathAction_apply line 40
  6. def OAI.KadisonKastler.randomWalkAdvance line 43
  7. theorem OAI.KadisonKastler.randomWalkAdvance_measurable line 46
  8. theorem OAI.KadisonKastler.randomWalkAdvance_action line 52
  9. theorem OAI.KadisonKastler.randomWalkAdvance_iterate_action line 59
  10. def OAI.KadisonKastler.randomWalkPosition line 68
  11. theorem OAI.KadisonKastler.randomWalkPosition_action line 71