The constants of a polygonal collar exist

Schoenflies.StripData names the three numbers the two-sided strip lemma runs on — a cone radius R, a trim lam and a half-width rho — together with the separation hypotheses they have to satisfy. Everything in Schoenflies/Strip.lean is stated for a given StripData; this module produces one, removing that parameter from the resulting theorem.

The recipe is the blueprint's own, in the blueprint's order:

1. R from three sources — the pairwise vertex separations, the distance from each vertex to each nonincident edge, and the prescribed open set — each an instance of Lemma 1.4, plus R ≤ len i so that a sector cannot run past the far end of an incident edge. The vertex separations are asked for with a factor 2 of slack, which is what the block-versus-sector estimates of Strip.lean spend.
2. lam := R / 5, which gives 2 * lam < R and, through R ≤ len i, also 4 * lam < len i.
3. rho from the distance of each trimmed edge to every other edge, and from the germ threshold rho * (1 + |⟪r₁, r₂⟫|) ≤ lam * |det r₁ r₂| at every vertex. The determinant is nonzero at a corner, so the threshold is a positive upper bound on rho and is met by shrinking; rho < lam is one more shrinking.

Steps 1 and 3 are finite families of positive bounds, combined by Schoenflies.exists_pos_forall_of_finite.

What simplicity is used for

Two of the separations are false for a self-touching closed polygonal curve, and each is the exact point where ClosedPolygon.edges_meet is consumed:

• ClosedPolygon.vertex_notMem_edge — a vertex lies on no edge but the two incident to it. This is what makes {vertex i} and edge j disjoint compact sets.
• ClosedPolygon.trimmed_disjoint_edge — the trimmed core of an edge misses every other edge. Here the two endpoints allowed by edges_meet are excluded by the trim itself, since a point of the core is at distance at least lam from both.

edges_meet as stated is one-sided (edge i ∩ edge j ⊆ {vertex i, vertex (i + 1)}), but it is quantified over all ordered pairs, so the symmetric instance is available and both proofs below use whichever side is convenient. It carries enough simplicity for both statements.

Blueprint

• Schoenflies.exists_stripData_subset — the constants of Lemma 1.8 (Two-sided polygonal strips), chosen inside a prescribed open set containing the curve; this is the "Lemma 1.4 (a) lets all disks and strips be chosen inside the prescribed open set" of the last paragraph of the proof.
• Schoenflies.exists_stripData — the same without a prescribed open set.
• Schoenflies.ClosedPolygon.exists_cone_radius, Schoenflies.ClosedPolygon.exists_half_width — steps 1 and 3 of the recipe, which are the instances of Lemma 1.4 that Lemma 1.8 consumes.
• Schoenflies.StripData.nbhd_subset_thickening — the collar of Lemma 1.8 lies in the R-neighbourhood of the curve, which is how the prescribed open set is honoured.

Compactness of the pieces

theorem Schoenflies.ClosedPolygon.isCompact_edge {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} : IsCompact (P.edge i)

theorem Schoenflies.ClosedPolygon.isCompact_carrier {m : ℕ} (P : ClosedPolygon m) : IsCompact P.carrier

theorem Schoenflies.ClosedPolygon.continuous_pt {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) : Continuous (P.pt i)

What simplicity gives

The two statements below are the only consumers of ClosedPolygon.edges_meet in the whole choice of constants, and neither is true without it.

theorem Schoenflies.ClosedPolygon.vertex_notMem_edge {m : ℕ} {P : ClosedPolygon m} {i j : ZMod (m + 3)} (hj1 : j ≠ i - 1) (hj2 : j ≠ i) : P.vertex i ∉ P.edge j

Simplicity, first form. A vertex lies on no edge but the two edges incident to it. Without this the "a vertex is 2R away from every nonincident edge" hypothesis of StripData would be unsatisfiable, since the vertex would sit on one of those edges.

def Schoenflies.ClosedPolygon.trimmed {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) (lam : ℝ) : Set Plane

The trimmed core of edge i: the points of the edge at distance at least lam from both of its endpoints. An edge block of StripData hugs this core.

Equations

• P.trimmed i lam = P.pt i '' Set.Icc lam (P.len i - lam)

theorem Schoenflies.ClosedPolygon.pt_mem_trimmed {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {c lam : ℝ} (hc : c ∈ Set.Icc lam (P.len i - lam)) : P.pt i c ∈ P.trimmed i lam

theorem Schoenflies.ClosedPolygon.isCompact_trimmed {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {lam : ℝ} : IsCompact (P.trimmed i lam)

theorem Schoenflies.ClosedPolygon.trimmed_disjoint_edge {m : ℕ} {P : ClosedPolygon m} {i j : ZMod (m + 3)} {lam : ℝ} (hlam : 0 < lam) (hij : j ≠ i) : Disjoint (P.trimmed i lam) (P.edge j)

Simplicity, second form. The trimmed core of an edge misses every other edge. The two common points edges_meet allows are the endpoints of the edge, and the trim removes them: a core point is at distance at least lam from either endpoint. No lower bound on the edge length is needed: if the trim eats the whole edge the core is empty.

Where the collar lives

The collar sits inside the R-neighbourhood of the curve: a sector is inside a ball of radius R about a point of the curve, and a block is within rho < R of the foot of its perpendicular, which is on the curve. This is the whole content of "the neighbourhoods may be chosen inside any prescribed open set containing the curve".

theorem Schoenflies.StripData.nbhd_subset_thickening {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : D.nbhd ⊆ Metric.thickening D.R P.carrier

The collar of Strip.lean lies in the R-neighbourhood of the polygon.

Choosing the constants

theorem Schoenflies.ClosedPolygon.exists_cone_radius {m : ℕ} (P : ClosedPolygon m) {U : Set Plane} (hU : IsOpen U) (hPU : P.carrier ⊆ U) : ∃ R > 0, (∀ (i : ZMod (m + 3)), R ≤ P.len i) ∧ (∀ (i j : ZMod (m + 3)), i ≠ j → 2 * R ≤ dist (P.vertex i) (P.vertex j)) ∧ (∀ (i j : ZMod (m + 3)), j ≠ i - 1 → j ≠ i → ∀ y ∈ P.edge j, 2 * R ≤ dist (P.vertex i) y) ∧ Metric.thickening R P.carrier ⊆ U

Step 1: the cone radius. One positive R that is below every edge length, that separates the vertices pairwise with a factor 2 to spare, that keeps every vertex 2R away from every nonincident edge, and whose neighbourhood of the curve stays inside the prescribed open set.

theorem Schoenflies.ClosedPolygon.exists_germ_bound {m : ℕ} (P : ClosedPolygon m) (i : ZMod (m + 3)) {lam : ℝ} (hlam : 0 < lam) : ∃ ε > 0, ε * (1 + |inner ℝ (P.rayIn i) (P.tang i)|) ≤ lam * |(P.rayIn i).det (P.tang i)|

The germ threshold at a single vertex. The corner condition makes det ≠ 0, so the right side is positive and the inequality is a genuine upper bound on the half-width.

theorem Schoenflies.ClosedPolygon.exists_half_width {m : ℕ} (P : ClosedPolygon m) {lam : ℝ} (hlam : 0 < lam) : ∃ rho > 0, rho < lam ∧ (∀ (i j : ZMod (m + 3)), j ≠ i → ∀ c ∈ Set.Icc lam (P.len i - lam), ∀ y ∈ P.edge j, 2 * rho ≤ dist (P.pt i c) y) ∧ ∀ (i : ZMod (m + 3)), rho * (1 + |inner ℝ (P.rayIn i) (P.tang i)|) ≤ lam * |(P.rayIn i).det (P.tang i)|

Step 3: the half-width. One positive rho below lam, separating each trimmed edge from every other edge with a factor 2 to spare, and meeting the germ threshold at every vertex. Only 0 < lam is needed: if lam were so large that a trimmed edge came out empty, its separation clause would be vacuous.

theorem Schoenflies.exists_stripData_subset {m : ℕ} (P : ClosedPolygon m) {U : Set Plane} (hU : IsOpen U) (hPU : P.carrier ⊆ U) : ∃ (D : StripData P), D.nbhd ⊆ U

Lemma 1.8, the constants. Every simple closed polygon carries a StripData, and its collar can be put inside any prescribed open set containing the curve. This is what makes Schoenflies/Strip.lean with the required constants supplied.

theorem Schoenflies.exists_stripData {m : ℕ} (P : ClosedPolygon m) : Nonempty (StripData P)

Every simple closed polygon carries a StripData.