SmallDistanceRatio.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform small-distance threshold for Cartan word coordinates

theorem OAI.PolycyclicRecognition.exists_small_distance_ratio line 11

Source documentation

The polynomial coordinate bound becomes uniformly small when the distance is a sufficiently small fraction of a sufficiently large scale.

theorem exists_small_distance_ratio (B R : ℝ) (d : ℕ) {ε : ℝ} (hε : 0 < ε) :
    ∃ η S : ℝ, 0 < η ∧ 1 ≤ S ∧ ∀ s : ℝ, S ≤ s → ∀ a : ℝ, 0 ≤ a → a ≤ η * s →
      B * ((a + 1) * R / s) * (1 + (a + 1) * R / s) ^ d ≤ ε := by
…