author paulson Mon Aug 28 22:32:22 2017 +0100 (2017-08-28) changeset 66540 1f955cdd9e59 parent 66531 d9641709f2df parent 66539 0ad3fc48c9ec child 66541 4d9c4cb9e9a5 child 66552 507a42c0a0ff
merged
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 21:18:47 2017 +0200
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Aug 28 22:32:22 2017 +0100
1.3 @@ -3617,22 +3617,24 @@
1.4        and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> 0 \<le> Im (vector_derivative \<gamma> (at x) * cnj(\<gamma> x - z))"
1.5      shows "0 \<le> Re(winding_number \<gamma> z)"
1.6  proof -
1.7 -  have *: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
1.8 +  have ge0: "0 \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))" if x: "0 < x" "x < 1" for x
1.9      using ge by (simp add: Complex.Im_divide algebra_simps x)
1.10 -  show ?thesis
1.11 -    apply (simp add: Re_winding_number [OF \<gamma>] field_simps)
1.12 +  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
1.13 +            (cbox 0 1)"
1.14 +    unfolding box_real
1.15 +    apply (subst has_contour_integral [symmetric])
1.16 +    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
1.17 +  have "0 \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
1.18      apply (rule has_integral_component_nonneg
1.19               [of \<i> "\<lambda>x. if x \<in> {0<..<1}
1.20                           then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else 0", simplified])
1.21 -      prefer 3 apply (force simp: *)
1.22 +      prefer 3 apply (force simp: ge0)
1.24 -    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)"])
1.25 +    apply (rule has_integral_spike_interior [OF hi])
1.26      apply simp
1.27 -    apply (simp only: box_real)
1.28 -    apply (subst has_contour_integral [symmetric])
1.29 -    using \<gamma>
1.30 -    apply (simp add: contour_integrable_inversediff has_contour_integral_integral)
1.31      done
1.32 +  then show ?thesis
1.33 +    by (simp add: Re_winding_number [OF \<gamma>] field_simps)
1.34  qed
1.35
1.36  lemma winding_number_pos_lt_lemma:
1.37 @@ -3641,19 +3643,20 @@
1.38        and ge: "\<And>x. \<lbrakk>0 < x; x < 1\<rbrakk> \<Longrightarrow> e \<le> Im (vector_derivative \<gamma> (at x) / (\<gamma> x - z))"
1.39      shows "0 < Re(winding_number \<gamma> z)"
1.40  proof -
1.41 +  have hi: "((\<lambda>x. 1 / (\<gamma> x - z) * vector_derivative \<gamma> (at x)) has_integral contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))
1.42 +            (cbox 0 1)"
1.43 +    unfolding box_real
1.44 +    apply (subst has_contour_integral [symmetric])
1.45 +    using \<gamma> by (simp add: contour_integrable_inversediff has_contour_integral_integral)
1.46    have "e \<le> Im (contour_integral \<gamma> (\<lambda>w. 1 / (w - z)))"
1.47      apply (rule has_integral_component_le
1.48               [of \<i> "\<lambda>x. \<i>*e" "\<i>*e" "{0..1}"
1.49                      "\<lambda>x. if x \<in> {0<..<1} then 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x) else \<i>*e"
1.50                      "contour_integral \<gamma> (\<lambda>w. 1/(w - z))", simplified])
1.51 -    using e
1.52 -    apply (simp_all add: Basis_complex_def)
1.53 +    using e apply (simp_all add: Basis_complex_def)
1.54      using has_integral_const_real [of _ 0 1] apply force
1.55 -    apply (rule has_integral_spike_interior [of 0 1 _ "\<lambda>x. 1/(\<gamma> x - z) * vector_derivative \<gamma> (at x)", simplified box_real])
1.56 -    apply simp
1.57 -    apply (subst has_contour_integral [symmetric])
1.58 -    using \<gamma>
1.59 -    apply (simp_all add: contour_integrable_inversediff has_contour_integral_integral ge)
1.60 +     apply (rule has_integral_spike_interior [OF hi, simplified box_real])
1.61 +    apply (simp_all add: ge)
1.62      done
1.63    with e show ?thesis
1.64      by (simp add: Re_winding_number [OF \<gamma>] field_simps)
```
```     2.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 21:18:47 2017 +0200
2.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Aug 28 22:32:22 2017 +0100
2.3 @@ -324,7 +324,7 @@
2.4    assumes "(f has_integral k1) i" "(f has_integral k2) i"
2.5    shows "k1 = k2"
2.6  proof (rule ccontr)
2.7 -  let ?e = "norm (k1 - k2) / 2"
2.8 +  let ?e = "norm (k1 - k2)/2"
2.9    let ?F = "(\<lambda>x. if x \<in> i then f x else 0)"
2.10    assume "k1 \<noteq> k2"
2.11    then have e: "?e > 0"
2.12 @@ -334,25 +334,25 @@
2.13    obtain B1 where B1:
2.14        "0 < B1"
2.15        "\<And>a b. ball 0 B1 \<subseteq> cbox a b \<Longrightarrow>
2.16 -        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2) / 2"
2.17 +        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k1) < norm (k1 - k2)/2"
2.18      by (rule has_integral_altD[OF assms(1) nonbox,OF e]) blast
2.19    obtain B2 where B2:
2.20        "0 < B2"
2.21        "\<And>a b. ball 0 B2 \<subseteq> cbox a b \<Longrightarrow>
2.22 -        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2) / 2"
2.23 +        \<exists>z. (?F has_integral z) (cbox a b) \<and> norm (z - k2) < norm (k1 - k2)/2"
2.24      by (rule has_integral_altD[OF assms(2) nonbox,OF e]) blast
2.25    obtain a b :: 'n where ab: "ball 0 B1 \<subseteq> cbox a b" "ball 0 B2 \<subseteq> cbox a b"
2.26      by (metis Un_subset_iff bounded_Un bounded_ball bounded_subset_cbox)
2.27 -  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2) / 2"
2.28 +  obtain w where w: "(?F has_integral w) (cbox a b)" "norm (w - k1) < norm (k1 - k2)/2"
2.29      using B1(2)[OF ab(1)] by blast
2.30 -  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2) / 2"
2.31 +  obtain z where z: "(?F has_integral z) (cbox a b)" "norm (z - k2) < norm (k1 - k2)/2"
2.32      using B2(2)[OF ab(2)] by blast
2.33    have "z = w"
2.34      using has_integral_unique_cbox[OF w(1) z(1)] by auto
2.35    then have "norm (k1 - k2) \<le> norm (z - k2) + norm (w - k1)"
2.36      using norm_triangle_ineq4 [of "k1 - w" "k2 - z"]
2.37      by (auto simp add: norm_minus_commute)
2.38 -  also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
2.39 +  also have "\<dots> < norm (k1 - k2)/2 + norm (k1 - k2)/2"
2.40      by (metis add_strict_mono z(2) w(2))
2.41    finally show False by auto
2.42  qed
2.43 @@ -1290,10 +1290,10 @@
2.44            using mem_interior by metis
2.45          have x: "x\<bullet>k = c"
2.46            using x interior_subset by fastforce
2.47 -        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon> / 2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
2.48 +        have *: "\<And>i. i \<in> Basis \<Longrightarrow> \<bar>(x - (x + (\<epsilon>/2) *\<^sub>R k)) \<bullet> i\<bar> = (if i = k then \<epsilon>/2 else 0)"
2.49            using \<open>0 < \<epsilon>\<close> k by (auto simp: inner_simps inner_not_same_Basis)
2.50 -        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon> / 2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
2.51 -              (\<Sum>i\<in>Basis. (if i = k then \<epsilon> / 2 else 0))"
2.52 +        have "(\<Sum>i\<in>Basis. \<bar>(x - (x + (\<epsilon>/2 ) *\<^sub>R k)) \<bullet> i\<bar>) =
2.53 +              (\<Sum>i\<in>Basis. (if i = k then \<epsilon>/2 else 0))"
2.54            using "*" by (blast intro: sum.cong)
2.55          also have "\<dots> < \<epsilon>"
2.56            by (subst sum.delta) (use \<open>0 < \<epsilon>\<close> in auto)
2.57 @@ -1964,132 +1964,116 @@
2.58        assume c: "c < a \<bullet> k"
2.59        moreover have "x \<in> cbox a b \<Longrightarrow> c \<le> x \<bullet> k" for x
2.60          using k c by (auto simp: cbox_def)
2.61 -      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c) / 2} = {}"
2.62 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (a \<bullet> k - c)/2} = {}"
2.63          using k by (auto simp: cbox_def)
2.64 -      with \<open>0<e\<close> c that[of "(a \<bullet> k - c) / 2"] show ?thesis
2.65 +      with \<open>0<e\<close> c that[of "(a \<bullet> k - c)/2"] show ?thesis
2.66          by auto
2.67      next
2.68        assume c: "b \<bullet> k < c"
2.69        moreover have "x \<in> cbox a b \<Longrightarrow> x \<bullet> k \<le> c" for x
2.70          using k c by (auto simp: cbox_def)
2.71 -      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k) / 2} = {}"
2.72 +      ultimately have "cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> (c - b \<bullet> k)/2} = {}"
2.73          using k by (auto simp: cbox_def)
2.74 -      with \<open>0<e\<close> c that[of "(c - b \<bullet> k) / 2"] show ?thesis
2.75 +      with \<open>0<e\<close> c that[of "(c - b \<bullet> k)/2"] show ?thesis
2.76          by auto
2.77      qed
2.78    qed
2.79  qed
2.80
2.81
2.82 -lemma negligible_standard_hyperplane[intro]:
2.83 +proposition negligible_standard_hyperplane[intro]:
2.84    fixes k :: "'a::euclidean_space"
2.85    assumes k: "k \<in> Basis"
2.86    shows "negligible {x. x\<bullet>k = c}"
2.87    unfolding negligible_def has_integral
2.88 -proof (clarify, goal_cases)
2.89 -  case (1 a b e)
2.90 -  from this and k obtain d where d: "0 < d" "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
2.91 -    by (rule content_doublesplit)
2.92 +proof clarsimp
2.93 +  fix a b and e::real assume "e > 0"
2.94 +  with k obtain d where "0 < d" and d: "content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) < e"
2.95 +    by (metis content_doublesplit)
2.96    let ?i = "indicator {x::'a. x\<bullet>k = c} :: 'a\<Rightarrow>real"
2.97 -  show ?case
2.98 -    apply (rule_tac x="\<lambda>x. ball x d" in exI)
2.99 -    apply rule
2.100 -    apply (rule gauge_ball)
2.101 -    apply (rule d)
2.102 -  proof (rule, rule)
2.103 -    fix p
2.104 -    assume p: "p tagged_division_of (cbox a b) \<and> (\<lambda>x. ball x d) fine p"
2.105 -    have *: "(\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) =
2.106 -      (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
2.107 -      apply (rule sum.cong)
2.108 -      apply (rule refl)
2.109 -      unfolding split_paired_all real_scaleR_def mult_cancel_right split_conv
2.110 -      apply cases
2.111 -      apply (rule disjI1)
2.112 -      apply assumption
2.113 -      apply (rule disjI2)
2.114 +  show "\<exists>\<gamma>. gauge \<gamma> \<and>
2.115 +           (\<forall>\<D>. \<D> tagged_division_of cbox a b \<and> \<gamma> fine \<D> \<longrightarrow>
2.116 +                 \<bar>\<Sum>(x,K) \<in> \<D>. content K * ?i x\<bar> < e)"
2.117 +  proof (intro exI, safe)
2.118 +    show "gauge (\<lambda>x. ball x d)"
2.119 +      using \<open>0 < d\<close> by blast
2.120 +  next
2.121 +    fix \<D>
2.122 +    assume p: "\<D> tagged_division_of (cbox a b)" "(\<lambda>x. ball x d) fine \<D>"
2.123 +    have "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
2.124 +      if "(x, L) \<in> \<D>" "?i x \<noteq> 0" for x L
2.125      proof -
2.126 -      fix x l
2.127 -      assume as: "(x, l) \<in> p" "?i x \<noteq> 0"
2.128 -      then have xk: "x\<bullet>k = c"
2.129 -        unfolding indicator_def
2.130 -        apply -
2.131 -        apply (rule ccontr)
2.132 -        apply auto
2.133 -        done
2.134 -      show "content l = content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
2.135 -        apply (rule arg_cong[where f=content])
2.136 -        apply (rule set_eqI)
2.137 -        apply rule
2.138 -        apply rule
2.139 -        unfolding mem_Collect_eq
2.140 -      proof -
2.141 +      have xk: "x\<bullet>k = c"
2.142 +        using that by (simp add: indicator_def split: if_split_asm)
2.143 +      have "L \<subseteq> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
2.144 +      proof
2.145          fix y
2.146 -        assume y: "y \<in> l"
2.147 -        note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv]
2.148 -        note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y]
2.149 -        note le_less_trans[OF Basis_le_norm[OF k] this]
2.150 -        then show "\<bar>y \<bullet> k - c\<bar> \<le> d"
2.151 +        assume y: "y \<in> L"
2.152 +        have "L \<subseteq> ball x d"
2.153 +          using p(2) that(1) by auto
2.154 +        then have "norm (x - y) < d"
2.155 +          by (simp add: dist_norm subset_iff y)
2.156 +        then have "\<bar>(x - y) \<bullet> k\<bar> < d"
2.157 +          using k norm_bound_Basis_lt by blast
2.158 +        then show "y \<in> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
2.159            unfolding inner_simps xk by auto
2.160 -      qed auto
2.161 +      qed
2.162 +      then show "content L = content (L \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
2.163 +        by (metis inf.orderE)
2.164      qed
2.165 -    note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]]
2.166 -    have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
2.167 +    then have *: "(\<Sum>(x,K)\<in>\<D>. content K * ?i x) = (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x\<bullet>k - c\<bar> \<le> d}) *\<^sub>R ?i x)"
2.168 +      by (force simp add: split_paired_all intro!: sum.cong [OF refl])
2.169 +    note p'= tagged_division_ofD[OF p(1)] and p''=division_of_tagged_division[OF p(1)]
2.170 +    have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * indicator {x. x \<bullet> k = c} x) < e"
2.171      proof -
2.172 -      have "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le>
2.173 -        (\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
2.174 -        apply (rule sum_mono)
2.175 -        unfolding split_paired_all split_conv
2.176 -        apply (rule mult_right_le_one_le)
2.177 -        apply (drule p'(4))
2.178 -        apply (auto simp add:interval_doublesplit[OF k])
2.179 -        done
2.180 +      have "(\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) \<le> (\<Sum>(x,K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}))"
2.181 +        by (force simp add: indicator_def intro!: sum_mono)
2.182        also have "\<dots> < e"
2.183 -      proof (subst sum.over_tagged_division_lemma[OF p[THEN conjunct1]], goal_cases)
2.184 -        case prems: (1 u v)
2.185 +      proof (subst sum.over_tagged_division_lemma[OF p(1)])
2.186 +        fix u v::'a
2.187 +        assume "box u v = {}"
2.188          then have *: "content (cbox u v) = 0"
2.189            unfolding content_eq_0_interior by simp
2.190 -        have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
2.191 -          unfolding interval_doublesplit[OF k]
2.192 -          apply (rule content_subset)
2.193 -          unfolding interval_doublesplit[symmetric,OF k]
2.194 -          apply auto
2.195 -          done
2.196 -        then show ?case
2.197 +        have "cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<subseteq> cbox u v"
2.198 +          by auto
2.199 +        then have "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<le> content (cbox u v)"
2.200 +          unfolding interval_doublesplit[OF k] by (rule content_subset)
2.201 +        then show "content (cbox u v \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
2.202            unfolding * interval_doublesplit[OF k]
2.203            by (blast intro: antisym)
2.204        next
2.205 -        have "(\<Sum>l\<in>snd ` p. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
2.206 -          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
2.207 +        have "(\<Sum>l\<in>snd ` \<D>. content (l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) =
2.208 +          sum content ((\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}})"
2.209          proof (subst (2) sum.reindex_nontrivial)
2.210 -          fix x y assume "x \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
2.211 +          fix x y assume "x \<in> {l \<in> snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}" "y \<in> {l \<in> snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}"
2.212              "x \<noteq> y" and eq: "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} = y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}"
2.213 -          then obtain x' y' where "(x', x) \<in> p" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> p" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
2.214 +          then obtain x' y' where "(x', x) \<in> \<D>" "x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}" "(y', y) \<in> \<D>" "y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}"
2.215              by (auto)
2.216 -          from p'(5)[OF \<open>(x', x) \<in> p\<close> \<open>(y', y) \<in> p\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
2.217 +          from p'(5)[OF \<open>(x', x) \<in> \<D>\<close> \<open>(y', y) \<in> \<D>\<close>] \<open>x \<noteq> y\<close> have "interior (x \<inter> y) = {}"
2.218              by auto
2.219            moreover have "interior ((x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) \<inter> (y \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) \<subseteq> interior (x \<inter> y)"
2.220              by (auto intro: interior_mono)
2.221            ultimately have "interior (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = {}"
2.222              by (auto simp: eq)
2.223            then show "content (x \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) = 0"
2.224 -            using p'(4)[OF \<open>(x', x) \<in> p\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
2.225 +            using p'(4)[OF \<open>(x', x) \<in> \<D>\<close>] by (auto simp: interval_doublesplit[OF k] content_eq_0_interior simp del: interior_Int)
2.226          qed (insert p'(1), auto intro!: sum.mono_neutral_right)
2.227 -        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` p. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
2.228 +        also have "\<dots> \<le> norm (\<Sum>l\<in>(\<lambda>l. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})`{l\<in>snd ` \<D>. l \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d} \<noteq> {}}. content l *\<^sub>R 1::real)"
2.229            by simp
2.230          also have "\<dots> \<le> 1 * content (cbox a b \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})"
2.231            using division_doublesplit[OF p'' k, unfolded interval_doublesplit[OF k]]
2.232            unfolding interval_doublesplit[OF k] by (intro dsum_bound) auto
2.233          also have "\<dots> < e"
2.234 -          using d(2) by simp
2.235 -        finally show "(\<Sum>ka\<in>snd ` p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
2.236 +          using d by simp
2.237 +        finally show "(\<Sum>K\<in>snd ` \<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d})) < e" .
2.238        qed
2.239 -      finally show "(\<Sum>(x, ka)\<in>p. content (ka \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
2.240 +      finally show "(\<Sum>(x, K)\<in>\<D>. content (K \<inter> {x. \<bar>x \<bullet> k - c\<bar> \<le> d}) * ?i x) < e" .
2.241      qed
2.242 -    then show "norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R ?i x) - 0) < e"
2.243 -      unfolding * real_norm_def
2.244 +    then show "\<bar>\<Sum>(x, K)\<in>\<D>. content K * ?i x\<bar> < e"
2.245 +      unfolding *
2.246        apply (subst abs_of_nonneg)
2.247 -      using measure_nonneg  by (force simp add: indicator_def intro: sum_nonneg)+
2.248 +      using measure_nonneg
2.249 +      by (force simp add: indicator_def intro: sum_nonneg)+
2.250    qed
2.251  qed
2.252
2.253 @@ -2194,21 +2178,21 @@
2.254          done
2.255        also have "... \<le> (\<Sum>i\<le>N + 1. (real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar>)"
2.256          by (rule sum_mono) (simp add: sum_distrib_left [symmetric])
2.257 -      also have "... \<le> (\<Sum>i\<le>N + 1. e/2 / 2 ^ i)"
2.258 +      also have "... \<le> (\<Sum>i\<le>N + 1. e/2/2 ^ i)"
2.259        proof (rule sum_mono)
2.260 -        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2 / 2 ^ i"
2.261 +        show "(real i + 1) * \<bar>\<Sum>(x,K) \<in> q i. content K *\<^sub>R indicator S x\<bar> \<le> e/2/2 ^ i"
2.262            if "i \<in> {..N + 1}" for i
2.263            using \<gamma>[of "q i" i] q by (simp add: divide_simps mult.left_commute)
2.264        qed
2.265 -      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1 / 2) ^ i)"
2.266 +      also have "... = e/2 * (\<Sum>i\<le>N + 1. (1/2) ^ i)"
2.267          unfolding sum_distrib_left by (metis divide_inverse inverse_eq_divide power_one_over)
2.268        also have "\<dots> < e/2 * 2"
2.269        proof (rule mult_strict_left_mono)
2.270 -        have "sum (op ^ (1 / 2)) {..N + 1} = sum (op ^ (1 / 2::real)) {..<N + 2}"
2.271 +        have "sum (op ^ (1/2)) {..N + 1} = sum (op ^ (1/2::real)) {..<N + 2}"
2.272            using lessThan_Suc_atMost by auto
2.273          also have "... < 2"
2.274            by (auto simp: geometric_sum)
2.275 -        finally show "sum (op ^ (1 / 2::real)) {..N + 1} < 2" .
2.276 +        finally show "sum (op ^ (1/2::real)) {..N + 1} < 2" .
2.277        qed (use \<open>0 < e\<close> in auto)
2.278        finally  show ?thesis by auto
2.279      qed
2.280 @@ -2406,47 +2390,30 @@
2.281  lemma negligible_frontier_interval: "negligible(cbox (a::'a::euclidean_space) b - box a b)"
2.282  proof -
2.283    let ?A = "\<Union>((\<lambda>k. {x. x\<bullet>k = a\<bullet>k} \<union> {x::'a. x\<bullet>k = b\<bullet>k}) ` Basis)"
2.284 -  have "cbox a b - box a b \<subseteq> ?A"
2.285 -    apply rule unfolding Diff_iff mem_box
2.286 -    apply simp
2.287 -    apply(erule conjE bexE)+
2.288 -    apply(rule_tac x=i in bexI)
2.289 -    apply auto
2.290 -    done
2.291 -  then show ?thesis
2.292 -    apply -
2.293 -    apply (rule negligible_subset[of ?A])
2.294 -    apply (rule negligible_Union[OF finite_imageI])
2.295 -    apply auto
2.296 -    done
2.297 +  have "negligible ?A"
2.298 +    by (force simp add: negligible_Union[OF finite_imageI])
2.299 +  moreover have "cbox a b - box a b \<subseteq> ?A"
2.300 +    by (force simp add: mem_box)
2.301 +  ultimately show ?thesis
2.302 +    by (rule negligible_subset)
2.303  qed
2.304
2.305  lemma has_integral_spike_interior:
2.306 -  assumes "\<forall>x\<in>box a b. g x = f x"
2.307 -    and "(f has_integral y) (cbox a b)"
2.308 +  assumes f: "(f has_integral y) (cbox a b)" and gf: "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
2.309    shows "(g has_integral y) (cbox a b)"
2.310 -  apply (rule has_integral_spike[OF negligible_frontier_interval _ assms(2)])
2.311 -  using assms(1)
2.312 -  apply auto
2.313 -  done
2.314 +  apply (rule has_integral_spike[OF negligible_frontier_interval _ f])
2.315 +  using gf by auto
2.316
2.317  lemma has_integral_spike_interior_eq:
2.318 -  assumes "\<forall>x\<in>box a b. g x = f x"
2.319 +  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
2.320    shows "(f has_integral y) (cbox a b) \<longleftrightarrow> (g has_integral y) (cbox a b)"
2.321 -  apply rule
2.322 -  apply (rule_tac[!] has_integral_spike_interior)
2.323 -  using assms
2.324 -  apply auto
2.325 -  done
2.326 +  by (metis assms has_integral_spike_interior)
2.327
2.328  lemma integrable_spike_interior:
2.329 -  assumes "\<forall>x\<in>box a b. g x = f x"
2.330 +  assumes "\<And>x. x \<in> box a b \<Longrightarrow> g x = f x"
2.331      and "f integrable_on cbox a b"
2.332    shows "g integrable_on cbox a b"
2.333 -  using assms
2.334 -  unfolding integrable_on_def
2.335 -  using has_integral_spike_interior[OF assms(1)]
2.336 -  by auto
2.337 +  using assms has_integral_spike_interior_eq by blast
2.338
2.339
2.340  subsection \<open>Integrability of continuous functions.\<close>
2.341 @@ -2727,7 +2694,7 @@
2.342  lemma ident_has_integral:
2.343    fixes a::real
2.344    assumes "a \<le> b"
2.345 -  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2) / 2) {a..b}"
2.346 +  shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
2.347  proof -
2.348    have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
2.349      apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
2.350 @@ -2740,7 +2707,7 @@
2.351  lemma integral_ident [simp]:
2.352    fixes a::real
2.353    assumes "a \<le> b"
2.354 -  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2) / 2 else 0)"
2.355 +  shows "integral {a..b} (\<lambda>x. x) = (if a \<le> b then (b\<^sup>2 - a\<^sup>2)/2 else 0)"
2.356    by (metis assms ident_has_integral integral_unique)
2.357
2.358  lemma ident_integrable_on:
2.359 @@ -2798,9 +2765,9 @@
2.360    and ivl: "a \<le> b"
2.361    defines "i \<equiv> \<lambda>x. ((b - x) ^ (p - 1) / fact (p - 1)) *\<^sub>R Df p x"
2.362    shows taylor_has_integral:
2.363 -    "(i has_integral f b - (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
2.364 +    "(i has_integral f b - (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)) {a..b}"
2.365    and taylor_integral:
2.366 -    "f b = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
2.367 +    "f b = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a) + integral {a..b} i"
2.368    and taylor_integrable:
2.369      "i integrable_on {a..b}"
2.370  proof goal_cases
2.371 @@ -2855,7 +2822,7 @@
2.372        by (auto intro!: image_eqI[where x = "p - x - 1"])
2.373    qed simp
2.374    from _ this
2.375 -  have "?sum a = (\<Sum>i<p. ((b - a) ^ i / fact i) *\<^sub>R Df i a)"
2.376 +  have "?sum a = (\<Sum>i<p. ((b-a) ^ i / fact i) *\<^sub>R Df i a)"
2.377      by (rule sum.reindex_cong) (auto simp add: inj_on_def Dg_def one)
2.378    finally show c: ?case .
2.379    case 2 show ?case using c integral_unique
2.380 @@ -2900,8 +2867,8 @@
2.381        by (meson content_eq_0 dual_order.antisym)
2.382      then have xi: "x\<bullet>i = d\<bullet>i"
2.383        using \<open>x \<in> K\<close> unfolding keq mem_box by (metis antisym)
2.384 -    define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i) / 2 then c\<bullet>i +
2.385 -      min e (b\<bullet>i - c\<bullet>i) / 2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i) / 2 else x\<bullet>j) *\<^sub>R j)"
2.386 +    define y where "y = (\<Sum>j\<in>Basis. (if j = i then if c\<bullet>i \<le> (a\<bullet>i + b\<bullet>i)/2 then c\<bullet>i +
2.387 +      min e (b\<bullet>i - c\<bullet>i)/2 else c\<bullet>i - min e (c\<bullet>i - a\<bullet>i)/2 else x\<bullet>j) *\<^sub>R j)"
2.388      show "\<exists>x'\<in>\<Union>(\<D> - {K}). x' \<noteq> x \<and> dist x' x < e"
2.389      proof (intro bexI conjI)
2.390        have "d \<in> cbox c d"
2.391 @@ -2960,18 +2927,17 @@
2.392  proof -
2.393    interpret comm_monoid conj True
2.394      by standard auto
2.395 +  have 1: "\<And>a b. box a b = {} \<Longrightarrow> f integrable_on cbox a b"
2.396 +    by (simp add: content_eq_0_interior integrable_on_null)
2.397 +  have 2: "\<And>a b c k.
2.398 +       \<lbrakk>k \<in> Basis;
2.399 +        f integrable_on cbox a b \<inter> {x. x \<bullet> k \<le> c};
2.400 +        f integrable_on cbox a b \<inter> {x. c \<le> x \<bullet> k}\<rbrakk>
2.401 +       \<Longrightarrow> f integrable_on cbox a b"
2.402 +    unfolding integrable_on_def by (auto intro!: has_integral_split)
2.403    show ?thesis
2.404      apply standard
2.405 -    apply safe
2.406 -       apply (subst integrable_on_def)
2.407 -       apply rule
2.408 -       apply (rule has_integral_null_eq[where i=0, THEN iffD2])
2.409 -        apply (simp add: content_eq_0_interior)
2.410 -       apply rule
2.411 -      apply (rule, assumption, assumption)+
2.412 -    unfolding integrable_on_def
2.413 -    apply (auto intro!: has_integral_split)
2.414 -    done
2.415 +    using 1 2 by blast+
2.416  qed
2.417
2.418  lemma integrable_subinterval:
2.419 @@ -3162,12 +3128,8 @@
2.420  lemma antiderivative_continuous:
2.421    fixes q b :: real
2.422    assumes "continuous_on {a..b} f"
2.423 -  obtains g where "\<forall>x\<in>{a..b}. (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
2.424 -  apply (rule that)
2.425 -  apply rule
2.426 -  using integral_has_vector_derivative[OF assms]
2.427 -  apply auto
2.428 -  done
2.429 +  obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
2.430 +  using integral_has_vector_derivative[OF assms] by auto
2.431
2.432
2.433  subsection \<open>Combined fundamental theorem of calculus.\<close>
2.434 @@ -3414,7 +3376,7 @@
2.435        apply (erule_tac x=i in ballE)
2.436        apply (auto simp: inner_simps mult_left_mono)
2.437        done
2.438 -    moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b - a) \<bullet> i"
2.439 +    moreover from True have *: "\<And>i. (m *\<^sub>R b + c) \<bullet> i - (m *\<^sub>R a + c) \<bullet> i = m *\<^sub>R (b-a) \<bullet> i"
2.440        by (simp add: inner_simps field_simps)
2.441      ultimately show ?thesis
2.442        by (simp add: image_affinity_cbox True content_cbox'
2.443 @@ -3427,7 +3389,7 @@
2.444        apply (erule_tac x=i in ballE)
2.445        apply (auto simp: inner_simps mult_left_mono)
2.446        done
2.447 -    moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b - a) \<bullet> i"
2.448 +    moreover from False have *: "\<And>i. (m *\<^sub>R a + c) \<bullet> i - (m *\<^sub>R b + c) \<bullet> i = (-m) *\<^sub>R (b-a) \<bullet> i"
2.449        by (simp add: inner_simps field_simps)
2.450      ultimately show ?thesis using False
2.451        by (simp add: image_affinity_cbox content_cbox'
2.452 @@ -3491,12 +3453,10 @@
2.453  lemma uminus_interval_vector[simp]:
2.454    fixes a b :: "'a::euclidean_space"
2.455    shows "uminus ` cbox a b = cbox (-b) (-a)"
2.456 -  apply (rule set_eqI)
2.457 -  apply rule
2.458 -  defer
2.459 -  unfolding image_iff
2.460 -  apply (rule_tac x="-x" in bexI)
2.461 -  apply (auto simp add:minus_le_iff le_minus_iff mem_box)
2.462 +  apply safe
2.463 +   apply (simp add: mem_box(2))
2.464 +  apply (rule_tac x="-x" in image_eqI)
2.465 +   apply (auto simp add: mem_box)
2.466    done
2.467
2.468  lemma has_integral_reflect_lemma[intro]:
2.469 @@ -3514,10 +3474,7 @@
2.470
2.471  lemma has_integral_reflect[simp]:
2.472    "((\<lambda>x. f (-x)) has_integral i) (cbox (-b) (-a)) \<longleftrightarrow> (f has_integral i) (cbox a b)"
2.473 -  apply rule
2.474 -  apply (drule_tac[!] has_integral_reflect_lemma)
2.475 -  apply auto
2.476 -  done
2.477 +  by (auto dest: has_integral_reflect_lemma)
2.478
2.479  lemma integrable_reflect[simp]: "(\<lambda>x. f(-x)) integrable_on cbox (-b) (-a) \<longleftrightarrow> f integrable_on cbox a b"
2.480    unfolding integrable_on_def by auto
2.481 @@ -3543,7 +3500,7 @@
2.482    fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
2.483    assumes "a \<le> b"
2.484      and contf: "continuous_on {a..b} f"
2.485 -    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f'(x)) (at x)"
2.486 +    and derf: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
2.487    shows "(f' has_integral (f b - f a)) {a..b}"
2.488  proof (cases "a = b")
2.489    case True
2.490 @@ -3553,165 +3510,163 @@
2.491  next
2.492    case False
2.493    with \<open>a \<le> b\<close> have ab: "a < b" by arith
2.494 -  let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<longrightarrow> d fine p \<longrightarrow>
2.495 -    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
2.496 -  { presume "\<And>e. e > 0 \<Longrightarrow> ?P e" then show ?thesis unfolding has_integral_factor_content_real by force }
2.497 -  fix e :: real
2.498 -  assume e: "e > 0"
2.499 -  then have eba8: "(e * (b - a)) / 8 > 0"
2.500 -    using ab by (auto simp add: field_simps)
2.501 -  note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
2.502 -  have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
2.503 -    using derf_exp by simp
2.504 -  have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
2.505 -    (is "\<forall>x \<in> box a b. ?Q x")
2.506 -  proof
2.507 -    fix x assume x: "x \<in> box a b"
2.508 -    show "?Q x"
2.509 -      apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
2.510 -      using x e by auto
2.511 -  qed
2.512 -  from this [unfolded bgauge_existence_lemma]
2.513 -  obtain d where d: "\<And>x. 0 < d x"
2.514 -    "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
2.515 +  show ?thesis
2.516 +    unfolding has_integral_factor_content_real
2.517 +  proof (intro allI impI)
2.518 +    fix e :: real
2.519 +    assume e: "e > 0"
2.520 +    then have eba8: "(e * (b-a)) / 8 > 0"
2.521 +      using ab by (auto simp add: field_simps)
2.522 +    note derf_exp = derf[unfolded has_vector_derivative_def has_derivative_at_alt]
2.523 +    have bounded: "\<And>x. x \<in> {a<..<b} \<Longrightarrow> bounded_linear (\<lambda>u. u *\<^sub>R f' x)"
2.524 +      using derf_exp by simp
2.525 +    have "\<forall>x \<in> box a b. \<exists>d>0. \<forall>y. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
2.526 +      (is "\<forall>x \<in> box a b. ?Q x")
2.527 +    proof
2.528 +      fix x assume x: "x \<in> box a b"
2.529 +      show "?Q x"
2.530 +        apply (rule allE [where x="e/2", OF derf_exp [THEN conjunct2, of x]])
2.531 +        using x e by auto
2.532 +    qed
2.533 +    from this [unfolded bgauge_existence_lemma]
2.534 +    obtain d where d: "\<And>x. 0 < d x"
2.535 +      "\<And>x y. \<lbrakk>x \<in> box a b; norm (y-x) < d x\<rbrakk>
2.536                 \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e/2 * norm (y-x)"
2.537 -    by metis
2.538 -  have "bounded (f ` cbox a b)"
2.539 -    apply (rule compact_imp_bounded compact_continuous_image)+
2.540 -    using compact_cbox assms by auto
2.541 -  then obtain B
2.542 -    where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
2.543 -    unfolding bounded_pos by metis
2.544 -  obtain da where "0 < da"
2.545 -    and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
2.546 -                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b - a)) / 4"
2.547 -  proof -
2.548 -    have "continuous (at a within {a..b}) f"
2.549 -      using contf continuous_on_eq_continuous_within by force
2.550 -    with eba8 obtain k where "0 < k"
2.551 -      and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk>
2.552 -                          \<Longrightarrow> norm (f x - f a) < e * (b - a) / 8"
2.553 -      unfolding continuous_within Lim_within dist_norm by metis
2.554 -    obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b - a) / 8"
2.555 -    proof (cases "f' a = 0")
2.556 -      case True with ab e that show ?thesis by auto
2.557 -    next
2.558 -      case False
2.559 -      then show ?thesis
2.560 -        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' a)" in that)
2.561 -        using ab e apply (auto simp add: field_simps)
2.562 -        done
2.563 -    qed
2.564 -    have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
2.565 -      if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
2.566 +      by metis
2.567 +    have "bounded (f ` cbox a b)"
2.568 +      using compact_cbox assms by (auto simp: compact_imp_bounded compact_continuous_image)
2.569 +    then obtain B
2.570 +      where "0 < B" and B: "\<And>x. x \<in> f ` cbox a b \<Longrightarrow> norm x \<le> B"
2.571 +      unfolding bounded_pos by metis
2.572 +    obtain da where "0 < da"
2.573 +      and da: "\<And>c. \<lbrakk>a \<le> c; {a..c} \<subseteq> {a..b}; {a..c} \<subseteq> ball a da\<rbrakk>
2.574 +                          \<Longrightarrow> norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> (e * (b-a)) / 4"
2.575      proof -
2.576 -      have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
2.577 -        using bmin dist_real_def that by auto
2.578 -      then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
2.579 -        using that by force
2.580 -      have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)"
2.581 -        by (rule norm_triangle_ineq4)
2.582 -      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
2.584 -        have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
2.585 -          by (auto intro: mult_right_mono [OF lel])
2.586 -        also have "... \<le> e * (b - a) / 8"
2.587 -          by (rule l)
2.588 -        finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b - a) / 8" .
2.589 +      have "continuous (at a within {a..b}) f"
2.590 +        using contf continuous_on_eq_continuous_within by force
2.591 +      with eba8 obtain k where "0 < k"
2.592 +        and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm (x-a); norm (x-a) < k\<rbrakk> \<Longrightarrow> norm (f x - f a) < e * (b-a) / 8"
2.593 +        unfolding continuous_within Lim_within dist_norm by metis
2.594 +      obtain l where l: "0 < l" "norm (l *\<^sub>R f' a) \<le> e * (b-a) / 8"
2.595 +      proof (cases "f' a = 0")
2.596 +        case True with ab e that show ?thesis by auto
2.597        next
2.598 -        have "norm (f c - f a) < e * (b - a) / 8"
2.599 -        proof (cases "a = c")
2.600 -          case True then show ?thesis
2.601 -            using eba8 by auto
2.602 -        next
2.603 -          case False show ?thesis
2.604 -            by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
2.605 -        qed
2.606 -        then show "norm (f c - f a) \<le> e * (b - a) / 8" by simp
2.607 +        case False
2.608 +        then show ?thesis
2.609 +          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' a)" in that)
2.610 +          using ab e apply (auto simp add: field_simps)
2.611 +          done
2.612        qed
2.613 -      finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b - a) / 4"
2.614 -        unfolding content_real[OF \<open>a \<le> c\<close>] by auto
2.615 +      have "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
2.616 +        if "a \<le> c" "{a..c} \<subseteq> {a..b}" and bmin: "{a..c} \<subseteq> ball a (min k l)" for c
2.617 +      proof -
2.618 +        have minkl: "\<bar>a - x\<bar> < min k l" if "x \<in> {a..c}" for x
2.619 +          using bmin dist_real_def that by auto
2.620 +        then have lel: "\<bar>c - a\<bar> \<le> \<bar>l\<bar>"
2.621 +          using that by force
2.622 +        have "norm ((c - a) *\<^sub>R f' a - (f c - f a)) \<le> norm ((c - a) *\<^sub>R f' a) + norm (f c - f a)"
2.623 +          by (rule norm_triangle_ineq4)
2.624 +        also have "\<dots> \<le> e * (b-a) / 8 + e * (b-a) / 8"
2.626 +          have "norm ((c - a) *\<^sub>R f' a) \<le> norm (l *\<^sub>R f' a)"
2.627 +            by (auto intro: mult_right_mono [OF lel])
2.628 +          also have "... \<le> e * (b-a) / 8"
2.629 +            by (rule l)
2.630 +          finally show "norm ((c - a) *\<^sub>R f' a) \<le> e * (b-a) / 8" .
2.631 +        next
2.632 +          have "norm (f c - f a) < e * (b-a) / 8"
2.633 +          proof (cases "a = c")
2.634 +            case True then show ?thesis
2.635 +              using eba8 by auto
2.636 +          next
2.637 +            case False show ?thesis
2.638 +              by (rule k) (use minkl \<open>a \<le> c\<close> that False in auto)
2.639 +          qed
2.640 +          then show "norm (f c - f a) \<le> e * (b-a) / 8" by simp
2.641 +        qed
2.642 +        finally show "norm (content {a..c} *\<^sub>R f' a - (f c - f a)) \<le> e * (b-a) / 4"
2.643 +          unfolding content_real[OF \<open>a \<le> c\<close>] by auto
2.644 +      qed
2.645 +      then show ?thesis
2.646 +        by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
2.647      qed
2.648 -    then show ?thesis
2.649 -      by (rule_tac da="min k l" in that) (auto simp: l \<open>0 < k\<close>)
2.650 -  qed
2.651 -  obtain db where "0 < db"
2.652 -            and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
2.653 -                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b - a)) / 4"
2.654 -  proof -
2.655 -    have "continuous (at b within {a..b}) f"
2.656 -      using contf continuous_on_eq_continuous_within by force
2.657 -    with eba8 obtain k
2.658 -      where "0 < k"
2.659 -        and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
2.660 -                     \<Longrightarrow> norm (f b - f x) < e * (b - a) / 8"
2.661 -      unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
2.662 -    obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b - a)) / 8"
2.663 -    proof (cases "f' b = 0")
2.664 -      case True thus ?thesis
2.665 -        using ab e that by auto
2.666 -    next
2.667 -      case False then show ?thesis
2.668 -        apply (rule_tac l="(e * (b - a)) / 8 / norm (f' b)" in that)
2.669 -        using ab e by (auto simp add: field_simps)
2.670 -    qed
2.671 -    have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4"
2.672 -      if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
2.673 +    obtain db where "0 < db"
2.674 +      and db: "\<And>c. \<lbrakk>c \<le> b; {c..b} \<subseteq> {a..b}; {c..b} \<subseteq> ball b db\<rbrakk>
2.675 +                          \<Longrightarrow> norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> (e * (b-a)) / 4"
2.676      proof -
2.677 -      have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
2.678 -        using bmin dist_real_def that by auto
2.679 -      then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
2.680 -        using that by force
2.681 -      have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)"
2.682 -        by (rule norm_triangle_ineq4)
2.683 -      also have "\<dots> \<le> e * (b - a) / 8 + e * (b - a) / 8"
2.685 -        have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
2.686 -          by (auto intro: mult_right_mono [OF lel])
2.687 -        also have "... \<le> e * (b - a) / 8"
2.688 -          by (rule l)
2.689 -        finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b - a) / 8" .
2.690 +      have "continuous (at b within {a..b}) f"
2.691 +        using contf continuous_on_eq_continuous_within by force
2.692 +      with eba8 obtain k
2.693 +        where "0 < k"
2.694 +          and k: "\<And>x. \<lbrakk>x \<in> {a..b}; 0 < norm(x-b); norm(x-b) < k\<rbrakk>
2.695 +                     \<Longrightarrow> norm (f b - f x) < e * (b-a) / 8"
2.696 +        unfolding continuous_within Lim_within dist_norm norm_minus_commute by metis
2.697 +      obtain l where l: "0 < l" "norm (l *\<^sub>R f' b) \<le> (e * (b-a)) / 8"
2.698 +      proof (cases "f' b = 0")
2.699 +        case True thus ?thesis
2.700 +          using ab e that by auto
2.701        next
2.702 -        have "norm (f b - f c) < e * (b - a) / 8"
2.703 -        proof (cases "b = c")
2.704 -          case True with eba8 show ?thesis
2.705 -            by auto
2.706 -        next
2.707 -          case False show ?thesis
2.708 -            by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
2.709 -        qed
2.710 -        then show "norm (f b - f c) \<le> e * (b - a) / 8" by simp
2.711 +        case False then show ?thesis
2.712 +          apply (rule_tac l="(e * (b-a)) / 8 / norm (f' b)" in that)
2.713 +          using ab e by (auto simp add: field_simps)
2.714        qed
2.715 -      finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b - a) / 4"
2.716 -        unfolding content_real[OF \<open>c \<le> b\<close>] by auto
2.717 +      have "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4"
2.718 +        if "c \<le> b" "{c..b} \<subseteq> {a..b}" and bmin: "{c..b} \<subseteq> ball b (min k l)" for c
2.719 +      proof -
2.720 +        have minkl: "\<bar>b - x\<bar> < min k l" if "x \<in> {c..b}" for x
2.721 +          using bmin dist_real_def that by auto
2.722 +        then have lel: "\<bar>b - c\<bar> \<le> \<bar>l\<bar>"
2.723 +          using that by force
2.724 +        have "norm ((b - c) *\<^sub>R f' b - (f b - f c)) \<le> norm ((b - c) *\<^sub>R f' b) + norm (f b - f c)"
2.725 +          by (rule norm_triangle_ineq4)
2.726 +        also have "\<dots> \<le> e * (b-a) / 8 + e * (b-a) / 8"
2.728 +          have "norm ((b - c) *\<^sub>R f' b) \<le> norm (l *\<^sub>R f' b)"
2.729 +            by (auto intro: mult_right_mono [OF lel])
2.730 +          also have "... \<le> e * (b-a) / 8"
2.731 +            by (rule l)
2.732 +          finally show "norm ((b - c) *\<^sub>R f' b) \<le> e * (b-a) / 8" .
2.733 +        next
2.734 +          have "norm (f b - f c) < e * (b-a) / 8"
2.735 +          proof (cases "b = c")
2.736 +            case True with eba8 show ?thesis
2.737 +              by auto
2.738 +          next
2.739 +            case False show ?thesis
2.740 +              by (rule k) (use minkl \<open>c \<le> b\<close> that False in auto)
2.741 +          qed
2.742 +          then show "norm (f b - f c) \<le> e * (b-a) / 8" by simp
2.743 +        qed
2.744 +        finally show "norm (content {c..b} *\<^sub>R f' b - (f b - f c)) \<le> e * (b-a) / 4"
2.745 +          unfolding content_real[OF \<open>c \<le> b\<close>] by auto
2.746 +      qed
2.747 +      then show ?thesis
2.748 +        by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
2.749      qed
2.750 -    then show ?thesis
2.751 -      by (rule_tac db="min k l" in that) (auto simp: l \<open>0 < k\<close>)
2.752 -  qed
2.753 -  let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
2.754 -  show "?P e"
2.755 -  proof (intro exI conjI allI impI)
2.756 -    show "gauge ?d"
2.757 -      using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
2.758 -  next
2.759 -    fix p
2.760 -    assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
2.761 -    let ?A = "{t. fst t \<in> {a, b}}"
2.762 -    note p = tagged_division_ofD[OF ptag]
2.763 -    have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
2.764 -      using ptag fine by auto
2.765 -    note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
2.766 -    have **: "\<And>n1 s1 n2 s2::real. n2 \<le> s2 / 2 \<Longrightarrow> n1 - s1 \<le> s2 / 2 \<Longrightarrow> n1 + n2 \<le> s1 + s2"
2.767 -      by arith
2.768 -    have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
2.769 -         and less: "e * (Sup K - Inf K) / 2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
2.770 -         for x K
2.771 +    let ?d = "(\<lambda>x. ball x (if x=a then da else if x=b then db else d x))"
2.772 +    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
2.773 +              norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b})"
2.774 +    proof (rule exI, safe)
2.775 +      show "gauge ?d"
2.776 +        using ab \<open>db > 0\<close> \<open>da > 0\<close> d(1) by (auto intro: gauge_ball_dependent)
2.777 +    next
2.778 +      fix p
2.779 +      assume ptag: "p tagged_division_of {a..b}" and fine: "?d fine p"
2.780 +      let ?A = "{t. fst t \<in> {a, b}}"
2.781 +      note p = tagged_division_ofD[OF ptag]
2.782 +      have pA: "p = (p \<inter> ?A) \<union> (p - ?A)" "finite (p \<inter> ?A)" "finite (p - ?A)" "(p \<inter> ?A) \<inter> (p - ?A) = {}"
2.783 +        using ptag fine by auto
2.784 +      have le_xz: "\<And>w x y z::real. y \<le> z/2 \<Longrightarrow> w - x \<le> z/2 \<Longrightarrow> w + y \<le> x + z"
2.785 +        by arith
2.786 +      have non: False if xk: "(x,K) \<in> p" and "x \<noteq> a" "x \<noteq> b"
2.787 +        and less: "e * (Sup K - Inf K)/2 < norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
2.788 +      for x K
2.789        proof -
2.790          obtain u v where k: "K = cbox u v"
2.791            using p(4) xk by blast
2.792          then have "u \<le> v" and uv: "{u, v} \<subseteq> cbox u v"
2.793            using p(2)[OF xk] by auto
2.794 -        then have result: "e * (v - u) / 2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
2.795 +        then have result: "e * (v - u)/2 < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
2.796            using less[unfolded k box_real interval_bounds_real content_real] by auto
2.797          then have "x \<in> box a b"
2.798            using p(2) p(3) \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> xk by fastforce
2.799 @@ -3721,8 +3676,8 @@
2.800          have xd: "norm (u - x) < d x" "norm (v - x) < d x"
2.801            using fineD[OF fine xk] \<open>x \<noteq> a\<close> \<open>x \<noteq> b\<close> uv
2.802            by (auto simp add: k subset_eq dist_commute dist_real_def)
2.803 -        have "norm ((v - u) *\<^sub>R f' (x) - (f (v) - f (u))) =
2.804 -              norm ((f (u) - f (x) - (u - x) *\<^sub>R f' (x)) - (f (v) - f (x) - (v - x) *\<^sub>R f' (x)))"
2.805 +        have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) =
2.806 +              norm ((f u - f x - (u - x) *\<^sub>R f' x) - (f v - f x - (v - x) *\<^sub>R f' x))"
2.807            by (rule arg_cong[where f=norm]) (auto simp: scaleR_left.diff)
2.808          also have "\<dots> \<le> e/2 * norm (u - x) + e/2 * norm (v - x)"
2.809            by (metis norm_triangle_le_diff add_mono * xd)
2.810 @@ -3730,211 +3685,184 @@
2.811            using p(2)[OF xk] by (auto simp add: field_simps k)
2.812          also have "\<dots> < norm ((v - u) *\<^sub>R f' x - (f v - f u))"
2.813            using result by (simp add: \<open>u \<le> v\<close>)
2.814 -        finally have "e * (v - u) / 2 < e * (v - u) / 2"
2.815 +        finally have "e * (v - u)/2 < e * (v - u)/2"
2.816            using uv by auto
2.817          then show False by auto
2.818        qed
2.819 -    have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
2.820 +      have "norm (\<Sum>(x, K)\<in>p - ?A. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
2.821            \<le> (\<Sum>(x, K)\<in>p - ?A. norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
2.822 -      by (auto intro: sum_norm_le)
2.823 -    also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k) / 2)"
2.824 -      using non by (force intro: sum_mono)
2.825 -    finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
2.826 +        by (auto intro: sum_norm_le)
2.827 +      also have "... \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)/2)"
2.828 +        using non by (fastforce intro: sum_mono)
2.829 +      finally have I: "norm (\<Sum>(x, k)\<in>p - ?A.
2.830                    content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
2.831 -             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
2.832 -      by (simp add: sum_divide_distrib)
2.833 -    have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
2.834 +             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
2.835 +        by (simp add: sum_divide_distrib)
2.836 +      have II: "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) -
2.837               (\<Sum>n\<in>p \<inter> ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))
2.838 -             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
2.839 -    proof -
2.840 -      have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
2.841 +             \<le> (\<Sum>n\<in>p - ?A. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
2.842        proof -
2.843 -        obtain u v where uv: "k = cbox u v"
2.844 -          by (meson Int_iff xkp p(4))
2.845 -        with p(2) that uv have "cbox u v \<noteq> {}"
2.846 -          by blast
2.847 -        then show "0 \<le> e * ((Sup k) - (Inf k))"
2.848 -          unfolding uv using e by (auto simp add: field_simps)
2.849 -      qed
2.850 -      let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
2.851 -      let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
2.852 -      have "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a) / 2"
2.853 -      proof -
2.854 -        have *: "\<And>s f e. sum f s = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f s) \<le> e"
2.855 -          by auto
2.856 -        have 1: "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
2.857 -                if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
2.858 +        have ge0: "0 \<le> e * (Sup k - Inf k)" if xkp: "(x, k) \<in> p \<inter> ?A" for x k
2.859          proof -
2.860 -          have xk: "(x, K) \<in> p" and k0: "content K = 0"
2.861 -            using that by auto
2.862 -          then obtain u v where uv: "K = cbox u v"
2.863 -            using p(4) by blast
2.864 -          then have "u = v"
2.865 -            using xk k0 p(2) by force
2.866 -          then show "content K *\<^sub>R (f' (x)) - (f ((Sup K)) - f ((Inf K))) = 0"
2.867 -            using xk unfolding uv by auto
2.868 -        qed
2.869 -        have 2: "norm(\<Sum>(x,k)\<in>p \<inter> ?C. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
2.870 -                 \<le> e * (b - a) / 2"
2.871 -        proof -
2.872 -          have *: "p \<inter> ?C = ?B a \<union> ?B b"
2.873 +          obtain u v where uv: "k = cbox u v"
2.874 +            by (meson Int_iff xkp p(4))
2.875 +          with p(2) that uv have "cbox u v \<noteq> {}"
2.876              by blast
2.877 -          have **: "norm (sum f s) \<le> e"
2.878 -            if "\<forall>x y. x \<in> s \<and> y \<in> s \<longrightarrow> x = y" "\<forall>x. x \<in> s \<longrightarrow> norm (f x) \<le> e" "e > 0"
2.879 -            for s f and e :: real
2.880 -          proof (cases "s = {}")
2.881 -            case True
2.882 -            with that show ?thesis by auto
2.883 -          next
2.884 -            case False
2.885 -            then obtain x where "x \<in> s"
2.886 -              by auto
2.887 -            then have "s = {x}"
2.888 -              using that(1) by auto
2.889 -            then show ?thesis
2.890 -              using \<open>x \<in> s\<close> that(2) by auto
2.891 +          then show "0 \<le> e * ((Sup k) - (Inf k))"
2.892 +            unfolding uv using e by (auto simp add: field_simps)
2.893 +        qed
2.894 +        let ?B = "\<lambda>x. {t \<in> p. fst t = x \<and> content (snd t) \<noteq> 0}"
2.895 +        let ?C = "{t \<in> p. fst t \<in> {a, b} \<and> content (snd t) \<noteq> 0}"
2.896 +        have "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2"
2.897 +        proof -
2.898 +          have *: "\<And>S f e. sum f S = sum f (p \<inter> ?C) \<Longrightarrow> norm (sum f (p \<inter> ?C)) \<le> e \<Longrightarrow> norm (sum f S) \<le> e"
2.899 +            by auto
2.900 +          have 1: "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
2.901 +            if "(x,K) \<in> p \<inter> {t. fst t \<in> {a, b}} - p \<inter> ?C" for x K
2.902 +          proof -
2.903 +            have xk: "(x,K) \<in> p" and k0: "content K = 0"
2.904 +              using that by auto
2.905 +            then obtain u v where uv: "K = cbox u v"
2.906 +              using p(4) by blast
2.907 +            then have "u = v"
2.908 +              using xk k0 p(2) by force
2.909 +            then show "content K *\<^sub>R (f' x) - (f ((Sup K)) - f ((Inf K))) = 0"
2.910 +              using xk unfolding uv by auto
2.911            qed
2.912 -          show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
2.913 -                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b - a) / 2"
2.914 -            apply (subst *)
2.915 -            apply (subst sum.union_disjoint)
2.916 -               prefer 4
2.917 -               apply (rule order_trans[of _ "e * (b - a)/4 + e * (b - a)/4"])
2.918 -                apply (rule norm_triangle_le,rule add_mono)
2.919 -                 apply (rule_tac[1-2] **)
2.920 -
2.921 +          have 2: "norm(\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))  \<le> e * (b-a)/2"
2.922            proof -
2.923 -            have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
2.924 -            proof -
2.925 -              obtain u v where uv: "k = cbox u v"
2.926 -                using \<open>(a, k) \<in> p\<close> p(4) by blast
2.927 -              moreover have "u \<le> v"
2.928 -                using uv p(2)[OF that] by auto
2.929 -              moreover have "u = a"
2.930 -                using p(2) p(3) that uv by force
2.931 -              ultimately show ?thesis
2.932 -                by blast
2.933 -            qed
2.934 -            have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
2.935 -            proof -
2.936 -              obtain u v where uv: "k = cbox u v"
2.937 -                using \<open>(b, k) \<in> p\<close> p(4) by blast
2.938 -              moreover have "u \<le> v"
2.939 -                using p(2)[OF that] unfolding uv by auto
2.940 -              moreover have "v = b"
2.941 -                using p(2) p(3) that uv by force
2.942 -              ultimately show ?thesis
2.943 -                by blast
2.944 +            have norm_le: "norm (sum f S) \<le> e"
2.945 +              if "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> x = y" "\<And>x. x \<in> S \<Longrightarrow> norm (f x) \<le> e" "e > 0"
2.946 +              for S f and e :: real
2.947 +            proof (cases "S = {}")
2.948 +              case True
2.949 +              with that show ?thesis by auto
2.950 +            next
2.951 +              case False then obtain x where "x \<in> S"
2.952 +                by auto
2.953 +              then have "S = {x}"
2.954 +                using that(1) by auto
2.955 +              then show ?thesis
2.956 +                using \<open>x \<in> S\<close> that(2) by auto
2.957              qed
2.958 -            show "\<forall>x y. x \<in> ?B a \<and> y \<in> ?B a \<longrightarrow> x = y"
2.959 -            proof (safe; clarsimp)
2.960 -              fix x k k'
2.961 -              assume k: "(a, k) \<in> p" "(a, k') \<in> p" "content k \<noteq> 0" "content k' \<noteq> 0"
2.962 -              obtain v where v: "k = cbox a v" "a \<le> v"
2.963 -                using pa[OF k(1)] by blast
2.964 -              obtain v' where v': "k' = cbox a v'" "a \<le> v'"
2.965 -                using pa[OF k(2)] by blast
2.966 -              let ?v = "min v v'"
2.967 -              have "box a ?v \<subseteq> k \<inter> k'"
2.968 -                unfolding v v' by (auto simp add: mem_box)
2.969 -              then have "interior (box a (min v v')) \<subseteq> interior k \<inter> interior k'"
2.970 -                using interior_Int interior_mono by blast
2.971 -              moreover have "(a + ?v)/2 \<in> box a ?v"
2.972 -                using k(3-)
2.973 -                unfolding v v' content_eq_0 not_le
2.974 -                by (auto simp add: mem_box)
2.975 -              ultimately have "(a + ?v)/2 \<in> interior k \<inter> interior k'"
2.976 -                unfolding interior_open[OF open_box] by auto
2.977 -              then have eq: "k = k'"
2.978 -                using p(5)[OF k(1-2)] by auto
2.979 -              { assume "x \<in> k" then show "x \<in> k'" unfolding eq . }
2.980 -              { assume "x \<in> k'" then show "x \<in> k" unfolding eq . }
2.981 -            qed
2.982 -
2.983 -            show "\<forall>x y. x \<in> ?B b \<and> y \<in> ?B b \<longrightarrow> x = y"
2.984 -            proof (safe; clarsimp)
2.985 -              fix x K K'
2.986 -              assume k: "(b, K) \<in> p" "(b, K') \<in> p" "content K \<noteq> 0" "content K' \<noteq> 0"
2.987 -              obtain v where v: "K = cbox v b" "v \<le> b"
2.988 -                using pb[OF k(1)] by blast
2.989 -              obtain v' where v': "K' = cbox v' b" "v' \<le> b"
2.990 -                using pb[OF k(2)] by blast
2.991 -              let ?v = "max v v'"
2.992 -              have "box ?v b \<subseteq> K \<inter> K'"
2.993 -                unfolding v v' by (auto simp: mem_box)
2.994 -              then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
2.995 -                using interior_Int interior_mono by blast
2.996 -              moreover have " ((b + ?v)/2) \<in> box ?v b"
2.997 -                using k(3-) unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
2.998 -              ultimately have " ((b + ?v)/2) \<in> interior K \<inter> interior K'"
2.999 -                unfolding interior_open[OF open_box] by auto
2.1000 -              then have eq: "K = K'"
2.1001 -                using p(5)[OF k(1-2)] by auto
2.1002 -              { assume "x \<in> K" then show "x \<in> K'" unfolding eq . }
2.1003 -              { assume "x \<in> K'" then show "x \<in> K" unfolding eq . }
2.1004 +            have *: "p \<inter> ?C = ?B a \<union> ?B b"
2.1005 +              by blast
2.1006 +            then have "norm (\<Sum>(x,K)\<in>p \<inter> ?C. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) =
2.1007 +                       norm (\<Sum>(x,K) \<in> ?B a \<union> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))"
2.1008 +              by simp
2.1009 +            also have "... = norm ((\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) +
2.1010 +                                   (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))))"
2.1011 +              apply (subst sum.union_disjoint)
2.1012 +              using p(1) ab e by auto
2.1013 +            also have "... \<le> e * (b - a) / 4 + e * (b - a) / 4"
2.1014 +            proof (rule norm_triangle_le [OF add_mono])
2.1015 +              have pa: "\<exists>v. k = cbox a v \<and> a \<le> v" if "(a, k) \<in> p" for k
2.1016 +                using p(2) p(3) p(4) that by fastforce
2.1017 +              show "norm (\<Sum>(x,K) \<in> ?B a. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
2.1018 +              proof (intro norm_le; clarsimp)
2.1019 +                fix K K'
2.1020 +                assume K: "(a, K) \<in> p" "(a, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
2.1021 +                with pa obtain v v' where v: "K = cbox a v" "a \<le> v" and v': "K' = cbox a v'" "a \<le> v'"
2.1022 +                  by blast
2.1023 +                let ?v = "min v v'"
2.1024 +                have "box a ?v \<subseteq> K \<inter> K'"
2.1025 +                  unfolding v v' by (auto simp add: mem_box)
2.1026 +                then have "interior (box a (min v v')) \<subseteq> interior K \<inter> interior K'"
2.1027 +                  using interior_Int interior_mono by blast
2.1028 +                moreover have "(a + ?v)/2 \<in> box a ?v"
2.1029 +                  using ne0  unfolding v v' content_eq_0 not_le
2.1030 +                  by (auto simp add: mem_box)
2.1031 +                ultimately have "(a + ?v)/2 \<in> interior K \<inter> interior K'"
2.1032 +                  unfolding interior_open[OF open_box] by auto
2.1033 +                then show "K = K'"
2.1034 +                  using p(5)[OF K] by auto
2.1035 +              next
2.1036 +                fix K
2.1037 +                assume K: "(a, K) \<in> p" and ne0: "content K \<noteq> 0"
2.1038 +                show "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
2.1039 +                  if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
2.1040 +                proof -
2.1041 +                  obtain v where v: "c = cbox a v" and "a \<le> v"
2.1042 +                    using pa[OF \<open>(a, c) \<in> p\<close>] by metis
2.1043 +                  then have "a \<in> {a..v}" "v \<le> b"
2.1044 +                    using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
2.1045 +                  moreover have "{a..v} \<subseteq> ball a da"
2.1046 +                    using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
2.1047 +                  ultimately show ?thesis
2.1048 +                    unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
2.1049 +                    using da \<open>a \<le> v\<close> by auto
2.1050 +                qed
2.1051 +              qed (use ab e in auto)
2.1052 +            next
2.1053 +              have pb: "\<exists>v. k = cbox v b \<and> b \<ge> v" if "(b, k) \<in> p" for k
2.1054 +                using p(2) p(3) p(4) that by fastforce
2.1055 +              show "norm (\<Sum>(x,K) \<in> ?B b. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (b - a) / 4"
2.1056 +              proof (intro norm_le; clarsimp)
2.1057 +                fix K K'
2.1058 +                assume K: "(b, K) \<in> p" "(b, K') \<in> p" and ne0: "content K \<noteq> 0" "content K' \<noteq> 0"
2.1059 +                with pb obtain v v' where v: "K = cbox v b" "v \<le> b" and v': "K' = cbox v' b" "v' \<le> b"
2.1060 +                  by blast
2.1061 +                let ?v = "max v v'"
2.1062 +                have "box ?v b \<subseteq> K \<inter> K'"
2.1063 +                  unfolding v v' by (auto simp: mem_box)
2.1064 +                then have "interior (box (max v v') b) \<subseteq> interior K \<inter> interior K'"
2.1065 +                  using interior_Int interior_mono by blast
2.1066 +                moreover have " ((b + ?v)/2) \<in> box ?v b"
2.1067 +                  using ne0 unfolding v v' content_eq_0 not_le by (auto simp: mem_box)
2.1068 +                ultimately have "((b + ?v)/2) \<in> interior K \<inter> interior K'"
2.1069 +                  unfolding interior_open[OF open_box] by auto
2.1070 +                then show "K = K'"
2.1071 +                  using p(5)[OF K] by auto
2.1072 +              next
2.1073 +                fix K
2.1074 +                assume K: "(b, K) \<in> p" and ne0: "content K \<noteq> 0"
2.1075 +                show "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) * 4 \<le> e * (b-a)"
2.1076 +                  if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
2.1077 +                proof -
2.1078 +                obtain v where v: "c = cbox v b" and "v \<le> b"
2.1079 +                  using \<open>(b, c) \<in> p\<close> pb by blast
2.1080 +                then have "v \<ge> a""b \<in> {v.. b}"
2.1081 +                  using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
2.1082 +                moreover have "{v..b} \<subseteq> ball b db"
2.1083 +                  using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
2.1084 +                ultimately show ?thesis
2.1085 +                  using db v by auto
2.1086 +                qed
2.1087 +              qed (use ab e in auto)
2.1088              qed
2.1089 -
2.1090 -            have "norm (content c *\<^sub>R f' a - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
2.1091 -              if "(a, c) \<in> p" and ne0: "content c \<noteq> 0" for c
2.1092 -            proof -
2.1093 -              obtain v where v: "c = cbox a v" and "a \<le> v"
2.1094 -                using pa[OF \<open>(a, c) \<in> p\<close>] by metis
2.1095 -              then have "a \<in> {a..v}" "v \<le> b"
2.1096 -                using p(3)[OF \<open>(a, c) \<in> p\<close>] by auto
2.1097 -              moreover have "{a..v} \<subseteq> ball a da"
2.1098 -                using fineD[OF \<open>?d fine p\<close> \<open>(a, c) \<in> p\<close>] by (simp add: v split: if_split_asm)
2.1099 -              ultimately show ?thesis
2.1100 -                unfolding v interval_bounds_real[OF \<open>a \<le> v\<close>] box_real
2.1101 -                using da \<open>a \<le> v\<close> by auto
2.1102 -            qed
2.1103 -            then show "\<forall>x. x \<in> ?B a \<longrightarrow> norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) -
2.1104 -              f (Inf k))) x) \<le> e * (b - a) / 4"
2.1105 -              by auto
2.1106 -
2.1107 -            have "norm (content c *\<^sub>R f' b - (f (Sup c) - f (Inf c))) \<le> e * (b - a) / 4"
2.1108 -              if "(b, c) \<in> p" and ne0: "content c \<noteq> 0" for c
2.1109 -            proof -
2.1110 -              obtain v where v: "c = cbox v b" and "v \<le> b"
2.1111 -                using \<open>(b, c) \<in> p\<close> pb by blast
2.1112 -              then have "v \<ge> a""b \<in> {v.. b}"
2.1113 -                using p(3)[OF \<open>(b, c) \<in> p\<close>] by auto
2.1114 -              moreover have "{v..b} \<subseteq> ball b db"
2.1115 -                using fineD[OF \<open>?d fine p\<close> \<open>(b, c) \<in> p\<close>] box_real(2) v False by force
2.1116 -              ultimately show ?thesis
2.1117 -                using db v by auto
2.1118 -            qed
2.1119 -            then show "\<forall>x. x \<in> ?B b \<longrightarrow>
2.1120 -                           norm ((\<lambda>(x, k). content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) x)
2.1121 -                           \<le> e * (b - a) / 4"
2.1122 -              by auto
2.1123 -          qed (insert p(1) ab e, auto simp add: field_simps)
2.1124 +            also have "... = e * (b-a)/2"
2.1125 +              by simp
2.1126 +            finally show "norm (\<Sum>(x,k)\<in>p \<inter> ?C.
2.1127 +                        content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le> e * (b-a)/2" .
2.1128 +          qed
2.1129 +          show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \<le> e * (b-a)/2"
2.1130 +            apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
2.1131 +            using 1 2 by (auto simp: split_paired_all)
2.1132          qed
2.1133 -        show "norm (\<Sum>(x, k)\<in>p \<inter> ?A. content k *\<^sub>R f' x - (f ((Sup k)) - f ((Inf k)))) \<le> e * (b - a) / 2"
2.1134 -          apply (rule * [OF sum.mono_neutral_right[OF pA(2)]])
2.1135 -          using 1 2 by (auto simp: split_paired_all)
2.1136 +        also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))/2"
2.1137 +          unfolding sum_distrib_left[symmetric]
2.1138 +          apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
2.1139 +          by auto
2.1140 +        finally have norm_le: "norm (\<Sum>(x,K)\<in>p \<inter> {t. fst t \<in> {a, b}}. content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
2.1141 +                \<le> (\<Sum>n\<in>p. e * (case n of (x, K) \<Rightarrow> Sup K - Inf K))/2" .
2.1142 +        have le2: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2)/2 \<Longrightarrow> x - s1 \<le> s2/2"
2.1143 +          by auto
2.1144 +        show ?thesis
2.1145 +          apply (rule le2 [OF sum_nonneg])
2.1146 +          using ge0 apply force
2.1147 +          unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
2.1148 +          by (metis norm_le)
2.1149        qed
2.1150 -      also have "... = (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2"
2.1151 -        unfolding sum_distrib_left[symmetric]
2.1152 -        apply (subst additive_tagged_division_1[OF \<open>a \<le> b\<close> ptag])
2.1153 -        by auto
2.1154 -      finally have norm_le: "norm (\<Sum>(x, k)\<in>p \<inter> {t. fst t \<in> {a, b}}. content k *\<^sub>R f' x - (f (Sup k) - f (Inf k)))
2.1155 -                \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k)) / 2" .
2.1156 -      have *: "\<And>x s1 s2::real. 0 \<le> s1 \<Longrightarrow> x \<le> (s1 + s2) / 2 \<Longrightarrow> x - s1 \<le> s2 / 2"
2.1157 -        by auto
2.1158 -      show ?thesis
2.1159 -        apply (rule * [OF sum_nonneg])
2.1160 -        using ge0 apply force
2.1161 -        unfolding sum.union_disjoint[OF pA(2-), symmetric] pA(1)[symmetric]
2.1162 -        by (metis norm_le)
2.1163 +      note * = additive_tagged_division_1[OF assms(1) ptag, symmetric]
2.1164 +      have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
2.1165 +               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
2.1166 +        unfolding sum_distrib_left
2.1167 +        unfolding sum.union_disjoint[OF pA(2-)]
2.1168 +        using le_xz norm_triangle_le I II by blast
2.1169 +      then
2.1170 +      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
2.1171 +        by (simp only: content_real[OF \<open>a \<le> b\<close>] *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus pA(1) [symmetric])
2.1172      qed
2.1173 -    have "norm (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). content K *\<^sub>R f' x - (f (Sup K) - f (Inf K)))
2.1174 -               \<le> e * (\<Sum>(x,K)\<in>p \<inter> ?A \<union> (p - ?A). Sup K - Inf K)"
2.1175 -      unfolding sum_distrib_left
2.1176 -      unfolding sum.union_disjoint[OF pA(2-)]
2.1177 -      using ** norm_triangle_le I II by blast
2.1178 -    then
2.1179 -    show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content {a..b}"
2.1180 -      by (simp only: content_real[OF \<open>a \<le> b\<close>] *[of "\<lambda>x. x"] *[of f] sum_subtractf[symmetric] split_minus pA(1) [symmetric])
2.1181    qed
2.1182  qed
2.1183
2.1184 @@ -3992,12 +3920,9 @@
2.1185    using vec apply (auto simp: mem_box)
2.1186    done
2.1187
2.1188 -lemma indefinite_integral_continuous_left:
2.1189 +proposition indefinite_integral_continuous_left:
2.1190    fixes f:: "real \<Rightarrow> 'a::banach"
2.1191 -  assumes intf: "f integrable_on {a..b}"
2.1192 -    and "a < c"
2.1193 -    and "c \<le> b"
2.1194 -    and "e > 0"
2.1195 +  assumes intf: "f integrable_on {a..b}" and "a < c" "c \<le> b" "e > 0"
2.1196    obtains d where "d > 0"
2.1197      and "\<forall>t. c - d < t \<and> t \<le> c \<longrightarrow> norm (integral {a..c} f - integral {a..t} f) < e"
2.1198  proof -
2.1199 @@ -4020,14 +3945,14 @@
2.1200        using \<open>e > 0\<close> that by auto
2.1201    qed
2.1202
2.1203 +  let ?SUM = "\<lambda>p. (\<Sum>(x,K) \<in> p. content K *\<^sub>R f x)"
2.1204    have e3: "e/3 > 0"
2.1205      using \<open>e > 0\<close> by auto
2.1206    have "f integrable_on {a..c}"
2.1207      apply (rule integrable_subinterval_real[OF intf])
2.1208      using \<open>a < c\<close> \<open>c \<le> b\<close> by auto
2.1209    then obtain d1 where "gauge d1" and d1:
2.1210 -    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow>
2.1211 -            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..c} f) < e/3"
2.1212 +    "\<And>p. \<lbrakk>p tagged_division_of {a..c}; d1 fine p\<rbrakk> \<Longrightarrow> norm (?SUM p - integral {a..c} f) < e/3"
2.1213      using integrable_integral has_integral_real e3 by metis
2.1214    define d where [abs_def]: "d x = ball x w \<inter> d1 x" for x
2.1215    have "gauge d"
2.1216 @@ -4035,132 +3960,102 @@
2.1217    then obtain k where "0 < k" and k: "ball c k \<subseteq> d c"
2.1218      by (meson gauge_def open_contains_ball)
2.1219
2.1220 -  let ?d = "min k (c - a) / 2"
2.1221 -  show ?thesis
2.1222 -    apply (rule that[of ?d])
2.1223 -    apply safe
2.1224 -  proof -
2.1225 +  let ?d = "min k (c - a)/2"
2.1226 +  show thesis
2.1227 +  proof (intro that[of ?d] allI impI, safe)
2.1228      show "?d > 0"
2.1229 -      using \<open>0 < k\<close> using assms(2) by auto
2.1230 +      using \<open>0 < k\<close> \<open>a < c\<close> by auto
2.1231 +  next
2.1232      fix t
2.1233 -    assume as: "c - ?d < t" "t \<le> c"
2.1234 -    let ?thesis = "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
2.1235 -    {
2.1236 -      presume *: "t < c \<Longrightarrow> ?thesis"
2.1237 -      show ?thesis
2.1238 -      proof (cases "t = c")
2.1239 -        case True
2.1240 -        then show ?thesis
2.1241 -          by (simp add: \<open>e > 0\<close>)
2.1242 -      next
2.1243 -        case False
2.1244 -        then show ?thesis
2.1245 -          using "*" \<open>t \<le> c\<close> by linarith
2.1246 -      qed
2.1247 -    }
2.1248 -    assume "t < c"
2.1249 -
2.1250 -    have "f integrable_on {a..t}"
2.1251 -      apply (rule integrable_subinterval_real[OF intf])
2.1252 -      using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
2.1253 -    then obtain d2 where d2: "gauge d2"
2.1254 -      "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow>
2.1255 -            norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
2.1256 -      using integrable_integral has_integral_real e3 by metis
2.1257 -    define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
2.1258 -    have "gauge d3"
2.1259 -      using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
2.1260 -    then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
2.1261 -      by (metis box_real(2) fine_division_exists)
2.1262 -    note p'=tagged_division_ofD[OF ptag]
2.1263 -    have pt: "(x,k)\<in>p \<Longrightarrow> x \<le> t" for x k
2.1264 -      by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
2.1265 -    with pfine have "d2 fine p"
2.1266 -      unfolding fine_def d3_def by fastforce
2.1267 -    then have d2_fin: "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f x) - integral {a..t} f) < e/3"
2.1268 -      using d2(2) ptag by auto
2.1269 -    have *: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
2.1270 -      using as by (auto simp add: field_simps)
2.1271 -
2.1272 -    have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
2.1273 -      apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
2.1274 -      using  \<open>t \<le> c\<close> by (auto simp: * ptag tagged_division_of_self_real)
2.1275 -    moreover
2.1276 -    have "d1 fine p \<union> {(c, {t..c})}"
2.1277 -      unfolding fine_def
2.1278 -    proof safe
2.1279 -      fix x K y
2.1280 -      assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
2.1281 -        by (metis Int_iff d3_def subsetD fineD pfine)
2.1282 +    assume t: "c - ?d < t" "t \<le> c"
2.1283 +    show "norm (integral ({a..c}) f - integral ({a..t}) f) < e"
2.1284 +    proof (cases "t < c")
2.1285 +      case False with \<open>t \<le> c\<close> show ?thesis
2.1286 +        by (simp add: \<open>e > 0\<close>)
2.1287      next
2.1288 -      fix x assume "x \<in> {t..c}"
2.1289 -      then have "dist c x < k"
2.1290 -        using as(1)
2.1291 -        by (auto simp add: field_simps dist_real_def)
2.1292 -      with k show "x \<in> d1 c"
2.1293 -        unfolding d_def by auto
2.1294 -    qed
2.1295 -    ultimately have d1_fin: "norm ((\<Sum>(x,K) \<in> p \<union> {(c, {t..c})}. content K *\<^sub>R f x) - integral {a..c} f) < e/3"
2.1296 -      using d1 by metis
2.1297 -
2.1298 -    have *: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)) -
2.1299 -      integral {a..c} f) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - integral {a..t} f) + (c - t) *\<^sub>R f c"
2.1300 -      "e = (e/3 + e/3) + e/3"
2.1301 -      by auto
2.1302 -    have **: "(\<Sum>(x, k)\<in>p \<union> {(c, {t..c})}. content k *\<^sub>R f x) =
2.1303 -      (c - t) *\<^sub>R f c + (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
2.1304 -    proof -
2.1305 -      have **: "\<And>x F. F \<union> {x} = insert x F"
2.1306 -        by auto
2.1307 -      have "(c, cbox t c) \<notin> p"
2.1308 -      proof (safe, goal_cases)
2.1309 -        case prems: 1
2.1310 -        from p'(2-3)[OF prems] have "c \<in> cbox a t"
2.1311 -          by auto
2.1312 -        then show False using \<open>t < c\<close>
2.1313 -          by auto
2.1314 +      case True
2.1315 +      have "f integrable_on {a..t}"
2.1316 +        apply (rule integrable_subinterval_real[OF intf])
2.1317 +        using \<open>t < c\<close> \<open>c \<le> b\<close> by auto
2.1318 +      then obtain d2 where d2: "gauge d2"
2.1319 +        "\<And>p. p tagged_division_of {a..t} \<and> d2 fine p \<Longrightarrow> norm (?SUM p - integral {a..t} f) < e/3"
2.1320 +        using integrable_integral has_integral_real e3 by metis
2.1321 +      define d3 where "d3 x = (if x \<le> t then d1 x \<inter> d2 x else d1 x)" for x
2.1322 +      have "gauge d3"
2.1323 +        using \<open>gauge d1\<close> \<open>gauge d2\<close> unfolding d3_def gauge_def by auto
2.1324 +      then obtain p where ptag: "p tagged_division_of {a..t}" and pfine: "d3 fine p"
2.1325 +        by (metis box_real(2) fine_division_exists)
2.1326 +      note p' = tagged_division_ofD[OF ptag]
2.1327 +      have pt: "(x,K)\<in>p \<Longrightarrow> x \<le> t" for x K
2.1328 +        by (meson atLeastAtMost_iff p'(2) p'(3) subsetCE)
2.1329 +      with pfine have "d2 fine p"
2.1330 +        unfolding fine_def d3_def by fastforce
2.1331 +      then have d2_fin: "norm (?SUM p - integral {a..t} f) < e/3"
2.1332 +        using d2(2) ptag by auto
2.1333 +      have eqs: "{a..c} \<inter> {x. x \<le> t} = {a..t}" "{a..c} \<inter> {x. x \<ge> t} = {t..c}"
2.1334 +        using t by (auto simp add: field_simps)
2.1335 +      have "p \<union> {(c, {t..c})} tagged_division_of {a..c}"
2.1336 +        apply (rule tagged_division_Un_interval_real[of _ _ _ 1 "t"])
2.1337 +        using  \<open>t \<le> c\<close> by (auto simp: eqs ptag tagged_division_of_self_real)
2.1338 +      moreover
2.1339 +      have "d1 fine p \<union> {(c, {t..c})}"
2.1340 +        unfolding fine_def
2.1341 +      proof safe
2.1342 +        fix x K y
2.1343 +        assume "(x,K) \<in> p" and "y \<in> K" then show "y \<in> d1 x"
2.1344 +          by (metis Int_iff d3_def subsetD fineD pfine)
2.1345 +      next
2.1346 +        fix x assume "x \<in> {t..c}"
2.1347 +        then have "dist c x < k"
2.1348 +          using t(1) by (auto simp add: field_simps dist_real_def)
2.1349 +        with k show "x \<in> d1 c"
2.1350 +          unfolding d_def by auto
2.1351 +      qed
2.1352 +      ultimately have d1_fin: "norm (?SUM(p \<union> {(c, {t..c})}) - integral {a..c} f) < e/3"
2.1353 +        using d1 by metis
2.1354 +      have SUMEQ: "?SUM(p \<union> {(c, {t..c})}) = (c - t) *\<^sub>R f c + ?SUM p"
2.1355 +      proof -
2.1356 +        have "?SUM(p \<union> {(c, {t..c})}) = (content{t..c} *\<^sub>R f c) + ?SUM p"
2.1357 +        proof (subst sum.union_disjoint)
2.1358 +          show "p \<inter> {(c, {t..c})} = {}"
2.1359 +            using \<open>t < c\<close> pt by force
2.1360 +        qed (use p'(1) in auto)
2.1361 +        also have "... = (c - t) *\<^sub>R f c + ?SUM p"
2.1362 +          using \<open>t \<le> c\<close> by auto
2.1363 +        finally show ?thesis .
2.1364        qed
2.1365 -      then show ?thesis
2.1366 -        unfolding ** box_real
2.1367 -        apply -
2.1368 -        apply (subst sum.insert)
2.1369 -        apply (rule p')
2.1370 -        unfolding split_conv
2.1371 -        defer
2.1372 -        apply (subst content_real)
2.1373 -        using as(2)
2.1374 -        apply auto
2.1375 -        done
2.1376 -    qed
2.1377 -    have ***: "c - w < t \<and> t < c"
2.1378 -    proof -
2.1379        have "c - k < t"
2.1380 -        using \<open>k>0\<close> as(1) by (auto simp add: field_simps)
2.1381 +        using \<open>k>0\<close> t(1) by (auto simp add: field_simps)
2.1382        moreover have "k \<le> w"
2.1383 -        apply (rule ccontr)
2.1384 -        using k
2.1385 -        unfolding subset_eq
2.1386 -        apply (erule_tac x="c + ((k + w)/2)" in ballE)
2.1387 -        unfolding d_def
2.1388 -        using \<open>k > 0\<close> \<open>w > 0\<close>
2.1389 -        apply (auto simp add: field_simps not_le not_less dist_real_def)
2.1390 -        done
2.1391 -      ultimately show ?thesis using \<open>t < c\<close>
2.1392 +      proof (rule ccontr)
2.1393 +        assume "\<not> k \<le> w"
2.1394 +        then have "c + (k + w) / 2 \<notin> d c"
2.1395 +          by (auto simp add: field_simps not_le not_less dist_real_def d_def)
2.1396 +        then have "c + (k + w) / 2 \<notin> ball c k"
2.1397 +          using k by blast
2.1398 +        then show False
2.1399 +          using \<open>0 < w\<close> \<open>\<not> k \<le> w\<close> dist_real_def by auto
2.1400 +      qed
2.1401 +      ultimately have cwt: "c - w < t"
2.1402          by (auto simp add: field_simps)
2.1403 +      have eq: "integral {a..c} f - integral {a..t} f = -(((c - t) *\<^sub>R f c + ?SUM p) -
2.1404 +             integral {a..c} f) + (?SUM p - integral {a..t} f) + (c - t) *\<^sub>R f c"
2.1405 +        by auto
2.1406 +      have "norm (integral {a..c} f - integral {a..t} f) < e/3 + e/3 + e/3"
2.1407 +        unfolding eq
2.1408 +      proof (intro norm_triangle_lt add_strict_mono)
2.1409 +        show "norm (- ((c - t) *\<^sub>R f c + ?SUM p - integral {a..c} f)) < e/3"
2.1410 +          by (metis SUMEQ d1_fin norm_minus_cancel)
2.1411 +        show "norm (?SUM p - integral {a..t} f) < e/3"
2.1412 +          using d2_fin by blast
2.1413 +        show "norm ((c - t) *\<^sub>R f c) < e/3"
2.1414 +          using w cwt \<open>t < c\<close> by (auto simp add: field_simps)
2.1415 +      qed
2.1416 +      then show ?thesis by simp
2.1417      qed
2.1418 -    show ?thesis
2.1419 -      unfolding *(1)
2.1420 -      apply (subst *(2))
2.1421 -      apply (rule norm_triangle_lt add_strict_mono)+
2.1422 -      apply (metis "**" d1_fin norm_minus_cancel)
2.1423 -      using d2_fin apply blast
2.1424 -      using w ***
2.1425 -      apply (auto simp add: field_simps)
2.1426 -      done
2.1427    qed
2.1428  qed
2.1429
2.1430 -
2.1431  lemma indefinite_integral_continuous_right:
2.1432    fixes f :: "real \<Rightarrow> 'a::banach"
2.1433    assumes "f integrable_on {a..b}"
2.1434 @@ -4424,97 +4319,66 @@
2.1435    assumes intf: "(f has_integral i) (cbox c d)"
2.1436      and cb: "cbox c d \<subseteq> cbox a b"
2.1437    shows "((\<lambda>x. if x \<in> box c d then f x else 0) has_integral i) (cbox a b)"
2.1438 -proof -
2.1439 +proof (cases "cbox c d = {}")
2.1440 +  case True
2.1441 +  then have "box c d = {}"
2.1442 +    by (metis bot.extremum_uniqueI box_subset_cbox)
2.1443 +  then show ?thesis
2.1444 +    using True intf by auto
2.1445 +next
2.1446 +  case False
2.1447 +  then obtain p where pdiv: "p division_of cbox a b" and inp: "cbox c d \<in> p"
2.1448 +    using cb partial_division_extend_1 by blast
2.1449    define g where [abs_def]: "g x = (if x \<in>box c d then f x else 0)" for x
2.1450 -  {
2.1451 -    presume *: "cbox c d \<noteq> {} \<Longrightarrow> ?thesis"
2.1452 -    show ?thesis
2.1453 -      apply cases
2.1454 -      apply (rule *)
2.1455 -      apply assumption
2.1456 -    proof goal_cases
2.1457 -      case prems: 1
2.1458 -      then have *: "box c d = {}"
2.1459 -        by (metis bot.extremum_uniqueI box_subset_cbox)
2.1460 -      show ?thesis
2.1461 -        using assms(1)
2.1462 -        unfolding *
2.1463 -        using prems
2.1464 -        by auto
2.1465 -    qed
2.1466 -  }
2.1467 -  assume "cbox c d \<noteq> {}"
2.1468 -  then obtain p where p: "p division_of cbox a b" "cbox c d \<in> p"
2.1469 -    using cb partial_division_extend_1 by blast
2.1470    interpret operative "lift_option plus" "Some (0 :: 'b)"
2.1471      "\<lambda>i. if g integrable_on i then Some (integral i g) else None"
2.1472      by (fact operative_integralI)
2.1473 -  note operat = division
2.1474 -    [OF p(1), symmetric]
2.1475 -  let ?P = "(if g integrable_on cbox a b then Some (integral (cbox a b) g) else None) = Some i"
2.1476 -  {
2.1477 -    presume "?P"
2.1478 -    then have "g integrable_on cbox a b \<and> integral (cbox a b) g = i"
2.1479 -      apply -
2.1480 -      apply cases
2.1481 -      apply (subst(asm) if_P)
2.1482 -      apply assumption
2.1483 -      apply auto
2.1484 -      done
2.1485 -    then show ?thesis
2.1486 -      using integrable_integral
2.1487 -      unfolding g_def
2.1488 -      by auto
2.1489 -  }
2.1490 -  let ?F = F
2.1491 -  have iterate:"?F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
2.1492 -  proof (intro neutral ballI)
2.1493 -    fix x
2.1494 -    assume x: "x \<in> p - {cbox c d}"
2.1495 -    then have "x \<in> p"
2.1496 -      by auto
2.1497 -    note div = division_ofD(2-5)[OF p(1) this]
2.1498 -    then obtain u v where uv: "x = cbox u v" by blast
2.1499 -    have "interior x \<inter> interior (cbox c d) = {}"
2.1500 -      using div(4)[OF p(2)] x by auto
2.1501 -    then have "(g has_integral 0) x"
2.1502 -      unfolding uv
2.1503 -      using has_integral_spike_interior[where f="\<lambda>x. 0"]
2.1504 -      by (metis (no_types, lifting) disjoint_iff_not_equal g_def has_integral_0_eq interior_cbox)
2.1505 -    then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
2.1506 -      by auto
2.1507 +  note operat = division [OF pdiv, symmetric]
2.1508 +  show ?thesis
2.1509 +  proof (cases "(g has_integral i) (cbox a b)")
2.1510 +    case True then show ?thesis
2.1511 +      by (simp add: g_def)
2.1512 +  next
2.1513 +    case False
2.1514 +    have iterate:"F (\<lambda>i. if g integrable_on i then Some (integral i g) else None) (p - {cbox c d}) = Some 0"
2.1515 +    proof (intro neutral ballI)
2.1516 +      fix x
2.1517 +      assume x: "x \<in> p - {cbox c d}"
2.1518 +      then have "x \<in> p"
2.1519 +        by auto
2.1520 +      then obtain u v where uv: "x = cbox u v"
2.1521 +        using pdiv by blast
2.1522 +      have "interior x \<inter> interior (cbox c d) = {}"
2.1523 +        using pdiv inp x by blast
2.1524 +      then have "(g has_integral 0) x"
2.1525 +        unfolding uv using has_integral_spike_interior[where f="\<lambda>x. 0"]
2.1526 +        by (metis (no_types, lifting) disjoint_iff_not_equal g_def has_integral_0_eq interior_cbox)
2.1527 +      then show "(if g integrable_on x then Some (integral x g) else None) = Some 0"
2.1528 +        by auto
2.1529 +    qed
2.1530 +    interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
2.1531 +      by (intro comm_monoid_set.intro comm_monoid_lift_option add.comm_monoid_axioms)
2.1532 +    have intg: "g integrable_on cbox c d"
2.1533 +      using integrable_spike_interior[where f=f]
2.1534 +      by (meson g_def has_integral_integrable intf)
2.1535 +    moreover have "integral (cbox c d) g = i"
2.1536 +    proof (rule has_integral_unique[OF has_integral_spike_interior intf])
2.1537 +      show "\<And>x. x \<in> box c d \<Longrightarrow> f x = g x"
2.1538 +        by (auto simp: g_def)
2.1539 +      show "(g has_integral integral (cbox c d) g) (cbox c d)"
2.1540 +        by (rule integrable_integral[OF intg])
2.1541 +    qed
2.1542 +    ultimately have "F (\<lambda>A. if g integrable_on A then Some (integral A g) else None) p = Some i"
2.1543 +      by (metis (full_types, lifting) division_of_finite inp iterate pdiv remove right_neutral)
2.1544 +    then
2.1545 +    have "(g has_integral i) (cbox a b)"
2.1546 +      by (metis integrable_on_def integral_unique operat option.inject option.simps(3))
2.1547 +    with False show ?thesis
2.1548 +      by blast
2.1549    qed
2.1550 -
2.1551 -  have *: "p = insert (cbox c d) (p - {cbox c d})"
2.1552 -    using p by auto
2.1553 -  interpret comm_monoid_set "lift_option plus" "Some (0 :: 'b)"
2.1554 -    apply (rule comm_monoid_set.intro)
2.1555 -    apply (rule comm_monoid_lift_option)
2.1557 -    done
2.1558 -  have **: "g integrable_on cbox c d"
2.1559 -    apply (rule integrable_spike_interior[where f=f])
2.1560 -    unfolding g_def  using assms(1)
2.1561 -    apply auto
2.1562 -    done
2.1563 -  moreover
2.1564 -  have "integral (cbox c d) g = i"
2.1565 -    apply (rule has_integral_unique[OF _ assms(1)])
2.1566 -    apply (rule has_integral_spike_interior[where f=g])
2.1567 -    defer
2.1568 -    apply (rule integrable_integral[OF **])
2.1569 -    unfolding g_def
2.1570 -    apply auto
2.1571 -    done
2.1572 -  ultimately show ?P
2.1573 -    unfolding operat
2.1574 -    using p
2.1575 -    apply (subst *)
2.1576 -    apply (subst insert)
2.1577 -    apply (simp_all add: division_of_finite iterate)
2.1578 -    done
2.1579  qed
2.1580
2.1581 +
2.1582  lemma has_integral_restrict_closed_subinterval:
2.1583    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::banach"
2.1584    assumes "(f has_integral i) (cbox c d)"
2.1585 @@ -4539,28 +4403,21 @@
2.1586    case False
2.1587    let ?g = "\<lambda>x. if x \<in> cbox c d then f x else 0"
2.1588    show ?thesis
2.1589 -    apply rule
2.1590 -    defer
2.1591 -    apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
2.1592 -    apply assumption
2.1593 -  proof -
2.1594 +  proof
2.1595      assume ?l
2.1596      then have "?g integrable_on cbox c d"
2.1597        using assms has_integral_integrable integrable_subinterval by blast
2.1598 -    then have *: "f integrable_on cbox c d"
2.1599 +    then have "f integrable_on cbox c d"
2.1600        apply -
2.1601        apply (rule integrable_eq)
2.1602        apply auto
2.1603        done
2.1604 -    then have "i = integral (cbox c d) f"
2.1605 -      apply -
2.1606 -      apply (rule has_integral_unique)
2.1607 -      apply (rule \<open>?l\<close>)
2.1608 -      apply (rule has_integral_restrict_closed_subinterval[OF _ assms])
2.1609 -      apply auto
2.1610 -      done
2.1611 -    then show ?r
2.1612 -      using * by auto
2.1613 +    moreover then have "i = integral (cbox c d) f"
2.1614 +      by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
2.1615 +    ultimately show ?r by auto
2.1616 +  next
2.1617 +    assume ?r then show ?l
2.1618 +      by (rule has_integral_restrict_closed_subinterval[OF _ assms])
2.1619    qed
2.1620  qed auto
2.1621
2.1622 @@ -4672,10 +4529,9 @@
2.1623
2.1624  lemma integral_nonneg:
2.1625    fixes f :: "'n::euclidean_space \<Rightarrow> real"
2.1626 -  assumes "f integrable_on S"
2.1627 -    and "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
2.1628 +  assumes f: "f integrable_on S" and 0: "\<And>x. x \<in> S \<Longrightarrow> 0 \<le> f x"
2.1629    shows "0 \<le> integral S f"
2.1630 -  by (rule has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)])
2.1631 +  by (rule has_integral_nonneg[OF f[unfolded has_integral_integral] 0])
2.1632
2.1633
2.1634  text \<open>Hence a general restriction property.\<close>
2.1635 @@ -5033,11 +4889,11 @@
2.1636      if "e > 0" for e
2.1637    proof -
2.1638      have *: "e/2 > 0" using that by auto
2.1639 -    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e / 2"
2.1640 +    then obtain N where N: "\<And>n. N \<le> n \<Longrightarrow> norm (i - integral (?cube n) ?F) < e/2"
2.1641        using i[THEN LIMSEQ_D, simplified norm_minus_commute] by meson
2.1642      obtain B where "0 < B"
2.1643        and B: "\<And>a b c d. \<lbrakk>ball 0 B \<subseteq> cbox a b; ball 0 B \<subseteq> cbox c d\<rbrakk> \<Longrightarrow>
2.1644 -                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e / 2"
2.1645 +                  norm (integral (cbox a b) ?F - integral (cbox c d) ?F) < e/2"
2.1646        using rhs * by meson
2.1647      let ?B = "max (real N) B"
2.1648      show ?thesis
2.1649 @@ -6017,9 +5873,9 @@
2.1650          proof (rule *)
2.1651            show "\<bar>integral (cbox a b) (?f N) - i\<bar> < e/2"
2.1652            proof (rule abs_triangle_half_l)
2.1653 -            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2 / 2"
2.1654 +            show "\<bar>integral (cbox a b) (?f N) - integral S (f N)\<bar> < e/2/2"
2.1655                using B[OF ab] by simp
2.1656 -            show "abs (i - integral S (f N)) < e/2 / 2"
2.1657 +            show "abs (i - integral S (f N)) < e/2/2"
2.1658                using N by (simp add: abs_minus_commute)
2.1659            qed
2.1660            show "\<bar>integral (cbox a b) (?f (M + N)) - integral (cbox a b) ?g\<bar> < e/2"
2.1661 @@ -6953,7 +6809,7 @@
2.1662          also have "norm (t1 - x1, t2 - x2) < k"
2.1663            using xuvwz ls uwvz_sub unfolding ball_def
2.1664            by (force simp add: cbox_Pair_eq dist_norm )
2.1665 -        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX / 2"
2.1666 +        finally have "norm (f (x1,x2) - f (t1,t2)) \<le> e/content ?CBOX/2"
2.1667            using nf [OF t x]  by simp
2.1668        } note nf' = this
2.1669        have f_int_uwvz: "f integrable_on cbox (u,w) (v,z)"
2.1670 @@ -6962,9 +6818,9 @@
2.1671          using assms continuous_on_subset uwvz_sub
2.1672          by (blast intro: continuous_on_imp_integrable_on_Pair1)
2.1673        have 1: "norm (integral (cbox (u,w) (v,z)) f - integral (cbox (u,w) (v,z)) (\<lambda>x. f (t1,t2)))
2.1674 -         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
2.1675 +         \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
2.1676          apply (simp only: integral_diff [symmetric] f_int_uwvz integrable_const)
2.1677 -        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
2.1678 +        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
2.1679          using cbp \<open>0 < e/content ?CBOX\<close> nf'
2.1680          apply (auto simp: integrable_diff f_int_uwvz integrable_const)
2.1681          done
2.1682 @@ -6973,24 +6829,24 @@
2.1683        have normint_wz:
2.1684           "\<And>x. x \<in> cbox u v \<Longrightarrow>
2.1685                 norm (integral (cbox w z) (\<lambda>y. f (x, y)) - integral (cbox w z) (\<lambda>y. f (t1, t2)))
2.1686 -               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d)) / 2"
2.1687 +               \<le> e * content (cbox w z) / content (cbox (a, c) (b, d))/2"
2.1688          apply (simp only: integral_diff [symmetric] f_int_uv integrable_const)
2.1689 -        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX / 2"]])
2.1690 +        apply (rule order_trans [OF integrable_bound [of "e/content ?CBOX/2"]])
2.1691          using cbp \<open>0 < e/content ?CBOX\<close> nf'
2.1692          apply (auto simp: integrable_diff f_int_uv integrable_const)
2.1693          done
2.1694        have "norm (integral (cbox u v)
2.1695                 (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y)) - integral (cbox w z) (\<lambda>y. f (t1,t2))))
2.1696 -            \<le> e * content (cbox w z) / content ?CBOX / 2 * content (cbox u v)"
2.1697 +            \<le> e * content (cbox w z) / content ?CBOX/2 * content (cbox u v)"
2.1698          apply (rule integrable_bound [OF _ _ normint_wz])
2.1699          using cbp \<open>0 < e/content ?CBOX\<close>
2.1700          apply (auto simp: divide_simps content_pos_le integrable_diff int_integrable integrable_const)
2.1701          done
2.1702 -      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
2.1703 +      also have "... \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
2.1704          by (simp add: content_Pair divide_simps)
2.1705        finally have 2: "norm (integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))) -
2.1706                        integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (t1,t2))))
2.1707 -                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX / 2"
2.1708 +                \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
2.1709          by (simp only: integral_diff [symmetric] int_integrable integrable_const)
2.1710        have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
2.1711          using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
```