src/HOL/ex/Gauge_Integration.thy
 changeset 37765 26bdfb7b680b parent 35441 ae742caa0c5b child 45605 a89b4bc311a5
equal 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:`