OAI/GroupTheory/PolycyclicRecognition/Geometry/SemidirectProductHaar.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Haar measure in genuine semidirect product coordinates

  1. def OAI.PolycyclicRecognition.semidirectProductMeasurableSpace line 23
  2. theorem OAI.PolycyclicRecognition.semidirectProduct_borelSpace line 29
  3. def OAI.PolycyclicRecognition.semidirectProductMeasure line 38
  4. def OAI.PolycyclicRecognition.semidirectProductRectangle line 41
  5. theorem OAI.PolycyclicRecognition.semidirectProductRectangle_compact line 48
  6. theorem OAI.PolycyclicRecognition.semidirectProductRectangle_nonempty line 57
  7. theorem OAI.PolycyclicRecognition.semidirectProductMeasure_rectangle line 67
  8. theorem OAI.PolycyclicRecognition.semidirectProductMeasure_left_invariant line 82
  9. theorem OAI.PolycyclicRecognition.semidirectProductMeasure_isHaarMeasure line 99
  10. theorem OAI.PolycyclicRecognition.semidirectProductMeasure_isInvInvariant line 114

    Source documentation

    Inversion in the cover is the factorwise inversion followed by the measure-preserving Cartan action on the nilpotent coordinate.

    theorem semidirectProductMeasure_isInvInvariant
    [μN.IsInvInvariant] [μD.IsInvInvariant]
    (hφ : Continuous (fun p : D × N => φ p.1 p.2))
    (hpres : ∀ d, MeasurePreserving (φ d) μN μN) :
    (semidirectProductMeasure φ μN μD).IsInvInvariant := by
…

    Mentions: OAI.PolycyclicRecognition.semidirectProductMeasure