OAI/GroupTheory/PolycyclicRecognition/Analysis/PolynomialNegativePaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.polynomial_negative_path_chains line 18

   Source documentation

   A polynomial coarse speed with a constant mesh error suffices for polynomially many unit steps. Negative linear height survives subdivision.

   theorem polynomial_negative_path_chains
       (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
         ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
           dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
       (height : G → ℝ) {K C R a : ℝ} {q : ℕ}
       (hK : 0 ≤ K) (hC : 0 ≤ C) (hR : 0 ≤ R) (ha : 0 < a)
       (hheight : ∀ x y, |height x - height y| ≤ K * dist x y)
       (source target : ℕ → G)
       (hsource : ∀ n, dist 1 (source n) ≤ R * n)
       (hγ : ∀ᶠ n : ℕ in atTop, ∃ γ : Path (source n) (target n),
         PathMetricBound γ (C * (1 + n) ^ q) C ∧
         (∀ t, height (γ t) ≤ -a * n) ∧ (∀ t, dist 1 (γ t) ≤ R * n)) :
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound