Documentation

Mathlib.Topology.Connected.HausdorffMeasure

Connected sets and Hausdorff measure #

In this file we relate connectedness of a subset s of an extended metric space to its Hausdorff measure.

The key geometric idea is that the distance from a fixed base point is Lipschitz, so it does not increase Hausdorff measures, and the image of a preconnected set under this map is an interval whose one-dimensional Hausdorff measure equals its length. Comparing the two turns distances inside s into lower bounds for μH[1] s.

Main results #

TODO #

Prove that a preconnected and complete subset with finite one-dimensional Hausdorff measure is path connected and locally path connected. In fact, any two points in such a set can be connected by an injective geodesic with constant speed whose length is bounded above by the one-dimensional Hausdorff measure of this set.

source
theorem IsPreconnected.edist_ne_top {X : Type u_1} [EMetricSpace X] {s : Set X} {a b : X} (hs : IsPreconnected s) (ha : a ∈ s) (hb : b ∈ s) :
edist a b ≠ ⊤

In a preconnected subset of an extended metric space, any two points are at finite distance.

source
theorem IsPreconnected.subset_boundedComponent {X : Type u_1} [EMetricSpace X] {s : Set X} {a : X} (hs : IsPreconnected s) (ha : a ∈ s) :
s ⊆ Metric.boundedComponent a

A preconnected set lies in the bounded component of any of its points.

source
theorem lipschitzOnWith_toReal_edist {X : Type u_1} [EMetricSpace X] {s : Set X} {a : X} (hs : IsPreconnected s) (ha : a ∈ s) :
LipschitzOnWith 1 (fun (x : X) => (edist a x).toReal) s

The distance function x => (edist a x).toReal is Lipschitz on any preconnected set s that contains a.

source
theorem IsPreconnected.le_hausdorffMeasure_of_le_edist {X : Type u_1} [EMetricSpace X] {s : Set X} {a b : X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) (ha : a ∈ s) (hb : b ∈ s) {r : ENNReal} (hr : r ≤ edist a b) :
r ≤ (MeasureTheory.Measure.hausdorffMeasure 1) (s ∩ Metric.eball a r)

For any a, b in a preconnected set s and any r ≤ edist a b, the radius r is at most the one-dimensional Hausdorff measure of the part of s lying in the open ball of radius r around a. This lemma is needed in the proof of IsPreconnected.totallyBounded_of_hausdorffMeasure_lt_top.

source
theorem IsPreconnected.edist_le_hausdorffMeasure {X : Type u_1} [EMetricSpace X] {s : Set X} {a b : X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) (ha : a ∈ s) (hb : b ∈ s) :
edist a b ≤ (MeasureTheory.Measure.hausdorffMeasure 1) s

The distance between two points of a preconnected set s is at most the one-dimensional Hausdorff measure of s.

source
theorem IsPreconnected.ediam_le_hausdorffMeasure {X : Type u_1} [EMetricSpace X] {s : Set X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) :
Metric.ediam s ≤ (MeasureTheory.Measure.hausdorffMeasure 1) s

The extended diameter of a preconnected set is at most its one-dimensional Hausdorff measure.

source
theorem IsPreconnected.subsingleton_of_hausdorffMeasure_lt_top {X : Type u_1} [EMetricSpace X] {s : Set X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) {d : ℝ} (hd : d < 1) (hle : (MeasureTheory.Measure.hausdorffMeasure d) s < ⊤) :
s.Subsingleton

A preconnected set with finite d-dimensional Hausdorff measure for some d < 1 is a subsingleton.

source
theorem isTotallyDisconnected_of_hausdorffMeasure_lt_top {X : Type u_1} [EMetricSpace X] {s : Set X} [MeasurableSpace X] [BorelSpace X] {d : ℝ} (hd : d < 1) (hle : (MeasureTheory.Measure.hausdorffMeasure d) s < ⊤) :
IsTotallyDisconnected s

A set with finite d-dimensional Hausdorff measure for some d < 1 is totally disconnected.

source
theorem IsPreconnected.totallyBounded_of_hausdorffMeasure_lt_top {X : Type u_1} [EMetricSpace X] {s : Set X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) (hle : (MeasureTheory.Measure.hausdorffMeasure 1) s < ⊤) :
TotallyBounded s

A preconnected set with finite one-dimensional Hausdorff measure is totally bounded.

source
theorem IsPreconnected.isCompact_of_hausdorffMeasure_lt_top_isComplete {X : Type u_1} [EMetricSpace X] {s : Set X} [MeasurableSpace X] [BorelSpace X] (hs : IsPreconnected s) (hle : (MeasureTheory.Measure.hausdorffMeasure 1) s < ⊤) (hc : IsComplete s) :
IsCompact s