|
13958
|
1 |
(* Title : Integration.thy
|
|
|
2 |
Author : Jacques D. Fleuriot
|
|
|
3 |
Copyright : 2000 University of Edinburgh
|
|
|
4 |
Description : Theory of integration (cf. Harrison's HOL development)
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
Integration = MacLaurin +
|
|
|
8 |
|
|
|
9 |
|
|
|
10 |
constdefs
|
|
|
11 |
|
|
|
12 |
|
|
|
13 |
(* ------------------------------------------------------------------------ *)
|
|
|
14 |
(* Partitions and tagged partitions etc. *)
|
|
|
15 |
(* ------------------------------------------------------------------------ *)
|
|
|
16 |
|
|
|
17 |
partition :: "[(real*real),nat => real] => bool"
|
|
|
18 |
"partition == %(a,b) D. ((D 0 = a) &
|
|
|
19 |
(EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
|
|
|
20 |
(ALL n. N <= n --> (D(n) = b)))))"
|
|
|
21 |
|
|
|
22 |
psize :: (nat => real) => nat
|
|
|
23 |
"psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
|
|
|
24 |
(ALL n. N <= n --> (D(n) = D(N)))"
|
|
|
25 |
|
|
|
26 |
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
|
|
|
27 |
"tpart == %(a,b) (D,p). partition(a,b) D &
|
|
|
28 |
(ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"
|
|
|
29 |
|
|
|
30 |
(* ------------------------------------------------------------------------ *)
|
|
|
31 |
(* Gauges and gauge-fine divisions *)
|
|
|
32 |
(* ------------------------------------------------------------------------ *)
|
|
|
33 |
|
|
|
34 |
gauge :: [real => bool, real => real] => bool
|
|
|
35 |
"gauge E g == ALL x. E x --> 0 < g(x)"
|
|
|
36 |
|
|
|
37 |
fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
|
|
|
38 |
"fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
|
|
|
39 |
|
|
|
40 |
(* ------------------------------------------------------------------------ *)
|
|
|
41 |
(* Riemann sum *)
|
|
|
42 |
(* ------------------------------------------------------------------------ *)
|
|
|
43 |
|
|
|
44 |
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
|
|
|
45 |
"rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
|
|
|
46 |
|
|
|
47 |
(* ------------------------------------------------------------------------ *)
|
|
|
48 |
(* Gauge integrability (definite) *)
|
|
|
49 |
(* ------------------------------------------------------------------------ *)
|
|
|
50 |
|
|
|
51 |
Integral :: "[(real*real),real=>real,real] => bool"
|
|
|
52 |
"Integral == %(a,b) f k. ALL e. 0 < e -->
|
|
|
53 |
(EX g. gauge(%x. a <= x & x <= b) g &
|
|
|
54 |
(ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
|
|
|
55 |
abs(rsum(D,p) f - k) < e))"
|
|
|
56 |
end
|
|
|
57 |
|
|
|
58 |
|