OAI/GroupTheory/PolycyclicRecognition/Analysis/SubexponentialQuotientVolume.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_haar_subexponential_quotient_boxes line 16

   Source documentation

   The actual nilpotent exponential chart gives finite quotient log boxes with subexponential volume whenever their radii are subexponential.

   theorem exists_haar_subexponential_quotient_boxes
       {E Q : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       [FiniteDimensional ℝ E] [TopologicalSpace Q] [ChartedSpace E Q] [Group Q]
       [LieGroup (𝓘(ℝ, E)) ⊤ Q] [T2Space Q] [SimplyConnectedSpace Q]
       [MeasurableSpace Q] [BorelSpace Q]
       (haar : NilpotentExponentialHaarInput E Q)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) Q → Q) (hExp : IsGroupExponential Exp)
       (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) Q))
       {n : ℕ} (b : Basis (Fin n) ℝ (GroupLieAlgebra (𝓘(ℝ, E)) Q)) :
       ∃ μ : Measure Q, μ.IsHaarMeasure ∧ ∀ R : ℝ → ℝ,
         (∀ r, 0 ≤ R r) → HasSubexponentialUpperBound R →
         (∀ r, μ (exponentialCoordinateBox Exp b (R r)) ≠ ⊤) ∧
   …

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