chore(measure_theory/{constructions/prod,measure/lebesgue}): split (#…

…19039) Reorganize some files in measure theory, with the goal of removing the dependence of Lebesgue measure on the Bochner integral. `measure_theory/constructions/prod` is split into `prod/basic` and `prod/integral`; the former imports the Lebesgue integral but not the Bochner integral. `measure_theory/measure/haar` is renamed `measure_theory/measure/haar/basic`. `measure_theory/measure/haar_of_inner` is renamed `measure_theory/measure/haar/inner_product_space`. `measure_theory/measure/haar_of_basis` is renamed `measure_theory/measure/haar/of_basis`. `measure_theory/measure/lebesgue` is split into `measure_theory/measure/lebesgue/basic` and `measure_theory/measure/lebesgue/integral`, with the former not importing the Bochner integral. `measure_theory/measure/complex_lebesgue` is renamed `measure_theory/measure/lebesgue/complex`. `measure_theory/measure/haar_lebesgue` is split into `measure_theory/measure/lebesgue/eq_haar` and `measure_theory/measure/haar/normed_space`, with the former not importing the Bochner integral. A few lemmas about Haar measure in normed spaces or fields are also moved from `measure_theory/group/measure` to the newly-created `measure_theory/measure/haar/normed_space`, since the former no longer imports `normed_space`.
leanprover-community · May 18, 2023 · fd5edc4 · fd5edc4
1 parent aa66698
commit fd5edc4
Show file tree

Hide file tree

Showing 41 changed files with 738 additions and 600 deletions.
diff --git a/archive/100-theorems-list/9_area_of_a_circle.lean b/archive/100-theorems-list/9_area_of_a_circle.lean
@@ -3,9 +3,10 @@ Copyright (c) 2021 James Arthur, Benjamin Davidson, Andrew Souther. All rights r
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Benjamin Davidson, Andrew Souther
 -/
-import measure_theory.integral.fund_thm_calculus
 import analysis.special_functions.sqrt
 import analysis.special_functions.trigonometric.inverse_deriv
+import measure_theory.integral.fund_thm_calculus
+import measure_theory.measure.lebesgue.integral
 
 /-!
 # Freek № 9: The Area of a Circle

diff --git a/counterexamples/phillips.lean b/counterexamples/phillips.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.hahn_banach.extension
-import measure_theory.measure.lebesgue
+import measure_theory.integral.set_integral
+import measure_theory.measure.lebesgue.basic
+import topology.continuous_function.bounded
 
 /-!
 # A counterexample on Pettis integrability

diff --git a/src/analysis/box_integral/integrability.lean b/src/analysis/box_integral/integrability.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.box_integral.basic
+import measure_theory.integral.set_integral
 import measure_theory.measure.regular
 
 /-!

diff --git a/src/analysis/box_integral/partition/measure.lean b/src/analysis/box_integral/partition/measure.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.box_integral.partition.additive
-import measure_theory.measure.lebesgue
+import measure_theory.measure.lebesgue.basic
 
 /-!
 # Box-additive functions defined by measures

diff --git a/src/analysis/calculus/bump_function_findim.lean b/src/analysis/calculus/bump_function_findim.lean
@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
 import analysis.calculus.series
 import analysis.convolution
 import analysis.inner_product_space.euclidean_dist
-import measure_theory.measure.haar_lebesgue
+import measure_theory.measure.haar.normed_space
 import data.set.pointwise.support
 
 /-!

diff --git a/src/analysis/complex/cauchy_integral.lean b/src/analysis/complex/cauchy_integral.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
-import measure_theory.measure.complex_lebesgue
+import measure_theory.measure.lebesgue.complex
 import measure_theory.integral.divergence_theorem
 import measure_theory.integral.circle_integral
 import analysis.calculus.dslope

diff --git a/src/analysis/convex/measure.lean b/src/analysis/convex/measure.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 import analysis.convex.topology
 import analysis.normed_space.add_torsor_bases
-import measure_theory.measure.haar_lebesgue
+import measure_theory.measure.lebesgue.eq_haar
 
 /-!
 # Convex sets are null-measurable

diff --git a/src/analysis/convolution.lean b/src/analysis/convolution.lean
@@ -3,12 +3,13 @@ Copyright (c) 2022 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
+import analysis.calculus.bump_function_inner
+import analysis.calculus.parametric_integral
+import measure_theory.constructions.prod.integral
+import measure_theory.function.locally_integrable
 import measure_theory.group.integration
 import measure_theory.group.prod
-import measure_theory.function.locally_integrable
-import analysis.calculus.bump_function_inner
 import measure_theory.integral.interval_integral
-import analysis.calculus.parametric_integral
 
 /-!
 # Convolution of functions

diff --git a/src/analysis/fourier/fourier_transform.lean b/src/analysis/fourier/fourier_transform.lean
@@ -6,7 +6,7 @@ Authors: David Loeffler
 
 import analysis.complex.circle
 import measure_theory.group.integration
-import measure_theory.measure.haar_of_basis
+import measure_theory.measure.haar.of_basis
 
 /-!
 # The Fourier transform

diff --git a/src/analysis/fourier/poisson_summation.lean b/src/analysis/fourier/poisson_summation.lean
@@ -7,6 +7,7 @@ import analysis.fourier.add_circle
 import analysis.fourier.fourier_transform
 import analysis.p_series
 import analysis.schwartz_space
+import measure_theory.measure.lebesgue.integral
 
 /-!
 # Poisson's summation formula

diff --git a/src/analysis/fourier/riemann_lebesgue_lemma.lean b/src/analysis/fourier/riemann_lebesgue_lemma.lean
@@ -4,12 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
 
-import measure_theory.function.continuous_map_dense
-import measure_theory.group.integration
 import analysis.fourier.fourier_transform
 import analysis.inner_product_space.dual
-import topology.metric_space.emetric_paracompact
 import analysis.inner_product_space.euclidean_dist
+import measure_theory.function.continuous_map_dense
+import measure_theory.group.integration
+import measure_theory.integral.set_integral
+import measure_theory.measure.haar.normed_space
+import topology.metric_space.emetric_paracompact
 
 /-!
 # The Riemann-Lebesgue Lemma

diff --git a/src/analysis/special_functions/improper_integrals.lean b/src/analysis/special_functions/improper_integrals.lean
@@ -3,10 +3,11 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
-import measure_theory.integral.integral_eq_improper
+import analysis.special_functions.integrals
 import measure_theory.group.integration
 import measure_theory.integral.exp_decay
-import analysis.special_functions.integrals
+import measure_theory.integral.integral_eq_improper
+import measure_theory.measure.lebesgue.integral
 
 /-!
 # Evaluation of specific improper integrals

diff --git a/src/analysis/special_functions/japanese_bracket.lean b/src/analysis/special_functions/japanese_bracket.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Moritz Doll. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Moritz Doll
 -/
-import measure_theory.measure.haar_lebesgue
+import measure_theory.measure.lebesgue.eq_haar
 import measure_theory.integral.layercake
 
 /-!

diff --git a/src/measure_theory/constructions/pi.lean b/src/measure_theory/constructions/pi.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import measure_theory.constructions.prod
+import measure_theory.constructions.prod.basic
 import measure_theory.group.measure
 import topology.constructions