OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialHaarMultiplier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact Haar multiplier of an exponential-coordinate automorphism

  1. theorem OAI.PolycyclicRecognition.exponentialConjugate_map_measure line 25

    Source documentation

    The pushforward multiplier is the reciprocal absolute determinant. Consequently the multiplier of image volumes is the absolute determinant.

    theorem exponentialConjugate_map_measure (F : L ≃ₗ⁅ℝ⁆ L) :
    Measure.map (exponentialConjugate e Exp hbij F)
      (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume) =
    ENNReal.ofReal |(LinearMap.det F.toLinearEquiv.toLinearMap)⁻¹| •
      Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume := by
…

    Mentions: OAI.PolycyclicRecognition.exponentialConjugate