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.

  • open_pos : ∀ (U : Set X), IsOpen UU.Nonemptyμ U 0
Instances
    theorem MeasureTheory.Measure.IsOpenPosMeasure.open_pos {X : Type u_1} :
    ∀ {inst : TopologicalSpace X} {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [self : μ.IsOpenPosMeasure] (U : Set X), IsOpen UU.Nonemptyμ U 0
    theorem IsOpen.measure_ne_zero {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) (hne : U.Nonempty) :
    μ U 0
    theorem IsOpen.measure_pos {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) (hne : U.Nonempty) :
    0 < μ U
    @[instance 100]
    instance MeasureTheory.Measure.instNeZeroOfNonempty {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [Nonempty X] :
    Equations
    • =
    theorem IsOpen.measure_pos_iff {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) :
    0 < μ U U.Nonempty
    theorem IsOpen.measure_eq_zero_iff {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) :
    μ U = 0 U =
    theorem MeasureTheory.Measure.measure_pos_of_nonempty_interior {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {s : Set X} (h : (interior s).Nonempty) :
    0 < μ s
    theorem MeasureTheory.Measure.measure_pos_of_mem_nhds {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {s : Set X} {x : X} (h : s nhds x) :
    0 < μ s
    theorem MeasureTheory.Measure.isOpenPosMeasure_smul {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {c : ENNReal} (h : c 0) :
    (c μ).IsOpenPosMeasure
    theorem MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] (h : μ.AbsolutelyContinuous ν) :
    ν.IsOpenPosMeasure
    theorem LE.le.isOpenPosMeasure {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] (h : μ ν) :
    ν.IsOpenPosMeasure
    theorem IsOpen.measure_zero_iff_eq_empty {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) :
    μ U = 0 U =
    theorem IsOpen.ae_eq_empty_iff_eq {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) :
    theorem IsOpen.eq_empty_of_measure_zero {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {U : Set X} (hU : IsOpen U) (h₀ : μ U = 0) :
    U =

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

    theorem IsClosed.ae_eq_univ_iff_eq {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {F : Set X} (hF : IsClosed F) :
    F =ᵐ[μ] Set.univ F = Set.univ
    theorem IsClosed.measure_eq_univ_iff_eq {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {F : Set X} [OpensMeasurableSpace X] [MeasureTheory.IsFiniteMeasure μ] (hF : IsClosed F) :
    μ F = μ Set.univ F = Set.univ
    theorem IsClosed.measure_eq_one_iff_eq_univ {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {F : Set X} [OpensMeasurableSpace X] [MeasureTheory.IsProbabilityMeasure μ] (hF : IsClosed F) :
    μ F = 1 F = Set.univ
    theorem MeasureTheory.Measure.interior_eq_empty_of_null {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s : Set X} (hs : μ s = 0) :

    A null set has empty interior.

    theorem MeasureTheory.Measure.dense_of_ae {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {p : XProp} (hp : ∀ᵐ (x : X) ∂μ, p x) :
    Dense {x : X | p x}

    A property satisfied almost everywhere is satisfied on a dense subset.

    theorem MeasureTheory.Measure.eqOn_open_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {U : Set X} {f : XY} {g : XY} (h : f =ᵐ[μ.restrict U] g) (hU : IsOpen U) (hf : ContinuousOn f U) (hg : ContinuousOn g U) :
    Set.EqOn f g 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} [μ.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 MeasureTheory.Measure.eqOn_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] {s : Set X} {f : XY} {g : XY} (h : f =ᵐ[μ.restrict s] g) (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hU : s closure (interior s)) :
    Set.EqOn f g s
    theorem Continuous.ae_eq_iff_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {f : XY} {g : XY} (hf : Continuous f) (hg : Continuous g) :
    f =ᵐ[μ] g f = g
    theorem Continuous.isOpenPosMeasure_map {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [OpensMeasurableSpace X] {Z : Type u_3} [TopologicalSpace Z] [MeasurableSpace Z] [BorelSpace Z] {f : XZ} (hf : Continuous f) (hf_surj : Function.Surjective f) :
    (MeasureTheory.Measure.map f μ).IsOpenPosMeasure
    theorem MeasureTheory.Measure.measure_Ioi_pos {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [NoMaxOrder X] (a : X) :
    0 < μ (Set.Ioi a)
    theorem MeasureTheory.Measure.measure_Iio_pos {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [NoMinOrder X] (a : X) :
    0 < μ (Set.Iio a)
    theorem MeasureTheory.Measure.measure_Ioo_pos {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a : X} {b : X} :
    0 < μ (Set.Ioo a b) a < b
    theorem MeasureTheory.Measure.measure_Ioo_eq_zero {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a : X} {b : X} :
    μ (Set.Ioo a b) = 0 b a
    theorem MeasureTheory.Measure.eqOn_Ioo_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {a : X} {b : X} {f : XY} {g : XY} (hfg : f =ᵐ[μ.restrict (Set.Ioo a b)] g) (hf : ContinuousOn f (Set.Ioo a b)) (hg : ContinuousOn g (Set.Ioo a b)) :
    Set.EqOn f g (Set.Ioo a b)
    theorem MeasureTheory.Measure.eqOn_Ioc_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a : X} {b : X} {f : XY} {g : XY} (hfg : f =ᵐ[μ.restrict (Set.Ioc a b)] g) (hf : ContinuousOn f (Set.Ioc a b)) (hg : ContinuousOn g (Set.Ioc a b)) :
    Set.EqOn f g (Set.Ioc a b)
    theorem MeasureTheory.Measure.eqOn_Ico_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a : X} {b : X} {f : XY} {g : XY} (hfg : f =ᵐ[μ.restrict (Set.Ico a b)] g) (hf : ContinuousOn f (Set.Ico a b)) (hg : ContinuousOn g (Set.Ico a b)) :
    Set.EqOn f g (Set.Ico a b)
    theorem MeasureTheory.Measure.eqOn_Icc_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} [TopologicalSpace Y] [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [DenselyOrdered X] {a : X} {b : X} (hne : a b) {f : XY} {g : XY} (hfg : f =ᵐ[μ.restrict (Set.Icc a b)] g) (hf : ContinuousOn f (Set.Icc a b)) (hg : ContinuousOn g (Set.Icc a b)) :
    Set.EqOn f g (Set.Icc a b)
    theorem Metric.measure_ball_pos {X : Type u_1} [PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : } (hr : 0 < r) :
    0 < μ (Metric.ball x r)
    theorem Metric.measure_closedBall_pos {X : Type u_1} [PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : } (hr : 0 < r) :
    0 < μ (Metric.closedBall x r)

    See also Metric.measure_closedBall_pos_iff.

    @[simp]
    theorem Metric.measure_closedBall_pos_iff {X : Type u_2} [MetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] [MeasureTheory.NoAtoms μ] {x : X} {r : } :
    0 < μ (Metric.closedBall x r) 0 < r
    theorem EMetric.measure_ball_pos {X : Type u_1} [PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : ENNReal} (hr : r 0) :
    0 < μ (EMetric.ball x r)
    theorem EMetric.measure_closedBall_pos {X : Type u_1} [PseudoEMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] (x : X) {r : ENNReal} (hr : r 0) :

    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.

    theorem IsNowhereDense.of_isClosed_null {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] (h₁s : IsClosed s) (h₂s : μ s = 0) :

    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).

    theorem IsMeagre.of_isSigmaCompact_null {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure] [T2Space X] (h₁s : IsSigmaCompact s) (h₂s : μ s = 0) :

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