BasisDynkinHaar.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Lebesgue invariance of actual rescaled Dynkin translations

Every coordinate basis is allowed. Hence the lemma applies directly to the scale-dependent maximizing bases used by the occupation measures.

theorem OAI.PolycyclicRecognition.measurePreserving_basis_dynkin_right line 22

Source documentation

The actual exponential-coordinate multiplication preserves coordinate Lebesgue measure under right translations, in every basis.

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

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