Surgery on continua

This file develops the continuum-surgery argument for countably many open convex holes.

theorem IsCompact.exists_edist_eq_ediam {X : Type u_1} [MetricSpace X] {C : Set X} (hC : IsCompact C) (hCne : C.Nonempty) : ∃ x ∈ C, ∃ y ∈ C, edist x y = Metric.ediam C

A nonempty compact set in a metric space contains two points realizing its extended diameter.

def LeanPool.Besicovitch.brokenSegment (a c b : EuclideanSpace ℝ (Fin 2)) : Set (EuclideanSpace ℝ (Fin 2))

The two-segment bridge through an interior point of a convex hole.

Equations

• LeanPool.Besicovitch.brokenSegment a c b = segment ℝ a c ∪ segment ℝ c b

def LeanPool.Besicovitch.IsOneHoleSurgery (K U : Set (EuclideanSpace ℝ (Fin 2))) (x y : EuclideanSpace ℝ (Fin 2)) (epsilon : ℝ) (D bridge : Set (EuclideanSpace ℝ (Fin 2))) : Prop

A one-hole surgery preserves a continuum's diameter and changes it only inside the hole.

Equations

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

theorem LeanPool.Besicovitch.exists_oneHoleSurgery {K U : Set (EuclideanSpace ℝ (Fin 2))} (hKcompact : IsCompact K) (hKconnected : IsConnected K) {x y : EuclideanSpace ℝ (Fin 2)} (hxK : x ∈ K) (hyK : y ∈ K) (hxy : edist x y = Metric.ediam K) (hUopen : IsOpen U) (hUconvex : Convex ℝ U) (hUbounded : Bornology.IsBounded U) (hUdiam : Metric.ediam U < Metric.ediam K) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (D : Set (EuclideanSpace ℝ (Fin 2))) (bridge : Set (EuclideanSpace ℝ (Fin 2))), IsOneHoleSurgery K U x y epsilon D bridge

A continuum can be surgically changed inside one open convex hole while preserving a diameter-realizing pair. The bridge inserted in the hole has length at most the hole diameter, up to an arbitrarily small error.

theorem LeanPool.Besicovitch.exists_continuum_surgery {C : Set (EuclideanSpace ℝ (Fin 2))} (hCcompact : IsCompact C) (hCconnected : IsConnected C) {x y : EuclideanSpace ℝ (Fin 2)} (hxC : x ∈ C) (hyC : y ∈ C) (hxy : edist x y = Metric.ediam C) (U : ℕ → Set (EuclideanSpace ℝ (Fin 2))) (hUopen : ∀ (i : ℕ), IsOpen (U i)) (hUconvex : ∀ (i : ℕ), Convex ℝ (U i)) (hUbounded : ∀ (i : ℕ), Bornology.IsBounded (U i)) (hUdisjoint : Pairwise fun (i j : ℕ) => Disjoint (U i) (U j)) (hsum : ∑' (i : ℕ), Metric.ediam (U i) < Metric.ediam C) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (D : Set (EuclideanSpace ℝ (Fin 2))), IsCompact D ∧ IsConnected D ∧ x ∈ D ∧ y ∈ D ∧ Metric.ediam D = Metric.ediam C ∧ D ⊆ (convexHull ℝ) C ∧ D \ ⋃ (i : ℕ), U i ⊆ C \ ⋃ (i : ℕ), U i ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (D ∩ ⋃ (i : ℕ), U i) ≤ ∑' (i : ℕ), Metric.ediam (U i) + ENNReal.ofReal epsilon ∧ (MeasureTheory.Measure.hausdorffMeasure 1) D ≤ (MeasureTheory.Measure.hausdorffMeasure 1) C + ∑' (i : ℕ), Metric.ediam (U i) + ENNReal.ofReal epsilon

Countably many disjoint open convex holes can be bypassed without changing a diameter-realizing pair, at a total length cost bounded by their diameters.

theorem LeanPool.Besicovitch.exists_continuum_surgery_countable {iota : Type u_1} [Countable iota] {C : Set (EuclideanSpace ℝ (Fin 2))} (hCcompact : IsCompact C) (hCconnected : IsConnected C) {x y : EuclideanSpace ℝ (Fin 2)} (hxC : x ∈ C) (hyC : y ∈ C) (hxy : edist x y = Metric.ediam C) (U : iota → Set (EuclideanSpace ℝ (Fin 2))) (hUopen : ∀ (i : iota), IsOpen (U i)) (hUconvex : ∀ (i : iota), Convex ℝ (U i)) (hUbounded : ∀ (i : iota), Bornology.IsBounded (U i)) (hUdisjoint : Pairwise fun (i j : iota) => Disjoint (U i) (U j)) (hsum : ∑' (i : iota), Metric.ediam (U i) < Metric.ediam C) {epsilon : ℝ} (hepsilon : 0 < epsilon) : ∃ (D : Set (EuclideanSpace ℝ (Fin 2))), IsCompact D ∧ IsConnected D ∧ x ∈ D ∧ y ∈ D ∧ Metric.ediam D = Metric.ediam C ∧ D ⊆ (convexHull ℝ) C ∧ D \ ⋃ (i : iota), U i ⊆ C \ ⋃ (i : iota), U i ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (D ∩ ⋃ (i : iota), U i) ≤ ∑' (i : iota), Metric.ediam (U i) + ENNReal.ofReal epsilon ∧ (MeasureTheory.Measure.hausdorffMeasure 1) D ≤ (MeasureTheory.Measure.hausdorffMeasure 1) C + ∑' (i : iota), Metric.ediam (U i) + ENNReal.ofReal epsilon

The continuum-surgery theorem for a countable index type.

theorem LeanPool.Besicovitch.exists_pairwiseDisjoint_convex_hole_cover_countable {iota : Type u_1} [Countable iota] (U : iota → Set (EuclideanSpace ℝ (Fin 2))) (hUopen : ∀ (i : iota), IsOpen (U i)) (hsum : ∑' (i : iota), Metric.ediam (U i) ≠ ⊤) : ∃ (W : Set (Set (EuclideanSpace ℝ (Fin 2)))), W.Countable ∧ W.PairwiseDisjoint id ∧ (∀ (V : ↑W), IsOpen ↑V ∧ Convex ℝ ↑V ∧ Bornology.IsBounded ↑V) ∧ ⋃ (i : iota), U i ⊆ ⋃ (V : ↑W), ↑V ∧ ∑' (V : ↑W), Metric.ediam ↑V ≤ ∑' (i : iota), Metric.ediam (U i)

A countable family of open holes has a pairwise-disjoint open convex enlargement whose total diameter is no larger.

theorem LeanPool.Besicovitch.exists_continuum_surgery_open_holes {iota : Type u_1} [Countable iota] {C : Set (EuclideanSpace ℝ (Fin 2))} (hCcompact : IsCompact C) (hCconnected : IsConnected C) {x y : EuclideanSpace ℝ (Fin 2)} (hxC : x ∈ C) (hyC : y ∈ C) (hxy : edist x y = Metric.ediam C) (U : iota → Set (EuclideanSpace ℝ (Fin 2))) (hUopen : ∀ (i : iota), IsOpen (U i)) (hsum : ∑' (i : iota), Metric.ediam (U i) < Metric.ediam C) : ∃ (D : Set (EuclideanSpace ℝ (Fin 2))), IsCompact D ∧ IsConnected D ∧ x ∈ D ∧ y ∈ D ∧ Metric.ediam D = Metric.ediam C ∧ D ⊆ (convexHull ℝ) C ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (D \ (C \ ⋃ (i : iota), U i)) < Metric.ediam C ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (D ∩ ⋃ (i : iota), U i) < Metric.ediam C ∧ (MeasureTheory.Measure.hausdorffMeasure 1) D ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (C \ ⋃ (i : iota), U i) + Metric.ediam C

Surgery for arbitrary countably many open holes. The part not inherited from the old continuum outside the holes has measure strictly smaller than the preserved diameter.