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) : Prop

• open_pos : ∀ (U : Set X), IsOpen U → Set.Nonempty U → ↑↑μ U ≠ 0

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

theorem IsOpen.measure_ne_zero {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) : ↑↑μ U ≠ 0

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

instance MeasureTheory.Measure.instNeZeroMeasureInstZero {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.IsOpenPosMeasure μ] [Nonempty X] : NeZero μ

Equations

• @MeasureTheory.Measure.instNeZeroMeasureInstZero = @MeasureTheory.Measure.instNeZeroMeasureInstZero.proof_1

theorem IsOpen.measure_pos_iff {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.IsOpenPosMeasure μ] {U : Set X} (hU : IsOpen U) : 0 < ↑↑μ U ↔ Set.Nonempty U

theorem IsOpen.measure_eq_zero_iff {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] {s : Set X} (h : Set.Nonempty (interior s)) : 0 < ↑↑μ s

theorem MeasureTheory.Measure.measure_pos_of_mem_nhds {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] {c : ENNReal} (h : c ≠ 0) : MeasureTheory.Measure.IsOpenPosMeasure (c • μ)

theorem MeasureTheory.Measure.AbsolutelyContinuous.isOpenPosMeasure {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} [MeasureTheory.Measure.IsOpenPosMeasure μ] (h : MeasureTheory.Measure.AbsolutelyContinuous μ ν) : MeasureTheory.Measure.IsOpenPosMeasure ν

theorem LE.le.isOpenPosMeasure {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure X} [MeasureTheory.Measure.IsOpenPosMeasure μ] (h : μ ≤ ν) : MeasureTheory.Measure.IsOpenPosMeasure ν

theorem IsOpen.measure_zero_iff_eq_empty {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.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} [MeasureTheory.Measure.IsOpenPosMeasure μ] {U : Set X} (hU : IsOpen U) : U =ᶠ[MeasureTheory.Measure.ae μ] ∅ ↔ 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 = ∅

theorem IsClosed.ae_eq_univ_iff_eq {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.IsOpenPosMeasure μ] {F : Set X} (hF : IsClosed F) : F =ᶠ[MeasureTheory.Measure.ae μ] Set.univ ↔ F = Set.univ

theorem IsClosed.measure_eq_univ_iff_eq {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.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} [MeasureTheory.Measure.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} [MeasureTheory.Measure.IsOpenPosMeasure μ] {s : Set X} (hs : ↑↑μ s = 0) : interior s = ∅

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} [MeasureTheory.Measure.IsOpenPosMeasure μ] {U : Set X} {f : X → Y} {g : X → Y} (h : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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} [MeasureTheory.Measure.IsOpenPosMeasure μ] {f : X → Y} {g : X → Y} (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 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} [MeasureTheory.Measure.IsOpenPosMeasure μ] {s : Set X} {f : X → Y} {g : X → Y} (h : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] {f : X → Y} {g : X → Y} (hf : Continuous f) (hg : Continuous g) : f =ᶠ[MeasureTheory.Measure.ae μ] g ↔ f = g

theorem Continuous.isOpenPosMeasure_map {X : Type u_1} [TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [MeasureTheory.Measure.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.IsOpenPosMeasure (MeasureTheory.Measure.map f μ)

theorem MeasureTheory.Measure.measure_Ioi_pos {X : Type u_1} [TopologicalSpace X] [LinearOrder X] [OrderTopology X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] {a : X} {b : X} {f : X → Y} {g : X → Y} (hfg : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] [DenselyOrdered X] {a : X} {b : X} {f : X → Y} {g : X → Y} (hfg : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] [DenselyOrdered X] {a : X} {b : X} {f : X → Y} {g : X → Y} (hfg : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] [DenselyOrdered X] {a : X} {b : X} (hne : a ≠ b) {f : X → Y} {g : X → Y} (hfg : f =ᶠ[MeasureTheory.Measure.ae (MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.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) [MeasureTheory.Measure.IsOpenPosMeasure μ] (x : X) {r : ENNReal} (hr : r ≠ 0) : 0 < ↑↑μ (EMetric.closedBall x r)