Local subdivision window control
ProvedLocalSubdivisionWindowControlgeometry
For an open set U containing the carrier of a polygonal path γ and a positive tolerance δ, there is a positive radius ρ such that every same-length list sufficiently close to an anchor list whose consecutive anchor segments lie in γ has its endpoint-and-segment carrier inside U and within δ of γ.carrier.
Preamble
import Definitions.Def_PolygonalPath open Classical noncomputable section
Formal statement
lemma LocalSubdivisionWindowControl
(U : Set (EuclideanSpace ℝ (Fin 2))) (γ : PolygonalPath) (δ : ℝ) :
IsOpen U →
γ.carrier ⊆ U →
0 < δ →
∃ ρ : ℝ, 0 < ρ ∧
∀ anchors xs : List (EuclideanSpace ℝ (Fin 2)),
xs.length = anchors.length →
(∀ (i : ℕ) (hi : i + 1 < anchors.length),
segment ℝ anchors[i] anchors[i + 1] ⊆ γ.carrier) →
(∀ (i : ℕ) (hxi : i < xs.length) (hai : i < anchors.length),
dist xs[i] anchors[i] < ρ) →
(({γ.source, γ.target} : Set (EuclideanSpace ℝ (Fin 2))) ∪
{p : EuclideanSpace ℝ (Fin 2) |
∃ i : ℕ, ∃ hi : i + 1 < xs.length,
p ∈ segment ℝ xs[i] xs[i + 1]}) ⊆ U ∧
(({γ.source, γ.target} : Set (EuclideanSpace ℝ (Fin 2))) ∪
{p : EuclideanSpace ℝ (Fin 2) |
∃ i : ℕ, ∃ hi : i + 1 < xs.length,
p ∈ segment ℝ xs[i] xs[i + 1]}) ⊆
{p : EuclideanSpace ℝ (Fin 2) |
∃ q : EuclideanSpace ℝ (Fin 2), q ∈ γ.carrier ∧ dist p q < δ} := by sorrySource