diff --git a/Mathlib.lean b/Mathlib.lean
index b51d41f92d98c8..0063ab4c102196 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -5484,6 +5484,12 @@ public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
 public import Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
 public import Mathlib.MeasureTheory.Integral.DivergenceTheorem
 public import Mathlib.MeasureTheory.Integral.DominatedConvergence
+public import Mathlib.MeasureTheory.Integral.EReal.AuxLemmas
+public import Mathlib.MeasureTheory.Integral.EReal.Bochner
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegrable
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegral
+public import Mathlib.MeasureTheory.Integral.EReal.Kernel
+public import Mathlib.MeasureTheory.Integral.EReal.Prod
 public import Mathlib.MeasureTheory.Integral.ExpDecay
 public import Mathlib.MeasureTheory.Integral.FinMeasAdditive
 public import Mathlib.MeasureTheory.Integral.Gamma
diff --git a/Mathlib/Algebra/Order/Group/PosPart.lean b/Mathlib/Algebra/Order/Group/PosPart.lean
index 6f94e2f0ebf43a..c5af92da0e612d 100644
--- a/Mathlib/Algebra/Order/Group/PosPart.lean
+++ b/Mathlib/Algebra/Order/Group/PosPart.lean
@@ -75,9 +75,16 @@ instance instLeOnePart : LeOnePart α where
 @[to_additive (attr := simp) posPart_nonneg]
 lemma one_le_oneLePart (a : α) : 1 ≤ a⁺ᵐ := le_sup_right
 
+-- even though it is almost a duplicate of `one_le_oneLePart`, it allows `simp` to work on its goal.
+@[to_additive (attr := simp) posPart_fun_nonneg]
+lemma one_le_oneLePart_fun {β : Type*} (f : β → α) (x : β) : 1 ≤ f⁺ᵐ x := one_le_oneLePart f x
+
 @[to_additive (attr := simp) negPart_nonneg]
 lemma one_le_leOnePart (a : α) : 1 ≤ a⁻ᵐ := le_sup_right
 
+@[to_additive (attr := simp) negPart_fun_nonneg]
+lemma one_le_leOnePart_fun {β : Type*} (f : β → α) (x : β) : 1 ≤ f⁻ᵐ x := one_le_leOnePart f x
+
 -- TODO: `to_additive` guesses `nonposPart`
 @[to_additive le_posPart] lemma le_oneLePart (a : α) : a ≤ a⁺ᵐ := le_sup_left
 
diff --git a/Mathlib/Data/EReal/Basic.lean b/Mathlib/Data/EReal/Basic.lean
index 2e8a1d014a1c2c..793cedb4e8a0fb 100644
--- a/Mathlib/Data/EReal/Basic.lean
+++ b/Mathlib/Data/EReal/Basic.lean
@@ -614,6 +614,9 @@ theorem coe_nnreal_lt_top (x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) < ⊤ := co
 theorem coe_ennreal_le_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) ≤ (y : EReal) ↔ x ≤ y :=
   coe_ennreal_strictMono.le_iff_le
 
+@[gcongr]
+alias ⟨_, coe_ennreal_le_coe_ennreal⟩ := coe_ennreal_le_coe_ennreal_iff
+
 @[simp, norm_cast]
 theorem coe_ennreal_lt_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) < (y : EReal) ↔ x < y :=
   coe_ennreal_strictMono.lt_iff_lt
@@ -764,6 +767,7 @@ lemma toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
     x.toENNReal = y.toENNReal ↔ x = y := by
   induction x <;> induction y <;> simp_all
 
+@[gcongr]
 lemma toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal := by
   induction x
   · simp
diff --git a/Mathlib/MeasureTheory/Integral/EReal/AuxLemmas.lean b/Mathlib/MeasureTheory/Integral/EReal/AuxLemmas.lean
new file mode 100644
index 00000000000000..147cc4f7e1119f
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/AuxLemmas.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.Analysis.Normed.Group.Defs
+public import Mathlib.MeasureTheory.Group.Arithmetic
+public import Mathlib.MeasureTheory.Order.Lattice
+public import Mathlib.MeasureTheory.Order.Group.Lattice
+
+/-!
+# Aux lemmas: move them elsewhere
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal
+
+noncomputable
+instance : ENorm EReal where
+  enorm x := x⁺.toENNReal + x⁻.toENNReal
+
+section PosNeg
+
+open MeasureTheory
+
+lemma EReal.posPart_sub_negPart (x : EReal) : x⁺ - x⁻ = x := by
+  rcases le_total 0 x with h | h <;> simp [negPart_def, h]
+
+variable {α : Type*} {mα : MeasurableSpace α}
+
+lemma EReal.posPart_fun_sub_negPart_fun_apply (f : α → EReal) (x : α) : f⁺ x - f⁻ x = f x := by
+  rcases le_total 0 (f x) with h | h <;> simp [posPart_def, negPart_def, h]
+
+lemma EReal.posPart_fun_sub_negPart_fun (f : α → EReal) : f⁺ - f⁻ = f := by
+  ext x
+  simp only [Pi.sub_apply]
+  exact EReal.posPart_fun_sub_negPart_fun_apply f x
+
+lemma EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero (f : α → EReal) (x : α) :
+    f⁺ x = 0 ∨ f⁻ x = 0 := by
+  rcases le_total 0 (f x) with h | h <;> simp [posPart_def, negPart_def, h]
+
+end PosNeg
diff --git a/Mathlib/MeasureTheory/Integral/EReal/Bochner.lean b/Mathlib/MeasureTheory/Integral/EReal/Bochner.lean
new file mode 100644
index 00000000000000..32f5a9840e5427
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/Bochner.lean
@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.Bochner.Basic
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegral
+
+/-!
+# TODO
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → EReal}
+
+/-- For `Integrable` real-valued functions, the extended integral coincides with the
+standard Bochner integral. -/
+lemma eintegral_eq_integral {f : α → ℝ} (hf : Integrable f μ) :
+    ∫ᵉ x, f x ∂μ = ∫ x, f x ∂μ := by
+  rw [eintegral_eq_posPartFun_sub_negPartFun, eintegral_of_nonneg (by simp),
+    eintegral_of_nonneg (by simp)]
+  simp only [posPart_def, Pi.sup_apply, Pi.zero_apply, ne_eq, max_eq_top, EReal.coe_ne_top,
+    EReal.zero_ne_top, or_self, not_false_eq_true, EReal.toENNReal_of_ne_top, negPart_def,
+    Pi.neg_apply, EReal.neg_eq_top_iff, EReal.coe_ne_bot]
+  have h_int_max : Integrable (fun x ↦ (max (f x : EReal) 0).toReal) μ := by
+    refine hf.mono ?_ ?_
+    · exact AEMeasurable.aestronglyMeasurable (by fun_prop)
+    · filter_upwards with x
+      rcases le_total 0 (f x) with h | h <;> simp [h]
+  have h_int_min : Integrable (fun x ↦ (max (- f x : EReal) 0).toReal) μ := by
+    refine hf.mono ?_ ?_
+    · exact AEMeasurable.aestronglyMeasurable (by fun_prop)
+    · filter_upwards with x
+      rcases le_total 0 (f x) with h | h <;> simp [h]
+  rw [← ofReal_integral_eq_lintegral_ofReal, ← ofReal_integral_eq_lintegral_ofReal]
+  rotate_left
+  · exact h_int_min
+  · filter_upwards with x
+    simp only [Pi.zero_apply]
+    rw [← EReal.toReal_zero]
+    exact EReal.toReal_le_toReal (by simp) (by simp) (by simp)
+  · exact h_int_max
+  · filter_upwards with x
+    simp only [Pi.zero_apply]
+    rw [← EReal.toReal_zero]
+    exact EReal.toReal_le_toReal (by simp) (by simp) (by simp)
+  simp only [EReal.coe_ennreal_ofReal]
+  rw [max_eq_left, max_eq_left]
+  rotate_left
+  · exact integral_nonneg fun x ↦ by rcases le_total 0 (f x) with h | h <;> simp [h]
+  · exact integral_nonneg fun x ↦ by rcases le_total 0 (f x) with h | h <;> simp [h]
+  norm_cast
+  rw [← integral_sub]
+  rotate_left
+  · exact h_int_max
+  · exact h_int_min
+  congr with x
+  rcases le_total 0 (f x) with h | h <;> simp [h]
+
+lemma EReal.enorm_ereal_toReal {x : EReal} (h_top : x ≠ ⊤) (h_bot : x ≠ ⊥) :
+    ‖x.toReal‖ₑ = ‖x‖ₑ := by
+  lift x to ℝ using ⟨h_top, h_bot⟩ with r
+  simp only [enorm, nnnorm, EReal.toReal_coe, Real.norm_eq_abs, abs, posPart_def, ne_eq, max_eq_top,
+    EReal.coe_ne_top, EReal.zero_ne_top, or_self, not_false_eq_true, EReal.toENNReal_of_ne_top,
+    negPart_def, EReal.neg_eq_top_iff, EReal.coe_ne_bot]
+  rcases le_total 0 r with h | h <;> simp [ENNReal.ofReal, Real.toNNReal, h]
+
+lemma lintegral_enorm_ereal_toReal (hf_ne_bot : ∀ᵐ x ∂μ, f x ≠ ⊥) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ⊤) :
+    ∫⁻ a, ‖(f a).toReal‖ₑ ∂μ = ∫⁻ a, ‖f a‖ₑ ∂μ := by
+  refine lintegral_congr_ae ?_
+  filter_upwards [hf_ne_bot, hf_ne_top] with x hfx_ne_bot hfx_ne_top
+  rw [EReal.enorm_ereal_toReal hfx_ne_top hfx_ne_bot]
+
+lemma integrable_toReal (hf_meas : AEMeasurable f μ) (h_int_bot : ∫ᵉ x, f x ∂μ ≠ ⊥)
+    (h_int_top : ∫ᵉ x, f x ∂μ ≠ ⊤) :
+    Integrable (fun x ↦ (f x).toReal) μ := by
+  refine ⟨AEMeasurable.aestronglyMeasurable <| by fun_prop, ?_⟩
+  rw [HasFiniteIntegral]
+  suffices (∫⁻ a, ‖(f a).toReal‖ₑ ∂μ : EReal) < ⊤ by
+    simp only [lt_top_iff_ne_top, ne_eq, EReal.coe_ennreal_eq_top_iff] at this
+    rwa [lt_top_iff_ne_top]
+  have h_eq : ∫⁻ a, ‖(f a).toReal‖ₑ ∂μ = ∫⁻ a, ‖f a‖ₑ ∂μ := by
+    have hf_ne_bot : ∀ᵐ x ∂μ, f x ≠ ⊥ := ae_ne_bot_of_eintegral_ne_bot hf_meas h_int_bot
+    have hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ⊤ := ae_ne_top_of_eintegral_ne_top hf_meas h_int_bot h_int_top
+    exact lintegral_enorm_ereal_toReal hf_ne_bot hf_ne_top
+  rw [h_eq, lintegral_enorm_eq_posPartFun_add_negPartFun hf_meas]
+  refine EReal.add_lt_top ?_ ?_
+  · exact eintegral_posPartFun_ne_top h_int_bot h_int_top
+  · exact eintegral_negPartFun_ne_top h_int_bot
+
+lemma integrable_ereal_toReal_iff (hf_meas : AEMeasurable f μ)
+    (h_bot : ∀ᵐ x ∂μ, f x ≠ ⊥) (h_top : ∀ᵐ x ∂μ, f x ≠ ⊤) :
+    Integrable (fun x ↦ (f x).toReal) μ ↔ ∫ᵉ x, f x ∂μ ≠ ⊥ ∧ ∫ᵉ x, f x ∂μ ≠ ⊤ := by
+  refine ⟨fun h ↦ ?_, fun ⟨h1, h2⟩ ↦ integrable_toReal hf_meas h1 h2⟩
+  have h_lintegral : ∫⁻ a, ‖(f a).toReal‖ₑ ∂μ < ∞ := h.hasFiniteIntegral
+  rw [lintegral_enorm_ereal_toReal h_bot h_top] at h_lintegral
+  rw [eintegral_eq_posPartFun_sub_negPartFun]
+  have := lintegral_enorm_eq_posPartFun_add_negPartFun hf_meas
+  have h_pos_ne_bot : ∫ᵉ x, f⁺ x ∂μ ≠ ⊥ := by simp [eintegral_of_nonneg (posPart_fun_nonneg _)]
+  have h_neg_ne_bot : ∫ᵉ x, f⁻ x ∂μ ≠ ⊥ := by simp [eintegral_of_nonneg (negPart_fun_nonneg _)]
+  have h_pos_ne_top : ∫ᵉ x, f⁺ x ∂μ ≠ ⊤ := by
+    intro h_contra
+    simp only [h_contra] at this
+    rw [EReal.top_add_of_ne_bot h_neg_ne_bot] at this
+    simp_all
+  have h_neg_ne_top : ∫ᵉ x, f⁻ x ∂μ ≠ ⊤ := by
+    intro h_contra
+    simp only [h_contra] at this
+    rw [EReal.add_top_of_ne_bot h_pos_ne_bot] at this
+    simp_all
+  lift ∫ᵉ x, f⁺ x ∂μ to ℝ using ⟨h_pos_ne_top, h_pos_ne_bot⟩ with int_pos
+  lift ∫ᵉ x, f⁻ x ∂μ to ℝ using ⟨h_neg_ne_top, h_neg_ne_bot⟩ with int_neg
+  norm_cast
+  simp only [EReal.coe_ne_bot, EReal.coe_ne_top, not_false_eq_true, and_true]
+
+/-- If the extended integral is finite, then it equals the integral of the real part. -/
+lemma eintegral_eq_integral_toReal (hf_meas : AEMeasurable f μ) (h_int_bot : ∫ᵉ x, f x ∂μ ≠ ⊥)
+    (h_int_top : ∫ᵉ x, f x ∂μ ≠ ⊤) :
+    ∫ᵉ x, f x ∂μ = ∫ x, (f x).toReal ∂μ := by
+  have hf_ne_bot : ∀ᵐ x ∂μ, f x ≠ ⊥ := ae_ne_bot_of_eintegral_ne_bot hf_meas h_int_bot
+  have hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ⊤ := ae_ne_top_of_eintegral_ne_top hf_meas h_int_bot h_int_top
+  have hf_eq : ∀ᵐ x ∂μ, f x = (f x).toReal := by
+    filter_upwards [hf_ne_bot, hf_ne_top] with x hx_bot hx_top
+    rw [EReal.coe_toReal hx_top hx_bot]
+  rw [eintegral_congr_ae hf_eq, eintegral_eq_integral]
+  exact integrable_toReal hf_meas h_int_bot h_int_top
+
+end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Integral/EReal/EIntegrable.lean b/Mathlib/MeasureTheory/Integral/EReal/EIntegrable.lean
new file mode 100644
index 00000000000000..a8083d9e0ef80f
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/EIntegrable.lean
@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.Lebesgue.Map
+
+
+/-!
+# Integrable functions with values in `EReal`
+
+The integral of a function with values in `EReal` is defined as the difference of the Lebesgue
+integrals of its positive and negative parts. This definition is meaningful only if at least one of
+these integrals is finite (if not, it has value `⊤ - ⊤ = ⊥` in Lean, but that value is not useful).
+The `EIntegrable` predicate we introduce in this file states that at least one of the integrals
+of the positive and negative parts is finite.
+
+## Main definitions
+
+* `EIntegrable f μ`: A condition ensuring the integral of `f : α → EReal` with respect to `μ` is
+  well-defined (avoiding `⊤ - ⊤`), which is that at least one of the integrals of the positive and
+  negative parts of the function is finite.
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal NNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → EReal}
+
+/-- Condition for a function to have a well-defined extended integral,
+avoiding the `⊤ - ⊤` bad case in the definition. -/
+def EIntegrable (f : α → EReal) (μ : Measure α := by volume_tac) : Prop :=
+  ∫⁻ x, (f x).toENNReal ∂μ ≠ ⊤ ∨ ∫⁻ x, (-f x).toENNReal ∂μ ≠ ⊤
+
+lemma eintegrable_congr (h_ae : f =ᵐ[μ] g) :
+    EIntegrable f μ ↔ EIntegrable g μ := by
+  suffices ∀ {f g : α → EReal} (h_ae : f =ᵐ[μ] g) (hf : EIntegrable f μ), EIntegrable g μ from
+    ⟨fun h ↦ this h_ae h, fun h ↦ this h_ae.symm h⟩
+  intro f g h_ae hf
+  cases hf with
+  | inl hf =>
+    left
+    convert hf using 1
+    refine lintegral_congr_ae ?_
+    filter_upwards [h_ae] with x hx using by simp [hx]
+  | inr hf =>
+    right
+    convert hf using 1
+    refine lintegral_congr_ae ?_
+    filter_upwards [h_ae] with x hx using by simp [hx]
+
+lemma eintegrable_of_nonneg (hf : ∀ x, 0 ≤ f x) : EIntegrable f μ := by right; simp [hf]
+
+lemma eintegrable_of_nonpos (hf : ∀ x, f x ≤ 0) : EIntegrable f μ := by left; simp [hf]
+
+@[simp]
+lemma eintegrable_const {μ : Measure α} {c : EReal} : EIntegrable (fun _ ↦ c) μ := by
+  rcases le_total c 0 with hc | hc <;> simp [EIntegrable, hc]
+
+@[simp]
+lemma eintegrable_zero {μ : Measure α} : EIntegrable 0 μ := by simp [EIntegrable]
+
+lemma EIntegrable.neg (hf : EIntegrable f μ) : EIntegrable (fun x ↦ - f x) μ := by
+  cases hf with
+  | inl h => right; simpa
+  | inr h => left; simpa
+
+lemma EIntegrable.real_const_mul {c : ℝ} (hf : EIntegrable f μ) :
+    EIntegrable (fun x ↦ c * f x) μ := by
+  rcases le_total 0 c with hc | hc
+  · have hc' : 0 ≤ (c : EReal) := by simp [hc]
+    cases hf with
+    | inl h =>
+      left
+      simp only [EReal.toENNReal_mul hc', ne_eq, EReal.coe_ne_top, not_false_eq_true,
+        EReal.toENNReal_of_ne_top, EReal.toReal_coe]
+      rw [lintegral_const_mul' _ _ (by simp)]
+      exact ENNReal.mul_ne_top (by simp) h
+    | inr h =>
+      right
+      simp_rw [mul_comm _ (f _), ← EReal.neg_mul, EReal.toENNReal_mul' hc']
+      rw [lintegral_mul_const' _ _ (by simp)]
+      exact ENNReal.mul_ne_top h (by simp)
+  · have hc' : 0 ≤ -(c : EReal) := by simp [hc]
+    cases hf with
+    | inl h =>
+      right
+      simp only [ne_eq]
+      simp_rw [← EReal.neg_mul, EReal.toENNReal_mul hc']
+      rw [lintegral_const_mul' _ _ (by simp)]
+      exact ENNReal.mul_ne_top (by simp) h
+    | inr h =>
+      left
+      have h_eq_neg x : c * f x = (-(c : EReal) * -f x) := by simp
+      simp_rw [h_eq_neg, EReal.toENNReal_mul hc']
+      rw [lintegral_const_mul' _ _ (by simp)]
+      exact ENNReal.mul_ne_top (by simp) h
+
+lemma EIntegrable.const_mul {c : EReal} (hf : EIntegrable f μ) (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) :
+    EIntegrable (fun x ↦ c * f x) μ := by
+  lift c to ℝ using ⟨hc_top, hc_bot⟩
+  exact hf.real_const_mul
+
+lemma EIntegrable.add_real_const [IsFiniteMeasure μ] {c : ℝ} (hf : EIntegrable f μ) :
+    EIntegrable (fun x ↦ f x + c) μ := by
+  cases hf with
+  | inl h =>
+    left
+    have h' : ∫⁻ x, (f x).toENNReal + ENNReal.ofReal c ∂μ ≠ ∞ := by
+      rw [lintegral_add_right _ (by fun_prop)]
+      simp only [lintegral_const, ne_eq, ENNReal.add_eq_top, h, false_or]
+      exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)
+    refine ne_top_of_le_ne_top h' ?_
+    gcongr with x
+    exact EReal.toENNReal_add_le
+  | inr h =>
+    right
+    simp_rw [EReal.neg_add (.inr (by simp : (c : EReal) ≠ ⊤)) (.inr (by simp : (c : EReal) ≠ ⊥))]
+    have h' : ∫⁻ x, (-f x).toENNReal + ENNReal.ofReal (-c) ∂μ ≠ ∞ := by
+      rw [lintegral_add_right _ (by fun_prop)]
+      simp only [lintegral_const, ne_eq, ENNReal.add_eq_top, h, false_or]
+      exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)
+    refine ne_top_of_le_ne_top h' ?_
+    gcongr with x
+    simp_rw [sub_eq_add_neg]
+    exact EReal.toENNReal_add_le
+
+lemma EIntegrable.add_const [IsFiniteMeasure μ] {c : EReal}
+    (hf : EIntegrable f μ) (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) :
+    EIntegrable (fun x ↦ f x + c) μ := by
+  lift c to ℝ using ⟨hc_top, hc_bot⟩
+  exact hf.add_real_const
+
+lemma EIntegrable.real_const_add [IsFiniteMeasure μ] {c : ℝ} (hf : EIntegrable f μ) :
+    EIntegrable (fun x ↦ c + f x) μ := by
+  simp_rw [add_comm]
+  exact hf.add_real_const
+
+lemma EIntegrable.const_add [IsFiniteMeasure μ] {c : EReal}
+    (hf : EIntegrable f μ) (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) :
+    EIntegrable (fun x ↦ c + f x) μ := by
+  lift c to ℝ using ⟨hc_top, hc_bot⟩
+  exact hf.real_const_add
+
+lemma EIntegrable.sub_real_const [IsFiniteMeasure μ] {c : ℝ} (hf : EIntegrable f μ) :
+    EIntegrable (fun x ↦ f x - c) μ := by
+  simp_rw [sub_eq_add_neg]
+  exact hf.add_real_const
+
+lemma EIntegrable.sub_const [IsFiniteMeasure μ] {c : EReal}
+    (hf : EIntegrable f μ) (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) :
+    EIntegrable (fun x ↦ f x - c) μ := by
+  simp_rw [sub_eq_add_neg]
+  exact hf.add_const (by simp [hc_top]) (by simp [hc_bot])
+
+lemma EIntegrable.real_const_sub [IsFiniteMeasure μ] {c : ℝ} (hf : EIntegrable f μ) :
+    EIntegrable (fun x ↦ c - f x) μ := by
+  simp_rw [sub_eq_add_neg]
+  exact hf.neg.real_const_add
+
+lemma EIntegrable.const_sub [IsFiniteMeasure μ] {c : EReal}
+    (hf : EIntegrable f μ) (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) :
+    EIntegrable (fun x ↦ c - f x) μ := by
+  simp_rw [sub_eq_add_neg]
+  exact hf.neg.const_add hc_bot hc_top
+
+lemma EIntegrable.smul_measure (hf : EIntegrable f μ) {c : ℝ≥0∞} (hc : c ≠ ∞) :
+    EIntegrable f (c • μ) := by
+  cases hf with
+  | inl hf => left; simp [hc, hf, ENNReal.mul_eq_top]
+  | inr hf => right; simp [hc, hf, ENNReal.mul_eq_top]
+
+lemma EIntegrable.nnreal_smul_measure (hf : EIntegrable f μ) (c : ℝ≥0) :
+    EIntegrable f (c • μ) := hf.smul_measure (by simp)
+
+lemma eintegrable_map {β : Type*} {mβ : MeasurableSpace β} {f : α → β} {g : β → EReal}
+    (hf : AEMeasurable f μ) (hg : AEMeasurable g (μ.map f)) :
+    EIntegrable g (μ.map f) ↔ EIntegrable (g ∘ f) μ := by
+  unfold EIntegrable
+  congr! <;> rw [lintegral_map' (by fun_prop) hf] <;> rfl
+
+lemma eintegrable_of_le {b : EReal} (hf : ∀ x, f x ≤ b) (hb : b ≠ ⊤)
+    (P : Measure α) [IsFiniteMeasure P] :
+    EIntegrable f P := by
+  refine .inl (ne_of_lt ?_)
+  calc ∫⁻ x, (f x).toENNReal ∂P
+  _ ≤ ∫⁻ x, b.toENNReal ∂P := by gcongr; exact hf _
+  _ = b.toENNReal * P .univ := by simp [lintegral_const]
+  _ < ⊤ := by simp [hb, lt_top_iff_ne_top, ENNReal.mul_eq_top]
+
+end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Integral/EReal/EIntegral.lean b/Mathlib/MeasureTheory/Integral/EReal/EIntegral.lean
new file mode 100644
index 00000000000000..d301230372c366
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/EIntegral.lean
@@ -0,0 +1,847 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.Lebesgue.Countable
+public import Mathlib.MeasureTheory.Integral.Lebesgue.Markov
+public import Mathlib.MeasureTheory.Integral.EReal.AuxLemmas
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegrable
+
+/-!
+# Extended Real Integral
+
+This file defines integration for functions taking values in `EReal` (the extended reals).
+
+## Main definitions
+
+* `eintegral`: The integral of an `EReal`-valued function, defined as the difference
+  between the lower Lebesgue integrals of the positive and negative parts.
+* `EIntegrable`: A condition ensuring the integral is well-defined (avoiding `⊤ - ⊤`).
+* instances for positive and negative parts of an `EReal`-valued function.
+
+## Main statements
+
+* `eintegral_add`: The integral of a sum is the sum of integrals (under suitable integrability
+  conditions to avoid indeterminate forms).
+* `eintegral_sub`: The integral of a difference is the difference of integrals (under suitable
+  integrability conditions).
+
+## Notation
+
+* `∫ᵉ x, f x ∂μ`: The extended integral of `f` with respect to measure `μ`.
+* `f⁺` and `f⁻`: Positive and negative parts of a function.
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → EReal}
+
+/-- The integral of an `EReal`-valued function with respect to a measure `μ`, defined as the
+difference of the Lebesgue integrals of its positive and negative parts.
+
+If both integrals are infinite, the result is `⊥`. See also `EIntegrable`, which is the property
+that at least one of the integrals is finite. -/
+noncomputable def eintegral (μ : Measure α) (f : α → EReal) : EReal :=
+    ∫⁻ x, (f x).toENNReal ∂μ - ∫⁻ x, (-f x).toENNReal ∂μ
+
+@[inherit_doc MeasureTheory.eintegral]
+notation3 "∫ᵉ "(...)", "r:60:(scoped f => f)" ∂"μ:70 => eintegral μ r
+
+@[inherit_doc MeasureTheory.eintegral]
+notation3 "∫ᵉ "(...)", "r:60:(scoped f => eintegral volume f) => r
+
+@[inherit_doc MeasureTheory.eintegral]
+notation3 "∫ᵉ "(...)" in "s", "r:60:(scoped f => f)" ∂"μ:70 =>
+    eintegral (Measure.restrict μ s) r
+
+@[inherit_doc MeasureTheory.eintegral]
+notation3 "∫ᵉ "(...)" in "s", "r:60:(scoped f => eintegral (Measure.restrict volume s) f) => r
+
+@[simp]
+lemma eintegral_of_not_eintegrable (hf : ¬ EIntegrable f μ) :
+    ∫ᵉ x, f x ∂μ = ⊥ := by
+  simp only [EIntegrable, ne_eq, not_or, Decidable.not_not] at hf
+  simp [eintegral, hf]
+
+lemma eintegrable_of_eintegral_ne_bot (hf : ∫ᵉ x, f x ∂μ ≠ ⊥) : EIntegrable f μ := by
+  contrapose! hf
+  exact eintegral_of_not_eintegrable hf
+
+@[simp]
+lemma eintegral_zero (μ : Measure α) : ∫ᵉ _, (0 : EReal) ∂μ = 0 := by simp [eintegral]
+
+@[simp]
+lemma eintegral_zero_measure (f : α → EReal) : ∫ᵉ x, f x ∂(0 : Measure α) = 0 := by simp [eintegral]
+
+lemma eintegral_congr (h : ∀ x, f x = g x) : ∫ᵉ x, f x ∂μ = ∫ᵉ x, g x ∂μ := by simp_rw [h]
+
+/-- The extended integral is compatible with almost-everywhere equality. -/
+lemma eintegral_congr_ae (h : ∀ᵐ x ∂μ, f x = g x) : ∫ᵉ x, f x ∂μ = ∫ᵉ x, g x ∂μ := by
+  simp_rw [eintegral]
+  congr 2 <;> exact lintegral_congr_ae <| by filter_upwards [h] with x hx using by rw [hx]
+
+lemma eintegral_of_nonneg (hf : ∀ x, 0 ≤ f x) : ∫ᵉ x, f x ∂μ = ∫⁻ x, (f x).toENNReal ∂μ := by
+  simp [eintegral, hf]
+
+lemma eintegral_of_ae_nonneg (hf : AEMeasurable f μ) (hf_nonneg : ∀ᵐ x ∂μ, 0 ≤ f x) :
+    ∫ᵉ x, f x ∂μ = ∫⁻ x, (f x).toENNReal ∂μ := by
+  rw [eintegral]
+  suffices ∫⁻ x, (-f x).toENNReal ∂μ = 0 by simp [this]
+  rw [lintegral_eq_zero_iff']
+  · filter_upwards [hf_nonneg] with x hx using by simp [hx]
+  · fun_prop
+
+lemma eintegral_of_nonpos (hf : ∀ x, f x ≤ 0) : ∫ᵉ x, f x ∂μ = - ∫⁻ x, (-f x).toENNReal ∂μ := by
+  simp [eintegral, hf]
+
+lemma eintegral_of_ae_nonpos (hf : AEMeasurable f μ) (hf_nonpos : ∀ᵐ x ∂μ, f x ≤ 0) :
+    ∫ᵉ x, f x ∂μ = - ∫⁻ x, (-f x).toENNReal ∂μ := by
+  rw [eintegral]
+  suffices ∫⁻ x, (f x).toENNReal ∂μ = 0 by simp [this]
+  rw [lintegral_eq_zero_iff']
+  · filter_upwards [hf_nonpos] with x hx using by simp [hx]
+  · fun_prop
+
+lemma eintegral_nonneg (hf : ∀ x, 0 ≤ f x) : 0 ≤ ∫ᵉ x, f x ∂μ := by
+  rw [eintegral_of_nonneg hf]
+  positivity
+
+lemma eintegral_nonneg' (hf_meas : AEMeasurable f μ) (hf : ∀ᵐ x ∂μ, 0 ≤ f x) :
+    0 ≤ ∫ᵉ x, f x ∂μ := by
+  rw [eintegral_of_ae_nonneg hf_meas hf]
+  positivity
+
+lemma eintegral_nonpos (hf : ∀ x, f x ≤ 0) : ∫ᵉ x, f x ∂μ ≤ 0 := by
+  rw [eintegral_of_nonpos hf]
+  simp only [EReal.neg_le_zero]
+  positivity
+
+lemma eintegral_nonpos' (hf_meas : AEMeasurable f μ) (hf : ∀ᵐ x ∂μ, f x ≤ 0) :
+    ∫ᵉ x, f x ∂μ ≤ 0 := by
+  rw [eintegral_of_ae_nonpos hf_meas hf]
+  simp only [EReal.neg_le_zero]
+  positivity
+
+@[simp]
+lemma eintegral_const (c : EReal) (μ : Measure α) : ∫ᵉ _, c ∂μ = c * (μ Set.univ : EReal) := by
+  rcases le_total 0 c with hc | hc
+  · rw [eintegral_of_nonneg (fun _ ↦ hc)]
+    simp only [lintegral_const, EReal.coe_ennreal_mul]
+    rw [EReal.coe_toENNReal hc]
+  · rw [eintegral_of_nonpos (fun _ ↦ hc)]
+    simp only [lintegral_const, EReal.coe_ennreal_mul]
+    rw [EReal.coe_toENNReal]
+    · simp
+    · exact EReal.neg_nonneg.mpr hc
+
+lemma eintegral_lt_top_of_le {f : α → EReal} {b : EReal} (hf : ∀ x, f x ≤ b) (hb : b ≠ ⊤)
+    (P : Measure α) [IsFiniteMeasure P] :
+    ∫ᵉ x, f x ∂P < ⊤ := by
+  rw [eintegral]
+  calc (∫⁻ x, (f x).toENNReal ∂P : EReal) - ∫⁻ x, (-f x).toENNReal ∂P
+  _ ≤ ∫⁻ x, (f x).toENNReal ∂P - 0 := EReal.sub_le_sub le_rfl (by positivity)
+  _ ≤ ∫⁻ x, b.toENNReal ∂P := by
+    simp only [sub_zero]
+    gcongr
+    exact hf _
+  _ = b.toENNReal * P .univ := by simp [lintegral_const]
+  _ < ⊤ := by
+    norm_cast
+    rw [lt_top_iff_ne_top, ne_eq, EReal.coe_ennreal_eq_top_iff]
+    simp [hb, ENNReal.mul_eq_top]
+
+lemma setEIntegral_measure_zero {μ : Measure α} (s : Set α) (f : α → EReal) (hs' : μ s = 0) :
+    ∫ᵉ x in s, f x ∂μ = 0 := by
+  simp [eintegral, setLIntegral_measure_zero s _ hs']
+
+/-- The extended integral is monotone with respect to almost-everywhere inequality. -/
+lemma eintegral_mono_ae (hfg : f ≤ᵐ[μ] g) : ∫ᵉ x, f x ∂μ ≤ ∫ᵉ x, g x ∂μ := by
+  refine EReal.sub_le_sub ?_ ?_
+  · rw [EReal.coe_ennreal_le_coe_ennreal_iff]
+    refine lintegral_mono_ae ?_
+    filter_upwards [hfg] with x hfgx
+    exact EReal.toENNReal_le_toENNReal hfgx
+  · rw [EReal.coe_ennreal_le_coe_ennreal_iff]
+    refine lintegral_mono_ae ?_
+    filter_upwards [hfg] with x hfgx
+    rw [← EReal.neg_le_neg_iff] at hfgx
+    exact EReal.toENNReal_le_toENNReal hfgx
+
+@[gcongr]
+lemma eintegral_mono (hfg : f ≤ g) : ∫ᵉ x, f x ∂μ ≤ ∫ᵉ x, g x ∂μ :=
+  eintegral_mono_ae <| ae_of_all _ hfg
+
+-- TODO: rename
+lemma eintegral_neg_eq_top_eq_bot (hf_neg_top : ∫⁻ x, (-f x).toENNReal ∂μ = ⊤) :
+    ∫ᵉ x, f x ∂μ = ⊥ := by
+  simp [eintegral, hf_neg_top]
+
+/-- The extended integral is strictly monotone with respect to almost-everywhere strict
+inequality. -/
+lemma eintegral_strict_mono_ae (hμ : μ ≠ 0) (hg : AEMeasurable g μ) (hf : AEMeasurable f μ)
+    (hfg : ∀ᵐ x ∂μ, f x < g x) (hfi : ∫ᵉ x, f x ∂μ < ⊤) (hgi : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x ∂μ < ∫ᵉ x, g x ∂μ := by
+  by_cases hg_top : ∫ᵉ x, g x ∂μ = ⊤
+  · simpa [hg_top]
+  by_cases hf_neg_top : ∫⁻ x, (-f x).toENNReal ∂μ = ⊤
+  · have := eintegral_neg_eq_top_eq_bot hf_neg_top
+    simp_all only [bot_lt_top, gt_iff_lt]
+    exact Ne.bot_lt' hgi.symm
+  obtain ⟨s, hμs, h_cases⟩ : ∃ s, μ s ≠ 0 ∧
+      ((∀ ⦃x⦄, x ∈ s → 0 ≤ f x ∧ f x < g x) ∨
+      (∀ ⦃x⦄, x ∈ s → g x ≤ 0 ∧ f x < g x) ∨
+      (∀ ⦃x⦄, x ∈ s → f x < 0 ∧ 0 < g x ∧ f x < g x)) := by
+    let S := {x | f x < g x}
+    let S₁ := S ∩ {x | 0 ≤ f x}
+    let S₂ := S ∩ {x | g x ≤ 0}
+    let S₃ := S ∩ {x | f x < 0 ∧ 0 < g x}
+    have : μ S₁ ≠ 0 ∨ μ S₂ ≠ 0 ∨ μ S₃ ≠ 0 := by
+      by_contra! h_zero
+      have : 0 < μ (S₁ ∪ S₂ ∪ S₃) := by
+        have hS_eq_union : S = S₁ ∪ S₂ ∪ S₃ := by ext; grind
+        rw [← hS_eq_union]
+        refine pos_of_ne_zero ?_
+        rw [measure_of_measure_compl_eq_zero hfg]
+        exact μ.measure_univ_ne_zero.mpr hμ
+      have : μ (S₁ ∪ S₂ ∪ S₃) ≤ 0 := by
+        calc
+        _ ≤ μ (S₁ ∪ S₂) + μ S₃ := measure_union_le _ _
+        _ ≤ μ S₁ + μ S₂ + μ S₃ := by
+          gcongr
+          exact measure_union_le _ _
+        _ = 0 := by simp [h_zero]
+      grind
+    rcases this with hμ1 | hμ2 | hμ3
+    · exact ⟨S₁, hμ1, by grind⟩
+    · exact ⟨S₂, hμ2, by grind⟩
+    · exact ⟨S₃, hμ3, by grind⟩
+  simp only [eintegral]
+  rcases h_cases with h_pos | h_neg | h_mixed
+  · refine EReal.sub_lt_sub_of_lt_of_le ?_ ?_ (by simp) (by simpa)
+    · norm_cast
+      refine lintegral_strict_mono_of_ae_le_of_ae_lt_on (by fun_prop) ?_ ?_ hμs ?_
+      · by_contra!
+        simp_all [eintegral]
+      · filter_upwards [hfg] with x hx
+        exact EReal.toENNReal_le_toENNReal hx.le
+      · filter_upwards with x hxs
+        exact EReal.toENNReal_lt_toENNReal (h_pos hxs).1 (h_pos hxs).2
+    · norm_cast
+      refine lintegral_mono_ae ?_
+      filter_upwards [hfg] with x hx
+      refine EReal.toENNReal_le_toENNReal ?_
+      exact EReal.neg_le_neg_iff.mpr hx.le
+  · refine EReal.sub_lt_sub_of_le_of_gt ?_ ?_ ?_ (by simp)
+    · norm_cast
+      refine lintegral_mono_ae ?_
+      filter_upwards [hfg] with x hx
+      exact EReal.toENNReal_le_toENNReal hx.le
+    · norm_cast
+      refine lintegral_strict_mono_of_ae_le_of_ae_lt_on (by fun_prop) ?_ ?_ hμs ?_
+      · by_contra!
+        simp_all [eintegral]
+      · filter_upwards [hfg] with x hx
+        refine EReal.toENNReal_le_toENNReal ?_
+        exact EReal.neg_le_neg_iff.mpr hx.le
+      · filter_upwards with x hxs
+        refine EReal.toENNReal_lt_toENNReal ?_ ?_
+        · exact EReal.neg_nonneg.mpr (h_neg hxs).1
+        · exact EReal.neg_lt_neg_iff.mpr (h_neg hxs).2
+    · by_contra! h
+      simp_all only [ne_eq, eintegral, EReal.coe_ennreal_eq_top_iff]
+      by_cases h_neg_top : ∫⁻ x, (-g x).toENNReal ∂μ = ∞ <;> simp_all
+  · refine EReal.sub_lt_sub_of_lt_of_le ?_ ?_ (by simp) (by simpa)
+    · norm_cast
+      refine lintegral_strict_mono_of_ae_le_of_ae_lt_on (by fun_prop) ?_ ?_ hμs ?_
+      · by_contra!
+        simp_all [eintegral]
+      · filter_upwards [hfg] with x hx
+        exact EReal.toENNReal_le_toENNReal hx.le
+      · filter_upwards with x hxs
+        specialize h_mixed hxs
+        have : f x ≤ 0 := h_mixed.1.le
+        simp_all
+    · norm_cast
+      refine lintegral_mono_ae ?_
+      filter_upwards [hfg] with x hx
+      refine EReal.toENNReal_le_toENNReal ?_
+      exact EReal.neg_le_neg_iff.mpr hx.le
+
+lemma eintegral_strict_mono (hμ : μ ≠ 0) (hg : AEMeasurable g μ) (hf : AEMeasurable f μ)
+    (hfg : ∀ x, f x < g x) (hfi : ∫ᵉ x, f x ∂μ < ⊤) (hgi : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x ∂μ < ∫ᵉ x, g x ∂μ :=
+  eintegral_strict_mono_ae hμ hg hf (ae_of_all μ hfg) hfi hgi
+
+lemma eintegral_add_compl {A : Set α} (hA : MeasurableSet A) :
+    ∫ᵉ x in A, f x ∂μ + ∫ᵉ x in Aᶜ, f x ∂μ = ∫ᵉ x, f x ∂μ := by
+  simp only [eintegral]
+  symm
+  rw [← lintegral_add_compl (f := fun x ↦ (f x).toENNReal) hA,
+    ← lintegral_add_compl (f := fun x ↦ (-f x).toENNReal) hA]
+  push_cast
+  rw [EReal.add_sub_add_comm (by simp) (by simp)]
+
+lemma ae_ne_bot_of_eintegral_ne_bot (hf_meas : AEMeasurable f μ) (hf : ∫ᵉ x, f x ∂μ ≠ ⊥) :
+    ∀ᵐ x ∂μ, f x ≠ ⊥ := by
+  rw [eintegral, sub_eq_add_neg, ne_eq, EReal.add_eq_bot_iff] at hf
+  simp only [EReal.coe_ennreal_ne_bot, EReal.neg_eq_bot_iff, EReal.coe_ennreal_eq_top_iff,
+    false_or] at hf
+  have h := ae_lt_top' (by fun_prop) hf
+  filter_upwards [h] with x hx
+  rw [lt_top_iff_ne_top, ne_eq, EReal.toENNReal_eq_top_iff] at hx
+  simpa using hx
+
+lemma eintegral_sub_of_nonneg_of_eq_zero (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, 0 ≤ g x)
+    (h_or : ∀ x, f x = 0 ∨ g x = 0) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  simp_rw [eintegral_of_nonneg hf, eintegral_of_nonneg hg, eintegral]
+  congr with x
+  · cases h_or x with
+    | inl h =>
+      simp only [h, zero_sub, ne_eq, EReal.zero_ne_top, not_false_eq_true,
+        EReal.toENNReal_of_ne_top, EReal.toReal_zero, ENNReal.ofReal_zero]
+      rw [EReal.toENNReal_of_nonpos]
+      simp [hg x]
+    | inr h => simp [h]
+  · by_cases hg_top : g x = ⊤
+    · simp [hg_top]
+    rw [EReal.neg_sub]
+    · cases h_or x with
+      | inl h => simp [h]
+      | inr h =>
+        simp only [h, add_zero, ne_eq, EReal.zero_ne_top, not_false_eq_true,
+          EReal.toENNReal_of_ne_top, EReal.toReal_zero, ENNReal.ofReal_zero]
+        rw [EReal.toENNReal_of_nonpos]
+        simp [hf x]
+    · left
+      specialize hf x
+      intro h_false
+      simp [h_false] at hf
+    · exact .inr hg_top
+
+lemma eintegral_sub_of_nonneg_of_eq_zero_ae (hf : ∀ᵐ x ∂μ, 0 ≤ f x) (hg : ∀ᵐ x ∂μ, 0 ≤ g x)
+    (h_or : ∀ᵐ x ∂μ, f x = 0 ∨ g x = 0) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  let f' := fun x ↦ if (0 ≤ f x ∧ 0 ≤ g x ∧ (f x = 0 ∨ g x = 0)) then f x else 0
+  let g' := fun x ↦ if (0 ≤ f x ∧ 0 ≤ g x ∧ (f x = 0 ∨ g x = 0)) then g x else 0
+  have hf' x : 0 ≤ f' x := by simp only [f']; split_ifs with h <;> simp [h]
+  have hg' x : 0 ≤ g' x := by simp only [g']; split_ifs with h <;> simp [h]
+  have h_or' x : f' x = 0 ∨ g' x = 0 := by
+    simp only [f', g']; split_ifs with h <;> simp [h]
+  have hf_eq : ∀ᵐ x ∂μ, f x = f' x := by
+    filter_upwards [hf, hg, h_or] with x hf_x hg_x h_or_x
+    simp [f', hf_x, hg_x, h_or_x]
+  have hg_eq : ∀ᵐ x ∂μ, g x = g' x := by
+    filter_upwards [hf, hg, h_or] with x hf_x hg_x h_or_x
+    simp [g', hf_x, hg_x, h_or_x]
+  have hf_sub_g : ∀ᵐ x ∂μ, f x - g x = f' x - g' x := by
+    filter_upwards [hf_eq, hg_eq] with x hfx hgx
+    rw [hfx, hgx]
+  rw [eintegral_congr_ae hf_eq, eintegral_congr_ae hg_eq, eintegral_congr_ae hf_sub_g,
+    eintegral_sub_of_nonneg_of_eq_zero hf' hg' h_or']
+
+/-- The extended integral decomposes as the difference between the integrals of the positive
+and negative parts of the function. -/
+lemma eintegral_eq_posPartFun_sub_negPartFun (f : α → EReal) :
+    ∫ᵉ x, f x ∂μ = ∫ᵉ x, f⁺ x ∂μ - ∫ᵉ x, f⁻ x ∂μ := by
+  rw [← eintegral_sub_of_nonneg_of_eq_zero (posPart_nonneg f) (negPart_nonneg f)
+    (EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f)]
+  simp_rw [← EReal.posPart_fun_sub_negPart_fun_apply f]
+
+lemma EIntegrable.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top
+    (hf : EIntegrable f μ) :
+    ∫ᵉ x, f⁺ x ∂μ ≠ ⊤ ∨ ∫ᵉ x, f⁻ x ∂μ ≠ ⊤ := by
+  rcases hf with h | h
+  · left
+    rw [eintegral_of_nonneg (posPart_nonneg f)]
+    simp only [ne_eq, EReal.coe_ennreal_eq_top_iff, posPart_def]
+    convert h using 4 with x
+    rcases le_total 0 (f x) with h | h <;> simp [h]
+  · right
+    rw [eintegral_of_nonneg (negPart_nonneg f)]
+    simp only [ne_eq, EReal.coe_ennreal_eq_top_iff, negPart_def]
+    convert h using 4 with x
+    rcases le_total 0 (f x) with h | h <;> simp [h]
+
+lemma eintegral_negPartFun_ne_top (hf_bot : ∫ᵉ x, f x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f⁻ x ∂μ ≠ ⊤ := by
+  rw [eintegral_eq_posPartFun_sub_negPartFun, sub_eq_add_neg, ne_eq, EReal.add_eq_bot_iff] at hf_bot
+  simp only [EReal.neg_eq_bot_iff, not_or] at hf_bot
+  exact hf_bot.2
+
+lemma eintegral_posPartFun_ne_top (hf_bot : ∫ᵉ x, f x ∂μ ≠ ⊥) (hf_top : ∫ᵉ x, f x ∂μ ≠ ⊤) :
+    ∫ᵉ x, f⁺ x ∂μ ≠ ⊤ := by
+  by_contra h
+  rw [eintegral_eq_posPartFun_sub_negPartFun, h, EReal.top_sub] at hf_top
+  · exact hf_top rfl
+  · exact eintegral_negPartFun_ne_top hf_bot
+
+lemma ae_ne_top_of_eintegral_ne_top (hf_meas : AEMeasurable f μ) (hf_bot : ∫ᵉ x, f x ∂μ ≠ ⊥)
+    (hf_top : ∫ᵉ x, f x ∂μ ≠ ⊤) :
+    ∀ᵐ x ∂μ, f x ≠ ⊤ := by
+  suffices ∀ᵐ x ∂μ, f⁺ x < ⊤ by
+    filter_upwards [this] with x hfx using by simpa [posPart_def, lt_top_iff_ne_top] using hfx
+  have h_pos_ne_top : ∫ᵉ x, f⁺ x ∂μ ≠ ⊤ := eintegral_posPartFun_ne_top hf_bot hf_top
+  rw [eintegral_of_nonneg (posPart_nonneg f), ne_eq, EReal.coe_ennreal_eq_top_iff]
+    at h_pos_ne_top
+  have h_lt_top : ∀ᵐ x ∂μ, (f⁺ x).toENNReal < ⊤ := ae_lt_top' (by fun_prop) h_pos_ne_top
+  filter_upwards [h_lt_top] with x hx
+  rwa [lt_top_iff_ne_top, ne_eq, EReal.toENNReal_eq_top_iff, ← ne_eq, ← lt_top_iff_ne_top] at hx
+
+lemma lintegral_enorm_eq_posPartFun_add_negPartFun (hf : AEMeasurable f μ) :
+    ∫⁻ x, ‖f x‖ₑ ∂μ = ∫ᵉ x, f⁺ x ∂μ + ∫ᵉ x, f⁻ x ∂μ := by
+  simp_rw [enorm]
+  rw [lintegral_add_left' (by fun_prop), eintegral_of_nonneg (posPart_nonneg f),
+    eintegral_of_nonneg (negPart_nonneg f)]
+  norm_cast
+
+lemma eintegral_eq_lintegral (f : α → ℝ≥0∞) : ∫ᵉ x, f x ∂μ = ∫⁻ x, f x ∂μ := by
+  rw [eintegral_of_nonneg (fun _ ↦ by positivity)]
+  simp
+
+lemma lintegral_eq_eintegral (f : α → ℝ≥0∞) : ∫⁻ x, f x ∂μ = (∫ᵉ x, f x ∂μ).toENNReal := by
+  rw [eintegral_of_nonneg (fun _ ↦ by positivity)]
+  simp
+
+lemma eintegral_real_const_mul_of_nonneg (c : ℝ) (hf : ∀ x, 0 ≤ f x) :
+    ∫ᵉ x, c * f x ∂μ = c * ∫ᵉ x, f x ∂μ := by
+  rcases le_total 0 c with hc | hc
+  · have hc' : 0 ≤ (c : EReal) := mod_cast hc
+    rw [eintegral_of_nonneg (fun x ↦ mul_nonneg hc' (hf x)), eintegral_of_nonneg hf]
+    simp_rw [EReal.toENNReal_mul hc']
+    simp only [ne_eq, EReal.coe_ne_top, not_false_eq_true, EReal.toENNReal_of_ne_top,
+      EReal.toReal_coe]
+    rw [lintegral_const_mul' _ _ (by simp)]
+    simp [hc]
+  · have hc' : (c : EReal) ≤ 0 := mod_cast hc
+    rw [eintegral_of_nonpos, eintegral_of_nonneg hf]
+    swap; · exact fun x ↦ EReal.mul_nonpos_iff.mpr <| by simp [hc, hf]
+    have : 0 ≤ - (c : EReal) := by simp [hc']
+    simp_rw [← EReal.neg_mul, EReal.toENNReal_mul this]
+    simp only [ne_eq, EReal.neg_eq_top_iff, EReal.coe_ne_bot, not_false_eq_true,
+      EReal.toENNReal_of_ne_top]
+    rw [lintegral_const_mul' _ _ (by simp)]
+    simp [hc]
+
+lemma eintegral_real_const_mul (c : ℝ) (hf : EIntegrable f μ) :
+    ∫ᵉ x, c * f x ∂μ = c * ∫ᵉ x, f x ∂μ := by
+  have h_mul x : c * (f⁺ x - f⁻ x) = c * f⁺ x - c * f⁻ x := by
+    rcases le_total 0 (f x) with h | h <;> simp [posPart_def, negPart_def, h]
+  simp_rw [eintegral_eq_posPartFun_sub_negPartFun f, ← EReal.posPart_fun_sub_negPart_fun_apply f,
+    h_mul]
+  rcases le_total 0 c with hc | hc
+  · have hc' : 0 ≤ (c : EReal) := mod_cast hc
+    rw [eintegral_sub_of_nonneg_of_eq_zero (fun x ↦ ?_) (fun x ↦ ?_) (fun x ↦ ?_),
+      eintegral_real_const_mul_of_nonneg _ (by simp),
+      eintegral_real_const_mul_of_nonneg _ (by simp)]
+    · rw [EReal.mul_sub_of_nonneg_of_ne_top hc' (by simp)]
+    · have : 0 ≤ f⁺ x := posPart_nonneg f x
+      positivity
+    · have : 0 ≤ f⁻ x := negPart_nonneg f x
+      positivity
+    · rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f x with h | h <;> simp [h]
+  · have hc' : (c : EReal) ≤ 0 := mod_cast hc
+    have h_sub x : c * f⁺ x - c * f⁻ x = (-c) * f⁻ x - (-c) * f⁺ x := by
+      rw [EReal.neg_mul, EReal.neg_mul, sub_eq_add_neg, sub_eq_add_neg, add_comm, neg_neg]
+    simp_rw [h_sub]
+    rw [eintegral_sub_of_nonneg_of_eq_zero]
+    rotate_left
+    · intro x
+      rw [EReal.mul_nonneg_iff]
+      simp [hc]
+    · intro x
+      rw [EReal.mul_nonneg_iff]
+      simp [hc]
+    · intro x
+      rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f x with h | h <;> simp [h]
+    simp_rw [← EReal.coe_neg]
+    rw [eintegral_real_const_mul_of_nonneg _ (by simp),
+      eintegral_real_const_mul_of_nonneg _ (by simp)]
+    · conv_rhs => rw [← neg_neg (c : EReal), neg_mul]
+      rw [EReal.mul_sub_of_nonneg_of_ne_top (by simp [hc]) (by simp)]
+      suffices ∀ (a b : EReal), 0 ≤ a → 0 ≤ b → (a ≠ ⊤ ∨ b ≠ ⊤) →
+          -c * b - -c * a = -(-c * a - -c * b) from
+        this _ _ (eintegral_nonneg (by simp)) (eintegral_nonneg (by simp))
+          hf.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top
+      intro a b ha hb h_or
+      cases h_or with
+      | inl h =>
+        rw [EReal.neg_sub, add_comm, ← sub_eq_add_neg]
+        · left; rw [EReal.mul_ne_bot]; simp [hc, ne_bot_of_le_ne_bot (by simp) ha]
+        · left; rw [EReal.mul_ne_top]; simp [hc, h]
+      | inr h =>
+        rw [EReal.neg_sub, add_comm, ← sub_eq_add_neg]
+        · left; rw [EReal.mul_ne_bot]; simp [hc, ne_bot_of_le_ne_bot (by simp) ha]
+        · right; rw [EReal.mul_ne_top]; simp [hc, h]
+
+lemma eintegral_const_mul {c : EReal} (hc_bot : c ≠ ⊥) (hc_top : c ≠ ⊤) (hf : EIntegrable f μ) :
+    ∫ᵉ x, c * f x ∂μ = c * ∫ᵉ x, f x ∂μ := by
+  lift c to ℝ using ⟨hc_top, hc_bot⟩ with c
+  exact eintegral_real_const_mul c hf
+
+lemma eintegral_neg (hf : EIntegrable f μ) :
+    ∫ᵉ x, -f x ∂μ = - ∫ᵉ x, f x ∂μ := by
+  have h₁ : ∀ x, -f x = (-1 : EReal) * f x := fun _ ↦ (neg_one_mul _).symm
+  simp_rw [h₁]
+  rw [eintegral_const_mul (by norm_cast) (by norm_cast) hf]
+  simp
+
+lemma eintegral_add_of_nonneg (hf_meas : AEMeasurable f μ)
+    (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, 0 ≤ g x) :
+    ∫ᵉ x, f x + g x ∂μ = ∫ᵉ x, f x ∂μ + ∫ᵉ x, g x ∂μ := by
+  rw [eintegral_of_nonneg (fun x ↦ add_nonneg (hf x) (hg x)),
+    eintegral_of_nonneg hf, eintegral_of_nonneg hg, ← EReal.coe_ennreal_add,
+    ← lintegral_add_left' (by fun_prop)]
+  simp_rw [EReal.toENNReal_add (hf _) (hg _)]
+
+lemma eintegral_add_of_nonneg_of_measurable'
+    (hf_meas : Measurable f) (hg_meas : Measurable g)
+    (hf : ∀ᵐ x ∂μ, 0 ≤ f x) (hg : ∀ᵐ x ∂μ, 0 ≤ g x) :
+    ∫ᵉ x, f x + g x ∂μ = ∫ᵉ x, f x ∂μ + ∫ᵉ x, g x ∂μ := by
+  let f' := fun x ↦ if (0 ≤ f x ∧ 0 ≤ g x) then f x else 0
+  let g' := fun x ↦ if (0 ≤ f x ∧ 0 ≤ g x) then g x else 0
+  have hf' x : 0 ≤ f' x := by simp only [f']; split_ifs with h <;> simp [h]
+  have hg' x : 0 ≤ g' x := by simp only [g']; split_ifs with h <;> simp [h]
+  have hf_eq : ∀ᵐ x ∂μ, f x = f' x := by
+    filter_upwards [hf, hg] with x hf_x hg_x using by simp [f', hf_x, hg_x]
+  have hg_eq : ∀ᵐ x ∂μ, g x = g' x := by
+    filter_upwards [hf, hg] with x hf_x hg_x using by simp [g', hf_x, hg_x]
+  have hf_add_g : ∀ᵐ x ∂μ, f x + g x = f' x + g' x := by
+    filter_upwards [hf_eq, hg_eq] with x hfx hgx
+    rw [hfx, hgx]
+  rw [eintegral_congr_ae hf_eq, eintegral_congr_ae hg_eq, eintegral_congr_ae hf_add_g,
+    eintegral_add_of_nonneg _ hf' hg']
+  refine (Measurable.ite ?_ hf_meas measurable_const).aemeasurable
+  exact MeasurableSet.inter (measurableSet_le measurable_const hf_meas)
+    (measurableSet_le measurable_const hg_meas)
+
+lemma eintegral_add_of_nonneg_ae (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ)
+    (hf : ∀ᵐ x ∂μ, 0 ≤ f x) (hg : ∀ᵐ x ∂μ, 0 ≤ g x) :
+    ∫ᵉ x, f x + g x ∂μ = ∫ᵉ x, f x ∂μ + ∫ᵉ x, g x ∂μ := by
+  rw [eintegral_congr_ae hf_meas.ae_eq_mk, eintegral_congr_ae hg_meas.ae_eq_mk,
+    ← eintegral_add_of_nonneg_of_measurable' hf_meas.measurable_mk hg_meas.measurable_mk]
+  · refine eintegral_congr_ae ?_
+    filter_upwards [hf_meas.ae_eq_mk, hg_meas.ae_eq_mk] with x hfx hgx using by rw [hfx, hgx]
+  · filter_upwards [hf_meas.ae_eq_mk, hf] with x hfx hfx_nonneg using by rwa [← hfx]
+  · filter_upwards [hg_meas.ae_eq_mk, hg] with x hgx hgx_nonneg using by rwa [← hgx]
+
+lemma eintegral_sub_of_nonneg (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, 0 ≤ g x)
+    (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ)
+    (hfg : ∫ᵉ x, min (f x) (g x) ∂μ ≠ ⊤) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  have hf_ne_bot x : f x ≠ ⊥ := fun h_false ↦ by simpa [h_false] using hf x
+  have hg_ne_bot x : g x ≠ ⊥ := fun h_false ↦ by simpa [h_false] using hg x
+  by_cases hg_top : ∀ᵐ x ∂μ, g x ≠ ⊤
+  swap
+  · -- right side is `⊥`
+    have h_imp : ∫ᵉ x, -g x ∂μ ≠ ⊥ → ∀ᵐ x ∂μ, -g x ≠ ⊥ := ae_ne_bot_of_eintegral_ne_bot hg_meas.neg
+    rw [← not_imp_not] at h_imp
+    simp only [ne_eq, EReal.neg_eq_bot_iff, Decidable.not_not] at h_imp
+    specialize h_imp hg_top
+    rw [eintegral_neg] at h_imp
+    swap; · exact eintegrable_of_nonneg hg
+    rw [sub_eq_add_neg, h_imp, EReal.add_bot]
+    -- left side is also `⊥`
+    have h_imp' : ∫ᵉ x, f x - g x ∂μ ≠ ⊥ → ∀ᵐ x ∂μ, f x - g x ≠ ⊥ :=
+      ae_ne_bot_of_eintegral_ne_bot (hf_meas.sub hg_meas)
+    rw [← not_imp_not] at h_imp'
+    simp only [ne_eq, Filter.not_eventually, Decidable.not_not] at h_imp'
+    refine h_imp' ?_
+    simp only [ne_eq, Filter.not_eventually, Decidable.not_not] at hg_top
+    exact hg_top.mono fun x hx ↦ by simp [hx]
+  let f' := fun x ↦ f x - min (f x) (g x)
+  let g' := fun x ↦ g x - min (f x) (g x)
+  have hf' : ∀ᵐ x ∂μ, 0 ≤ f' x := by
+    filter_upwards [hg_top] with x hgx
+    unfold f'
+    rw [EReal.sub_nonneg (by simp [hgx]) (by simp [hf_ne_bot])]
+    simp
+  have hg' : ∀ᵐ x ∂μ, 0 ≤ g' x := by
+    filter_upwards [hg_top] with x hgx
+    unfold g'
+    rw [EReal.sub_nonneg (by simp [hgx]) (by simp [hg_ne_bot])]
+    simp
+  have hf_eq : ∀ᵐ x ∂μ, f x = f' x + min (f x) (g x) := by
+    unfold f'
+    filter_upwards [hg_top] with x hgx
+    rcases le_total (f x) (g x) with h | h
+    · simp only [h, inf_of_le_left]
+      rw [EReal.sub_self (ne_top_of_le_ne_top hgx h) (hf_ne_bot x), zero_add]
+    · simp only [h, inf_of_le_right]
+      lift g x to ℝ using ⟨hgx, hg_ne_bot x⟩ with gx
+      rw [EReal.sub_add_cancel]
+  have hg_eq : ∀ᵐ x ∂μ, g x = g' x + min (f x) (g x) := by
+    unfold g'
+    filter_upwards [hg_top] with x hgx
+    rcases le_total (f x) (g x) with h | h
+    · simp only [h, inf_of_le_left]
+      lift f x to ℝ using ⟨ne_top_of_le_ne_top hgx h, hf_ne_bot x⟩ with gx
+      rw [EReal.sub_add_cancel]
+    · simp only [h, inf_of_le_right]
+      rw [EReal.sub_self hgx (hg_ne_bot x), zero_add]
+  have h_or : ∀ᵐ x ∂μ, f' x = 0 ∨ g' x = 0 := by
+    filter_upwards [hg_top] with x hgx
+    unfold f' g'
+    rcases le_total (f x) (g x) with h | h
+    · left
+      simp only [h, inf_of_le_left]
+      rw [EReal.sub_self _ (hf_ne_bot x)]
+      exact ne_top_of_le_ne_top hgx h
+    · right
+      simp only [h, inf_of_le_right]
+      rw [EReal.sub_self hgx (hg_ne_bot x)]
+  have hf_sub_g : ∀ᵐ x ∂μ, f x - g x = f' x - g' x := by
+    filter_upwards [hg_top] with x hgx
+    unfold f' g'
+    rcases le_total (f x) (g x) with h | h
+    · simp only [h, inf_of_le_left]
+      rw [EReal.sub_self, zero_sub, EReal.neg_sub, add_comm, ← sub_eq_add_neg]
+      · simp [hf_ne_bot x]
+      · simp [hgx]
+      · exact ne_top_of_le_ne_top hgx h
+      · exact hf_ne_bot x
+    · simp [h, inf_of_le_right, EReal.sub_self hgx (hg_ne_bot x)]
+  rw [eintegral_congr_ae hf_sub_g, eintegral_congr_ae hf_eq, eintegral_congr_ae hg_eq,
+    eintegral_sub_of_nonneg_of_eq_zero_ae hf' hg' h_or,
+    eintegral_add_of_nonneg_ae (by fun_prop) (by fun_prop) hg',
+    eintegral_add_of_nonneg_ae (by fun_prop) (by fun_prop) hf']
+  rotate_left
+  · filter_upwards with x using by simp [hf, hg]
+  · filter_upwards with x using by simp [hf, hg]
+  rw [EReal.add_sub_add_comm]
+  rotate_left
+  · left
+    refine ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg' ?_ hg'
+    simp only [g']; fun_prop
+  · right
+    exact ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp [hf, hg])
+  rw [EReal.sub_self hfg]
+  · simp
+  · exact ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp [hf, hg])
+
+/-- The extended integral of the difference of two ENNReal-valued functions (coerced to EReal) is
+the difference of their Lebesgue integrals, provided at least one of the integrals is finite. -/
+lemma eintegral_coe_ennreal_sub {u v : α → ℝ≥0∞} (hu : AEMeasurable u μ) (hv : AEMeasurable v μ)
+    (h : ∫⁻ x, u x ∂μ ≠ ⊤ ∨ ∫⁻ x, v x ∂μ ≠ ⊤) :
+    ∫ᵉ x, u x - v x ∂μ = ∫⁻ x, u x ∂μ - ∫⁻ x, v x ∂μ := by
+  rw [eintegral_sub_of_nonneg (fun _ ↦ by positivity) (fun _ ↦ by positivity)
+      (by fun_prop) (by fun_prop),
+    eintegral_eq_lintegral, eintegral_eq_lintegral]
+  rcases h with h | h
+  · have h' : ∫ᵉ x, u x ∂μ ≠ ⊤ := by simpa [eintegral_eq_lintegral]
+    exact ne_top_of_le_ne_top h' (eintegral_mono fun _ ↦ min_le_left _ _)
+  · have h' : ∫ᵉ x, v x ∂μ ≠ ⊤ := by simpa [eintegral_eq_lintegral]
+    exact ne_top_of_le_ne_top h' (eintegral_mono fun _ ↦ min_le_right _ _)
+
+/-- The integral of a sum is the sum of integrals (requires compatibility conditions to
+avoid `⊤ - ⊤`).
+
+See also `eintegral_add'` for a version with stronger hypotheses on `g` and weaker hypotheses
+on `f`. -/
+lemma eintegral_add (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hf_int : EIntegrable f μ) (hg_int : EIntegrable g μ)
+    (h_ne_bot_1 : ∫ᵉ x, f x ∂μ ≠ ⊥ ∨ ∫ᵉ x, g x ∂μ ≠ ⊤)
+    (h_ne_bot_2 : ∫ᵉ x, f x ∂μ ≠ ⊤ ∨ ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x + g x ∂μ = ∫ᵉ x, f x ∂μ + ∫ᵉ x, g x ∂μ := by
+  have hf_add_g : ∀ x, f x + g x = (f⁺ x + g⁺ x) - (f⁻ x + g⁻ x) := by
+    intro x
+    rw [← EReal.posPart_fun_sub_negPart_fun_apply f x,
+      ← EReal.posPart_fun_sub_negPart_fun_apply g x, EReal.add_sub_add_comm]
+    · left; exact ne_bot_of_le_ne_bot (by simp) (negPart_nonneg f x)
+    · right; exact ne_bot_of_le_ne_bot (by simp) (negPart_nonneg g x)
+  simp_rw [hf_add_g, ← EReal.posPart_fun_sub_negPart_fun_apply f,
+    ← EReal.posPart_fun_sub_negPart_fun_apply g]
+  rw [eintegral_sub_of_nonneg_of_eq_zero (by simp) (by simp)
+      (EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f),
+    eintegral_sub_of_nonneg_of_eq_zero (by simp) (by simp)
+      (EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero g)]
+  have : ∫ᵉ x, f⁺ x ∂μ - ∫ᵉ x, f⁻ x ∂μ + (∫ᵉ x, g⁺ x ∂μ - ∫ᵉ x, g⁻ x ∂μ)
+      = ∫ᵉ x, f⁺ x ∂μ + ∫ᵉ x, g⁺ x ∂μ - (∫ᵉ x, f⁻ x ∂μ + ∫ᵉ x, g⁻ x ∂μ) := by
+    rw [EReal.add_sub_add_comm]
+    · left; exact ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp)
+    · right; exact ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp)
+  rw [this, ← eintegral_add_of_nonneg (by fun_prop) (by simp) (by simp),
+    ← eintegral_add_of_nonneg (by fun_prop) (by simp) (by simp),
+    ← eintegral_sub_of_nonneg _ _ (by fun_prop) (by fun_prop)]
+  · have h_le x : min (f⁺ x + g⁺ x) (f⁻ x + g⁻ x) ≤ min (f⁺ x) (g⁻ x) + min (f⁻ x) (g⁺ x) := by
+      rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f x with hf | hf
+        <;> rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero g x with hg | hg
+        <;> simp [hf, hg]
+    refine ne_of_lt ?_
+    refine lt_of_le_of_lt (eintegral_mono h_le) ?_
+    rw [eintegral_add_of_nonneg_ae (by fun_prop) (by fun_prop) (by simp) (by simp)]
+    rw [eintegral_eq_posPartFun_sub_negPartFun f, eintegral_eq_posPartFun_sub_negPartFun g]
+      at h_ne_bot_1 h_ne_bot_2
+    refine EReal.add_lt_top (ne_of_lt ?_) (ne_of_lt ?_)
+    · cases h_ne_bot_2 with
+      | inl h =>
+        refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_left _ _)) (Ne.lt_top ?_)
+        cases hf_int.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top with
+        | inl h' => exact h'
+        | inr h' =>
+          intro h_false
+          simp [h_false, EReal.top_sub h'] at h
+      | inr h =>
+        refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_right _ _)) (Ne.lt_top ?_)
+        intro h_false
+        simp [h_false] at h
+    · cases h_ne_bot_1 with
+      | inl h =>
+        refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_left _ _)) (Ne.lt_top ?_)
+        intro h_false
+        simp [h_false] at h
+      | inr h =>
+        refine lt_of_le_of_lt (eintegral_mono (fun _ ↦ min_le_right _ _)) (Ne.lt_top ?_)
+        cases hg_int.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top with
+        | inl h' => exact h'
+        | inr h' =>
+          intro h_false
+          simp [h_false, EReal.top_sub h'] at h
+  · exact fun _ ↦ add_nonneg (by simp) (by simp)
+  · exact fun _ ↦ add_nonneg (by simp) (by simp)
+
+/-- The integral of a sum is the sum of integrals (requires compatibility conditions to
+avoid `⊤ - ⊤`).
+
+See also `eintegral_add` for a version with balanced hypotheses for `f` and `g`. -/
+lemma eintegral_add' (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hg_ne_top : ∫ᵉ x, g x ∂μ ≠ ⊤) (hg_ne_bot : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x + g x ∂μ = ∫ᵉ x, f x ∂μ + ∫ᵉ x, g x ∂μ := by
+  have hg_int : EIntegrable g μ := by
+    by_contra h_false
+    simp [eintegral_of_not_eintegrable h_false] at hg_ne_bot
+  by_cases hf_int : EIntegrable f μ
+  · rw [eintegral_add hf hg hf_int hg_int (.inr hg_ne_top) (.inr hg_ne_bot)]
+  simp only [eintegral_of_not_eintegrable hf_int, EReal.bot_add]
+  have hf₂_int : ∫ᵉ x, f⁻ x ∂μ = ⊤ := by
+    have hf_int_eq_bot : ∫ᵉ x, f x ∂μ = ⊥ := by simp [hf_int]
+    simp only [eintegral_eq_posPartFun_sub_negPartFun f, sub_eq_add_neg, EReal.add_eq_bot_iff,
+      EReal.neg_eq_bot_iff] at hf_int_eq_bot
+    have : ∫ᵉ x, f⁺ x ∂μ ≠ ⊥ := ne_bot_of_le_ne_bot (by simp) <| eintegral_nonneg (by simp)
+    simpa [this] using hf_int_eq_bot
+  have hg₂_int : ∫ᵉ x, g⁻ x ∂μ ≠ ⊤ := by
+    intro h_false
+    simp [eintegral_eq_posPartFun_sub_negPartFun g, h_false] at hg_ne_bot
+  have hg₁_int : ∫ᵉ x, g⁺ x ∂μ ≠ ⊤ := by
+    intro h_false
+    rw [eintegral_eq_posPartFun_sub_negPartFun g, h_false, EReal.top_sub hg₂_int] at hg_ne_top
+    simp at hg_ne_top
+  have hf_add_g : ∀ x, f x + g x = (f⁺ x + g⁺ x) - (f⁻ x + g⁻ x) := by
+    intro x
+    rw [← EReal.posPart_fun_sub_negPart_fun_apply f x,
+      ← EReal.posPart_fun_sub_negPart_fun_apply g x, EReal.add_sub_add_comm]
+    · left; exact ne_bot_of_le_ne_bot (b := 0) (by simp) (by simp)
+    · right; exact ne_bot_of_le_ne_bot (b := 0) (by simp) (by simp)
+  simp_rw [hf_add_g]
+  rw [eintegral_sub_of_nonneg (fun _ ↦ add_nonneg (by simp) (by simp))
+    (fun _ ↦ add_nonneg (by simp) (by simp)) (by fun_prop) (by fun_prop)]
+  · suffices ∫ᵉ x, f⁻ x + g⁻ x ∂μ = ⊤ by simp [this]
+    rw [← top_le_iff]
+    calc ⊤
+    _ = ∫ᵉ x, f⁻ x ∂μ := by rw [hf₂_int]
+    _ ≤ ∫ᵉ x, f⁻ x + g⁻ x ∂μ := eintegral_mono (fun _ ↦ le_add_of_nonneg_right (by simp))
+  · have h_le x : min (f⁺ x + g⁺ x) (f⁻ x + g⁻ x) ≤ min (f⁺ x) (g⁻ x) + min (f⁻ x) (g⁺ x) := by
+      rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero f x with hf | hf <;>
+        rcases EReal.posPart_fun_eq_zero_or_negPart_fun_eq_zero g x with hg | hg <;>
+        simp [hf, hg]
+    refine (lt_of_le_of_lt (eintegral_mono h_le) ?_).ne
+    rw [eintegral_add_of_nonneg_ae (by fun_prop) (by fun_prop) (by simp) (by simp)]
+    refine EReal.add_lt_top (ne_of_lt ?_) (ne_of_lt ?_)
+    · calc ∫ᵉ x, min (f⁺ x) (g⁻ x) ∂μ
+      _ ≤ ∫ᵉ x, g⁻ x ∂μ := eintegral_mono (fun _ ↦ min_le_right _ _)
+      _ < ⊤ := hg₂_int.lt_top
+    · calc ∫ᵉ x, min (f⁻ x) (g⁺ x) ∂μ
+      _ ≤ ∫ᵉ x, g⁺ x ∂μ := eintegral_mono (fun _ ↦ min_le_right _ _)
+      _ < ⊤ := hg₁_int.lt_top
+
+/-- The integral of a difference is the difference of integrals (requires compatibility
+conditions to avoid `⊤ - ⊤`). -/
+lemma eintegral_sub (hf : EIntegrable f μ)
+    (hf_meas : AEMeasurable f μ) (hg : EIntegrable g μ) (hg_meas : AEMeasurable g μ)
+    (h_ne_top : ∫ᵉ x, f x ∂μ ≠ ⊤ ∨ ∫ᵉ x, g x ∂μ ≠ ⊤)
+    (h_ne_bot : ∫ᵉ x, f x ∂μ ≠ ⊥ ∨ ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  simp_rw [sub_eq_add_neg, ← Pi.neg_apply]
+  rw [eintegral_add hf_meas hg_meas.neg hf hg.neg]
+  · simp_rw [Pi.neg_apply]
+    rw [eintegral_neg hg]
+  · cases h_ne_bot with
+    | inl h => exact .inl h
+    | inr h => right; simp_rw [Pi.neg_apply]; rw [eintegral_neg hg]; simpa
+  · cases h_ne_top with
+    | inl h => exact .inl h
+    | inr h => right; simp_rw [Pi.neg_apply]; rw [eintegral_neg hg]; simpa
+
+lemma eintegral_sub' (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ)
+    (hg_ne_top : ∫ᵉ x, g x ∂μ ≠ ⊤) (hg_ne_bot : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  have hg_int : EIntegrable g μ := by
+    by_contra h_false
+    simp [eintegral_of_not_eintegrable h_false] at hg_ne_bot
+  simp_rw [sub_eq_add_neg, ← Pi.neg_apply]
+  rw [eintegral_add' hf_meas hg_meas.neg]
+  · simp_rw [Pi.neg_apply]
+    rw [eintegral_neg hg_int]
+  · simpa [eintegral_neg hg_int]
+  · simpa [eintegral_neg hg_int]
+
+lemma eintegral_sub'' (hf_meas : AEMeasurable f μ) (hg_meas : AEMeasurable g μ)
+    (hf_ne_top : ∫ᵉ x, f x ∂μ ≠ ⊤) (hf_ne_bot : ∫ᵉ x, f x ∂μ ≠ ⊥) (hg_int : EIntegrable g μ) :
+    ∫ᵉ x, f x - g x ∂μ = ∫ᵉ x, f x ∂μ - ∫ᵉ x, g x ∂μ := by
+  rw [eintegral_sub _ hf_meas hg_int hg_meas (by simp [hf_ne_top]) (by simp [hf_ne_bot])]
+  by_contra h_false
+  simp [eintegral_of_not_eintegrable h_false] at hf_ne_bot
+
+lemma eintegral_add_ne_bot (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hf_int : ∫ᵉ x, f x ∂μ ≠ ⊥) (hg_int : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    ∫ᵉ x, f x + g x ∂μ ≠ ⊥ := by
+  rw [eintegral_add (by fun_prop) (by fun_prop) (eintegrable_of_eintegral_ne_bot hf_int)
+    (eintegrable_of_eintegral_ne_bot hg_int)]
+  · simp [hf_int, hg_int]
+  · simp [hf_int]
+  · simp [hg_int]
+
+lemma eintegrable_add_of_ne_bot (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
+    (hf_int : ∫ᵉ x, f x ∂μ ≠ ⊥) (hg_int : ∫ᵉ x, g x ∂μ ≠ ⊥) :
+    EIntegrable (fun x ↦ f x + g x) μ :=
+  eintegrable_of_eintegral_ne_bot (eintegral_add_ne_bot hf hg hf_int hg_int)
+
+theorem eintegral_map {β : Type*} {mβ : MeasurableSpace β} {f : β → EReal} {g : α → β}
+    (hf : Measurable f) (hg : Measurable g) : ∫ᵉ a, f a ∂μ.map g = ∫ᵉ a, f (g a) ∂μ := by
+  simp only [eintegral]
+  repeat rw [lintegral_map (by fun_prop) hg]
+
+theorem eintegral_map' {β : Type*} {mβ : MeasurableSpace β} {f : β → EReal} {g : α → β}
+    (hf : AEMeasurable f (μ.map g)) (hg : AEMeasurable g μ) :
+    ∫ᵉ a, f a ∂μ.map g = ∫ᵉ a, f (g a) ∂μ := by
+  simp only [eintegral]
+  repeat rw [lintegral_map' (by fun_prop) hg]
+
+lemma eintegral_add_measure {ν : Measure α} (f : α → EReal) :
+    ∫ᵉ x, f x ∂(μ + ν) = ∫ᵉ x, f x ∂μ + ∫ᵉ x, f x ∂ν := by
+  simp only [eintegral, lintegral_add_measure, EReal.coe_ennreal_add]
+  rw [EReal.add_sub_add_comm (by simp) (by simp)]
+
+lemma eintegral_smul_measure {c : ℝ≥0∞} (hc : c ≠ ∞) (f : α → EReal) :
+    ∫ᵉ x, f x ∂(c • μ) = c * ∫ᵉ x, f x ∂μ := by
+  simp only [eintegral, lintegral_smul_measure, smul_eq_mul, EReal.coe_ennreal_mul]
+  rw [EReal.mul_sub_of_nonneg_of_ne_top _ (by simp [hc])]
+  norm_cast
+  exact zero_le
+
+@[simp]
+lemma eintegral_dirac {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
+    {x₀ : α} {f : α → EReal} :
+    ∫ᵉ x, f x ∂(Measure.dirac x₀) = f x₀ := by
+  simp only [eintegral, lintegral_dirac]
+  rcases le_total (f x₀) 0 with (h | h) <;> simp [h]
+
+end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Integral/EReal/Kernel.lean b/Mathlib/MeasureTheory/Integral/EReal/Kernel.lean
new file mode 100644
index 00000000000000..69d127c556e396
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/Kernel.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegral
+public import Mathlib.Probability.Kernel.Composition.MeasureComp
+
+/-!
+# TODO
+
+-/
+
+@[expose] public section
+
+open ProbabilityTheory
+
+open scoped ENNReal
+
+namespace MeasureTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ : Measure α} {f g : α → EReal}
+
+lemma eintegral_bind_of_nonneg {β : Type*} {mβ : MeasurableSpace β} {m : α → Measure β}
+    {f : β → EReal} (hf_nonneg : ∀ x, 0 ≤ f x)
+    (hμ : AEMeasurable m μ) (hf : AEMeasurable f (μ.bind m)) :
+    ∫ᵉ x, f x ∂μ.bind m = ∫ᵉ a, ∫ᵉ x, f x ∂m a ∂μ := by
+  rw [eintegral_of_nonneg hf_nonneg, μ.lintegral_bind hμ (by fun_prop), eintegral_of_nonneg]
+  swap; · exact fun _ ↦ eintegral_nonneg hf_nonneg
+  congr with x
+  rw [eintegral_of_nonneg hf_nonneg]
+  simp_rw [EReal.toENNReal_coe]
+
+theorem eintegral_comp_measure {β : Type*} {mβ : MeasurableSpace β} {κ : Kernel α β} {f : β → EReal}
+    (hf : Measurable f) (hf_int : EIntegrable f (κ ∘ₘ μ)) :
+    ∫ᵉ x, f x ∂(κ ∘ₘ μ) = ∫ᵉ a, ∫ᵉ x, f x ∂κ a ∂μ := by
+  rw [eintegral_eq_posPartFun_sub_negPartFun f, eintegral_bind_of_nonneg (by simp) κ.aemeasurable,
+    eintegral_bind_of_nonneg (by simp) κ.aemeasurable]
+  rotate_left
+  · fun_prop
+  · fun_prop
+  rw [← eintegral_sub_of_nonneg]
+  rotate_left
+  · exact fun _ ↦ eintegral_nonneg (by simp)
+  · exact fun _ ↦ eintegral_nonneg (by simp)
+  · simp_rw [eintegral_of_nonneg (posPart_fun_nonneg f)]
+    suffices AEMeasurable (fun a ↦ ∫⁻ x, (f⁺ x).toENNReal ∂κ a) μ by fun_prop
+    exact (Measurable.lintegral_kernel (by fun_prop)).aemeasurable
+  · simp_rw [eintegral_of_nonneg (negPart_fun_nonneg f)]
+    suffices AEMeasurable (fun a ↦ ∫⁻ x, (f⁻ x).toENNReal ∂κ a) μ by fun_prop
+    exact (Measurable.lintegral_kernel (by fun_prop)).aemeasurable
+  · refine ne_of_lt ?_
+    cases hf_int.eintegral_posPartFun_ne_top_or_eintegral_negPartFun_ne_top with
+    | inl h =>
+      calc ∫ᵉ x, min (∫ᵉ y, f⁺ y ∂κ x) (∫ᵉ y, f⁻ y ∂κ x) ∂μ
+      _ ≤ ∫ᵉ x, ∫ᵉ y, f⁺ y ∂κ x ∂μ := eintegral_mono (fun _ ↦ min_le_left _ _)
+      _ = ∫ᵉ p, f⁺ p ∂(κ ∘ₘ μ) := by
+        rw [eintegral_bind_of_nonneg (posPart_fun_nonneg f) κ.aemeasurable (by fun_prop)]
+      _ < ⊤ := h.lt_top
+    | inr h =>
+      calc ∫ᵉ x, min (∫ᵉ y, f⁺ y ∂κ x) (∫ᵉ y, f⁻ y ∂κ x) ∂μ
+      _ ≤ ∫ᵉ x, ∫ᵉ y, f⁻ y ∂κ x ∂μ := eintegral_mono (fun _ ↦ min_le_right _ _)
+      _ = ∫ᵉ p, f⁻ p ∂(κ ∘ₘ μ) := by
+        rw [eintegral_bind_of_nonneg (negPart_fun_nonneg f) κ.aemeasurable (by fun_prop)]
+      _ < ⊤ := h.lt_top
+  congr with x
+  rw [← eintegral_eq_posPartFun_sub_negPartFun]
+
+lemma eintegral_comp_measure_le {β : Type*} {mβ : MeasurableSpace β} {κ : Kernel α β}
+    {f : β → EReal} (hf : Measurable f) :
+    ∫ᵉ x, f x ∂(κ ∘ₘ μ) ≤ ∫ᵉ a, ∫ᵉ x, f x ∂κ a ∂μ := by
+  by_cases hf_int : EIntegrable f (κ ∘ₘ μ)
+  · rw [eintegral_comp_measure hf hf_int]
+  · simp [eintegral_of_not_eintegrable hf_int]
+
+end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Integral/EReal/Prod.lean b/Mathlib/MeasureTheory/Integral/EReal/Prod.lean
new file mode 100644
index 00000000000000..695c5fb24ddfc6
--- /dev/null
+++ b/Mathlib/MeasureTheory/Integral/EReal/Prod.lean
@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2025 Gaëtan Serré. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gaëtan Serré, Rémy Degenne
+-/
+module
+
+public import Mathlib.MeasureTheory.Integral.EReal.EIntegral
+public import Mathlib.MeasureTheory.Integral.Prod
+
+/-!
+# TODO
+
+## Main statements
+
+* `eintegral_prod`: Fubini's theorem for extended real-valued functions on product measures,
+  allowing interchange of integration order.
+
+-/
+
+@[expose] public section
+
+open ProbabilityTheory
+
+open scoped ENNReal
+
+
+
+namespace MeasureTheory
+
+variable {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
+  {μ : Measure α} {ν : Measure β} [SFinite ν]
+
+lemma eintegral_prod_of_nonneg
+    (f : α × β → EReal) (hf : AEMeasurable f (μ.prod ν)) (hf_nonneg : ∀ x, 0 ≤ f x) :
+    ∫ᵉ z, f z ∂(μ.prod ν) = ∫ᵉ x, ∫ᵉ y, f (x, y) ∂ν ∂μ := by
+  have hf_nonneg' x : ∀ y, 0 ≤ f (x, y) := fun y ↦ hf_nonneg (x, y)
+  rw [eintegral_of_nonneg hf_nonneg, eintegral_of_nonneg (fun x ↦ eintegral_nonneg (hf_nonneg' x))]
+  simp_rw [eintegral_of_nonneg (hf_nonneg' _)]
+  congr
+  rw [lintegral_prod _ (by fun_prop)]
+  congr with x
+  rw [EReal.toENNReal_coe]
+
+/-- Fubini's theorem for extended reals: the integral over the product equals the iterated
+integral. -/
+lemma eintegral_prod
+    (f : α × β → EReal) (hf : AEMeasurable f (μ.prod ν)) (hf_int : EIntegrable f (μ.prod ν)) :
+    ∫ᵉ z, f z ∂(μ.prod ν) = ∫ᵉ x, ∫ᵉ y, f (x, y) ∂ν ∂μ := by
+  set u : α × β → ℝ≥0∞ := fun z => (f z).toENNReal
+  set v : α × β → ℝ≥0∞ := fun z => (-f z).toENNReal
+  have hf_eq : f = fun z => (u z : EReal) - (v z : EReal) := by
+    simp only [u, v]
+    ext z
+    rcases le_total (f z) 0 with h | h <;> simp [h]
+  rw [hf_eq]
+  have hu_aemeasurable : AEMeasurable u (μ.prod ν) := by fun_prop
+  have hv_aemeasurable : AEMeasurable v (μ.prod ν) := by fun_prop
+  have h_u_v : (∫⁻ x, u x ∂(μ.prod ν) : EReal) - ∫⁻ x, v x ∂(μ.prod ν) =
+      ∫⁻ x, ∫⁻ y, u (x, y) ∂ν ∂μ - ∫⁻ x, ∫⁻ y, v (x, y) ∂ν ∂μ := by
+    rw [lintegral_prod _ (by fun_prop), lintegral_prod _ (by fun_prop)]
+  convert h_u_v using 1
+  · exact congrArg (eintegral (μ.prod ν)) hf_eq.symm
+  · convert eintegral_coe_ennreal_sub _ _ _ using 1
+    · congr! 2
+      rw [eintegral]
+      grind
+    · exact hu_aemeasurable.lintegral_prod_right'
+    · refine AEMeasurable.lintegral_prod_right ?_
+      convert hv_aemeasurable using 1
+      grind
+    · cases hf_int with
+      | inl h => left; convert h; rw [lintegral_prod _ (by fun_prop)]
+      | inr h => right; convert h; rw [lintegral_prod _ (by fun_prop)]
+
+lemma eintegral_prod_symm [SFinite μ]
+    (f : α × β → EReal) (hf : AEMeasurable f (μ.prod ν)) (hf_int : EIntegrable f (μ.prod ν)) :
+    ∫ᵉ z, f z ∂(μ.prod ν) = ∫ᵉ y, ∫ᵉ x, f (x, y) ∂μ ∂ν := by
+  calc ∫ᵉ z, f z ∂(μ.prod ν)
+  _ = ∫ᵉ z, (f ∘ Prod.swap) z ∂(ν.prod μ) := by
+    simp only [Function.comp_apply]
+    rw [← eintegral_map' _ measurable_swap.aemeasurable, Measure.prod_swap]
+    rwa [Measure.prod_swap]
+  _ = ∫ᵉ y, ∫ᵉ x, (f ∘ Prod.swap) (y, x) ∂μ ∂ν := by
+    rw [eintegral_prod]
+    · refine AEMeasurable.comp_aemeasurable ?_ (by fun_prop)
+      rwa [Measure.prod_swap]
+    · convert hf_int using 1
+      -- TODO: extract lemma EIntegrable.swap
+      unfold MeasureTheory.EIntegrable
+      simp only [Function.comp_apply, ne_eq]
+      rw [lintegral_prod_swap (ν := ν) (fun p ↦ (f p).toENNReal),
+        lintegral_prod_swap (ν := ν) (fun p ↦ (-f p).toENNReal)]
+  _ = ∫ᵉ y, ∫ᵉ x, f (x, y) ∂μ ∂ν := by simp
+
+end MeasureTheory
diff --git a/Mathlib/MeasureTheory/Order/Group/Lattice.lean b/Mathlib/MeasureTheory/Order/Group/Lattice.lean
index 0f9321d2d36a79..da1b836c75cae6 100644
--- a/Mathlib/MeasureTheory/Order/Group/Lattice.lean
+++ b/Mathlib/MeasureTheory/Order/Group/Lattice.lean
@@ -18,42 +18,63 @@ measurable function, group, lattice operation
 
 public section
 
-variable {α β : Type*} [Lattice α] [Group α] [MeasurableSpace α]
-  [MeasurableSpace β] {f : β → α}
+variable {α β : Type*} [Lattice α] [MeasurableSpace α] [MeasurableSpace β] {f : β → α}
+
+section DivInvMonoid
+
+variable [DivInvMonoid α] [MeasurableSup α]
 
 @[to_additive]
-theorem measurable_oneLePart [MeasurableSup α] : Measurable (oneLePart : α → α) :=
+theorem measurable_oneLePart : Measurable (oneLePart : α → α) :=
   measurable_sup_const _
 
 @[to_additive (attr := fun_prop)]
-protected theorem Measurable.oneLePart [MeasurableSup α] (hf : Measurable f) :
-    Measurable fun x ↦ oneLePart (f x) :=
+protected theorem Measurable.oneLePart (hf : Measurable f) :
+    Measurable fun x ↦ (f x)⁺ᵐ :=
   measurable_oneLePart.comp hf
 
 @[to_additive (attr := fun_prop)]
-protected theorem AEMeasurable.oneLePart {μ : MeasureTheory.Measure β} [MeasurableSup α]
-    (hf : AEMeasurable f μ) :
-    AEMeasurable (fun x ↦ oneLePart (f x)) μ :=
+protected theorem Measurable.oneLePart' (hf : Measurable f) :
+    Measurable f⁺ᵐ := hf.oneLePart
+
+@[to_additive (attr := fun_prop)]
+protected theorem AEMeasurable.oneLePart {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
+    AEMeasurable (fun x ↦ (f x)⁺ᵐ) μ :=
   hf.sup_const 1
 
+@[to_additive (attr := fun_prop)]
+protected theorem AEMeasurable.oneLePart' {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
+    AEMeasurable f⁺ᵐ μ := hf.oneLePart
+
 variable [MeasurableInv α]
 
 @[to_additive]
-theorem measurable_leOnePart [MeasurableSup α] : Measurable (leOnePart : α → α) :=
+theorem measurable_leOnePart : Measurable (leOnePart : α → α) :=
   (measurable_sup_const _).comp measurable_inv
 
 @[to_additive (attr := fun_prop)]
-protected theorem Measurable.leOnePart [MeasurableSup α] (hf : Measurable f) :
-    Measurable fun x ↦ leOnePart (f x) :=
+protected theorem Measurable.leOnePart (hf : Measurable f) :
+    Measurable fun x ↦ (f x)⁻ᵐ :=
   measurable_leOnePart.comp hf
 
 @[to_additive (attr := fun_prop)]
-protected theorem AEMeasurable.leOnePart {μ : MeasureTheory.Measure β} [MeasurableSup α]
-    (hf : AEMeasurable f μ) :
-    AEMeasurable (fun x ↦ leOnePart (f x)) μ :=
+protected theorem Measurable.leOnePart' (hf : Measurable f) :
+    Measurable f⁻ᵐ := hf.leOnePart
+
+@[to_additive (attr := fun_prop)]
+protected theorem AEMeasurable.leOnePart {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
+    AEMeasurable (fun x ↦ (f x)⁻ᵐ) μ :=
   hf.inv.sup_const 1
 
-variable [MeasurableSup₂ α]
+@[to_additive (attr := fun_prop)]
+protected theorem AEMeasurable.leOnePart' {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
+    AEMeasurable f⁻ᵐ μ := hf.leOnePart
+
+end DivInvMonoid
+
+section Group
+
+variable [Group α] [MeasurableInv α] [MeasurableSup₂ α]
 
 @[to_additive]
 theorem measurable_mabs : Measurable (mabs : α → α) :=
@@ -67,3 +88,5 @@ protected theorem Measurable.mabs (hf : Measurable f) : Measurable fun x ↦ mab
 protected theorem AEMeasurable.mabs {μ : MeasureTheory.Measure β} (hf : AEMeasurable f μ) :
     AEMeasurable (fun x ↦ mabs (f x)) μ :=
   measurable_mabs.comp_aemeasurable hf
+
+end Group