Commit 2023-07-30 12:08 33baf7d8

View on Github →

feat: The convolution of a locally integrable function f with a sequence of bump functions converges ae to f (#6102)

Estimated changes

Modified Mathlib/Analysis/Calculus/BumpFunction/Convolution.lean

added theorem ContDiffBump.ae_convolution_tendsto_right_of_locally_integrable

Modified Mathlib/Analysis/Calculus/BumpFunction/Normed.lean

added theorem ContDiffBump.integral_le_measure_closedBall

added theorem ContDiffBump.measure_closedBall_div_le_integral

added theorem ContDiffBump.measure_closedBall_le_integral

added theorem ContDiffBump.normed_le_div_measure_closedBall_rIn

added theorem ContDiffBump.normed_le_div_measure_closedBall_rOut

Modified Mathlib/MeasureTheory/Covering/DensityTheorem.lean

modified theorem IsUnifLocDoublingMeasure.ae_tendsto_average

modified theorem IsUnifLocDoublingMeasure.ae_tendsto_average_norm_sub

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

modified theorem VitaliFamily.ae_tendsto_average

modified theorem VitaliFamily.ae_tendsto_average_norm_sub

deleted theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'

added theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable

modified theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div

added theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div_of_integrable

added theorem VitaliFamily.eventually_filterAt_integrableOn

Modified Mathlib/MeasureTheory/Integral/Average.lean

added theorem MeasureTheory.tendsto_integral_smul_of_tendsto_average_norm_sub

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem MeasureTheory.set_integral_le_integral