src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
changeset 63941 f353674c2528
parent 63940 0d82c4c94014
child 63944 21eaff8c8fc9
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 10:26:04 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 23 18:34:34 2016 +0200
     1.3 @@ -6180,7 +6180,7 @@
     1.4  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
     1.5  using assms
     1.6  by auto
     1.7 - 
     1.8 +
     1.9  
    1.10  lemma integrable_stretch:
    1.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
    1.12 @@ -9608,31 +9608,6 @@
    1.13      by auto
    1.14  qed
    1.15  
    1.16 -
    1.17 -subsection \<open>Absolute integrability (this is the same as Lebesgue integrability)\<close>
    1.18 -
    1.19 -definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46)
    1.20 -  where "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
    1.21 -
    1.22 -lemma absolutely_integrable_onI[intro?]:
    1.23 -  "f integrable_on s \<Longrightarrow>
    1.24 -    (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
    1.25 -  unfolding absolutely_integrable_on_def
    1.26 -  by auto
    1.27 -
    1.28 -lemma absolutely_integrable_onD[dest]:
    1.29 -  assumes "f absolutely_integrable_on s"
    1.30 -  shows "f integrable_on s"
    1.31 -    and "(\<lambda>x. norm (f x)) integrable_on s"
    1.32 -  using assms
    1.33 -  unfolding absolutely_integrable_on_def
    1.34 -  by auto
    1.35 -
    1.36 -(*lemma absolutely_integrable_on_trans[simp]:
    1.37 -  fixes f::"'n::euclidean_space \<Rightarrow> real"
    1.38 -  shows "(vec1 \<circ> f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
    1.39 -  unfolding absolutely_integrable_on_def o_def by auto*)
    1.40 -
    1.41  lemma integral_norm_bound_integral:
    1.42    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.43    assumes "f integrable_on s"
    1.44 @@ -9768,1174 +9743,6 @@
    1.45    using assms
    1.46    by auto
    1.47  
    1.48 -lemma absolutely_integrable_le:
    1.49 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.50 -  assumes "f absolutely_integrable_on s"
    1.51 -  shows "norm (integral s f) \<le> integral s (\<lambda>x. norm (f x))"
    1.52 -  apply (rule integral_norm_bound_integral)
    1.53 -  using assms
    1.54 -  apply auto
    1.55 -  done
    1.56 -
    1.57 -lemma absolutely_integrable_0[intro]:
    1.58 -  "(\<lambda>x. 0) absolutely_integrable_on s"
    1.59 -  unfolding absolutely_integrable_on_def
    1.60 -  by auto
    1.61 -
    1.62 -lemma absolutely_integrable_cmul[intro]:
    1.63 -  "f absolutely_integrable_on s \<Longrightarrow>
    1.64 -    (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
    1.65 -  unfolding absolutely_integrable_on_def
    1.66 -  using integrable_cmul[of f s c]
    1.67 -  using integrable_cmul[of "\<lambda>x. norm (f x)" s "\<bar>c\<bar>"]
    1.68 -  by auto
    1.69 -
    1.70 -lemma absolutely_integrable_neg[intro]:
    1.71 -  "f absolutely_integrable_on s \<Longrightarrow>
    1.72 -    (\<lambda>x. -f(x)) absolutely_integrable_on s"
    1.73 -  apply (drule absolutely_integrable_cmul[where c="-1"])
    1.74 -  apply auto
    1.75 -  done
    1.76 -
    1.77 -lemma absolutely_integrable_norm[intro]:
    1.78 -  "f absolutely_integrable_on s \<Longrightarrow>
    1.79 -    (\<lambda>x. norm (f x)) absolutely_integrable_on s"
    1.80 -  unfolding absolutely_integrable_on_def
    1.81 -  by auto
    1.82 -
    1.83 -lemma absolutely_integrable_abs[intro]:
    1.84 -  "f absolutely_integrable_on s \<Longrightarrow>
    1.85 -    (\<lambda>x. \<bar>f x::real\<bar>) absolutely_integrable_on s"
    1.86 -  apply (drule absolutely_integrable_norm)
    1.87 -  unfolding real_norm_def
    1.88 -  apply assumption
    1.89 -  done
    1.90 -
    1.91 -lemma absolutely_integrable_on_subinterval:
    1.92 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.93 -  shows "f absolutely_integrable_on s \<Longrightarrow>
    1.94 -    cbox a b \<subseteq> s \<Longrightarrow> f absolutely_integrable_on cbox a b"
    1.95 -  unfolding absolutely_integrable_on_def
    1.96 -  by (metis integrable_on_subcbox)
    1.97 -
    1.98 -lemma absolutely_integrable_bounded_variation:
    1.99 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
   1.100 -  assumes "f absolutely_integrable_on UNIV"
   1.101 -  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   1.102 -  apply (rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
   1.103 -  apply safe
   1.104 -proof goal_cases
   1.105 -  case prems: (1 d)
   1.106 -  note d = division_ofD[OF prems(2)]
   1.107 -  have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
   1.108 -    apply (rule setsum_mono,rule absolutely_integrable_le)
   1.109 -    apply (drule d(4))
   1.110 -    apply safe
   1.111 -    apply (rule absolutely_integrable_on_subinterval[OF assms])
   1.112 -    apply auto
   1.113 -    done
   1.114 -  also have "\<dots> \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
   1.115 -    apply (subst integral_combine_division_topdown[OF _ prems(2)])
   1.116 -    using integrable_on_subdivision[OF prems(2)]
   1.117 -    using assms
   1.118 -    apply auto
   1.119 -    done
   1.120 -  also have "\<dots> \<le> integral UNIV (\<lambda>x. norm (f x))"
   1.121 -    apply (rule integral_subset_le)
   1.122 -    using integrable_on_subdivision[OF prems(2)]
   1.123 -    using assms
   1.124 -    apply auto
   1.125 -    done
   1.126 -  finally show ?case .
   1.127 -qed
   1.128 -
   1.129 -lemma helplemma:
   1.130 -  assumes "setsum (\<lambda>x. norm (f x - g x)) s < e"
   1.131 -    and "finite s"
   1.132 -  shows "\<bar>setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s\<bar> < e"
   1.133 -  unfolding setsum_subtractf[symmetric]
   1.134 -  apply (rule le_less_trans[OF setsum_abs])
   1.135 -  apply (rule le_less_trans[OF _ assms(1)])
   1.136 -  apply (rule setsum_mono)
   1.137 -  apply (rule norm_triangle_ineq3)
   1.138 -  done
   1.139 -
   1.140 -lemma bounded_variation_absolutely_integrable_interval:
   1.141 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.142 -  assumes f: "f integrable_on cbox a b"
   1.143 -    and *: "\<forall>d. d division_of (cbox a b) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   1.144 -  shows "f absolutely_integrable_on cbox a b"
   1.145 -proof -
   1.146 -  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of (cbox a b)}"
   1.147 -  have D_1: "?D \<noteq> {}"
   1.148 -    by (rule elementary_interval[of a b]) auto
   1.149 -  have D_2: "bdd_above (?f`?D)"
   1.150 -    by (metis * mem_Collect_eq bdd_aboveI2)
   1.151 -  note D = D_1 D_2
   1.152 -  let ?S = "SUP x:?D. ?f x"
   1.153 -  show ?thesis
   1.154 -    apply (rule absolutely_integrable_onI [OF f has_integral_integrable])
   1.155 -    apply (subst has_integral[of _ ?S])
   1.156 -    apply safe
   1.157 -  proof goal_cases
   1.158 -    case e: (1 e)
   1.159 -    then have "?S - e / 2 < ?S" by simp
   1.160 -    then obtain d where d: "d division_of (cbox a b)" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
   1.161 -      unfolding less_cSUP_iff[OF D] by auto
   1.162 -    note d' = division_ofD[OF this(1)]
   1.163 -
   1.164 -    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   1.165 -    proof
   1.166 -      fix x
   1.167 -      have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
   1.168 -        apply (rule separate_point_closed)
   1.169 -        apply (rule closed_Union)
   1.170 -        apply (rule finite_subset[OF _ d'(1)])
   1.171 -        using d'(4)
   1.172 -        apply auto
   1.173 -        done
   1.174 -      then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
   1.175 -        by force
   1.176 -    qed
   1.177 -    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
   1.178 -
   1.179 -    have "e/2 > 0"
   1.180 -      using e by auto
   1.181 -    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
   1.182 -    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
   1.183 -    show ?case
   1.184 -      apply (rule_tac x="?g" in exI)
   1.185 -      apply safe
   1.186 -    proof -
   1.187 -      show "gauge ?g"
   1.188 -        using g(1) k(1)
   1.189 -        unfolding gauge_def
   1.190 -        by auto
   1.191 -      fix p
   1.192 -      assume "p tagged_division_of (cbox a b)" and "?g fine p"
   1.193 -      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
   1.194 -      note p' = tagged_division_ofD[OF p(1)]
   1.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}"
   1.196 -      have gp': "g fine p'"
   1.197 -        using p(2)
   1.198 -        unfolding p'_def fine_def
   1.199 -        by auto
   1.200 -      have p'': "p' tagged_division_of (cbox a b)"
   1.201 -        apply (rule tagged_division_ofI)
   1.202 -      proof -
   1.203 -        show "finite p'"
   1.204 -          apply (rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l)) `
   1.205 -            {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"])
   1.206 -          unfolding p'_def
   1.207 -          defer
   1.208 -          apply (rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
   1.209 -          apply safe
   1.210 -          unfolding image_iff
   1.211 -          apply (rule_tac x="(i,x,l)" in bexI)
   1.212 -          apply auto
   1.213 -          done
   1.214 -        fix x k
   1.215 -        assume "(x, k) \<in> p'"
   1.216 -        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   1.217 -          unfolding p'_def by auto
   1.218 -        then guess i l by (elim exE) note il=conjunctD4[OF this]
   1.219 -        show "x \<in> k" and "k \<subseteq> cbox a b"
   1.220 -          using p'(2-3)[OF il(3)] il by auto
   1.221 -        show "\<exists>a b. k = cbox a b"
   1.222 -          unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
   1.223 -          apply safe
   1.224 -          unfolding inter_interval
   1.225 -          apply auto
   1.226 -          done
   1.227 -      next
   1.228 -        fix x1 k1
   1.229 -        assume "(x1, k1) \<in> p'"
   1.230 -        then have "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l"
   1.231 -          unfolding p'_def by auto
   1.232 -        then guess i1 l1 by (elim exE) note il1=conjunctD4[OF this]
   1.233 -        fix x2 k2
   1.234 -        assume "(x2,k2)\<in>p'"
   1.235 -        then have "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l"
   1.236 -          unfolding p'_def by auto
   1.237 -        then guess i2 l2 by (elim exE) note il2=conjunctD4[OF this]
   1.238 -        assume "(x1, k1) \<noteq> (x2, k2)"
   1.239 -        then have "interior i1 \<inter> interior i2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   1.240 -          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)]
   1.241 -          unfolding il1 il2
   1.242 -          by auto
   1.243 -        then show "interior k1 \<inter> interior k2 = {}"
   1.244 -          unfolding il1 il2 by auto
   1.245 -      next
   1.246 -        have *: "\<forall>(x, X) \<in> p'. X \<subseteq> cbox a b"
   1.247 -          unfolding p'_def using d' by auto
   1.248 -        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = cbox a b"
   1.249 -          apply rule
   1.250 -          apply (rule Union_least)
   1.251 -          unfolding mem_Collect_eq
   1.252 -          apply (erule exE)
   1.253 -          apply (drule *[rule_format])
   1.254 -          apply safe
   1.255 -        proof -
   1.256 -          fix y
   1.257 -          assume y: "y \<in> cbox a b"
   1.258 -          then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
   1.259 -            unfolding p'(6)[symmetric] by auto
   1.260 -          then guess x l by (elim exE) note xl=conjunctD2[OF this]
   1.261 -          then have "\<exists>k. k \<in> d \<and> y \<in> k"
   1.262 -            using y unfolding d'(6)[symmetric] by auto
   1.263 -          then guess i .. note i = conjunctD2[OF this]
   1.264 -          have "x \<in> i"
   1.265 -            using fineD[OF p(3) xl(1)]
   1.266 -            using k(2)[OF i(1), of x]
   1.267 -            using i(2) xl(2)
   1.268 -            by auto
   1.269 -          then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
   1.270 -            unfolding p'_def Union_iff
   1.271 -            apply (rule_tac x="i \<inter> l" in bexI)
   1.272 -            using i xl
   1.273 -            apply auto
   1.274 -            done
   1.275 -        qed
   1.276 -      qed
   1.277 -
   1.278 -      then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
   1.279 -        apply -
   1.280 -        apply (rule g(2)[rule_format])
   1.281 -        unfolding tagged_division_of_def
   1.282 -        apply safe
   1.283 -        apply (rule gp')
   1.284 -        done
   1.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"
   1.286 -        unfolding split_def
   1.287 -        using p''
   1.288 -        by (force intro!: helplemma)
   1.289 -
   1.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> {}}"
   1.291 -      proof (safe, goal_cases)
   1.292 -        case prems: (2 _ _ x i l)
   1.293 -        have "x \<in> i"
   1.294 -          using fineD[OF p(3) prems(1)] k(2)[OF prems(2), of x] prems(4-)
   1.295 -          by auto
   1.296 -        then have "(x, i \<inter> l) \<in> p'"
   1.297 -          unfolding p'_def
   1.298 -          using prems
   1.299 -          apply safe
   1.300 -          apply (rule_tac x=x in exI)
   1.301 -          apply (rule_tac x="i \<inter> l" in exI)
   1.302 -          apply safe
   1.303 -          using prems
   1.304 -          apply auto
   1.305 -          done
   1.306 -        then show ?case
   1.307 -          using prems(3) by auto
   1.308 -      next
   1.309 -        fix x k
   1.310 -        assume "(x, k) \<in> p'"
   1.311 -        then have "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l"
   1.312 -          unfolding p'_def by auto
   1.313 -        then guess i l by (elim exE) note il=conjunctD4[OF this]
   1.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> {}"
   1.315 -          apply (rule_tac x=x in exI)
   1.316 -          apply (rule_tac x=i in exI)
   1.317 -          apply (rule_tac x=l in exI)
   1.318 -          using p'(2)[OF il(3)]
   1.319 -          apply auto
   1.320 -          done
   1.321 -      qed
   1.322 -      have sum_p': "(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
   1.323 -        apply (subst setsum.over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
   1.324 -        unfolding norm_eq_zero
   1.325 -        apply (rule integral_null)
   1.326 -        apply assumption
   1.327 -        apply rule
   1.328 -        done
   1.329 -      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
   1.330 -
   1.331 -      have *: "\<And>sni sni' sf sf'. \<bar>sf' - sni'\<bar> < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
   1.332 -        sni \<le> sni' \<and> sf' = sf \<longrightarrow> \<bar>sf - ?S\<bar> < e"
   1.333 -        by arith
   1.334 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
   1.335 -        unfolding real_norm_def
   1.336 -        apply (rule *[rule_format,OF **])
   1.337 -        apply safe
   1.338 -        apply(rule d(2))
   1.339 -      proof goal_cases
   1.340 -        case 1
   1.341 -        show ?case
   1.342 -          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
   1.343 -      next
   1.344 -        case 2
   1.345 -        have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
   1.346 -          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}"
   1.347 -          by auto
   1.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))"
   1.349 -        proof (rule setsum_mono, goal_cases)
   1.350 -          case k: (1 k)
   1.351 -          from d'(4)[OF this] guess u v by (elim exE) note uv=this
   1.352 -          define d' where "d' = {cbox u v \<inter> l |l. l \<in> snd ` p \<and>  cbox u v \<inter> l \<noteq> {}}"
   1.353 -          note uvab = d'(2)[OF k[unfolded uv]]
   1.354 -          have "d' division_of cbox u v"
   1.355 -            apply (subst d'_def)
   1.356 -            apply (rule division_inter_1)
   1.357 -            apply (rule division_of_tagged_division[OF p(1)])
   1.358 -            apply (rule uvab)
   1.359 -            done
   1.360 -          then have "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
   1.361 -            unfolding uv
   1.362 -            apply (subst integral_combine_division_topdown[of _ _ d'])
   1.363 -            apply (rule integrable_on_subcbox[OF assms(1) uvab])
   1.364 -            apply assumption
   1.365 -            apply (rule setsum_norm_le)
   1.366 -            apply auto
   1.367 -            done
   1.368 -          also have "\<dots> = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
   1.369 -            apply (rule setsum.mono_neutral_left)
   1.370 -            apply (subst Setcompr_eq_image)
   1.371 -            apply (rule finite_imageI)+
   1.372 -            apply fact
   1.373 -            unfolding d'_def uv
   1.374 -            apply blast
   1.375 -          proof (rule, goal_cases)
   1.376 -            case prems: (1 i)
   1.377 -            then have "i \<in> {cbox u v \<inter> l |l. l \<in> snd ` p}"
   1.378 -              by auto
   1.379 -            from this[unfolded mem_Collect_eq] guess l .. note l=this
   1.380 -            then have "cbox u v \<inter> l = {}"
   1.381 -              using prems by auto
   1.382 -            then show ?case
   1.383 -              using l by auto
   1.384 -          qed
   1.385 -          also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))"
   1.386 -            unfolding Setcompr_eq_image
   1.387 -            apply (rule setsum.reindex_nontrivial [unfolded o_def])
   1.388 -            apply (rule finite_imageI)
   1.389 -            apply (rule p')
   1.390 -          proof goal_cases
   1.391 -            case prems: (1 l y)
   1.392 -            have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)"
   1.393 -              apply (subst(2) interior_Int)
   1.394 -              apply (rule Int_greatest)
   1.395 -              defer
   1.396 -              apply (subst prems(4))
   1.397 -              apply auto
   1.398 -              done
   1.399 -            then have *: "interior (k \<inter> l) = {}"
   1.400 -              using snd_p(5)[OF prems(1-3)] by auto
   1.401 -            from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   1.402 -            show ?case
   1.403 -              using *
   1.404 -              unfolding uv inter_interval content_eq_0_interior[symmetric]
   1.405 -              by auto
   1.406 -          qed
   1.407 -          finally show ?case .
   1.408 -        qed
   1.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))"
   1.410 -          apply (subst sum_sum_product[symmetric])
   1.411 -          apply fact
   1.412 -          using p'(1)
   1.413 -          apply auto
   1.414 -          done
   1.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))"
   1.416 -          unfolding split_def ..
   1.417 -        also have "\<dots> = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
   1.418 -          unfolding *
   1.419 -          apply (rule setsum.reindex_nontrivial [symmetric, unfolded o_def])
   1.420 -          apply (rule finite_product_dependent)
   1.421 -          apply fact
   1.422 -          apply (rule finite_imageI)
   1.423 -          apply (rule p')
   1.424 -          unfolding split_paired_all mem_Collect_eq split_conv o_def
   1.425 -        proof -
   1.426 -          note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
   1.427 -          fix l1 l2 k1 k2
   1.428 -          assume as:
   1.429 -            "(l1, k1) \<noteq> (l2, k2)"
   1.430 -            "l1 \<inter> k1 = l2 \<inter> k2"
   1.431 -            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   1.432 -            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
   1.433 -          then have "l1 \<in> d" and "k1 \<in> snd ` p"
   1.434 -            by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
   1.435 -          guess u1 v1 u2 v2 by (elim exE) note uv=this
   1.436 -          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   1.437 -            using as by auto
   1.438 -          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   1.439 -            apply -
   1.440 -            apply (erule disjE)
   1.441 -            apply (rule disjI2)
   1.442 -            apply (rule d'(5))
   1.443 -            prefer 4
   1.444 -            apply (rule disjI1)
   1.445 -            apply (rule *)
   1.446 -            using as
   1.447 -            apply auto
   1.448 -            done
   1.449 -          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   1.450 -            using as(2) by auto
   1.451 -          ultimately have "interior(l1 \<inter> k1) = {}"
   1.452 -            by auto
   1.453 -          then show "norm (integral (l1 \<inter> k1) f) = 0"
   1.454 -            unfolding uv inter_interval
   1.455 -            unfolding content_eq_0_interior[symmetric]
   1.456 -            by auto
   1.457 -        qed
   1.458 -        also have "\<dots> = (\<Sum>(x, k)\<in>p'. norm (integral k f))"
   1.459 -          unfolding sum_p'
   1.460 -          apply (rule setsum.mono_neutral_right)
   1.461 -          apply (subst *)
   1.462 -          apply (rule finite_imageI[OF finite_product_dependent])
   1.463 -          apply fact
   1.464 -          apply (rule finite_imageI[OF p'(1)])
   1.465 -          apply safe
   1.466 -        proof goal_cases
   1.467 -          case (2 i ia l a b)
   1.468 -          then have "ia \<inter> b = {}"
   1.469 -            unfolding p'alt image_iff Bex_def not_ex
   1.470 -            apply (erule_tac x="(a, ia \<inter> b)" in allE)
   1.471 -            apply auto
   1.472 -            done
   1.473 -          then show ?case
   1.474 -            by auto
   1.475 -        next
   1.476 -          case (1 x a b)
   1.477 -          then show ?case
   1.478 -            unfolding p'_def
   1.479 -            apply safe
   1.480 -            apply (rule_tac x=i in exI)
   1.481 -            apply (rule_tac x=l in exI)
   1.482 -            unfolding snd_conv image_iff
   1.483 -            apply safe
   1.484 -            apply (rule_tac x="(a,l)" in bexI)
   1.485 -            apply auto
   1.486 -            done
   1.487 -        qed
   1.488 -        finally show ?case .
   1.489 -      next
   1.490 -        case 3
   1.491 -        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
   1.492 -        have Sigma_alt: "\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}"
   1.493 -          by auto
   1.494 -        have *: "?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)"
   1.495 -          apply safe
   1.496 -          unfolding image_iff
   1.497 -          apply (rule_tac x="((x,l),i)" in bexI)
   1.498 -          apply auto
   1.499 -          done
   1.500 -        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
   1.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))"
   1.502 -          unfolding norm_scaleR
   1.503 -          apply (rule setsum.mono_neutral_left)
   1.504 -          apply (subst *)
   1.505 -          apply (rule finite_imageI)
   1.506 -          apply fact
   1.507 -          unfolding p'alt
   1.508 -          apply blast
   1.509 -          apply safe
   1.510 -          apply (rule_tac x=x in exI)
   1.511 -          apply (rule_tac x=i in exI)
   1.512 -          apply (rule_tac x=l in exI)
   1.513 -          apply auto
   1.514 -          done
   1.515 -        also have "\<dots> = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))"
   1.516 -          unfolding *
   1.517 -          apply (subst setsum.reindex_nontrivial)
   1.518 -          apply fact
   1.519 -          unfolding split_paired_all
   1.520 -          unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff prod.inject
   1.521 -          apply (elim conjE)
   1.522 -        proof -
   1.523 -          fix x1 l1 k1 x2 l2 k2
   1.524 -          assume as: "(x1, l1) \<in> p" "(x2, l2) \<in> p" "k1 \<in> d" "k2 \<in> d"
   1.525 -            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
   1.526 -          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this
   1.527 -          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2"
   1.528 -            by auto
   1.529 -          then have "interior k1 \<inter> interior k2 = {} \<or> interior l1 \<inter> interior l2 = {}"
   1.530 -            apply -
   1.531 -            apply (erule disjE)
   1.532 -            apply (rule disjI2)
   1.533 -            defer
   1.534 -            apply (rule disjI1)
   1.535 -            apply (rule d'(5)[OF as(3-4)])
   1.536 -            apply assumption
   1.537 -            apply (rule p'(5)[OF as(1-2)])
   1.538 -            apply auto
   1.539 -            done
   1.540 -          moreover have "interior (l1 \<inter> k1) = interior (l2 \<inter> k2)"
   1.541 -            unfolding  as ..
   1.542 -          ultimately have "interior (l1 \<inter> k1) = {}"
   1.543 -            by auto
   1.544 -          then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
   1.545 -            unfolding uv inter_interval
   1.546 -            unfolding content_eq_0_interior[symmetric]
   1.547 -            by auto
   1.548 -        qed safe
   1.549 -        also have "\<dots> = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))"
   1.550 -          unfolding Sigma_alt
   1.551 -          apply (subst sum_sum_product[symmetric])
   1.552 -          apply (rule p')
   1.553 -          apply rule
   1.554 -          apply (rule d')
   1.555 -          apply (rule setsum.cong)
   1.556 -          apply (rule refl)
   1.557 -          unfolding split_paired_all split_conv
   1.558 -        proof -
   1.559 -          fix x l
   1.560 -          assume as: "(x, l) \<in> p"
   1.561 -          note xl = p'(2-4)[OF this]
   1.562 -          from this(3) guess u v by (elim exE) note uv=this
   1.563 -          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> cbox u v))"
   1.564 -            apply (rule setsum.cong)
   1.565 -            apply (rule refl)
   1.566 -            apply (drule d'(4))
   1.567 -            apply safe
   1.568 -            apply (subst Int_commute)
   1.569 -            unfolding inter_interval uv
   1.570 -            apply (subst abs_of_nonneg)
   1.571 -            apply auto
   1.572 -            done
   1.573 -          also have "\<dots> = setsum content {k \<inter> cbox u v| k. k \<in> d}"
   1.574 -            unfolding Setcompr_eq_image
   1.575 -            apply (rule setsum.reindex_nontrivial [unfolded o_def, symmetric])
   1.576 -            apply (rule d')
   1.577 -          proof goal_cases
   1.578 -            case prems: (1 k y)
   1.579 -            from d'(4)[OF this(1)] d'(4)[OF this(2)]
   1.580 -            guess u1 v1 u2 v2 by (elim exE) note uv=this
   1.581 -            have "{} = interior ((k \<inter> y) \<inter> cbox u v)"
   1.582 -              apply (subst interior_Int)
   1.583 -              using d'(5)[OF prems(1-3)]
   1.584 -              apply auto
   1.585 -              done
   1.586 -            also have "\<dots> = interior (y \<inter> (k \<inter> cbox u v))"
   1.587 -              by auto
   1.588 -            also have "\<dots> = interior (k \<inter> cbox u v)"
   1.589 -              unfolding prems(4) by auto
   1.590 -            finally show ?case
   1.591 -              unfolding uv inter_interval content_eq_0_interior ..
   1.592 -          qed
   1.593 -          also have "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
   1.594 -            apply (rule setsum.mono_neutral_right)
   1.595 -            unfolding Setcompr_eq_image
   1.596 -            apply (rule finite_imageI)
   1.597 -            apply (rule d')
   1.598 -            apply blast
   1.599 -            apply safe
   1.600 -            apply (rule_tac x=k in exI)
   1.601 -          proof goal_cases
   1.602 -            case prems: (1 i k)
   1.603 -            from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
   1.604 -            have "interior (k \<inter> cbox u v) \<noteq> {}"
   1.605 -              using prems(2)
   1.606 -              unfolding ab inter_interval content_eq_0_interior
   1.607 -              by auto
   1.608 -            then show ?case
   1.609 -              using prems(1)
   1.610 -              using interior_subset[of "k \<inter> cbox u v"]
   1.611 -              by auto
   1.612 -          qed
   1.613 -          finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
   1.614 -            unfolding setsum_distrib_right[symmetric] real_scaleR_def
   1.615 -            apply (subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
   1.616 -            using xl(2)[unfolded uv]
   1.617 -            unfolding uv
   1.618 -            apply auto
   1.619 -            done
   1.620 -        qed
   1.621 -        finally show ?case .
   1.622 -      qed
   1.623 -    qed
   1.624 -  qed
   1.625 -qed
   1.626 -
   1.627 -lemma bounded_variation_absolutely_integrable:
   1.628 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.629 -  assumes "f integrable_on UNIV"
   1.630 -    and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   1.631 -  shows "f absolutely_integrable_on UNIV"
   1.632 -proof (rule absolutely_integrable_onI, fact, rule)
   1.633 -  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
   1.634 -  have D_1: "?D \<noteq> {}"
   1.635 -    by (rule elementary_interval) auto
   1.636 -  have D_2: "bdd_above (?f`?D)"
   1.637 -    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
   1.638 -  note D = D_1 D_2
   1.639 -  let ?S = "SUP d:?D. ?f d"
   1.640 -  have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
   1.641 -    apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
   1.642 -    apply (rule integrable_on_subcbox[OF assms(1)])
   1.643 -    defer
   1.644 -    apply safe
   1.645 -    apply (rule assms(2)[rule_format])
   1.646 -    apply auto
   1.647 -    done
   1.648 -  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
   1.649 -    apply (subst has_integral_alt')
   1.650 -    apply safe
   1.651 -  proof goal_cases
   1.652 -    case (1 a b)
   1.653 -    show ?case
   1.654 -      using f_int[of a b] by auto
   1.655 -  next
   1.656 -    case prems: (2 e)
   1.657 -    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
   1.658 -    proof (rule ccontr)
   1.659 -      assume "\<not> ?thesis"
   1.660 -      then have "?S \<le> ?S - e"
   1.661 -        by (intro cSUP_least[OF D(1)]) auto
   1.662 -      then show False
   1.663 -        using prems by auto
   1.664 -    qed
   1.665 -    then obtain K where *: "\<exists>x\<in>{d. d division_of \<Union>d}. K = (\<Sum>k\<in>x. norm (integral k f))"
   1.666 -      "SUPREMUM {d. d division_of \<Union>d} (setsum (\<lambda>k. norm (integral k f))) - e < K"
   1.667 -      by (auto simp add: image_iff not_le)
   1.668 -    from this(1) obtain d where "d division_of \<Union>d"
   1.669 -      and "K = (\<Sum>k\<in>d. norm (integral k f))"
   1.670 -      by auto
   1.671 -    note d = this(1) *(2)[unfolded this(2)]
   1.672 -    note d'=division_ofD[OF this(1)]
   1.673 -    have "bounded (\<Union>d)"
   1.674 -      by (rule elementary_bounded,fact)
   1.675 -    from this[unfolded bounded_pos] obtain K where
   1.676 -       K: "0 < K" "\<forall>x\<in>\<Union>d. norm x \<le> K" by auto
   1.677 -    show ?case
   1.678 -      apply (rule_tac x="K + 1" in exI)
   1.679 -      apply safe
   1.680 -    proof -
   1.681 -      fix a b :: 'n
   1.682 -      assume ab: "ball 0 (K + 1) \<subseteq> cbox a b"
   1.683 -      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> \<bar>s - ?S\<bar> < e"
   1.684 -        by arith
   1.685 -      show "norm (integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
   1.686 -        unfolding real_norm_def
   1.687 -        apply (rule *[rule_format])
   1.688 -        apply safe
   1.689 -        apply (rule d(2))
   1.690 -      proof goal_cases
   1.691 -        case 1
   1.692 -        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
   1.693 -          apply (rule setsum_mono)
   1.694 -          apply (rule absolutely_integrable_le)
   1.695 -          apply (drule d'(4))
   1.696 -          apply safe
   1.697 -          apply (rule f_int)
   1.698 -          done
   1.699 -        also have "\<dots> = integral (\<Union>d) (\<lambda>x. norm (f x))"
   1.700 -          apply (rule integral_combine_division_bottomup[symmetric])
   1.701 -          apply (rule d)
   1.702 -          unfolding forall_in_division[OF d(1)]
   1.703 -          using f_int
   1.704 -          apply auto
   1.705 -          done
   1.706 -        also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)"
   1.707 -        proof -
   1.708 -          have "\<Union>d \<subseteq> cbox a b"
   1.709 -            apply rule
   1.710 -            apply (drule K(2)[rule_format])
   1.711 -            apply (rule ab[unfolded subset_eq,rule_format])
   1.712 -            apply (auto simp add: dist_norm)
   1.713 -            done
   1.714 -          then show ?thesis
   1.715 -            apply -
   1.716 -            apply (subst if_P)
   1.717 -            apply rule
   1.718 -            apply (rule integral_subset_le)
   1.719 -            defer
   1.720 -            apply (rule integrable_on_subdivision[of _ _ _ "cbox a b"])
   1.721 -            apply (rule d)
   1.722 -            using f_int[of a b]
   1.723 -            apply auto
   1.724 -            done
   1.725 -        qed
   1.726 -        finally show ?case .
   1.727 -      next
   1.728 -        note f = absolutely_integrable_onD[OF f_int[of a b]]
   1.729 -        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
   1.730 -        have "e/2>0"
   1.731 -          using \<open>e > 0\<close> by auto
   1.732 -        from * [OF this] obtain d1 where
   1.733 -          d1: "gauge d1" "\<forall>p. p tagged_division_of (cbox a b) \<and> d1 fine p \<longrightarrow>
   1.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"
   1.735 -          by auto
   1.736 -        from henstock_lemma [OF f(1) \<open>e/2>0\<close>] obtain d2 where
   1.737 -          d2: "gauge d2" "\<forall>p. p tagged_partial_division_of (cbox a b) \<and> d2 fine p \<longrightarrow>
   1.738 -            (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2" .
   1.739 -         obtain p where
   1.740 -          p: "p tagged_division_of (cbox a b)" "d1 fine p" "d2 fine p"
   1.741 -          by (rule fine_division_exists [OF gauge_inter [OF d1(1) d2(1)], of a b])
   1.742 -            (auto simp add: fine_inter)
   1.743 -        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> \<bar>sf - si\<bar> < e / 2 \<longrightarrow>
   1.744 -          \<bar>sf' - di\<bar> < e / 2 \<longrightarrow> di < ?S + e"
   1.745 -          by arith
   1.746 -        show "integral (cbox a b) (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
   1.747 -          apply (subst if_P)
   1.748 -          apply rule
   1.749 -        proof (rule *[rule_format])
   1.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"
   1.751 -            unfolding split_def
   1.752 -            apply (rule helplemma)
   1.753 -            using d2(2)[rule_format,of p]
   1.754 -            using p(1,3)
   1.755 -            unfolding tagged_division_of_def split_def
   1.756 -            apply auto
   1.757 -            done
   1.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"
   1.759 -            using d1(2)[rule_format,OF conjI[OF p(1,2)]]
   1.760 -            by (simp only: real_norm_def)
   1.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))"
   1.762 -            apply (rule setsum.cong)
   1.763 -            apply (rule refl)
   1.764 -            unfolding split_paired_all split_conv
   1.765 -            apply (drule tagged_division_ofD(4)[OF p(1)])
   1.766 -            unfolding norm_scaleR
   1.767 -            apply (subst abs_of_nonneg)
   1.768 -            apply auto
   1.769 -            done
   1.770 -          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
   1.771 -            using partial_division_of_tagged_division[of p "cbox a b"] p(1)
   1.772 -            apply (subst setsum.over_tagged_division_lemma[OF p(1)])
   1.773 -            apply (simp add: integral_null)
   1.774 -            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
   1.775 -            apply (auto simp: tagged_partial_division_of_def)
   1.776 -            done
   1.777 -        qed
   1.778 -      qed
   1.779 -    qed (insert K, auto)
   1.780 -  qed
   1.781 -qed
   1.782 -
   1.783 -lemma absolutely_integrable_restrict_univ:
   1.784 -  "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow>
   1.785 -    f absolutely_integrable_on s"
   1.786 -  unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
   1.787 -
   1.788 -lemma absolutely_integrable_add[intro]:
   1.789 -  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.790 -  assumes "f absolutely_integrable_on s"
   1.791 -    and "g absolutely_integrable_on s"
   1.792 -  shows "(\<lambda>x. f x + g x) absolutely_integrable_on s"
   1.793 -proof -
   1.794 -  let ?P = "\<And>f g::'n \<Rightarrow> 'm. f absolutely_integrable_on UNIV \<Longrightarrow>
   1.795 -    g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
   1.796 -  {
   1.797 -    presume as: "PROP ?P"
   1.798 -    note a = absolutely_integrable_restrict_univ[symmetric]
   1.799 -    have *: "\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0) =
   1.800 -      (if x \<in> s then f x + g x else 0)" by auto
   1.801 -    show ?thesis
   1.802 -      apply (subst a)
   1.803 -      using as[OF assms[unfolded a[of f] a[of g]]]
   1.804 -      apply (simp only: *)
   1.805 -      done
   1.806 -  }
   1.807 -  fix f g :: "'n \<Rightarrow> 'm"
   1.808 -  assume assms: "f absolutely_integrable_on UNIV" "g absolutely_integrable_on UNIV"
   1.809 -  note absolutely_integrable_bounded_variation
   1.810 -  from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
   1.811 -  show "(\<lambda>x. f x + g x) absolutely_integrable_on UNIV"
   1.812 -    apply (rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
   1.813 -    apply (rule integrable_add)
   1.814 -    prefer 3
   1.815 -    apply safe
   1.816 -  proof goal_cases
   1.817 -    case prems: (1 d)
   1.818 -    have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
   1.819 -      apply (drule division_ofD(4)[OF prems])
   1.820 -      apply safe
   1.821 -      apply (rule_tac[!] integrable_on_subcbox[of _ UNIV])
   1.822 -      using assms
   1.823 -      apply auto
   1.824 -      done
   1.825 -    then have "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
   1.826 -      (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))"
   1.827 -      apply -
   1.828 -      unfolding setsum.distrib [symmetric]
   1.829 -      apply (rule setsum_mono)
   1.830 -      apply (subst integral_add)
   1.831 -      prefer 3
   1.832 -      apply (rule norm_triangle_ineq)
   1.833 -      apply auto
   1.834 -      done
   1.835 -    also have "\<dots> \<le> B1 + B2"
   1.836 -      using B(1)[OF prems] B(2)[OF prems] by auto
   1.837 -    finally show ?case .
   1.838 -  qed (insert assms, auto)
   1.839 -qed
   1.840 -
   1.841 -lemma absolutely_integrable_sub[intro]:
   1.842 -  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.843 -  assumes "f absolutely_integrable_on s"
   1.844 -    and "g absolutely_integrable_on s"
   1.845 -  shows "(\<lambda>x. f x - g x) absolutely_integrable_on s"
   1.846 -  using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
   1.847 -  by (simp add: algebra_simps)
   1.848 -
   1.849 -lemma absolutely_integrable_linear:
   1.850 -  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   1.851 -    and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
   1.852 -  assumes "f absolutely_integrable_on s"
   1.853 -    and "bounded_linear h"
   1.854 -  shows "(h \<circ> f) absolutely_integrable_on s"
   1.855 -proof -
   1.856 -  {
   1.857 -    presume as: "\<And>f::'m \<Rightarrow> 'n. \<And>h::'n \<Rightarrow> 'p. f absolutely_integrable_on UNIV \<Longrightarrow>
   1.858 -      bounded_linear h \<Longrightarrow> (h \<circ> f) absolutely_integrable_on UNIV"
   1.859 -    note a = absolutely_integrable_restrict_univ[symmetric]
   1.860 -    show ?thesis
   1.861 -      apply (subst a)
   1.862 -      using as[OF assms[unfolded a[of f] a[of g]]]
   1.863 -      apply (simp only: o_def if_distrib linear_simps[OF assms(2)])
   1.864 -      done
   1.865 -  }
   1.866 -  fix f :: "'m \<Rightarrow> 'n"
   1.867 -  fix h :: "'n \<Rightarrow> 'p"
   1.868 -  assume assms: "f absolutely_integrable_on UNIV" "bounded_linear h"
   1.869 -  from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
   1.870 -  from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
   1.871 -  show "(h \<circ> f) absolutely_integrable_on UNIV"
   1.872 -    apply (rule bounded_variation_absolutely_integrable[of _ "B * b"])
   1.873 -    apply (rule integrable_linear[OF _ assms(2)])
   1.874 -    apply safe
   1.875 -  proof goal_cases
   1.876 -    case prems: (2 d)
   1.877 -    have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
   1.878 -      unfolding setsum_distrib_right
   1.879 -      apply (rule setsum_mono)
   1.880 -    proof goal_cases
   1.881 -      case (1 k)
   1.882 -      from division_ofD(4)[OF prems this]
   1.883 -      guess u v by (elim exE) note uv=this
   1.884 -      have *: "f integrable_on k"
   1.885 -        unfolding uv
   1.886 -        apply (rule integrable_on_subcbox[of _ UNIV])
   1.887 -        using assms
   1.888 -        apply auto
   1.889 -        done
   1.890 -      note this[unfolded has_integral_integral]
   1.891 -      note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
   1.892 -      note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
   1.893 -      show ?case
   1.894 -        unfolding * using b by auto
   1.895 -    qed
   1.896 -    also have "\<dots> \<le> B * b"
   1.897 -      apply (rule mult_right_mono)
   1.898 -      using B prems b
   1.899 -      apply auto
   1.900 -      done
   1.901 -    finally show ?case .
   1.902 -  qed (insert assms, auto)
   1.903 -qed
   1.904 -
   1.905 -lemma absolutely_integrable_setsum:
   1.906 -  fixes f :: "'a \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.907 -  assumes "finite t"
   1.908 -    and "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
   1.909 -  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
   1.910 -  using assms(1,2)
   1.911 -  by induct auto
   1.912 -
   1.913 -lemma absolutely_integrable_vector_abs:
   1.914 -  fixes f :: "'a::euclidean_space => 'b::euclidean_space"
   1.915 -    and T :: "'c::euclidean_space \<Rightarrow> 'b"
   1.916 -  assumes f: "f absolutely_integrable_on s"
   1.917 -  shows "(\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>T i\<bar> *\<^sub>R i)) absolutely_integrable_on s"
   1.918 -  (is "?Tf absolutely_integrable_on s")
   1.919 -proof -
   1.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)"
   1.921 -    by simp
   1.922 -  have *: "\<And>x. ?Tf x = (\<Sum>i\<in>Basis.
   1.923 -    ((\<lambda>y. (\<Sum>j\<in>Basis. (if j = i then y else 0) *\<^sub>R j)) o
   1.924 -     (\<lambda>x. (norm (\<Sum>j\<in>Basis. (if j = i then f x\<bullet>T i else 0) *\<^sub>R j)))) x)"
   1.925 -    by (simp add: comp_def if_distrib setsum.If_cases)
   1.926 -  show ?thesis
   1.927 -    unfolding *
   1.928 -    apply (rule absolutely_integrable_setsum[OF finite_Basis])
   1.929 -    apply (rule absolutely_integrable_linear)
   1.930 -    apply (rule absolutely_integrable_norm)
   1.931 -    apply (rule absolutely_integrable_linear[OF f, unfolded o_def])
   1.932 -    apply (auto simp: linear_linear euclidean_eq_iff[where 'a='c] inner_simps intro!: linearI)
   1.933 -    done
   1.934 -qed
   1.935 -
   1.936 -lemma absolutely_integrable_max:
   1.937 -  fixes f g :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   1.938 -  assumes "f absolutely_integrable_on s"
   1.939 -    and "g absolutely_integrable_on s"
   1.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"
   1.941 -proof -
   1.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)) =
   1.943 -      (\<Sum>i\<in>Basis. max (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
   1.944 -    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
   1.945 -  note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
   1.946 -  note absolutely_integrable_vector_abs[OF this(1), where T="\<lambda>x. x"] this(2)
   1.947 -  note absolutely_integrable_add[OF this]
   1.948 -  note absolutely_integrable_cmul[OF this, of "1/2"]
   1.949 -  then show ?thesis unfolding * .
   1.950 -qed
   1.951 -
   1.952 -lemma absolutely_integrable_min:
   1.953 -  fixes f g::"'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
   1.954 -  assumes "f absolutely_integrable_on s"
   1.955 -    and "g absolutely_integrable_on s"
   1.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"
   1.957 -proof -
   1.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)) =
   1.959 -      (\<Sum>i\<in>Basis. min (f(x)\<bullet>i) (g(x)\<bullet>i) *\<^sub>R i)"
   1.960 -    unfolding euclidean_eq_iff[where 'a='n] by (auto simp: inner_simps)
   1.961 -
   1.962 -  note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
   1.963 -  note this(1) absolutely_integrable_vector_abs[OF this(2), where T="\<lambda>x. x"]
   1.964 -  note absolutely_integrable_sub[OF this]
   1.965 -  note absolutely_integrable_cmul[OF this,of "1/2"]
   1.966 -  then show ?thesis unfolding * .
   1.967 -qed
   1.968 -
   1.969 -lemma absolutely_integrable_abs_eq:
   1.970 -  fixes f::"'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
   1.971 -  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
   1.972 -    (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on s"
   1.973 -  (is "?l = ?r")
   1.974 -proof
   1.975 -  assume ?l
   1.976 -  then show ?r
   1.977 -    apply -
   1.978 -    apply rule
   1.979 -    defer
   1.980 -    apply (drule absolutely_integrable_vector_abs)
   1.981 -    apply auto
   1.982 -    done
   1.983 -next
   1.984 -  assume ?r
   1.985 -  {
   1.986 -    presume lem: "\<And>f::'n \<Rightarrow> 'm. f integrable_on UNIV \<Longrightarrow>
   1.987 -      (\<lambda>x. (\<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i)::'m) integrable_on UNIV \<Longrightarrow>
   1.988 -        f absolutely_integrable_on UNIV"
   1.989 -    have *: "\<And>x. (\<Sum>i\<in>Basis. \<bar>(if x \<in> s then f x else 0) \<bullet> i\<bar> *\<^sub>R i) =
   1.990 -      (if x \<in> s then (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) else (0::'m))"
   1.991 -      unfolding euclidean_eq_iff[where 'a='m]
   1.992 -      by auto
   1.993 -    show ?l
   1.994 -      apply (subst absolutely_integrable_restrict_univ[symmetric])
   1.995 -      apply (rule lem)
   1.996 -      unfolding integrable_restrict_univ *
   1.997 -      using \<open>?r\<close>
   1.998 -      apply auto
   1.999 -      done
  1.1000 -  }
  1.1001 -  fix f :: "'n \<Rightarrow> 'm"
  1.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"
  1.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"
  1.1004 -  show "f absolutely_integrable_on UNIV"
  1.1005 -    apply (rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"])
  1.1006 -    apply safe
  1.1007 -  proof goal_cases
  1.1008 -    case d: (1 d)
  1.1009 -    note d'=division_ofD[OF d]
  1.1010 -    have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
  1.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)"
  1.1012 -      apply (rule setsum_mono)
  1.1013 -      apply (rule order_trans[OF norm_le_l1])
  1.1014 -      apply (rule setsum_mono)
  1.1015 -      unfolding lessThan_iff
  1.1016 -    proof -
  1.1017 -      fix k
  1.1018 -      fix i :: 'm
  1.1019 -      assume "k \<in> d" and i: "i \<in> Basis"
  1.1020 -      from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this
  1.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"
  1.1022 -        apply (rule abs_leI)
  1.1023 -        unfolding inner_minus_left[symmetric]
  1.1024 -        defer
  1.1025 -        apply (subst integral_neg[symmetric])
  1.1026 -        apply (rule_tac[1-2] integral_component_le[OF i])
  1.1027 -        using integrable_on_subcbox[OF assms(1),of a b]
  1.1028 -          integrable_on_subcbox[OF assms(2),of a b] i  integrable_neg
  1.1029 -        unfolding ab
  1.1030 -        apply auto
  1.1031 -        done
  1.1032 -    qed
  1.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"
  1.1034 -      apply (subst setsum.commute)
  1.1035 -      apply (rule setsum_mono)
  1.1036 -    proof goal_cases
  1.1037 -      case (1 j)
  1.1038 -      have *: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) integrable_on \<Union>d"
  1.1039 -        using integrable_on_subdivision[OF d assms(2)] by auto
  1.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) =
  1.1041 -        integral (\<Union>d) (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x\<bullet>i\<bar> *\<^sub>R i::'m) \<bullet> j"
  1.1042 -        unfolding inner_setsum_left[symmetric] integral_combine_division_topdown[OF * d] ..
  1.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"
  1.1044 -        apply (rule integral_subset_component_le)
  1.1045 -        using assms * \<open>j \<in> Basis\<close>
  1.1046 -        apply auto
  1.1047 -        done
  1.1048 -      finally show ?case .
  1.1049 -    qed
  1.1050 -    finally show ?case .
  1.1051 -  qed
  1.1052 -qed
  1.1053 -
  1.1054 -lemma nonnegative_absolutely_integrable:
  1.1055 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1.1056 -  assumes "\<forall>x\<in>s. \<forall>i\<in>Basis. 0 \<le> f x \<bullet> i"
  1.1057 -    and "f integrable_on s"
  1.1058 -  shows "f absolutely_integrable_on s"
  1.1059 -  unfolding absolutely_integrable_abs_eq
  1.1060 -  apply rule
  1.1061 -  apply (rule assms)thm integrable_eq
  1.1062 -  apply (rule integrable_eq[of _ f])
  1.1063 -  using assms
  1.1064 -  apply (auto simp: euclidean_eq_iff[where 'a='m])
  1.1065 -  done
  1.1066 -
  1.1067 -lemma absolutely_integrable_integrable_bound:
  1.1068 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1.1069 -  assumes "\<forall>x\<in>s. norm (f x) \<le> g x"
  1.1070 -    and "f integrable_on s"
  1.1071 -    and "g integrable_on s"
  1.1072 -  shows "f absolutely_integrable_on s"
  1.1073 -proof -
  1.1074 -  {
  1.1075 -    presume *: "\<And>f::'n \<Rightarrow> 'm. \<And>g. \<forall>x. norm (f x) \<le> g x \<Longrightarrow> f integrable_on UNIV \<Longrightarrow>
  1.1076 -      g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
  1.1077 -    show ?thesis
  1.1078 -      apply (subst absolutely_integrable_restrict_univ[symmetric])
  1.1079 -      apply (rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
  1.1080 -      using assms
  1.1081 -      unfolding integrable_restrict_univ
  1.1082 -      apply auto
  1.1083 -      done
  1.1084 -  }
  1.1085 -  fix g
  1.1086 -  fix f :: "'n \<Rightarrow> 'm"
  1.1087 -  assume assms: "\<forall>x. norm (f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
  1.1088 -  show "f absolutely_integrable_on UNIV"
  1.1089 -    apply (rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
  1.1090 -    apply safe
  1.1091 -  proof goal_cases
  1.1092 -    case d: (1 d)
  1.1093 -    note d'=division_ofD[OF d]
  1.1094 -    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
  1.1095 -      apply (rule setsum_mono)
  1.1096 -      apply (rule integral_norm_bound_integral)
  1.1097 -      apply (drule_tac[!] d'(4))
  1.1098 -      apply safe
  1.1099 -      apply (rule_tac[1-2] integrable_on_subcbox)
  1.1100 -      using assms
  1.1101 -      apply auto
  1.1102 -      done
  1.1103 -    also have "\<dots> = integral (\<Union>d) g"
  1.1104 -      apply (rule integral_combine_division_bottomup[symmetric])
  1.1105 -      apply (rule d)
  1.1106 -      apply safe
  1.1107 -      apply (drule d'(4))
  1.1108 -      apply safe
  1.1109 -      apply (rule integrable_on_subcbox[OF assms(3)])
  1.1110 -      apply auto
  1.1111 -      done
  1.1112 -    also have "\<dots> \<le> integral UNIV g"
  1.1113 -      apply (rule integral_subset_le)
  1.1114 -      defer
  1.1115 -      apply (rule integrable_on_subdivision[OF d,of _ UNIV])
  1.1116 -      prefer 4
  1.1117 -      apply rule
  1.1118 -      apply (rule_tac y="norm (f x)" in order_trans)
  1.1119 -      using assms
  1.1120 -      apply auto
  1.1121 -      done
  1.1122 -    finally show ?case .
  1.1123 -  qed
  1.1124 -qed
  1.1125 -
  1.1126 -lemma absolutely_integrable_absolutely_integrable_bound:
  1.1127 -  fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1.1128 -    and g :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
  1.1129 -  assumes "\<forall>x\<in>s. norm (f x) \<le> norm (g x)"
  1.1130 -    and "f integrable_on s"
  1.1131 -    and "g absolutely_integrable_on s"
  1.1132 -  shows "f absolutely_integrable_on s"
  1.1133 -  apply (rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
  1.1134 -  using assms
  1.1135 -  apply auto
  1.1136 -  done
  1.1137 -
  1.1138 -lemma absolutely_integrable_inf_real:
  1.1139 -  assumes "finite k"
  1.1140 -    and "k \<noteq> {}"
  1.1141 -    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  1.1142 -  shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s"
  1.1143 -  using assms
  1.1144 -proof induct
  1.1145 -  case (insert a k)
  1.1146 -  let ?P = "(\<lambda>x.
  1.1147 -    if fs x ` k = {} then fs x a
  1.1148 -    else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
  1.1149 -  show ?case
  1.1150 -    unfolding image_insert
  1.1151 -    apply (subst Inf_insert_finite)
  1.1152 -    apply (rule finite_imageI[OF insert(1)])
  1.1153 -  proof (cases "k = {}")
  1.1154 -    case True
  1.1155 -    then show ?P
  1.1156 -      apply (subst if_P)
  1.1157 -      defer
  1.1158 -      apply (rule insert(5)[rule_format])
  1.1159 -      apply auto
  1.1160 -      done
  1.1161 -  next
  1.1162 -    case False
  1.1163 -    then show ?P
  1.1164 -      apply (subst if_not_P)
  1.1165 -      defer
  1.1166 -      apply (rule absolutely_integrable_min[where 'n=real, unfolded Basis_real_def, simplified])
  1.1167 -      defer
  1.1168 -      apply(rule insert(3)[OF False])
  1.1169 -      using insert(5)
  1.1170 -      apply auto
  1.1171 -      done
  1.1172 -  qed
  1.1173 -next
  1.1174 -  case empty
  1.1175 -  then show ?case by auto
  1.1176 -qed
  1.1177 -
  1.1178 -lemma absolutely_integrable_sup_real:
  1.1179 -  assumes "finite k"
  1.1180 -    and "k \<noteq> {}"
  1.1181 -    and "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  1.1182 -  shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s"
  1.1183 -  using assms
  1.1184 -proof induct
  1.1185 -  case (insert a k)
  1.1186 -  let ?P = "(\<lambda>x.
  1.1187 -    if fs x ` k = {} then fs x a
  1.1188 -    else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
  1.1189 -  show ?case
  1.1190 -    unfolding image_insert
  1.1191 -    apply (subst Sup_insert_finite)
  1.1192 -    apply (rule finite_imageI[OF insert(1)])
  1.1193 -  proof (cases "k = {}")
  1.1194 -    case True
  1.1195 -    then show ?P
  1.1196 -      apply (subst if_P)
  1.1197 -      defer
  1.1198 -      apply (rule insert(5)[rule_format])
  1.1199 -      apply auto
  1.1200 -      done
  1.1201 -  next
  1.1202 -    case False
  1.1203 -    then show ?P
  1.1204 -      apply (subst if_not_P)
  1.1205 -      defer
  1.1206 -      apply (rule absolutely_integrable_max[where 'n=real, unfolded Basis_real_def, simplified])
  1.1207 -      defer
  1.1208 -      apply (rule insert(3)[OF False])
  1.1209 -      using insert(5)
  1.1210 -      apply auto
  1.1211 -      done
  1.1212 -  qed
  1.1213 -qed auto
  1.1214 -
  1.1215 -
  1.1216  subsection \<open>differentiation under the integral sign\<close>
  1.1217  
  1.1218  lemma tube_lemma:
  1.1219 @@ -11296,8 +10103,7 @@
  1.1220            by (simp add: integral_diff dist_norm)
  1.1221          also have "\<dots> \<le> integral (cbox a b) (\<lambda>x. (e' / content (cbox a b)))"
  1.1222            using elim
  1.1223 -          by (intro integral_norm_bound_integral)
  1.1224 -            (auto intro!: integrable_diff absolutely_integrable_onI)
  1.1225 +          by (intro integral_norm_bound_integral) (auto intro!: integrable_diff)
  1.1226          also have "\<dots> < e"
  1.1227            using \<open>0 < e\<close>
  1.1228            by (simp add: e'_def)
  1.1229 @@ -11309,358 +10115,6 @@
  1.1230  qed
  1.1231  
  1.1232  
  1.1233 -subsection \<open>Dominated convergence\<close>
  1.1234 -
  1.1235 -context
  1.1236 -begin
  1.1237 -
  1.1238 -private lemma dominated_convergence_real:
  1.1239 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> real"
  1.1240 -  assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
  1.1241 -    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  1.1242 -    and "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
  1.1243 -  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  1.1244 -proof
  1.1245 -  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
  1.1246 -  proof (safe intro!: bdd_belowI)
  1.1247 -    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
  1.1248 -      using assms(3)[rule_format, of x n] by simp
  1.1249 -  qed
  1.1250 -  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
  1.1251 -  proof (safe intro!: bdd_aboveI)
  1.1252 -    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
  1.1253 -      using assms(3)[rule_format, of x n] by simp
  1.1254 -  qed
  1.1255 -
  1.1256 -  have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
  1.1257 -    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
  1.1258 -    integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
  1.1259 -  proof (rule monotone_convergence_decreasing, safe)
  1.1260 -    fix m :: nat
  1.1261 -    show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
  1.1262 -      unfolding bounded_iff
  1.1263 -      apply (rule_tac x="integral s h" in exI)
  1.1264 -    proof safe
  1.1265 -      fix k :: nat
  1.1266 -      show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  1.1267 -        apply (rule integral_norm_bound_integral)
  1.1268 -        unfolding Setcompr_eq_image
  1.1269 -        apply (rule absolutely_integrable_onD)
  1.1270 -        apply (rule absolutely_integrable_inf_real)
  1.1271 -        prefer 5
  1.1272 -        unfolding real_norm_def
  1.1273 -        apply rule
  1.1274 -        apply (rule cInf_abs_ge)
  1.1275 -        prefer 5
  1.1276 -        apply rule
  1.1277 -        apply (rule_tac g = h in absolutely_integrable_integrable_bound)
  1.1278 -        using assms
  1.1279 -        unfolding real_norm_def
  1.1280 -        apply auto
  1.1281 -        done
  1.1282 -    qed
  1.1283 -    fix k :: nat
  1.1284 -    show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  1.1285 -      unfolding Setcompr_eq_image
  1.1286 -      apply (rule absolutely_integrable_onD)
  1.1287 -      apply (rule absolutely_integrable_inf_real)
  1.1288 -      prefer 3
  1.1289 -      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
  1.1290 -      apply auto
  1.1291 -      done
  1.1292 -    fix x
  1.1293 -    assume x: "x \<in> s"
  1.1294 -    show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
  1.1295 -      by (rule cInf_superset_mono) auto
  1.1296 -    let ?S = "{f j x| j. m \<le> j}"
  1.1297 -    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Inf ?S) sequentially"
  1.1298 -    proof (rule LIMSEQ_I, goal_cases)
  1.1299 -      case r: (1 r)
  1.1300 -
  1.1301 -      have "\<exists>y\<in>?S. y < Inf ?S + r"
  1.1302 -        by (subst cInf_less_iff[symmetric]) (auto simp: \<open>x\<in>s\<close> r)
  1.1303 -      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
  1.1304 -        by blast
  1.1305 -
  1.1306 -      show ?case
  1.1307 -        apply (rule_tac x=N in exI)
  1.1308 -        apply safe
  1.1309 -      proof goal_cases
  1.1310 -        case prems: (1 n)
  1.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"
  1.1312 -          by arith
  1.1313 -        show ?case
  1.1314 -          unfolding real_norm_def
  1.1315 -            apply (rule *[rule_format, OF N(1)])
  1.1316 -            apply (rule cInf_superset_mono, auto simp: \<open>x\<in>s\<close>) []
  1.1317 -            apply (rule cInf_lower)
  1.1318 -            using N prems
  1.1319 -            apply auto []
  1.1320 -            apply simp
  1.1321 -            done
  1.1322 -      qed
  1.1323 -    qed
  1.1324 -  qed
  1.1325 -  note dec1 = conjunctD2[OF this]
  1.1326 -
  1.1327 -  have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
  1.1328 -    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<longlongrightarrow>
  1.1329 -    integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
  1.1330 -  proof (rule monotone_convergence_increasing,safe)
  1.1331 -    fix m :: nat
  1.1332 -    show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
  1.1333 -      unfolding bounded_iff
  1.1334 -      apply (rule_tac x="integral s h" in exI)
  1.1335 -    proof safe
  1.1336 -      fix k :: nat
  1.1337 -      show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  1.1338 -        apply (rule integral_norm_bound_integral) unfolding Setcompr_eq_image
  1.1339 -        apply (rule absolutely_integrable_onD)
  1.1340 -        apply(rule absolutely_integrable_sup_real)
  1.1341 -        prefer 5 unfolding real_norm_def
  1.1342 -        apply rule
  1.1343 -        apply (rule cSup_abs_le)
  1.1344 -        using assms
  1.1345 -        apply (force simp add: )
  1.1346 -        prefer 4
  1.1347 -        apply rule
  1.1348 -        apply (rule_tac g=h in absolutely_integrable_integrable_bound)
  1.1349 -        using assms
  1.1350 -        unfolding real_norm_def
  1.1351 -        apply auto
  1.1352 -        done
  1.1353 -    qed
  1.1354 -    fix k :: nat
  1.1355 -    show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  1.1356 -      unfolding Setcompr_eq_image
  1.1357 -      apply (rule absolutely_integrable_onD)
  1.1358 -      apply (rule absolutely_integrable_sup_real)
  1.1359 -      prefer 3
  1.1360 -      using absolutely_integrable_integrable_bound[OF assms(3,1,2)]
  1.1361 -      apply auto
  1.1362 -      done
  1.1363 -    fix x
  1.1364 -    assume x: "x\<in>s"
  1.1365 -    show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
  1.1366 -      by (rule cSup_subset_mono) auto
  1.1367 -    let ?S = "{f j x| j. m \<le> j}"
  1.1368 -    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) \<longlongrightarrow> Sup ?S) sequentially"
  1.1369 -    proof (rule LIMSEQ_I, goal_cases)
  1.1370 -      case r: (1 r)
  1.1371 -      have "\<exists>y\<in>?S. Sup ?S - r < y"
  1.1372 -        by (subst less_cSup_iff[symmetric]) (auto simp: r \<open>x\<in>s\<close>)
  1.1373 -      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
  1.1374 -        by blast
  1.1375 -
  1.1376 -      show ?case
  1.1377 -        apply (rule_tac x=N in exI)
  1.1378 -        apply safe
  1.1379 -      proof goal_cases
  1.1380 -        case prems: (1 n)
  1.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"
  1.1382 -          by arith
  1.1383 -        show ?case
  1.1384 -          apply simp
  1.1385 -          apply (rule *[rule_format, OF N(1)])
  1.1386 -          apply (rule cSup_subset_mono, auto simp: \<open>x\<in>s\<close>) []
  1.1387 -          apply (subst cSup_upper)
  1.1388 -          using N prems
  1.1389 -          apply auto
  1.1390 -          done
  1.1391 -      qed
  1.1392 -    qed
  1.1393 -  qed
  1.1394 -  note inc1 = conjunctD2[OF this]
  1.1395 -
  1.1396 -  have "g integrable_on s \<and>
  1.1397 -    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
  1.1398 -    apply (rule monotone_convergence_increasing,safe)
  1.1399 -    apply fact
  1.1400 -  proof -
  1.1401 -    show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
  1.1402 -      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  1.1403 -    proof safe
  1.1404 -      fix k :: nat
  1.1405 -      show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
  1.1406 -        apply (rule integral_norm_bound_integral)
  1.1407 -        apply fact+
  1.1408 -        unfolding real_norm_def
  1.1409 -        apply rule
  1.1410 -        apply (rule cInf_abs_ge)
  1.1411 -        using assms(3)
  1.1412 -        apply auto
  1.1413 -        done
  1.1414 -    qed
  1.1415 -    fix k :: nat and x
  1.1416 -    assume x: "x \<in> s"
  1.1417 -
  1.1418 -    have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  1.1419 -    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
  1.1420 -      by (intro cInf_superset_mono) (auto simp: \<open>x\<in>s\<close>)
  1.1421 -
  1.1422 -    show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) \<longlonglongrightarrow> g x"
  1.1423 -    proof (rule LIMSEQ_I, goal_cases)
  1.1424 -      case r: (1 r)
  1.1425 -      then have "0<r/2"
  1.1426 -        by auto
  1.1427 -      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N = this
  1.1428 -      show ?case
  1.1429 -        apply (rule_tac x=N in exI)
  1.1430 -        apply safe
  1.1431 -        unfolding real_norm_def
  1.1432 -        apply (rule le_less_trans[of _ "r/2"])
  1.1433 -        apply (rule cInf_asclose)
  1.1434 -        apply safe
  1.1435 -        defer
  1.1436 -        apply (rule less_imp_le)
  1.1437 -        using N r
  1.1438 -        apply auto
  1.1439 -        done
  1.1440 -    qed
  1.1441 -  qed
  1.1442 -  note inc2 = conjunctD2[OF this]
  1.1443 -
  1.1444 -  have "g integrable_on s \<and>
  1.1445 -    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<longlongrightarrow> integral s g) sequentially"
  1.1446 -    apply (rule monotone_convergence_decreasing,safe)
  1.1447 -    apply fact
  1.1448 -  proof -
  1.1449 -    show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
  1.1450 -      unfolding bounded_iff
  1.1451 -      apply (rule_tac x="integral s h" in exI)
  1.1452 -    proof safe
  1.1453 -      fix k :: nat
  1.1454 -      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
  1.1455 -        apply (rule integral_norm_bound_integral)
  1.1456 -        apply fact+
  1.1457 -        unfolding real_norm_def
  1.1458 -        apply rule
  1.1459 -        apply (rule cSup_abs_le)
  1.1460 -        using assms(3)
  1.1461 -        apply auto
  1.1462 -        done
  1.1463 -    qed
  1.1464 -    fix k :: nat
  1.1465 -    fix x
  1.1466 -    assume x: "x \<in> s"
  1.1467 -
  1.1468 -    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
  1.1469 -      by (rule cSup_subset_mono) (auto simp: \<open>x\<in>s\<close>)
  1.1470 -    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) \<longlongrightarrow> g x) sequentially"
  1.1471 -    proof (rule LIMSEQ_I, goal_cases)
  1.1472 -      case r: (1 r)
  1.1473 -      then have "0<r/2"
  1.1474 -        by auto
  1.1475 -      from assms(4)[THEN bspec, THEN LIMSEQ_D, OF x this] guess N .. note N=this
  1.1476 -      show ?case
  1.1477 -        apply (rule_tac x=N in exI,safe)
  1.1478 -        unfolding real_norm_def
  1.1479 -        apply (rule le_less_trans[of _ "r/2"])
  1.1480 -        apply (rule cSup_asclose)
  1.1481 -        apply safe
  1.1482 -        defer
  1.1483 -        apply (rule less_imp_le)
  1.1484 -        using N r
  1.1485 -        apply auto
  1.1486 -        done
  1.1487 -    qed
  1.1488 -  qed
  1.1489 -  note dec2 = conjunctD2[OF this]
  1.1490 -
  1.1491 -  show "g integrable_on s" by fact
  1.1492 -  show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  1.1493 -  proof (rule LIMSEQ_I, goal_cases)
  1.1494 -    case r: (1 r)
  1.1495 -    from LIMSEQ_D [OF inc2(2) r] guess N1 .. note N1=this[unfolded real_norm_def]
  1.1496 -    from LIMSEQ_D [OF dec2(2) r] guess N2 .. note N2=this[unfolded real_norm_def]
  1.1497 -    show ?case
  1.1498 -    proof (rule_tac x="N1+N2" in exI, safe)
  1.1499 -      fix n
  1.1500 -      assume n: "n \<ge> N1 + N2"
  1.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"
  1.1502 -        by arith
  1.1503 -      show "norm (integral s (f n) - integral s g) < r"
  1.1504 -        unfolding real_norm_def
  1.1505 -      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
  1.1506 -        show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
  1.1507 -          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
  1.1508 -        show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
  1.1509 -          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
  1.1510 -      qed (insert n, auto)
  1.1511 -    qed
  1.1512 -  qed
  1.1513 -qed
  1.1514 -
  1.1515 -lemma dominated_convergence:
  1.1516 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1.1517 -  assumes f: "\<And>k. (f k) integrable_on s" and h: "h integrable_on s"
  1.1518 -    and le: "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  1.1519 -    and conv: "\<forall>x \<in> s. ((\<lambda>k. f k x) \<longlongrightarrow> g x) sequentially"
  1.1520 -  shows "g integrable_on s"
  1.1521 -    and "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  1.1522 -proof -
  1.1523 -  {
  1.1524 -    fix b :: 'm assume b: "b \<in> Basis"
  1.1525 -    have A: "(\<lambda>x. g x \<bullet> b) integrable_on s \<and>
  1.1526 -               (\<lambda>k. integral s (\<lambda>x. f k x \<bullet> b)) \<longlonglongrightarrow> integral s (\<lambda>x. g x \<bullet> b)"
  1.1527 -    proof (rule dominated_convergence_real)
  1.1528 -      fix k :: nat
  1.1529 -      from f show "(\<lambda>x. f k x \<bullet> b) integrable_on s" by (rule integrable_component)
  1.1530 -    next
  1.1531 -      from h show "h integrable_on s" .
  1.1532 -    next
  1.1533 -      fix k :: nat
  1.1534 -      show "\<forall>x\<in>s. norm (f k x \<bullet> b) \<le> h x"
  1.1535 -      proof
  1.1536 -        fix x assume x: "x \<in> s"
  1.1537 -        have "norm (f k x \<bullet> b) \<le> norm (f k x)" by (simp add: Basis_le_norm b)
  1.1538 -        also have "\<dots> \<le> h x" using le[of k] x by simp
  1.1539 -        finally show "norm (f k x \<bullet> b) \<le> h x" .
  1.1540 -      qed
  1.1541 -    next
  1.1542 -      from conv show "\<forall>x\<in>s. (\<lambda>k. f k x \<bullet> b) \<longlonglongrightarrow> g x \<bullet> b"
  1.1543 -        by (auto intro!: tendsto_inner)
  1.1544 -    qed
  1.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"
  1.1546 -      for k by (rule integral_linear)
  1.1547 -               (simp_all add: f integrable_component bounded_linear_scaleR_left)
  1.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"
  1.1549 -      using A by (intro integral_linear)
  1.1550 -                 (simp_all add: integrable_component bounded_linear_scaleR_left)
  1.1551 -    note A B C
  1.1552 -  } note A = this
  1.1553 -
  1.1554 -  show "g integrable_on s" by (rule integrable_componentwise) (insert A, blast)
  1.1555 -  with A f show "((\<lambda>k. integral s (f k)) \<longlongrightarrow> integral s g) sequentially"
  1.1556 -    by (subst (1 2) integral_componentwise)
  1.1557 -       (auto intro!: tendsto_setsum tendsto_scaleR simp: o_def)
  1.1558 -qed
  1.1559 -
  1.1560 -lemma has_integral_dominated_convergence:
  1.1561 -  fixes f :: "nat \<Rightarrow> 'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
  1.1562 -  assumes "\<And>k. (f k has_integral y k) s" "h integrable_on s"
  1.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"
  1.1564 -    and x: "y \<longlonglongrightarrow> x"
  1.1565 -  shows "(g has_integral x) s"
  1.1566 -proof -
  1.1567 -  have int_f: "\<And>k. (f k) integrable_on s"
  1.1568 -    using assms by (auto simp: integrable_on_def)
  1.1569 -  have "(g has_integral (integral s g)) s"
  1.1570 -    by (intro integrable_integral dominated_convergence[OF int_f assms(2)]) fact+
  1.1571 -  moreover have "integral s g = x"
  1.1572 -  proof (rule LIMSEQ_unique)
  1.1573 -    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> x"
  1.1574 -      using integral_unique[OF assms(1)] x by simp
  1.1575 -    show "(\<lambda>i. integral s (f i)) \<longlonglongrightarrow> integral s g"
  1.1576 -      by (intro dominated_convergence[OF int_f assms(2)]) fact+
  1.1577 -  qed
  1.1578 -  ultimately show ?thesis
  1.1579 -    by simp
  1.1580 -qed
  1.1581 -
  1.1582 -end
  1.1583 -
  1.1584 -
  1.1585  subsection \<open>Integration by parts\<close>
  1.1586  
  1.1587  lemma integration_by_parts_interior_strong: