OAI/Analysis/KadisonKastler/ShiftInvariantSigma.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The invariant sigma algebra of the nonsingular boundary shift

Using this measurable space directly avoids a redundant point-set coding of the boundary. Its measurable sets are exactly the ambient measurable sets fixed by the shift modulo null sets.

  1. def OAI.KadisonKastler.shiftInvariantSigma line 23
  2. theorem OAI.KadisonKastler.shiftInvariantSigma_le line 32
  3. def OAI.KadisonKastler.shiftInvariantMeasure line 35
  4. instance OAI.KadisonKastler.shiftInvariantMeasure_probability line 38
  5. theorem OAI.KadisonKastler.shiftInvariantSigma_of_null line 44
  6. theorem OAI.KadisonKastler.measurable_shiftInvariantSigma_of_fixed line 55
  7. theorem OAI.KadisonKastler.measurable_shiftInvariantSigma_of_commuting line 65
  8. theorem OAI.KadisonKastler.quasi_shiftInvariantSigma_of_commuting line 76