src/HOL/ex/Gauge_Integration.thy
changeset 37765 26bdfb7b680b
parent 35441 ae742caa0c5b
child 45605 a89b4bc311a5
equal deleted inserted replaced
37764:3489daf839d5 37765:26bdfb7b680b
    26 
    26 
    27 subsection {* Gauges *}
    27 subsection {* Gauges *}
    28 
    28 
    29 definition
    29 definition
    30   gauge :: "[real set, real => real] => bool" where
    30   gauge :: "[real set, real => real] => bool" where
    31   [code del]: "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    31   "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
    32 
    32 
    33 
    33 
    34 subsection {* Gauge-fine divisions *}
    34 subsection {* Gauge-fine divisions *}
    35 
    35 
    36 inductive
    36 inductive
   257 
   257 
   258 subsection {* Gauge integrability (definite) *}
   258 subsection {* Gauge integrability (definite) *}
   259 
   259 
   260 definition
   260 definition
   261   Integral :: "[(real*real),real=>real,real] => bool" where
   261   Integral :: "[(real*real),real=>real,real] => bool" where
   262   [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
   262   "Integral = (%(a,b) f k. \<forall>e > 0.
   263                                (\<exists>\<delta>. gauge {a .. b} \<delta> &
   263                                (\<exists>\<delta>. gauge {a .. b} \<delta> &
   264                                (\<forall>D. fine \<delta> (a,b) D -->
   264                                (\<forall>D. fine \<delta> (a,b) D -->
   265                                          \<bar>rsum D f - k\<bar> < e)))"
   265                                          \<bar>rsum D f - k\<bar> < e)))"
   266 
   266 
   267 lemma Integral_eq:
   267 lemma Integral_eq: