OAI/GroupTheory/PolycyclicRecognition/Analysis/QuotientSectionHaar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Haar measure in quotient-section coordinates

  1. theorem OAI.PolycyclicRecognition.quotientSection_product_isHaarMeasure line 23

    Source documentation

    The coordinate product is itself Haar: left invariance follows from the explicit skew action, and the homeomorphism preserves finiteness on compact sets and positivity on open sets.

    theorem quotientSection_product_isHaarMeasure
    (hconj : ∀ n : N, MeasurePreserving (quotientKernelConjugate π n) μI μI) :
    (Measure.map (quotientSectionHomeomorph π hπ s hs).symm (μQ.prod μI)).IsHaarMeasure := by
…

    Mentions: OAI.PolycyclicRecognition.quotientKernelConjugate, OAI.PolycyclicRecognition.quotientSectionHomeomorph