PolygonalArcCollarCompatibleOrientedTubeDataExistsBelow
ProvedPolygonalArcCollarCompatibleOrientedTubeDataExistsBelowcrossing-consequencesgeometrypolygonal
Given a polygonal arc, collar-control radii, middle segments, forbidden margins, endpoint-isolation radii, and positive cone bounds, there exist compatible oriented tube data whose endpoint cone bounds fit the prescribed constants and whose non-endpoint tubes avoid the endpoint balls.
Preamble
import Definitions.Def_PolygonalArcCollarCompatibleOrientedTubeData import Definitions.Def_PolygonalArcEndpointIsolation import Mathlib.Tactic open Classical noncomputable section
Formal statement
lemma PolygonalArcCollarCompatibleOrientedTubeDataExistsBelow (γ : PolygonalArc)
{η : ℝ} (controlRadii : PolygonalArcCollarControlRadii γ η)
(middleSegments : PolygonalArcCollarMiddleSegmentData γ controlRadii)
(forbiddenMargins :
PolygonalArcCollarMiddleForbiddenMargins γ controlRadii middleSegments)
(r₀ r₁ K₀ K₁ : ℝ) :
PolygonalArcEndpointIsolation γ r₀ r₁ →
0 < K₀ →
0 < K₁ →
let hfirst : 0 + 1 < γ.vertices.length := by
have hlen := γ.length_ge_two
omega
let jlast : ℕ := γ.vertices.length - 2
let hlast : jlast + 1 < γ.vertices.length := by
have hlen := γ.length_ge_two
dsimp [jlast]
omega
∃ compatibleTubes :
PolygonalArcCollarCompatibleOrientedTubeData γ controlRadii
middleSegments forbiddenMargins,
compatibleTubes.initialConeBound 0 hfirst < K₀ ∧
compatibleTubes.terminalConeBound jlast hlast < K₁ ∧
(∀ (j : ℕ) (hj : j + 1 < γ.vertices.length), j ≠ 0 →
Disjoint
(compatibleTubes.orientedTubes.toPolygonalArcCollarSeparatedTubeData.tube
j hj)
(Metric.ball γ.source r₀)) ∧
(∀ (j : ℕ) (hj : j + 1 < γ.vertices.length), j ≠ jlast →
Disjoint
(compatibleTubes.orientedTubes.toPolygonalArcCollarSeparatedTubeData.tube
j hj)
(Metric.ball γ.target r₁)) := by sorrySource