feat: integration by parts for stieltjes vector measures

Mathlib.lean

@@ -5611,9 +5611,13 @@ public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
 public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
 public import Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym
 public import Mathlib.MeasureTheory.VectorMeasure.Integral
+public import Mathlib.MeasureTheory.VectorMeasure.Prod
+public import Mathlib.MeasureTheory.VectorMeasure.SetIntegral
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
 public import Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
+public import Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation
 public import Mathlib.MeasureTheory.VectorMeasure.WithDensity
+public import Mathlib.MeasureTheory.VectorMeasure.WithDensityVec
 public import Mathlib.ModelTheory.Algebra.Field.Basic
 public import Mathlib.ModelTheory.Algebra.Field.CharP
 public import Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Mathlib/Analysis/Normed/Group/Continuity.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Analysis.Normed.Group.Basic
 public import Mathlib.Topology.Algebra.Ring.Real
+public import Mathlib.Topology.Instances.ENNReal.Lemmas
 public import Mathlib.Topology.Metrizable.Uniformity
 public import Mathlib.Topology.Sequences
 
@@ -68,6 +69,16 @@ theorem tendsto_one_iff_norm_tendsto_zero {f : α → E} {a : Filter α} :
     Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖) a (𝓝 0) :=
   tendsto_iff_norm_inv_mul_tendsto_zero.trans <| by simp
 
+@[to_additive]
+theorem tendsto_iff_enorm_inv_mul_tendsto_zero {f : α → E} {a : Filter α} {b : E} :
+    Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖(f e)⁻¹ * b‖ₑ) a (𝓝 0) := by
+  simp only [← edist_eq_enorm_inv_mul, ← tendsto_iff_edist_tendsto_0]
+
+@[to_additive]
+theorem tendsto_one_iff_enorm_tendsto_zero {f : α → E} {a : Filter α} :
+    Tendsto f a (𝓝 1) ↔ Tendsto (‖f ·‖ₑ) a (𝓝 0) :=
+  tendsto_iff_enorm_inv_mul_tendsto_zero.trans <| by simp
+
 @[to_additive (attr := simp 1100)]
 theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E) := by
   simpa only [dist_one_right] using nhds_comap_dist (1 : E)
@@ -302,6 +313,11 @@ theorem tendsto_iff_norm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E}
     Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖) a (𝓝 0) := by
   simp only [← dist_eq_norm_div, ← tendsto_iff_dist_tendsto_zero]
 
+@[to_additive]
+theorem tendsto_iff_enorm_div_tendsto_zero {f : α → E} {a : Filter α} {b : E} :
+    Tendsto f a (𝓝 b) ↔ Tendsto (fun e => ‖f e / b‖ₑ) a (𝓝 0) := by
+  simp only [← edist_eq_enorm_div, ← tendsto_iff_edist_tendsto_0]
+
 @[to_additive]
 theorem SeminormedCommGroup.mem_closure_iff {s : Set E} :
     a ∈ closure s ↔ ∀ ε, 0 < ε → ∃ b ∈ s, ‖a / b‖ < ε := by

Mathlib/Analysis/Normed/Operator/Bilinear.lean

@@ -165,6 +165,14 @@ theorem flip_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : f.flip.flip = f
 theorem opNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ = ‖f‖ :=
   le_antisymm (by simpa only [flip_flip] using le_norm_flip f.flip) (le_norm_flip f)
 
+@[simp]
+theorem opNNNorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖₊ = ‖f‖₊ := by
+  simp [← NNReal.coe_inj]
+
+@[simp]
+theorem opENorm_flip (f : E →SL[σ₁₃] F →SL[σ₂₃] G) : ‖f.flip‖ₑ = ‖f‖ₑ := by
+  simp [enorm_eq_nnnorm]
+
 @[simp]
 lemma flip_zero : flip (0 : E →SL[σ₁₃] F →SL[σ₂₃] G) = 0 := rfl
 

Mathlib/Analysis/Normed/Operator/Mul.lean

@@ -221,6 +221,10 @@ theorem opNNNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖
   rw [← NNReal.coe_le_coe]
   simpa using opNorm_lsmul_le
 
+theorem opENorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ ≤ 1 := by
+  rw [enorm_eq_nnnorm]
+  simpa using opNNNorm_lsmul_le
+
 end SMulLinear
 
 end ContinuousLinearMap
@@ -247,6 +251,10 @@ theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 :=
 theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 :=
   Subtype.ext <| opNorm_mul 𝕜 R
 
+@[simp]
+theorem opENorm_mul : ‖mul 𝕜 R‖ₑ = 1 := by
+  simp [enorm_eq_nnnorm]
+
 end
 
 /-- The norm of `lsmul` equals 1 in any nontrivial normed group.
@@ -268,6 +276,11 @@ theorem opNNNorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E
   rw [← NNReal.coe_inj]
   simp
 
+@[simp]
+theorem opENorm_lsmul [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E] [NormSMulClass R E]
+    [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ₑ = 1 := by
+  simp [enorm_eq_nnnorm]
+
 /-- The norm of `lsmul x` equals `‖x‖` in any nontrivial normed group.
 
 This is `ContinuousLinearMap.opNorm_lsmul_apply_le` as an equality. -/
@@ -288,6 +301,12 @@ theorem opNNNorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Modu
   rw [← NNReal.coe_inj]
   simp
 
+@[simp]
+theorem opENorm_lsmul_apply [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [Module R E]
+    [NormSMulClass R E] [IsScalarTower 𝕜 R E] [Nontrivial E] {a : R} :
+    ‖(lsmul 𝕜 R a : E →L[𝕜] E)‖ₑ = ‖a‖ₑ := by
+  simp [enorm_eq_nnnorm]
+
 end ContinuousLinearMap
 
 end Normed

Mathlib/Data/NNReal/Defs.lean

@@ -127,6 +127,8 @@ noncomputable instance : LinearOrderedCommGroupWithZero ℝ≥0 where
 example {p q : ℝ≥0} (h1p : 0 < p) (h2p : p ≤ q) : q⁻¹ ≤ p⁻¹ := by
   with_reducible_and_instances exact inv_anti₀ h1p h2p
 
+@[simp] lemma mk_coe (a : ℝ≥0) (ha : 0 ≤ (a : ℝ)) : NNReal.mk (a : ℝ) ha = a := rfl
+
 -- Simp lemma to put back `n.val` into the normal form given by the coercion.
 @[simp]
 theorem val_eq_coe (n : ℝ≥0) : n.val = n :=

Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean

@@ -82,12 +82,22 @@ variable {X E ι : Type*} [MeasurableSpace X] [CommMonoid E] [TopologicalSpace E
 
 section
 
-variable [IsCompletelyPseudoMetrizableSpace E] [ContinuousMul E]
-  [Countable ι] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
+variable [ContinuousMul E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated]
 
-/-- The product of strongly measurable functions is measurable. -/
+/-- The infinite product of strongly measurable functions is measurable, `HasProd` version. -/
 @[to_additive (attr := fun_prop)
-/-- The sum of strongly measurable functions is measurable. -/]
+/-- The infinite sum of strongly measurable functions is measurable, `HasSum` version. -/]
+theorem StronglyMeasurable.hasProd [PseudoMetrizableSpace E] {f : ι → X → E} {g : X → E}
+    (h : ∀ i : ι, StronglyMeasurable (f i)) (h' : ∀ x, HasProd (fun i ↦ f i x) (g x) L) :
+    StronglyMeasurable g := by
+  refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr h')
+  fun_prop
+
+variable [IsCompletelyPseudoMetrizableSpace E] [Countable ι]
+
+/-- The infinite product of strongly measurable functions is measurable. -/
+@[to_additive (attr := fun_prop)
+/-- The infinite sum of strongly measurable functions is measurable. -/]
 theorem StronglyMeasurable.tprod {f : ι → X → E} (h : ∀ i : ι, StronglyMeasurable (f i)) :
     StronglyMeasurable (fun x => ∏'[L] i : ι, f i x) := by
   let E := { x | Multipliable (f · x) L }

Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -661,6 +661,12 @@ theorem eLpNorm_smul_measure_of_ne_zero {c : ℝ≥0∞} (hc : c ≠ 0) (f : α
   · simp [*]
   exact eLpNorm_smul_measure_of_ne_zero_of_ne_top hp0 hp_top c
 
+theorem eLpNorm_smul_measure_le (c : ℝ≥0∞) (f : α → ε) (p : ℝ≥0∞)
+    (μ : Measure α) : eLpNorm f p (c • μ) ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by
+  rcases eq_or_ne c 0 with rfl | hc
+  · simp
+  · exact (eLpNorm_smul_measure_of_ne_zero hc f p μ ).le
+
 /-- See `eLpNorm_smul_measure_of_ne_zero` for a version with scalar multiplication by `ℝ≥0∞`. -/
 lemma eLpNorm_smul_measure_of_ne_zero' {c : ℝ≥0} (hc : c ≠ 0) (f : α → ε) (p : ℝ≥0∞)
     (μ : Measure α) : eLpNorm f p (c • μ) = c ^ p.toReal⁻¹ • eLpNorm f p μ :=
@@ -684,15 +690,16 @@ theorem eLpNorm_one_smul_measure {f : α → ε} (c : ℝ≥0∞) :
     eLpNorm f 1 (c • μ) = c * eLpNorm f 1 μ := by
   rw [eLpNorm_smul_measure_of_ne_top] <;> simp
 
+theorem eLpNorm_le_of_measure_le_smul {c : ℝ≥0∞}
+    {μ μ' : Measure α} (h : μ' ≤ c • μ) {f : α → ε} {p : ℝ≥0∞} :
+    eLpNorm f p μ' ≤ c ^ (1 / p).toReal • eLpNorm f p μ := by
+  grw [eLpNorm_mono_measure f h, eLpNorm_smul_measure_le]
+
 theorem MemLp.of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞)
     (hμ'_le : μ' ≤ c • μ) {f : α → ε} (hf : MemLp f p μ) : MemLp f p μ' := by
   refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
-  refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_
-  by_cases hc0 : c = 0
-  · simp [hc0]
-  rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]
-  refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2
-  simp [hc, hc0]
+  grw [eLpNorm_le_of_measure_le_smul hμ'_le]
+  exact ENNReal.mul_lt_top (Ne.lt_top (by simp [hc])) hf.2
 
 theorem MemLp.smul_measure {f : α → ε} {c : ℝ≥0∞} (hf : MemLp f p μ) (hc : c ≠ ∞) :
     MemLp f p (c • μ) :=

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

@@ -232,7 +232,6 @@ theorem nnnorm_def (f : Lp E p μ) : ‖f‖₊ = ENNReal.toNNReal (eLpNorm f p
 protected theorem coe_nnnorm (f : Lp E p μ) : (‖f‖₊ : ℝ) = ‖f‖ :=
   rfl
 
-@[simp]
 theorem enorm_def (f : Lp E p μ) : ‖f‖ₑ = eLpNorm f p μ :=
   ENNReal.coe_toNNReal <| Lp.eLpNorm_ne_top f
 
@@ -245,6 +244,7 @@ theorem nnnorm_toLp (f : α → E) (hf : MemLp f p μ) :
     ‖hf.toLp f‖₊ = ENNReal.toNNReal (eLpNorm f p μ) :=
   NNReal.eq <| norm_toLp f hf
 
+@[simp]
 lemma enorm_toLp {f : α → E} (hf : MemLp f p μ) : ‖hf.toLp f‖ₑ = eLpNorm f p μ := by
   simp_rw [enorm, nnnorm_toLp f hf, ENNReal.coe_toNNReal hf.2.ne]
 
@@ -869,6 +869,66 @@ end ContinuousLinearMap
 
 namespace MeasureTheory.Lp
 
+section LpToLpOfMeasureLeSMul
+
+variable [NormedSpace ℝ E] {ν : Measure α} {c : ℝ≥0∞}
+
+/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`.
+This is the linear map version. Use instead the continuous linear map
+version `LpToLpOfMeasureLeSMul` -/
+noncomputable def LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    Lp E p ν →ₗ[ℝ] Lp E p μ where
+  toFun f := ((Lp.memLp f).of_measure_le_smul hc h).toLp f
+  map_add' f g := by
+    ext
+    grw [MemLp.coeFn_toLp, Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp]
+    have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h
+    apply Measure.AbsolutelyContinuous.ae_eq this
+    grw [Lp.coeFn_add]
+  map_smul' c f := by
+    ext
+    grw [MemLp.coeFn_toLp, Lp.coeFn_smul, MemLp.coeFn_toLp]
+    have : μ ≪ ν := Measure.absolutelyContinuous_of_le_smul h
+    apply Measure.AbsolutelyContinuous.ae_eq this
+    grw [Lp.coeFn_smul]
+    rfl
+
+lemma coeFn_LpToLpOfMeasureLeSMulₗ (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) :
+    LpToLpOfMeasureLeSMulₗ hc h f =ᵐ[μ] f := by
+  simp [LpToLpOfMeasureLeSMulₗ, MemLp.coeFn_toLp]
+
+lemma enorm_LpToLpOfMeasureLeSMulₗ_apply_le
+    (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} :
+    ‖LpToLpOfMeasureLeSMulₗ hc h f‖ₑ ≤ c ^ (1 / p).toReal * ‖f‖ₑ := by
+  simp only [Lp.enorm_def]
+  grw [eLpNorm_congr_ae (coeFn_LpToLpOfMeasureLeSMulₗ hc h f)]
+  exact eLpNorm_le_of_measure_le_smul h
+
+lemma norm_LpToLpOfMeasureLeSMulₗ_apply_le
+    (hc : c ≠ ∞) (h : μ ≤ c • ν) [Fact (1 ≤ p)] {f : Lp E p ν} :
+    ‖LpToLpOfMeasureLeSMulₗ hc h f‖ ≤ c.toReal ^ (1 / p).toReal * ‖f‖ := by
+  simp only [← toReal_enorm]
+  rw [ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
+  apply (ENNReal.toReal_le_toReal (by simp only [ne_eq, enorm_ne_top, not_false_eq_true]) _).2
+    (enorm_LpToLpOfMeasureLeSMulₗ_apply_le hc h)
+  simp [ENNReal.mul_eq_top, hc]
+
+/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a multiple of `ν`. -/
+noncomputable def LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    Lp E p ν →L[ℝ] Lp E p μ :=
+  LinearMap.mkContinuous (LpToLpOfMeasureLeSMulₗ hc h) (c.toReal ^ (1 / p).toReal)
+    (fun _ ↦ norm_LpToLpOfMeasureLeSMulₗ_apply_le hc h)
+
+lemma coeFn_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) (f : Lp E p ν) :
+    LpToLpOfMeasureLeSMul hc h f =ᵐ[μ] f :=
+  coeFn_LpToLpOfMeasureLeSMulₗ hc h f
+
+lemma norm_LpToLpOfMeasureLeSMul [Fact (1 ≤ p)] (hc : c ≠ ∞) (h : μ ≤ c • ν) :
+    ‖(LpToLpOfMeasureLeSMul hc h : Lp E p ν →L[ℝ] Lp E p μ)‖ ≤ c.toReal ^ (1 / p).toReal :=
+  LinearMap.mkContinuous_norm_le _ (Real.rpow_nonneg (by simp) _) _
+
+end LpToLpOfMeasureLeSMul
+
 section PosPart
 
 theorem lipschitzWith_pos_part : LipschitzWith 1 fun x : ℝ => max x 0 :=

Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

@@ -322,6 +322,18 @@ theorem setToSimpleFunc_eq_sum_filter [DecidablePred fun x ↦ x ≠ (0 : F)]
   rw [hx0]
   exact map_zero _
 
+/-- The `setToSimpleFunc` is equal to a sum over any set that includes `f.range` (except `0`). -/
+theorem setToSimpleFunc_eq_sum_of_subset [DecidablePred fun x : F => x ≠ 0]
+    (T : Set α → F →L[ℝ] F') (hT : T ∅ = 0) {f : α →ₛ F} {s : Finset F}
+    (hs : {x ∈ f.range | x ≠ 0} ⊆ s) :
+    setToSimpleFunc T f = ∑ x ∈ s, T (f ⁻¹' {x}) x := by
+  rw [setToSimpleFunc_eq_sum_filter, Finset.sum_subset hs]
+  rintro x - hx; rw [Finset.mem_filter, not_and_or, Ne, Classical.not_not] at hx
+  rcases hx.symm with (rfl | hx)
+  · simp
+  rw [SimpleFunc.mem_range] at hx
+  rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx, hT]
+
 theorem map_setToSimpleFunc (T : Set α → F →L[ℝ] F') (h_add : FinMeasAdditive μ T) {f : α →ₛ G}
     (hf : Integrable f μ) {g : G → F} (hg : g 0 = 0) :
     (f.map g).setToSimpleFunc T = ∑ x ∈ f.range, T (f ⁻¹' {x}) (g x) := by

Mathlib/MeasureTheory/Integral/Prod.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.MeasureTheory.Function.LpSeminorm.Prod
 public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+public import Mathlib.MeasureTheory.Integral.SetToL1
 public import Mathlib.MeasureTheory.Integral.Bochner.Set
 public import Mathlib.MeasureTheory.Measure.Prod
 
@@ -37,7 +38,6 @@ product measure, Fubini's theorem, Fubini-Tonelli theorem
 
 public section
 
-
 noncomputable section
 
 open scoped Topology ENNReal MeasureTheory
@@ -60,12 +60,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.
 -/
 
-
-theorem measurableSet_integrable [SFinite ν] ⦃f : α → β → E⦄
-    (hf : StronglyMeasurable (uncurry f)) : MeasurableSet {x | Integrable (f x) ν} := by
-  simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]
-  exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const
-
 section
 
 variable [NormedSpace ℝ E]
@@ -75,49 +69,10 @@ variable [NormedSpace ℝ E]
   This version has `f` in curried form. -/
 theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SFinite ν] ⦃f : α → β → E⦄
     (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂ν := by
-  classical
-  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
-  let s : ℕ → SimpleFunc (α × β) E :=
-    SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp)
-  let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prodMk_left
-  let f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => (s' n x).integral ν
-  have hf' : ∀ n, StronglyMeasurable (f' n) := by
-    intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
-    have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
-      intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
-      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
-    simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
-    refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_
-    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
-    simp only [s', SimpleFunc.coe_comp, preimage_comp]
-    apply measurable_measure_prodMk_left
-    exact (s n).measurableSet_fiber x
-  have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂ν) := by
-    rw [tendsto_pi_nhds]; intro x
-    by_cases hfx : Integrable (f x) ν
-    · have (n : _) : Integrable (s' n x) ν := by
-        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
-        filter_upwards with y
-        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
-      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
-        mem_setOf_eq]
-      refine
-        tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
-          (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_
-      · refine fun n => Eventually.of_forall fun y =>
-          SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n
-        · exact hf.measurable
-        · simp
-      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_
-        · exact hf.measurable.of_uncurry_left
-        · simp
-        apply subset_closure
-        simp [-uncurry_apply_pair]
-    · simp [f', hfx, integral_undef]
-  exact stronglyMeasurable_of_tendsto _ hf' h2f'
+  simp only [integral_eq_setToFun]
+  apply StronglyMeasurable.setToFun_prod_right _ (fun s hs ↦ ?_) hf
+  refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
+  exact measurable_measure_prodMk_left hs
 
 /-- The Bochner integral is measurable. This shows that the integrand of (the right-hand-side of)
   Fubini's theorem is measurable. -/
@@ -380,13 +335,11 @@ end
 variable [NormedSpace ℝ E]
 
 theorem Integrable.integral_prod_left ⦃f : α × β → E⦄ (hf : Integrable f (μ.prod ν)) :
-    Integrable (fun x => ∫ y, f (x, y) ∂ν) μ :=
-  Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right' <|
-    Eventually.of_forall fun x =>
-      (norm_integral_le_integral_norm _).trans_eq <|
-        (norm_of_nonneg <|
-            integral_nonneg_of_ae <|
-              Eventually.of_forall fun y => (norm_nonneg (f (x, y)) :)).symm
+    Integrable (fun x => ∫ y, f (x, y) ∂ν) μ := by
+  apply Integrable.mono hf.integral_norm_prod_left hf.aestronglyMeasurable.integral_prod_right'
+  filter_upwards with x
+  grw [norm_integral_le_integral_norm]
+  exact le_abs_self _
 
 theorem Integrable.integral_prod_right [SFinite μ] ⦃f : α × β → E⦄
     (hf : Integrable f (μ.prod ν)) : Integrable (fun y => ∫ x, f (x, y) ∂μ) ν :=