OAI/NumberTheory/DukePrimeDegree/Dynamics/TranslationInvariantSlices.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Haar slices of a measure invariant in its second coordinate

Only relatively compact transverse sets are needed for local product charts. The transverse measure itself is allowed to be singular.

  1. def OAI.DukePrimeDegree.secondCoordinateSlice line 18
  2. lemma OAI.DukePrimeDegree.secondCoordinateSlice_apply line 21
  3. theorem OAI.DukePrimeDegree.secondCoordinateSlice_invariant line 31
  4. theorem OAI.DukePrimeDegree.secondCoordinateSlice_finiteOnCompacts line 51
  5. theorem OAI.DukePrimeDegree.secondCoordinateSlice_eq_haar line 61
  6. theorem OAI.DukePrimeDegree.translationInvariant_rectangle line 73