src/HOL/Analysis/Set_Integral.thy

 
 (*
     Notation
 *)
 
-abbreviation "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
-
-abbreviation "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
-
-abbreviation "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
+definition "set_borel_measurable M A f \<equiv> (\<lambda>x. indicator A x *\<^sub>R f x) \<in> borel_measurable M"
+
+definition "set_integrable M A f \<equiv> integrable M (\<lambda>x. indicator A x *\<^sub>R f x)"
+
+definition "set_lebesgue_integral M A f \<equiv> lebesgue_integral M (\<lambda>x. indicator A x *\<^sub>R f x)"
 
 syntax
-"_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
-("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
+  "_ascii_set_lebesgue_integral" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a measure \<Rightarrow> real \<Rightarrow> real"
+  ("(4LINT (_):(_)/|(_)./ _)" [0,60,110,61] 60)
 
 translations
-"LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+  "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
 
 (*
     Notation for integration wrt lebesgue measure on the reals:
 
       LBINT x. f

 
     TODO: keep all these? Need unicode.
 *)
 
 syntax
-"_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
-("(2LBINT _./ _)" [0,60] 60)
+  "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
+  ("(2LBINT _./ _)" [0,60] 60)
 
 syntax
-"_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
-("(3LBINT _:_./ _)" [0,60,61] 60)
+  "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
+  ("(3LBINT _:_./ _)" [0,60,61] 60)
 
 (*
     Basic properties
 *)
 

   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   assumes "set_borel_measurable M X f" "B \<in> sets borel" "X \<in> sets M"
   shows "f -` B \<inter> X \<in> sets M"
 proof -
   have "f \<in> borel_measurable (restrict_space M X)"
-    using assms by (subst borel_measurable_restrict_space_iff) auto
+    using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto
   then have "f -` B \<inter> space (restrict_space M X) \<in> sets (restrict_space M X)"
     by (rule measurable_sets) fact
   with \<open>X \<in> sets M\<close> show ?thesis
     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
 qed
 
 lemma set_lebesgue_integral_cong:
   assumes "A \<in> sets M" and "\<forall>x. x \<in> A \<longrightarrow> f x = g x"
   shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)"
-  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
+  unfolding set_lebesgue_integral_def
+  using assms
+  by (metis indicator_simps(2) real_vector.scale_zero_left)
 
 lemma set_lebesgue_integral_cong_AE:
   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   assumes "AE x \<in> A in M. f x = g x"
   shows "LINT x:A|M. f x = LINT x:A|M. g x"
 proof-
   have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x"
     using assms by auto
-  thus ?thesis by (intro integral_cong_AE) auto
+  thus ?thesis
+  unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto
 qed
 
 lemma set_integrable_cong_AE:
     "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
     AE x \<in> A in M. f x = g x \<Longrightarrow> A \<in> sets M \<Longrightarrow>
     set_integrable M A f = set_integrable M A g"
+  unfolding set_integrable_def
   by (rule integrable_cong_AE) auto
 
 lemma set_integrable_subset:
   fixes M A B and f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_integrable M A f" "B \<in> sets M" "B \<subseteq> A"
   shows "set_integrable M B f"
 proof -
   have "set_integrable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
-    by (rule integrable_mult_indicator) fact+
+    using assms integrable_mult_indicator set_integrable_def by blast
   with \<open>B \<subseteq> A\<close> show ?thesis
+    unfolding set_integrable_def
     by (simp add: indicator_inter_arith[symmetric] Int_absorb2)
 qed
 
 lemma set_integrable_restrict_space:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f: "set_integrable M S f" and T: "T \<in> sets (restrict_space M S)"
   shows "set_integrable M T f"
 proof -
-  obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" using T by (auto simp: sets_restrict_space)
-
+  obtain T' where T_eq: "T = S \<inter> T'" and "T' \<in> sets M" 
+    using T by (auto simp: sets_restrict_space)
   have \<open>integrable M (\<lambda>x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\<close>
-    by (rule integrable_mult_indicator; fact)
+    using \<open>T' \<in> sets M\<close> f integrable_mult_indicator set_integrable_def by blast
   then show ?thesis
+    unfolding set_integrable_def
     unfolding T_eq indicator_inter_arith by (simp add: ac_simps)
 qed
 
 (* TODO: integral_cmul_indicator should be named set_integral_const *)
 (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *)
 
 lemma set_integral_scaleR_right [simp]: "LINT t:A|M. a *\<^sub>R f t = a *\<^sub>R (LINT t:A|M. f t)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong)
 
 lemma set_integral_mult_right [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. a * f t = a * (LINT t:A|M. f t)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_mult_right_zero[symmetric]) auto
 
 lemma set_integral_mult_left [simp]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "LINT t:A|M. f t * a = (LINT t:A|M. f t) * a"
+  unfolding set_lebesgue_integral_def
   by (subst integral_mult_left_zero[symmetric]) auto
 
 lemma set_integral_divide_zero [simp]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   shows "LINT t:A|M. f t / a = (LINT t:A|M. f t) / a"
+  unfolding set_lebesgue_integral_def
   by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
      (auto split: split_indicator)
 
 lemma set_integrable_scaleR_right [simp, intro]:
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a *\<^sub>R f t)"
+  unfolding set_integrable_def
   unfolding scaleR_left_commute by (rule integrable_scaleR_right)
 
 lemma set_integrable_scaleR_left [simp, intro]:
   fixes a :: "_ :: {banach, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t *\<^sub>R a)"
+  unfolding set_integrable_def
   using integrable_scaleR_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_mult_right [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. a * f t)"
+  unfolding set_integrable_def
   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_mult_left [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
+  unfolding set_integrable_def
   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
 lemma set_integrable_divide [simp, intro]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
   shows "set_integrable M A (\<lambda>t. f t / a)"
 proof -
   have "integrable M (\<lambda>x. indicator A x *\<^sub>R f x / a)"
-    using assms by (rule integrable_divide_zero)
+    using assms unfolding set_integrable_def by (rule integrable_divide_zero)
   also have "(\<lambda>x. indicator A x *\<^sub>R f x / a) = (\<lambda>x. indicator A x *\<^sub>R (f x / a))"
     by (auto split: split_indicator)
-  finally show ?thesis .
+  finally show ?thesis 
+    unfolding set_integrable_def .
 qed
 
 lemma set_integral_add [simp, intro]:
   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_integrable M A f" "set_integrable M A g"
   shows "set_integrable M A (\<lambda>x. f x + g x)"
     and "LINT x:A|M. f x + g x = (LINT x:A|M. f x) + (LINT x:A|M. g x)"
-  using assms by (simp_all add: scaleR_add_right)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right)
 
 lemma set_integral_diff [simp, intro]:
   assumes "set_integrable M A f" "set_integrable M A g"
   shows "set_integrable M A (\<lambda>x. f x - g x)" and "LINT x:A|M. f x - g x =
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
-  using assms by (simp_all add: scaleR_diff_right)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
 
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
+  unfolding set_integrable_def set_lebesgue_integral_def
   by (subst integral_minus[symmetric]) simp_all
 
 lemma set_integral_complex_of_real:
   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
+  unfolding set_lebesgue_integral_def
   by (subst integral_complex_of_real[symmetric])
      (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 lemma set_integral_mono:
   fixes f g :: "_ \<Rightarrow> real"
   assumes "set_integrable M A f" "set_integrable M A g"
     "\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x"
   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono split: split_indicator)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto intro: integral_mono split: split_indicator)
 
 lemma set_integral_mono_AE:
   fixes f g :: "_ \<Rightarrow> real"
   assumes "set_integrable M A f" "set_integrable M A g"
     "AE x \<in> A in M. f x \<le> g x"
   shows "(LINT x:A|M. f x) \<le> (LINT x:A|M. g x)"
-using assms by (auto intro: integral_mono_AE split: split_indicator)
+  using assms unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto intro: integral_mono_AE split: split_indicator)
 
 lemma set_integrable_abs: "set_integrable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar> :: real)"
-  using integrable_abs[of M "\<lambda>x. f x * indicator A x"] by (simp add: abs_mult ac_simps)
+  using integrable_abs[of M "\<lambda>x. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps)
 
 lemma set_integrable_abs_iff:
   fixes f :: "_ \<Rightarrow> real"
   shows "set_borel_measurable M A f \<Longrightarrow> set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
+  unfolding set_integrable_def set_borel_measurable_def
   by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps)
 
 lemma set_integrable_abs_iff':
   fixes f :: "_ \<Rightarrow> real"
   shows "f \<in> borel_measurable M \<Longrightarrow> A \<in> sets M \<Longrightarrow>
     set_integrable M A (\<lambda>x. \<bar>f x\<bar>) = set_integrable M A f"
-by (intro set_integrable_abs_iff) auto
+  by (simp add: set_borel_measurable_def set_integrable_abs_iff)
 
 lemma set_integrable_discrete_difference:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes "countable X"
   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "set_integrable M A f \<longleftrightarrow> set_integrable M B f"
+  unfolding set_integrable_def
 proof (rule integrable_discrete_difference[where X=X])
   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
     using diff by (auto split: split_indicator)
 qed fact+
 

   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes "countable X"
   assumes diff: "(A - B) \<union> (B - A) \<subseteq> X"
   assumes "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0" "\<And>x. x \<in> X \<Longrightarrow> {x} \<in> sets M"
   shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_discrete_difference[where X=X])
   show "\<And>x. x \<in> space M \<Longrightarrow> x \<notin> X \<Longrightarrow> indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x"
     using diff by (auto split: split_indicator)
 qed fact+
 

     and [measurable]: "A \<in> sets M" "B \<in> sets M"
   shows "set_integrable M (A \<union> B) f"
 proof -
   have "set_integrable M (A - B) f"
     using f_A by (rule set_integrable_subset) auto
-  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
+  with f_B have "integrable M (\<lambda>x. indicator (A - B) x *\<^sub>R f x + indicator B x *\<^sub>R f x)"
+    unfolding set_integrable_def using integrable_add by blast
+  then show ?thesis
+    unfolding set_integrable_def
     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
 qed
+
+lemma set_integrable_empty [simp]: "set_integrable M {} f"
+  by (auto simp: set_integrable_def)
 
 lemma set_integrable_UN:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "finite I" "\<And>i. i\<in>I \<Longrightarrow> set_integrable M (A i) f"
     "\<And>i. i\<in>I \<Longrightarrow> A i \<in> sets M"
   shows "set_integrable M (\<Union>i\<in>I. A i) f"
-using assms by (induct I) (auto intro!: set_integrable_Un)
+  using assms
+  by (induct I) (auto simp: set_integrable_Un sets.finite_UN)
 
 lemma set_integral_Un:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "A \<inter> B = {}"
   and "set_integrable M A f"
   and "set_integrable M B f"
-  shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
-by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric]
-      scaleR_add_left assms)
+shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
+  using assms
+  unfolding set_integrable_def set_lebesgue_integral_def
+  by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left)
 
 lemma set_integral_cong_set:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
-  assumes [measurable]: "set_borel_measurable M A f" "set_borel_measurable M B f"
+  assumes "set_borel_measurable M A f" "set_borel_measurable M B f"
     and ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
   shows "LINT x:B|M. f x = LINT x:A|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_cong_AE)
   show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x"
     using ae by (auto simp: subset_eq split: split_indicator)
-qed fact+
+qed (use assms in \<open>auto simp: set_borel_measurable_def\<close>)
 
 lemma set_borel_measurable_subset:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes [measurable]: "set_borel_measurable M A f" "B \<in> sets M" and "B \<subseteq> A"
   shows "set_borel_measurable M B f"
 proof -
   have "set_borel_measurable M B (\<lambda>x. indicator A x *\<^sub>R f x)"
-    by measurable
-  also have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
+    using assms unfolding set_borel_measurable_def
+    using borel_measurable_indicator borel_measurable_scaleR by blast 
+  moreover have "(\<lambda>x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\<lambda>x. indicator B x *\<^sub>R f x)"
     using \<open>B \<subseteq> A\<close> by (auto simp: fun_eq_iff split: split_indicator)
-  finally show ?thesis .
+  ultimately show ?thesis 
+    unfolding set_borel_measurable_def by simp
 qed
 
 lemma set_integral_Un_AE:
   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes ae: "AE x in M. \<not> (x \<in> A \<and> x \<in> B)" and [measurable]: "A \<in> sets M" "B \<in> sets M"

   shows "LINT x:A\<union>B|M. f x = (LINT x:A|M. f x) + (LINT x:B|M. f x)"
 proof -
   have f: "set_integrable M (A \<union> B) f"
     by (intro set_integrable_Un assms)
   then have f': "set_borel_measurable M (A \<union> B) f"
-    by (rule borel_measurable_integrable)
+    using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast
   have "LINT x:A\<union>B|M. f x = LINT x:(A - A \<inter> B) \<union> (B - A \<inter> B)|M. f x"
   proof (rule set_integral_cong_set)
     show "AE x in M. (x \<in> A - A \<inter> B \<union> (B - A \<inter> B)) = (x \<in> A \<union> B)"
       using ae by auto
     show "set_borel_measurable M (A - A \<inter> B \<union> (B - A \<inter> B)) f"

   fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "finite I" "disjoint_family_on A I"
     and "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   shows "(LINT x:(\<Union>i\<in>I. A i)|M. f x) = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   using assms
-  apply induct
-  apply (auto intro!: set_integral_Un set_integrable_Un set_integrable_UN simp: disjoint_family_on_def)
-by (subst set_integral_Un, auto intro: set_integrable_UN)
+proof induction
+  case (insert x F)
+  then have "A x \<inter> UNION F A = {}"
+    by (meson disjoint_family_on_insert)
+  with insert show ?case
+    by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert)
+qed (simp add: set_lebesgue_integral_def)
 
 (* TODO: find a better name? *)
 lemma pos_integrable_to_top:
   fixes l::real
   assumes "\<And>i. A i \<in> sets M" "mono A"
   assumes nneg: "\<And>x i. x \<in> A i \<Longrightarrow> 0 \<le> f x"
   and intgbl: "\<And>i::nat. set_integrable M (A i) f"
   and lim: "(\<lambda>i::nat. LINT x:A i|M. f x) \<longlonglongrightarrow> l"
-  shows "set_integrable M (\<Union>i. A i) f"
+shows "set_integrable M (\<Union>i. A i) f"
+    unfolding set_integrable_def
   apply (rule integrable_monotone_convergence[where f = "\<lambda>i::nat. \<lambda>x. indicator (A i) x *\<^sub>R f x" and x = l])
-  apply (rule intgbl)
-  prefer 3 apply (rule lim)
+  apply (rule intgbl [unfolded set_integrable_def])
+  prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def])
   apply (rule AE_I2)
   using \<open>mono A\<close> apply (auto simp: mono_def nneg split: split_indicator) []
 proof (rule AE_I2)
   { fix x assume "x \<in> space M"
     show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"

         done
     qed auto }
   then show "(\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R f x) \<in> borel_measurable M"
     apply (rule borel_measurable_LIMSEQ_real)
     apply assumption
-    apply (intro borel_measurable_integrable intgbl)
-    done
+    using intgbl set_integrable_def by blast
 qed
 
 (* Proof from Royden Real Analysis, p. 91. *)
 lemma lebesgue_integral_countable_add:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes meas[intro]: "\<And>i::nat. A i \<in> sets M"
     and disj: "\<And>i j. i \<noteq> j \<Longrightarrow> A i \<inter> A j = {}"
     and intgbl: "set_integrable M (\<Union>i. A i) f"
   shows "LINT x:(\<Union>i. A i)|M. f x = (\<Sum>i. (LINT x:(A i)|M. f x))"
+    unfolding set_lebesgue_integral_def
 proof (subst integral_suminf[symmetric])
-  show int_A: "\<And>i. set_integrable M (A i) f"
-    using intgbl by (rule set_integrable_subset) auto
+  show int_A: "integrable M (\<lambda>x. indicat_real (A i) x *\<^sub>R f x)" for i
+    using intgbl unfolding set_integrable_def [symmetric]
+    by (rule set_integrable_subset) auto
   { fix x assume "x \<in> space M"
     have "(\<lambda>i. indicator (A i) x *\<^sub>R f x) sums (indicator (\<Union>i. A i) x *\<^sub>R f x)"
       by (intro sums_scaleR_left indicator_sums) fact }
   note sums = this
 
   have norm_f: "\<And>i. set_integrable M (A i) (\<lambda>x. norm (f x))"
-    using int_A[THEN integrable_norm] by auto
+    using int_A[THEN integrable_norm] unfolding set_integrable_def by auto
 
   show "AE x in M. summable (\<lambda>i. norm (indicator (A i) x *\<^sub>R f x))"
     using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums])
 
   show "summable (\<lambda>i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))"
   proof (rule summableI_nonneg_bounded)
     fix n
     show "0 \<le> LINT x|M. norm (indicator (A n) x *\<^sub>R f x)"
       using norm_f by (auto intro!: integral_nonneg_AE)
 
-    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) =
-      (\<Sum>i<n. set_lebesgue_integral M (A i) (\<lambda>x. norm (f x)))"
-      by (simp add: abs_mult)
+    have "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) = (\<Sum>i<n. LINT x:A i|M. norm (f x))"
+      by (simp add: abs_mult set_lebesgue_integral_def)
     also have "\<dots> = set_lebesgue_integral M (\<Union>i<n. A i) (\<lambda>x. norm (f x))"
       using norm_f
       by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj)
     also have "\<dots> \<le> set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
-      using intgbl[THEN integrable_norm]
-      by (intro integral_mono set_integrable_UN[of "{..<n}"] norm_f)
-         (auto split: split_indicator)
+      using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f
+      unfolding set_lebesgue_integral_def set_integrable_def
+      apply (intro integral_mono set_integrable_UN[of "{..<n}", unfolded set_integrable_def])
+          apply (auto split: split_indicator)
+      done
     finally show "(\<Sum>i<n. LINT x|M. norm (indicator (A i) x *\<^sub>R f x)) \<le>
       set_lebesgue_integral M (\<Union>i. A i) (\<lambda>x. norm (f x))"
       by simp
   qed
-  show "set_lebesgue_integral M (UNION UNIV A) f = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
+  show "LINT x|M. indicator (UNION UNIV A) x *\<^sub>R f x = LINT x|M. (\<Sum>i. indicator (A i) x *\<^sub>R f x)"
     apply (rule Bochner_Integration.integral_cong[OF refl])
     apply (subst suminf_scaleR_left[OF sums_summable[OF indicator_sums, OF disj], symmetric])
     using sums_unique[OF indicator_sums[OF disj]]
     apply auto
     done

 
 lemma set_integral_cont_up:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "incseq A"
   and intgbl: "set_integrable M (\<Union>i. A i) f"
-  shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+shows "(\<lambda>i. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Union>i. A i)|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (intro integral_dominated_convergence[where w="\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x)"])
   have int_A: "\<And>i. set_integrable M (A i) f"
     using intgbl by (rule set_integrable_subset) auto
-  then show "\<And>i. set_borel_measurable M (A i) f" "set_borel_measurable M (\<Union>i. A i) f"
-    "set_integrable M (\<Union>i. A i) (\<lambda>x. norm (f x))"
-    using intgbl integrable_norm[OF intgbl] by auto
-
+  show "\<And>i. (\<lambda>x. indicator (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+    using int_A integrable_iff_bounded set_integrable_def by blast
+  show "(\<lambda>x. indicator (UNION UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+    using integrable_iff_bounded intgbl set_integrable_def by blast
+  show "integrable M (\<lambda>x. indicator (\<Union>i. A i) x *\<^sub>R norm (f x))"
+    using int_A intgbl integrable_norm unfolding set_integrable_def 
+    by fastforce
   { fix x i assume "x \<in> A i"
     with A have "(\<lambda>xa. indicator (A xa) x::real) \<longlonglongrightarrow> 1 \<longleftrightarrow> (\<lambda>xa. 1::real) \<longlonglongrightarrow> 1"
       by (intro filterlim_cong refl)
          (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) }
   then show "AE x in M. (\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"

 lemma set_integral_cont_down:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes [measurable]: "\<And>i. A i \<in> sets M" and A: "decseq A"
   and int0: "set_integrable M (A 0) f"
   shows "(\<lambda>i::nat. LINT x:(A i)|M. f x) \<longlonglongrightarrow> LINT x:(\<Inter>i. A i)|M. f x"
+  unfolding set_lebesgue_integral_def
 proof (rule integral_dominated_convergence)
   have int_A: "\<And>i. set_integrable M (A i) f"
     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
-  show "set_integrable M (A 0) (\<lambda>x. norm (f x))"
-    using int0[THEN integrable_norm] by simp
+  have "integrable M (\<lambda>c. norm (indicat_real (A 0) c *\<^sub>R f c))"
+    by (metis (no_types) int0 integrable_norm set_integrable_def)
+  then show "integrable M (\<lambda>x. indicator (A 0) x *\<^sub>R norm (f x))"
+    by force
   have "set_integrable M (\<Inter>i. A i) f"
     using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def)
-  with int_A show "set_borel_measurable M (\<Inter>i. A i) f" "\<And>i. set_borel_measurable M (A i) f"
-    by auto
+  with int_A show "(\<lambda>x. indicat_real (INTER UNIV A) x *\<^sub>R f x) \<in> borel_measurable M"
+                  "\<And>i. (\<lambda>x. indicat_real (A i) x *\<^sub>R f x) \<in> borel_measurable M"
+    by (auto simp: set_integrable_def)
   show "\<And>i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \<le> indicator (A 0) x *\<^sub>R norm (f x)"
     using A by (auto split: split_indicator simp: decseq_def)
   { fix x i assume "x \<in> space M" "x \<notin> A i"
     with A have "(\<lambda>i. indicator (A i) x::real) \<longlonglongrightarrow> 0 \<longleftrightarrow> (\<lambda>i. 0::real) \<longlonglongrightarrow> 0"
       by (intro filterlim_cong refl)

   and [simp]: "{a} \<in> sets M" and "(emeasure M) {a} \<noteq> \<infinity>"
   shows "(LINT x:{a} | M. f x) = f a * measure M {a}"
 proof-
   have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)"
     by (intro set_lebesgue_integral_cong) simp_all
-  then show ?thesis using assms by simp
+  then show ?thesis using assms
+    unfolding set_lebesgue_integral_def by simp
 qed
 
 
 abbreviation complex_integrable :: "'a measure \<Rightarrow> ('a \<Rightarrow> complex) \<Rightarrow> bool" where
   "complex_integrable M f \<equiv> integrable M f"

 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
 lemma set_measurable_continuous_on_ivl:
   assumes "continuous_on {a..b} (f :: real \<Rightarrow> real)"
   shows "set_borel_measurable borel {a..b} f"
+  unfolding set_borel_measurable_def
   by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp
 
 
 text\<open>This notation is from Sébastien Gouëzel: His use is not directly in line with the
 notations in this file, they are more in line with sum, and more readable he thinks.\<close>

 qed
 
 lemma set_integral_null_delta:
   fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
-    and "(A - B) \<union> (B - A) \<in> null_sets M"
+    and null: "(A - B) \<union> (B - A) \<in> null_sets M"
   shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
-proof (rule set_integral_cong_set, auto)
+proof (rule set_integral_cong_set)
   have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
-    using assms(4) AE_not_in by blast
+    using null AE_not_in by blast
   then show "AE x in M. (x \<in> B) = (x \<in> A)"
     by auto
-qed
+qed (simp_all add: set_borel_measurable_def)
 
 lemma set_integral_space:
   assumes "integrable M f"
   shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
-by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
+  by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def)
 
 lemma null_if_pos_func_has_zero_nn_int:
   fixes f::"'a \<Rightarrow> ennreal"
   assumes [measurable]: "f \<in> borel_measurable M" "A \<in> sets M"
     and "AE x\<in>A in M. f x > 0" "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = 0"

       and "AE x\<in>A in M. f x > 0" "(\<integral>x\<in>A. f x \<partial>M) = (0::real)"
   shows "A \<in> null_sets M"
 proof -
   have "AE x in M. indicator A x * f x = 0"
     apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
-    using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
+    using assms integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)]
+    by (auto simp: set_lebesgue_integral_def)
   then have "AE x\<in>A in M. f x = 0" by auto
   then have "AE x\<in>A in M. False" using assms(3) by auto
   then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
 qed
 

 using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
 only formulate it for real-valued functions.\<close>
 
 lemma density_unique_real:
   fixes f f'::"_ \<Rightarrow> real"
-  assumes [measurable]: "integrable M f" "integrable M f'"
+  assumes M[measurable]: "integrable M f" "integrable M f'"
   assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
   shows "AE x in M. f x = f' x"
 proof -
   define A where "A = {x \<in> space M. f x < f' x}"
   then have [measurable]: "A \<in> sets M" by simp
   have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
-    using \<open>A \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+    using \<open>A \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
   then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
   then have "A \<in> null_sets M"
     using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
   then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
   then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
 
-
   define B where "B = {x \<in> space M. f' x < f x}"
   then have [measurable]: "B \<in> sets M" by simp
   have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
-    using \<open>B \<in> sets M\<close> assms(1) assms(2) integrable_mult_indicator by blast
+    using \<open>B \<in> sets M\<close> M integrable_mult_indicator set_integrable_def by blast
   then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
   then have "B \<in> null_sets M"
     using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
   then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
   then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
-
   then show ?thesis using * by auto
 qed
 
 text \<open>The next lemma shows that $L^1$ convergence of a sequence of functions follows from almost
 everywhere convergence and the weaker condition of the convergence of the integrated norms (or even