Commit 2025-12-02 22:30 6e8bf48c

View on Github →

feat(Analysis/ContDiff): smooth compactly supported functions are dense in Lp (#31079)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

added theorem HasCompactSupport.exist_eLpNorm_sub_le_of_continuous

added theorem MeasureTheory.Lp.dense_hasCompactSupport_contDiff

added theorem MeasureTheory.MemLp.exist_eLpNorm_sub_le

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

added theorem MeasureTheory.eLpNorm_indicator_sub_le_of_dist_bdd

added theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

deleted theorem MeasureTheory.eLpNorm_sub_le_of_dist_bdd

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.measure_support_eq_zero_iff