use filter to define Henstock-Kurzweil integration
authorhoelzl
Mon Sep 26 16:57:05 2016 +0200 (2016-09-26)
changeset 6394421eaff8c8fc9
parent 63943 fbc2b562331b
child 63945 444eafb6e864
use filter to define Henstock-Kurzweil integration
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
     1.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Sep 24 15:56:54 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon Sep 26 16:57:05 2016 +0200
     1.3 @@ -1927,108 +1927,6 @@
     1.4  lemma fine_subset: "p \<subseteq> q \<Longrightarrow> d fine q \<Longrightarrow> d fine p"
     1.5    unfolding fine_def by blast
     1.6  
     1.7 -
     1.8 -subsection \<open>Gauge integral. Define on compact intervals first, then use a limit.\<close>
     1.9 -
    1.10 -definition has_integral_compact_interval (infixr "has'_integral'_compact'_interval" 46)
    1.11 -  where "(f has_integral_compact_interval y) i \<longleftrightarrow>
    1.12 -    (\<forall>e>0. \<exists>d. gauge d \<and>
    1.13 -      (\<forall>p. p tagged_division_of i \<and> d fine p \<longrightarrow> norm ((\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) - y) < e))"
    1.14 -
    1.15 -definition has_integral ::
    1.16 -    "('n::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
    1.17 -  (infixr "has'_integral" 46)
    1.18 -  where "(f has_integral y) i \<longleftrightarrow>
    1.19 -    (if \<exists>a b. i = cbox a b
    1.20 -     then (f has_integral_compact_interval y) i
    1.21 -     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
    1.22 -      (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral_compact_interval z) (cbox a b) \<and>
    1.23 -        norm (z - y) < e)))"
    1.24 -
    1.25 -lemma has_integral:
    1.26 -  "(f has_integral y) (cbox a b) \<longleftrightarrow>
    1.27 -    (\<forall>e>0. \<exists>d. gauge d \<and>
    1.28 -      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
    1.29 -        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.30 -  unfolding has_integral_def has_integral_compact_interval_def
    1.31 -  by auto
    1.32 -
    1.33 -lemma has_integral_real:
    1.34 -  "(f has_integral y) {a .. b::real} \<longleftrightarrow>
    1.35 -    (\<forall>e>0. \<exists>d. gauge d \<and>
    1.36 -      (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
    1.37 -        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
    1.38 -  unfolding box_real[symmetric]
    1.39 -  by (rule has_integral)
    1.40 -
    1.41 -lemma has_integralD[dest]:
    1.42 -  assumes "(f has_integral y) (cbox a b)"
    1.43 -    and "e > 0"
    1.44 -  obtains d where "gauge d"
    1.45 -    and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
    1.46 -      norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f(x)) p - y) < e"
    1.47 -  using assms unfolding has_integral by auto
    1.48 -
    1.49 -lemma has_integral_alt:
    1.50 -  "(f has_integral y) i \<longleftrightarrow>
    1.51 -    (if \<exists>a b. i = cbox a b
    1.52 -     then (f has_integral y) i
    1.53 -     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
    1.54 -      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
    1.55 -  unfolding has_integral
    1.56 -  unfolding has_integral_compact_interval_def has_integral_def
    1.57 -  by auto
    1.58 -
    1.59 -lemma has_integral_altD:
    1.60 -  assumes "(f has_integral y) i"
    1.61 -    and "\<not> (\<exists>a b. i = cbox a b)"
    1.62 -    and "e>0"
    1.63 -  obtains B where "B > 0"
    1.64 -    and "\<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
    1.65 -      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
    1.66 -  using assms
    1.67 -  unfolding has_integral
    1.68 -  unfolding has_integral_compact_interval_def has_integral_def
    1.69 -  by auto
    1.70 -
    1.71 -definition integrable_on (infixr "integrable'_on" 46)
    1.72 -  where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
    1.73 -
    1.74 -definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
    1.75 -
    1.76 -lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
    1.77 -  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
    1.78 -
    1.79 -lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
    1.80 -  unfolding integrable_on_def integral_def by blast
    1.81 -
    1.82 -lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
    1.83 -  unfolding integrable_on_def by auto
    1.84 -
    1.85 -lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
    1.86 -  by auto
    1.87 -
    1.88 -lemma setsum_content_null:
    1.89 -  assumes "content (cbox a b) = 0"
    1.90 -    and "p tagged_division_of (cbox a b)"
    1.91 -  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
    1.92 -proof (rule setsum.neutral, rule)
    1.93 -  fix y
    1.94 -  assume y: "y \<in> p"
    1.95 -  obtain x k where xk: "y = (x, k)"
    1.96 -    using surj_pair[of y] by blast
    1.97 -  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
    1.98 -  from this(2) obtain c d where k: "k = cbox c d" by blast
    1.99 -  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
   1.100 -    unfolding xk by auto
   1.101 -  also have "\<dots> = 0"
   1.102 -    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
   1.103 -    unfolding assms(1) k
   1.104 -    by auto
   1.105 -  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
   1.106 -qed
   1.107 -
   1.108 -
   1.109  subsection \<open>Some basic combining lemmas.\<close>
   1.110  
   1.111  lemma tagged_division_unions_exists:
   1.112 @@ -2421,6 +2319,128 @@
   1.113    obtains p where "p tagged_division_of {a .. b}" "g fine p"
   1.114    by (metis assms box_real(2) fine_division_exists)
   1.115  
   1.116 +subsection \<open>Division filter\<close>
   1.117 +
   1.118 +text \<open>Divisions over all gauges towards finer divisions.\<close>
   1.119 +
   1.120 +definition division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
   1.121 +  where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
   1.122 +
   1.123 +lemma eventually_division_filter:
   1.124 +  "(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
   1.125 +    (\<exists>g. gauge g \<and> (\<forall>p. p tagged_division_of s \<and> g fine p \<longrightarrow> P p))"
   1.126 +  unfolding division_filter_def
   1.127 +proof (subst eventually_INF_base; clarsimp)
   1.128 +  fix g1 g2 :: "'a \<Rightarrow> 'a set" show "gauge g1 \<Longrightarrow> gauge g2 \<Longrightarrow> \<exists>x. gauge x \<and>
   1.129 +    {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g1 fine p} \<and>
   1.130 +    {p. p tagged_division_of s \<and> x fine p} \<subseteq> {p. p tagged_division_of s \<and> g2 fine p}"
   1.131 +    by (intro exI[of _ "\<lambda>x. g1 x \<inter> g2 x"]) (auto simp: fine_inter)
   1.132 +qed (auto simp: eventually_principal)
   1.133 +
   1.134 +lemma division_filter_not_empty: "division_filter (cbox a b) \<noteq> bot"
   1.135 +  unfolding trivial_limit_def eventually_division_filter
   1.136 +  by (auto elim: fine_division_exists)
   1.137 +
   1.138 +lemma eventually_division_filter_tagged_division:
   1.139 +  "eventually (\<lambda>p. p tagged_division_of s) (division_filter s)"
   1.140 +  unfolding eventually_division_filter by (intro exI[of _ "\<lambda>x. ball x 1"]) auto
   1.141 +
   1.142 +subsection \<open>Gauge integral\<close>
   1.143 +
   1.144 +text \<open>Case distinction to define it first on compact intervals first, then use a limit. This is only
   1.145 +much later unified. In Fremlin: Measure Theory, Volume 4I this is generalized using residual sets.\<close>
   1.146 +
   1.147 +definition has_integral :: "('n::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'b \<Rightarrow> 'n set \<Rightarrow> bool"
   1.148 +  (infixr "has'_integral" 46)
   1.149 +  where "(f has_integral I) s \<longleftrightarrow>
   1.150 +    (if \<exists>a b. s = cbox a b
   1.151 +      then ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter s)
   1.152 +      else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.153 +        (\<exists>z. ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R (if x \<in> s then f x else 0)) \<longlongrightarrow> z) (division_filter (cbox a b)) \<and>
   1.154 +          norm (z - I) < e)))"
   1.155 +
   1.156 +lemma has_integral_cbox:
   1.157 +  "(f has_integral I) (cbox a b) \<longleftrightarrow> ((\<lambda>p. \<Sum>(x,k)\<in>p. content k *\<^sub>R f x) \<longlongrightarrow> I) (division_filter (cbox a b))"
   1.158 +  by (auto simp add: has_integral_def)
   1.159 +
   1.160 +lemma has_integral:
   1.161 +  "(f has_integral y) (cbox a b) \<longleftrightarrow>
   1.162 +    (\<forall>e>0. \<exists>d. gauge d \<and>
   1.163 +      (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.164 +        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
   1.165 +  by (auto simp: dist_norm eventually_division_filter has_integral_def tendsto_iff)
   1.166 +
   1.167 +lemma has_integral_real:
   1.168 +  "(f has_integral y) {a .. b::real} \<longleftrightarrow>
   1.169 +    (\<forall>e>0. \<exists>d. gauge d \<and>
   1.170 +      (\<forall>p. p tagged_division_of {a .. b} \<and> d fine p \<longrightarrow>
   1.171 +        norm (setsum (\<lambda>(x,k). content(k) *\<^sub>R f x) p - y) < e))"
   1.172 +  unfolding box_real[symmetric]
   1.173 +  by (rule has_integral)
   1.174 +
   1.175 +lemma has_integralD[dest]:
   1.176 +  assumes "(f has_integral y) (cbox a b)"
   1.177 +    and "e > 0"
   1.178 +  obtains d
   1.179 +    where "gauge d"
   1.180 +      and "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d fine p \<Longrightarrow>
   1.181 +        norm ((\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) - y) < e"
   1.182 +  using assms unfolding has_integral by auto
   1.183 +
   1.184 +lemma has_integral_alt:
   1.185 +  "(f has_integral y) i \<longleftrightarrow>
   1.186 +    (if \<exists>a b. i = cbox a b
   1.187 +     then (f has_integral y) i
   1.188 +     else (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.189 +      (\<exists>z. ((\<lambda>x. if x \<in> i then f x else 0) has_integral z) (cbox a b) \<and> norm (z - y) < e)))"
   1.190 +  by (subst has_integral_def) (auto simp add: has_integral_cbox)
   1.191 +
   1.192 +lemma has_integral_altD:
   1.193 +  assumes "(f has_integral y) i"
   1.194 +    and "\<not> (\<exists>a b. i = cbox a b)"
   1.195 +    and "e>0"
   1.196 +  obtains B where "B > 0"
   1.197 +    and "\<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
   1.198 +      (\<exists>z. ((\<lambda>x. if x \<in> i then f(x) else 0) has_integral z) (cbox a b) \<and> norm(z - y) < e)"
   1.199 +  using assms has_integral_alt[of f y i] by auto
   1.200 +
   1.201 +definition integrable_on (infixr "integrable'_on" 46)
   1.202 +  where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
   1.203 +
   1.204 +definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
   1.205 +
   1.206 +lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
   1.207 +  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
   1.208 +
   1.209 +lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
   1.210 +  unfolding integrable_on_def integral_def by blast
   1.211 +
   1.212 +lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
   1.213 +  unfolding integrable_on_def by auto
   1.214 +
   1.215 +lemma has_integral_integral: "f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
   1.216 +  by auto
   1.217 +
   1.218 +lemma setsum_content_null:
   1.219 +  assumes "content (cbox a b) = 0"
   1.220 +    and "p tagged_division_of (cbox a b)"
   1.221 +  shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
   1.222 +proof (rule setsum.neutral, rule)
   1.223 +  fix y
   1.224 +  assume y: "y \<in> p"
   1.225 +  obtain x k where xk: "y = (x, k)"
   1.226 +    using surj_pair[of y] by blast
   1.227 +  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
   1.228 +  from this(2) obtain c d where k: "k = cbox c d" by blast
   1.229 +  have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
   1.230 +    unfolding xk by auto
   1.231 +  also have "\<dots> = 0"
   1.232 +    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
   1.233 +    unfolding assms(1) k
   1.234 +    by auto
   1.235 +  finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
   1.236 +qed
   1.237 +
   1.238  subsection \<open>Basic theorems about integrals.\<close>
   1.239  
   1.240  lemma has_integral_unique:
   1.241 @@ -2433,40 +2453,9 @@
   1.242    assume as: "k1 \<noteq> k2"
   1.243    then have e: "?e > 0"
   1.244      by auto
   1.245 -  have lem: False
   1.246 -    if f_k1: "(f has_integral k1) (cbox a b)"
   1.247 -    and f_k2: "(f has_integral k2) (cbox a b)"
   1.248 -    and "k1 \<noteq> k2"
   1.249 +  have lem: "(f has_integral k1) (cbox a b) \<Longrightarrow> (f has_integral k2) (cbox a b) \<Longrightarrow> k1 = k2"
   1.250      for f :: "'n \<Rightarrow> 'a" and a b k1 k2
   1.251 -  proof -
   1.252 -    let ?e = "norm (k1 - k2) / 2"
   1.253 -    from \<open>k1 \<noteq> k2\<close> have e: "?e > 0" by auto
   1.254 -    obtain d1 where d1:
   1.255 -        "gauge d1"
   1.256 -        "\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
   1.257 -          d1 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k1) < norm (k1 - k2) / 2"
   1.258 -      by (rule has_integralD[OF f_k1 e]) blast
   1.259 -    obtain d2 where d2:
   1.260 -        "gauge d2"
   1.261 -        "\<And>p. p tagged_division_of cbox a b \<Longrightarrow>
   1.262 -          d2 fine p \<Longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k2) < norm (k1 - k2) / 2"
   1.263 -      by (rule has_integralD[OF f_k2 e]) blast
   1.264 -    obtain p where p:
   1.265 -        "p tagged_division_of cbox a b"
   1.266 -        "(\<lambda>x. d1 x \<inter> d2 x) fine p"
   1.267 -      by (rule fine_division_exists[OF gauge_inter[OF d1(1) d2(1)]])
   1.268 -    let ?c = "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
   1.269 -    have "norm (k1 - k2) \<le> norm (?c - k2) + norm (?c - k1)"
   1.270 -      using norm_triangle_ineq4[of "k1 - ?c" "k2 - ?c"]
   1.271 -      by (auto simp add:algebra_simps norm_minus_commute)
   1.272 -    also have "\<dots> < norm (k1 - k2) / 2 + norm (k1 - k2) / 2"
   1.273 -      apply (rule add_strict_mono)
   1.274 -      apply (rule_tac[!] d2(2) d1(2))
   1.275 -      using p unfolding fine_def
   1.276 -      apply auto
   1.277 -      done
   1.278 -    finally show False by auto
   1.279 -  qed
   1.280 +    by (auto simp: has_integral_cbox intro: tendsto_unique[OF division_filter_not_empty])
   1.281    {
   1.282      presume "\<not> (\<exists>a b. i = cbox a b) \<Longrightarrow> False"
   1.283      then show False
   1.284 @@ -2522,40 +2511,40 @@
   1.285    apply (rule someI_ex)
   1.286    by blast
   1.287  
   1.288 +
   1.289 +lemma has_integral_const [intro]:
   1.290 +  fixes a b :: "'a::euclidean_space"
   1.291 +  shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
   1.292 +  using eventually_division_filter_tagged_division[of "cbox a b"]
   1.293 +     additive_content_tagged_division[of _ a b]
   1.294 +  by (auto simp: has_integral_cbox split_beta' scaleR_setsum_left[symmetric]
   1.295 +           elim!: eventually_mono intro!: tendsto_cong[THEN iffD1, OF _ tendsto_const])
   1.296 +
   1.297 +lemma has_integral_const_real [intro]:
   1.298 +  fixes a b :: real
   1.299 +  shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}"
   1.300 +  by (metis box_real(2) has_integral_const)
   1.301 +
   1.302 +lemma integral_const [simp]:
   1.303 +  fixes a b :: "'a::euclidean_space"
   1.304 +  shows "integral (cbox a b) (\<lambda>x. c) = content (cbox a b) *\<^sub>R c"
   1.305 +  by (rule integral_unique) (rule has_integral_const)
   1.306 +
   1.307 +lemma integral_const_real [simp]:
   1.308 +  fixes a b :: real
   1.309 +  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
   1.310 +  by (metis box_real(2) integral_const)
   1.311 +
   1.312  lemma has_integral_is_0:
   1.313    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   1.314    assumes "\<forall>x\<in>s. f x = 0"
   1.315    shows "(f has_integral 0) s"
   1.316  proof -
   1.317 -  have lem: "\<And>a b. \<And>f::'n \<Rightarrow> 'a.
   1.318 -    (\<forall>x\<in>cbox a b. f(x) = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)"
   1.319 -    unfolding has_integral
   1.320 -  proof clarify
   1.321 -    fix a b e
   1.322 -    fix f :: "'n \<Rightarrow> 'a"
   1.323 -    assume as: "\<forall>x\<in>cbox a b. f x = 0" "0 < (e::real)"
   1.324 -    have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
   1.325 -      if p: "p tagged_division_of cbox a b" for p
   1.326 -    proof -
   1.327 -      have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) = 0"
   1.328 -      proof (rule setsum.neutral, rule)
   1.329 -        fix x
   1.330 -        assume x: "x \<in> p"
   1.331 -        have "f (fst x) = 0"
   1.332 -          using tagged_division_ofD(2-3)[OF p, of "fst x" "snd x"] using as x by auto
   1.333 -        then show "(\<lambda>(x, k). content k *\<^sub>R f x) x = 0"
   1.334 -          apply (subst surjective_pairing[of x])
   1.335 -          unfolding split_conv
   1.336 -          apply auto
   1.337 -          done
   1.338 -      qed
   1.339 -      then show ?thesis
   1.340 -        using as by auto
   1.341 -    qed
   1.342 -    then show "\<exists>d. gauge d \<and>
   1.343 -        (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e)"
   1.344 -      by auto
   1.345 -  qed
   1.346 +  have lem: "(\<forall>x\<in>cbox a b. f x = 0) \<Longrightarrow> (f has_integral 0) (cbox a b)" for a  b and f :: "'n \<Rightarrow> 'a"
   1.347 +    unfolding has_integral_cbox
   1.348 +    using eventually_division_filter_tagged_division[of "cbox a b"]
   1.349 +    by (subst tendsto_cong[where g="\<lambda>_. 0"])
   1.350 +       (auto elim!: eventually_mono intro!: setsum.neutral simp: tag_in_interval)
   1.351    {
   1.352      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
   1.353      with assms lem show ?thesis
   1.354 @@ -2588,40 +2577,8 @@
   1.355      using assms(2) .
   1.356    from pos_bounded obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
   1.357      by blast
   1.358 -  have lem: "\<And>(f :: 'n \<Rightarrow> 'a) y a b.
   1.359 -    (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
   1.360 -    unfolding has_integral
   1.361 -  proof (clarify, goal_cases)
   1.362 -    case prems: (1 f y a b e)
   1.363 -    from pos_bounded
   1.364 -    obtain B where B: "0 < B" "\<And>x. norm (h x) \<le> norm x * B"
   1.365 -      by blast
   1.366 -    have "e / B > 0" using prems(2) B by simp
   1.367 -    then obtain g
   1.368 -      where g: "gauge g"
   1.369 -               "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> g fine p \<Longrightarrow>
   1.370 -                    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - y) < e / B"
   1.371 -        using prems(1) by auto
   1.372 -    {
   1.373 -      fix p
   1.374 -      assume as: "p tagged_division_of (cbox a b)" "g fine p"
   1.375 -      have hc: "\<And>x k. h ((\<lambda>(x, k). content k *\<^sub>R f x) x) = (\<lambda>(x, k). h (content k *\<^sub>R f x)) x"
   1.376 -        by auto
   1.377 -      then have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = setsum (h \<circ> (\<lambda>(x, k). content k *\<^sub>R f x)) p"
   1.378 -        unfolding o_def unfolding scaleR[symmetric] hc by simp
   1.379 -      also have "\<dots> = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)"
   1.380 -        using setsum[of "\<lambda>(x,k). content k *\<^sub>R f x" p] using as by auto
   1.381 -      finally have "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) = h (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x)" .
   1.382 -      then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (h \<circ> f) x) - h y) < e"
   1.383 -        apply (simp add: diff[symmetric])
   1.384 -        apply (rule le_less_trans[OF B(2)])
   1.385 -        using g(2)[OF as] B(1)
   1.386 -        apply (auto simp add: field_simps)
   1.387 -        done
   1.388 -    }
   1.389 -    with g show ?case
   1.390 -      by (rule_tac x=g in exI) auto
   1.391 -  qed
   1.392 +  have lem: "\<And>a b y f::'n\<Rightarrow>'a. (f has_integral y) (cbox a b) \<Longrightarrow> ((h \<circ> f) has_integral h y) (cbox a b)"
   1.393 +    unfolding has_integral_cbox by (drule tendsto) (simp add: setsum scaleR split_beta')
   1.394    {
   1.395      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
   1.396      then show ?thesis
   1.397 @@ -2650,7 +2607,7 @@
   1.398          using zero by auto
   1.399        show ?case
   1.400          apply (rule_tac x="h z" in exI)
   1.401 -        apply (simp add: * lem z(1))
   1.402 +        apply (simp add: * lem[OF z(1)])
   1.403          apply (metis B diff le_less_trans pos_less_divide_eq z(2))
   1.404          done
   1.405      qed
   1.406 @@ -2723,49 +2680,11 @@
   1.407      and "(g has_integral l) s"
   1.408    shows "((\<lambda>x. f x + g x) has_integral (k + l)) s"
   1.409  proof -
   1.410 -  have lem: "((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
   1.411 -    if f_k: "(f has_integral k) (cbox a b)"
   1.412 -    and g_l: "(g has_integral l) (cbox a b)"
   1.413 +  have lem: "(f has_integral k) (cbox a b) \<Longrightarrow> (g has_integral l) (cbox a b) \<Longrightarrow>
   1.414 +    ((\<lambda>x. f x + g x) has_integral (k + l)) (cbox a b)"
   1.415      for f :: "'n \<Rightarrow> 'a" and g a b k l
   1.416 -    unfolding has_integral
   1.417 -  proof clarify
   1.418 -    fix e :: real
   1.419 -    assume e: "e > 0"
   1.420 -    then have *: "e / 2 > 0"
   1.421 -      by auto
   1.422 -    obtain d1 where d1:
   1.423 -      "gauge d1"
   1.424 -      "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d1 fine p \<Longrightarrow>
   1.425 -        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) < e / 2"
   1.426 -      using has_integralD[OF f_k *] by blast
   1.427 -    obtain d2 where d2:
   1.428 -      "gauge d2"
   1.429 -      "\<And>p. p tagged_division_of (cbox a b) \<Longrightarrow> d2 fine p \<Longrightarrow>
   1.430 -        norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l) < e / 2"
   1.431 -      using has_integralD[OF g_l *] by blast
   1.432 -    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
   1.433 -              norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e)"
   1.434 -    proof (rule exI [where x="\<lambda>x. (d1 x) \<inter> (d2 x)"], clarsimp simp add: gauge_inter[OF d1(1) d2(1)])
   1.435 -      fix p
   1.436 -      assume as: "p tagged_division_of (cbox a b)" "(\<lambda>x. d1 x \<inter> d2 x) fine p"
   1.437 -      have *: "(\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) =
   1.438 -        (\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>p. content k *\<^sub>R g x)"
   1.439 -        unfolding scaleR_right_distrib setsum.distrib[of "\<lambda>(x,k). content k *\<^sub>R f x" "\<lambda>(x,k). content k *\<^sub>R g x" p,symmetric]
   1.440 -        by (rule setsum.cong) auto
   1.441 -      from as have fine: "d1 fine p" "d2 fine p"
   1.442 -        unfolding fine_inter by auto
   1.443 -      have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) =
   1.444 -            norm (((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k) + ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - l))"
   1.445 -        unfolding * by (auto simp add: algebra_simps)
   1.446 -      also have "\<dots> < e/2 + e/2"
   1.447 -        apply (rule le_less_trans[OF norm_triangle_ineq])
   1.448 -        using as d1 d2 fine
   1.449 -        apply (blast intro: add_strict_mono)
   1.450 -        done
   1.451 -      finally show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f x + g x)) - (k + l)) < e"
   1.452 -        by auto
   1.453 -    qed
   1.454 -  qed
   1.455 +    unfolding has_integral_cbox
   1.456 +    by (simp add: split_beta' scaleR_add_right setsum.distrib[abs_def] tendsto_add)
   1.457    {
   1.458      presume "\<not> (\<exists>a b. s = cbox a b) \<Longrightarrow> ?thesis"
   1.459      then show ?thesis
   1.460 @@ -2991,32 +2910,13 @@
   1.461    shows "(\<lambda>x. f x / of_real c) integrable_on s \<longleftrightarrow> f integrable_on s"
   1.462  by (simp add: divide_inverse assms of_real_inverse [symmetric] del: of_real_inverse)
   1.463  
   1.464 -lemma has_integral_null [intro]:
   1.465 -  assumes "content(cbox a b) = 0"
   1.466 -  shows "(f has_integral 0) (cbox a b)"
   1.467 -proof -
   1.468 -  have "gauge (\<lambda>x. ball x 1)"
   1.469 -    by auto
   1.470 -  moreover
   1.471 -  {
   1.472 -    fix e :: real
   1.473 -    fix p
   1.474 -    assume e: "e > 0"
   1.475 -    assume p: "p tagged_division_of (cbox a b)"
   1.476 -    have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) = 0"
   1.477 -      unfolding norm_eq_zero diff_0_right
   1.478 -      using setsum_content_null[OF assms(1) p, of f] .
   1.479 -    then have "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - 0) < e"
   1.480 -      using e by auto
   1.481 -  }
   1.482 -  ultimately show ?thesis
   1.483 -    by (auto simp: has_integral)
   1.484 -qed
   1.485 -
   1.486 -lemma has_integral_null_real [intro]:
   1.487 -  assumes "content {a .. b::real} = 0"
   1.488 -  shows "(f has_integral 0) {a .. b}"
   1.489 -  by (metis assms box_real(2) has_integral_null)
   1.490 +lemma has_integral_null [intro]: "content(cbox a b) = 0 \<Longrightarrow> (f has_integral 0) (cbox a b)"
   1.491 +  unfolding has_integral_cbox
   1.492 +  using eventually_division_filter_tagged_division[of "cbox a b"]
   1.493 +  by (subst tendsto_cong[where g="\<lambda>_. 0"]) (auto elim: eventually_mono intro: setsum_content_null)
   1.494 +
   1.495 +lemma has_integral_null_real [intro]: "content {a .. b::real} = 0 \<Longrightarrow> (f has_integral 0) {a .. b}"
   1.496 +  by (metis box_real(2) has_integral_null)
   1.497  
   1.498  lemma has_integral_null_eq[simp]: "content (cbox a b) = 0 \<Longrightarrow> (f has_integral i) (cbox a b) \<longleftrightarrow> i = 0"
   1.499    by (auto simp add: has_integral_null dest!: integral_unique)
   1.500 @@ -3154,11 +3054,10 @@
   1.501  lemma integrable_cauchy:
   1.502    fixes f :: "'n::euclidean_space \<Rightarrow> 'a::{real_normed_vector,complete_space}"
   1.503    shows "f integrable_on cbox a b \<longleftrightarrow>
   1.504 -    (\<forall>e>0.\<exists>d. gauge d \<and>
   1.505 +    (\<forall>e>0. \<exists>d. gauge d \<and>
   1.506        (\<forall>p1 p2. p1 tagged_division_of (cbox a b) \<and> d fine p1 \<and>
   1.507          p2 tagged_division_of (cbox a b) \<and> d fine p2 \<longrightarrow>
   1.508 -        norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p1 -
   1.509 -        setsum (\<lambda>(x,k). content k *\<^sub>R f x) p2) < e))"
   1.510 +        norm ((\<Sum>(x,k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x,k)\<in>p2. content k *\<^sub>R f x)) < e))"
   1.511    (is "?l = (\<forall>e>0. \<exists>d. ?P e d)")
   1.512  proof
   1.513    assume ?l
   1.514 @@ -3707,33 +3606,6 @@
   1.515    qed
   1.516  qed
   1.517  
   1.518 -subsection \<open>Finally, the integral of a constant\<close>
   1.519 -
   1.520 -lemma has_integral_const [intro]:
   1.521 -  fixes a b :: "'a::euclidean_space"
   1.522 -  shows "((\<lambda>x. c) has_integral (content (cbox a b) *\<^sub>R c)) (cbox a b)"
   1.523 -  apply (auto intro!: exI [where x="\<lambda>x. ball x 1"] simp: split_def has_integral)
   1.524 -  apply (subst scaleR_left.setsum[symmetric, unfolded o_def])
   1.525 -  apply (subst additive_content_tagged_division[unfolded split_def])
   1.526 -  apply auto
   1.527 -  done
   1.528 -
   1.529 -lemma has_integral_const_real [intro]:
   1.530 -  fixes a b :: real
   1.531 -  shows "((\<lambda>x. c) has_integral (content {a .. b} *\<^sub>R c)) {a .. b}"
   1.532 -  by (metis box_real(2) has_integral_const)
   1.533 -
   1.534 -lemma integral_const [simp]:
   1.535 -  fixes a b :: "'a::euclidean_space"
   1.536 -  shows "integral (cbox a b) (\<lambda>x. c) = content (cbox a b) *\<^sub>R c"
   1.537 -  by (rule integral_unique) (rule has_integral_const)
   1.538 -
   1.539 -lemma integral_const_real [simp]:
   1.540 -  fixes a b :: real
   1.541 -  shows "integral {a .. b} (\<lambda>x. c) = content {a .. b} *\<^sub>R c"
   1.542 -  by (metis box_real(2) integral_const)
   1.543 -
   1.544 -
   1.545  subsection \<open>Bounds on the norm of Riemann sums and the integral itself.\<close>
   1.546  
   1.547  lemma dsum_bound:
   1.548 @@ -3807,7 +3679,7 @@
   1.549  lemma has_integral_bound:
   1.550    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   1.551    assumes "0 \<le> B"
   1.552 -      and "(f has_integral i) (cbox a b)"
   1.553 +      and *: "(f has_integral i) (cbox a b)"
   1.554        and "\<forall>x\<in>cbox a b. norm (f x) \<le> B"
   1.555      shows "norm i \<le> B * content (cbox a b)"
   1.556  proof (rule ccontr)
   1.557 @@ -5892,7 +5764,7 @@
   1.558      and "\<forall>x. g(h x) = x"
   1.559      and contg: "\<And>x. continuous (at x) g"
   1.560      and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
   1.561 -    and "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
   1.562 +    and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
   1.563      and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
   1.564      and "(f has_integral i) (cbox a b)"
   1.565    shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
   1.566 @@ -5924,12 +5796,10 @@
   1.567      apply(erule_tac x=y in allE)
   1.568      apply auto
   1.569      done
   1.570 +  from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
   1.571    show ?thesis
   1.572 -    unfolding has_integral_def has_integral_compact_interval_def
   1.573 -    apply (subst if_P)
   1.574 -    apply rule
   1.575 -    apply rule
   1.576 -    apply (rule wz)
   1.577 +    unfolding h_eq has_integral
   1.578 +    unfolding h_eq[symmetric]
   1.579    proof safe
   1.580      fix e :: real
   1.581      assume e: "e > 0"