feat: separable measure and sufficient condition for Lp spaces to be …

…second-countable (#12519) Define the notion of measure-dense family in a measure space, and the notion of separable measure. Prove that if a measure is separable and E is a second-countable `NormedAddCommGroup`, then the corresponding Lp space is second-countable. True in particular when the measurable space is countably generated and the measure is s-finite. Co-authored-by: Etienne <[email protected]>
leanprover-community · Sep 19, 2024 · f0308a5 · f0308a5
1 parent c8f01e7
commit f0308a5
Show file tree

Hide file tree

Showing 2 changed files with 516 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3331,6 +3331,7 @@ import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.MeasureTheory.Measure.Restrict
+import Mathlib.MeasureTheory.Measure.SeparableMeasure
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Measure.Sub
 import Mathlib.MeasureTheory.Measure.Tilted