Boundedness and diameter of filled hulls

The filled hull TauCeti.filledHull K is K together with the bounded connected components of its complement. Its topological API is in TauCeti/Topology/FilledHull.lean. In a real seminormed space, filling preserves boundedness and diameter: for nonempty K, the filled hull lies in closedConvexHull ℝ K, which has the same diameter as K.

The containment uses the geometric Hahn–Banach separation theorem (geometric_hahn_banach_point_closed). A point outside the closed convex hull lies in an open half-space disjoint from K. This half-space is preconnected and unbounded, so the point's component in Kᶜ is unbounded. In a seminormed space, the continuous separating functional sends bounded sets to bounded sets, while its image of this half-space contains every real number below the separating level.

Nonemptiness is essential for the convex-hull containment: with the zero seminorm, the filled hull of ∅ is the whole space, whereas its convex hull is empty. The diameter results need no nonemptiness assumption because the empty hull lies in a radius-zero ball. As usual for Metric.diam, an unbounded set has diameter 0.

These bounds apply to sets enclosed by a boundary: IsPreconnected.subset_filledHull places a preconnected set disjoint from K inside the filled hull as soon as it meets it. Thus a preconnected set cut off from infinity by a bounded K has diameter at most diam K, without regularity assumptions on K. The related frontier bound in TauCeti/Analysis/Normed/Module/DiamFrontier.lean requires the whole frontier to lie in K; TauCeti.subset_filledHull_of_frontier_subset connects the two forms of enclosure.

Main results

• TauCeti.filledHull_sphere — filling a sphere gives the closed ball.
• TauCeti.filledHull_subset_closedConvexHull — the filled hull of a nonempty set lies in its closed convex hull.
• TauCeti.isBounded_filledHull and TauCeti.diam_filledHull — filling preserves boundedness and diameter.
• TauCeti.diam_le_diam_of_subset_filledHull and IsPreconnected.diam_le_diam_of_disjoint — sets enclosed by a bounded K are no wider than K.
• TauCeti.filledHull_empty — the empty hull is empty in a nontrivial real normed space.
• TauCeti.connectedComponentIn_compl_eq_of_unbounded_component — the unbounded complementary component of a bounded set is unique in dimension at least two.
• TauCeti.mem_filledHull_or_mem_filledHull_of_notMem_connectedComponentIn — of two points in different complementary components, at least one lies in the filled hull, in dimension at least two.

@[simp]

theorem TauCeti.filledHull_sphere {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ} (hr : 0 ≤ r) : filledHull (Metric.sphere x r) = Metric.closedBall x r

The filled hull of a sphere of nonnegative radius is the closed ball. No nontriviality or separation assumption is needed: when the seminorm vanishes identically, both sides are the whole space.

theorem TauCeti.filledHull_subset_closedConvexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} (hK : K.Nonempty) : filledHull K ⊆ (closedConvexHull ℝ) K

The filled hull of a nonempty set lies in its closed convex hull. Nonemptiness is essential: with the zero seminorm, filledHull ∅ = univ, while closedConvexHull ℝ ∅ = ∅.

@[simp]

theorem TauCeti.isBounded_filledHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} : Bornology.IsBounded (filledHull K) ↔ Bornology.IsBounded K

A filled hull is bounded exactly when the set filled is.

@[simp]

theorem TauCeti.diam_filledHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} : Metric.diam (filledHull K) = Metric.diam K

Filling preserves the diameter, including for empty and unbounded sets.

theorem TauCeti.diam_le_diam_of_subset_filledHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K S : Set E} (hK : Bornology.IsBounded K) (h : S ⊆ filledHull K) : Metric.diam S ≤ Metric.diam K

A set inside the filled hull of a bounded K has diameter at most diam K.

theorem IsPreconnected.diam_le_diam_of_disjoint {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {K S : Set E} (hS : IsPreconnected S) (hSK : Disjoint S K) (hne : (S ∩ TauCeti.filledHull K).Nonempty) (hK : Bornology.IsBounded K) : Metric.diam S ≤ Metric.diam K

A preconnected set disjoint from a bounded K that meets its filled hull has diameter at most diam K. No regularity is required of K.

@[simp]

theorem TauCeti.filledHull_empty {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] : filledHull ∅ = ∅

The filled hull of the empty set is empty in a nontrivial real normed space. This does not extend to seminormed spaces with identically zero seminorm.

theorem TauCeti.connectedComponentIn_compl_eq_of_unbounded_component {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {x y : E} (h : 1 < Module.rank ℝ E) (hK : Bornology.IsBounded K) (hx : ¬Bornology.IsBounded (connectedComponentIn Kᶜ x)) (hy : ¬Bornology.IsBounded (connectedComponentIn Kᶜ y)) : connectedComponentIn Kᶜ x = connectedComponentIn Kᶜ y

The unbounded component of the complement of a bounded set is unique in a real normed space of dimension at least two.

theorem TauCeti.mem_filledHull_or_mem_filledHull_of_notMem_connectedComponentIn {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : Set E} {x y : E} (h : 1 < Module.rank ℝ E) (hK : Bornology.IsBounded K) (hxy : y ∉ connectedComponentIn Kᶜ x) : x ∈ filledHull K ∨ y ∈ filledHull K

Two points in different components of the complement of a bounded set cannot both lie outside the filled hull in a real normed space of dimension at least two.