Mathlib Changelog
v4
Changelog
About
Github
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