OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSmallMetricFactors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_metric_cartan_factor_bound line 38

   Source documentation

   The nilpotent factor has the usual exponential distance bound, while the Cartan factor is small in the word chart whenever distance divided by chart scale is small. Both bounds hold for the same factor lift.

   theorem exists_small_metric_cartan_factor_bound
       (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
       (γ₀ : M.Bases) {J : Type*} [Fintype J]
       (b : Basis J ℝ (cartanRootIdeal H))
       (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|)
       {K : ℝ} (hK : 0 ≤ K)
   …

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