ModelCubeHaar.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Haar normalization in a Lie-algebra model basis

theorem OAI.PolycyclicRecognition.exists_model_haar_cube_volume line 16

Source documentation

Normalize the published nilpotent exponential Haar measure in a basis of an isomorphic Lie algebra, as used for the actual Cartan factor.

theorem exists_model_haar_cube_volume
    {L : Type*} [LieRing L] [LieAlgebra ℝ L]
    {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace G] [ChartedSpace E G] [Group G]
    [LieGroup (𝓘(ℝ, E)) ⊤ G] [T2Space G] [SimplyConnectedSpace G]
    [MeasurableSpace G] [BorelSpace G]
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (hnil : LieRing.IsNilpotent L) {n : ℕ} (b : Basis (Fin n) ℝ L) :
    ∃ μ : Measure G, μ.IsHaarMeasure ∧ ∀ R : ℝ, 0 ≤ R →
      μ (exponentialCoordinateBox (Exp ∘ e) b R) = ENNReal.ofReal (2 * R) ^ n := by
…

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