From 9cf8354382b38c0e24de68b4a6ea251b8b5bce41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Mon, 30 Oct 2023 09:53:14 +0100
Subject: [PATCH 1/3] 1st commit

---
 .../Measure/Lebesgue/Integral.lean            | 24 +++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
index 1779f92122ed7..ce0b7176c5e0f 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
@@ -104,3 +104,27 @@ theorem integral_comp_neg_Ioi {E : Type*} [NormedAddCommGroup E] [NormedSpace 
   rw [← neg_neg c, ← integral_comp_neg_Iic]
   simp only [neg_neg]
 #align integral_comp_neg_Ioi integral_comp_neg_Ioi
+
+theorem integral_comp_abs {f : ℝ → ℝ} (hf : IntegrableOn (fun x => f x) (Ioi 0)) :
+    ∫ x, f |x| = 2 * ∫ x in Ioi (0:ℝ), f x := by
+  have int_Ioi : IntegrableOn (fun x => f |x|) (Ioi 0) := by
+      refine IntegrableOn.congr_fun hf (fun _ hx => ?_) measurableSet_Ioi
+      rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
+  have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
+    rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
+    let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
+    rw [m.integrableOn_map_iff]
+    simp_rw [Function.comp, abs_neg, neg_preimage, preimage_neg_Iic, neg_zero]
+    exact integrableOn_Ici_iff_integrableOn_Ioi.mpr int_Ioi
+  calc
+    _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
+      rw [← integral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic int_Ioi,
+        Iic_union_Ioi, restrict_univ]
+    _ = 2 * ∫ x in Ioi 0, f x := by
+      rw [two_mul]
+      congr! 1
+      · rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
+        refine set_integral_congr measurableSet_Iic (fun _ hx => ?_)
+        rw [abs_eq_neg_self.mpr (by exact hx)]
+      · refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_)
+        rw [abs_eq_self.mpr (le_of_lt (by exact hx))]

From 8d9285d64ad8251c28155841ffe8981df2525bdd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Mon, 30 Oct 2023 10:50:19 +0100
Subject: [PATCH 2/3] Remove hypothesis

---
 .../Measure/Lebesgue/Integral.lean            | 43 ++++++++++---------
 1 file changed, 23 insertions(+), 20 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
index ce0b7176c5e0f..51f8de42fdcaa 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
@@ -105,26 +105,29 @@ theorem integral_comp_neg_Ioi {E : Type*} [NormedAddCommGroup E] [NormedSpace 
   simp only [neg_neg]
 #align integral_comp_neg_Ioi integral_comp_neg_Ioi
 
-theorem integral_comp_abs {f : ℝ → ℝ} (hf : IntegrableOn (fun x => f x) (Ioi 0)) :
+theorem integral_comp_abs {f : ℝ → ℝ} :
     ∫ x, f |x| = 2 * ∫ x in Ioi (0:ℝ), f x := by
-  have int_Ioi : IntegrableOn (fun x => f |x|) (Ioi 0) := by
-      refine IntegrableOn.congr_fun hf (fun _ hx => ?_) measurableSet_Ioi
-      rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
-  have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
-    rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
-    let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
-    rw [m.integrableOn_map_iff]
-    simp_rw [Function.comp, abs_neg, neg_preimage, preimage_neg_Iic, neg_zero]
-    exact integrableOn_Ici_iff_integrableOn_Ioi.mpr int_Ioi
-  calc
-    _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
-      rw [← integral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic int_Ioi,
-        Iic_union_Ioi, restrict_univ]
-    _ = 2 * ∫ x in Ioi 0, f x := by
-      rw [two_mul]
-      congr! 1
-      · rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
+  have eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x := by
+    refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_)
+    rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
+  obtain hf | hf := em (IntegrableOn (fun x => f |x|) (Ioi 0))
+  · have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
+      rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
+      let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding
+      rw [m.integrableOn_map_iff]
+      simp_rw [Function.comp, abs_neg, neg_preimage, preimage_neg_Iic, neg_zero]
+      exact integrableOn_Ici_iff_integrableOn_Ioi.mpr hf
+    calc
+      _ = (∫ x in Iic 0, f |x|) + ∫ x in Ioi 0, f |x| := by
+        rw [← integral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi int_Iic hf,
+          Iic_union_Ioi, restrict_univ]
+      _ = 2 * ∫ x in Ioi 0, f x := by
+        rw [two_mul, eq]
+        congr! 1
+        rw [← neg_zero, ← integral_comp_neg_Iic, neg_zero]
         refine set_integral_congr measurableSet_Iic (fun _ hx => ?_)
         rw [abs_eq_neg_self.mpr (by exact hx)]
-      · refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_)
-        rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
+  · have : ¬ Integrable (fun x => f |x|) := by
+      contrapose! hf
+      exact hf.integrableOn
+    rw [← eq, integral_undef hf, integral_undef this, mul_zero]

From 7c207f9b6f45ec25cecc760fec78300855380876 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Xavier-Fran=C3=A7ois=20Roblot?=
 <46200072+xroblot@users.noreply.github.com>
Date: Mon, 30 Oct 2023 16:51:37 +0100
Subject: [PATCH 3/3] review

---
 Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
index 51f8de42fdcaa..5a4ccf2b9cf7f 100644
--- a/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
+++ b/Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
@@ -110,7 +110,7 @@ theorem integral_comp_abs {f : ℝ → ℝ} :
   have eq : ∫ (x : ℝ) in Ioi 0, f |x| = ∫ (x : ℝ) in Ioi 0, f x := by
     refine set_integral_congr measurableSet_Ioi (fun _ hx => ?_)
     rw [abs_eq_self.mpr (le_of_lt (by exact hx))]
-  obtain hf | hf := em (IntegrableOn (fun x => f |x|) (Ioi 0))
+  by_cases hf : IntegrableOn (fun x => f |x|) (Ioi 0)
   · have int_Iic : IntegrableOn (fun x ↦ f |x|) (Iic 0) := by
       rw [← Measure.map_neg_eq_self (volume : Measure ℝ)]
       let m : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).measurableEmbedding