Documentation

Mathlib.MeasureTheory.Covering.OneDim

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)) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt 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)) ((IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).filterAt x)