Documentation

Mathlib.MeasureTheory.Measure.OpenPos

Measures positive on nonempty opens #

In this file we define a typeclass for measures that are positive on nonempty opens, see MeasureTheory.Measure.IsOpenPosMeasure. Examples include (additive) Haar measures, as well as measures that have positive density with respect to a Haar measure. We also prove some basic facts about these measures.

A measure is said to be IsOpenPosMeasure if it is positive on nonempty open sets.

Instances
    theorem IsOpen.measure_pos {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.IsOpenPosMeasure μ] {U : Set X} (hU : IsOpen U) (hne : Set.Nonempty U) :
    0 < μ U
    theorem IsOpen.eq_empty_of_measure_zero {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.IsOpenPosMeasure μ] {U : Set X} (hU : IsOpen U) (h₀ : μ U = 0) :
    U =

    An open null set w.r.t. an IsOpenPosMeasure is empty.

    A null set has empty interior.

    If two functions are a.e. equal on an open set and are continuous on this set, then they are equal on this set.

    theorem MeasureTheory.Measure.eq_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.IsOpenPosMeasure μ] {f : XY} {g : XY} (h : f =ᶠ[MeasureTheory.Measure.ae μ] g) (hf : Continuous f) (hg : Continuous g) :
    f = g

    If two continuous functions are a.e. equal, then they are equal.

    theorem Metric.measure_ball_pos {X : Type u_1} [PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.IsOpenPosMeasure μ] (x : X) {r : } (hr : 0 < r) :
    0 < μ (Metric.ball x r)

    Meagre sets and measure zero #

    In general, neither of meagre and measure zero implies the other.

    However, with respect to a measure which is positive on non-empty open sets, closed measure zero sets are nowhere dense and σ-compact measure zero sets in a Hausdorff space are meagre.

    A closed measure zero subset is nowhere dense. (Closedness is required: for instance, the rational numbers are countable (thus have measure zero), but are dense (hence not nowhere dense).

    A σ-compact measure zero subset is meagre. (More generally, every Fσ set of measure zero is meagre.)