Dimensional densities

This file defines dimensional density ratios and their upper and lower limits, then proves their basic order-theoretic properties.

noncomputable def dimensionalDensityRatio {X : Type u_1} [PseudoEMetricSpace X] (μ : MeasureTheory.OuterMeasure X) (s : ℝ) (x : X) (r : ℝ) : ENNReal

The s-density ratio of an outer measure μ at point x with radius r: μ(B̄(x, r)) / (2r) ^ s.

The closed ball is taken in the extended-distance sense, Metric.closedEBall x (ofReal r), so that the definition makes sense in a PseudoEMetricSpace. For 0 ≤ r in a (pseudo) metric space this is the usual closed ball Metric.closedBall x r, by Metric.closedEBall_ofReal.

Equations

• dimensionalDensityRatio μ s x r = μ (Metric.closedEBall x (ENNReal.ofReal r)) / ENNReal.ofReal ((2 * r) ^ s)

noncomputable def dimensionalUpperDensity {X : Type u_1} [PseudoEMetricSpace X] (μ : MeasureTheory.OuterMeasure X) (s : ℝ) (x : X) : ENNReal

Upper s-density of μ at x: limsup_{r → 0⁺} μ(B̄(x, r)) / (2r) ^ s.

Equations

• dimensionalUpperDensity μ s x = Filter.limsup (dimensionalDensityRatio μ s x) (nhdsWithin 0 (Set.Ioi 0))

noncomputable def dimensionalLowerDensity {X : Type u_1} [PseudoEMetricSpace X] (μ : MeasureTheory.OuterMeasure X) (s : ℝ) (x : X) : ENNReal

Lower s-density of μ at x: liminf_{r → 0⁺} μ(B̄(x, r)) / (2r) ^ s.

Equations

• dimensionalLowerDensity μ s x = Filter.liminf (dimensionalDensityRatio μ s x) (nhdsWithin 0 (Set.Ioi 0))

class HasDensity {X : Type u_1} [PseudoEMetricSpace X] (μ : MeasureTheory.OuterMeasure X) (s : ℝ) (x : X) : Prop

The s-dimensional density of μ at x exists if the density ratio converges as r → 0⁺.

• exists_tendsto : ∃ (y : ENNReal), Filter.Tendsto (dimensionalDensityRatio μ s x) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)

noncomputable def dimensionalDensity {X : Type u_1} [PseudoEMetricSpace X] (μ : MeasureTheory.OuterMeasure X) (s : ℝ) (x : X) : ENNReal

The s-dimensional density of μ at x (Definition 1.5).

When the limit exists (HasDensity μ s x), this equals lim_{r → 0⁺} μ(B̄(x, r)) / (2r) ^ s. When the limit does not exist, this returns a junk value.

Equations

• dimensionalDensity μ s x = sInf {y : ENNReal | Filter.Tendsto (dimensionalDensityRatio μ s x) (nhdsWithin 0 (Set.Ioi 0)) (nhds y)}

theorem lower_le_upper_density {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) : dimensionalLowerDensity μ s x ≤ dimensionalUpperDensity μ s x

Comparison between lower and upper density: Θ_*^s(μ, x) ≤ Θ^{*s}(μ, x).

theorem lower_density_nonneg {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) : 0 ≤ dimensionalLowerDensity μ s x

Non-negativity of lower density: 0 ≤ Θ_*^s(μ, x).

theorem upper_density_nonneg {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) : 0 ≤ dimensionalUpperDensity μ s x

Non-negativity of upper density: 0 ≤ Θ^{*s}(μ, x).

theorem density_exists_of_lower_eq_upper {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (h : dimensionalLowerDensity μ s x = dimensionalUpperDensity μ s x) : HasDensity μ s x

If the lower and upper densities are equal, then the density limit exists.

Uses tendsto_of_liminf_eq_limsup from Mathlib, which directly gives convergence when liminf = limsup in a conditionally complete linear order with order topology (which ℝ≥0∞ satisfies).

theorem upper_density_ge_of_lower_density_ge {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : α ≤ dimensionalLowerDensity μ s x) : α ≤ dimensionalUpperDensity μ s x

Lemma 2.4: If Θ_*^s(μ, x) ≥ α, then Θ^{*s}(μ, x) ≥ α.

theorem lower_density_le_of_upper_density_le {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : dimensionalUpperDensity μ s x ≤ α) : dimensionalLowerDensity μ s x ≤ α

Lemma 2.5: If Θ^{s}(μ, x) ≤ α, then Θ_^s(μ, x) ≤ α.

theorem eventually_gt_of_lower_density_gt {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : α < dimensionalLowerDensity μ s x) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), α < dimensionalDensityRatio μ s x r

Lemma 2.6: If Θ_*^s(μ, x) > α, then eventually (for small enough r > 0) the density ratio is > α.

theorem eventually_lt_of_upper_density_lt {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : dimensionalUpperDensity μ s x < α) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), dimensionalDensityRatio μ s x r < α

Lemma 2.7: If Θ^{*s}(μ, x) < α, then eventually (for small enough r > 0) the density ratio is < α.

theorem frequently_lt_of_lower_density_lt {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : dimensionalLowerDensity μ s x < α) : ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), dimensionalDensityRatio μ s x r < α

Lemma 2.8: If Θ_*^s(μ, x) < α, then frequently (along r → 0⁺) the density ratio is < α.

theorem frequently_gt_of_upper_density_gt {X : Type u_1} [PseudoEMetricSpace X] {μ : MeasureTheory.OuterMeasure X} (s : ℝ) (x : X) (α : ENNReal) (h : α < dimensionalUpperDensity μ s x) : ∃ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), α < dimensionalDensityRatio μ s x r

Lemma 2.9: If Θ^{*s}(μ, x) > α, then frequently (along r → 0⁺) the density ratio is > α.

theorem dimensional_density_ratio_closedBall {Y : Type u_2} [PseudoMetricSpace Y] (ν : MeasureTheory.OuterMeasure Y) (s : ℝ) (x : Y) {r : ℝ} (hr : 0 ≤ r) : dimensionalDensityRatio ν s x r = ν (Metric.closedBall x r) / ENNReal.ofReal ((2 * r) ^ s)

In a (pseudo) metric space, and for a nonnegative radius, the density ratio is computed with the usual closed ball.