CartanWeightHaar.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PolycyclicRecognition.CartanWordModel.weightDilation_preserves_haar line 33
Source documentation
The actual scalar dilation preserves any chosen Haar normalization. Thus moving the contact pivot costs no probe volume.
```
theorem weightDilation_preserves_haar (μ : Measure N) [μ.IsHaarMeasure] (h : H) :
    MeasurePreserving
      (integrateNilpotentLieEquiv e Exp hbij dynkin hExp M.bound_zero
        (cartanIdealWeightDilation T H h)) μ μ := by
…
```
Mentions: OAI.PolycyclicRecognition.integrateNilpotentLieEquiv, OAI.PolycyclicRecognition.cartanIdealWeightDilation
theorem OAI.PolycyclicRecognition.CartanWordModel.weightDilation_preserves_haar_of_exp_action line 53
Source documentation
Source dilations with the same exponential formula preserve the same Haar volume.
```
theorem weightDilation_preserves_haar_of_exp_action
    (μ : Measure N) [μ.IsHaarMeasure] (h : H) (S : N → N)
    (hS : ∀ v, S (Exp (e v)) = Exp (e (cartanIdealWeightDilation T H h v))) :
    MeasurePreserving S μ μ := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation