Measures positive on nonempty opens #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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]
structure
measure_theory.measure.is_open_pos_measure
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
(μ : measure_theory.measure X) :
Prop
A measure is said to be is_open_pos_measure if it is positive on nonempty open sets.
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) :
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) :
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) :
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) :
theorem
measure_theory.measure.measure_pos_of_nonempty_interior
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
{s : set X}
(h : (interior s).nonempty) :
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) :
theorem
measure_theory.measure.is_open_pos_measure_smul
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
{c : ennreal}
(h : c ≠ 0) :
(c • μ).is_open_pos_measure
@[protected]
theorem
measure_theory.measure.absolutely_continuous.is_open_pos_measure
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
{μ ν : measure_theory.measure X}
[μ.is_open_pos_measure]
(h : μ.absolutely_continuous ν) :
theorem
has_le.le.is_open_pos_measure
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
{μ ν : measure_theory.measure X}
[μ.is_open_pos_measure]
(h : μ ≤ ν) :
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) :
theorem
measure_theory.measure.interior_eq_empty_of_null
{X : Type u_1}
[topological_space X]
{m : measurable_space X}
{μ : measure_theory.measure X}
[μ.is_open_pos_measure]
{s : set X}
(hs : ⇑μ s = 0) :
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) :
theorem
measure_theory.measure.measure_Ioi_pos
{X : Type u_1}
[topological_space X]
[linear_order X]
[order_topology X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
[no_max_order X]
(a : X) :
theorem
measure_theory.measure.measure_Iio_pos
{X : Type u_1}
[topological_space X]
[linear_order X]
[order_topology X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
[no_min_order X]
(a : X) :
theorem
measure_theory.measure.measure_Ioo_pos
{X : Type u_1}
[topological_space X]
[linear_order X]
[order_topology X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
[densely_ordered X]
{a b : X} :
theorem
measure_theory.measure.measure_Ioo_eq_zero
{X : Type u_1}
[topological_space X]
[linear_order X]
[order_topology X]
{m : measurable_space X}
(μ : measure_theory.measure X)
[μ.is_open_pos_measure]
[densely_ordered X]
{a b : X} :
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)) :
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)) :
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)) :
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)) :
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) :
0 < ⇑μ (metric.closed_ball x 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) :
0 < ⇑μ (emetric.closed_ball x r)