Consequences of positivity on open sets

Mathlib's Metric.measure_ball_pos says that a measure positive on nonempty open sets gives positive measure to every ball of positive radius. In a proper space, where balls are bounded and so have finite measure under a measure finite on compact sets, the same holds for the real-valued measure μ.real, and likewise for closed balls. For a locally finite measure, closed balls of small positive radius around a point have positive finite measure, so proportions of sets in shrinking balls are well behaved. Since a property holding almost everywhere holds on a dense set, an almost everywhere inequality between continuous functions holds everywhere.

An almost-everywhere inclusion of an open set in another set implies inclusion in its closure. In particular, two almost-everywhere equal open sets have the same closure. Taking interiors then shows that regular open sets are determined by their almost-everywhere classes. Likewise a continuous function on the closure of an open set is determined by its values almost everywhere on the set.

On a discrete space, such a measure charges every point, so the only null set is empty and almost everywhere means everywhere.

Main results

• IsOpen.subset_closure_of_ae_le: an open set lies in the closure of any set containing it a.e.
• IsOpen.closure_eq_of_ae_eq: a.e. equal open sets have equal closures.
• IsOpen.ext_closure_of_ae_eq: a continuous function on the closure of an open set is determined by its values at almost every point of the set.
• TauCeti.eq_of_ae_eq_of_interior_closure_eq: a.e. equal regular open sets are equal.
• Metric.measureReal_ball_pos: a ball of positive radius has positive real measure.
• Metric.measureReal_closedBall_pos: a closed ball of positive radius has positive real measure.
• Metric.eventually_measure_closedBall_ne_zero_ne_top: closed balls of small positive radius have positive finite measure.
• MeasureTheory.Measure.restrict_closedBall_ne_zero_of_mul_le: a closed ball of positive radius in which a set has positive density charges the restriction of the measure to that set.
• Continuous.ae_le_iff_le: continuous functions satisfy f ≤ᵐ[μ] g if and only if f ≤ g.
• MeasureTheory.ae_eq_top_of_discreteTopology: on a discrete space, for a measure positive on open sets, almost everywhere means everywhere.

theorem IsOpen.subset_closure_of_ae_le {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s t : Set X} (hs : IsOpen s) (hst : s ≤ᵐ[μ] t) : s ⊆ closure t

An open set contained almost everywhere in another set is contained in its closure. No measurability assumption on either set is needed.

theorem IsOpen.closure_eq_of_ae_eq {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s t : Set X} (hs : IsOpen s) (ht : IsOpen t) (hst : s =ᵐ[μ] t) : closure s = closure t

Almost-everywhere equal open sets have the same closure for a measure positive on nonempty open sets. The open sets themselves need not be equal.

theorem IsOpen.ext_closure_of_ae_eq {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] {U : Set X} (hU : IsOpen U) {f g : ↑(closure U) → Y} (hf : Continuous f) (hg : Continuous g) (h : ∀ᵐ (x : X) ∂μ, ∀ (hx : x ∈ U), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩) : f = g

A continuous function on the closure of an open set U is determined by its values at almost every point of U, for a measure which charges every nonempty open set.

theorem TauCeti.eq_of_ae_eq_of_interior_closure_eq {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s t : Set X} (hs : interior (closure s) = s) (ht : interior (closure t) = t) (hst : s =ᵐ[μ] t) : s = t

Regular open sets are determined by their almost-everywhere classes for a measure positive on nonempty open sets. Regular openness is expressed by interior (closure s) = s; ordinary openness alone does not suffice.

theorem Metric.measureReal_ball_pos {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ.real (ball x r)

In a proper space, a measure that is positive on nonempty open sets and finite on compact sets gives every ball of positive radius positive real measure.

theorem Metric.measureReal_closedBall_pos {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ.real (closedBall x r)

In a proper space, a measure that is positive on nonempty open sets and finite on compact sets gives every closed ball of positive radius positive real measure.

theorem Metric.eventually_measure_closedBall_ne_zero_ne_top {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (x : X) : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), μ (closedBall x r) ≠ 0 ∧ μ (closedBall x r) ≠ ⊤

For a locally finite measure that is positive on nonempty open sets, closed balls of small positive radius around a point have positive finite measure.

theorem MeasureTheory.Measure.restrict_closedBall_ne_zero_of_mul_le {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) [μ.IsOpenPosMeasure] {s : Set X} {c : NNReal} {y : X} {ε : ℝ} (hc : 0 < c) (hε : 0 < ε) (hd : ↑c * μ (Metric.closedBall y ε) ≤ μ (Metric.closedBall y ε ∩ s)) : (μ.restrict s) (Metric.closedBall y ε) ≠ 0

A closed ball in which a set s has density at least c > 0, in the sense that c μ(closedBall y ε) ≤ μ(closedBall y ε ∩ s), charges μ.restrict s.

theorem Continuous.ae_le_iff_le {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [TopologicalSpace Y] [Preorder Y] [OrderClosedTopology Y] {f g : X → Y} (hf : Continuous f) (hg : Continuous g) : f ≤ᵐ[μ] g ↔ f ≤ g

Under a measure positive on nonempty open sets, an almost everywhere inequality between continuous functions into an order-closed space holds everywhere.

theorem MeasureTheory.ae_eq_top_of_discreteTopology {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] [MeasurableSpace α] (μ : Measure α) [μ.IsOpenPosMeasure] : ae μ = ⊤

On a discrete space, a measure positive on nonempty open sets charges every point, so almost everywhere means everywhere.