PolygonalArcCollarControlRadiiExistsBelow
ProvedPolygonalArcCollarControlRadiiExistsBelowcrossing-consequencesgeometrypolygonal
For a polygonal arc, positive tolerance, and positive endpoint-isolation radii, there exist positive collar-control radii smaller than the tolerance, with endpoint radii below the isolation radii and the required endpoint-ball disjointness properties.
Preamble
import Definitions.Def_PolygonalArcCollarControlRadii import Definitions.Def_PolygonalArcEndpointIsolation import Mathlib.Tactic open Classical noncomputable section
Formal statement
lemma PolygonalArcCollarControlRadiiExistsBelow (γ : PolygonalArc)
(η r₀ r₁ : ℝ) :
0 < η →
0 < r₀ →
0 < r₁ →
PolygonalArcEndpointIsolation γ r₀ r₁ →
let hsource : 0 < γ.vertices.length := by
have hlen := γ.length_ge_two
omega
let htarget : γ.vertices.length - 1 < γ.vertices.length := by
have hlen := γ.length_ge_two
omega
∃ controlRadii : PolygonalArcCollarControlRadii γ η,
controlRadii.radius ⟨0, hsource⟩ < r₀ ∧
controlRadii.radius ⟨γ.vertices.length - 1, htarget⟩ < r₁ ∧
(∀ i : Fin γ.vertices.length, i.1 ≠ 0 →
Disjoint
(Metric.ball γ.vertices[i.1] (controlRadii.radius i))
(Metric.ball γ.source r₀)) ∧
(∀ i : Fin γ.vertices.length,
i.1 + 1 ≠ γ.vertices.length →
Disjoint
(Metric.ball γ.vertices[i.1] (controlRadii.radius i))
(Metric.ball γ.target r₁)) := by sorrySource