# HG changeset patch
# User hoelzl
# Date 1474027011 -7200
# Node ID 685fb01256af401d6fea2fd4a73e06812d9df36f
# Parent  a6cd18af8bf941cae81c622a9f3e8e2f5fe6b1dc
move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel

diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -187,7 +187,7 @@
       using U by (auto
           intro: borel_measurable_simple_function
           intro!: borel_measurable_enn2real borel_measurable_times
-          simp: U'_def zero_le_mult_iff enn2real_nonneg)
+          simp: U'_def zero_le_mult_iff)
     show "incseq U'"
       using U(2,3)
       by (auto simp: incseq_def le_fun_def image_iff eq_commute U'_def indicator_def enn2real_mono)
@@ -212,7 +212,7 @@
     ultimately have U': "(\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z) = U' i"
       by (simp add: U'_def fun_eq_iff)
     have "\<And>x. x \<in> U' i ` space M \<Longrightarrow> 0 \<le> x"
-      by (auto simp: U'_def enn2real_nonneg)
+      by (auto simp: U'_def)
     with fin have "P (\<lambda>z. \<Sum>y\<in>U' i`space M. y * indicator {x\<in>space M. U' i x = y} z)"
     proof induct
       case empty from set[of "{}"] show ?case
@@ -866,7 +866,7 @@
     simple_bochner_integrable M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x)"
   by (simp add: simple_bochner_integrable.simps space_restrict_space
     simple_function_restrict_space[OF \<Omega>] emeasure_restrict_space[OF \<Omega>] Collect_restrict
-    indicator_eq_0_iff conj_ac)
+    indicator_eq_0_iff conj_left_commute)
 
 lemma simple_bochner_integral_restrict_space:
   fixes f :: "_ \<Rightarrow> 'b::real_normed_vector"
@@ -1624,7 +1624,7 @@
       with seq show "\<exists>N. \<forall>n\<ge>N. 0 \<le> integral\<^sup>L M (U n)"
         by auto
     qed
-  qed (auto simp: measure_nonneg integrable_mult_left_iff)
+  qed (auto simp: integrable_mult_left_iff)
   also have "\<dots> = integral\<^sup>L M f"
     using nonneg by (auto intro!: integral_cong_AE)
   finally show ?thesis .
@@ -2466,10 +2466,10 @@
   shows "ennreal (\<integral>x. enn2real (f x) \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
 proof (subst nn_integral_eq_integral[symmetric])
   show "integrable M (\<lambda>x. enn2real (f x))"
-    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI enn2real_nonneg)
+    using ae by (intro integrable_const_bound[where B=B]) (auto simp: enn2real_leI)
   show "(\<integral>\<^sup>+ x. ennreal (enn2real (f x)) \<partial>M) = integral\<^sup>N M f"
     using ae by (intro nn_integral_cong_AE) (auto simp: le_less_trans[OF _ ennreal_less_top])
-qed (auto simp: enn2real_nonneg)
+qed auto
 
 lemma (in finite_measure) integral_less_AE:
   fixes X Y :: "'a \<Rightarrow> real"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -1,7 +1,7 @@
 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
 
 theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Henstock_Kurzweil_Integration
+imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *)
 begin
 
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -927,7 +927,6 @@
   unfolding dot_matrix_product transpose_columnvector[symmetric]
     dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
 
-
 lemma infnorm_cart:"infnorm (x::real^'n) = Sup {\<bar>x$i\<bar> |i. i\<in>UNIV}"
   by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right)
 
@@ -1409,12 +1408,6 @@
   apply (rule bounded_linearI[where K=1])
   using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
 
-lemma integral_component_eq_cart[simp]:
-  fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
-  assumes "f integrable_on s"
-  shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
-  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
-
 lemma interval_split_cart:
   "{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}"
   "cbox a b \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports Cartesian_Euclidean_Space "~~/src/HOL/Library/Nonpos_Ints"
+imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
 begin
 
 
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -9,6 +9,9 @@
 imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
 begin
 
+lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
+  by (rule bounded_linear_inner_left)
+
 lemma onorm_inner_left:
   assumes "bounded_linear r"
   shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
@@ -2906,5 +2909,4 @@
     by eventually_elim (auto simp: dist_norm field_simps)
 qed (auto intro!: bounded_linear_intros simp: split_beta')
 
-
 end
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Embed_Measure.thy
--- a/src/HOL/Analysis/Embed_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Embed_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -47,7 +47,7 @@
 lemma sets_embed_eq_vimage_algebra:
   assumes "inj_on f (space M)"
   shows "sets (embed_measure M f) = sets (vimage_algebra (f`space M) (the_inv_into (space M) f) M)"
-  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 simple_image
+  by (auto simp: sets_embed_measure'[OF assms] Pi_iff the_inv_into_f_f assms sets_vimage_algebra2 Setcompr_eq_image
            dest: sets.sets_into_space
            intro!: image_cong the_inv_into_vimage[symmetric])
 
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -0,0 +1,606 @@
+theory Equivalence_Lebesgue_Henstock_Integration
+  imports Lebesgue_Measure Henstock_Kurzweil_Integration
+begin
+
+subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
+
+lemma has_integral_measure_lborel:
+  fixes A :: "'a::euclidean_space set"
+  assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
+  shows "((\<lambda>x. 1) has_integral measure lborel A) A"
+proof -
+  { fix l u :: 'a
+    have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
+    proof cases
+      assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
+      then show ?thesis
+        apply simp
+        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
+        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
+        using has_integral_const[of "1::real" l u]
+        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
+        done
+    next
+      assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
+      then have "box l u = {}"
+        unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
+      then show ?thesis
+        by simp
+    qed }
+  note has_integral_box = this
+
+  { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
+    have "Int_stable  (range (\<lambda>(a, b). box a b))"
+      by (auto simp: Int_stable_def box_Int_box)
+    moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
+      by auto
+    moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
+       using A unfolding borel_eq_box by simp
+    ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
+    proof (induction rule: sigma_sets_induct_disjoint)
+      case (basic A) then show ?case
+        by (auto simp: box_Int_box has_integral_box)
+    next
+      case empty then show ?case
+        by simp
+    next
+      case (compl A)
+      then have [measurable]: "A \<in> sets borel"
+        by (simp add: borel_eq_box)
+
+      have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
+        by (simp add: has_integral_box)
+      moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
+        by (subst has_integral_restrict) (auto intro: compl)
+      ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+        by (rule has_integral_sub)
+      then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
+        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
+      then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
+        by (subst (asm) has_integral_restrict) auto
+      also have "?M (box a b) - ?M A = ?M (UNIV - A)"
+        by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
+      finally show ?case .
+    next
+      case (union F)
+      then have [measurable]: "\<And>i. F i \<in> sets borel"
+        by (simp add: borel_eq_box subset_eq)
+      have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
+      proof (rule has_integral_monotone_convergence_increasing)
+        let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
+        show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
+          using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
+        show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+          by (intro setsum_mono2) auto
+        from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
+          by (auto simp add: disjoint_family_on_def)
+        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
+          apply (auto simp: * setsum.If_cases Iio_Int_singleton)
+          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
+          apply simp
+          done
+        have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
+          by (intro emeasure_mono) auto
+
+        with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
+          unfolding sums_def[symmetric] UN_extend_simps
+          by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
+      qed
+      then show ?case
+        by (subst (asm) has_integral_restrict) auto
+    qed }
+  note * = this
+
+  show ?thesis
+  proof (rule has_integral_monotone_convergence_increasing)
+    let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
+    let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
+    let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
+
+    show "\<And>n::nat. (?f n has_integral ?M n) A"
+      using * by (subst has_integral_restrict) simp_all
+    show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
+      by (auto simp: box_def)
+    { fix x assume "x \<in> A"
+      moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
+        by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
+      ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
+        by (simp add: indicator_def UN_box_eq_UNIV) }
+
+    have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
+      by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
+    also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
+    proof (intro ext emeasure_eq_ennreal_measure)
+      fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
+        by (intro emeasure_mono) auto
+      then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
+        by (auto simp: top_unique)
+    qed
+    finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
+      using emeasure_eq_ennreal_measure[of lborel A] finite
+      by (simp add: UN_box_eq_UNIV less_top)
+  qed
+qed
+
+lemma nn_integral_has_integral:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+  shows "(f has_integral r) UNIV"
+using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
+  case (set A)
+  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+    by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
+  with set show ?case
+    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
+next
+  case (mult g c)
+  then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
+    by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
+  with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
+  obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
+    by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
+       (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
+  with mult show ?case
+    by (auto intro!: has_integral_cmult_real)
+next
+  case (add g h)
+  then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
+    by (simp add: nn_integral_add)
+  with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
+    by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
+       (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
+  with add show ?case
+    by (auto intro!: has_integral_add)
+next
+  case (seq U)
+  note seq(1)[measurable] and f[measurable]
+
+  { fix i x
+    have "U i x \<le> f x"
+      using seq(5)
+      apply (rule LIMSEQ_le_const)
+      using seq(4)
+      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
+      done }
+  note U_le_f = this
+
+  { fix i
+    have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
+      using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
+    then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
+      using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
+    moreover note seq
+    ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
+      by auto }
+  then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
+    and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
+    and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
+
+  have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
+
+  have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
+  proof (rule monotone_convergence_increasing)
+    show "\<forall>k. U k integrable_on UNIV" using U_int by auto
+    show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
+    then show "bounded {integral UNIV (U k) |k. True}"
+      using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
+    show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
+      using seq by auto
+  qed
+  moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
+    using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
+  ultimately have "integral UNIV f = r"
+    by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
+  with * show ?case
+    by (simp add: has_integral_integral)
+qed
+
+lemma nn_integral_lborel_eq_integral:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+  shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
+proof -
+  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
+  then show ?thesis
+    using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
+qed
+
+lemma nn_integral_integrable_on:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
+  shows "f integrable_on UNIV"
+proof -
+  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
+    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
+  then show ?thesis
+    by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
+qed
+
+lemma nn_integral_has_integral_lborel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
+  assumes I: "(f has_integral I) UNIV"
+  shows "integral\<^sup>N lborel f = I"
+proof -
+  from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
+  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
+  let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
+
+  note F(1)[THEN borel_measurable_simple_function, measurable]
+
+  have "0 \<le> I"
+    using I by (rule has_integral_nonneg) (simp add: nonneg)
+
+  have F_le_f: "enn2real (F i x) \<le> f x" for i x
+    using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
+    by (cases "F i x" rule: ennreal_cases) auto
+  let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
+  have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
+  proof (subst nn_integral_monotone_convergence_SUP[symmetric])
+    { fix x
+      obtain j where j: "x \<in> ?B j"
+        using UN_box_eq_UNIV by auto
+
+      have "ennreal (f x) = (SUP i. F i x)"
+        using F(4)[of x] nonneg[of x] by (simp add: max_def)
+      also have "\<dots> = (SUP i. ?F i x)"
+      proof (rule SUP_eq)
+        fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
+          using j F(2)
+          by (intro bexI[of _ "max i j"])
+             (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
+      qed (auto intro!: F split: split_indicator)
+      finally have "ennreal (f x) =  (SUP i. ?F i x)" . }
+    then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
+      by simp
+  qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
+  also have "\<dots> \<le> ennreal I"
+  proof (rule SUP_least)
+    fix i :: nat
+    have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
+    proof (rule nn_integral_bound_simple_function)
+      have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
+        emeasure lborel (?B i)"
+        by (intro emeasure_mono)  (auto split: split_indicator)
+      then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
+        by (auto simp: less_top[symmetric] top_unique)
+    qed (auto split: split_indicator
+              intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
+
+    have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
+      using F(4) finite_F
+      by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
+
+    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
+      (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
+      using F(3,4)
+      by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
+    also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
+      using F
+      by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
+         (auto split: split_indicator intro: enn2real_nonneg)
+    also have "\<dots> \<le> ennreal I"
+      by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
+               simp: \<open>0 \<le> I\<close> split: split_indicator )
+    finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
+  qed
+  finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
+    by (auto simp: less_top[symmetric] top_unique)
+  from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
+    by (simp add: integral_unique)
+qed
+
+lemma has_integral_iff_emeasure_lborel:
+  fixes A :: "'a::euclidean_space set"
+  assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
+  shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
+proof (cases "emeasure lborel A = \<infinity>")
+  case emeasure_A: True
+  have "\<not> (\<lambda>x. 1::real) integrable_on A"
+  proof
+    assume int: "(\<lambda>x. 1::real) integrable_on A"
+    then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
+      unfolding indicator_def[abs_def] integrable_restrict_univ .
+    then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
+      by auto
+    from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
+      by (simp add: ennreal_indicator)
+  qed
+  with emeasure_A show ?thesis
+    by auto
+next
+  case False
+  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
+    by (simp add: has_integral_measure_lborel less_top)
+  with False show ?thesis
+    by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
+qed
+
+lemma has_integral_integral_real:
+  fixes f::"'a::euclidean_space \<Rightarrow> real"
+  assumes f: "integrable lborel f"
+  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
+using f proof induct
+  case (base A c) then show ?case
+    by (auto intro!: has_integral_mult_left simp: )
+       (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
+next
+  case (add f g) then show ?case
+    by (auto intro!: has_integral_add)
+next
+  case (lim f s)
+  show ?case
+  proof (rule has_integral_dominated_convergence)
+    show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
+    show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
+      using \<open>integrable lborel f\<close>
+      by (intro nn_integral_integrable_on)
+         (auto simp: integrable_iff_bounded abs_mult  nn_integral_cmult ennreal_mult ennreal_mult_less_top)
+    show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
+      using lim by (auto simp add: abs_mult)
+    show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
+      using lim by auto
+    show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
+      using lim lim(1)[THEN borel_measurable_integrable]
+      by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
+  qed
+qed
+
+context
+  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+begin
+
+lemma has_integral_integral_lborel:
+  assumes f: "integrable lborel f"
+  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
+proof -
+  have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
+    using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
+  also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
+    by (simp add: fun_eq_iff euclidean_representation)
+  also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
+    using f by (subst (2) eq_f[symmetric]) simp
+  finally show ?thesis .
+qed
+
+lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
+  using has_integral_integral_lborel by auto
+
+lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
+  using has_integral_integral_lborel by auto
+
+end
+
+subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
+
+text \<open>
+
+For the positive integral we replace continuity with Borel-measurability.
+
+\<close>
+
+lemma
+  fixes f :: "real \<Rightarrow> real"
+  assumes [measurable]: "f \<in> borel_measurable borel"
+  assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
+  shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
+    and has_bochner_integral_FTC_Icc_nonneg:
+      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+    and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+    and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
+proof -
+  have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
+    using f(2) by (auto split: split_indicator)
+
+  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
+    using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
+
+  have "(f has_integral F b - F a) {a..b}"
+    by (intro fundamental_theorem_of_calculus)
+       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+             intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
+  then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
+    unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
+    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
+  then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
+    by (rule nn_integral_has_integral_lborel[OF *])
+  then show ?has
+    by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
+  then show ?eq ?int
+    unfolding has_bochner_integral_iff by auto
+  show ?nn
+    by (subst nn[symmetric])
+       (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
+qed
+
+lemma
+  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+  assumes "a \<le> b"
+  assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+  assumes cont: "continuous_on {a .. b} f"
+  shows has_bochner_integral_FTC_Icc:
+      "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
+    and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
+proof -
+  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+  have int: "integrable lborel ?f"
+    using borel_integrable_compact[OF _ cont] by auto
+  have "(f has_integral F b - F a) {a..b}"
+    using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
+  moreover
+  have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
+    using has_integral_integral_lborel[OF int]
+    unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
+    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
+  ultimately show ?eq
+    by (auto dest: has_integral_unique)
+  then show ?has
+    using int by (auto simp: has_bochner_integral_iff)
+qed
+
+lemma
+  fixes f :: "real \<Rightarrow> real"
+  assumes "a \<le> b"
+  assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
+  assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
+  shows has_bochner_integral_FTC_Icc_real:
+      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
+    and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
+proof -
+  have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+    using deriv by (auto intro: DERIV_subset)
+  have 2: "continuous_on {a .. b} f"
+    using cont by (intro continuous_at_imp_continuous_on) auto
+  show ?has ?eq
+    using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
+    by (auto simp: mult.commute)
+qed
+
+lemma nn_integral_FTC_atLeast:
+  fixes f :: "real \<Rightarrow> real"
+  assumes f_borel: "f \<in> borel_measurable borel"
+  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
+  assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
+  assumes lim: "(F \<longlongrightarrow> T) at_top"
+  shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
+proof -
+  let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
+  let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
+
+  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
+    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
+  then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
+    by (intro tendsto_le_const[OF _ lim])
+       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
+
+  have "(SUP i::nat. ?f i x) = ?fR x" for x
+  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
+    from reals_Archimedean2[of "x - a"] guess n ..
+    then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
+      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
+    then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
+      by (rule Lim_eventually)
+  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
+  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+    by simp
+  also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
+  proof (rule nn_integral_monotone_convergence_SUP)
+    show "incseq ?f"
+      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
+    show "\<And>i. (?f i) \<in> borel_measurable lborel"
+      using f_borel by auto
+  qed
+  also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
+    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
+  also have "\<dots> = T - F a"
+  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
+    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
+      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
+      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
+      apply (rule filterlim_real_sequentially)
+      done
+    then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
+      by (simp add: F_mono F_le_T tendsto_diff)
+  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
+  finally show ?thesis .
+qed
+
+lemma integral_power:
+  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
+proof (subst integral_FTC_Icc_real)
+  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
+    by (intro derivative_eq_intros) auto
+qed (auto simp: field_simps simp del: of_nat_Suc)
+
+subsection \<open>Integration by parts\<close>
+
+lemma integral_by_parts_integrable:
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes "a \<le> b"
+  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes [intro]: "!!x. DERIV F x :> f x"
+  assumes [intro]: "!!x. DERIV G x :> g x"
+  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
+  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
+
+lemma integral_by_parts:
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes [arith]: "a \<le> b"
+  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes [intro]: "!!x. DERIV F x :> f x"
+  assumes [intro]: "!!x. DERIV G x :> g x"
+  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
+            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+proof-
+  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
+    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
+      (auto intro!: DERIV_isCont)
+
+  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
+    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
+    apply (subst Bochner_Integration.integral_add[symmetric])
+    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
+    by (auto intro!: DERIV_isCont Bochner_Integration.integral_cong split: split_indicator)
+
+  thus ?thesis using 0 by auto
+qed
+
+lemma integral_by_parts':
+  fixes f g F G::"real \<Rightarrow> real"
+  assumes "a \<le> b"
+  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
+  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
+  assumes "!!x. DERIV F x :> f x"
+  assumes "!!x. DERIV G x :> g x"
+  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
+            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
+  using integral_by_parts[OF assms] by (simp add: ac_simps)
+
+lemma has_bochner_integral_even_function:
+  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+  assumes even: "\<And>x. f (- x) = f x"
+  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
+proof -
+  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+    by (auto split: split_indicator)
+  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
+    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+       (auto simp: indicator even f)
+  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
+    by (rule has_bochner_integral_add)
+  then have "has_bochner_integral lborel f (x + x)"
+    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+       (auto split: split_indicator)
+  then show ?thesis
+    by (simp add: scaleR_2)
+qed
+
+lemma has_bochner_integral_odd_function:
+  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
+  assumes odd: "\<And>x. f (- x) = - f x"
+  shows "has_bochner_integral lborel f 0"
+proof -
+  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
+    by (auto split: split_indicator)
+  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
+    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
+       (auto simp: indicator odd f)
+  from has_bochner_integral_minus[OF this]
+  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
+    by simp
+  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
+    by (rule has_bochner_integral_add)
+  then have "has_bochner_integral lborel f (x + - x)"
+    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
+       (auto split: split_indicator)
+  then show ?thesis
+    by simp
+qed
+
+end
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -6,9 +6,7 @@
 
 theory Henstock_Kurzweil_Integration
 imports
-  Derivative
-  Uniform_Limit
-  "~~/src/HOL/Library/Indicator_Function"
+  Lebesgue_Measure
 begin
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -22,122 +20,19 @@
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
 
+lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
+  by auto
+
 declare norm_triangle_ineq4[intro]
 
-lemma simple_image: "{f x |x . x \<in> s} = f ` s"
-  by blast
-
-lemma linear_simps:
-  assumes "bounded_linear f"
-  shows
-    "f (a + b) = f a + f b"
-    "f (a - b) = f a - f b"
-    "f 0 = 0"
-    "f (- a) = - f a"
-    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
-proof -
-  interpret f: bounded_linear f by fact
-  show "f (a + b) = f a + f b" by (rule f.add)
-  show "f (a - b) = f a - f b" by (rule f.diff)
-  show "f 0 = 0" by (rule f.zero)
-  show "f (- a) = - f a" by (rule f.minus)
-  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
-qed
-
-lemma bounded_linearI:
-  assumes "\<And>x y. f (x + y) = f x + f y"
-    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
-    and "\<And>x. norm (f x) \<le> norm x * K"
-  shows "bounded_linear f"
-  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
-
-lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
-  by (rule bounded_linear_inner_left)
-
-lemma transitive_stepwise_lt_eq:
-  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
-  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))"
-  (is "?l = ?r")
-proof safe
-  assume ?r
-  fix n m :: nat
-  assume "m < n"
-  then show "R m n"
-  proof (induct n arbitrary: m)
-    case 0
-    then show ?case by auto
-  next
-    case (Suc n)
-    show ?case
-    proof (cases "m < n")
-      case True
-      show ?thesis
-        apply (rule assms[OF Suc(1)[OF True]])
-        using \<open>?r\<close>
-        apply auto
-        done
-    next
-      case False
-      then have "m = n"
-        using Suc(2) by auto
-      then show ?thesis
-        using \<open>?r\<close> by auto
-    qed
-  qed
-qed auto
-
-lemma transitive_stepwise_gt:
-  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n)"
-  shows "\<forall>n>m. R m n"
-proof -
-  have "\<forall>m. \<forall>n>m. R m n"
-    apply (subst transitive_stepwise_lt_eq)
-    apply (blast intro: assms)+
-    done
-  then show ?thesis by auto
-qed
-
-lemma transitive_stepwise_le_eq:
-  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
-  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))"
-  (is "?l = ?r")
-proof safe
-  assume ?r
-  fix m n :: nat
-  assume "m \<le> n"
-  then show "R m n"
-  proof (induct n arbitrary: m)
-    case 0
-    with assms show ?case by auto
-  next
-    case (Suc n)
-    show ?case
-    proof (cases "m \<le> n")
-      case True
-      with Suc.hyps \<open>\<forall>n. R n (Suc n)\<close> assms show ?thesis
-        by blast
-    next
-      case False
-      then have "m = Suc n"
-        using Suc(2) by auto
-      then show ?thesis
-        using assms(1) by auto
-    qed
-  qed
-qed auto
-
 lemma transitive_stepwise_le:
-  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
-    and "\<And>n. R n (Suc n)"
+  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" and "\<And>n. R n (Suc n)"
   shows "\<forall>n\<ge>m. R m n"
-proof -
-  have "\<forall>m. \<forall>n\<ge>m. R m n"
-    apply (subst transitive_stepwise_le_eq)
-    apply (blast intro: assms)+
-    done
-  then show ?thesis by auto
-qed
-
+proof (intro allI impI)
+  show "m \<le> n \<Longrightarrow> R m n" for n
+    by (induction rule: dec_induct)
+       (use assms in blast)+
+qed
 
 subsection \<open>Some useful lemmas about intervals.\<close>
 
@@ -208,13 +103,28 @@
     "finite f \<Longrightarrow> open s \<Longrightarrow> \<forall>t\<in>f. \<exists>a b. t = cbox a b \<Longrightarrow> \<forall>t\<in>f. s \<inter> (interior t) = {} \<Longrightarrow> s \<inter> interior (\<Union>f) = {}"
   using interior_Union_subset_cbox[of f "UNIV - s"] by auto
 
+lemma interval_split:
+  fixes a :: "'a::euclidean_space"
+  assumes "k \<in> Basis"
+  shows
+    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
+    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
+  apply (rule_tac[!] set_eqI)
+  unfolding Int_iff mem_box mem_Collect_eq
+  using assms
+  apply auto
+  done
+
+lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
+  by (simp add: box_ne_empty)
+
 subsection \<open>Bounds on intervals where they exist.\<close>
 
 definition interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
   where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
 
 definition interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
-   where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
+  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
@@ -242,7 +152,6 @@
     and "interval_lowerbound (cbox a b) = a"
   using assms unfolding box_ne_empty by auto
 
-
 lemma interval_upperbound_Times:
   assumes "A \<noteq> {}" and "B \<noteq> {}"
   shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
@@ -273,219 +182,83 @@
 
 subsection \<open>Content (length, area, volume...) of an interval.\<close>
 
-definition "content (s::('a::euclidean_space) set) =
-  (if s = {} then 0 else (\<Prod>i\<in>Basis. (interval_upperbound s)\<bullet>i - (interval_lowerbound s)\<bullet>i))"
-
-lemma interval_not_empty: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> cbox a b \<noteq> {}"
-  unfolding box_eq_empty unfolding not_ex not_less by auto
-
-lemma content_cbox:
-  fixes a :: "'a::euclidean_space"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-  using interval_not_empty[OF assms]
-  unfolding content_def
-  by auto
-
-lemma content_cbox':
-  fixes a :: "'a::euclidean_space"
-  assumes "cbox a b \<noteq> {}"
-  shows "content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-    using assms box_ne_empty(1) content_cbox by blast
+abbreviation content :: "'a::euclidean_space set \<Rightarrow> real"
+  where "content s \<equiv> measure lborel s"
+
+lemma content_cbox_cases:
+  "content (cbox a b) = (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
+  by (simp add: measure_lborel_cbox_eq inner_diff)
+
+lemma content_cbox: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  unfolding content_cbox_cases by simp
+
+lemma content_cbox': "cbox a b \<noteq> {} \<Longrightarrow> content (cbox a b) = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  by (simp add: box_ne_empty inner_diff)
 
 lemma content_real: "a \<le> b \<Longrightarrow> content {a..b} = b - a"
-  by (auto simp: interval_upperbound_def interval_lowerbound_def content_def)
+  by simp
 
 lemma abs_eq_content: "\<bar>y - x\<bar> = (if x\<le>y then content {x .. y} else content {y..x})"
   by (auto simp: content_real)
 
-lemma content_singleton[simp]: "content {a} = 0"
-proof -
-  have "content (cbox a a) = 0"
-    by (subst content_cbox) (auto simp: ex_in_conv)
-  then show ?thesis by (simp add: cbox_sing)
-qed
-
-lemma content_unit[iff]: "content(cbox 0 (One::'a::euclidean_space)) = 1"
- proof -
-   have *: "\<forall>i\<in>Basis. (0::'a)\<bullet>i \<le> (One::'a)\<bullet>i"
-    by auto
-  have "0 \<in> cbox 0 (One::'a)"
-    unfolding mem_box by auto
-  then show ?thesis
-     unfolding content_def interval_bounds[OF *] using setprod.neutral_const by auto
- qed
-
-lemma content_pos_le[intro]:
-  fixes a::"'a::euclidean_space"
-  shows "0 \<le> content (cbox a b)"
-proof (cases "cbox a b = {}")
-  case False
-  then have *: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-    unfolding box_ne_empty .
-  have "0 \<le> (\<Prod>i\<in>Basis. interval_upperbound (cbox a b) \<bullet> i - interval_lowerbound (cbox a b) \<bullet> i)"
-    apply (rule setprod_nonneg)
-    unfolding interval_bounds[OF *]
-    using *
-    apply auto
-    done
-  also have "\<dots> = content (cbox a b)" using False by (simp add: content_def)
-  finally show ?thesis .
-qed (simp add: content_def)
-
-corollary content_nonneg [simp]:
-  fixes a::"'a::euclidean_space"
-  shows "~ content (cbox a b) < 0"
-using not_le by blast
-
-lemma content_pos_lt:
-  fixes a :: "'a::euclidean_space"
-  assumes "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
-  shows "0 < content (cbox a b)"
-  using assms
-  by (auto simp: content_def box_eq_empty intro!: setprod_pos)
-
-lemma content_eq_0:
-  "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
-  by (auto simp: content_def box_eq_empty intro!: setprod_pos bexI)
-
-lemma cond_cases: "(P \<Longrightarrow> Q x) \<Longrightarrow> (\<not> P \<Longrightarrow> Q y) \<Longrightarrow> Q (if P then x else y)"
-  by auto
-
-lemma content_cbox_cases:
-  "content (cbox a (b::'a::euclidean_space)) =
-    (if \<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i then setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) Basis else 0)"
-  by (auto simp: not_le content_eq_0 intro: less_imp_le content_cbox)
+lemma content_singleton: "content {a} = 0"
+  by simp
+
+lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
+  by simp
+
+lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
+  by simp
+
+corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
+  using not_le by blast
+
+lemma content_pos_lt: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i \<Longrightarrow> 0 < content (cbox a b)"
+  by (auto simp: less_imp_le inner_diff box_eq_empty intro!: setprod_pos)
+
+lemma content_eq_0: "content (cbox a b) = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i)"
+  by (auto simp: content_cbox_cases not_le intro: less_imp_le antisym eq_refl)
 
 lemma content_eq_0_interior: "content (cbox a b) = 0 \<longleftrightarrow> interior(cbox a b) = {}"
-  unfolding content_eq_0 interior_cbox box_eq_empty
-  by auto
-
-lemma content_pos_lt_eq:
-  "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
-proof (rule iffI)
-  assume "0 < content (cbox a b)"
-  then have "content (cbox a b) \<noteq> 0" by auto
-  then show "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"
-    unfolding content_eq_0 not_ex not_le by fastforce
-next
-  assume "\<forall>i\<in>Basis. a \<bullet> i < b \<bullet> i"
-  then show "0 < content (cbox a b)"
-    by (metis content_pos_lt)
-qed
+  unfolding content_eq_0 interior_cbox box_eq_empty by auto
+
+lemma content_pos_lt_eq: "0 < content (cbox a (b::'a::euclidean_space)) \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)"
+  by (auto simp add: content_cbox_cases less_le setprod_nonneg)
 
 lemma content_empty [simp]: "content {} = 0"
-  unfolding content_def by auto
+  by simp
 
 lemma content_real_if [simp]: "content {a..b} = (if a \<le> b then b - a else 0)"
   by (simp add: content_real)
 
-lemma content_subset:
-  assumes "cbox a b \<subseteq> cbox c d"
-  shows "content (cbox a b) \<le> content (cbox c d)"
-proof (cases "cbox a b = {}")
-  case True
-  then show ?thesis
-    using content_pos_le[of c d] by auto
-next
-  case False
-  then have ab_ne: "\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i"
-    unfolding box_ne_empty by auto
-  then have ab_ab: "a\<in>cbox a b" "b\<in>cbox a b"
-    unfolding mem_box by auto
-  have "cbox c d \<noteq> {}" using assms False by auto
-  then have cd_ne: "\<forall>i\<in>Basis. c \<bullet> i \<le> d \<bullet> i"
-    using assms unfolding box_ne_empty by auto
-  have "\<And>i. i \<in> Basis \<Longrightarrow> 0 \<le> b \<bullet> i - a \<bullet> i"
-    using ab_ne by auto
-  moreover
-  have "\<And>i. i \<in> Basis \<Longrightarrow> b \<bullet> i - a \<bullet> i \<le> d \<bullet> i - c \<bullet> i"
-    using assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(2)]
-          assms[unfolded subset_eq mem_box,rule_format,OF ab_ab(1)]
-      by (metis diff_mono)
-  ultimately show ?thesis
-    unfolding content_def interval_bounds[OF ab_ne] interval_bounds[OF cd_ne]
-    by (simp add: setprod_mono if_not_P[OF False] if_not_P[OF \<open>cbox c d \<noteq> {}\<close>])
-qed
+lemma content_subset: "cbox a b \<subseteq> cbox c d \<Longrightarrow> content (cbox a b) \<le> content (cbox c d)"
+  unfolding measure_def
+  by (intro enn2real_mono emeasure_mono) (auto simp: emeasure_lborel_cbox_eq)
 
 lemma content_lt_nz: "0 < content (cbox a b) \<longleftrightarrow> content (cbox a b) \<noteq> 0"
   unfolding content_pos_lt_eq content_eq_0 unfolding not_ex not_le by fastforce
 
-lemma content_times[simp]: "content (A \<times> B) = content A * content B"
-proof (cases "A \<times> B = {}")
-  let ?ub1 = "interval_upperbound" and ?lb1 = "interval_lowerbound"
-  let ?ub2 = "interval_upperbound" and ?lb2 = "interval_lowerbound"
-  assume nonempty: "A \<times> B \<noteq> {}"
-  hence "content (A \<times> B) = (\<Prod>i\<in>Basis. (?ub1 A, ?ub2 B) \<bullet> i - (?lb1 A, ?lb2 B) \<bullet> i)"
-      unfolding content_def by (simp add: interval_upperbound_Times interval_lowerbound_Times)
-  also have "... = content A * content B" unfolding content_def using nonempty
-    apply (subst Basis_prod_def, subst setprod.union_disjoint, force, force, force, simp)
-    apply (subst (1 2) setprod.reindex, auto intro: inj_onI)
-    done
-  finally show ?thesis .
-qed (auto simp: content_def)
-
 lemma content_Pair: "content (cbox (a,c) (b,d)) = content (cbox a b) * content (cbox c d)"
-  by (simp add: cbox_Pair_eq)
+  unfolding measure_lborel_cbox_eq Basis_prod_def
+  apply (subst setprod.union_disjoint)
+  apply (auto simp: bex_Un ball_Un)
+  apply (subst (1 2) setprod.reindex_nontrivial)
+  apply auto
+  done
 
 lemma content_cbox_pair_eq0_D:
    "content (cbox (a,c) (b,d)) = 0 \<Longrightarrow> content (cbox a b) = 0 \<or> content (cbox c d) = 0"
   by (simp add: content_Pair)
 
-lemma content_eq_0_gen:
-  fixes s :: "'a::euclidean_space set"
-  assumes "bounded s"
-  shows "content s = 0 \<longleftrightarrow> (\<exists>i\<in>Basis. \<exists>v. \<forall>x \<in> s. x \<bullet> i = v)"  (is "_ = ?rhs")
-proof safe
-  assume "content s = 0" then show ?rhs
-    apply (clarsimp simp: ex_in_conv content_def split: if_split_asm)
-    apply (rule_tac x=a in bexI)
-    apply (rule_tac x="interval_lowerbound s \<bullet> a" in exI)
-    apply (clarsimp simp: interval_upperbound_def interval_lowerbound_def)
-    apply (drule cSUP_eq_cINF_D)
-    apply (auto simp: bounded_inner_imp_bdd_above [OF assms]  bounded_inner_imp_bdd_below [OF assms])
-    done
-next
-  fix i a
-  assume "i \<in> Basis" "\<forall>x\<in>s. x \<bullet> i = a"
-  then show "content s = 0"
-    apply (clarsimp simp: content_def)
-    apply (rule_tac x=i in bexI)
-    apply (auto simp: interval_upperbound_def interval_lowerbound_def)
-    done
-qed
-
-lemma content_0_subset_gen:
-  fixes a :: "'a::euclidean_space"
-  assumes "content t = 0" "s \<subseteq> t" "bounded t" shows "content s = 0"
-proof -
-  have "bounded s"
-    using assms by (metis bounded_subset)
-  then show ?thesis
-    using assms
-    by (auto simp: content_eq_0_gen)
-qed
-
-lemma content_0_subset: "\<lbrakk>content(cbox a b) = 0; s \<subseteq> cbox a b\<rbrakk> \<Longrightarrow> content s = 0"
-  by (simp add: content_0_subset_gen bounded_cbox)
-
-
-lemma interval_split:
-  fixes a :: "'a::euclidean_space"
-  assumes "k \<in> Basis"
-  shows
-    "cbox a b \<inter> {x. x\<bullet>k \<le> c} = cbox a (\<Sum>i\<in>Basis. (if i = k then min (b\<bullet>k) c else b\<bullet>i) *\<^sub>R i)"
-    "cbox a b \<inter> {x. x\<bullet>k \<ge> c} = cbox (\<Sum>i\<in>Basis. (if i = k then max (a\<bullet>k) c else a\<bullet>i) *\<^sub>R i) b"
-  apply (rule_tac[!] set_eqI)
-  unfolding Int_iff mem_box mem_Collect_eq
-  using assms
-  apply auto
-  done
+lemma content_0_subset: "content(cbox a b) = 0 \<Longrightarrow> s \<subseteq> cbox a b \<Longrightarrow> content s = 0"
+  using emeasure_mono[of s "cbox a b" lborel]
+  by (auto simp: measure_def enn2real_eq_0_iff emeasure_lborel_cbox_eq)
 
 lemma content_split:
   fixes a :: "'a::euclidean_space"
   assumes "k \<in> Basis"
   shows "content (cbox a b) = content(cbox a b \<inter> {x. x\<bullet>k \<le> c}) + content(cbox a b \<inter> {x. x\<bullet>k \<ge> c})"
+  -- \<open>Prove using measure theory\<close>
 proof cases
   note simps = interval_split[OF assms] content_cbox_cases
   have *: "Basis = insert k (Basis - {k})" "\<And>x. finite (Basis-{x})" "\<And>x. x\<notin>Basis-{x}"
@@ -2040,11 +1813,6 @@
   "d tagged_division_of (cbox a b) \<Longrightarrow> setsum (\<lambda>(x,l). content l) d = content (cbox a b)"
   unfolding setsum.operative_tagged_division[OF operative_content, symmetric] by blast
 
-lemma
-  shows real_inner_1_left: "inner 1 x = x"
-  and real_inner_1_right: "inner x 1 = x"
-  by simp_all
-
 lemma content_real_eq_0: "content {a .. b::real} = 0 \<longleftrightarrow> a \<ge> b"
   by (metis atLeastatMost_empty_iff2 content_empty content_real diff_self eq_iff le_cases le_iff_diff_le_0)
 
@@ -3988,8 +3756,7 @@
   have "norm (setsum (\<lambda>l. content l *\<^sub>R c) p) \<le> (\<Sum>i\<in>p. norm (content i *\<^sub>R c))"
     using norm_setsum by blast
   also have "...  \<le> e * (\<Sum>i\<in>p. \<bar>content i\<bar>)"
-    apply (simp add: setsum_right_distrib[symmetric] mult.commute)
-    using assms(2) mult_right_mono by blast
+    by (simp add: setsum_right_distrib[symmetric] mult.commute assms(2) mult_right_mono setsum_nonneg)
   also have "... \<le> e * content (cbox a b)"
     apply (rule mult_left_mono [OF _ e])
     apply (simp add: sumeq)
@@ -4458,65 +4225,70 @@
   assumes "0 < e"
     and k: "k \<in> Basis"
   obtains d where "0 < d" and "content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) < e"
-proof (cases "content (cbox a b) = 0")
-  case True
-  then have ce: "content (cbox a b) < e"
-    by (metis \<open>0 < e\<close>)
+proof cases
+  assume *: "a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j)"
+  define a' where "a' d = (\<Sum>j\<in>Basis. (if j = k then max (a\<bullet>j) (c - d) else a\<bullet>j) *\<^sub>R j)" for d
+  define b' where "b' d = (\<Sum>j\<in>Basis. (if j = k then min (b\<bullet>j) (c + d) else b\<bullet>j) *\<^sub>R j)" for d
+
+  have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> (\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j)) (at_right 0)"
+    by (auto simp: b'_def a'_def intro!: tendsto_min tendsto_max tendsto_eq_intros)
+  also have "(\<Prod>j\<in>Basis. (b' 0 - a' 0) \<bullet> j) = 0"
+    using k *
+    by (intro setprod_zero bexI[OF _ k])
+       (auto simp: b'_def a'_def inner_diff inner_setsum_left inner_not_same_Basis intro!: setsum.cong)
+  also have "((\<lambda>d. \<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) \<longlongrightarrow> 0) (at_right 0) =
+    ((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)"
+  proof (intro tendsto_cong eventually_at_rightI)
+    fix d :: real assume d: "d \<in> {0<..<1}"
+    have "cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d} = cbox (a' d) (b' d)" for d
+      using * d k by (auto simp add: cbox_def set_eq_iff Int_def ball_conj_distrib abs_diff_le_iff a'_def b'_def)
+    moreover have "j \<in> Basis \<Longrightarrow> a' d \<bullet> j \<le> b' d \<bullet> j" for j
+      using * d k by (auto simp: a'_def b'_def)
+    ultimately show "(\<Prod>j\<in>Basis. (b' d - a' d) \<bullet> j) = content (cbox a b \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d})"
+      by simp
+  qed simp
+  finally have "((\<lambda>d. content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<longlongrightarrow> 0) (at_right 0)" .
+  from order_tendstoD(2)[OF this \<open>0<e\<close>]
+  obtain d' where "0 < d'" and d': "\<And>y. y > 0 \<Longrightarrow> y < d' \<Longrightarrow> content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> y}) < e"
+    by (subst (asm) eventually_at_right[of _ 1]) auto
   show ?thesis
-    apply (rule that[of 1])
-    apply simp
-    unfolding interval_doublesplit[OF k]
-    apply (rule le_less_trans[OF content_subset ce])
-    apply (auto simp: interval_doublesplit[symmetric] k)
-    done
+    by (rule that[of "d'/2"], insert \<open>0<d'\<close> d'[of "d'/2"], auto)
 next
-  case False
-  define d where "d = e / 3 / setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
-  note False[unfolded content_eq_0 not_ex not_le, rule_format]
-  then have "\<And>x. x \<in> Basis \<Longrightarrow> b\<bullet>x > a\<bullet>x"
-    by (auto simp add:not_le)
-  then have prod0: "0 < setprod (\<lambda>i. b\<bullet>i - a\<bullet>i) (Basis - {k})"
-    by (force simp add: setprod_pos field_simps)
-  then have "d > 0"
-    using assms
-    by (auto simp add: d_def field_simps)
-  then show ?thesis
-  proof (rule that[of d])
-    have *: "Basis = insert k (Basis - {k})"
-      using k by auto
-    have less_e: "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
-    proof -
-      have "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) \<le> 2 * d"
+  assume *: "\<not> (a \<bullet> k \<le> c \<and> c \<le> b \<bullet> k \<and> (\<forall>j\<in>Basis. a \<bullet> j \<le> b \<bullet> j))"
+  then have "(\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j) \<or> (c < a \<bullet> k \<or> b \<bullet> k < c)"
+    by (auto simp: not_le)
+  show thesis
+  proof cases
+    assume "\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j"
+    then have [simp]: "cbox a b = {}"
+      using box_ne_empty(1)[of a b] by auto
+    show ?thesis
+      by (rule that[of 1]) (simp_all add: \<open>0<e\<close>)
+  next
+    assume "\<not> (\<exists>j\<in>Basis. b \<bullet> j < a \<bullet> j)"
+    with * have "c < a \<bullet> k \<or> b \<bullet> k < c"
+      by auto
+    then show thesis
+    proof
+      assume c: "c < a \<bullet> k"
+      moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
+        using k c by (auto simp: cbox_def)
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
+        using k by (auto simp: cbox_def)
+      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
         by auto
-      also have "\<dots> < e / (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i)"
-        unfolding d_def
-        using assms prod0
-        by (auto simp add: field_simps)
-      finally show "(min (b \<bullet> k) (c + d) - max (a \<bullet> k) (c - d)) * (\<Prod>i\<in>Basis - {k}. b \<bullet> i - a \<bullet> i) < e"
-        unfolding pos_less_divide_eq[OF prod0] .
-    qed
-    show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
-    proof (cases "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = {}")
-      case True
-      then show ?thesis
-        using assms by simp
     next
-      case False
-      then have
-          "(\<Prod>i\<in>Basis - {k}. interval_upperbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i -
-                interval_lowerbound (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<bullet> i)
-           = (\<Prod>i\<in>Basis - {k}. b\<bullet>i - a\<bullet>i)"
-        by (simp add: box_eq_empty interval_doublesplit[OF k])
-      then show "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
-        unfolding content_def
-        using assms False
-        apply (subst *)
-        apply (subst setprod.insert)
-        apply (simp_all add: interval_doublesplit[OF k] box_eq_empty not_less less_e)
-        done
-    qed
-  qed
-qed
+      assume c: "b \<bullet> k < c"
+      moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
+        using k c by (auto simp: cbox_def)
+      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
+        using k by (auto simp: cbox_def)
+      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
+        by auto
+    qed
+  qed
+qed
+
 
 lemma negligible_standard_hyperplane[intro]:
   fixes k :: "'a::euclidean_space"
@@ -5695,6 +5467,7 @@
     by auto
   from fundamental_theorem_of_calculus[rule_format, OF \<open>a \<le> b\<close> deriv]
   have "(i has_integral ?sum b - ?sum a) {a .. b}"
+    using atLeastatMost_empty'[simp del]
     by (simp add: i_def g_def Dg_def)
   also
   have one: "(- 1) ^ p' * (- 1) ^ p' = (1::real)"
@@ -6036,7 +5809,7 @@
         done
       show ?thesis
         using False
-        apply (simp add: abs_eq_content del: content_real_if)
+        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
         using yx False d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
@@ -6054,7 +5827,7 @@
         done
       have "norm (integral {a..x} f - integral {a..y} f - (x - y) *\<^sub>R f x) \<le> e * \<bar>y - x\<bar>"
         using True
-        apply (simp add: abs_eq_content del: content_real_if)
+        apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
         apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
         using yx True d x y \<open>e>0\<close> apply (auto simp add: Idiff fux_int)
         done
@@ -6274,6 +6047,62 @@
 
 subsection \<open>Special case of a basic affine transformation.\<close>
 
+lemma AE_lborel_inner_neq:
+  assumes k: "k \<in> Basis"
+  shows "AE x in lborel. x \<bullet> k \<noteq> c"
+proof -
+  interpret finite_product_sigma_finite "\<lambda>_. lborel" Basis
+    proof qed simp
+
+  have "emeasure lborel {x\<in>space lborel. x \<bullet> k = c} = emeasure (\<Pi>\<^sub>M j::'a\<in>Basis. lborel) (\<Pi>\<^sub>E j\<in>Basis. if j = k then {c} else UNIV)"
+    using k
+    by (auto simp add: lborel_eq[where 'a='a] emeasure_distr intro!: arg_cong2[where f=emeasure])
+       (auto simp: space_PiM PiE_iff extensional_def split: if_split_asm)
+  also have "\<dots> = (\<Prod>j\<in>Basis. emeasure lborel (if j = k then {c} else UNIV))"
+    by (intro measure_times) auto
+  also have "\<dots> = 0"
+    by (intro setprod_zero bexI[OF _ k]) auto
+  finally show ?thesis
+    by (subst AE_iff_measurable[OF _ refl]) auto
+qed
+
+lemma content_image_stretch_interval:
+  fixes m :: "'a::euclidean_space \<Rightarrow> real"
+  defines "s f x \<equiv> (\<Sum>k::'a\<in>Basis. (f k * (x\<bullet>k)) *\<^sub>R k)"
+  shows "content (s m ` cbox a b) = \<bar>\<Prod>k\<in>Basis. m k\<bar> * content (cbox a b)"
+proof cases
+  have s[measurable]: "s f \<in> borel \<rightarrow>\<^sub>M borel" for f
+    by (auto simp: s_def[abs_def])
+  assume m: "\<forall>k\<in>Basis. m k \<noteq> 0"
+  then have s_comp_s: "s (\<lambda>k. 1 / m k) \<circ> s m = id" "s m \<circ> s (\<lambda>k. 1 / m k) = id"
+    by (auto simp: s_def[abs_def] fun_eq_iff euclidean_representation)
+  then have "inv (s (\<lambda>k. 1 / m k)) = s m" "bij (s (\<lambda>k. 1 / m k))"
+    by (auto intro: inv_unique_comp o_bij)
+  then have eq: "s m ` cbox a b = s (\<lambda>k. 1 / m k) -` cbox a b"
+    using bij_vimage_eq_inv_image[OF \<open>bij (s (\<lambda>k. 1 / m k))\<close>, of "cbox a b"] by auto
+  show ?thesis
+    using m unfolding eq measure_def
+    by (subst lborel_affine_euclidean[where c=m and t=0])
+       (simp_all add: emeasure_density measurable_sets_borel[OF s] abs_setprod nn_integral_cmult
+                      s_def[symmetric] emeasure_distr vimage_comp s_comp_s enn2real_mult setprod_nonneg)
+next
+  assume "\<not> (\<forall>k\<in>Basis. m k \<noteq> 0)"
+  then obtain k where k: "k \<in> Basis" "m k = 0" by auto
+  then have [simp]: "(\<Prod>k\<in>Basis. m k) = 0"
+    by (intro setprod_zero) auto
+  have "emeasure lborel {x\<in>space lborel. x \<in> s m ` cbox a b} = 0"
+  proof (rule emeasure_eq_0_AE)
+    show "AE x in lborel. x \<notin> s m ` cbox a b"
+      using AE_lborel_inner_neq[OF \<open>k\<in>Basis\<close>]
+    proof eventually_elim
+      show "x \<bullet> k \<noteq> 0 \<Longrightarrow> x \<notin> s m ` cbox a b " for x
+        using k by (auto simp: s_def[abs_def] cbox_def)
+    qed
+  qed
+  then show ?thesis
+    by (simp add: measure_def)
+qed
+
 lemma interval_image_affinity_interval:
   "\<exists>u v. (\<lambda>x. m *\<^sub>R (x::'a::euclidean_space) + c) ` cbox a b = cbox u v"
   unfolding image_affinity_cbox
@@ -6344,43 +6173,6 @@
 
 subsection \<open>Special case of stretching coordinate axes separately.\<close>
 
-lemma content_image_stretch_interval:
-  "content ((\<lambda>x::'a::euclidean_space. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)::'a) ` cbox a b) =
-    \<bar>setprod m Basis\<bar> * content (cbox a b)"
-proof (cases "cbox a b = {}")
-  case True
-  then show ?thesis
-    unfolding content_def image_is_empty image_stretch_interval if_P[OF True] by auto
-next
-  case False
-  then have "(\<lambda>x. (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b \<noteq> {}"
-    by auto
-  then show ?thesis
-    using False
-    unfolding content_def image_stretch_interval
-    apply -
-    unfolding interval_bounds' if_not_P
-    unfolding abs_setprod setprod.distrib[symmetric]
-    apply (rule setprod.cong)
-    apply (rule refl)
-    unfolding lessThan_iff
-    apply (simp only: inner_setsum_left_Basis)
-  proof -
-    fix i :: 'a
-    assume i: "i \<in> Basis"
-    have "(m i < 0 \<or> m i > 0) \<or> m i = 0"
-      by auto
-    then show "max (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) - min (m i * (a \<bullet> i)) (m i * (b \<bullet> i)) =
-      \<bar>m i\<bar> * (b \<bullet> i - a \<bullet> i)"
-      apply -
-      apply (erule disjE)+
-      unfolding min_def max_def
-      using False[unfolded box_ne_empty,rule_format,of i] i
-      apply (auto simp add:field_simps not_le mult_le_cancel_left_neg mult_le_cancel_left_pos)
-      done
-  qed
-qed
-
 lemma has_integral_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "(f has_integral i) (cbox a b)"
@@ -9324,7 +9116,7 @@
     proof (rule, goal_cases)
       case prems: (1 x)
       have "e / (4 * content (cbox a b)) > 0"
-        using \<open>e>0\<close> False content_pos_le[of a b] by auto
+        using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
       from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
       guess n .. note n=this
       then show ?case
@@ -10314,7 +10106,7 @@
             done
           also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
             apply (rule setsum.mono_neutral_left)
-            apply (subst simple_image)
+            apply (subst Setcompr_eq_image)
             apply (rule finite_imageI)+
             apply fact
             unfolding d'_def uv
@@ -10330,7 +10122,7 @@
               using l by auto
           qed
           also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule setsum.reindex_nontrivial [unfolded o_def])
             apply (rule finite_imageI)
             apply (rule p')
@@ -10518,7 +10310,7 @@
             apply auto
             done
           also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
             apply (rule d')
           proof goal_cases
@@ -10539,7 +10331,7 @@
           qed
           also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
             apply (rule setsum.mono_neutral_right)
-            unfolding simple_image
+            unfolding Setcompr_eq_image
             apply (rule finite_imageI)
             apply (rule d')
             apply blast
@@ -11394,7 +11186,7 @@
       also have "\<dots> < e' * norm (x - x0)"
         using \<open>e' > 0\<close> content_pos_le[of a b]
         by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
-          (auto simp: divide_simps e_def)
+           (auto simp: divide_simps e_def simp del: measure_nonneg)
       finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
       then show ?case
         by (auto simp: divide_simps)
@@ -11509,7 +11301,7 @@
       with \<open>e > 0\<close> have "e' > 0" by simp
       then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
         using u content_nonzero content_pos_le[of a b]
-        by (auto simp: uniform_limit_iff dist_norm)
+        by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
       then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
       proof eventually_elim
         case (elim n)
@@ -11568,7 +11360,7 @@
       fix k :: nat
       show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
         apply (rule integral_norm_bound_integral)
-        unfolding simple_image
+        unfolding Setcompr_eq_image
         apply (rule absolutely_integrable_onD)
         apply (rule absolutely_integrable_inf_real)
         prefer 5
@@ -11585,7 +11377,7 @@
     qed
     fix k :: nat
     show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image
+      unfolding Setcompr_eq_image
       apply (rule absolutely_integrable_onD)
       apply (rule absolutely_integrable_inf_real)
       prefer 3
@@ -11638,7 +11430,7 @@
     proof safe
       fix k :: nat
       show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
-        apply (rule integral_norm_bound_integral) unfolding simple_image
+        apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
         apply (rule absolutely_integrable_onD)
         apply(rule absolutely_integrable_sup_real)
         prefer 5 unfolding real_norm_def
@@ -11656,7 +11448,7 @@
     qed
     fix k :: nat
     show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding simple_image
+      unfolding Setcompr_eq_image
       apply (rule absolutely_integrable_onD)
       apply (rule absolutely_integrable_sup_real)
       prefer 3
@@ -12541,11 +12333,11 @@
   define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
   define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
 
-  have has_integral_f: "(f n has_integral (F n - F a)) {a..}" 
+  have has_integral_f: "(f n has_integral (F n - F a)) {a..}"
     if n: "n \<ge> a" for n :: nat
   proof -
     from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
-      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros 
+      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
             simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
     hence "(f n has_integral (F n - F a)) {a..n}"
       by (rule has_integral_eq [rotated]) (simp add: f_def)
@@ -12559,12 +12351,12 @@
   next
     case False
     have "(f n has_integral 0) {a}" by (rule has_integral_refl)
-    hence "(f n has_integral 0) {a..}" 
+    hence "(f n has_integral 0) {a..}"
       by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
     with False show ?thesis by (simp add: integral_unique)
   qed
-  
-  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and> 
+
+  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and>
            (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
   proof (intro monotone_convergence_increasing allI ballI)
     fix n :: nat
@@ -12582,7 +12374,7 @@
     from filterlim_real_sequentially
       have "eventually (\<lambda>n. real n \<ge> x) at_top"
       by (simp add: filterlim_at_top)
-    with x have "eventually (\<lambda>n. f n x = x powr e) at_top" 
+    with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
       by (auto elim!: eventually_mono simp: f_def)
     thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
   next
@@ -12603,11 +12395,11 @@
   hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
     by eventually_elim (simp add: integral_f)
   moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
-    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr] 
+    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
           filterlim_ident filterlim_real_sequentially | simp)+)
   hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
   ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
-  from conjunct2[OF *] and this 
+  from conjunct2[OF *] and this
     have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
   with conjunct1[OF *] show ?thesis
     by (simp add: has_integral_integral F_def)
@@ -12620,7 +12412,7 @@
 proof -
   from assms have "real_of_int (-int n) < -1" by simp
   note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
-  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 
+  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) =
                  1 / (real (n - 1) * a powr (real (n - 1)))" using assms
     by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
   also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
@@ -12630,4 +12422,33 @@
        (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
 qed
 
+subsubsection \<open>Adaption to ordered Euclidean spaces and the Cartesian Euclidean space\<close>
+
+lemma integral_component_eq_cart[simp]:
+  fixes f :: "'n::euclidean_space \<Rightarrow> real^'m"
+  assumes "f integrable_on s"
+  shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
+  using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] .
+
+lemma content_closed_interval:
+  fixes a :: "'a::ordered_euclidean_space"
+  assumes "a \<le> b"
+  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
+  using content_cbox[of a b] assms
+  by (simp add: cbox_interval eucl_le[where 'a='a])
+
+lemma integrable_const_ivl[intro]:
+  fixes a::"'a::ordered_euclidean_space"
+  shows "(\<lambda>x. c) integrable_on {a .. b}"
+  unfolding cbox_interval[symmetric]
+  by (rule integrable_const)
+
+lemma integrable_on_subinterval:
+  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
+  assumes "f integrable_on s"
+    and "{a .. b} \<subseteq> s"
+  shows "f integrable_on {a .. b}"
+  using integrable_on_subcbox[of f s a b] assms
+  by (simp add: cbox_interval)
+
 end
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -311,7 +311,7 @@
                    ereal_uminus_le_reorder ereal_uminus_less_reorder not_less
                    uminus_ereal.simps[symmetric]
              simp del: uminus_ereal.simps
-             intro!: integral_cong
+             intro!: Bochner_Integration.integral_cong
              split: split_indicator)
 qed
 
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -469,6 +469,10 @@
   "emeasure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
   using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
 
+lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
+  using emeasure_lborel_cbox[of x x] nonempty_Basis
+  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
+
 lemma
   fixes l u :: real
   assumes [simp]: "l \<le> u"
@@ -484,6 +488,17 @@
     and measure_lborel_cbox[simp]: "measure lborel (cbox l u) = (\<Prod>b\<in>Basis. (u - l) \<bullet> b)"
   by (simp_all add: measure_def inner_diff_left setprod_nonneg)
 
+lemma measure_lborel_cbox_eq:
+  "measure lborel (cbox l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+  using box_eq_empty(2)[THEN iffD2, of u l] by (auto simp: not_le)
+
+lemma measure_lborel_box_eq:
+  "measure lborel (box l u) = (if \<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b then \<Prod>b\<in>Basis. (u - l) \<bullet> b else 0)"
+  using box_eq_empty(1)[THEN iffD2, of u l] by (auto simp: not_le dest!: less_imp_le) force
+
+lemma measure_lborel_singleton[simp]: "measure lborel {x} = 0"
+  by (simp add: measure_def)
+
 lemma sigma_finite_lborel: "sigma_finite_measure lborel"
 proof
   show "\<exists>A::'a set set. countable A \<and> A \<subseteq> sets lborel \<and> \<Union>A = space lborel \<and> (\<forall>a\<in>A. emeasure lborel a \<noteq> \<infinity>)"
@@ -516,10 +531,6 @@
     done
 qed
 
-lemma emeasure_lborel_singleton[simp]: "emeasure lborel {x} = 0"
-  using emeasure_lborel_cbox[of x x] nonempty_Basis
-  by (auto simp del: emeasure_lborel_cbox nonempty_Basis simp add: cbox_sing setprod_constant)
-
 lemma emeasure_lborel_countable:
   fixes A :: "'a::euclidean_space set"
   assumes "countable A"
@@ -572,46 +583,38 @@
 
   { fix i show "emeasure lborel (?A i) \<noteq> \<infinity>" by auto }
   { fix X assume "X \<in> ?E" then show "emeasure lborel X = emeasure M X"
-      apply (auto simp: emeasure_eq emeasure_lborel_box_eq )
+      apply (auto simp: emeasure_eq emeasure_lborel_box_eq)
       apply (subst box_eq_empty(1)[THEN iffD2])
       apply (auto intro: less_imp_le simp: not_le)
       done }
 qed
 
-lemma lborel_affine:
-  fixes t :: "'a::euclidean_space" assumes "c \<noteq> 0"
-  shows "lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))" (is "_ = ?D")
+lemma lborel_affine_euclidean:
+  fixes c :: "'a::euclidean_space \<Rightarrow> real" and t
+  defines "T x \<equiv> t + (\<Sum>j\<in>Basis. (c j * (x \<bullet> j)) *\<^sub>R j)"
+  assumes c: "\<And>j. j \<in> Basis \<Longrightarrow> c j \<noteq> 0"
+  shows "lborel = density (distr lborel borel T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" (is "_ = ?D")
 proof (rule lborel_eqI)
   let ?B = "Basis :: 'a set"
   fix l u assume le: "\<And>b. b \<in> ?B \<Longrightarrow> l \<bullet> b \<le> u \<bullet> b"
-  show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
-  proof cases
-    assume "0 < c"
-    then have "(\<lambda>x. t + c *\<^sub>R x) -` box l u = box ((l - t) /\<^sub>R c) ((u - t) /\<^sub>R c)"
-      by (auto simp: field_simps box_def inner_simps)
-    with \<open>0 < c\<close> show ?thesis
-      using le
-      by (auto simp: field_simps inner_simps setprod_dividef setprod_constant setprod_nonneg
-                     ennreal_mult[symmetric] emeasure_density nn_integral_distr emeasure_distr
-                     nn_integral_cmult emeasure_lborel_box_eq borel_measurable_indicator')
-  next
-    assume "\<not> 0 < c" with \<open>c \<noteq> 0\<close> have "c < 0" by auto
-    then have "box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c) = (\<lambda>x. t + c *\<^sub>R x) -` box l u"
-      by (auto simp: field_simps box_def inner_simps)
-    then have *: "\<And>x. indicator (box l u) (t + c *\<^sub>R x) = (indicator (box ((u - t) /\<^sub>R c) ((l - t) /\<^sub>R c)) x :: ennreal)"
-      by (auto split: split_indicator)
-    have **: "(\<Prod>x\<in>Basis. (l \<bullet> x - u \<bullet> x) / c) = (\<Prod>x\<in>Basis. u \<bullet> x - l \<bullet> x) / (-c) ^ card (Basis::'a set)"
-      using \<open>c < 0\<close>
-      by (auto simp add: field_simps setprod_dividef[symmetric] setprod_constant[symmetric]
-               intro!: setprod.cong)
-    show ?thesis
-      using \<open>c < 0\<close> le
-      by (auto simp: * ** field_simps emeasure_density nn_integral_distr nn_integral_cmult
-                     emeasure_lborel_box_eq inner_simps setprod_nonneg ennreal_mult[symmetric]
-                     borel_measurable_indicator')
-  qed
+  have [measurable]: "T \<in> borel \<rightarrow>\<^sub>M borel"
+    by (simp add: T_def[abs_def])
+  have eq: "T -` box l u = box
+    (\<Sum>j\<in>Basis. (((if 0 < c j then l - t else u - t) \<bullet> j) / c j) *\<^sub>R j)
+    (\<Sum>j\<in>Basis. (((if 0 < c j then u - t else l - t) \<bullet> j) / c j) *\<^sub>R j)"
+    using c by (auto simp: box_def T_def field_simps inner_simps divide_less_eq)
+  with le c show "emeasure ?D (box l u) = (\<Prod>b\<in>?B. (u - l) \<bullet> b)"
+    by (auto simp: emeasure_density emeasure_distr nn_integral_multc emeasure_lborel_box_eq inner_simps
+                   field_simps divide_simps ennreal_mult'[symmetric] setprod_nonneg setprod.distrib[symmetric]
+             intro!: setprod.cong)
 qed simp
 
+lemma lborel_affine:
+  fixes t :: "'a::euclidean_space"
+  shows "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c *\<^sub>R x)) (\<lambda>_. \<bar>c\<bar>^DIM('a))"
+  using lborel_affine_euclidean[where c="\<lambda>_::'a. c" and t=t]
+  unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation setprod_constant by simp
+
 lemma lborel_real_affine:
   "c \<noteq> 0 \<Longrightarrow> lborel = density (distr lborel borel (\<lambda>x. t + c * x)) (\<lambda>_. ennreal (abs c))"
   using lborel_affine[of c t] by simp
@@ -726,378 +729,6 @@
 lemma lborelD_Collect[measurable (raw)]: "{x\<in>space borel. P x} \<in> sets borel \<Longrightarrow> {x\<in>space lborel. P x} \<in> sets lborel" by simp
 lemma lborelD[measurable (raw)]: "A \<in> sets borel \<Longrightarrow> A \<in> sets lborel" by simp
 
-subsection \<open>Equivalence Lebesgue integral on @{const lborel} and HK-integral\<close>
-
-lemma has_integral_measure_lborel:
-  fixes A :: "'a::euclidean_space set"
-  assumes A[measurable]: "A \<in> sets borel" and finite: "emeasure lborel A < \<infinity>"
-  shows "((\<lambda>x. 1) has_integral measure lborel A) A"
-proof -
-  { fix l u :: 'a
-    have "((\<lambda>x. 1) has_integral measure lborel (box l u)) (box l u)"
-    proof cases
-      assume "\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b"
-      then show ?thesis
-        apply simp
-        apply (subst has_integral_restrict[symmetric, OF box_subset_cbox])
-        apply (subst has_integral_spike_interior_eq[where g="\<lambda>_. 1"])
-        using has_integral_const[of "1::real" l u]
-        apply (simp_all add: inner_diff_left[symmetric] content_cbox_cases)
-        done
-    next
-      assume "\<not> (\<forall>b\<in>Basis. l \<bullet> b \<le> u \<bullet> b)"
-      then have "box l u = {}"
-        unfolding box_eq_empty by (auto simp: not_le intro: less_imp_le)
-      then show ?thesis
-        by simp
-    qed }
-  note has_integral_box = this
-
-  { fix a b :: 'a let ?M = "\<lambda>A. measure lborel (A \<inter> box a b)"
-    have "Int_stable  (range (\<lambda>(a, b). box a b))"
-      by (auto simp: Int_stable_def box_Int_box)
-    moreover have "(range (\<lambda>(a, b). box a b)) \<subseteq> Pow UNIV"
-      by auto
-    moreover have "A \<in> sigma_sets UNIV (range (\<lambda>(a, b). box a b))"
-       using A unfolding borel_eq_box by simp
-    ultimately have "((\<lambda>x. 1) has_integral ?M A) (A \<inter> box a b)"
-    proof (induction rule: sigma_sets_induct_disjoint)
-      case (basic A) then show ?case
-        by (auto simp: box_Int_box has_integral_box)
-    next
-      case empty then show ?case
-        by simp
-    next
-      case (compl A)
-      then have [measurable]: "A \<in> sets borel"
-        by (simp add: borel_eq_box)
-
-      have "((\<lambda>x. 1) has_integral ?M (box a b)) (box a b)"
-        by (simp add: has_integral_box)
-      moreover have "((\<lambda>x. if x \<in> A \<inter> box a b then 1 else 0) has_integral ?M A) (box a b)"
-        by (subst has_integral_restrict) (auto intro: compl)
-      ultimately have "((\<lambda>x. 1 - (if x \<in> A \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
-        by (rule has_integral_sub)
-      then have "((\<lambda>x. (if x \<in> (UNIV - A) \<inter> box a b then 1 else 0)) has_integral ?M (box a b) - ?M A) (box a b)"
-        by (rule has_integral_cong[THEN iffD1, rotated 1]) auto
-      then have "((\<lambda>x. 1) has_integral ?M (box a b) - ?M A) ((UNIV - A) \<inter> box a b)"
-        by (subst (asm) has_integral_restrict) auto
-      also have "?M (box a b) - ?M A = ?M (UNIV - A)"
-        by (subst measure_Diff[symmetric]) (auto simp: emeasure_lborel_box_eq Diff_Int_distrib2)
-      finally show ?case .
-    next
-      case (union F)
-      then have [measurable]: "\<And>i. F i \<in> sets borel"
-        by (simp add: borel_eq_box subset_eq)
-      have "((\<lambda>x. if x \<in> UNION UNIV F \<inter> box a b then 1 else 0) has_integral ?M (\<Union>i. F i)) (box a b)"
-      proof (rule has_integral_monotone_convergence_increasing)
-        let ?f = "\<lambda>k x. \<Sum>i<k. if x \<in> F i \<inter> box a b then 1 else 0 :: real"
-        show "\<And>k. (?f k has_integral (\<Sum>i<k. ?M (F i))) (box a b)"
-          using union.IH by (auto intro!: has_integral_setsum simp del: Int_iff)
-        show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
-          by (intro setsum_mono2) auto
-        from union(1) have *: "\<And>x i j. x \<in> F i \<Longrightarrow> x \<in> F j \<longleftrightarrow> j = i"
-          by (auto simp add: disjoint_family_on_def)
-        show "\<And>x. (\<lambda>k. ?f k x) \<longlonglongrightarrow> (if x \<in> UNION UNIV F \<inter> box a b then 1 else 0)"
-          apply (auto simp: * setsum.If_cases Iio_Int_singleton)
-          apply (rule_tac k="Suc xa" in LIMSEQ_offset)
-          apply simp
-          done
-        have *: "emeasure lborel ((\<Union>x. F x) \<inter> box a b) \<le> emeasure lborel (box a b)"
-          by (intro emeasure_mono) auto
-
-        with union(1) show "(\<lambda>k. \<Sum>i<k. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
-          unfolding sums_def[symmetric] UN_extend_simps
-          by (intro measure_UNION) (auto simp: disjoint_family_on_def emeasure_lborel_box_eq top_unique)
-      qed
-      then show ?case
-        by (subst (asm) has_integral_restrict) auto
-    qed }
-  note * = this
-
-  show ?thesis
-  proof (rule has_integral_monotone_convergence_increasing)
-    let ?B = "\<lambda>n::nat. box (- real n *\<^sub>R One) (real n *\<^sub>R One) :: 'a set"
-    let ?f = "\<lambda>n::nat. \<lambda>x. if x \<in> A \<inter> ?B n then 1 else 0 :: real"
-    let ?M = "\<lambda>n. measure lborel (A \<inter> ?B n)"
-
-    show "\<And>n::nat. (?f n has_integral ?M n) A"
-      using * by (subst has_integral_restrict) simp_all
-    show "\<And>k x. ?f k x \<le> ?f (Suc k) x"
-      by (auto simp: box_def)
-    { fix x assume "x \<in> A"
-      moreover have "(\<lambda>k. indicator (A \<inter> ?B k) x :: real) \<longlonglongrightarrow> indicator (\<Union>k::nat. A \<inter> ?B k) x"
-        by (intro LIMSEQ_indicator_incseq) (auto simp: incseq_def box_def)
-      ultimately show "(\<lambda>k. if x \<in> A \<inter> ?B k then 1 else 0::real) \<longlonglongrightarrow> 1"
-        by (simp add: indicator_def UN_box_eq_UNIV) }
-
-    have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> emeasure lborel (\<Union>n::nat. A \<inter> ?B n)"
-      by (intro Lim_emeasure_incseq) (auto simp: incseq_def box_def)
-    also have "(\<lambda>n. emeasure lborel (A \<inter> ?B n)) = (\<lambda>n. measure lborel (A \<inter> ?B n))"
-    proof (intro ext emeasure_eq_ennreal_measure)
-      fix n have "emeasure lborel (A \<inter> ?B n) \<le> emeasure lborel (?B n)"
-        by (intro emeasure_mono) auto
-      then show "emeasure lborel (A \<inter> ?B n) \<noteq> top"
-        by (auto simp: top_unique)
-    qed
-    finally show "(\<lambda>n. measure lborel (A \<inter> ?B n)) \<longlonglongrightarrow> measure lborel A"
-      using emeasure_eq_ennreal_measure[of lborel A] finite
-      by (simp add: UN_box_eq_UNIV less_top)
-  qed
-qed
-
-lemma nn_integral_has_integral:
-  fixes f::"'a::euclidean_space \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
-  shows "(f has_integral r) UNIV"
-using f proof (induct f arbitrary: r rule: borel_measurable_induct_real)
-  case (set A)
-  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
-    by (intro has_integral_measure_lborel) (auto simp: ennreal_indicator)
-  with set show ?case
-    by (simp add: ennreal_indicator measure_def) (simp add: indicator_def)
-next
-  case (mult g c)
-  then have "ennreal c * (\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal r"
-    by (subst nn_integral_cmult[symmetric]) (auto simp: ennreal_mult)
-  with \<open>0 \<le> r\<close> \<open>0 \<le> c\<close>
-  obtain r' where "(c = 0 \<and> r = 0) \<or> (0 \<le> r' \<and> (\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel) = ennreal r' \<and> r = c * r')"
-    by (cases "\<integral>\<^sup>+ x. ennreal (g x) \<partial>lborel" rule: ennreal_cases)
-       (auto split: if_split_asm simp: ennreal_mult_top ennreal_mult[symmetric])
-  with mult show ?case
-    by (auto intro!: has_integral_cmult_real)
-next
-  case (add g h)
-  then have "(\<integral>\<^sup>+ x. h x + g x \<partial>lborel) = (\<integral>\<^sup>+ x. h x \<partial>lborel) + (\<integral>\<^sup>+ x. g x \<partial>lborel)"
-    by (simp add: nn_integral_add)
-  with add obtain a b where "0 \<le> a" "0 \<le> b" "(\<integral>\<^sup>+ x. h x \<partial>lborel) = ennreal a" "(\<integral>\<^sup>+ x. g x \<partial>lborel) = ennreal b" "r = a + b"
-    by (cases "\<integral>\<^sup>+ x. h x \<partial>lborel" "\<integral>\<^sup>+ x. g x \<partial>lborel" rule: ennreal2_cases)
-       (auto simp: add_top nn_integral_add top_add ennreal_plus[symmetric] simp del: ennreal_plus)
-  with add show ?case
-    by (auto intro!: has_integral_add)
-next
-  case (seq U)
-  note seq(1)[measurable] and f[measurable]
-
-  { fix i x
-    have "U i x \<le> f x"
-      using seq(5)
-      apply (rule LIMSEQ_le_const)
-      using seq(4)
-      apply (auto intro!: exI[of _ i] simp: incseq_def le_fun_def)
-      done }
-  note U_le_f = this
-
-  { fix i
-    have "(\<integral>\<^sup>+x. U i x \<partial>lborel) \<le> (\<integral>\<^sup>+x. f x \<partial>lborel)"
-      using seq(2) f(2) U_le_f by (intro nn_integral_mono) simp
-    then obtain p where "(\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p" "p \<le> r" "0 \<le> p"
-      using seq(6) \<open>0\<le>r\<close> by (cases "\<integral>\<^sup>+x. U i x \<partial>lborel" rule: ennreal_cases) (auto simp: top_unique)
-    moreover note seq
-    ultimately have "\<exists>p. (\<integral>\<^sup>+x. U i x \<partial>lborel) = ennreal p \<and> 0 \<le> p \<and> p \<le> r \<and> (U i has_integral p) UNIV"
-      by auto }
-  then obtain p where p: "\<And>i. (\<integral>\<^sup>+x. ennreal (U i x) \<partial>lborel) = ennreal (p i)"
-    and bnd: "\<And>i. p i \<le> r" "\<And>i. 0 \<le> p i"
-    and U_int: "\<And>i.(U i has_integral (p i)) UNIV" by metis
-
-  have int_eq: "\<And>i. integral UNIV (U i) = p i" using U_int by (rule integral_unique)
-
-  have *: "f integrable_on UNIV \<and> (\<lambda>k. integral UNIV (U k)) \<longlonglongrightarrow> integral UNIV f"
-  proof (rule monotone_convergence_increasing)
-    show "\<forall>k. U k integrable_on UNIV" using U_int by auto
-    show "\<forall>k. \<forall>x\<in>UNIV. U k x \<le> U (Suc k) x" using \<open>incseq U\<close> by (auto simp: incseq_def le_fun_def)
-    then show "bounded {integral UNIV (U k) |k. True}"
-      using bnd int_eq by (auto simp: bounded_real intro!: exI[of _ r])
-    show "\<forall>x\<in>UNIV. (\<lambda>k. U k x) \<longlonglongrightarrow> f x"
-      using seq by auto
-  qed
-  moreover have "(\<lambda>i. (\<integral>\<^sup>+x. U i x \<partial>lborel)) \<longlonglongrightarrow> (\<integral>\<^sup>+x. f x \<partial>lborel)"
-    using seq f(2) U_le_f by (intro nn_integral_dominated_convergence[where w=f]) auto
-  ultimately have "integral UNIV f = r"
-    by (auto simp add: bnd int_eq p seq intro: LIMSEQ_unique)
-  with * show ?case
-    by (simp add: has_integral_integral)
-qed
-
-lemma nn_integral_lborel_eq_integral:
-  fixes f::"'a::euclidean_space \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
-  shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = integral UNIV f"
-proof -
-  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
-    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
-  then show ?thesis
-    using nn_integral_has_integral[OF f(1,2) r] by (simp add: integral_unique)
-qed
-
-lemma nn_integral_integrable_on:
-  fixes f::"'a::euclidean_space \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable borel" "\<And>x. 0 \<le> f x" "(\<integral>\<^sup>+x. f x \<partial>lborel) < \<infinity>"
-  shows "f integrable_on UNIV"
-proof -
-  from f(3) obtain r where r: "(\<integral>\<^sup>+x. f x \<partial>lborel) = ennreal r" "0 \<le> r"
-    by (cases "\<integral>\<^sup>+x. f x \<partial>lborel" rule: ennreal_cases) auto
-  then show ?thesis
-    by (intro has_integral_integrable[where i=r] nn_integral_has_integral[where r=r] f)
-qed
-
-lemma nn_integral_has_integral_lborel:
-  fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes f_borel: "f \<in> borel_measurable borel" and nonneg: "\<And>x. 0 \<le> f x"
-  assumes I: "(f has_integral I) UNIV"
-  shows "integral\<^sup>N lborel f = I"
-proof -
-  from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
-  from borel_measurable_implies_simple_function_sequence'[OF this] guess F . note F = this
-  let ?B = "\<lambda>i::nat. box (- (real i *\<^sub>R One)) (real i *\<^sub>R One) :: 'a set"
-
-  note F(1)[THEN borel_measurable_simple_function, measurable]
-
-  have "0 \<le> I"
-    using I by (rule has_integral_nonneg) (simp add: nonneg)
-
-  have F_le_f: "enn2real (F i x) \<le> f x" for i x
-    using F(3,4)[where x=x] nonneg SUP_upper[of i UNIV "\<lambda>i. F i x"]
-    by (cases "F i x" rule: ennreal_cases) auto
-  let ?F = "\<lambda>i x. F i x * indicator (?B i) x"
-  have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (SUP i. integral\<^sup>N lborel (\<lambda>x. ?F i x))"
-  proof (subst nn_integral_monotone_convergence_SUP[symmetric])
-    { fix x
-      obtain j where j: "x \<in> ?B j"
-        using UN_box_eq_UNIV by auto
-
-      have "ennreal (f x) = (SUP i. F i x)"
-        using F(4)[of x] nonneg[of x] by (simp add: max_def)
-      also have "\<dots> = (SUP i. ?F i x)"
-      proof (rule SUP_eq)
-        fix i show "\<exists>j\<in>UNIV. F i x \<le> ?F j x"
-          using j F(2)
-          by (intro bexI[of _ "max i j"])
-             (auto split: split_max split_indicator simp: incseq_def le_fun_def box_def)
-      qed (auto intro!: F split: split_indicator)
-      finally have "ennreal (f x) =  (SUP i. ?F i x)" . }
-    then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) = (\<integral>\<^sup>+ x. (SUP i. ?F i x) \<partial>lborel)"
-      by simp
-  qed (insert F, auto simp: incseq_def le_fun_def box_def split: split_indicator)
-  also have "\<dots> \<le> ennreal I"
-  proof (rule SUP_least)
-    fix i :: nat
-    have finite_F: "(\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel) < \<infinity>"
-    proof (rule nn_integral_bound_simple_function)
-      have "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} \<le>
-        emeasure lborel (?B i)"
-        by (intro emeasure_mono)  (auto split: split_indicator)
-      then show "emeasure lborel {x \<in> space lborel. ennreal (enn2real (F i x) * indicator (?B i) x) \<noteq> 0} < \<infinity>"
-        by (auto simp: less_top[symmetric] top_unique)
-    qed (auto split: split_indicator
-              intro!: F simple_function_compose1[where g="enn2real"] simple_function_ennreal)
-
-    have int_F: "(\<lambda>x. enn2real (F i x) * indicator (?B i) x) integrable_on UNIV"
-      using F(4) finite_F
-      by (intro nn_integral_integrable_on) (auto split: split_indicator simp: enn2real_nonneg)
-
-    have "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) =
-      (\<integral>\<^sup>+ x. ennreal (enn2real (F i x) * indicator (?B i) x) \<partial>lborel)"
-      using F(3,4)
-      by (intro nn_integral_cong) (auto simp: image_iff eq_commute split: split_indicator)
-    also have "\<dots> = ennreal (integral UNIV (\<lambda>x. enn2real (F i x) * indicator (?B i) x))"
-      using F
-      by (intro nn_integral_lborel_eq_integral[OF _ _ finite_F])
-         (auto split: split_indicator intro: enn2real_nonneg)
-    also have "\<dots> \<le> ennreal I"
-      by (auto intro!: has_integral_le[OF integrable_integral[OF int_F] I] nonneg F_le_f
-               simp: \<open>0 \<le> I\<close> split: split_indicator )
-    finally show "(\<integral>\<^sup>+ x. F i x * indicator (?B i) x \<partial>lborel) \<le> ennreal I" .
-  qed
-  finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>lborel) < \<infinity>"
-    by (auto simp: less_top[symmetric] top_unique)
-  from nn_integral_lborel_eq_integral[OF assms(1,2) this] I show ?thesis
-    by (simp add: integral_unique)
-qed
-
-lemma has_integral_iff_emeasure_lborel:
-  fixes A :: "'a::euclidean_space set"
-  assumes A[measurable]: "A \<in> sets borel" and [simp]: "0 \<le> r"
-  shows "((\<lambda>x. 1) has_integral r) A \<longleftrightarrow> emeasure lborel A = ennreal r"
-proof (cases "emeasure lborel A = \<infinity>")
-  case emeasure_A: True
-  have "\<not> (\<lambda>x. 1::real) integrable_on A"
-  proof
-    assume int: "(\<lambda>x. 1::real) integrable_on A"
-    then have "(indicator A::'a \<Rightarrow> real) integrable_on UNIV"
-      unfolding indicator_def[abs_def] integrable_restrict_univ .
-    then obtain r where "((indicator A::'a\<Rightarrow>real) has_integral r) UNIV"
-      by auto
-    from nn_integral_has_integral_lborel[OF _ _ this] emeasure_A show False
-      by (simp add: ennreal_indicator)
-  qed
-  with emeasure_A show ?thesis
-    by auto
-next
-  case False
-  then have "((\<lambda>x. 1) has_integral measure lborel A) A"
-    by (simp add: has_integral_measure_lborel less_top)
-  with False show ?thesis
-    by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
-qed
-
-lemma has_integral_integral_real:
-  fixes f::"'a::euclidean_space \<Rightarrow> real"
-  assumes f: "integrable lborel f"
-  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
-using f proof induct
-  case (base A c) then show ?case
-    by (auto intro!: has_integral_mult_left simp: )
-       (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
-next
-  case (add f g) then show ?case
-    by (auto intro!: has_integral_add)
-next
-  case (lim f s)
-  show ?case
-  proof (rule has_integral_dominated_convergence)
-    show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
-    show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
-      using \<open>integrable lborel f\<close>
-      by (intro nn_integral_integrable_on)
-         (auto simp: integrable_iff_bounded abs_mult  nn_integral_cmult ennreal_mult ennreal_mult_less_top)
-    show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
-      using lim by (auto simp add: abs_mult)
-    show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
-      using lim by auto
-    show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
-      using lim lim(1)[THEN borel_measurable_integrable]
-      by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
-  qed
-qed
-
-context
-  fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-begin
-
-lemma has_integral_integral_lborel:
-  assumes f: "integrable lborel f"
-  shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
-proof -
-  have "((\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) has_integral (\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b)) UNIV"
-    using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_real) auto
-  also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
-    by (simp add: fun_eq_iff euclidean_representation)
-  also have "(\<Sum>b\<in>Basis. integral\<^sup>L lborel (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lborel f"
-    using f by (subst (2) eq_f[symmetric]) simp
-  finally show ?thesis .
-qed
-
-lemma integrable_on_lborel: "integrable lborel f \<Longrightarrow> f integrable_on UNIV"
-  using has_integral_integral_lborel by auto
-
-lemma integral_lborel: "integrable lborel f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lborel)"
-  using has_integral_integral_lborel by auto
-
-end
-
-subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
-
 lemma emeasure_bounded_finite:
   assumes "bounded A" shows "emeasure lborel A < \<infinity>"
 proof -
@@ -1149,233 +780,4 @@
     by (auto simp: mult.commute)
 qed
 
-text \<open>
-
-For the positive integral we replace continuity with Borel-measurability.
-
-\<close>
-
-lemma
-  fixes f :: "real \<Rightarrow> real"
-  assumes [measurable]: "f \<in> borel_measurable borel"
-  assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
-  shows nn_integral_FTC_Icc: "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?nn)
-    and has_bochner_integral_FTC_Icc_nonneg:
-      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
-    and integral_FTC_Icc_nonneg: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
-    and integrable_FTC_Icc_nonneg: "integrable lborel (\<lambda>x. f x * indicator {a .. b} x)" (is ?int)
-proof -
-  have *: "(\<lambda>x. f x * indicator {a..b} x) \<in> borel_measurable borel" "\<And>x. 0 \<le> f x * indicator {a..b} x"
-    using f(2) by (auto split: split_indicator)
-
-  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b\<Longrightarrow> F x \<le> F y" for x y
-    using f by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
-
-  have "(f has_integral F b - F a) {a..b}"
-    by (intro fundamental_theorem_of_calculus)
-       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
-             intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
-  then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
-    unfolding indicator_def if_distrib[where f="\<lambda>x. a * x" for a]
-    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
-  then have nn: "(\<integral>\<^sup>+x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a"
-    by (rule nn_integral_has_integral_lborel[OF *])
-  then show ?has
-    by (rule has_bochner_integral_nn_integral[rotated 3]) (simp_all add: * F_mono \<open>a \<le> b\<close>)
-  then show ?eq ?int
-    unfolding has_bochner_integral_iff by auto
-  show ?nn
-    by (subst nn[symmetric])
-       (auto intro!: nn_integral_cong simp add: ennreal_mult f split: split_indicator)
-qed
-
-lemma
-  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
-  assumes "a \<le> b"
-  assumes "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
-  assumes cont: "continuous_on {a .. b} f"
-  shows has_bochner_integral_FTC_Icc:
-      "has_bochner_integral lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) (F b - F a)" (is ?has)
-    and integral_FTC_Icc: "(\<integral>x. indicator {a .. b} x *\<^sub>R f x \<partial>lborel) = F b - F a" (is ?eq)
-proof -
-  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
-  have int: "integrable lborel ?f"
-    using borel_integrable_compact[OF _ cont] by auto
-  have "(f has_integral F b - F a) {a..b}"
-    using assms(1,2) by (intro fundamental_theorem_of_calculus) auto
-  moreover
-  have "(f has_integral integral\<^sup>L lborel ?f) {a..b}"
-    using has_integral_integral_lborel[OF int]
-    unfolding indicator_def if_distrib[where f="\<lambda>x. x *\<^sub>R a" for a]
-    by (simp cong del: if_weak_cong del: atLeastAtMost_iff)
-  ultimately show ?eq
-    by (auto dest: has_integral_unique)
-  then show ?has
-    using int by (auto simp: has_bochner_integral_iff)
-qed
-
-lemma
-  fixes f :: "real \<Rightarrow> real"
-  assumes "a \<le> b"
-  assumes deriv: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> DERIV F x :> f x"
-  assumes cont: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> isCont f x"
-  shows has_bochner_integral_FTC_Icc_real:
-      "has_bochner_integral lborel (\<lambda>x. f x * indicator {a .. b} x) (F b - F a)" (is ?has)
-    and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
-proof -
-  have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
-    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
-    using deriv by (auto intro: DERIV_subset)
-  have 2: "continuous_on {a .. b} f"
-    using cont by (intro continuous_at_imp_continuous_on) auto
-  show ?has ?eq
-    using has_bochner_integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2] integral_FTC_Icc[OF \<open>a \<le> b\<close> 1 2]
-    by (auto simp: mult.commute)
-qed
-
-lemma nn_integral_FTC_atLeast:
-  fixes f :: "real \<Rightarrow> real"
-  assumes f_borel: "f \<in> borel_measurable borel"
-  assumes f: "\<And>x. a \<le> x \<Longrightarrow> DERIV F x :> f x"
-  assumes nonneg: "\<And>x. a \<le> x \<Longrightarrow> 0 \<le> f x"
-  assumes lim: "(F \<longlongrightarrow> T) at_top"
-  shows "(\<integral>\<^sup>+x. ennreal (f x) * indicator {a ..} x \<partial>lborel) = T - F a"
-proof -
-  let ?f = "\<lambda>(i::nat) (x::real). ennreal (f x) * indicator {a..a + real i} x"
-  let ?fR = "\<lambda>x. ennreal (f x) * indicator {a ..} x"
-
-  have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
-    using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
-  then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
-    by (intro tendsto_le_const[OF _ lim])
-       (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
-
-  have "(SUP i::nat. ?f i x) = ?fR x" for x
-  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    from reals_Archimedean2[of "x - a"] guess n ..
-    then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
-      by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
-    then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
-      by (rule Lim_eventually)
-  qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
-  then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
-    by simp
-  also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
-  proof (rule nn_integral_monotone_convergence_SUP)
-    show "incseq ?f"
-      using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
-    show "\<And>i. (?f i) \<in> borel_measurable lborel"
-      using f_borel by auto
-  qed
-  also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
-    by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
-  also have "\<dots> = T - F a"
-  proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
-    have "(\<lambda>x. F (a + real x)) \<longlonglongrightarrow> T"
-      apply (rule filterlim_compose[OF lim filterlim_tendsto_add_at_top])
-      apply (rule LIMSEQ_const_iff[THEN iffD2, OF refl])
-      apply (rule filterlim_real_sequentially)
-      done
-    then show "(\<lambda>n. ennreal (F (a + real n) - F a)) \<longlonglongrightarrow> ennreal (T - F a)"
-      by (simp add: F_mono F_le_T tendsto_diff)
-  qed (auto simp: incseq_def intro!: ennreal_le_iff[THEN iffD2] F_mono)
-  finally show ?thesis .
-qed
-
-lemma integral_power:
-  "a \<le> b \<Longrightarrow> (\<integral>x. x^k * indicator {a..b} x \<partial>lborel) = (b^Suc k - a^Suc k) / Suc k"
-proof (subst integral_FTC_Icc_real)
-  fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
-    by (intro derivative_eq_intros) auto
-qed (auto simp: field_simps simp del: of_nat_Suc)
-
-subsection \<open>Integration by parts\<close>
-
-lemma integral_by_parts_integrable:
-  fixes f g F G::"real \<Rightarrow> real"
-  assumes "a \<le> b"
-  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
-  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
-  assumes [intro]: "!!x. DERIV F x :> f x"
-  assumes [intro]: "!!x. DERIV G x :> g x"
-  shows  "integrable lborel (\<lambda>x.((F x) * (g x) + (f x) * (G x)) * indicator {a .. b} x)"
-  by (auto intro!: borel_integrable_atLeastAtMost continuous_intros) (auto intro!: DERIV_isCont)
-
-lemma integral_by_parts:
-  fixes f g F G::"real \<Rightarrow> real"
-  assumes [arith]: "a \<le> b"
-  assumes cont_f[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
-  assumes cont_g[intro]: "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
-  assumes [intro]: "!!x. DERIV F x :> f x"
-  assumes [intro]: "!!x. DERIV G x :> g x"
-  shows "(\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel)
-            =  F b * G b - F a * G a - \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
-proof-
-  have 0: "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) = F b * G b - F a * G a"
-    by (rule integral_FTC_Icc_real, auto intro!: derivative_eq_intros continuous_intros)
-      (auto intro!: DERIV_isCont)
-
-  have "(\<integral>x. (F x * g x + f x * G x) * indicator {a .. b} x \<partial>lborel) =
-    (\<integral>x. (F x * g x) * indicator {a .. b} x \<partial>lborel) + \<integral>x. (f x * G x) * indicator {a .. b} x \<partial>lborel"
-    apply (subst integral_add[symmetric])
-    apply (auto intro!: borel_integrable_atLeastAtMost continuous_intros)
-    by (auto intro!: DERIV_isCont integral_cong split:split_indicator)
-
-  thus ?thesis using 0 by auto
-qed
-
-lemma integral_by_parts':
-  fixes f g F G::"real \<Rightarrow> real"
-  assumes "a \<le> b"
-  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont f x"
-  assumes "!!x. a \<le>x \<Longrightarrow> x\<le>b \<Longrightarrow> isCont g x"
-  assumes "!!x. DERIV F x :> f x"
-  assumes "!!x. DERIV G x :> g x"
-  shows "(\<integral>x. indicator {a .. b} x *\<^sub>R (F x * g x) \<partial>lborel)
-            =  F b * G b - F a * G a - \<integral>x. indicator {a .. b} x *\<^sub>R (f x * G x) \<partial>lborel"
-  using integral_by_parts[OF assms] by (simp add: ac_simps)
-
-lemma has_bochner_integral_even_function:
-  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
-  assumes even: "\<And>x. f (- x) = f x"
-  shows "has_bochner_integral lborel f (2 *\<^sub>R x)"
-proof -
-  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
-    by (auto split: split_indicator)
-  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) x"
-    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
-       (auto simp: indicator even f)
-  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + x)"
-    by (rule has_bochner_integral_add)
-  then have "has_bochner_integral lborel f (x + x)"
-    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
-       (auto split: split_indicator)
-  then show ?thesis
-    by (simp add: scaleR_2)
-qed
-
-lemma has_bochner_integral_odd_function:
-  fixes f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  assumes f: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x) x"
-  assumes odd: "\<And>x. f (- x) = - f x"
-  shows "has_bochner_integral lborel f 0"
-proof -
-  have indicator: "\<And>x::real. indicator {..0} (- x) = indicator {0..} x"
-    by (auto split: split_indicator)
-  have "has_bochner_integral lborel (\<lambda>x. - indicator {.. 0} x *\<^sub>R f x) x"
-    by (subst lborel_has_bochner_integral_real_affine_iff[where c="-1" and t=0])
-       (auto simp: indicator odd f)
-  from has_bochner_integral_minus[OF this]
-  have "has_bochner_integral lborel (\<lambda>x. indicator {.. 0} x *\<^sub>R f x) (- x)"
-    by simp
-  with f have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R f x + indicator {.. 0} x *\<^sub>R f x) (x + - x)"
-    by (rule has_bochner_integral_add)
-  then have "has_bochner_integral lborel f (x + - x)"
-    by (rule has_bochner_integral_discrete_difference[where X="{0}", THEN iffD1, rotated 4])
-       (auto split: split_indicator)
-  then show ?thesis
-    by simp
-qed
-
 end
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -10,6 +10,30 @@
   "~~/src/HOL/Library/Infinite_Set"
 begin
 
+lemma linear_simps:
+  assumes "bounded_linear f"
+  shows
+    "f (a + b) = f a + f b"
+    "f (a - b) = f a - f b"
+    "f 0 = 0"
+    "f (- a) = - f a"
+    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
+proof -
+  interpret f: bounded_linear f by fact
+  show "f (a + b) = f a + f b" by (rule f.add)
+  show "f (a - b) = f a - f b" by (rule f.diff)
+  show "f 0 = 0" by (rule f.zero)
+  show "f (- a) = - f a" by (rule f.minus)
+  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
+qed
+
+lemma bounded_linearI:
+  assumes "\<And>x y. f (x + y) = f x + f y"
+    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
+    and "\<And>x. norm (f x) \<le> norm x * K"
+  shows "bounded_linear f"
+  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
+
 subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
 
 definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -243,27 +243,6 @@
 lemma One_nonneg: "0 \<le> (\<Sum>Basis::'a::ordered_euclidean_space)"
   by (auto intro: setsum_nonneg)
 
-lemma content_closed_interval:
-  fixes a :: "'a::ordered_euclidean_space"
-  assumes "a \<le> b"
-  shows "content {a .. b} = (\<Prod>i\<in>Basis. b\<bullet>i - a\<bullet>i)"
-  using content_cbox[of a b] assms
-  by (simp add: cbox_interval eucl_le[where 'a='a])
-
-lemma integrable_const_ivl[intro]:
-  fixes a::"'a::ordered_euclidean_space"
-  shows "(\<lambda>x. c) integrable_on {a .. b}"
-  unfolding cbox_interval[symmetric]
-  by (rule integrable_const)
-
-lemma integrable_on_subinterval:
-  fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f integrable_on s"
-    and "{a .. b} \<subseteq> s"
-  shows "f integrable_on {a .. b}"
-  using integrable_on_subcbox[of f s a b] assms
-  by (simp add: cbox_interval)
-
 lemma
   fixes a b::"'a::ordered_euclidean_space"
   shows bdd_above_cbox[intro, simp]: "bdd_above (cbox a b)"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Set_Integral
-  imports Bochner_Integration Lebesgue_Measure
+  imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
 (*
@@ -85,7 +85,7 @@
 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!: integral_cong split: split_indicator simp add: sets.sets_into_space)
+  using assms by (auto intro!: Bochner_Integration.integral_cong split: split_indicator simp add: sets.sets_into_space)
 
 lemma set_lebesgue_integral_cong_AE:
   assumes [measurable]: "A \<in> sets M" "f \<in> borel_measurable M" "g \<in> borel_measurable M"
@@ -118,22 +118,22 @@
 (* 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)"
-  by (subst integral_scaleR_right[symmetric]) (auto intro!: integral_cong)
+  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)"
-  by (subst integral_mult_right_zero[symmetric]) (auto intro!: integral_cong)
+  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"
-  by (subst integral_mult_left_zero[symmetric]) (auto intro!: integral_cong)
+  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"
-  by (subst integral_divide_zero[symmetric], intro integral_cong)
+  by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong)
      (auto split: split_indicator)
 
 lemma set_integrable_scaleR_right [simp, intro]:
@@ -184,7 +184,7 @@
   fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   by (subst lborel_integral_real_affine[where c="-1" and t=0])
-     (auto intro!: integral_cong split: split_indicator)
+     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
@@ -194,7 +194,7 @@
 lemma set_integral_complex_of_real:
   "LINT x:A|M. complex_of_real (f x) = of_real (LINT x:A|M. f x)"
   by (subst integral_complex_of_real[symmetric])
-     (auto intro!: integral_cong split: split_indicator)
+     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
 
 lemma set_integral_mono:
   fixes f g :: "_ \<Rightarrow> real"
@@ -254,7 +254,7 @@
 proof -
   have "set_integrable M (A - B) f"
     using f_A by (rule set_integrable_subset) auto
-  from integrable_add[OF this f_B] show ?thesis
+  from Bochner_Integration.integrable_add[OF this f_B] show ?thesis
     by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator)
 qed
 
@@ -410,7 +410,7 @@
       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)"
-    apply (rule integral_cong[OF refl])
+    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
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Library/Inner_Product.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -260,6 +260,11 @@
 
 end
 
+lemma
+  shows real_inner_1_left[simp]: "inner 1 x = x"
+    and real_inner_1_right[simp]: "inner x 1 = x"
+  by simp_all
+
 instantiation complex :: real_inner
 begin
 
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -316,13 +316,13 @@
   then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
     by (simp add: integ_c)
   also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+    unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
   proof (rule integral_mono)
     show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
-      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+      by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
     show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
       unfolding power_abs[symmetric]
       by (intro integrable_mult_right integrable_abs integrable_moments) simp
@@ -360,16 +360,16 @@
   then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
     by (simp add: integ_c)
   also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
+    unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
+    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
   also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
     (is "_ \<le> expectation ?f")
   proof (rule integral_mono)
     show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
-      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
+      by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_setsum integ_c) simp
     show "integrable M ?f"
-      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
+      by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
          (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
     show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x
       using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n]
@@ -377,9 +377,9 @@
   qed
   also have "\<dots> = (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
     unfolding *
-  proof (rule integral_mult_right)
+  proof (rule Bochner_Integration.integral_mult_right)
     show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))"
-      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
+      by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
          (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
   qed
   finally show ?thesis
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Distributions.thy
--- a/src/HOL/Probability/Distributions.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Distributions.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -608,7 +608,7 @@
     using D by (rule entropy_distr) simp
   also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) =
     (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
-    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
+    by (intro Bochner_Integration.integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
   also have "\<dots> = (ln l - 1) / ln b"
     by simp
   finally show ?thesis
@@ -750,7 +750,7 @@
     uniform_distributed_bounds[of X a b]
     uniform_distributed_measure[of X a b]
     distributed_measurable[of M lborel X]
-  by (auto intro!: uniform_distrI_borel_atLeastAtMost)
+  by (auto intro!: uniform_distrI_borel_atLeastAtMost simp del: content_real_if)
 
 lemma (in prob_space) uniform_distributed_expectation:
   fixes a b :: real
@@ -762,13 +762,13 @@
 
   have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) =
     (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
-    by (intro integral_cong) auto
+    by (intro Bochner_Integration.integral_cong) auto
   also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
   proof (subst integral_FTC_Icc_real)
     fix x
     show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
       using uniform_distributed_params[OF D]
-      by (auto intro!: derivative_eq_intros)
+      by (auto intro!: derivative_eq_intros simp del: content_real_if)
     show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
       using uniform_distributed_params[OF D]
       by (auto intro!: isCont_divide)
@@ -791,12 +791,12 @@
   have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
   let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
   have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
-    by (intro integral_cong) (auto split: split_indicator)
+    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator)
   also have "\<dots> = (b - a)\<^sup>2 / 12"
     by (simp add: integral_power uniform_distributed_expectation[OF D])
        (simp add: eval_nat_numeral field_simps )
   finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
-qed (auto intro: D simp: measure_nonneg)
+qed (auto intro: D simp del: content_real_if)
 
 subsection \<open>Normal distribution\<close>
 
@@ -949,7 +949,7 @@
     proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
       fix b :: real assume b: "0 \<le> b"
       have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
-        unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto
+        unfolding integral_mult_right_zero[symmetric] by (intro Bochner_Integration.integral_cong) auto
       also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
           (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
         by (rule integral_by_parts')
@@ -957,7 +957,7 @@
                  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 integral_cong) auto
+        by (intro Bochner_Integration.integral_cong) auto
       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])
@@ -1361,10 +1361,10 @@
   have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
     using D by (rule entropy_distr) simp
   also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
-    by (intro arg_cong[where f="uminus"] integral_cong)
+    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong)
        (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
   also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
-    by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
+    by (intro arg_cong[where f="uminus"] Bochner_Integration.integral_cong) (auto simp: divide_simps field_simps)
   also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
     by (simp del: minus_add_distrib)
   also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -862,15 +862,15 @@
   show ?integrable
     using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
   have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"
-  proof(rule integral_cong)
+  proof(rule Bochner_Integration.integral_cong)
     fix M'
     assume "M' \<in> space M"
     with sets_eq_imp_space_eq[OF M] have "space M' = space N"
       by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
-    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)
+    with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty)
   qed simp
   then show ?integral
-    using M * by(simp add: integral_empty)
+    using M * by(simp add: Bochner_Integration.integral_empty)
 next
   assume *: "space N \<noteq> {}"
 
@@ -1213,7 +1213,7 @@
   also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M"
     by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
   finally show ?integral by(simp add: bind_nonempty''[where N=K])
-qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty)
+qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
 
 lemma (in prob_space) prob_space_bind:
   assumes ae: "AE x in M. prob_space (N x)"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Information.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -840,7 +840,7 @@
   also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
     unfolding distributed_distr_eq_density[OF X] using Px Px_nn
     apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
-    by (subst integral_density) (auto simp del: integral_indicator intro!: integral_cong)
+    by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"
@@ -901,11 +901,11 @@
   have eq: "(\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
     (\<integral> x. (- log b (measure MX A) / measure MX A) * indicator A x \<partial>MX)"
     using uniform_distributed_params[OF X]
-    by (intro integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
+    by (intro Bochner_Integration.integral_cong) (auto split: split_indicator simp: log_divide_eq zero_less_measure_iff)
   show "- (\<integral> x. indicator A x / measure MX A * log b (indicator A x / measure MX A) \<partial>MX) =
     log b (measure MX A)"
     unfolding eq using uniform_distributed_params[OF X]
-    by (subst integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
+    by (subst Bochner_Integration.integral_mult_right) (auto simp: measure_def less_top[symmetric] intro!: integrable_real_indicator)
 qed simp
 
 lemma (in information_space) entropy_simple_distributed:
@@ -1038,8 +1038,8 @@
     apply (subst mi_eq)
     apply (subst mutual_information_distr[OF S TP Px Px_nn Pyz _ Pxyz])
     apply (auto simp: space_pair_measure)
-    apply (subst integral_diff[symmetric])
-    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
+    apply (subst Bochner_Integration.integral_diff[symmetric])
+    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
     done
 
   let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
@@ -1112,7 +1112,7 @@
     done
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
-    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
+    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
     using ae
     apply (auto simp: split_beta')
     done
@@ -1297,8 +1297,8 @@
     apply simp
     apply simp
     apply (simp add: space_pair_measure)
-    apply (subst integral_diff[symmetric])
-    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: integral_diff)
+    apply (subst Bochner_Integration.integral_diff[symmetric])
+    apply (auto intro!: integral_cong_AE simp: split_beta' simp del: Bochner_Integration.integral_diff)
     done
 
   let ?P = "density (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) Pxyz"
@@ -1373,7 +1373,7 @@
        (auto simp: split_beta' AE_density space_pair_measure intro!: AE_I2 ennreal_neg)
 
   have I3: "integrable (S \<Otimes>\<^sub>M T \<Otimes>\<^sub>M P) (\<lambda>(x, y, z). Pxyz (x, y, z) * log b (Pxyz (x, y, z) / (Pxz (x, z) * (Pyz (y,z) / Pz z))))"
-    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ integrable_diff[OF I1 I2]])
+    apply (rule integrable_cong_AE[THEN iffD1, OF _ _ _ Bochner_Integration.integrable_diff[OF I1 I2]])
     using ae
     apply (auto simp: split_beta')
     done
@@ -1593,7 +1593,7 @@
   also have "\<dots> = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))"
     using b_gt_1
     by (subst distributed_transform_integral[OF Pxy _ Py, where T=snd])
-       (auto intro!: integral_cong simp: space_pair_measure)
+       (auto intro!: Bochner_Integration.integral_cong simp: space_pair_measure)
   finally have e_eq: "entropy b T Y = - (\<integral>(x,y). Pxy (x,y) * log b (Py y) \<partial>(S \<Otimes>\<^sub>M T))" .
 
   have **: "\<And>x. x \<in> space (S \<Otimes>\<^sub>M T) \<Longrightarrow> 0 \<le> Pxy x"
@@ -1618,7 +1618,7 @@
     apply auto
     done
   also have "\<dots> = - (\<integral>x. Pxy x * log b (Pxy x) \<partial>(S \<Otimes>\<^sub>M T)) - - (\<integral>x.  Pxy x * log b (Py (snd x)) \<partial>(S \<Otimes>\<^sub>M T))"
-    by (simp add: integral_diff[OF I1 I2])
+    by (simp add: Bochner_Integration.integral_diff[OF I1 I2])
   finally show ?thesis
     using conditional_entropy_generic_eq[OF S T Py Py_nn Pxy Pxy_nn, simplified]
       entropy_distr[OF Pxy **, simplified] e_eq
@@ -1785,9 +1785,9 @@
 
   have "entropy b S X + entropy b T Y - entropy b (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) = integral\<^sup>L (S \<Otimes>\<^sub>M T) ?f"
     unfolding X Y XY
-    apply (subst integral_diff)
-    apply (intro integrable_diff Ixy Ix Iy)+
-    apply (subst integral_diff)
+    apply (subst Bochner_Integration.integral_diff)
+    apply (intro Bochner_Integration.integrable_diff Ixy Ix Iy)+
+    apply (subst Bochner_Integration.integral_diff)
     apply (intro Ixy Ix Iy)+
     apply (simp add: field_simps)
     done
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -136,9 +136,9 @@
     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
-      by (auto split: split_indicator intro!: integral_cong)
+      by (auto split: split_indicator intro!: Bochner_Integration.integral_cong)
     also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))"
-      by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
+      by (auto intro!: Bochner_Integration.integral_cong simp: field_simps exp_diff exp_minus split: split_indicator)
     also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))"
     proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"])
       show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>"
@@ -151,7 +151,7 @@
     qed (auto split: split_indicator split_indicator_asm)
     also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))"
-       using main_eq by (intro integral_cong, auto)
+       using main_eq by (intro Bochner_Integration.integral_cong, auto)
     also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) *
          Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))"
        by (rule integral_complex_of_real)
@@ -336,11 +336,11 @@
         (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))))"
-      by (rule integral_cong) (auto split: split_indicator)
+      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')
     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 integral_cong, auto simp add: * simp del: of_real_mult)
+      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)))"
       by (rule integral_complex_of_real)
     finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) =
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -167,7 +167,7 @@
 
 lemma pmf_nonneg[simp]: "0 \<le> pmf p x"
   by transfer simp
-  
+
 lemma pmf_not_neg [simp]: "\<not>pmf p x < 0"
   by (simp add: not_less pmf_nonneg)
 
@@ -546,7 +546,7 @@
 
 lemma measure_return_pmf [simp]: "measure_pmf.prob (return_pmf x) A = indicator A x"
 proof -
-  have "ennreal (measure_pmf.prob (return_pmf x) A) = 
+  have "ennreal (measure_pmf.prob (return_pmf x) A) =
           emeasure (measure_pmf (return_pmf x)) A"
     by (simp add: measure_pmf.emeasure_eq_measure)
   also have "\<dots> = ennreal (indicator A x)" by (simp add: ennreal_indicator)
@@ -778,10 +778,10 @@
   have "1 = measure (measure_pmf M) UNIV" by simp
   also have "\<dots> = measure (measure_pmf N) {x} + measure (measure_pmf N) (UNIV - {x})"
     by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
-  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}" 
+  also from gt have "measure (measure_pmf N) {x} < measure (measure_pmf M) {x}"
     by (simp add: measure_pmf_single)
   also have "measure (measure_pmf N) (UNIV - {x}) \<le> measure (measure_pmf M) (UNIV - {x})"
-    by (subst (1 2) integral_pmf [symmetric]) 
+    by (subst (1 2) integral_pmf [symmetric])
        (intro integral_mono integrable_pmf, simp_all add: ge)
   also have "measure (measure_pmf M) {x} + \<dots> = 1"
     by (subst measure_pmf.finite_measure_Union [symmetric]) simp_all
@@ -803,7 +803,7 @@
     by unfold_locales
 
   have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
-    by (rule integral_cong) (auto intro!: integral_pmf_restrict)
+    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict)
   also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
     by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
               countable_set_pmf borel_measurable_count_space)
@@ -815,7 +815,7 @@
     by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
               countable_set_pmf borel_measurable_count_space)
   also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
-    by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
+    by (rule Bochner_Integration.integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
 qed
 
@@ -1629,7 +1629,7 @@
 
 lemma map_pmf_of_set:
   assumes "finite A" "A \<noteq> {}"
-  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))" 
+  shows   "map_pmf f (pmf_of_set A) = pmf_of_multiset (image_mset f (mset_set A))"
     (is "?lhs = ?rhs")
 proof (intro pmf_eqI)
   fix x
@@ -1641,13 +1641,13 @@
 
 lemma pmf_bind_pmf_of_set:
   assumes "A \<noteq> {}" "finite A"
-  shows   "pmf (bind_pmf (pmf_of_set A) f) x = 
+  shows   "pmf (bind_pmf (pmf_of_set A) f) x =
              (\<Sum>xa\<in>A. pmf (f xa) x) / real_of_nat (card A)" (is "?lhs = ?rhs")
 proof -
   from assms have "card A > 0" by auto
   with assms have "ennreal ?lhs = ennreal ?rhs"
-    by (subst ennreal_pmf_bind) 
-       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric] 
+    by (subst ennreal_pmf_bind)
+       (simp_all add: nn_integral_pmf_of_set max_def pmf_nonneg divide_ennreal [symmetric]
         setsum_nonneg ennreal_of_nat_eq_real_of_nat)
   thus ?thesis by (subst (asm) ennreal_inj) (auto intro!: setsum_nonneg divide_nonneg_nonneg)
 qed
@@ -1675,10 +1675,10 @@
 qed
 
 text \<open>
-  Choosing an element uniformly at random from the union of a disjoint family 
-  of finite non-empty sets with the same size is the same as first choosing a set 
-  from the family uniformly at random and then choosing an element from the chosen set 
-  uniformly at random.  
+  Choosing an element uniformly at random from the union of a disjoint family
+  of finite non-empty sets with the same size is the same as first choosing a set
+  from the family uniformly at random and then choosing an element from the chosen set
+  uniformly at random.
 \<close>
 lemma pmf_of_set_UN:
   assumes "finite (UNION A f)" "A \<noteq> {}" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> {}"
@@ -1694,8 +1694,8 @@
     by (subst pmf_of_set) auto
   also from assms have "card (\<Union>x\<in>A. f x) = card A * n"
     by (subst card_UN_disjoint) (auto simp: disjoint_family_on_def)
-  also from assms 
-    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> = 
+  also from assms
+    have "indicator (\<Union>x\<in>A. f x) x / real \<dots> =
               indicator (\<Union>x\<in>A. f x) x / (n * real (card A))"
       by (simp add: setsum_divide_distrib [symmetric] mult_ac)
   also from assms have "indicator (\<Union>x\<in>A. f x) x = (\<Sum>y\<in>A. indicator (f y) x)"
@@ -1794,17 +1794,17 @@
 
 lemma replicate_pmf_1: "replicate_pmf 1 p = map_pmf (\<lambda>x. [x]) p"
   by (simp add: map_pmf_def bind_return_pmf)
-  
-lemma set_replicate_pmf: 
+
+lemma set_replicate_pmf:
   "set_pmf (replicate_pmf n p) = {xs\<in>lists (set_pmf p). length xs = n}"
   by (induction n) (auto simp: length_Suc_conv)
 
 lemma replicate_pmf_distrib:
-  "replicate_pmf (m + n) p = 
+  "replicate_pmf (m + n) p =
      do {xs \<leftarrow> replicate_pmf m p; ys \<leftarrow> replicate_pmf n p; return_pmf (xs @ ys)}"
   by (induction m) (simp_all add: bind_return_pmf bind_return_pmf' bind_assoc_pmf)
 
-lemma power_diff': 
+lemma power_diff':
   assumes "b \<le> a"
   shows   "x ^ (a - b) = (if x = 0 \<and> a = b then 1 else x ^ a / (x::'a::field) ^ b)"
 proof (cases "x = 0")
@@ -1812,12 +1812,12 @@
   with assms show ?thesis by (cases "a - b") simp_all
 qed (insert assms, simp_all add: power_diff)
 
-  
+
 lemma binomial_pmf_Suc:
   assumes "p \<in> {0..1}"
-  shows   "binomial_pmf (Suc n) p = 
-             do {b \<leftarrow> bernoulli_pmf p; 
-                 k \<leftarrow> binomial_pmf n p; 
+  shows   "binomial_pmf (Suc n) p =
+             do {b \<leftarrow> bernoulli_pmf p;
+                 k \<leftarrow> binomial_pmf n p;
                  return_pmf ((if b then 1 else 0) + k)}" (is "_ = ?rhs")
 proof (intro pmf_eqI)
   fix k
@@ -1835,14 +1835,14 @@
 lemma binomial_pmf_altdef:
   assumes "p \<in> {0..1}"
   shows   "binomial_pmf n p = map_pmf (length \<circ> filter id) (replicate_pmf n (bernoulli_pmf p))"
-  by (induction n) 
-     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf 
+  by (induction n)
+     (insert assms, auto simp: binomial_pmf_Suc map_pmf_def bind_return_pmf bind_assoc_pmf
         bind_return_pmf' binomial_pmf_0 intro!: bind_pmf_cong)
 
 
 subsection \<open>PMFs from assiciation lists\<close>
 
-definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where 
+definition pmf_of_list ::" ('a \<times> real) list \<Rightarrow> 'a pmf" where
   "pmf_of_list xs = embed_pmf (\<lambda>x. sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
 
 definition pmf_of_list_wf where
@@ -1870,12 +1870,12 @@
     from Cons.prems have "snd x \<ge> 0" by simp
     moreover have "b \<ge> 0" if "(a,b) \<in> set xs" for a b
       using Cons.prems[of b] that by force
-    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) = 
-            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) + 
+    ultimately have "(\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>x # xs. indicator {x'} y * p) \<partial>count_space UNIV) =
+            (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) +
             ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
-      by (intro nn_integral_cong, subst ennreal_plus [symmetric]) 
+      by (intro nn_integral_cong, subst ennreal_plus [symmetric])
          (auto simp: case_prod_unfold indicator_def intro!: sum_list_nonneg)
-    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) + 
+    also have "\<dots> = (\<integral>\<^sup>+ y. ennreal (indicator {fst x} y * snd x) \<partial>count_space UNIV) +
                       (\<integral>\<^sup>+ y. ennreal (\<Sum>(x', p)\<leftarrow>xs. indicator {x'} y * p) \<partial>count_space UNIV)"
       by (intro nn_integral_add)
          (force intro!: sum_list_nonneg AE_I2 intro: Cons simp: indicator_def)+
@@ -1934,20 +1934,20 @@
 proof -
   have "emeasure (pmf_of_list xs) A = nn_integral (measure_pmf (pmf_of_list xs)) (indicator A)"
     by simp
-  also from assms 
+  also from assms
     have "\<dots> = (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. ennreal (sum_list (map snd [z\<leftarrow>xs . fst z = x])))"
     by (subst nn_integral_measure_pmf_finite) (simp_all add: finite_set_pmf_of_list pmf_pmf_of_list)
-  also from assms 
+  also from assms
     have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. sum_list (map snd [z\<leftarrow>xs . fst z = x]))"
     by (subst setsum_ennreal) (auto simp: pmf_of_list_wf_def intro!: sum_list_nonneg)
-  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A. 
+  also have "\<dots> = ennreal (\<Sum>x\<in>set_pmf (pmf_of_list xs) \<inter> A.
       indicator A x * pmf (pmf_of_list xs) x)" (is "_ = ennreal ?S")
     using assms by (intro ennreal_cong setsum.cong) (auto simp: pmf_pmf_of_list)
   also have "?S = (\<Sum>x\<in>set_pmf (pmf_of_list xs). indicator A x * pmf (pmf_of_list xs) x)"
     using assms by (intro setsum.mono_neutral_left set_pmf_of_list finite_set_pmf_of_list) auto
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * pmf (pmf_of_list xs) x)"
     using assms by (intro setsum.mono_neutral_left set_pmf_of_list) (auto simp: set_pmf_eq)
-  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x * 
+  also have "\<dots> = (\<Sum>x\<in>set (map fst xs). indicator A x *
                       sum_list (map snd (filter (\<lambda>z. fst z = x) xs)))"
     using assms by (simp add: pmf_pmf_of_list)
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). sum_list (map snd (filter (\<lambda>z. fst z = x \<and> x \<in> A) xs)))"
@@ -1955,17 +1955,17 @@
   also have "\<dots> = (\<Sum>x\<in>set (map fst xs). (\<Sum>xa = 0..<length xs.
                      if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
     by (intro setsum.cong refl, subst sum_list_map_filter', subst sum_list_setsum_nth) simp
-  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs). 
+  also have "\<dots> = (\<Sum>xa = 0..<length xs. (\<Sum>x\<in>set (map fst xs).
                      if fst (xs ! xa) = x \<and> x \<in> A then snd (xs ! xa) else 0))"
     by (rule setsum.commute)
-  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then 
+  also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
                      (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
     by (auto intro!: setsum.cong setsum.neutral)
   also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
     by (intro setsum.cong refl) (simp_all add: setsum.delta)
   also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
     by (subst sum_list_map_filter', subst sum_list_setsum_nth) simp_all
-  finally show ?thesis . 
+  finally show ?thesis .
 qed
 
 lemma measure_pmf_of_list:
@@ -1989,7 +1989,7 @@
   "sum_list (filter (\<lambda>x. x \<noteq> 0) xs) = sum_list xs"
   by (induction xs) simp_all
 (* END MOVE *)
-  
+
 lemma set_pmf_of_list_eq:
   assumes "pmf_of_list_wf xs" "\<And>x. x \<in> snd ` set xs \<Longrightarrow> x > 0"
   shows   "set_pmf (pmf_of_list xs) = fst ` set xs"
@@ -2000,13 +2000,13 @@
     from B have "sum_list (map snd [z\<leftarrow>xs. fst z = x]) = 0"
       by (simp add: pmf_pmf_of_list[OF assms(1)] set_pmf_eq)
     moreover from y have "y \<in> snd ` {xa \<in> set xs. fst xa = x}" by force
-    ultimately have "y = 0" using assms(1) 
+    ultimately have "y = 0" using assms(1)
       by (subst (asm) sum_list_nonneg_eq_zero_iff) (auto simp: pmf_of_list_wf_def)
     with assms(2) y have False by force
   }
   thus "fst ` set xs \<subseteq> set_pmf (pmf_of_list xs)" by blast
 qed (insert set_pmf_of_list[OF assms(1)], simp_all)
-  
+
 lemma pmf_of_list_remove_zeros:
   assumes "pmf_of_list_wf xs"
   defines "xs' \<equiv> filter (\<lambda>z. snd z \<noteq> 0) xs"
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -225,7 +225,7 @@
       using prob_space by (simp add: X)
     also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
       using \<open>x \<in> I\<close> \<open>open I\<close> X(2)
-      apply (intro integral_mono_AE integrable_add integrable_mult_right integrable_diff
+      apply (intro integral_mono_AE Bochner_Integration.integrable_add Bochner_Integration.integrable_mult_right Bochner_Integration.integrable_diff
                 integrable_const X q)
       apply (elim eventually_mono)
       apply (intro convex_le_Inf_differential)
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/SPMF.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -554,11 +554,11 @@
   have "?lhs = \<integral> x. ?f x \<partial>measure_pmf p"
     by(simp add: bind_spmf_def pmf_bind)
   also have "\<dots> = \<integral> x. ?f None * indicator {None} x + ?f x * indicator (range Some) x \<partial>measure_pmf p"
-    by(rule integral_cong)(auto simp add: indicator_def)
+    by(rule Bochner_Integration.integral_cong)(auto simp add: indicator_def)
   also have "\<dots> = (\<integral> x. ?f None * indicator {None} x \<partial>measure_pmf p) + (\<integral> x. ?f x * indicator (range Some) x \<partial>measure_pmf p)"
-    by(rule integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
+    by(rule Bochner_Integration.integral_add)(auto 4 3 intro: integrable_real_mult_indicator measure_pmf.integrable_const_bound[where B=1] simp add: AE_measure_pmf_iff pmf_le_1)
   also have "\<dots> = pmf p None + \<integral> x. indicator (range Some) x * pmf (f (the x)) None \<partial>measure_pmf p"
-    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: integral_cong)
+    by(auto simp add: measure_measure_pmf_finite indicator_eq_0_iff intro!: Bochner_Integration.integral_cong)
   also have "\<dots> = ?rhs" unfolding measure_spmf_def
     by(subst integral_distr)(auto simp add: integral_restrict_space)
   finally show ?thesis .
@@ -566,7 +566,7 @@
 
 lemma spmf_bind: "spmf (p \<bind> f) y = \<integral> x. spmf (f x) y \<partial>measure_spmf p"
 unfolding measure_spmf_def
-by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: integral_cong split: option.split)
+by(subst integral_distr)(auto simp add: bind_spmf_def pmf_bind integral_restrict_space indicator_eq_0_iff intro!: Bochner_Integration.integral_cong split: option.split)
 
 lemma ennreal_spmf_bind: "ennreal (spmf (p \<bind> f) x) = \<integral>\<^sup>+ y. spmf (f y) x \<partial>measure_spmf p"
 by(auto simp add: bind_spmf_def ennreal_pmf_bind nn_integral_measure_spmf_conv_measure_pmf nn_integral_restrict_space intro: nn_integral_cong split: split_indicator option.split)
@@ -2688,7 +2688,7 @@
 lemma pmf_try_spmf_None [simp]: "pmf (TRY p ELSE q) None = pmf p None * pmf q None" (is "?lhs = ?rhs")
 proof -
   have "?lhs = \<integral> x. pmf q None * indicator {None} x \<partial>measure_pmf p"
-    unfolding try_spmf_def pmf_bind by(rule integral_cong)(simp_all split: option.split)
+    unfolding try_spmf_def pmf_bind by(rule Bochner_Integration.integral_cong)(simp_all split: option.split)
   also have "\<dots> = ?rhs" by(simp add: measure_pmf_single)
   finally show ?thesis .
 qed
diff -r a6cd18af8bf9 -r 685fb01256af src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Thu Sep 15 22:41:05 2016 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy	Fri Sep 16 13:56:51 2016 +0200
@@ -263,7 +263,7 @@
   from lborel_integrable_real_affine[OF this, of t 0]
   show ?thesis
     unfolding interval_lebesgue_integral_0_infty
-    by (rule integrable_bound) (auto simp: field_simps * split: split_indicator)
+    by (rule Bochner_Integration.integrable_bound) (auto simp: field_simps * split: split_indicator)
 qed
 
 lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
@@ -291,7 +291,7 @@
         fix x :: real assume x: "x \<noteq> 0" "x \<noteq> t"
         have "LBINT y. \<bar>indicator ({0<..} \<times> {0<..<t}) (y, x) *\<^sub>R (sin x * exp (- (y * x)))\<bar> =
             LBINT y. \<bar>sin x\<bar> * exp (- (y * x)) * indicator {0<..} y * indicator {0<..<t} x"
-          by (intro integral_cong) (auto split: split_indicator simp: abs_mult)
+          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)
@@ -315,7 +315,7 @@
     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
-               split: split_indicator intro!: integral_cong)
+               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)
     also have "... = pi / 2 - (LBINT u=0..\<infinity>. exp (- (u * t)) * (u * sin t + cos t) / (1 + u^2))"