src/HOL/Hyperreal/Integration.thy

New material on integration, etc. Moving Hyperreal/ex
to directory Complex

(*  Title       : Integration.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 2000  University of Edinburgh
    Description : Theory of integration (cf. Harrison's HOL development)
*)

Integration = MacLaurin + 


constdefs

  
(* ------------------------------------------------------------------------ *)
(* Partitions and tagged partitions etc.                                    *)
(* ------------------------------------------------------------------------ *)

  partition :: "[(real*real),nat => real] => bool"
  "partition == %(a,b) D. ((D 0 = a) & 
                         (EX N. ((ALL n. n < N --> D(n) < D(Suc n)) &
                            (ALL n. N <= n --> (D(n) = b)))))"
  
  psize :: (nat => real) => nat
  "psize D == @N. (ALL n. n < N --> D(n) < D(Suc n)) &
                  (ALL n. N <= n --> (D(n) = D(N)))"
  
  tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
  "tpart == %(a,b) (D,p). partition(a,b) D &
                          (ALL n. D(n) <= p(n) & p(n) <= D(Suc n))"

(* ------------------------------------------------------------------------ *)
(* Gauges and gauge-fine divisions                                          *)
(* ------------------------------------------------------------------------ *)
  
  gauge :: [real => bool, real => real] => bool
  "gauge E g == ALL x. E x --> 0 < g(x)"

  fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
  "fine == % g (D,p). ALL n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"

(* ------------------------------------------------------------------------ *)
(* Riemann sum                                                              *)
(* ------------------------------------------------------------------------ *)

  rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
  "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"

(* ------------------------------------------------------------------------ *)
(* Gauge integrability (definite)                                           *)
(* ------------------------------------------------------------------------ *)

   Integral :: "[(real*real),real=>real,real] => bool"
   "Integral == %(a,b) f k. ALL e. 0 < e -->
                               (EX g. gauge(%x. a <= x & x <= b) g &
                               (ALL D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
                                         abs(rsum(D,p) f - k) < e))"    
end