BoundedCoarseRayFactorBounds.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform factor bounds for coarse families with bounded initial points

theorem OAI.PolycyclicRecognition.bounded_coarse_ray_factor_bounds line 13

Source documentation

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

theorem bounded_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) {start : ℝ} (hstart : ∀ p, dist 1 (f p 1) ≤ start)
    {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)
…