chore(MeasureTheory/Constructions/Prod/Basic: split (#18286)

There were two things going on in this file:
* Measurability according to the product sigma-algebra
* The product measure

The former can be defined much earlier than the latter, in particular without importing `Measure`.

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Enrico Z. Borba
 -/
 
-import Mathlib.Probability.Density
-import Mathlib.Probability.Notation
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.Probability.Density
 import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Probability.Notation
 
 /-!
 

Mathlib.lean

@@ -3324,8 +3324,6 @@ import Mathlib.MeasureTheory.Constructions.HaarToSphere
 import Mathlib.MeasureTheory.Constructions.Pi
 import Mathlib.MeasureTheory.Constructions.Polish.Basic
 import Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Constructions.Projective
 import Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
 import Mathlib.MeasureTheory.Constructions.UnitInterval
@@ -3427,6 +3425,7 @@ import Mathlib.MeasureTheory.Integral.MeanInequalities
 import Mathlib.MeasureTheory.Integral.PeakFunction
 import Mathlib.MeasureTheory.Integral.Periodic
 import Mathlib.MeasureTheory.Integral.Pi
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.RieszMarkovKakutani
 import Mathlib.MeasureTheory.Integral.SetIntegral
 import Mathlib.MeasureTheory.Integral.SetToL1
@@ -3441,6 +3440,7 @@ import Mathlib.MeasureTheory.MeasurableSpace.Instances
 import Mathlib.MeasureTheory.MeasurableSpace.Invariants
 import Mathlib.MeasureTheory.MeasurableSpace.NCard
 import Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict
+import Mathlib.MeasureTheory.MeasurableSpace.Prod
 import Mathlib.MeasureTheory.Measure.AEDisjoint
 import Mathlib.MeasureTheory.Measure.AEMeasurable
 import Mathlib.MeasureTheory.Measure.AddContent
@@ -3478,6 +3478,7 @@ import Mathlib.MeasureTheory.Measure.NullMeasurable
 import Mathlib.MeasureTheory.Measure.OpenPos
 import Mathlib.MeasureTheory.Measure.Portmanteau
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.MeasureTheory.Measure.Regular
 import Mathlib.MeasureTheory.Measure.Restrict
 import Mathlib.MeasureTheory.Measure.SeparableMeasure

Mathlib/Analysis/Convolution.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Analysis.Calculus.ContDiff.Basic
 import Mathlib.Analysis.Calculus.ParametricIntegral
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Group.Integral
 import Mathlib.MeasureTheory.Group.Prod

Mathlib/Analysis/Fourier/FourierTransform.lean

@@ -3,13 +3,13 @@ Copyright (c) 2023 David Loeffler. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Loeffler
 -/
+import Mathlib.Algebra.Group.AddChar
 import Mathlib.Analysis.Complex.Circle
 import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Integral.SetIntegral
-import Mathlib.MeasureTheory.Measure.Haar.OfBasis
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
-import Mathlib.Algebra.Group.AddChar
+import Mathlib.MeasureTheory.Measure.Haar.OfBasis
 
 /-!
 # The Fourier transform

Mathlib/MeasureTheory/Constructions/HaarToSphere.lean

@@ -6,7 +6,7 @@ Authors: Yury Kudryashov
 import Mathlib.Algebra.Order.Field.Pointwise
 import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 import Mathlib.Analysis.SpecialFunctions.Integrals
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 
 /-!

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -3,8 +3,8 @@ 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 Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Measure
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.Topology.Constructions
 
 /-!

Mathlib/MeasureTheory/Group/Convolution.lean

@@ -3,8 +3,8 @@ Copyright (c) 2023 Josha Dekker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Josha Dekker
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Measure.MeasureSpace
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # The multiplicative and additive convolution of measures

Mathlib/MeasureTheory/Group/Measure.lean

@@ -3,8 +3,8 @@ 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 Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Action
+import Mathlib.MeasureTheory.Measure.Prod
 import Mathlib.Topology.ContinuousMap.CocompactMap
 
 /-!

Mathlib/MeasureTheory/Group/Prod.lean

@@ -3,8 +3,8 @@ Copyright (c) 2021 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Group.Measure
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Measure theory in the product of groups

Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

@@ -6,9 +6,9 @@ Authors: Yury Kudryashov
 import Mathlib.Analysis.BoxIntegral.DivergenceTheorem
 import Mathlib.Analysis.BoxIntegral.Integrability
 import Mathlib.Analysis.Calculus.Deriv.Basic
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
-import Mathlib.MeasureTheory.Integral.IntervalIntegral
 import Mathlib.Analysis.Calculus.FDeriv.Equiv
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.MeasureTheory.Integral.IntervalIntegral
 
 /-!
 # Divergence theorem for Bochner integral

Mathlib/MeasureTheory/Integral/Pi.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xavier Roblot
 -/
 import Mathlib.MeasureTheory.Constructions.Pi
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
+import Mathlib.MeasureTheory.Integral.Prod
 
 /-!
 # Integration with respect to a finite product of measures

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean → Mathlib/MeasureTheory/Integral/Prod.lean

@@ -3,9 +3,9 @@ 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 Mathlib.MeasureTheory.Constructions.Prod.Basic
 import Mathlib.MeasureTheory.Integral.DominatedConvergence
 import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Integration with respect to the product measure

Mathlib/MeasureTheory/Integral/TorusIntegral.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Cuma Kökmen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Cuma Kökmen, Yury Kudryashov
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Integral.CircleIntegral
+import Mathlib.MeasureTheory.Integral.Prod
 import Mathlib.Order.Fin.Tuple
 
 /-!

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -1268,6 +1268,13 @@ theorem isCountablySpanning_measurableSet [MeasurableSpace α] :
     IsCountablySpanning { s : Set α | MeasurableSet s } :=
   ⟨fun _ => univ, fun _ => MeasurableSet.univ, iUnion_const _⟩
 
+/-- Rectangles of countably spanning sets are countably spanning. -/
+lemma IsCountablySpanning.prod {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
+    (hD : IsCountablySpanning D) : IsCountablySpanning (image2 (· ×ˢ ·) C D) := by
+  rcases hC, hD with ⟨⟨s, h1s, h2s⟩, t, h1t, h2t⟩
+  refine ⟨fun n => s n.unpair.1 ×ˢ t n.unpair.2, fun n => mem_image2_of_mem (h1s _) (h1t _), ?_⟩
+  rw [iUnion_unpair_prod, h2s, h2t, univ_prod_univ]
+
 namespace MeasurableSet
 
 /-!

Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

@@ -0,0 +1,136 @@
+/-
+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 Mathlib.MeasureTheory.MeasurableSpace.Embedding
+import Mathlib.MeasureTheory.PiSystem
+
+/-!
+# The product sigma algebra
+
+This file talks about the measurability of operations on binary functions.
+-/
+
+assert_not_exists MeasureTheory.Measure
+
+noncomputable section
+
+open Set MeasurableSpace
+
+variable {α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
+
+/-- The product of generated σ-algebras is the one generated by rectangles, if both generating sets
+  are countably spanning. -/
+theorem generateFrom_prod_eq {α β} {C : Set (Set α)} {D : Set (Set β)} (hC : IsCountablySpanning C)
+    (hD : IsCountablySpanning D) :
+    @Prod.instMeasurableSpace _ _ (generateFrom C) (generateFrom D) =
+      generateFrom (image2 (· ×ˢ ·) C D) := by
+  apply le_antisymm
+  · refine sup_le ?_ ?_ <;> rw [comap_generateFrom] <;> apply generateFrom_le <;>
+      rintro _ ⟨s, hs, rfl⟩
+    · rcases hD with ⟨t, h1t, h2t⟩
+      rw [← prod_univ, ← h2t, prod_iUnion]
+      apply MeasurableSet.iUnion
+      intro n
+      apply measurableSet_generateFrom
+      exact ⟨s, hs, t n, h1t n, rfl⟩
+    · rcases hC with ⟨t, h1t, h2t⟩
+      rw [← univ_prod, ← h2t, iUnion_prod_const]
+      apply MeasurableSet.iUnion
+      rintro n
+      apply measurableSet_generateFrom
+      exact mem_image2_of_mem (h1t n) hs
+  · apply generateFrom_le
+    rintro _ ⟨s, hs, t, ht, rfl⟩
+    dsimp only
+    rw [prod_eq]
+    apply (measurable_fst _).inter (measurable_snd _)
+    · exact measurableSet_generateFrom hs
+    · exact measurableSet_generateFrom ht
+
+/-- If `C` and `D` generate the σ-algebras on `α` resp. `β`, then rectangles formed by `C` and `D`
+  generate the σ-algebra on `α × β`. -/
+theorem generateFrom_eq_prod {C : Set (Set α)} {D : Set (Set β)} (hC : generateFrom C = ‹_›)
+    (hD : generateFrom D = ‹_›) (h2C : IsCountablySpanning C) (h2D : IsCountablySpanning D) :
+    generateFrom (image2 (· ×ˢ ·) C D) = Prod.instMeasurableSpace := by
+  rw [← hC, ← hD, generateFrom_prod_eq h2C h2D]
+
+/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : Set α` and
+  `t : Set β`. -/
+lemma generateFrom_prod :
+    generateFrom (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) =
+      Prod.instMeasurableSpace :=
+  generateFrom_eq_prod generateFrom_measurableSet generateFrom_measurableSet
+    isCountablySpanning_measurableSet isCountablySpanning_measurableSet
+
+/-- Rectangles form a π-system. -/
+lemma isPiSystem_prod :
+    IsPiSystem (image2 (· ×ˢ ·) { s : Set α | MeasurableSet s } { t : Set β | MeasurableSet t }) :=
+  isPiSystem_measurableSet.prod isPiSystem_measurableSet
+
+lemma MeasurableEmbedding.prod_mk {α β γ δ : Type*} {mα : MeasurableSpace α}
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β}
+    {g : γ → δ} (hg : MeasurableEmbedding g) (hf : MeasurableEmbedding f) :
+    MeasurableEmbedding fun x : γ × α => (g x.1, f x.2) := by
+  have h_inj : Function.Injective fun x : γ × α => (g x.fst, f x.snd) := by
+    intro x y hxy
+    rw [← @Prod.mk.eta _ _ x, ← @Prod.mk.eta _ _ y]
+    simp only [Prod.mk.inj_iff] at hxy ⊢
+    exact ⟨hg.injective hxy.1, hf.injective hxy.2⟩
+  refine ⟨h_inj, ?_, ?_⟩
+  · exact (hg.measurable.comp measurable_fst).prod_mk (hf.measurable.comp measurable_snd)
+  · -- Induction using the π-system of rectangles
+    refine fun s hs =>
+      @MeasurableSpace.induction_on_inter _
+        (fun s => MeasurableSet ((fun x : γ × α => (g x.fst, f x.snd)) '' s)) _ _
+        generateFrom_prod.symm isPiSystem_prod ?_ ?_ ?_ ?_ _ hs
+    · simp only [Set.image_empty, MeasurableSet.empty]
+    · rintro t ⟨t₁, ht₁, t₂, ht₂, rfl⟩
+      rw [← Set.prod_image_image_eq]
+      exact (hg.measurableSet_image.mpr ht₁).prod (hf.measurableSet_image.mpr ht₂)
+    · intro t _ ht_m
+      rw [← Set.range_diff_image h_inj, ← Set.prod_range_range_eq]
+      exact
+        MeasurableSet.diff (MeasurableSet.prod hg.measurableSet_range hf.measurableSet_range) ht_m
+    · intro g _ _ hg
+      simp_rw [Set.image_iUnion]
+      exact MeasurableSet.iUnion hg
+
+lemma MeasurableEmbedding.prod_mk_left {β γ : Type*} [MeasurableSingletonClass α]
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    (x : α) {f : γ → β} (hf : MeasurableEmbedding f) :
+    MeasurableEmbedding (fun y ↦ (x, f y)) where
+  injective := by
+    intro y y'
+    simp only [Prod.mk.injEq, true_and]
+    exact fun h ↦ hf.injective h
+  measurable := Measurable.prod_mk measurable_const hf.measurable
+  measurableSet_image' := by
+    intro s hs
+    convert (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
+    ext x
+    simp
+
+lemma measurableEmbedding_prod_mk_left [MeasurableSingletonClass α] (x : α) :
+    MeasurableEmbedding (Prod.mk x : β → α × β) :=
+  MeasurableEmbedding.prod_mk_left x MeasurableEmbedding.id
+
+lemma MeasurableEmbedding.prod_mk_right {β γ : Type*} [MeasurableSingletonClass α]
+    {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
+    {f : γ → β} (hf : MeasurableEmbedding f) (x : α) :
+    MeasurableEmbedding (fun y ↦ (f y, x)) where
+  injective := by
+    intro y y'
+    simp only [Prod.mk.injEq, and_true]
+    exact fun h ↦ hf.injective h
+  measurable := Measurable.prod_mk hf.measurable measurable_const
+  measurableSet_image' := by
+    intro s hs
+    convert (hf.measurableSet_image.mpr hs).prod (MeasurableSet.singleton x)
+    ext x
+    simp
+
+lemma measurableEmbedding_prod_mk_right [MeasurableSingletonClass α] (x : α) :
+    MeasurableEmbedding (fun y ↦ (y, x) : β → β × α) :=
+  MeasurableEmbedding.prod_mk_right MeasurableEmbedding.id x

Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kalle Kytölä
 -/
 import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
-import Mathlib.MeasureTheory.Constructions.Prod.Basic
+import Mathlib.MeasureTheory.Measure.Prod
 
 /-!
 # Products of finite measures and probability measures

Mathlib/MeasureTheory/Measure/Haar/Unique.lean

@@ -3,14 +3,14 @@ Copyright (c) 2023 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.MeasureTheory.Function.LocallyIntegrable
 import Mathlib.MeasureTheory.Group.Integral
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.MeasureTheory.Integral.SetIntegral
+import Mathlib.MeasureTheory.Measure.EverywherePos
+import Mathlib.MeasureTheory.Measure.Haar.Basic
 import Mathlib.Topology.Metrizable.Urysohn
 import Mathlib.Topology.UrysohnsLemma
-import Mathlib.MeasureTheory.Measure.Haar.Basic
-import Mathlib.MeasureTheory.Measure.EverywherePos
-import Mathlib.MeasureTheory.Integral.SetIntegral
 
 /-!
 # Uniqueness of Haar measure in locally compact groups