src/HOL/ex/Gauge_Integration.thy
 author wenzelm Wed Jun 22 10:09:20 2016 +0200 (2016-06-22) changeset 63343 fb5d8a50c641 parent 63060 293ede07b775 child 63627 6ddb43c6b711 permissions -rw-r--r--
bundle lifting_syntax;
```     1 (*  Author:     Jacques D. Fleuriot, University of Edinburgh
```
```     2     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
```
```     3
```
```     4     Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
```
```     5 *)
```
```     6
```
```     7 section\<open>Theory of Integration on real intervals\<close>
```
```     8
```
```     9 theory Gauge_Integration
```
```    10 imports Complex_Main
```
```    11 begin
```
```    12
```
```    13 text \<open>
```
```    14
```
```    15 \textbf{Attention}: This theory defines the Integration on real
```
```    16 intervals.  This is just a example theory for historical / expository interests.
```
```    17 A better replacement is found in the Multivariate Analysis library. This defines
```
```    18 the gauge integral on real vector spaces and in the Real Integral theory
```
```    19 is a specialization to the integral on arbitrary real intervals.  The
```
```    20 Multivariate Analysis package also provides a better support for analysis on
```
```    21 integrals.
```
```    22
```
```    23 \<close>
```
```    24
```
```    25 text\<open>We follow John Harrison in formalizing the Gauge integral.\<close>
```
```    26
```
```    27 subsection \<open>Gauges\<close>
```
```    28
```
```    29 definition
```
```    30   gauge :: "[real set, real => real] => bool" where
```
```    31   "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
```
```    32
```
```    33
```
```    34 subsection \<open>Gauge-fine divisions\<close>
```
```    35
```
```    36 inductive
```
```    37   fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
```
```    38 for
```
```    39   \<delta> :: "real \<Rightarrow> real"
```
```    40 where
```
```    41   fine_Nil:
```
```    42     "fine \<delta> (a, a) []"
```
```    43 | fine_Cons:
```
```    44     "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
```
```    45       \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
```
```    46
```
```    47 lemmas fine_induct [induct set: fine] =
```
```    48   fine.induct [of "\<delta>" "(a,b)" "D" "case_prod P", unfolded split_conv] for \<delta> a b D P
```
```    49
```
```    50 lemma fine_single:
```
```    51   "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
```
```    52 by (rule fine_Cons [OF fine_Nil])
```
```    53
```
```    54 lemma fine_append:
```
```    55   "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
```
```    56 by (induct set: fine, simp, simp add: fine_Cons)
```
```    57
```
```    58 lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
```
```    59 by (induct set: fine, simp_all)
```
```    60
```
```    61 lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
```
```    62 apply (induct set: fine, simp)
```
```    63 apply (drule fine_imp_le, simp)
```
```    64 done
```
```    65
```
```    66 lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b"
```
```    67 by (auto elim: fine.cases intro: fine.intros)
```
```    68
```
```    69 lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []"
```
```    70 proof
```
```    71   assume "fine \<delta> (a, a) D" thus "D = []"
```
```    72     by (metis nonempty_fine_imp_less less_irrefl)
```
```    73 next
```
```    74   assume "D = []" thus "fine \<delta> (a, a) D"
```
```    75     by (simp add: fine_Nil)
```
```    76 qed
```
```    77
```
```    78 lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
```
```    79 by (simp add: fine_Nil_iff)
```
```    80
```
```    81 lemma mem_fine:
```
```    82   "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
```
```    83 by (induct set: fine, simp, force)
```
```    84
```
```    85 lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
```
```    86 apply (induct arbitrary: z u v set: fine, auto)
```
```    87 apply (simp add: fine_imp_le)
```
```    88 apply (erule order_trans [OF less_imp_le], simp)
```
```    89 done
```
```    90
```
```    91 lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
```
```    92 by (induct arbitrary: z u v set: fine) auto
```
```    93
```
```    94 lemma BOLZANO:
```
```    95   fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
```
```    96   assumes 1: "a \<le> b"
```
```    97   assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
```
```    98   assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
```
```    99   shows "P a b"
```
```   100   using 1 2 3 by (rule Bolzano)
```
```   101
```
```   102 text\<open>We can always find a division that is fine wrt any gauge\<close>
```
```   103
```
```   104 lemma fine_exists:
```
```   105   assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
```
```   106 proof -
```
```   107   {
```
```   108     fix u v :: real assume "u \<le> v"
```
```   109     have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
```
```   110       apply (induct u v rule: BOLZANO, rule \<open>u \<le> v\<close>)
```
```   111        apply (simp, fast intro: fine_append)
```
```   112       apply (case_tac "a \<le> x \<and> x \<le> b")
```
```   113        apply (rule_tac x="\<delta> x" in exI)
```
```   114        apply (rule conjI)
```
```   115         apply (simp add: \<open>gauge {a..b} \<delta>\<close> [unfolded gauge_def])
```
```   116        apply (clarify, rename_tac u v)
```
```   117        apply (case_tac "u = v")
```
```   118         apply (fast intro: fine_Nil)
```
```   119        apply (subgoal_tac "u < v", fast intro: fine_single, simp)
```
```   120       apply (rule_tac x="1" in exI, clarsimp)
```
```   121       done
```
```   122   }
```
```   123   with \<open>a \<le> b\<close> show ?thesis by auto
```
```   124 qed
```
```   125
```
```   126 lemma fine_covers_all:
```
```   127   assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
```
```   128   shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
```
```   129   using assms
```
```   130 proof (induct set: fine)
```
```   131   case (2 b c D a t)
```
```   132   thus ?case
```
```   133   proof (cases "b < x")
```
```   134     case True
```
```   135     with 2 obtain N where *: "N < length D"
```
```   136       and **: "D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" for d t e by auto
```
```   137     hence "Suc N < length ((a,t,b)#D) \<and>
```
```   138            (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
```
```   139     thus ?thesis by auto
```
```   140   next
```
```   141     case False with 2
```
```   142     have "0 < length ((a,t,b)#D) \<and>
```
```   143            (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
```
```   144     thus ?thesis by auto
```
```   145   qed
```
```   146 qed auto
```
```   147
```
```   148 lemma fine_append_split:
```
```   149   assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
```
```   150   shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
```
```   151   and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
```
```   152 proof -
```
```   153   from assms
```
```   154   have "?fine1 \<and> ?fine2"
```
```   155   proof (induct arbitrary: D1 D2)
```
```   156     case (2 b c D a' x D1 D2)
```
```   157     note induct = this
```
```   158
```
```   159     thus ?case
```
```   160     proof (cases D1)
```
```   161       case Nil
```
```   162       hence "fst (hd D2) = a'" using 2 by auto
```
```   163       with fine_Cons[OF \<open>fine \<delta> (b,c) D\<close> induct(3,4,5)] Nil induct
```
```   164       show ?thesis by (auto intro: fine_Nil)
```
```   165     next
```
```   166       case (Cons d1 D1')
```
```   167       with induct(2)[OF \<open>D2 \<noteq> []\<close>, of D1'] induct(8)
```
```   168       have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
```
```   169         "d1 = (a', x, b)" by auto
```
```   170       with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
```
```   171       show ?thesis by auto
```
```   172     qed
```
```   173   qed auto
```
```   174   thus ?fine1 and ?fine2 by auto
```
```   175 qed
```
```   176
```
```   177 lemma fine_\<delta>_expand:
```
```   178   assumes "fine \<delta> (a,b) D"
```
```   179   and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x"
```
```   180   shows "fine \<delta>' (a,b) D"
```
```   181 using assms proof induct
```
```   182   case 1 show ?case by (rule fine_Nil)
```
```   183 next
```
```   184   case (2 b c D a x)
```
```   185   show ?case
```
```   186   proof (rule fine_Cons)
```
```   187     show "fine \<delta>' (b,c) D" using 2 by auto
```
```   188     from fine_imp_le[OF 2(1)] 2(6) \<open>x \<le> b\<close>
```
```   189     show "b - a < \<delta>' x"
```
```   190       using 2(7)[OF \<open>a \<le> x\<close>] by auto
```
```   191   qed (auto simp add: 2)
```
```   192 qed
```
```   193
```
```   194 lemma fine_single_boundaries:
```
```   195   assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
```
```   196   shows "a = d \<and> b = e"
```
```   197 using assms proof induct
```
```   198   case (2 b c  D a x)
```
```   199   hence "D = []" and "a = d" and "b = e" by auto
```
```   200   moreover
```
```   201   from \<open>fine \<delta> (b,c) D\<close> \<open>D = []\<close> have "b = c"
```
```   202     by (rule empty_fine_imp_eq)
```
```   203   ultimately show ?case by simp
```
```   204 qed auto
```
```   205
```
```   206 lemma fine_listsum_eq_diff:
```
```   207   fixes f :: "real \<Rightarrow> real"
```
```   208   shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
```
```   209 by (induct set: fine) simp_all
```
```   210
```
```   211 text\<open>Lemmas about combining gauges\<close>
```
```   212
```
```   213 lemma gauge_min:
```
```   214      "[| gauge(E) g1; gauge(E) g2 |]
```
```   215       ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
```
```   216 by (simp add: gauge_def)
```
```   217
```
```   218 lemma fine_min:
```
```   219       "fine (%x. min (g1(x)) (g2(x))) (a,b) D
```
```   220        ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
```
```   221 apply (erule fine.induct)
```
```   222 apply (simp add: fine_Nil)
```
```   223 apply (simp add: fine_Cons)
```
```   224 done
```
```   225
```
```   226 subsection \<open>Riemann sum\<close>
```
```   227
```
```   228 definition
```
```   229   rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
```
```   230   "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
```
```   231
```
```   232 lemma rsum_Nil [simp]: "rsum [] f = 0"
```
```   233 unfolding rsum_def by simp
```
```   234
```
```   235 lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
```
```   236 unfolding rsum_def by simp
```
```   237
```
```   238 lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
```
```   239 by (induct D, auto)
```
```   240
```
```   241 lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
```
```   242 by (induct D, auto simp add: algebra_simps)
```
```   243
```
```   244 lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
```
```   245 by (induct D, auto simp add: algebra_simps)
```
```   246
```
```   247 lemma rsum_add: "rsum D (\<lambda>x. f x + g x) =  rsum D f + rsum D g"
```
```   248 by (induct D, auto simp add: algebra_simps)
```
```   249
```
```   250 lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
```
```   251 unfolding rsum_def map_append listsum_append ..
```
```   252
```
```   253
```
```   254 subsection \<open>Gauge integrability (definite)\<close>
```
```   255
```
```   256 definition
```
```   257   Integral :: "[(real*real),real=>real,real] => bool" where
```
```   258   "Integral = (%(a,b) f k. \<forall>e > 0.
```
```   259                                (\<exists>\<delta>. gauge {a .. b} \<delta> &
```
```   260                                (\<forall>D. fine \<delta> (a,b) D -->
```
```   261                                          \<bar>rsum D f - k\<bar> < e)))"
```
```   262
```
```   263 lemma Integral_eq:
```
```   264   "Integral (a, b) f k \<longleftrightarrow>
```
```   265     (\<forall>e>0. \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a,b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e))"
```
```   266 unfolding Integral_def by simp
```
```   267
```
```   268 lemma IntegralI:
```
```   269   assumes "\<And>e. 0 < e \<Longrightarrow>
```
```   270     \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e)"
```
```   271   shows "Integral (a, b) f k"
```
```   272 using assms unfolding Integral_def by auto
```
```   273
```
```   274 lemma IntegralE:
```
```   275   assumes "Integral (a, b) f k" and "0 < e"
```
```   276   obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e"
```
```   277 using assms unfolding Integral_def by auto
```
```   278
```
```   279 lemma Integral_def2:
```
```   280   "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
```
```   281                                (\<forall>D. fine \<delta> (a,b) D -->
```
```   282                                          \<bar>rsum D f - k\<bar> \<le> e)))"
```
```   283 unfolding Integral_def
```
```   284 apply (safe intro!: ext)
```
```   285 apply (fast intro: less_imp_le)
```
```   286 apply (drule_tac x="e/2" in spec)
```
```   287 apply force
```
```   288 done
```
```   289
```
```   290 text\<open>The integral is unique if it exists\<close>
```
```   291
```
```   292 lemma Integral_unique:
```
```   293   assumes le: "a \<le> b"
```
```   294   assumes 1: "Integral (a, b) f k1"
```
```   295   assumes 2: "Integral (a, b) f k2"
```
```   296   shows "k1 = k2"
```
```   297 proof (rule ccontr)
```
```   298   assume "k1 \<noteq> k2"
```
```   299   hence e: "0 < \<bar>k1 - k2\<bar> / 2" by simp
```
```   300   obtain d1 where "gauge {a..b} d1" and
```
```   301     d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2"
```
```   302     using 1 e by (rule IntegralE)
```
```   303   obtain d2 where "gauge {a..b} d2" and
```
```   304     d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
```
```   305     using 2 e by (rule IntegralE)
```
```   306   have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))"
```
```   307     using \<open>gauge {a..b} d1\<close> and \<open>gauge {a..b} d2\<close>
```
```   308     by (rule gauge_min)
```
```   309   then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D"
```
```   310     using fine_exists [OF le] by fast
```
```   311   hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
```
```   312     by (auto dest: fine_min)
```
```   313   hence "\<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2" and "\<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
```
```   314     using d1 d2 by simp_all
```
```   315   hence "\<bar>rsum D f - k1\<bar> + \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2 + \<bar>k1 - k2\<bar> / 2"
```
```   316     by (rule add_strict_mono)
```
```   317   thus False by auto
```
```   318 qed
```
```   319
```
```   320 lemma Integral_zero: "Integral(a,a) f 0"
```
```   321 apply (rule IntegralI)
```
```   322 apply (rule_tac x = "\<lambda>x. 1" in exI)
```
```   323 apply (simp add: fine_same_iff gauge_def)
```
```   324 done
```
```   325
```
```   326 lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0"
```
```   327   by (auto intro: Integral_zero Integral_unique)
```
```   328
```
```   329 lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0"
```
```   330 apply (rule IntegralI)
```
```   331 apply (rule_tac x="\<lambda>x. 1" in exI, simp add: gauge_def)
```
```   332 done
```
```   333
```
```   334 lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
```
```   335 unfolding rsum_def
```
```   336 by (induct set: fine, auto simp add: algebra_simps)
```
```   337
```
```   338 lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. c) (c * (b - a))"
```
```   339 apply (cases "a = b", simp)
```
```   340 apply (rule IntegralI)
```
```   341 apply (rule_tac x = "\<lambda>x. b - a" in exI)
```
```   342 apply (rule conjI, simp add: gauge_def)
```
```   343 apply (clarify)
```
```   344 apply (subst fine_rsum_const, assumption, simp)
```
```   345 done
```
```   346
```
```   347 lemma Integral_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b - a)"
```
```   348   using Integral_mult_const [of a b 1] by simp
```
```   349
```
```   350 lemma Integral_mult:
```
```   351      "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
```
```   352 apply (auto simp add: order_le_less)
```
```   353 apply (cases "c = 0", simp add: Integral_zero_fun)
```
```   354 apply (rule IntegralI)
```
```   355 apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp)
```
```   356 apply (rule_tac x="\<delta>" in exI, clarify)
```
```   357 apply (drule_tac x="D" in spec, clarify)
```
```   358 apply (simp add: pos_less_divide_eq abs_mult [symmetric]
```
```   359                  algebra_simps rsum_right_distrib)
```
```   360 done
```
```   361
```
```   362 lemma Integral_add:
```
```   363   assumes "Integral (a, b) f x1"
```
```   364   assumes "Integral (b, c) f x2"
```
```   365   assumes "a \<le> b" and "b \<le> c"
```
```   366   shows "Integral (a, c) f (x1 + x2)"
```
```   367 proof (cases "a < b \<and> b < c", rule IntegralI)
```
```   368   fix \<epsilon> :: real assume "0 < \<epsilon>"
```
```   369   hence "0 < \<epsilon> / 2" by auto
```
```   370
```
```   371   assume "a < b \<and> b < c"
```
```   372   hence "a < b" and "b < c" by auto
```
```   373
```
```   374   obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
```
```   375     and I1: "fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" for D
```
```   376     using IntegralE [OF \<open>Integral (a, b) f x1\<close> \<open>0 < \<epsilon>/2\<close>] by auto
```
```   377
```
```   378   obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
```
```   379     and I2: "fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" for D
```
```   380     using IntegralE [OF \<open>Integral (b, c) f x2\<close> \<open>0 < \<epsilon>/2\<close>] by auto
```
```   381
```
```   382   define \<delta> where "\<delta> x =
```
```   383     (if x < b then min (\<delta>1 x) (b - x)
```
```   384      else if x = b then min (\<delta>1 b) (\<delta>2 b)
```
```   385      else min (\<delta>2 x) (x - b))" for x
```
```   386
```
```   387   have "gauge {a..c} \<delta>"
```
```   388     using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
```
```   389
```
```   390   moreover {
```
```   391     fix D :: "(real \<times> real \<times> real) list"
```
```   392     assume fine: "fine \<delta> (a,c) D"
```
```   393     from fine_covers_all[OF this \<open>a < b\<close> \<open>b \<le> c\<close>]
```
```   394     obtain N where "N < length D"
```
```   395       and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
```
```   396       by auto
```
```   397     obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
```
```   398     with * have "d < b" and "b \<le> e" by auto
```
```   399     have in_D: "(d, t, e) \<in> set D"
```
```   400       using D_eq[symmetric] using \<open>N < length D\<close> by auto
```
```   401
```
```   402     from mem_fine[OF fine in_D]
```
```   403     have "d < e" and "d \<le> t" and "t \<le> e" by auto
```
```   404
```
```   405     have "t = b"
```
```   406     proof (rule ccontr)
```
```   407       assume "t \<noteq> b"
```
```   408       with mem_fine3[OF fine in_D] \<open>b \<le> e\<close> \<open>d \<le> t\<close> \<open>t \<le> e\<close> \<open>d < b\<close> \<delta>_def
```
```   409       show False by (cases "t < b") auto
```
```   410     qed
```
```   411
```
```   412     let ?D1 = "take N D"
```
```   413     let ?D2 = "drop N D"
```
```   414     define D1 where "D1 = take N D @ [(d, t, b)]"
```
```   415     define D2 where "D2 = (if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
```
```   416
```
```   417     from hd_drop_conv_nth[OF \<open>N < length D\<close>]
```
```   418     have "fst (hd ?D2) = d" using \<open>D ! N = (d, t, e)\<close> by auto
```
```   419     with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
```
```   420     have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
```
```   421       using \<open>N < length D\<close> fine by auto
```
```   422
```
```   423     have "fine \<delta>1 (a,b) D1" unfolding D1_def
```
```   424     proof (rule fine_append)
```
```   425       show "fine \<delta>1 (a, d) ?D1"
```
```   426       proof (rule fine1[THEN fine_\<delta>_expand])
```
```   427         fix x assume "a \<le> x" "x \<le> d"
```
```   428         hence "x \<le> b" using \<open>d < b\<close> \<open>x \<le> d\<close> by auto
```
```   429         thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
```
```   430       qed
```
```   431
```
```   432       have "b - d < \<delta>1 t"
```
```   433         using mem_fine3[OF fine in_D] \<delta>_def \<open>b \<le> e\<close> \<open>t = b\<close> by auto
```
```   434       from \<open>d < b\<close> \<open>d \<le> t\<close> \<open>t = b\<close> this
```
```   435       show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
```
```   436     qed
```
```   437     note rsum1 = I1[OF this]
```
```   438
```
```   439     have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
```
```   440       using Cons_nth_drop_Suc[OF \<open>N < length D\<close>] by simp
```
```   441
```
```   442     have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
```
```   443     proof (cases "drop (Suc N) D = []")
```
```   444       case True
```
```   445       note * = fine2[simplified drop_split True D_eq append_Nil2]
```
```   446       have "e = c" using fine_single_boundaries[OF * refl] by auto
```
```   447       thus ?thesis unfolding True using fine_Nil by auto
```
```   448     next
```
```   449       case False
```
```   450       note * = fine_append_split[OF fine2 False drop_split]
```
```   451       from fine_single_boundaries[OF *(1)]
```
```   452       have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
```
```   453       with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
```
```   454       thus ?thesis
```
```   455       proof (rule fine_\<delta>_expand)
```
```   456         fix x assume "e \<le> x" and "x \<le> c"
```
```   457         thus "\<delta> x \<le> \<delta>2 x" using \<open>b \<le> e\<close> unfolding \<delta>_def by auto
```
```   458       qed
```
```   459     qed
```
```   460
```
```   461     have "fine \<delta>2 (b, c) D2"
```
```   462     proof (cases "e = b")
```
```   463       case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
```
```   464     next
```
```   465       case False
```
```   466       have "e - b < \<delta>2 b"
```
```   467         using mem_fine3[OF fine in_D] \<delta>_def \<open>d < b\<close> \<open>t = b\<close> by auto
```
```   468       with False \<open>t = b\<close> \<open>b \<le> e\<close>
```
```   469       show ?thesis using D2_def
```
```   470         by (auto intro!: fine_append[OF _ fine2] fine_single
```
```   471                simp del: append_Cons)
```
```   472     qed
```
```   473     note rsum2 = I2[OF this]
```
```   474
```
```   475     have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
```
```   476       using rsum_append[symmetric] Cons_nth_drop_Suc[OF \<open>N < length D\<close>] by auto
```
```   477     also have "\<dots> = rsum D1 f + rsum D2 f"
```
```   478       by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
```
```   479     finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
```
```   480       using add_strict_mono[OF rsum1 rsum2] by simp
```
```   481   }
```
```   482   ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
```
```   483     (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
```
```   484     by blast
```
```   485 next
```
```   486   case False
```
```   487   hence "a = b \<or> b = c" using \<open>a \<le> b\<close> and \<open>b \<le> c\<close> by auto
```
```   488   thus ?thesis
```
```   489   proof (rule disjE)
```
```   490     assume "a = b" hence "x1 = 0"
```
```   491       using \<open>Integral (a, b) f x1\<close> by simp
```
```   492     thus ?thesis using \<open>a = b\<close> \<open>Integral (b, c) f x2\<close> by simp
```
```   493   next
```
```   494     assume "b = c" hence "x2 = 0"
```
```   495       using \<open>Integral (b, c) f x2\<close> by simp
```
```   496     thus ?thesis using \<open>b = c\<close> \<open>Integral (a, b) f x1\<close> by simp
```
```   497   qed
```
```   498 qed
```
```   499
```
```   500 text\<open>Fundamental theorem of calculus (Part I)\<close>
```
```   501
```
```   502 text\<open>"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988\<close>
```
```   503
```
```   504 lemma strad1:
```
```   505   fixes z x s e :: real
```
```   506   assumes P: "(\<And>z. z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2)"
```
```   507   assumes "\<bar>z - x\<bar> < s"
```
```   508   shows "\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e / 2 * \<bar>z - x\<bar>"
```
```   509 proof (cases "z = x")
```
```   510   case True then show ?thesis by simp
```
```   511 next
```
```   512   case False
```
```   513   then have "inverse (z - x) * (f z - f x - f' x * (z - x)) = (f z - f x) / (z - x) - f' x"
```
```   514     apply (subst mult.commute)
```
```   515     apply (simp add: left_diff_distrib)
```
```   516     apply (simp add: mult.assoc divide_inverse)
```
```   517     apply (simp add: ring_distribs)
```
```   518     done
```
```   519   moreover from False \<open>\<bar>z - x\<bar> < s\<close> have "\<bar>(f z - f x) / (z - x) - f' x\<bar> < e / 2"
```
```   520     by (rule P)
```
```   521   ultimately have "\<bar>inverse (z - x)\<bar> * (\<bar>f z - f x - f' x * (z - x)\<bar> * 2)
```
```   522     \<le> \<bar>inverse (z - x)\<bar> * (e * \<bar>z - x\<bar>)"
```
```   523     using False by (simp del: abs_inverse add: abs_mult [symmetric] ac_simps)
```
```   524   with False have "\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
```
```   525     by simp
```
```   526   then show ?thesis by simp
```
```   527 qed
```
```   528
```
```   529 lemma lemma_straddle:
```
```   530   assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
```
```   531   shows "\<exists>g. gauge {a..b} g &
```
```   532                 (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
```
```   533                   --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
```
```   534 proof -
```
```   535   have "\<forall>x\<in>{a..b}.
```
```   536         (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
```
```   537                        \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
```
```   538   proof (clarsimp)
```
```   539     fix x :: real assume "a \<le> x" and "x \<le> b"
```
```   540     with f' have "DERIV f x :> f'(x)" by simp
```
```   541     then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
```
```   542       by (simp add: DERIV_iff2 LIM_eq)
```
```   543     with \<open>0 < e\<close> obtain s
```
```   544     where "z \<noteq> x \<Longrightarrow> \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s" for z
```
```   545       by (drule_tac x="e/2" in spec, auto)
```
```   546     with strad1 [of x s f f' e] have strad:
```
```   547         "\<And>z. \<bar>z - x\<bar> < s \<Longrightarrow> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
```
```   548       by auto
```
```   549     show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
```
```   550     proof (safe intro!: exI)
```
```   551       show "0 < s" by fact
```
```   552     next
```
```   553       fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
```
```   554       have "\<bar>f v - f u - f' x * (v - u)\<bar> =
```
```   555             \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
```
```   556         by (simp add: right_diff_distrib)
```
```   557       also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
```
```   558         by (rule abs_triangle_ineq)
```
```   559       also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
```
```   560         by (simp add: right_diff_distrib)
```
```   561       also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
```
```   562         using \<open>u \<le> x\<close> \<open>x \<le> v\<close> \<open>v - u < s\<close> by (intro add_mono strad, simp_all)
```
```   563       also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
```
```   564         using \<open>u \<le> x\<close> \<open>x \<le> v\<close> \<open>0 < e\<close> by (intro add_mono, simp_all)
```
```   565       also have "\<dots> = e * (v - u)"
```
```   566         by simp
```
```   567       finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
```
```   568     qed
```
```   569   qed
```
```   570   thus ?thesis
```
```   571     by (simp add: gauge_def) (drule bchoice, auto)
```
```   572 qed
```
```   573
```
```   574 lemma fundamental_theorem_of_calculus:
```
```   575   assumes "a \<le> b"
```
```   576   assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)"
```
```   577   shows "Integral (a, b) f' (f(b) - f(a))"
```
```   578 proof (cases "a = b")
```
```   579   assume "a = b" thus ?thesis by simp
```
```   580 next
```
```   581   assume "a \<noteq> b" with \<open>a \<le> b\<close> have "a < b" by simp
```
```   582   show ?thesis
```
```   583   proof (simp add: Integral_def2, clarify)
```
```   584     fix e :: real assume "0 < e"
```
```   585     with \<open>a < b\<close> have "0 < e / (b - a)" by simp
```
```   586
```
```   587     from lemma_straddle [OF f' this]
```
```   588     obtain \<delta> where "gauge {a..b} \<delta>"
```
```   589       and \<delta>: "\<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
```
```   590            \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" for x u v by auto
```
```   591
```
```   592     have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
```
```   593     proof (clarify)
```
```   594       fix D assume D: "fine \<delta> (a, b) D"
```
```   595       hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
```
```   596         by (rule fine_listsum_eq_diff)
```
```   597       hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
```
```   598         by simp
```
```   599       also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
```
```   600         by (rule abs_minus_commute)
```
```   601       also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
```
```   602         by (simp only: rsum_def listsum_subtractf split_def)
```
```   603       also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
```
```   604         by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
```
```   605       also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
```
```   606         apply (rule listsum_mono, clarify, rename_tac u x v)
```
```   607         using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
```
```   608         done
```
```   609       also have "\<dots> = e"
```
```   610         using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
```
```   611         unfolding split_def listsum_const_mult
```
```   612         using \<open>a < b\<close> by simp
```
```   613       finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
```
```   614     qed
```
```   615
```
```   616     with \<open>gauge {a..b} \<delta>\<close>
```
```   617     show "\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e)"
```
```   618       by auto
```
```   619   qed
```
```   620 qed
```
```   621
```
```   622 end
```