OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteSupportChainPaths.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_finite_chain_path line 16

   Source documentation

   Concatenate the actual selected edges. Both the metric constants and the common image restriction are retained with a fixed finite loss.

   theorem exists_finite_chain_path
       {X : Type*} [PseudoMetricSpace X] (L κ : ℝ) (hL : 0 ≤ L) (hκ : 0 ≤ κ)
       (S : Set X) :
       ∀ (N : ℕ) (vertex : Fin (N + 1) → X)
         (edge : ∀ j : Fin N, Path (vertex j.castSucc) (vertex j.succ)),
         vertex 0 ∈ S →
         (∀ j, PathMetricBound (edge j) L κ) →
         (∀ j t, edge j t ∈ S) →
         ∃ path : Path (vertex 0) (vertex (Fin.last N)),
           PathMetricBound path (L * 2 ^ N) (κ * 2 ^ N) ∧ ∀ t, path t ∈ S := by
   …

   Mentions: OAI.PolycyclicRecognition.PathMetricBound

2. theorem OAI.PolycyclicRecognition.exists_profile_controlled_support_chain line 54

   Source documentation

   Good profile bounds on both endpoint sheets control each outward and return leg. A short switch costs only its Lipschitz error; concatenating all selected switches yields one path with a controlled image.

   theorem exists_profile_controlled_support_chain
       {G W : Type*} [Group G] [PseudoMetricSpace G] [IsTopologicalGroup G]
       [NormedAddCommGroup W] [NormedSpace ℝ W]
       {N : ℕ} (vertex : Fin (N + 1) → G) (d₀ : G)
       (d f : Fin N → ℝ → G) (hd : ∀ j, Continuous (d j)) (hd₀ : ∀ j, d j 0 = 1)
       (hf : ∀ j, Continuous (f j)) (hf₀ : ∀ j, f j 0 = 1)
       (b : Fin N → ℝ) (hstep : ∀ j, vertex j.succ = vertex j.castSucc * f j (b j))
       (J : G → W) {K : ℝ≥0} (hJ : LipschitzWith K J)
       (center w₀ : W) (E : Set W) (r B B₀ L κ δ : ℝ)
       (hL : 0 ≤ L) (hκ : 0 ≤ κ) (hδ : 0 ≤ δ)
       (hstart : ‖J (vertex 0 * d₀) - center - r • w₀‖ ≤ B₀)
       (hbase : ∀ j, ∃ w ∈ E, ‖J (vertex j * d₀) - center - r • w‖ ≤ B)
   …