CoarsePathWords.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Subdividing coarse paths into bounded-increment words

A path with speed L and additive error κ admits a unit-step word of length at most (L + 1) * (κ + 2). Its prefixes remain within κ + 2 of points on the path. In the application L = O(r) and κ = O(log r), so this loss is polynomial and its extra height error is sublinear.

def OAI.PolycyclicRecognition.subdivisionPoint line 21
Source documentation
The uniform subdivision of the unit interval, constant after its endpoint.
```
def subdivisionPoint (n : ℕ) (hn : 0 < n) (i : ℕ) : unitInterval :=
…
```
theorem OAI.PolycyclicRecognition.subdivisionPoint_coe line 28
theorem OAI.PolycyclicRecognition.subdivisionPoint_zero line 32
theorem OAI.PolycyclicRecognition.subdivisionPoint_self line 37

theorem OAI.PolycyclicRecognition.exists_word_near_coarse_path line 46

Source documentation

A coarse path has a polynomially controlled unit-step word, with every prefix close to an actual point on that same path.

theorem exists_word_near_coarse_path
    (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
      ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
        dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
    {g : G} (γ : Path (1 : G) g) {L κ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
    (hγ : PathMetricBound γ L κ) :
    ∃ w : List G, (∀ x ∈ w, x ∈ closedBall (1 : G) 1) ∧ w.prod = g ∧
      (w.length : ℝ) ≤ (L + 1) * (κ + 2) ∧
      ∀ j : ℕ, ∃ t : unitInterval, dist (w.take j).prod (γ t) ≤ κ + 2 := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound