OAI/GroupTheory/PolycyclicRecognition/Geometry/CoarsePathHeightWords.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_height_controlled_word_of_coarse_path line 20

   Source documentation

   Every prefix of the short word remains close in height to the original coarse path, with exactly the metric subdivision error.

   theorem exists_height_controlled_word_of_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 →* Multiplicative W) {K : ℝ} (hK : 0 ≤ K)
       (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y)
       {g : G} (γ : Path (1 : G) g) {L κ : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ)
       (hγ : PathMetricBound γ L κ) (E : Set W) (r B : ℝ)
       (hheight : ∀ t, ∃ z ∈ E, ‖(π (γ t)).toAdd - r • z‖ ≤ B) :
       ∃ w : List G, (∀ x ∈ w, x ∈ closedBall (1 : G) 1) ∧ w.prod = g ∧
         (w.length : ℝ) ≤ (L + 1) * (κ + 2) ∧
         ∀ j : ℕ, ∃ z ∈ E,
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound

2. theorem OAI.PolycyclicRecognition.exists_scaled_thickening_of_norm_sub_smul_le line 50

   Source documentation

   An error at scale r is absorbed into a fixed compact thickening of the height template.

   theorem exists_scaled_thickening_of_norm_sub_smul_le
       {E : Set W} {z y : W} (hz : z ∈ E) {r ε : ℝ} (hr : 0 < r)
       (h : ‖y - r • z‖ ≤ r * ε) :
       ∃ v ∈ E + closedBall (0 : W) ε, y = r • v := by
   …