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

class MeasureTheory.Measure.IsOpenPosMeasure {X : Type u_1} [] {m : } (μ : ) :
• open_pos : ∀ (U : Set X), μ U 0

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} [] {m : } (μ : ) {U : Set X} (hU : ) (hne : ) :
μ U 0
theorem IsOpen.measure_pos {X : Type u_1} [] {m : } (μ : ) {U : Set X} (hU : ) (hne : ) :
0 < μ U
instance MeasureTheory.Measure.instNeZeroMeasureInstZero {X : Type u_1} [] {m : } (μ : ) [] :
theorem IsOpen.measure_pos_iff {X : Type u_1} [] {m : } (μ : ) {U : Set X} (hU : ) :
0 < μ U
theorem IsOpen.measure_eq_zero_iff {X : Type u_1} [] {m : } (μ : ) {U : Set X} (hU : ) :
μ U = 0 U =
theorem MeasureTheory.Measure.measure_pos_of_nonempty_interior {X : Type u_1} [] {m : } (μ : ) {s : Set X} (h : ) :
0 < μ s
theorem MeasureTheory.Measure.measure_pos_of_mem_nhds {X : Type u_1} [] {m : } (μ : ) {s : Set X} {x : X} (h : s nhds x) :
0 < μ s
theorem MeasureTheory.Measure.isOpenPosMeasure_smul {X : Type u_1} [] {m : } (μ : ) {c : ENNReal} (h : c 0) :
theorem LE.le.isOpenPosMeasure {X : Type u_1} [] {m : } {μ : } {ν : } (h : μ ν) :
theorem IsOpen.measure_zero_iff_eq_empty {X : Type u_1} [] {m : } {μ : } {U : Set X} (hU : ) :
μ U = 0 U =
theorem IsOpen.ae_eq_empty_iff_eq {X : Type u_1} [] {m : } {μ : } {U : Set X} (hU : ) :
U =
theorem IsOpen.eq_empty_of_measure_zero {X : Type u_1} [] {m : } {μ : } {U : Set X} (hU : ) (h₀ : μ U = 0) :
U =
theorem IsClosed.ae_eq_univ_iff_eq {X : Type u_1} [] {m : } {μ : } {F : Set X} (hF : ) :
F =ᶠ[] Set.univ F = Set.univ
theorem IsClosed.measure_eq_univ_iff_eq {X : Type u_1} [] {m : } {μ : } {F : Set X} (hF : ) :
μ F = μ Set.univ F = Set.univ
theorem IsClosed.measure_eq_one_iff_eq_univ {X : Type u_1} [] {m : } {μ : } {F : Set X} (hF : ) :
μ F = 1 F = Set.univ
theorem MeasureTheory.Measure.interior_eq_empty_of_null {X : Type u_1} [] {m : } {μ : } {s : Set X} (hs : μ s = 0) :
theorem MeasureTheory.Measure.eqOn_open_of_ae_eq {X : Type u_1} {Y : Type u_2} [] {m : } [] [] {μ : } {U : Set X} {f : XY} {g : XY} (h : ) (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 : } [] [] {μ : } {f : XY} {g : XY} (h : ) (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 : } [] [] {μ : } {s : Set X} {f : XY} {g : XY} (h : ) (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 : } [] [] (μ : ) {f : XY} {g : XY} (hf : ) (hg : ) :
f = g
theorem Continuous.isOpenPosMeasure_map {X : Type u_1} [] {m : } {μ : } {Z : Type u_3} [] [] [] {f : XZ} (hf : ) (hf_surj : ) :
theorem MeasureTheory.Measure.measure_Ioi_pos {X : Type u_1} [] [] [] {m : } (μ : ) [] (a : X) :
0 < μ ()
theorem MeasureTheory.Measure.measure_Iio_pos {X : Type u_1} [] [] [] {m : } (μ : ) [] (a : X) :
0 < μ ()
theorem MeasureTheory.Measure.measure_Ioo_pos {X : Type u_1} [] [] [] {m : } (μ : ) [] {a : X} {b : X} :
0 < μ (Set.Ioo a b) a < b
theorem MeasureTheory.Measure.measure_Ioo_eq_zero {X : Type u_1} [] [] [] {m : } (μ : ) [] {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 : } [] [] (μ : ) {a : X} {b : X} {f : XY} {g : XY} (hfg : ) (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 : } [] [] (μ : ) [] {a : X} {b : X} {f : XY} {g : XY} (hfg : ) (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 : } [] [] (μ : ) [] {a : X} {b : X} {f : XY} {g : XY} (hfg : ) (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 : } [] [] (μ : ) [] {a : X} {b : X} (hne : a b) {f : XY} {g : XY} (hfg : ) (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 : } (μ : ) (x : X) {r : } (hr : 0 < r) :
0 < μ ()
theorem Metric.measure_closedBall_pos {X : Type u_1} {m : } (μ : ) (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 : } (μ : ) {x : X} {r : } :
0 < μ () 0 < r
theorem EMetric.measure_ball_pos {X : Type u_1} {m : } (μ : ) (x : X) {r : ENNReal} (hr : r 0) :
0 < μ ()
theorem EMetric.measure_closedBall_pos {X : Type u_1} {m : } (μ : ) (x : X) {r : ENNReal} (hr : r 0) :
0 < μ ()