ModelBoxTranslation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Small translations for an identified nilpotent Lie algebra

The Cartan root algebra is identified with the tangent Lie algebra of its integrating group. Transporting the basis preserves the normalized bracket, so the actual Haar-cell estimate applies before or after that identification.

theorem OAI.PolycyclicRecognition.model_rescaled_cell_translation_tendsto_zero line 21

Source documentation

The finite-cell translation estimate in the original model coordinates.

theorem model_rescaled_cell_translation_tendsto_zero
    {E G L ι : 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] [LieRing L] [LieAlgebra ℝ L]
    (haar : NilpotentExponentialHaarInput E G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) G))
    {n c : ℕ} (b : ι → Basis (Fin n) ℝ L)
    (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial