OAI/GroupTheory/PolycyclicRecognition/Analysis/AffineProfileControlledPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_affine_profile_controlled_path line 17

   Source documentation

   Uniform approximation by one affine profile controls the actual outward legs, short switches and return legs. The affine offset cancels when the image path is centered at its original endpoint.

   theorem exists_affine_profile_controlled_path
       {G W V Z : Type*} [Group G] [PseudoMetricSpace G] [IsTopologicalGroup G]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [AddCommGroup V] [Module ℝ V]
       {N : ℕ} (x : G) (vertex : Fin (N + 1) → G)
       (φ : Z → G) (q : Z → V) (z₀ : Z)
       (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)
       (A : V →ₗ[ℝ] W) (offset : W) (r ε L κ δ : ℝ)
       (hL : 0 ≤ L) (hκ : 0 ≤ κ) (hδ : 0 ≤ δ)
       (Q : Set Z) (hz₀ : z₀ ∈ Q)
   …