Hausdorff measure and metric (outer) measures

In this file we define the d-dimensional Hausdorff measure on an (extended) metric space X and the Hausdorff dimension of a set in an (extended) metric space. Let μ d δ be the maximal outer measure such that μ d δ s ≤ (EMetric.diam s) ^ d for every set of diameter less than δ. Then the Hausdorff measure μH[d] s of s is defined as ⨆ δ > 0, μ d δ s. By Caratheodory theorem MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, this is a Borel measure on X.

The value of μH[d], d > 0, on a set s (measurable or not) is given by

μH[d] s = ⨆ (r : ℝ≥0∞) (hr : 0 < r), ⨅ (t : ℕ → Set X) (hts : s ⊆ ⋃ n, t n) (ht : ∀ n, EMetric.diam (t n) ≤ r), ∑' n, EMetric.diam (t n) ^ d 

For every set s for any d < d' we have either μH[d] s = ∞ or μH[d'] s = 0, see MeasureTheory.Measure.hausdorffMeasure_zero_or_top. In Mathlib/Topology/MetricSpace/HausdorffDimension.lean we use this fact to define the Hausdorff dimension dimH of a set in an (extended) metric space.

We also define two generalizations of the Hausdorff measure. In one generalization (see MeasureTheory.Measure.mkMetric) we take any function m (diam s) instead of (diam s) ^ d. In an even more general definition (see MeasureTheory.Measure.mkMetric') we use any function of m : Set X → ℝ≥0∞. Some authors start with a partial function m defined only on some sets s : Set X (e.g., only on balls or only on measurable sets). This is equivalent to our definition applied to MeasureTheory.extend m.

We also define a predicate MeasureTheory.OuterMeasure.IsMetric which says that an outer measure is additive on metric separated pairs of sets: μ (s ∪ t) = μ s + μ t provided that ⨅ (x ∈ s) (y ∈ t), edist x y ≠ 0. This is the property required for the Caratheodory theorem MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory, so we prove this theorem for any metric outer measure, then prove that outer measures constructed using mkMetric' are metric outer measures.

Main definitions

• MeasureTheory.OuterMeasure.IsMetric: an outer measure μ is called metric if μ (s ∪ t) = μ s + μ t for any two metric separated sets s and t. A metric outer measure in a Borel extended metric space is guaranteed to satisfy the Caratheodory condition, see MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory.
• MeasureTheory.OuterMeasure.mkMetric' and its particular case MeasureTheory.OuterMeasure.mkMetric: a construction of an outer measure that is guaranteed to be metric. Both constructions are generalizations of the Hausdorff measure. The same measures interpreted as Borel measures are called MeasureTheory.Measure.mkMetric' and MeasureTheory.Measure.mkMetric.
• MeasureTheory.Measure.hausdorffMeasure a.k.a. μH[d]: the d-dimensional Hausdorff measure. There are many definitions of the Hausdorff measure that differ from each other by a multiplicative constant. We put μH[d] s = ⨆ r > 0, ⨅ (t : ℕ → Set X) (hts : s ⊆ ⋃ n, t n) (ht : ∀ n, EMetric.diam (t n) ≤ r), ∑' n, ⨆ (ht : ¬Set.Subsingleton (t n)), (EMetric.diam (t n)) ^ d, see MeasureTheory.Measure.hausdorffMeasure_apply. In the most interesting case 0 < d one can omit the ⨆ (ht : ¬Set.Subsingleton (t n)) part.

Main statements

Basic properties

• MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory: if μ is a metric outer measure on an extended metric space X (that is, it is additive on pairs of metric separated sets), then every Borel set is Caratheodory measurable (hence, μ defines an actual MeasureTheory.Measure). See also MeasureTheory.Measure.mkMetric.
• MeasureTheory.Measure.hausdorffMeasure_mono: μH[d] s is an antitone function of d.
• MeasureTheory.Measure.hausdorffMeasure_zero_or_top: if d₁ < d₂, then for any s, either μH[d₂] s = 0 or μH[d₁] s = ∞. Together with the previous lemma, this means that μH[d] s is equal to infinity on some ray (-∞, D) and is equal to zero on (D, +∞), where D is a possibly infinite number called the Hausdorff dimension of s; μH[D] s can be zero, infinity, or anything in between.
• MeasureTheory.Measure.noAtoms_hausdorff: Hausdorff measure has no atoms.

Hausdorff measure in ℝⁿ

• MeasureTheory.hausdorffMeasure_pi_real: for a nonempty ι, μH[card ι] on ι → ℝ equals Lebesgue measure.

Notation

We use the following notation localized in MeasureTheory.

• μH[d] : MeasureTheory.Measure.hausdorffMeasure d

Implementation notes

There are a few similar constructions called the d-dimensional Hausdorff measure. E.g., some sources only allow coverings by balls and use r ^ d instead of (diam s) ^ d. While these construction lead to different Hausdorff measures, they lead to the same notion of the Hausdorff dimension.

References

• Herbert Federer, Geometric Measure Theory, Chapter 2.10

Tags

Hausdorff measure, measure, metric measure

Metric outer measures

In this section we define metric outer measures and prove Caratheodory theorem: a metric outer measure has the Caratheodory property.

def MeasureTheory.OuterMeasure.IsMetric {X : Type u_2} [EMetricSpace X] (μ : OuterMeasure X) : Prop

We say that an outer measure μ in an (e)metric space is metric if μ (s ∪ t) = μ s + μ t for any two metric separated sets s, t.

Equations

• μ.IsMetric = ∀ (s t : Set X), Metric.AreSeparated s t → μ (s ∪ t) = μ s + μ t

theorem MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {μ : OuterMeasure X} (hm : μ.IsMetric) {I : Finset ι} {s : ι → Set X} (hI : ∀ i ∈ I, ∀ j ∈ I, i ≠ j → Metric.AreSeparated (s i) (s j)) : μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)

A metric outer measure is additive on a finite set of pairwise metric separated sets.

theorem MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory {X : Type u_2} [EMetricSpace X] {μ : OuterMeasure X} (hm : μ.IsMetric) : borel X ≤ μ.caratheodory

Caratheodory theorem. If m is a metric outer measure, then every Borel measurable set t is Caratheodory measurable: for any (not necessarily measurable) set s we have μ (s ∩ t) + μ (s \ t) = μ s.

theorem MeasureTheory.OuterMeasure.IsMetric.le_caratheodory {X : Type u_2} [EMetricSpace X] {μ : OuterMeasure X} [MeasurableSpace X] [BorelSpace X] (hm : μ.IsMetric) : inst✝ ≤ μ.caratheodory

Constructors of metric outer measures

In this section we provide constructors MeasureTheory.OuterMeasure.mkMetric' and MeasureTheory.OuterMeasure.mkMetric and prove that these outer measures are metric outer measures. We also prove basic lemmas about map/comap of these measures.

def MeasureTheory.OuterMeasure.mkMetric'.pre {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) (r : ENNReal) : OuterMeasure X

Auxiliary definition for OuterMeasure.mkMetric': given a function on sets m : Set X → ℝ≥0∞, returns the maximal outer measure μ such that μ s ≤ m s for any set s of diameter at most r.

Equations

• MeasureTheory.OuterMeasure.mkMetric'.pre m r = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.extend fun (s : Set X) (x : EMetric.diam s ≤ r) => m s)

def MeasureTheory.OuterMeasure.mkMetric' {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) : OuterMeasure X

Given a function m : Set X → ℝ≥0∞, mkMetric' m is the supremum of mkMetric'.pre m r over r > 0. Equivalently, it is the limit of mkMetric'.pre m r as r tends to zero from the right.

Equations

• MeasureTheory.OuterMeasure.mkMetric' m = ⨆ (r : ENNReal), ⨆ (_ : r > 0), MeasureTheory.OuterMeasure.mkMetric'.pre m r

def MeasureTheory.OuterMeasure.mkMetric {X : Type u_2} [EMetricSpace X] (m : ENNReal → ENNReal) : OuterMeasure X

Given a function m : ℝ≥0∞ → ℝ≥0∞ and r > 0, let μ r be the maximal outer measure such that μ s ≤ m (EMetric.diam s) whenever EMetric.diam s < r. Then mkMetric m = ⨆ r > 0, μ r.

Equations

• MeasureTheory.OuterMeasure.mkMetric m = MeasureTheory.OuterMeasure.mkMetric' fun (s : Set X) => m (EMetric.diam s)

theorem MeasureTheory.OuterMeasure.mkMetric'.le_pre {X : Type u_2} [EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {μ : OuterMeasure X} : μ ≤ pre m r ↔ ∀ (s : Set X), EMetric.diam s ≤ r → μ s ≤ m s

theorem MeasureTheory.OuterMeasure.mkMetric'.pre_le {X : Type u_2} [EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {s : Set X} (hs : EMetric.diam s ≤ r) : (pre m r) s ≤ m s

theorem MeasureTheory.OuterMeasure.mkMetric'.mono_pre {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) {r r' : ENNReal} (h : r ≤ r') : pre m r' ≤ pre m r

theorem MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) : Monotone fun (k : ℕ) => pre m (↑k)⁻¹

theorem MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) (s : Set X) : Filter.Tendsto (fun (r : ENNReal) => (pre m r) s) (nhdsWithin 0 (Set.Ioi 0)) (nhds ((mkMetric' m) s))

theorem MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) (s : Set X) : Filter.Tendsto (fun (n : ℕ) => (pre m (↑n)⁻¹) s) Filter.atTop (nhds ((mkMetric' m) s))

theorem MeasureTheory.OuterMeasure.mkMetric'.eq_iSup_nat {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) : mkMetric' m = ⨆ (n : ℕ), pre m (↑n)⁻¹

theorem MeasureTheory.OuterMeasure.mkMetric'.trim_pre {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (m : Set X → ENNReal) (hcl : ∀ (s : Set X), m (closure s) = m s) (r : ENNReal) : (pre m r).trim = pre m r

MeasureTheory.OuterMeasure.mkMetric'.pre m r is a trimmed measure provided that m (closure s) = m s for any set s.

theorem MeasureTheory.OuterMeasure.mkMetric'_isMetric {X : Type u_2} [EMetricSpace X] (m : Set X → ENNReal) : (mkMetric' m).IsMetric

An outer measure constructed using OuterMeasure.mkMetric' is a metric outer measure.

theorem MeasureTheory.OuterMeasure.mkMetric_mono_smul {X : Type u_2} [EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) (h0 : c ≠ 0) (hle : m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] c • m₂) : mkMetric m₁ ≤ c • mkMetric m₂

If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 0] to state this), then mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂.

@[simp]

theorem MeasureTheory.OuterMeasure.mkMetric_top {X : Type u_2} [EMetricSpace X] : (mkMetric fun (x : ENNReal) => ⊤) = ⊤

theorem MeasureTheory.OuterMeasure.mkMetric_mono {X : Type u_2} [EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal} (hle : m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] m₂) : mkMetric m₁ ≤ mkMetric m₂

If m₁ d ≤ m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 0] to state this), then mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂.

theorem MeasureTheory.OuterMeasure.isometry_comap_mkMetric {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (m : ENNReal → ENNReal) {f : X → Y} (hf : Isometry f) (H : Monotone m ∨ Function.Surjective f) : (comap f) (mkMetric m) = mkMetric m

theorem MeasureTheory.OuterMeasure.mkMetric_smul {X : Type u_2} [EMetricSpace X] (m : ENNReal → ENNReal) {c : ENNReal} (hc : c ≠ ⊤) (hc' : c ≠ 0) : mkMetric (c • m) = c • mkMetric m

theorem MeasureTheory.OuterMeasure.mkMetric_nnreal_smul {X : Type u_2} [EMetricSpace X] (m : ENNReal → ENNReal) {c : NNReal} (hc : c ≠ 0) : mkMetric (c • m) = c • mkMetric m

theorem MeasureTheory.OuterMeasure.isometry_map_mkMetric {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (m : ENNReal → ENNReal) {f : X → Y} (hf : Isometry f) (H : Monotone m ∨ Function.Surjective f) : (map f) (mkMetric m) = (restrict (Set.range f)) (mkMetric m)

theorem MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (m : ENNReal → ENNReal) (f : X ≃ᵢ Y) : (comap ⇑f) (mkMetric m) = mkMetric m

theorem MeasureTheory.OuterMeasure.isometryEquiv_map_mkMetric {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] (m : ENNReal → ENNReal) (f : X ≃ᵢ Y) : (map ⇑f) (mkMetric m) = mkMetric m

theorem MeasureTheory.OuterMeasure.trim_mkMetric {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) : (mkMetric m).trim = mkMetric m

theorem MeasureTheory.OuterMeasure.le_mkMetric {X : Type u_2} [EMetricSpace X] (m : ENNReal → ENNReal) (μ : OuterMeasure X) (r : ENNReal) (h0 : 0 < r) (hr : ∀ (s : Set X), EMetric.diam s ≤ r → μ s ≤ m (EMetric.diam s)) : μ ≤ mkMetric m

Metric measures

In this section we use MeasureTheory.OuterMeasure.toMeasure and theorems about MeasureTheory.OuterMeasure.mkMetric'/MeasureTheory.OuterMeasure.mkMetric to define MeasureTheory.Measure.mkMetric'/MeasureTheory.Measure.mkMetric. We also restate some lemmas about metric outer measures for metric measures.

def MeasureTheory.Measure.mkMetric' {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : Set X → ENNReal) : Measure X

Given a function m : Set X → ℝ≥0∞, mkMetric' m is the supremum of μ r over r > 0, where μ r is the maximal outer measure μ such that μ s ≤ m s for all s. While each μ r is an outer measure, the supremum is a measure.

Equations

• MeasureTheory.Measure.mkMetric' m = (MeasureTheory.OuterMeasure.mkMetric' m).toMeasure ⋯

def MeasureTheory.Measure.mkMetric {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) : Measure X

Given a function m : ℝ≥0∞ → ℝ≥0∞, mkMetric m is the supremum of μ r over r > 0, where μ r is the maximal outer measure μ such that μ s ≤ m s for all sets s that contain at least two points. While each mkMetric'.pre is an outer measure, the supremum is a measure.

Equations

• MeasureTheory.Measure.mkMetric m = (MeasureTheory.OuterMeasure.mkMetric m).toMeasure ⋯

@[simp]

theorem MeasureTheory.Measure.mkMetric'_toOuterMeasure {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : Set X → ENNReal) : (mkMetric' m).toOuterMeasure = (OuterMeasure.mkMetric' m).trim

@[simp]

theorem MeasureTheory.Measure.mkMetric_toOuterMeasure {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) : (mkMetric m).toOuterMeasure = OuterMeasure.mkMetric m

theorem MeasureTheory.OuterMeasure.coe_mkMetric {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) : ⇑(mkMetric m) = ⇑(Measure.mkMetric m)

theorem MeasureTheory.Measure.mkMetric_mono_smul {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) (h0 : c ≠ 0) (hle : m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] c • m₂) : mkMetric m₁ ≤ c • mkMetric m₂

If c ∉ {0, ∞} and m₁ d ≤ c * m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 0] to state this), then mkMetric m₁ hm₁ ≤ c • mkMetric m₂ hm₂.

@[simp]

theorem MeasureTheory.Measure.mkMetric_top {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] : (mkMetric fun (x : ENNReal) => ⊤) = ⊤

theorem MeasureTheory.Measure.mkMetric_mono {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {m₁ m₂ : ENNReal → ENNReal} (hle : m₁ ≤ᶠ[nhdsWithin 0 (Set.Ici 0)] m₂) : mkMetric m₁ ≤ mkMetric m₂

If m₁ d ≤ m₂ d for d < ε for some ε > 0 (we use ≤ᶠ[𝓝[≥] 0] to state this), then mkMetric m₁ hm₁ ≤ mkMetric m₂ hm₂.

theorem MeasureTheory.Measure.mkMetric_apply {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) (s : Set X) : (mkMetric m) s = ⨆ (r : ENNReal), ⨆ (_ : 0 < r), ⨅ (t : ℕ → Set X), ⨅ (_ : s ⊆ Set.iUnion t), ⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (EMetric.diam (t n))

A formula for MeasureTheory.Measure.mkMetric.

theorem MeasureTheory.Measure.le_mkMetric {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal) (μ : Measure X) (ε : ENNReal) (h₀ : 0 < ε) (h : ∀ (s : Set X), EMetric.diam s ≤ ε → μ s ≤ m (EMetric.diam s)) : μ ≤ mkMetric m

theorem MeasureTheory.Measure.mkMetric_le_liminf_tsum {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i) (m : ENNReal → ENNReal) : (mkMetric m) s ≤ Filter.liminf (fun (n : β) => ∑' (i : ι n), m (EMetric.diam (t n i))) l

To bound the Hausdorff measure (or, more generally, for a measure defined using MeasureTheory.Measure.mkMetric) of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of countable types.

theorem MeasureTheory.Measure.mkMetric_le_liminf_sum {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [hι : (n : β) → Fintype (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i) (m : ENNReal → ENNReal) : (mkMetric m) s ≤ Filter.liminf (fun (n : β) => ∑ i : ι n, m (EMetric.diam (t n i))) l

To bound the Hausdorff measure (or, more generally, for a measure defined using MeasureTheory.Measure.mkMetric) of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of finite types.

Hausdorff measure and Hausdorff dimension

def MeasureTheory.Measure.hausdorffMeasure {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ℝ) : Measure X

Hausdorff measure on an (e)metric space.

Equations

• MeasureTheory.Measure.hausdorffMeasure d = MeasureTheory.Measure.mkMetric fun (r : ENNReal) => r ^ d

def MeasureTheory.«termμH[_]» : Lean.ParserDescr

Hausdorff measure on an (e)metric space.

Equations

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

theorem MeasureTheory.Measure.le_hausdorffMeasure {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ℝ) (μ : Measure X) (ε : ENNReal) (h₀ : 0 < ε) (h : ∀ (s : Set X), EMetric.diam s ≤ ε → μ s ≤ EMetric.diam s ^ d) : μ ≤ hausdorffMeasure d

theorem MeasureTheory.Measure.hausdorffMeasure_apply {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ℝ) (s : Set X) : (hausdorffMeasure d) s = ⨆ (r : ENNReal), ⨆ (_ : 0 < r), ⨅ (t : ℕ → Set X), ⨅ (_ : s ⊆ ⋃ (n : ℕ), t n), ⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), EMetric.diam (t n) ^ d

A formula for μH[d] s.

theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i) : (hausdorffMeasure d) s ≤ Filter.liminf (fun (n : β) => ∑' (i : ι n), EMetric.diam (t n i) ^ d) l

To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of countable types.

theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {β : Type u_4} {ι : β → Type u_5} [(n : β) → Fintype (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal) (hr : Filter.Tendsto r l (nhds 0)) (t : (n : β) → ι n → Set X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) (hst : ∀ᶠ (n : β) in l, s ⊆ ⋃ (i : ι n), t n i) : (hausdorffMeasure d) s ≤ Filter.liminf (fun (n : β) => ∑ i : ι n, EMetric.diam (t n i) ^ d) l

To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of finite types.

theorem MeasureTheory.Measure.hausdorffMeasure_zero_or_top {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d₁ d₂ : ℝ} (h : d₁ < d₂) (s : Set X) : (hausdorffMeasure d₂) s = 0 ∨ (hausdorffMeasure d₁) s = ⊤

If d₁ < d₂, then for any set s we have either μH[d₂] s = 0, or μH[d₁] s = ∞.

theorem MeasureTheory.Measure.hausdorffMeasure_mono {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d₁ d₂ : ℝ} (h : d₁ ≤ d₂) (s : Set X) : (hausdorffMeasure d₂) s ≤ (hausdorffMeasure d₁) s

Hausdorff measure μH[d] s is monotone in d.

theorem MeasureTheory.Measure.noAtoms_hausdorff (X : Type u_2) [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℝ} (hd : 0 < d) : NoAtoms (hausdorffMeasure d)

@[simp]

theorem MeasureTheory.Measure.hausdorffMeasure_zero_singleton {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (x : X) : (hausdorffMeasure 0) {x} = 1

theorem MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (h : s.Nonempty) : 1 ≤ (hausdorffMeasure 0) s

theorem MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : s.Subsingleton) {d : ℝ} (hd : 0 ≤ d) : (hausdorffMeasure d) s ≤ 1

Hausdorff measure, Hausdorff dimension, and Hölder or Lipschitz continuous maps

theorem HolderOnWith.hausdorffMeasure_image_le {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {C r : NNReal} {f : X → Y} {s : Set X} (h : HolderOnWith C r f s) (hr : 0 < r) {d : ℝ} (hd : 0 ≤ d) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑C ^ d * (MeasureTheory.Measure.hausdorffMeasure (↑r * d)) s

If f : X → Y is Hölder continuous on s with a positive exponent r, then μH[d] (f '' s) ≤ C ^ d * μH[r * d] s.

theorem LipschitzOnWith.hausdorffMeasure_image_le {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {K : NNReal} {f : X → Y} {s : Set X} (h : LipschitzOnWith K f s) {d : ℝ} (hd : 0 ≤ d) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s

If f : X → Y is K-Lipschitz on s, then μH[d] (f '' s) ≤ K ^ d * μH[d] s.

theorem LipschitzWith.hausdorffMeasure_image_le {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {K : NNReal} {f : X → Y} (h : LipschitzWith K f) {d : ℝ} (hd : 0 ≤ d) (s : Set X) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s

If f is a K-Lipschitz map, then it increases the Hausdorff d-measures of sets at most by the factor of K ^ d.

theorem MeasureTheory.Measure.hausdorffMeasure_smul₀ {𝕜 : Type u_4} {E : Type u_5} [NormedAddCommGroup E] [NormedDivisionRing 𝕜] [Module 𝕜 E] [NormSMulClass 𝕜 E] [MeasurableSpace E] [BorelSpace E] {d : ℝ} (hd : 0 ≤ d) {r : 𝕜} (hr : r ≠ 0) (s : Set E) : (hausdorffMeasure d) (r • s) = ‖r‖₊ ^ d • (hausdorffMeasure d) s

Antilipschitz maps do not decrease Hausdorff measures and dimension

theorem AntilipschitzWith.hausdorffMeasure_preimage_le {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {K : NNReal} {d : ℝ} (hf : AntilipschitzWith K f) (hd : 0 ≤ d) (s : Set Y) : (MeasureTheory.Measure.hausdorffMeasure d) (f ⁻¹' s) ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) s

theorem AntilipschitzWith.le_hausdorffMeasure_image {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {K : NNReal} {d : ℝ} (hf : AntilipschitzWith K f) (hd : 0 ≤ d) (s : Set X) : (MeasureTheory.Measure.hausdorffMeasure d) s ≤ ↑K ^ d * (MeasureTheory.Measure.hausdorffMeasure d) (f '' s)

Isometries preserve the Hausdorff measure and Hausdorff dimension

theorem Isometry.hausdorffMeasure_image {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℝ} (hf : Isometry f) (hd : 0 ≤ d ∨ Function.Surjective f) (s : Set X) : (MeasureTheory.Measure.hausdorffMeasure d) (f '' s) = (MeasureTheory.Measure.hausdorffMeasure d) s

theorem Isometry.hausdorffMeasure_preimage {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℝ} (hf : Isometry f) (hd : 0 ≤ d ∨ Function.Surjective f) (s : Set Y) : (MeasureTheory.Measure.hausdorffMeasure d) (f ⁻¹' s) = (MeasureTheory.Measure.hausdorffMeasure d) (s ∩ Set.range f)

theorem Isometry.map_hausdorffMeasure {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} {d : ℝ} (hf : Isometry f) (hd : 0 ≤ d ∨ Function.Surjective f) : MeasureTheory.Measure.map f (MeasureTheory.Measure.hausdorffMeasure d) = (MeasureTheory.Measure.hausdorffMeasure d).restrict (Set.range f)

@[simp]

theorem IsometryEquiv.hausdorffMeasure_image {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) (s : Set X) : (MeasureTheory.Measure.hausdorffMeasure d) (⇑e '' s) = (MeasureTheory.Measure.hausdorffMeasure d) s

@[simp]

theorem IsometryEquiv.hausdorffMeasure_preimage {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) (s : Set Y) : (MeasureTheory.Measure.hausdorffMeasure d) (⇑e ⁻¹' s) = (MeasureTheory.Measure.hausdorffMeasure d) s

@[simp]

theorem IsometryEquiv.map_hausdorffMeasure {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) : MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.hausdorffMeasure d) = MeasureTheory.Measure.hausdorffMeasure d

theorem IsometryEquiv.measurePreserving_hausdorffMeasure {X : Type u_2} {Y : Type u_3} [EMetricSpace X] [EMetricSpace Y] [MeasurableSpace X] [BorelSpace X] [MeasurableSpace Y] [BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) : MeasureTheory.MeasurePreserving (⇑e) (MeasureTheory.Measure.hausdorffMeasure d) (MeasureTheory.Measure.hausdorffMeasure d)

theorem MeasureTheory.hausdorffMeasure_smul {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {α : Type u_4} [SMul α X] [IsIsometricSMul α X] {d : ℝ} (c : α) (h : 0 ≤ d ∨ Function.Surjective fun (x : X) => c • x) (s : Set X) : (Measure.hausdorffMeasure d) (c • s) = (Measure.hausdorffMeasure d) s

theorem MeasureTheory.hausdorffMeasure_vadd {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {α : Type u_4} [VAdd α X] [IsIsometricVAdd α X] {d : ℝ} (c : α) (h : 0 ≤ d ∨ Function.Surjective fun (x : X) => c +ᵥ x) (s : Set X) : (Measure.hausdorffMeasure d) (c +ᵥ s) = (Measure.hausdorffMeasure d) s

instance MeasureTheory.instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℝ} [Group X] [IsIsometricSMul X X] : (Measure.hausdorffMeasure d).IsMulLeftInvariant

instance MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℝ} [AddGroup X] [IsIsometricVAdd X X] : (Measure.hausdorffMeasure d).IsAddLeftInvariant

instance MeasureTheory.instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℝ} [Group X] [IsIsometricSMul Xᵐᵒᵖ X] : (Measure.hausdorffMeasure d).IsMulRightInvariant

instance MeasureTheory.instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] {d : ℝ} [AddGroup X] [IsIsometricVAdd Xᵃᵒᵖ X] : (Measure.hausdorffMeasure d).IsAddRightInvariant

Hausdorff measure and Lebesgue measure

@[simp]

theorem MeasureTheory.hausdorffMeasure_pi_real {ι : Type u_4} [Fintype ι] : Measure.hausdorffMeasure ↑(Fintype.card ι) = volume

In the space ι → ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

instance MeasureTheory.isAddHaarMeasure_hausdorffMeasure {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : (Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).IsAddHaarMeasure

theorem MeasureTheory.hausdorffMeasure_measurePreserving_funUnique (ι : Type u_1) (X : Type u_2) [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] [Unique ι] [SecondCountableTopology X] (d : ℝ) : MeasurePreserving (⇑(MeasurableEquiv.funUnique ι X)) (Measure.hausdorffMeasure d) (Measure.hausdorffMeasure d)

theorem MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo (α : Fin 2 → Type u_4) [(i : Fin 2) → MeasurableSpace (α i)] [(i : Fin 2) → EMetricSpace (α i)] [∀ (i : Fin 2), BorelSpace (α i)] [∀ (i : Fin 2), SecondCountableTopology (α i)] (d : ℝ) : MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.hausdorffMeasure d) (Measure.hausdorffMeasure d)

@[simp]

theorem MeasureTheory.hausdorffMeasure_real : Measure.hausdorffMeasure 1 = volume

In the space ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

@[simp]

theorem MeasureTheory.hausdorffMeasure_prod_real : Measure.hausdorffMeasure 2 = volume

In the space ℝ × ℝ, the Hausdorff measure coincides exactly with the Lebesgue measure.

Geometric results in affine spaces

theorem MeasureTheory.hausdorffMeasure_smul_right_image {E : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (v : E) (s : Set ℝ) : (Measure.hausdorffMeasure 1) ((fun (r : ℝ) => r • v) '' s) = ‖v‖₊ • (Measure.hausdorffMeasure 1) s

theorem MeasureTheory.hausdorffMeasure_homothety_image {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor E P] [BorelSpace P] {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0) (s : Set P) : (Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) = ‖c‖₊ ^ d • (Measure.hausdorffMeasure d) s

Scaling by c around x scales the measure by ‖c‖₊ ^ d.

theorem MeasureTheory.hausdorffMeasure_homothety_preimage {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [NormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor E P] [BorelSpace P] {d : ℝ} (hd : 0 ≤ d) (x : P) {c : 𝕜} (hc : c ≠ 0) (s : Set P) : (Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) ⁻¹' s) = ‖c‖₊⁻¹ ^ d • (Measure.hausdorffMeasure d) s

TODO: prove Measure.map (AffineMap.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d], which needs a more general version of AffineMap.homothety_continuous.

theorem MeasureTheory.hausdorffMeasure_lineMap_image {E : Type u_5} {P : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor E P] [BorelSpace P] (x y : P) (s : Set ℝ) : (Measure.hausdorffMeasure 1) (⇑(AffineMap.lineMap x y) '' s) = nndist x y • (Measure.hausdorffMeasure 1) s

Mapping a set of reals along a line segment scales the measure by the length of a segment.

This is an auxiliary result used to prove hausdorffMeasure_affineSegment.

@[simp]

theorem MeasureTheory.hausdorffMeasure_affineSegment {E : Type u_5} {P : Type u_6} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace P] [MetricSpace P] [NormedAddTorsor E P] [BorelSpace P] (x y : P) : (Measure.hausdorffMeasure 1) (affineSegment ℝ x y) = edist x y

The measure of a segment is the distance between its endpoints.

@[simp]

theorem MeasureTheory.hausdorffMeasure_segment {E : Type u_7} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (x y : E) : (Measure.hausdorffMeasure 1) (segment ℝ x y) = edist x y

The measure of a segment is the distance between its endpoints.

theorem MeasureTheory.hausdorffMeasure_orthogonalProjection_le {𝕜 : Type u_4} {E : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] (K : Submodule 𝕜 E) [K.HasOrthogonalProjection] (d : ℝ) (s : Set E) (hs : 0 ≤ d) : (Measure.hausdorffMeasure d) (⇑K.orthogonalProjection '' s) ≤ (Measure.hausdorffMeasure d) s

Let s be a subset of 𝕜-inner product space, and K a subspace. Then the d-dimensional Hausdorff measure of the orthogonal projection of s onto K is less than or equal to the d-dimensional Hausdorff measure of s.