OAI/Analysis/KadisonKastler/ShiftBoundarySpace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The boundary as the invariant measurable space

Only its measurable structure enters the application. Keeping the original points and restricting their sigma algebra gives the probability boundary directly, with a nonsingular action induced by the rooted path action.

  1. def OAI.KadisonKastler.ShiftBoundarySpace line 21
  2. instance OAI.KadisonKastler.(instance at line 23) line 23
  3. def OAI.KadisonKastler.shiftBoundaryMeasure line 26
  4. instance OAI.KadisonKastler.(instance at line 28) line 28
  5. def OAI.KadisonKastler.shiftBoundaryMap line 31
  6. theorem OAI.KadisonKastler.shiftBoundaryMap_measurePreserving line 33
  7. def OAI.KadisonKastler.shiftBoundaryAction line 40
  8. theorem OAI.KadisonKastler.shiftBoundaryAction_apply line 47
  9. abbrev OAI.KadisonKastler.RandomWalkBoundary line 54
  10. def OAI.KadisonKastler.randomWalkBoundaryMeasure line 57
  11. instance OAI.KadisonKastler.(instance at line 60) line 60
  12. def OAI.KadisonKastler.randomWalkBoundaryAction line 64