mathlib documentation

measure_theory.measure.open_pos

Measures positive on nonempty opens #

In this file we define a typeclass for measures that are positive on nonempty opens, see measure_theory.measure.is_open_pos_measure. 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]

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

Instances of this typeclass
theorem is_open.measure_ne_zero {X : Type u_1} [topological_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] {U : set X} (hU : is_open U) (hne : U.nonempty) :
μ U 0
theorem is_open.measure_pos {X : Type u_1} [topological_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] {U : set X} (hU : is_open U) (hne : U.nonempty) :
0 < μ U
theorem is_open.measure_pos_iff {X : Type u_1} [topological_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] {U : set X} (hU : is_open U) :
0 < μ U U.nonempty
theorem is_open.measure_eq_zero_iff {X : Type u_1} [topological_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] {U : set X} (hU : is_open U) :
μ U = 0 U =
theorem measure_theory.measure.measure_pos_of_mem_nhds {X : Type u_1} [topological_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] {s : set X} {x : X} (h : s nhds x) :
0 < μ s
theorem is_open.eq_empty_of_measure_zero {X : Type u_1} [topological_space X] {m : measurable_space X} {μ : measure_theory.measure X} [μ.is_open_pos_measure] {U : set X} (hU : is_open U) (h₀ : μ U = 0) :
U =
theorem measure_theory.measure.eq_on_open_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] {m : measurable_space X} [topological_space Y] [t2_space Y] {μ : measure_theory.measure X} [μ.is_open_pos_measure] {U : set X} {f g : X → Y} (h : f =ᵐ[μ.restrict U] g) (hU : is_open U) (hf : continuous_on f U) (hg : continuous_on g U) :
set.eq_on 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 measure_theory.measure.eq_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] {m : measurable_space X} [topological_space Y] [t2_space Y] {μ : measure_theory.measure X} [μ.is_open_pos_measure] {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 measure_theory.measure.eq_on_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] {m : measurable_space X} [topological_space Y] [t2_space Y] {μ : measure_theory.measure X} [μ.is_open_pos_measure] {s : set X} {f g : X → Y} (h : f =ᵐ[μ.restrict s] g) (hf : continuous_on f s) (hg : continuous_on g s) (hU : s closure (interior s)) :
set.eq_on f g s
theorem continuous.ae_eq_iff_eq {X : Type u_1} {Y : Type u_2} [topological_space X] {m : measurable_space X} [topological_space Y] [t2_space Y] (μ : measure_theory.measure X) [μ.is_open_pos_measure] {f g : X → Y} (hf : continuous f) (hg : continuous g) :
f =ᵐ[μ] g f = g
theorem measure_theory.measure.eq_on_Ioo_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [linear_order X] [order_topology X] {m : measurable_space X} [topological_space Y] [t2_space Y] (μ : measure_theory.measure X) [μ.is_open_pos_measure] {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (set.Ioo a b)] g) (hf : continuous_on f (set.Ioo a b)) (hg : continuous_on g (set.Ioo a b)) :
set.eq_on f g (set.Ioo a b)
theorem measure_theory.measure.eq_on_Ioc_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [linear_order X] [order_topology X] {m : measurable_space X} [topological_space Y] [t2_space Y] (μ : measure_theory.measure X) [μ.is_open_pos_measure] [densely_ordered X] {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (set.Ioc a b)] g) (hf : continuous_on f (set.Ioc a b)) (hg : continuous_on g (set.Ioc a b)) :
set.eq_on f g (set.Ioc a b)
theorem measure_theory.measure.eq_on_Ico_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [linear_order X] [order_topology X] {m : measurable_space X} [topological_space Y] [t2_space Y] (μ : measure_theory.measure X) [μ.is_open_pos_measure] [densely_ordered X] {a b : X} {f g : X → Y} (hfg : f =ᵐ[μ.restrict (set.Ico a b)] g) (hf : continuous_on f (set.Ico a b)) (hg : continuous_on g (set.Ico a b)) :
set.eq_on f g (set.Ico a b)
theorem measure_theory.measure.eq_on_Icc_of_ae_eq {X : Type u_1} {Y : Type u_2} [topological_space X] [linear_order X] [order_topology X] {m : measurable_space X} [topological_space Y] [t2_space Y] (μ : measure_theory.measure X) [μ.is_open_pos_measure] [densely_ordered X] {a b : X} (hne : a b) {f g : X → Y} (hfg : f =ᵐ[μ.restrict (set.Icc a b)] g) (hf : continuous_on f (set.Icc a b)) (hg : continuous_on g (set.Icc a b)) :
set.eq_on f g (set.Icc a b)
theorem metric.measure_ball_pos {X : Type u_1} [pseudo_metric_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] (x : X) {r : } (hr : 0 < r) :
0 < μ (metric.ball x r)
theorem metric.measure_closed_ball_pos {X : Type u_1} [pseudo_metric_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] (x : X) {r : } (hr : 0 < r) :
theorem emetric.measure_ball_pos {X : Type u_1} [pseudo_emetric_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] (x : X) {r : ennreal} (hr : r 0) :
0 < μ (emetric.ball x r)
theorem emetric.measure_closed_ball_pos {X : Type u_1} [pseudo_emetric_space X] {m : measurable_space X} (μ : measure_theory.measure X) [μ.is_open_pos_measure] (x : X) {r : ennreal} (hr : r 0) :