OAI/GroupTheory/PolycyclicRecognition/Analysis/GradedHaar.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.measurePreserving_graded_dynkin_right_of_rescaled line 20
2. theorem OAI.PolycyclicRecognition.measurePreserving_model_graded_dynkin_right line 52

   Source documentation

   The published exponential-Haar input gives the finite-scale invariance; the limiting invariance follows from the actual rescaled brackets.

   theorem measurePreserving_model_graded_dynkin_right
       {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 c : ℕ} (b : Basis (Fin n) ℝ L)
       (cost : Fin n → ℝ)
       (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

3. theorem OAI.PolycyclicRecognition.polynomialCoordinate_haar_of_right_translations line 87

   Source documentation

   Lebesgue measure in polynomial exponential coordinates is Haar once right translations preserve it. Inversion is coordinate negation.

   theorem polynomialCoordinate_haar_of_right_translations
       {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V]
       [MeasureSpace V] [BorelSpace V]
       [(volume : Measure V).IsAddHaarMeasure]
       (m : V → V → V) (h : PolynomialGroupLaws m)
       (hc : Continuous (fun p : V × V => m p.1 p.2))
       (hm : ∀ q, MeasurePreserving (fun x => m x q) volume volume) :
       let e := PolynomialCoordinateGroup.expHomeomorph m h
   …

   Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.expHomeomorph