OAI/GroupTheory/PolycyclicRecognition/Analysis/NilpotentConjugationMetric.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_nilpotent_right_translate_coarse_metric line 21

   Source documentation

   In any continuously embedded nilpotent factor, right translation by a ray has polynomial coarse speed on each fixed exponential line.

   theorem exists_nilpotent_right_translate_coarse_metric
       (κ : D →* G) (hκ : Continuous κ)
       (dynkin : NilpotentDynkinExpansionInput E D)
       (Exp : GroupLieAlgebra (𝓘(ℝ, E)) D → D) (hExp : IsGroupExponential Exp)
       (chart : GroupLieAlgebra (𝓘(ℝ, E)) D ≃ₜ D) (hchart : ∀ x, chart x = Exp x)
       {c : ℕ} (hc : lowerCentralSeries ℝ (GroupLieAlgebra (𝓘(ℝ, E)) D)
         (GroupLieAlgebra (𝓘(ℝ, E)) D) c = ⊥)
       {m : ℕ} (b : Basis (Fin m) ℝ (GroupLieAlgebra (𝓘(ℝ, E)) D))
       (u v : GroupLieAlgebra (𝓘(ℝ, E)) D) :
       ∃ C : ℝ, 0 ≤ C ∧ ∀ (n : ℕ) (s t : ℝ), |t - s| ≤ 1 →
         dist (κ (Exp (s • u) * Exp ((n : ℝ) • v)))
           (κ (Exp (t • u) * Exp ((n : ℝ) • v))) ≤
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput