Hausdorff measure and metric (outer) measures #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
measure_theory.outer_measure.is_metric.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
measure_theory.measure.hausdorff_measure_zero_or_top
. In
topology.metric_space.hausdorff_dimension
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
measure_theory.measure.mk_metric
) we take any function m (diam s)
instead of (diam s) ^ d
. In
an even more general definition (see measure_theory.measure.mk_metric'
) 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 measure_theory.extend m
.
We also define a predicate measure_theory.outer_measure.is_metric
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
measure_theory.outer_measure.is_metric.borel_le_caratheodory
, so we prove this theorem for any
metric outer measure, then prove that outer measures constructed using mk_metric'
are metric outer
measures.
Main definitions #
measure_theory.outer_measure.is_metric
: an outer measureμ
is called metric ifμ (s ∪ t) = μ s + μ t
for any two metric separated setss
andt
. A metric outer measure in a Borel extended metric space is guaranteed to satisfy the Caratheodory condition, seemeasure_theory.outer_measure.is_metric.borel_le_caratheodory
.measure_theory.outer_measure.mk_metric'
and its particular casemeasure_theory.outer_measure.mk_metric
: 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 calledmeasure_theory.measure.mk_metric'
andmeasure_theory.measure.mk_metric
.measure_theory.measure.hausdorff_measure
a.k.a.μH[d]
: thed
-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
, seemeasure_theory.measure.hausdorff_measure_apply'
. In the most interesting case0 < d
one can omit the⨆ (ht : ¬set.subsingleton (t n))
part.
Main statements #
Basic properties #
measure_theory.outer_measure.is_metric.borel_le_caratheodory
: ifμ
is a metric outer measure on an extended metric spaceX
(that is, it is additive on pairs of metric separated sets), then every Borel set is Caratheodory measurable (hence,μ
defines an actualmeasure_theory.measure
). See alsomeasure_theory.measure.mk_metric
.measure_theory.measure.hausdorff_measure_mono
:μH[d] s
is an antitone function ofd
.measure_theory.measure.hausdorff_measure_zero_or_top
: ifd₁ < d₂
, then for anys
, 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, +∞)
, whereD
is a possibly infinite number called the Hausdorff dimension ofs
;μH[D] s
can be zero, infinity, or anything in between.measure_theory.measure.no_atoms_hausdorff
: Hausdorff measure has no atoms.
Hausdorff measure in ℝⁿ
#
measure_theory.hausdorff_measure_pi_real
: for a nonemptyι
,μH[card ι]
onι → ℝ
equals Lebesgue measure.
Notations #
We use the following notation localized in measure_theory
.
μH[d]
:measure_theory.measure.hausdorff_measure 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 #
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
.
A metric outer measure is additive on a finite set of pairwise metric separated sets.
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
.
Constructors of metric outer measures #
In this section we provide constructors measure_theory.outer_measure.mk_metric'
and
measure_theory.outer_measure.mk_metric
and prove that these outer measures are metric outer
measures. We also prove basic lemmas about map
/comap
of these measures.
Auxiliary definition for outer_measure.mk_metric'
: 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
- measure_theory.outer_measure.mk_metric'.pre m r = measure_theory.outer_measure.bounded_by (measure_theory.extend (λ (s : set X) (hs : emetric.diam s ≤ r), m s))
Given a function m : set X → ℝ≥0∞
, mk_metric' m
is the supremum of mk_metric'.pre m r
over r > 0
. Equivalently, it is the limit of mk_metric'.pre m r
as r
tends to zero from
the right.
Equations
- measure_theory.outer_measure.mk_metric' m = ⨆ (r : ennreal) (H : r > 0), measure_theory.outer_measure.mk_metric'.pre m r
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
mk_metric m = ⨆ r > 0, μ r
.
Equations
- measure_theory.outer_measure.mk_metric m = measure_theory.outer_measure.mk_metric' (λ (s : set X), m (emetric.diam s))
measure_theory.outer_measure.mk_metric'.pre m r
is a trimmed measure provided that
m (closure s) = m s
for any set s
.
An outer measure constructed using outer_measure.mk_metric'
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 mk_metric m₁ hm₁ ≤ c • mk_metric m₂ hm₂
.
If m₁ d ≤ m₂ d
for d < ε
for some ε > 0
(we use ≤ᶠ[𝓝[≥] 0]
to state this), then
mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂
Metric measures #
In this section we use measure_theory.outer_measure.to_measure
and theorems about
measure_theory.outer_measure.mk_metric'
/measure_theory.outer_measure.mk_metric
to define
measure_theory.measure.mk_metric'
/measure_theory.measure.mk_metric
. We also restate some lemmas
about metric outer measures for metric measures.
Given a function m : set X → ℝ≥0∞
, mk_metric' 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
Given a function m : ℝ≥0∞ → ℝ≥0∞
, mk_metric 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 mk_metric'.pre
is an outer measure, the supremum is a measure.
Equations
If c ∉ {0, ∞}
and m₁ d ≤ c * m₂ d
for d < ε
for some ε > 0
(we use ≤ᶠ[𝓝[≥] 0]
to state this), then mk_metric m₁ hm₁ ≤ c • mk_metric m₂ hm₂
.
If m₁ d ≤ m₂ d
for d < ε
for some ε > 0
(we use ≤ᶠ[𝓝[≥] 0]
to state this), then
mk_metric m₁ hm₁ ≤ mk_metric m₂ hm₂
A formula for measure_theory.measure.mk_metric
.
To bound the Hausdorff measure (or, more generally, for a measure defined using
measure_theory.measure.mk_metric
) of a set, one may use coverings with maximum diameter tending to
0
, indexed by any sequence of countable types.
To bound the Hausdorff measure (or, more generally, for a measure defined using
measure_theory.measure.mk_metric
) 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
- measure_theory.measure.hausdorff_measure d = measure_theory.measure.mk_metric (λ (r : ennreal), r ^ d)
Instances for measure_theory.measure.hausdorff_measure
A formula for μH[d] s
.
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.
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 #
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 #
In the space ι → ℝ
, the Hausdorff measure coincides exactly with the Lebesgue measure.
In the space ℝ
, the Hausdorff measure coincides exactly with the Lebesgue measure.
In the space ℝ × ℝ
, the Hausdorff measure coincides exactly with the Lebesgue measure.
Geometric results in affine spaces #
Scaling by c
around x
scales the measure by ‖c‖₊ ^ d
.
TODO: prove measure.map (affine_map.homothety x c) μH[d] = ‖c‖₊⁻¹ ^ d • μH[d]
, which needs a
more general version of affine_map.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 hausdorff_measure_affine_segment
.
The measure of a segment is the distance between its endpoints.
The measure of a segment is the distance between its endpoints.