ExponentialRightHaar.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Right invariance of exponential-coordinate Haar measure

Negation preserves coordinate Lebesgue measure and corresponds to group inversion. Thus the exponential-coordinate left Haar measure is also right invariant, without a separate group nilpotence assertion.

theorem OAI.PolycyclicRecognition.isInvInvariant_map_of_neg line 21

Source documentation

Oddness of an exponential chart makes its coordinate measure invariant under group inversion.

theorem isInvInvariant_map_of_neg
    {V G : Type*} [AddCommGroup V] [MeasurableSpace V] [MeasurableNeg V]
    [Group G] [MeasurableSpace G] [MeasurableInv G]
    (ν : Measure V) [ν.IsNegInvariant]
    (f : V → G) (hf : Measurable f) (hneg : ∀ x, f (-x) = (f x)⁻¹) :
    (Measure.map f ν).IsInvInvariant := by
…

theorem OAI.PolycyclicRecognition.isMulRightInvariant_map_of_neg line 36

Source documentation

The same coordinate measure is right Haar as soon as it is left invariant.

theorem isMulRightInvariant_map_of_neg
    {V G : Type*} [AddCommGroup V] [MeasurableSpace V] [MeasurableNeg V]
    [Group G] [MeasurableSpace G] [MeasurableMul G] [MeasurableInv G]
    (ν : Measure V) [ν.IsNegInvariant]
    (f : V → G) (hf : Measurable f) (hneg : ∀ x, f (-x) = (f x)⁻¹)
    [(Measure.map f ν).IsMulLeftInvariant] :
    (Measure.map f ν).IsMulRightInvariant := by
…

theorem OAI.PolycyclicRecognition.coordinate_right_translation_preserving line 51

Source documentation

Pull right translation back through the actual coordinate equivalence.

theorem coordinate_right_translation_preserving
    {V G : Type*} [MeasurableSpace V] [Group G] [MeasurableSpace G]
    [MeasurableMul G] (ν : Measure V) (μ : Measure G) [μ.IsMulRightInvariant]
    (e : V ≃ᵐ G) (he : Measure.map e ν = μ)
    (m : V → V → V) (hm : ∀ x y, e (m x y) = e x * e y) (q : V) :
    MeasurePreserving (fun x => m x q) ν ν := by
…