Densities, essential interior and essential boundary

Let μ be a measure on a metric space. A set s has density d at x (TauCeti.HasDensityAt μ s x d) when the proportion μ (s ∩ closedBall x r) / μ (closedBall x r) of s in closed balls around x tends to d as r → 0⁺. The points of density one form the essential interior TauCeti.essentialInterior μ s, those of density zero the essential exterior TauCeti.essentialExterior μ s, and the points of neither kind the essential boundary TauCeti.essentialBoundary μ s. For Lebesgue measure these are the sets E⁽¹⁾, E⁽⁰⁾ and ∂ᵉE of the theory of sets of finite perimeter.

All three sets depend only on the μ-a.e. class of s, unlike the topological interior and frontier. They are nevertheless comparable to them: for a locally finite measure that charges every open set, interior s ⊆ essentialInterior μ s ⊆ closure s and essentialBoundary μ s ⊆ frontier s. For such a measure and a null-measurable set s, complements exchange the essential interior and exterior, so the essential boundary of sᶜ is that of s. The essential boundary of a union of any two sets lies in the union of their essential boundaries; the same holds for an intersection of two sets one of which is null-measurable, for any measure.

For a locally finite measure on a second-countable metric space with its Borel σ-algebra and the Besicovitch covering property, such as a finite-dimensional real normed space, Lebesgue's density theorem shows that the essential interior of a null-measurable set s agrees with s almost everywhere and the essential boundary is null. The essential interior is thus a canonical representative of the a.e. class of s.

For an additive Haar measure on a finite-dimensional real normed space of dimension n, a set filling a proportion r ^ n ≤ c μ(s ∩ ball x r) of every small ball around x does not have density zero at x.

Main declarations

• TauCeti.HasDensityAt μ s x d: the set s has density d at x with respect to μ.
• TauCeti.essentialInterior, TauCeti.essentialExterior, TauCeti.essentialBoundary.
• TauCeti.essentialInterior_congr_ae and its companions: invariance under null modification.
• TauCeti.essentialInterior_compl and TauCeti.essentialBoundary_compl: complements.
• TauCeti.essentialBoundary_union_subset and TauCeti.essentialBoundary_inter_subset.
• TauCeti.essentialInterior_preimage_add_right and its companions: for a translation-invariant measure, the three sets commute with translations.
• TauCeti.interior_subset_essentialInterior, TauCeti.essentialInterior_subset_closure and TauCeti.essentialBoundary_subset_frontier: comparison with the topological notions.
• TauCeti.essentialInterior_ae_eq and TauCeti.measure_essentialBoundary: Lebesgue's density theorem.
• TauCeti.not_hasDensityAt_zero_of_eventually_ofReal_pow_le_mul_measure_inter_ball: a lower volume density bound against a Haar measure rules out density zero.

References

• F. Maggi, Sets of Finite Perimeter and Geometric Variational Problems, §5.4 and §16.1.
• L. C. Evans and R. F. Gariepy, Measure Theory and Fine Properties of Functions, §1.7 and §5.8.

def TauCeti.HasDensityAt {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) (x : α) (d : ENNReal) : Prop

The set s has density d at x with respect to μ: the proportion μ (s ∩ closedBall x r) / μ (closedBall x r) of s in the closed ball of radius r around x tends to d as r → 0⁺.

theorem TauCeti.hasDensityAt_iff {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} {d : ENNReal} : HasDensityAt μ s x d ↔ Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)

theorem TauCeti.HasDensityAt.unique {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} {d d' : ENNReal} (h : HasDensityAt μ s x d) (h' : HasDensityAt μ s x d') : d = d'

A density is unique.

theorem TauCeti.HasDensityAt.le_one {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} {d : ENNReal} (h : HasDensityAt μ s x d) : d ≤ 1

A density is at most one.

theorem TauCeti.HasDensityAt.congr_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {x : α} {d : ENNReal} (h : HasDensityAt μ s x d) (hst : s =ᵐ[μ] t) : HasDensityAt μ t x d

Densities only depend on the set up to μ-null sets.

theorem TauCeti.HasDensityAt.eventually_measure_closedBall_ne_zero_ne_top {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} {d : ENNReal} (h : HasDensityAt μ s x d) (hd : d ≠ 0) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.closedBall x r) ≠ 0 ∧ μ (Metric.closedBall x r) ≠ ⊤

A positive density forces closed balls of small positive radius around the point to have positive finite measure: otherwise the proportions vanish.

theorem TauCeti.HasDensityAt.compl {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} {d : ENNReal} (hs : MeasureTheory.NullMeasurableSet s μ) (hx : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (Metric.closedBall x r) ≠ 0 ∧ μ (Metric.closedBall x r) ≠ ⊤) (h : HasDensityAt μ s x d) : HasDensityAt μ sᶜ x (1 - d)

Complements. If a null-measurable set s has density d at x, then sᶜ has density 1 - d there, provided closed balls of small positive radius around x have positive finite measure. This holds at every point for a locally finite measure that charges every open set (Metric.eventually_measure_closedBall_ne_zero_ne_top).

theorem TauCeti.hasDensityAt_congr_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {x : α} {d : ENNReal} (hst : s =ᵐ[μ] t) : HasDensityAt μ s x d ↔ HasDensityAt μ t x d

Densities only depend on the set up to μ-null sets.

Essential interior, exterior and boundary

def TauCeti.essentialInterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : Set α

The essential interior of s with respect to μ: the points at which s has density one. For Lebesgue measure this is the set E⁽¹⁾ of points of density one of E.

def TauCeti.essentialExterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : Set α

The essential exterior of s with respect to μ: the points at which s has density zero. For Lebesgue measure this is the set E⁽⁰⁾ of points of density zero of E.

def TauCeti.essentialBoundary {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : Set α

The essential boundary of s with respect to μ: the points at which s has neither density one nor density zero. This is the measure-theoretic boundary ∂ᵉE, which ignores modifications of E by null sets.

@[simp]

theorem TauCeti.mem_essentialInterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} : x ∈ essentialInterior μ s ↔ HasDensityAt μ s x 1

@[simp]

theorem TauCeti.mem_essentialExterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} : x ∈ essentialExterior μ s ↔ HasDensityAt μ s x 0

@[simp]

theorem TauCeti.mem_essentialBoundary {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {x : α} : x ∈ essentialBoundary μ s ↔ x ∉ essentialInterior μ s ∧ x ∉ essentialExterior μ s

theorem TauCeti.essentialBoundary_def {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : essentialBoundary μ s = (essentialInterior μ s ∪ essentialExterior μ s)ᶜ

theorem TauCeti.disjoint_essentialInterior_essentialExterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : Disjoint (essentialInterior μ s) (essentialExterior μ s)

The essential interior and the essential exterior are disjoint.

theorem TauCeti.essentialInterior_congr_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s =ᵐ[μ] t) : essentialInterior μ s = essentialInterior μ t

The essential interior is invariant under modification of the set by null sets.

theorem TauCeti.essentialExterior_congr_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s =ᵐ[μ] t) : essentialExterior μ s = essentialExterior μ t

The essential exterior is invariant under modification of the set by null sets.

theorem TauCeti.essentialBoundary_congr_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s =ᵐ[μ] t) : essentialBoundary μ s = essentialBoundary μ t

The essential boundary is invariant under modification of the set by null sets.

Monotonicity, unions and intersections

theorem TauCeti.essentialInterior_mono_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ≤ᵐ[μ] t) : essentialInterior μ s ⊆ essentialInterior μ t

The essential interior is monotone, up to null sets.

theorem TauCeti.essentialInterior_mono {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ⊆ t) : essentialInterior μ s ⊆ essentialInterior μ t

The essential interior is monotone.

theorem TauCeti.essentialExterior_anti_ae {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ≤ᵐ[μ] t) : essentialExterior μ t ⊆ essentialExterior μ s

The essential exterior is antitone, up to null sets.

theorem TauCeti.essentialExterior_anti {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (h : s ⊆ t) : essentialExterior μ t ⊆ essentialExterior μ s

The essential exterior is antitone.

@[simp]

theorem TauCeti.essentialExterior_union {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} : essentialExterior μ (s ∪ t) = essentialExterior μ s ∩ essentialExterior μ t

A point is in the essential exterior of a union exactly when it is in the essential exterior of both sets.

theorem TauCeti.essentialBoundary_union_subset {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} : essentialBoundary μ (s ∪ t) ⊆ essentialBoundary μ s ∪ essentialBoundary μ t

The essential boundary of a union lies in the union of the essential boundaries.

@[simp]

theorem TauCeti.essentialInterior_inter {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : essentialInterior μ (s ∩ t) = essentialInterior μ s ∩ essentialInterior μ t

A point is in the essential interior of an intersection with a null-measurable set exactly when it is in the essential interior of both sets.

theorem TauCeti.essentialBoundary_inter_subset {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : essentialBoundary μ (s ∩ t) ⊆ essentialBoundary μ s ∪ essentialBoundary μ t

The essential boundary of an intersection with a null-measurable set lies in the union of the essential boundaries.

@[simp]

theorem TauCeti.essentialInterior_compl {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : MeasureTheory.NullMeasurableSet s μ) : essentialInterior μ sᶜ = essentialExterior μ s

The essential interior of the complement of a null-measurable set is its essential exterior.

@[simp]

theorem TauCeti.essentialExterior_compl {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : MeasureTheory.NullMeasurableSet s μ) : essentialExterior μ sᶜ = essentialInterior μ s

The essential exterior of the complement of a null-measurable set is its essential interior.

@[simp]

theorem TauCeti.essentialBoundary_compl {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (hs : MeasureTheory.NullMeasurableSet s μ) : essentialBoundary μ sᶜ = essentialBoundary μ s

A null-measurable set and its complement have the same essential boundary.

Comparison with the topological interior and frontier

theorem TauCeti.compl_closure_subset_essentialExterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : (closure s)ᶜ ⊆ essentialExterior μ s

A point outside the closure of s is in its essential exterior.

theorem TauCeti.essentialInterior_subset_closure {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} : essentialInterior μ s ⊆ closure s

The essential interior of s lies in its closure.

theorem TauCeti.interior_subset_essentialInterior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] : interior s ⊆ essentialInterior μ s

An interior point of s is in its essential interior, for a locally finite measure that charges every open set.

theorem TauCeti.essentialExterior_subset_compl_interior {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] : essentialExterior μ s ⊆ (interior s)ᶜ

The essential exterior of s lies in the complement of its interior.

theorem TauCeti.essentialBoundary_subset_frontier {α : Type u_1} [PseudoMetricSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] : essentialBoundary μ s ⊆ frontier s

The essential boundary lies in the topological frontier, for a locally finite measure that charges every open set.

Translations

@[simp]

theorem TauCeti.hasDensityAt_preimage_add_right {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [MeasurableAdd E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} {x h : E} {d : ENNReal} : HasDensityAt μ ((fun (x : E) => x + h) ⁻¹' s) x d ↔ HasDensityAt μ s (x + h) d

For a translation-invariant measure, the density of the translate (· + h) ⁻¹' s at x is the density of s at x + h.

@[simp]

theorem TauCeti.essentialInterior_preimage_add_right {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [MeasurableAdd E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} {h : E} : essentialInterior μ ((fun (x : E) => x + h) ⁻¹' s) = (fun (x : E) => x + h) ⁻¹' essentialInterior μ s

For a translation-invariant measure, the essential interior commutes with translations.

@[simp]

theorem TauCeti.essentialExterior_preimage_add_right {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [MeasurableAdd E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} {h : E} : essentialExterior μ ((fun (x : E) => x + h) ⁻¹' s) = (fun (x : E) => x + h) ⁻¹' essentialExterior μ s

For a translation-invariant measure, the essential exterior commutes with translations.

@[simp]

theorem TauCeti.essentialBoundary_preimage_add_right {E : Type u_1} [SeminormedAddCommGroup E] [MeasurableSpace E] [MeasurableAdd E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] {s : Set E} {h : E} : essentialBoundary μ ((fun (x : E) => x + h) ⁻¹' s) = (fun (x : E) => x + h) ⁻¹' essentialBoundary μ s

For a translation-invariant measure, the essential boundary commutes with translations.

Lebesgue's density theorem

theorem TauCeti.ae_hasDensityAt_indicator {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : ∀ᵐ (x : α) ∂μ, HasDensityAt μ s x (s.indicator 1 x)

Lebesgue's density theorem. At almost every point a null-measurable set has density one or zero, according to whether the point lies in the set.

theorem TauCeti.essentialInterior_ae_eq {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : essentialInterior μ s =ᵐ[μ] s

Lebesgue's density theorem. A null-measurable set agrees almost everywhere with its essential interior.

theorem TauCeti.essentialExterior_ae_eq {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : essentialExterior μ s =ᵐ[μ] sᶜ

Lebesgue's density theorem. The essential exterior of a null-measurable set agrees almost everywhere with its complement.

theorem TauCeti.measure_essentialBoundary {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : μ (essentialBoundary μ s) = 0

Lebesgue's density theorem. The essential boundary of a null-measurable set is null.

@[simp]

theorem TauCeti.essentialInterior_essentialInterior {α : Type u_1} [MetricSpace α] [MeasurableSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasureTheory.NullMeasurableSet s μ) : essentialInterior μ (essentialInterior μ s) = essentialInterior μ s

The essential interior is idempotent: it is a canonical representative of the a.e. class of a null-measurable set.

Lower volume density bounds for Haar measures

theorem TauCeti.not_hasDensityAt_zero_of_eventually_ofReal_pow_le_mul_measure_inter_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E} {x : E} {c : ENNReal} (hc : c ≠ ⊤) (h : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ENNReal.ofReal (r ^ Module.finrank ℝ E) ≤ c * μ (s ∩ Metric.ball x r)) : ¬HasDensityAt μ s x 0

Against an additive Haar measure on a space of dimension n, a set filling a proportion ofReal (r ^ n) ≤ c μ(s ∩ ball x r), c ≠ ∞, of every small ball around x does not have density zero at x.