OAI/GroupTheory/PolycyclicRecognition/Analysis/JacobianMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measure transport from a unit Jacobian

This is the change-of-variables step used by the nilpotent BCH chart.

  1. theorem OAI.PolycyclicRecognition.map_eq_self_of_unit_jacobian line 20
  2. theorem OAI.PolycyclicRecognition.homeomorph_map_isHaar_of_translations line 39

    Source documentation

    A homeomorphism transports additive Haar measure to Haar measure when the conjugates of left translations preserve it.

    theorem homeomorph_map_isHaar_of_translations
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [MeasurableSpace G] [BorelSpace G]
    (c : E ≃ₜ G) (μ : Measure E) [μ.IsAddHaarMeasure]
    (htranslations : ∀ g : G,
      Measure.map (fun x => c.symm (g * c x)) μ = μ) :
    (Measure.map c μ).IsHaarMeasure := by
…