OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseRayFactorBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.centered_coarse_ray_factor_bounds line 13

   Source documentation

   A common sublinear height estimate makes every centered coarse ray uniformly negative after one shift. Actual metric factorization then gives uniform polynomial Cartan coordinates and bounded relative increments.

   theorem centered_coarse_ray_factor_bounds
       {P S N D G : Type*} [MetricSpace S] [One S]
       [Group N] [Group D] [Group G] [MetricSpace G] [IsIsometricSMul G G]
       (ι : N →* G) (κ : D →* G) (size height : D → ℝ)
       (sourceHeight : S → ℝ) (targetHeight : G → ℝ)
       (f : P → S → G) (hcenter : ∀ p, f p 1 = 1)
       {L error R gap step B : ℝ} (hL : 0 ≤ L) (hR : 0 ≤ R) (hgap : 0 < gap) (hB : 0 ≤ B)
       (hf : ∀ p x y, dist (f p x) (f p y) ≤ L * dist x y + error)
       (hsub : ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 ≤ C ∧ ∀ p x,
         |targetHeight (f p x) - sourceHeight x| ≤ ε * dist 1 x + C)
       (ray : ℕ → S) (hray : ∀ n, dist 1 (ray n) ≤ R * n)
       (hnegative : ∀ n, sourceHeight (ray n) ≤ -gap * n)
   …