move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
authorhoelzl
Fri Sep 23 18:34:34 2016 +0200 (2016-09-23)
changeset 63941f353674c2528
parent 63940 0d82c4c94014
child 63942 9195600fcc7c
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Interval_Integral.thy
src/HOL/Analysis/Set_Integral.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
     1.3 @@ -2311,7 +2311,7 @@
     1.4  
     1.5  lemma integrableE:
     1.6    assumes "integrable M f"
     1.7 -  obtains r q where
     1.8 +  obtains r q where "0 \<le> r" "0 \<le> q"
     1.9      "(\<integral>\<^sup>+x. ennreal (f x)\<partial>M) = ennreal r"
    1.10      "(\<integral>\<^sup>+x. ennreal (-f x)\<partial>M) = ennreal q"
    1.11      "f \<in> borel_measurable M" "integral\<^sup>L M f = r - q"
     2.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 23 10:26:04 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Fri Sep 23 18:34:34 2016 +0200
     2.3 @@ -342,6 +342,7 @@
     2.4  lemma null_sets_restrict_space:
     2.5    "\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M"
     2.6    by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)
     2.7 +
     2.8  lemma completion_ex_borel_measurable_real:
     2.9    fixes g :: "'a \<Rightarrow> real"
    2.10    assumes g: "g \<in> borel_measurable (completion M)"
     3.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 23 10:26:04 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Fri Sep 23 18:34:34 2016 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  section \<open>Complex Analysis Basics\<close>
     3.5  
     3.6  theory Complex_Analysis_Basics
     3.7 -imports Henstock_Kurzweil_Integration "~~/src/HOL/Library/Nonpos_Ints"
     3.8 +imports Equivalence_Lebesgue_Henstock_Integration "~~/src/HOL/Library/Nonpos_Ints"
     3.9  begin
    3.10  
    3.11  
     4.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
     4.3 @@ -1,5 +1,10 @@
     4.4 +(*  Title:      HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
     4.5 +    Author:     Johannes Hölzl, TU München
     4.6 +    Author:     Robert Himmelmann, TU München
     4.7 +*)
     4.8 +
     4.9  theory Equivalence_Lebesgue_Henstock_Integration
    4.10 -  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure
    4.11 +  imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
    4.12  begin
    4.13  
    4.14  lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
    4.15 @@ -650,34 +655,27 @@
    4.16      by (auto simp: emeasure_eq_ennreal_measure has_integral_unique)
    4.17  qed
    4.18  
    4.19 +lemma ennreal_max_0: "ennreal (max 0 x) = ennreal x"
    4.20 +  by (auto simp: max_def ennreal_neg)
    4.21 +
    4.22  lemma has_integral_integral_real:
    4.23    fixes f::"'a::euclidean_space \<Rightarrow> real"
    4.24    assumes f: "integrable lborel f"
    4.25    shows "(f has_integral (integral\<^sup>L lborel f)) UNIV"
    4.26 -using f proof induct
    4.27 -  case (base A c) then show ?case
    4.28 -    by (auto intro!: has_integral_mult_left simp: )
    4.29 -       (simp add: emeasure_eq_ennreal_measure indicator_def has_integral_measure_lborel)
    4.30 -next
    4.31 -  case (add f g) then show ?case
    4.32 -    by (auto intro!: has_integral_add)
    4.33 -next
    4.34 -  case (lim f s)
    4.35 -  show ?case
    4.36 -  proof (rule has_integral_dominated_convergence)
    4.37 -    show "\<And>i. (s i has_integral integral\<^sup>L lborel (s i)) UNIV" by fact
    4.38 -    show "(\<lambda>x. norm (2 * f x)) integrable_on UNIV"
    4.39 -      using \<open>integrable lborel f\<close>
    4.40 -      by (intro nn_integral_integrable_on)
    4.41 -         (auto simp: integrable_iff_bounded abs_mult  nn_integral_cmult ennreal_mult ennreal_mult_less_top)
    4.42 -    show "\<And>k. \<forall>x\<in>UNIV. norm (s k x) \<le> norm (2 * f x)"
    4.43 -      using lim by (auto simp add: abs_mult)
    4.44 -    show "\<forall>x\<in>UNIV. (\<lambda>k. s k x) \<longlonglongrightarrow> f x"
    4.45 -      using lim by auto
    4.46 -    show "(\<lambda>k. integral\<^sup>L lborel (s k)) \<longlonglongrightarrow> integral\<^sup>L lborel f"
    4.47 -      using lim lim(1)[THEN borel_measurable_integrable]
    4.48 -      by (intro integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"]) auto
    4.49 -  qed
    4.50 +proof -
    4.51 +  from integrableE[OF f] obtain r q
    4.52 +    where "0 \<le> r" "0 \<le> q"
    4.53 +      and r: "(\<integral>\<^sup>+ x. ennreal (max 0 (f x)) \<partial>lborel) = ennreal r"
    4.54 +      and q: "(\<integral>\<^sup>+ x. ennreal (max 0 (- f x)) \<partial>lborel) = ennreal q"
    4.55 +      and f: "f \<in> borel_measurable lborel" and eq: "integral\<^sup>L lborel f = r - q"
    4.56 +    unfolding ennreal_max_0 by auto
    4.57 +  then have "((\<lambda>x. max 0 (f x)) has_integral r) UNIV" "((\<lambda>x. max 0 (- f x)) has_integral q) UNIV"
    4.58 +    using nn_integral_has_integral[OF _ _ r] nn_integral_has_integral[OF _ _ q] by auto
    4.59 +  note has_integral_sub[OF this]
    4.60 +  moreover have "(\<lambda>x. max 0 (f x) - max 0 (- f x)) = f"
    4.61 +    by auto
    4.62 +  ultimately show ?thesis
    4.63 +    by (simp add: eq)
    4.64  qed
    4.65  
    4.66  lemma has_integral_AE:
    4.67 @@ -781,6 +779,997 @@
    4.68  
    4.69  end
    4.70  
    4.71 +lemma measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
    4.72 +  by (auto simp: measurable_def)
    4.73 +
    4.74 +lemma integrable_completion:
    4.75 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    4.76 +  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
    4.77 +  by (rule integrable_subalgebra[symmetric]) auto
    4.78 +
    4.79 +lemma integral_completion:
    4.80 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    4.81 +  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
    4.82 +  by (rule integral_subalgebra[symmetric]) (auto intro: f)
    4.83 +
    4.84 +context
    4.85 +begin
    4.86 +
    4.87 +private lemma has_integral_integral_lebesgue_real:
    4.88 +  fixes f :: "'a::euclidean_space \<Rightarrow> real"
    4.89 +  assumes f: "integrable lebesgue f"
    4.90 +  shows "(f has_integral (integral\<^sup>L lebesgue f)) UNIV"
    4.91 +proof -
    4.92 +  obtain f' where f': "f' \<in> borel \<rightarrow>\<^sub>M borel" "AE x in lborel. f x = f' x"
    4.93 +    using completion_ex_borel_measurable_real[OF borel_measurable_integrable[OF f]] by auto
    4.94 +  moreover have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>lborel) = (\<integral>\<^sup>+ x. ennreal (norm (f' x)) \<partial>lborel)"
    4.95 +    using f' by (intro nn_integral_cong_AE) auto
    4.96 +  ultimately have "integrable lborel f'"
    4.97 +    using f by (auto simp: integrable_iff_bounded nn_integral_completion cong: nn_integral_cong_AE)
    4.98 +  note has_integral_integral_real[OF this]
    4.99 +  moreover have "integral\<^sup>L lebesgue f = integral\<^sup>L lebesgue f'"
   4.100 +    using f' f by (intro integral_cong_AE) (auto intro: AE_completion measurable_completion)
   4.101 +  moreover have "integral\<^sup>L lebesgue f' = integral\<^sup>L lborel f'"
   4.102 +    using f' by (simp add: integral_completion)
   4.103 +  moreover have "(f' has_integral integral\<^sup>L lborel f') UNIV \<longleftrightarrow> (f has_integral integral\<^sup>L lborel f') UNIV"
   4.104 +    using f' by (intro has_integral_AE) auto
   4.105 +  ultimately show ?thesis
   4.106 +    by auto
   4.107 +qed
   4.108 +
   4.109 +lemma has_integral_integral_lebesgue:
   4.110 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.111 +  assumes f: "integrable lebesgue f"
   4.112 +  shows "(f has_integral (integral\<^sup>L lebesgue f)) UNIV"
   4.113 +proof -
   4.114 +  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"
   4.115 +    using f by (intro has_integral_setsum finite_Basis ballI has_integral_scaleR_left has_integral_integral_lebesgue_real) auto
   4.116 +  also have eq_f: "(\<lambda>x. \<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b) = f"
   4.117 +    by (simp add: fun_eq_iff euclidean_representation)
   4.118 +  also have "(\<Sum>b\<in>Basis. integral\<^sup>L lebesgue (\<lambda>x. f x \<bullet> b) *\<^sub>R b) = integral\<^sup>L lebesgue f"
   4.119 +    using f by (subst (2) eq_f[symmetric]) simp
   4.120 +  finally show ?thesis .
   4.121 +qed
   4.122 +
   4.123 +lemma integrable_on_lebesgue:
   4.124 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.125 +  shows "integrable lebesgue f \<Longrightarrow> f integrable_on UNIV"
   4.126 +  using has_integral_integral_lebesgue by auto
   4.127 +
   4.128 +lemma integral_lebesgue:
   4.129 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.130 +  shows "integrable lebesgue f \<Longrightarrow> integral UNIV f = (\<integral>x. f x \<partial>lebesgue)"
   4.131 +  using has_integral_integral_lebesgue by auto
   4.132 +
   4.133 +end
   4.134 +
   4.135 +subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
   4.136 +
   4.137 +translations
   4.138 +"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
   4.139 +
   4.140 +translations
   4.141 +"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
   4.142 +
   4.143 +lemma set_integral_reflect:
   4.144 +  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
   4.145 +  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
   4.146 +  by (subst lborel_integral_real_affine[where c="-1" and t=0])
   4.147 +     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
   4.148 +
   4.149 +lemma borel_integrable_atLeastAtMost':
   4.150 +  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   4.151 +  assumes f: "continuous_on {a..b} f"
   4.152 +  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
   4.153 +  by (intro borel_integrable_compact compact_Icc f)
   4.154 +
   4.155 +lemma integral_FTC_atLeastAtMost:
   4.156 +  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
   4.157 +  assumes "a \<le> b"
   4.158 +    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
   4.159 +    and f: "continuous_on {a .. b} f"
   4.160 +  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
   4.161 +proof -
   4.162 +  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
   4.163 +  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
   4.164 +    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
   4.165 +  moreover
   4.166 +  have "(f has_integral F b - F a) {a .. b}"
   4.167 +    by (intro fundamental_theorem_of_calculus ballI assms) auto
   4.168 +  then have "(?f has_integral F b - F a) {a .. b}"
   4.169 +    by (subst has_integral_cong[where g=f]) auto
   4.170 +  then have "(?f has_integral F b - F a) UNIV"
   4.171 +    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
   4.172 +  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
   4.173 +    by (rule has_integral_unique)
   4.174 +qed
   4.175 +
   4.176 +lemma set_borel_integral_eq_integral:
   4.177 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.178 +  assumes "set_integrable lborel S f"
   4.179 +  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
   4.180 +proof -
   4.181 +  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   4.182 +  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
   4.183 +    by (rule has_integral_integral_lborel) fact
   4.184 +  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
   4.185 +    apply (subst has_integral_restrict_univ [symmetric])
   4.186 +    apply (rule has_integral_eq)
   4.187 +    by auto
   4.188 +  thus "f integrable_on S"
   4.189 +    by (auto simp add: integrable_on_def)
   4.190 +  with 1 have "(f has_integral (integral S f)) S"
   4.191 +    by (intro integrable_integral, auto simp add: integrable_on_def)
   4.192 +  thus "LINT x : S | lborel. f x = integral S f"
   4.193 +    by (intro has_integral_unique [OF 1])
   4.194 +qed
   4.195 +
   4.196 +lemma has_integral_set_lebesgue:
   4.197 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.198 +  assumes f: "set_integrable lebesgue S f"
   4.199 +  shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
   4.200 +  using has_integral_integral_lebesgue[OF f]
   4.201 +  by (simp_all add: indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] has_integral_restrict_univ cong: if_cong)
   4.202 +
   4.203 +lemma set_lebesgue_integral_eq_integral:
   4.204 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.205 +  assumes f: "set_integrable lebesgue S f"
   4.206 +  shows "f integrable_on S" "LINT x:S | lebesgue. f x = integral S f"
   4.207 +  using has_integral_set_lebesgue[OF f] by (auto simp: integral_unique integrable_on_def)
   4.208 +
   4.209 +abbreviation
   4.210 +  absolutely_integrable_on :: "('a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}) \<Rightarrow> 'a set \<Rightarrow> bool"
   4.211 +  (infixr "absolutely'_integrable'_on" 46)
   4.212 +  where "f absolutely_integrable_on s \<equiv> set_integrable lebesgue s f"
   4.213 +
   4.214 +lemma absolutely_integrable_on_def:
   4.215 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.216 +  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. norm (f x)) integrable_on s"
   4.217 +proof safe
   4.218 +  assume f: "f absolutely_integrable_on s"
   4.219 +  then have nf: "integrable lebesgue (\<lambda>x. norm (indicator s x *\<^sub>R f x))"
   4.220 +    by (intro integrable_norm)
   4.221 +  note integrable_on_lebesgue[OF f] integrable_on_lebesgue[OF nf]
   4.222 +  moreover have
   4.223 +    "(\<lambda>x. indicator s x *\<^sub>R f x) = (\<lambda>x. if x \<in> s then f x else 0)"
   4.224 +    "(\<lambda>x. norm (indicator s x *\<^sub>R f x)) = (\<lambda>x. if x \<in> s then norm (f x) else 0)"
   4.225 +    by auto
   4.226 +  ultimately show "f integrable_on s" "(\<lambda>x. norm (f x)) integrable_on s"
   4.227 +    by (simp_all add: integrable_restrict_univ)
   4.228 +next
   4.229 +  assume f: "f integrable_on s" and nf: "(\<lambda>x. norm (f x)) integrable_on s"
   4.230 +  show "f absolutely_integrable_on s"
   4.231 +  proof (rule integrableI_bounded)
   4.232 +    show "(\<lambda>x. indicator s x *\<^sub>R f x) \<in> borel_measurable lebesgue"
   4.233 +      using f has_integral_implies_lebesgue_measurable[of f _ s] by (auto simp: integrable_on_def)
   4.234 +    show "(\<integral>\<^sup>+ x. ennreal (norm (indicator s x *\<^sub>R f x)) \<partial>lebesgue) < \<infinity>"
   4.235 +      using nf nn_integral_has_integral_lebesgue[of "\<lambda>x. norm (f x)" _ s]
   4.236 +      by (auto simp: integrable_on_def nn_integral_completion)
   4.237 +  qed
   4.238 +qed
   4.239 +
   4.240 +lemma absolutely_integrable_onI:
   4.241 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.242 +  shows "f integrable_on s \<Longrightarrow> (\<lambda>x. norm (f x)) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
   4.243 +  unfolding absolutely_integrable_on_def by auto
   4.244 +
   4.245 +lemma set_integral_norm_bound:
   4.246 +  fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   4.247 +  shows "set_integrable M k f \<Longrightarrow> norm (LINT x:k|M. f x) \<le> LINT x:k|M. norm (f x)"
   4.248 +  using integral_norm_bound[of M "\<lambda>x. indicator k x *\<^sub>R f x"] by simp
   4.249 +
   4.250 +lemma set_integral_finite_UN_AE:
   4.251 +  fixes f :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   4.252 +  assumes "finite I"
   4.253 +    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"
   4.254 +    and [measurable]: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
   4.255 +    and f: "\<And>i. i \<in> I \<Longrightarrow> set_integrable M (A i) f"
   4.256 +  shows "LINT x:(\<Union>i\<in>I. A i)|M. f x = (\<Sum>i\<in>I. LINT x:A i|M. f x)"
   4.257 +  using \<open>finite I\<close> order_refl[of I]
   4.258 +proof (induction I rule: finite_subset_induct')
   4.259 +  case (insert i I')
   4.260 +  have "AE x in M. (\<forall>j\<in>I'. x \<in> A i \<longrightarrow> x \<notin> A j)"
   4.261 +  proof (intro AE_ball_countable[THEN iffD2] ballI)
   4.262 +    fix j assume "j \<in> I'"
   4.263 +    with \<open>I' \<subseteq> I\<close> \<open>i \<notin> I'\<close> have "i \<noteq> j" "j \<in> I"
   4.264 +      by auto
   4.265 +    then show "AE x in M. x \<in> A i \<longrightarrow> x \<notin> A j"
   4.266 +      using ae[of i j] \<open>i \<in> I\<close> by auto
   4.267 +  qed (use \<open>finite I'\<close> in \<open>rule countable_finite\<close>)
   4.268 +  then have "AE x\<in>A i in M. \<forall>xa\<in>I'. x \<notin> A xa "
   4.269 +    by auto
   4.270 +  with insert.hyps insert.IH[symmetric]
   4.271 +  show ?case
   4.272 +    by (auto intro!: set_integral_Un_AE sets.finite_UN f set_integrable_UN)
   4.273 +qed simp
   4.274 +
   4.275 +lemma set_integrable_norm:
   4.276 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   4.277 +  assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
   4.278 +  using integrable_norm[OF f] by simp
   4.279 +
   4.280 +lemma absolutely_integrable_bounded_variation:
   4.281 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   4.282 +  assumes f: "f absolutely_integrable_on UNIV"
   4.283 +  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   4.284 +proof (rule that[of "integral UNIV (\<lambda>x. norm (f x))"]; safe)
   4.285 +  fix d :: "'a set set" assume d: "d division_of \<Union>d"
   4.286 +  have *: "k \<in> d \<Longrightarrow> f absolutely_integrable_on k" for k
   4.287 +    using f[THEN set_integrable_subset, of k] division_ofD(2,4)[OF d, of k] by auto
   4.288 +  note d' = division_ofD[OF d]
   4.289 +
   4.290 +  have "(\<Sum>k\<in>d. norm (integral k f)) = (\<Sum>k\<in>d. norm (LINT x:k|lebesgue. f x))"
   4.291 +    by (intro setsum.cong refl arg_cong[where f=norm] set_lebesgue_integral_eq_integral(2)[symmetric] *)
   4.292 +  also have "\<dots> \<le> (\<Sum>k\<in>d. LINT x:k|lebesgue. norm (f x))"
   4.293 +    by (intro setsum_mono set_integral_norm_bound *)
   4.294 +  also have "\<dots> = (\<Sum>k\<in>d. integral k (\<lambda>x. norm (f x)))"
   4.295 +    by (intro setsum.cong refl set_lebesgue_integral_eq_integral(2) set_integrable_norm *)
   4.296 +  also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
   4.297 +    using integrable_on_subdivision[OF d] assms f unfolding absolutely_integrable_on_def
   4.298 +    by (subst integral_combine_division_topdown[OF _ d]) auto
   4.299 +  also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
   4.300 +    using integrable_on_subdivision[OF d] assms unfolding absolutely_integrable_on_def
   4.301 +    by (intro integral_subset_le) auto
   4.302 +  finally show "(\<Sum>k\<in>d. norm (integral k f)) \<le> integral UNIV (\<lambda>x. norm (f x))" .
   4.303 +qed
   4.304 +
   4.305 +lemma helplemma:
   4.306 +  assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
   4.307 +    and "finite s"
   4.308 +  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
   4.309 +  unfolding setsum_subtractf[symmetric]
   4.310 +  apply (rule le_less_trans[OF setsum_abs])
   4.311 +  apply (rule le_less_trans[OF _ assms(1)])
   4.312 +  apply (rule setsum_mono)
   4.313 +  apply (rule norm_triangle_ineq3)
   4.314 +  done
   4.315 +
   4.316 +lemma bounded_variation_absolutely_integrable_interval:
   4.317 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.318 +  assumes f: "f integrable_on cbox a b"
   4.319 +    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   4.320 +  shows "f absolutely_integrable_on cbox a b"
   4.321 +proof -
   4.322 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
   4.323 +  have D_1: "?D \<noteq> {}"
   4.324 +    by (rule elementary_interval[of a b]) auto
   4.325 +  have D_2: "bdd_above (?f`?D)"
   4.326 +    by (metis * mem_Collect_eq bdd_aboveI2)
   4.327 +  note D = D_1 D_2
   4.328 +  let ?S = "SUP x:?D. ?f x"
   4.329 +  show ?thesis
   4.330 +    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
   4.331 +    apply (subst has_integral[of _ ?S])
   4.332 +    apply safe
   4.333 +  proof goal_cases
   4.334 +    case e: (1 e)
   4.335 +    then have "?S - e / 2 < ?S" by simp
   4.336 +    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
   4.337 +      unfolding less_cSUP_iff[OF D] by auto
   4.338 +    note d' = division_ofD[OF this(1)]
   4.339 +
   4.340 +    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   4.341 +    proof
   4.342 +      fix x
   4.343 +      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
   4.344 +        apply (rule separate_point_closed)
   4.345 +        apply (rule closed_Union)
   4.346 +        apply (rule finite_subset[OF _ d'(1)])
   4.347 +        using d'(4)
   4.348 +        apply auto
   4.349 +        done
   4.350 +      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   4.351 +        by force
   4.352 +    qed
   4.353 +    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
   4.354 +
   4.355 +    have "e/2 > 0"
   4.356 +      using e by auto
   4.357 +    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
   4.358 +    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
   4.359 +    show ?case
   4.360 +      apply (rule_tac x="?g" in exI)
   4.361 +      apply safe
   4.362 +    proof -
   4.363 +      show "gauge ?g"
   4.364 +        using g(1) k(1)
   4.365 +        unfolding gauge_def
   4.366 +        by auto
   4.367 +      fix p
   4.368 +      assume "p tagged_division_of (cbox a b)" and "?g fine p"
   4.369 +      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
   4.370 +      note p' = tagged_division_ofD[OF p(1)]
   4.371 +      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}"
   4.372 +      have gp': "g fine p'"
   4.373 +        using p(2)
   4.374 +        unfolding p'_def fine_def
   4.375 +        by auto
   4.376 +      have p'': "p' tagged_division_of (cbox a b)"
   4.377 +        apply (rule tagged_division_ofI)
   4.378 +      proof -
   4.379 +        show "finite p'"
   4.380 +          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
   4.381 +            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
   4.382 +          unfolding p'_def
   4.383 +          defer
   4.384 +          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
   4.385 +          apply safe
   4.386 +          unfolding image_iff
   4.387 +          apply (rule_tac x="(i,x,l)" in bexI)
   4.388 +          apply auto
   4.389 +          done
   4.390 +        fix x k
   4.391 +        assume "(x, k) \<in> p'"
   4.392 +        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   4.393 +          unfolding p'_def by auto
   4.394 +        then guess i l by (elim exE) note il=conjunctD4[OF this]
   4.395 +        show "x \<in> k" and "k \<subseteq> cbox a b"
   4.396 +          using p'(2-3)[OF il(3)] il by auto
   4.397 +        show "\<exists>a b. k = cbox a b"
   4.398 +          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
   4.399 +          apply safe
   4.400 +          unfolding inter_interval
   4.401 +          apply auto
   4.402 +          done
   4.403 +      next
   4.404 +        fix x1 k1
   4.405 +        assume "(x1, k1) \<in> p'"
   4.406 +        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
   4.407 +          unfolding p'_def by auto
   4.408 +        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
   4.409 +        fix x2 k2
   4.410 +        assume "(x2,k2)\<in>p'"
   4.411 +        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
   4.412 +          unfolding p'_def by auto
   4.413 +        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
   4.414 +        assume "(x1, k1) \<noteq> (x2, k2)"
   4.415 +        then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   4.416 +          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
   4.417 +          unfolding il1 il2
   4.418 +          by auto
   4.419 +        then show "interior k1 \<inter> interior k2 = {}"
   4.420 +          unfolding il1 il2 by auto
   4.421 +      next
   4.422 +        have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
   4.423 +          unfolding p'_def using d' by auto
   4.424 +        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
   4.425 +          apply rule
   4.426 +          apply (rule Union_least)
   4.427 +          unfolding mem_Collect_eq
   4.428 +          apply (erule exE)
   4.429 +          apply (drule *[rule_format])
   4.430 +          apply safe
   4.431 +        proof -
   4.432 +          fix y
   4.433 +          assume y: "y \<in> cbox a b"
   4.434 +          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
   4.435 +            unfolding p'(6)[symmetric] by auto
   4.436 +          then guess x l by (elim exE) note xl=conjunctD2[OF this]
   4.437 +          then have "\<exists>k. k \<in> d \<and> y \<in> k"
   4.438 +            using y unfolding d'(6)[symmetric] by auto
   4.439 +          then guess i .. note i = conjunctD2[OF this]
   4.440 +          have "x \<in> i"
   4.441 +            using fineD[OF p(3) xl(1)]
   4.442 +            using k(2)[OF i(1), of x]
   4.443 +            using i(2) xl(2)
   4.444 +            by auto
   4.445 +          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
   4.446 +            unfolding p'_def Union_iff
   4.447 +            apply (rule_tac x="i \<inter> l" in bexI)
   4.448 +            using i xl
   4.449 +            apply auto
   4.450 +            done
   4.451 +        qed
   4.452 +      qed
   4.453 +
   4.454 +      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
   4.455 +        apply -
   4.456 +        apply (rule g(2)[rule_format])
   4.457 +        unfolding tagged_division_of_def
   4.458 +        apply safe
   4.459 +        apply (rule gp')
   4.460 +        done
   4.461 +      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"
   4.462 +        unfolding split_def
   4.463 +        using p''
   4.464 +        by (force intro!: helplemma)
   4.465 +
   4.466 +      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
   4.467 +      proof (safe, goal_cases)
   4.468 +        case prems: (2 _ _ x i l)
   4.469 +        have "x \<in> i"
   4.470 +          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
   4.471 +          by auto
   4.472 +        then have "(x, i \<inter> l) \<in> p'"
   4.473 +          unfolding p'_def
   4.474 +          using prems
   4.475 +          apply safe
   4.476 +          apply (rule_tac x=x in exI)
   4.477 +          apply (rule_tac x="i \<inter> l" in exI)
   4.478 +          apply safe
   4.479 +          using prems
   4.480 +          apply auto
   4.481 +          done
   4.482 +        then show ?case
   4.483 +          using prems(3) by auto
   4.484 +      next
   4.485 +        fix x k
   4.486 +        assume "(x, k) \<in> p'"
   4.487 +        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   4.488 +          unfolding p'_def by auto
   4.489 +        then guess i l by (elim exE) note il=conjunctD4[OF this]
   4.490 +        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> {}"
   4.491 +          apply (rule_tac x=x in exI)
   4.492 +          apply (rule_tac x=i in exI)
   4.493 +          apply (rule_tac x=l in exI)
   4.494 +          using p'(2)[OF il(3)]
   4.495 +          apply auto
   4.496 +          done
   4.497 +      qed
   4.498 +      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
   4.499 +        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
   4.500 +        unfolding norm_eq_zero
   4.501 +        apply (rule integral_null)
   4.502 +        apply assumption
   4.503 +        apply rule
   4.504 +        done
   4.505 +      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
   4.506 +
   4.507 +      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
   4.508 +        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
   4.509 +        by arith
   4.510 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
   4.511 +        unfolding real_norm_def
   4.512 +        apply (rule *[rule_format,OF **])
   4.513 +        apply safe
   4.514 +        apply(rule d(2))
   4.515 +      proof goal_cases
   4.516 +        case 1
   4.517 +        show ?case
   4.518 +          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
   4.519 +      next
   4.520 +        case 2
   4.521 +        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
   4.522 +          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
   4.523 +          by auto
   4.524 +        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))"
   4.525 +        proof (rule setsum_mono, goal_cases)
   4.526 +          case k: (1 k)
   4.527 +          from d'(4)[OF this] guess u v by (elim exE) note uv=this
   4.528 +          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
   4.529 +          note uvab = d'(2)[OF k[unfolded uv]]
   4.530 +          have "d' division_of cbox u v"
   4.531 +            apply (subst d'_def)
   4.532 +            apply (rule division_inter_1)
   4.533 +            apply (rule division_of_tagged_division[OF p(1)])
   4.534 +            apply (rule uvab)
   4.535 +            done
   4.536 +          then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
   4.537 +            unfolding uv
   4.538 +            apply (subst integral_combine_division_topdown[of _ _ d'])
   4.539 +            apply (rule integrable_on_subcbox[OF assms(1) uvab])
   4.540 +            apply assumption
   4.541 +            apply (rule setsum_norm_le)
   4.542 +            apply auto
   4.543 +            done
   4.544 +          also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
   4.545 +            apply (rule setsum.mono_neutral_left)
   4.546 +            apply (subst Setcompr_eq_image)
   4.547 +            apply (rule finite_imageI)+
   4.548 +            apply fact
   4.549 +            unfolding d'_def uv
   4.550 +            apply blast
   4.551 +          proof (rule, goal_cases)
   4.552 +            case prems: (1 i)
   4.553 +            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
   4.554 +              by auto
   4.555 +            from this[unfolded mem_Collect_eq] guess l .. note l=this
   4.556 +            then have "cbox u v \<inter> l = {}"
   4.557 +              using prems by auto
   4.558 +            then show ?case
   4.559 +              using l by auto
   4.560 +          qed
   4.561 +          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
   4.562 +            unfolding Setcompr_eq_image
   4.563 +            apply (rule setsum.reindex_nontrivial [unfolded o_def])
   4.564 +            apply (rule finite_imageI)
   4.565 +            apply (rule p')
   4.566 +          proof goal_cases
   4.567 +            case prems: (1 l y)
   4.568 +            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
   4.569 +              apply (subst(2) interior_Int)
   4.570 +              apply (rule Int_greatest)
   4.571 +              defer
   4.572 +              apply (subst prems(4))
   4.573 +              apply auto
   4.574 +              done
   4.575 +            then have *: "interior (k \<inter> l) = {}"
   4.576 +              using snd_p(5)[OF prems(1-3)] by auto
   4.577 +            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   4.578 +            show ?case
   4.579 +              using *
   4.580 +              unfolding uv inter_interval content_eq_0_interior[symmetric]
   4.581 +              by auto
   4.582 +          qed
   4.583 +          finally show ?case .
   4.584 +        qed
   4.585 +        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))"
   4.586 +          apply (subst sum_sum_product[symmetric])
   4.587 +          apply fact
   4.588 +          using p'(1)
   4.589 +          apply auto
   4.590 +          done
   4.591 +        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))"
   4.592 +          unfolding split_def ..
   4.593 +        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
   4.594 +          unfolding *
   4.595 +          apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
   4.596 +          apply (rule finite_product_dependent)
   4.597 +          apply fact
   4.598 +          apply (rule finite_imageI)
   4.599 +          apply (rule p')
   4.600 +          unfolding split_paired_all mem_Collect_eq split_conv o_def
   4.601 +        proof -
   4.602 +          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
   4.603 +          fix l1 l2 k1 k2
   4.604 +          assume as:
   4.605 +            "(l1, k1) \<noteq> (l2, k2)"
   4.606 +            "l1 \<inter> k1 = l2 \<inter> k2"
   4.607 +            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   4.608 +            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   4.609 +          then have "l1 \<in> d" and "k1 \<in> snd ` p"
   4.610 +            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
   4.611 +          guess u1 v1 u2 v2 by (elim exE) note uv=this
   4.612 +          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   4.613 +            using as by auto
   4.614 +          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   4.615 +            apply -
   4.616 +            apply (erule disjE)
   4.617 +            apply (rule disjI2)
   4.618 +            apply (rule d'(5))
   4.619 +            prefer 4
   4.620 +            apply (rule disjI1)
   4.621 +            apply (rule *)
   4.622 +            using as
   4.623 +            apply auto
   4.624 +            done
   4.625 +          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   4.626 +            using as(2) by auto
   4.627 +          ultimately have "interior(l1 \<inter> k1) = {}"
   4.628 +            by auto
   4.629 +          then show "norm (integral (l1 \<inter> k1) f) = 0"
   4.630 +            unfolding uv inter_interval
   4.631 +            unfolding content_eq_0_interior[symmetric]
   4.632 +            by auto
   4.633 +        qed
   4.634 +        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
   4.635 +          unfolding sum_p'
   4.636 +          apply (rule setsum.mono_neutral_right)
   4.637 +          apply (subst *)
   4.638 +          apply (rule finite_imageI[OF finite_product_dependent])
   4.639 +          apply fact
   4.640 +          apply (rule finite_imageI[OF p'(1)])
   4.641 +          apply safe
   4.642 +        proof goal_cases
   4.643 +          case (2 i ia l a b)
   4.644 +          then have "ia \<inter> b = {}"
   4.645 +            unfolding p'alt image_iff Bex_def not_ex
   4.646 +            apply (erule_tac x="(a, ia \<inter> b)" in allE)
   4.647 +            apply auto
   4.648 +            done
   4.649 +          then show ?case
   4.650 +            by auto
   4.651 +        next
   4.652 +          case (1 x a b)
   4.653 +          then show ?case
   4.654 +            unfolding p'_def
   4.655 +            apply safe
   4.656 +            apply (rule_tac x=i in exI)
   4.657 +            apply (rule_tac x=l in exI)
   4.658 +            unfolding snd_conv image_iff
   4.659 +            apply safe
   4.660 +            apply (rule_tac x="(a,l)" in bexI)
   4.661 +            apply auto
   4.662 +            done
   4.663 +        qed
   4.664 +        finally show ?case .
   4.665 +      next
   4.666 +        case 3
   4.667 +        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
   4.668 +        have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
   4.669 +          by auto
   4.670 +        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
   4.671 +          apply safe
   4.672 +          unfolding image_iff
   4.673 +          apply (rule_tac x="((x,l),i)" in bexI)
   4.674 +          apply auto
   4.675 +          done
   4.676 +        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
   4.677 +        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))"
   4.678 +          unfolding norm_scaleR
   4.679 +          apply (rule setsum.mono_neutral_left)
   4.680 +          apply (subst *)
   4.681 +          apply (rule finite_imageI)
   4.682 +          apply fact
   4.683 +          unfolding p'alt
   4.684 +          apply blast
   4.685 +          apply safe
   4.686 +          apply (rule_tac x=x in exI)
   4.687 +          apply (rule_tac x=i in exI)
   4.688 +          apply (rule_tac x=l in exI)
   4.689 +          apply auto
   4.690 +          done
   4.691 +        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
   4.692 +          unfolding *
   4.693 +          apply (subst setsum.reindex_nontrivial)
   4.694 +          apply fact
   4.695 +          unfolding split_paired_all
   4.696 +          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
   4.697 +          apply (elim conjE)
   4.698 +        proof -
   4.699 +          fix x1 l1 k1 x2 l2 k2
   4.700 +          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
   4.701 +            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
   4.702 +          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   4.703 +          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   4.704 +            by auto
   4.705 +          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   4.706 +            apply -
   4.707 +            apply (erule disjE)
   4.708 +            apply (rule disjI2)
   4.709 +            defer
   4.710 +            apply (rule disjI1)
   4.711 +            apply (rule d'(5)[OF as(3-4)])
   4.712 +            apply assumption
   4.713 +            apply (rule p'(5)[OF as(1-2)])
   4.714 +            apply auto
   4.715 +            done
   4.716 +          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   4.717 +            unfolding  as ..
   4.718 +          ultimately have "interior (l1 \<inter> k1) = {}"
   4.719 +            by auto
   4.720 +          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
   4.721 +            unfolding uv inter_interval
   4.722 +            unfolding content_eq_0_interior[symmetric]
   4.723 +            by auto
   4.724 +        qed safe
   4.725 +        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
   4.726 +          unfolding Sigma_alt
   4.727 +          apply (subst sum_sum_product[symmetric])
   4.728 +          apply (rule p')
   4.729 +          apply rule
   4.730 +          apply (rule d')
   4.731 +          apply (rule setsum.cong)
   4.732 +          apply (rule refl)
   4.733 +          unfolding split_paired_all split_conv
   4.734 +        proof -
   4.735 +          fix x l
   4.736 +          assume as: "(x, l) \<in> p"
   4.737 +          note xl = p'(2-4)[OF this]
   4.738 +          from this(3) guess u v by (elim exE) note uv=this
   4.739 +          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
   4.740 +            apply (rule setsum.cong)
   4.741 +            apply (rule refl)
   4.742 +            apply (drule d'(4))
   4.743 +            apply safe
   4.744 +            apply (subst Int_commute)
   4.745 +            unfolding inter_interval uv
   4.746 +            apply (subst abs_of_nonneg)
   4.747 +            apply auto
   4.748 +            done
   4.749 +          also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
   4.750 +            unfolding Setcompr_eq_image
   4.751 +            apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
   4.752 +            apply (rule d')
   4.753 +          proof goal_cases
   4.754 +            case prems: (1 k y)
   4.755 +            from d'(4)[OF this(1)] d'(4)[OF this(2)]
   4.756 +            guess u1 v1 u2 v2 by (elim exE) note uv=this
   4.757 +            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
   4.758 +              apply (subst interior_Int)
   4.759 +              using d'(5)[OF prems(1-3)]
   4.760 +              apply auto
   4.761 +              done
   4.762 +            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
   4.763 +              by auto
   4.764 +            also have "\<dots> = interior (k \<inter> cbox u v)"
   4.765 +              unfolding prems(4) by auto
   4.766 +            finally show ?case
   4.767 +              unfolding uv inter_interval content_eq_0_interior ..
   4.768 +          qed
   4.769 +          also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
   4.770 +            apply (rule setsum.mono_neutral_right)
   4.771 +            unfolding Setcompr_eq_image
   4.772 +            apply (rule finite_imageI)
   4.773 +            apply (rule d')
   4.774 +            apply blast
   4.775 +            apply safe
   4.776 +            apply (rule_tac x=k in exI)
   4.777 +          proof goal_cases
   4.778 +            case prems: (1 i k)
   4.779 +            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
   4.780 +            have "interior (k \<inter> cbox u v) \<noteq> {}"
   4.781 +              using prems(2)
   4.782 +              unfolding ab inter_interval content_eq_0_interior
   4.783 +              by auto
   4.784 +            then show ?case
   4.785 +              using prems(1)
   4.786 +              using interior_subset[of "k \<inter> cbox u v"]
   4.787 +              by auto
   4.788 +          qed
   4.789 +          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
   4.790 +            unfolding setsum_distrib_right[symmetric] real_scaleR_def
   4.791 +            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
   4.792 +            using xl(2)[unfolded uv]
   4.793 +            unfolding uv
   4.794 +            apply auto
   4.795 +            done
   4.796 +        qed
   4.797 +        finally show ?case .
   4.798 +      qed
   4.799 +    qed
   4.800 +  qed
   4.801 +qed
   4.802 +
   4.803 +lemma bounded_variation_absolutely_integrable:
   4.804 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.805 +  assumes "f integrable_on UNIV"
   4.806 +    and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   4.807 +  shows "f absolutely_integrable_on UNIV"
   4.808 +proof (rule absolutely_integrable_onI, fact, rule)
   4.809 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
   4.810 +  have D_1: "?D \<noteq> {}"
   4.811 +    by (rule elementary_interval) auto
   4.812 +  have D_2: "bdd_above (?f`?D)"
   4.813 +    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   4.814 +  note D = D_1 D_2
   4.815 +  let ?S = "SUP d:?D. ?f d"
   4.816 +  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
   4.817 +    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
   4.818 +    apply (rule integrable_on_subcbox[OF assms(1)])
   4.819 +    defer
   4.820 +    apply safe
   4.821 +    apply (rule assms(2)[rule_format])
   4.822 +    apply auto
   4.823 +    done
   4.824 +  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
   4.825 +    apply (subst has_integral_alt')
   4.826 +    apply safe
   4.827 +  proof goal_cases
   4.828 +    case (1 a b)
   4.829 +    show ?case
   4.830 +      using f_int[of a b] unfolding absolutely_integrable_on_def by auto
   4.831 +  next
   4.832 +    case prems: (2 e)
   4.833 +    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
   4.834 +    proof (rule ccontr)
   4.835 +      assume "\<not> ?thesis"
   4.836 +      then have "?S \<le> ?S - e"
   4.837 +        by (intro cSUP_least[OF D(1)]) auto
   4.838 +      then show False
   4.839 +        using prems by auto
   4.840 +    qed
   4.841 +    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
   4.842 +      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
   4.843 +      by (auto simp add: image_iff not_le)
   4.844 +    from this(1) obtain d where "d division_of \<Union>d"
   4.845 +      and "K = (\<Sum>k\<in>d. norm (integral k f))"
   4.846 +      by auto
   4.847 +    note d = this(1) *(2)[unfolded this(2)]
   4.848 +    note d'=division_ofD[OF this(1)]
   4.849 +    have "bounded (\<Union>d)"
   4.850 +      by (rule elementary_bounded,fact)
   4.851 +    from this[unfolded bounded_pos] obtain K where
   4.852 +       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
   4.853 +    show ?case
   4.854 +      apply (rule_tac x="K + 1" in exI)
   4.855 +      apply safe
   4.856 +    proof -
   4.857 +      fix a b :: 'n
   4.858 +      assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
   4.859 +      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
   4.860 +        by arith
   4.861 +      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
   4.862 +        unfolding real_norm_def
   4.863 +        apply (rule *[rule_format])
   4.864 +        apply safe
   4.865 +        apply (rule d(2))
   4.866 +      proof goal_cases
   4.867 +        case 1
   4.868 +        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
   4.869 +          apply (intro setsum_mono)
   4.870 +          subgoal for k
   4.871 +            using d'(4)[of k] f_int
   4.872 +            by (auto simp: absolutely_integrable_on_def integral_norm_bound_integral)
   4.873 +          done
   4.874 +        also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
   4.875 +          apply (rule integral_combine_division_bottomup[symmetric])
   4.876 +          apply (rule d)
   4.877 +          unfolding forall_in_division[OF d(1)]
   4.878 +          using f_int unfolding absolutely_integrable_on_def
   4.879 +          apply auto
   4.880 +          done
   4.881 +        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
   4.882 +        proof -
   4.883 +          have "\<Union>d \<subseteq> cbox a b"
   4.884 +            apply rule
   4.885 +            apply (drule K(2)[rule_format])
   4.886 +            apply (rule ab[unfolded subset_eq,rule_format])
   4.887 +            apply (auto simp add: dist_norm)
   4.888 +            done
   4.889 +          then show ?thesis
   4.890 +            apply -
   4.891 +            apply (subst if_P)
   4.892 +            apply rule
   4.893 +            apply (rule integral_subset_le)
   4.894 +            defer
   4.895 +            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
   4.896 +            apply (rule d)
   4.897 +            using f_int[of a b] unfolding absolutely_integrable_on_def
   4.898 +            apply auto
   4.899 +            done
   4.900 +        qed
   4.901 +        finally show ?case .
   4.902 +      next
   4.903 +        note f' = f_int[of a b, unfolded absolutely_integrable_on_def]
   4.904 +        note f = f'[THEN conjunct1] f'[THEN conjunct2]
   4.905 +        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
   4.906 +        have "e/2>0"
   4.907 +          using \<open>e > 0\<close> by auto
   4.908 +        from * [OF this] obtain d1 where
   4.909 +          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
   4.910 +            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
   4.911 +          by auto
   4.912 +        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
   4.913 +          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
   4.914 +            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
   4.915 +         obtain p where
   4.916 +          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
   4.917 +          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
   4.918 +            (auto simp add: fine_inter)
   4.919 +        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
   4.920 +          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
   4.921 +          by arith
   4.922 +        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
   4.923 +          apply (subst if_P)
   4.924 +          apply rule
   4.925 +        proof (rule *[rule_format])
   4.926 +          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"
   4.927 +            unfolding split_def
   4.928 +            apply (rule helplemma)
   4.929 +            using d2(2)[rule_format,of p]
   4.930 +            using p(1,3)
   4.931 +            unfolding tagged_division_of_def split_def
   4.932 +            apply auto
   4.933 +            done
   4.934 +          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"
   4.935 +            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
   4.936 +            by (simp only: real_norm_def)
   4.937 +          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))"
   4.938 +            apply (rule setsum.cong)
   4.939 +            apply (rule refl)
   4.940 +            unfolding split_paired_all split_conv
   4.941 +            apply (drule tagged_division_ofD(4)[OF p(1)])
   4.942 +            unfolding norm_scaleR
   4.943 +            apply (subst abs_of_nonneg)
   4.944 +            apply auto
   4.945 +            done
   4.946 +          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
   4.947 +            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
   4.948 +            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
   4.949 +            apply (simp add: integral_null)
   4.950 +            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
   4.951 +            apply (auto simp: tagged_partial_division_of_def)
   4.952 +            done
   4.953 +        qed
   4.954 +      qed
   4.955 +    qed (insert K, auto)
   4.956 +  qed
   4.957 +qed
   4.958 +
   4.959 +lemma absolutely_integrable_restrict_univ:
   4.960 +  "(\<lambda>x. if x \<in> s then f x else 0) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
   4.961 +  by (intro arg_cong2[where f=integrable]) auto
   4.962 +
   4.963 +lemma absolutely_integrable_add[intro]:
   4.964 +  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.965 +  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
   4.966 +  by (rule set_integral_add)
   4.967 +
   4.968 +lemma absolutely_integrable_sub[intro]:
   4.969 +  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.970 +  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
   4.971 +  by (rule set_integral_diff)
   4.972 +
   4.973 +lemma absolutely_integrable_linear:
   4.974 +  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   4.975 +    and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
   4.976 +  shows "f absolutely_integrable_on s \<Longrightarrow> bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on s"
   4.977 +  using integrable_bounded_linear[of h lebesgue "\<lambda>x. indicator s x *\<^sub>R f x"]
   4.978 +  by (simp add: linear_simps[of h])
   4.979 +
   4.980 +lemma absolutely_integrable_setsum:
   4.981 +  fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.982 +  assumes "finite t" and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
   4.983 +  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
   4.984 +  using assms(1,2) by induct auto
   4.985 +
   4.986 +lemma absolutely_integrable_integrable_bound:
   4.987 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   4.988 +  assumes le: "\<forall>x\<in>s. norm (f x) \<le> g x" and f: "f integrable_on s" and g: "g integrable_on s"
   4.989 +  shows "f absolutely_integrable_on s"
   4.990 +proof (rule Bochner_Integration.integrable_bound)
   4.991 +  show "g absolutely_integrable_on s"
   4.992 +    unfolding absolutely_integrable_on_def
   4.993 +  proof
   4.994 +    show "(\<lambda>x. norm (g x)) integrable_on s"
   4.995 +      using le norm_ge_zero[of "f _"]
   4.996 +      by (intro integrable_spike_finite[OF _ _ g, where s="{}"])
   4.997 +         (auto intro!: abs_of_nonneg intro: order_trans simp del: norm_ge_zero)
   4.998 +  qed fact
   4.999 +  show "set_borel_measurable lebesgue s f"
  4.1000 +    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
  4.1001 +qed (use le in \<open>auto intro!: always_eventually split: split_indicator\<close>)
  4.1002 +
  4.1003 +subsection \<open>Dominated convergence\<close>
  4.1004 +
  4.1005 +lemma dominated_convergence:
  4.1006 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  4.1007 +  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
  4.1008 +    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  4.1009 +    and conv: "\<forall>x \<in> s. (\<lambda>k. f k x) \<longlonglongrightarrow> g x"
  4.1010 +  shows "g integrable_on s" "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
  4.1011 +proof -
  4.1012 +  have 3: "h absolutely_integrable_on s"
  4.1013 +    unfolding absolutely_integrable_on_def
  4.1014 +  proof
  4.1015 +    show "(\<lambda>x. norm (h x)) integrable_on s"
  4.1016 +    proof (intro integrable_spike_finite[OF _ _ h, where s="{}"] ballI)
  4.1017 +      fix x assume "x \<in> s - {}" then show "norm (h x) = h x"
  4.1018 +        using order_trans[OF norm_ge_zero le[THEN bspec, of x]] by auto
  4.1019 +    qed auto
  4.1020 +  qed fact
  4.1021 +  have 2: "set_borel_measurable lebesgue s (f k)" for k
  4.1022 +    using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
  4.1023 +  then have 1: "set_borel_measurable lebesgue s g"
  4.1024 +    by (rule borel_measurable_LIMSEQ_metric) (use conv in \<open>auto split: split_indicator\<close>)
  4.1025 +  have 4: "AE x in lebesgue. (\<lambda>i. indicator s x *\<^sub>R f i x) \<longlonglongrightarrow> indicator s x *\<^sub>R g x"
  4.1026 +    "AE x in lebesgue. norm (indicator s x *\<^sub>R f k x) \<le> indicator s x *\<^sub>R h x" for k
  4.1027 +    using conv le by (auto intro!: always_eventually split: split_indicator)
  4.1028 +
  4.1029 +  have g: "g absolutely_integrable_on s"
  4.1030 +    using 1 2 3 4 by (rule integrable_dominated_convergence)
  4.1031 +  then show "g integrable_on s"
  4.1032 +    by (auto simp: absolutely_integrable_on_def)
  4.1033 +  have "(\<lambda>k. (LINT x:s|lebesgue. f k x)) \<longlonglongrightarrow> (LINT x:s|lebesgue. g x)"
  4.1034 +    using 1 2 3 4 by (rule integral_dominated_convergence)
  4.1035 +  then show "(\<lambda>k. integral s (f k)) \<longlonglongrightarrow> integral s g"
  4.1036 +    using g absolutely_integrable_integrable_bound[OF le f h]
  4.1037 +    by (subst (asm) (1 2) set_lebesgue_integral_eq_integral) auto
  4.1038 +qed
  4.1039 +
  4.1040 +lemma has_integral_dominated_convergence:
  4.1041 +  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  4.1042 +  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
  4.1043 +    "\<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"
  4.1044 +    and x: "y \<longlonglongrightarrow> x"
  4.1045 +  shows "(g has_integral x) s"
  4.1046 +proof -
  4.1047 +  have int_f: "\<And>k. (f k) integrable_on s"
  4.1048 +    using assms by (auto simp: integrable_on_def)
  4.1049 +  have "(g has_integral (integral s g)) s"
  4.1050 +    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
  4.1051 +  moreover have "integral s g = x"
  4.1052 +  proof (rule LIMSEQ_unique)
  4.1053 +    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
  4.1054 +      using integral_unique[OF assms(1)] x by simp
  4.1055 +    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
  4.1056 +      by (intro dominated_convergence[OF int_f assms(2)]) fact+
  4.1057 +  qed
  4.1058 +  ultimately show ?thesis
  4.1059 +    by simp
  4.1060 +qed
  4.1061 +
  4.1062  subsection \<open>Fundamental Theorem of Calculus for the Lebesgue integral\<close>
  4.1063  
  4.1064  text \<open>
     5.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
     5.3 @@ -6180,7 +6180,7 @@
     5.4  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
     5.5  using assms
     5.6  by auto
     5.7 - 
     5.8 +
     5.9  
    5.10  lemma integrable_stretch:
    5.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    5.12 @@ -9608,31 +9608,6 @@
    5.13      by auto
    5.14  qed
    5.15  
    5.16 -
    5.17 -subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
    5.18 -
    5.19 -definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46)
    5.20 -  where "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
    5.21 -
    5.22 -lemma absolutely_integrable_onI[intro?]:
    5.23 -  "f integrable_on s \<Longrightarrow>
    5.24 -    (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
    5.25 -  unfolding absolutely_integrable_on_def
    5.26 -  by auto
    5.27 -
    5.28 -lemma absolutely_integrable_onD[dest]:
    5.29 -  assumes "f absolutely_integrable_on s"
    5.30 -  shows "f integrable_on s"
    5.31 -    and "(\<lambda>x. norm (f x)) integrable_on s"
    5.32 -  using assms
    5.33 -  unfolding absolutely_integrable_on_def
    5.34 -  by auto
    5.35 -
    5.36 -(*lemma absolutely_integrable_on_trans[simp]:
    5.37 -  fixes f::"'n::euclidean_space \<Rightarrow> real"
    5.38 -  shows "(vec1 \<circ> f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
    5.39 -  unfolding absolutely_integrable_on_def o_def by auto*)
    5.40 -
    5.41  lemma integral_norm_bound_integral:
    5.42    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    5.43    assumes "f integrable_on s"
    5.44 @@ -9768,1174 +9743,6 @@
    5.45    using assms
    5.46    by auto
    5.47  
    5.48 -lemma absolutely_integrable_le:
    5.49 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    5.50 -  assumes "f absolutely_integrable_on s"
    5.51 -  shows "norm (integral s f) \<le> integral s (\<lambda>x. norm (f x))"
    5.52 -  apply (rule integral_norm_bound_integral)
    5.53 -  using assms
    5.54 -  apply auto
    5.55 -  done
    5.56 -
    5.57 -lemma absolutely_integrable_0[intro]:
    5.58 -  "(\<lambda>x. 0) absolutely_integrable_on s"
    5.59 -  unfolding absolutely_integrable_on_def
    5.60 -  by auto
    5.61 -
    5.62 -lemma absolutely_integrable_cmul[intro]:
    5.63 -  "f absolutely_integrable_on s \<Longrightarrow>
    5.64 -    (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
    5.65 -  unfolding absolutely_integrable_on_def
    5.66 -  using integrable_cmul[of f s c]
    5.67 -  using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
    5.68 -  by auto
    5.69 -
    5.70 -lemma absolutely_integrable_neg[intro]:
    5.71 -  "f absolutely_integrable_on s \<Longrightarrow>
    5.72 -    (\<lambda>x. -f(x)) absolutely_integrable_on s"
    5.73 -  apply (drule absolutely_integrable_cmul[where c="-1"])
    5.74 -  apply auto
    5.75 -  done
    5.76 -
    5.77 -lemma absolutely_integrable_norm[intro]:
    5.78 -  "f absolutely_integrable_on s \<Longrightarrow>
    5.79 -    (\<lambda>x. norm (f x)) absolutely_integrable_on s"
    5.80 -  unfolding absolutely_integrable_on_def
    5.81 -  by auto
    5.82 -
    5.83 -lemma absolutely_integrable_abs[intro]:
    5.84 -  "f absolutely_integrable_on s \<Longrightarrow>
    5.85 -    (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
    5.86 -  apply (drule absolutely_integrable_norm)
    5.87 -  unfolding real_norm_def
    5.88 -  apply assumption
    5.89 -  done
    5.90 -
    5.91 -lemma absolutely_integrable_on_subinterval:
    5.92 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    5.93 -  shows "f absolutely_integrable_on s \<Longrightarrow>
    5.94 -    cbox a b \<subseteq> s \<Longrightarrow> f absolutely_integrable_on cbox a b"
    5.95 -  unfolding absolutely_integrable_on_def
    5.96 -  by (metis integrable_on_subcbox)
    5.97 -
    5.98 -lemma absolutely_integrable_bounded_variation:
    5.99 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   5.100 -  assumes "f absolutely_integrable_on UNIV"
   5.101 -  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   5.102 -  apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
   5.103 -  apply safe
   5.104 -proof goal_cases
   5.105 -  case prems: (1 d)
   5.106 -  note d = division_ofD[OF prems(2)]
   5.107 -  have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
   5.108 -    apply (rule setsum_mono,rule absolutely_integrable_le)
   5.109 -    apply (drule d(4))
   5.110 -    apply safe
   5.111 -    apply (rule absolutely_integrable_on_subinterval[OF assms])
   5.112 -    apply auto
   5.113 -    done
   5.114 -  also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
   5.115 -    apply (subst integral_combine_division_topdown[OF _ prems(2)])
   5.116 -    using integrable_on_subdivision[OF prems(2)]
   5.117 -    using assms
   5.118 -    apply auto
   5.119 -    done
   5.120 -  also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
   5.121 -    apply (rule integral_subset_le)
   5.122 -    using integrable_on_subdivision[OF prems(2)]
   5.123 -    using assms
   5.124 -    apply auto
   5.125 -    done
   5.126 -  finally show ?case .
   5.127 -qed
   5.128 -
   5.129 -lemma helplemma:
   5.130 -  assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
   5.131 -    and "finite s"
   5.132 -  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
   5.133 -  unfolding setsum_subtractf[symmetric]
   5.134 -  apply (rule le_less_trans[OF setsum_abs])
   5.135 -  apply (rule le_less_trans[OF _ assms(1)])
   5.136 -  apply (rule setsum_mono)
   5.137 -  apply (rule norm_triangle_ineq3)
   5.138 -  done
   5.139 -
   5.140 -lemma bounded_variation_absolutely_integrable_interval:
   5.141 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.142 -  assumes f: "f integrable_on cbox a b"
   5.143 -    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   5.144 -  shows "f absolutely_integrable_on cbox a b"
   5.145 -proof -
   5.146 -  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
   5.147 -  have D_1: "?D \<noteq> {}"
   5.148 -    by (rule elementary_interval[of a b]) auto
   5.149 -  have D_2: "bdd_above (?f`?D)"
   5.150 -    by (metis * mem_Collect_eq bdd_aboveI2)
   5.151 -  note D = D_1 D_2
   5.152 -  let ?S = "SUP x:?D. ?f x"
   5.153 -  show ?thesis
   5.154 -    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
   5.155 -    apply (subst has_integral[of _ ?S])
   5.156 -    apply safe
   5.157 -  proof goal_cases
   5.158 -    case e: (1 e)
   5.159 -    then have "?S - e / 2 < ?S" by simp
   5.160 -    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
   5.161 -      unfolding less_cSUP_iff[OF D] by auto
   5.162 -    note d' = division_ofD[OF this(1)]
   5.163 -
   5.164 -    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   5.165 -    proof
   5.166 -      fix x
   5.167 -      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
   5.168 -        apply (rule separate_point_closed)
   5.169 -        apply (rule closed_Union)
   5.170 -        apply (rule finite_subset[OF _ d'(1)])
   5.171 -        using d'(4)
   5.172 -        apply auto
   5.173 -        done
   5.174 -      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   5.175 -        by force
   5.176 -    qed
   5.177 -    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
   5.178 -
   5.179 -    have "e/2 > 0"
   5.180 -      using e by auto
   5.181 -    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
   5.182 -    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
   5.183 -    show ?case
   5.184 -      apply (rule_tac x="?g" in exI)
   5.185 -      apply safe
   5.186 -    proof -
   5.187 -      show "gauge ?g"
   5.188 -        using g(1) k(1)
   5.189 -        unfolding gauge_def
   5.190 -        by auto
   5.191 -      fix p
   5.192 -      assume "p tagged_division_of (cbox a b)" and "?g fine p"
   5.193 -      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
   5.194 -      note p' = tagged_division_ofD[OF p(1)]
   5.195 -      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}"
   5.196 -      have gp': "g fine p'"
   5.197 -        using p(2)
   5.198 -        unfolding p'_def fine_def
   5.199 -        by auto
   5.200 -      have p'': "p' tagged_division_of (cbox a b)"
   5.201 -        apply (rule tagged_division_ofI)
   5.202 -      proof -
   5.203 -        show "finite p'"
   5.204 -          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
   5.205 -            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
   5.206 -          unfolding p'_def
   5.207 -          defer
   5.208 -          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
   5.209 -          apply safe
   5.210 -          unfolding image_iff
   5.211 -          apply (rule_tac x="(i,x,l)" in bexI)
   5.212 -          apply auto
   5.213 -          done
   5.214 -        fix x k
   5.215 -        assume "(x, k) \<in> p'"
   5.216 -        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   5.217 -          unfolding p'_def by auto
   5.218 -        then guess i l by (elim exE) note il=conjunctD4[OF this]
   5.219 -        show "x \<in> k" and "k \<subseteq> cbox a b"
   5.220 -          using p'(2-3)[OF il(3)] il by auto
   5.221 -        show "\<exists>a b. k = cbox a b"
   5.222 -          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
   5.223 -          apply safe
   5.224 -          unfolding inter_interval
   5.225 -          apply auto
   5.226 -          done
   5.227 -      next
   5.228 -        fix x1 k1
   5.229 -        assume "(x1, k1) \<in> p'"
   5.230 -        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
   5.231 -          unfolding p'_def by auto
   5.232 -        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
   5.233 -        fix x2 k2
   5.234 -        assume "(x2,k2)\<in>p'"
   5.235 -        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
   5.236 -          unfolding p'_def by auto
   5.237 -        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
   5.238 -        assume "(x1, k1) \<noteq> (x2, k2)"
   5.239 -        then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   5.240 -          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
   5.241 -          unfolding il1 il2
   5.242 -          by auto
   5.243 -        then show "interior k1 \<inter> interior k2 = {}"
   5.244 -          unfolding il1 il2 by auto
   5.245 -      next
   5.246 -        have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
   5.247 -          unfolding p'_def using d' by auto
   5.248 -        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
   5.249 -          apply rule
   5.250 -          apply (rule Union_least)
   5.251 -          unfolding mem_Collect_eq
   5.252 -          apply (erule exE)
   5.253 -          apply (drule *[rule_format])
   5.254 -          apply safe
   5.255 -        proof -
   5.256 -          fix y
   5.257 -          assume y: "y \<in> cbox a b"
   5.258 -          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
   5.259 -            unfolding p'(6)[symmetric] by auto
   5.260 -          then guess x l by (elim exE) note xl=conjunctD2[OF this]
   5.261 -          then have "\<exists>k. k \<in> d \<and> y \<in> k"
   5.262 -            using y unfolding d'(6)[symmetric] by auto
   5.263 -          then guess i .. note i = conjunctD2[OF this]
   5.264 -          have "x \<in> i"
   5.265 -            using fineD[OF p(3) xl(1)]
   5.266 -            using k(2)[OF i(1), of x]
   5.267 -            using i(2) xl(2)
   5.268 -            by auto
   5.269 -          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
   5.270 -            unfolding p'_def Union_iff
   5.271 -            apply (rule_tac x="i \<inter> l" in bexI)
   5.272 -            using i xl
   5.273 -            apply auto
   5.274 -            done
   5.275 -        qed
   5.276 -      qed
   5.277 -
   5.278 -      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
   5.279 -        apply -
   5.280 -        apply (rule g(2)[rule_format])
   5.281 -        unfolding tagged_division_of_def
   5.282 -        apply safe
   5.283 -        apply (rule gp')
   5.284 -        done
   5.285 -      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"
   5.286 -        unfolding split_def
   5.287 -        using p''
   5.288 -        by (force intro!: helplemma)
   5.289 -
   5.290 -      have p'alt: "p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}}"
   5.291 -      proof (safe, goal_cases)
   5.292 -        case prems: (2 _ _ x i l)
   5.293 -        have "x \<in> i"
   5.294 -          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
   5.295 -          by auto
   5.296 -        then have "(x, i \<inter> l) \<in> p'"
   5.297 -          unfolding p'_def
   5.298 -          using prems
   5.299 -          apply safe
   5.300 -          apply (rule_tac x=x in exI)
   5.301 -          apply (rule_tac x="i \<inter> l" in exI)
   5.302 -          apply safe
   5.303 -          using prems
   5.304 -          apply auto
   5.305 -          done
   5.306 -        then show ?case
   5.307 -          using prems(3) by auto
   5.308 -      next
   5.309 -        fix x k
   5.310 -        assume "(x, k) \<in> p'"
   5.311 -        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   5.312 -          unfolding p'_def by auto
   5.313 -        then guess i l by (elim exE) note il=conjunctD4[OF this]
   5.314 -        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> {}"
   5.315 -          apply (rule_tac x=x in exI)
   5.316 -          apply (rule_tac x=i in exI)
   5.317 -          apply (rule_tac x=l in exI)
   5.318 -          using p'(2)[OF il(3)]
   5.319 -          apply auto
   5.320 -          done
   5.321 -      qed
   5.322 -      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
   5.323 -        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
   5.324 -        unfolding norm_eq_zero
   5.325 -        apply (rule integral_null)
   5.326 -        apply assumption
   5.327 -        apply rule
   5.328 -        done
   5.329 -      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
   5.330 -
   5.331 -      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
   5.332 -        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
   5.333 -        by arith
   5.334 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
   5.335 -        unfolding real_norm_def
   5.336 -        apply (rule *[rule_format,OF **])
   5.337 -        apply safe
   5.338 -        apply(rule d(2))
   5.339 -      proof goal_cases
   5.340 -        case 1
   5.341 -        show ?case
   5.342 -          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
   5.343 -      next
   5.344 -        case 2
   5.345 -        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
   5.346 -          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
   5.347 -          by auto
   5.348 -        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))"
   5.349 -        proof (rule setsum_mono, goal_cases)
   5.350 -          case k: (1 k)
   5.351 -          from d'(4)[OF this] guess u v by (elim exE) note uv=this
   5.352 -          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
   5.353 -          note uvab = d'(2)[OF k[unfolded uv]]
   5.354 -          have "d' division_of cbox u v"
   5.355 -            apply (subst d'_def)
   5.356 -            apply (rule division_inter_1)
   5.357 -            apply (rule division_of_tagged_division[OF p(1)])
   5.358 -            apply (rule uvab)
   5.359 -            done
   5.360 -          then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
   5.361 -            unfolding uv
   5.362 -            apply (subst integral_combine_division_topdown[of _ _ d'])
   5.363 -            apply (rule integrable_on_subcbox[OF assms(1) uvab])
   5.364 -            apply assumption
   5.365 -            apply (rule setsum_norm_le)
   5.366 -            apply auto
   5.367 -            done
   5.368 -          also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
   5.369 -            apply (rule setsum.mono_neutral_left)
   5.370 -            apply (subst Setcompr_eq_image)
   5.371 -            apply (rule finite_imageI)+
   5.372 -            apply fact
   5.373 -            unfolding d'_def uv
   5.374 -            apply blast
   5.375 -          proof (rule, goal_cases)
   5.376 -            case prems: (1 i)
   5.377 -            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
   5.378 -              by auto
   5.379 -            from this[unfolded mem_Collect_eq] guess l .. note l=this
   5.380 -            then have "cbox u v \<inter> l = {}"
   5.381 -              using prems by auto
   5.382 -            then show ?case
   5.383 -              using l by auto
   5.384 -          qed
   5.385 -          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
   5.386 -            unfolding Setcompr_eq_image
   5.387 -            apply (rule setsum.reindex_nontrivial [unfolded o_def])
   5.388 -            apply (rule finite_imageI)
   5.389 -            apply (rule p')
   5.390 -          proof goal_cases
   5.391 -            case prems: (1 l y)
   5.392 -            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
   5.393 -              apply (subst(2) interior_Int)
   5.394 -              apply (rule Int_greatest)
   5.395 -              defer
   5.396 -              apply (subst prems(4))
   5.397 -              apply auto
   5.398 -              done
   5.399 -            then have *: "interior (k \<inter> l) = {}"
   5.400 -              using snd_p(5)[OF prems(1-3)] by auto
   5.401 -            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   5.402 -            show ?case
   5.403 -              using *
   5.404 -              unfolding uv inter_interval content_eq_0_interior[symmetric]
   5.405 -              by auto
   5.406 -          qed
   5.407 -          finally show ?case .
   5.408 -        qed
   5.409 -        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))"
   5.410 -          apply (subst sum_sum_product[symmetric])
   5.411 -          apply fact
   5.412 -          using p'(1)
   5.413 -          apply auto
   5.414 -          done
   5.415 -        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))"
   5.416 -          unfolding split_def ..
   5.417 -        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
   5.418 -          unfolding *
   5.419 -          apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
   5.420 -          apply (rule finite_product_dependent)
   5.421 -          apply fact
   5.422 -          apply (rule finite_imageI)
   5.423 -          apply (rule p')
   5.424 -          unfolding split_paired_all mem_Collect_eq split_conv o_def
   5.425 -        proof -
   5.426 -          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
   5.427 -          fix l1 l2 k1 k2
   5.428 -          assume as:
   5.429 -            "(l1, k1) \<noteq> (l2, k2)"
   5.430 -            "l1 \<inter> k1 = l2 \<inter> k2"
   5.431 -            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   5.432 -            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   5.433 -          then have "l1 \<in> d" and "k1 \<in> snd ` p"
   5.434 -            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
   5.435 -          guess u1 v1 u2 v2 by (elim exE) note uv=this
   5.436 -          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   5.437 -            using as by auto
   5.438 -          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   5.439 -            apply -
   5.440 -            apply (erule disjE)
   5.441 -            apply (rule disjI2)
   5.442 -            apply (rule d'(5))
   5.443 -            prefer 4
   5.444 -            apply (rule disjI1)
   5.445 -            apply (rule *)
   5.446 -            using as
   5.447 -            apply auto
   5.448 -            done
   5.449 -          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   5.450 -            using as(2) by auto
   5.451 -          ultimately have "interior(l1 \<inter> k1) = {}"
   5.452 -            by auto
   5.453 -          then show "norm (integral (l1 \<inter> k1) f) = 0"
   5.454 -            unfolding uv inter_interval
   5.455 -            unfolding content_eq_0_interior[symmetric]
   5.456 -            by auto
   5.457 -        qed
   5.458 -        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
   5.459 -          unfolding sum_p'
   5.460 -          apply (rule setsum.mono_neutral_right)
   5.461 -          apply (subst *)
   5.462 -          apply (rule finite_imageI[OF finite_product_dependent])
   5.463 -          apply fact
   5.464 -          apply (rule finite_imageI[OF p'(1)])
   5.465 -          apply safe
   5.466 -        proof goal_cases
   5.467 -          case (2 i ia l a b)
   5.468 -          then have "ia \<inter> b = {}"
   5.469 -            unfolding p'alt image_iff Bex_def not_ex
   5.470 -            apply (erule_tac x="(a, ia \<inter> b)" in allE)
   5.471 -            apply auto
   5.472 -            done
   5.473 -          then show ?case
   5.474 -            by auto
   5.475 -        next
   5.476 -          case (1 x a b)
   5.477 -          then show ?case
   5.478 -            unfolding p'_def
   5.479 -            apply safe
   5.480 -            apply (rule_tac x=i in exI)
   5.481 -            apply (rule_tac x=l in exI)
   5.482 -            unfolding snd_conv image_iff
   5.483 -            apply safe
   5.484 -            apply (rule_tac x="(a,l)" in bexI)
   5.485 -            apply auto
   5.486 -            done
   5.487 -        qed
   5.488 -        finally show ?case .
   5.489 -      next
   5.490 -        case 3
   5.491 -        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
   5.492 -        have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
   5.493 -          by auto
   5.494 -        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
   5.495 -          apply safe
   5.496 -          unfolding image_iff
   5.497 -          apply (rule_tac x="((x,l),i)" in bexI)
   5.498 -          apply auto
   5.499 -          done
   5.500 -        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
   5.501 -        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))"
   5.502 -          unfolding norm_scaleR
   5.503 -          apply (rule setsum.mono_neutral_left)
   5.504 -          apply (subst *)
   5.505 -          apply (rule finite_imageI)
   5.506 -          apply fact
   5.507 -          unfolding p'alt
   5.508 -          apply blast
   5.509 -          apply safe
   5.510 -          apply (rule_tac x=x in exI)
   5.511 -          apply (rule_tac x=i in exI)
   5.512 -          apply (rule_tac x=l in exI)
   5.513 -          apply auto
   5.514 -          done
   5.515 -        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
   5.516 -          unfolding *
   5.517 -          apply (subst setsum.reindex_nontrivial)
   5.518 -          apply fact
   5.519 -          unfolding split_paired_all
   5.520 -          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
   5.521 -          apply (elim conjE)
   5.522 -        proof -
   5.523 -          fix x1 l1 k1 x2 l2 k2
   5.524 -          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
   5.525 -            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
   5.526 -          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   5.527 -          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   5.528 -            by auto
   5.529 -          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   5.530 -            apply -
   5.531 -            apply (erule disjE)
   5.532 -            apply (rule disjI2)
   5.533 -            defer
   5.534 -            apply (rule disjI1)
   5.535 -            apply (rule d'(5)[OF as(3-4)])
   5.536 -            apply assumption
   5.537 -            apply (rule p'(5)[OF as(1-2)])
   5.538 -            apply auto
   5.539 -            done
   5.540 -          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   5.541 -            unfolding  as ..
   5.542 -          ultimately have "interior (l1 \<inter> k1) = {}"
   5.543 -            by auto
   5.544 -          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
   5.545 -            unfolding uv inter_interval
   5.546 -            unfolding content_eq_0_interior[symmetric]
   5.547 -            by auto
   5.548 -        qed safe
   5.549 -        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
   5.550 -          unfolding Sigma_alt
   5.551 -          apply (subst sum_sum_product[symmetric])
   5.552 -          apply (rule p')
   5.553 -          apply rule
   5.554 -          apply (rule d')
   5.555 -          apply (rule setsum.cong)
   5.556 -          apply (rule refl)
   5.557 -          unfolding split_paired_all split_conv
   5.558 -        proof -
   5.559 -          fix x l
   5.560 -          assume as: "(x, l) \<in> p"
   5.561 -          note xl = p'(2-4)[OF this]
   5.562 -          from this(3) guess u v by (elim exE) note uv=this
   5.563 -          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
   5.564 -            apply (rule setsum.cong)
   5.565 -            apply (rule refl)
   5.566 -            apply (drule d'(4))
   5.567 -            apply safe
   5.568 -            apply (subst Int_commute)
   5.569 -            unfolding inter_interval uv
   5.570 -            apply (subst abs_of_nonneg)
   5.571 -            apply auto
   5.572 -            done
   5.573 -          also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
   5.574 -            unfolding Setcompr_eq_image
   5.575 -            apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
   5.576 -            apply (rule d')
   5.577 -          proof goal_cases
   5.578 -            case prems: (1 k y)
   5.579 -            from d'(4)[OF this(1)] d'(4)[OF this(2)]
   5.580 -            guess u1 v1 u2 v2 by (elim exE) note uv=this
   5.581 -            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
   5.582 -              apply (subst interior_Int)
   5.583 -              using d'(5)[OF prems(1-3)]
   5.584 -              apply auto
   5.585 -              done
   5.586 -            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
   5.587 -              by auto
   5.588 -            also have "\<dots> = interior (k \<inter> cbox u v)"
   5.589 -              unfolding prems(4) by auto
   5.590 -            finally show ?case
   5.591 -              unfolding uv inter_interval content_eq_0_interior ..
   5.592 -          qed
   5.593 -          also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
   5.594 -            apply (rule setsum.mono_neutral_right)
   5.595 -            unfolding Setcompr_eq_image
   5.596 -            apply (rule finite_imageI)
   5.597 -            apply (rule d')
   5.598 -            apply blast
   5.599 -            apply safe
   5.600 -            apply (rule_tac x=k in exI)
   5.601 -          proof goal_cases
   5.602 -            case prems: (1 i k)
   5.603 -            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
   5.604 -            have "interior (k \<inter> cbox u v) \<noteq> {}"
   5.605 -              using prems(2)
   5.606 -              unfolding ab inter_interval content_eq_0_interior
   5.607 -              by auto
   5.608 -            then show ?case
   5.609 -              using prems(1)
   5.610 -              using interior_subset[of "k \<inter> cbox u v"]
   5.611 -              by auto
   5.612 -          qed
   5.613 -          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
   5.614 -            unfolding setsum_distrib_right[symmetric] real_scaleR_def
   5.615 -            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
   5.616 -            using xl(2)[unfolded uv]
   5.617 -            unfolding uv
   5.618 -            apply auto
   5.619 -            done
   5.620 -        qed
   5.621 -        finally show ?case .
   5.622 -      qed
   5.623 -    qed
   5.624 -  qed
   5.625 -qed
   5.626 -
   5.627 -lemma bounded_variation_absolutely_integrable:
   5.628 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.629 -  assumes "f integrable_on UNIV"
   5.630 -    and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   5.631 -  shows "f absolutely_integrable_on UNIV"
   5.632 -proof (rule absolutely_integrable_onI, fact, rule)
   5.633 -  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
   5.634 -  have D_1: "?D \<noteq> {}"
   5.635 -    by (rule elementary_interval) auto
   5.636 -  have D_2: "bdd_above (?f`?D)"
   5.637 -    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   5.638 -  note D = D_1 D_2
   5.639 -  let ?S = "SUP d:?D. ?f d"
   5.640 -  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
   5.641 -    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
   5.642 -    apply (rule integrable_on_subcbox[OF assms(1)])
   5.643 -    defer
   5.644 -    apply safe
   5.645 -    apply (rule assms(2)[rule_format])
   5.646 -    apply auto
   5.647 -    done
   5.648 -  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
   5.649 -    apply (subst has_integral_alt')
   5.650 -    apply safe
   5.651 -  proof goal_cases
   5.652 -    case (1 a b)
   5.653 -    show ?case
   5.654 -      using f_int[of a b] by auto
   5.655 -  next
   5.656 -    case prems: (2 e)
   5.657 -    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
   5.658 -    proof (rule ccontr)
   5.659 -      assume "\<not> ?thesis"
   5.660 -      then have "?S \<le> ?S - e"
   5.661 -        by (intro cSUP_least[OF D(1)]) auto
   5.662 -      then show False
   5.663 -        using prems by auto
   5.664 -    qed
   5.665 -    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
   5.666 -      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
   5.667 -      by (auto simp add: image_iff not_le)
   5.668 -    from this(1) obtain d where "d division_of \<Union>d"
   5.669 -      and "K = (\<Sum>k\<in>d. norm (integral k f))"
   5.670 -      by auto
   5.671 -    note d = this(1) *(2)[unfolded this(2)]
   5.672 -    note d'=division_ofD[OF this(1)]
   5.673 -    have "bounded (\<Union>d)"
   5.674 -      by (rule elementary_bounded,fact)
   5.675 -    from this[unfolded bounded_pos] obtain K where
   5.676 -       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
   5.677 -    show ?case
   5.678 -      apply (rule_tac x="K + 1" in exI)
   5.679 -      apply safe
   5.680 -    proof -
   5.681 -      fix a b :: 'n
   5.682 -      assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
   5.683 -      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
   5.684 -        by arith
   5.685 -      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
   5.686 -        unfolding real_norm_def
   5.687 -        apply (rule *[rule_format])
   5.688 -        apply safe
   5.689 -        apply (rule d(2))
   5.690 -      proof goal_cases
   5.691 -        case 1
   5.692 -        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
   5.693 -          apply (rule setsum_mono)
   5.694 -          apply (rule absolutely_integrable_le)
   5.695 -          apply (drule d'(4))
   5.696 -          apply safe
   5.697 -          apply (rule f_int)
   5.698 -          done
   5.699 -        also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
   5.700 -          apply (rule integral_combine_division_bottomup[symmetric])
   5.701 -          apply (rule d)
   5.702 -          unfolding forall_in_division[OF d(1)]
   5.703 -          using f_int
   5.704 -          apply auto
   5.705 -          done
   5.706 -        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
   5.707 -        proof -
   5.708 -          have "\<Union>d \<subseteq> cbox a b"
   5.709 -            apply rule
   5.710 -            apply (drule K(2)[rule_format])
   5.711 -            apply (rule ab[unfolded subset_eq,rule_format])
   5.712 -            apply (auto simp add: dist_norm)
   5.713 -            done
   5.714 -          then show ?thesis
   5.715 -            apply -
   5.716 -            apply (subst if_P)
   5.717 -            apply rule
   5.718 -            apply (rule integral_subset_le)
   5.719 -            defer
   5.720 -            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
   5.721 -            apply (rule d)
   5.722 -            using f_int[of a b]
   5.723 -            apply auto
   5.724 -            done
   5.725 -        qed
   5.726 -        finally show ?case .
   5.727 -      next
   5.728 -        note f = absolutely_integrable_onD[OF f_int[of a b]]
   5.729 -        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
   5.730 -        have "e/2>0"
   5.731 -          using \<open>e > 0\<close> by auto
   5.732 -        from * [OF this] obtain d1 where
   5.733 -          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
   5.734 -            norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e / 2"
   5.735 -          by auto
   5.736 -        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
   5.737 -          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
   5.738 -            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
   5.739 -         obtain p where
   5.740 -          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
   5.741 -          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
   5.742 -            (auto simp add: fine_inter)
   5.743 -        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
   5.744 -          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
   5.745 -          by arith
   5.746 -        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
   5.747 -          apply (subst if_P)
   5.748 -          apply rule
   5.749 -        proof (rule *[rule_format])
   5.750 -          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"
   5.751 -            unfolding split_def
   5.752 -            apply (rule helplemma)
   5.753 -            using d2(2)[rule_format,of p]
   5.754 -            using p(1,3)
   5.755 -            unfolding tagged_division_of_def split_def
   5.756 -            apply auto
   5.757 -            done
   5.758 -          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"
   5.759 -            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
   5.760 -            by (simp only: real_norm_def)
   5.761 -          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))"
   5.762 -            apply (rule setsum.cong)
   5.763 -            apply (rule refl)
   5.764 -            unfolding split_paired_all split_conv
   5.765 -            apply (drule tagged_division_ofD(4)[OF p(1)])
   5.766 -            unfolding norm_scaleR
   5.767 -            apply (subst abs_of_nonneg)
   5.768 -            apply auto
   5.769 -            done
   5.770 -          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
   5.771 -            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
   5.772 -            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
   5.773 -            apply (simp add: integral_null)
   5.774 -            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
   5.775 -            apply (auto simp: tagged_partial_division_of_def)
   5.776 -            done
   5.777 -        qed
   5.778 -      qed
   5.779 -    qed (insert K, auto)
   5.780 -  qed
   5.781 -qed
   5.782 -
   5.783 -lemma absolutely_integrable_restrict_univ:
   5.784 -  "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow>
   5.785 -    f absolutely_integrable_on s"
   5.786 -  unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
   5.787 -
   5.788 -lemma absolutely_integrable_add[intro]:
   5.789 -  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.790 -  assumes "f absolutely_integrable_on s"
   5.791 -    and "g absolutely_integrable_on s"
   5.792 -  shows "(\<lambda>x. f x + g x) absolutely_integrable_on s"
   5.793 -proof -
   5.794 -  let ?P = "\<And>f g::'n \<Rightarrow> 'm. f absolutely_integrable_on UNIV \<Longrightarrow>
   5.795 -    g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
   5.796 -  {
   5.797 -    presume as: "PROP ?P"
   5.798 -    note a = absolutely_integrable_restrict_univ[symmetric]
   5.799 -    have *: "\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0) =
   5.800 -      (if x \<in> s then f x + g x else 0)" by auto
   5.801 -    show ?thesis
   5.802 -      apply (subst a)
   5.803 -      using as[OF assms[unfolded a[of f] a[of g]]]
   5.804 -      apply (simp only: *)
   5.805 -      done
   5.806 -  }
   5.807 -  fix f g :: "'n \<Rightarrow> 'm"
   5.808 -  assume assms: "f absolutely_integrable_on UNIV" "g absolutely_integrable_on UNIV"
   5.809 -  note absolutely_integrable_bounded_variation
   5.810 -  from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
   5.811 -  show "(\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
   5.812 -    apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
   5.813 -    apply (rule integrable_add)
   5.814 -    prefer 3
   5.815 -    apply safe
   5.816 -  proof goal_cases
   5.817 -    case prems: (1 d)
   5.818 -    have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
   5.819 -      apply (drule division_ofD(4)[OF prems])
   5.820 -      apply safe
   5.821 -      apply (rule_tac[!] integrable_on_subcbox[of _ UNIV])
   5.822 -      using assms
   5.823 -      apply auto
   5.824 -      done
   5.825 -    then have "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
   5.826 -      (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))"
   5.827 -      apply -
   5.828 -      unfolding setsum.distrib [symmetric]
   5.829 -      apply (rule setsum_mono)
   5.830 -      apply (subst integral_add)
   5.831 -      prefer 3
   5.832 -      apply (rule norm_triangle_ineq)
   5.833 -      apply auto
   5.834 -      done
   5.835 -    also have "\<dots> \<le> B1 + B2"
   5.836 -      using B(1)[OF prems] B(2)[OF prems] by auto
   5.837 -    finally show ?case .
   5.838 -  qed (insert assms, auto)
   5.839 -qed
   5.840 -
   5.841 -lemma absolutely_integrable_sub[intro]:
   5.842 -  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.843 -  assumes "f absolutely_integrable_on s"
   5.844 -    and "g absolutely_integrable_on s"
   5.845 -  shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
   5.846 -  using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
   5.847 -  by (simp add: algebra_simps)
   5.848 -
   5.849 -lemma absolutely_integrable_linear:
   5.850 -  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   5.851 -    and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
   5.852 -  assumes "f absolutely_integrable_on s"
   5.853 -    and "bounded_linear h"
   5.854 -  shows "(h \<circ> f) absolutely_integrable_on s"
   5.855 -proof -
   5.856 -  {
   5.857 -    presume as: "\<And>f::'m \<Rightarrow> 'n. \<And>h::'n \<Rightarrow> 'p. f absolutely_integrable_on UNIV \<Longrightarrow>
   5.858 -      bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on UNIV"
   5.859 -    note a = absolutely_integrable_restrict_univ[symmetric]
   5.860 -    show ?thesis
   5.861 -      apply (subst a)
   5.862 -      using as[OF assms[unfolded a[of f] a[of g]]]
   5.863 -      apply (simp only: o_def if_distrib linear_simps[OF assms(2)])
   5.864 -      done
   5.865 -  }
   5.866 -  fix f :: "'m \<Rightarrow> 'n"
   5.867 -  fix h :: "'n \<Rightarrow> 'p"
   5.868 -  assume assms: "f absolutely_integrable_on UNIV" "bounded_linear h"
   5.869 -  from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
   5.870 -  from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
   5.871 -  show "(h \<circ> f) absolutely_integrable_on UNIV"
   5.872 -    apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
   5.873 -    apply (rule integrable_linear[OF _ assms(2)])
   5.874 -    apply safe
   5.875 -  proof goal_cases
   5.876 -    case prems: (2 d)
   5.877 -    have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
   5.878 -      unfolding setsum_distrib_right
   5.879 -      apply (rule setsum_mono)
   5.880 -    proof goal_cases
   5.881 -      case (1 k)
   5.882 -      from division_ofD(4)[OF prems this]
   5.883 -      guess u v by (elim exE) note uv=this
   5.884 -      have *: "f integrable_on k"
   5.885 -        unfolding uv
   5.886 -        apply (rule integrable_on_subcbox[of _ UNIV])
   5.887 -        using assms
   5.888 -        apply auto
   5.889 -        done
   5.890 -      note this[unfolded has_integral_integral]
   5.891 -      note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
   5.892 -      note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
   5.893 -      show ?case
   5.894 -        unfolding * using b by auto
   5.895 -    qed
   5.896 -    also have "\<dots> \<le> B * b"
   5.897 -      apply (rule mult_right_mono)
   5.898 -      using B prems b
   5.899 -      apply auto
   5.900 -      done
   5.901 -    finally show ?case .
   5.902 -  qed (insert assms, auto)
   5.903 -qed
   5.904 -
   5.905 -lemma absolutely_integrable_setsum:
   5.906 -  fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.907 -  assumes "finite t"
   5.908 -    and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
   5.909 -  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
   5.910 -  using assms(1,2)
   5.911 -  by induct auto
   5.912 -
   5.913 -lemma absolutely_integrable_vector_abs:
   5.914 -  fixes f :: "'a::euclidean_space => 'b::euclidean_space"
   5.915 -    and T :: "'c::euclidean_space \<Rightarrow> 'b"
   5.916 -  assumes f: "f absolutely_integrable_on s"
   5.917 -  shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
   5.918 -  (is "?Tf absolutely_integrable_on s")
   5.919 -proof -
   5.920 -  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)"
   5.921 -    by simp
   5.922 -  have *: "\<And>x. ?Tf x = (\<Sum>i\<in>Basis.
   5.923 -    ((\<lambda>y. (\<Sum>j\<in>Basis. (if j = i then y else 0) *\<^sub>R j)) o
   5.924 -     (\<lambda>x. (norm (\<Sum>j\<in>Basis. (if j = i then f x\<bullet>T i else 0) *\<^sub>R j)))) x)"
   5.925 -    by (simp add: comp_def if_distrib setsum.If_cases)
   5.926 -  show ?thesis
   5.927 -    unfolding *
   5.928 -    apply (rule absolutely_integrable_setsum[OF finite_Basis])
   5.929 -    apply (rule absolutely_integrable_linear)
   5.930 -    apply (rule absolutely_integrable_norm)
   5.931 -    apply (rule absolutely_integrable_linear[OF f, unfolded o_def])
   5.932 -    apply (auto simp: linear_linear euclidean_eq_iff[where 'a='c] inner_simps intro!: linearI)
   5.933 -    done
   5.934 -qed
   5.935 -
   5.936 -lemma absolutely_integrable_max:
   5.937 -  fixes f g :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   5.938 -  assumes "f absolutely_integrable_on s"
   5.939 -    and "g absolutely_integrable_on s"
   5.940 -  shows "(\<lambda>x. (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
   5.941 -proof -
   5.942 -  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)) =
   5.943 -      (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
   5.944 -    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
   5.945 -  note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
   5.946 -  note absolutely_integrable_vector_abs[OF this(1), where T="\<lambda>x. x"] this(2)
   5.947 -  note absolutely_integrable_add[OF this]
   5.948 -  note absolutely_integrable_cmul[OF this, of "1/2"]
   5.949 -  then show ?thesis unfolding * .
   5.950 -qed
   5.951 -
   5.952 -lemma absolutely_integrable_min:
   5.953 -  fixes f g::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   5.954 -  assumes "f absolutely_integrable_on s"
   5.955 -    and "g absolutely_integrable_on s"
   5.956 -  shows "(\<lambda>x. (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)::'n) absolutely_integrable_on s"
   5.957 -proof -
   5.958 -  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)) =
   5.959 -      (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
   5.960 -    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
   5.961 -
   5.962 -  note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
   5.963 -  note this(1) absolutely_integrable_vector_abs[OF this(2), where T="\<lambda>x. x"]
   5.964 -  note absolutely_integrable_sub[OF this]
   5.965 -  note absolutely_integrable_cmul[OF this,of "1/2"]
   5.966 -  then show ?thesis unfolding * .
   5.967 -qed
   5.968 -
   5.969 -lemma absolutely_integrable_abs_eq:
   5.970 -  fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   5.971 -  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
   5.972 -    (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
   5.973 -  (is "?l = ?r")
   5.974 -proof
   5.975 -  assume ?l
   5.976 -  then show ?r
   5.977 -    apply -
   5.978 -    apply rule
   5.979 -    defer
   5.980 -    apply (drule absolutely_integrable_vector_abs)
   5.981 -    apply auto
   5.982 -    done
   5.983 -next
   5.984 -  assume ?r
   5.985 -  {
   5.986 -    presume lem: "\<And>f::'n \<Rightarrow> 'm. f integrable_on UNIV \<Longrightarrow>
   5.987 -      (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV \<Longrightarrow>
   5.988 -        f absolutely_integrable_on UNIV"
   5.989 -    have *: "\<And>x. (\<Sum>i\<in>Basis. \<bar>(if x \<in> s then f x else 0) \<bullet> i\<bar> *\<^sub>R i) =
   5.990 -      (if x \<in> s then (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) else (0::'m))"
   5.991 -      unfolding euclidean_eq_iff[where 'a='m]
   5.992 -      by auto
   5.993 -    show ?l
   5.994 -      apply (subst absolutely_integrable_restrict_univ[symmetric])
   5.995 -      apply (rule lem)
   5.996 -      unfolding integrable_restrict_univ *
   5.997 -      using \<open>?r\<close>
   5.998 -      apply auto
   5.999 -      done
  5.1000 -  }
  5.1001 -  fix f :: "'n \<Rightarrow> 'm"
  5.1002 -  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"
  5.1003 -  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"
  5.1004 -  show "f absolutely_integrable_on UNIV"
  5.1005 -    apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
  5.1006 -    apply safe
  5.1007 -  proof goal_cases
  5.1008 -    case d: (1 d)
  5.1009 -    note d'=division_ofD[OF d]
  5.1010 -    have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
  5.1011 -      (\<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)"
  5.1012 -      apply (rule setsum_mono)
  5.1013 -      apply (rule order_trans[OF norm_le_l1])
  5.1014 -      apply (rule setsum_mono)
  5.1015 -      unfolding lessThan_iff
  5.1016 -    proof -
  5.1017 -      fix k
  5.1018 -      fix i :: 'm
  5.1019 -      assume "k \<in> d" and i: "i \<in> Basis"
  5.1020 -      from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
  5.1021 -      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"
  5.1022 -        apply (rule abs_leI)
  5.1023 -        unfolding inner_minus_left[symmetric]
  5.1024 -        defer
  5.1025 -        apply (subst integral_neg[symmetric])
  5.1026 -        apply (rule_tac[1-2] integral_component_le[OF i])
  5.1027 -        using integrable_on_subcbox[OF assms(1),of a b]
  5.1028 -          integrable_on_subcbox[OF assms(2),of a b] i  integrable_neg
  5.1029 -        unfolding ab
  5.1030 -        apply auto
  5.1031 -        done
  5.1032 -    qed
  5.1033 -    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"
  5.1034 -      apply (subst setsum.commute)
  5.1035 -      apply (rule setsum_mono)
  5.1036 -    proof goal_cases
  5.1037 -      case (1 j)
  5.1038 -      have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
  5.1039 -        using integrable_on_subdivision[OF d assms(2)] by auto
  5.1040 -      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) =
  5.1041 -        integral (\<Union>d) (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
  5.1042 -        unfolding inner_setsum_left[symmetric] integral_combine_division_topdown[OF * d] ..
  5.1043 -      also have "\<dots> \<le> integral UNIV (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
  5.1044 -        apply (rule integral_subset_component_le)
  5.1045 -        using assms * \<open>j \<in> Basis\<close>
  5.1046 -        apply auto
  5.1047 -        done
  5.1048 -      finally show ?case .
  5.1049 -    qed
  5.1050 -    finally show ?case .
  5.1051 -  qed
  5.1052 -qed
  5.1053 -
  5.1054 -lemma nonnegative_absolutely_integrable:
  5.1055 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  5.1056 -  assumes "\<forall>x\<in>s. \<forall>i\<in>Basis. 0 \<le> f x \<bullet> i"
  5.1057 -    and "f integrable_on s"
  5.1058 -  shows "f absolutely_integrable_on s"
  5.1059 -  unfolding absolutely_integrable_abs_eq
  5.1060 -  apply rule
  5.1061 -  apply (rule assms)thm integrable_eq
  5.1062 -  apply (rule integrable_eq[of _ f])
  5.1063 -  using assms
  5.1064 -  apply (auto simp: euclidean_eq_iff[where 'a='m])
  5.1065 -  done
  5.1066 -
  5.1067 -lemma absolutely_integrable_integrable_bound:
  5.1068 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  5.1069 -  assumes "\<forall>x\<in>s. norm (f x) \<le> g x"
  5.1070 -    and "f integrable_on s"
  5.1071 -    and "g integrable_on s"
  5.1072 -  shows "f absolutely_integrable_on s"
  5.1073 -proof -
  5.1074 -  {
  5.1075 -    presume *: "\<And>f::'n \<Rightarrow> 'm. \<And>g. \<forall>x. norm (f x) \<le> g x \<Longrightarrow> f integrable_on UNIV \<Longrightarrow>
  5.1076 -      g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
  5.1077 -    show ?thesis
  5.1078 -      apply (subst absolutely_integrable_restrict_univ[symmetric])
  5.1079 -      apply (rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
  5.1080 -      using assms
  5.1081 -      unfolding integrable_restrict_univ
  5.1082 -      apply auto
  5.1083 -      done
  5.1084 -  }
  5.1085 -  fix g
  5.1086 -  fix f :: "'n \<Rightarrow> 'm"
  5.1087 -  assume assms: "\<forall>x. norm (f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
  5.1088 -  show "f absolutely_integrable_on UNIV"
  5.1089 -    apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
  5.1090 -    apply safe
  5.1091 -  proof goal_cases
  5.1092 -    case d: (1 d)
  5.1093 -    note d'=division_ofD[OF d]
  5.1094 -    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
  5.1095 -      apply (rule setsum_mono)
  5.1096 -      apply (rule integral_norm_bound_integral)
  5.1097 -      apply (drule_tac[!] d'(4))
  5.1098 -      apply safe
  5.1099 -      apply (rule_tac[1-2] integrable_on_subcbox)
  5.1100 -      using assms
  5.1101 -      apply auto
  5.1102 -      done
  5.1103 -    also have "\<dots> = integral (\<Union>d) g"
  5.1104 -      apply (rule integral_combine_division_bottomup[symmetric])
  5.1105 -      apply (rule d)
  5.1106 -      apply safe
  5.1107 -      apply (drule d'(4))
  5.1108 -      apply safe
  5.1109 -      apply (rule integrable_on_subcbox[OF assms(3)])
  5.1110 -      apply auto
  5.1111 -      done
  5.1112 -    also have "\<dots> \<le> integral UNIV g"
  5.1113 -      apply (rule integral_subset_le)
  5.1114 -      defer
  5.1115 -      apply (rule integrable_on_subdivision[OF d,of _ UNIV])
  5.1116 -      prefer 4
  5.1117 -      apply rule
  5.1118 -      apply (rule_tac y="norm (f x)" in order_trans)
  5.1119 -      using assms
  5.1120 -      apply auto
  5.1121 -      done
  5.1122 -    finally show ?case .
  5.1123 -  qed
  5.1124 -qed
  5.1125 -
  5.1126 -lemma absolutely_integrable_absolutely_integrable_bound:
  5.1127 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  5.1128 -    and g :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
  5.1129 -  assumes "\<forall>x\<in>s. norm (f x) \<le> norm (g x)"
  5.1130 -    and "f integrable_on s"
  5.1131 -    and "g absolutely_integrable_on s"
  5.1132 -  shows "f absolutely_integrable_on s"
  5.1133 -  apply (rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
  5.1134 -  using assms
  5.1135 -  apply auto
  5.1136 -  done
  5.1137 -
  5.1138 -lemma absolutely_integrable_inf_real:
  5.1139 -  assumes "finite k"
  5.1140 -    and "k \<noteq> {}"
  5.1141 -    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  5.1142 -  shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s"
  5.1143 -  using assms
  5.1144 -proof induct
  5.1145 -  case (insert a k)
  5.1146 -  let ?P = "(\<lambda>x.
  5.1147 -    if fs x ` k = {} then fs x a
  5.1148 -    else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
  5.1149 -  show ?case
  5.1150 -    unfolding image_insert
  5.1151 -    apply (subst Inf_insert_finite)
  5.1152 -    apply (rule finite_imageI[OF insert(1)])
  5.1153 -  proof (cases "k = {}")
  5.1154 -    case True
  5.1155 -    then show ?P
  5.1156 -      apply (subst if_P)
  5.1157 -      defer
  5.1158 -      apply (rule insert(5)[rule_format])
  5.1159 -      apply auto
  5.1160 -      done
  5.1161 -  next
  5.1162 -    case False
  5.1163 -    then show ?P
  5.1164 -      apply (subst if_not_P)
  5.1165 -      defer
  5.1166 -      apply (rule absolutely_integrable_min[where 'n=real, unfolded Basis_real_def, simplified])
  5.1167 -      defer
  5.1168 -      apply(rule insert(3)[OF False])
  5.1169 -      using insert(5)
  5.1170 -      apply auto
  5.1171 -      done
  5.1172 -  qed
  5.1173 -next
  5.1174 -  case empty
  5.1175 -  then show ?case by auto
  5.1176 -qed
  5.1177 -
  5.1178 -lemma absolutely_integrable_sup_real:
  5.1179 -  assumes "finite k"
  5.1180 -    and "k \<noteq> {}"
  5.1181 -    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  5.1182 -  shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s"
  5.1183 -  using assms
  5.1184 -proof induct
  5.1185 -  case (insert a k)
  5.1186 -  let ?P = "(\<lambda>x.
  5.1187 -    if fs x ` k = {} then fs x a
  5.1188 -    else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
  5.1189 -  show ?case
  5.1190 -    unfolding image_insert
  5.1191 -    apply (subst Sup_insert_finite)
  5.1192 -    apply (rule finite_imageI[OF insert(1)])
  5.1193 -  proof (cases "k = {}")
  5.1194 -    case True
  5.1195 -    then show ?P
  5.1196 -      apply (subst if_P)
  5.1197 -      defer
  5.1198 -      apply (rule insert(5)[rule_format])
  5.1199 -      apply auto
  5.1200 -      done
  5.1201 -  next
  5.1202 -    case False
  5.1203 -    then show ?P
  5.1204 -      apply (subst if_not_P)
  5.1205 -      defer
  5.1206 -      apply (rule absolutely_integrable_max[where 'n=real, unfolded Basis_real_def, simplified])
  5.1207 -      defer
  5.1208 -      apply (rule insert(3)[OF False])
  5.1209 -      using insert(5)
  5.1210 -      apply auto
  5.1211 -      done
  5.1212 -  qed
  5.1213 -qed auto
  5.1214 -
  5.1215 -
  5.1216  subsection \<open>differentiation under the integral sign\<close>
  5.1217  
  5.1218  lemma tube_lemma:
  5.1219 @@ -11296,8 +10103,7 @@
  5.1220            by (simp add: integral_diff dist_norm)
  5.1221          also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
  5.1222            using elim
  5.1223 -          by (intro integral_norm_bound_integral)
  5.1224 -            (auto intro!: integrable_diff absolutely_integrable_onI)
  5.1225 +          by (intro integral_norm_bound_integral) (auto intro!: integrable_diff)
  5.1226          also have "\<dots> < e"
  5.1227            using \<open>0 < e\<close>
  5.1228            by (simp add: e'_def)
  5.1229 @@ -11309,358 +10115,6 @@
  5.1230  qed
  5.1231  
  5.1232  
  5.1233 -subsection \<open>Dominated convergence\<close>
  5.1234 -
  5.1235 -context
  5.1236 -begin
  5.1237 -
  5.1238 -private lemma dominated_convergence_real:
  5.1239 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
  5.1240 -  assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
  5.1241 -    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  5.1242 -    and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
  5.1243 -  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  5.1244 -proof
  5.1245 -  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
  5.1246 -  proof (safe intro!: bdd_belowI)
  5.1247 -    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
  5.1248 -      using assms(3)[rule_format, of x n] by simp
  5.1249 -  qed
  5.1250 -  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
  5.1251 -  proof (safe intro!: bdd_aboveI)
  5.1252 -    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
  5.1253 -      using assms(3)[rule_format, of x n] by simp
  5.1254 -  qed
  5.1255 -
  5.1256 -  have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
  5.1257 -    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
  5.1258 -    integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
  5.1259 -  proof (rule monotone_convergence_decreasing, safe)
  5.1260 -    fix m :: nat
  5.1261 -    show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
  5.1262 -      unfolding bounded_iff
  5.1263 -      apply (rule_tac x="integral s h" in exI)
  5.1264 -    proof safe
  5.1265 -      fix k :: nat
  5.1266 -      show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  5.1267 -        apply (rule integral_norm_bound_integral)
  5.1268 -        unfolding Setcompr_eq_image
  5.1269 -        apply (rule absolutely_integrable_onD)
  5.1270 -        apply (rule absolutely_integrable_inf_real)
  5.1271 -        prefer 5
  5.1272 -        unfolding real_norm_def
  5.1273 -        apply rule
  5.1274 -        apply (rule cInf_abs_ge)
  5.1275 -        prefer 5
  5.1276 -        apply rule
  5.1277 -        apply (rule_tac g = h in absolutely_integrable_integrable_bound)
  5.1278 -        using assms
  5.1279 -        unfolding real_norm_def
  5.1280 -        apply auto
  5.1281 -        done
  5.1282 -    qed
  5.1283 -    fix k :: nat
  5.1284 -    show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  5.1285 -      unfolding Setcompr_eq_image
  5.1286 -      apply (rule absolutely_integrable_onD)
  5.1287 -      apply (rule absolutely_integrable_inf_real)
  5.1288 -      prefer 3
  5.1289 -      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
  5.1290 -      apply auto
  5.1291 -      done
  5.1292 -    fix x
  5.1293 -    assume x: "x \<in> s"
  5.1294 -    show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
  5.1295 -      by (rule cInf_superset_mono) auto
  5.1296 -    let ?S = "{f j x| j. m \<le> j}"
  5.1297 -    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Inf ?S) sequentially"
  5.1298 -    proof (rule LIMSEQ_I, goal_cases)
  5.1299 -      case r: (1 r)
  5.1300 -
  5.1301 -      have "\<exists>y\<in>?S. y < Inf ?S + r"
  5.1302 -        by (subst cInf_less_iff[symmetric]) (auto simp: \<open>x\<in>s\<close> r)
  5.1303 -      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
  5.1304 -        by blast
  5.1305 -
  5.1306 -      show ?case
  5.1307 -        apply (rule_tac x=N in exI)
  5.1308 -        apply safe
  5.1309 -      proof goal_cases
  5.1310 -        case prems: (1 n)
  5.1311 -        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> \<bar>ix - Inf ?S\<bar> < r"
  5.1312 -          by arith
  5.1313 -        show ?case
  5.1314 -          unfolding real_norm_def
  5.1315 -            apply (rule *[rule_format, OF N(1)])
  5.1316 -            apply (rule cInf_superset_mono, auto simp: \<open>x\<in>s\<close>) []
  5.1317 -            apply (rule cInf_lower)
  5.1318 -            using N prems
  5.1319 -            apply auto []
  5.1320 -            apply simp
  5.1321 -            done
  5.1322 -      qed
  5.1323 -    qed
  5.1324 -  qed
  5.1325 -  note dec1 = conjunctD2[OF this]
  5.1326 -
  5.1327 -  have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
  5.1328 -    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
  5.1329 -    integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
  5.1330 -  proof (rule monotone_convergence_increasing,safe)
  5.1331 -    fix m :: nat
  5.1332 -    show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
  5.1333 -      unfolding bounded_iff
  5.1334 -      apply (rule_tac x="integral s h" in exI)
  5.1335 -    proof safe
  5.1336 -      fix k :: nat
  5.1337 -      show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  5.1338 -        apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
  5.1339 -        apply (rule absolutely_integrable_onD)
  5.1340 -        apply(rule absolutely_integrable_sup_real)
  5.1341 -        prefer 5 unfolding real_norm_def
  5.1342 -        apply rule
  5.1343 -        apply (rule cSup_abs_le)
  5.1344 -        using assms
  5.1345 -        apply (force simp add: )
  5.1346 -        prefer 4
  5.1347 -        apply rule
  5.1348 -        apply (rule_tac g=h in absolutely_integrable_integrable_bound)
  5.1349 -        using assms
  5.1350 -        unfolding real_norm_def
  5.1351 -        apply auto
  5.1352 -        done
  5.1353 -    qed
  5.1354 -    fix k :: nat
  5.1355 -    show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  5.1356 -      unfolding Setcompr_eq_image
  5.1357 -      apply (rule absolutely_integrable_onD)
  5.1358 -      apply (rule absolutely_integrable_sup_real)
  5.1359 -      prefer 3
  5.1360 -      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
  5.1361 -      apply auto
  5.1362 -      done
  5.1363 -    fix x
  5.1364 -    assume x: "x\<in>s"
  5.1365 -    show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
  5.1366 -      by (rule cSup_subset_mono) auto
  5.1367 -    let ?S = "{f j x| j. m \<le> j}"
  5.1368 -    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Sup ?S) sequentially"
  5.1369 -    proof (rule LIMSEQ_I, goal_cases)
  5.1370 -      case r: (1 r)
  5.1371 -      have "\<exists>y\<in>?S. Sup ?S - r < y"
  5.1372 -        by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
  5.1373 -      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
  5.1374 -        by blast
  5.1375 -
  5.1376 -      show ?case
  5.1377 -        apply (rule_tac x=N in exI)
  5.1378 -        apply safe
  5.1379 -      proof goal_cases
  5.1380 -        case prems: (1 n)
  5.1381 -        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> \<bar>ix - Sup ?S\<bar> < r"
  5.1382 -          by arith
  5.1383 -        show ?case
  5.1384 -          apply simp
  5.1385 -          apply (rule *[rule_format, OF N(1)])
  5.1386 -          apply (rule cSup_subset_mono, auto simp: \<open>x\<in>s\<close>) []
  5.1387 -          apply (subst cSup_upper)
  5.1388 -          using N prems
  5.1389 -          apply auto
  5.1390 -          done
  5.1391 -      qed
  5.1392 -    qed
  5.1393 -  qed
  5.1394 -  note inc1 = conjunctD2[OF this]
  5.1395 -
  5.1396 -  have "g integrable_on s \<and>
  5.1397 -    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
  5.1398 -    apply (rule monotone_convergence_increasing,safe)
  5.1399 -    apply fact
  5.1400 -  proof -
  5.1401 -    show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
  5.1402 -      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  5.1403 -    proof safe
  5.1404 -      fix k :: nat
  5.1405 -      show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
  5.1406 -        apply (rule integral_norm_bound_integral)
  5.1407 -        apply fact+
  5.1408 -        unfolding real_norm_def
  5.1409 -        apply rule
  5.1410 -        apply (rule cInf_abs_ge)
  5.1411 -        using assms(3)
  5.1412 -        apply auto
  5.1413 -        done
  5.1414 -    qed
  5.1415 -    fix k :: nat and x
  5.1416 -    assume x: "x \<in> s"
  5.1417 -
  5.1418 -    have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  5.1419 -    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
  5.1420 -      by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
  5.1421 -
  5.1422 -    show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) \<longlonglongrightarrow> g x"
  5.1423 -    proof (rule LIMSEQ_I, goal_cases)
  5.1424 -      case r: (1 r)
  5.1425 -      then have "0<r/2"
  5.1426 -        by auto
  5.1427 -      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
  5.1428 -      show ?case
  5.1429 -        apply (rule_tac x=N in exI)
  5.1430 -        apply safe
  5.1431 -        unfolding real_norm_def
  5.1432 -        apply (rule le_less_trans[of _ "r/2"])
  5.1433 -        apply (rule cInf_asclose)
  5.1434 -        apply safe
  5.1435 -        defer
  5.1436 -        apply (rule less_imp_le)
  5.1437 -        using N r
  5.1438 -        apply auto
  5.1439 -        done
  5.1440 -    qed
  5.1441 -  qed
  5.1442 -  note inc2 = conjunctD2[OF this]
  5.1443 -
  5.1444 -  have "g integrable_on s \<and>
  5.1445 -    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
  5.1446 -    apply (rule monotone_convergence_decreasing,safe)
  5.1447 -    apply fact
  5.1448 -  proof -
  5.1449 -    show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
  5.1450 -      unfolding bounded_iff
  5.1451 -      apply (rule_tac x="integral s h" in exI)
  5.1452 -    proof safe
  5.1453 -      fix k :: nat
  5.1454 -      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
  5.1455 -        apply (rule integral_norm_bound_integral)
  5.1456 -        apply fact+
  5.1457 -        unfolding real_norm_def
  5.1458 -        apply rule
  5.1459 -        apply (rule cSup_abs_le)
  5.1460 -        using assms(3)
  5.1461 -        apply auto
  5.1462 -        done
  5.1463 -    qed
  5.1464 -    fix k :: nat
  5.1465 -    fix x
  5.1466 -    assume x: "x \<in> s"
  5.1467 -
  5.1468 -    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
  5.1469 -      by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
  5.1470 -    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) \<longlongrightarrow> g x) sequentially"
  5.1471 -    proof (rule LIMSEQ_I, goal_cases)
  5.1472 -      case r: (1 r)
  5.1473 -      then have "0<r/2"
  5.1474 -        by auto
  5.1475 -      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
  5.1476 -      show ?case
  5.1477 -        apply (rule_tac x=N in exI,safe)
  5.1478 -        unfolding real_norm_def
  5.1479 -        apply (rule le_less_trans[of _ "r/2"])
  5.1480 -        apply (rule cSup_asclose)
  5.1481 -        apply safe
  5.1482 -        defer
  5.1483 -        apply (rule less_imp_le)
  5.1484 -        using N r
  5.1485 -        apply auto
  5.1486 -        done
  5.1487 -    qed
  5.1488 -  qed
  5.1489 -  note dec2 = conjunctD2[OF this]
  5.1490 -
  5.1491 -  show "g integrable_on s" by fact
  5.1492 -  show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  5.1493 -  proof (rule LIMSEQ_I, goal_cases)
  5.1494 -    case r: (1 r)
  5.1495 -    from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
  5.1496 -    from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
  5.1497 -    show ?case
  5.1498 -    proof (rule_tac x="N1+N2" in exI, safe)
  5.1499 -      fix n
  5.1500 -      assume n: "n \<ge> N1 + N2"
  5.1501 -      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"
  5.1502 -        by arith
  5.1503 -      show "norm (integral s (f n) - integral s g) < r"
  5.1504 -        unfolding real_norm_def
  5.1505 -      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
  5.1506 -        show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
  5.1507 -          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
  5.1508 -        show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
  5.1509 -          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
  5.1510 -      qed (insert n, auto)
  5.1511 -    qed
  5.1512 -  qed
  5.1513 -qed
  5.1514 -
  5.1515 -lemma dominated_convergence:
  5.1516 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  5.1517 -  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
  5.1518 -    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  5.1519 -    and conv: "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
  5.1520 -  shows "g integrable_on s"
  5.1521 -    and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  5.1522 -proof -
  5.1523 -  {
  5.1524 -    fix b :: 'm assume b: "b \<in> Basis"
  5.1525 -    have A: "(\<lambda>x. g x \<bullet> b) integrable_on s \<and>
  5.1526 -               (\<lambda>k. integral s (\<lambda>x. f k x \<bullet> b)) \<longlonglongrightarrow> integral s (\<lambda>x. g x \<bullet> b)"
  5.1527 -    proof (rule dominated_convergence_real)
  5.1528 -      fix k :: nat
  5.1529 -      from f show "(\<lambda>x. f k x \<bullet> b) integrable_on s" by (rule integrable_component)
  5.1530 -    next
  5.1531 -      from h show "h integrable_on s" .
  5.1532 -    next
  5.1533 -      fix k :: nat
  5.1534 -      show "\<forall>x\<in>s. norm (f k x \<bullet> b) \<le> h x"
  5.1535 -      proof
  5.1536 -        fix x assume x: "x \<in> s"
  5.1537 -        have "norm (f k x \<bullet> b) \<le> norm (f k x)" by (simp add: Basis_le_norm b)
  5.1538 -        also have "\<dots> \<le> h x" using le[of k] x by simp
  5.1539 -        finally show "norm (f k x \<bullet> b) \<le> h x" .
  5.1540 -      qed
  5.1541 -    next
  5.1542 -      from conv show "\<forall>x\<in>s. (\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
  5.1543 -        by (auto intro!: tendsto_inner)
  5.1544 -    qed
  5.1545 -    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"
  5.1546 -      for k by (rule integral_linear)
  5.1547 -               (simp_all add: f integrable_component bounded_linear_scaleR_left)
  5.1548 -    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"
  5.1549 -      using A by (intro integral_linear)
  5.1550 -                 (simp_all add: integrable_component bounded_linear_scaleR_left)
  5.1551 -    note A B C
  5.1552 -  } note A = this
  5.1553 -
  5.1554 -  show "g integrable_on s" by (rule integrable_componentwise) (insert A, blast)
  5.1555 -  with A f show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  5.1556 -    by (subst (1 2) integral_componentwise)
  5.1557 -       (auto intro!: tendsto_setsum tendsto_scaleR simp: o_def)
  5.1558 -qed
  5.1559 -
  5.1560 -lemma has_integral_dominated_convergence:
  5.1561 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  5.1562 -  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
  5.1563 -    "\<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"
  5.1564 -    and x: "y \<longlonglongrightarrow> x"
  5.1565 -  shows "(g has_integral x) s"
  5.1566 -proof -
  5.1567 -  have int_f: "\<And>k. (f k) integrable_on s"
  5.1568 -    using assms by (auto simp: integrable_on_def)
  5.1569 -  have "(g has_integral (integral s g)) s"
  5.1570 -    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
  5.1571 -  moreover have "integral s g = x"
  5.1572 -  proof (rule LIMSEQ_unique)
  5.1573 -    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
  5.1574 -      using integral_unique[OF assms(1)] x by simp
  5.1575 -    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
  5.1576 -      by (intro dominated_convergence[OF int_f assms(2)]) fact+
  5.1577 -  qed
  5.1578 -  ultimately show ?thesis
  5.1579 -    by simp
  5.1580 -qed
  5.1581 -
  5.1582 -end
  5.1583 -
  5.1584 -
  5.1585  subsection \<open>Integration by parts\<close>
  5.1586  
  5.1587  lemma integration_by_parts_interior_strong:
     6.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 23 10:26:04 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Sep 23 18:34:34 2016 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  *)
     6.5  
     6.6  theory Interval_Integral
     6.7 -  imports Set_Integral
     6.8 +  imports Equivalence_Lebesgue_Henstock_Integration
     6.9  begin
    6.10  
    6.11  lemma continuous_on_vector_derivative:
    6.12 @@ -1062,19 +1062,16 @@
    6.13  qed
    6.14  
    6.15  
    6.16 -syntax
    6.17 -"_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
    6.18 -("(2CLBINT _. _)" [0,60] 60)
    6.19 +syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
    6.20 +  ("(2CLBINT _. _)" [0,60] 60)
    6.21 +
    6.22 +translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
    6.23 +
    6.24 +syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
    6.25 +  ("(3CLBINT _:_. _)" [0,60,61] 60)
    6.26  
    6.27  translations
    6.28 -"CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
    6.29 -
    6.30 -syntax
    6.31 -"_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
    6.32 -("(3CLBINT _:_. _)" [0,60,61] 60)
    6.33 -
    6.34 -translations
    6.35 -"CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    6.36 +  "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    6.37  
    6.38  abbreviation complex_interval_lebesgue_integral ::
    6.39      "real measure \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> (real \<Rightarrow> complex) \<Rightarrow> complex" where
     7.1 --- a/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 10:26:04 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Fri Sep 23 18:34:34 2016 +0200
     7.3 @@ -7,7 +7,7 @@
     7.4  *)
     7.5  
     7.6  theory Set_Integral
     7.7 -  imports Equivalence_Lebesgue_Henstock_Integration
     7.8 +  imports Bochner_Integration
     7.9  begin
    7.10  
    7.11  (*
    7.12 @@ -50,16 +50,10 @@
    7.13  "_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real"
    7.14  ("(2LBINT _./ _)" [0,60] 60)
    7.15  
    7.16 -translations
    7.17 -"LBINT x. f" == "CONST lebesgue_integral CONST lborel (\<lambda>x. f)"
    7.18 -
    7.19  syntax
    7.20  "_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> real"
    7.21  ("(3LBINT _:_./ _)" [0,60,61] 60)
    7.22  
    7.23 -translations
    7.24 -"LBINT x:A. f" == "CONST set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
    7.25 -
    7.26  (*
    7.27      Basic properties
    7.28  *)
    7.29 @@ -180,12 +174,6 @@
    7.30      (LINT x:A|M. f x) - (LINT x:A|M. g x)"
    7.31    using assms by (simp_all add: scaleR_diff_right)
    7.32  
    7.33 -lemma set_integral_reflect:
    7.34 -  fixes S and f :: "real \<Rightarrow> 'a :: {banach, second_countable_topology}"
    7.35 -  shows "(LBINT x : S. f x) = (LBINT x : {x. - x \<in> S}. f (- x))"
    7.36 -  by (subst lborel_integral_real_affine[where c="-1" and t=0])
    7.37 -     (auto intro!: Bochner_Integration.integral_cong split: split_indicator)
    7.38 -
    7.39  (* question: why do we have this for negation, but multiplication by a constant
    7.40     requires an integrability assumption? *)
    7.41  lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
    7.42 @@ -528,59 +516,6 @@
    7.43  translations
    7.44  "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\<lambda>x. f)"
    7.45  
    7.46 -(*
    7.47 -lemma cmod_mult: "cmod ((a :: real) * (x :: complex)) = \<bar>a\<bar> * cmod x"
    7.48 -  apply (simp add: norm_mult)
    7.49 -  by (subst norm_mult, auto)
    7.50 -*)
    7.51 -
    7.52 -lemma borel_integrable_atLeastAtMost':
    7.53 -  fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
    7.54 -  assumes f: "continuous_on {a..b} f"
    7.55 -  shows "set_integrable lborel {a..b} f" (is "integrable _ ?f")
    7.56 -  by (intro borel_integrable_compact compact_Icc f)
    7.57 -
    7.58 -lemma integral_FTC_atLeastAtMost:
    7.59 -  fixes f :: "real \<Rightarrow> 'a :: euclidean_space"
    7.60 -  assumes "a \<le> b"
    7.61 -    and F: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
    7.62 -    and f: "continuous_on {a .. b} f"
    7.63 -  shows "integral\<^sup>L lborel (\<lambda>x. indicator {a .. b} x *\<^sub>R f x) = F b - F a"
    7.64 -proof -
    7.65 -  let ?f = "\<lambda>x. indicator {a .. b} x *\<^sub>R f x"
    7.66 -  have "(?f has_integral (\<integral>x. ?f x \<partial>lborel)) UNIV"
    7.67 -    using borel_integrable_atLeastAtMost'[OF f] by (rule has_integral_integral_lborel)
    7.68 -  moreover
    7.69 -  have "(f has_integral F b - F a) {a .. b}"
    7.70 -    by (intro fundamental_theorem_of_calculus ballI assms) auto
    7.71 -  then have "(?f has_integral F b - F a) {a .. b}"
    7.72 -    by (subst has_integral_cong[where g=f]) auto
    7.73 -  then have "(?f has_integral F b - F a) UNIV"
    7.74 -    by (intro has_integral_on_superset[where t=UNIV and s="{a..b}"]) auto
    7.75 -  ultimately show "integral\<^sup>L lborel ?f = F b - F a"
    7.76 -    by (rule has_integral_unique)
    7.77 -qed
    7.78 -
    7.79 -lemma set_borel_integral_eq_integral:
    7.80 -  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
    7.81 -  assumes "set_integrable lborel S f"
    7.82 -  shows "f integrable_on S" "LINT x : S | lborel. f x = integral S f"
    7.83 -proof -
    7.84 -  let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
    7.85 -  have "(?f has_integral LINT x : S | lborel. f x) UNIV"
    7.86 -    by (rule has_integral_integral_lborel) fact
    7.87 -  hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
    7.88 -    apply (subst has_integral_restrict_univ [symmetric])
    7.89 -    apply (rule has_integral_eq)
    7.90 -    by auto
    7.91 -  thus "f integrable_on S"
    7.92 -    by (auto simp add: integrable_on_def)
    7.93 -  with 1 have "(f has_integral (integral S f)) S"
    7.94 -    by (intro integrable_integral, auto simp add: integrable_on_def)
    7.95 -  thus "LINT x : S | lborel. f x = integral S f"
    7.96 -    by (intro has_integral_unique [OF 1])
    7.97 -qed
    7.98 -
    7.99  lemma set_borel_measurable_continuous:
   7.100    fixes f :: "_ \<Rightarrow> _::real_normed_vector"
   7.101    assumes "S \<in> sets borel" "continuous_on S f"