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