The local windows W_n(p) of the stage recursion

The paragraph of jordan_schoenflies.tex between thm:finite-transfer and prop:local-grid-attachment fixes, for each p ∈ D and each n,

r(p)   = dist_∞(p, C),
s_n(p) = r(p) - min(r(p)/2, ε_n),
W_n(p) = { x : ‖x - p‖_∞ ≤ s_n(p) },

and records 0 < s_n(p) < r(p), r(p) - s_n(p) ≤ ε_n, and W_n(p) ⊆ D. Those four lines and the arithmetic that prop:shrinking-stars performs on them are all this module contains. It is entirely metric: no cell structure, no graph, nothing from Part II. That is deliberate — the window bookkeeping is the one part of the quantitative refinement that can be finished before the recursion it serves exists, and getting the constants wrong later, inside a proof that also has to manage cellulations, is expensive.

Why an ℓ^∞ distance-to-a-set had to be built

Plane carries the Euclidean metric, so Metric.infDist is the Euclidean distance to a set and Schoenflies.Plane.supDist is a bare two-argument function with no set version. Schoenflies.supRadius is the ℓ^∞ distance to a compact set, defined as the infimum of the attained values. Everything the blueprint uses of it is here: it is attained (exists_supRadius_eq), it is positive off the set (supRadius_pos), it is 1-Lipschitz in the ℓ^∞ metric (supRadius_le_add, abs_supRadius_sub_le) — "the distance-to-C function is 1-Lipschitz in the ℓ^∞ metric" — and the open ℓ^∞ ball of radius r(p) about a point of the Jordan domain lies in the Jordan domain (openSquare_supRadius_subset_inside), which is the blueprint's "since C = ∂D, the open axis-parallel square of radius r(p) centred at p lies in D".

The last one is not proved through C = ∂D but through the component characterisation: the square is convex, hence connected, and misses C by the very definition of r(p), so it lies in the connected component of Cᶜ containing p — which is inside C by thm:jordan.

What prop:shrinking-stars extracts from this

Schoenflies.mem_openWindow_of_supDist_lt is the whole first half of that proof's arithmetic, with the blueprint's constants:

Fix x ∈ D and put d = dist_∞(x, C) > 0. Choose b ∈ B with ‖b - x‖_∞ < d/8 … Since r(·) is 1-Lipschitz, r(b) ≥ r(x) - ‖b - x‖_∞ > 7d/8. Consequently s_n(b) ≥ r(b) - ε_n > 3d/4. Because ‖b - x‖_∞ < d/8, the point x lies in the interior of W_n(b).

Nothing here mentions the enumeration b_1, b_2, … of B = ℚ² ∩ D or the sequence ε_n = 2^{-n}; windowRadius takes ε as a parameter, so the recursion may pick the sequence. Schoenflies.exists_mem_rat_supDist_lt is the one fact about B the proof uses — that a dense subset of the plane supplies a b as close to x as asked, inside D.

Blueprint

• Schoenflies.supRadius, .exists_supRadius_eq, .supRadius_le, .supRadius_nonneg, .supRadius_pos, .notMem_of_supDist_lt_supRadius — r(p) = dist_∞(p, C).
• Schoenflies.supRadius_le_add, .abs_supRadius_sub_le — "the distance-to-C function is 1-Lipschitz in the ℓ^∞ metric".
• Schoenflies.openSquare_supRadius_subset_inside — "since C = ∂D, the open axis-parallel square of radius r(p) centred at p lies in D".
• Schoenflies.windowRadius, Schoenflies.window, Schoenflies.openWindow — s_n(p), W_n(p), and its interior.
• Schoenflies.windowRadius_pos, .windowRadius_lt_supRadius, .sub_windowRadius_le, .window_subset_inside — the three displayed inequalities and W_n(p) ⊆ D.
• Schoenflies.mem_openWindow_of_supDist_lt — the arithmetic of prop:shrinking-stars.
• Schoenflies.exists_mem_rat_supDist_lt — the only property of B = ℚ² ∩ D used.
• Schoenflies.recur, .exists_le_recur_eq — "a sequence in which every point of B occurs infinitely often", and the consequence prop:shrinking-stars uses.
• Schoenflies.tendsto_two_pow_neg, .two_pow_neg_pos — ε_n = 2^{-n}.

One missing fact about supDist

Schoenflies/Square.lean has the ℓ^∞ norm, the ℓ^∞ distance, the triangle inequality and the two comparisons with the Euclidean norm, but not that supDist separates points. It is needed once below, to see that r(p) > 0 off a compact set. It belongs in Square.lean; it is here because this is its first use.

theorem Schoenflies.Plane.eq_of_supDist_eq_zero {p q : Plane} (h : p.supDist q = 0) : p = q

The ℓ^∞ distance separates points.

The ℓ^∞ distance to a compact set

noncomputable def Schoenflies.supRadius (C : Set Plane) (p : Plane) : ℝ

r(p) = dist_∞(p, C), the ℓ^∞ distance from a point to a set.

Defined as the infimum of the attained values rather than through Metric.infDist, which is the Euclidean distance: Plane carries the Euclidean metric and the blueprint's windows are axis-parallel squares. On a compact nonempty set the infimum is attained (exists_supRadius_eq), which is all that is ever used.

Equations

• Schoenflies.supRadius C p = sInf (p.supDist '' C)

theorem Schoenflies.supDist_continuousOn (p : Plane) : Continuous p.supDist

theorem Schoenflies.exists_supRadius_eq {C : Set Plane} (hC : IsCompact C) (hCne : C.Nonempty) (p : Plane) : ∃ q ∈ C, supRadius C p = p.supDist q ∧ ∀ z ∈ C, p.supDist q ≤ p.supDist z

The ℓ^∞ distance to a nonempty compact set is attained.

theorem Schoenflies.supRadius_le {C : Set Plane} {q : Plane} (hC : IsCompact C) (hCne : C.Nonempty) (p : Plane) (hq : q ∈ C) : supRadius C p ≤ p.supDist q

Every point of the set is at least r(p) away, in the ℓ^∞ metric.

theorem Schoenflies.supRadius_nonneg {C : Set Plane} (hC : IsCompact C) (hCne : C.Nonempty) (p : Plane) : 0 ≤ supRadius C p

theorem Schoenflies.supRadius_pos {C : Set Plane} {p : Plane} (hC : IsCompact C) (hCne : C.Nonempty) (hp : p ∉ C) : 0 < supRadius C p

Off a compact set the ℓ^∞ distance to it is positive.

theorem Schoenflies.notMem_of_supDist_lt_supRadius {C : Set Plane} {p x : Plane} (hC : IsCompact C) (hCne : C.Nonempty) (h : x.supDist p < supRadius C p) : x ∉ C

A point strictly nearer than r(p) is off the set: this is the definition read backwards, and it is what makes the window miss C.

1-Lipschitz

"The distance-to-C function is 1-Lipschitz in the ℓ^∞ metric." Only the one-sided form is used — r(b) ≥ r(x) - ‖b - x‖_∞ — but both are recorded.

theorem Schoenflies.supRadius_le_add {C : Set Plane} (hC : IsCompact C) (hCne : C.Nonempty) (p q : Plane) : supRadius C p ≤ supRadius C q + p.supDist q

r(p) ≤ r(q) + ‖p - q‖_∞.

theorem Schoenflies.abs_supRadius_sub_le {C : Set Plane} (hC : IsCompact C) (hCne : C.Nonempty) (p q : Plane) : |supRadius C p - supRadius C q| ≤ p.supDist q

The 1-Lipschitz property in its symmetric form.

The square of radius r(p) lies in the domain

theorem Schoenflies.openSquare_supRadius_subset_inside {C : Set Plane} {p : Plane} (hC : IsCompact C) (hCne : C.Nonempty) (hsep : IsSeparating C) (hp : p ∈ inside C) : p.openSquare (supRadius C p) ⊆ inside C

"The open axis-parallel square of radius r(p) centred at p lies in D." The square is convex, hence connected; it misses C because every one of its points is nearer to p than r(p); and it contains p. So it lies in the connected component of Cᶜ through p, which is inside C by thm:jordan.

The windows

windowRadius ε p is the blueprint's s_n(p) with ε_n a parameter: the recursion chooses the sequence, and nothing here needs to know that it is 2^{-n}.

noncomputable def Schoenflies.windowRadius (C : Set Plane) (ε : ℝ) (p : Plane) : ℝ

s_n(p) = r(p) - min(r(p)/2, ε_n).

Equations

• Schoenflies.windowRadius C ε p = Schoenflies.supRadius C p - min (Schoenflies.supRadius C p / 2) ε

noncomputable def Schoenflies.window (C : Set Plane) (ε : ℝ) (p : Plane) : Set Plane

W_n(p), the closed window.

Equations

• Schoenflies.window C ε p = p.closedSquare (Schoenflies.windowRadius C ε p)

noncomputable def Schoenflies.openWindow (C : Set Plane) (ε : ℝ) (p : Plane) : Set Plane

The interior of the window, which is where lem:grid-star-estimate places its point.

Equations

• Schoenflies.openWindow C ε p = p.openSquare (Schoenflies.windowRadius C ε p)

theorem Schoenflies.windowRadius_pos {C : Set Plane} {p : Plane} {ε : ℝ} (hC : IsCompact C) (hCne : C.Nonempty) (hp : p ∉ C) : 0 < windowRadius C ε p

0 < s_n(p).

theorem Schoenflies.windowRadius_lt_supRadius {C : Set Plane} {p : Plane} {ε : ℝ} (hC : IsCompact C) (hCne : C.Nonempty) (hp : p ∉ C) (hε : 0 < ε) : windowRadius C ε p < supRadius C p

s_n(p) < r(p).

theorem Schoenflies.sub_windowRadius_le (C : Set Plane) (ε : ℝ) (p : Plane) : supRadius C p - windowRadius C ε p ≤ ε

r(p) - s_n(p) ≤ ε_n.

theorem Schoenflies.le_windowRadius (C : Set Plane) (ε : ℝ) (p : Plane) : supRadius C p - ε ≤ windowRadius C ε p

The lower bound s_n(p) ≥ r(p) - ε_n, which is the form prop:shrinking-stars uses.

theorem Schoenflies.window_subset_inside {C : Set Plane} {p : Plane} {ε : ℝ} (hC : IsCompact C) (hCne : C.Nonempty) (hsep : IsSeparating C) (hp : p ∈ inside C) (hε : 0 < ε) : window C ε p ⊆ inside C

W_n(p) ⊆ D: the closed window sits strictly inside the square of radius r(p).

The arithmetic of prop:shrinking-stars

theorem Schoenflies.mem_openWindow_of_supDist_lt {C : Set Plane} {x b : Plane} {ε : ℝ} (hC : IsCompact C) (hCne : C.Nonempty) (hbx : b.supDist x < supRadius C x / 8) (hε : ε < supRadius C x / 8) : x ∈ openWindow C ε b

The window-catching estimate. If b is within d/8 of x in the ℓ^∞ metric and the mesh parameter ε is below d/8, where d = dist_∞(x, C), then x lies in the interior of the window W(b).

This is the displayed chain of the proof of prop:shrinking-stars: r(b) > 7d/8 by 1-Lipschitzness, hence s(b) ≥ r(b) - ε > 3d/4, and ‖b - x‖_∞ < d/8 < 3d/4.

The two sequences the recursion fixes

"Choose a sequence b_1, b_2, … in which every point of B occurs infinitely often, and put ε_n = 2^{-n}." Both are here, each with the one property prop:shrinking-stars uses: every value of the enumeration recurs at arbitrarily large indices, and the mesh sequence is null.

def Schoenflies.recur {α : Type u_1} (f : ℕ → α) (n : ℕ) : α

An enumeration in which every value of f occurs infinitely often. Cantor pairing, read off the first component: the value f k reappears at Nat.pair k m for every m.

Equations

• Schoenflies.recur f n = f (Nat.unpair n).1

theorem Schoenflies.exists_le_recur_eq {α : Type u_1} (f : ℕ → α) (k N : ℕ) : ∃ (n : ℕ), N ≤ n ∧ recur f n = f k

"The point b occurs at arbitrarily large indices." This is the step of prop:shrinking-stars that lets the mesh parameter be taken as small as the point requires: the window centre is fixed first, and only then is a late enough stage chosen.

theorem Schoenflies.tendsto_two_pow_neg : Filter.Tendsto (fun (n : ℕ) => (2 ^ n)⁻¹) Filter.atTop (nhds 0)

ε_n = 2^{-n} is a null sequence.

theorem Schoenflies.two_pow_neg_pos (n : ℕ) : 0 < (2 ^ n)⁻¹

theorem Schoenflies.exists_mem_rat_supDist_lt {U : Set Plane} {x : Plane} {δ : ℝ} {B : Set Plane} (hB : Dense B) (hU : IsOpen U) (hx : x ∈ U) (hδ : 0 < δ) : ∃ b ∈ B, b ∈ U ∧ b.supDist x < δ

The only property of B = ℚ² ∩ D that prop:shrinking-stars uses: an open set contains points of a dense subset of the plane as close to any of its points as asked.