# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523631507 -3600
# Node ID 557ea2740125b35d5fbcf6cc4ad7419134b789f1
# Parent  75b94eb58c3d85d353d190ccc1e0baab7a91faa0
Probability builds with new definitions

diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -67,6 +67,9 @@
     by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space)
 qed
 
+lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\<lambda>x. 0) = 0"
+  by (auto simp: set_lebesgue_integral_def)
+
 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)"
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -274,7 +274,8 @@
   have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
       \<bar>LBINT s=a..b. f s\<bar> \<le> \<bar>LBINT s=a..b. g s\<bar>"
     if f: "\<And>s. 0 \<le> f s" and g: "\<And>s. f s \<le> g s" for f g :: "_ \<Rightarrow> real"
-    using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
+    using order_trans[OF f g] f g 
+    unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def set_integrable_def
     by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
 
   have "iexp x - (\<Sum>k \<le> Suc n. (\<i> * x)^k / fact k) =
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Conditional_Expectation.thy
--- a/src/HOL/Probability/Conditional_Expectation.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -739,7 +739,8 @@
 proof -
   have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
   have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
-  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
+  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric]
+    unfolding set_lebesgue_integral_def by auto
 qed
 
 lemma real_cond_exp_int [intro]:
@@ -760,14 +761,14 @@
     then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
     then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
     have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)"
-      by (simp add: integral_subalgebra2 subalg)
+      unfolding set_lebesgue_integral_def  by (simp add: integral_subalgebra2 subalg)
     also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp
-    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
     also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)"
       apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
-    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def)
     also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)"
-      by (simp add: integral_subalgebra2 subalg)
+      by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def)
     finally show "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)" by simp
   next
     have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
@@ -791,12 +792,12 @@
   then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
   have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
   have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
-    by (simp add: mult.commute mult.left_commute)
+    by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
   also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
     apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
   also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
-    by (simp add: mult.commute mult.left_commute)
+    by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
   finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
 qed (auto simp add: real_cond_exp_intg(1) assms)
 
@@ -817,17 +818,17 @@
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
 
   have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
-    apply (rule set_integral_add, auto simp add: assms)
+    apply (rule set_integral_add, auto simp add: assms set_integrable_def)
     using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
           integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
   also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)"
-    by auto
+    unfolding set_lebesgue_integral_def by auto
   also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
     using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
   also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
-    by auto
+    unfolding set_lebesgue_integral_def by auto
   also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
-    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
+    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg)
   finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
     by simp
 qed (auto simp add: assms)
@@ -911,7 +912,7 @@
 
 lemma real_cond_exp_gr_c:
   assumes [measurable]: "integrable M f"
-      and "AE x in M. f x > c"
+      and AE: "AE x in M. f x > c"
   shows "AE x in M. real_cond_exp M F f x > c"
 proof -
   define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}"
@@ -931,24 +932,33 @@
     then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
     then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
     have Ic: "set_integrable M A (\<lambda>x. c)"
+      unfolding set_integrable_def
       using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
     have If: "set_integrable M A f"
+      unfolding set_integrable_def
       by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
-    have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
-    proof (rule antisym)
-      show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
-        apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
-      have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
-        by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
-      also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
-        apply (rule set_integral_mono)
-        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
-        using Ic X_def \<open>A \<subseteq> X\<close> by auto
-      finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
-    qed
     have "AE x in M. indicator A x * c = indicator A x * f x"
-      apply (rule integral_ineq_eq_0_then_AE) using Ic If * apply auto
-      using assms(2) unfolding indicator_def by auto
+    proof (rule integral_ineq_eq_0_then_AE)
+      have "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
+      proof (rule antisym)
+        show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
+          apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
+        have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
+          by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
+        also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
+          apply (rule set_integral_mono)
+          unfolding set_integrable_def
+            apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
+          using Ic X_def \<open>A \<subseteq> X\<close> by (auto simp: set_integrable_def)
+        finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
+      qed
+      then have "measure M A * c = LINT x|M. indicat_real A x * f x"
+        by (auto simp: set_lebesgue_integral_def)
+      then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x"
+        by auto
+      show "AE x in M. indicat_real A x * c \<le> indicat_real A x * f x"
+      using AE unfolding indicator_def by auto
+    qed (use Ic If  in \<open>auto simp: set_integrable_def\<close>)
     then have "AE x\<in>A in M. c = f x" by auto
     then have "AE x\<in>A in M. False" using assms(2) by auto
     have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>)
@@ -1045,7 +1055,7 @@
     by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
 
   have "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A x * f i x)\<partial>M)"
-    by (simp add: sum_distrib_left)
+    by (simp add: sum_distrib_left set_lebesgue_integral_def)
   also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))"
     by (rule Bochner_Integration.integral_sum, simp add: *)
   also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))"
@@ -1053,7 +1063,7 @@
   also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)"
     by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
   also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)"
-    by (simp add: sum_distrib_left)
+    by (simp add: sum_distrib_left set_lebesgue_integral_def)
   finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto
 qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
 
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Distributions.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -955,12 +955,13 @@
         by (rule integral_by_parts')
            (auto intro!: derivative_eq_intros b
                  simp: diff_Suc of_nat_Suc field_simps split: nat.split)
-      also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
-        (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
-        by (intro Bochner_Integration.integral_cong) auto
+      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) - (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
+        by (auto simp: intro!: Bochner_Integration.integral_cong)
+      also have "... = exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
+        unfolding Bochner_Integration.integral_mult_right_zero [symmetric]
+        by (simp del: real_scaleR_def)
       finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
-        exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
-        by (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
+        exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)" .
       then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
         by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
     qed
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Levy.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -90,12 +90,12 @@
     { fix x
       have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real
         using Levy_Inversion_aux2[of "x - b" "x - a"]
-        apply (simp add: interval_lebesgue_integrable_def del: times_divide_eq_left)
+        apply (simp add: interval_lebesgue_integrable_def set_integrable_def del: times_divide_eq_left)
         apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI)
         apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms)
         done
       have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)"
-        using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def)
+        using \<open>T \<ge> 0\<close> by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def)
       also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)"
           (is "_ = _ + ?t")
         using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>)
@@ -130,7 +130,7 @@
     } note main_eq = this
     have "(CLBINT t=-T..T. ?F t * \<phi> t) =
       (CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))"
-      using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def
+      using \<open>T \<ge> 0\<close> unfolding \<phi>_def char_def interval_lebesgue_integral_def set_lebesgue_integral_def
       by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
       by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
@@ -323,6 +323,7 @@
       by (rule Mn.integrable_const_bound [where B = 1], auto)
     have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))"
       using \<open>0 < u\<close>
+      unfolding set_integrable_def
       by (intro integrableI_bounded_set_indicator [where B="2"])
          (auto simp: lborel.emeasure_pair_measure_Times ennreal_mult_less_top not_less top_unique
                split: split_indicator
@@ -331,9 +332,10 @@
         (CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))"
       unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult)
     also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))"
+      unfolding set_lebesgue_integral_def
       by (rule Bochner_Integration.integral_cong) (auto split: split_indicator)
     also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))"
-      using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta')
+      using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta' set_integrable_def set_lebesgue_integral_def)
     also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
       using \<open>u > 0\<close> by (intro Bochner_Integration.integral_cong, auto simp add: * simp del: of_real_mult)
     also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u  - sin (u * x) / x)))"
@@ -343,9 +345,12 @@
     also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} | M n. u)"
     proof -
       have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))"
-        using Mn3 by (intro P.integrable_fst) (simp add: indicator_times split_beta')
+        using Mn3 unfolding set_integrable_def set_lebesgue_integral_def
+        by (intro P.integrable_fst) (simp add: indicator_times split_beta')
       hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
-        using \<open>u > 0\<close> by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
+        using \<open>u > 0\<close>
+        unfolding set_integrable_def
+        by (subst integrable_cong) (auto simp add: * simp del: of_real_mult)
       hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u  - sin (u * x) / x))"
         unfolding complex_of_real_integrable_eq .
       have "2 * sin x \<le> x" if "2 \<le> x" for x :: real
@@ -355,13 +360,13 @@
       moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real
         using sin_x_le_x[of "-x"] by simp
       ultimately show ?thesis
-        using \<open>u > 0\<close>
+        using \<open>u > 0\<close> unfolding set_lebesgue_integral_def
         by (intro integral_mono [OF _ **])
            (auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos top_unique less_top[symmetric]
                  split: split_indicator)
     qed
-    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) =
-        u * measure (M n) {x. abs x \<ge> 2 / u}"
+    also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) = u * measure (M n) {x. abs x \<ge> 2 / u}"
+      unfolding set_lebesgue_integral_def
       by (simp add: Mn.emeasure_eq_measure)
     finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" .
   qed
@@ -380,13 +385,16 @@
     have 1: "\<And>x. cmod (1 - char M' x) \<le> 2"
       by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1)
     then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)"
+      unfolding set_integrable_def
       by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq)
-    have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))"
+    have 3: "\<And>u v. integrable lborel (\<lambda>x. indicat_real {u..v} x *\<^sub>R cmod (1 - char M' x))"
       by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
                 continuous_intros ballI M'.isCont_char continuous_intros)
     have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
+      unfolding set_lebesgue_integral_def
       using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
     also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
+      unfolding set_lebesgue_integral_def
       apply (rule integral_mono [OF 3])
        apply (simp add: emeasure_lborel_Icc_eq)
       apply (case_tac "x \<in> {-d/2..d/2}")
@@ -397,11 +405,12 @@
       using d0 apply auto
       done
     also from d0 4 have "\<dots> = d * \<epsilon> / 4"
-      by simp
+      unfolding set_lebesgue_integral_def by simp
     finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" .
     have "cmod (1 - char (M n) x) \<le> 2" for n x
       by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1)
     then have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)"
+      unfolding set_lebesgue_integral_def
       apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"])
       apply (auto intro!: char_conv tendsto_intros
                   simp: emeasure_lborel_Icc_eq
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -541,7 +541,7 @@
   shows   "infsetsum (pmf p) A = 1"
 proof -
   have "infsetsum (pmf p) A = lebesgue_integral (count_space UNIV) (pmf p)"
-    using assms unfolding infsetsum_altdef
+    using assms unfolding infsetsum_altdef set_lebesgue_integral_def
     by (intro Bochner_Integration.integral_cong) (auto simp: indicator_def set_pmf_eq)
   also have "\<dots> = 1"
     by (subst integral_eq_nn_integral) (auto simp: nn_integral_pmf)
diff -r 75b94eb58c3d -r 557ea2740125 src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Thu Apr 12 12:16:34 2018 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Apr 13 15:58:27 2018 +0100
@@ -33,12 +33,12 @@
 lemma integrable_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> set_integrable lborel {0 <..} (\<lambda>x. exp (-(x * u)))"
   using lborel_integrable_real_affine_iff[of u "\<lambda>x. indicator {0 <..} x *\<^sub>R exp (- x)" 0]
         has_bochner_integral_I0i_power_exp_m[of 0]
-  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros)
+  by (simp add: indicator_def zero_less_mult_iff mult_ac integrable.intros set_integrable_def)
 
 lemma LBINT_I0i_exp_mscale: "0 < (u::real) \<Longrightarrow> LBINT x=0..\<infinity>. exp (-(x * u)) = 1 / u"
   using lborel_integral_real_affine[of u "\<lambda>x. indicator {0<..} x *\<^sub>R exp (- x)" 0]
         has_bochner_integral_I0i_power_exp_m[of 0]
-  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty field_simps
+  by (auto simp: indicator_def zero_less_mult_iff interval_lebesgue_integral_0_infty set_lebesgue_integral_def field_simps
            dest!: has_bochner_integral_integral_eq)
 
 lemma LBINT_I0c_exp_mscale_sin:
@@ -83,11 +83,11 @@
   show "LBINT x=-\<infinity>..\<infinity>. inverse (1 + x^2) = pi"
     by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
-             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
   show "set_integrable lborel (einterval (-\<infinity>) \<infinity>) (\<lambda>x. inverse (1 + x^2))"
     by (subst interval_integral_substitution_nonneg[of "-pi/2" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 filterlim_tan_at_right
-             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left add_nonneg_eq_0_iff set_integrable_def)
 qed
 
 lemma
@@ -103,12 +103,12 @@
   show "LBINT x=0..\<infinity>. 1 / (1 + x^2) = pi / 2"
     by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
-             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
   show "interval_lebesgue_integrable lborel 0 \<infinity> (\<lambda>x. 1 / (1 + x^2))"
     unfolding interval_lebesgue_integrable_def
     by (subst interval_integral_substitution_nonneg[of "0" "pi/2" tan "\<lambda>x. 1 + (tan x)^2"])
        (auto intro: derivative_eq_intros 1 2 tendsto_eq_intros
-             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff)
+             simp add: ereal_tendsto_simps filterlim_tan_at_left zero_ereal_def add_nonneg_eq_0_iff set_integrable_def)
 qed
 
 section \<open>The sinc function, and the sine integral (Si)\<close>
@@ -212,10 +212,12 @@
   have int: "set_integrable lborel {0<..} (\<lambda>x. exp (- x) * (x + 1) :: real)"
     unfolding distrib_left
     using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
-    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps)
+    by (intro set_integral_add) (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
 
   have "((\<lambda>t::real. LBINT x:{0<..}. ?F x t) \<longlongrightarrow> LBINT x::real:{0<..}. 0) at_top"
-  proof (rule integral_dominated_convergence_at_top[OF _ _ int], simp_all del: abs_divide split: split_indicator)
+    unfolding set_lebesgue_integral_def
+  proof (rule integral_dominated_convergence_at_top[OF _ _ int [unfolded set_integrable_def]], 
+         simp_all del: abs_divide split: split_indicator)
     have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
       by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
          (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
@@ -241,7 +243,7 @@
     qed
   qed
   then show "((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
-    by (simp add: interval_lebesgue_integral_0_infty)
+    by (simp add: interval_lebesgue_integral_0_infty set_lebesgue_integral_def)
 qed
 
 lemma Si_at_top_integrable:
@@ -258,10 +260,10 @@
   have "set_integrable lborel {0<..} (\<lambda>x. (exp (- x) * x) * (sin t/t) + exp (- x) * cos t)"
     using has_bochner_integral_I0i_power_exp_m[of 0] has_bochner_integral_I0i_power_exp_m[of 1]
     by (intro set_integral_add set_integrable_mult_left)
-       (auto dest!: integrable.intros simp: ac_simps)
-  from lborel_integrable_real_affine[OF this, of t 0]
+       (auto dest!: integrable.intros simp: ac_simps set_integrable_def)
+  from lborel_integrable_real_affine[OF this [unfolded set_integrable_def], of t 0]
   show ?thesis
-    unfolding interval_lebesgue_integral_0_infty
+    unfolding interval_lebesgue_integral_0_infty set_integrable_def
     by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
 qed
 
@@ -275,9 +277,10 @@
       unfolding Si_def using \<open>0 \<le> t\<close>
       by (intro interval_integral_discrete_difference[where X="{0}"]) (auto simp: LBINT_I0i_exp_mscale)
     also have "\<dots> = LBINT x. (LBINT u=ereal 0..\<infinity>. indicator {0 <..< t} x *\<^sub>R sin x * exp (-(u * x)))"
-      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac)
+      using \<open>0\<le>t\<close> by (simp add: zero_ereal_def interval_lebesgue_integral_le_eq mult_ac set_lebesgue_integral_def)
     also have "\<dots> = LBINT x. (LBINT u. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
-      by (subst interval_integral_Ioi) (simp_all add: indicator_times ac_simps)
+      apply (subst interval_integral_Ioi)
+      unfolding set_lebesgue_integral_def  by(simp_all add: indicator_times ac_simps )
     also have "\<dots> = LBINT u. (LBINT x. indicator ({0<..} \<times> {0 <..< t}) (u, x) *\<^sub>R (sin x * exp (-(u * x))))"
     proof (intro lborel_pair.Fubini_integral[symmetric] lborel_pair.Fubini_integrable)
       show "(\<lambda>(x, y). indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x))))
@@ -293,7 +296,7 @@
           by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: abs_mult)
         also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (LBINT y=0..\<infinity>.  exp (- (y * x)))"
           by (cases "x > 0")
-             (auto simp: field_simps interval_lebesgue_integral_0_infty split: split_indicator)
+             (auto simp: field_simps interval_lebesgue_integral_0_infty set_lebesgue_integral_def split: split_indicator)
         also have "\<dots> = \<bar>sin x\<bar> * indicator {0<..<t} x * (1 / x)"
           by (cases "x > 0") (auto simp add: LBINT_I0i_exp_mscale)
         also have "\<dots> = indicator {0..t} x *\<^sub>R \<bar>sinc x\<bar>"
@@ -301,7 +304,7 @@
         finally show "indicator {0..t} x *\<^sub>R abs (sinc x) = LBINT y. norm (?f (x, y))"
           by simp
       qed
-      moreover have "set_integrable lborel {0 .. t} (\<lambda>x. abs (sinc x))"
+      moreover have "integrable lborel (\<lambda>x. indicat_real {0..t} x *\<^sub>R \<bar>sinc x\<bar>)"
         by (auto intro!: borel_integrable_compact continuous_intros simp del: real_scaleR_def)
       ultimately show "integrable lborel (\<lambda>x. LBINT y. norm (?f (x, y)))"
         by (rule integrable_cong_AE_imp[rotated 2]) simp
@@ -309,11 +312,11 @@
       have "0 < x \<Longrightarrow> set_integrable lborel {0<..} (\<lambda>y. sin x * exp (- (y * x)))" for x :: real
           by (intro set_integrable_mult_right integrable_I0i_exp_mscale)
       then show "AE x in lborel. integrable lborel (\<lambda>y. ?f (x, y))"
-        by (intro AE_I2) (auto simp: indicator_times split: split_indicator)
+        by (intro AE_I2) (auto simp: indicator_times set_integrable_def split: split_indicator)
     qed
     also have "... = LBINT u=0..\<infinity>. (LBINT x=0..t. exp (-(u * x)) * sin x)"
       using \<open>0\<le>t\<close>
-      by (auto simp: interval_lebesgue_integral_def zero_ereal_def ac_simps
+      by (auto simp: interval_lebesgue_integral_def set_lebesgue_integral_def zero_ereal_def ac_simps
                split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = LBINT u=0..\<infinity>. 1 / (1 + u\<^sup>2) - 1 / (1 + u\<^sup>2) * (exp (- (u * t)) * (u * sin t + cos t))"
       by (auto simp: divide_simps LBINT_I0c_exp_mscale_sin intro!: interval_integral_cong)
@@ -369,12 +372,12 @@
     hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
         LBINT x. indicator {0<..<T * \<theta>} x * sin x / x"
       using assms \<open>0 < \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
-        by (auto simp: ac_simps)
+        by (auto simp: ac_simps set_lebesgue_integral_def)
   } note aux1 = this
   { assume "0 > \<theta>"
     have [simp]: "integrable lborel (\<lambda>x. sin (x * \<theta>) * indicator {0<..<T} x / x)"
       using integrable_sinc' [of T \<theta>] assms
-      by (simp add: interval_lebesgue_integrable_def ac_simps)
+      by (simp add: interval_lebesgue_integrable_def set_integrable_def ac_simps)
     have "(LBINT t=ereal 0..T. sin (t * -\<theta>) / t) = (LBINT t=ereal 0..T. -\<theta> *\<^sub>R sinc (t * -\<theta>))"
       by (rule interval_integral_discrete_difference[of "{0}"]) auto
     also have "\<dots> = (LBINT t=ereal (0 * -\<theta>)..T * -\<theta>. sinc t)"
@@ -388,10 +391,10 @@
     hence "LBINT x. indicator {0<..<T} x * sin (x * \<theta>) / x =
        - (LBINT x. indicator {0<..<- (T * \<theta>)} x * sin x / x)"
       using assms \<open>0 > \<theta>\<close> unfolding interval_lebesgue_integral_def einterval_eq zero_ereal_def
-        by (auto simp add: field_simps mult_le_0_iff split: if_split_asm)
+        by (auto simp add: field_simps mult_le_0_iff set_lebesgue_integral_def split: if_split_asm)
   } note aux2 = this
   show ?thesis
-    using assms unfolding Si_def interval_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
+    using assms unfolding Si_def interval_lebesgue_integral_def set_lebesgue_integral_def sgn_real_def einterval_eq zero_ereal_def
     apply auto
     apply (erule aux1)
     apply (rule aux2)