OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanContinuousRayLimits.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.continuous_bounded_ray_quotient_limits line 37

   Source documentation

   Uniform sublinear height control and bounded initial points give a continuous compact limit for a family of actual projected Cartan rays.

   theorem continuous_bounded_ray_quotient_limits
       [TopologicalSpace P]
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (γ₀ : M.Bases)
       (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
         (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
         (cartanLog H F.D.equiv F.ExpD
           (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) d))
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
       {Kheight : ℝ} (hKheight : 0 ≤ Kheight)
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog