OAI/Analysis/KadisonKastler/ProductInvariantIntegrals.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Invariant sections and rectangle tests

For a function invariant under a shift in its first coordinate, integrating over a set in the second coordinate gives a function on the invariant sigma algebra. Consequently invariant rectangles already determine such a function.

  1. theorem OAI.KadisonKastler.integrable_section_setIntegral line 25
  2. theorem OAI.KadisonKastler.invariant_section_setIntegral line 32
  3. theorem OAI.KadisonKastler.invariant_section_measurable line 39
  4. theorem OAI.KadisonKastler.invariant_integrable_zero_of_rectangle_tests line 46