OAI/Analysis/KadisonKastler/BilateralCoordinateSigma.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Coordinate measurability and independence for the bilateral product law.

  1. theorem OAI.KadisonKastler.bilateralCoordinateSigma_independent line 16
  2. theorem OAI.KadisonKastler.bilateralCoordinate_indepFun line 29
  3. theorem OAI.KadisonKastler.bilateralTranslate_coordinate_measurable line 43
  4. theorem OAI.KadisonKastler.bilateralIncrementProduct_coordinate_measurable line 52
  5. theorem OAI.KadisonKastler.bilateralTranslate_coordinate_aestronglyMeasurable line 64