NilpotentHaarInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exponential-coordinate Haar measure

E. Le Donne, Metric Lie Groups, Graduate Texts in Mathematics 306, Springer (2025), Theorem 9.4.7 (exponential coordinates) and Corollary 9.4.21. https://doi.org/10.1007/978-3-031-98832-5_9

A global exponential chart identifies Haar measure on a simply connected nilpotent Lie group with Lebesgue measure. The Euclidean determinant formula then gives the volume of weighted boxes, including their scale factors.

def OAI.PolycyclicRecognition.NilpotentExponentialHaarInput line 31
Source documentation
The part of the nilpotent exponential-coordinate theorem needed for Haar volume. The hypotheses concern the actual tangent Lie algebra of the group.
```
def NilpotentExponentialHaarInput [T2Space G] [SimplyConnectedSpace G]
    [MeasurableSpace G] [BorelSpace G] : Prop :=
…
```

theorem OAI.PolycyclicRecognition.exists_haar_exponential_cube_volume line 44

Source documentation

Normalize Haar measure using one exponential coordinate basis.

theorem exists_haar_exponential_cube_volume
    (haarInput : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {n : ℕ} (b : Basis (Fin n) ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) :
    ∃ (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (μ : Measure G),
      (∀ x, chart x = Exp x) ∧ μ.IsHaarMeasure ∧
      ∀ R : ℝ, 0 ≤ R → μ (exponentialCoordinateBox Exp b R) = ENNReal.ofReal (2 * R) ^ n := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.exists_haar_measure_model_weighted_boxes line 69

Source documentation

An actual Haar measure with the exact exponential weighted-box formula. All template dependence is in the already proved finite determinant sum.

theorem exists_haar_measure_model_weighted_boxes
    (haarInput : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    {L : Type*} [LieRing L] [LieAlgebra ℝ L]
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hnil : LieRing.IsNilpotent L)
    {I : Type*} (X : I → L) (S : Finset (FreeMagma I))
    (b₀ : Basis (Fin (finrank ℝ L)) ℝ L) :
    ∃ μ : Measure G, μ.IsHaarMeasure ∧
      ∀ (cost : S → ℝ) (β : WordBasisSelections X S) (r R : ℝ), 0 ≤ R →
        μ (exponentialCoordinateBox (Exp ∘ e)
          (exponentialRescaleBasis (WordBasisSelections.basis X S β)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis