OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanRayFactorPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanFactorModel.exists_negative_height_cartan_fiber_chains line 25

   Source documentation

   Every fixed Cartan-factor displacement admits actual unit-step chains along the chosen negative ray, with polynomial length and linear radius.

   theorem exists_negative_height_cartan_fiber_chains
       (eW : HeightSpace T.character ≃ₗ[ℝ] W)
       (height : G →* Multiplicative W)
       (hheight : ∀ x, (height (ExpG x)).toAdd = eW (heightProjection T.character x))
       (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
       (hchartD : ∀ x, chartD x = F.ExpD x)
       (dynkinD : NilpotentDynkinExpansionInput F.D.modelSpace F.D.carrier)
       {Kheight : ℝ} (hKheight : 0 ≤ Kheight)
       (hLip : ∀ x y, ‖(height x).toAdd - (height y).toAdd‖ ≤ Kheight * dist x y)
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
   …

   Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput