Measures of intervals #
This file provide lemmas regarding the properties of measures and intervals,
such as continuity statements specialized to intervals or the fact that if µ {a} = 0
then Icc a b =ᵐ[μ] Ioc a b.
Tags #
measure, interval
theorem
MeasureTheory.biSup_measure_Iic
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[Preorder α]
{s : Set α}
(hsc : s.Countable)
(hst : ∀ (x : α), ∃ y ∈ s, x ≤ y)
(hdir : DirectedOn (fun (x1 x2 : α) => x1 ≤ x2) s)
:
theorem
MeasureTheory.tendsto_measure_Ico_atTop
{α : Type u_1}
{mα : MeasurableSpace α}
[Preorder α]
[NoMaxOrder α]
[Filter.atTop.IsCountablyGenerated]
(μ : Measure α)
(a : α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ico a x)) Filter.atTop (nhds (μ (Set.Ici a)))
theorem
MeasureTheory.tendsto_measure_Ioc_atBot
{α : Type u_1}
{mα : MeasurableSpace α}
[Preorder α]
[NoMinOrder α]
[Filter.atBot.IsCountablyGenerated]
(μ : Measure α)
(a : α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ioc x a)) Filter.atBot (nhds (μ (Set.Iic a)))
theorem
MeasureTheory.tendsto_measure_Iic_atTop
{α : Type u_1}
{mα : MeasurableSpace α}
[Preorder α]
[Filter.atTop.IsCountablyGenerated]
(μ : Measure α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Iic x)) Filter.atTop (nhds (μ Set.univ))
theorem
MeasureTheory.tendsto_measure_Ici_atBot
{α : Type u_1}
{mα : MeasurableSpace α}
[Preorder α]
[Filter.atBot.IsCountablyGenerated]
(μ : Measure α)
:
Filter.Tendsto (fun (x : α) => μ (Set.Ici x)) Filter.atBot (nhds (μ Set.univ))
theorem
MeasureTheory.Iio_ae_eq_Iic'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioi_ae_eq_Ici'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioo_ae_eq_Ioc'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a b : α}
(hb : μ {b} = 0)
:
theorem
MeasureTheory.Ioc_ae_eq_Icc'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ioo_ae_eq_Ico'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a b : α}
(ha : μ {a} = 0)
:
theorem
MeasureTheory.Ico_ae_eq_Icc'
{α : Type u_1}
{mα : MeasurableSpace α}
{μ : Measure α}
[PartialOrder α]
{a b : α}
(hb : μ {b} = 0)
: