feat(MeasureTheory/../Prod): drop unneeded assumptions (#7620)

* Drop `CompleteSpace` assumption in all theorems about Bochner
  integral on `α × β`.
* Drop measurability assumption in `lintegral_prod_swap`.

Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

@@ -99,7 +99,6 @@ functions. We show that if `f` is a binary measurable function, then the functio
 along one of the variables (using either the Lebesgue or Bochner integral) is measurable.
 -/
 
-
 /-- 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)
@@ -812,10 +811,9 @@ namespace MeasureTheory
 
 variable [SigmaFinite ν]
 
-theorem lintegral_prod_swap [SigmaFinite μ] (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
-    ∫⁻ z, f z.swap ∂ν.prod μ = ∫⁻ z, f z ∂μ.prod ν := by
-  rw [← prod_swap] at hf
-  rw [← lintegral_map' hf measurable_swap.aemeasurable, prod_swap]
+theorem lintegral_prod_swap [SigmaFinite μ] (f : α × β → ℝ≥0∞) :
+    ∫⁻ z, f z.swap ∂ν.prod μ = ∫⁻ z, f z ∂μ.prod ν :=
+  measurePreserving_swap.lintegral_comp_emb MeasurableEquiv.prodComm.measurableEmbedding f
 #align measure_theory.lintegral_prod_swap MeasureTheory.lintegral_prod_swap
 
 /-- **Tonelli's Theorem**: For `ℝ≥0∞`-valued measurable functions on `α × β`,
@@ -863,7 +861,7 @@ theorem lintegral_prod (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.pr
 functions on `α × β`, the integral of `f` is equal to the iterated integral, in reverse order. -/
 theorem lintegral_prod_symm [SigmaFinite μ] (f : α × β → ℝ≥0∞) (hf : AEMeasurable f (μ.prod ν)) :
     ∫⁻ z, f z ∂μ.prod ν = ∫⁻ y, ∫⁻ x, f (x, y) ∂μ ∂ν := by
-  simp_rw [← lintegral_prod_swap f hf]
+  simp_rw [← lintegral_prod_swap f]
   exact lintegral_prod _ hf.prod_swap
 #align measure_theory.lintegral_prod_symm MeasureTheory.lintegral_prod_symm
 

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

@@ -69,13 +69,14 @@ theorem measurableSet_integrable [SigmaFinite ν] ⦃f : α → β → E⦄
 
 section
 
-variable [NormedSpace ℝ E] [CompleteSpace E]
+variable [NormedSpace ℝ E]
 
 /-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
   Fubini's theorem is measurable.
   This version has `f` in curried form. -/
 theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SigmaFinite ν] ⦃f : α → β → E⦄
     (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂ν := by
+  by_cases hE : CompleteSpace E; swap; · simp [integral, hE, stronglyMeasurable_const]
   borelize E
   haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
     hf.separableSpace_range_union_singleton
@@ -195,7 +196,7 @@ theorem MeasureTheory.AEStronglyMeasurable.snd {γ} [TopologicalSpace γ] [Sigma
 /-- The Bochner integral is a.e.-measurable.
   This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable. -/
 theorem MeasureTheory.AEStronglyMeasurable.integral_prod_right' [SigmaFinite ν] [NormedSpace ℝ E]
-    [CompleteSpace E] ⦃f : α × β → E⦄ (hf : AEStronglyMeasurable f (μ.prod ν)) :
+    ⦃f : α × β → E⦄ (hf : AEStronglyMeasurable f (μ.prod ν)) :
     AEStronglyMeasurable (fun x => ∫ y, f (x, y) ∂ν) μ :=
   ⟨fun x => ∫ y, hf.mk f (x, y) ∂ν, hf.stronglyMeasurable_mk.integral_prod_right', by
     filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx⟩
@@ -217,7 +218,6 @@ variable [SigmaFinite ν]
 
 /-! ### Integrability on a product -/
 
-
 section
 
 theorem integrable_swap_iff [SigmaFinite μ] {f : α × β → E} :
@@ -316,7 +316,7 @@ theorem integrable_prod_mul {L : Type*} [IsROrC L] {f : α → L} {g : β → L}
 
 end
 
-variable [NormedSpace ℝ E] [CompleteSpace E]
+variable [NormedSpace ℝ E]
 
 theorem Integrable.integral_prod_left ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
     Integrable (fun x => ∫ y, f (x, y) ∂ν) μ :=
@@ -342,7 +342,7 @@ theorem integral_prod_swap (f : α × β → E) :
   measurePreserving_swap.integral_comp MeasurableEquiv.prodComm.measurableEmbedding _
 #align measure_theory.integral_prod_swap MeasureTheory.integral_prod_swap
 
-variable {E' : Type*} [NormedAddCommGroup E'] [CompleteSpace E'] [NormedSpace ℝ E']
+variable {E' : Type*} [NormedAddCommGroup E'] [NormedSpace ℝ E']
 
 /-! Some rules about the sum/difference of double integrals. They follow from `integral_add`, but
   we separate them out as separate lemmas, because they involve quite some steps. -/
@@ -447,9 +447,10 @@ theorem continuous_integral_integral :
   `integrable_prod_iff` can be useful to show that the function in question in integrable.
   `MeasureTheory.Integrable.integral_prod_right` is useful to show that the inner integral
   of the right-hand side is integrable. -/
-theorem integral_prod :
-    ∀ (f : α × β → E) (_ : Integrable f (μ.prod ν)),
-      ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := by
+theorem integral_prod (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
+    ∫ z, f z ∂μ.prod ν = ∫ x, ∫ y, f (x, y) ∂ν ∂μ := by
+  by_cases hE : CompleteSpace E; swap; · simp only [integral, dif_neg hE]
+  revert f
   apply Integrable.induction
   · intro c s hs h2s
     simp_rw [integral_indicator hs, ← indicator_comp_right, Function.comp,
@@ -519,7 +520,7 @@ theorem set_integral_prod_mul {L : Type*} [IsROrC L] (f : α → L) (g : β →
     ∫ z in s ×ˢ t, f z.1 * g z.2 ∂μ.prod ν = (∫ x in s, f x ∂μ) * ∫ y in t, g y ∂ν := by
   -- Porting note: added
   rw [← Measure.prod_restrict s t]
-  simp only [← Measure.prod_restrict s t, IntegrableOn, integral_prod_mul]
+  apply integral_prod_mul
 #align measure_theory.set_integral_prod_mul MeasureTheory.set_integral_prod_mul
 
 end MeasureTheory