Commit 2023-06-07 08:40 51cf5975

View on Github →

feat: port MeasureTheory.Covering.Differentiation (#4779)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Covering/Differentiation.lean

added theorem VitaliFamily.ae_eventually_measure_pos

added theorem VitaliFamily.ae_eventually_measure_zero_of_singular

added theorem VitaliFamily.ae_tendsto_average

added theorem VitaliFamily.ae_tendsto_average_norm_sub

added theorem VitaliFamily.ae_tendsto_div

added theorem VitaliFamily.ae_tendsto_limRatio

added theorem VitaliFamily.ae_tendsto_limRatioMeas

added theorem VitaliFamily.ae_tendsto_lintegral_div'

added theorem VitaliFamily.ae_tendsto_lintegral_div

added theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'

added theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div

added theorem VitaliFamily.ae_tendsto_measure_inter_div

added theorem VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet

added theorem VitaliFamily.ae_tendsto_rnDeriv

added theorem VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous

added theorem VitaliFamily.aemeasurable_limRatio

added theorem VitaliFamily.eventually_measure_lt_top

added theorem VitaliFamily.exists_measurable_supersets_limRatio

added theorem VitaliFamily.le_mul_withDensity

added theorem VitaliFamily.limRatioMeas_measurable

added theorem VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt

added theorem VitaliFamily.measure_le_of_frequently_le

added theorem VitaliFamily.measure_limRatioMeas_top

added theorem VitaliFamily.measure_limRatioMeas_zero

added theorem VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas

added theorem VitaliFamily.null_of_frequently_le_of_frequently_ge

added theorem VitaliFamily.withDensity_le_mul

added theorem VitaliFamily.withDensity_limRatioMeas_eq