Cutting a set by a sphere

Removing the sphere sphere x ρ from a set s leaves two pieces: the near side s ∩ ball x ρ, of the points of s closer to x than ρ, and the far side s \ closedBall x ρ, of those further away. This file records that they cover s \ sphere x ρ, that they are disjoint, that the two sides together with the cut cover all of s (also after applying an arbitrary map), and — when s is open, so that both sides are open — that a preconnected subset of s missing the sphere lies entirely in one of them.

Nothing beyond the containments ball x ρ ⊆ closedBall x ρ and sphere x ρ ⊆ closedBall x ρ, and the openness of a ball against the closedness of a closed ball, is used, so s is an arbitrary set in an arbitrary pseudo-metric space.

The one quantitative statement is about shrinking the cut. When the cut point x lies off s, the far side keeps two prescribed points of s once ρ is small enough, so the image of the far side stays at least as wide as the distance between their two distinct images: the far side does not degenerate as the cut shrinks. Distinctness of those two images is what forces a genuine metric, rather than pseudo-metric, structure on both sides, and that statement alone is stated for one.

The intended consumer is layer L5 of TauCetiRoadmap/ConformalMapping/README.md, Carathéodory's boundary correspondence, through TauCeti/Analysis/Complex/Conformal/Crosscut/Basic.lean and TauCeti/Analysis/Complex/Conformal/CutDiameter.lean: there X = ℂ and the sphere is the circular crosscut of a plane domain at a boundary point, whose near side is the approach region along which the boundary behaviour of a conformal map is read off. Nothing here is specific to that use, and Mathlib has no form of the decomposition.

Main results

• TauCeti.sdiff_sphere_eq_inter_ball_union_sdiff_closedBall — the two sides cover the cut set.
• TauCeti.disjoint_inter_ball_sdiff_closedBall — the two sides are disjoint, and TauCeti.disjoint_inter_ball_inter_sphere, TauCeti.disjoint_sdiff_closedBall_inter_sphere — each of them is disjoint from the cut.
• TauCeti.eq_inter_ball_union_sdiff_closedBall_union_inter_sphere — the two sides and the cut cover the whole set, and TauCeti.image_eq_image_inter_ball_union_image_sdiff_closedBall_union_image_inter_sphere is its image under an arbitrary map.
• TauCeti.subset_inter_ball_or_subset_sdiff_closedBall — a preconnected subset of an open cut set missing the sphere lies on one side of it.
• TauCeti.exists_pos_forall_le_diam_image_sdiff_closedBall — cutting at a point off the set, the image of the far side stays at least as wide as a fixed positive number for every small enough radius.

theorem TauCeti.sdiff_sphere_eq_inter_ball_union_sdiff_closedBall {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s : Set X} : s \ Metric.sphere x ρ = s ∩ Metric.ball x ρ ∪ s \ Metric.closedBall x ρ

A circular cut splits a set into a near side and a far side. Removing the sphere sphere x ρ from a set s leaves the points of s at distance less than ρ from x together with those at distance more than ρ.

theorem TauCeti.disjoint_inter_ball_sdiff_closedBall {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s : Set X} : Disjoint (s ∩ Metric.ball x ρ) (s \ Metric.closedBall x ρ)

The two sides of a circular cut are disjoint, the near side lying inside closedBall x ρ and the far side outside it.

theorem TauCeti.disjoint_inter_ball_inter_sphere {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s : Set X} : Disjoint (s ∩ Metric.ball x ρ) (s ∩ Metric.sphere x ρ)

The near side of a circular cut misses the cut itself, the ball and the sphere being disjoint.

theorem TauCeti.disjoint_sdiff_closedBall_inter_sphere {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s : Set X} : Disjoint (s \ Metric.closedBall x ρ) (s ∩ Metric.sphere x ρ)

The far side of a circular cut misses the cut itself, the sphere lying in the closed ball.

theorem TauCeti.eq_inter_ball_union_sdiff_closedBall_union_inter_sphere {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s : Set X} : s = s ∩ Metric.ball x ρ ∪ s \ Metric.closedBall x ρ ∪ s ∩ Metric.sphere x ρ

A circular cut splits a set into a near side, a far side and the cut. The three-piece form of TauCeti.sdiff_sphere_eq_inter_ball_union_sdiff_closedBall.

theorem TauCeti.image_eq_image_inter_ball_union_image_sdiff_closedBall_union_image_inter_sphere {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {Y : Type u_2} (f : X → Y) {s : Set X} : f '' s = f '' (s ∩ Metric.ball x ρ) ∪ f '' (s \ Metric.closedBall x ρ) ∪ f '' (s ∩ Metric.sphere x ρ)

The image of a circular cut is the union of the images of its two sides and the cut. This is the image form of TauCeti.eq_inter_ball_union_sdiff_closedBall_union_inter_sphere; the target of f carries no structure.

theorem TauCeti.subset_inter_ball_or_subset_sdiff_closedBall {X : Type u_1} [PseudoMetricSpace X] {x : X} {ρ : ℝ} {s S : Set X} (hs : IsOpen s) (hS : IsPreconnected S) (hSsub : S ⊆ s \ Metric.sphere x ρ) : S ⊆ s ∩ Metric.ball x ρ ∨ S ⊆ s \ Metric.closedBall x ρ

A connected subset of an open set missing a circular cut lies on one side of it. This is the separation statement the decomposition exists for: the two sides are open and disjoint, so a preconnected subset of their union cannot meet both. Only openness of the cut set is used.

The far side does not degenerate

theorem TauCeti.exists_pos_forall_le_diam_image_sdiff_closedBall {X : Type u_2} {Y : Type u_3} [MetricSpace X] [MetricSpace Y] {f : X → Y} {s : Set X} {x : X} (hfs : ¬(f '' s).Subsingleton) (hx : x ∉ s) (hb : Bornology.IsBounded (f '' s)) : ∃ d > 0, ∃ ρ₀ > 0, ∀ ρ ≤ ρ₀, d ≤ Metric.diam (f '' (s \ Metric.closedBall x ρ))

Cutting at a point off the set, the far side keeps a fixed width as the cut shrinks. Let the image of s under f have at least two points, let x lie off s, and suppose the image is bounded. Then there are d > 0 and ρ₀ > 0 such that

d ≤ diam (f '' (s \ closedBall x ρ)) for every ρ ≤ ρ₀.

No hypothesis relates f to the metric of X.