# HG changeset patch
# User hoelzl
# Date 1474648474 -7200
# Node ID f353674c2528a121ccbcc6f6ecd2404375bf71d2
# Parent  0d82c4c94014b5a6410cc6fde1ca9b101f55c7f7
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral

diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -2311,7 +2311,7 @@
 
 lemma integrableE:
   assumes "integrable M f"
-  obtains r q where
+  obtains r q where "0 \<le> r" "0 \<le> q"
     "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
     "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M) = ennreal q"
     "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -342,6 +342,7 @@
 lemma null_sets_restrict_space:
   "\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M"
   by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)
+
 lemma completion_ex_borel_measurable_real:
   fixes g :: "'a \<Rightarrow> real"
   assumes g: "g \<in> borel_measurable (completion M)"
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -5,7 +5,7 @@
 section \<open>Complex Analysis Basics\<close>
 
 theory Complex_Analysis_Basics
-imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
+imports Equivalence_Lebesgue_Henstock_Integration "~~/src/HOL/Library/Nonpos_Ints"
 begin
 
 
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -1,5 +1,10 @@
+(*  Title:      HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
+    Author:     Johannes Hölzl, TU München
+    Author:     Robert Himmelmann, TU München
+*)
+
 theory Equivalence_Lebesgue_Henstock_Integration
-  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure
+  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
 begin
 
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
@@ -650,34 +655,27 @@
     by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
 qed
 
+lemma ennreal_max_0: "ennreal (max 0 x) = ennreal x"
+  by (auto simp: max_def ennreal_neg)
+
 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
+proof -
+  from integrableE[OF f] obtain r q
+    where "0 \<le> r" "0 \<le> q"
+      and r: "(\<integral>\<^sup>+ x. ennreal (max 0 (f x)) \<partial>lborel) = ennreal r"
+      and q: "(\<integral>\<^sup>+ x. ennreal (max 0 (- f x)) \<partial>lborel) = ennreal q"
+      and f: "f \<in> borel_measurable lborel" and eq: "integral\<^sup>L lborel f = r - q"
+    unfolding ennreal_max_0 by auto
+  then have "((\<lambda>x. max 0 (f x)) has_integral r) UNIV" "((\<lambda>x. max 0 (- f x)) has_integral q) UNIV"
+    using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
+  note has_integral_sub[OF this]
+  moreover have "(\<lambda>x. max 0 (f x) - max 0 (- f x)) = f"
+    by auto
+  ultimately show ?thesis
+    by (simp add: eq)
 qed
 
 lemma has_integral_AE:
@@ -781,6 +779,997 @@
 
 end
 
+lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
+  by (auto simp: measurable_def)
+
+lemma integrable_completion:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
+  by (rule integrable_subalgebra[symmetric]) auto
+
+lemma integral_completion:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
+  by (rule integral_subalgebra[symmetric]) (auto intro: f)
+
+context
+begin
+
+private lemma has_integral_integral_lebesgue_real:
+  fixes f :: "'a::euclidean_space \<Rightarrow> real"
+  assumes f: "integrable lebesgue f"
+  shows "(f has_integral (integral\<^sup>L lebesgue f)) UNIV"
+proof -
+  obtain f' where f': "f' \<in> borel \<rightarrow>\<^sub>M borel" "AE x in lborel. f x = f' x"
+    using completion_ex_borel_measurable_real[OF borel_measurable_integrable[OF f]] by auto
+  moreover have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>lborel) = (\<integral>\<^sup>+ x. ennreal (norm (f' x)) \<partial>lborel)"
+    using f' by (intro nn_integral_cong_AE) auto
+  ultimately have "integrable lborel f'"
+    using f by (auto simp: integrable_iff_bounded nn_integral_completion cong: nn_integral_cong_AE)
+  note has_integral_integral_real[OF this]
+  moreover have "integral\<^sup>L lebesgue f = integral\<^sup>L lebesgue f'"
+    using f' f by (intro integral_cong_AE) (auto intro: AE_completion measurable_completion)
+  moreover have "integral\<^sup>L lebesgue f' = integral\<^sup>L lborel f'"
+    using f' by (simp add: integral_completion)
+  moreover have "(f' has_integral integral\<^sup>L lborel f') UNIV \<longleftrightarrow> (f has_integral integral\<^sup>L lborel f') UNIV"
+    using f' by (intro has_integral_AE) auto
+  ultimately show ?thesis
+    by auto
+qed
+
+lemma has_integral_integral_lebesgue:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "integrable lebesgue f"
+  shows "(f has_integral (integral\<^sup>L lebesgue 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 lebesgue (\<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_lebesgue_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 lebesgue (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lebesgue f"
+    using f by (subst (2) eq_f[symmetric]) simp
+  finally show ?thesis .
+qed
+
+lemma integrable_on_lebesgue:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "integrable lebesgue f \<Longrightarrow> f integrable_on UNIV"
+  using has_integral_integral_lebesgue by auto
+
+lemma integral_lebesgue:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "integrable lebesgue f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lebesgue)"
+  using has_integral_integral_lebesgue by auto
+
+end
+
+subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
+
+translations
+"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+translations
+"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+
+lemma set_integral_reflect:
+  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!: Bochner_Integration.integral_cong split: split_indicator)
+
+lemma borel_integrable_atLeastAtMost':
+  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
+  assumes f: "continuous_on {a..b} f"
+  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
+  by (intro borel_integrable_compact compact_Icc f)
+
+lemma integral_FTC_atLeastAtMost:
+  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
+  assumes "a \<le> b"
+    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
+    and f: "continuous_on {a .. b} f"
+  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
+proof -
+  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
+  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
+    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
+  moreover
+  have "(f has_integral F b - F a) {a .. b}"
+    by (intro fundamental_theorem_of_calculus ballI assms) auto
+  then have "(?f has_integral F b - F a) {a .. b}"
+    by (subst has_integral_cong[where g=f]) auto
+  then have "(?f has_integral F b - F a) UNIV"
+    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
+  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
+    by (rule has_integral_unique)
+qed
+
+lemma set_borel_integral_eq_integral:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "set_integrable lborel S f"
+  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
+proof -
+  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
+  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
+    by (rule has_integral_integral_lborel) fact
+  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
+    apply (subst has_integral_restrict_univ [symmetric])
+    apply (rule has_integral_eq)
+    by auto
+  thus "f integrable_on S"
+    by (auto simp add: integrable_on_def)
+  with 1 have "(f has_integral (integral S f)) S"
+    by (intro integrable_integral, auto simp add: integrable_on_def)
+  thus "LINT x : S | lborel. f x = integral S f"
+    by (intro has_integral_unique [OF 1])
+qed
+
+lemma has_integral_set_lebesgue:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "set_integrable lebesgue S f"
+  shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
+  using has_integral_integral_lebesgue[OF f]
+  by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_univ cong: if_cong)
+
+lemma set_lebesgue_integral_eq_integral:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "set_integrable lebesgue S f"
+  shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
+  using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
+
+abbreviation
+  absolutely_integrable_on :: "('a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
+  (infixr "absolutely'_integrable'_on" 46)
+  where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
+
+lemma absolutely_integrable_on_def:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
+proof safe
+  assume f: "f absolutely_integrable_on s"
+  then have nf: "integrable lebesgue (\<lambda>x. norm (indicator s x *\<^sub>R f x))"
+    by (intro integrable_norm)
+  note integrable_on_lebesgue[OF f] integrable_on_lebesgue[OF nf]
+  moreover have
+    "(\<lambda>x. indicator s x *\<^sub>R f x) = (\<lambda>x. if x \<in> s then f x else 0)"
+    "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
+    by auto
+  ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
+    by (simp_all add: integrable_restrict_univ)
+next
+  assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
+  show "f absolutely_integrable_on s"
+  proof (rule integrableI_bounded)
+    show "(\<lambda>x. indicator s x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+      using f has_integral_implies_lebesgue_measurable[of f _ s] by (auto simp: integrable_on_def)
+    show "(\<integral>\<^sup>+ x. ennreal (norm (indicator s x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
+      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ s]
+      by (auto simp: integrable_on_def nn_integral_completion)
+  qed
+qed
+
+lemma absolutely_integrable_onI:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
+  unfolding absolutely_integrable_on_def by auto
+
+lemma set_integral_norm_bound:
+  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
+  shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
+  using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by simp
+
+lemma set_integral_finite_UN_AE:
+  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes "finite I"
+    and ae: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> AE x in M. (x \<in> A i \<and> x \<in> A j) \<longrightarrow> i = j"
+    and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
+    and f: "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f"
+  shows "LINT x:(\<Union>i\<in>I. A i)|M. f x = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
+  using \<open>finite I\<close> order_refl[of I]
+proof (induction I rule: finite_subset_induct')
+  case (insert i I')
+  have "AE x in M. (\<forall>j\<in>I'. x \<in> A i \<longrightarrow> x \<notin> A j)"
+  proof (intro AE_ball_countable[THEN iffD2] ballI)
+    fix j assume "j \<in> I'"
+    with \<open>I' \<subseteq> I\<close> \<open>i \<notin> I'\<close> have "i \<noteq> j" "j \<in> I"
+      by auto
+    then show "AE x in M. x \<in> A i \<longrightarrow> x \<notin> A j"
+      using ae[of i j] \<open>i \<in> I\<close> by auto
+  qed (use \<open>finite I'\<close> in \<open>rule countable_finite\<close>)
+  then have "AE x\<in>A i in M. \<forall>xa\<in>I'. x \<notin> A xa "
+    by auto
+  with insert.hyps insert.IH[symmetric]
+  show ?case
+    by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
+qed simp
+
+lemma set_integrable_norm:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
+  using integrable_norm[OF f] by simp
+
+lemma absolutely_integrable_bounded_variation:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "f absolutely_integrable_on UNIV"
+  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
+proof (rule that[of "integral UNIV (\<lambda>x. norm (f x))"]; safe)
+  fix d :: "'a set set" assume d: "d division_of \<Union>d"
+  have *: "k \<in> d \<Longrightarrow> f absolutely_integrable_on k" for k
+    using f[THEN set_integrable_subset, of k] division_ofD(2,4)[OF d, of k] by auto
+  note d' = division_ofD[OF d]
+
+  have "(\<Sum>k\<in>d. norm (integral k f)) = (\<Sum>k\<in>d. norm (LINT x:k|lebesgue. f x))"
+    by (intro setsum.cong refl arg_cong[where f=norm] set_lebesgue_integral_eq_integral(2)[symmetric] *)
+  also have "\<dots> \<le> (\<Sum>k\<in>d. LINT x:k|lebesgue. norm (f x))"
+    by (intro setsum_mono set_integral_norm_bound *)
+  also have "\<dots> = (\<Sum>k\<in>d. integral k (\<lambda>x. norm (f x)))"
+    by (intro setsum.cong refl set_lebesgue_integral_eq_integral(2) set_integrable_norm *)
+  also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
+    using integrable_on_subdivision[OF d] assms f unfolding absolutely_integrable_on_def
+    by (subst integral_combine_division_topdown[OF _ d]) auto
+  also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
+    using integrable_on_subdivision[OF d] assms unfolding absolutely_integrable_on_def
+    by (intro integral_subset_le) auto
+  finally show "(\<Sum>k\<in>d. norm (integral k f)) \<le> integral UNIV (\<lambda>x. norm (f x))" .
+qed
+
+lemma helplemma:
+  assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
+    and "finite s"
+  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
+  unfolding setsum_subtractf[symmetric]
+  apply (rule le_less_trans[OF setsum_abs])
+  apply (rule le_less_trans[OF _ assms(1)])
+  apply (rule setsum_mono)
+  apply (rule norm_triangle_ineq3)
+  done
+
+lemma bounded_variation_absolutely_integrable_interval:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes f: "f integrable_on cbox a b"
+    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+  shows "f absolutely_integrable_on cbox a b"
+proof -
+  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
+  have D_1: "?D \<noteq> {}"
+    by (rule elementary_interval[of a b]) auto
+  have D_2: "bdd_above (?f`?D)"
+    by (metis * mem_Collect_eq bdd_aboveI2)
+  note D = D_1 D_2
+  let ?S = "SUP x:?D. ?f x"
+  show ?thesis
+    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
+    apply (subst has_integral[of _ ?S])
+    apply safe
+  proof goal_cases
+    case e: (1 e)
+    then have "?S - e / 2 < ?S" by simp
+    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
+      unfolding less_cSUP_iff[OF D] by auto
+    note d' = division_ofD[OF this(1)]
+
+    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
+    proof
+      fix x
+      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
+        apply (rule separate_point_closed)
+        apply (rule closed_Union)
+        apply (rule finite_subset[OF _ d'(1)])
+        using d'(4)
+        apply auto
+        done
+      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
+        by force
+    qed
+    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
+
+    have "e/2 > 0"
+      using e by auto
+    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
+    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
+    show ?case
+      apply (rule_tac x="?g" in exI)
+      apply safe
+    proof -
+      show "gauge ?g"
+        using g(1) k(1)
+        unfolding gauge_def
+        by auto
+      fix p
+      assume "p tagged_division_of (cbox a b)" and "?g fine p"
+      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
+      note p' = tagged_division_ofD[OF p(1)]
+      define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
+      have gp': "g fine p'"
+        using p(2)
+        unfolding p'_def fine_def
+        by auto
+      have p'': "p' tagged_division_of (cbox a b)"
+        apply (rule tagged_division_ofI)
+      proof -
+        show "finite p'"
+          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
+            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
+          unfolding p'_def
+          defer
+          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
+          apply safe
+          unfolding image_iff
+          apply (rule_tac x="(i,x,l)" in bexI)
+          apply auto
+          done
+        fix x k
+        assume "(x, k) \<in> p'"
+        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+          unfolding p'_def by auto
+        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        show "x \<in> k" and "k \<subseteq> cbox a b"
+          using p'(2-3)[OF il(3)] il by auto
+        show "\<exists>a b. k = cbox a b"
+          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
+          apply safe
+          unfolding inter_interval
+          apply auto
+          done
+      next
+        fix x1 k1
+        assume "(x1, k1) \<in> p'"
+        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
+          unfolding p'_def by auto
+        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
+        fix x2 k2
+        assume "(x2,k2)\<in>p'"
+        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
+          unfolding p'_def by auto
+        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
+        assume "(x1, k1) \<noteq> (x2, k2)"
+        then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
+          unfolding il1 il2
+          by auto
+        then show "interior k1 \<inter> interior k2 = {}"
+          unfolding il1 il2 by auto
+      next
+        have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
+          unfolding p'_def using d' by auto
+        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
+          apply rule
+          apply (rule Union_least)
+          unfolding mem_Collect_eq
+          apply (erule exE)
+          apply (drule *[rule_format])
+          apply safe
+        proof -
+          fix y
+          assume y: "y \<in> cbox a b"
+          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
+            unfolding p'(6)[symmetric] by auto
+          then guess x l by (elim exE) note xl=conjunctD2[OF this]
+          then have "\<exists>k. k \<in> d \<and> y \<in> k"
+            using y unfolding d'(6)[symmetric] by auto
+          then guess i .. note i = conjunctD2[OF this]
+          have "x \<in> i"
+            using fineD[OF p(3) xl(1)]
+            using k(2)[OF i(1), of x]
+            using i(2) xl(2)
+            by auto
+          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
+            unfolding p'_def Union_iff
+            apply (rule_tac x="i \<inter> l" in bexI)
+            using i xl
+            apply auto
+            done
+        qed
+      qed
+
+      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+        apply -
+        apply (rule g(2)[rule_format])
+        unfolding tagged_division_of_def
+        apply safe
+        apply (rule gp')
+        done
+      then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
+        unfolding split_def
+        using p''
+        by (force intro!: helplemma)
+
+      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
+      proof (safe, goal_cases)
+        case prems: (2 _ _ x i l)
+        have "x \<in> i"
+          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
+          by auto
+        then have "(x, i \<inter> l) \<in> p'"
+          unfolding p'_def
+          using prems
+          apply safe
+          apply (rule_tac x=x in exI)
+          apply (rule_tac x="i \<inter> l" in exI)
+          apply safe
+          using prems
+          apply auto
+          done
+        then show ?case
+          using prems(3) by auto
+      next
+        fix x k
+        assume "(x, k) \<in> p'"
+        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
+          unfolding p'_def by auto
+        then guess i l by (elim exE) note il=conjunctD4[OF this]
+        then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
+          apply (rule_tac x=x in exI)
+          apply (rule_tac x=i in exI)
+          apply (rule_tac x=l in exI)
+          using p'(2)[OF il(3)]
+          apply auto
+          done
+      qed
+      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
+        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
+        unfolding norm_eq_zero
+        apply (rule integral_null)
+        apply assumption
+        apply rule
+        done
+      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
+
+      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
+        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
+        by arith
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
+        unfolding real_norm_def
+        apply (rule *[rule_format,OF **])
+        apply safe
+        apply(rule d(2))
+      proof goal_cases
+        case 1
+        show ?case
+          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
+      next
+        case 2
+        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
+          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
+          by auto
+        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
+        proof (rule setsum_mono, goal_cases)
+          case k: (1 k)
+          from d'(4)[OF this] guess u v by (elim exE) note uv=this
+          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
+          note uvab = d'(2)[OF k[unfolded uv]]
+          have "d' division_of cbox u v"
+            apply (subst d'_def)
+            apply (rule division_inter_1)
+            apply (rule division_of_tagged_division[OF p(1)])
+            apply (rule uvab)
+            done
+          then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
+            unfolding uv
+            apply (subst integral_combine_division_topdown[of _ _ d'])
+            apply (rule integrable_on_subcbox[OF assms(1) uvab])
+            apply assumption
+            apply (rule setsum_norm_le)
+            apply auto
+            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 Setcompr_eq_image)
+            apply (rule finite_imageI)+
+            apply fact
+            unfolding d'_def uv
+            apply blast
+          proof (rule, goal_cases)
+            case prems: (1 i)
+            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
+              by auto
+            from this[unfolded mem_Collect_eq] guess l .. note l=this
+            then have "cbox u v \<inter> l = {}"
+              using prems by auto
+            then show ?case
+              using l by auto
+          qed
+          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
+            unfolding Setcompr_eq_image
+            apply (rule setsum.reindex_nontrivial [unfolded o_def])
+            apply (rule finite_imageI)
+            apply (rule p')
+          proof goal_cases
+            case prems: (1 l y)
+            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
+              apply (subst(2) interior_Int)
+              apply (rule Int_greatest)
+              defer
+              apply (subst prems(4))
+              apply auto
+              done
+            then have *: "interior (k \<inter> l) = {}"
+              using snd_p(5)[OF prems(1-3)] by auto
+            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
+            show ?case
+              using *
+              unfolding uv inter_interval content_eq_0_interior[symmetric]
+              by auto
+          qed
+          finally show ?case .
+        qed
+        also have "\<dots> = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))"
+          apply (subst sum_sum_product[symmetric])
+          apply fact
+          using p'(1)
+          apply auto
+          done
+        also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
+          unfolding split_def ..
+        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
+          unfolding *
+          apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
+          apply (rule finite_product_dependent)
+          apply fact
+          apply (rule finite_imageI)
+          apply (rule p')
+          unfolding split_paired_all mem_Collect_eq split_conv o_def
+        proof -
+          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
+          fix l1 l2 k1 k2
+          assume as:
+            "(l1, k1) \<noteq> (l2, k2)"
+            "l1 \<inter> k1 = l2 \<inter> k2"
+            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
+            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
+          then have "l1 \<in> d" and "k1 \<in> snd ` p"
+            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
+          guess u1 v1 u2 v2 by (elim exE) note uv=this
+          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+            using as by auto
+          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+            apply -
+            apply (erule disjE)
+            apply (rule disjI2)
+            apply (rule d'(5))
+            prefer 4
+            apply (rule disjI1)
+            apply (rule *)
+            using as
+            apply auto
+            done
+          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+            using as(2) by auto
+          ultimately have "interior(l1 \<inter> k1) = {}"
+            by auto
+          then show "norm (integral (l1 \<inter> k1) f) = 0"
+            unfolding uv inter_interval
+            unfolding content_eq_0_interior[symmetric]
+            by auto
+        qed
+        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
+          unfolding sum_p'
+          apply (rule setsum.mono_neutral_right)
+          apply (subst *)
+          apply (rule finite_imageI[OF finite_product_dependent])
+          apply fact
+          apply (rule finite_imageI[OF p'(1)])
+          apply safe
+        proof goal_cases
+          case (2 i ia l a b)
+          then have "ia \<inter> b = {}"
+            unfolding p'alt image_iff Bex_def not_ex
+            apply (erule_tac x="(a, ia \<inter> b)" in allE)
+            apply auto
+            done
+          then show ?case
+            by auto
+        next
+          case (1 x a b)
+          then show ?case
+            unfolding p'_def
+            apply safe
+            apply (rule_tac x=i in exI)
+            apply (rule_tac x=l in exI)
+            unfolding snd_conv image_iff
+            apply safe
+            apply (rule_tac x="(a,l)" in bexI)
+            apply auto
+            done
+        qed
+        finally show ?case .
+      next
+        case 3
+        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
+        have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
+          by auto
+        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
+          apply safe
+          unfolding image_iff
+          apply (rule_tac x="((x,l),i)" in bexI)
+          apply auto
+          done
+        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
+        have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
+          unfolding norm_scaleR
+          apply (rule setsum.mono_neutral_left)
+          apply (subst *)
+          apply (rule finite_imageI)
+          apply fact
+          unfolding p'alt
+          apply blast
+          apply safe
+          apply (rule_tac x=x in exI)
+          apply (rule_tac x=i in exI)
+          apply (rule_tac x=l in exI)
+          apply auto
+          done
+        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
+          unfolding *
+          apply (subst setsum.reindex_nontrivial)
+          apply fact
+          unfolding split_paired_all
+          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
+          apply (elim conjE)
+        proof -
+          fix x1 l1 k1 x2 l2 k2
+          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
+            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
+          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
+          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
+            by auto
+          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
+            apply -
+            apply (erule disjE)
+            apply (rule disjI2)
+            defer
+            apply (rule disjI1)
+            apply (rule d'(5)[OF as(3-4)])
+            apply assumption
+            apply (rule p'(5)[OF as(1-2)])
+            apply auto
+            done
+          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
+            unfolding  as ..
+          ultimately have "interior (l1 \<inter> k1) = {}"
+            by auto
+          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
+            unfolding uv inter_interval
+            unfolding content_eq_0_interior[symmetric]
+            by auto
+        qed safe
+        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
+          unfolding Sigma_alt
+          apply (subst sum_sum_product[symmetric])
+          apply (rule p')
+          apply rule
+          apply (rule d')
+          apply (rule setsum.cong)
+          apply (rule refl)
+          unfolding split_paired_all split_conv
+        proof -
+          fix x l
+          assume as: "(x, l) \<in> p"
+          note xl = p'(2-4)[OF this]
+          from this(3) guess u v by (elim exE) note uv=this
+          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
+            apply (rule setsum.cong)
+            apply (rule refl)
+            apply (drule d'(4))
+            apply safe
+            apply (subst Int_commute)
+            unfolding inter_interval uv
+            apply (subst abs_of_nonneg)
+            apply auto
+            done
+          also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
+            unfolding Setcompr_eq_image
+            apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
+            apply (rule d')
+          proof goal_cases
+            case prems: (1 k y)
+            from d'(4)[OF this(1)] d'(4)[OF this(2)]
+            guess u1 v1 u2 v2 by (elim exE) note uv=this
+            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
+              apply (subst interior_Int)
+              using d'(5)[OF prems(1-3)]
+              apply auto
+              done
+            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
+              by auto
+            also have "\<dots> = interior (k \<inter> cbox u v)"
+              unfolding prems(4) by auto
+            finally show ?case
+              unfolding uv inter_interval content_eq_0_interior ..
+          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 Setcompr_eq_image
+            apply (rule finite_imageI)
+            apply (rule d')
+            apply blast
+            apply safe
+            apply (rule_tac x=k in exI)
+          proof goal_cases
+            case prems: (1 i k)
+            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
+            have "interior (k \<inter> cbox u v) \<noteq> {}"
+              using prems(2)
+              unfolding ab inter_interval content_eq_0_interior
+              by auto
+            then show ?case
+              using prems(1)
+              using interior_subset[of "k \<inter> cbox u v"]
+              by auto
+          qed
+          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
+            unfolding setsum_distrib_right[symmetric] real_scaleR_def
+            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
+            using xl(2)[unfolded uv]
+            unfolding uv
+            apply auto
+            done
+        qed
+        finally show ?case .
+      qed
+    qed
+  qed
+qed
+
+lemma bounded_variation_absolutely_integrable:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "f integrable_on UNIV"
+    and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
+  shows "f absolutely_integrable_on UNIV"
+proof (rule absolutely_integrable_onI, fact, rule)
+  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
+  have D_1: "?D \<noteq> {}"
+    by (rule elementary_interval) auto
+  have D_2: "bdd_above (?f`?D)"
+    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
+  note D = D_1 D_2
+  let ?S = "SUP d:?D. ?f d"
+  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
+    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
+    apply (rule integrable_on_subcbox[OF assms(1)])
+    defer
+    apply safe
+    apply (rule assms(2)[rule_format])
+    apply auto
+    done
+  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
+    apply (subst has_integral_alt')
+    apply safe
+  proof goal_cases
+    case (1 a b)
+    show ?case
+      using f_int[of a b] unfolding absolutely_integrable_on_def by auto
+  next
+    case prems: (2 e)
+    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      then have "?S \<le> ?S - e"
+        by (intro cSUP_least[OF D(1)]) auto
+      then show False
+        using prems by auto
+    qed
+    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
+      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
+      by (auto simp add: image_iff not_le)
+    from this(1) obtain d where "d division_of \<Union>d"
+      and "K = (\<Sum>k\<in>d. norm (integral k f))"
+      by auto
+    note d = this(1) *(2)[unfolded this(2)]
+    note d'=division_ofD[OF this(1)]
+    have "bounded (\<Union>d)"
+      by (rule elementary_bounded,fact)
+    from this[unfolded bounded_pos] obtain K where
+       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
+    show ?case
+      apply (rule_tac x="K + 1" in exI)
+      apply safe
+    proof -
+      fix a b :: 'n
+      assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
+      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
+        by arith
+      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
+        unfolding real_norm_def
+        apply (rule *[rule_format])
+        apply safe
+        apply (rule d(2))
+      proof goal_cases
+        case 1
+        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
+          apply (intro setsum_mono)
+          subgoal for k
+            using d'(4)[of k] f_int
+            by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
+          done
+        also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
+          apply (rule integral_combine_division_bottomup[symmetric])
+          apply (rule d)
+          unfolding forall_in_division[OF d(1)]
+          using f_int unfolding absolutely_integrable_on_def
+          apply auto
+          done
+        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
+        proof -
+          have "\<Union>d \<subseteq> cbox a b"
+            apply rule
+            apply (drule K(2)[rule_format])
+            apply (rule ab[unfolded subset_eq,rule_format])
+            apply (auto simp add: dist_norm)
+            done
+          then show ?thesis
+            apply -
+            apply (subst if_P)
+            apply rule
+            apply (rule integral_subset_le)
+            defer
+            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
+            apply (rule d)
+            using f_int[of a b] unfolding absolutely_integrable_on_def
+            apply auto
+            done
+        qed
+        finally show ?case .
+      next
+        note f' = f_int[of a b, unfolded absolutely_integrable_on_def]
+        note f = f'[THEN conjunct1] f'[THEN conjunct2]
+        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
+        have "e/2>0"
+          using \<open>e > 0\<close> by auto
+        from * [OF this] obtain d1 where
+          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
+            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
+          by auto
+        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
+          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
+            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
+         obtain p where
+          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
+          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
+            (auto simp add: fine_inter)
+        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
+          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
+          by arith
+        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
+          apply (subst if_P)
+          apply rule
+        proof (rule *[rule_format])
+          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
+            unfolding split_def
+            apply (rule helplemma)
+            using d2(2)[rule_format,of p]
+            using p(1,3)
+            unfolding tagged_division_of_def split_def
+            apply auto
+            done
+          show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
+            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
+            by (simp only: real_norm_def)
+          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
+            apply (rule setsum.cong)
+            apply (rule refl)
+            unfolding split_paired_all split_conv
+            apply (drule tagged_division_ofD(4)[OF p(1)])
+            unfolding norm_scaleR
+            apply (subst abs_of_nonneg)
+            apply auto
+            done
+          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
+            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
+            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
+            apply (simp add: integral_null)
+            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
+            apply (auto simp: tagged_partial_division_of_def)
+            done
+        qed
+      qed
+    qed (insert K, auto)
+  qed
+qed
+
+lemma absolutely_integrable_restrict_univ:
+  "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
+  by (intro arg_cong2[where f=integrable]) auto
+
+lemma absolutely_integrable_add[intro]:
+  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
+  by (rule set_integral_add)
+
+lemma absolutely_integrable_sub[intro]:
+  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
+  by (rule set_integral_diff)
+
+lemma absolutely_integrable_linear:
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+    and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
+  shows "f absolutely_integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on s"
+  using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
+  by (simp add: linear_simps[of h])
+
+lemma absolutely_integrable_setsum:
+  fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "finite t" and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
+  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
+  using assms(1,2) by induct auto
+
+lemma absolutely_integrable_integrable_bound:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes le: "\<forall>x\<in>s. norm (f x) \<le> g x" and f: "f integrable_on s" and g: "g integrable_on s"
+  shows "f absolutely_integrable_on s"
+proof (rule Bochner_Integration.integrable_bound)
+  show "g absolutely_integrable_on s"
+    unfolding absolutely_integrable_on_def
+  proof
+    show "(\<lambda>x. norm (g x)) integrable_on s"
+      using le norm_ge_zero[of "f _"]
+      by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
+         (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
+  qed fact
+  show "set_borel_measurable lebesgue s f"
+    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
+qed (use le in \<open>auto intro!: always_eventually split: split_indicator\<close>)
+
+subsection \<open>Dominated convergence\<close>
+
+lemma dominated_convergence:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
+    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
+    and conv: "\<forall>x \<in> s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+  shows "g integrable_on s" "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+proof -
+  have 3: "h absolutely_integrable_on s"
+    unfolding absolutely_integrable_on_def
+  proof
+    show "(\<lambda>x. norm (h x)) integrable_on s"
+    proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
+      fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
+        using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
+    qed auto
+  qed fact
+  have 2: "set_borel_measurable lebesgue s (f k)" for k
+    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
+  then have 1: "set_borel_measurable lebesgue s g"
+    by (rule borel_measurable_LIMSEQ_metric) (use conv in \<open>auto split: split_indicator\<close>)
+  have 4: "AE x in lebesgue. (\<lambda>i. indicator s x *\<^sub>R f i x) \<longlonglongrightarrow> indicator s x *\<^sub>R g x"
+    "AE x in lebesgue. norm (indicator s x *\<^sub>R f k x) \<le> indicator s x *\<^sub>R h x" for k
+    using conv le by (auto intro!: always_eventually split: split_indicator)
+
+  have g: "g absolutely_integrable_on s"
+    using 1 2 3 4 by (rule integrable_dominated_convergence)
+  then show "g integrable_on s"
+    by (auto simp: absolutely_integrable_on_def)
+  have "(\<lambda>k. (LINT x:s|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:s|lebesgue. g x)"
+    using 1 2 3 4 by (rule integral_dominated_convergence)
+  then show "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
+    using g absolutely_integrable_integrable_bound[OF le f h]
+    by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
+qed
+
+lemma has_integral_dominated_convergence:
+  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
+  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
+    "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
+    and x: "y \<longlonglongrightarrow> x"
+  shows "(g has_integral x) s"
+proof -
+  have int_f: "\<And>k. (f k) integrable_on s"
+    using assms by (auto simp: integrable_on_def)
+  have "(g has_integral (integral s g)) s"
+    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
+  moreover have "integral s g = x"
+  proof (rule LIMSEQ_unique)
+    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
+      using integral_unique[OF assms(1)] x by simp
+    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
+      by (intro dominated_convergence[OF int_f assms(2)]) fact+
+  qed
+  ultimately show ?thesis
+    by simp
+qed
+
 subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
 
 text \<open>
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -6180,7 +6180,7 @@
 unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
 using assms
 by auto
- 
+
 
 lemma integrable_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -9608,31 +9608,6 @@
     by auto
 qed
 
-
-subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
-
-definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46)
-  where "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
-
-lemma absolutely_integrable_onI[intro?]:
-  "f integrable_on s \<Longrightarrow>
-    (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def
-  by auto
-
-lemma absolutely_integrable_onD[dest]:
-  assumes "f absolutely_integrable_on s"
-  shows "f integrable_on s"
-    and "(\<lambda>x. norm (f x)) integrable_on s"
-  using assms
-  unfolding absolutely_integrable_on_def
-  by auto
-
-(*lemma absolutely_integrable_on_trans[simp]:
-  fixes f::"'n::euclidean_space \<Rightarrow> real"
-  shows "(vec1 \<circ> f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def o_def by auto*)
-
 lemma integral_norm_bound_integral:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on s"
@@ -9768,1174 +9743,6 @@
   using assms
   by auto
 
-lemma absolutely_integrable_le:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f absolutely_integrable_on s"
-  shows "norm (integral s f) \<le> integral s (\<lambda>x. norm (f x))"
-  apply (rule integral_norm_bound_integral)
-  using assms
-  apply auto
-  done
-
-lemma absolutely_integrable_0[intro]:
-  "(\<lambda>x. 0) absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def
-  by auto
-
-lemma absolutely_integrable_cmul[intro]:
-  "f absolutely_integrable_on s \<Longrightarrow>
-    (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def
-  using integrable_cmul[of f s c]
-  using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
-  by auto
-
-lemma absolutely_integrable_neg[intro]:
-  "f absolutely_integrable_on s \<Longrightarrow>
-    (\<lambda>x. -f(x)) absolutely_integrable_on s"
-  apply (drule absolutely_integrable_cmul[where c="-1"])
-  apply auto
-  done
-
-lemma absolutely_integrable_norm[intro]:
-  "f absolutely_integrable_on s \<Longrightarrow>
-    (\<lambda>x. norm (f x)) absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def
-  by auto
-
-lemma absolutely_integrable_abs[intro]:
-  "f absolutely_integrable_on s \<Longrightarrow>
-    (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
-  apply (drule absolutely_integrable_norm)
-  unfolding real_norm_def
-  apply assumption
-  done
-
-lemma absolutely_integrable_on_subinterval:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  shows "f absolutely_integrable_on s \<Longrightarrow>
-    cbox a b \<subseteq> s \<Longrightarrow> f absolutely_integrable_on cbox a b"
-  unfolding absolutely_integrable_on_def
-  by (metis integrable_on_subcbox)
-
-lemma absolutely_integrable_bounded_variation:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "f absolutely_integrable_on UNIV"
-  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
-  apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
-  apply safe
-proof goal_cases
-  case prems: (1 d)
-  note d = division_ofD[OF prems(2)]
-  have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
-    apply (rule setsum_mono,rule absolutely_integrable_le)
-    apply (drule d(4))
-    apply safe
-    apply (rule absolutely_integrable_on_subinterval[OF assms])
-    apply auto
-    done
-  also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
-    apply (subst integral_combine_division_topdown[OF _ prems(2)])
-    using integrable_on_subdivision[OF prems(2)]
-    using assms
-    apply auto
-    done
-  also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
-    apply (rule integral_subset_le)
-    using integrable_on_subdivision[OF prems(2)]
-    using assms
-    apply auto
-    done
-  finally show ?case .
-qed
-
-lemma helplemma:
-  assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
-    and "finite s"
-  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
-  unfolding setsum_subtractf[symmetric]
-  apply (rule le_less_trans[OF setsum_abs])
-  apply (rule le_less_trans[OF _ assms(1)])
-  apply (rule setsum_mono)
-  apply (rule norm_triangle_ineq3)
-  done
-
-lemma bounded_variation_absolutely_integrable_interval:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes f: "f integrable_on cbox a b"
-    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
-  shows "f absolutely_integrable_on cbox a b"
-proof -
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
-  have D_1: "?D \<noteq> {}"
-    by (rule elementary_interval[of a b]) auto
-  have D_2: "bdd_above (?f`?D)"
-    by (metis * mem_Collect_eq bdd_aboveI2)
-  note D = D_1 D_2
-  let ?S = "SUP x:?D. ?f x"
-  show ?thesis
-    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
-    apply (subst has_integral[of _ ?S])
-    apply safe
-  proof goal_cases
-    case e: (1 e)
-    then have "?S - e / 2 < ?S" by simp
-    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
-      unfolding less_cSUP_iff[OF D] by auto
-    note d' = division_ofD[OF this(1)]
-
-    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
-    proof
-      fix x
-      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
-        apply (rule separate_point_closed)
-        apply (rule closed_Union)
-        apply (rule finite_subset[OF _ d'(1)])
-        using d'(4)
-        apply auto
-        done
-      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
-        by force
-    qed
-    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
-
-    have "e/2 > 0"
-      using e by auto
-    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
-    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
-    show ?case
-      apply (rule_tac x="?g" in exI)
-      apply safe
-    proof -
-      show "gauge ?g"
-        using g(1) k(1)
-        unfolding gauge_def
-        by auto
-      fix p
-      assume "p tagged_division_of (cbox a b)" and "?g fine p"
-      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
-      note p' = tagged_division_ofD[OF p(1)]
-      define p' where "p' = {(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
-      have gp': "g fine p'"
-        using p(2)
-        unfolding p'_def fine_def
-        by auto
-      have p'': "p' tagged_division_of (cbox a b)"
-        apply (rule tagged_division_ofI)
-      proof -
-        show "finite p'"
-          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
-            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
-          unfolding p'_def
-          defer
-          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="(i,x,l)" in bexI)
-          apply auto
-          done
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
-          unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
-        show "x \<in> k" and "k \<subseteq> cbox a b"
-          using p'(2-3)[OF il(3)] il by auto
-        show "\<exists>a b. k = cbox a b"
-          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
-          apply safe
-          unfolding inter_interval
-          apply auto
-          done
-      next
-        fix x1 k1
-        assume "(x1, k1) \<in> p'"
-        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
-          unfolding p'_def by auto
-        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
-        fix x2 k2
-        assume "(x2,k2)\<in>p'"
-        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
-          unfolding p'_def by auto
-        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
-        assume "(x1, k1) \<noteq> (x2, k2)"
-        then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
-          unfolding il1 il2
-          by auto
-        then show "interior k1 \<inter> interior k2 = {}"
-          unfolding il1 il2 by auto
-      next
-        have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
-          unfolding p'_def using d' by auto
-        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
-          apply rule
-          apply (rule Union_least)
-          unfolding mem_Collect_eq
-          apply (erule exE)
-          apply (drule *[rule_format])
-          apply safe
-        proof -
-          fix y
-          assume y: "y \<in> cbox a b"
-          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
-            unfolding p'(6)[symmetric] by auto
-          then guess x l by (elim exE) note xl=conjunctD2[OF this]
-          then have "\<exists>k. k \<in> d \<and> y \<in> k"
-            using y unfolding d'(6)[symmetric] by auto
-          then guess i .. note i = conjunctD2[OF this]
-          have "x \<in> i"
-            using fineD[OF p(3) xl(1)]
-            using k(2)[OF i(1), of x]
-            using i(2) xl(2)
-            by auto
-          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
-            unfolding p'_def Union_iff
-            apply (rule_tac x="i \<inter> l" in bexI)
-            using i xl
-            apply auto
-            done
-        qed
-      qed
-
-      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
-        apply -
-        apply (rule g(2)[rule_format])
-        unfolding tagged_division_of_def
-        apply safe
-        apply (rule gp')
-        done
-      then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
-        unfolding split_def
-        using p''
-        by (force intro!: helplemma)
-
-      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
-      proof (safe, goal_cases)
-        case prems: (2 _ _ x i l)
-        have "x \<in> i"
-          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
-          by auto
-        then have "(x, i \<inter> l) \<in> p'"
-          unfolding p'_def
-          using prems
-          apply safe
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x="i \<inter> l" in exI)
-          apply safe
-          using prems
-          apply auto
-          done
-        then show ?case
-          using prems(3) by auto
-      next
-        fix x k
-        assume "(x, k) \<in> p'"
-        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
-          unfolding p'_def by auto
-        then guess i l by (elim exE) note il=conjunctD4[OF this]
-        then show "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x=i in exI)
-          apply (rule_tac x=l in exI)
-          using p'(2)[OF il(3)]
-          apply auto
-          done
-      qed
-      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
-        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
-        unfolding norm_eq_zero
-        apply (rule integral_null)
-        apply assumption
-        apply rule
-        done
-      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
-
-      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
-        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
-        by arith
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
-        unfolding real_norm_def
-        apply (rule *[rule_format,OF **])
-        apply safe
-        apply(rule d(2))
-      proof goal_cases
-        case 1
-        show ?case
-          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
-      next
-        case 2
-        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
-          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
-          by auto
-        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
-        proof (rule setsum_mono, goal_cases)
-          case k: (1 k)
-          from d'(4)[OF this] guess u v by (elim exE) note uv=this
-          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
-          note uvab = d'(2)[OF k[unfolded uv]]
-          have "d' division_of cbox u v"
-            apply (subst d'_def)
-            apply (rule division_inter_1)
-            apply (rule division_of_tagged_division[OF p(1)])
-            apply (rule uvab)
-            done
-          then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
-            unfolding uv
-            apply (subst integral_combine_division_topdown[of _ _ d'])
-            apply (rule integrable_on_subcbox[OF assms(1) uvab])
-            apply assumption
-            apply (rule setsum_norm_le)
-            apply auto
-            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 Setcompr_eq_image)
-            apply (rule finite_imageI)+
-            apply fact
-            unfolding d'_def uv
-            apply blast
-          proof (rule, goal_cases)
-            case prems: (1 i)
-            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
-              by auto
-            from this[unfolded mem_Collect_eq] guess l .. note l=this
-            then have "cbox u v \<inter> l = {}"
-              using prems by auto
-            then show ?case
-              using l by auto
-          qed
-          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
-            unfolding Setcompr_eq_image
-            apply (rule setsum.reindex_nontrivial [unfolded o_def])
-            apply (rule finite_imageI)
-            apply (rule p')
-          proof goal_cases
-            case prems: (1 l y)
-            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
-              apply (subst(2) interior_Int)
-              apply (rule Int_greatest)
-              defer
-              apply (subst prems(4))
-              apply auto
-              done
-            then have *: "interior (k \<inter> l) = {}"
-              using snd_p(5)[OF prems(1-3)] by auto
-            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-            show ?case
-              using *
-              unfolding uv inter_interval content_eq_0_interior[symmetric]
-              by auto
-          qed
-          finally show ?case .
-        qed
-        also have "\<dots> = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))"
-          apply (subst sum_sum_product[symmetric])
-          apply fact
-          using p'(1)
-          apply auto
-          done
-        also have "\<dots> = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (case_prod op \<inter> x) f))"
-          unfolding split_def ..
-        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
-          unfolding *
-          apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
-          apply (rule finite_product_dependent)
-          apply fact
-          apply (rule finite_imageI)
-          apply (rule p')
-          unfolding split_paired_all mem_Collect_eq split_conv o_def
-        proof -
-          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
-          fix l1 l2 k1 k2
-          assume as:
-            "(l1, k1) \<noteq> (l2, k2)"
-            "l1 \<inter> k1 = l2 \<inter> k2"
-            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
-          then have "l1 \<in> d" and "k1 \<in> snd ` p"
-            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
-          guess u1 v1 u2 v2 by (elim exE) note uv=this
-          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-            using as by auto
-          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            apply -
-            apply (erule disjE)
-            apply (rule disjI2)
-            apply (rule d'(5))
-            prefer 4
-            apply (rule disjI1)
-            apply (rule *)
-            using as
-            apply auto
-            done
-          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-            using as(2) by auto
-          ultimately have "interior(l1 \<inter> k1) = {}"
-            by auto
-          then show "norm (integral (l1 \<inter> k1) f) = 0"
-            unfolding uv inter_interval
-            unfolding content_eq_0_interior[symmetric]
-            by auto
-        qed
-        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
-          unfolding sum_p'
-          apply (rule setsum.mono_neutral_right)
-          apply (subst *)
-          apply (rule finite_imageI[OF finite_product_dependent])
-          apply fact
-          apply (rule finite_imageI[OF p'(1)])
-          apply safe
-        proof goal_cases
-          case (2 i ia l a b)
-          then have "ia \<inter> b = {}"
-            unfolding p'alt image_iff Bex_def not_ex
-            apply (erule_tac x="(a, ia \<inter> b)" in allE)
-            apply auto
-            done
-          then show ?case
-            by auto
-        next
-          case (1 x a b)
-          then show ?case
-            unfolding p'_def
-            apply safe
-            apply (rule_tac x=i in exI)
-            apply (rule_tac x=l in exI)
-            unfolding snd_conv image_iff
-            apply safe
-            apply (rule_tac x="(a,l)" in bexI)
-            apply auto
-            done
-        qed
-        finally show ?case .
-      next
-        case 3
-        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
-        have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
-          by auto
-        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
-          apply safe
-          unfolding image_iff
-          apply (rule_tac x="((x,l),i)" in bexI)
-          apply auto
-          done
-        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
-        have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
-          unfolding norm_scaleR
-          apply (rule setsum.mono_neutral_left)
-          apply (subst *)
-          apply (rule finite_imageI)
-          apply fact
-          unfolding p'alt
-          apply blast
-          apply safe
-          apply (rule_tac x=x in exI)
-          apply (rule_tac x=i in exI)
-          apply (rule_tac x=l in exI)
-          apply auto
-          done
-        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
-          unfolding *
-          apply (subst setsum.reindex_nontrivial)
-          apply fact
-          unfolding split_paired_all
-          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
-          apply (elim conjE)
-        proof -
-          fix x1 l1 k1 x2 l2 k2
-          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
-            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
-          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
-          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
-            by auto
-          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
-            apply -
-            apply (erule disjE)
-            apply (rule disjI2)
-            defer
-            apply (rule disjI1)
-            apply (rule d'(5)[OF as(3-4)])
-            apply assumption
-            apply (rule p'(5)[OF as(1-2)])
-            apply auto
-            done
-          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
-            unfolding  as ..
-          ultimately have "interior (l1 \<inter> k1) = {}"
-            by auto
-          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
-            unfolding uv inter_interval
-            unfolding content_eq_0_interior[symmetric]
-            by auto
-        qed safe
-        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
-          unfolding Sigma_alt
-          apply (subst sum_sum_product[symmetric])
-          apply (rule p')
-          apply rule
-          apply (rule d')
-          apply (rule setsum.cong)
-          apply (rule refl)
-          unfolding split_paired_all split_conv
-        proof -
-          fix x l
-          assume as: "(x, l) \<in> p"
-          note xl = p'(2-4)[OF this]
-          from this(3) guess u v by (elim exE) note uv=this
-          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
-            apply (rule setsum.cong)
-            apply (rule refl)
-            apply (drule d'(4))
-            apply safe
-            apply (subst Int_commute)
-            unfolding inter_interval uv
-            apply (subst abs_of_nonneg)
-            apply auto
-            done
-          also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
-            unfolding Setcompr_eq_image
-            apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
-            apply (rule d')
-          proof goal_cases
-            case prems: (1 k y)
-            from d'(4)[OF this(1)] d'(4)[OF this(2)]
-            guess u1 v1 u2 v2 by (elim exE) note uv=this
-            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
-              apply (subst interior_Int)
-              using d'(5)[OF prems(1-3)]
-              apply auto
-              done
-            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
-              by auto
-            also have "\<dots> = interior (k \<inter> cbox u v)"
-              unfolding prems(4) by auto
-            finally show ?case
-              unfolding uv inter_interval content_eq_0_interior ..
-          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 Setcompr_eq_image
-            apply (rule finite_imageI)
-            apply (rule d')
-            apply blast
-            apply safe
-            apply (rule_tac x=k in exI)
-          proof goal_cases
-            case prems: (1 i k)
-            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
-            have "interior (k \<inter> cbox u v) \<noteq> {}"
-              using prems(2)
-              unfolding ab inter_interval content_eq_0_interior
-              by auto
-            then show ?case
-              using prems(1)
-              using interior_subset[of "k \<inter> cbox u v"]
-              by auto
-          qed
-          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
-            unfolding setsum_distrib_right[symmetric] real_scaleR_def
-            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
-            using xl(2)[unfolded uv]
-            unfolding uv
-            apply auto
-            done
-        qed
-        finally show ?case .
-      qed
-    qed
-  qed
-qed
-
-lemma bounded_variation_absolutely_integrable:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "f integrable_on UNIV"
-    and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
-  shows "f absolutely_integrable_on UNIV"
-proof (rule absolutely_integrable_onI, fact, rule)
-  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
-  have D_1: "?D \<noteq> {}"
-    by (rule elementary_interval) auto
-  have D_2: "bdd_above (?f`?D)"
-    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
-  note D = D_1 D_2
-  let ?S = "SUP d:?D. ?f d"
-  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
-    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
-    apply (rule integrable_on_subcbox[OF assms(1)])
-    defer
-    apply safe
-    apply (rule assms(2)[rule_format])
-    apply auto
-    done
-  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
-    apply (subst has_integral_alt')
-    apply safe
-  proof goal_cases
-    case (1 a b)
-    show ?case
-      using f_int[of a b] by auto
-  next
-    case prems: (2 e)
-    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
-    proof (rule ccontr)
-      assume "\<not> ?thesis"
-      then have "?S \<le> ?S - e"
-        by (intro cSUP_least[OF D(1)]) auto
-      then show False
-        using prems by auto
-    qed
-    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
-      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
-      by (auto simp add: image_iff not_le)
-    from this(1) obtain d where "d division_of \<Union>d"
-      and "K = (\<Sum>k\<in>d. norm (integral k f))"
-      by auto
-    note d = this(1) *(2)[unfolded this(2)]
-    note d'=division_ofD[OF this(1)]
-    have "bounded (\<Union>d)"
-      by (rule elementary_bounded,fact)
-    from this[unfolded bounded_pos] obtain K where
-       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
-    show ?case
-      apply (rule_tac x="K + 1" in exI)
-      apply safe
-    proof -
-      fix a b :: 'n
-      assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
-      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
-        by arith
-      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
-        unfolding real_norm_def
-        apply (rule *[rule_format])
-        apply safe
-        apply (rule d(2))
-      proof goal_cases
-        case 1
-        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
-          apply (rule setsum_mono)
-          apply (rule absolutely_integrable_le)
-          apply (drule d'(4))
-          apply safe
-          apply (rule f_int)
-          done
-        also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
-          apply (rule integral_combine_division_bottomup[symmetric])
-          apply (rule d)
-          unfolding forall_in_division[OF d(1)]
-          using f_int
-          apply auto
-          done
-        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
-        proof -
-          have "\<Union>d \<subseteq> cbox a b"
-            apply rule
-            apply (drule K(2)[rule_format])
-            apply (rule ab[unfolded subset_eq,rule_format])
-            apply (auto simp add: dist_norm)
-            done
-          then show ?thesis
-            apply -
-            apply (subst if_P)
-            apply rule
-            apply (rule integral_subset_le)
-            defer
-            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
-            apply (rule d)
-            using f_int[of a b]
-            apply auto
-            done
-        qed
-        finally show ?case .
-      next
-        note f = absolutely_integrable_onD[OF f_int[of a b]]
-        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
-        have "e/2>0"
-          using \<open>e > 0\<close> by auto
-        from * [OF this] obtain d1 where
-          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
-            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
-          by auto
-        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
-          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
-            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
-         obtain p where
-          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
-          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
-            (auto simp add: fine_inter)
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
-          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
-          by arith
-        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
-          apply (subst if_P)
-          apply rule
-        proof (rule *[rule_format])
-          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
-            unfolding split_def
-            apply (rule helplemma)
-            using d2(2)[rule_format,of p]
-            using p(1,3)
-            unfolding tagged_division_of_def split_def
-            apply auto
-            done
-          show "\<bar>(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm(f x))\<bar> < e / 2"
-            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
-            by (simp only: real_norm_def)
-          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
-            apply (rule setsum.cong)
-            apply (rule refl)
-            unfolding split_paired_all split_conv
-            apply (drule tagged_division_ofD(4)[OF p(1)])
-            unfolding norm_scaleR
-            apply (subst abs_of_nonneg)
-            apply auto
-            done
-          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
-            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
-            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
-            apply (simp add: integral_null)
-            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
-            apply (auto simp: tagged_partial_division_of_def)
-            done
-        qed
-      qed
-    qed (insert K, auto)
-  qed
-qed
-
-lemma absolutely_integrable_restrict_univ:
-  "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow>
-    f absolutely_integrable_on s"
-  unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
-
-lemma absolutely_integrable_add[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "f absolutely_integrable_on s"
-    and "g absolutely_integrable_on s"
-  shows "(\<lambda>x. f x + g x) absolutely_integrable_on s"
-proof -
-  let ?P = "\<And>f g::'n \<Rightarrow> 'm. f absolutely_integrable_on UNIV \<Longrightarrow>
-    g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
-  {
-    presume as: "PROP ?P"
-    note a = absolutely_integrable_restrict_univ[symmetric]
-    have *: "\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0) =
-      (if x \<in> s then f x + g x else 0)" by auto
-    show ?thesis
-      apply (subst a)
-      using as[OF assms[unfolded a[of f] a[of g]]]
-      apply (simp only: *)
-      done
-  }
-  fix f g :: "'n \<Rightarrow> 'm"
-  assume assms: "f absolutely_integrable_on UNIV" "g absolutely_integrable_on UNIV"
-  note absolutely_integrable_bounded_variation
-  from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
-  show "(\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
-    apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
-    apply (rule integrable_add)
-    prefer 3
-    apply safe
-  proof goal_cases
-    case prems: (1 d)
-    have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
-      apply (drule division_ofD(4)[OF prems])
-      apply safe
-      apply (rule_tac[!] integrable_on_subcbox[of _ UNIV])
-      using assms
-      apply auto
-      done
-    then have "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
-      (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))"
-      apply -
-      unfolding setsum.distrib [symmetric]
-      apply (rule setsum_mono)
-      apply (subst integral_add)
-      prefer 3
-      apply (rule norm_triangle_ineq)
-      apply auto
-      done
-    also have "\<dots> \<le> B1 + B2"
-      using B(1)[OF prems] B(2)[OF prems] by auto
-    finally show ?case .
-  qed (insert assms, auto)
-qed
-
-lemma absolutely_integrable_sub[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "f absolutely_integrable_on s"
-    and "g absolutely_integrable_on s"
-  shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
-  using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
-  by (simp add: algebra_simps)
-
-lemma absolutely_integrable_linear:
-  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-    and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
-  assumes "f absolutely_integrable_on s"
-    and "bounded_linear h"
-  shows "(h \<circ> f) absolutely_integrable_on s"
-proof -
-  {
-    presume as: "\<And>f::'m \<Rightarrow> 'n. \<And>h::'n \<Rightarrow> 'p. f absolutely_integrable_on UNIV \<Longrightarrow>
-      bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on UNIV"
-    note a = absolutely_integrable_restrict_univ[symmetric]
-    show ?thesis
-      apply (subst a)
-      using as[OF assms[unfolded a[of f] a[of g]]]
-      apply (simp only: o_def if_distrib linear_simps[OF assms(2)])
-      done
-  }
-  fix f :: "'m \<Rightarrow> 'n"
-  fix h :: "'n \<Rightarrow> 'p"
-  assume assms: "f absolutely_integrable_on UNIV" "bounded_linear h"
-  from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
-  from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
-  show "(h \<circ> f) absolutely_integrable_on UNIV"
-    apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
-    apply (rule integrable_linear[OF _ assms(2)])
-    apply safe
-  proof goal_cases
-    case prems: (2 d)
-    have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
-      unfolding setsum_distrib_right
-      apply (rule setsum_mono)
-    proof goal_cases
-      case (1 k)
-      from division_ofD(4)[OF prems this]
-      guess u v by (elim exE) note uv=this
-      have *: "f integrable_on k"
-        unfolding uv
-        apply (rule integrable_on_subcbox[of _ UNIV])
-        using assms
-        apply auto
-        done
-      note this[unfolded has_integral_integral]
-      note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
-      note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
-      show ?case
-        unfolding * using b by auto
-    qed
-    also have "\<dots> \<le> B * b"
-      apply (rule mult_right_mono)
-      using B prems b
-      apply auto
-      done
-    finally show ?case .
-  qed (insert assms, auto)
-qed
-
-lemma absolutely_integrable_setsum:
-  fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "finite t"
-    and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
-  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
-  using assms(1,2)
-  by induct auto
-
-lemma absolutely_integrable_vector_abs:
-  fixes f :: "'a::euclidean_space => 'b::euclidean_space"
-    and T :: "'c::euclidean_space \<Rightarrow> 'b"
-  assumes f: "f absolutely_integrable_on s"
-  shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
-  (is "?Tf absolutely_integrable_on s")
-proof -
-  have if_distrib: "\<And>P A B x. (if P then A else B) *\<^sub>R x = (if P then A *\<^sub>R x else B *\<^sub>R x)"
-    by simp
-  have *: "\<And>x. ?Tf x = (\<Sum>i\<in>Basis.
-    ((\<lambda>y. (\<Sum>j\<in>Basis. (if j = i then y else 0) *\<^sub>R j)) o
-     (\<lambda>x. (norm (\<Sum>j\<in>Basis. (if j = i then f x\<bullet>T i else 0) *\<^sub>R j)))) x)"
-    by (simp add: comp_def if_distrib setsum.If_cases)
-  show ?thesis
-    unfolding *
-    apply (rule absolutely_integrable_setsum[OF finite_Basis])
-    apply (rule absolutely_integrable_linear)
-    apply (rule absolutely_integrable_norm)
-    apply (rule absolutely_integrable_linear[OF f, unfolded o_def])
-    apply (auto simp: linear_linear euclidean_eq_iff[where 'a='c] inner_simps intro!: linearI)
-    done
-qed
-
-lemma absolutely_integrable_max:
-  fixes f g :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f absolutely_integrable_on s"
-    and "g absolutely_integrable_on s"
-  shows "(\<lambda>x. (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
-proof -
-  have *:"\<And>x. (1 / 2) *\<^sub>R (((\<Sum>i\<in>Basis. \<bar>(f x - g x) \<bullet> i\<bar> *\<^sub>R i)::'n) + (f x + g x)) =
-      (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
-    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
-  note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
-  note absolutely_integrable_vector_abs[OF this(1), where T="\<lambda>x. x"] this(2)
-  note absolutely_integrable_add[OF this]
-  note absolutely_integrable_cmul[OF this, of "1/2"]
-  then show ?thesis unfolding * .
-qed
-
-lemma absolutely_integrable_min:
-  fixes f g::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
-  assumes "f absolutely_integrable_on s"
-    and "g absolutely_integrable_on s"
-  shows "(\<lambda>x. (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
-proof -
-  have *:"\<And>x. (1 / 2) *\<^sub>R ((f x + g x) - (\<Sum>i\<in>Basis. \<bar>(f x - g x) \<bullet> i\<bar> *\<^sub>R i::'n)) =
-      (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
-    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
-
-  note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
-  note this(1) absolutely_integrable_vector_abs[OF this(2), where T="\<lambda>x. x"]
-  note absolutely_integrable_sub[OF this]
-  note absolutely_integrable_cmul[OF this,of "1/2"]
-  then show ?thesis unfolding * .
-qed
-
-lemma absolutely_integrable_abs_eq:
-  fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
-    (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
-  (is "?l = ?r")
-proof
-  assume ?l
-  then show ?r
-    apply -
-    apply rule
-    defer
-    apply (drule absolutely_integrable_vector_abs)
-    apply auto
-    done
-next
-  assume ?r
-  {
-    presume lem: "\<And>f::'n \<Rightarrow> 'm. f integrable_on UNIV \<Longrightarrow>
-      (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV \<Longrightarrow>
-        f absolutely_integrable_on UNIV"
-    have *: "\<And>x. (\<Sum>i\<in>Basis. \<bar>(if x \<in> s then f x else 0) \<bullet> i\<bar> *\<^sub>R i) =
-      (if x \<in> s then (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) else (0::'m))"
-      unfolding euclidean_eq_iff[where 'a='m]
-      by auto
-    show ?l
-      apply (subst absolutely_integrable_restrict_univ[symmetric])
-      apply (rule lem)
-      unfolding integrable_restrict_univ *
-      using \<open>?r\<close>
-      apply auto
-      done
-  }
-  fix f :: "'n \<Rightarrow> 'm"
-  assume assms: "f integrable_on UNIV" "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV"
-  let ?B = "\<Sum>i\<in>Basis. integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) \<bullet> i"
-  show "f absolutely_integrable_on UNIV"
-    apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
-    apply safe
-  proof goal_cases
-    case d: (1 d)
-    note d'=division_ofD[OF d]
-    have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
-      (\<Sum>k\<in>d. setsum (op \<bullet> (integral k (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis)"
-      apply (rule setsum_mono)
-      apply (rule order_trans[OF norm_le_l1])
-      apply (rule setsum_mono)
-      unfolding lessThan_iff
-    proof -
-      fix k
-      fix i :: 'm
-      assume "k \<in> d" and i: "i \<in> Basis"
-      from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
-      show "\<bar>integral k f \<bullet> i\<bar> \<le> integral k (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) \<bullet> i"
-        apply (rule abs_leI)
-        unfolding inner_minus_left[symmetric]
-        defer
-        apply (subst integral_neg[symmetric])
-        apply (rule_tac[1-2] integral_component_le[OF i])
-        using integrable_on_subcbox[OF assms(1),of a b]
-          integrable_on_subcbox[OF assms(2),of a b] i  integrable_neg
-        unfolding ab
-        apply auto
-        done
-    qed
-    also have "\<dots> \<le> setsum (op \<bullet> (integral UNIV (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m))) Basis"
-      apply (subst setsum.commute)
-      apply (rule setsum_mono)
-    proof goal_cases
-      case (1 j)
-      have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
-        using integrable_on_subdivision[OF d assms(2)] by auto
-      have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j) =
-        integral (\<Union>d) (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
-        unfolding inner_setsum_left[symmetric] integral_combine_division_topdown[OF * d] ..
-      also have "\<dots> \<le> integral UNIV (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
-        apply (rule integral_subset_component_le)
-        using assms * \<open>j \<in> Basis\<close>
-        apply auto
-        done
-      finally show ?case .
-    qed
-    finally show ?case .
-  qed
-qed
-
-lemma nonnegative_absolutely_integrable:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "\<forall>x\<in>s. \<forall>i\<in>Basis. 0 \<le> f x \<bullet> i"
-    and "f integrable_on s"
-  shows "f absolutely_integrable_on s"
-  unfolding absolutely_integrable_abs_eq
-  apply rule
-  apply (rule assms)thm integrable_eq
-  apply (rule integrable_eq[of _ f])
-  using assms
-  apply (auto simp: euclidean_eq_iff[where 'a='m])
-  done
-
-lemma absolutely_integrable_integrable_bound:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "\<forall>x\<in>s. norm (f x) \<le> g x"
-    and "f integrable_on s"
-    and "g integrable_on s"
-  shows "f absolutely_integrable_on s"
-proof -
-  {
-    presume *: "\<And>f::'n \<Rightarrow> 'm. \<And>g. \<forall>x. norm (f x) \<le> g x \<Longrightarrow> f integrable_on UNIV \<Longrightarrow>
-      g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
-    show ?thesis
-      apply (subst absolutely_integrable_restrict_univ[symmetric])
-      apply (rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
-      using assms
-      unfolding integrable_restrict_univ
-      apply auto
-      done
-  }
-  fix g
-  fix f :: "'n \<Rightarrow> 'm"
-  assume assms: "\<forall>x. norm (f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
-  show "f absolutely_integrable_on UNIV"
-    apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
-    apply safe
-  proof goal_cases
-    case d: (1 d)
-    note d'=division_ofD[OF d]
-    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
-      apply (rule setsum_mono)
-      apply (rule integral_norm_bound_integral)
-      apply (drule_tac[!] d'(4))
-      apply safe
-      apply (rule_tac[1-2] integrable_on_subcbox)
-      using assms
-      apply auto
-      done
-    also have "\<dots> = integral (\<Union>d) g"
-      apply (rule integral_combine_division_bottomup[symmetric])
-      apply (rule d)
-      apply safe
-      apply (drule d'(4))
-      apply safe
-      apply (rule integrable_on_subcbox[OF assms(3)])
-      apply auto
-      done
-    also have "\<dots> \<le> integral UNIV g"
-      apply (rule integral_subset_le)
-      defer
-      apply (rule integrable_on_subdivision[OF d,of _ UNIV])
-      prefer 4
-      apply rule
-      apply (rule_tac y="norm (f x)" in order_trans)
-      using assms
-      apply auto
-      done
-    finally show ?case .
-  qed
-qed
-
-lemma absolutely_integrable_absolutely_integrable_bound:
-  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-    and g :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
-  assumes "\<forall>x\<in>s. norm (f x) \<le> norm (g x)"
-    and "f integrable_on s"
-    and "g absolutely_integrable_on s"
-  shows "f absolutely_integrable_on s"
-  apply (rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
-  using assms
-  apply auto
-  done
-
-lemma absolutely_integrable_inf_real:
-  assumes "finite k"
-    and "k \<noteq> {}"
-    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
-  shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s"
-  using assms
-proof induct
-  case (insert a k)
-  let ?P = "(\<lambda>x.
-    if fs x ` k = {} then fs x a
-    else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
-  show ?case
-    unfolding image_insert
-    apply (subst Inf_insert_finite)
-    apply (rule finite_imageI[OF insert(1)])
-  proof (cases "k = {}")
-    case True
-    then show ?P
-      apply (subst if_P)
-      defer
-      apply (rule insert(5)[rule_format])
-      apply auto
-      done
-  next
-    case False
-    then show ?P
-      apply (subst if_not_P)
-      defer
-      apply (rule absolutely_integrable_min[where 'n=real, unfolded Basis_real_def, simplified])
-      defer
-      apply(rule insert(3)[OF False])
-      using insert(5)
-      apply auto
-      done
-  qed
-next
-  case empty
-  then show ?case by auto
-qed
-
-lemma absolutely_integrable_sup_real:
-  assumes "finite k"
-    and "k \<noteq> {}"
-    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
-  shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s"
-  using assms
-proof induct
-  case (insert a k)
-  let ?P = "(\<lambda>x.
-    if fs x ` k = {} then fs x a
-    else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
-  show ?case
-    unfolding image_insert
-    apply (subst Sup_insert_finite)
-    apply (rule finite_imageI[OF insert(1)])
-  proof (cases "k = {}")
-    case True
-    then show ?P
-      apply (subst if_P)
-      defer
-      apply (rule insert(5)[rule_format])
-      apply auto
-      done
-  next
-    case False
-    then show ?P
-      apply (subst if_not_P)
-      defer
-      apply (rule absolutely_integrable_max[where 'n=real, unfolded Basis_real_def, simplified])
-      defer
-      apply (rule insert(3)[OF False])
-      using insert(5)
-      apply auto
-      done
-  qed
-qed auto
-
-
 subsection \<open>differentiation under the integral sign\<close>
 
 lemma tube_lemma:
@@ -11296,8 +10103,7 @@
           by (simp add: integral_diff dist_norm)
         also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
           using elim
-          by (intro integral_norm_bound_integral)
-            (auto intro!: integrable_diff absolutely_integrable_onI)
+          by (intro integral_norm_bound_integral) (auto intro!: integrable_diff)
         also have "\<dots> < e"
           using \<open>0 < e\<close>
           by (simp add: e'_def)
@@ -11309,358 +10115,6 @@
 qed
 
 
-subsection \<open>Dominated convergence\<close>
-
-context
-begin
-
-private lemma dominated_convergence_real:
-  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
-  assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
-    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
-    and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-proof
-  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
-  proof (safe intro!: bdd_belowI)
-    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
-      using assms(3)[rule_format, of x n] by simp
-  qed
-  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
-  proof (safe intro!: bdd_aboveI)
-    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
-      using assms(3)[rule_format, of x n] by simp
-  qed
-
-  have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
-    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
-    integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
-  proof (rule monotone_convergence_decreasing, safe)
-    fix m :: nat
-    show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
-      unfolding bounded_iff
-      apply (rule_tac x="integral s h" in exI)
-    proof safe
-      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 Setcompr_eq_image
-        apply (rule absolutely_integrable_onD)
-        apply (rule absolutely_integrable_inf_real)
-        prefer 5
-        unfolding real_norm_def
-        apply rule
-        apply (rule cInf_abs_ge)
-        prefer 5
-        apply rule
-        apply (rule_tac g = h in absolutely_integrable_integrable_bound)
-        using assms
-        unfolding real_norm_def
-        apply auto
-        done
-    qed
-    fix k :: nat
-    show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding Setcompr_eq_image
-      apply (rule absolutely_integrable_onD)
-      apply (rule absolutely_integrable_inf_real)
-      prefer 3
-      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
-      apply auto
-      done
-    fix x
-    assume x: "x \<in> s"
-    show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
-      by (rule cInf_superset_mono) auto
-    let ?S = "{f j x| j. m \<le> j}"
-    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Inf ?S) sequentially"
-    proof (rule LIMSEQ_I, goal_cases)
-      case r: (1 r)
-
-      have "\<exists>y\<in>?S. y < Inf ?S + r"
-        by (subst cInf_less_iff[symmetric]) (auto simp: \<open>x\<in>s\<close> r)
-      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
-        by blast
-
-      show ?case
-        apply (rule_tac x=N in exI)
-        apply safe
-      proof goal_cases
-        case prems: (1 n)
-        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> \<bar>ix - Inf ?S\<bar> < r"
-          by arith
-        show ?case
-          unfolding real_norm_def
-            apply (rule *[rule_format, OF N(1)])
-            apply (rule cInf_superset_mono, auto simp: \<open>x\<in>s\<close>) []
-            apply (rule cInf_lower)
-            using N prems
-            apply auto []
-            apply simp
-            done
-      qed
-    qed
-  qed
-  note dec1 = conjunctD2[OF this]
-
-  have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
-    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
-    integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
-  proof (rule monotone_convergence_increasing,safe)
-    fix m :: nat
-    show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
-      unfolding bounded_iff
-      apply (rule_tac x="integral s h" in exI)
-    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 Setcompr_eq_image
-        apply (rule absolutely_integrable_onD)
-        apply(rule absolutely_integrable_sup_real)
-        prefer 5 unfolding real_norm_def
-        apply rule
-        apply (rule cSup_abs_le)
-        using assms
-        apply (force simp add: )
-        prefer 4
-        apply rule
-        apply (rule_tac g=h in absolutely_integrable_integrable_bound)
-        using assms
-        unfolding real_norm_def
-        apply auto
-        done
-    qed
-    fix k :: nat
-    show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
-      unfolding Setcompr_eq_image
-      apply (rule absolutely_integrable_onD)
-      apply (rule absolutely_integrable_sup_real)
-      prefer 3
-      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
-      apply auto
-      done
-    fix x
-    assume x: "x\<in>s"
-    show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
-      by (rule cSup_subset_mono) auto
-    let ?S = "{f j x| j. m \<le> j}"
-    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Sup ?S) sequentially"
-    proof (rule LIMSEQ_I, goal_cases)
-      case r: (1 r)
-      have "\<exists>y\<in>?S. Sup ?S - r < y"
-        by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
-      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
-        by blast
-
-      show ?case
-        apply (rule_tac x=N in exI)
-        apply safe
-      proof goal_cases
-        case prems: (1 n)
-        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> \<bar>ix - Sup ?S\<bar> < r"
-          by arith
-        show ?case
-          apply simp
-          apply (rule *[rule_format, OF N(1)])
-          apply (rule cSup_subset_mono, auto simp: \<open>x\<in>s\<close>) []
-          apply (subst cSup_upper)
-          using N prems
-          apply auto
-          done
-      qed
-    qed
-  qed
-  note inc1 = conjunctD2[OF this]
-
-  have "g integrable_on s \<and>
-    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
-    apply (rule monotone_convergence_increasing,safe)
-    apply fact
-  proof -
-    show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
-      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
-    proof safe
-      fix k :: nat
-      show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
-        apply (rule integral_norm_bound_integral)
-        apply fact+
-        unfolding real_norm_def
-        apply rule
-        apply (rule cInf_abs_ge)
-        using assms(3)
-        apply auto
-        done
-    qed
-    fix k :: nat and x
-    assume x: "x \<in> s"
-
-    have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
-    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
-      by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
-
-    show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) \<longlonglongrightarrow> g x"
-    proof (rule LIMSEQ_I, goal_cases)
-      case r: (1 r)
-      then have "0<r/2"
-        by auto
-      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
-      show ?case
-        apply (rule_tac x=N in exI)
-        apply safe
-        unfolding real_norm_def
-        apply (rule le_less_trans[of _ "r/2"])
-        apply (rule cInf_asclose)
-        apply safe
-        defer
-        apply (rule less_imp_le)
-        using N r
-        apply auto
-        done
-    qed
-  qed
-  note inc2 = conjunctD2[OF this]
-
-  have "g integrable_on s \<and>
-    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
-    apply (rule monotone_convergence_decreasing,safe)
-    apply fact
-  proof -
-    show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
-      unfolding bounded_iff
-      apply (rule_tac x="integral s h" in exI)
-    proof safe
-      fix k :: nat
-      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
-        apply (rule integral_norm_bound_integral)
-        apply fact+
-        unfolding real_norm_def
-        apply rule
-        apply (rule cSup_abs_le)
-        using assms(3)
-        apply auto
-        done
-    qed
-    fix k :: nat
-    fix x
-    assume x: "x \<in> s"
-
-    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
-      by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
-    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) \<longlongrightarrow> g x) sequentially"
-    proof (rule LIMSEQ_I, goal_cases)
-      case r: (1 r)
-      then have "0<r/2"
-        by auto
-      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
-      show ?case
-        apply (rule_tac x=N in exI,safe)
-        unfolding real_norm_def
-        apply (rule le_less_trans[of _ "r/2"])
-        apply (rule cSup_asclose)
-        apply safe
-        defer
-        apply (rule less_imp_le)
-        using N r
-        apply auto
-        done
-    qed
-  qed
-  note dec2 = conjunctD2[OF this]
-
-  show "g integrable_on s" by fact
-  show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-  proof (rule LIMSEQ_I, goal_cases)
-    case r: (1 r)
-    from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
-    from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
-    show ?case
-    proof (rule_tac x="N1+N2" in exI, safe)
-      fix n
-      assume n: "n \<ge> N1 + N2"
-      have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
-        by arith
-      show "norm (integral s (f n) - integral s g) < r"
-        unfolding real_norm_def
-      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
-        show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
-          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
-        show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
-          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
-      qed (insert n, auto)
-    qed
-  qed
-qed
-
-lemma dominated_convergence:
-  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
-    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
-    and conv: "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
-  shows "g integrable_on s"
-    and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-proof -
-  {
-    fix b :: 'm assume b: "b \<in> Basis"
-    have A: "(\<lambda>x. g x \<bullet> b) integrable_on s \<and>
-               (\<lambda>k. integral s (\<lambda>x. f k x \<bullet> b)) \<longlonglongrightarrow> integral s (\<lambda>x. g x \<bullet> b)"
-    proof (rule dominated_convergence_real)
-      fix k :: nat
-      from f show "(\<lambda>x. f k x \<bullet> b) integrable_on s" by (rule integrable_component)
-    next
-      from h show "h integrable_on s" .
-    next
-      fix k :: nat
-      show "\<forall>x\<in>s. norm (f k x \<bullet> b) \<le> h x"
-      proof
-        fix x assume x: "x \<in> s"
-        have "norm (f k x \<bullet> b) \<le> norm (f k x)" by (simp add: Basis_le_norm b)
-        also have "\<dots> \<le> h x" using le[of k] x by simp
-        finally show "norm (f k x \<bullet> b) \<le> h x" .
-      qed
-    next
-      from conv show "\<forall>x\<in>s. (\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
-        by (auto intro!: tendsto_inner)
-    qed
-    have B: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. f k x \<bullet> b)) = integral s (\<lambda>x. f k x \<bullet> b) *\<^sub>R b"
-      for k by (rule integral_linear)
-               (simp_all add: f integrable_component bounded_linear_scaleR_left)
-    have C: "integral s ((\<lambda>x. x *\<^sub>R b) \<circ> (\<lambda>x. g x \<bullet> b)) = integral s (\<lambda>x. g x \<bullet> b) *\<^sub>R b"
-      using A by (intro integral_linear)
-                 (simp_all add: integrable_component bounded_linear_scaleR_left)
-    note A B C
-  } note A = this
-
-  show "g integrable_on s" by (rule integrable_componentwise) (insert A, blast)
-  with A f show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
-    by (subst (1 2) integral_componentwise)
-       (auto intro!: tendsto_setsum tendsto_scaleR simp: o_def)
-qed
-
-lemma has_integral_dominated_convergence:
-  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
-    "\<And>k. \<forall>x\<in>s. norm (f k x) \<le> h x" "\<forall>x\<in>s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
-    and x: "y \<longlonglongrightarrow> x"
-  shows "(g has_integral x) s"
-proof -
-  have int_f: "\<And>k. (f k) integrable_on s"
-    using assms by (auto simp: integrable_on_def)
-  have "(g has_integral (integral s g)) s"
-    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
-  moreover have "integral s g = x"
-  proof (rule LIMSEQ_unique)
-    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
-      using integral_unique[OF assms(1)] x by simp
-    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
-      by (intro dominated_convergence[OF int_f assms(2)]) fact+
-  qed
-  ultimately show ?thesis
-    by simp
-qed
-
-end
-
-
 subsection \<open>Integration by parts\<close>
 
 lemma integration_by_parts_interior_strong:
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -5,7 +5,7 @@
 *)
 
 theory Interval_Integral
-  imports Set_Integral
+  imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
 lemma continuous_on_vector_derivative:
@@ -1062,19 +1062,16 @@
 qed
 
 
-syntax
-"_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
-("(2CLBINT _. _)" [0,60] 60)
+syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
+  ("(2CLBINT _. _)" [0,60] 60)
+
+translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
+
+syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
+  ("(3CLBINT _:_. _)" [0,60,61] 60)
 
 translations
-"CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
-
-syntax
-"_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
-("(3CLBINT _:_. _)" [0,60,61] 60)
-
-translations
-"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
+  "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
 
 abbreviation complex_interval_lebesgue_integral ::
     "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
diff -r 0d82c4c94014 -r f353674c2528 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 10:26:04 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 18:34:34 2016 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Set_Integral
-  imports Equivalence_Lebesgue_Henstock_Integration
+  imports Bochner_Integration
 begin
 
 (*
@@ -50,16 +50,10 @@
 "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
 ("(2LBINT _./ _)" [0,60] 60)
 
-translations
-"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
-
 syntax
 "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
 ("(3LBINT _:_./ _)" [0,60,61] 60)
 
-translations
-"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
-
 (*
     Basic properties
 *)
@@ -180,12 +174,6 @@
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   using assms by (simp_all add: scaleR_diff_right)
 
-lemma set_integral_reflect:
-  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!: Bochner_Integration.integral_cong split: split_indicator)
-
 (* question: why do we have this for negation, but multiplication by a constant
    requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
@@ -528,59 +516,6 @@
 translations
 "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
 
-(*
-lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
-  apply (simp add: norm_mult)
-  by (subst norm_mult, auto)
-*)
-
-lemma borel_integrable_atLeastAtMost':
-  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
-  assumes f: "continuous_on {a..b} f"
-  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
-  by (intro borel_integrable_compact compact_Icc f)
-
-lemma integral_FTC_atLeastAtMost:
-  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
-  assumes "a \<le> b"
-    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
-    and f: "continuous_on {a .. b} f"
-  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
-proof -
-  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
-  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
-    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
-  moreover
-  have "(f has_integral F b - F a) {a .. b}"
-    by (intro fundamental_theorem_of_calculus ballI assms) auto
-  then have "(?f has_integral F b - F a) {a .. b}"
-    by (subst has_integral_cong[where g=f]) auto
-  then have "(?f has_integral F b - F a) UNIV"
-    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
-  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
-    by (rule has_integral_unique)
-qed
-
-lemma set_borel_integral_eq_integral:
-  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
-  assumes "set_integrable lborel S f"
-  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
-proof -
-  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
-  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
-    by (rule has_integral_integral_lborel) fact
-  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
-    apply (subst has_integral_restrict_univ [symmetric])
-    apply (rule has_integral_eq)
-    by auto
-  thus "f integrable_on S"
-    by (auto simp add: integrable_on_def)
-  with 1 have "(f has_integral (integral S f)) S"
-    by (intro integrable_integral, auto simp add: integrable_on_def)
-  thus "LINT x : S | lborel. f x = integral S f"
-    by (intro has_integral_unique [OF 1])
-qed
-
 lemma set_borel_measurable_continuous:
   fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   assumes "S \<in> sets borel" "continuous_on S f"