CenteredProfilePaths.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Centering profile-controlled paths at their actual initial image

theorem OAI.PolycyclicRecognition.norm_centered_sub_smul_le line 15

Source documentation

Centering costs only the profile error at the initial point.

theorem norm_centered_sub_smul_le {u a c w w₀ : W} {r B B₀ : ℝ}
    (hu : ‖u - c - r • w‖ ≤ B) (ha : ‖a - c - r • w₀‖ ≤ B₀) :
    ‖u - a - r • (w - w₀)‖ ≤ B + B₀ := by
…

theorem OAI.PolycyclicRecognition.centered_path_height_bound line 26

Source documentation

An entire path over a prescribed profile image lies over its translated image when centered at its actual start, with the same explicit error.

theorem centered_path_height_bound
    {X : Type*} [TopologicalSpace X] {a b : X} (γ : Path a b) (J : X → W)
    (center w₀ : W) (E : Set W) (r B B₀ : ℝ)
    (hstart : ‖J a - center - r • w₀‖ ≤ B₀)
    (hpath : ∀ t, ∃ w ∈ E, ‖J (γ t) - center - r • w‖ ≤ B) :
    ∀ t, ∃ w ∈ (fun z => z - w₀) '' E, ‖J (γ t) - J a - r • w‖ ≤ B + B₀ := by
…

theorem OAI.PolycyclicRecognition.relative_height_of_rescaled_profile line 38

Source documentation

Two points of the same good normalized profile give an unnormalized relative height bound at the true exponential scale.

theorem relative_height_of_rescaled_profile
    {G Z : Type*} [Group G] (J : G → W) (x n : G) (s : ℝ) (φ : Z → G)
    (z z₀ : Z) (w w₀ : W) {ε ε₀ : ℝ}
    (hz : ‖rescaledMapProfile J x n s φ z - w‖ ≤ ε)
    (hz₀ : ‖rescaledMapProfile J x n s φ z₀ - w₀‖ ≤ ε₀) :
    ‖J (x * n * φ z) - J (x * n * φ z₀) - Real.exp s • (w - w₀)‖ ≤
      Real.exp s * (ε + ε₀) := by
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile