Inversion in the unit circle, and the density of strongly accessible points

Two consequences of the Jordan curve theorem which have nothing to do with one another beyond becoming available at the same moment.

Inversion exchanges the two sides

Inversion about the unit circle centred at a,

I_a(x) = a + (x - a) / ‖x - a‖²,

is the device that turns the bounded Schönflies theorem into the unbounded one: it swaps the two sides of a Jordan curve C around any interior point a, sending the exterior of C onto the interior of C^a = I_a(C) punctured at a. So a closed-interior extension for C^a, pushed back through I_a, is a closed-exterior extension for C, which is prop:exterior-extension and the second half of thm:main.

The map is Mathlib's EuclideanGeometry.inversion a 1, repackaged here as Schoenflies.invert with the three facts the geometry needs: Schoenflies.dist_invert_center (‖I_a(x) - a‖ = 1/‖x - a‖), Schoenflies.invert_involutive, and continuity away from a. Schoenflies.invertHomeo bundles it as a self-homeomorphism of the punctured plane, which is the form the conjugation I_b ∘ f ∘ I_a of prop:exterior-extension will want.

The proof of lem:inversion-sides is the blueprint's. Put U = I_a(Ext C) ∪ {a}. It is

• open: away from a because I_a is a homeomorphism of the punctured plane, and at a because C ∪ Int(C) is bounded, so the complement of a large closed ball B(a, R) lies in Ext(C) and inverts onto B(a, 1/R) ∖ {a};
• bounded: a ball B(a, δ) lies in Int(C), so exterior points stay at distance ≥ δ from a and their inverses at distance ≤ 1/δ;
• connected: the continuous image of Ext(C), together with a, which is a limit of it because Ext(C) is unbounded;
• bounded by C^a: the third region I_a(Int(C) ∖ {a}) is open, so the frontier of U can only be C^a, and every point of C^a is in it because C = ∂Ext(C).

Being open, connected and with frontier disjoint from (C^a)ᶜ, U is a component of (C^a)ᶜ (Schoenflies.Plane.connectedComponentIn_eq_of_frontier_disjoint); being bounded, it is Int(C^a).

The closed-exterior extension

prop:exterior-extension is the short assembly that sits on top of it, stated parametrically over prop:pointed-extension. Schoenflies.PointedInteriorExtension is that interface, written out: the bounded theorem with a prescribed interior point. Schoenflies/Endgame.lean derives it from the closed-interior extension together with lem:square-point-mover, and Schoenflies/JordanSchoenflies.lean supplies the square-extension input.

The assembly needs a name for "restricts to a homeomorphism onto", since it composes four of them; Schoenflies.IsHomeoOn is that, in the unbundled Schoenflies.Plane.IsSquareMover style.

Density of strongly accessible points

lem:tangent-dense is three lines on top of thm:jordan and lem:nearest-strong: a point of C is a limit of points of the region because C is the region's frontier, and the nearest point of C to such a point is strongly accessible and no further from p than twice the distance we started with. It is stated here for either region, since nothing in the argument distinguishes them.

Everything below inherits the standing hypothesis of thm:jordan on main,

harc : ∀ A : Set Plane, IsArc A → IsConnected Aᶜ

threaded verbatim through every statement that consumes Schoenflies.IsJordanCurve.isSeparating. The two density statements, which are about an abstract IsSeparating curve, do not need it.

Blueprint

• Schoenflies.invert and its algebra — the map I_a of §"The closed exteriors".
• Schoenflies.invertHomeo — "I_a is an involutive homeomorphism of ℝ² ∖ {a}".
• Schoenflies.IsJordanCurve.invert_image — "C^a is a Jordan curve", the first sentence of the proof of lem:inversion-sides.
• Schoenflies.invert_image_outside, Schoenflies.invert_image_outside_union_singleton, Schoenflies.invert_image_inside_diff, Schoenflies.invert_image_union_outside, Schoenflies.inversion_sides — lem:inversion-sides.
• Schoenflies.exists_stronglyAccessible_dist_lt, Schoenflies.tangent_dense, Schoenflies.tangent_dense_inside — lem:tangent-dense.
• Schoenflies.PointedInteriorExtension — the prop:pointed-extension interface, discharged by Schoenflies.pointed_extension in Schoenflies/Endgame.lean.
• Schoenflies.exterior_extension — prop:exterior-extension, parametrically on that interface.
• Schoenflies.IsHomeoOn — no blueprint statement; the language "restricts to a homeomorphism of S onto T" that prop:exterior-extension is phrased in.

Inversion about the unit circle centred at a point

Schoenflies.invert a is EuclideanGeometry.inversion a 1, which Mathlib defines for every point including the centre, sending a to itself. That convention is what makes Schoenflies.invert_involutive hypothesis-free, and it costs nothing: every statement below that cares about the centre says so.

noncomputable def Schoenflies.invert (a x : Plane) : Plane

Inversion about the unit circle centred at a: I_a(x) = a + (x - a)/‖x - a‖², extended by I_a(a) = a so that it is an involution of the whole plane.

Equations

• Schoenflies.invert a x = EuclideanGeometry.inversion a 1 x

theorem Schoenflies.invert_apply (a x : Plane) : invert a x = a + (‖x - a‖ ^ 2)⁻¹ • (x - a)

@[simp]

theorem Schoenflies.invert_center (a : Plane) : invert a a = a

theorem Schoenflies.dist_invert_center (a x : Plane) : dist (invert a x) a = (dist x a)⁻¹

The defining metric identity: inversion inverts the distance to the centre.

theorem Schoenflies.invert_invert (a x : Plane) : invert a (invert a x) = x

theorem Schoenflies.invert_involutive (a : Plane) : Function.Involutive (invert a)

theorem Schoenflies.invert_injective (a : Plane) : Function.Injective (invert a)

theorem Schoenflies.invert_image_eq_preimage (a : Plane) (S : Set Plane) : invert a '' S = invert a ⁻¹' S

Being an involution, inversion has image and preimage the same operation. This is what makes openness of an image as cheap as openness of a preimage.

@[simp]

theorem Schoenflies.invert_image_invert_image (a : Plane) (S : Set Plane) : invert a '' invert a '' S = S

theorem Schoenflies.invert_eq_center_iff {a x : Plane} : invert a x = a ↔ x = a

theorem Schoenflies.invert_ne_center {a x : Plane} (h : x ≠ a) : invert a x ≠ a

theorem Schoenflies.continuousAt_invert {a x : Plane} (h : x ≠ a) : ContinuousAt (invert a) x

theorem Schoenflies.continuousOn_invert (a : Plane) : ContinuousOn (invert a) {a}ᶜ

theorem Schoenflies.isOpen_invert_image {a : Plane} {S : Set Plane} (hS : IsOpen S) (ha : a ∉ S) : IsOpen (invert a '' S)

An open set missing the centre has open image: on the punctured plane, which is itself open, inversion is a continuous involution, so the image is a preimage.

noncomputable def Schoenflies.invertHomeo (a : Plane) : ↑{a}ᶜ ≃ₜ ↑{a}ᶜ

"I_a is an involutive homeomorphism of ℝ² ∖ {a}", bundled. Its inverse is itself.

Equations

• One or more equations did not get rendered due to their size.

theorem Schoenflies.invertHomeo_apply (a : Plane) (z : ↑{a}ᶜ) : (invertHomeo a) z = ⟨invert a ↑z, ⋯⟩

The image of a Jordan curve

Inversion is a homeomorphism on a neighbourhood of a curve avoiding the centre, so it carries loops to loops.

theorem Schoenflies.IsJordanCurve.invert_image {C : Set Plane} {a : Plane} (hC : IsJordanCurve C) (ha : a ∉ C) : IsJordanCurve (invert a '' C)

The first sentence of the proof of lem:inversion-sides: C^a = I_a(C) is a Jordan curve.

Inversion exchanges the two sides

The whole of lem:inversion-sides. The proof is carried in one theorem, because every step speaks about the same set U = I_a(Ext C) ∪ {a}; the consequences that consumers want are peeled off afterwards.

theorem Schoenflies.exists_radius_compl_closedBall_subset_outside {C : Set Plane} (hC : IsSeparating C) (a : Plane) : ∃ R > 0, (Metric.closedBall a R)ᶜ ⊆ outside C

Everything beyond a large enough closed ball about any point is exterior to a separating curve: the curve and its interior together are bounded.

theorem Schoenflies.invert_image_outside_union_singleton {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : invert a '' outside C ∪ {a} = inside (invert a '' C)

lem:inversion-sides. For a interior to the Jordan curve C, the image of the exterior of C under inversion about a, together with the centre, is exactly the interior of C^a = I_a(C).

This is the form the proof produces; Schoenflies.invert_image_outside is the blueprint's statement, obtained by removing a from both sides.

theorem Schoenflies.notMem_invert_image {C : Set Plane} {a : Plane} (ha : a ∉ C) : a ∉ invert a '' C

The centre is never on C^a, since it is not on C.

theorem Schoenflies.invert_image_outside {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : invert a '' outside C = inside (invert a '' C) \ {a}

lem:inversion-sides, the blueprint's statement: I_a(Ext(C)) = Int(C^a) ∖ {a}.

theorem Schoenflies.invert_image_inside_diff {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : invert a '' (inside C \ {a}) = outside (invert a '' C)

The other half of the exchange: the punctured interior of C inverts onto the exterior of C^a. Not used by prop:exterior-extension, but it is what makes the name of the lemma true.

theorem Schoenflies.invert_image_union_outside {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : invert a '' (C ∪ outside C) = (invert a '' C ∪ inside (invert a '' C)) \ {a}

The closed-exterior form of lem:inversion-sides: inversion carries C ∪ Ext(C) onto (C^a ∪ Int(C^a)) ∖ {a}.

theorem Schoenflies.inversion_sides {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : IsJordanCurve (invert a '' C) ∧ invert a '' outside C = inside (invert a '' C) \ {a} ∧ invert a '' (C ∪ outside C) = (invert a '' C ∪ inside (invert a '' C)) \ {a} ∧ invert a '' ((invert a '' C ∪ inside (invert a '' C)) \ {a}) = C ∪ outside C ∧ Set.InjOn (invert a) (C ∪ outside C) ∧ ContinuousOn (invert a) (C ∪ outside C) ∧ ContinuousOn (invert a) ((invert a '' C ∪ inside (invert a '' C)) \ {a})

lem:inversion-sides, bundled. C^a is a Jordan curve, inversion carries the exterior of C onto the punctured interior of C^a, and it restricts to a homeomorphism from C ∪ Ext(C) onto (C^a ∪ Int(C^a)) ∖ {a}: it is injective and continuous on the source, its image is the target, and — being an involution — it is its own inverse there, continuous as well.

theorem Schoenflies.mem_inside_invert_image {C : Set Plane} {a : Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) (ha : a ∈ inside C) : a ∈ inside (invert a '' C)

The centre of the inversion is interior to the inverted curve.

Homeomorphisms between subsets of the plane

prop:exterior-extension is a composition of four restricted homeomorphisms, so it needs a name for "f restricts to a homeomorphism of S onto T". Schoenflies.IsHomeoOn is that name, written the way Schoenflies.Plane.IsSquareMover writes the same thing: unbundled, with the inverse named, so that composing two of them composes two honest functions Plane → Plane instead of producing a subtype-valued Homeomorph that must be unwrapped at every use.

This notion is general and belongs in a lower module. It is here because prop:exterior-extension is the first statement that needs it; the integrator should hoist it (and check that no concurrent branch introduced a twin).

structure Schoenflies.IsHomeoOn (f g : Plane → Plane) (S T : Set Plane) : Prop

IsHomeoOn f g S T: the maps f and g restrict to mutually inverse continuous bijections between S and T.

• mapsTo : Set.MapsTo f S T

  f carries S into T

• mapsTo_inv : Set.MapsTo g T S

  g carries T into S

• continuousOn : ContinuousOn f S

  f is continuous on S

• continuousOn_inv : ContinuousOn g T

  g is continuous on T

• invOn : Set.InvOn g f S T

  the two are mutually inverse there

theorem Schoenflies.IsHomeoOn.symm {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) : IsHomeoOn g f T S

theorem Schoenflies.IsHomeoOn.bijOn {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) : Set.BijOn f S T

theorem Schoenflies.IsHomeoOn.injOn {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) : Set.InjOn f S

theorem Schoenflies.IsHomeoOn.image_eq {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) : f '' S = T

theorem Schoenflies.IsHomeoOn.comp {f g f' g' : Plane → Plane} {S T U : Set Plane} (h : IsHomeoOn f g S T) (h' : IsHomeoOn f' g' T U) : IsHomeoOn (f' ∘ f) (g ∘ g') S U

Composing two restricted homeomorphisms.

theorem Schoenflies.IsHomeoOn.mono {f g : Plane → Plane} {S T S' T' : Set Plane} (h : IsHomeoOn f g S T) (hS : S' ⊆ S) (hT : T' ⊆ T) (hf : Set.MapsTo f S' T') (hg : Set.MapsTo g T' S') : IsHomeoOn f g S' T'

Restricting to a smaller pair of sets, once the two MapsTo clauses are known there.

theorem Schoenflies.IsHomeoOn.sdiff_singleton {f g : Plane → Plane} {S T : Set Plane} (h : IsHomeoOn f g S T) {u v : Plane} (hu : u ∈ S) (huv : f u = v) : IsHomeoOn f g (S \ {u}) (T \ {v})

Deleting a matched pair of points. This is the step "Φ* restricts to a homeomorphism after the two points a, b are removed" of prop:exterior-extension.

theorem Schoenflies.isHomeoOn_invert {a : Plane} {S : Set Plane} (ha : a ∉ S) : IsHomeoOn (invert a) (invert a) S (invert a '' S)

Inversion restricts to a homeomorphism of any set missing the centre onto its image.

The closed-exterior extension

prop:exterior-extension, assuming prop:pointed-extension. That is the blueprint's own citation, and it is the one statement of the endgame that is not yet available: it rests on thm:closed-interior-extension (open) together with lem:square-point-mover (Schoenflies.Plane.exists_squareMover, on main) and lem:jordan-circle (Schoenflies.IsJordanCurve.homeomorph, on main).

Everything that inversion contributes is here; discharging Schoenflies.PointedInteriorExtension finishes the exterior half of thm:main.

def Schoenflies.PointedInteriorExtension : Prop

prop:pointed-extension, as a hypothesis: a boundary homeomorphism between two Jordan curves extends to a homeomorphism of the closed interiors carrying one prescribed interior point to another.

This is not a restatement of prop:exterior-extension: it is about the two interiors, which is the bounded theorem, and it is what the blueprint proves from thm:closed-interior-extension and lem:square-point-mover.

Equations

• One or more equations did not get rendered due to their size.

theorem Schoenflies.exterior_extension (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hpt : PointedInteriorExtension) {C C' : Set Plane} {f g : Plane → Plane} (hC : IsJordanCurve C) (hC' : IsJordanCurve C') (hfg : IsHomeoOn f g C C') : ∃ (F : Plane → Plane) (G : Plane → Plane), IsHomeoOn F G (C ∪ outside C) (C' ∪ outside C') ∧ Set.EqOn F f C

prop:exterior-extension (closed-exterior extension). Every homeomorphism between two Jordan curves extends to a homeomorphism of their closed exteriors.

Assumes prop:pointed-extension (Schoenflies.PointedInteriorExtension) and the standing hypothesis harc of thm:jordan. The proof is the blueprint's: choose a ∈ Int(C) and b ∈ Int(C'), invert about each, extend the conjugated boundary map I_b ∘ f ∘ I_a over the interior of C^a so that a ↦ b, delete the two centres, and conjugate back — the deleted punctured closed interiors being exactly the closed exteriors, by lem:inversion-sides.

Density of strongly accessible points

lem:tangent-dense. Nothing here distinguishes the two regions, so the lemma is proved for either. The hypotheses are those of Schoenflies.stronglyAccessible_of_isMinOn: the region swallows the component of each of its points, and the curve is in its closure — which for a separating curve is C = ∂Ω.

theorem Schoenflies.exists_stronglyAccessible_dist_lt {C Ω : Set Plane} {p : Plane} {ε : ℝ} (hCcpt : IsCompact C) (hCne : C.Nonempty) (hΩC : Ω ⊆ Cᶜ) (hΩmax : ∀ q ∈ Ω, connectedComponentIn Cᶜ q ⊆ Ω) (hCΩ : C ⊆ closure Ω) (hp : p ∈ C) (hε : 0 < ε) : ∃ b ∈ C, StronglyAccessible Ω b ∧ dist b p < ε

The core estimate. If C is compact and every point of C is a limit of points of Ω, and Ω swallows the component in Cᶜ of each of its points, then near any p ∈ C there is a strongly accessible point of C: pick q ∈ Ω within ε/2 of p, and take the point of C nearest to q; it is strongly accessible by lem:nearest-strong and within 2‖q - p‖ of p.

theorem Schoenflies.tangent_dense {C Ω : Set Plane} (hC : IsSeparating C) (hΩ : IsRegionOf C Ω) : C ⊆ closure {b : Plane | b ∈ C ∧ StronglyAccessible Ω b}

lem:tangent-dense (density of strongly accessible points), for either region of a separating Jordan curve: the points of C strongly accessible from Ω are dense in C.

theorem Schoenflies.tangent_dense_inside {C : Set Plane} (hC : IsSeparating C) : C ⊆ closure {b : Plane | b ∈ C ∧ StronglyAccessible (inside C) b}

lem:tangent-dense in the blueprint's own setting, D = Int(C).

theorem Schoenflies.IsJordanCurve.tangent_dense {C : Set Plane} (harc : ∀ (A : Set Plane), IsArc A → IsConnected Aᶜ) (hC : IsJordanCurve C) : C ⊆ closure {b : Plane | b ∈ C ∧ StronglyAccessible (inside C) b}

lem:tangent-dense for a Jordan curve, threading the standing hypothesis of thm:jordan.