OAI/GroupTheory/PolycyclicRecognition/Analysis/HaarInvariantRepresentative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exactly invariant representatives for locally compact groups

The probability equivalent to Haar measure supplies the group averaging measure. This removes countability of the acting group from the invariant representative construction.

  1. theorem OAI.PolycyclicRecognition.measurable_haarInvariantRepresentative line 26
  2. theorem OAI.PolycyclicRecognition.aemeasurable_haarInvariantRepresentative line 36