The local two-sidedness assertion of Lemma 1.8

Schoenflies/Strip.lean, Schoenflies/StripConstants.lean and Schoenflies/StripConnected.lean build the collar of a simple closed polygon and prove the global half of Lemma 1.8 (a): the collar minus the curve is the disjoint union of two connected open sets. This module adds the local half, the sentence of the blueprint that begins "In either case the two sets N_L, N_R are the two local sides of the curve in the following precise sense".

Two statements come out of it, and they are the two the polygonal Jordan curve theorem consumes.

• Schoenflies.StripData.local_two_sided and its packaging Schoenflies.StripData.exists_reference_points: a small enough disk about a point of the relative interior of an edge meets the polygon exactly in that edge, and the rest of the disk is the two open half-disks, one in each side. This is what supplies the two reference points z_L, z_R of the parity argument, together with the fact that they are separated by a single crossing of the curve.
• Schoenflies.StripData.carrier_subset_closure_sideL and …_sideR: every point of the polygon is in the closure of both sides. With StripData.sideL_disjoint_carrier this says the polygon is contained in the boundary of each side, which is what turns "there are exactly two regions" into "both regions have boundary C".

What is proved, and how

The disk argument along an edge is StripData.core_ball_trichotomy: both frame coordinates are 1-Lipschitz, so a ball of radius at most min lam rho about a point of the middle stretch of an edge cannot leave the block range in the longitudinal coordinate nor the block width in the transverse one; the sign of the transverse coordinate then reads off which of the three pieces — left block, edge, right block — the point is in.

Approaching a point of the polygon from a given side is StripData.exists_near_sides. Away from the vertices the block does it. Near a vertex the block is not available (it stops short by lam), and the approach is through the sector, reached by shrinking the transverse offset with the longitudinal one held fixed: the germ lemmas ClosedPolygon.off_sub_mem_arcL_start and friends need only that the offset be small against the progress, so at a point at distance t > 0 from the vertex any offset below t · |det| / (1 + |⟪·,·⟫|) works. At the vertex itself neither is available and the approach is instead by shrinking a point of the sector towards the vertex, which stays in the sector because an arc of directions is a cone (Plane.smul_mem_arcCCW).

Blueprint

• Schoenflies.StripData.local_two_sided, Schoenflies.StripData.exists_reference_points — Lemma 1.8, the local two-sidedness assertion, along the relative interior of an edge.
• Schoenflies.StripData.carrier_subset_closure_sideL, …_sideR — the consequence of it used for "both regions have boundary C".
• Schoenflies.ClosedPolygon.exists_two_sided_collar — Lemma 1.8 (a) with those two clauses added, in existential form.

The local two-sidedness assertion at a vertex is not proved here; see the module note at the end.

theorem Schoenflies.Plane.zero_notMem_arcCCW (u w : Plane) : 0 ∉ u.arcCCW w

The origin is on no arc: the arcs are open arcs of directions.

theorem Schoenflies.ClosedPolygon.off_sub_vertex_succ_ray {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : P.off i t s - P.vertex (i + 1) = (P.len i - t) • P.rayIn (i + 1) - s • (P.rayIn (i + 1)).perp

Seen from the vertex it arrives at, a frame position of edge i is a germ at the incoming ray there. This is the companion of ClosedPolygon.off_sub_vertex, which does the same at the vertex the edge leaves.

The four germs, for an arbitrary frame position

StripData.blockL_sub_mem_arcL_start and its three companions apply Plane.germs_split' to a point of a block, where the smallness of the offset comes from the germ field of the StripData. The four lemmas here are the same projections with the smallness left as a hypothesis, which is what an approach to a point of the curve needs: there the progress t is fixed by the point being approached and only the offset shrinks.

theorem Schoenflies.ClosedPolygon.off_sub_mem_arcL_start {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} (hs : 0 < s) (hsm : s * |inner ℝ (P.rayIn i) (P.tang i)| < t * |(P.rayIn i).det (P.tang i)|) : P.off i t s - P.vertex i ∈ (P.tang i).arcCCW (P.rayIn i)

theorem Schoenflies.ClosedPolygon.off_sub_mem_arcR_start {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} (hs : s < 0) (hsm : -s * |inner ℝ (P.rayIn i) (P.tang i)| < t * |(P.rayIn i).det (P.tang i)|) : P.off i t s - P.vertex i ∈ (P.rayIn i).arcCCW (P.tang i)

theorem Schoenflies.ClosedPolygon.off_sub_mem_arcL_finish {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} (hs : 0 < s) (hsm : s * |inner ℝ (P.rayIn (i + 1)) (P.tang (i + 1))| < (P.len i - t) * |(P.rayIn (i + 1)).det (P.tang (i + 1))|) : P.off i t s - P.vertex (i + 1) ∈ (P.tang (i + 1)).arcCCW (P.rayIn (i + 1))

theorem Schoenflies.ClosedPolygon.off_sub_mem_arcR_finish {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} (hs : s < 0) (hsm : -s * |inner ℝ (P.rayIn (i + 1)) (P.tang (i + 1))| < (P.len i - t) * |(P.rayIn (i + 1)).det (P.tang (i + 1))|) : P.off i t s - P.vertex (i + 1) ∈ (P.rayIn (i + 1)).arcCCW (P.tang (i + 1))

theorem Schoenflies.ClosedPolygon.dist_off_pt {m : ℕ} {P : ClosedPolygon m} {i : ZMod (m + 3)} {t s : ℝ} : dist (P.off i t s) (P.pt i t) = |s|

Offsetting a point of an edge moves it exactly the offset.

The disk about a point in the middle of an edge

theorem Schoenflies.StripData.core_ball_trichotomy {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {c η : ℝ} (h1 : 2 * D.lam ≤ c) (h2 : c ≤ P.len i - 2 * D.lam) (hη : η ≤ min D.lam D.rho) {y : Plane} (hy0 : y ∈ Metric.ball (P.pt i c) η) : (0 < (P.vertex i).coordAcross (P.tang i) y → y ∈ D.blockL i) ∧ ((P.vertex i).coordAcross (P.tang i) y < 0 → y ∈ D.blockR i) ∧ ((P.vertex i).coordAcross (P.tang i) y = 0 → y ∈ P.edge i)

The local picture along an edge. A ball of radius at most min lam rho about a point of the middle stretch of an edge is split by the sign of the transverse coordinate: positive is the left block, negative the right block, zero the edge itself. Both coordinates are 1-Lipschitz, which is the whole proof.

theorem Schoenflies.StripData.local_two_sided {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {i : ZMod (m + 3)} {c η : ℝ} (h1 : 2 * D.lam ≤ c) (h2 : c ≤ P.len i - 2 * D.lam) (hηpos : 0 < η) (hη : η ≤ min D.lam D.rho) : Metric.ball (P.pt i c) η ∩ P.carrier ⊆ P.edge i ∧ (∀ y ∈ Metric.ball (P.pt i c) η, y ∉ P.carrier → 0 < (P.vertex i).coordAcross (P.tang i) y ∧ y ∈ D.sideL ∨ (P.vertex i).coordAcross (P.tang i) y < 0 ∧ y ∈ D.sideR) ∧ P.off i c (η / 2) ∈ Metric.ball (P.pt i c) η ∩ D.sideL ∧ P.off i c (-(η / 2)) ∈ Metric.ball (P.pt i c) η ∩ D.sideR

Local two-sidedness at an interior point of an edge. A small enough disk about a point in the middle stretch of an edge meets the polygon exactly in that edge; off the edge the disk lies in the two blocks, one on each side; and both sides are met, at the two points obtained by offsetting the centre.

theorem Schoenflies.StripData.exists_reference_points {m : ℕ} {P : ClosedPolygon m} (D : StripData P) (i : ZMod (m + 3)) : ∃ (p : Plane) (η : ℝ), 0 < η ∧ p ∈ P.edge i ∧ Metric.ball p η ∩ P.carrier ⊆ P.edge i ∧ (∃ zL ∈ Metric.ball p η, zL ∈ D.sideL ∧ 0 < (P.vertex i).coordAcross (P.tang i) zL) ∧ ∃ zR ∈ Metric.ball p η, zR ∈ D.sideR ∧ (P.vertex i).coordAcross (P.tang i) zR < 0

The two reference points of the parity argument. On every edge there is a disk that meets the polygon only in that edge and contains a point of each side, on the two sides of the edge's line. A horizontal segment joining the two crosses the polygon exactly once, which is what makes the two reference points have opposite parity.

Every point of the polygon is on the boundary of both sides

theorem Schoenflies.StripData.exists_near_sectorL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {ε : ℝ} (hε : 0 < ε) (i : ZMod (m + 3)) : ∃ y ∈ D.sectorL i, dist y (P.vertex i) < ε

A sector comes arbitrarily close to its vertex: shrink a point of it towards the vertex, which stays in the arc because an arc of directions is a cone.

theorem Schoenflies.StripData.exists_near_sectorR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {ε : ℝ} (hε : 0 < ε) (i : ZMod (m + 3)) : ∃ y ∈ D.sectorR i, dist y (P.vertex i) < ε

theorem Schoenflies.StripData.exists_near_sides {m : ℕ} {P : ClosedPolygon m} (D : StripData P) {x : Plane} (hx : x ∈ P.carrier) {ε : ℝ} (hε : 0 < ε) : (∃ y ∈ D.sideL, dist x y < ε) ∧ ∃ y ∈ D.sideR, dist x y < ε

Both sides come arbitrarily close to every point of the polygon. Away from the vertices this is the block; at a vertex it is exists_near_sectorL; in between it is the germ with the progress held fixed and the offset shrunk below the corner's threshold.

theorem Schoenflies.StripData.carrier_subset_closure_sideL {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : P.carrier ⊆ closure D.sideL

Every point of the polygon is in the closure of the left side. With StripData.sideL_disjoint_carrier this says the polygon is contained in the boundary of the left side.

theorem Schoenflies.StripData.carrier_subset_closure_sideR {m : ℕ} {P : ClosedPolygon m} (D : StripData P) : P.carrier ⊆ closure D.sideR

theorem Schoenflies.ClosedPolygon.exists_two_sided_collar {m : ℕ} (P : ClosedPolygon m) {U : Set Plane} (hU : IsOpen U) (hPU : P.carrier ⊆ U) : ∃ (N : Set Plane) (NL : Set Plane) (NR : Set Plane), IsOpen N ∧ P.carrier ⊆ N ∧ N ⊆ U ∧ IsOpen NL ∧ IsOpen NR ∧ IsConnected NL ∧ IsConnected NR ∧ Disjoint NL NR ∧ N \ P.carrier = NL ∪ NR ∧ P.carrier ⊆ closure NL ∧ P.carrier ⊆ closure NR

Lemma 1.8 (a), with the boundary clause. A simple closed polygon has an open neighbourhood N, inside any prescribed open set containing it, whose complement in N is the disjoint union of two connected open sets, each of which has the polygon in its closure.

What is still missing from Lemma 1.8

Two things.

• The local two-sidedness assertion at a vertex. StripData.ball_diff_carrier_subset already says that a ball of radius R about a vertex minus the polygon lies in the two sectors there, and StripData.sectorL_disjoint_sectorR (through sideL_disjoint_sideR) says those are disjoint; what is not proved is that each of the two intersections ball (P.vertex i) η ∩ sectorL i is connected, i.e. that the ball minus the curve has exactly two components at a vertex rather than merely being covered by two disjoint open sets. For a ball of radius η ≤ R this is true and the proof is the one in Plane.isConnected_arcCCW_ball, since ball (P.vertex i) η ∩ sectorL i = cone (P.vertex i) A η for the same arc A. Nothing in the polygonal Jordan curve theorem needs it.
• Lemma 1.8 (b), the case of a polygonal arc with a compact subarc of its interior. The blocks and sectors here are built from a cyclic vertex family; the arc case needs the same construction along a linear chain, with the two end cross-sections and no cap. None of it is formalised.