OAI/GroupTheory/PolycyclicRecognition/Analysis/HaarOrbitAverages.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Convex orbit averages for locally compact group actions

  1. theorem OAI.PolycyclicRecognition.fixedL2_haarInvariantRepresentative line 21
  2. theorem OAI.PolycyclicRecognition.exists_L2_haarOrbitAverage line 35
  3. theorem OAI.PolycyclicRecognition.exists_pointwise_haarOrbitAverages line 43