MeasureTheory.OuterMeasure.mkMetric'.trim_pre
theorem MeasureTheory.OuterMeasure.mkMetric'.trim_pre :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
(m : Set X → ENNReal),
(∀ (s : Set X), m (closure s) = m s) →
∀ (r : ENNReal),
(MeasureTheory.OuterMeasure.mkMetric'.pre m r).trim = MeasureTheory.OuterMeasure.mkMetric'.pre m r
The theorem `MeasureTheory.OuterMeasure.mkMetric'.trim_pre` states that for any type `X` equipped with an `EMetricSpace` structure, a `MeasurableSpace` structure, and an `OpensMeasurableSpace` structure, and for any function `m` from sets of `X` to the extended nonnegative real numbers (ENNReal), if for every set `s` the value of `m` at the closure of `s` is equal to the value of `m` at `s`, then for any extended nonnegative real number `r`, the "trimmed" version of the measure produced by `MeasureTheory.OuterMeasure.mkMetric'.pre m r` is equal to the original measure `MeasureTheory.OuterMeasure.mkMetric'.pre m r`.
In essence, this theorem asserts that if a measure-like function `m` is invariant under taking closures of sets, then the process of "trimming" does not alter the outer measure induced by `m` at any given scale `r` in the extended nonnegative real numbers.
More concisely: If a measure-function `m` on an `EMetricSpace` with `MeasurableSpace` and `OpensMeasurableSpace` structures satisfies `m(cl(s)) = m(s)` for all sets `s`, then `MeasureTheory.OuterMeasure.mkMetric'.trim_pre m r` equals `MeasureTheory.OuterMeasure.mkMetric'.pre m r` for any extended nonnegative real number `r`.
|
MeasureTheory.Measure.mkMetric_le_liminf_sum
theorem MeasureTheory.Measure.mkMetric_le_liminf_sum :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
{ι : β → Type u_5} [hι : (n : β) → Fintype (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal),
Filter.Tendsto r l (nhds 0) →
∀ (t : (n : β) → ι n → Set X),
(∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) →
(∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
∀ (m : ENNReal → ENNReal),
↑↑(MeasureTheory.Measure.mkMetric m) s ≤
Filter.liminf (fun n => Finset.univ.sum fun i => m (EMetric.diam (t n i))) l
This theorem states that to bound the Hausdorff measure of a set (or more generally a measure defined using `MeasureTheory.Measure.mkMetric`) in an extended metric space, one can use coverings with maximum diameter tending to `0`. These coverings can be indexed by any sequence of finite types. Given a set `s` and a sequence `r` that converges to `0` along a filter `l`, if there exists a sequence of sets `t` such that the diameter of each `t` doesn't exceed `r` and `s` is a subset of the union of the `t`, then for any function `m` from extended nonnegative real numbers to itself, the measure of `s` is less than or equal to the limit inferior (liminf) of the sum of `m` applied to the diameters of `t`, where the sum is over all elements of a universal finite set.
More concisely: Given a set $s$ in an extended metric space and a sequence $r$ converging to $0$, if there exists a sequence of sets $t$ with diameter less than $r$ for each $t$ and $s$ is a subset of their union, then the Hausdorff measure of $s$ is less than or equal to the liminf of the sum of the measures of $t$ over a universal finite set.
|
MeasureTheory.hausdorffMeasure_lineMap_image
theorem MeasureTheory.hausdorffMeasure_lineMap_image :
∀ {E : Type u_5} {P : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : MeasurableSpace P] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor E P] [inst_5 : BorelSpace P]
(x y : P) (s : Set ℝ),
↑↑(MeasureTheory.Measure.hausdorffMeasure 1) (⇑(AffineMap.lineMap x y) '' s) =
nndist x y • ↑↑(MeasureTheory.Measure.hausdorffMeasure 1) s
This theorem states that for a given set of real numbers `s` and two points `x` and `y` in a metric space `P` (which is also a measurable space, a normed add-torsor, and a Borel space) with a normed add-commutative group `E` and where `E` is a normed space over the real numbers, mapping the set `s` along the line segment defined by `x` and `y` scales the Hausdorff measure of the set by the distance between `x` and `y`. In other words, the Hausdorff measure of the image of the set `s` under the line map defined by `x` and `y` is equal to the distance between `x` and `y` times the Hausdorff measure of the original set `s`.
In mathematical terms, if `AffineMap.lineMap x y` is the affine map from the real numbers to `P` sending `0` to `x` and `1` to `y`, then the Hausdorff measure of the image of `s` under this map is equal to the distance between `x` and `y` times the Hausdorff measure of `s`. This is denoted as `nndist x y • ↑↑(MeasureTheory.Measure.hausdorffMeasure 1) s`.
More concisely: The Hausdorff measure of a set in a metric space, when mapped along the line segment between two points via an affine map, scales by the distance between the points.
|
MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum
theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
{ι : β → Type u_5} [inst_3 : ∀ (n : β), Countable (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal),
Filter.Tendsto r l (nhds 0) →
∀ (t : (n : β) → ι n → Set X),
(∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) →
(∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
↑↑(MeasureTheory.Measure.hausdorffMeasure d) s ≤
Filter.liminf (fun n => ∑' (i : ι n), EMetric.diam (t n i) ^ d) l
This theorem states that in order to bound the Hausdorff measure of a set in an eMetric space, one can use coverings whose maximum diameter tends to zero. These coverings are indexed by any sequence of countable types. Specifically, given an eMetric space `X`, a measurable space `X`, a Borel space `X`, a sequence of countable types `ι` indexed by `β`, a real number `d`, a set `s` in `X`, a filter `l` on `β`, and a function `r` from `β` to the extended nonnegative real numbers, if `r` tends to zero as `l` tends to the neighborhood of zero and there exists a function `t` such that for all eventually `n` in `l`, for all `i` in `ι n`, the diameter of `t n i` is less than or equal to `r n` and `s` is a subset of the union over `i` of `t n i`, then the Hausdorff measure of `s` with respect to `d` is less than or equal to the limit inferior of the function which takes `n` to the sum over `i` in `ι n` of the diameter of `t n i` to the power of `d` as `l` tends to the neighborhood of the limit inferior.
More concisely: Given an eMetric space `X`, a measurable set `s`, a filter `l` on a countable index set `β`, and a function `r` tending to zero as `l` approaches zero, if there exists a covering `{ti}_i∈ι of s by sets, such that the diameters of `ti` are bounded by `r` and `s` is contained in their union, then the Hausdorff measure of `s` is less than the limit inferior of the sum of the diameters of `ti` raised to the power of `d`.
|
MeasureTheory.OuterMeasure.mkMetric'_isMetric
theorem MeasureTheory.OuterMeasure.mkMetric'_isMetric :
∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal), (MeasureTheory.OuterMeasure.mkMetric' m).IsMetric
This theorem states that for any type `X` equipped with an `EMetricSpace` structure and a function `m` mapping sets of `X` to extended nonnegative real numbers (or `ENNReal`), the outer measure constructed using `MeasureTheory.OuterMeasure.mkMetric'` with `m` as input is a metric outer measure. In other words, given a function `m` that assigns a nonnegative extended real number (`ENNReal`) to each set in a metric space `X`, the measure constructed by `MeasureTheory.OuterMeasure.mkMetric'` from `m` obeys the properties of a metric outer measure.
More concisely: Given a type `X` with an `EMetricSpace` structure and a function `m : Set X → ENNReal` assigning extended nonnegative real numbers to sets, the outer measure constructed using `MeasureTheory.OuterMeasure.mkMetric'` from `m` is a metric outer measure.
|
MeasureTheory.Measure.mkMetric_mono_smul
theorem MeasureTheory.Measure.mkMetric_mono_smul :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
{m₁ m₂ : ENNReal → ENNReal} {c : ENNReal},
c ≠ ⊤ →
c ≠ 0 →
(nhdsWithin 0 (Set.Ici 0)).EventuallyLE m₁ (c • m₂) →
MeasureTheory.Measure.mkMetric m₁ ≤ c • MeasureTheory.Measure.mkMetric m₂
This theorem states that if we have a nonzero and non-infinite constant `c`, and two functions `m₁` and `m₂` from the extended nonnegative real numbers to themselves, such that for some positive `ε`, `m₁ d` is less than or equal to `c * m₂ d` for all `d` smaller than `ε` (expressed as `m₁` is eventually less than or equal to `c • m₂` in the filter of neighborhoods of `0` within the set of nonnegative reals), then the measure created using `mkMetric` with `m₁` is less than or equal to `c` times the measure created using `mkMetric` with `m₂`.
In other words, if `m₁` is eventually dominated by `c * m₂` near `0`, then the corresponding measure constructed from `m₁` is dominated by the `c`-scaled measure constructed from `m₂`. This is a statement about the comparison of measures derived from two different functions under certain conditions.
More concisely: If functions `m₁` and `m₂` on the extended nonnegative reals satisfy `m₁ ≤ c * m₂` in the filter of neighborhoods of `0`, then the metric measures induced by `m₁` and `c * m₂` are comparable, with the measure induced by `m₁` less than or equal to that induced by `m₂`.
|
LipschitzOnWith.hausdorffMeasure_image_le
theorem LipschitzOnWith.hausdorffMeasure_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {K : NNReal} {f : X → Y} {s : Set X},
LipschitzOnWith K f s →
∀ {d : ℝ},
0 ≤ d →
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤
↑K ^ d * ↑↑(MeasureTheory.Measure.hausdorffMeasure d) s
The theorem `LipschitzOnWith.hausdorffMeasure_image_le` states that if a function `f`, mapping from a type `X` to a type `Y`, is `K`-Lipschitz continuous on a set `s` of type `X`, then the Hausdorff measure (of dimension `d`) of the image of the set `s` under the function `f` is less than or equal to `K` to the power of `d` times the Hausdorff measure of the set `s` itself. Note that `K` is a nonnegative real number, `d` is a real number that is greater than or equal to zero, and `X` and `Y` are types equipped with an eMetric space structure, a measurable space structure, and a Borel space structure.
More concisely: If `f: X → Y` is `K`-Lipschitz continuous on the set `s ⊆ X` (of Hausdorff measure `μ_d(s)`), then `μ_d(f[s]) ≤ K^d * μ_d(s)`, where `μ_d` denotes the Hausdorff measure of dimension `d` on types `X` and `Y`.
|
MeasureTheory.Measure.hausdorffMeasure_zero_or_top
theorem MeasureTheory.Measure.hausdorffMeasure_zero_or_top :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℝ},
d₁ < d₂ →
∀ (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d₂) s = 0 ∨ ↑↑(MeasureTheory.Measure.hausdorffMeasure d₁) s = ⊤
The theorem `MeasureTheory.Measure.hausdorffMeasure_zero_or_top` states that for any type `X` equipped with an eMetric space, a Measurable space, and a Borel space, and for any two real numbers `d₁` and `d₂` such that `d₁` is less than `d₂`, for any set `s` of type `X`, the Hausdorff measure of `s` with respect to `d₂` is either zero or the Hausdorff measure of `s` with respect to `d₁` is infinity. In simpler terms, it states that if we are considering two dimensions for the Hausdorff measure and the first dimension is less than the second, then for any set, the measure in the higher dimension is either zero or the measure in the lower dimension is infinity.
More concisely: For any set in a metric space endowed with a Borel structure, the Hausdorff measure in a larger dimension is either zero or equals infinity in a smaller dimension.
|
MeasureTheory.OuterMeasure.mkMetric_mono
theorem MeasureTheory.OuterMeasure.mkMetric_mono :
∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal},
(nhdsWithin 0 (Set.Ici 0)).EventuallyLE m₁ m₂ →
MeasureTheory.OuterMeasure.mkMetric m₁ ≤ MeasureTheory.OuterMeasure.mkMetric m₂
If we have two functions `m₁` and `m₂` from the extended non-negative real numbers to themselves, denoted as `ENNReal → ENNReal`, and if `m₁ d ≤ m₂ d` for all `d` in a neighborhood within the set of non-negative real numbers containing 0 (expressed as `nhdsWithin 0 (Set.Ici 0)`), then the maximal outer measure generated by `m₁` (denoted as `mkMetric m₁`) is less than or equal to the maximal outer measure generated by `m₂` (denoted as `mkMetric m₂`). This is stated for some `ε > 0`, using `≤ᶠ[𝓝[≥] 0]` to express this quantitatively.
More concisely: If `m₁` and `m₂` are functions from the extended non-negative real numbers to themselves such that `m₁ (d) ≤ m₂ (d)` for all `d` in a neighborhood containing 0, then `mkMetric m₁ ≤ mkMetric m₂`.
|
MeasureTheory.hausdorffMeasure_homothety_image
theorem MeasureTheory.hausdorffMeasure_homothety_image :
∀ {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
[inst_6 : BorelSpace P] {d : ℝ},
0 ≤ d →
∀ (x : P) {c : 𝕜},
c ≠ 0 →
∀ (s : Set P),
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) =
‖c‖₊ ^ d • ↑↑(MeasureTheory.Measure.hausdorffMeasure d) s
This theorem states that if you take a set `s` in a metric space, and scale it by a factor `c` around a point `x` using a homothety (which is a type of transformation that scales a shape), then the Hausdorff measure of the transformed set is scaled by the norm of `c` raised to the power `d`. This is valid when `d` is non-negative and `c` is non-zero. The Hausdorff measure reflects the 'size' or 'volume' of a set, so this theorem is saying that scaling the set scales its 'volume' by the same factor, but the factor is raised to the power `d`.
More concisely: The Hausdorff measure of a set scaled by a homothety in a metric space is multiplied by the norm of the scaling factor raised to the power of the Hausdorff dimension.
|
LipschitzWith.hausdorffMeasure_image_le
theorem LipschitzWith.hausdorffMeasure_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {K : NNReal} {f : X → Y},
LipschitzWith K f →
∀ {d : ℝ},
0 ≤ d →
∀ (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤
↑K ^ d * ↑↑(MeasureTheory.Measure.hausdorffMeasure d) s
This theorem states that if a function `f` is `K`-Lipschitz continuous (meaning the distance between `f(x)` and `f(y)` is at most `K` times the distance between `x` and `y`), then the Hausdorff `d`-measure (a measure of size in an eMetric space) of the image of any set under `f` is at most `K` to the power of `d` times the Hausdorff `d`-measure of the original set. The Hausdorff `d`-measure is defined as a measure generated by a function that raises the distance `r` to the power `d`. This is valid for any nonnegative real `d`. In other words, a `K`-Lipschitz continuous function does not increase the Hausdorff `d`-measure of a set by more than a factor of `K` to the power of `d`.
More concisely: If `f` is a `K`-Lipschitz continuous function on an eMetric space, then the Hausdorff `d`-measure of `f`'s image of a set is at most `K^d` times the Hausdorff `d`-measure of the original set.
|
MeasureTheory.Measure.hausdorffMeasure_apply
theorem MeasureTheory.Measure.hausdorffMeasure_apply :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d : ℝ) (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d) s =
⨆ r,
⨆ (_ : 0 < r),
⨅ t,
⨅ (_ : s ⊆ ⋃ n, t n),
⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), EMetric.diam (t n) ^ d
This theorem provides an expression for the Hausdorff measure of a set in an e-metric space. For any real number `d` and any set `s` in an e-metric space `X` (with a measurable space structure and a Borel space structure), the Hausdorff measure of `s` at `d`, `MeasureTheory.Measure.hausdorffMeasure d s`, is equal to the supremum over all positive real numbers `r`, of the infimum over all sequences `t` of subsets of `X` such that `s` is contained in the union of the `t` sets, and each `t n` has diameter less than or equal to `r`, of the sum over all natural numbers `n`, of the supremum of the `d`-th power of the diameter of `t n`, given that `t n` is nonempty. This expression is a formal way to capture the "size" of irregular sets in a metric space.
More concisely: The Hausdorff measure of a set in an e-metric space is equal to the supremum of the inf infimum of the sum of the d-th power diameters of nonempty subsets with diameters bounded by r, over all sequences of subsets covering the set.
|
MeasureTheory.hausdorffMeasure_pi_real
theorem MeasureTheory.hausdorffMeasure_pi_real :
∀ {ι : Type u_4} [inst : Fintype ι],
MeasureTheory.Measure.hausdorffMeasure ↑(Fintype.card ι) = MeasureTheory.volume
This theorem states that in the function space `ι → ℝ` (which represents the set of all functions from `ι` to `ℝ`), the Hausdorff measure is equivalent to the Lebesgue measure. Specifically, the equivalence holds when the Hausdorff measure is raised to the power equal to the number of elements in `ι` (denoted as `Fintype.card ι`). In mathematical terms, in an `n`-dimensional space (`n` being the cardinality of `ι`), the `n`-dimensional Hausdorff measure equals the Lebesgue measure.
More concisely: In the function space `ι → ℝ`, the Hausdorff measure equals the Lebesgue measure when raised to the power of `Fintype.card ι`. That is, for any `ι` of cardinality `n`, the `n`-dimensional Hausdorff measure equals the Lebesgue measure.
|
MeasureTheory.hausdorffMeasure_prod_real
theorem MeasureTheory.hausdorffMeasure_prod_real : MeasureTheory.Measure.hausdorffMeasure 2 = MeasureTheory.volume := by
sorry
The theorem `MeasureTheory.hausdorffMeasure_prod_real` states that in the product space `ℝ × ℝ` (the set of all ordered pairs of real numbers), the Hausdorff measure (a measure of the 'size' of a set in a metric space, especially of fractal sets) with parameter 2 coincides exactly with the Lebesgue measure (a way of assigning a size to subsets of a given set, specifically in the context of measure theory). In other words, when considering the set of all ordered pairs of real numbers, the size of a subset as measured by the 2-dimensional Hausdorff measure is exactly the same as the size of the subset as measured by the Lebesgue measure.
More concisely: The Hausdorff measure of dimension 2 in the product space ℝ×ℝ equals the Lebesgue measure.
|
MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated
theorem MeasureTheory.OuterMeasure.IsMetric.finset_iUnion_of_pairwise_separated :
∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {μ : MeasureTheory.OuterMeasure X},
μ.IsMetric →
∀ {I : Finset ι} {s : ι → Set X},
(∀ i ∈ I, ∀ j ∈ I, i ≠ j → IsMetricSeparated (s i) (s j)) → ↑μ (⋃ i ∈ I, s i) = I.sum fun i => ↑μ (s i)
This theorem states that, given a finite set of indices `I` and a family of sets `s` indexed by `I` in an extended metric space `X`, if all pairs of sets from this family are metric separated (i.e., the minimum possible distance between any two points, each from a different set, is a positive constant), then a metric outer measure `μ` on `X`, which is additive on metric separated sets, behaves additively on the union of these sets. In other words, the measure of the union of these sets is equal to the sum of the measures of individual sets.
Mathematically, this can be written as: if `μ` is a metric outer measure on `X`, and `s : ι → Set X` is such that for all `i`, `j` in `I` (with `i ≠ j`), `s i` and `s j` are metric separated, then `μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)`.
More concisely: Given a finite family `s : I → X` of sets in an extended metric space `(X, δ)` with metric outer measure `μ`, if all pairs of sets are metric separated, then `μ (⋃ i ∈ I, s i) = ∑ i ∈ I, μ (s i)`.
|
MeasureTheory.Measure.hausdorffMeasure_mono
theorem MeasureTheory.Measure.hausdorffMeasure_mono :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d₁ d₂ : ℝ},
d₁ ≤ d₂ →
∀ (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d₂) s ≤ ↑↑(MeasureTheory.Measure.hausdorffMeasure d₁) s
The theorem `MeasureTheory.Measure.hausdorffMeasure_mono` states that the Hausdorff measure, denoted as `μH[d] s`, is monotone in `d`, in any eMetric Space `X` that is also a Measurable Space and a Borel Space. More explicitly, for any two real numbers `d₁` and `d₂` such that `d₁` is less than or equal to `d₂`, and for any set `s` of elements from `X`, the Hausdorff measure of `s` with respect to `d₂`, `μH[d₂] s`, is always less than or equal to the Hausdorff measure of `s` with respect to `d₁`, `μH[d₁] s`.
More concisely: For any measurable and Borel sets in a metric space, the Hausdorff measure is decreasing with respect to the metric, i.e., for two metrics `d₁` and `d₂` with `d₁`≤`d₂`, we have `μH[d₁](s) ≤ μH[d₂](s)` for all sets `s`.
|
MeasureTheory.OuterMeasure.mkMetric'.pre_le
theorem MeasureTheory.OuterMeasure.mkMetric'.pre_le :
∀ {X : Type u_2} [inst : EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {s : Set X},
EMetric.diam s ≤ r → ↑(MeasureTheory.OuterMeasure.mkMetric'.pre m r) s ≤ m s
This theorem states that for any type `X` which is an e-Metric space, for any function `m` mapping sets of `X` to extended nonnegative real numbers (`ENNReal`), for any extended nonnegative real number `r` and for any set `s` of `X`, if the `e-Metric` diameter of the set `s` is less than or equal to `r`, then the outer measure (created by `MeasureTheory.OuterMeasure.mkMetric'.pre m r`) of the set `s` is less than or equal to `m(s)`. In other words, for sets with a diameter at most `r`, the outer measure created by `MeasureTheory.OuterMeasure.mkMetric'.pre m r` is an upper bound for the function `m` on these sets.
More concisely: For any e-Metric space `X`, any function `m` mapping sets of `X` to extended nonnegative real numbers, and any set `s` in `X` with e-Metric diameter less than or equal to `r`, we have `MeasureTheory.OuterMeasure.mkMetric'.pre m r s <= m s`.
|
IsometryEquiv.hausdorffMeasure_image
theorem IsometryEquiv.hausdorffMeasure_image :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ) (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (⇑e '' s) = ↑↑(MeasureTheory.Measure.hausdorffMeasure d) s
This theorem states that for any isometric equivalence `e` from a set `X` to a set `Y`, where both `X` and `Y` are equipped with an eMetricSpace, a MeasurableSpace, and a BorelSpace structure, and for any real number `d` and subset `s` of `X`, the Hausdorff measure of the image of `s` under `e` equals the Hausdorff measure of `s` itself. In other words, isometric transformations preserve the Hausdorff measure of sets.
More concisely: For any isometric equivalence between two metric spaces equipped with MeasurableSpace and BorelSpace structures, the Hausdorff measure of the image of a set under the equivalence equals the Hausdorff measure of the original set.
|
MeasureTheory.OuterMeasure.isometry_comap_mkMetric
theorem MeasureTheory.OuterMeasure.isometry_comap_mkMetric :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (m : ENNReal → ENNReal)
{f : X → Y},
Isometry f →
Monotone m ∨ Function.Surjective f →
(MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.mkMetric m) =
MeasureTheory.OuterMeasure.mkMetric m
The theorem `MeasureTheory.OuterMeasure.isometry_comap_mkMetric` states that for any types `X` and `Y` equipped with PseudoEMetricSpace instances, a function `m` mapping from extended nonnegative real numbers to extended nonnegative real numbers, and a function `f` from `X` to `Y`, if `f` is an isometry and either `m` is monotone or `f` is surjective, then the pullback of the maximal outer measure created by `m` under the function `f` is equal to the original maximal outer measure created by `m`. In mathematical terms, it indicates that under specific conditions, the measure of a set and its image under an isometry are the same.
More concisely: If `m` is a monotone PseudoEMetricSpace value on `X` or `f` is a surjective isometry from `X` to `Y`, then the pullback of the maximal outer measure of a set in `X` under `f` is equal to the original maximal outer measure of its image in `Y`.
|
MeasureTheory.Measure.mkMetric_mono
theorem MeasureTheory.Measure.mkMetric_mono :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
{m₁ m₂ : ENNReal → ENNReal},
(nhdsWithin 0 (Set.Ici 0)).EventuallyLE m₁ m₂ →
MeasureTheory.Measure.mkMetric m₁ ≤ MeasureTheory.Measure.mkMetric m₂
The theorem `MeasureTheory.Measure.mkMetric_mono` states that for any two functions `m₁` and `m₂` from the extended nonnegative real numbers to the extended nonnegative real numbers, if `m₁ d ≤ m₂ d` eventually for `d` near `0` and greater than or equal to `0` (expressed as `≤ᶠ[𝓝[≥] 0]`), then the measure generated by `m₁` is less than or equal to the measure generated by `m₂`. Here the measure is generated using `mkMetric`, which constructs a measure as the supremum of certain outer measures associated with a function from the extended nonnegative real numbers. This theorem is set in the context of an Emetric space, a measurable space, and a Borel space.
More concisely: If two functions from the extended nonnegative real numbers to the extended nonnegative real numbers satisfy `m₁(d) ≤ m₂(d)` eventually for `d` near 0, then the measure generated by `m₁` is less than or equal to the measure generated by `m₂` in an Emetric, measurable, and Borel space.
|
MeasureTheory.OuterMeasure.mkMetric_mono_smul
theorem MeasureTheory.OuterMeasure.mkMetric_mono_smul :
∀ {X : Type u_2} [inst : EMetricSpace X] {m₁ m₂ : ENNReal → ENNReal} {c : ENNReal},
c ≠ ⊤ →
c ≠ 0 →
(nhdsWithin 0 (Set.Ici 0)).EventuallyLE m₁ (c • m₂) →
MeasureTheory.OuterMeasure.mkMetric m₁ ≤ c • MeasureTheory.OuterMeasure.mkMetric m₂
The theorem `MeasureTheory.OuterMeasure.mkMetric_mono_smul` says that for any type `X` equipped with an `EMetricSpace` structure and given two extended nonnegative real-valued functions `m₁` and `m₂`, and a scalar `c` which is neither 0 nor infinity, if `m₁ d ≤ c * m₂ d` holds for `d` in a neighborhood within the set of non-negative real numbers around 0, then the outer measure created by `mkMetric` applied to `m₁` is less than or equal to `c` times the outer measure created by `mkMetric` applied to `m₂`. This "neighborhood condition" is denoted in Lean 4 as `≤ᶠ[𝓝[≥] 0]`.
More concisely: If `m₁` and `m₂` are extended nonnegative real-valued functions on an `EMetricSpace` `X`, and `m₁ d ≤ c * m₂ d` holds for all `d` in a neighborhood of 0, then the outer measures of `m₁` and `c * m₂` are equal up to a set of measure zero. (Note that the statement in Lean 4 only guarantees that the outer measure of `m₁` is less than or equal to `c` times the outer measure of `m₂`, but the equality up to a set of measure zero follows from the definitions of outer measures and the given condition.)
|
MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum
theorem MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
{ι : β → Type u_5} [inst_3 : (n : β) → Fintype (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal),
Filter.Tendsto r l (nhds 0) →
∀ (t : (n : β) → ι n → Set X),
(∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) →
(∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
↑↑(MeasureTheory.Measure.hausdorffMeasure d) s ≤
Filter.liminf (fun n => Finset.univ.sum fun i => EMetric.diam (t n i) ^ d) l
The theorem `MeasureTheory.Measure.hausdorffMeasure_le_liminf_sum` states that, for a given set in an emetric space, its Hausdorff measure can be upper-bounded by the limit inferior (as a function tends to zero at a specified filter) of the sum of the d-th power of diameters of coverings of the set. These coverings are indexed by sequences of finite types, and their maximum diameter tends to zero. Specifically, if we have a sequence of radii `r` that tends to `0` at filter `l`, and for every `n` in the filter, we have a corresponding covering of the set `s` such that each of its elements has a diameter less than or equal to `r n`, and the union of all elements in the covering includes the set `s`, then the Hausdorff measure of the set `s` is less than or equal to the limit inferior of the sum of the d-th power of diameters of the coverings of the set.
More concisely: Given a set in a metric space and a filter base, if for each radius tending to 0 in the filter, there exists a covering of the set with diameter less than t and finite elements whose union contains the set, then the Hausdorff measure of the set is less than or equal to the limit inferior of the sum of the d-th powers of the diameters of these coverings.
|
MeasureTheory.Measure.mkMetric_apply
theorem MeasureTheory.Measure.mkMetric_apply :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
(m : ENNReal → ENNReal) (s : Set X),
↑↑(MeasureTheory.Measure.mkMetric m) s =
⨆ r,
⨆ (_ : 0 < r),
⨅ t,
⨅ (_ : s ⊆ Set.iUnion t),
⨅ (_ : ∀ (n : ℕ), EMetric.diam (t n) ≤ r), ∑' (n : ℕ), ⨆ (_ : (t n).Nonempty), m (EMetric.diam (t n))
This theorem provides a formula for creating a measure using the function `MeasureTheory.Measure.mkMetric`. For any extended nonnegative real-valued function `m` and a set `s` in an E-metric and measurable space, the measure of `s` under the measure created by `m` is equivalent to the supremum over all `r` greater than 0 of the infimum over all collections `t` of sets such that `s` is contained in the indexed union of `t`, and every set in `t` has diameter at most `r`. For each such collection `t`, the innermost infimum is the series over all natural numbers `n` of the supremum (over nonempty sets in `t`) of the function `m` applied to the diameter of the `n`-th set in `t`.
More concisely: For any extended nonnegative real-valued function `m` and measurable set `s` in an E-metric space, the measure of `s` under the measure created by `m` equals the supremum over all `r > 0` of the infimum of series, indexed by `n`, of supremums (over nonempty sets in the collection `t`) of `m(diameter(t\_n))`, where `t` is any collection of sets containing `s` with the property that the diameter of each set in `t` is at most `r`.
|
MeasureTheory.hausdorffMeasure_affineSegment
theorem MeasureTheory.hausdorffMeasure_affineSegment :
∀ {E : Type u_5} {P : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : MeasurableSpace P] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor E P] [inst_5 : BorelSpace P]
(x y : P), ↑↑(MeasureTheory.Measure.hausdorffMeasure 1) (affineSegment ℝ x y) = edist x y
This theorem states that in a given measurable and metric space, with a specific normed structure, the Hausdorff measure of a line segment is equal to the Euclidean distance between its endpoints. In other words, when the parameter 'd' in the Hausdorff measure is set to 1, the Hausdorff measure of the line segment (defined by the function 'affineSegment') between two points 'x' and 'y', is equivalent to the Euclidean distance between 'x' and 'y'. This is one of the properties that characterizes the Hausdorff measure in metric spaces.
More concisely: In a measurable and metric space with a normed structure, the Hausdorff measure of a line segment between two points, with parameter 'd' set to 1, equals the Euclidean distance between the points.
|
IsometryEquiv.map_hausdorffMeasure
theorem IsometryEquiv.map_hausdorffMeasure :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] (e : X ≃ᵢ Y) (d : ℝ),
MeasureTheory.Measure.map (⇑e) (MeasureTheory.Measure.hausdorffMeasure d) =
MeasureTheory.Measure.hausdorffMeasure d
The given theorem, `IsometryEquiv.map_hausdorffMeasure`, states that for any isometric equivalence, `e`, between two e-Metric spaces `X` and `Y`, and a real number `d`, the Hausdorff measure of `d` on `X` mapped under the isometry to `Y` is the same as the Hausdorff measure of `d` on `Y`. That is, the Hausdorff measure of `d` is preserved under an isometric mapping. This is a property of the Hausdorff measure in the context of e-Metric spaces.
More concisely: For any isometric equivalence between two e-Metric spaces and a real number, the Hausdorff measure of radius `d` in one space is equal to the Hausdorff measure of the image of that radius under the isometric mapping in the other space.
|
MeasureTheory.Measure.mkMetric_le_liminf_tsum
theorem MeasureTheory.Measure.mkMetric_le_liminf_tsum :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
{ι : β → Type u_5} [inst_3 : ∀ (n : β), Countable (ι n)] (s : Set X) {l : Filter β} (r : β → ENNReal),
Filter.Tendsto r l (nhds 0) →
∀ (t : (n : β) → ι n → Set X),
(∀ᶠ (n : β) in l, ∀ (i : ι n), EMetric.diam (t n i) ≤ r n) →
(∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
∀ (m : ENNReal → ENNReal),
↑↑(MeasureTheory.Measure.mkMetric m) s ≤
Filter.liminf (fun n => ∑' (i : ι n), m (EMetric.diam (t n i))) l
This theorem states that for bounding the Hausdorff measure (or more generally, any measure defined using `MeasureTheory.Measure.mkMetric`) of a set, one can use coverings whose maximum diameter tends to `0`. This covering is indexed by any sequence of countable types. More formally, given an extended metric space `X`, a measurable space on `X`, and a borel space on `X`, for any sequence `β` and a corresponding sequence of countable sets `ι n`, a set `s` in `X`, a filter `l` on `β`, and a function `r : β → ENNReal` that tends to `0` with respect to `l`, for every sequence of sets `t n i` for each `n` in `β` and `i` in `ι n` such that the diameter of `t n i` is less than or equal to `r n` eventually for `l` and `s` is a subset of the union of `t n i` eventually for `l`, for any function `m : ENNReal → ENNReal`, the measure of `s` with respect to the measure created by `m` using `MeasureTheory.Measure.mkMetric` is less than or equal to the limit inferior of the sum of `m (EMetric.diam (t n i))` for all `i` in `ι n`, as `n` tends to infinity according to `l`.
More concisely: Given an extended metric space, a measurable space, and a borel space, for any sequence of countable sets covering a set with decreasing diameters tending to 0, the set's measure is less than or equal to the limit inferior of the sum of the diameters' measures.
|
Isometry.hausdorffMeasure_image
theorem Isometry.hausdorffMeasure_image :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℝ},
Isometry f →
0 ≤ d ∨ Function.Surjective f →
∀ (s : Set X),
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (f '' s) = ↑↑(MeasureTheory.Measure.hausdorffMeasure d) s
This theorem states that for any two types `X` and `Y` equipped with an eMetricSpace structure, and a function `f` from `X` to `Y`, given that `f` is an isometry and `d` is a real number that is either non-negative or such that `f` is surjective, then for any set `s` of type `X`, the Hausdorff measure of the image of `s` under `f` is equal to the Hausdorff measure of `s` itself. Here, the Hausdorff measure is a particular way of measuring sets in a metric space, and an isometry is a function between metric spaces that preserves distances.
More concisely: For any eMetricSpace structures on types `X` and `Y`, if `f: X → Y` is an isometry, `d ≥ 0` or `f` surjective, then the Hausdorff measure of `f`(`s`) equals the Hausdorff measure of `s` for any set `s` in `X`.
|
MeasureTheory.OuterMeasure.mkMetric'.le_pre
theorem MeasureTheory.OuterMeasure.mkMetric'.le_pre :
∀ {X : Type u_2} [inst : EMetricSpace X] {m : Set X → ENNReal} {r : ENNReal} {μ : MeasureTheory.OuterMeasure X},
μ ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r ↔ ∀ (s : Set X), EMetric.diam s ≤ r → ↑μ s ≤ m s
This theorem states that for any type `X` equipped with an `EMetricSpace` structure, a function `m` from sets of `X` to the extended nonnegative real numbers `ENNReal`, a real number `r`, and an outer measure `μ` on `X`, the outer measure `μ` is less than or equal to the maximal outer measure `MeasureTheory.OuterMeasure.mkMetric'.pre m r`, if and only if for all sets `s` of `X`, if the diameter of `s` (given by `EMetric.diam s`) is less than or equal to `r`, then the measure of `s` under `μ` (given by `↑μ s`) is less than or equal to `m s`. In other words, this theorem provides an equivalence between the inequality of two measures and a property about the diameter of all sets.
More concisely: For any `EMetricSpace` `X` with an `ENNReal-valued` measure `μ` and a function `m` from sets of `X` to `ENNReal`, real number `r`, if `μ(s) ≤ MeasureTheory.OuterMeasure.mkMetric'.pre m r` for all sets `s` with `EMetric.diam s ≤ r`, then `μ ≤ m` as outer measures.
|
MeasureTheory.hausdorffMeasure_segment
theorem MeasureTheory.hausdorffMeasure_segment :
∀ {E : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
[inst_3 : BorelSpace E] (x y : E), ↑↑(MeasureTheory.Measure.hausdorffMeasure 1) (segment ℝ x y) = edist x y
The theorem `MeasureTheory.hausdorffMeasure_segment` states that in a Real normed space, the Hausdorff measure of a segment between two points is equal to the extended distance between those two points. In other words, for any two points in such a space, the Hausdorff measure with dimension parameter 1 of the set of all convex combinations of these two points equals the extended distance between these points.
More concisely: In a Real normed space, the Hausdorff measure of a segment connecting two points equals the extended distance between those points. (Dimenson 1)
|
MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory
theorem MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodory :
∀ {X : Type u_2} [inst : EMetricSpace X] {μ : MeasureTheory.OuterMeasure X},
μ.IsMetric → borel X ≤ μ.caratheodory
The Caratheodory's theorem states that, given a metric outer measure `μ`, any Borel measurable set `t` is Caratheodory measurable. This means for any set `s` (which doesn't necessarily have to be measurable), the measure of the intersection of `s` and `t` plus the measure of the difference between `s` and `t` equals the measure of `s`. The theorem enforces this statement for all types `X` equipped with an instance of an extended metric space.
More concisely: Given a Borel measurable set `t` and a metric outer measure `μ`, for any set `s`, the measure of `s ∩ t` plus the measure of `s \ t` equals the measure of `s` (Caratheodory's theorem).
|
MeasureTheory.Measure.mkMetric_toOuterMeasure
theorem MeasureTheory.Measure.mkMetric_toOuterMeasure :
∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
(m : ENNReal → ENNReal), ↑(MeasureTheory.Measure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m
This theorem states that for any type `X` that is an extended metric space, a measurable space, and a Borel space, and any function `m` from extended nonnegative real numbers to extended nonnegative real numbers, the measure induced by `m` when considered as an outer measure (by applying the outer measure constructor to the measure) is equal to the outer measure directly constructed from `m` using the `MeasureTheory.OuterMeasure.mkMetric` function. In mathematical terms, this theorem asserts that if `m : [0, ∞] → [0, ∞]` is a function, then the measure induced by `m`, when viewed as an outer measure, is the same as the outer measure directly defined from `m`.
More concisely: For any extended real-valued measurable function `m` on an extended metric space `X` that is also a Borel space, the outer measure induced by `m` equals the outer measure constructed directly from `m` using the `MeasureTheory.OuterMeasure.mkMetric` function.
|
MeasureTheory.hausdorffMeasure_real
theorem MeasureTheory.hausdorffMeasure_real : MeasureTheory.Measure.hausdorffMeasure 1 = MeasureTheory.volume := by
sorry
This theorem states that in the space of real numbers (`ℝ`), the Hausdorff measure with parameter 1 (`MeasureTheory.Measure.hausdorffMeasure 1`) is exactly equal to the Lebesgue measure (`MeasureTheory.volume`). In other words, when the dimension parameter for the Hausdorff measure is set to 1, it coincides with the standard measure used in real analysis, the Lebesgue measure.
More concisely: The Hausdorff measure with parameter 1 in the real numbers is equivalent to the Lebesgue measure.
|
HolderOnWith.hausdorffMeasure_image_le
theorem HolderOnWith.hausdorffMeasure_image_le :
∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [inst_2 : MeasurableSpace X]
[inst_3 : BorelSpace X] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {C r : NNReal} {f : X → Y}
{s : Set X},
HolderOnWith C r f s →
0 < r →
∀ {d : ℝ},
0 ≤ d →
↑↑(MeasureTheory.Measure.hausdorffMeasure d) (f '' s) ≤
↑C ^ d * ↑↑(MeasureTheory.Measure.hausdorffMeasure (↑r * d)) s
The theorem states in natural language:
Given a function `f` from `X` to `Y` that is Hölder continuous on a set `s` with a positive real number `r` as an exponent, then the Hausdorff measure (denoted as `μH[d]`) of the image of `s` under `f` is less than or equal to `C` to the power of `d` times the Hausdorff measure of `s` with dimension `r * d`. This holds for any real number `d` that is greater than or equal to zero. Here, `C` is the Hölder constant, `X` and `Y` are eMetric spaces, and `s` is a subset of `X`.
More concisely: For any Hölder continuous function `f` from a subset `s` of an eMetric space `X` to another eMetric space `Y` with exponent `r` and Hausdorff measure `μH[d](s)`, the Hausdorff measure `μH[d](f[s])` of the image `f[s]` is bounded above by `C^d * μH[r*d](s)`, where `C` is the Hölder constant.
|