OAI/GroupTheory/PolycyclicRecognition/Algebra/GoodSheetWordImage.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.supportWordPath_good_image_bound line 23

   Source documentation

   Both support legs have good profiles. Every point of each switch is near its outgoing endpoint, so no condition on intermediate root sheets is introduced when concatenating the word.

   theorem supportWordPath_good_image_bound
       (d f : I → ℝ → G) (hd : ∀ i, Continuous (d i)) (hf : ∀ i, Continuous (f i))
       (hd₀ : ∀ i, d i 0 = 1) (hf₀ : ∀ i, f i 0 = 1) (d₀ : G) (r : ℝ)
       (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
       (A : Set G) (P : I → ℝ → Prop) (center : W) (E : Set W)
       {L κ B switchError : ℝ} (hL : 0 ≤ L) (hκ : 0 ≤ κ) (hswitchError : 0 ≤ switchError)
       (hbase : ∀ n ∈ A, ∃ w ∈ E, ‖J (n * d₀) - center - r • w‖ ≤ B)
       (hleg : ∀ n ∈ A, ∀ i, ∀ t : unitInterval,
         ∃ w ∈ E, ‖J ((n * d₀) * d i (r * t)) - center - r • w‖ ≤ B)
       (hmetric : ∀ n ∈ A, ∀ i b, P i b → n * f i b ∈ A →
         PathMetricBound (supportVisitPath (d i) (hd i) (hd₀ i)
           (f i) (hf i) (hf₀ i) n d₀ r b) L κ)
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.supportVisitPath