OAI/GroupTheory/PolycyclicRecognition/Analysis/ConjugatedSheetPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_common_sheet_word_path line 19

   Source documentation

   The same pivot bridge bound applies at both ends of every bundle; the initial good state and its accumulated prefix cancel by left invariance.

   theorem exists_common_sheet_word_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|)
       (ι : N →* G) (x d : G) (n n' k : N)
       (middle : Path (x * ι (n * k) * d) (x * ι (n' * k) * d))
       {L κ δ B r : ℝ} (hκ : 0 ≤ κ) (hδ : 0 ≤ δ) (hB : 0 ≤ B)
       (hm : PathMetricBound middle L κ) (hk : dist d (ι k * d) ≤ δ)
       (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
       (E : Set W) (hE0 : (0 : W) ∈ E)
       (himage : ∀ t, ∃ w ∈ E,
         ‖J (middle t) - J (x * ι (n * k) * d) - r • w‖ ≤ B) :
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound