diff -r aea11797247b -r 9c295f84d55f src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Feb 19 21:21:19 2023 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Feb 20 15:19:53 2023 +0000
@@ -696,7 +696,7 @@
 
 lemma nn_integral_has_integral_lebesgue:
   fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes nonneg: "\<And>x. 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
+  assumes nonneg: "\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
   shows "integral\<^sup>N lborel (\<lambda>x. indicator \<Omega> x * f x) = I"
 proof -
   from I have "(\<lambda>x. indicator \<Omega> x *\<^sub>R f x) \<in> lebesgue \<rightarrow>\<^sub>M borel"
@@ -713,8 +713,9 @@
     by (rule nn_integral_has_integral_lborel[rotated 2]) auto
   also have "integral\<^sup>N lborel (\<lambda>x. abs (f' x)) = integral\<^sup>N lborel (\<lambda>x. abs (indicator \<Omega> x * f x))"
     using eq by (intro nn_integral_cong_AE) auto
-  finally show ?thesis
-    using nonneg by auto
+  also have "(\<lambda>x. abs (indicator \<Omega> x * f x)) = (\<lambda>x. indicator \<Omega> x * f x)"
+    using nonneg by (auto simp: indicator_def fun_eq_iff)
+  finally show ?thesis .
 qed
 
 lemma has_integral_iff_nn_integral_lebesgue:
@@ -741,6 +742,38 @@
     using f by (auto simp: nn_integral_completion)
 qed
 
+lemma set_nn_integral_lborel_eq_integral:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes "set_borel_measurable borel A f"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x" "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) < \<infinity>"
+  shows "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) = integral A f"
+proof -
+  have eq: "(\<integral>\<^sup>+x\<in>A. f x \<partial>lborel) = (\<integral>\<^sup>+x. ennreal (indicator A x * f x) \<partial>lborel)"
+    by (intro nn_integral_cong) (auto simp: indicator_def)
+  also have "\<dots> = integral UNIV (\<lambda>x. indicator A x * f x)"
+    using assms eq by (intro nn_integral_lborel_eq_integral)
+                      (auto simp: indicator_def set_borel_measurable_def)
+  also have "integral UNIV (\<lambda>x. indicator A x * f x) = integral A (\<lambda>x. indicator A x * f x)"
+    by (rule integral_spike_set) (auto intro: empty_imp_negligible)
+ 
+  also have "\<dots> = integral A f"
+    by (rule integral_cong) (auto simp: indicator_def)
+  finally show ?thesis .
+qed
+
+lemma nn_integral_has_integral_lebesgue':
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes nonneg: "\<And>x. x \<in> \<Omega> \<Longrightarrow> 0 \<le> f x" and I: "(f has_integral I) \<Omega>"
+  shows "integral\<^sup>N lborel (\<lambda>x. ennreal (f x) * indicator \<Omega> x) = ennreal I"
+proof -
+  have "integral\<^sup>N lborel (\<lambda>x. ennreal (f x) * indicator \<Omega> x) =
+        integral\<^sup>N lborel (\<lambda>x. ennreal (indicator \<Omega> x * f x))"
+    by (intro nn_integral_cong) (auto simp: indicator_def)
+  also have "\<dots> = ennreal I"
+    using assms by (intro nn_integral_has_integral_lebesgue)
+  finally show ?thesis .
+qed
+
 context
   fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
 begin
@@ -959,7 +992,7 @@
     show "(\<lambda>x. indicator S x *\<^sub>R f x) \<in> borel_measurable lebesgue"
       using f has_integral_implies_lebesgue_measurable[of f _ S] by (auto simp: integrable_on_def)
     show "(\<integral>\<^sup>+ x. ennreal (norm (indicator S x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
-      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ S]
+      using nf nn_integral_has_integral_lebesgue[of _ "\<lambda>x. norm (f x)"]
       by (auto simp: integrable_on_def nn_integral_completion)
   qed
 qed