Commit 2023-06-07 11:17 f5cf43d1

View on Github →

feat: port MeasureTheory.Covering.DensityTheorem (#4789)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Covering/DensityTheorem.lean

added theorem IsUnifLocDoublingMeasure.ae_tendsto_average

added theorem IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub

added theorem IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div

added theorem IsUnifLocDoublingMeasure.closedBall_mem_vitaliFamily_of_dist_le_mul

added theorem IsUnifLocDoublingMeasure.tendsto_closedBall_filterAt