MetricFactorBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic factor bounds for short ambient bridges

Unit words and the actual Cartan factorization give logarithmic bounds for every ambient element and its fixed compact right thickening. The nilpotent factor grows exponentially in ambient distance; the Cartan logarithm grows only polynomially.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_metric_factor_thickening_bound line 42

Source documentation

One factor lift controls the entire right cell. The bounds use the actual ambient metric and preserve the endpoint's canonical height.

theorem exists_metric_factor_thickening_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ₀ : M.Bases) {J : Type*} [Fintype J]
    (b : Basis J ℝ (cartanRootIdeal H)) {U : Set (F.N.carrier × F.D.carrier)} (hU : IsCompact U)
    (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