OAI/GroupTheory/PolycyclicRecognition/Analysis/HaarMeasureTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transfer of an invariant automorphism to the section-coordinate Haar measure

  1. theorem OAI.PolycyclicRecognition.measurePreserving_of_haarMeasure line 16

    Source documentation

    A map preserving one Haar measure preserves every Haar normalization. This permits use of the Haar measure constructed from ideal-section coordinates.

    theorem measurePreserving_of_haarMeasure (μ ν : Measure G)
    [μ.IsHaarMeasure] [ν.IsHaarMeasure] (f : G → G)
    (hf : MeasurePreserving f μ μ) : MeasurePreserving f ν ν := by
…