OAI/Analysis/KadisonKastler/RandomWalkShiftLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Independence of the first increment and the remaining random walk

  1. theorem OAI.KadisonKastler.independent_first_increment_tail line 16
  2. theorem OAI.KadisonKastler.iid_first_increment_tail_law line 37
  3. def OAI.KadisonKastler.randomWalkSplit line 51
  4. theorem OAI.KadisonKastler.randomWalkSplit_measurable line 55
  5. theorem OAI.KadisonKastler.randomWalkSplit_law line 59
  6. theorem OAI.KadisonKastler.randomWalkAdvance_law line 77
  7. theorem OAI.KadisonKastler.randomWalkAdvance_quasi line 90