chore: split MeasureSpace.lean into 3 files (#8389)

The original file `MeasureSpace.lean` is a mess of 4580 lines, with a lot of changes of namespaces, active variables, and so on. We split it into three files: * `MeasureSpace`, with 2095 lines left (some stuff could still be moved to other files, but it already makes much more sense) * `Restrict`, with everything on restriction of measures (1100 lines) * `Typeclasses`, defining finite measures, sigma-finite measures, and so on (1443 lines) The new files are still large, but less so. This is 99% moving around and ensuring that variables and namespaces remain the same (#align statements have been very useful for this), and 1% adding `classical` in proofs and `[Decidable ...]` assumptions in statements, as I haven't opened `Classical` in the new files.
leanprover-community · Nov 13, 2023 · 5c9c13d · 5c9c13d
1 parent aa0957f
commit 5c9c13d
Show file tree

Hide file tree

Showing 11 changed files with 2,557 additions and 2,495 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2588,9 +2588,11 @@ import Mathlib.MeasureTheory.Measure.OuterMeasure
 import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
 import Mathlib.MeasureTheory.Measure.Regular
+import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.Stieltjes
 import Mathlib.MeasureTheory.Measure.Sub
 import Mathlib.MeasureTheory.Measure.Trim
+import Mathlib.MeasureTheory.Measure.Typeclasses
 import Mathlib.MeasureTheory.Measure.VectorMeasure
 import Mathlib.MeasureTheory.Measure.WithDensity
 import Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure

diff --git a/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean b/Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Typeclasses
 
 #align_import measure_theory.decomposition.unsigned_hahn from "leanprover-community/mathlib"@"0f1becb755b3d008b242c622e248a70556ad19e6"
 

diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean
@@ -3,7 +3,9 @@ Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import Mathlib.MeasureTheory.Measure.Typeclasses
 import Mathlib.MeasureTheory.Measure.MutuallySingular
+
 /-!
 # Dirac measure
 

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
diff --git a/Mathlib/MeasureTheory/Measure/MutuallySingular.lean b/Mathlib/MeasureTheory/Measure/MutuallySingular.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying, Yury Kudryashov
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Restrict
 
 #align_import measure_theory.measure.mutually_singular from "leanprover-community/mathlib"@"70a4f2197832bceab57d7f41379b2592d1110570"
 

diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean
diff --git a/Mathlib/MeasureTheory/Measure/Sub.lean b/Mathlib/MeasureTheory/Measure/Sub.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Martin Zinkevich. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Zinkevich
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Typeclasses
 
 #align_import measure_theory.measure.sub from "leanprover-community/mathlib"@"562bbf524c595c153470e53d36c57b6f891cc480"
 

diff --git a/Mathlib/MeasureTheory/Measure/Trim.lean b/Mathlib/MeasureTheory/Measure/Trim.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Rémy Degenne. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Typeclasses
 
 /-!
 # Restriction of a measure to a sub-σ-algebra

diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean
diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Kexing Ying. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Typeclasses
 import Mathlib.Analysis.Complex.Basic
 
 #align_import measure_theory.measure.vector_measure from "leanprover-community/mathlib"@"70a4f2197832bceab57d7f41379b2592d1110570"

diff --git a/Mathlib/Probability/ConditionalProbability.lean b/Mathlib/Probability/ConditionalProbability.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Rishikesh Vaishnav. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rishikesh Vaishnav
 -/
-import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Typeclasses
 
 #align_import probability.conditional_probability from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"