Translated remaining theorems about integration from HOL light.
authorhimmelma
Tue Apr 20 14:07:52 2010 +0200 (2010-04-20)
changeset 36243027ae62681be
parent 36101 bae883012af3
child 36244 009b0ee1b838
Translated remaining theorems about integration from HOL light.
src/HOL/Multivariate_Analysis/Integration.cert
src/HOL/Multivariate_Analysis/Integration.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Integration.cert	Fri Apr 09 13:35:54 2010 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Integration.cert	Tue Apr 20 14:07:52 2010 +0200
     1.3 @@ -3210,3 +3210,772 @@
     1.4  #228 := [unit-resolution #200 #220]: #173
     1.5  [th-lemma #228 #227 #211]: false
     1.6  unsat
     1.7 +610fb185d846b293ce6bb466b6770a65def3e59c 768 0
     1.8 +#2 := false
     1.9 +#7 := 0::real
    1.10 +decl uf_2 :: real
    1.11 +#5 := uf_2
    1.12 +#75 := -1::real
    1.13 +#76 := (* -1::real uf_2)
    1.14 +decl uf_1 :: real
    1.15 +#4 := uf_1
    1.16 +#77 := (+ uf_1 #76)
    1.17 +#316 := (>= #77 0::real)
    1.18 +#317 := (not #316)
    1.19 +decl uf_8 :: real
    1.20 +#39 := uf_8
    1.21 +#216 := (* -1::real uf_8)
    1.22 +#220 := (+ uf_1 #216)
    1.23 +#221 := (<= #220 0::real)
    1.24 +#86 := (* -1::real uf_1)
    1.25 +#87 := (+ #86 uf_2)
    1.26 +#323 := (ite #316 #77 #87)
    1.27 +#331 := (* -1::real #323)
    1.28 +decl uf_3 :: real
    1.29 +#11 := uf_3
    1.30 +#95 := 1/3::real
    1.31 +#96 := (* 1/3::real uf_3)
    1.32 +#332 := (+ #96 #331)
    1.33 +#333 := (<= #332 0::real)
    1.34 +#334 := (not #333)
    1.35 +decl uf_4 :: real
    1.36 +#15 := uf_4
    1.37 +#111 := (* -1::real uf_4)
    1.38 +#112 := (+ uf_2 #111)
    1.39 +#102 := (+ #76 uf_4)
    1.40 +#293 := (<= #112 0::real)
    1.41 +#300 := (ite #293 #102 #112)
    1.42 +#308 := (* -1::real #300)
    1.43 +#309 := (+ #96 #308)
    1.44 +#310 := (<= #309 0::real)
    1.45 +#311 := (not #310)
    1.46 +decl uf_6 :: real
    1.47 +#22 := uf_6
    1.48 +decl uf_5 :: real
    1.49 +#21 := uf_5
    1.50 +#133 := (* -1::real uf_5)
    1.51 +#134 := (+ #133 uf_6)
    1.52 +#123 := (* -1::real uf_6)
    1.53 +#124 := (+ uf_5 #123)
    1.54 +#270 := (>= #124 0::real)
    1.55 +#277 := (ite #270 #124 #134)
    1.56 +#285 := (* -1::real #277)
    1.57 +#286 := (+ #96 #285)
    1.58 +#287 := (<= #286 0::real)
    1.59 +#288 := (not #287)
    1.60 +decl uf_7 :: real
    1.61 +#28 := uf_7
    1.62 +#154 := (* -1::real uf_7)
    1.63 +#155 := (+ uf_6 #154)
    1.64 +#145 := (+ #123 uf_7)
    1.65 +#247 := (<= #155 0::real)
    1.66 +#254 := (ite #247 #145 #155)
    1.67 +#262 := (* -1::real #254)
    1.68 +#263 := (+ #96 #262)
    1.69 +#264 := (<= #263 0::real)
    1.70 +#265 := (not #264)
    1.71 +#175 := (+ #76 uf_6)
    1.72 +#166 := (+ uf_2 #123)
    1.73 +#224 := (>= #166 0::real)
    1.74 +#231 := (ite #224 #166 #175)
    1.75 +#239 := (* -1::real #231)
    1.76 +#240 := (+ #96 #239)
    1.77 +#241 := (<= #240 0::real)
    1.78 +#242 := (not #241)
    1.79 +#217 := (+ uf_5 #216)
    1.80 +#215 := (>= #217 0::real)
    1.81 +decl uf_9 :: real
    1.82 +#42 := uf_9
    1.83 +#206 := (* -1::real uf_9)
    1.84 +#212 := (+ uf_7 #206)
    1.85 +#211 := (>= #212 0::real)
    1.86 +#207 := (+ uf_4 #206)
    1.87 +#208 := (<= #207 0::real)
    1.88 +#363 := (and #208 #211 #215 #221 #242 #265 #288 #311 #334)
    1.89 +#44 := (<= uf_9 uf_7)
    1.90 +#43 := (<= uf_4 uf_9)
    1.91 +#45 := (and #43 #44)
    1.92 +#41 := (<= uf_8 uf_5)
    1.93 +#46 := (and #41 #45)
    1.94 +#40 := (<= uf_1 uf_8)
    1.95 +#47 := (and #40 #46)
    1.96 +#12 := 3::real
    1.97 +#13 := (/ uf_3 3::real)
    1.98 +#34 := (- uf_2 uf_6)
    1.99 +#36 := (- #34)
   1.100 +#35 := (< #34 0::real)
   1.101 +#37 := (ite #35 #36 #34)
   1.102 +#38 := (< #37 #13)
   1.103 +#48 := (and #38 #47)
   1.104 +#29 := (- uf_7 uf_6)
   1.105 +#31 := (- #29)
   1.106 +#30 := (< #29 0::real)
   1.107 +#32 := (ite #30 #31 #29)
   1.108 +#33 := (< #32 #13)
   1.109 +#49 := (and #33 #48)
   1.110 +#23 := (- uf_5 uf_6)
   1.111 +#25 := (- #23)
   1.112 +#24 := (< #23 0::real)
   1.113 +#26 := (ite #24 #25 #23)
   1.114 +#27 := (< #26 #13)
   1.115 +#50 := (and #27 #49)
   1.116 +#16 := (- uf_4 uf_2)
   1.117 +#18 := (- #16)
   1.118 +#17 := (< #16 0::real)
   1.119 +#19 := (ite #17 #18 #16)
   1.120 +#20 := (< #19 #13)
   1.121 +#51 := (and #20 #50)
   1.122 +#6 := (- uf_1 uf_2)
   1.123 +#9 := (- #6)
   1.124 +#8 := (< #6 0::real)
   1.125 +#10 := (ite #8 #9 #6)
   1.126 +#14 := (< #10 #13)
   1.127 +#52 := (and #14 #51)
   1.128 +#368 := (iff #52 #363)
   1.129 +#169 := (< #166 0::real)
   1.130 +#180 := (ite #169 #175 #166)
   1.131 +#183 := (< #180 #96)
   1.132 +#189 := (and #47 #183)
   1.133 +#148 := (< #145 0::real)
   1.134 +#160 := (ite #148 #155 #145)
   1.135 +#163 := (< #160 #96)
   1.136 +#194 := (and #163 #189)
   1.137 +#127 := (< #124 0::real)
   1.138 +#139 := (ite #127 #134 #124)
   1.139 +#142 := (< #139 #96)
   1.140 +#197 := (and #142 #194)
   1.141 +#105 := (< #102 0::real)
   1.142 +#117 := (ite #105 #112 #102)
   1.143 +#120 := (< #117 #96)
   1.144 +#200 := (and #120 #197)
   1.145 +#80 := (< #77 0::real)
   1.146 +#92 := (ite #80 #87 #77)
   1.147 +#99 := (< #92 #96)
   1.148 +#203 := (and #99 #200)
   1.149 +#366 := (iff #203 #363)
   1.150 +#339 := (and #208 #211)
   1.151 +#342 := (and #215 #339)
   1.152 +#345 := (and #221 #342)
   1.153 +#348 := (and #345 #242)
   1.154 +#351 := (and #265 #348)
   1.155 +#354 := (and #288 #351)
   1.156 +#357 := (and #311 #354)
   1.157 +#360 := (and #334 #357)
   1.158 +#364 := (iff #360 #363)
   1.159 +#365 := [rewrite]: #364
   1.160 +#361 := (iff #203 #360)
   1.161 +#358 := (iff #200 #357)
   1.162 +#355 := (iff #197 #354)
   1.163 +#352 := (iff #194 #351)
   1.164 +#349 := (iff #189 #348)
   1.165 +#245 := (iff #183 #242)
   1.166 +#236 := (< #231 #96)
   1.167 +#243 := (iff #236 #242)
   1.168 +#244 := [rewrite]: #243
   1.169 +#237 := (iff #183 #236)
   1.170 +#234 := (= #180 #231)
   1.171 +#225 := (not #224)
   1.172 +#228 := (ite #225 #175 #166)
   1.173 +#232 := (= #228 #231)
   1.174 +#233 := [rewrite]: #232
   1.175 +#229 := (= #180 #228)
   1.176 +#226 := (iff #169 #225)
   1.177 +#227 := [rewrite]: #226
   1.178 +#230 := [monotonicity #227]: #229
   1.179 +#235 := [trans #230 #233]: #234
   1.180 +#238 := [monotonicity #235]: #237
   1.181 +#246 := [trans #238 #244]: #245
   1.182 +#346 := (iff #47 #345)
   1.183 +#343 := (iff #46 #342)
   1.184 +#340 := (iff #45 #339)
   1.185 +#213 := (iff #44 #211)
   1.186 +#214 := [rewrite]: #213
   1.187 +#209 := (iff #43 #208)
   1.188 +#210 := [rewrite]: #209
   1.189 +#341 := [monotonicity #210 #214]: #340
   1.190 +#218 := (iff #41 #215)
   1.191 +#219 := [rewrite]: #218
   1.192 +#344 := [monotonicity #219 #341]: #343
   1.193 +#222 := (iff #40 #221)
   1.194 +#223 := [rewrite]: #222
   1.195 +#347 := [monotonicity #223 #344]: #346
   1.196 +#350 := [monotonicity #347 #246]: #349
   1.197 +#268 := (iff #163 #265)
   1.198 +#259 := (< #254 #96)
   1.199 +#266 := (iff #259 #265)
   1.200 +#267 := [rewrite]: #266
   1.201 +#260 := (iff #163 #259)
   1.202 +#257 := (= #160 #254)
   1.203 +#248 := (not #247)
   1.204 +#251 := (ite #248 #155 #145)
   1.205 +#255 := (= #251 #254)
   1.206 +#256 := [rewrite]: #255
   1.207 +#252 := (= #160 #251)
   1.208 +#249 := (iff #148 #248)
   1.209 +#250 := [rewrite]: #249
   1.210 +#253 := [monotonicity #250]: #252
   1.211 +#258 := [trans #253 #256]: #257
   1.212 +#261 := [monotonicity #258]: #260
   1.213 +#269 := [trans #261 #267]: #268
   1.214 +#353 := [monotonicity #269 #350]: #352
   1.215 +#291 := (iff #142 #288)
   1.216 +#282 := (< #277 #96)
   1.217 +#289 := (iff #282 #288)
   1.218 +#290 := [rewrite]: #289
   1.219 +#283 := (iff #142 #282)
   1.220 +#280 := (= #139 #277)
   1.221 +#271 := (not #270)
   1.222 +#274 := (ite #271 #134 #124)
   1.223 +#278 := (= #274 #277)
   1.224 +#279 := [rewrite]: #278
   1.225 +#275 := (= #139 #274)
   1.226 +#272 := (iff #127 #271)
   1.227 +#273 := [rewrite]: #272
   1.228 +#276 := [monotonicity #273]: #275
   1.229 +#281 := [trans #276 #279]: #280
   1.230 +#284 := [monotonicity #281]: #283
   1.231 +#292 := [trans #284 #290]: #291
   1.232 +#356 := [monotonicity #292 #353]: #355
   1.233 +#314 := (iff #120 #311)
   1.234 +#305 := (< #300 #96)
   1.235 +#312 := (iff #305 #311)
   1.236 +#313 := [rewrite]: #312
   1.237 +#306 := (iff #120 #305)
   1.238 +#303 := (= #117 #300)
   1.239 +#294 := (not #293)
   1.240 +#297 := (ite #294 #112 #102)
   1.241 +#301 := (= #297 #300)
   1.242 +#302 := [rewrite]: #301
   1.243 +#298 := (= #117 #297)
   1.244 +#295 := (iff #105 #294)
   1.245 +#296 := [rewrite]: #295
   1.246 +#299 := [monotonicity #296]: #298
   1.247 +#304 := [trans #299 #302]: #303
   1.248 +#307 := [monotonicity #304]: #306
   1.249 +#315 := [trans #307 #313]: #314
   1.250 +#359 := [monotonicity #315 #356]: #358
   1.251 +#337 := (iff #99 #334)
   1.252 +#328 := (< #323 #96)
   1.253 +#335 := (iff #328 #334)
   1.254 +#336 := [rewrite]: #335
   1.255 +#329 := (iff #99 #328)
   1.256 +#326 := (= #92 #323)
   1.257 +#320 := (ite #317 #87 #77)
   1.258 +#324 := (= #320 #323)
   1.259 +#325 := [rewrite]: #324
   1.260 +#321 := (= #92 #320)
   1.261 +#318 := (iff #80 #317)
   1.262 +#319 := [rewrite]: #318
   1.263 +#322 := [monotonicity #319]: #321
   1.264 +#327 := [trans #322 #325]: #326
   1.265 +#330 := [monotonicity #327]: #329
   1.266 +#338 := [trans #330 #336]: #337
   1.267 +#362 := [monotonicity #338 #359]: #361
   1.268 +#367 := [trans #362 #365]: #366
   1.269 +#204 := (iff #52 #203)
   1.270 +#201 := (iff #51 #200)
   1.271 +#198 := (iff #50 #197)
   1.272 +#195 := (iff #49 #194)
   1.273 +#192 := (iff #48 #189)
   1.274 +#186 := (and #183 #47)
   1.275 +#190 := (iff #186 #189)
   1.276 +#191 := [rewrite]: #190
   1.277 +#187 := (iff #48 #186)
   1.278 +#184 := (iff #38 #183)
   1.279 +#97 := (= #13 #96)
   1.280 +#98 := [rewrite]: #97
   1.281 +#181 := (= #37 #180)
   1.282 +#167 := (= #34 #166)
   1.283 +#168 := [rewrite]: #167
   1.284 +#178 := (= #36 #175)
   1.285 +#172 := (- #166)
   1.286 +#176 := (= #172 #175)
   1.287 +#177 := [rewrite]: #176
   1.288 +#173 := (= #36 #172)
   1.289 +#174 := [monotonicity #168]: #173
   1.290 +#179 := [trans #174 #177]: #178
   1.291 +#170 := (iff #35 #169)
   1.292 +#171 := [monotonicity #168]: #170
   1.293 +#182 := [monotonicity #171 #179 #168]: #181
   1.294 +#185 := [monotonicity #182 #98]: #184
   1.295 +#188 := [monotonicity #185]: #187
   1.296 +#193 := [trans #188 #191]: #192
   1.297 +#164 := (iff #33 #163)
   1.298 +#161 := (= #32 #160)
   1.299 +#146 := (= #29 #145)
   1.300 +#147 := [rewrite]: #146
   1.301 +#158 := (= #31 #155)
   1.302 +#151 := (- #145)
   1.303 +#156 := (= #151 #155)
   1.304 +#157 := [rewrite]: #156
   1.305 +#152 := (= #31 #151)
   1.306 +#153 := [monotonicity #147]: #152
   1.307 +#159 := [trans #153 #157]: #158
   1.308 +#149 := (iff #30 #148)
   1.309 +#150 := [monotonicity #147]: #149
   1.310 +#162 := [monotonicity #150 #159 #147]: #161
   1.311 +#165 := [monotonicity #162 #98]: #164
   1.312 +#196 := [monotonicity #165 #193]: #195
   1.313 +#143 := (iff #27 #142)
   1.314 +#140 := (= #26 #139)
   1.315 +#125 := (= #23 #124)
   1.316 +#126 := [rewrite]: #125
   1.317 +#137 := (= #25 #134)
   1.318 +#130 := (- #124)
   1.319 +#135 := (= #130 #134)
   1.320 +#136 := [rewrite]: #135
   1.321 +#131 := (= #25 #130)
   1.322 +#132 := [monotonicity #126]: #131
   1.323 +#138 := [trans #132 #136]: #137
   1.324 +#128 := (iff #24 #127)
   1.325 +#129 := [monotonicity #126]: #128
   1.326 +#141 := [monotonicity #129 #138 #126]: #140
   1.327 +#144 := [monotonicity #141 #98]: #143
   1.328 +#199 := [monotonicity #144 #196]: #198
   1.329 +#121 := (iff #20 #120)
   1.330 +#118 := (= #19 #117)
   1.331 +#103 := (= #16 #102)
   1.332 +#104 := [rewrite]: #103
   1.333 +#115 := (= #18 #112)
   1.334 +#108 := (- #102)
   1.335 +#113 := (= #108 #112)
   1.336 +#114 := [rewrite]: #113
   1.337 +#109 := (= #18 #108)
   1.338 +#110 := [monotonicity #104]: #109
   1.339 +#116 := [trans #110 #114]: #115
   1.340 +#106 := (iff #17 #105)
   1.341 +#107 := [monotonicity #104]: #106
   1.342 +#119 := [monotonicity #107 #116 #104]: #118
   1.343 +#122 := [monotonicity #119 #98]: #121
   1.344 +#202 := [monotonicity #122 #199]: #201
   1.345 +#100 := (iff #14 #99)
   1.346 +#93 := (= #10 #92)
   1.347 +#78 := (= #6 #77)
   1.348 +#79 := [rewrite]: #78
   1.349 +#90 := (= #9 #87)
   1.350 +#83 := (- #77)
   1.351 +#88 := (= #83 #87)
   1.352 +#89 := [rewrite]: #88
   1.353 +#84 := (= #9 #83)
   1.354 +#85 := [monotonicity #79]: #84
   1.355 +#91 := [trans #85 #89]: #90
   1.356 +#81 := (iff #8 #80)
   1.357 +#82 := [monotonicity #79]: #81
   1.358 +#94 := [monotonicity #82 #91 #79]: #93
   1.359 +#101 := [monotonicity #94 #98]: #100
   1.360 +#205 := [monotonicity #101 #202]: #204
   1.361 +#369 := [trans #205 #367]: #368
   1.362 +#74 := [asserted]: #52
   1.363 +#370 := [mp #74 #369]: #363
   1.364 +#374 := [and-elim #370]: #221
   1.365 +#373 := [and-elim #370]: #215
   1.366 +#504 := (+ #96 #134)
   1.367 +#514 := (<= #504 0::real)
   1.368 +#635 := (not #514)
   1.369 +#456 := -1/3::real
   1.370 +#457 := (* -1/3::real uf_3)
   1.371 +#544 := (+ #457 #111)
   1.372 +#545 := (+ uf_2 #544)
   1.373 +#546 := (>= #545 0::real)
   1.374 +#390 := (+ #216 uf_9)
   1.375 +#593 := (+ uf_3 #390)
   1.376 +#603 := (<= #593 0::real)
   1.377 +#381 := (+ uf_8 #206)
   1.378 +#404 := (>= #381 0::real)
   1.379 +#594 := (+ uf_3 #381)
   1.380 +#604 := (<= #594 0::real)
   1.381 +#736 := (not #604)
   1.382 +#477 := (+ #96 #155)
   1.383 +#487 := (<= #477 0::real)
   1.384 +#733 := [hypothesis]: #604
   1.385 +#564 := (+ #76 #96)
   1.386 +#565 := (+ uf_1 #564)
   1.387 +#577 := (<= #565 0::real)
   1.388 +#767 := (or #577 #736)
   1.389 +#658 := (not #577)
   1.390 +#673 := [hypothesis]: #658
   1.391 +#478 := (+ #96 #145)
   1.392 +#488 := (<= #478 0::real)
   1.393 +#628 := (not #488)
   1.394 +#446 := (+ #96 #123)
   1.395 +#447 := (+ uf_2 #446)
   1.396 +#461 := (<= #447 0::real)
   1.397 +#618 := (not #461)
   1.398 +#754 := (or #224 #736)
   1.399 +#625 := (not #487)
   1.400 +#718 := [hypothesis]: #225
   1.401 +#744 := (or #577 #736 #224)
   1.402 +#681 := (or #224 #618)
   1.403 +#458 := (+ #457 #123)
   1.404 +#459 := (+ uf_2 #458)
   1.405 +#460 := (>= #459 0::real)
   1.406 +#462 := (ite #224 #460 #461)
   1.407 +#467 := (not #462)
   1.408 +#468 := (iff #242 #467)
   1.409 +#465 := (iff #241 #462)
   1.410 +#444 := (+ #96 uf_6)
   1.411 +#445 := (+ #76 #444)
   1.412 +#448 := (ite #224 #445 #447)
   1.413 +#453 := (<= #448 0::real)
   1.414 +#463 := (iff #453 #462)
   1.415 +#464 := [rewrite]: #463
   1.416 +#454 := (iff #241 #453)
   1.417 +#451 := (= #240 #448)
   1.418 +#439 := (ite #224 #175 #166)
   1.419 +#441 := (+ #96 #439)
   1.420 +#449 := (= #441 #448)
   1.421 +#450 := [rewrite]: #449
   1.422 +#442 := (= #240 #441)
   1.423 +#437 := (= #239 #439)
   1.424 +#440 := [rewrite]: #437
   1.425 +#443 := [monotonicity #440]: #442
   1.426 +#452 := [trans #443 #450]: #451
   1.427 +#455 := [monotonicity #452]: #454
   1.428 +#466 := [trans #455 #464]: #465
   1.429 +#469 := [monotonicity #466]: #468
   1.430 +#375 := [and-elim #370]: #242
   1.431 +#470 := [mp #375 #469]: #467
   1.432 +#619 := (or #462 #224 #618)
   1.433 +#620 := [def-axiom]: #619
   1.434 +#682 := [unit-resolution #620 #470]: #681
   1.435 +#719 := [unit-resolution #682 #718]: #618
   1.436 +#737 := (or #487 #461 #736 #577)
   1.437 +#372 := [and-elim #370]: #211
   1.438 +#734 := [hypothesis]: #625
   1.439 +#675 := [hypothesis]: #618
   1.440 +#735 := [th-lemma #675 #374 #734 #372 #733 #673]: false
   1.441 +#738 := [lemma #735]: #737
   1.442 +#739 := [unit-resolution #738 #673 #733 #719]: #487
   1.443 +#740 := (or #248 #625)
   1.444 +#489 := (ite #247 #487 #488)
   1.445 +#494 := (not #489)
   1.446 +#495 := (iff #265 #494)
   1.447 +#492 := (iff #264 #489)
   1.448 +#479 := (ite #247 #477 #478)
   1.449 +#484 := (<= #479 0::real)
   1.450 +#490 := (iff #484 #489)
   1.451 +#491 := [rewrite]: #490
   1.452 +#485 := (iff #264 #484)
   1.453 +#482 := (= #263 #479)
   1.454 +#471 := (ite #247 #155 #145)
   1.455 +#474 := (+ #96 #471)
   1.456 +#480 := (= #474 #479)
   1.457 +#481 := [rewrite]: #480
   1.458 +#475 := (= #263 #474)
   1.459 +#472 := (= #262 #471)
   1.460 +#473 := [rewrite]: #472
   1.461 +#476 := [monotonicity #473]: #475
   1.462 +#483 := [trans #476 #481]: #482
   1.463 +#486 := [monotonicity #483]: #485
   1.464 +#493 := [trans #486 #491]: #492
   1.465 +#496 := [monotonicity #493]: #495
   1.466 +#376 := [and-elim #370]: #265
   1.467 +#497 := [mp #376 #496]: #494
   1.468 +#626 := (or #489 #248 #625)
   1.469 +#627 := [def-axiom]: #626
   1.470 +#741 := [unit-resolution #627 #497]: #740
   1.471 +#742 := [unit-resolution #741 #739]: #248
   1.472 +#743 := [th-lemma #673 #719 #372 #733 #742 #718 #374]: false
   1.473 +#745 := [lemma #743]: #744
   1.474 +#746 := [unit-resolution #745 #718 #733]: #577
   1.475 +#727 := (or #316 #658)
   1.476 +#574 := (+ #76 #457)
   1.477 +#575 := (+ uf_1 #574)
   1.478 +#576 := (>= #575 0::real)
   1.479 +#578 := (ite #316 #576 #577)
   1.480 +#583 := (not #578)
   1.481 +#584 := (iff #334 #583)
   1.482 +#581 := (iff #333 #578)
   1.483 +#562 := (+ uf_2 #96)
   1.484 +#563 := (+ #86 #562)
   1.485 +#566 := (ite #316 #563 #565)
   1.486 +#571 := (<= #566 0::real)
   1.487 +#579 := (iff #571 #578)
   1.488 +#580 := [rewrite]: #579
   1.489 +#572 := (iff #333 #571)
   1.490 +#569 := (= #332 #566)
   1.491 +#556 := (ite #316 #87 #77)
   1.492 +#559 := (+ #96 #556)
   1.493 +#567 := (= #559 #566)
   1.494 +#568 := [rewrite]: #567
   1.495 +#560 := (= #332 #559)
   1.496 +#557 := (= #331 #556)
   1.497 +#558 := [rewrite]: #557
   1.498 +#561 := [monotonicity #558]: #560
   1.499 +#570 := [trans #561 #568]: #569
   1.500 +#573 := [monotonicity #570]: #572
   1.501 +#582 := [trans #573 #580]: #581
   1.502 +#585 := [monotonicity #582]: #584
   1.503 +#379 := [and-elim #370]: #334
   1.504 +#586 := [mp #379 #585]: #583
   1.505 +#659 := (or #578 #316 #658)
   1.506 +#660 := [def-axiom]: #659
   1.507 +#728 := [unit-resolution #660 #586]: #727
   1.508 +#747 := [unit-resolution #728 #746]: #316
   1.509 +#748 := (not #211)
   1.510 +#710 := (not #221)
   1.511 +#749 := (or #247 #461 #710 #748 #736 #224 #317)
   1.512 +#750 := [th-lemma]: #749
   1.513 +#751 := [unit-resolution #750 #718 #374 #719 #372 #747 #733]: #247
   1.514 +#752 := [unit-resolution #741 #751]: #625
   1.515 +#753 := [th-lemma #719 #372 #733 #718 #747 #752 #374]: false
   1.516 +#755 := [lemma #753]: #754
   1.517 +#756 := [unit-resolution #755 #733]: #224
   1.518 +#615 := (not #460)
   1.519 +#757 := (or #225 #615)
   1.520 +#616 := (or #462 #225 #615)
   1.521 +#617 := [def-axiom]: #616
   1.522 +#758 := [unit-resolution #617 #470]: #757
   1.523 +#759 := [unit-resolution #758 #756]: #615
   1.524 +#760 := (or #618 #460 #225)
   1.525 +#761 := [th-lemma]: #760
   1.526 +#762 := [unit-resolution #761 #759 #756]: #618
   1.527 +#763 := [unit-resolution #738 #673 #733 #762]: #487
   1.528 +#764 := [unit-resolution #741 #763]: #248
   1.529 +#701 := (or #247 #628)
   1.530 +#629 := (or #489 #247 #628)
   1.531 +#630 := [def-axiom]: #629
   1.532 +#702 := [unit-resolution #630 #497]: #701
   1.533 +#765 := [unit-resolution #702 #764]: #628
   1.534 +#766 := [th-lemma #756 #374 #372 #733 #764 #765 #673]: false
   1.535 +#768 := [lemma #766]: #767
   1.536 +#769 := [unit-resolution #768 #733]: #577
   1.537 +#770 := [unit-resolution #728 #769]: #316
   1.538 +#771 := (or #487 #710 #748 #736 #225 #317 #460)
   1.539 +#772 := [th-lemma]: #771
   1.540 +#773 := [unit-resolution #772 #756 #374 #759 #372 #770 #733]: #487
   1.541 +#774 := (or #247 #460 #225 #710 #748 #736 #317)
   1.542 +#775 := [th-lemma]: #774
   1.543 +#776 := [unit-resolution #775 #756 #374 #759 #372 #770 #733]: #247
   1.544 +#777 := [unit-resolution #741 #776 #773]: false
   1.545 +#778 := [lemma #777]: #736
   1.546 +#668 := (or #404 #604)
   1.547 +#605 := (ite #404 #603 #604)
   1.548 +#411 := (ite #404 #381 #390)
   1.549 +#419 := (* -1::real #411)
   1.550 +#420 := (+ uf_3 #419)
   1.551 +#421 := (<= #420 0::real)
   1.552 +#608 := (iff #421 #605)
   1.553 +#595 := (ite #404 #593 #594)
   1.554 +#600 := (<= #595 0::real)
   1.555 +#606 := (iff #600 #605)
   1.556 +#607 := [rewrite]: #606
   1.557 +#601 := (iff #421 #600)
   1.558 +#598 := (= #420 #595)
   1.559 +#587 := (ite #404 #390 #381)
   1.560 +#590 := (+ uf_3 #587)
   1.561 +#596 := (= #590 #595)
   1.562 +#597 := [rewrite]: #596
   1.563 +#591 := (= #420 #590)
   1.564 +#588 := (= #419 #587)
   1.565 +#589 := [rewrite]: #588
   1.566 +#592 := [monotonicity #589]: #591
   1.567 +#599 := [trans #592 #597]: #598
   1.568 +#602 := [monotonicity #599]: #601
   1.569 +#609 := [trans #602 #607]: #608
   1.570 +#53 := (- uf_8 uf_9)
   1.571 +#55 := (- #53)
   1.572 +#54 := (< #53 0::real)
   1.573 +#56 := (ite #54 #55 #53)
   1.574 +#57 := (< #56 uf_3)
   1.575 +#58 := (not #57)
   1.576 +#434 := (iff #58 #421)
   1.577 +#384 := (< #381 0::real)
   1.578 +#395 := (ite #384 #390 #381)
   1.579 +#398 := (< #395 uf_3)
   1.580 +#401 := (not #398)
   1.581 +#432 := (iff #401 #421)
   1.582 +#422 := (not #421)
   1.583 +#427 := (not #422)
   1.584 +#430 := (iff #427 #421)
   1.585 +#431 := [rewrite]: #430
   1.586 +#428 := (iff #401 #427)
   1.587 +#425 := (iff #398 #422)
   1.588 +#416 := (< #411 uf_3)
   1.589 +#423 := (iff #416 #422)
   1.590 +#424 := [rewrite]: #423
   1.591 +#417 := (iff #398 #416)
   1.592 +#414 := (= #395 #411)
   1.593 +#405 := (not #404)
   1.594 +#408 := (ite #405 #390 #381)
   1.595 +#412 := (= #408 #411)
   1.596 +#413 := [rewrite]: #412
   1.597 +#409 := (= #395 #408)
   1.598 +#406 := (iff #384 #405)
   1.599 +#407 := [rewrite]: #406
   1.600 +#410 := [monotonicity #407]: #409
   1.601 +#415 := [trans #410 #413]: #414
   1.602 +#418 := [monotonicity #415]: #417
   1.603 +#426 := [trans #418 #424]: #425
   1.604 +#429 := [monotonicity #426]: #428
   1.605 +#433 := [trans #429 #431]: #432
   1.606 +#402 := (iff #58 #401)
   1.607 +#399 := (iff #57 #398)
   1.608 +#396 := (= #56 #395)
   1.609 +#382 := (= #53 #381)
   1.610 +#383 := [rewrite]: #382
   1.611 +#393 := (= #55 #390)
   1.612 +#387 := (- #381)
   1.613 +#391 := (= #387 #390)
   1.614 +#392 := [rewrite]: #391
   1.615 +#388 := (= #55 #387)
   1.616 +#389 := [monotonicity #383]: #388
   1.617 +#394 := [trans #389 #392]: #393
   1.618 +#385 := (iff #54 #384)
   1.619 +#386 := [monotonicity #383]: #385
   1.620 +#397 := [monotonicity #386 #394 #383]: #396
   1.621 +#400 := [monotonicity #397]: #399
   1.622 +#403 := [monotonicity #400]: #402
   1.623 +#435 := [trans #403 #433]: #434
   1.624 +#380 := [asserted]: #58
   1.625 +#436 := [mp #380 #435]: #421
   1.626 +#610 := [mp #436 #609]: #605
   1.627 +#661 := (not #605)
   1.628 +#666 := (or #404 #604 #661)
   1.629 +#667 := [def-axiom]: #666
   1.630 +#669 := [unit-resolution #667 #610]: #668
   1.631 +#700 := [unit-resolution #669 #778]: #404
   1.632 +#664 := (or #405 #603)
   1.633 +#662 := (or #405 #603 #661)
   1.634 +#663 := [def-axiom]: #662
   1.635 +#665 := [unit-resolution #663 #610]: #664
   1.636 +#703 := [unit-resolution #665 #700]: #603
   1.637 +#677 := (not #603)
   1.638 +#731 := (or #677 #546)
   1.639 +#648 := (not #546)
   1.640 +#672 := [hypothesis]: #648
   1.641 +#671 := [hypothesis]: #603
   1.642 +#723 := (or #224 #677 #546)
   1.643 +#689 := (or #461 #546 #677 #514)
   1.644 +#687 := [hypothesis]: #635
   1.645 +#371 := [and-elim #370]: #208
   1.646 +#688 := [th-lemma #373 #672 #371 #671 #675 #687]: false
   1.647 +#690 := [lemma #688]: #689
   1.648 +#720 := [unit-resolution #690 #719 #671 #672]: #514
   1.649 +#692 := (or #271 #635)
   1.650 +#505 := (+ #96 #124)
   1.651 +#515 := (<= #505 0::real)
   1.652 +#516 := (ite #270 #514 #515)
   1.653 +#521 := (not #516)
   1.654 +#522 := (iff #288 #521)
   1.655 +#519 := (iff #287 #516)
   1.656 +#506 := (ite #270 #504 #505)
   1.657 +#511 := (<= #506 0::real)
   1.658 +#517 := (iff #511 #516)
   1.659 +#518 := [rewrite]: #517
   1.660 +#512 := (iff #287 #511)
   1.661 +#509 := (= #286 #506)
   1.662 +#498 := (ite #270 #134 #124)
   1.663 +#501 := (+ #96 #498)
   1.664 +#507 := (= #501 #506)
   1.665 +#508 := [rewrite]: #507
   1.666 +#502 := (= #286 #501)
   1.667 +#499 := (= #285 #498)
   1.668 +#500 := [rewrite]: #499
   1.669 +#503 := [monotonicity #500]: #502
   1.670 +#510 := [trans #503 #508]: #509
   1.671 +#513 := [monotonicity #510]: #512
   1.672 +#520 := [trans #513 #518]: #519
   1.673 +#523 := [monotonicity #520]: #522
   1.674 +#377 := [and-elim #370]: #288
   1.675 +#524 := [mp #377 #523]: #521
   1.676 +#636 := (or #516 #271 #635)
   1.677 +#637 := [def-axiom]: #636
   1.678 +#693 := [unit-resolution #637 #524]: #692
   1.679 +#721 := [unit-resolution #693 #720]: #271
   1.680 +#722 := [th-lemma #719 #373 #371 #671 #721 #718 #672]: false
   1.681 +#724 := [lemma #722]: #723
   1.682 +#725 := [unit-resolution #724 #671 #672]: #224
   1.683 +#716 := (or #225 #317 #546 #677)
   1.684 +#704 := [hypothesis]: #224
   1.685 +#708 := [hypothesis]: #316
   1.686 +#709 := (not #215)
   1.687 +#711 := (or #270 #709 #317 #225 #710)
   1.688 +#712 := [th-lemma]: #711
   1.689 +#713 := [unit-resolution #712 #704 #374 #373 #708]: #270
   1.690 +#714 := [unit-resolution #693 #713]: #635
   1.691 +#715 := [th-lemma #708 #672 #371 #671 #714 #373 #704 #374]: false
   1.692 +#717 := [lemma #715]: #716
   1.693 +#726 := [unit-resolution #717 #725 #672 #671]: #317
   1.694 +#729 := [unit-resolution #728 #726]: #658
   1.695 +#698 := (or #316 #546 #677 #577)
   1.696 +#674 := [hypothesis]: #317
   1.697 +#685 := (or #270 #316 #577 #546 #677)
   1.698 +#670 := [hypothesis]: #271
   1.699 +#678 := (or #461 #316 #577 #546 #677 #270)
   1.700 +#676 := [th-lemma #675 #674 #673 #672 #371 #671 #670 #373]: false
   1.701 +#679 := [lemma #676]: #678
   1.702 +#680 := [unit-resolution #679 #670 #673 #672 #671 #674]: #461
   1.703 +#683 := [unit-resolution #682 #680]: #224
   1.704 +#684 := [th-lemma #674 #673 #672 #371 #671 #670 #683 #373]: false
   1.705 +#686 := [lemma #684]: #685
   1.706 +#691 := [unit-resolution #686 #674 #673 #672 #671]: #270
   1.707 +#694 := [unit-resolution #693 #691]: #635
   1.708 +#695 := [unit-resolution #690 #694 #671 #672]: #461
   1.709 +#696 := [unit-resolution #682 #695]: #224
   1.710 +#697 := [th-lemma #373 #672 #371 #671 #696 #674 #673 #694]: false
   1.711 +#699 := [lemma #697]: #698
   1.712 +#730 := [unit-resolution #699 #729 #726 #671 #672]: false
   1.713 +#732 := [lemma #730]: #731
   1.714 +#705 := [unit-resolution #732 #703]: #546
   1.715 +#706 := (or #293 #648)
   1.716 +#531 := (+ #96 #111)
   1.717 +#532 := (+ uf_2 #531)
   1.718 +#543 := (<= #532 0::real)
   1.719 +#547 := (ite #293 #543 #546)
   1.720 +#552 := (not #547)
   1.721 +#553 := (iff #311 #552)
   1.722 +#550 := (iff #310 #547)
   1.723 +#533 := (+ #96 uf_4)
   1.724 +#534 := (+ #76 #533)
   1.725 +#535 := (ite #293 #532 #534)
   1.726 +#540 := (<= #535 0::real)
   1.727 +#548 := (iff #540 #547)
   1.728 +#549 := [rewrite]: #548
   1.729 +#541 := (iff #310 #540)
   1.730 +#538 := (= #309 #535)
   1.731 +#525 := (ite #293 #112 #102)
   1.732 +#528 := (+ #96 #525)
   1.733 +#536 := (= #528 #535)
   1.734 +#537 := [rewrite]: #536
   1.735 +#529 := (= #309 #528)
   1.736 +#526 := (= #308 #525)
   1.737 +#527 := [rewrite]: #526
   1.738 +#530 := [monotonicity #527]: #529
   1.739 +#539 := [trans #530 #537]: #538
   1.740 +#542 := [monotonicity #539]: #541
   1.741 +#551 := [trans #542 #549]: #550
   1.742 +#554 := [monotonicity #551]: #553
   1.743 +#378 := [and-elim #370]: #311
   1.744 +#555 := [mp #378 #554]: #552
   1.745 +#649 := (or #547 #293 #648)
   1.746 +#650 := [def-axiom]: #649
   1.747 +#707 := [unit-resolution #650 #555]: #706
   1.748 +#779 := [unit-resolution #707 #705]: #293
   1.749 +#783 := (or #224 #270 #461)
   1.750 +#780 := (not #208)
   1.751 +#781 := (or #294 #709 #224 #780 #677 #270 #461)
   1.752 +#782 := [th-lemma]: #781
   1.753 +#784 := [unit-resolution #782 #373 #703 #779 #371]: #783
   1.754 +#785 := [unit-resolution #784 #719 #718]: #270
   1.755 +#786 := [unit-resolution #693 #785]: #635
   1.756 +#787 := [th-lemma #718 #719 #786 #373 #371 #703 #779]: false
   1.757 +#788 := [lemma #787]: #224
   1.758 +#798 := (or #270 #317 #225)
   1.759 +#799 := [unit-resolution #712 #374 #373]: #798
   1.760 +#800 := [unit-resolution #799 #708 #788]: #270
   1.761 +#801 := [unit-resolution #693 #800]: #635
   1.762 +#802 := [th-lemma #708 #779 #371 #703 #788 #801 #373 #374]: false
   1.763 +#803 := [lemma #802]: #317
   1.764 +#804 := [unit-resolution #728 #803]: #658
   1.765 +#796 := (or #316 #577)
   1.766 +#789 := (or #514 #294 #225 #709 #780 #677 #577 #316)
   1.767 +#790 := [th-lemma]: #789
   1.768 +#791 := [unit-resolution #790 #674 #788 #371 #779 #373 #673 #703]: #514
   1.769 +#792 := (or #270 #577 #316 #294 #225 #709 #780 #677)
   1.770 +#793 := [th-lemma]: #792
   1.771 +#794 := [unit-resolution #793 #674 #788 #371 #779 #373 #673 #703]: #270
   1.772 +#795 := [unit-resolution #693 #794 #791]: false
   1.773 +#797 := [lemma #795]: #796
   1.774 +[unit-resolution #797 #804 #803]: false
   1.775 +unsat
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Apr 09 13:35:54 2010 +0200
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Apr 20 14:07:52 2010 +0200
     2.3 @@ -8,9 +8,11 @@
     2.4  begin
     2.5  
     2.6  declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]]
     2.7 -declare [[smt_fixed=true]]
     2.8 +declare [[smt_fixed=false]]
     2.9  declare [[z3_proofs=true]]
    2.10  
    2.11 +subsection {* Sundries *}
    2.12 +
    2.13  lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
    2.14  lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
    2.15  lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
    2.16 @@ -18,6 +20,81 @@
    2.17  
    2.18  declare smult_conv_scaleR[simp]
    2.19  
    2.20 +lemma simple_image: "{f x |x . x \<in> s} = f ` s" by blast
    2.21 +
    2.22 +lemma linear_simps:  assumes "bounded_linear f"
    2.23 +  shows "f (a + b) = f a + f b" "f (a - b) = f a - f b" "f 0 = 0" "f (- a) = - f a" "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
    2.24 +  apply(rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR)
    2.25 +  using assms unfolding bounded_linear_def additive_def by auto
    2.26 +
    2.27 +lemma bounded_linearI:assumes "\<And>x y. f (x + y) = f x + f y"
    2.28 +  "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
    2.29 +  shows "bounded_linear f"
    2.30 +  unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
    2.31 + 
    2.32 +lemma real_le_inf_subset:
    2.33 +  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s" shows "Inf s <= Inf (t::real set)"
    2.34 +  apply(rule isGlb_le_isLb) apply(rule Inf[OF assms(1)])
    2.35 +  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
    2.36 +  unfolding isLb_def setge_def by auto
    2.37 +
    2.38 +lemma real_ge_sup_subset:
    2.39 +  assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. s *<= b" shows "Sup s >= Sup (t::real set)"
    2.40 +  apply(rule isLub_le_isUb) apply(rule Sup[OF assms(1)])
    2.41 +  using assms apply-apply(erule exE) apply(rule_tac x=b in exI)
    2.42 +  unfolding isUb_def setle_def by auto
    2.43 +
    2.44 +lemma dist_trans[simp]:"dist (vec1 x) (vec1 y) = dist x (y::real)"
    2.45 +  unfolding dist_real_def dist_vec1 ..
    2.46 +
    2.47 +lemma Lim_trans[simp]: fixes f::"'a \<Rightarrow> real"
    2.48 +  shows "((\<lambda>x. vec1 (f x)) ---> vec1 l) net \<longleftrightarrow> (f ---> l) net"
    2.49 +  using assms unfolding Lim dist_trans ..
    2.50 +
    2.51 +lemma bounded_linear_component[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
    2.52 +  apply(rule bounded_linearI[where K=1]) 
    2.53 +  using component_le_norm[of _ k] unfolding real_norm_def by auto
    2.54 +
    2.55 +lemma bounded_vec1[intro]:  "bounded s \<Longrightarrow> bounded (vec1 ` (s::real set))"
    2.56 +  unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI) by auto
    2.57 +
    2.58 +lemma transitive_stepwise_lt_eq:
    2.59 +  assumes "(\<And>x y z::nat. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z)"
    2.60 +  shows "((\<forall>m. \<forall>n>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n)))" (is "?l = ?r")
    2.61 +proof(safe) assume ?r fix n m::nat assume "m < n" thus "R m n" apply-
    2.62 +  proof(induct n arbitrary: m) case (Suc n) show ?case 
    2.63 +    proof(cases "m < n") case True
    2.64 +      show ?thesis apply(rule assms[OF Suc(1)[OF True]]) using `?r` by auto
    2.65 +    next case False hence "m = n" using Suc(2) by auto
    2.66 +      thus ?thesis using `?r` by auto
    2.67 +    qed qed auto qed auto
    2.68 +
    2.69 +lemma transitive_stepwise_gt:
    2.70 +  assumes "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
    2.71 +  shows "\<forall>n>m. R m n"
    2.72 +proof- have "\<forall>m. \<forall>n>m. R m n" apply(subst transitive_stepwise_lt_eq)
    2.73 +    apply(rule assms) apply(assumption,assumption) using assms(2) by auto
    2.74 +  thus ?thesis by auto qed
    2.75 +
    2.76 +lemma transitive_stepwise_le_eq:
    2.77 +  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
    2.78 +  shows "(\<forall>m. \<forall>n\<ge>m. R m n) \<longleftrightarrow> (\<forall>n. R n (Suc n))" (is "?l = ?r")
    2.79 +proof safe assume ?r fix m n::nat assume "m\<le>n" thus "R m n" apply-
    2.80 +  proof(induct n arbitrary: m) case (Suc n) show ?case 
    2.81 +    proof(cases "m \<le> n") case True show ?thesis apply(rule assms(2))
    2.82 +        apply(rule Suc(1)[OF True]) using `?r` by auto
    2.83 +    next case False hence "m = Suc n" using Suc(2) by auto
    2.84 +      thus ?thesis using assms(1) by auto
    2.85 +    qed qed(insert assms(1), auto) qed auto
    2.86 +
    2.87 +lemma transitive_stepwise_le:
    2.88 +  assumes "\<And>x. R x x" "\<And>x y z. R x y \<Longrightarrow> R y z \<Longrightarrow> R x z" "\<And>n. R n (Suc n) "
    2.89 +  shows "\<forall>n\<ge>m. R m n"
    2.90 +proof- have "\<forall>m. \<forall>n\<ge>m. R m n" apply(subst transitive_stepwise_le_eq)
    2.91 +    apply(rule assms) apply(rule assms,assumption,assumption) using assms(3) by auto
    2.92 +  thus ?thesis by auto qed
    2.93 +
    2.94 +
    2.95  subsection {* Some useful lemmas about intervals. *}
    2.96  
    2.97  lemma empty_as_interval: "{} = {1..0::real^'n}"
    2.98 @@ -1246,6 +1323,10 @@
    2.99    apply(drule has_integral_linear,assumption,assumption) unfolding has_integral_integral[THEN sym]
   2.100    apply(rule integrable_linear) by assumption+
   2.101  
   2.102 +lemma integral_component_eq[simp]: fixes f::"real^'n \<Rightarrow> real^'m"
   2.103 +  assumes "f integrable_on s" shows "integral s (\<lambda>x. f x $ k) = integral s f $ k"
   2.104 +  using integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] .
   2.105 +
   2.106  lemma has_integral_setsum:
   2.107    assumes "finite t" "\<forall>a\<in>t. ((f a) has_integral (i a)) s"
   2.108    shows "((\<lambda>x. setsum (\<lambda>a. f a x) t) has_integral (setsum i t)) s"
   2.109 @@ -2225,22 +2306,22 @@
   2.110    shows "dest_vec1(integral s f) \<le> dest_vec1(integral s g)"
   2.111    apply(rule has_integral_dest_vec1_le) apply(rule_tac[1-2] integrable_integral) using assms by auto
   2.112  
   2.113 -lemma has_integral_component_pos: fixes f::"real^'n \<Rightarrow> real^'m"
   2.114 +lemma has_integral_component_nonneg: fixes f::"real^'n \<Rightarrow> real^'m"
   2.115    assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> (f x)$k" shows "0 \<le> i$k"
   2.116    using has_integral_component_le[OF has_integral_0 assms(1)] using assms(2) by auto
   2.117  
   2.118 -lemma integral_component_pos: fixes f::"real^'n \<Rightarrow> real^'m"
   2.119 +lemma integral_component_nonneg: fixes f::"real^'n \<Rightarrow> real^'m"
   2.120    assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> (f x)$k" shows "0 \<le> (integral s f)$k"
   2.121 -  apply(rule has_integral_component_pos) using assms by auto
   2.122 -
   2.123 -lemma has_integral_dest_vec1_pos: fixes f::"real^'n \<Rightarrow> real^1"
   2.124 +  apply(rule has_integral_component_nonneg) using assms by auto
   2.125 +
   2.126 +lemma has_integral_dest_vec1_nonneg: fixes f::"real^'n \<Rightarrow> real^1"
   2.127    assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> i"
   2.128 -  using has_integral_component_pos[OF assms(1), of 1]
   2.129 +  using has_integral_component_nonneg[OF assms(1), of 1]
   2.130    using assms(2) unfolding vector_le_def by auto
   2.131  
   2.132 -lemma integral_dest_vec1_pos: fixes f::"real^'n \<Rightarrow> real^1"
   2.133 +lemma integral_dest_vec1_nonneg: fixes f::"real^'n \<Rightarrow> real^1"
   2.134    assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> integral s f"
   2.135 -  apply(rule has_integral_dest_vec1_pos) using assms by auto
   2.136 +  apply(rule has_integral_dest_vec1_nonneg) using assms by auto
   2.137  
   2.138  lemma has_integral_component_neg: fixes f::"real^'n \<Rightarrow> real^'m"
   2.139    assumes "(f has_integral i) s" "\<forall>x\<in>s. (f x)$k \<le> 0" shows "i$k \<le> 0"
   2.140 @@ -3779,6 +3860,57 @@
   2.141        thus False by auto qed
   2.142      thus ?l using y unfolding s by auto qed qed 
   2.143  
   2.144 +lemma has_integral_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
   2.145 +  "((\<lambda>x. vec1 (f x)) has_integral vec1 i) s \<longleftrightarrow> (f has_integral i) s"
   2.146 +  unfolding has_integral'[unfolded has_integral] 
   2.147 +proof case goal1 thus ?case apply safe
   2.148 +  apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe)
   2.149 +  apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) 
   2.150 +  apply(rule_tac x="dest_vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) 
   2.151 +  apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe)
   2.152 +  apply(subst(asm)(2) norm_vector_1) unfolding split_def
   2.153 +  unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1]
   2.154 +    Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption
   2.155 +  apply(subst(asm)(2) norm_vector_1) by auto
   2.156 +next case goal2 thus ?case apply safe
   2.157 +  apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe)
   2.158 +  apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) 
   2.159 +  apply(rule_tac x="vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) 
   2.160 +  apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe)
   2.161 +  apply(subst norm_vector_1) unfolding split_def
   2.162 +  unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1]
   2.163 +    Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption
   2.164 +  apply(subst norm_vector_1) by auto qed
   2.165 +
   2.166 +lemma integral_trans[simp]: assumes "(f::real^'n \<Rightarrow> real) integrable_on s"
   2.167 +  shows "integral s (\<lambda>x. vec1 (f x)) = vec1 (integral s f)"
   2.168 +  apply(rule integral_unique) using assms by auto
   2.169 +
   2.170 +lemma integrable_on_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
   2.171 +  "(\<lambda>x. vec1 (f x)) integrable_on s \<longleftrightarrow> (f integrable_on s)"
   2.172 +  unfolding integrable_on_def
   2.173 +  apply(subst(2) vec1_dest_vec1(1)[THEN sym]) unfolding has_integral_trans
   2.174 +  apply safe defer apply(rule_tac x="vec1 y" in exI) by auto
   2.175 +
   2.176 +lemma has_integral_le: fixes f::"real^'n \<Rightarrow> real"
   2.177 +  assumes "(f has_integral i) s" "(g has_integral j) s"  "\<forall>x\<in>s. (f x) \<le> (g x)"
   2.178 +  shows "i \<le> j" using has_integral_component_le[of "vec1 o f" "vec1 i" s "vec1 o g" "vec1 j" 1]
   2.179 +  unfolding o_def using assms by auto 
   2.180 +
   2.181 +lemma integral_le: fixes f::"real^'n \<Rightarrow> real"
   2.182 +  assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. f x \<le> g x"
   2.183 +  shows "integral s f \<le> integral s g"
   2.184 +  using has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)] .
   2.185 +
   2.186 +lemma has_integral_nonneg: fixes f::"real^'n \<Rightarrow> real"
   2.187 +  assumes "(f has_integral i) s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> i" 
   2.188 +  using has_integral_component_nonneg[of "vec1 o f" "vec1 i" s 1]
   2.189 +  unfolding o_def using assms by auto
   2.190 +
   2.191 +lemma integral_nonneg: fixes f::"real^'n \<Rightarrow> real"
   2.192 +  assumes "f integrable_on s" "\<forall>x\<in>s. 0 \<le> f x" shows "0 \<le> integral s f" 
   2.193 +  using has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)] .
   2.194 +
   2.195  subsection {* Hence a general restriction property. *}
   2.196  
   2.197  lemma has_integral_restrict[simp]: assumes "s \<subseteq> t" shows
   2.198 @@ -3875,11 +4007,21 @@
   2.199    note assms(2-3)[unfolded this] note * = has_integral_component_le[OF this]
   2.200    show ?thesis apply(rule *) using assms(1,4) by auto qed
   2.201  
   2.202 +lemma has_integral_subset_le: fixes f::"real^'n \<Rightarrow> real"
   2.203 +  assumes "s \<subseteq> t" "(f has_integral i) s" "(f has_integral j) t" "\<forall>x\<in>t. 0 \<le> f(x)"
   2.204 +  shows "i \<le> j" using has_integral_subset_component_le[OF assms(1), of "vec1 o f" "vec1 i" "vec1 j" 1]
   2.205 +  unfolding o_def using assms by auto
   2.206 +
   2.207  lemma integral_subset_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
   2.208    assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)$k"
   2.209    shows "(integral s f)$k \<le> (integral t f)$k"
   2.210    apply(rule has_integral_subset_component_le) using assms by auto
   2.211  
   2.212 +lemma integral_subset_le: fixes f::"real^'n \<Rightarrow> real"
   2.213 +  assumes "s \<subseteq> t" "f integrable_on s" "f integrable_on t" "\<forall>x \<in> t. 0 \<le> f(x)"
   2.214 +  shows "(integral s f) \<le> (integral t f)"
   2.215 +  apply(rule has_integral_subset_le) using assms by auto
   2.216 +
   2.217  lemma has_integral_alt': fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.218    shows "(f has_integral i) s \<longleftrightarrow> (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
   2.219    (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> {a..b} \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e)" (is "?l = ?r")
   2.220 @@ -3909,6 +4051,1478 @@
   2.221        from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed 
   2.222  
   2.223  
   2.224 +subsection {* Continuity of the integral (for a 1-dimensional interval). *}
   2.225 +
   2.226 +lemma integrable_alt: fixes f::"real^'n \<Rightarrow> 'a::banach" shows 
   2.227 +  "f integrable_on s \<longleftrightarrow>
   2.228 +          (\<forall>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}) \<and>
   2.229 +          (\<forall>e>0. \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
   2.230 +  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) -
   2.231 +          integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e)" (is "?l = ?r")
   2.232 +proof assume ?l then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]]
   2.233 +  note y=conjunctD2[OF this,rule_format] show ?r apply safe apply(rule y)
   2.234 +  proof- case goal1 hence "e/2 > 0" by auto from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format]
   2.235 +    show ?case apply(rule,rule,rule B)
   2.236 +    proof safe case goal1 show ?case apply(rule norm_triangle_half_l)
   2.237 +        using B(2)[OF goal1(1)] B(2)[OF goal1(2)] by auto qed qed
   2.238 +        
   2.239 +next assume ?r note as = conjunctD2[OF this,rule_format]
   2.240 +  have "Cauchy (\<lambda>n. integral ({(\<chi> i. - real n) .. (\<chi> i. real n)}) (\<lambda>x. if x \<in> s then f x else 0))"
   2.241 +  proof(unfold Cauchy_def,safe) case goal1
   2.242 +    from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format]
   2.243 +    from real_arch_simple[of B] guess N .. note N = this
   2.244 +    { fix n assume n:"n \<ge> N" have "ball 0 B \<subseteq> {\<chi> i. - real n..\<chi> i. real n}" apply safe
   2.245 +        unfolding mem_ball mem_interval vector_dist_norm
   2.246 +      proof case goal1 thus ?case using component_le_norm[of x i]
   2.247 +          using n N by(auto simp add:field_simps) qed }
   2.248 +    thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto
   2.249 +  qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i ..
   2.250 +  note i = this[unfolded Lim_sequentially, rule_format]
   2.251 +
   2.252 +  show ?l unfolding integrable_on_def has_integral_alt'[of f] apply(rule_tac x=i in exI)
   2.253 +    apply safe apply(rule as(1)[unfolded integrable_on_def])
   2.254 +  proof- case goal1 hence *:"e/2 > 0" by auto
   2.255 +    from i[OF this] guess N .. note N =this[rule_format]
   2.256 +    from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B"
   2.257 +    show ?case apply(rule_tac x="?B" in exI)
   2.258 +    proof safe show "0 < ?B" using B(1) by auto
   2.259 +      fix a b assume ab:"ball 0 ?B \<subseteq> {a..b::real^'n}"
   2.260 +      from real_arch_simple[of ?B] guess n .. note n=this
   2.261 +      show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - i) < e"
   2.262 +        apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute)
   2.263 +        apply(rule N[unfolded vector_dist_norm, of n])
   2.264 +      proof safe show "N \<le> n" using n by auto
   2.265 +        fix x::"real^'n" assume x:"x \<in> ball 0 B" hence "x\<in> ball 0 ?B" by auto
   2.266 +        thus "x\<in>{a..b}" using ab by blast 
   2.267 +        show "x\<in>{\<chi> i. - real n..\<chi> i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply-
   2.268 +        proof case goal1 thus ?case using component_le_norm[of x i]
   2.269 +            using n by(auto simp add:field_simps) qed qed qed qed qed
   2.270 +
   2.271 +lemma integrable_altD: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.272 +  assumes "f integrable_on s"
   2.273 +  shows "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}"
   2.274 +  "\<And>e. e>0 \<Longrightarrow> \<exists>B>0. \<forall>a b c d. ball 0 B \<subseteq> {a..b} \<and> ball 0 B \<subseteq> {c..d}
   2.275 +  \<longrightarrow> norm(integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d}  (\<lambda>x. if x \<in> s then f x else 0)) < e"
   2.276 +  using assms[unfolded integrable_alt[of f]] by auto
   2.277 +
   2.278 +lemma integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.279 +  assumes "f integrable_on s" "{a..b} \<subseteq> s" shows "f integrable_on {a..b}"
   2.280 +  apply(rule integrable_eq) defer apply(rule integrable_altD(1)[OF assms(1)])
   2.281 +  using assms(2) by auto
   2.282 +
   2.283 +subsection {* A straddling criterion for integrability. *}
   2.284 +
   2.285 +lemma integrable_straddle_interval: fixes f::"real^'n \<Rightarrow> real"
   2.286 +  assumes "\<forall>e>0. \<exists>g  h i j. (g has_integral i) ({a..b}) \<and> (h has_integral j) ({a..b}) \<and>
   2.287 +  norm(i - j) < e \<and> (\<forall>x\<in>{a..b}. (g x) \<le> (f x) \<and> (f x) \<le>(h x))"
   2.288 +  shows "f integrable_on {a..b}"
   2.289 +proof(subst integrable_cauchy,safe)
   2.290 +  case goal1 hence e:"e/3 > 0" by auto note assms[rule_format,OF this]
   2.291 +  then guess g h i j apply- by(erule exE conjE)+ note obt = this
   2.292 +  from obt(1)[unfolded has_integral[of g], rule_format, OF e] guess d1 .. note d1=conjunctD2[OF this,rule_format]
   2.293 +  from obt(2)[unfolded has_integral[of h], rule_format, OF e] guess d2 .. note d2=conjunctD2[OF this,rule_format]
   2.294 +  show ?case apply(rule_tac x="\<lambda>x. d1 x \<inter> d2 x" in exI) apply(rule conjI gauge_inter d1 d2)+ unfolding fine_inter
   2.295 +  proof safe have **:"\<And>i j g1 g2 h1 h2 f1 f2. g1 - h2 \<le> f1 - f2 \<Longrightarrow> f1 - f2 \<le> h1 - g2 \<Longrightarrow>
   2.296 +      abs(i - j) < e / 3 \<Longrightarrow> abs(g2 - i) < e / 3 \<Longrightarrow>  abs(g1 - i) < e / 3 \<Longrightarrow> 
   2.297 +      abs(h2 - j) < e / 3 \<Longrightarrow> abs(h1 - j) < e / 3 \<Longrightarrow> abs(f1 - f2) < e" using `e>0` by arith
   2.298 +    case goal1 note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)]
   2.299 +
   2.300 +    have "(\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R g x) \<ge> 0"
   2.301 +      "0 \<le> (\<Sum>(x, k)\<in>p2. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x)" 
   2.302 +      "(\<Sum>(x, k)\<in>p2. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p2. content k *\<^sub>R g x) \<ge> 0"
   2.303 +      "0 \<le> (\<Sum>(x, k)\<in>p1. content k *\<^sub>R h x) - (\<Sum>(x, k)\<in>p1. content k *\<^sub>R f x)" 
   2.304 +      unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg)
   2.305 +      apply safe unfolding real_scaleR_def mult.diff_right[THEN sym]
   2.306 +      apply(rule_tac[!] mult_nonneg_nonneg)
   2.307 +    proof- fix a b assume ab:"(a,b) \<in> p1"
   2.308 +      show "0 \<le> content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
   2.309 +      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(1-2)[OF ab] using obt(4)[rule_format,of a] by auto
   2.310 +    next fix a b assume ab:"(a,b) \<in> p2"
   2.311 +      show "0 \<le> content b" using *(6)[OF ab] apply safe using content_pos_le . thus "0 \<le> content b" .
   2.312 +      show "0 \<le> f a - g a" "0 \<le> h a - f a" using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto qed 
   2.313 +
   2.314 +    thus ?case apply- unfolding real_norm_def apply(rule **) defer defer
   2.315 +      unfolding real_norm_def[THEN sym] apply(rule obt(3))
   2.316 +      apply(rule d1(2)[OF conjI[OF goal1(4,5)]])
   2.317 +      apply(rule d1(2)[OF conjI[OF goal1(1,2)]])
   2.318 +      apply(rule d2(2)[OF conjI[OF goal1(4,6)]])
   2.319 +      apply(rule d2(2)[OF conjI[OF goal1(1,3)]]) by auto qed qed 
   2.320 +     
   2.321 +lemma integrable_straddle: fixes f::"real^'n \<Rightarrow> real"
   2.322 +  assumes "\<forall>e>0. \<exists>g h i j. (g has_integral i) s \<and> (h has_integral j) s \<and>
   2.323 +  norm(i - j) < e \<and> (\<forall>x\<in>s. (g x) \<le>(f x) \<and>(f x) \<le>(h x))"
   2.324 +  shows "f integrable_on s"
   2.325 +proof- have "\<And>a b. (\<lambda>x. if x \<in> s then f x else 0) integrable_on {a..b}"
   2.326 +  proof(rule integrable_straddle_interval,safe) case goal1 hence *:"e/4 > 0" by auto
   2.327 +    from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this
   2.328 +    note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format]
   2.329 +    note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
   2.330 +    note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
   2.331 +    note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
   2.332 +    def c \<equiv> "\<chi> i. min (a$i) (- (max B1 B2))" and d \<equiv> "\<chi> i. max (b$i) (max B1 B2)"
   2.333 +    have *:"ball 0 B1 \<subseteq> {c..d}" "ball 0 B2 \<subseteq> {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm
   2.334 +    proof(rule_tac[!] allI)
   2.335 +      case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next
   2.336 +      case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed
   2.337 +    have **:"\<And>ch cg ag ah::real. norm(ah - ag) \<le> norm(ch - cg) \<Longrightarrow> norm(cg - i) < e / 4 \<Longrightarrow>
   2.338 +      norm(ch - j) < e / 4 \<Longrightarrow> norm(ag - ah) < e"
   2.339 +      using obt(3) unfolding real_norm_def by arith 
   2.340 +    show ?case apply(rule_tac x="\<lambda>x. if x \<in> s then g x else 0" in exI)
   2.341 +               apply(rule_tac x="\<lambda>x. if x \<in> s then h x else 0" in exI)
   2.342 +      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)" in exI)
   2.343 +      apply(rule_tac x="integral {a..b} (\<lambda>x. if x \<in> s then h x else 0)" in exI)
   2.344 +      apply safe apply(rule_tac[1-2] integrable_integral,rule g,rule h)
   2.345 +      apply(rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]])
   2.346 +    proof- have *:"\<And>x f g. (if x \<in> s then f x else 0) - (if x \<in> s then g x else 0) =
   2.347 +        (if x \<in> s then f x - g x else (0::real))" by auto
   2.348 +      note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]]
   2.349 +      show " norm (integral {a..b} (\<lambda>x. if x \<in> s then h x else 0) -
   2.350 +                   integral {a..b} (\<lambda>x. if x \<in> s then g x else 0))
   2.351 +           \<le> norm (integral {c..d} (\<lambda>x. if x \<in> s then h x else 0) -
   2.352 +                   integral {c..d} (\<lambda>x. if x \<in> s then g x else 0))"
   2.353 +        unfolding integral_sub[OF h g,THEN sym] real_norm_def apply(subst **) defer apply(subst **) defer
   2.354 +        apply(rule has_integral_subset_le) defer apply(rule integrable_integral integrable_sub h g)+
   2.355 +      proof safe fix x assume "x\<in>{a..b}" thus "x\<in>{c..d}" unfolding mem_interval c_def d_def
   2.356 +          apply - apply rule apply(erule_tac x=i in allE) by auto
   2.357 +      qed(insert obt(4), auto) qed(insert obt(4), auto) qed note interv = this
   2.358 +
   2.359 +  show ?thesis unfolding integrable_alt[of f] apply safe apply(rule interv)
   2.360 +  proof- case goal1 hence *:"e/3 > 0" by auto
   2.361 +    from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this
   2.362 +    note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format]
   2.363 +    note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format]
   2.364 +    note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format]
   2.365 +    note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format]
   2.366 +    show ?case apply(rule_tac x="max B1 B2" in exI) apply safe apply(rule min_max.less_supI1,rule B1)
   2.367 +    proof- fix a b c d::"real^'n" assume as:"ball 0 (max B1 B2) \<subseteq> {a..b}" "ball 0 (max B1 B2) \<subseteq> {c..d}"
   2.368 +      have **:"ball 0 B1 \<subseteq> ball (0::real^'n) (max B1 B2)" "ball 0 B2 \<subseteq> ball (0::real^'n) (max B1 B2)" by auto
   2.369 +      have *:"\<And>ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \<and> abs(gc - i) < e / 3 \<and> abs(ha - j) < e / 3 \<and>
   2.370 +        abs(hc - j) < e / 3 \<and> abs(i - j) < e / 3 \<and> ga \<le> fa \<and> fa \<le> ha \<and> gc \<le> fc \<and> fc \<le> hc\<Longrightarrow> abs(fa - fc) < e" by smt
   2.371 +      show "norm (integral {a..b} (\<lambda>x. if x \<in> s then f x else 0) - integral {c..d} (\<lambda>x. if x \<in> s then f x else 0)) < e"
   2.372 +        unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym]
   2.373 +        apply(rule B1(2),rule order_trans,rule **,rule as(1)) 
   2.374 +        apply(rule B1(2),rule order_trans,rule **,rule as(2)) 
   2.375 +        apply(rule B2(2),rule order_trans,rule **,rule as(1)) 
   2.376 +        apply(rule B2(2),rule order_trans,rule **,rule as(2)) 
   2.377 +        apply(rule obt) apply(rule_tac[!] integral_le) using obt
   2.378 +        by(auto intro!: h g interv) qed qed qed 
   2.379 +
   2.380 +subsection {* Adding integrals over several sets. *}
   2.381 +
   2.382 +lemma has_integral_union: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.383 +  assumes "(f has_integral i) s" "(f has_integral j) t" "negligible(s \<inter> t)"
   2.384 +  shows "(f has_integral (i + j)) (s \<union> t)"
   2.385 +proof- note * = has_integral_restrict_univ[THEN sym, of f]
   2.386 +  show ?thesis unfolding * apply(rule has_integral_spike[OF assms(3)])
   2.387 +    defer apply(rule has_integral_add[OF assms(1-2)[unfolded *]]) by auto qed
   2.388 +
   2.389 +lemma has_integral_unions: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.390 +  assumes "finite t" "\<forall>s\<in>t. (f has_integral (i s)) s"  "\<forall>s\<in>t. \<forall>s'\<in>t. ~(s = s') \<longrightarrow> negligible(s \<inter> s')"
   2.391 +  shows "(f has_integral (setsum i t)) (\<Union>t)"
   2.392 +proof- note * = has_integral_restrict_univ[THEN sym, of f]
   2.393 +  have **:"negligible (\<Union>((\<lambda>(a,b). a \<inter> b) ` {(a,b). a \<in> t \<and> b \<in> {y. y \<in> t \<and> ~(a = y)}}))"
   2.394 +    apply(rule negligible_unions) apply(rule finite_imageI) apply(rule finite_subset[of _ "t \<times> t"]) defer 
   2.395 +    apply(rule finite_cartesian_product[OF assms(1,1)]) using assms(3) by auto 
   2.396 +  note assms(2)[unfolded *] note has_integral_setsum[OF assms(1) this]
   2.397 +  thus ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption
   2.398 +  proof safe case goal1 thus ?case
   2.399 +    proof(cases "x\<in>\<Union>t") case True then guess s unfolding Union_iff .. note s=this
   2.400 +      hence *:"\<forall>b\<in>t. x \<in> b \<longleftrightarrow> b = s" using goal1(3) by blast
   2.401 +      show ?thesis unfolding if_P[OF True] apply(rule trans) defer
   2.402 +        apply(rule setsum_cong2) apply(subst *, assumption) apply(rule refl)
   2.403 +        unfolding setsum_delta[OF assms(1)] using s by auto qed auto qed qed
   2.404 +
   2.405 +subsection {* In particular adding integrals over a division, maybe not of an interval. *}
   2.406 +
   2.407 +lemma has_integral_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.408 +  assumes "d division_of s" "\<forall>k\<in>d. (f has_integral (i k)) k"
   2.409 +  shows "(f has_integral (setsum i d)) s"
   2.410 +proof- note d = division_ofD[OF assms(1)]
   2.411 +  show ?thesis unfolding d(6)[THEN sym] apply(rule has_integral_unions)
   2.412 +    apply(rule d assms)+ apply(rule,rule,rule)
   2.413 +  proof- case goal1 from d(4)[OF this(1)] d(4)[OF this(2)]
   2.414 +    guess a c b d apply-by(erule exE)+ note obt=this
   2.415 +    from d(5)[OF goal1] show ?case unfolding obt interior_closed_interval
   2.416 +      apply-apply(rule negligible_subset[of "({a..b}-{a<..<b}) \<union> ({c..d}-{c<..<d})"])
   2.417 +      apply(rule negligible_union negligible_frontier_interval)+ by auto qed qed
   2.418 +
   2.419 +lemma integral_combine_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.420 +  assumes "d division_of s" "\<forall>k\<in>d. f integrable_on k"
   2.421 +  shows "integral s f = setsum (\<lambda>i. integral i f) d"
   2.422 +  apply(rule integral_unique) apply(rule has_integral_combine_division[OF assms(1)])
   2.423 +  using assms(2) unfolding has_integral_integral .
   2.424 +
   2.425 +lemma has_integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.426 +  assumes "f integrable_on s" "d division_of k" "k \<subseteq> s"
   2.427 +  shows "(f has_integral (setsum (\<lambda>i. integral i f) d)) k"
   2.428 +  apply(rule has_integral_combine_division[OF assms(2)])
   2.429 +  apply safe unfolding has_integral_integral[THEN sym]
   2.430 +proof- case goal1 from division_ofD(2,4)[OF assms(2) this]
   2.431 +  show ?case apply safe apply(rule integrable_on_subinterval)
   2.432 +    apply(rule assms) using assms(3) by auto qed
   2.433 +
   2.434 +lemma integral_combine_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.435 +  assumes "f integrable_on s" "d division_of s"
   2.436 +  shows "integral s f = setsum (\<lambda>i. integral i f) d"
   2.437 +  apply(rule integral_unique,rule has_integral_combine_division_topdown) using assms by auto
   2.438 +
   2.439 +lemma integrable_combine_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.440 +  assumes "d division_of s" "\<forall>i\<in>d. f integrable_on i"
   2.441 +  shows "f integrable_on s"
   2.442 +  using assms(2) unfolding integrable_on_def
   2.443 +  by(metis has_integral_combine_division[OF assms(1)])
   2.444 +
   2.445 +lemma integrable_on_subdivision: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.446 +  assumes "d division_of i" "f integrable_on s" "i \<subseteq> s"
   2.447 +  shows "f integrable_on i"
   2.448 +  apply(rule integrable_combine_division assms)+
   2.449 +proof safe case goal1 note division_ofD(2,4)[OF assms(1) this]
   2.450 +  thus ?case apply safe apply(rule integrable_on_subinterval[OF assms(2)])
   2.451 +    using assms(3) by auto qed
   2.452 +
   2.453 +subsection {* Also tagged divisions. *}
   2.454 +
   2.455 +lemma has_integral_combine_tagged_division: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.456 +  assumes "p tagged_division_of s" "\<forall>(x,k) \<in> p. (f has_integral (i k)) k"
   2.457 +  shows "(f has_integral (setsum (\<lambda>(x,k). i k) p)) s"
   2.458 +proof- have *:"(f has_integral (setsum (\<lambda>k. integral k f) (snd ` p))) s"
   2.459 +    apply(rule has_integral_combine_division) apply(rule division_of_tagged_division[OF assms(1)])
   2.460 +    using assms(2) unfolding has_integral_integral[THEN sym] by(safe,auto)
   2.461 +  thus ?thesis apply- apply(rule subst[where P="\<lambda>i. (f has_integral i) s"]) defer apply assumption
   2.462 +    apply(rule trans[of _ "setsum (\<lambda>(x,k). integral k f) p"]) apply(subst eq_commute)
   2.463 +    apply(rule setsum_over_tagged_division_lemma[OF assms(1)]) apply(rule integral_null,assumption)
   2.464 +    apply(rule setsum_cong2) using assms(2) by auto qed
   2.465 +
   2.466 +lemma integral_combine_tagged_division_bottomup: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.467 +  assumes "p tagged_division_of {a..b}" "\<forall>(x,k)\<in>p. f integrable_on k"
   2.468 +  shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p"
   2.469 +  apply(rule integral_unique) apply(rule has_integral_combine_tagged_division[OF assms(1)])
   2.470 +  using assms(2) by auto
   2.471 +
   2.472 +lemma has_integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.473 +  assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}"
   2.474 +  shows "(f has_integral (setsum (\<lambda>(x,k). integral k f) p)) {a..b}"
   2.475 +  apply(rule has_integral_combine_tagged_division[OF assms(2)])
   2.476 +proof safe case goal1 note tagged_division_ofD(3-4)[OF assms(2) this]
   2.477 +  thus ?case using integrable_subinterval[OF assms(1)] by auto qed
   2.478 +
   2.479 +lemma integral_combine_tagged_division_topdown: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.480 +  assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}"
   2.481 +  shows "integral {a..b} f = setsum (\<lambda>(x,k). integral k f) p"
   2.482 +  apply(rule integral_unique,rule has_integral_combine_tagged_division_topdown) using assms by auto
   2.483 +
   2.484 +subsection {* Henstock's lemma. *}
   2.485 +
   2.486 +lemma henstock_lemma_part1: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.487 +  assumes "f integrable_on {a..b}" "0 < e" "gauge d"
   2.488 +  "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)"
   2.489 +  and p:"p tagged_partial_division_of {a..b}" "d fine p"
   2.490 +  shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
   2.491 +proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith }
   2.492 +  fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
   2.493 +  have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
   2.494 +  note partial_division_of_tagged_division[OF p(1)] this
   2.495 +  from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
   2.496 +  def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto
   2.497 +  have r:"finite r" using q' unfolding r_def by auto
   2.498 +
   2.499 +  have "\<forall>i\<in>r. \<exists>p. p tagged_division_of i \<and> d fine p \<and>
   2.500 +    norm(setsum (\<lambda>(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)"
   2.501 +  proof safe case goal1 hence i:"i \<in> q" unfolding r_def by auto
   2.502 +    from q'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
   2.503 +    have *:"k / (real (card r) + 1) > 0" apply(rule divide_pos_pos,rule k) by auto
   2.504 +    have "f integrable_on {u..v}" apply(rule integrable_subinterval[OF assms(1)])
   2.505 +      using q'(2)[OF i] unfolding uv by auto
   2.506 +    note integrable_integral[OF this, unfolded has_integral[of f]]
   2.507 +    from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format]
   2.508 +    note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq .
   2.509 +    thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed
   2.510 +  from bchoice[OF this] guess qq .. note qq=this[rule_format]
   2.511 +
   2.512 +  let ?p = "p \<union> \<Union>qq ` r" have "norm ((\<Sum>(x, k)\<in>?p. content k *\<^sub>R f x) - integral {a..b} f) < e"
   2.513 +    apply(rule assms(4)[rule_format])
   2.514 +  proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto 
   2.515 +    note * = tagged_partial_division_of_union_self[OF p(1)]
   2.516 +    have "p \<union> \<Union>qq ` r tagged_division_of \<Union>snd ` p \<union> \<Union>r"
   2.517 +    proof(rule tagged_division_union[OF * tagged_division_unions])
   2.518 +      show "finite r" by fact case goal2 thus ?case using qq by auto
   2.519 +    next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto
   2.520 +    next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule)
   2.521 +        apply(rule,rule q') defer apply(rule,subst Int_commute) 
   2.522 +        apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer
   2.523 +        apply(rule,rule q') using q(1) p' unfolding r_def by auto qed
   2.524 +    moreover have "\<Union>snd ` p \<union> \<Union>r = {a..b}" "{qq i |i. i \<in> r} = qq ` r"
   2.525 +      unfolding Union_Un_distrib[THEN sym] r_def using q by auto
   2.526 +    ultimately show "?p tagged_division_of {a..b}" by fastsimp qed
   2.527 +
   2.528 +  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + (\<Sum>(x, k)\<in>\<Union>qq ` r. content k *\<^sub>R f x) -
   2.529 +    integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 
   2.530 +    apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq)
   2.531 +  proof- fix x l k assume as:"(x,l)\<in>p" "(x,l)\<in>qq k" "k\<in>r"
   2.532 +    note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)]
   2.533 +    from this(2) guess u v apply-by(erule exE)+ note uv=this
   2.534 +    have "l\<in>snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto
   2.535 +    hence "l\<in>q" "k\<in>q" "l\<noteq>k" using as(1,3) q(1) unfolding r_def by auto
   2.536 +    note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \<subseteq> k`] by blast
   2.537 +    thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto
   2.538 +
   2.539 +  hence "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x))
   2.540 +    (qq ` r) - integral {a..b} f) < e" apply(subst(asm) setsum_UNION_zero)
   2.541 +    prefer 4 apply assumption apply(rule finite_imageI,fact)
   2.542 +    unfolding split_paired_all split_conv image_iff defer apply(erule bexE)+
   2.543 +  proof- fix x m k l T1 T2 assume "(x,m)\<in>T1" "(x,m)\<in>T2" "T1\<noteq>T2" "k\<in>r" "l\<in>r" "T1 = qq k" "T2 = qq l"
   2.544 +    note as = this(1-5)[unfolded this(6-)] note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
   2.545 +    from this(2)[OF as(4,1)] guess u v apply-by(erule exE)+ note uv=this
   2.546 +    have *:"interior (k \<inter> l) = {}" unfolding interior_inter apply(rule q')
   2.547 +      using as unfolding r_def by auto
   2.548 +    have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym]
   2.549 +      apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto
   2.550 +    thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto 
   2.551 +  qed(insert qq, auto)
   2.552 +
   2.553 +  hence **:"norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) + setsum (setsum (\<lambda>(x, k). content k *\<^sub>R f x) \<circ> qq) r -
   2.554 +    integral {a..b} f) < e" apply(subst(asm) setsum_reindex_nonzero) apply fact
   2.555 +    apply(rule setsum_0',rule) unfolding split_paired_all split_conv defer apply assumption
   2.556 +  proof- fix k l x m assume as:"k\<in>r" "l\<in>r" "k\<noteq>l" "qq k = qq l" "(x,m)\<in>qq k"
   2.557 +    note tagged_division_ofD(6)[OF qq[THEN conjunct1]] from this[OF as(1)] this[OF as(2)] 
   2.558 +    show "content m *\<^sub>R f x = 0"  using as(3) unfolding as by auto qed
   2.559 +  
   2.560 +  have *:"\<And>ir ip i cr cp. norm((cp + cr) - i) < e \<Longrightarrow> norm(cr - ir) < k \<Longrightarrow> 
   2.561 +    ip + ir = i \<Longrightarrow> norm(cp - ip) \<le> e + k" 
   2.562 +  proof- case goal1 thus ?case  using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"]  
   2.563 +      unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed
   2.564 +  
   2.565 +  have "?x =  norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - (\<Sum>(x, k)\<in>p. integral k f))"
   2.566 +    unfolding split_def setsum_subtractf ..
   2.567 +  also have "... \<le> e + k" apply(rule *[OF **, where ir="setsum (\<lambda>k. integral k f) r"])
   2.568 +  proof- case goal2 have *:"(\<Sum>(x, k)\<in>p. integral k f) = (\<Sum>k\<in>snd ` p. integral k f)"
   2.569 +      apply(subst setsum_reindex_nonzero) apply fact
   2.570 +      unfolding split_paired_all snd_conv split_def o_def
   2.571 +    proof- fix x l y m assume as:"(x,l)\<in>p" "(y,m)\<in>p" "(x,l)\<noteq>(y,m)" "l = m"
   2.572 +      from p'(4)[OF as(1)] guess u v apply-by(erule exE)+ note uv=this
   2.573 +      show "integral l f = 0" unfolding uv apply(rule integral_unique)
   2.574 +        apply(rule has_integral_null) unfolding content_eq_0_interior
   2.575 +        using p'(5)[OF as(1-3)] unfolding uv as(4)[THEN sym] by auto
   2.576 +    qed auto 
   2.577 +    show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def
   2.578 +      apply(rule setsum_Un_disjoint'[THEN sym]) using q(1) q'(1) p'(1) by auto
   2.579 +  next  case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps)
   2.580 +    show ?case apply(rule le_less_trans[of _ "setsum (\<lambda>x. k / (real (card r) + 1)) r"])
   2.581 +      unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact)
   2.582 +      apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym]
   2.583 +      unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat)
   2.584 +  qed finally show "?x \<le> e + k" . qed
   2.585 +
   2.586 +lemma henstock_lemma_part2: fixes f::"real^'m \<Rightarrow> real^'n"
   2.587 +  assumes "f integrable_on {a..b}" "0 < e" "gauge d"
   2.588 +  "\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p -
   2.589 +          integral({a..b}) f) < e"    "p tagged_partial_division_of {a..b}" "d fine p"
   2.590 +  shows "setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p \<le> 2 * real (CARD('n)) * e"
   2.591 +  unfolding split_def apply(rule vsum_norm_allsubsets_bound) defer 
   2.592 +  apply(rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)])
   2.593 +  apply safe apply(rule assms[rule_format,unfolded split_def]) defer
   2.594 +  apply(rule tagged_partial_division_subset,rule assms,assumption)
   2.595 +  apply(rule fine_subset,assumption,rule assms) using assms(5) by auto
   2.596 +  
   2.597 +lemma henstock_lemma: fixes f::"real^'m \<Rightarrow> real^'n"
   2.598 +  assumes "f integrable_on {a..b}" "e>0"
   2.599 +  obtains d where "gauge d"
   2.600 +  "\<forall>p. p tagged_partial_division_of {a..b} \<and> d fine p
   2.601 +  \<longrightarrow> setsum (\<lambda>(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e"
   2.602 +proof- have *:"e / (2 * (real CARD('n) + 1)) > 0" apply(rule divide_pos_pos) using assms(2) by auto
   2.603 +  from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this]
   2.604 +  guess d .. note d = conjunctD2[OF this] show thesis apply(rule that,rule d)
   2.605 +  proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this]
   2.606 +    show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed
   2.607 +
   2.608 +subsection {* monotone convergence (bounded interval first). *}
   2.609 +
   2.610 +lemma monotone_convergence_interval: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
   2.611 +  assumes "\<forall>k. (f k) integrable_on {a..b}"
   2.612 +  "\<forall>k. \<forall>x\<in>{a..b}. dest_vec1(f k x) \<le> dest_vec1(f (Suc k) x)"
   2.613 +  "\<forall>x\<in>{a..b}. ((\<lambda>k. f k x) ---> g x) sequentially"
   2.614 +  "bounded {integral {a..b} (f k) | k . k \<in> UNIV}"
   2.615 +  shows "g integrable_on {a..b} \<and> ((\<lambda>k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially"
   2.616 +proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0"
   2.617 +  show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto
   2.618 +next assume ab:"content {a..b} \<noteq> 0"
   2.619 +  have fg:"\<forall>x\<in>{a..b}. \<forall> k. (f k x)$1 \<le> (g x)$1"
   2.620 +  proof safe case goal1 note assms(3)[rule_format,OF this]
   2.621 +    note * = Lim_component_ge[OF this trivial_limit_sequentially]
   2.622 +    show ?case apply(rule *) unfolding eventually_sequentially
   2.623 +      apply(rule_tac x=k in exI) apply- apply(rule transitive_stepwise_le)
   2.624 +      using assms(2)[rule_format,OF goal1] by auto qed
   2.625 +  have "\<exists>i. ((\<lambda>k. integral ({a..b}) (f k)) ---> i) sequentially"
   2.626 +    apply(rule bounded_increasing_convergent) defer
   2.627 +    apply rule apply(rule integral_component_le) apply safe
   2.628 +    apply(rule assms(1-2)[rule_format])+ using assms(4) by auto
   2.629 +  then guess i .. note i=this
   2.630 +  have i':"\<And>k. dest_vec1(integral({a..b}) (f k)) \<le> dest_vec1 i"
   2.631 +    apply(rule Lim_component_ge,rule i) apply(rule trivial_limit_sequentially)
   2.632 +    unfolding eventually_sequentially apply(rule_tac x=k in exI)
   2.633 +    apply(rule transitive_stepwise_le) prefer 3 apply(rule integral_dest_vec1_le)
   2.634 +    apply(rule assms(1-2)[rule_format])+ using assms(2) by auto
   2.635 +
   2.636 +  have "(g has_integral i) {a..b}" unfolding has_integral
   2.637 +  proof safe case goal1 note e=this
   2.638 +    hence "\<forall>k. (\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow>
   2.639 +             norm ((\<Sum>(x, ka)\<in>p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))"
   2.640 +      apply-apply(rule,rule assms(1)[unfolded has_integral_integral has_integral,rule_format])
   2.641 +      apply(rule divide_pos_pos) by auto
   2.642 +    from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format]
   2.643 +
   2.644 +    have "\<exists>r. \<forall>k\<ge>r. 0 \<le> i$1 - dest_vec1(integral {a..b} (f k)) \<and>
   2.645 +                   i$1 - dest_vec1(integral {a..b} (f k)) < e / 4"
   2.646 +    proof- case goal1 have "e/4 > 0" using e by auto
   2.647 +      from i[unfolded Lim_sequentially,rule_format,OF this] guess r ..
   2.648 +      thus ?case apply(rule_tac x=r in exI) apply rule
   2.649 +        apply(erule_tac x=k in allE)
   2.650 +      proof- case goal1 thus ?case using i'[of k] unfolding dist_real by auto qed qed
   2.651 +    then guess r .. note r=conjunctD2[OF this[rule_format]]
   2.652 +
   2.653 +    have "\<forall>x\<in>{a..b}. \<exists>n\<ge>r. \<forall>k\<ge>n. 0 \<le> (g x)$1 - (f k x)$1 \<and>
   2.654 +           (g x)$1 - (f k x)$1 < e / (4 * content({a..b}))"
   2.655 +    proof case goal1 have "e / (4 * content {a..b}) > 0" apply(rule divide_pos_pos,fact)
   2.656 +        using ab content_pos_le[of a b] by auto
   2.657 +      from assms(3)[rule_format,OF goal1,unfolded Lim_sequentially,rule_format,OF this]
   2.658 +      guess n .. note n=this
   2.659 +      thus ?case apply(rule_tac x="n + r" in exI) apply safe apply(erule_tac[2-3] x=k in allE)
   2.660 +        unfolding dist_real using fg[rule_format,OF goal1] by(auto simp add:field_simps) qed
   2.661 +    from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format]
   2.662 +    def d \<equiv> "\<lambda>x. c (m x) x" 
   2.663 +
   2.664 +    show ?case apply(rule_tac x=d in exI)
   2.665 +    proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto
   2.666 +    next fix p assume p:"p tagged_division_of {a..b}" "d fine p"
   2.667 +      note p'=tagged_division_ofD[OF p(1)]
   2.668 +      have "\<exists>a. \<forall>x\<in>p. m (fst x) \<le> a" by(rule upper_bound_finite_set,fact)
   2.669 +      then guess s .. note s=this
   2.670 +      have *:"\<forall>a b c d. norm(a - b) \<le> e / 4 \<and> norm(b - c) < e / 2 \<and>
   2.671 +            norm(c - d) < e / 4 \<longrightarrow> norm(a - d) < e" 
   2.672 +      proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"]
   2.673 +          norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel
   2.674 +          by(auto simp add:group_simps) qed
   2.675 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where
   2.676 +          b="\<Sum>(x, k)\<in>p. content k *\<^sub>R f (m x) x" and c="\<Sum>(x, k)\<in>p. integral k (f (m x))"])
   2.677 +      proof safe case goal1
   2.678 +         show ?case apply(rule order_trans[of _ "\<Sum>(x, k)\<in>p. content k * (e / (4 * content {a..b}))"])
   2.679 +           unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule setsum_norm[OF p'(1)])
   2.680 +           apply(rule setsum_mono) unfolding split_paired_all split_conv
   2.681 +           unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym]
   2.682 +           unfolding additive_content_tagged_division[OF p(1), unfolded split_def]
   2.683 +         proof- fix x k assume xk:"(x,k) \<in> p" hence x:"x\<in>{a..b}" using p'(2-3)[OF xk] by auto
   2.684 +           from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this
   2.685 +           show " norm (content k *\<^sub>R (g x - f (m x) x)) \<le> content k * (e / (4 * content {a..b}))"
   2.686 +             unfolding norm_scaleR uv unfolding abs_of_nonneg[OF content_pos_le] 
   2.687 +             apply(rule mult_left_mono) unfolding norm_real using m(2)[OF x,of "m x"] by auto
   2.688 +         qed(insert ab,auto)
   2.689 +         
   2.690 +       next case goal2 show ?case apply(rule le_less_trans[of _ "norm (\<Sum>j = 0..s.
   2.691 +           \<Sum>(x, k)\<in>{xk\<in>p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"])
   2.692 +           apply(subst setsum_group) apply fact apply(rule finite_atLeastAtMost) defer
   2.693 +           apply(subst split_def)+ unfolding setsum_subtractf apply rule
   2.694 +         proof- show "norm (\<Sum>j = 0..s. \<Sum>(x, k)\<in>{xk \<in> p.
   2.695 +             m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2"
   2.696 +             apply(rule le_less_trans[of _ "setsum (\<lambda>i. e / 2^(i+2)) {0..s}"])
   2.697 +             apply(rule setsum_norm_le[OF finite_atLeastAtMost])
   2.698 +           proof show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
   2.699 +               unfolding power_add real_divide_def inverse_mult_distrib
   2.700 +               unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym]
   2.701 +               unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e])
   2.702 +               unfolding power2_eq_square by auto
   2.703 +             fix t assume "t\<in>{0..s}"
   2.704 +             show "norm (\<Sum>(x, k)\<in>{xk \<in> p. m (fst xk) = t}. content k *\<^sub>R f (m x) x -
   2.705 +               integral k (f (m x))) \<le> e / 2 ^ (t + 2)"apply(rule order_trans[of _
   2.706 +               "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \<in> p. m (fst xk) = t})"])
   2.707 +               apply(rule eq_refl) apply(rule arg_cong[where f=norm]) apply(rule setsum_cong2) defer
   2.708 +               apply(rule henstock_lemma_part1) apply(rule assms(1)[rule_format])
   2.709 +               apply(rule divide_pos_pos,rule e) defer  apply safe apply(rule c)+
   2.710 +               apply rule apply assumption+ apply(rule tagged_partial_division_subset[of p])
   2.711 +               apply(rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) defer
   2.712 +               unfolding fine_def apply safe apply(drule p(2)[unfolded fine_def,rule_format])
   2.713 +               unfolding d_def by auto qed
   2.714 +         qed(insert s, auto)
   2.715 +
   2.716 +       next case goal3
   2.717 +         note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)]
   2.718 +         have *:"\<And>sr sx ss ks kr::real^1. kr = sr \<longrightarrow> ks = ss \<longrightarrow> ks \<le> i \<and> sr \<le> sx \<and> sx \<le> ss \<and> 0 \<le> i$1 - kr$1
   2.719 +           \<and> i$1 - kr$1 < e/4 \<longrightarrow> abs(sx$1 - i$1) < e/4" unfolding Cart_eq forall_1 vector_le_def by arith
   2.720 +         show ?case unfolding norm_real Cart_nth.diff apply(rule *[rule_format],safe)
   2.721 +           apply(rule comb[of r],rule comb[of s]) unfolding vector_le_def forall_1 setsum_component
   2.722 +           apply(rule i') apply(rule_tac[1-2] setsum_mono) unfolding split_paired_all split_conv
   2.723 +           apply(rule_tac[1-2] integral_component_le[OF ])
   2.724 +         proof safe show "0 \<le> i$1 - (integral {a..b} (f r))$1" using r(1) by auto
   2.725 +           show "i$1 - (integral {a..b} (f r))$1 < e / 4" using r(2) by auto
   2.726 +           fix x k assume xk:"(x,k)\<in>p" from p'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
   2.727 +           show "f r integrable_on k" "f s integrable_on k" "f (m x) integrable_on k" "f (m x) integrable_on k" 
   2.728 +             unfolding uv apply(rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]])
   2.729 +             using p'(3)[OF xk] unfolding uv by auto 
   2.730 +           fix y assume "y\<in>k" hence "y\<in>{a..b}" using p'(3)[OF xk] by auto
   2.731 +           hence *:"\<And>m. \<forall>n\<ge>m. (f m y)$1 \<le> (f n y)$1" apply-apply(rule transitive_stepwise_le) using assms(2) by auto
   2.732 +           show "(f r y)$1 \<le> (f (m x) y)$1" "(f (m x) y)$1 \<le> (f s y)$1"
   2.733 +             apply(rule_tac[!] *[rule_format]) using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] by auto
   2.734 +         qed qed qed qed note * = this 
   2.735 +
   2.736 +   have "integral {a..b} g = i" apply(rule integral_unique) using * .
   2.737 +   thus ?thesis using i * by auto qed
   2.738 +
   2.739 +lemma monotone_convergence_increasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
   2.740 +  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1"
   2.741 +  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
   2.742 +  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   2.743 +proof- have lem:"\<And>f::nat \<Rightarrow> real^'n \<Rightarrow> real^1. \<And> g s. \<forall>k.\<forall>x\<in>s. 0\<le>dest_vec1 (f k x) \<Longrightarrow> \<forall>k. (f k) integrable_on s \<Longrightarrow>
   2.744 +    \<forall>k. \<forall>x\<in>s. (f k x)$1 \<le> (f (Suc k) x)$1 \<Longrightarrow> \<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially  \<Longrightarrow>
   2.745 +    bounded {integral s (f k)| k. True} \<Longrightarrow> g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   2.746 +  proof- case goal1 note assms=this[rule_format]
   2.747 +    have "\<forall>x\<in>s. \<forall>k. dest_vec1(f k x) \<le> dest_vec1(g x)" apply safe apply(rule Lim_component_ge)
   2.748 +      apply(rule goal1(4)[rule_format],assumption) apply(rule trivial_limit_sequentially)
   2.749 +      unfolding eventually_sequentially apply(rule_tac x=k in exI)
   2.750 +      apply(rule transitive_stepwise_le) using goal1(3) by auto note fg=this[rule_format]
   2.751 +
   2.752 +    have "\<exists>i. ((\<lambda>k. integral s (f k)) ---> i) sequentially" apply(rule bounded_increasing_convergent)
   2.753 +      apply(rule goal1(5)) apply(rule,rule integral_component_le) apply(rule goal1(2)[rule_format])+
   2.754 +      using goal1(3) by auto then guess i .. note i=this
   2.755 +    have "\<And>k. \<forall>x\<in>s. \<forall>n\<ge>k. f k x \<le> f n x" apply(rule,rule transitive_stepwise_le) using goal1(3) by auto
   2.756 +    hence i':"\<forall>k. (integral s (f k))$1 \<le> i$1" apply-apply(rule,rule Lim_component_ge)
   2.757 +      apply(rule i,rule trivial_limit_sequentially) unfolding eventually_sequentially
   2.758 +      apply(rule_tac x=k in exI,safe) apply(rule integral_dest_vec1_le)
   2.759 +      apply(rule goal1(2)[rule_format])+ by auto 
   2.760 +
   2.761 +    note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format]
   2.762 +    have ifif:"\<And>k t. (\<lambda>x. if x \<in> t then if x \<in> s then f k x else 0 else 0) =
   2.763 +      (\<lambda>x. if x \<in> t\<inter>s then f k x else 0)" apply(rule ext) by auto
   2.764 +    have int':"\<And>k a b. f k integrable_on {a..b} \<inter> s" apply(subst integrable_restrict_univ[THEN sym])
   2.765 +      apply(subst ifif[THEN sym]) apply(subst integrable_restrict_univ) using int .
   2.766 +    have "\<And>a b. (\<lambda>x. if x \<in> s then g x else 0) integrable_on {a..b} \<and>
   2.767 +      ((\<lambda>k. integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) --->
   2.768 +      integral {a..b} (\<lambda>x. if x \<in> s then g x else 0)) sequentially"
   2.769 +    proof(rule monotone_convergence_interval,safe)
   2.770 +      case goal1 show ?case using int .
   2.771 +    next case goal2 thus ?case apply-apply(cases "x\<in>s") using assms(3) by auto
   2.772 +    next case goal3 thus ?case apply-apply(cases "x\<in>s") using assms(4) by auto
   2.773 +    next case goal4 note * = integral_dest_vec1_nonneg[unfolded vector_le_def forall_1 zero_index]
   2.774 +      have "\<And>k. norm (integral {a..b} (\<lambda>x. if x \<in> s then f k x else 0)) \<le> norm (integral s (f k))"
   2.775 +        unfolding norm_real apply(subst abs_of_nonneg) apply(rule *[OF int])
   2.776 +        apply(safe,case_tac "x\<in>s") apply(drule assms(1)) prefer 3
   2.777 +        apply(subst abs_of_nonneg) apply(rule *[OF assms(2) goal1(1)[THEN spec]])
   2.778 +        apply(subst integral_restrict_univ[THEN sym,OF int]) 
   2.779 +        unfolding ifif unfolding integral_restrict_univ[OF int']
   2.780 +        apply(rule integral_subset_component_le[OF _ int' assms(2)]) using assms(1) by auto
   2.781 +      thus ?case using assms(5) unfolding bounded_iff apply safe
   2.782 +        apply(rule_tac x=aa in exI,safe) apply(erule_tac x="integral s (f k)" in ballE)
   2.783 +        apply(rule order_trans) apply assumption by auto qed note g = conjunctD2[OF this]
   2.784 +
   2.785 +    have "(g has_integral i) s" unfolding has_integral_alt' apply safe apply(rule g(1))
   2.786 +    proof- case goal1 hence "e/4>0" by auto
   2.787 +      from i[unfolded Lim_sequentially,rule_format,OF this] guess N .. note N=this
   2.788 +      note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]]
   2.789 +      from this[THEN conjunct2,rule_format,OF `e/4>0`] guess B .. note B=conjunctD2[OF this]
   2.790 +      show ?case apply(rule,rule,rule B,safe)
   2.791 +      proof- fix a b::"real^'n" assume ab:"ball 0 B \<subseteq> {a..b}"
   2.792 +        from `e>0` have "e/2>0" by auto
   2.793 +        from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this
   2.794 +        have **:"norm (integral {a..b} (\<lambda>x. if x \<in> s then f N x else 0) - i) < e/2"
   2.795 +          apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N]
   2.796 +          unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto
   2.797 +        have *:"\<And>f1 f2 g. abs(f1 - i$1) < e / 2 \<longrightarrow> abs(f2 - g) < e / 2 \<longrightarrow> f1 \<le> f2 \<longrightarrow> f2 \<le> i$1
   2.798 +          \<longrightarrow> abs(g - i$1) < e" by arith
   2.799 +        show "norm (integral {a..b} (\<lambda>x. if x \<in> s then g x else 0) - i) < e" 
   2.800 +          unfolding norm_real Cart_simps apply(rule *[rule_format])
   2.801 +          apply(rule **[unfolded norm_real Cart_simps])
   2.802 +          apply(rule M[rule_format,of "M + N",unfolded dist_real]) apply(rule le_add1)
   2.803 +          apply(rule integral_component_le[OF int int]) defer
   2.804 +          apply(rule order_trans[OF _ i'[rule_format,of "M + N"]])
   2.805 +        proof safe case goal2 have "\<And>m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. (f m x)$1 \<le> (f n x)$1"
   2.806 +            apply(rule transitive_stepwise_le) using assms(3) by auto thus ?case by auto
   2.807 +        next case goal1 show ?case apply(subst integral_restrict_univ[THEN sym,OF int]) 
   2.808 +            unfolding ifif integral_restrict_univ[OF int']
   2.809 +            apply(rule integral_subset_component_le[OF _ int']) using assms by auto
   2.810 +        qed qed qed 
   2.811 +    thus ?case apply safe defer apply(drule integral_unique) using i by auto qed
   2.812 +
   2.813 +  have sub:"\<And>k. integral s (\<lambda>x. f k x - f 0 x) = integral s (f k) - integral s (f 0)"
   2.814 +    apply(subst integral_sub) apply(rule assms(1)[rule_format])+ by rule
   2.815 +  have "\<And>x m. x\<in>s \<Longrightarrow> \<forall>n\<ge>m. dest_vec1 (f m x) \<le> dest_vec1 (f n x)" apply(rule transitive_stepwise_le)
   2.816 +    using assms(2) by auto note * = this[rule_format]
   2.817 +  have "(\<lambda>x. g x - f 0 x) integrable_on s \<and>((\<lambda>k. integral s (\<lambda>x. f (Suc k) x - f 0 x)) --->
   2.818 +      integral s (\<lambda>x. g x - f 0 x)) sequentially" apply(rule lem,safe)
   2.819 +  proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto
   2.820 +  next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto
   2.821 +  next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto
   2.822 +  next case goal4 thus ?case apply-apply(rule Lim_sub) 
   2.823 +      using seq_offset[OF assms(3)[rule_format],of x 1] by auto
   2.824 +  next case goal5 thus ?case using assms(4) unfolding bounded_iff
   2.825 +      apply safe apply(rule_tac x="a + norm (integral s (\<lambda>x. f 0 x))" in exI)
   2.826 +      apply safe apply(erule_tac x="integral s (\<lambda>x. f (Suc k) x)" in ballE) unfolding sub
   2.827 +      apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed
   2.828 +  note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]]
   2.829 +    integrable_add[OF this(1) assms(1)[rule_format,of 0]]
   2.830 +  thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub)
   2.831 +    using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed
   2.832 +
   2.833 +lemma monotone_convergence_decreasing: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real^1"
   2.834 +  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x)$1 \<le> (f k x)$1"
   2.835 +  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
   2.836 +  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   2.837 +proof- note assm = assms[rule_format]
   2.838 +  have *:"{integral s (\<lambda>x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}"
   2.839 +    apply safe unfolding image_iff apply(rule_tac x="integral s (f k)" in bexI) prefer 3
   2.840 +    apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto
   2.841 +  have "(\<lambda>x. - g x) integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. - f k x))
   2.842 +    ---> integral s (\<lambda>x. - g x))  sequentially" apply(rule monotone_convergence_increasing)
   2.843 +    apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg)
   2.844 +    apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto
   2.845 +  note * = conjunctD2[OF this]
   2.846 +  show ?thesis apply rule using integrable_neg[OF *(1)] defer
   2.847 +    using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)]
   2.848 +    unfolding integral_neg[OF *(1),THEN sym] by auto qed
   2.849 +
   2.850 +lemma monotone_convergence_increasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
   2.851 +  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<ge> (f k x)"
   2.852 +  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
   2.853 +  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   2.854 +proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} =  vec1 ` {integral s (f k) |k. True}"
   2.855 +    unfolding integral_trans[OF assms(1)[rule_format]] by auto
   2.856 +  have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially"
   2.857 +    apply(rule monotone_convergence_increasing) unfolding o_def integrable_on_trans
   2.858 +    unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto
   2.859 +  thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed
   2.860 +
   2.861 +lemma monotone_convergence_decreasing_real: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
   2.862 +  assumes "\<forall>k. (f k) integrable_on s"  "\<forall>k. \<forall>x\<in>s. (f (Suc k) x) \<le> (f k x)"
   2.863 +  "\<forall>x\<in>s. ((\<lambda>k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}"
   2.864 +  shows "g integrable_on s \<and> ((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
   2.865 +proof- have *:"{integral s (\<lambda>x. vec1 (f k x)) |k. True} =  vec1 ` {integral s (f k) |k. True}"
   2.866 +    unfolding integral_trans[OF assms(1)[rule_format]] by auto
   2.867 +  have "vec1 \<circ> g integrable_on s \<and> ((\<lambda>k. integral s (vec1 \<circ> f k)) ---> integral s (vec1 \<circ> g)) sequentially"
   2.868 +    apply(rule monotone_convergence_decreasing) unfolding o_def integrable_on_trans
   2.869 +    unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto
   2.870 +  thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed
   2.871 +
   2.872 +subsection {* absolute integrability (this is the same as Lebesgue integrability). *}
   2.873 +
   2.874 +definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) where
   2.875 +  "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and> (\<lambda>x. (norm(f x))) integrable_on s"
   2.876 +
   2.877 +lemma absolutely_integrable_onI[intro?]:
   2.878 +  "f integrable_on s \<Longrightarrow> (\<lambda>x. (norm(f x))) integrable_on s \<Longrightarrow> f absolutely_integrable_on s"
   2.879 +  unfolding absolutely_integrable_on_def by auto
   2.880 +
   2.881 +lemma absolutely_integrable_onD[dest]: assumes "f absolutely_integrable_on s"
   2.882 +  shows "f integrable_on s" "(\<lambda>x. (norm(f x))) integrable_on s"
   2.883 +  using assms unfolding absolutely_integrable_on_def by auto
   2.884 +
   2.885 +lemma absolutely_integrable_on_trans[simp]: fixes f::"real^'n \<Rightarrow> real" shows
   2.886 +  "(vec1 o f) absolutely_integrable_on s \<longleftrightarrow> f absolutely_integrable_on s"
   2.887 +  unfolding absolutely_integrable_on_def o_def by auto
   2.888 +
   2.889 +lemma integral_norm_bound_integral: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.890 +  assumes "f integrable_on s" "g integrable_on s" "\<forall>x\<in>s. norm(f x) \<le> g x"
   2.891 +  shows "norm(integral s f) \<le> (integral s g)"
   2.892 +proof- have *:"\<And>x y. (\<forall>e::real. 0 < e \<longrightarrow> x < y + e) \<longrightarrow> x \<le> y" apply(safe,rule ccontr)
   2.893 +    apply(erule_tac x="x - y" in allE) by auto
   2.894 +  have "\<And>e sg dsa dia ig. norm(sg) \<le> dsa \<longrightarrow> abs(dsa - dia) < e / 2 \<longrightarrow> norm(sg - ig) < e / 2
   2.895 +    \<longrightarrow> norm(ig) < dia + e" 
   2.896 +  proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]])
   2.897 +      apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a
   2.898 +      apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1)
   2.899 +      apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith
   2.900 +  qed note norm=this[rule_format]
   2.901 +  have lem:"\<And>f::real^'n \<Rightarrow> 'a. \<And> g a b. f integrable_on {a..b} \<Longrightarrow> g integrable_on {a..b} \<Longrightarrow>
   2.902 +    \<forall>x\<in>{a..b}. norm(f x) \<le> (g x) \<Longrightarrow> norm(integral({a..b}) f) \<le> (integral({a..b}) g)"
   2.903 +  proof(rule *[rule_format]) case goal1 hence *:"e/2>0" by auto
   2.904 +    from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *]
   2.905 +    guess d1 .. note d1 = conjunctD2[OF this,rule_format]
   2.906 +    from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *]
   2.907 +    guess d2 .. note d2 = conjunctD2[OF this,rule_format]
   2.908 +    note gauge_inter[OF d1(1) d2(1)]
   2.909 +    from fine_division_exists[OF this, of a b] guess p . note p=this
   2.910 +    show ?case apply(rule norm) defer
   2.911 +      apply(rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) defer
   2.912 +      apply(rule d1(2)[OF conjI[OF p(1)]]) defer apply(rule setsum_norm_le)
   2.913 +    proof safe fix x k assume "(x,k)\<in>p" note as = tagged_division_ofD(2-4)[OF p(1) this]
   2.914 +      from this(3) guess u v apply-by(erule exE)+ note uv=this
   2.915 +      show "norm (content k *\<^sub>R f x) \<le> content k *\<^sub>R g x" unfolding uv norm_scaleR
   2.916 +        unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def
   2.917 +        apply(rule mult_left_mono) using goal1(3) as by auto
   2.918 +    qed(insert p[unfolded fine_inter],auto) qed
   2.919 +
   2.920 +  { presume "\<And>e. 0 < e \<Longrightarrow> norm (integral s f) < integral s g + e" 
   2.921 +    thus ?thesis apply-apply(rule *[rule_format]) by auto }
   2.922 +  fix e::real assume "e>0" hence e:"e/2 > 0" by auto
   2.923 +  note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format]
   2.924 +  note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format]
   2.925 +  from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e]
   2.926 +  guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format]
   2.927 +  from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e]
   2.928 +  guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format]
   2.929 +  from bounded_subset_closed_interval[OF bounded_ball, of "0::real^'n" "max B1 B2"]
   2.930 +  guess a b apply-by(erule exE)+ note ab=this[unfolded ball_max_Un]
   2.931 +
   2.932 +  have "ball 0 B1 \<subseteq> {a..b}" using ab by auto
   2.933 +  from B1(2)[OF this] guess z .. note z=conjunctD2[OF this]
   2.934 +  have "ball 0 B2 \<subseteq> {a..b}" using ab by auto
   2.935 +  from B2(2)[OF this] guess w .. note w=conjunctD2[OF this]
   2.936 +
   2.937 +  show "norm (integral s f) < integral s g + e" apply(rule norm)
   2.938 +    apply(rule lem[OF f g, of a b]) unfolding integral_unique[OF z(1)] integral_unique[OF w(1)]
   2.939 +    defer apply(rule w(2)[unfolded real_norm_def],rule z(2))
   2.940 +    apply safe apply(case_tac "x\<in>s") unfolding if_P apply(rule assms(3)[rule_format]) by auto qed
   2.941 +
   2.942 +lemma integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.943 +  assumes "f integrable_on s" "g integrable_on s"  "\<forall>x\<in>s. norm(f x) \<le> (g x)$k"
   2.944 +  shows "norm(integral s f) \<le> (integral s g)$k"
   2.945 +proof- have "norm (integral s f) \<le> integral s ((\<lambda>x. x $ k) o g)"
   2.946 +    apply(rule integral_norm_bound_integral[OF assms(1)])
   2.947 +    apply(rule integrable_linear[OF assms(2)],rule)
   2.948 +    unfolding o_def by(rule assms)
   2.949 +  thus ?thesis unfolding o_def integral_component_eq[OF assms(2)] . qed
   2.950 +
   2.951 +lemma has_integral_norm_bound_integral_component: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.952 +  assumes "(f has_integral i) s" "(g has_integral j) s" "\<forall>x\<in>s. norm(f x) \<le> (g x)$k"
   2.953 +  shows "norm(i) \<le> j$k" using integral_norm_bound_integral_component[of f s g k]
   2.954 +  unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)]
   2.955 +  using assms by auto
   2.956 +
   2.957 +lemma absolutely_integrable_le: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.958 +  assumes "f absolutely_integrable_on s"
   2.959 +  shows "norm(integral s f) \<le> integral s (\<lambda>x. norm(f x))"
   2.960 +  apply(rule integral_norm_bound_integral) using assms by auto
   2.961 +
   2.962 +lemma absolutely_integrable_0[intro]: "(\<lambda>x. 0) absolutely_integrable_on s"
   2.963 +  unfolding absolutely_integrable_on_def by auto
   2.964 +
   2.965 +lemma absolutely_integrable_cmul[intro]:
   2.966 + "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) absolutely_integrable_on s"
   2.967 +  unfolding absolutely_integrable_on_def using integrable_cmul[of f s c]
   2.968 +  using integrable_cmul[of "\<lambda>x. norm (f x)" s "abs c"] by auto
   2.969 +
   2.970 +lemma absolutely_integrable_neg[intro]:
   2.971 + "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. -f(x)) absolutely_integrable_on s"
   2.972 +  apply(drule absolutely_integrable_cmul[where c="-1"]) by auto
   2.973 +
   2.974 +lemma absolutely_integrable_norm[intro]:
   2.975 + "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. norm(f x)) absolutely_integrable_on s"
   2.976 +  unfolding absolutely_integrable_on_def by auto
   2.977 +
   2.978 +lemma absolutely_integrable_abs[intro]:
   2.979 + "f absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. abs(f x::real)) absolutely_integrable_on s"
   2.980 +  apply(drule absolutely_integrable_norm) unfolding real_norm_def .
   2.981 +
   2.982 +lemma absolutely_integrable_on_subinterval: fixes f::"real^'n \<Rightarrow> 'a::banach" shows
   2.983 +  "f absolutely_integrable_on s \<Longrightarrow> {a..b} \<subseteq> s \<Longrightarrow> f absolutely_integrable_on {a..b}" 
   2.984 +  unfolding absolutely_integrable_on_def by(meson integrable_on_subinterval)
   2.985 +
   2.986 +lemma absolutely_integrable_bounded_variation: fixes f::"real^'n \<Rightarrow> 'a::banach"
   2.987 +  assumes "f absolutely_integrable_on UNIV"
   2.988 +  obtains B where "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   2.989 +  apply(rule that[of "integral UNIV (\<lambda>x. norm (f x))"])
   2.990 +proof safe case goal1 note d = division_ofD[OF this(2)]
   2.991 +  have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. integral i (\<lambda>x. norm (f x)))"
   2.992 +    apply(rule setsum_mono,rule absolutely_integrable_le) apply(drule d(4),safe)
   2.993 +    apply(rule absolutely_integrable_on_subinterval[OF assms]) by auto
   2.994 +  also have "... \<le> integral (\<Union>d) (\<lambda>x. norm (f x))"
   2.995 +    apply(subst integral_combine_division_topdown[OF _ goal1(2)])
   2.996 +    using integrable_on_subdivision[OF goal1(2)] using assms by auto
   2.997 +  also have "... \<le> integral UNIV (\<lambda>x. norm (f x))"
   2.998 +    apply(rule integral_subset_le) 
   2.999 +    using integrable_on_subdivision[OF goal1(2)] using assms by auto
  2.1000 +  finally show ?case . qed
  2.1001 +
  2.1002 +lemma helplemma:
  2.1003 +  assumes "setsum (\<lambda>x. norm(f x - g x)) s < e" "finite s"
  2.1004 +  shows "abs(setsum (\<lambda>x. norm(f x)) s - setsum (\<lambda>x. norm(g x)) s) < e"
  2.1005 +  unfolding setsum_subtractf[THEN sym] apply(rule le_less_trans[OF setsum_abs])
  2.1006 +  apply(rule le_less_trans[OF _ assms(1)]) apply(rule setsum_mono)
  2.1007 +  using norm_triangle_ineq3 .
  2.1008 +
  2.1009 +lemma bounded_variation_absolutely_integrable_interval:
  2.1010 +  fixes f::"real^'n \<Rightarrow> real^'m" assumes "f integrable_on {a..b}"
  2.1011 +  "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
  2.1012 +  shows "f absolutely_integrable_on {a..b}"
  2.1013 +proof- let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \<equiv> "Sup ?S"
  2.1014 +  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
  2.1015 +    apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
  2.1016 +    apply(rule setleI) using assms(2) by auto
  2.1017 +  show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i])
  2.1018 +  proof safe case goal1 hence "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
  2.1019 +        {d. d division_of {a..b}}))" using isLub_ubs[OF i,rule_format]
  2.1020 +      unfolding setge_def ubs_def by auto 
  2.1021 +    hence " \<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
  2.1022 +      unfolding mem_Collect_eq isUb_def setle_def by simp then guess d .. note d=conjunctD2[OF this]
  2.1023 +    note d' = division_ofD[OF this(1)]
  2.1024 +
  2.1025 +    have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
  2.1026 +    proof case goal1 have "\<exists>da>0. \<forall>xa\<in>\<Union>{i \<in> d. x \<notin> i}. da \<le> dist x xa"
  2.1027 +        apply(rule separate_point_closed) apply(rule closed_Union)
  2.1028 +        apply(rule finite_subset[OF _ d'(1)]) apply safe apply(drule d'(4)) by auto
  2.1029 +      thus ?case apply safe apply(rule_tac x=da in exI,safe)
  2.1030 +        apply(erule_tac x=xa in ballE) by auto
  2.1031 +    qed from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
  2.1032 +
  2.1033 +    have "e/2 > 0" using goal1 by auto
  2.1034 +    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
  2.1035 +    let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
  2.1036 +    show ?case apply(rule_tac x="?g" in exI) apply safe
  2.1037 +    proof- show "gauge ?g" using g(1) unfolding gauge_def using k(1) by auto
  2.1038 +      fix p assume "p tagged_division_of {a..b}" "?g fine p"
  2.1039 +      note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
  2.1040 +      note p' = tagged_division_ofD[OF p(1)]
  2.1041 +      def p' \<equiv> "{(x,k) | x k. \<exists>i l. x \<in> i \<and> i \<in> d \<and> (x,l) \<in> p \<and> k = i \<inter> l}"
  2.1042 +      have gp':"g fine p'" using p(2) unfolding p'_def fine_def by auto
  2.1043 +      have p'':"p' tagged_division_of {a..b}" apply(rule tagged_division_ofI)
  2.1044 +      proof- show "finite p'" apply(rule finite_subset[of _ "(\<lambda>(k,(x,l)). (x,k \<inter> l))
  2.1045 +          ` {(k,xl) | k xl. k \<in> d \<and> xl \<in> p}"]) unfolding p'_def 
  2.1046 +          defer apply(rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)])
  2.1047 +          apply safe unfolding image_iff apply(rule_tac x="(i,x,l)" in bexI) by auto
  2.1048 +        fix x k assume "(x,k)\<in>p'"
  2.1049 +        hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto
  2.1050 +        then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this]
  2.1051 +        show "x\<in>k" "k\<subseteq>{a..b}" using p'(2-3)[OF il(3)] il by auto
  2.1052 +        show "\<exists>a b. k = {a..b}" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)]
  2.1053 +          apply safe unfolding inter_interval by auto
  2.1054 +      next fix x1 k1 assume "(x1,k1)\<in>p'"
  2.1055 +        hence "\<exists>i l. x1 \<in> i \<and> i \<in> d \<and> (x1, l) \<in> p \<and> k1 = i \<inter> l" unfolding p'_def by auto
  2.1056 +        then guess i1 l1 apply-by(erule exE)+ note il1=conjunctD4[OF this]
  2.1057 +        fix x2 k2 assume "(x2,k2)\<in>p'"
  2.1058 +        hence "\<exists>i l. x2 \<in> i \<and> i \<in> d \<and> (x2, l) \<in> p \<and> k2 = i \<inter> l" unfolding p'_def by auto
  2.1059 +        then guess i2 l2 apply-by(erule exE)+ note il2=conjunctD4[OF this]
  2.1060 +        assume "(x1, k1) \<noteq> (x2, k2)"
  2.1061 +        hence "interior(i1) \<inter> interior(i2) = {} \<or> interior(l1) \<inter> interior(l2) = {}"
  2.1062 +          using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] unfolding il1 il2 by auto
  2.1063 +        thus "interior k1 \<inter> interior k2 = {}" unfolding il1 il2 by auto
  2.1064 +      next have *:"\<forall>(x, X) \<in> p'. X \<subseteq> {a..b}" unfolding p'_def using d' by auto
  2.1065 +        show "\<Union>{k. \<exists>x. (x, k) \<in> p'} = {a..b}" apply rule apply(rule Union_least)
  2.1066 +          unfolding mem_Collect_eq apply(erule exE) apply(drule *[rule_format]) apply safe
  2.1067 +        proof- fix y assume y:"y\<in>{a..b}"
  2.1068 +          hence "\<exists>x l. (x, l) \<in> p \<and> y\<in>l" unfolding p'(6)[THEN sym] by auto
  2.1069 +          then guess x l apply-by(erule exE)+ note xl=conjunctD2[OF this]
  2.1070 +          hence "\<exists>k. k\<in>d \<and> y\<in>k" using y unfolding d'(6)[THEN sym] by auto
  2.1071 +          then guess i .. note i = conjunctD2[OF this]
  2.1072 +          have "x\<in>i" using fineD[OF p(3) xl(1)] using k(2)[OF i(1), of x] using i(2) xl(2) by auto
  2.1073 +          thus "y\<in>\<Union>{k. \<exists>x. (x, k) \<in> p'}" unfolding p'_def Union_iff apply(rule_tac x="i \<inter> l" in bexI)
  2.1074 +            defer unfolding mem_Collect_eq apply(rule_tac x=x in exI)+ apply(rule_tac x="i\<inter>l" in exI)
  2.1075 +            apply safe apply(rule_tac x=i in exI) apply(rule_tac x=l in exI) using i xl by auto 
  2.1076 +        qed qed 
  2.1077 +
  2.1078 +      hence "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
  2.1079 +        apply-apply(rule g(2)[rule_format]) unfolding tagged_division_of_def apply safe using gp' .
  2.1080 +      hence **:" \<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
  2.1081 +        unfolding split_def apply(rule helplemma) using p'' by auto
  2.1082 +
  2.1083 +      have p'alt:"p' = {(x,(i \<inter> l)) | x i l. (x,l) \<in> p \<and> i \<in> d \<and> ~(i \<inter> l = {})}"
  2.1084 +      proof safe case goal2
  2.1085 +        have "x\<in>i" using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) by auto
  2.1086 +        hence "(x, i \<inter> l) \<in> p'" unfolding p'_def apply safe
  2.1087 +          apply(rule_tac x=x in exI,rule_tac x="i\<inter>l" in exI) apply safe using goal2 by auto
  2.1088 +        thus ?case using goal2(3) by auto
  2.1089 +      next fix x k assume "(x,k)\<in>p'"
  2.1090 +        hence "\<exists>i l. x \<in> i \<and> i \<in> d \<and> (x, l) \<in> p \<and> k = i \<inter> l" unfolding p'_def by auto
  2.1091 +        then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this]
  2.1092 +        thus "\<exists>y i l. (x, k) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
  2.1093 +          apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI)
  2.1094 +          using p'(2)[OF il(3)] by auto
  2.1095 +      qed
  2.1096 +      have sum_p':"(\<Sum>(x, k)\<in>p'. norm (integral k f)) = (\<Sum>k\<in>snd ` p'. norm (integral k f))"
  2.1097 +        apply(subst setsum_over_tagged_division_lemma[OF p'',of "\<lambda>k. norm (integral k f)"])
  2.1098 +        unfolding norm_eq_zero apply(rule integral_null,assumption) ..
  2.1099 +      note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
  2.1100 +
  2.1101 +      have *:"\<And>sni sni' sf sf'. abs(sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
  2.1102 +        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs(sf - i) < e" by arith
  2.1103 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e" 
  2.1104 +        unfolding real_norm_def apply(rule *[rule_format,OF **],safe) apply(rule d(2))
  2.1105 +      proof- case goal1 show ?case unfolding sum_p'
  2.1106 +          apply(rule isLubD2[OF i]) using division_of_tagged_division[OF p''] by auto
  2.1107 +      next case goal2 have *:"{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
  2.1108 +          (\<lambda>(k,l). k \<inter> l) ` {(k,l)|k l. k \<in> d \<and> l \<in> snd ` p}" by auto
  2.1109 +        have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>i\<in>d. \<Sum>l\<in>snd ` p. norm (integral (i \<inter> l) f))"
  2.1110 +        proof(rule setsum_mono) case goal1 note k=this
  2.1111 +          from d'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this
  2.1112 +          def d' \<equiv> "{{u..v} \<inter> l |l. l \<in> snd ` p \<and>  ~({u..v} \<inter> l = {})}" note uvab = d'(2)[OF k[unfolded uv]]
  2.1113 +          have "d' division_of {u..v}" apply(subst d'_def) apply(rule division_inter_1) 
  2.1114 +            apply(rule division_of_tagged_division[OF p(1)]) using uvab .
  2.1115 +          hence "norm (integral k f) \<le> setsum (\<lambda>k. norm (integral k f)) d'"
  2.1116 +            unfolding uv apply(subst integral_combine_division_topdown[of _ _ d'])
  2.1117 +            apply(rule integrable_on_subinterval[OF assms(1) uvab]) apply assumption
  2.1118 +            apply(rule setsum_norm_le) by auto
  2.1119 +          also have "... = (\<Sum>k\<in>{k \<inter> l |l. l \<in> snd ` p}. norm (integral k f))"
  2.1120 +            apply(rule setsum_mono_zero_left) apply(subst simple_image)
  2.1121 +            apply(rule finite_imageI)+ apply fact unfolding d'_def uv apply blast
  2.1122 +          proof case goal1 hence "i \<in> {{u..v} \<inter> l |l. l \<in> snd ` p}" by auto
  2.1123 +            from this[unfolded mem_Collect_eq] guess l .. note l=this
  2.1124 +            hence "{u..v} \<inter> l = {}" using goal1 by auto thus ?case using l by auto
  2.1125 +          qed also have "... = (\<Sum>l\<in>snd ` p. norm (integral (k \<inter> l) f))" unfolding  simple_image
  2.1126 +            apply(rule setsum_reindex_nonzero[unfolded o_def])apply(rule finite_imageI,rule p')
  2.1127 +          proof- case goal1 have "interior (k \<inter> l) \<subseteq> interior (l \<inter> y)" apply(subst(2) interior_inter)
  2.1128 +              apply(rule Int_greatest) defer apply(subst goal1(4)) by auto
  2.1129 +            hence *:"interior (k \<inter> l) = {}" using snd_p(5)[OF goal1(1-3)] by auto
  2.1130 +            from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
  2.1131 +            show ?case using * unfolding uv inter_interval content_eq_0_interior[THEN sym] by auto
  2.1132 +          qed finally show ?case .
  2.1133 +        qed also have "... = (\<Sum>(i,l)\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (i\<inter>l) f))"
  2.1134 +          apply(subst sum_sum_product[THEN sym],fact) using p'(1) by auto
  2.1135 +        also have "... = (\<Sum>x\<in>{(i, l) |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral (split op \<inter> x) f))"
  2.1136 +          unfolding split_def ..
  2.1137 +        also have "... = (\<Sum>k\<in>{i \<inter> l |i l. i \<in> d \<and> l \<in> snd ` p}. norm (integral k f))"
  2.1138 +          unfolding * apply(rule setsum_reindex_nonzero[THEN sym,unfolded o_def])
  2.1139 +          apply(rule finite_product_dependent) apply(fact,rule finite_imageI,rule p')
  2.1140 +          unfolding split_paired_all mem_Collect_eq split_conv o_def
  2.1141 +        proof- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)]
  2.1142 +          fix l1 l2 k1 k2 assume as:"(l1, k1) \<noteq> (l2, k2)"  "l1 \<inter> k1 = l2 \<inter> k2" 
  2.1143 +            "\<exists>i l. (l1, k1) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
  2.1144 +            "\<exists>i l. (l2, k2) = (i, l) \<and> i \<in> d \<and> l \<in> snd ` p"
  2.1145 +          hence "l1 \<in> d" "k1 \<in> snd ` p" by auto from d'(4)[OF this(1)] *(1)[OF this(2)]
  2.1146 +          guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
  2.1147 +          have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" using as by auto
  2.1148 +          hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" apply-
  2.1149 +            apply(erule disjE) apply(rule disjI2) apply(rule d'(5)) prefer 4 apply(rule disjI1)
  2.1150 +            apply(rule *) using as by auto
  2.1151 +          moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" using as(2) by auto
  2.1152 +          ultimately have "interior(l1 \<inter> k1) = {}" by auto
  2.1153 +          thus "norm (integral (l1 \<inter> k1) f) = 0" unfolding uv inter_interval
  2.1154 +            unfolding content_eq_0_interior[THEN sym] by auto
  2.1155 +        qed also have "... = (\<Sum>(x, k)\<in>p'. norm (integral k f))" unfolding sum_p'
  2.1156 +          apply(rule setsum_mono_zero_right) apply(subst *)
  2.1157 +          apply(rule finite_imageI[OF finite_product_dependent]) apply fact
  2.1158 +          apply(rule finite_imageI[OF p'(1)]) apply safe
  2.1159 +        proof- case goal2 have "ia \<inter> b = {}" using goal2 unfolding p'alt image_iff Bex_def not_ex
  2.1160 +            apply(erule_tac x="(a,ia\<inter>b)" in allE) by auto thus ?case by auto
  2.1161 +        next case goal1 thus ?case unfolding p'_def apply safe
  2.1162 +            apply(rule_tac x=i in exI,rule_tac x=l in exI) unfolding snd_conv image_iff 
  2.1163 +            apply safe apply(rule_tac x="(a,l)" in bexI) by auto
  2.1164 +        qed finally show ?case .
  2.1165 +
  2.1166 +      next case goal3
  2.1167 +        let ?S = "{(x, i \<inter> l) |x i l. (x, l) \<in> p \<and> i \<in> d}"
  2.1168 +        have Sigma_alt:"\<And>s t. s \<times> t = {(i, j) |i j. i \<in> s \<and> j \<in> t}" by auto
  2.1169 +        have *:"?S = (\<lambda>(xl,i). (fst xl, snd xl \<inter> i)) ` (p \<times> d)" (*{(xl,i)|xl i. xl\<in>p \<and> i\<in>d}"**)
  2.1170 +          apply safe unfolding image_iff apply(rule_tac x="((x,l),i)" in bexI) by auto
  2.1171 +        note pdfin = finite_cartesian_product[OF p'(1) d'(1)]
  2.1172 +        have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x)) = (\<Sum>(x, k)\<in>?S. \<bar>content k\<bar> * norm (f x))"
  2.1173 +          unfolding norm_scaleR apply(rule setsum_mono_zero_left)
  2.1174 +          apply(subst *, rule finite_imageI) apply fact unfolding p'alt apply blast
  2.1175 +          apply safe apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) by auto
  2.1176 +        also have "... = (\<Sum>((x,l),i)\<in>p \<times> d. \<bar>content (l \<inter> i)\<bar> * norm (f x))" unfolding *
  2.1177 +          apply(subst setsum_reindex_nonzero,fact) unfolding split_paired_all
  2.1178 +          unfolding  o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq apply(erule_tac conjE)+
  2.1179 +        proof- fix x1 l1 k1 x2 l2 k2 assume as:"(x1,l1)\<in>p" "(x2,l2)\<in>p" "k1\<in>d" "k2\<in>d"
  2.1180 +            "x1 = x2" "l1 \<inter> k1 = l2 \<inter> k2" "\<not> ((x1 = x2 \<and> l1 = l2) \<and> k1 = k2)"
  2.1181 +          from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this
  2.1182 +          from as have "l1 \<noteq> l2 \<or> k1 \<noteq> k2" by auto
  2.1183 +          hence "(interior(k1) \<inter> interior(k2) = {} \<or> interior(l1) \<inter> interior(l2) = {})" 
  2.1184 +            apply-apply(erule disjE) apply(rule disjI2) defer apply(rule disjI1)
  2.1185 +            apply(rule d'(5)[OF as(3-4)],assumption) apply(rule p'(5)[OF as(1-2)]) by auto
  2.1186 +          moreover have "interior(l1 \<inter> k1) = interior(l2 \<inter> k2)" unfolding  as ..
  2.1187 +          ultimately have "interior (l1 \<inter> k1) = {}" by auto
  2.1188 +          thus "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0" unfolding uv inter_interval
  2.1189 +            unfolding content_eq_0_interior[THEN sym] by auto
  2.1190 +        qed safe also have "... = (\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x))" unfolding Sigma_alt
  2.1191 +          apply(subst sum_sum_product[THEN sym]) apply(rule p', rule,rule d')
  2.1192 +          apply(rule setsum_cong2) unfolding split_paired_all split_conv
  2.1193 +        proof- fix x l assume as:"(x,l)\<in>p"
  2.1194 +          note xl = p'(2-4)[OF this] from this(3) guess u v apply-by(erule exE)+ note uv=this
  2.1195 +          have "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar>) = (\<Sum>k\<in>d. content (k \<inter> {u..v}))"
  2.1196 +            apply(rule setsum_cong2) apply(drule d'(4),safe) apply(subst Int_commute)
  2.1197 +            unfolding inter_interval uv apply(subst abs_of_nonneg) by auto
  2.1198 +          also have "... = setsum content {k\<inter>{u..v}| k. k\<in>d}" unfolding simple_image
  2.1199 +            apply(rule setsum_reindex_nonzero[unfolded o_def,THEN sym]) apply(rule d')
  2.1200 +          proof- case goal1 from d'(4)[OF this(1)] d'(4)[OF this(2)]
  2.1201 +            guess u1 v1 u2 v2 apply- by(erule exE)+ note uv=this
  2.1202 +            have "{} = interior ((k \<inter> y) \<inter> {u..v})" apply(subst interior_inter)
  2.1203 +              using d'(5)[OF goal1(1-3)] by auto
  2.1204 +            also have "... = interior (y \<inter> (k \<inter> {u..v}))" by auto
  2.1205 +            also have "... = interior (k \<inter> {u..v})" unfolding goal1(4) by auto
  2.1206 +            finally show ?case unfolding uv inter_interval content_eq_0_interior ..
  2.1207 +          qed also have "... = setsum content {{u..v} \<inter> k |k. k \<in> d \<and> ~({u..v} \<inter> k = {})}"
  2.1208 +            apply(rule setsum_mono_zero_right) unfolding simple_image
  2.1209 +            apply(rule finite_imageI,rule d') apply blast apply safe
  2.1210 +            apply(rule_tac x=k in exI)
  2.1211 +          proof- case goal1 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this
  2.1212 +            have "interior (k \<inter> {u..v}) \<noteq> {}" using goal1(2)
  2.1213 +              unfolding ab inter_interval content_eq_0_interior by auto
  2.1214 +            thus ?case using goal1(1) using interior_subset[of "k \<inter> {u..v}"] by auto
  2.1215 +          qed finally show "(\<Sum>i\<in>d. \<bar>content (l \<inter> i)\<bar> * norm (f x)) = content l *\<^sub>R norm (f x)"
  2.1216 +            unfolding setsum_left_distrib[THEN sym] real_scaleR_def apply -
  2.1217 +            apply(subst(asm) additive_content_division[OF division_inter_1[OF d(1)]])
  2.1218 +            using xl(2)[unfolded uv] unfolding uv by auto
  2.1219 +        qed finally show ?case . 
  2.1220 +      qed qed qed qed 
  2.1221 +
  2.1222 +lemma bounded_variation_absolutely_integrable:  fixes f::"real^'n \<Rightarrow> real^'m"
  2.1223 +  assumes "f integrable_on UNIV" "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
  2.1224 +  shows "f absolutely_integrable_on UNIV"
  2.1225 +proof(rule absolutely_integrable_onI,fact,rule)
  2.1226 +  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}" def i \<equiv> "Sup ?S"
  2.1227 +  have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
  2.1228 +    apply(rule elementary_interval) defer apply(rule_tac x=B in exI)
  2.1229 +    apply(rule setleI) using assms(2) by auto
  2.1230 +  have f_int:"\<And>a b. f absolutely_integrable_on {a..b}"
  2.1231 +    apply(rule bounded_variation_absolutely_integrable_interval[where B=B])
  2.1232 +    apply(rule integrable_on_subinterval[OF assms(1)]) defer apply safe
  2.1233 +    apply(rule assms(2)[rule_format]) by auto 
  2.1234 +  show "((\<lambda>x. norm (f x)) has_integral i) UNIV" apply(subst has_integral_alt',safe)
  2.1235 +  proof- case goal1 show ?case using f_int[of a b] by auto
  2.1236 +  next case goal2 have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
  2.1237 +    proof(rule ccontr) case goal1 hence "i \<le> i - e" apply-
  2.1238 +        apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by auto
  2.1239 +      thus False using goal2 by auto
  2.1240 +    qed then guess K .. note * = this[unfolded image_iff not_le]
  2.1241 +    from this(1) guess d .. note this[unfolded mem_Collect_eq]
  2.1242 +    note d = this(1) *(2)[unfolded this(2)] note d'=division_ofD[OF this(1)]
  2.1243 +    have "bounded (\<Union>d)" by(rule elementary_bounded,fact)
  2.1244 +    from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this]
  2.1245 +    show ?case apply(rule_tac x="K + 1" in exI,safe)
  2.1246 +    proof- fix a b assume ab:"ball 0 (K + 1) \<subseteq> {a..b::real^'n}"
  2.1247 +      have *:"\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs(s - i) < (e::real)" by arith
  2.1248 +      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
  2.1249 +        unfolding real_norm_def apply(rule *[rule_format],safe) apply(rule d(2))
  2.1250 +      proof- case goal1 have "(\<Sum>k\<in>d. norm (integral k f)) \<le> setsum (\<lambda>k. integral k (\<lambda>x. norm (f x))) d"
  2.1251 +          apply(rule setsum_mono) apply(rule absolutely_integrable_le)
  2.1252 +          apply(drule d'(4),safe) by(rule f_int)
  2.1253 +        also have "... = integral (\<Union>d) (\<lambda>x. norm(f x))" 
  2.1254 +          apply(rule integral_combine_division_bottomup[THEN sym])
  2.1255 +          apply(rule d) unfolding forall_in_division[OF d(1)] using f_int by auto
  2.1256 +        also have "... \<le> integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0)" 
  2.1257 +        proof- case goal1 have "\<Union>d \<subseteq> {a..b}" apply rule apply(drule K(2)[rule_format]) 
  2.1258 +            apply(rule ab[unfolded subset_eq,rule_format]) by(auto simp add:dist_norm)
  2.1259 +          thus ?case apply- apply(subst if_P,rule) apply(rule integral_subset_le) defer
  2.1260 +            apply(rule integrable_on_subdivision[of _ _ _ "{a..b}"])
  2.1261 +            apply(rule d) using f_int[of a b] by auto
  2.1262 +        qed finally show ?case .
  2.1263 +
  2.1264 +      next note f = absolutely_integrable_onD[OF f_int[of a b]]
  2.1265 +        note * = this(2)[unfolded has_integral_integral has_integral[of "\<lambda>x. norm (f x)"],rule_format]
  2.1266 +        have "e/2>0" using `e>0` by auto from *[OF this] guess d1 .. note d1=conjunctD2[OF this]
  2.1267 +        from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
  2.1268 +        from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
  2.1269 +        note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
  2.1270 +        have *:"\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs(sf - si) < e / 2
  2.1271 +          \<longrightarrow> abs(sf' - di) < e / 2 \<longrightarrow> di < i + e" by arith
  2.1272 +        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e" apply(subst if_P,rule)
  2.1273 +        proof(rule *[rule_format]) 
  2.1274 +          show "\<bar>(\<Sum>(x,k)\<in>p. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p. norm (integral k f))\<bar> < e / 2"
  2.1275 +            unfolding split_def apply(rule helplemma) using d2(2)[rule_format,of p]
  2.1276 +            using p(1,3) unfolding tagged_division_of_def split_def by auto
  2.1277 +          show "abs ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - integral {a..b} (\<lambda>x. norm(f x))) < e / 2"
  2.1278 +            using d1(2)[rule_format,OF conjI[OF p(1,2)]] unfolding real_norm_def .
  2.1279 +          show "(\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) = (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x))"
  2.1280 +            apply(rule setsum_cong2) unfolding split_paired_all split_conv
  2.1281 +            apply(drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR
  2.1282 +            apply(subst abs_of_nonneg) by auto
  2.1283 +          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
  2.1284 +            apply(subst setsum_over_tagged_division_lemma[OF p(1)]) defer apply(rule isLubD2[OF i])
  2.1285 +            unfolding image_iff apply(rule_tac x="snd ` p" in bexI) unfolding mem_Collect_eq defer
  2.1286 +            apply(rule partial_division_of_tagged_division[of _ "{a..b}"])
  2.1287 +            using p(1) unfolding tagged_division_of_def by auto
  2.1288 +        qed qed qed(insert K,auto) qed qed 
  2.1289 +
  2.1290 +lemma absolutely_integrable_restrict_univ:
  2.1291 + "(\<lambda>x. if x \<in> s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \<longleftrightarrow> f absolutely_integrable_on s"
  2.1292 +  unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ ..
  2.1293 +
  2.1294 +lemma absolutely_integrable_add[intro]: fixes f g::"real^'n \<Rightarrow> real^'m"
  2.1295 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1296 +  shows "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on s"
  2.1297 +proof- let ?P = "\<And>f g::real^'n \<Rightarrow> real^'m. f absolutely_integrable_on UNIV \<Longrightarrow>
  2.1298 +    g absolutely_integrable_on UNIV \<Longrightarrow> (\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV"
  2.1299 +  { presume as:"PROP ?P" note a = absolutely_integrable_restrict_univ[THEN sym]
  2.1300 +    have *:"\<And>x. (if x \<in> s then f x else 0) + (if x \<in> s then g x else 0)
  2.1301 +      = (if x \<in> s then f x + g x else 0)" by auto
  2.1302 +    show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] unfolding * . }
  2.1303 +  fix f g::"real^'n \<Rightarrow> real^'m" assume assms:"f absolutely_integrable_on UNIV"
  2.1304 +    "g absolutely_integrable_on UNIV" 
  2.1305 +  note absolutely_integrable_bounded_variation
  2.1306 +  from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format]
  2.1307 +  show "(\<lambda>x. f(x) + g(x)) absolutely_integrable_on UNIV"
  2.1308 +    apply(rule bounded_variation_absolutely_integrable[of _ "B1+B2"])
  2.1309 +    apply(rule integrable_add) prefer 3
  2.1310 +  proof safe case goal1 have "\<And>k. k \<in> d \<Longrightarrow> f integrable_on k \<and> g integrable_on k"
  2.1311 +      apply(drule division_ofD(4)[OF goal1]) apply safe
  2.1312 +      apply(rule_tac[!] integrable_on_subinterval[of _ UNIV]) using assms by auto
  2.1313 +    hence "(\<Sum>k\<in>d. norm (integral k (\<lambda>x. f x + g x))) \<le>
  2.1314 +      (\<Sum>k\<in>d. norm (integral k f)) + (\<Sum>k\<in>d. norm (integral k g))" apply-
  2.1315 +      unfolding setsum_addf[THEN sym] apply(rule setsum_mono)
  2.1316 +      apply(subst integral_add) prefer 3 apply(rule norm_triangle_ineq) by auto
  2.1317 +    also have "... \<le> B1 + B2" using B(1)[OF goal1] B(2)[OF goal1] by auto
  2.1318 +    finally show ?case .
  2.1319 +  qed(insert assms,auto) qed
  2.1320 +
  2.1321 +lemma absolutely_integrable_sub[intro]: fixes f g::"real^'n \<Rightarrow> real^'m"
  2.1322 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1323 +  shows "(\<lambda>x. f(x) - g(x)) absolutely_integrable_on s"
  2.1324 +  using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]]
  2.1325 +  unfolding group_simps .
  2.1326 +
  2.1327 +lemma absolutely_integrable_linear: fixes f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
  2.1328 +  assumes "f absolutely_integrable_on s" "bounded_linear h"
  2.1329 +  shows "(h o f) absolutely_integrable_on s"
  2.1330 +proof- { presume as:"\<And>f::real^'m \<Rightarrow> real^'n. \<And>h::real^'n \<Rightarrow> real^'p. 
  2.1331 +    f absolutely_integrable_on UNIV \<Longrightarrow> bounded_linear h \<Longrightarrow>
  2.1332 +    (h o f) absolutely_integrable_on UNIV" note a = absolutely_integrable_restrict_univ[THEN sym]
  2.1333 +    show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]]
  2.1334 +      unfolding o_def if_distrib linear_simps[OF assms(2)] . }
  2.1335 +  fix f::"real^'m \<Rightarrow> real^'n" and h::"real^'n \<Rightarrow> real^'p"
  2.1336 +  assume assms:"f absolutely_integrable_on UNIV" "bounded_linear h" 
  2.1337 +  from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this
  2.1338 +  from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this]
  2.1339 +  show "(h o f) absolutely_integrable_on UNIV"
  2.1340 +    apply(rule bounded_variation_absolutely_integrable[of _ "B * b"])
  2.1341 +    apply(rule integrable_linear[OF _ assms(2)]) 
  2.1342 +  proof safe case goal2
  2.1343 +    have "(\<Sum>k\<in>d. norm (integral k (h \<circ> f))) \<le> setsum (\<lambda>k. norm(integral k f)) d * b"
  2.1344 +      unfolding setsum_left_distrib apply(rule setsum_mono)
  2.1345 +    proof- case goal1 from division_ofD(4)[OF goal2 this]
  2.1346 +      guess u v apply-by(erule exE)+ note uv=this
  2.1347 +      have *:"f integrable_on k" unfolding uv apply(rule integrable_on_subinterval[of _ UNIV])
  2.1348 +        using assms by auto note this[unfolded has_integral_integral]
  2.1349 +      note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)]
  2.1350 +      note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)]
  2.1351 +      show ?case unfolding * using b by auto
  2.1352 +    qed also have "... \<le> B * b" apply(rule mult_right_mono) using B goal2 b by auto
  2.1353 +    finally show ?case .
  2.1354 +  qed(insert assms,auto) qed
  2.1355 +
  2.1356 +lemma absolutely_integrable_setsum: fixes f::"'a \<Rightarrow> real^'n \<Rightarrow> real^'m"
  2.1357 +  assumes "finite t" "\<And>a. a \<in> t \<Longrightarrow> (f a) absolutely_integrable_on s"
  2.1358 +  shows "(\<lambda>x. setsum (\<lambda>a. f a x) t) absolutely_integrable_on s"
  2.1359 +  using assms(1,2) apply induct defer apply(subst setsum.insert) apply assumption+ by(rule,auto)
  2.1360 +
  2.1361 +lemma absolutely_integrable_vector_abs:
  2.1362 +  assumes "f absolutely_integrable_on s"
  2.1363 +  shows "(\<lambda>x. (\<chi> i. abs(f x$i))::real^'n) absolutely_integrable_on s"
  2.1364 +proof- have *:"\<And>x. ((\<chi> i. abs(f x$i))::real^'n) = (setsum (\<lambda>i.
  2.1365 +    (((\<lambda>y. (\<chi> j. if j = i then y$1 else 0)) o
  2.1366 +    (vec1 o ((\<lambda>x. (norm((\<chi> j. if j = i then x$i else 0)::real^'n))) o f))) x)) UNIV)"
  2.1367 +    unfolding Cart_eq setsum_component Cart_lambda_beta
  2.1368 +  proof case goal1 have *:"\<And>i xa. ((if i = xa then f x $ xa else 0) \<bullet> (if i = xa then f x $ xa else 0)) =
  2.1369 +      (if i = xa then (f x $ xa) * (f x $ xa) else 0)" by auto
  2.1370 +    have "\<bar>f x $ i\<bar> = (setsum (\<lambda>k. if k = i then abs ((f x)$i) else 0) UNIV)"
  2.1371 +      unfolding setsum_delta[OF finite_UNIV] by auto
  2.1372 +    also have "... = (\<Sum>xa\<in>UNIV. ((\<lambda>y. \<chi> j. if j = xa then dest_vec1 y else 0) \<circ>
  2.1373 +                      (\<lambda>x. vec1 (norm (\<chi> j. if j = xa then x $ xa else 0))) \<circ> f) x $ i)"
  2.1374 +      unfolding norm_eq_sqrt_inner inner_vector_def Cart_lambda_beta o_def *
  2.1375 +      apply(rule setsum_cong2) unfolding setsum_delta[OF finite_UNIV] by auto 
  2.1376 +    finally show ?case unfolding o_def . qed
  2.1377 +  show ?thesis unfolding * apply(rule absolutely_integrable_setsum) apply(rule finite_UNIV)
  2.1378 +    apply(rule absolutely_integrable_linear) 
  2.1379 +    unfolding absolutely_integrable_on_trans unfolding o_def apply(rule absolutely_integrable_norm)
  2.1380 +    apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear
  2.1381 +    apply(rule_tac[!] linearI) unfolding Cart_eq by auto
  2.1382 +qed
  2.1383 +
  2.1384 +lemma absolutely_integrable_max: fixes f::"real^'m \<Rightarrow> real^'n"
  2.1385 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1386 +  shows "(\<lambda>x. (\<chi> i. max (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s"
  2.1387 +proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((\<chi> i. \<bar>(f x - g x) $ i\<bar>) + (f x + g x)) = (\<chi> i. max (f(x)$i) (g(x)$i))"
  2.1388 +    unfolding Cart_eq by auto
  2.1389 +  note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms]
  2.1390 +  note absolutely_integrable_vector_abs[OF this(1)] this(2)
  2.1391 +  note absolutely_integrable_add[OF this] note absolutely_integrable_cmul[OF this,of "1/2"]
  2.1392 +  thus ?thesis unfolding * . qed
  2.1393 +
  2.1394 +lemma absolutely_integrable_max_real: fixes f::"real^'m \<Rightarrow> real"
  2.1395 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1396 +  shows "(\<lambda>x. max (f x) (g x)) absolutely_integrable_on s"
  2.1397 +proof- have *:"(\<lambda>x. \<chi> i. max ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. max (f x) (g x))"
  2.1398 +    apply rule unfolding Cart_eq by auto note absolutely_integrable_max[of "vec1 o f" s "vec1 o g"]
  2.1399 +  note this[unfolded absolutely_integrable_on_trans,OF assms]
  2.1400 +  thus ?thesis unfolding * by auto qed
  2.1401 +
  2.1402 +lemma absolutely_integrable_min: fixes f::"real^'m \<Rightarrow> real^'n"
  2.1403 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1404 +  shows "(\<lambda>x. (\<chi> i. min (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s"
  2.1405 +proof- have *:"\<And>x. (1 / 2) *\<^sub>R ((f x + g x) - (\<chi> i. \<bar>(f x - g x) $ i\<bar>)) = (\<chi> i. min (f(x)$i) (g(x)$i))"
  2.1406 +    unfolding Cart_eq by auto
  2.1407 +  note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms]
  2.1408 +  note this(1) absolutely_integrable_vector_abs[OF this(2)]
  2.1409 +  note absolutely_integrable_sub[OF this] note absolutely_integrable_cmul[OF this,of "1/2"]
  2.1410 +  thus ?thesis unfolding * . qed
  2.1411 +
  2.1412 +lemma absolutely_integrable_min_real: fixes f::"real^'m \<Rightarrow> real"
  2.1413 +  assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s"
  2.1414 +  shows "(\<lambda>x. min (f x) (g x)) absolutely_integrable_on s"
  2.1415 +proof- have *:"(\<lambda>x. \<chi> i. min ((vec1 \<circ> f) x $ i) ((vec1 \<circ> g) x $ i)) = vec1 o (\<lambda>x. min (f x) (g x))"
  2.1416 +    apply rule unfolding Cart_eq by auto note absolutely_integrable_min[of "vec1 o f" s "vec1 o g"]
  2.1417 +  note this[unfolded absolutely_integrable_on_trans,OF assms]
  2.1418 +  thus ?thesis unfolding * by auto qed
  2.1419 +
  2.1420 +lemma absolutely_integrable_abs_eq: fixes f::"real^'n \<Rightarrow> real^'m"
  2.1421 +  shows "f absolutely_integrable_on s \<longleftrightarrow> f integrable_on s \<and>
  2.1422 +          (\<lambda>x. (\<chi> i. abs(f x$i))::real^'m) integrable_on s" (is "?l = ?r")
  2.1423 +proof assume ?l thus ?r apply-apply rule defer
  2.1424 +    apply(drule absolutely_integrable_vector_abs) by auto
  2.1425 +next assume ?r { presume lem:"\<And>f::real^'n \<Rightarrow> real^'m. f integrable_on UNIV \<Longrightarrow>
  2.1426 +    (\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
  2.1427 +    have *:"\<And>x. (\<chi> i. \<bar>(if x \<in> s then f x else 0) $ i\<bar>) = (if x\<in>s then (\<chi> i. \<bar>f x $ i\<bar>) else 0)"
  2.1428 +      unfolding Cart_eq by auto
  2.1429 +    show ?l apply(subst absolutely_integrable_restrict_univ[THEN sym]) apply(rule lem)
  2.1430 +      unfolding integrable_restrict_univ * using `?r` by auto }
  2.1431 +  fix f::"real^'n \<Rightarrow> real^'m" assume assms:"f integrable_on UNIV"
  2.1432 +    "(\<lambda>x. (\<chi> i. abs(f(x)$i))::real^'m) integrable_on UNIV"
  2.1433 +  let ?B = "setsum (\<lambda>i. integral UNIV (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ i) UNIV"
  2.1434 +  show "f absolutely_integrable_on UNIV"
  2.1435 +    apply(rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"],safe)
  2.1436 +  proof- case goal1 note d=this and d'=division_ofD[OF this]
  2.1437 +    have "(\<Sum>k\<in>d. norm (integral k f)) \<le>
  2.1438 +      (\<Sum>k\<in>d. setsum (op $ (integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV)" apply(rule setsum_mono)
  2.1439 +      apply(rule order_trans[OF norm_le_l1],rule setsum_mono)
  2.1440 +    proof- fix k and i::'m assume "k\<in>d"
  2.1441 +      from d'(4)[OF this] guess a b apply-by(erule exE)+ note ab=this
  2.1442 +      show "\<bar>integral k f $ i\<bar> \<le> integral k (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ i" apply(rule abs_leI)
  2.1443 +        unfolding vector_uminus_component[THEN sym] defer apply(subst integral_neg[THEN sym])
  2.1444 +        defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg)
  2.1445 +        using integrable_on_subinterval[OF assms(1),of a b]
  2.1446 +          integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto
  2.1447 +    qed also have "... \<le> setsum (op $ (integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>))) UNIV"
  2.1448 +      apply(subst setsum_commute,rule setsum_mono)
  2.1449 +    proof- case goal1 have *:"(\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) integrable_on \<Union>d"
  2.1450 +        using integrable_on_subdivision[OF d assms(2)] by auto
  2.1451 +      have "(\<Sum>i\<in>d. integral i (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j)
  2.1452 +        = integral (\<Union>d) (\<lambda>x. (\<chi> j. abs(f x$j)) ::real^'m) $ j"
  2.1453 +        unfolding setsum_component[THEN sym]
  2.1454 +        apply(subst integral_combine_division_topdown[THEN sym,OF * d]) by auto
  2.1455 +      also have "... \<le> integral UNIV (\<lambda>x. \<chi> j. \<bar>f x $ j\<bar>) $ j"
  2.1456 +        apply(rule integral_subset_component_le) using assms * by auto
  2.1457 +      finally show ?case .
  2.1458 +    qed finally show ?case . qed qed
  2.1459 +
  2.1460 +lemma nonnegative_absolutely_integrable: fixes f::"real^'n \<Rightarrow> real^'m"
  2.1461 +  assumes "\<forall>x\<in>s. \<forall>i. 0 \<le> f(x)$i" "f integrable_on s"
  2.1462 +  shows "f absolutely_integrable_on s"
  2.1463 +  unfolding absolutely_integrable_abs_eq apply rule defer
  2.1464 +  apply(rule integrable_eq[of _ f]) unfolding Cart_eq using assms by auto
  2.1465 +
  2.1466 +lemma absolutely_integrable_integrable_bound: fixes f::"real^'n \<Rightarrow> real^'m"
  2.1467 +  assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s"
  2.1468 +  shows "f absolutely_integrable_on s"
  2.1469 +proof- { presume *:"\<And>f::real^'n \<Rightarrow> real^'m. \<And> g. \<forall>x. norm(f x) \<le> g x \<Longrightarrow> f integrable_on UNIV
  2.1470 +    \<Longrightarrow> g integrable_on UNIV \<Longrightarrow> f absolutely_integrable_on UNIV"
  2.1471 +    show ?thesis apply(subst absolutely_integrable_restrict_univ[THEN sym])
  2.1472 +      apply(rule *[of _ "\<lambda>x. if x\<in>s then g x else 0"])
  2.1473 +      using assms unfolding integrable_restrict_univ by auto }
  2.1474 +  fix g and f :: "real^'n \<Rightarrow> real^'m"
  2.1475 +  assume assms:"\<forall>x. norm(f x) \<le> g x" "f integrable_on UNIV" "g integrable_on UNIV"
  2.1476 +  show "f absolutely_integrable_on UNIV"
  2.1477 +    apply(rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"])
  2.1478 +  proof safe case goal1 note d=this and d'=division_ofD[OF this]
  2.1479 +    have "(\<Sum>k\<in>d. norm (integral k f)) \<le> (\<Sum>k\<in>d. integral k g)"
  2.1480 +      apply(rule setsum_mono) apply(rule integral_norm_bound_integral) apply(drule_tac[!] d'(4),safe) 
  2.1481 +      apply(rule_tac[1-2] integrable_on_subinterval) using assms by auto
  2.1482 +    also have "... = integral (\<Union>d) g" apply(rule integral_combine_division_bottomup[THEN sym])
  2.1483 +      apply(rule d,safe) apply(drule d'(4),safe)
  2.1484 +      apply(rule integrable_on_subinterval[OF assms(3)]) by auto
  2.1485 +    also have "... \<le> integral UNIV g" apply(rule integral_subset_le) defer
  2.1486 +      apply(rule integrable_on_subdivision[OF d,of _ UNIV]) prefer 4
  2.1487 +      apply(rule,rule_tac y="norm (f x)" in order_trans) using assms by auto
  2.1488 +    finally show ?case . qed qed
  2.1489 +
  2.1490 +lemma absolutely_integrable_integrable_bound_real: fixes f::"real^'n \<Rightarrow> real"
  2.1491 +  assumes "\<forall>x\<in>s. norm(f x) \<le> g x" "f integrable_on s" "g integrable_on s"
  2.1492 +  shows "f absolutely_integrable_on s"
  2.1493 +  apply(subst absolutely_integrable_on_trans[THEN sym])
  2.1494 +  apply(rule absolutely_integrable_integrable_bound[where g=g])
  2.1495 +  using assms unfolding o_def by auto
  2.1496 +
  2.1497 +lemma absolutely_integrable_absolutely_integrable_bound:
  2.1498 +  fixes f::"real^'n \<Rightarrow> real^'m" and g::"real^'n \<Rightarrow> real^'p"
  2.1499 +  assumes "\<forall>x\<in>s. norm(f x) \<le> norm(g x)" "f integrable_on s" "g absolutely_integrable_on s"
  2.1500 +  shows "f absolutely_integrable_on s"
  2.1501 +  apply(rule absolutely_integrable_integrable_bound[of s f "\<lambda>x. norm (g x)"])
  2.1502 +  using assms by auto
  2.1503 +
  2.1504 +lemma absolutely_integrable_inf_real:
  2.1505 +  assumes "finite k" "k \<noteq> {}"
  2.1506 +  "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  2.1507 +  shows "(\<lambda>x. (Inf ((fs x) ` k))) absolutely_integrable_on s" using assms
  2.1508 +proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a
  2.1509 +         else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s"
  2.1510 +  show ?case unfolding image_insert
  2.1511 +    apply(subst Inf_insert_finite) apply(rule finite_imageI[OF insert(1)])
  2.1512 +  proof(cases "k={}") case True
  2.1513 +    thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto
  2.1514 +  next case False thus ?P apply(subst if_not_P) defer
  2.1515 +      apply(rule absolutely_integrable_min_real) 
  2.1516 +      defer apply(rule insert(3)[OF False]) using insert(5) by auto
  2.1517 +  qed qed auto
  2.1518 +
  2.1519 +lemma absolutely_integrable_sup_real:
  2.1520 +  assumes "finite k" "k \<noteq> {}"
  2.1521 +  "\<forall>i\<in>k. (\<lambda>x. (fs x i)::real) absolutely_integrable_on s"
  2.1522 +  shows "(\<lambda>x. (Sup ((fs x) ` k))) absolutely_integrable_on s" using assms
  2.1523 +proof induct case (insert a k) let ?P = " (\<lambda>x. if fs x ` k = {} then fs x a
  2.1524 +         else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s"
  2.1525 +  show ?case unfolding image_insert
  2.1526 +    apply(subst Sup_insert_finite) apply(rule finite_imageI[OF insert(1)])
  2.1527 +  proof(cases "k={}") case True
  2.1528 +    thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto
  2.1529 +  next case False thus ?P apply(subst if_not_P) defer
  2.1530 +      apply(rule absolutely_integrable_max_real) 
  2.1531 +      defer apply(rule insert(3)[OF False]) using insert(5) by auto
  2.1532 +  qed qed auto
  2.1533 +
  2.1534 +subsection {* Dominated convergence. *}
  2.1535 +
  2.1536 +lemma dominated_convergence: fixes f::"nat \<Rightarrow> real^'n \<Rightarrow> real"
  2.1537 +  assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
  2.1538 +  "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
  2.1539 +  "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
  2.1540 +  shows "g integrable_on s" "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
  2.1541 +proof- have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
  2.1542 +    ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
  2.1543 +    integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
  2.1544 +  proof(rule monotone_convergence_decreasing_real,safe) fix m::nat
  2.1545 +    show "bounded {integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) |k. True}"
  2.1546 +      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  2.1547 +    proof safe fix k::nat
  2.1548 +      show "norm (integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  2.1549 +        apply(rule integral_norm_bound_integral) unfolding simple_image
  2.1550 +        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real)
  2.1551 +        prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge)
  2.1552 +        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
  2.1553 +        using assms unfolding real_norm_def by auto
  2.1554 +    qed fix k::nat show "(\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  2.1555 +      unfolding simple_image apply(rule absolutely_integrable_onD)
  2.1556 +      apply(rule absolutely_integrable_inf_real) prefer 3 
  2.1557 +      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
  2.1558 +    fix x assume x:"x\<in>s" show "Inf {f j x |j. j \<in> {m..m + Suc k}}
  2.1559 +      \<le> Inf {f j x |j. j \<in> {m..m + k}}" apply(rule Inf_ge) unfolding setge_def
  2.1560 +      defer apply rule apply(subst Inf_finite_le_iff) prefer 3
  2.1561 +      apply(rule_tac x=xa in bexI) by auto
  2.1562 +    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Inf ?S"
  2.1563 +    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
  2.1564 +      unfolding Lim_sequentially
  2.1565 +    proof safe case goal1 note e=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf)
  2.1566 +        defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def
  2.1567 +      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
  2.1568 +      qed auto
  2.1569 +
  2.1570 +      have "\<exists>y\<in>?S. \<not> y \<ge> i + e"
  2.1571 +      proof(rule ccontr) case goal1 hence "i \<ge> i + e" apply-
  2.1572 +          apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastsimp+
  2.1573 +        thus False using e by auto
  2.1574 +      qed then guess y .. note y=this[unfolded not_le]
  2.1575 +      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
  2.1576 +      
  2.1577 +      show ?case apply(rule_tac x=N in exI)
  2.1578 +      proof safe case goal1
  2.1579 +        have *:"\<And>y ix. y < i + e \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < e" by arith
  2.1580 +        show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)])
  2.1581 +          unfolding i_def apply(rule real_le_inf_subset) prefer 3
  2.1582 +          apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff)
  2.1583 +          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
  2.1584 +      qed qed qed note dec1 = conjunctD2[OF this]
  2.1585 +
  2.1586 +  have "\<And>m. (\<lambda>x. Sup {f j x |j. m \<le> j}) integrable_on s \<and>
  2.1587 +    ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) --->
  2.1588 +    integral s (\<lambda>x. Sup {f j x |j. m \<le> j})) sequentially"
  2.1589 +  proof(rule monotone_convergence_increasing_real,safe) fix m::nat
  2.1590 +    show "bounded {integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) |k. True}"
  2.1591 +      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  2.1592 +    proof safe fix k::nat
  2.1593 +      show "norm (integral s (\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}})) \<le> integral s h"
  2.1594 +        apply(rule integral_norm_bound_integral) unfolding simple_image
  2.1595 +        apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real)
  2.1596 +        prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le)
  2.1597 +        prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real)
  2.1598 +        using assms unfolding real_norm_def by auto
  2.1599 +    qed fix k::nat show "(\<lambda>x. Sup {f j x |j. j \<in> {m..m + k}}) integrable_on s"
  2.1600 +      unfolding simple_image apply(rule absolutely_integrable_onD)
  2.1601 +      apply(rule absolutely_integrable_sup_real) prefer 3 
  2.1602 +      using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto
  2.1603 +    fix x assume x:"x\<in>s" show "Sup {f j x |j. j \<in> {m..m + Suc k}}
  2.1604 +      \<ge> Sup {f j x |j. j \<in> {m..m + k}}" apply(rule Sup_le) unfolding setle_def
  2.1605 +      defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto
  2.1606 +    let ?S = "{f j x| j.  m \<le> j}" def i \<equiv> "Sup ?S"
  2.1607 +    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
  2.1608 +      unfolding Lim_sequentially
  2.1609 +    proof safe case goal1 note e=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup)
  2.1610 +        defer apply(rule_tac x="h x" in exI) unfolding setle_def
  2.1611 +      proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto
  2.1612 +      qed auto
  2.1613 +      
  2.1614 +      have "\<exists>y\<in>?S. \<not> y \<le> i - e"
  2.1615 +      proof(rule ccontr) case goal1 hence "i \<le> i - e" apply-
  2.1616 +          apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastsimp+
  2.1617 +        thus False using e by auto
  2.1618 +      qed then guess y .. note y=this[unfolded not_le]
  2.1619 +      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
  2.1620 +      
  2.1621 +      show ?case apply(rule_tac x=N in exI)
  2.1622 +      proof safe case goal1
  2.1623 +        have *:"\<And>y ix. i - e < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < e" by arith
  2.1624 +        show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)])
  2.1625 +          unfolding i_def apply(rule real_ge_sup_subset) prefer 3
  2.1626 +          apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff)
  2.1627 +          prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto
  2.1628 +      qed qed qed note inc1 = conjunctD2[OF this]
  2.1629 +
  2.1630 +  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) ---> integral s g) sequentially"
  2.1631 +  apply(rule monotone_convergence_increasing_real,safe) apply fact 
  2.1632 +  proof- show "bounded {integral s (\<lambda>x. Inf {f j x |j. k \<le> j}) |k. True}"
  2.1633 +      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  2.1634 +    proof safe fix k::nat
  2.1635 +      show "norm (integral s (\<lambda>x. Inf {f j x |j. k \<le> j})) \<le> integral s h"
  2.1636 +        apply(rule integral_norm_bound_integral) apply fact+
  2.1637 +        unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto
  2.1638 +    qed fix k::nat and x assume x:"x\<in>s"
  2.1639 +
  2.1640 +    have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  2.1641 +    show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}" apply-
  2.1642 +      apply(rule real_le_inf_subset) prefer 3 unfolding setge_def
  2.1643 +      apply(rule_tac x="- h x" in exI) apply safe apply(rule *)
  2.1644 +      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
  2.1645 +    show "((\<lambda>k. Inf {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially
  2.1646 +    proof safe case goal1 hence "0<e/2" by auto
  2.1647 +      from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this
  2.1648 +      show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def
  2.1649 +        apply(rule le_less_trans[of _ "e/2"]) apply(rule Inf_asclose) apply safe
  2.1650 +        defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto
  2.1651 +    qed qed note inc2 = conjunctD2[OF this]
  2.1652 +
  2.1653 +  have "g integrable_on s \<and> ((\<lambda>k. integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) ---> integral s g) sequentially"
  2.1654 +  apply(rule monotone_convergence_decreasing_real,safe) apply fact 
  2.1655 +  proof- show "bounded {integral s (\<lambda>x. Sup {f j x |j. k \<le> j}) |k. True}"
  2.1656 +      unfolding bounded_iff apply(rule_tac x="integral s h" in exI)
  2.1657 +    proof safe fix k::nat
  2.1658 +      show "norm (integral s (\<lambda>x. Sup {f j x |j. k \<le> j})) \<le> integral s h"
  2.1659 +        apply(rule integral_norm_bound_integral) apply fact+
  2.1660 +        unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto
  2.1661 +    qed fix k::nat and x assume x:"x\<in>s"
  2.1662 +
  2.1663 +    show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}" apply-
  2.1664 +      apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def
  2.1665 +      apply(rule_tac x="h x" in exI) apply safe
  2.1666 +      using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
  2.1667 +    show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially" unfolding Lim_sequentially
  2.1668 +    proof safe case goal1 hence "0<e/2" by auto
  2.1669 +      from assms(4)[unfolded Lim_sequentially,rule_format,OF x this] guess N .. note N=this
  2.1670 +      show ?case apply(rule_tac x=N in exI,safe) unfolding dist_real_def
  2.1671 +        apply(rule le_less_trans[of _ "e/2"]) apply(rule Sup_asclose) apply safe
  2.1672 +        defer apply(rule less_imp_le) using N goal1 unfolding dist_real_def by auto
  2.1673 +    qed qed note dec2 = conjunctD2[OF this]
  2.1674 +
  2.1675 +  show "g integrable_on s" by fact
  2.1676 +  show "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially" unfolding Lim_sequentially
  2.1677 +  proof safe case goal1
  2.1678 +    from inc2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N1 .. note N1=this[unfolded dist_real_def]
  2.1679 +    from dec2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N2 .. note N2=this[unfolded dist_real_def]
  2.1680 +    show ?case apply(rule_tac x="N1+N2" in exI,safe)
  2.1681 +    proof- fix n assume n:"n \<ge> N1 + N2"
  2.1682 +      have *:"\<And>i0 i i1 g. \<bar>i0 - g\<bar> < e \<longrightarrow> \<bar>i1 - g\<bar> < e \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < e" by arith
  2.1683 +      show "dist (integral s (f n)) (integral s g) < e" unfolding dist_real_def
  2.1684 +        apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
  2.1685 +      proof- show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
  2.1686 +        proof(rule integral_le[OF dec1(1) assms(1)],safe) 
  2.1687 +          fix x assume x:"x \<in> s" have *:"\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  2.1688 +          show "Inf {f j x |j. n \<le> j} \<le> f n x" apply(rule Inf_lower[where z="- h x"]) defer
  2.1689 +            apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
  2.1690 +        qed show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
  2.1691 +        proof(rule integral_le[OF assms(1) inc1(1)],safe) 
  2.1692 +          fix x assume x:"x \<in> s"
  2.1693 +          show "f n x \<le> Sup {f j x |j. n \<le> j}" apply(rule Sup_upper[where z="h x"]) defer
  2.1694 +            using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto
  2.1695 +        qed qed(insert n,auto) qed qed qed
  2.1696  
  2.1697  declare [[smt_certificates=""]]
  2.1698