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.

    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

    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 =ᶠ[ μ] 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)