OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialHaarImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exponentialConjugate_image_measure line 25

   Source documentation

   A positive exponential determinant is the image-volume multiplier. This identity holds for arbitrary sets, using the measurable embedding.

   theorem exponentialConjugate_image_measure
       (F : L ≃ₗ⁅ℝ⁆ L) (d : ℝ)
       (hd : LinearMap.det F.toLinearEquiv.toLinearMap = Real.exp d) (S : Set G) :
       (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume)
         (exponentialConjugate e Exp hbij F '' S) =
       ENNReal.ofReal (Real.exp d) *
         (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume) S := by
   …

   Mentions: OAI.PolycyclicRecognition.exponentialConjugate