OAI/GroupTheory/PolycyclicRecognition/Analysis/BridgedProfileBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_bridged_profile_bounds line 15

   Source documentation

   Normalize the two pivot-bridge errors into the same tolerance used by the Cartan tuple lifting theorem. The endpoint bound has no logarithmic term.

   theorem exists_bridged_profile_bounds
       {X W : Type*} [PseudoMetricSpace X] [NormedAddCommGroup W] [NormedSpace ℝ W]
       (hpath : ∀ a b : X, ∃ γ : Path a b, PathMetricBound γ (dist a b) 0)
       {a a' b' b : X} (middle : Path a' b')
       {C r δ ε : ℝ} (hC : 0 ≤ C) (hr : 1 ≤ r) (hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hε : 0 ≤ ε)
       (hm : PathMetricBound middle (C * r) (C * (1 + Real.log (2 + r))))
       (ha : dist a a' ≤ δ * r) (hb : dist b' b ≤ δ * r)
       (J : X → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
       (E : Set W) (hE0 : (0 : W) ∈ E)
       (himage : ∀ t, ∃ w ∈ E, ‖J (middle t) - J a' - r • w‖ ≤
         2 * r * ε + C * (1 + Real.log (2 + r)))
       (hend : ‖J b' - J a'‖ ≤ 2 * r * ε) :
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound