C_c^∞ functions are dense in L^p for 1 ≤ p < ∞

leanprover-community · Jan 18, 2025 · 2845cc3 · 2845cc3
1 parent b10900e
commit 2845cc3
Show file tree

Hide file tree

Showing 2 changed files with 393 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3706,6 +3706,7 @@ import Mathlib.MeasureTheory.Function.AEEqOfIntegral
 import Mathlib.MeasureTheory.Function.AEEqOfLIntegral
 import Mathlib.MeasureTheory.Function.AEMeasurableOrder
 import Mathlib.MeasureTheory.Function.AEMeasurableSequence
+import Mathlib.MeasureTheory.Function.CompactDense
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1