ShortSheetBridges.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Short bridges between the two sheets at a common pivot

theorem OAI.PolycyclicRecognition.exists_short_path_of_minimizing_paths line 14

theorem OAI.PolycyclicRecognition.exists_bridged_profile_path line 43

Source documentation

Adding the two pivot bridges preserves the template, with only the Lipschitz image of their lengths added to the height error.

theorem exists_bridged_profile_path
    {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')
    {L κ δ B r : ℝ} (hκ : 0 ≤ κ) (hδ : 0 ≤ δ) (hB : 0 ≤ B)
    (hm : PathMetricBound middle L κ) (ha : dist a a' ≤ δ) (hb : dist b' b ≤ δ)
    (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‖ ≤ B) :
    ∃ γ : Path a b, PathMetricBound γ (4 * (max L 0 + δ)) (4 * κ) ∧
      ∀ t, ∃ w ∈ E, ‖J (γ t) - J a - r • w‖ ≤ B + 2 * K * δ := by
…

Mentions: OAI.PolycyclicRecognition.PathMetricBound