A bounded set is exactly as wide as its frontier

In a real normed space a bounded set V and its frontier have the same diameter: TauCeti.diam_frontier. One inequality is trivial, frontier V being contained in closure V. The other says that the frontier already realises every distance realised inside V, and it is the geometric content: a set cannot be wide and have a narrow boundary.

The mechanism is that a ray leaving a bounded set has to cross the frontier, and crossing it only later than it passes through a given point of the set. Precisely (TauCeti.exists_mem_frontier_dist_le), for x ∈ V and any base point y ≠ x the ray t ↦ y + t • (x - y), followed from t = 1 outwards, eventually leaves the bounded set V, and the segment it traces is connected, so IsPreconnected.inter_frontier_nonempty produces a frontier point p = y + t • (x - y) with t ≥ 1, whence dist y p = t * dist y x ≥ dist y x.

Applying this twice turns a pair of points of V into a pair of frontier points at least as far apart: first push x away from y to a frontier point p, then push y away from p to a frontier point q, and dist x y ≤ dist y p ≤ dist p q. Boundedness is essential and not merely a convenience of Metric.diam, which vanishes on unbounded sets: in ℝ the unbounded set Metric.ball 0 1 ∪ Set.Ici 2 has frontier {-1, 1, 2} of diameter 3.

Nothing here needs V to be open, connected, or measurable, and the ambient space is an arbitrary real normed space: only the segment and the norm are used.

The intended consumer is layer L5 of TauCetiRoadmap/ConformalMapping/README.md, Carathéodory's boundary correspondence. There the piece of a domain that a crosscut cuts off has to be shown small, and what is small is its boundary — the crosscut itself together with the arc of the domain boundary it separates; TauCeti.diam_frontier is what converts that into a bound on the piece. TauCeti/Analysis/Complex/Conformal/CutDiameter.lean carries out that conversion.

Main results

• TauCeti.exists_mem_frontier_dist_le — from a point of a bounded set, the ray away from any other base point reaches the frontier no sooner than it reaches that point.
• TauCeti.diam_le_diam_frontier and TauCeti.diam_frontier — a bounded set is exactly as wide as its frontier.
• TauCeti.diam_le_diam_of_frontier_subset — hence a bounded set is no wider than any bounded set containing its frontier, which is the form a boundary estimate is spent in.

theorem TauCeti.exists_mem_frontier_dist_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} {x y : E} (hV : Bornology.IsBounded V) (hx : x ∈ V) (hne : y ≠ x) : ∃ p ∈ frontier V, dist y x ≤ dist y p

A ray leaving a bounded set crosses its frontier, and does so no sooner than it passes through a given point of the set. For x in a bounded set V and any base point y ≠ x, the ray from y through x meets frontier V at a point p with dist y x ≤ dist y p.

The ray is followed from x outwards. It leaves V because V is bounded, the segment traced is connected, and IsPreconnected.inter_frontier_nonempty therefore hands back a frontier point on it; being beyond x on the ray, that point is at least as far from y as x is.

theorem TauCeti.diam_le_diam_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} (hV : Bornology.IsBounded V) : Metric.diam V ≤ Metric.diam (frontier V)

A bounded set is no wider than its frontier. Every distance realised between two points of a bounded set V is already realised between two points of frontier V: push the first point away from the second to the frontier, then the second away from the resulting frontier point.

theorem TauCeti.diam_frontier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V : Set E} (hV : Bornology.IsBounded V) : Metric.diam (frontier V) = Metric.diam V

The diameter of a bounded set is the diameter of its frontier. The frontier is contained in the closure, which gives one inequality, and TauCeti.diam_le_diam_frontier gives the other.

Boundedness cannot be dropped: Metric.diam is 0 on an unbounded set, while the frontier of Metric.ball 0 1 ∪ Set.Ici 2 in ℝ is {-1, 1, 2}.

theorem TauCeti.diam_le_diam_of_frontier_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {V W : Set E} (hV : Bornology.IsBounded V) (hW : Bornology.IsBounded W) (hVW : frontier V ⊆ W) : Metric.diam V ≤ Metric.diam W

A bounded set is no wider than anything bounded that contains its frontier. Enclosing frontier V in a bounded set W bounds diam V by diam W, since by TauCeti.diam_frontier the set and its frontier have the same diameter.

This is the form in which a boundary estimate is spent: what a geometric argument produces is a cover of the boundary of a piece — for a crosscut, the image of the cut together with the arc of the domain boundary it separates — and what is wanted is the width of the piece itself. Boundedness of W is what Metric.diam_mono needs and is not automatic from that of V, W being unconstrained apart from the inclusion.