Theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'

Modification history

2023-07-30 12:08

Mathlib/MeasureTheory/Covering/Differentiation.lean

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

Deleted VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'View on Github →

2023-06-07 08:40

Mathlib/MeasureTheory/Covering/Differentiation.lean

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

Added VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'View on Github →