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}
[TopologicalSpace X]
{m : MeasurableSpace X}
(μ : MeasureTheory.Measure X)
:
A measure is said to be IsOpenPosMeasure if it is positive on nonempty open sets.
Instances
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]
:
NeZero μ
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)
:
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)
:
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}
[μ.IsOpenPosMeasure]
(h : μ.AbsolutelyContinuous ν)
:
ν.IsOpenPosMeasure
theorem
LE.le.isOpenPosMeasure
{X : Type u_1}
[TopologicalSpace X]
{m : MeasurableSpace 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)
:
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)
:
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)
:
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)
:
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)
:
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 : X → Prop}
(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 g : X → Y}
(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 g : X → Y}
(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 g : X → Y}
(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 g : X → Y}
(hf : Continuous f)
(hg : Continuous 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 : X → Z}
(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)
:
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)
:
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 b : X}
:
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 b : X}
:
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 b : X}
{f g : X → Y}
(hfg : f =ᵐ[μ.restrict (Set.Ioo a b)] g)
(hf : ContinuousOn f (Set.Ioo a b))
(hg : ContinuousOn 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 b : X}
{f g : X → Y}
(hfg : f =ᵐ[μ.restrict (Set.Ioc a b)] g)
(hf : ContinuousOn f (Set.Ioc a b))
(hg : ContinuousOn 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 b : X}
{f g : X → Y}
(hfg : f =ᵐ[μ.restrict (Set.Ico a b)] g)
(hf : ContinuousOn f (Set.Ico a b))
(hg : ContinuousOn 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 b : X}
(hne : a ≠ b)
{f g : X → Y}
(hfg : f =ᵐ[μ.restrict (Set.Icc a b)] g)
(hf : ContinuousOn f (Set.Icc a b))
(hg : ContinuousOn 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)
:
0 < μ (EMetric.closedBall x r)
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}
[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)
:
IsMeagre s
A σ-compact measure zero subset is meagre. (More generally, every Fσ set of measure zero is meagre.)