Covering theorems for Lebesgue measure in one dimension #
We have a general theory of covering theorems for doubling measures, developed notably
in DensityTheorem.lean. In this file, we expand the API for this theory in one dimension,
by showing that intervals belong to the relevant Vitali family.
theorem
Real.Icc_mem_vitaliFamily_at_right
{x : ℝ}
{y : ℝ}
(hxy : x < y)
:
Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt x
theorem
Real.tendsto_Icc_vitaliFamily_right
(x : ℝ)
:
Filter.Tendsto (fun (y : ℝ) => Set.Icc x y) (nhdsWithin x (Set.Ioi x))
(VitaliFamily.filterAt (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1) x)
theorem
Real.Icc_mem_vitaliFamily_at_left
{x : ℝ}
{y : ℝ}
(hxy : x < y)
:
Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt y
theorem
Real.tendsto_Icc_vitaliFamily_left
(x : ℝ)
:
Filter.Tendsto (fun (y : ℝ) => Set.Icc y x) (nhdsWithin x (Set.Iio x))
(VitaliFamily.filterAt (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1) x)