OAI/GroupTheory/PolycyclicRecognition/Analysis/QuotientSectionRightHaar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Right Haar measure in quotient-section coordinates

Right translations translate each kernel fiber on the right. Consequently the product of right Haar measures gives a right-invariant measure without assuming that conjugation preserves the kernel measure. In a unimodular ambient group, Haar uniqueness then gives left invariance as well.

  1. def OAI.PolycyclicRecognition.quotientSectionRightCocycle line 24
  2. theorem OAI.PolycyclicRecognition.continuous_quotientSectionRightCocycle line 27
  3. theorem OAI.PolycyclicRecognition.quotientSection_right_translation line 33
  4. theorem OAI.PolycyclicRecognition.quotientSection_right_skew_measurePreserving line 52
  5. theorem OAI.PolycyclicRecognition.quotientSection_product_right_invariant line 62
  6. theorem OAI.PolycyclicRecognition.quotientSection_product_isMulRightInvariant line 78
  7. theorem OAI.PolycyclicRecognition.quotientSection_product_leftInvariant_of_unimodular line 87
  8. theorem OAI.PolycyclicRecognition.quotientKernelConjugate_preserves_of_unimodular line 107

    Source documentation

    Unimodularity of the ambient group and of the quotient forces conjugation to preserve the kernel's right Haar measure.

    theorem quotientKernelConjugate_preserves_of_unimodular
    [T2Space Q] [LocallyCompactSpace Q]
    [μQ.IsMulLeftInvariant] [μQ.IsOpenPosMeasure]
    (μ : Measure N) [μ.IsHaarMeasure] [μ.IsMulRightInvariant] (n : N) :
    MeasurePreserving (quotientKernelConjugate π n) μI μI := by
…

    Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate