OAI/Analysis/KadisonKastler/BilateralBoundaryPair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The two boundary endpoints of a bilateral random walk

The forward and reflected backward halves have the exact boundary product law. Every integer shift preserves the bilateral path probability.

  1. def OAI.KadisonKastler.bilateralPositiveBoundary line 19
  2. def OAI.KadisonKastler.bilateralNegativeBoundary line 22
  3. theorem OAI.KadisonKastler.bilateralPositiveBoundary_measurePreserving line 25
  4. theorem OAI.KadisonKastler.bilateralNegativeBoundary_measurePreserving line 30
  5. theorem OAI.KadisonKastler.bilateralBoundary_independent line 35
  6. def OAI.KadisonKastler.bilateralBoundaryPair line 41
  7. theorem OAI.KadisonKastler.bilateralBoundaryPair_measurePreserving line 44
  8. def OAI.KadisonKastler.bilateralTranslate line 53
  9. theorem OAI.KadisonKastler.bilateralTranslate_measurePreserving line 55