GeodesicWords.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Word decompositions by sampling minimizing paths

This supplies the bounded-step word decomposition used in the stationary estimate from actual metric paths. The number of steps is at most distance plus one.

theorem OAI.PolycyclicRecognition.wordFactorization_of_minimizing_paths line 21

Source documentation

Subdivision of a minimizing path gives a word in the unit ball, with length at most distance plus one.

theorem wordFactorization_of_minimizing_paths
    {G : Type*} [Group G] [MetricSpace G] [IsIsometricSMul G G]
    (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) :
    ∃ w : List G, (∀ q ∈ w, q ∈ closedBall 1 1) ∧ w.prod = g ∧
      (w.length : ℝ) ≤ dist 1 g + 1 := by
…