Documentation

Mathlib.MeasureTheory.Measure.Hausdorff

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 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 #

Main statements #

Basic properties #

Hausdorff measure in ℝⁿ #

Notations #

We use the following notation localized in MeasureTheory.

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 #

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.

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
Instances For
    theorem MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated {ι : Type u_1} {X : Type u_2} [EMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (hm : μ.IsMetric) {I : Finset ι} {s : ιSet X} (hI : iI, jI, i jIsMetricSeparated (s i) (s j)) :
    μ (⋃ iI, s i) = iI, μ (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] {μ : MeasureTheory.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] {μ : MeasureTheory.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.

    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
    Instances For

      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
      Instances For

        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
        Instances For

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

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

          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₂.

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

          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.

          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
          Instances For

            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
            Instances For

              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₂.

              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 : ENNRealENNReal) (s : Set X) :
              (MeasureTheory.Measure.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 : ENNRealENNReal) (μ : MeasureTheory.Measure X) (ε : ENNReal) (h₀ : 0 < ε) (h : ∀ (s : Set X), EMetric.diam s εμ s m (EMetric.diam s)) :
              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 : β) → ι nSet 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 : ENNRealENNReal) :
              (MeasureTheory.Measure.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 : β) → ι nSet 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 : ENNRealENNReal) :
              (MeasureTheory.Measure.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 #

              Hausdorff measure on an (e)metric space.

              Equations
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem MeasureTheory.Measure.hausdorffMeasure_apply {X : Type u_2} [EMetricSpace X] [MeasurableSpace X] [BorelSpace X] (d : ) (s : Set X) :
                  (MeasureTheory.Measure.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 : β) → ι nSet X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s ⋃ (i : ι n), t n i) :
                  (MeasureTheory.Measure.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 : β) → ι nSet X) (ht : ∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) r n) (hst : ∀ᶠ (n : β) in l, s ⋃ (i : ι n), t n i) :
                  (MeasureTheory.Measure.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.

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

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

                  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 : NNReal} {r : NNReal} {f : XY} {s : Set X} (h : HolderOnWith C r f s) (hr : 0 < r) {d : } (hd : 0 d) :

                  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.

                  If f : X → Y is K-Lipschitz on s, then μH[d] (f '' s) ≤ K ^ d * μH[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.

                  Antilipschitz maps do not decrease Hausdorff measures and dimension #

                  Isometries preserve the Hausdorff measure and Hausdorff dimension #

                  Hausdorff measure and Lebesgue measure #

                  @[simp]

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

                  @[simp]

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

                  @[simp]

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

                  Geometric results in affine spaces #

                  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) :

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

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

                  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]

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

                  @[simp]

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