Strongly accessible boundary points

A point p of the boundary of a region D is strongly accessible when an open disk contained in D is tangent to the boundary at p. Ordinary accessibility (some arc in D ending at p) is too weak for the iterative construction: what is wanted at p is a definite wedge of straight segments running into D, which can then be shrunk to avoid any compact set already built.

This module supplies that wedge. The tangent disk B(q, r) at p is turned into the open cone accessCone p v s of points seen from p in a direction within 60 degrees of v = (q - p)/r and at distance less than s; the content of Lemma 8.4 is that this cone lies in the disk as soon as s ≤ r, and hence in D.

Blueprint

• Schoenflies.StronglyAccessible — Definition 8.1 (strong accessibility).
• Schoenflies.stronglyAccessible_of_isMinOn — Lemma 8.2 (nearest points are strongly accessible).
• Schoenflies.tangent_cone — Lemma 8.4 (tangent-disk cone), in the literal form of the blueprint; Schoenflies.accessCone_subset_ball is the same estimate packaged as the inclusion of a truncated cone, which is the form the consumers use.
• Schoenflies.exists_countable_dense_stronglyAccessible — Proposition 8.5 (countable dense strong-access set).

Lemma 8.3 (density of strongly accessible points) is not formalized here: its proof runs through C = ∂D, i.e. through the Jordan curve theorem, which is not yet available. Its role is played by Proposition 8.5, which is stated with C ⊆ closure D as a hypothesis.

Strong accessibility

def Schoenflies.StronglyAccessible (D : Set Plane) (p : Plane) : Prop

Definition 8.1 (strong accessibility). A point p is strongly accessible from D when some open disk of positive radius contained in D is tangent to p, that is, has p on its boundary circle.

Equations

• Schoenflies.StronglyAccessible D p = ∃ (q : Schoenflies.Plane) (r : ℝ), 0 < r ∧ dist q p = r ∧ Metric.ball q r ⊆ D

theorem Schoenflies.StronglyAccessible.mono {D E : Set Plane} {p : Plane} (h : StronglyAccessible D p) (hDE : D ⊆ E) : StronglyAccessible E p

theorem Schoenflies.StronglyAccessible.exists_ne {D : Set Plane} {p : Plane} (h : StronglyAccessible D p) : ∃ q ∈ D, p ≠ q

The centre of a tangent disk is not the point of tangency.

theorem Schoenflies.stronglyAccessible_of_isMinOn {C D : Set Plane} {q a : Plane} (hq : q ∉ C) (ha : a ∈ C) (hmin : ∀ b ∈ C, dist q a ≤ dist q b) (hD : connectedComponentIn Cᶜ q ⊆ D) : StronglyAccessible D a

Lemma 8.2 (nearest points are strongly accessible). If a ∈ C is nearest to a point q off C, then the ball of radius dist q a around q misses C; being connected it stays inside the connected component of q in the complement of C, so any set D containing that component contains a disk tangent to C at a.

The hypothesis is phrased as connectedComponentIn Cᶜ q ⊆ D rather than as D being that component, so that it can be discharged by an inclusion when D is known only up to containment. No closedness of C is needed.

The cone of access directions

def Schoenflies.accessCone (p v : Plane) (s : ℝ) : Set Plane

The open cone of straight access segments at p around the unit direction v, truncated at radius s: the points seen from p in a direction w with ⟪v, w⟫ > 1/2 and at distance less than s. Writing the condition as ‖x - p‖ / 2 < ⟪v, x - p⟫ avoids normalizing x - p, and makes the openness of the cone immediate.

Equations

• Schoenflies.accessCone p v s = {x : Schoenflies.Plane | ‖x - p‖ < s ∧ ‖x - p‖ / 2 < inner ℝ v (x - p)}

theorem Schoenflies.mem_accessCone_iff {p v : Plane} {s : ℝ} {x : Plane} : x ∈ accessCone p v s ↔ ‖x - p‖ < s ∧ ‖x - p‖ / 2 < inner ℝ v (x - p)

theorem Schoenflies.accessCone_subset_ball_self {p v : Plane} {s : ℝ} : accessCone p v s ⊆ Metric.ball p s

theorem Schoenflies.notMem_accessCone {p v : Plane} {s : ℝ} : p ∉ accessCone p v s

The apex is not in the cone: the cone is a set of access points, all distinct from p.

theorem Schoenflies.accessCone_mono {p v : Plane} {s s' : ℝ} (hs : s ≤ s') : accessCone p v s ⊆ accessCone p v s'

theorem Schoenflies.isOpen_accessCone {p v : Plane} {s : ℝ} : IsOpen (accessCone p v s)

The cone is open.

theorem Schoenflies.mem_accessCone {p v w : Plane} {s t : ℝ} (hw : ‖w‖ = 1) (hcone : 1 / 2 < inner ℝ v w) (ht : 0 < t) (hts : t < s) : p + t • w ∈ accessCone p v s

Membership in the cone in the form used by the blueprint: a unit direction w making an angle of less than 60 degrees with v, and a distance t below the truncation radius.

theorem Schoenflies.accessCone_nonempty {p v : Plane} {s : ℝ} (hv : ‖v‖ = 1) (hs : 0 < s) : (accessCone p v s).Nonempty

The cone at p around the direction v is nonempty for every positive truncation radius: the direction v itself is admissible.

theorem Schoenflies.openSegment_subset_accessCone {p v w : Plane} {s : ℝ} (hw : ‖w‖ = 1) (hcone : 1 / 2 < inner ℝ v w) (hs : 0 < s) : openSegment ℝ p (p + s • w) ⊆ accessCone p v s

An open segment leaving p in an admissible direction lies in the cone.

The tangent-disk cone

theorem Schoenflies.accessCone_subset_ball {p q : Plane} {r s : ℝ} (hr : 0 < r) (hpq : ‖q - p‖ = r) (hs : s ≤ r) : accessCone p (r⁻¹ • (q - p)) s ⊆ Metric.ball q r

Lemma 8.4 (tangent-disk cone), in the form the construction uses. If the disk B(q, r) is tangent at p, then the whole truncated cone around v = (q - p)/r of any radius s ≤ r lies inside that disk.

The estimate behind it is the blueprint's: for x in the cone, with d = ‖x - p‖, ‖x - q‖² = d² - 2⟪x - p, q - p⟫ + r² < d² - rd + r² = r² + d(d - r) < r².

theorem Schoenflies.tangent_cone {p q w : Plane} {r t : ℝ} (hr : 0 < r) (hpq : ‖q - p‖ = r) (hw : ‖w‖ = 1) (hcone : 1 / 2 < inner ℝ (r⁻¹ • (q - p)) w) (ht : 0 < t) (htr : t < r) : p + t • w ∈ Metric.ball q r

Lemma 8.4 (tangent-disk cone), in the literal form of the blueprint: if B(q, r) is tangent at p, v = (q - p)/r, and w is a unit vector with ⟪v, w⟫ > 1/2, then the straight ray from p in the direction w stays in the disk up to distance r.

theorem Schoenflies.StronglyAccessible.exists_cone {D : Set Plane} {p : Plane} (h : StronglyAccessible D p) : ∃ (v : Plane), ‖v‖ = 1 ∧ ∃ r > 0, ∀ s ≤ r, accessCone p v s ⊆ D

A strongly accessible point has a nonempty open cone of straight access segments into D, and the cone may be truncated at any radius below the radius of the tangent disk — which is how the construction makes it avoid a compact set already built.

theorem Schoenflies.StronglyAccessible.openSegment_subset {D : Set Plane} {p : Plane} (h : StronglyAccessible D p) : ∃ z ∈ D, p ≠ z ∧ openSegment ℝ p z ⊆ D

A strongly accessible point is the endpoint of a straight access segment: the open segment from p to the centre of the tangent disk lies in D.

A countable dense set of strongly accessible points

theorem Schoenflies.exists_countable_dense_stronglyAccessible {C D : Set Plane} (hC : IsCompact C) (hCne : C.Nonempty) (hDopen : IsOpen D) (hDC : D ⊆ Cᶜ) (hDmax : ∀ q ∈ D, connectedComponentIn Cᶜ q ⊆ D) (hCD : C ⊆ closure D) : ∃ A ⊆ C, A.Countable ∧ (∀ a ∈ A, StronglyAccessible D a) ∧ C ⊆ closure A

Proposition 8.5 (countable dense strong-access set). For every rational point of D pick a nearest point of C; the chosen points are countably many, all strongly accessible, and dense in C, since a point of C is approximated by points of D and the nearest point of C to such a q is at most dist q p from q, hence at most 2 * dist q p from p.

The hypothesis C ⊆ closure D replaces the blueprint's appeal to C = ∂D (Theorem 6.1); hDmax says D swallows the connected component in Cᶜ of each of its points, which holds when D is such a component.