ControlledChainWords.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded-step words near a coarse chain

Sampling a coarse path gives finitely many jumps. Replacing each jump by a short word in the unit ball gives a controlled word whose every prefix stays near a sampled vertex. The minimizing-path hypothesis is the same concrete metric hypothesis used by GeodesicWords and the stationary sublinearity bridge.

theorem OAI.PolycyclicRecognition.dist_one_list_prod_le_length line 21
Source documentation
A unit-step word has distance at most its length from the identity.
```
theorem dist_one_list_prod_le_length (w : List G)
    (hw : ∀ g ∈ w, g ∈ closedBall (1 : G) 1) :
    dist (1 : G) w.prod ≤ w.length := by
…
```
theorem OAI.PolycyclicRecognition.wordPrefix_getD line 41
Source documentation
Padding a finite word by identity letters preserves all its prefixes.
```
theorem wordPrefix_getD (w : List G) (j : ℕ) :
    wordPrefix (fun i => w.getD i 1) j = (w.take j).prod := by
…
```
Mentions: OAI.PolycyclicRecognition.wordPrefix

theorem OAI.PolycyclicRecognition.getD_mem_closedBall_one line 57

Source documentation

Identity padding keeps every increment inside the closed unit ball.

theorem getD_mem_closedBall_one (w : List G)
    (hw : ∀ g ∈ w, g ∈ closedBall (1 : G) 1) (i : ℕ) :
    w.getD i 1 ∈ closedBall (1 : G) 1 := by
…

theorem OAI.PolycyclicRecognition.exists_word_near_chain line 67

Source documentation

Replacing the jumps of a finite chain by unit-step words preserves the endpoint, has controlled total length, and stays within one jump bound of the sampled chain at every prefix.

theorem exists_word_near_chain
    (hpath : ∀ g : G, ∃ γ : ℝ → G, γ 0 = 1 ∧ γ 1 = g ∧
      ∀ t ∈ Icc (0 : ℝ) 1, ∀ u ∈ Icc (0 : ℝ) 1,
        dist (γ t) (γ u) ≤ dist 1 g * |t - u|)
    (v : ℕ → G) (hv0 : v 0 = 1) {D : ℝ} (hD : 0 ≤ D) (n : ℕ)
    (hstep : ∀ i < n, dist (v i) (v (i + 1)) ≤ D) :
    ∃ w : List G, (∀ g ∈ w, g ∈ closedBall (1 : G) 1) ∧ w.prod = v n ∧
      (w.length : ℝ) ≤ (n : ℝ) * (D + 1) ∧
      ∀ j : ℕ, ∃ i ≤ n, dist (w.take j).prod (v i) ≤ D + 1 := by
…