1 (* ID : $Id$ |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 2000 University of Edinburgh |
|
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
|
5 *) |
|
6 |
|
7 header{*Theory of Integration*} |
|
8 |
|
9 theory Integration |
|
10 imports MacLaurin |
|
11 begin |
|
12 |
|
13 text{*We follow John Harrison in formalizing the Gauge integral.*} |
|
14 |
|
15 definition |
|
16 --{*Partitions and tagged partitions etc.*} |
|
17 |
|
18 partition :: "[(real*real),nat => real] => bool" where |
|
19 [code del]: "partition = (%(a,b) D. D 0 = a & |
|
20 (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) & |
|
21 (\<forall>n \<ge> N. D(n) = b)))" |
|
22 |
|
23 definition |
|
24 psize :: "(nat => real) => nat" where |
|
25 [code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) & |
|
26 (\<forall>n \<ge> N. D(n) = D(N)))" |
|
27 |
|
28 definition |
|
29 tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where |
|
30 [code del]:"tpart = (%(a,b) (D,p). partition(a,b) D & |
|
31 (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))" |
|
32 |
|
33 --{*Gauges and gauge-fine divisions*} |
|
34 |
|
35 definition |
|
36 gauge :: "[real => bool, real => real] => bool" where |
|
37 [code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))" |
|
38 |
|
39 definition |
|
40 fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where |
|
41 [code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))" |
|
42 |
|
43 --{*Riemann sum*} |
|
44 |
|
45 definition |
|
46 rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where |
|
47 "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))" |
|
48 |
|
49 --{*Gauge integrability (definite)*} |
|
50 |
|
51 definition |
|
52 Integral :: "[(real*real),real=>real,real] => bool" where |
|
53 [code del]: "Integral = (%(a,b) f k. \<forall>e > 0. |
|
54 (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g & |
|
55 (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) --> |
|
56 \<bar>rsum(D,p) f - k\<bar> < e)))" |
|
57 |
|
58 |
|
59 lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0" |
|
60 by (auto simp add: psize_def) |
|
61 |
|
62 lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1" |
|
63 apply (simp add: psize_def) |
|
64 apply (rule some_equality, auto) |
|
65 apply (drule_tac x = 1 in spec, auto) |
|
66 done |
|
67 |
|
68 lemma partition_single [simp]: |
|
69 "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)" |
|
70 by (auto simp add: partition_def order_le_less) |
|
71 |
|
72 lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)" |
|
73 by (simp add: partition_def) |
|
74 |
|
75 lemma partition: |
|
76 "(partition(a,b) D) = |
|
77 ((D 0 = a) & |
|
78 (\<forall>n < psize D. D n < D(Suc n)) & |
|
79 (\<forall>n \<ge> psize D. D n = b))" |
|
80 apply (simp add: partition_def, auto) |
|
81 apply (subgoal_tac [!] "psize D = N", auto) |
|
82 apply (simp_all (no_asm) add: psize_def) |
|
83 apply (rule_tac [!] some_equality, blast) |
|
84 prefer 2 apply blast |
|
85 apply (rule_tac [!] ccontr) |
|
86 apply (simp_all add: linorder_neq_iff, safe) |
|
87 apply (drule_tac x = Na in spec) |
|
88 apply (rotate_tac 3) |
|
89 apply (drule_tac x = "Suc Na" in spec, simp) |
|
90 apply (rotate_tac 2) |
|
91 apply (drule_tac x = N in spec, simp) |
|
92 apply (drule_tac x = Na in spec) |
|
93 apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto) |
|
94 done |
|
95 |
|
96 lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)" |
|
97 by (simp add: partition) |
|
98 |
|
99 lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)" |
|
100 by (simp add: partition) |
|
101 |
|
102 lemma lemma_partition_lt_gen [rule_format]: |
|
103 "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)" |
|
104 apply (induct "d", auto simp add: partition) |
|
105 apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans) |
|
106 done |
|
107 |
|
108 lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d" |
|
109 by (auto simp add: less_iff_Suc_add) |
|
110 |
|
111 lemma partition_lt_gen: |
|
112 "[|partition(a,b) D; m < n; n \<le> (psize D)|] ==> D(m) < D(n)" |
|
113 by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen) |
|
114 |
|
115 lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)" |
|
116 apply (induct "n") |
|
117 apply (auto simp add: partition) |
|
118 done |
|
119 |
|
120 lemma partition_le: "partition(a,b) D ==> a \<le> b" |
|
121 apply (frule partition [THEN iffD1], safe) |
|
122 apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe) |
|
123 apply (case_tac "psize D = 0") |
|
124 apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto) |
|
125 done |
|
126 |
|
127 lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)" |
|
128 by (auto intro: partition_lt_gen) |
|
129 |
|
130 lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))" |
|
131 apply (frule partition [THEN iffD1], safe) |
|
132 apply (rotate_tac 2) |
|
133 apply (drule_tac x = "psize D" in spec) |
|
134 apply (rule ccontr) |
|
135 apply (drule_tac n = "psize D - 1" in partition_lt) |
|
136 apply auto |
|
137 done |
|
138 |
|
139 lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)" |
|
140 apply (frule partition [THEN iffD1], safe) |
|
141 apply (induct "r") |
|
142 apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear) |
|
143 apply (auto intro: partition_le) |
|
144 apply (drule_tac x = r in spec) |
|
145 apply arith; |
|
146 done |
|
147 |
|
148 lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)" |
|
149 apply (rule_tac t = a in partition_lhs [THEN subst], assumption) |
|
150 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear) |
|
151 apply (frule partition [THEN iffD1], safe) |
|
152 apply (blast intro: partition_lt less_le_trans) |
|
153 apply (rotate_tac 3) |
|
154 apply (drule_tac x = "Suc n" in spec) |
|
155 apply (erule impE) |
|
156 apply (erule less_imp_le) |
|
157 apply (frule partition_rhs) |
|
158 apply (drule partition_gt[of _ _ _ 0], arith) |
|
159 apply (simp (no_asm_simp)) |
|
160 done |
|
161 |
|
162 lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b" |
|
163 apply (frule partition [THEN iffD1]) |
|
164 apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast) |
|
165 apply (subgoal_tac "\<forall>x. D ((psize D) - x) \<le> b") |
|
166 apply (rotate_tac 4) |
|
167 apply (drule_tac x = "psize D - r" in spec) |
|
168 apply (subgoal_tac "psize D - (psize D - r) = r") |
|
169 apply simp |
|
170 apply arith |
|
171 apply safe |
|
172 apply (induct_tac "x") |
|
173 apply (simp (no_asm), blast) |
|
174 apply (case_tac "psize D - Suc n = 0") |
|
175 apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl) |
|
176 apply (simp (no_asm_simp) add: partition_le) |
|
177 apply (rule order_trans) |
|
178 prefer 2 apply assumption |
|
179 apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)") |
|
180 prefer 2 apply arith |
|
181 apply (drule_tac x = "psize D - Suc n" in spec, simp) |
|
182 done |
|
183 |
|
184 lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b" |
|
185 by (blast intro: partition_rhs [THEN subst] partition_gt) |
|
186 |
|
187 lemma lemma_partition_append1: |
|
188 "[| partition (a, b) D1; partition (b, c) D2 |] |
|
189 ==> (\<forall>n < psize D1 + psize D2. |
|
190 (if n < psize D1 then D1 n else D2 (n - psize D1)) |
|
191 < (if Suc n < psize D1 then D1 (Suc n) |
|
192 else D2 (Suc n - psize D1))) & |
|
193 (\<forall>n \<ge> psize D1 + psize D2. |
|
194 (if n < psize D1 then D1 n else D2 (n - psize D1)) = |
|
195 (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) |
|
196 else D2 (psize D1 + psize D2 - psize D1)))" |
|
197 apply (auto intro: partition_lt_gen) |
|
198 apply (subgoal_tac "psize D1 = Suc n") |
|
199 apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt) |
|
200 apply (auto intro!: partition_rhs2 simp add: partition_rhs |
|
201 split: nat_diff_split) |
|
202 done |
|
203 |
|
204 lemma lemma_psize1: |
|
205 "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] |
|
206 ==> D1(N) < D2 (psize D2)" |
|
207 apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans) |
|
208 apply (erule partition_gt) |
|
209 apply (auto simp add: partition_rhs partition_le) |
|
210 done |
|
211 |
|
212 lemma lemma_partition_append2: |
|
213 "[| partition (a, b) D1; partition (b, c) D2 |] |
|
214 ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = |
|
215 psize D1 + psize D2" |
|
216 apply (unfold psize_def |
|
217 [of "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"]) |
|
218 apply (rule some1_equality) |
|
219 prefer 2 apply (blast intro!: lemma_partition_append1) |
|
220 apply (rule ex1I, rule lemma_partition_append1) |
|
221 apply (simp_all split: split_if_asm) |
|
222 txt{*The case @{term "N < psize D1"}*} |
|
223 apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec) |
|
224 apply (force dest: lemma_psize1) |
|
225 apply (rule order_antisym); |
|
226 txt{*The case @{term "psize D1 \<le> N"}: |
|
227 proving @{term "N \<le> psize D1 + psize D2"}*} |
|
228 apply (drule_tac x = "psize D1 + psize D2" in spec) |
|
229 apply (simp add: partition_rhs2) |
|
230 apply (case_tac "N - psize D1 < psize D2") |
|
231 prefer 2 apply arith |
|
232 txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*} |
|
233 apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n --> ?P n" in spec, simp) |
|
234 apply (drule_tac a = b and b = c in partition_gt, assumption, simp) |
|
235 done |
|
236 |
|
237 lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b" |
|
238 by (auto simp add: tpart_def partition_eq) |
|
239 |
|
240 lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D" |
|
241 by (simp add: tpart_def) |
|
242 |
|
243 lemma partition_append: |
|
244 "[| tpart(a,b) (D1,p1); fine(g) (D1,p1); |
|
245 tpart(b,c) (D2,p2); fine(g) (D2,p2) |] |
|
246 ==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)" |
|
247 apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)" |
|
248 in exI) |
|
249 apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)" |
|
250 in exI) |
|
251 apply (case_tac "psize D1 = 0") |
|
252 apply (auto dest: tpart_eq_lhs_rhs) |
|
253 prefer 2 |
|
254 apply (simp add: fine_def |
|
255 lemma_partition_append2 [OF tpart_partition tpart_partition]) |
|
256 --{*But must not expand @{term fine} in other subgoals*} |
|
257 apply auto |
|
258 apply (subgoal_tac "psize D1 = Suc n") |
|
259 prefer 2 apply arith |
|
260 apply (drule tpart_partition [THEN partition_rhs]) |
|
261 apply (drule tpart_partition [THEN partition_lhs]) |
|
262 apply (auto split: nat_diff_split) |
|
263 apply (auto simp add: tpart_def) |
|
264 defer 1 |
|
265 apply (subgoal_tac "psize D1 = Suc n") |
|
266 prefer 2 apply arith |
|
267 apply (drule partition_rhs) |
|
268 apply (drule partition_lhs, auto) |
|
269 apply (simp split: nat_diff_split) |
|
270 apply (subst partition) |
|
271 apply (subst (1 2) lemma_partition_append2, assumption+) |
|
272 apply (rule conjI) |
|
273 apply (simp add: partition_lhs) |
|
274 apply (drule lemma_partition_append1) |
|
275 apply assumption; |
|
276 apply (simp add: partition_rhs) |
|
277 done |
|
278 |
|
279 |
|
280 text{*We can always find a division that is fine wrt any gauge*} |
|
281 |
|
282 lemma partition_exists: |
|
283 "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |] |
|
284 ==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)" |
|
285 apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b --> |
|
286 (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" |
|
287 in lemma_BOLZANO2) |
|
288 apply safe |
|
289 apply (blast intro: order_trans)+ |
|
290 apply (auto intro: partition_append) |
|
291 apply (case_tac "a \<le> x & x \<le> b") |
|
292 apply (rule_tac [2] x = 1 in exI, auto) |
|
293 apply (rule_tac x = "g x" in exI) |
|
294 apply (auto simp add: gauge_def) |
|
295 apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI) |
|
296 apply (rule_tac x = "%n. if n = 0 then x else ba" in exI) |
|
297 apply (auto simp add: tpart_def fine_def) |
|
298 done |
|
299 |
|
300 text{*Lemmas about combining gauges*} |
|
301 |
|
302 lemma gauge_min: |
|
303 "[| gauge(E) g1; gauge(E) g2 |] |
|
304 ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))" |
|
305 by (simp add: gauge_def) |
|
306 |
|
307 lemma fine_min: |
|
308 "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) |
|
309 ==> fine(g1) (D,p) & fine(g2) (D,p)" |
|
310 by (auto simp add: fine_def split: split_if_asm) |
|
311 |
|
312 |
|
313 text{*The integral is unique if it exists*} |
|
314 |
|
315 lemma Integral_unique: |
|
316 "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2" |
|
317 apply (simp add: Integral_def) |
|
318 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+ |
|
319 apply auto |
|
320 apply (drule gauge_min, assumption) |
|
321 apply (drule_tac g = "%x. if g x < ga x then g x else ga x" |
|
322 in partition_exists, assumption, auto) |
|
323 apply (drule fine_min) |
|
324 apply (drule spec)+ |
|
325 apply auto |
|
326 apply (subgoal_tac "\<bar>(rsum (D,p) f - k2) - (rsum (D,p) f - k1)\<bar> < \<bar>k1 - k2\<bar>") |
|
327 apply arith |
|
328 apply (drule add_strict_mono, assumption) |
|
329 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
|
330 mult_less_cancel_right) |
|
331 done |
|
332 |
|
333 lemma Integral_zero [simp]: "Integral(a,a) f 0" |
|
334 apply (auto simp add: Integral_def) |
|
335 apply (rule_tac x = "%x. 1" in exI) |
|
336 apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def) |
|
337 done |
|
338 |
|
339 lemma sumr_partition_eq_diff_bounds [simp]: |
|
340 "(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0" |
|
341 by (induct "m", auto) |
|
342 |
|
343 lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)" |
|
344 apply (auto simp add: order_le_less rsum_def Integral_def) |
|
345 apply (rule_tac x = "%x. b - a" in exI) |
|
346 apply (auto simp add: gauge_def abs_less_iff tpart_def partition) |
|
347 done |
|
348 |
|
349 lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))" |
|
350 apply (auto simp add: order_le_less rsum_def Integral_def) |
|
351 apply (rule_tac x = "%x. b - a" in exI) |
|
352 apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_less_iff |
|
353 right_diff_distrib [symmetric] partition tpart_def) |
|
354 done |
|
355 |
|
356 lemma Integral_mult: |
|
357 "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)" |
|
358 apply (auto simp add: order_le_less |
|
359 dest: Integral_unique [OF order_refl Integral_zero]) |
|
360 apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc) |
|
361 apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE]) |
|
362 prefer 2 apply force |
|
363 apply (drule_tac x = "e/abs c" in spec, auto) |
|
364 apply (simp add: zero_less_mult_iff divide_inverse) |
|
365 apply (rule exI, auto) |
|
366 apply (drule spec)+ |
|
367 apply auto |
|
368 apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1]) |
|
369 apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric]) |
|
370 done |
|
371 |
|
372 text{*Fundamental theorem of calculus (Part I)*} |
|
373 |
|
374 text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *} |
|
375 |
|
376 lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))" |
|
377 by (insert bchoice [of "Collect P" Q], simp) |
|
378 |
|
379 (*UNUSED |
|
380 lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==> |
|
381 \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))" |
|
382 *) |
|
383 |
|
384 |
|
385 (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance |
|
386 they break the original proofs and make new proofs longer!*) |
|
387 lemma strad1: |
|
388 "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa - x\<bar> < s \<longrightarrow> |
|
389 \<bar>(f xa - f x) / (xa - x) - f' x\<bar> * 2 < e; |
|
390 0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk> |
|
391 \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>" |
|
392 apply auto |
|
393 apply (case_tac "0 < \<bar>z - x\<bar>") |
|
394 prefer 2 apply (simp add: zero_less_abs_iff) |
|
395 apply (drule_tac x = z in spec) |
|
396 apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" |
|
397 in real_mult_le_cancel_iff2 [THEN iffD1]) |
|
398 apply simp |
|
399 apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric] |
|
400 mult_assoc [symmetric]) |
|
401 apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) |
|
402 = (f z - f x) / (z - x) - f' x") |
|
403 apply (simp add: abs_mult [symmetric] mult_ac diff_minus) |
|
404 apply (subst mult_commute) |
|
405 apply (simp add: left_distrib diff_minus) |
|
406 apply (simp add: mult_assoc divide_inverse) |
|
407 apply (simp add: left_distrib) |
|
408 done |
|
409 |
|
410 lemma lemma_straddle: |
|
411 "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |] |
|
412 ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g & |
|
413 (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x) |
|
414 --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))" |
|
415 apply (simp add: gauge_def) |
|
416 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> |
|
417 (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> |
|
418 \<bar>(f (v) - f (u)) - (f' (x) * (v - u))\<bar> \<le> e * (v - u))") |
|
419 apply (drule choiceP, auto) |
|
420 apply (drule spec, auto) |
|
421 apply (auto simp add: DERIV_iff2 LIM_def) |
|
422 apply (drule_tac x = "e/2" in spec, auto) |
|
423 apply (frule strad1, assumption+) |
|
424 apply (rule_tac x = s in exI, auto) |
|
425 apply (rule_tac x = u and y = v in linorder_cases, auto) |
|
426 apply (rule_tac y = "\<bar>(f (v) - f (x)) - (f' (x) * (v - x))\<bar> + |
|
427 \<bar>(f (x) - f (u)) - (f' (x) * (x - u))\<bar>" |
|
428 in order_trans) |
|
429 apply (rule abs_triangle_ineq [THEN [2] order_trans]) |
|
430 apply (simp add: right_diff_distrib) |
|
431 apply (rule_tac t = "e* (v - u)" in real_sum_of_halves [THEN subst]) |
|
432 apply (rule add_mono) |
|
433 apply (rule_tac y = "(e/2) * \<bar>v - x\<bar>" in order_trans) |
|
434 prefer 2 apply simp |
|
435 apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' - x\<bar> < s --> ?P x'" in thin_rl) |
|
436 apply (drule_tac x = v in spec, simp add: times_divide_eq) |
|
437 apply (drule_tac x = u in spec, auto) |
|
438 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>") |
|
439 apply (rule order_trans) |
|
440 apply (auto simp add: abs_le_iff) |
|
441 apply (simp add: right_diff_distrib) |
|
442 done |
|
443 |
|
444 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |] |
|
445 ==> Integral(a,b) f' (f(b) - f(a))" |
|
446 apply (drule order_le_imp_less_or_eq, auto) |
|
447 apply (auto simp add: Integral_def) |
|
448 apply (rule ccontr) |
|
449 apply (subgoal_tac "\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e)") |
|
450 apply (rotate_tac 3) |
|
451 apply (drule_tac x = "e/2" in spec, auto) |
|
452 apply (drule spec, auto) |
|
453 apply ((drule spec)+, auto) |
|
454 apply (drule_tac e = "ea/ (b - a)" in lemma_straddle) |
|
455 apply (auto simp add: zero_less_divide_iff) |
|
456 apply (rule exI) |
|
457 apply (auto simp add: tpart_def rsum_def) |
|
458 apply (subgoal_tac "(\<Sum>n=0..<psize D. f(D(Suc n)) - f(D n)) = f b - f a") |
|
459 prefer 2 |
|
460 apply (cut_tac D = "%n. f (D n)" and m = "psize D" |
|
461 in sumr_partition_eq_diff_bounds) |
|
462 apply (simp add: partition_lhs partition_rhs) |
|
463 apply (drule sym, simp) |
|
464 apply (simp (no_asm) add: setsum_subtractf[symmetric]) |
|
465 apply (rule setsum_abs [THEN order_trans]) |
|
466 apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (ea / (b - a)) * (D (Suc n) - (D n)))") |
|
467 apply (simp add: abs_minus_commute) |
|
468 apply (rule_tac t = ea in ssubst, assumption) |
|
469 apply (rule setsum_mono) |
|
470 apply (rule_tac [2] setsum_right_distrib [THEN subst]) |
|
471 apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub |
|
472 fine_def) |
|
473 done |
|
474 |
|
475 |
|
476 lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2" |
|
477 by simp |
|
478 |
|
479 lemma Integral_add: |
|
480 "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2; |
|
481 \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |] |
|
482 ==> Integral(a,c) f' (k1 + k2)" |
|
483 apply (rule FTC1 [THEN Integral_subst], auto) |
|
484 apply (frule FTC1, auto) |
|
485 apply (frule_tac a = b in FTC1, auto) |
|
486 apply (drule_tac x = x in spec, auto) |
|
487 apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique) |
|
488 apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto) |
|
489 done |
|
490 |
|
491 lemma partition_psize_Least: |
|
492 "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)" |
|
493 apply (auto intro!: Least_equality [symmetric] partition_rhs) |
|
494 apply (auto dest: partition_ub_lt simp add: linorder_not_less [symmetric]) |
|
495 done |
|
496 |
|
497 lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))" |
|
498 apply safe |
|
499 apply (drule_tac r = n in partition_ub, auto) |
|
500 done |
|
501 |
|
502 lemma lemma_partition_eq: |
|
503 "partition (a, c) D ==> D = (%n. if D n < c then D n else c)" |
|
504 apply (rule ext, auto) |
|
505 apply (auto dest!: lemma_partition_bounded) |
|
506 apply (drule_tac x = n in spec, auto) |
|
507 done |
|
508 |
|
509 lemma lemma_partition_eq2: |
|
510 "partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)" |
|
511 apply (rule ext, auto) |
|
512 apply (auto dest!: lemma_partition_bounded) |
|
513 apply (drule_tac x = n in spec, auto) |
|
514 done |
|
515 |
|
516 lemma partition_lt_Suc: |
|
517 "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)" |
|
518 by (auto simp add: partition) |
|
519 |
|
520 lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)" |
|
521 apply (rule ext) |
|
522 apply (auto simp add: tpart_def) |
|
523 apply (drule linorder_not_less [THEN iffD1]) |
|
524 apply (drule_tac r = "Suc n" in partition_ub) |
|
525 apply (drule_tac x = n in spec, auto) |
|
526 done |
|
527 |
|
528 subsection{*Lemmas for Additivity Theorem of Gauge Integral*} |
|
529 |
|
530 lemma lemma_additivity1: |
|
531 "[| a \<le> D n; D n < b; partition(a,b) D |] ==> n < psize D" |
|
532 by (auto simp add: partition linorder_not_less [symmetric]) |
|
533 |
|
534 lemma lemma_additivity2: "[| a \<le> D n; partition(a,D n) D |] ==> psize D \<le> n" |
|
535 apply (rule ccontr, drule not_leE) |
|
536 apply (frule partition [THEN iffD1], safe) |
|
537 apply (frule_tac r = "Suc n" in partition_ub) |
|
538 apply (auto dest!: spec) |
|
539 done |
|
540 |
|
541 lemma partition_eq_bound: |
|
542 "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)" |
|
543 by (auto simp add: partition) |
|
544 |
|
545 lemma partition_ub2: "[| partition(a,b) D; psize D < m |] ==> D(r) \<le> D(m)" |
|
546 by (simp add: partition partition_ub) |
|
547 |
|
548 lemma tag_point_eq_partition_point: |
|
549 "[| tpart(a,b) (D,p); psize D \<le> m |] ==> p(m) = D(m)" |
|
550 apply (simp add: tpart_def, auto) |
|
551 apply (drule_tac x = m in spec) |
|
552 apply (auto simp add: partition_rhs2) |
|
553 done |
|
554 |
|
555 lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n" |
|
556 apply (cut_tac less_linear [of n "psize D"], auto) |
|
557 apply (cut_tac less_linear [of m n]) |
|
558 apply (cut_tac less_linear [of m "psize D"]) |
|
559 apply (auto dest: partition_gt) |
|
560 apply (drule_tac n = m in partition_lt_gen, auto) |
|
561 apply (frule partition_eq_bound) |
|
562 apply (drule_tac [2] partition_gt, auto) |
|
563 apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2) |
|
564 apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2) |
|
565 done |
|
566 |
|
567 lemma lemma_additivity4_psize_eq: |
|
568 "[| a \<le> D n; D n < b; partition (a, b) D |] |
|
569 ==> psize (%x. if D x < D n then D(x) else D n) = n" |
|
570 apply (unfold psize_def) |
|
571 apply (frule lemma_additivity1) |
|
572 apply (assumption, assumption) |
|
573 apply (rule some_equality) |
|
574 apply (auto intro: partition_lt_Suc) |
|
575 apply (drule_tac n = n in partition_lt_gen, assumption) |
|
576 apply (arith, arith) |
|
577 apply (cut_tac x = na and y = "psize D" in less_linear) |
|
578 apply (auto dest: partition_lt_cancel) |
|
579 apply (rule_tac x=N and y=n in linorder_cases) |
|
580 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp) |
|
581 apply (drule_tac n = n in partition_lt_gen, auto) |
|
582 apply (drule_tac x = n in spec) |
|
583 apply (simp split: split_if_asm) |
|
584 done |
|
585 |
|
586 lemma lemma_psize_left_less_psize: |
|
587 "partition (a, b) D |
|
588 ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D" |
|
589 apply (frule_tac r = n in partition_ub) |
|
590 apply (drule_tac x = "D n" in order_le_imp_less_or_eq) |
|
591 apply (auto simp add: lemma_partition_eq [symmetric]) |
|
592 apply (frule_tac r = n in partition_lb) |
|
593 apply (drule (2) lemma_additivity4_psize_eq) |
|
594 apply (rule ccontr, auto) |
|
595 apply (frule_tac not_leE [THEN [2] partition_eq_bound]) |
|
596 apply (auto simp add: partition_rhs) |
|
597 done |
|
598 |
|
599 lemma lemma_psize_left_less_psize2: |
|
600 "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |] |
|
601 ==> na < psize D" |
|
602 by (erule lemma_psize_left_less_psize [THEN [2] less_le_trans]) |
|
603 |
|
604 |
|
605 lemma lemma_additivity3: |
|
606 "[| partition(a,b) D; D na < D n; D n < D (Suc na); |
|
607 n < psize D |] |
|
608 ==> False" |
|
609 by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff) |
|
610 |
|
611 |
|
612 lemma psize_const [simp]: "psize (%x. k) = 0" |
|
613 by (auto simp add: psize_def) |
|
614 |
|
615 lemma lemma_additivity3a: |
|
616 "[| partition(a,b) D; D na < D n; D n < D (Suc na); |
|
617 na < psize D |] |
|
618 ==> False" |
|
619 apply (frule_tac m = n in partition_lt_cancel) |
|
620 apply (auto intro: lemma_additivity3) |
|
621 done |
|
622 |
|
623 lemma better_lemma_psize_right_eq1: |
|
624 "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D - n" |
|
625 apply (simp add: psize_def [of "(%x. D (x + n))"]); |
|
626 apply (rule_tac a = "psize D - n" in someI2, auto) |
|
627 apply (simp add: partition less_diff_conv) |
|
628 apply (simp add: le_diff_conv partition_rhs2 split: nat_diff_split) |
|
629 apply (drule_tac x = "psize D - n" in spec, auto) |
|
630 apply (frule partition_rhs, safe) |
|
631 apply (frule partition_lt_cancel, assumption) |
|
632 apply (drule partition [THEN iffD1], safe) |
|
633 apply (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))") |
|
634 apply blast |
|
635 apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)" |
|
636 in spec) |
|
637 apply simp |
|
638 done |
|
639 |
|
640 lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n" |
|
641 apply (rule ccontr, drule not_leE) |
|
642 apply (frule partition_lt_Suc, assumption) |
|
643 apply (frule_tac r = "Suc n" in partition_ub, auto) |
|
644 done |
|
645 |
|
646 lemma better_lemma_psize_right_eq1a: |
|
647 "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D - n" |
|
648 apply (simp add: psize_def [of "(%x. D (x + n))"]); |
|
649 apply (rule_tac a = "psize D - n" in someI2, auto) |
|
650 apply (simp add: partition less_diff_conv) |
|
651 apply (simp add: le_diff_conv) |
|
652 apply (case_tac "psize D \<le> n") |
|
653 apply (force intro: partition_rhs2) |
|
654 apply (simp add: partition linorder_not_le) |
|
655 apply (rule ccontr, drule not_leE) |
|
656 apply (frule psize_le_n) |
|
657 apply (drule_tac x = "psize D - n" in spec, simp) |
|
658 apply (drule partition [THEN iffD1], safe) |
|
659 apply (drule_tac x = "Suc n" and P="%na. ?s \<le> na \<longrightarrow> D na = D n" in spec, auto) |
|
660 done |
|
661 |
|
662 lemma better_lemma_psize_right_eq: |
|
663 "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n" |
|
664 apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) |
|
665 apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1) |
|
666 done |
|
667 |
|
668 lemma lemma_psize_right_eq1: |
|
669 "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D" |
|
670 apply (simp add: psize_def [of "(%x. D (x + n))"]) |
|
671 apply (rule_tac a = "psize D - n" in someI2, auto) |
|
672 apply (simp add: partition less_diff_conv) |
|
673 apply (subgoal_tac "n \<le> psize D") |
|
674 apply (simp add: partition le_diff_conv) |
|
675 apply (rule ccontr, drule not_leE) |
|
676 apply (drule_tac less_imp_le [THEN [2] partition_rhs2], assumption, simp) |
|
677 apply (drule_tac x = "psize D" in spec) |
|
678 apply (simp add: partition) |
|
679 done |
|
680 |
|
681 (* should be combined with previous theorem; also proof has redundancy *) |
|
682 lemma lemma_psize_right_eq1a: |
|
683 "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D" |
|
684 apply (simp add: psize_def [of "(%x. D (x + n))"]); |
|
685 apply (rule_tac a = "psize D - n" in someI2, auto) |
|
686 apply (simp add: partition less_diff_conv) |
|
687 apply (case_tac "psize D \<le> n") |
|
688 apply (force intro: partition_rhs2 simp add: le_diff_conv) |
|
689 apply (simp add: partition le_diff_conv) |
|
690 apply (rule ccontr, drule not_leE) |
|
691 apply (drule_tac x = "psize D" in spec) |
|
692 apply (simp add: partition) |
|
693 done |
|
694 |
|
695 lemma lemma_psize_right_eq: |
|
696 "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D" |
|
697 apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) |
|
698 apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1) |
|
699 done |
|
700 |
|
701 lemma tpart_left1: |
|
702 "[| a \<le> D n; tpart (a, b) (D, p) |] |
|
703 ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, |
|
704 %x. if D x < D n then p(x) else D n)" |
|
705 apply (frule_tac r = n in tpart_partition [THEN partition_ub]) |
|
706 apply (drule_tac x = "D n" in order_le_imp_less_or_eq) |
|
707 apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric]) |
|
708 apply (frule_tac tpart_partition [THEN [3] lemma_additivity1]) |
|
709 apply (auto simp add: tpart_def) |
|
710 apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto) |
|
711 prefer 3 apply (drule_tac x=na in spec, arith) |
|
712 prefer 2 apply (blast dest: lemma_additivity3) |
|
713 apply (frule (2) lemma_additivity4_psize_eq) |
|
714 apply (rule partition [THEN iffD2]) |
|
715 apply (frule partition [THEN iffD1]) |
|
716 apply safe |
|
717 apply (auto simp add: partition_lt_gen) |
|
718 apply (drule (1) partition_lt_cancel, arith) |
|
719 done |
|
720 |
|
721 lemma fine_left1: |
|
722 "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g; |
|
723 fine (%x. if x < D n then min (g x) ((D n - x)/ 2) |
|
724 else if x = D n then min (g (D n)) (ga (D n)) |
|
725 else min (ga x) ((x - D n)/ 2)) (D, p) |] |
|
726 ==> fine g |
|
727 (%x. if D x < D n then D(x) else D n, |
|
728 %x. if D x < D n then p(x) else D n)" |
|
729 apply (auto simp add: fine_def tpart_def gauge_def) |
|
730 apply (frule_tac [!] na=na in lemma_psize_left_less_psize2) |
|
731 apply (drule_tac [!] x = na in spec, auto) |
|
732 apply (drule_tac [!] x = na in spec, auto) |
|
733 apply (auto dest: lemma_additivity3a simp add: split_if_asm) |
|
734 done |
|
735 |
|
736 lemma tpart_right1: |
|
737 "[| a \<le> D n; tpart (a, b) (D, p) |] |
|
738 ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))" |
|
739 apply (simp add: tpart_def partition_def, safe) |
|
740 apply (rule_tac x = "N - n" in exI, auto) |
|
741 done |
|
742 |
|
743 lemma fine_right1: |
|
744 "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga; |
|
745 fine (%x. if x < D n then min (g x) ((D n - x)/ 2) |
|
746 else if x = D n then min (g (D n)) (ga (D n)) |
|
747 else min (ga x) ((x - D n)/ 2)) (D, p) |] |
|
748 ==> fine ga (%x. D(x + n),%x. p(x + n))" |
|
749 apply (auto simp add: fine_def gauge_def) |
|
750 apply (drule_tac x = "na + n" in spec) |
|
751 apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto) |
|
752 apply (simp add: tpart_def, safe) |
|
753 apply (subgoal_tac "D n \<le> p (na + n)") |
|
754 apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq) |
|
755 apply safe |
|
756 apply (simp split: split_if_asm, simp) |
|
757 apply (drule less_le_trans, assumption) |
|
758 apply (rotate_tac 5) |
|
759 apply (drule_tac x = "na + n" in spec, safe) |
|
760 apply (rule_tac y="D (na + n)" in order_trans) |
|
761 apply (case_tac "na = 0", auto) |
|
762 apply (erule partition_lt_gen [THEN order_less_imp_le]) |
|
763 apply arith |
|
764 apply arith |
|
765 done |
|
766 |
|
767 lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g" |
|
768 by (simp add: rsum_def setsum_addf left_distrib) |
|
769 |
|
770 text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *} |
|
771 lemma Integral_add_fun: |
|
772 "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |] |
|
773 ==> Integral(a,b) (%x. f x + g x) (k1 + k2)" |
|
774 apply (simp add: Integral_def, auto) |
|
775 apply ((drule_tac x = "e/2" in spec)+) |
|
776 apply auto |
|
777 apply (drule gauge_min, assumption) |
|
778 apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI) |
|
779 apply auto |
|
780 apply (drule fine_min) |
|
781 apply ((drule spec)+, auto) |
|
782 apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption) |
|
783 apply (auto simp only: rsum_add left_distrib [symmetric] |
|
784 mult_2_right [symmetric] real_mult_less_iff1) |
|
785 done |
|
786 |
|
787 lemma partition_lt_gen2: |
|
788 "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r" |
|
789 by (auto simp add: partition) |
|
790 |
|
791 lemma lemma_Integral_le: |
|
792 "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x; |
|
793 tpart(a,b) (D,p) |
|
794 |] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)" |
|
795 apply (simp add: tpart_def) |
|
796 apply (auto, frule partition [THEN iffD1], auto) |
|
797 apply (drule_tac x = "p n" in spec, auto) |
|
798 apply (case_tac "n = 0", simp) |
|
799 apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto) |
|
800 apply (drule le_imp_less_or_eq, auto) |
|
801 apply (drule_tac [2] x = "psize D" in spec, auto) |
|
802 apply (drule_tac r = "Suc n" in partition_ub) |
|
803 apply (drule_tac x = n in spec, auto) |
|
804 done |
|
805 |
|
806 lemma lemma_Integral_rsum_le: |
|
807 "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x; |
|
808 tpart(a,b) (D,p) |
|
809 |] ==> rsum(D,p) f \<le> rsum(D,p) g" |
|
810 apply (simp add: rsum_def) |
|
811 apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2] |
|
812 dest!: lemma_Integral_le) |
|
813 done |
|
814 |
|
815 lemma Integral_le: |
|
816 "[| a \<le> b; |
|
817 \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x); |
|
818 Integral(a,b) f k1; Integral(a,b) g k2 |
|
819 |] ==> k1 \<le> k2" |
|
820 apply (simp add: Integral_def) |
|
821 apply (rotate_tac 2) |
|
822 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec) |
|
823 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec, auto) |
|
824 apply (drule gauge_min, assumption) |
|
825 apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x" |
|
826 in partition_exists, assumption, auto) |
|
827 apply (drule fine_min) |
|
828 apply (drule_tac x = D in spec, drule_tac x = D in spec) |
|
829 apply (drule_tac x = p in spec, drule_tac x = p in spec, auto) |
|
830 apply (frule lemma_Integral_rsum_le, assumption) |
|
831 apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar>") |
|
832 apply arith |
|
833 apply (drule add_strict_mono, assumption) |
|
834 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
|
835 real_mult_less_iff1) |
|
836 done |
|
837 |
|
838 lemma Integral_imp_Cauchy: |
|
839 "(\<exists>k. Integral(a,b) f k) ==> |
|
840 (\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & |
|
841 (\<forall>D1 D2 p1 p2. |
|
842 tpart(a,b) (D1, p1) & fine g (D1,p1) & |
|
843 tpart(a,b) (D2, p2) & fine g (D2,p2) --> |
|
844 \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e))" |
|
845 apply (simp add: Integral_def, auto) |
|
846 apply (drule_tac x = "e/2" in spec, auto) |
|
847 apply (rule exI, auto) |
|
848 apply (frule_tac x = D1 in spec) |
|
849 apply (frule_tac x = D2 in spec) |
|
850 apply ((drule spec)+, auto) |
|
851 apply (erule_tac V = "0 < e" in thin_rl) |
|
852 apply (drule add_strict_mono, assumption) |
|
853 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
|
854 real_mult_less_iff1) |
|
855 done |
|
856 |
|
857 lemma Cauchy_iff2: |
|
858 "Cauchy X = |
|
859 (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))" |
|
860 apply (simp add: Cauchy_def, auto) |
|
861 apply (drule reals_Archimedean, safe) |
|
862 apply (drule_tac x = n in spec, auto) |
|
863 apply (rule_tac x = M in exI, auto) |
|
864 apply (drule_tac x = m in spec, simp) |
|
865 apply (drule_tac x = na in spec, auto) |
|
866 done |
|
867 |
|
868 lemma partition_exists2: |
|
869 "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |] |
|
870 ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)" |
|
871 by (blast dest: partition_exists) |
|
872 |
|
873 lemma monotonic_anti_derivative: |
|
874 fixes f g :: "real => real" shows |
|
875 "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c; |
|
876 \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |] |
|
877 ==> f b - f a \<le> g b - g a" |
|
878 apply (rule Integral_le, assumption) |
|
879 apply (auto intro: FTC1) |
|
880 done |
|
881 |
|
882 end |
|