CoarsePathMesh.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite meshes for paths with short jumps

The support-switch construction has a bounded number of logarithmically short switches. An additive coarse error in its parameterized path therefore contributes only the corresponding additive error to the height comparison.

theorem OAI.PolycyclicRecognition.coarse_image_path_height_control line 23

Source documentation

Sampled height estimates control a whole coarse path, retaining the additive distance error explicitly.

theorem coarse_image_path_height_control
    (p : NormalizedPair G Λ) (π : G →* Multiplicative W) (l : G →* Multiplicative W)
    {Lπ L r δ η ε κ : ℝ} (hLπ : 0 ≤ Lπ) (hL : 0 ≤ L) (hr : 0 ≤ r)
    (hπ : ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ Lπ * dist x y)
    (γ : T → G) (hγ : ∀ t u, dist (γ t) (γ u) ≤ L * r * dist t u + κ)
    (S : Finset T) (hmesh : ∀ t, ∃ u ∈ S, dist t u ≤ δ)
    (E : Set W)
    (hheight : ∀ u ∈ S, ∃ w ∈ E, ‖(l (γ u)).toAdd - r • w‖ ≤ ε * r)
    (herror : ∀ u ∈ S, ‖pairHeight π (γ u) p - (l (γ u)).toAdd‖ ≤ η * r) :
    ∀ t, ∃ w ∈ E,
      ‖pairHeight π (γ t) p - r • w‖ ≤
        (Lπ * Λ * L * δ + η + ε) * r + Lπ * Λ * κ := by
…

Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.pairHeight