NilpotentHaarAutomorphisms.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Haar preservation for the integrated automorphisms

A determinant-one Lie automorphism preserves Lebesgue measure in exponential coordinates. The global chart transfers this identity to actual group Haar measure; no invariant-measure premise for the automorphism is assumed.

theorem OAI.PolycyclicRecognition.exponentialConjugate_measurePreserving line 34
Source documentation
In exponential coordinates, the integrated automorphism preserves the same measure exactly when its linear determinant has absolute value one. Here the positive determinant-one case suffices for Cartan conjugation.
```
theorem exponentialConjugate_measurePreserving
    (F : L ≃ₗ⁅ℝ⁆ L) (hdet : LinearMap.det F.toLinearEquiv.toLinearMap = 1) :
    MeasurePreserving (exponentialConjugate e Exp hbij F)
      (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume)
      (Measure.map ((Exp ∘ e) ∘ b.equivFun.symm) volume) := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialConjugate

theorem OAI.PolycyclicRecognition.exponentialCoordinate_weighted_box_measure line 79

Source documentation

The same explicit coordinate measure has the exact weighted-box volume. Thus its automorphism invariance and its box normalization are compatible.

theorem exponentialCoordinate_weighted_box_measure
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L)
    {I : Type*} (X : I → L) (S : Finset (FreeMagma I))
    (cost : S → ℝ) (β : WordBasisSelections X S) (r R : ℝ) (hR : 0 ≤ R) :
    (Measure.map ((Exp ∘ e) ∘ b₀.equivFun.symm) volume)
      (exponentialCoordinateBox (Exp ∘ e)
        (exponentialRescaleBasis (WordBasisSelections.basis X S β)
          (fun i => cost (β.val i)) r) R) =
      ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates X S b₀) β.val).det| *
        ENNReal.ofReal (Real.exp (r * columnBasisWeight cost β.val)) *
          ENNReal.ofReal (2 * R) ^ finrank ℝ L := by
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.columnBasisWeight

theorem OAI.PolycyclicRecognition.exists_haar_preserved_by_exponentialConjugate line 108

Source documentation

The published exponential Haar theorem supplies one Haar measure preserved by every determinant-one integrated automorphism.

theorem exists_haar_preserved_by_exponentialConjugate
    (haar : NilpotentExponentialHaarInput E G)
    (hExp : IsGroupExponential Exp) (hnil : LieRing.IsNilpotent L) :
    ∃ μ : Measure G, μ.IsHaarMeasure ∧
      ∀ F : L ≃ₗ⁅ℝ⁆ L, LinearMap.det F.toLinearEquiv.toLinearMap = 1 →
        MeasurePreserving (exponentialConjugate e Exp hbij F) μ μ := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.exponentialConjugate