CenteredImagePaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Centered image paths for the two probe sheets

def OAI.PolycyclicRecognition.centeredImagePath line 19

Source documentation

Center the image path at its actual initial image.

def centeredImagePath (f : X → G) (hf : Continuous f) {a b : X} (γ : Path a b) :
    Path (1 : G) ((f a)⁻¹ * f b) where
…

theorem OAI.PolycyclicRecognition.centeredImagePath_metric_bound line 35
Source documentation
Quasi-isometry Lipschitz control transfers to the centered path with the same scaling of both the speed and the additive error.
```
theorem centeredImagePath_metric_bound (f : X → G) {K : ℝ≥0} (hf : LipschitzWith K f)
    {a b : X} (γ : Path a b) {L κ : ℝ} (hγ : PathMetricBound γ L κ) :
    PathMetricBound (centeredImagePath f hf.continuous γ) (K * L) (K * κ) := by
…
```
Mentions: OAI.PolycyclicRecognition.PathMetricBound, OAI.PolycyclicRecognition.centeredImagePath

theorem OAI.PolycyclicRecognition.centeredImagePath_height_bound line 55

Source documentation

The centered path has exactly the relative height required by the factor-lifting theorem. The profile error at its start is retained.

theorem centeredImagePath_height_bound
    (f : X → G) (hf : Continuous f) (π : G →* Multiplicative W)
    {a b : X} (γ : Path a b) (center w₀ : W) (E : Set W) (r B B₀ : ℝ)
    (hstart : ‖(π (f a)).toAdd - center - r • w₀‖ ≤ B₀)
    (hpath : ∀ t, ∃ w ∈ E, ‖(π (f (γ t))).toAdd - center - r • w‖ ≤ B) :
    ∀ t, ∃ w ∈ (fun z => z - w₀) '' E,
      ‖(π (centeredImagePath f hf γ t)).toAdd - r • w‖ ≤ B + B₀ := by
…

Mentions: OAI.PolycyclicRecognition.centeredImagePath