author hoelzl Fri Sep 23 18:34:34 2016 +0200 (2016-09-23) changeset 63941 f353674c2528 parent 63940 0d82c4c94014 child 63942 9195600fcc7c
move absolutely_integrable_on to Equivalence_Lebesgue_Henstock_Integration, now based on the Lebesgue integral
```     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.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.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"
```