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

class MeasureTheory.Measure.IsOpenPosMeasure {X : Type u_1} [] {m : } (μ : ) :

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

• open_pos : ∀ (U : Set X), U.Nonemptyμ U 0
Instances
theorem MeasureTheory.Measure.IsOpenPosMeasure.open_pos {X : Type u_1} [] {m : } {μ : } [self : μ.IsOpenPosMeasure] (U : Set X) :
U.Nonemptyμ U 0
theorem IsOpen.measure_ne_zero {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {U : Set X} (hU : ) (hne : U.Nonempty) :
μ U 0
theorem IsOpen.measure_pos {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {U : Set X} (hU : ) (hne : U.Nonempty) :
0 < μ U
@[instance 100]
instance MeasureTheory.Measure.instNeZeroOfNonempty {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] [] :
Equations
• =
theorem IsOpen.measure_pos_iff {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {U : Set X} (hU : ) :
0 < μ U U.Nonempty
theorem IsOpen.measure_eq_zero_iff {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {U : Set X} (hU : ) :
μ U = 0 U =
theorem MeasureTheory.Measure.measure_pos_of_nonempty_interior {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {s : Set X} (h : ().Nonempty) :
0 < μ s
theorem MeasureTheory.Measure.measure_pos_of_mem_nhds {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {s : Set X} {x : X} (h : s nhds x) :
0 < μ s
theorem MeasureTheory.Measure.isOpenPosMeasure_smul {X : Type u_1} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {c : ENNReal} (h : c 0) :
(c μ).IsOpenPosMeasure
theorem MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure {X : Type u_1} [] {m : } {μ : } {ν : } [μ.IsOpenPosMeasure] (h : μ.AbsolutelyContinuous ν) :
ν.IsOpenPosMeasure
theorem LE.le.isOpenPosMeasure {X : Type u_1} [] {m : } {μ : } {ν : } [μ.IsOpenPosMeasure] (h : μ ν) :
ν.IsOpenPosMeasure
theorem IsOpen.measure_zero_iff_eq_empty {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {U : Set X} (hU : ) :
μ U = 0 U =
theorem IsOpen.ae_eq_empty_iff_eq {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {U : Set X} (hU : ) :
theorem IsOpen.eq_empty_of_measure_zero {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {U : Set X} (hU : ) (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} [] {m : } {μ : } [μ.IsOpenPosMeasure] {F : Set X} (hF : ) :
F =ᵐ[μ] Set.univ F = Set.univ
theorem IsClosed.measure_eq_univ_iff_eq {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {F : Set X} (hF : ) :
μ F = μ Set.univ F = Set.univ
theorem IsClosed.measure_eq_one_iff_eq_univ {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {F : Set X} (hF : ) :
μ F = 1 F = Set.univ
theorem MeasureTheory.Measure.interior_eq_empty_of_null {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {s : Set X} (hs : μ s = 0) :

A null set has empty interior.

theorem MeasureTheory.Measure.eqOn_open_of_ae_eq {X : Type u_1} {Y : Type u_2} [] {m : } [] [] {μ : } [μ.IsOpenPosMeasure] {U : Set X} {f : XY} {g : XY} (h : f =ᵐ[μ.restrict U] g) (hU : ) (hf : ) (hg : ) :
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} [] {m : } [] [] {μ : } [μ.IsOpenPosMeasure] {f : XY} {g : XY} (h : f =ᵐ[μ] g) (hf : ) (hg : ) :
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} [] {m : } [] [] {μ : } [μ.IsOpenPosMeasure] {s : Set X} {f : XY} {g : XY} (h : f =ᵐ[μ.restrict s] g) (hf : ) (hg : ) (hU : s closure ()) :
Set.EqOn f g s
theorem Continuous.ae_eq_iff_eq {X : Type u_1} {Y : Type u_2} [] {m : } [] [] (μ : ) [μ.IsOpenPosMeasure] {f : XY} {g : XY} (hf : ) (hg : ) :
f =ᵐ[μ] g f = g
theorem Continuous.isOpenPosMeasure_map {X : Type u_1} [] {m : } {μ : } [μ.IsOpenPosMeasure] {Z : Type u_3} [] [] [] {f : XZ} (hf : ) (hf_surj : ) :
.IsOpenPosMeasure
theorem MeasureTheory.Measure.measure_Ioi_pos {X : Type u_1} [] [] [] {m : } (μ : ) [μ.IsOpenPosMeasure] [] (a : X) :
0 < μ ()
theorem MeasureTheory.Measure.measure_Iio_pos {X : Type u_1} [] [] [] {m : } (μ : ) [μ.IsOpenPosMeasure] [] (a : X) :
0 < μ ()
theorem MeasureTheory.Measure.measure_Ioo_pos {X : Type u_1} [] [] [] {m : } (μ : ) [μ.IsOpenPosMeasure] [] {a : X} {b : X} :
0 < μ (Set.Ioo a b) a < b
theorem MeasureTheory.Measure.measure_Ioo_eq_zero {X : Type u_1} [] [] [] {m : } (μ : ) [μ.IsOpenPosMeasure] [] {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} [] [] [] {m : } [] [] (μ : ) [μ.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} [] [] [] {m : } [] [] (μ : ) [μ.IsOpenPosMeasure] [] {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} [] [] [] {m : } [] [] (μ : ) [μ.IsOpenPosMeasure] [] {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} [] [] [] {m : } [] [] (μ : ) [μ.IsOpenPosMeasure] [] {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} {m : } (μ : ) [μ.IsOpenPosMeasure] (x : X) {r : } (hr : 0 < r) :
0 < μ ()
theorem Metric.measure_closedBall_pos {X : Type u_1} {m : } (μ : ) [μ.IsOpenPosMeasure] (x : X) {r : } (hr : 0 < r) :
0 < μ ()

See also Metric.measure_closedBall_pos_iff.

@[simp]
theorem Metric.measure_closedBall_pos_iff {X : Type u_2} [] {m : } (μ : ) [μ.IsOpenPosMeasure] {x : X} {r : } :
0 < μ () 0 < r
theorem EMetric.measure_ball_pos {X : Type u_1} {m : } (μ : ) [μ.IsOpenPosMeasure] (x : X) {r : ENNReal} (hr : r 0) :
0 < μ ()
theorem EMetric.measure_closedBall_pos {X : Type u_1} {m : } (μ : ) [μ.IsOpenPosMeasure] (x : X) {r : ENNReal} (hr : r 0) :
0 < μ ()

## Meagre sets and measure zero #

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

• The set of Liouville numbers is a Lebesgue measure zero subset of ℝ, but is not meagre. (In fact, its complement is meagre. See Real.disjoint_residual_ae.)

• The complement of the set of Liouville numbers in $[0,1]$ is meagre and has measure 1. For another counterexample, for all $α ∈ (0,1)$, there is a generalised Cantor set $C ⊆ [0,1]$ of measure α. Cantor sets are nowhere dense (hence meagre). Taking a countable union of fat Cantor sets whose measure approaches 1 even yields a meagre set of measure 1.

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} [] [] {s : Set X} {μ : } [μ.IsOpenPosMeasure] (h₁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} [] [] {s : Set X} {μ : } [μ.IsOpenPosMeasure] [] (h₁s : ) (h₂s : μ s = 0) :

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