# HG changeset patch # User himmelma # Date 1271765272 -7200 # Node ID 027ae62681be53412ab9ea79207b34200ebb30d1 # Parent bae883012af3a4b25b7a5fbddcce476c70c77aee Translated remaining theorems about integration from HOL light. diff -r bae883012af3 -r 027ae62681be src/HOL/Multivariate_Analysis/Integration.cert --- a/src/HOL/Multivariate_Analysis/Integration.cert Fri Apr 09 13:35:54 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.cert Tue Apr 20 14:07:52 2010 +0200 @@ -3210,3 +3210,772 @@ #228 := [unit-resolution #200 #220]: #173 [th-lemma #228 #227 #211]: false unsat +610fb185d846b293ce6bb466b6770a65def3e59c 768 0 +#2 := false +#7 := 0::real +decl uf_2 :: real +#5 := uf_2 +#75 := -1::real +#76 := (* -1::real uf_2) +decl uf_1 :: real +#4 := uf_1 +#77 := (+ uf_1 #76) +#316 := (>= #77 0::real) +#317 := (not #316) +decl uf_8 :: real +#39 := uf_8 +#216 := (* -1::real uf_8) +#220 := (+ uf_1 #216) +#221 := (<= #220 0::real) +#86 := (* -1::real uf_1) +#87 := (+ #86 uf_2) +#323 := (ite #316 #77 #87) +#331 := (* -1::real #323) +decl uf_3 :: real +#11 := uf_3 +#95 := 1/3::real +#96 := (* 1/3::real uf_3) +#332 := (+ #96 #331) +#333 := (<= #332 0::real) +#334 := (not #333) +decl uf_4 :: real +#15 := uf_4 +#111 := (* -1::real uf_4) +#112 := (+ uf_2 #111) +#102 := (+ #76 uf_4) +#293 := (<= #112 0::real) +#300 := (ite #293 #102 #112) +#308 := (* -1::real #300) +#309 := (+ #96 #308) +#310 := (<= #309 0::real) +#311 := (not #310) +decl uf_6 :: real +#22 := uf_6 +decl uf_5 :: real +#21 := uf_5 +#133 := (* -1::real uf_5) +#134 := (+ #133 uf_6) +#123 := (* -1::real uf_6) +#124 := (+ uf_5 #123) +#270 := (>= #124 0::real) +#277 := (ite #270 #124 #134) +#285 := (* -1::real #277) +#286 := (+ #96 #285) +#287 := (<= #286 0::real) +#288 := (not #287) +decl uf_7 :: real +#28 := uf_7 +#154 := (* -1::real uf_7) +#155 := (+ uf_6 #154) +#145 := (+ #123 uf_7) +#247 := (<= #155 0::real) +#254 := (ite #247 #145 #155) +#262 := (* -1::real #254) +#263 := (+ #96 #262) +#264 := (<= #263 0::real) +#265 := (not #264) +#175 := (+ #76 uf_6) +#166 := (+ uf_2 #123) +#224 := (>= #166 0::real) +#231 := (ite #224 #166 #175) +#239 := (* -1::real #231) +#240 := (+ #96 #239) +#241 := (<= #240 0::real) +#242 := (not #241) +#217 := (+ uf_5 #216) +#215 := (>= #217 0::real) +decl uf_9 :: real +#42 := uf_9 +#206 := (* -1::real uf_9) +#212 := (+ uf_7 #206) +#211 := (>= #212 0::real) +#207 := (+ uf_4 #206) +#208 := (<= #207 0::real) +#363 := (and #208 #211 #215 #221 #242 #265 #288 #311 #334) +#44 := (<= uf_9 uf_7) +#43 := (<= uf_4 uf_9) +#45 := (and #43 #44) +#41 := (<= uf_8 uf_5) +#46 := (and #41 #45) +#40 := (<= uf_1 uf_8) +#47 := (and #40 #46) +#12 := 3::real +#13 := (/ uf_3 3::real) +#34 := (- uf_2 uf_6) +#36 := (- #34) +#35 := (< #34 0::real) +#37 := (ite #35 #36 #34) +#38 := (< #37 #13) +#48 := (and #38 #47) +#29 := (- uf_7 uf_6) +#31 := (- #29) +#30 := (< #29 0::real) +#32 := (ite #30 #31 #29) +#33 := (< #32 #13) +#49 := (and #33 #48) +#23 := (- uf_5 uf_6) +#25 := (- #23) +#24 := (< #23 0::real) +#26 := (ite #24 #25 #23) +#27 := (< #26 #13) +#50 := (and #27 #49) +#16 := (- uf_4 uf_2) +#18 := (- #16) +#17 := (< #16 0::real) +#19 := (ite #17 #18 #16) +#20 := (< #19 #13) +#51 := (and #20 #50) +#6 := (- uf_1 uf_2) +#9 := (- #6) +#8 := (< #6 0::real) +#10 := (ite #8 #9 #6) +#14 := (< #10 #13) +#52 := (and #14 #51) +#368 := (iff #52 #363) +#169 := (< #166 0::real) +#180 := (ite #169 #175 #166) +#183 := (< #180 #96) +#189 := (and #47 #183) +#148 := (< #145 0::real) +#160 := (ite #148 #155 #145) +#163 := (< #160 #96) +#194 := (and #163 #189) +#127 := (< #124 0::real) +#139 := (ite #127 #134 #124) +#142 := (< #139 #96) +#197 := (and #142 #194) +#105 := (< #102 0::real) +#117 := (ite #105 #112 #102) +#120 := (< #117 #96) +#200 := (and #120 #197) +#80 := (< #77 0::real) +#92 := (ite #80 #87 #77) +#99 := (< #92 #96) +#203 := (and #99 #200) +#366 := (iff #203 #363) +#339 := (and #208 #211) +#342 := (and #215 #339) +#345 := (and #221 #342) +#348 := (and #345 #242) +#351 := (and #265 #348) +#354 := (and #288 #351) +#357 := (and #311 #354) +#360 := (and #334 #357) +#364 := (iff #360 #363) +#365 := [rewrite]: #364 +#361 := (iff #203 #360) +#358 := (iff #200 #357) +#355 := (iff #197 #354) +#352 := (iff #194 #351) +#349 := (iff #189 #348) +#245 := (iff #183 #242) +#236 := (< #231 #96) +#243 := (iff #236 #242) +#244 := [rewrite]: #243 +#237 := (iff #183 #236) +#234 := (= #180 #231) +#225 := (not #224) +#228 := (ite #225 #175 #166) +#232 := (= #228 #231) +#233 := [rewrite]: #232 +#229 := (= #180 #228) +#226 := (iff #169 #225) +#227 := [rewrite]: #226 +#230 := [monotonicity #227]: #229 +#235 := [trans #230 #233]: #234 +#238 := [monotonicity #235]: #237 +#246 := [trans #238 #244]: #245 +#346 := (iff #47 #345) +#343 := (iff #46 #342) +#340 := (iff #45 #339) +#213 := (iff #44 #211) +#214 := [rewrite]: #213 +#209 := (iff #43 #208) +#210 := [rewrite]: #209 +#341 := [monotonicity #210 #214]: #340 +#218 := (iff #41 #215) +#219 := [rewrite]: #218 +#344 := [monotonicity #219 #341]: #343 +#222 := (iff #40 #221) +#223 := [rewrite]: #222 +#347 := [monotonicity #223 #344]: #346 +#350 := [monotonicity #347 #246]: #349 +#268 := (iff #163 #265) +#259 := (< #254 #96) +#266 := (iff #259 #265) +#267 := [rewrite]: #266 +#260 := (iff #163 #259) +#257 := (= #160 #254) +#248 := (not #247) +#251 := (ite #248 #155 #145) +#255 := (= #251 #254) +#256 := [rewrite]: #255 +#252 := (= #160 #251) +#249 := (iff #148 #248) +#250 := [rewrite]: #249 +#253 := [monotonicity #250]: #252 +#258 := [trans #253 #256]: #257 +#261 := [monotonicity #258]: #260 +#269 := [trans #261 #267]: #268 +#353 := [monotonicity #269 #350]: #352 +#291 := (iff #142 #288) +#282 := (< #277 #96) +#289 := (iff #282 #288) +#290 := [rewrite]: #289 +#283 := (iff #142 #282) +#280 := (= #139 #277) +#271 := (not #270) +#274 := (ite #271 #134 #124) +#278 := (= #274 #277) +#279 := [rewrite]: #278 +#275 := (= #139 #274) +#272 := (iff #127 #271) +#273 := [rewrite]: #272 +#276 := [monotonicity #273]: #275 +#281 := [trans #276 #279]: #280 +#284 := [monotonicity #281]: #283 +#292 := [trans #284 #290]: #291 +#356 := [monotonicity #292 #353]: #355 +#314 := (iff #120 #311) +#305 := (< #300 #96) +#312 := (iff #305 #311) +#313 := [rewrite]: #312 +#306 := (iff #120 #305) +#303 := (= #117 #300) +#294 := (not #293) +#297 := (ite #294 #112 #102) +#301 := (= #297 #300) +#302 := [rewrite]: #301 +#298 := (= #117 #297) +#295 := (iff #105 #294) +#296 := [rewrite]: #295 +#299 := [monotonicity #296]: #298 +#304 := [trans #299 #302]: #303 +#307 := [monotonicity #304]: #306 +#315 := [trans #307 #313]: #314 +#359 := [monotonicity #315 #356]: #358 +#337 := (iff #99 #334) +#328 := (< #323 #96) +#335 := (iff #328 #334) +#336 := [rewrite]: #335 +#329 := (iff #99 #328) +#326 := (= #92 #323) +#320 := (ite #317 #87 #77) +#324 := (= #320 #323) +#325 := [rewrite]: #324 +#321 := (= #92 #320) +#318 := (iff #80 #317) +#319 := [rewrite]: #318 +#322 := [monotonicity #319]: #321 +#327 := [trans #322 #325]: #326 +#330 := [monotonicity #327]: #329 +#338 := [trans #330 #336]: #337 +#362 := [monotonicity #338 #359]: #361 +#367 := [trans #362 #365]: #366 +#204 := (iff #52 #203) +#201 := (iff #51 #200) +#198 := (iff #50 #197) +#195 := (iff #49 #194) +#192 := (iff #48 #189) +#186 := (and #183 #47) +#190 := (iff #186 #189) +#191 := [rewrite]: #190 +#187 := (iff #48 #186) +#184 := (iff #38 #183) +#97 := (= #13 #96) +#98 := [rewrite]: #97 +#181 := (= #37 #180) +#167 := (= #34 #166) +#168 := [rewrite]: #167 +#178 := (= #36 #175) +#172 := (- #166) +#176 := (= #172 #175) +#177 := [rewrite]: #176 +#173 := (= #36 #172) +#174 := [monotonicity #168]: #173 +#179 := [trans #174 #177]: #178 +#170 := (iff #35 #169) +#171 := [monotonicity #168]: #170 +#182 := [monotonicity #171 #179 #168]: #181 +#185 := [monotonicity #182 #98]: #184 +#188 := [monotonicity #185]: #187 +#193 := [trans #188 #191]: #192 +#164 := (iff #33 #163) +#161 := (= #32 #160) +#146 := (= #29 #145) +#147 := [rewrite]: #146 +#158 := (= #31 #155) +#151 := (- #145) +#156 := (= #151 #155) +#157 := [rewrite]: #156 +#152 := (= #31 #151) +#153 := [monotonicity #147]: #152 +#159 := [trans #153 #157]: #158 +#149 := (iff #30 #148) +#150 := [monotonicity #147]: #149 +#162 := [monotonicity #150 #159 #147]: #161 +#165 := [monotonicity #162 #98]: #164 +#196 := [monotonicity #165 #193]: #195 +#143 := (iff #27 #142) +#140 := (= #26 #139) +#125 := (= #23 #124) +#126 := [rewrite]: #125 +#137 := (= #25 #134) +#130 := (- #124) +#135 := (= #130 #134) +#136 := [rewrite]: #135 +#131 := (= #25 #130) +#132 := [monotonicity #126]: #131 +#138 := [trans #132 #136]: #137 +#128 := (iff #24 #127) +#129 := [monotonicity #126]: #128 +#141 := [monotonicity #129 #138 #126]: #140 +#144 := [monotonicity #141 #98]: #143 +#199 := [monotonicity #144 #196]: #198 +#121 := (iff #20 #120) +#118 := (= #19 #117) +#103 := (= #16 #102) +#104 := [rewrite]: #103 +#115 := (= #18 #112) +#108 := (- #102) +#113 := (= #108 #112) +#114 := [rewrite]: #113 +#109 := (= #18 #108) +#110 := [monotonicity #104]: #109 +#116 := [trans #110 #114]: #115 +#106 := (iff #17 #105) +#107 := [monotonicity #104]: #106 +#119 := [monotonicity #107 #116 #104]: #118 +#122 := [monotonicity #119 #98]: #121 +#202 := [monotonicity #122 #199]: #201 +#100 := (iff #14 #99) +#93 := (= #10 #92) +#78 := (= #6 #77) +#79 := [rewrite]: #78 +#90 := (= #9 #87) +#83 := (- #77) +#88 := (= #83 #87) +#89 := [rewrite]: #88 +#84 := (= #9 #83) +#85 := [monotonicity #79]: #84 +#91 := [trans #85 #89]: #90 +#81 := (iff #8 #80) +#82 := [monotonicity #79]: #81 +#94 := [monotonicity #82 #91 #79]: #93 +#101 := [monotonicity #94 #98]: #100 +#205 := [monotonicity #101 #202]: #204 +#369 := [trans #205 #367]: #368 +#74 := [asserted]: #52 +#370 := [mp #74 #369]: #363 +#374 := [and-elim #370]: #221 +#373 := [and-elim #370]: #215 +#504 := (+ #96 #134) +#514 := (<= #504 0::real) +#635 := (not #514) +#456 := -1/3::real +#457 := (* -1/3::real uf_3) +#544 := (+ #457 #111) +#545 := (+ uf_2 #544) +#546 := (>= #545 0::real) +#390 := (+ #216 uf_9) +#593 := (+ uf_3 #390) +#603 := (<= #593 0::real) +#381 := (+ uf_8 #206) +#404 := (>= #381 0::real) +#594 := (+ uf_3 #381) +#604 := (<= #594 0::real) +#736 := (not #604) +#477 := (+ #96 #155) +#487 := (<= #477 0::real) +#733 := [hypothesis]: #604 +#564 := (+ #76 #96) +#565 := (+ uf_1 #564) +#577 := (<= #565 0::real) +#767 := (or #577 #736) +#658 := (not #577) +#673 := [hypothesis]: #658 +#478 := (+ #96 #145) +#488 := (<= #478 0::real) +#628 := (not #488) +#446 := (+ #96 #123) +#447 := (+ uf_2 #446) +#461 := (<= #447 0::real) +#618 := (not #461) +#754 := (or #224 #736) +#625 := (not #487) +#718 := [hypothesis]: #225 +#744 := (or #577 #736 #224) +#681 := (or #224 #618) +#458 := (+ #457 #123) +#459 := (+ uf_2 #458) +#460 := (>= #459 0::real) +#462 := (ite #224 #460 #461) +#467 := (not #462) +#468 := (iff #242 #467) +#465 := (iff #241 #462) +#444 := (+ #96 uf_6) +#445 := (+ #76 #444) +#448 := (ite #224 #445 #447) +#453 := (<= #448 0::real) +#463 := (iff #453 #462) +#464 := [rewrite]: #463 +#454 := (iff #241 #453) +#451 := (= #240 #448) +#439 := (ite #224 #175 #166) +#441 := (+ #96 #439) +#449 := (= #441 #448) +#450 := [rewrite]: #449 +#442 := (= #240 #441) +#437 := (= #239 #439) +#440 := [rewrite]: #437 +#443 := [monotonicity #440]: #442 +#452 := [trans #443 #450]: #451 +#455 := [monotonicity #452]: #454 +#466 := [trans #455 #464]: #465 +#469 := [monotonicity #466]: #468 +#375 := [and-elim #370]: #242 +#470 := [mp #375 #469]: #467 +#619 := (or #462 #224 #618) +#620 := [def-axiom]: #619 +#682 := [unit-resolution #620 #470]: #681 +#719 := [unit-resolution #682 #718]: #618 +#737 := (or #487 #461 #736 #577) +#372 := [and-elim #370]: #211 +#734 := [hypothesis]: #625 +#675 := [hypothesis]: #618 +#735 := [th-lemma #675 #374 #734 #372 #733 #673]: false +#738 := [lemma #735]: #737 +#739 := [unit-resolution #738 #673 #733 #719]: #487 +#740 := (or #248 #625) +#489 := (ite #247 #487 #488) +#494 := (not #489) +#495 := (iff #265 #494) +#492 := (iff #264 #489) +#479 := (ite #247 #477 #478) +#484 := (<= #479 0::real) +#490 := (iff #484 #489) +#491 := [rewrite]: #490 +#485 := (iff #264 #484) +#482 := (= #263 #479) +#471 := (ite #247 #155 #145) +#474 := (+ #96 #471) +#480 := (= #474 #479) +#481 := [rewrite]: #480 +#475 := (= #263 #474) +#472 := (= #262 #471) +#473 := [rewrite]: #472 +#476 := [monotonicity #473]: #475 +#483 := [trans #476 #481]: #482 +#486 := [monotonicity #483]: #485 +#493 := [trans #486 #491]: #492 +#496 := [monotonicity #493]: #495 +#376 := [and-elim #370]: #265 +#497 := [mp #376 #496]: #494 +#626 := (or #489 #248 #625) +#627 := [def-axiom]: #626 +#741 := [unit-resolution #627 #497]: #740 +#742 := [unit-resolution #741 #739]: #248 +#743 := [th-lemma #673 #719 #372 #733 #742 #718 #374]: false +#745 := [lemma #743]: #744 +#746 := [unit-resolution #745 #718 #733]: #577 +#727 := (or #316 #658) +#574 := (+ #76 #457) +#575 := (+ uf_1 #574) +#576 := (>= #575 0::real) +#578 := (ite #316 #576 #577) +#583 := (not #578) +#584 := (iff #334 #583) +#581 := (iff #333 #578) +#562 := (+ uf_2 #96) +#563 := (+ #86 #562) +#566 := (ite #316 #563 #565) +#571 := (<= #566 0::real) +#579 := (iff #571 #578) +#580 := [rewrite]: #579 +#572 := (iff #333 #571) +#569 := (= #332 #566) +#556 := (ite #316 #87 #77) +#559 := (+ #96 #556) +#567 := (= #559 #566) +#568 := [rewrite]: #567 +#560 := (= #332 #559) +#557 := (= #331 #556) +#558 := [rewrite]: #557 +#561 := [monotonicity #558]: #560 +#570 := [trans #561 #568]: #569 +#573 := [monotonicity #570]: #572 +#582 := [trans #573 #580]: #581 +#585 := [monotonicity #582]: #584 +#379 := [and-elim #370]: #334 +#586 := [mp #379 #585]: #583 +#659 := (or #578 #316 #658) +#660 := [def-axiom]: #659 +#728 := [unit-resolution #660 #586]: #727 +#747 := [unit-resolution #728 #746]: #316 +#748 := (not #211) +#710 := (not #221) +#749 := (or #247 #461 #710 #748 #736 #224 #317) +#750 := [th-lemma]: #749 +#751 := [unit-resolution #750 #718 #374 #719 #372 #747 #733]: #247 +#752 := [unit-resolution #741 #751]: #625 +#753 := [th-lemma #719 #372 #733 #718 #747 #752 #374]: false +#755 := [lemma #753]: #754 +#756 := [unit-resolution #755 #733]: #224 +#615 := (not #460) +#757 := (or #225 #615) +#616 := (or #462 #225 #615) +#617 := [def-axiom]: #616 +#758 := [unit-resolution #617 #470]: #757 +#759 := [unit-resolution #758 #756]: #615 +#760 := (or #618 #460 #225) +#761 := [th-lemma]: #760 +#762 := [unit-resolution #761 #759 #756]: #618 +#763 := [unit-resolution #738 #673 #733 #762]: #487 +#764 := [unit-resolution #741 #763]: #248 +#701 := (or #247 #628) +#629 := (or #489 #247 #628) +#630 := [def-axiom]: #629 +#702 := [unit-resolution #630 #497]: #701 +#765 := [unit-resolution #702 #764]: #628 +#766 := [th-lemma #756 #374 #372 #733 #764 #765 #673]: false +#768 := [lemma #766]: #767 +#769 := [unit-resolution #768 #733]: #577 +#770 := [unit-resolution #728 #769]: #316 +#771 := (or #487 #710 #748 #736 #225 #317 #460) +#772 := [th-lemma]: #771 +#773 := [unit-resolution #772 #756 #374 #759 #372 #770 #733]: #487 +#774 := (or #247 #460 #225 #710 #748 #736 #317) +#775 := [th-lemma]: #774 +#776 := [unit-resolution #775 #756 #374 #759 #372 #770 #733]: #247 +#777 := [unit-resolution #741 #776 #773]: false +#778 := [lemma #777]: #736 +#668 := (or #404 #604) +#605 := (ite #404 #603 #604) +#411 := (ite #404 #381 #390) +#419 := (* -1::real #411) +#420 := (+ uf_3 #419) +#421 := (<= #420 0::real) +#608 := (iff #421 #605) +#595 := (ite #404 #593 #594) +#600 := (<= #595 0::real) +#606 := (iff #600 #605) +#607 := [rewrite]: #606 +#601 := (iff #421 #600) +#598 := (= #420 #595) +#587 := (ite #404 #390 #381) +#590 := (+ uf_3 #587) +#596 := (= #590 #595) +#597 := [rewrite]: #596 +#591 := (= #420 #590) +#588 := (= #419 #587) +#589 := [rewrite]: #588 +#592 := [monotonicity #589]: #591 +#599 := [trans #592 #597]: #598 +#602 := [monotonicity #599]: #601 +#609 := [trans #602 #607]: #608 +#53 := (- uf_8 uf_9) +#55 := (- #53) +#54 := (< #53 0::real) +#56 := (ite #54 #55 #53) +#57 := (< #56 uf_3) +#58 := (not #57) +#434 := (iff #58 #421) +#384 := (< #381 0::real) +#395 := (ite #384 #390 #381) +#398 := (< #395 uf_3) +#401 := (not #398) +#432 := (iff #401 #421) +#422 := (not #421) +#427 := (not #422) +#430 := (iff #427 #421) +#431 := [rewrite]: #430 +#428 := (iff #401 #427) +#425 := (iff #398 #422) +#416 := (< #411 uf_3) +#423 := (iff #416 #422) +#424 := [rewrite]: #423 +#417 := (iff #398 #416) +#414 := (= #395 #411) +#405 := (not #404) +#408 := (ite #405 #390 #381) +#412 := (= #408 #411) +#413 := [rewrite]: #412 +#409 := (= #395 #408) +#406 := (iff #384 #405) +#407 := [rewrite]: #406 +#410 := [monotonicity #407]: #409 +#415 := [trans #410 #413]: #414 +#418 := [monotonicity #415]: #417 +#426 := [trans #418 #424]: #425 +#429 := [monotonicity #426]: #428 +#433 := [trans #429 #431]: #432 +#402 := (iff #58 #401) +#399 := (iff #57 #398) +#396 := (= #56 #395) +#382 := (= #53 #381) +#383 := [rewrite]: #382 +#393 := (= #55 #390) +#387 := (- #381) +#391 := (= #387 #390) +#392 := [rewrite]: #391 +#388 := (= #55 #387) +#389 := [monotonicity #383]: #388 +#394 := [trans #389 #392]: #393 +#385 := (iff #54 #384) +#386 := [monotonicity #383]: #385 +#397 := [monotonicity #386 #394 #383]: #396 +#400 := [monotonicity #397]: #399 +#403 := [monotonicity #400]: #402 +#435 := [trans #403 #433]: #434 +#380 := [asserted]: #58 +#436 := [mp #380 #435]: #421 +#610 := [mp #436 #609]: #605 +#661 := (not #605) +#666 := (or #404 #604 #661) +#667 := [def-axiom]: #666 +#669 := [unit-resolution #667 #610]: #668 +#700 := [unit-resolution #669 #778]: #404 +#664 := (or #405 #603) +#662 := (or #405 #603 #661) +#663 := [def-axiom]: #662 +#665 := [unit-resolution #663 #610]: #664 +#703 := [unit-resolution #665 #700]: #603 +#677 := (not #603) +#731 := (or #677 #546) +#648 := (not #546) +#672 := [hypothesis]: #648 +#671 := [hypothesis]: #603 +#723 := (or #224 #677 #546) +#689 := (or #461 #546 #677 #514) +#687 := [hypothesis]: #635 +#371 := [and-elim #370]: #208 +#688 := [th-lemma #373 #672 #371 #671 #675 #687]: false +#690 := [lemma #688]: #689 +#720 := [unit-resolution #690 #719 #671 #672]: #514 +#692 := (or #271 #635) +#505 := (+ #96 #124) +#515 := (<= #505 0::real) +#516 := (ite #270 #514 #515) +#521 := (not #516) +#522 := (iff #288 #521) +#519 := (iff #287 #516) +#506 := (ite #270 #504 #505) +#511 := (<= #506 0::real) +#517 := (iff #511 #516) +#518 := [rewrite]: #517 +#512 := (iff #287 #511) +#509 := (= #286 #506) +#498 := (ite #270 #134 #124) +#501 := (+ #96 #498) +#507 := (= #501 #506) +#508 := [rewrite]: #507 +#502 := (= #286 #501) +#499 := (= #285 #498) +#500 := [rewrite]: #499 +#503 := [monotonicity #500]: #502 +#510 := [trans #503 #508]: #509 +#513 := [monotonicity #510]: #512 +#520 := [trans #513 #518]: #519 +#523 := [monotonicity #520]: #522 +#377 := [and-elim #370]: #288 +#524 := [mp #377 #523]: #521 +#636 := (or #516 #271 #635) +#637 := [def-axiom]: #636 +#693 := [unit-resolution #637 #524]: #692 +#721 := [unit-resolution #693 #720]: #271 +#722 := [th-lemma #719 #373 #371 #671 #721 #718 #672]: false +#724 := [lemma #722]: #723 +#725 := [unit-resolution #724 #671 #672]: #224 +#716 := (or #225 #317 #546 #677) +#704 := [hypothesis]: #224 +#708 := [hypothesis]: #316 +#709 := (not #215) +#711 := (or #270 #709 #317 #225 #710) +#712 := [th-lemma]: #711 +#713 := [unit-resolution #712 #704 #374 #373 #708]: #270 +#714 := [unit-resolution #693 #713]: #635 +#715 := [th-lemma #708 #672 #371 #671 #714 #373 #704 #374]: false +#717 := [lemma #715]: #716 +#726 := [unit-resolution #717 #725 #672 #671]: #317 +#729 := [unit-resolution #728 #726]: #658 +#698 := (or #316 #546 #677 #577) +#674 := [hypothesis]: #317 +#685 := (or #270 #316 #577 #546 #677) +#670 := [hypothesis]: #271 +#678 := (or #461 #316 #577 #546 #677 #270) +#676 := [th-lemma #675 #674 #673 #672 #371 #671 #670 #373]: false +#679 := [lemma #676]: #678 +#680 := [unit-resolution #679 #670 #673 #672 #671 #674]: #461 +#683 := [unit-resolution #682 #680]: #224 +#684 := [th-lemma #674 #673 #672 #371 #671 #670 #683 #373]: false +#686 := [lemma #684]: #685 +#691 := [unit-resolution #686 #674 #673 #672 #671]: #270 +#694 := [unit-resolution #693 #691]: #635 +#695 := [unit-resolution #690 #694 #671 #672]: #461 +#696 := [unit-resolution #682 #695]: #224 +#697 := [th-lemma #373 #672 #371 #671 #696 #674 #673 #694]: false +#699 := [lemma #697]: #698 +#730 := [unit-resolution #699 #729 #726 #671 #672]: false +#732 := [lemma #730]: #731 +#705 := [unit-resolution #732 #703]: #546 +#706 := (or #293 #648) +#531 := (+ #96 #111) +#532 := (+ uf_2 #531) +#543 := (<= #532 0::real) +#547 := (ite #293 #543 #546) +#552 := (not #547) +#553 := (iff #311 #552) +#550 := (iff #310 #547) +#533 := (+ #96 uf_4) +#534 := (+ #76 #533) +#535 := (ite #293 #532 #534) +#540 := (<= #535 0::real) +#548 := (iff #540 #547) +#549 := [rewrite]: #548 +#541 := (iff #310 #540) +#538 := (= #309 #535) +#525 := (ite #293 #112 #102) +#528 := (+ #96 #525) +#536 := (= #528 #535) +#537 := [rewrite]: #536 +#529 := (= #309 #528) +#526 := (= #308 #525) +#527 := [rewrite]: #526 +#530 := [monotonicity #527]: #529 +#539 := [trans #530 #537]: #538 +#542 := [monotonicity #539]: #541 +#551 := [trans #542 #549]: #550 +#554 := [monotonicity #551]: #553 +#378 := [and-elim #370]: #311 +#555 := [mp #378 #554]: #552 +#649 := (or #547 #293 #648) +#650 := [def-axiom]: #649 +#707 := [unit-resolution #650 #555]: #706 +#779 := [unit-resolution #707 #705]: #293 +#783 := (or #224 #270 #461) +#780 := (not #208) +#781 := (or #294 #709 #224 #780 #677 #270 #461) +#782 := [th-lemma]: #781 +#784 := [unit-resolution #782 #373 #703 #779 #371]: #783 +#785 := [unit-resolution #784 #719 #718]: #270 +#786 := [unit-resolution #693 #785]: #635 +#787 := [th-lemma #718 #719 #786 #373 #371 #703 #779]: false +#788 := [lemma #787]: #224 +#798 := (or #270 #317 #225) +#799 := [unit-resolution #712 #374 #373]: #798 +#800 := [unit-resolution #799 #708 #788]: #270 +#801 := [unit-resolution #693 #800]: #635 +#802 := [th-lemma #708 #779 #371 #703 #788 #801 #373 #374]: false +#803 := [lemma #802]: #317 +#804 := [unit-resolution #728 #803]: #658 +#796 := (or #316 #577) +#789 := (or #514 #294 #225 #709 #780 #677 #577 #316) +#790 := [th-lemma]: #789 +#791 := [unit-resolution #790 #674 #788 #371 #779 #373 #673 #703]: #514 +#792 := (or #270 #577 #316 #294 #225 #709 #780 #677) +#793 := [th-lemma]: #792 +#794 := [unit-resolution #793 #674 #788 #371 #779 #373 #673 #703]: #270 +#795 := [unit-resolution #693 #794 #791]: false +#797 := [lemma #795]: #796 +[unit-resolution #797 #804 #803]: false +unsat diff -r bae883012af3 -r 027ae62681be src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Apr 09 13:35:54 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Apr 20 14:07:52 2010 +0200 @@ -8,9 +8,11 @@ begin declare [[smt_certificates="~~/src/HOL/Multivariate_Analysis/Integration.cert"]] -declare [[smt_fixed=true]] +declare [[smt_fixed=false]] declare [[z3_proofs=true]] +subsection {* Sundries *} + lemma conjunctD2: assumes "a \ b" shows a b using assms by auto lemma conjunctD3: assumes "a \ b \ c" shows a b c using assms by auto lemma conjunctD4: assumes "a \ b \ c \ d" shows a b c d using assms by auto @@ -18,6 +20,81 @@ declare smult_conv_scaleR[simp] +lemma simple_image: "{f x |x . x \ s} = f ` s" by blast + +lemma linear_simps: assumes "bounded_linear f" + 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)" + apply(rule_tac[!] additive.add additive.minus additive.diff additive.zero bounded_linear.scaleR) + using assms unfolding bounded_linear_def additive_def by auto + +lemma bounded_linearI:assumes "\x y. f (x + y) = f x + f y" + "\r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\x. norm (f x) \ norm x * K" + shows "bounded_linear f" + unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto + +lemma real_le_inf_subset: + assumes "t \ {}" "t \ s" "\b. b <=* s" shows "Inf s <= Inf (t::real set)" + apply(rule isGlb_le_isLb) apply(rule Inf[OF assms(1)]) + using assms apply-apply(erule exE) apply(rule_tac x=b in exI) + unfolding isLb_def setge_def by auto + +lemma real_ge_sup_subset: + assumes "t \ {}" "t \ s" "\b. s *<= b" shows "Sup s >= Sup (t::real set)" + apply(rule isLub_le_isUb) apply(rule Sup[OF assms(1)]) + using assms apply-apply(erule exE) apply(rule_tac x=b in exI) + unfolding isUb_def setle_def by auto + +lemma dist_trans[simp]:"dist (vec1 x) (vec1 y) = dist x (y::real)" + unfolding dist_real_def dist_vec1 .. + +lemma Lim_trans[simp]: fixes f::"'a \ real" + shows "((\x. vec1 (f x)) ---> vec1 l) net \ (f ---> l) net" + using assms unfolding Lim dist_trans .. + +lemma bounded_linear_component[intro]: "bounded_linear (\x::real^'n. x $ k)" + apply(rule bounded_linearI[where K=1]) + using component_le_norm[of _ k] unfolding real_norm_def by auto + +lemma bounded_vec1[intro]: "bounded s \ bounded (vec1 ` (s::real set))" + unfolding bounded_def apply safe apply(rule_tac x="vec1 x" in exI,rule_tac x=e in exI) by auto + +lemma transitive_stepwise_lt_eq: + assumes "(\x y z::nat. R x y \ R y z \ R x z)" + shows "((\m. \n>m. R m n) \ (\n. R n (Suc n)))" (is "?l = ?r") +proof(safe) assume ?r fix n m::nat assume "m < n" thus "R m n" apply- + proof(induct n arbitrary: m) case (Suc n) show ?case + proof(cases "m < n") case True + show ?thesis apply(rule assms[OF Suc(1)[OF True]]) using `?r` by auto + next case False hence "m = n" using Suc(2) by auto + thus ?thesis using `?r` by auto + qed qed auto qed auto + +lemma transitive_stepwise_gt: + assumes "\x y z. R x y \ R y z \ R x z" "\n. R n (Suc n) " + shows "\n>m. R m n" +proof- have "\m. \n>m. R m n" apply(subst transitive_stepwise_lt_eq) + apply(rule assms) apply(assumption,assumption) using assms(2) by auto + thus ?thesis by auto qed + +lemma transitive_stepwise_le_eq: + assumes "\x. R x x" "\x y z. R x y \ R y z \ R x z" + shows "(\m. \n\m. R m n) \ (\n. R n (Suc n))" (is "?l = ?r") +proof safe assume ?r fix m n::nat assume "m\n" thus "R m n" apply- + proof(induct n arbitrary: m) case (Suc n) show ?case + proof(cases "m \ n") case True show ?thesis apply(rule assms(2)) + apply(rule Suc(1)[OF True]) using `?r` by auto + next case False hence "m = Suc n" using Suc(2) by auto + thus ?thesis using assms(1) by auto + qed qed(insert assms(1), auto) qed auto + +lemma transitive_stepwise_le: + assumes "\x. R x x" "\x y z. R x y \ R y z \ R x z" "\n. R n (Suc n) " + shows "\n\m. R m n" +proof- have "\m. \n\m. R m n" apply(subst transitive_stepwise_le_eq) + apply(rule assms) apply(rule assms,assumption,assumption) using assms(3) by auto + thus ?thesis by auto qed + + subsection {* Some useful lemmas about intervals. *} lemma empty_as_interval: "{} = {1..0::real^'n}" @@ -1246,6 +1323,10 @@ apply(drule has_integral_linear,assumption,assumption) unfolding has_integral_integral[THEN sym] apply(rule integrable_linear) by assumption+ +lemma integral_component_eq[simp]: fixes f::"real^'n \ real^'m" + assumes "f integrable_on s" shows "integral s (\x. f x $ k) = integral s f $ k" + using integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] . + lemma has_integral_setsum: assumes "finite t" "\a\t. ((f a) has_integral (i a)) s" shows "((\x. setsum (\a. f a x) t) has_integral (setsum i t)) s" @@ -2225,22 +2306,22 @@ shows "dest_vec1(integral s f) \ dest_vec1(integral s g)" apply(rule has_integral_dest_vec1_le) apply(rule_tac[1-2] integrable_integral) using assms by auto -lemma has_integral_component_pos: fixes f::"real^'n \ real^'m" +lemma has_integral_component_nonneg: fixes f::"real^'n \ real^'m" assumes "(f has_integral i) s" "\x\s. 0 \ (f x)$k" shows "0 \ i$k" using has_integral_component_le[OF has_integral_0 assms(1)] using assms(2) by auto -lemma integral_component_pos: fixes f::"real^'n \ real^'m" +lemma integral_component_nonneg: fixes f::"real^'n \ real^'m" assumes "f integrable_on s" "\x\s. 0 \ (f x)$k" shows "0 \ (integral s f)$k" - apply(rule has_integral_component_pos) using assms by auto - -lemma has_integral_dest_vec1_pos: fixes f::"real^'n \ real^1" + apply(rule has_integral_component_nonneg) using assms by auto + +lemma has_integral_dest_vec1_nonneg: fixes f::"real^'n \ real^1" assumes "(f has_integral i) s" "\x\s. 0 \ f x" shows "0 \ i" - using has_integral_component_pos[OF assms(1), of 1] + using has_integral_component_nonneg[OF assms(1), of 1] using assms(2) unfolding vector_le_def by auto -lemma integral_dest_vec1_pos: fixes f::"real^'n \ real^1" +lemma integral_dest_vec1_nonneg: fixes f::"real^'n \ real^1" assumes "f integrable_on s" "\x\s. 0 \ f x" shows "0 \ integral s f" - apply(rule has_integral_dest_vec1_pos) using assms by auto + apply(rule has_integral_dest_vec1_nonneg) using assms by auto lemma has_integral_component_neg: fixes f::"real^'n \ real^'m" assumes "(f has_integral i) s" "\x\s. (f x)$k \ 0" shows "i$k \ 0" @@ -3779,6 +3860,57 @@ thus False by auto qed thus ?l using y unfolding s by auto qed qed +lemma has_integral_trans[simp]: fixes f::"real^'n \ real" shows + "((\x. vec1 (f x)) has_integral vec1 i) s \ (f has_integral i) s" + unfolding has_integral'[unfolded has_integral] +proof case goal1 thus ?case apply safe + apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe) + apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) + apply(rule_tac x="dest_vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) + apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe) + apply(subst(asm)(2) norm_vector_1) unfolding split_def + unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1] + Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption + apply(subst(asm)(2) norm_vector_1) by auto +next case goal2 thus ?case apply safe + apply(erule_tac x=e in allE,safe) apply(rule_tac x=B in exI,safe) + apply(erule_tac x=a in allE, erule_tac x=b in allE,safe) + apply(rule_tac x="vec1 z" in exI,safe) apply(erule_tac x=ea in allE,safe) + apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe) + apply(subst norm_vector_1) unfolding split_def + unfolding setsum_component Cart_nth.diff cond_value_iff[of dest_vec1] + Cart_nth.scaleR vec1_dest_vec1 zero_index apply assumption + apply(subst norm_vector_1) by auto qed + +lemma integral_trans[simp]: assumes "(f::real^'n \ real) integrable_on s" + shows "integral s (\x. vec1 (f x)) = vec1 (integral s f)" + apply(rule integral_unique) using assms by auto + +lemma integrable_on_trans[simp]: fixes f::"real^'n \ real" shows + "(\x. vec1 (f x)) integrable_on s \ (f integrable_on s)" + unfolding integrable_on_def + apply(subst(2) vec1_dest_vec1(1)[THEN sym]) unfolding has_integral_trans + apply safe defer apply(rule_tac x="vec1 y" in exI) by auto + +lemma has_integral_le: fixes f::"real^'n \ real" + assumes "(f has_integral i) s" "(g has_integral j) s" "\x\s. (f x) \ (g x)" + shows "i \ j" using has_integral_component_le[of "vec1 o f" "vec1 i" s "vec1 o g" "vec1 j" 1] + unfolding o_def using assms by auto + +lemma integral_le: fixes f::"real^'n \ real" + assumes "f integrable_on s" "g integrable_on s" "\x\s. f x \ g x" + shows "integral s f \ integral s g" + using has_integral_le[OF assms(1,2)[unfolded has_integral_integral] assms(3)] . + +lemma has_integral_nonneg: fixes f::"real^'n \ real" + assumes "(f has_integral i) s" "\x\s. 0 \ f x" shows "0 \ i" + using has_integral_component_nonneg[of "vec1 o f" "vec1 i" s 1] + unfolding o_def using assms by auto + +lemma integral_nonneg: fixes f::"real^'n \ real" + assumes "f integrable_on s" "\x\s. 0 \ f x" shows "0 \ integral s f" + using has_integral_nonneg[OF assms(1)[unfolded has_integral_integral] assms(2)] . + subsection {* Hence a general restriction property. *} lemma has_integral_restrict[simp]: assumes "s \ t" shows @@ -3875,11 +4007,21 @@ note assms(2-3)[unfolded this] note * = has_integral_component_le[OF this] show ?thesis apply(rule *) using assms(1,4) by auto qed +lemma has_integral_subset_le: fixes f::"real^'n \ real" + assumes "s \ t" "(f has_integral i) s" "(f has_integral j) t" "\x\t. 0 \ f(x)" + shows "i \ j" using has_integral_subset_component_le[OF assms(1), of "vec1 o f" "vec1 i" "vec1 j" 1] + unfolding o_def using assms by auto + lemma integral_subset_component_le: fixes f::"real^'n \ real^'m" assumes "s \ t" "f integrable_on s" "f integrable_on t" "\x \ t. 0 \ f(x)$k" shows "(integral s f)$k \ (integral t f)$k" apply(rule has_integral_subset_component_le) using assms by auto +lemma integral_subset_le: fixes f::"real^'n \ real" + assumes "s \ t" "f integrable_on s" "f integrable_on t" "\x \ t. 0 \ f(x)" + shows "(integral s f) \ (integral t f)" + apply(rule has_integral_subset_le) using assms by auto + lemma has_integral_alt': fixes f::"real^'n \ 'a::banach" shows "(f has_integral i) s \ (\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}) \ (\e>0. \B>0. \a b. ball 0 B \ {a..b} \ norm(integral {a..b} (\x. if x \ s then f x else 0) - i) < e)" (is "?l = ?r") @@ -3909,6 +4051,1478 @@ from integral_unique[OF this(1)] show ?case using z(2) by auto qed qed qed +subsection {* Continuity of the integral (for a 1-dimensional interval). *} + +lemma integrable_alt: fixes f::"real^'n \ 'a::banach" shows + "f integrable_on s \ + (\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}) \ + (\e>0. \B>0. \a b c d. ball 0 B \ {a..b} \ ball 0 B \ {c..d} + \ norm(integral {a..b} (\x. if x \ s then f x else 0) - + integral {c..d} (\x. if x \ s then f x else 0)) < e)" (is "?l = ?r") +proof assume ?l then guess y unfolding integrable_on_def .. note this[unfolded has_integral_alt'[of f]] + note y=conjunctD2[OF this,rule_format] show ?r apply safe apply(rule y) + proof- case goal1 hence "e/2 > 0" by auto from y(2)[OF this] guess B .. note B=conjunctD2[OF this,rule_format] + show ?case apply(rule,rule,rule B) + proof safe case goal1 show ?case apply(rule norm_triangle_half_l) + using B(2)[OF goal1(1)] B(2)[OF goal1(2)] by auto qed qed + +next assume ?r note as = conjunctD2[OF this,rule_format] + have "Cauchy (\n. integral ({(\ i. - real n) .. (\ i. real n)}) (\x. if x \ s then f x else 0))" + proof(unfold Cauchy_def,safe) case goal1 + from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format] + from real_arch_simple[of B] guess N .. note N = this + { fix n assume n:"n \ N" have "ball 0 B \ {\ i. - real n..\ i. real n}" apply safe + unfolding mem_ball mem_interval vector_dist_norm + proof case goal1 thus ?case using component_le_norm[of x i] + using n N by(auto simp add:field_simps) qed } + thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto + qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i .. + note i = this[unfolded Lim_sequentially, rule_format] + + show ?l unfolding integrable_on_def has_integral_alt'[of f] apply(rule_tac x=i in exI) + apply safe apply(rule as(1)[unfolded integrable_on_def]) + proof- case goal1 hence *:"e/2 > 0" by auto + from i[OF this] guess N .. note N =this[rule_format] + from as(2)[OF *] guess B .. note B=conjunctD2[OF this,rule_format] let ?B = "max (real N) B" + show ?case apply(rule_tac x="?B" in exI) + proof safe show "0 < ?B" using B(1) by auto + fix a b assume ab:"ball 0 ?B \ {a..b::real^'n}" + from real_arch_simple[of ?B] guess n .. note n=this + show "norm (integral {a..b} (\x. if x \ s then f x else 0) - i) < e" + apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute) + apply(rule N[unfolded vector_dist_norm, of n]) + proof safe show "N \ n" using n by auto + fix x::"real^'n" assume x:"x \ ball 0 B" hence "x\ ball 0 ?B" by auto + thus "x\{a..b}" using ab by blast + show "x\{\ i. - real n..\ i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply- + proof case goal1 thus ?case using component_le_norm[of x i] + using n by(auto simp add:field_simps) qed qed qed qed qed + +lemma integrable_altD: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" + shows "\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}" + "\e. e>0 \ \B>0. \a b c d. ball 0 B \ {a..b} \ ball 0 B \ {c..d} + \ norm(integral {a..b} (\x. if x \ s then f x else 0) - integral {c..d} (\x. if x \ s then f x else 0)) < e" + using assms[unfolded integrable_alt[of f]] by auto + +lemma integrable_on_subinterval: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" "{a..b} \ s" shows "f integrable_on {a..b}" + apply(rule integrable_eq) defer apply(rule integrable_altD(1)[OF assms(1)]) + using assms(2) by auto + +subsection {* A straddling criterion for integrability. *} + +lemma integrable_straddle_interval: fixes f::"real^'n \ real" + assumes "\e>0. \g h i j. (g has_integral i) ({a..b}) \ (h has_integral j) ({a..b}) \ + norm(i - j) < e \ (\x\{a..b}. (g x) \ (f x) \ (f x) \(h x))" + shows "f integrable_on {a..b}" +proof(subst integrable_cauchy,safe) + case goal1 hence e:"e/3 > 0" by auto note assms[rule_format,OF this] + then guess g h i j apply- by(erule exE conjE)+ note obt = this + from obt(1)[unfolded has_integral[of g], rule_format, OF e] guess d1 .. note d1=conjunctD2[OF this,rule_format] + from obt(2)[unfolded has_integral[of h], rule_format, OF e] guess d2 .. note d2=conjunctD2[OF this,rule_format] + show ?case apply(rule_tac x="\x. d1 x \ d2 x" in exI) apply(rule conjI gauge_inter d1 d2)+ unfolding fine_inter + proof safe have **:"\i j g1 g2 h1 h2 f1 f2. g1 - h2 \ f1 - f2 \ f1 - f2 \ h1 - g2 \ + abs(i - j) < e / 3 \ abs(g2 - i) < e / 3 \ abs(g1 - i) < e / 3 \ + abs(h2 - j) < e / 3 \ abs(h1 - j) < e / 3 \ abs(f1 - f2) < e" using `e>0` by arith + case goal1 note tagged_division_ofD(2-4) note * = this[OF goal1(1)] this[OF goal1(4)] + + have "(\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p1. content k *\<^sub>R g x) \ 0" + "0 \ (\(x, k)\p2. content k *\<^sub>R h x) - (\(x, k)\p2. content k *\<^sub>R f x)" + "(\(x, k)\p2. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R g x) \ 0" + "0 \ (\(x, k)\p1. content k *\<^sub>R h x) - (\(x, k)\p1. content k *\<^sub>R f x)" + unfolding setsum_subtractf[THEN sym] apply- apply(rule_tac[!] setsum_nonneg) + apply safe unfolding real_scaleR_def mult.diff_right[THEN sym] + apply(rule_tac[!] mult_nonneg_nonneg) + proof- fix a b assume ab:"(a,b) \ p1" + show "0 \ content b" using *(3)[OF ab] apply safe using content_pos_le . thus "0 \ content b" . + show "0 \ f a - g a" "0 \ h a - f a" using *(1-2)[OF ab] using obt(4)[rule_format,of a] by auto + next fix a b assume ab:"(a,b) \ p2" + show "0 \ content b" using *(6)[OF ab] apply safe using content_pos_le . thus "0 \ content b" . + show "0 \ f a - g a" "0 \ h a - f a" using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto qed + + thus ?case apply- unfolding real_norm_def apply(rule **) defer defer + unfolding real_norm_def[THEN sym] apply(rule obt(3)) + apply(rule d1(2)[OF conjI[OF goal1(4,5)]]) + apply(rule d1(2)[OF conjI[OF goal1(1,2)]]) + apply(rule d2(2)[OF conjI[OF goal1(4,6)]]) + apply(rule d2(2)[OF conjI[OF goal1(1,3)]]) by auto qed qed + +lemma integrable_straddle: fixes f::"real^'n \ real" + assumes "\e>0. \g h i j. (g has_integral i) s \ (h has_integral j) s \ + norm(i - j) < e \ (\x\s. (g x) \(f x) \(f x) \(h x))" + shows "f integrable_on s" +proof- have "\a b. (\x. if x \ s then f x else 0) integrable_on {a..b}" + proof(rule integrable_straddle_interval,safe) case goal1 hence *:"e/4 > 0" by auto + from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this + note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] + note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] + note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] + note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] + def c \ "\ i. min (a$i) (- (max B1 B2))" and d \ "\ i. max (b$i) (max B1 B2)" + have *:"ball 0 B1 \ {c..d}" "ball 0 B2 \ {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm + proof(rule_tac[!] allI) + case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next + case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed + have **:"\ch cg ag ah::real. norm(ah - ag) \ norm(ch - cg) \ norm(cg - i) < e / 4 \ + norm(ch - j) < e / 4 \ norm(ag - ah) < e" + using obt(3) unfolding real_norm_def by arith + show ?case apply(rule_tac x="\x. if x \ s then g x else 0" in exI) + apply(rule_tac x="\x. if x \ s then h x else 0" in exI) + apply(rule_tac x="integral {a..b} (\x. if x \ s then g x else 0)" in exI) + apply(rule_tac x="integral {a..b} (\x. if x \ s then h x else 0)" in exI) + apply safe apply(rule_tac[1-2] integrable_integral,rule g,rule h) + apply(rule **[OF _ B1(2)[OF *(1)] B2(2)[OF *(2)]]) + proof- have *:"\x f g. (if x \ s then f x else 0) - (if x \ s then g x else 0) = + (if x \ s then f x - g x else (0::real))" by auto + note ** = abs_of_nonneg[OF integral_nonneg[OF integrable_sub, OF h g]] + show " norm (integral {a..b} (\x. if x \ s then h x else 0) - + integral {a..b} (\x. if x \ s then g x else 0)) + \ norm (integral {c..d} (\x. if x \ s then h x else 0) - + integral {c..d} (\x. if x \ s then g x else 0))" + unfolding integral_sub[OF h g,THEN sym] real_norm_def apply(subst **) defer apply(subst **) defer + apply(rule has_integral_subset_le) defer apply(rule integrable_integral integrable_sub h g)+ + proof safe fix x assume "x\{a..b}" thus "x\{c..d}" unfolding mem_interval c_def d_def + apply - apply rule apply(erule_tac x=i in allE) by auto + qed(insert obt(4), auto) qed(insert obt(4), auto) qed note interv = this + + show ?thesis unfolding integrable_alt[of f] apply safe apply(rule interv) + proof- case goal1 hence *:"e/3 > 0" by auto + from assms[rule_format,OF this] guess g h i j apply-by(erule exE conjE)+ note obt=this + note obt(1)[unfolded has_integral_alt'[of g]] note conjunctD2[OF this, rule_format] + note g = this(1) and this(2)[OF *] from this(2) guess B1 .. note B1 = conjunctD2[OF this,rule_format] + note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] + note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] + show ?case apply(rule_tac x="max B1 B2" in exI) apply safe apply(rule min_max.less_supI1,rule B1) + proof- fix a b c d::"real^'n" assume as:"ball 0 (max B1 B2) \ {a..b}" "ball 0 (max B1 B2) \ {c..d}" + have **:"ball 0 B1 \ ball (0::real^'n) (max B1 B2)" "ball 0 B2 \ ball (0::real^'n) (max B1 B2)" by auto + have *:"\ga gc ha hc fa fc::real. abs(ga - i) < e / 3 \ abs(gc - i) < e / 3 \ abs(ha - j) < e / 3 \ + abs(hc - j) < e / 3 \ abs(i - j) < e / 3 \ ga \ fa \ fa \ ha \ gc \ fc \ fc \ hc\ abs(fa - fc) < e" by smt + show "norm (integral {a..b} (\x. if x \ s then f x else 0) - integral {c..d} (\x. if x \ s then f x else 0)) < e" + unfolding real_norm_def apply(rule *, safe) unfolding real_norm_def[THEN sym] + apply(rule B1(2),rule order_trans,rule **,rule as(1)) + apply(rule B1(2),rule order_trans,rule **,rule as(2)) + apply(rule B2(2),rule order_trans,rule **,rule as(1)) + apply(rule B2(2),rule order_trans,rule **,rule as(2)) + apply(rule obt) apply(rule_tac[!] integral_le) using obt + by(auto intro!: h g interv) qed qed qed + +subsection {* Adding integrals over several sets. *} + +lemma has_integral_union: fixes f::"real^'n \ 'a::banach" + assumes "(f has_integral i) s" "(f has_integral j) t" "negligible(s \ t)" + shows "(f has_integral (i + j)) (s \ t)" +proof- note * = has_integral_restrict_univ[THEN sym, of f] + show ?thesis unfolding * apply(rule has_integral_spike[OF assms(3)]) + defer apply(rule has_integral_add[OF assms(1-2)[unfolded *]]) by auto qed + +lemma has_integral_unions: fixes f::"real^'n \ 'a::banach" + assumes "finite t" "\s\t. (f has_integral (i s)) s" "\s\t. \s'\t. ~(s = s') \ negligible(s \ s')" + shows "(f has_integral (setsum i t)) (\t)" +proof- note * = has_integral_restrict_univ[THEN sym, of f] + have **:"negligible (\((\(a,b). a \ b) ` {(a,b). a \ t \ b \ {y. y \ t \ ~(a = y)}}))" + apply(rule negligible_unions) apply(rule finite_imageI) apply(rule finite_subset[of _ "t \ t"]) defer + apply(rule finite_cartesian_product[OF assms(1,1)]) using assms(3) by auto + note assms(2)[unfolded *] note has_integral_setsum[OF assms(1) this] + thus ?thesis unfolding * apply-apply(rule has_integral_spike[OF **]) defer apply assumption + proof safe case goal1 thus ?case + proof(cases "x\\t") case True then guess s unfolding Union_iff .. note s=this + hence *:"\b\t. x \ b \ b = s" using goal1(3) by blast + show ?thesis unfolding if_P[OF True] apply(rule trans) defer + apply(rule setsum_cong2) apply(subst *, assumption) apply(rule refl) + unfolding setsum_delta[OF assms(1)] using s by auto qed auto qed qed + +subsection {* In particular adding integrals over a division, maybe not of an interval. *} + +lemma has_integral_combine_division: fixes f::"real^'n \ 'a::banach" + assumes "d division_of s" "\k\d. (f has_integral (i k)) k" + shows "(f has_integral (setsum i d)) s" +proof- note d = division_ofD[OF assms(1)] + show ?thesis unfolding d(6)[THEN sym] apply(rule has_integral_unions) + apply(rule d assms)+ apply(rule,rule,rule) + proof- case goal1 from d(4)[OF this(1)] d(4)[OF this(2)] + guess a c b d apply-by(erule exE)+ note obt=this + from d(5)[OF goal1] show ?case unfolding obt interior_closed_interval + apply-apply(rule negligible_subset[of "({a..b}-{a<.. ({c..d}-{c<.. 'a::banach" + assumes "d division_of s" "\k\d. f integrable_on k" + shows "integral s f = setsum (\i. integral i f) d" + apply(rule integral_unique) apply(rule has_integral_combine_division[OF assms(1)]) + using assms(2) unfolding has_integral_integral . + +lemma has_integral_combine_division_topdown: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" "d division_of k" "k \ s" + shows "(f has_integral (setsum (\i. integral i f) d)) k" + apply(rule has_integral_combine_division[OF assms(2)]) + apply safe unfolding has_integral_integral[THEN sym] +proof- case goal1 from division_ofD(2,4)[OF assms(2) this] + show ?case apply safe apply(rule integrable_on_subinterval) + apply(rule assms) using assms(3) by auto qed + +lemma integral_combine_division_topdown: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" "d division_of s" + shows "integral s f = setsum (\i. integral i f) d" + apply(rule integral_unique,rule has_integral_combine_division_topdown) using assms by auto + +lemma integrable_combine_division: fixes f::"real^'n \ 'a::banach" + assumes "d division_of s" "\i\d. f integrable_on i" + shows "f integrable_on s" + using assms(2) unfolding integrable_on_def + by(metis has_integral_combine_division[OF assms(1)]) + +lemma integrable_on_subdivision: fixes f::"real^'n \ 'a::banach" + assumes "d division_of i" "f integrable_on s" "i \ s" + shows "f integrable_on i" + apply(rule integrable_combine_division assms)+ +proof safe case goal1 note division_ofD(2,4)[OF assms(1) this] + thus ?case apply safe apply(rule integrable_on_subinterval[OF assms(2)]) + using assms(3) by auto qed + +subsection {* Also tagged divisions. *} + +lemma has_integral_combine_tagged_division: fixes f::"real^'n \ 'a::banach" + assumes "p tagged_division_of s" "\(x,k) \ p. (f has_integral (i k)) k" + shows "(f has_integral (setsum (\(x,k). i k) p)) s" +proof- have *:"(f has_integral (setsum (\k. integral k f) (snd ` p))) s" + apply(rule has_integral_combine_division) apply(rule division_of_tagged_division[OF assms(1)]) + using assms(2) unfolding has_integral_integral[THEN sym] by(safe,auto) + thus ?thesis apply- apply(rule subst[where P="\i. (f has_integral i) s"]) defer apply assumption + apply(rule trans[of _ "setsum (\(x,k). integral k f) p"]) apply(subst eq_commute) + apply(rule setsum_over_tagged_division_lemma[OF assms(1)]) apply(rule integral_null,assumption) + apply(rule setsum_cong2) using assms(2) by auto qed + +lemma integral_combine_tagged_division_bottomup: fixes f::"real^'n \ 'a::banach" + assumes "p tagged_division_of {a..b}" "\(x,k)\p. f integrable_on k" + shows "integral {a..b} f = setsum (\(x,k). integral k f) p" + apply(rule integral_unique) apply(rule has_integral_combine_tagged_division[OF assms(1)]) + using assms(2) by auto + +lemma has_integral_combine_tagged_division_topdown: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" + shows "(f has_integral (setsum (\(x,k). integral k f) p)) {a..b}" + apply(rule has_integral_combine_tagged_division[OF assms(2)]) +proof safe case goal1 note tagged_division_ofD(3-4)[OF assms(2) this] + thus ?case using integrable_subinterval[OF assms(1)] by auto qed + +lemma integral_combine_tagged_division_topdown: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on {a..b}" "p tagged_division_of {a..b}" + shows "integral {a..b} f = setsum (\(x,k). integral k f) p" + apply(rule integral_unique,rule has_integral_combine_tagged_division_topdown) using assms by auto + +subsection {* Henstock's lemma. *} + +lemma henstock_lemma_part1: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on {a..b}" "0 < e" "gauge d" + "(\p. p tagged_division_of {a..b} \ d fine p \ norm (setsum (\(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)" + and p:"p tagged_partial_division_of {a..b}" "d fine p" + shows "norm(setsum (\(x,k). content k *\<^sub>R f x - integral k f) p) \ e" (is "?x \ e") +proof- { presume "\k. 0 ?x \ e + k" thus ?thesis by arith } + fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)] + have "\snd ` p \ {a..b}" using p'(3) by fastsimp + note partial_division_of_tagged_division[OF p(1)] this + from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)] + def r \ "q - snd ` p" have "snd ` p \ r = {}" unfolding r_def by auto + have r:"finite r" using q' unfolding r_def by auto + + have "\i\r. \p. p tagged_division_of i \ d fine p \ + norm(setsum (\(x,j). content j *\<^sub>R f x) p - integral i f) < k / (real (card r) + 1)" + proof safe case goal1 hence i:"i \ q" unfolding r_def by auto + from q'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this + have *:"k / (real (card r) + 1) > 0" apply(rule divide_pos_pos,rule k) by auto + have "f integrable_on {u..v}" apply(rule integrable_subinterval[OF assms(1)]) + using q'(2)[OF i] unfolding uv by auto + note integrable_integral[OF this, unfolded has_integral[of f]] + from this[rule_format,OF *] guess dd .. note dd=conjunctD2[OF this,rule_format] + note gauge_inter[OF `gauge d` dd(1)] from fine_division_exists[OF this,of u v] guess qq . + thus ?case apply(rule_tac x=qq in exI) using dd(2)[of qq] unfolding fine_inter uv by auto qed + from bchoice[OF this] guess qq .. note qq=this[rule_format] + + let ?p = "p \ \qq ` r" have "norm ((\(x, k)\?p. content k *\<^sub>R f x) - integral {a..b} f) < e" + apply(rule assms(4)[rule_format]) + proof show "d fine ?p" apply(rule fine_union,rule p) apply(rule fine_unions) using qq by auto + note * = tagged_partial_division_of_union_self[OF p(1)] + have "p \ \qq ` r tagged_division_of \snd ` p \ \r" + proof(rule tagged_division_union[OF * tagged_division_unions]) + show "finite r" by fact case goal2 thus ?case using qq by auto + next case goal3 thus ?case apply(rule,rule,rule) apply(rule q'(5)) unfolding r_def by auto + next case goal4 thus ?case apply(rule inter_interior_unions_intervals) apply(fact,rule) + apply(rule,rule q') defer apply(rule,subst Int_commute) + apply(rule inter_interior_unions_intervals) apply(rule finite_imageI,rule p',rule) defer + apply(rule,rule q') using q(1) p' unfolding r_def by auto qed + moreover have "\snd ` p \ \r = {a..b}" "{qq i |i. i \ r} = qq ` r" + unfolding Union_Un_distrib[THEN sym] r_def using q by auto + ultimately show "?p tagged_division_of {a..b}" by fastsimp qed + + hence "norm ((\(x, k)\p. content k *\<^sub>R f x) + (\(x, k)\\qq ` r. content k *\<^sub>R f x) - + integral {a..b} f) < e" apply(subst setsum_Un_zero[THEN sym]) apply(rule p') prefer 3 + apply assumption apply rule apply(rule finite_imageI,rule r) apply safe apply(drule qq) + proof- fix x l k assume as:"(x,l)\p" "(x,l)\qq k" "k\r" + note qq[OF this(3)] note tagged_division_ofD(3,4)[OF conjunct1[OF this] as(2)] + from this(2) guess u v apply-by(erule exE)+ note uv=this + have "l\snd ` p" unfolding image_iff apply(rule_tac x="(x,l)" in bexI) using as by auto + hence "l\q" "k\q" "l\k" using as(1,3) q(1) unfolding r_def by auto + note q'(5)[OF this] hence "interior l = {}" using subset_interior[OF `l \ k`] by blast + thus "content l *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto qed auto + + hence "norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x)) + (qq ` r) - integral {a..b} f) < e" apply(subst(asm) setsum_UNION_zero) + prefer 4 apply assumption apply(rule finite_imageI,fact) + unfolding split_paired_all split_conv image_iff defer apply(erule bexE)+ + proof- fix x m k l T1 T2 assume "(x,m)\T1" "(x,m)\T2" "T1\T2" "k\r" "l\r" "T1 = qq k" "T2 = qq l" + note as = this(1-5)[unfolded this(6-)] note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]] + from this(2)[OF as(4,1)] guess u v apply-by(erule exE)+ note uv=this + have *:"interior (k \ l) = {}" unfolding interior_inter apply(rule q') + using as unfolding r_def by auto + have "interior m = {}" unfolding subset_empty[THEN sym] unfolding *[THEN sym] + apply(rule subset_interior) using kl(1)[OF as(4,1)] kl(1)[OF as(5,2)] by auto + thus "content m *\<^sub>R f x = 0" unfolding uv content_eq_0_interior[THEN sym] by auto + qed(insert qq, auto) + + hence **:"norm ((\(x, k)\p. content k *\<^sub>R f x) + setsum (setsum (\(x, k). content k *\<^sub>R f x) \ qq) r - + integral {a..b} f) < e" apply(subst(asm) setsum_reindex_nonzero) apply fact + apply(rule setsum_0',rule) unfolding split_paired_all split_conv defer apply assumption + proof- fix k l x m assume as:"k\r" "l\r" "k\l" "qq k = qq l" "(x,m)\qq k" + note tagged_division_ofD(6)[OF qq[THEN conjunct1]] from this[OF as(1)] this[OF as(2)] + show "content m *\<^sub>R f x = 0" using as(3) unfolding as by auto qed + + have *:"\ir ip i cr cp. norm((cp + cr) - i) < e \ norm(cr - ir) < k \ + ip + ir = i \ norm(cp - ip) \ e + k" + proof- case goal1 thus ?case using norm_triangle_le[of "cp + cr - i" "- (cr - ir)"] + unfolding goal1(3)[THEN sym] norm_minus_cancel by(auto simp add:group_simps) qed + + have "?x = norm ((\(x, k)\p. content k *\<^sub>R f x) - (\(x, k)\p. integral k f))" + unfolding split_def setsum_subtractf .. + also have "... \ e + k" apply(rule *[OF **, where ir="setsum (\k. integral k f) r"]) + proof- case goal2 have *:"(\(x, k)\p. integral k f) = (\k\snd ` p. integral k f)" + apply(subst setsum_reindex_nonzero) apply fact + unfolding split_paired_all snd_conv split_def o_def + proof- fix x l y m assume as:"(x,l)\p" "(y,m)\p" "(x,l)\(y,m)" "l = m" + from p'(4)[OF as(1)] guess u v apply-by(erule exE)+ note uv=this + show "integral l f = 0" unfolding uv apply(rule integral_unique) + apply(rule has_integral_null) unfolding content_eq_0_interior + using p'(5)[OF as(1-3)] unfolding uv as(4)[THEN sym] by auto + qed auto + show ?case unfolding integral_combine_division_topdown[OF assms(1) q(2)] * r_def + apply(rule setsum_Un_disjoint'[THEN sym]) using q(1) q'(1) p'(1) by auto + next case goal1 have *:"k * real (card r) / (1 + real (card r)) < k" using k by(auto simp add:field_simps) + show ?case apply(rule le_less_trans[of _ "setsum (\x. k / (real (card r) + 1)) r"]) + unfolding setsum_subtractf[THEN sym] apply(rule setsum_norm_le,fact) + apply rule apply(drule qq) defer unfolding real_divide_def setsum_left_distrib[THEN sym] + unfolding real_divide_def[THEN sym] using * by(auto simp add:field_simps real_eq_of_nat) + qed finally show "?x \ e + k" . qed + +lemma henstock_lemma_part2: fixes f::"real^'m \ real^'n" + assumes "f integrable_on {a..b}" "0 < e" "gauge d" + "\p. p tagged_division_of {a..b} \ d fine p \ norm (setsum (\(x,k). content k *\<^sub>R f x) p - + integral({a..b}) f) < e" "p tagged_partial_division_of {a..b}" "d fine p" + shows "setsum (\(x,k). norm(content k *\<^sub>R f x - integral k f)) p \ 2 * real (CARD('n)) * e" + unfolding split_def apply(rule vsum_norm_allsubsets_bound) defer + apply(rule henstock_lemma_part1[unfolded split_def,OF assms(1-3)]) + apply safe apply(rule assms[rule_format,unfolded split_def]) defer + apply(rule tagged_partial_division_subset,rule assms,assumption) + apply(rule fine_subset,assumption,rule assms) using assms(5) by auto + +lemma henstock_lemma: fixes f::"real^'m \ real^'n" + assumes "f integrable_on {a..b}" "e>0" + obtains d where "gauge d" + "\p. p tagged_partial_division_of {a..b} \ d fine p + \ setsum (\(x,k). norm(content k *\<^sub>R f x - integral k f)) p < e" +proof- have *:"e / (2 * (real CARD('n) + 1)) > 0" apply(rule divide_pos_pos) using assms(2) by auto + from integrable_integral[OF assms(1),unfolded has_integral[of f],rule_format,OF this] + guess d .. note d = conjunctD2[OF this] show thesis apply(rule that,rule d) + proof safe case goal1 note * = henstock_lemma_part2[OF assms(1) * d this] + show ?case apply(rule le_less_trans[OF *]) using `e>0` by(auto simp add:field_simps) qed qed + +subsection {* monotone convergence (bounded interval first). *} + +lemma monotone_convergence_interval: fixes f::"nat \ real^'n \ real^1" + assumes "\k. (f k) integrable_on {a..b}" + "\k. \x\{a..b}. dest_vec1(f k x) \ dest_vec1(f (Suc k) x)" + "\x\{a..b}. ((\k. f k x) ---> g x) sequentially" + "bounded {integral {a..b} (f k) | k . k \ UNIV}" + shows "g integrable_on {a..b} \ ((\k. integral ({a..b}) (f k)) ---> integral ({a..b}) g) sequentially" +proof(case_tac[!] "content {a..b} = 0") assume as:"content {a..b} = 0" + show ?thesis using integrable_on_null[OF as] unfolding integral_null[OF as] using Lim_const by auto +next assume ab:"content {a..b} \ 0" + have fg:"\x\{a..b}. \ k. (f k x)$1 \ (g x)$1" + proof safe case goal1 note assms(3)[rule_format,OF this] + note * = Lim_component_ge[OF this trivial_limit_sequentially] + show ?case apply(rule *) unfolding eventually_sequentially + apply(rule_tac x=k in exI) apply- apply(rule transitive_stepwise_le) + using assms(2)[rule_format,OF goal1] by auto qed + have "\i. ((\k. integral ({a..b}) (f k)) ---> i) sequentially" + apply(rule bounded_increasing_convergent) defer + apply rule apply(rule integral_component_le) apply safe + apply(rule assms(1-2)[rule_format])+ using assms(4) by auto + then guess i .. note i=this + have i':"\k. dest_vec1(integral({a..b}) (f k)) \ dest_vec1 i" + apply(rule Lim_component_ge,rule i) apply(rule trivial_limit_sequentially) + unfolding eventually_sequentially apply(rule_tac x=k in exI) + apply(rule transitive_stepwise_le) prefer 3 apply(rule integral_dest_vec1_le) + apply(rule assms(1-2)[rule_format])+ using assms(2) by auto + + have "(g has_integral i) {a..b}" unfolding has_integral + proof safe case goal1 note e=this + hence "\k. (\d. gauge d \ (\p. p tagged_division_of {a..b} \ d fine p \ + norm ((\(x, ka)\p. content ka *\<^sub>R f k x) - integral {a..b} (f k)) < e / 2 ^ (k + 2)))" + apply-apply(rule,rule assms(1)[unfolded has_integral_integral has_integral,rule_format]) + apply(rule divide_pos_pos) by auto + from choice[OF this] guess c .. note c=conjunctD2[OF this[rule_format],rule_format] + + have "\r. \k\r. 0 \ i$1 - dest_vec1(integral {a..b} (f k)) \ + i$1 - dest_vec1(integral {a..b} (f k)) < e / 4" + proof- case goal1 have "e/4 > 0" using e by auto + from i[unfolded Lim_sequentially,rule_format,OF this] guess r .. + thus ?case apply(rule_tac x=r in exI) apply rule + apply(erule_tac x=k in allE) + proof- case goal1 thus ?case using i'[of k] unfolding dist_real by auto qed qed + then guess r .. note r=conjunctD2[OF this[rule_format]] + + have "\x\{a..b}. \n\r. \k\n. 0 \ (g x)$1 - (f k x)$1 \ + (g x)$1 - (f k x)$1 < e / (4 * content({a..b}))" + proof case goal1 have "e / (4 * content {a..b}) > 0" apply(rule divide_pos_pos,fact) + using ab content_pos_le[of a b] by auto + from assms(3)[rule_format,OF goal1,unfolded Lim_sequentially,rule_format,OF this] + guess n .. note n=this + thus ?case apply(rule_tac x="n + r" in exI) apply safe apply(erule_tac[2-3] x=k in allE) + unfolding dist_real using fg[rule_format,OF goal1] by(auto simp add:field_simps) qed + from bchoice[OF this] guess m .. note m=conjunctD2[OF this[rule_format],rule_format] + def d \ "\x. c (m x) x" + + show ?case apply(rule_tac x=d in exI) + proof safe show "gauge d" using c(1) unfolding gauge_def d_def by auto + next fix p assume p:"p tagged_division_of {a..b}" "d fine p" + note p'=tagged_division_ofD[OF p(1)] + have "\a. \x\p. m (fst x) \ a" by(rule upper_bound_finite_set,fact) + then guess s .. note s=this + have *:"\a b c d. norm(a - b) \ e / 4 \ norm(b - c) < e / 2 \ + norm(c - d) < e / 4 \ norm(a - d) < e" + proof safe case goal1 thus ?case using norm_triangle_lt[of "a - b" "b - c" "3* e/4"] + norm_triangle_lt[of "a - b + (b - c)" "c - d" e] unfolding norm_minus_cancel + by(auto simp add:group_simps) qed + show "norm ((\(x, k)\p. content k *\<^sub>R g x) - i) < e" apply(rule *[rule_format,where + b="\(x, k)\p. content k *\<^sub>R f (m x) x" and c="\(x, k)\p. integral k (f (m x))"]) + proof safe case goal1 + show ?case apply(rule order_trans[of _ "\(x, k)\p. content k * (e / (4 * content {a..b}))"]) + unfolding setsum_subtractf[THEN sym] apply(rule order_trans,rule setsum_norm[OF p'(1)]) + apply(rule setsum_mono) unfolding split_paired_all split_conv + unfolding split_def setsum_left_distrib[THEN sym] scaleR.diff_right[THEN sym] + unfolding additive_content_tagged_division[OF p(1), unfolded split_def] + proof- fix x k assume xk:"(x,k) \ p" hence x:"x\{a..b}" using p'(2-3)[OF xk] by auto + from p'(4)[OF xk] guess u v apply-by(erule exE)+ note uv=this + show " norm (content k *\<^sub>R (g x - f (m x) x)) \ content k * (e / (4 * content {a..b}))" + unfolding norm_scaleR uv unfolding abs_of_nonneg[OF content_pos_le] + apply(rule mult_left_mono) unfolding norm_real using m(2)[OF x,of "m x"] by auto + qed(insert ab,auto) + + next case goal2 show ?case apply(rule le_less_trans[of _ "norm (\j = 0..s. + \(x, k)\{xk\p. m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x)))"]) + apply(subst setsum_group) apply fact apply(rule finite_atLeastAtMost) defer + apply(subst split_def)+ unfolding setsum_subtractf apply rule + proof- show "norm (\j = 0..s. \(x, k)\{xk \ p. + m (fst xk) = j}. content k *\<^sub>R f (m x) x - integral k (f (m x))) < e / 2" + apply(rule le_less_trans[of _ "setsum (\i. e / 2^(i+2)) {0..s}"]) + apply(rule setsum_norm_le[OF finite_atLeastAtMost]) + proof show "(\i = 0..s. e / 2 ^ (i + 2)) < e / 2" + unfolding power_add real_divide_def inverse_mult_distrib + unfolding setsum_right_distrib[THEN sym] setsum_left_distrib[THEN sym] + unfolding power_inverse sum_gp apply(rule mult_strict_left_mono[OF _ e]) + unfolding power2_eq_square by auto + fix t assume "t\{0..s}" + show "norm (\(x, k)\{xk \ p. m (fst xk) = t}. content k *\<^sub>R f (m x) x - + integral k (f (m x))) \ e / 2 ^ (t + 2)"apply(rule order_trans[of _ + "norm(setsum (\(x,k). content k *\<^sub>R f t x - integral k (f t)) {xk \ p. m (fst xk) = t})"]) + apply(rule eq_refl) apply(rule arg_cong[where f=norm]) apply(rule setsum_cong2) defer + apply(rule henstock_lemma_part1) apply(rule assms(1)[rule_format]) + apply(rule divide_pos_pos,rule e) defer apply safe apply(rule c)+ + apply rule apply assumption+ apply(rule tagged_partial_division_subset[of p]) + apply(rule p(1)[unfolded tagged_division_of_def,THEN conjunct1]) defer + unfolding fine_def apply safe apply(drule p(2)[unfolded fine_def,rule_format]) + unfolding d_def by auto qed + qed(insert s, auto) + + next case goal3 + note comb = integral_combine_tagged_division_topdown[OF assms(1)[rule_format] p(1)] + have *:"\sr sx ss ks kr::real^1. kr = sr \ ks = ss \ ks \ i \ sr \ sx \ sx \ ss \ 0 \ i$1 - kr$1 + \ i$1 - kr$1 < e/4 \ abs(sx$1 - i$1) < e/4" unfolding Cart_eq forall_1 vector_le_def by arith + show ?case unfolding norm_real Cart_nth.diff apply(rule *[rule_format],safe) + apply(rule comb[of r],rule comb[of s]) unfolding vector_le_def forall_1 setsum_component + apply(rule i') apply(rule_tac[1-2] setsum_mono) unfolding split_paired_all split_conv + apply(rule_tac[1-2] integral_component_le[OF ]) + proof safe show "0 \ i$1 - (integral {a..b} (f r))$1" using r(1) by auto + show "i$1 - (integral {a..b} (f r))$1 < e / 4" using r(2) by auto + fix x k assume xk:"(x,k)\p" from p'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this + show "f r integrable_on k" "f s integrable_on k" "f (m x) integrable_on k" "f (m x) integrable_on k" + unfolding uv apply(rule_tac[!] integrable_on_subinterval[OF assms(1)[rule_format]]) + using p'(3)[OF xk] unfolding uv by auto + fix y assume "y\k" hence "y\{a..b}" using p'(3)[OF xk] by auto + hence *:"\m. \n\m. (f m y)$1 \ (f n y)$1" apply-apply(rule transitive_stepwise_le) using assms(2) by auto + show "(f r y)$1 \ (f (m x) y)$1" "(f (m x) y)$1 \ (f s y)$1" + apply(rule_tac[!] *[rule_format]) using s[rule_format,OF xk] m(1)[of x] p'(2-3)[OF xk] by auto + qed qed qed qed note * = this + + have "integral {a..b} g = i" apply(rule integral_unique) using * . + thus ?thesis using i * by auto qed + +lemma monotone_convergence_increasing: fixes f::"nat \ real^'n \ real^1" + assumes "\k. (f k) integrable_on s" "\k. \x\s. (f k x)$1 \ (f (Suc k) x)$1" + "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" +proof- have lem:"\f::nat \ real^'n \ real^1. \ g s. \k.\x\s. 0\dest_vec1 (f k x) \ \k. (f k) integrable_on s \ + \k. \x\s. (f k x)$1 \ (f (Suc k) x)$1 \ \x\s. ((\k. f k x) ---> g x) sequentially \ + bounded {integral s (f k)| k. True} \ g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" + proof- case goal1 note assms=this[rule_format] + have "\x\s. \k. dest_vec1(f k x) \ dest_vec1(g x)" apply safe apply(rule Lim_component_ge) + apply(rule goal1(4)[rule_format],assumption) apply(rule trivial_limit_sequentially) + unfolding eventually_sequentially apply(rule_tac x=k in exI) + apply(rule transitive_stepwise_le) using goal1(3) by auto note fg=this[rule_format] + + have "\i. ((\k. integral s (f k)) ---> i) sequentially" apply(rule bounded_increasing_convergent) + apply(rule goal1(5)) apply(rule,rule integral_component_le) apply(rule goal1(2)[rule_format])+ + using goal1(3) by auto then guess i .. note i=this + have "\k. \x\s. \n\k. f k x \ f n x" apply(rule,rule transitive_stepwise_le) using goal1(3) by auto + hence i':"\k. (integral s (f k))$1 \ i$1" apply-apply(rule,rule Lim_component_ge) + apply(rule i,rule trivial_limit_sequentially) unfolding eventually_sequentially + apply(rule_tac x=k in exI,safe) apply(rule integral_dest_vec1_le) + apply(rule goal1(2)[rule_format])+ by auto + + note int = assms(2)[unfolded integrable_alt[of _ s],THEN conjunct1,rule_format] + have ifif:"\k t. (\x. if x \ t then if x \ s then f k x else 0 else 0) = + (\x. if x \ t\s then f k x else 0)" apply(rule ext) by auto + have int':"\k a b. f k integrable_on {a..b} \ s" apply(subst integrable_restrict_univ[THEN sym]) + apply(subst ifif[THEN sym]) apply(subst integrable_restrict_univ) using int . + have "\a b. (\x. if x \ s then g x else 0) integrable_on {a..b} \ + ((\k. integral {a..b} (\x. if x \ s then f k x else 0)) ---> + integral {a..b} (\x. if x \ s then g x else 0)) sequentially" + proof(rule monotone_convergence_interval,safe) + case goal1 show ?case using int . + next case goal2 thus ?case apply-apply(cases "x\s") using assms(3) by auto + next case goal3 thus ?case apply-apply(cases "x\s") using assms(4) by auto + next case goal4 note * = integral_dest_vec1_nonneg[unfolded vector_le_def forall_1 zero_index] + have "\k. norm (integral {a..b} (\x. if x \ s then f k x else 0)) \ norm (integral s (f k))" + unfolding norm_real apply(subst abs_of_nonneg) apply(rule *[OF int]) + apply(safe,case_tac "x\s") apply(drule assms(1)) prefer 3 + apply(subst abs_of_nonneg) apply(rule *[OF assms(2) goal1(1)[THEN spec]]) + apply(subst integral_restrict_univ[THEN sym,OF int]) + unfolding ifif unfolding integral_restrict_univ[OF int'] + apply(rule integral_subset_component_le[OF _ int' assms(2)]) using assms(1) by auto + thus ?case using assms(5) unfolding bounded_iff apply safe + apply(rule_tac x=aa in exI,safe) apply(erule_tac x="integral s (f k)" in ballE) + apply(rule order_trans) apply assumption by auto qed note g = conjunctD2[OF this] + + have "(g has_integral i) s" unfolding has_integral_alt' apply safe apply(rule g(1)) + proof- case goal1 hence "e/4>0" by auto + from i[unfolded Lim_sequentially,rule_format,OF this] guess N .. note N=this + note assms(2)[of N,unfolded has_integral_integral has_integral_alt'[of "f N"]] + from this[THEN conjunct2,rule_format,OF `e/4>0`] guess B .. note B=conjunctD2[OF this] + show ?case apply(rule,rule,rule B,safe) + proof- fix a b::"real^'n" assume ab:"ball 0 B \ {a..b}" + from `e>0` have "e/2>0" by auto + from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this + have **:"norm (integral {a..b} (\x. if x \ s then f N x else 0) - i) < e/2" + apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N] + unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto + have *:"\f1 f2 g. abs(f1 - i$1) < e / 2 \ abs(f2 - g) < e / 2 \ f1 \ f2 \ f2 \ i$1 + \ abs(g - i$1) < e" by arith + show "norm (integral {a..b} (\x. if x \ s then g x else 0) - i) < e" + unfolding norm_real Cart_simps apply(rule *[rule_format]) + apply(rule **[unfolded norm_real Cart_simps]) + apply(rule M[rule_format,of "M + N",unfolded dist_real]) apply(rule le_add1) + apply(rule integral_component_le[OF int int]) defer + apply(rule order_trans[OF _ i'[rule_format,of "M + N"]]) + proof safe case goal2 have "\m. x\s \ \n\m. (f m x)$1 \ (f n x)$1" + apply(rule transitive_stepwise_le) using assms(3) by auto thus ?case by auto + next case goal1 show ?case apply(subst integral_restrict_univ[THEN sym,OF int]) + unfolding ifif integral_restrict_univ[OF int'] + apply(rule integral_subset_component_le[OF _ int']) using assms by auto + qed qed qed + thus ?case apply safe defer apply(drule integral_unique) using i by auto qed + + have sub:"\k. integral s (\x. f k x - f 0 x) = integral s (f k) - integral s (f 0)" + apply(subst integral_sub) apply(rule assms(1)[rule_format])+ by rule + have "\x m. x\s \ \n\m. dest_vec1 (f m x) \ dest_vec1 (f n x)" apply(rule transitive_stepwise_le) + using assms(2) by auto note * = this[rule_format] + have "(\x. g x - f 0 x) integrable_on s \((\k. integral s (\x. f (Suc k) x - f 0 x)) ---> + integral s (\x. g x - f 0 x)) sequentially" apply(rule lem,safe) + proof- case goal1 thus ?case using *[of x 0 "Suc k"] by auto + next case goal2 thus ?case apply(rule integrable_sub) using assms(1) by auto + next case goal3 thus ?case using *[of x "Suc k" "Suc (Suc k)"] by auto + next case goal4 thus ?case apply-apply(rule Lim_sub) + using seq_offset[OF assms(3)[rule_format],of x 1] by auto + next case goal5 thus ?case using assms(4) unfolding bounded_iff + apply safe apply(rule_tac x="a + norm (integral s (\x. f 0 x))" in exI) + apply safe apply(erule_tac x="integral s (\x. f (Suc k) x)" in ballE) unfolding sub + apply(rule order_trans[OF norm_triangle_ineq4]) by auto qed + note conjunctD2[OF this] note Lim_add[OF this(2) Lim_const[of "integral s (f 0)"]] + integrable_add[OF this(1) assms(1)[rule_format,of 0]] + thus ?thesis unfolding sub apply-apply rule defer apply(subst(asm) integral_sub) + using assms(1) apply auto apply(rule seq_offset_rev[where k=1]) by auto qed + +lemma monotone_convergence_decreasing: fixes f::"nat \ real^'n \ real^1" + assumes "\k. (f k) integrable_on s" "\k. \x\s. (f (Suc k) x)$1 \ (f k x)$1" + "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" +proof- note assm = assms[rule_format] + have *:"{integral s (\x. - f k x) |k. True} = op *\<^sub>R -1 ` {integral s (f k)| k. True}" + apply safe unfolding image_iff apply(rule_tac x="integral s (f k)" in bexI) prefer 3 + apply(rule_tac x=k in exI) unfolding integral_neg[OF assm(1)] by auto + have "(\x. - g x) integrable_on s \ ((\k. integral s (\x. - f k x)) + ---> integral s (\x. - g x)) sequentially" apply(rule monotone_convergence_increasing) + apply(safe,rule integrable_neg) apply(rule assm) defer apply(rule Lim_neg) + apply(rule assm,assumption) unfolding * apply(rule bounded_scaling) using assm by auto + note * = conjunctD2[OF this] + show ?thesis apply rule using integrable_neg[OF *(1)] defer + using Lim_neg[OF *(2)] apply- unfolding integral_neg[OF assm(1)] + unfolding integral_neg[OF *(1),THEN sym] by auto qed + +lemma monotone_convergence_increasing_real: fixes f::"nat \ real^'n \ real" + assumes "\k. (f k) integrable_on s" "\k. \x\s. (f (Suc k) x) \ (f k x)" + "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" +proof- have *:"{integral s (\x. vec1 (f k x)) |k. True} = vec1 ` {integral s (f k) |k. True}" + unfolding integral_trans[OF assms(1)[rule_format]] by auto + have "vec1 \ g integrable_on s \ ((\k. integral s (vec1 \ f k)) ---> integral s (vec1 \ g)) sequentially" + apply(rule monotone_convergence_increasing) unfolding o_def integrable_on_trans + unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto + thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed + +lemma monotone_convergence_decreasing_real: fixes f::"nat \ real^'n \ real" + assumes "\k. (f k) integrable_on s" "\k. \x\s. (f (Suc k) x) \ (f k x)" + "\x\s. ((\k. f k x) ---> g x) sequentially" "bounded {integral s (f k)| k. True}" + shows "g integrable_on s \ ((\k. integral s (f k)) ---> integral s g) sequentially" +proof- have *:"{integral s (\x. vec1 (f k x)) |k. True} = vec1 ` {integral s (f k) |k. True}" + unfolding integral_trans[OF assms(1)[rule_format]] by auto + have "vec1 \ g integrable_on s \ ((\k. integral s (vec1 \ f k)) ---> integral s (vec1 \ g)) sequentially" + apply(rule monotone_convergence_decreasing) unfolding o_def integrable_on_trans + unfolding vec1_dest_vec1 apply(rule assms)+ unfolding Lim_trans unfolding * using assms(3,4) by auto + thus ?thesis unfolding o_def unfolding integral_trans[OF assms(1)[rule_format]] by auto qed + +subsection {* absolute integrability (this is the same as Lebesgue integrability). *} + +definition absolutely_integrable_on (infixr "absolutely'_integrable'_on" 46) where + "f absolutely_integrable_on s \ f integrable_on s \ (\x. (norm(f x))) integrable_on s" + +lemma absolutely_integrable_onI[intro?]: + "f integrable_on s \ (\x. (norm(f x))) integrable_on s \ f absolutely_integrable_on s" + unfolding absolutely_integrable_on_def by auto + +lemma absolutely_integrable_onD[dest]: assumes "f absolutely_integrable_on s" + shows "f integrable_on s" "(\x. (norm(f x))) integrable_on s" + using assms unfolding absolutely_integrable_on_def by auto + +lemma absolutely_integrable_on_trans[simp]: fixes f::"real^'n \ real" shows + "(vec1 o f) absolutely_integrable_on s \ f absolutely_integrable_on s" + unfolding absolutely_integrable_on_def o_def by auto + +lemma integral_norm_bound_integral: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" "g integrable_on s" "\x\s. norm(f x) \ g x" + shows "norm(integral s f) \ (integral s g)" +proof- have *:"\x y. (\e::real. 0 < e \ x < y + e) \ x \ y" apply(safe,rule ccontr) + apply(erule_tac x="x - y" in allE) by auto + have "\e sg dsa dia ig. norm(sg) \ dsa \ abs(dsa - dia) < e / 2 \ norm(sg - ig) < e / 2 + \ norm(ig) < dia + e" + proof safe case goal1 show ?case apply(rule le_less_trans[OF norm_triangle_sub[of ig sg]]) + apply(subst real_sum_of_halves[of e,THEN sym]) unfolding class_semiring.add_a + apply(rule add_le_less_mono) defer apply(subst norm_minus_commute,rule goal1) + apply(rule order_trans[OF goal1(1)]) using goal1(2) by arith + qed note norm=this[rule_format] + have lem:"\f::real^'n \ 'a. \ g a b. f integrable_on {a..b} \ g integrable_on {a..b} \ + \x\{a..b}. norm(f x) \ (g x) \ norm(integral({a..b}) f) \ (integral({a..b}) g)" + proof(rule *[rule_format]) case goal1 hence *:"e/2>0" by auto + from integrable_integral[OF goal1(1),unfolded has_integral[of f],rule_format,OF *] + guess d1 .. note d1 = conjunctD2[OF this,rule_format] + from integrable_integral[OF goal1(2),unfolded has_integral[of g],rule_format,OF *] + guess d2 .. note d2 = conjunctD2[OF this,rule_format] + note gauge_inter[OF d1(1) d2(1)] + from fine_division_exists[OF this, of a b] guess p . note p=this + show ?case apply(rule norm) defer + apply(rule d2(2)[OF conjI[OF p(1)],unfolded real_norm_def]) defer + apply(rule d1(2)[OF conjI[OF p(1)]]) defer apply(rule setsum_norm_le) + proof safe fix x k assume "(x,k)\p" note as = tagged_division_ofD(2-4)[OF p(1) this] + from this(3) guess u v apply-by(erule exE)+ note uv=this + show "norm (content k *\<^sub>R f x) \ content k *\<^sub>R g x" unfolding uv norm_scaleR + unfolding abs_of_nonneg[OF content_pos_le] real_scaleR_def + apply(rule mult_left_mono) using goal1(3) as by auto + qed(insert p[unfolded fine_inter],auto) qed + + { presume "\e. 0 < e \ norm (integral s f) < integral s g + e" + thus ?thesis apply-apply(rule *[rule_format]) by auto } + fix e::real assume "e>0" hence e:"e/2 > 0" by auto + note assms(1)[unfolded integrable_alt[of f]] note f=this[THEN conjunct1,rule_format] + note assms(2)[unfolded integrable_alt[of g]] note g=this[THEN conjunct1,rule_format] + from integrable_integral[OF assms(1),unfolded has_integral'[of f],rule_format,OF e] + guess B1 .. note B1=conjunctD2[OF this[rule_format],rule_format] + from integrable_integral[OF assms(2),unfolded has_integral'[of g],rule_format,OF e] + guess B2 .. note B2=conjunctD2[OF this[rule_format],rule_format] + from bounded_subset_closed_interval[OF bounded_ball, of "0::real^'n" "max B1 B2"] + guess a b apply-by(erule exE)+ note ab=this[unfolded ball_max_Un] + + have "ball 0 B1 \ {a..b}" using ab by auto + from B1(2)[OF this] guess z .. note z=conjunctD2[OF this] + have "ball 0 B2 \ {a..b}" using ab by auto + from B2(2)[OF this] guess w .. note w=conjunctD2[OF this] + + show "norm (integral s f) < integral s g + e" apply(rule norm) + apply(rule lem[OF f g, of a b]) unfolding integral_unique[OF z(1)] integral_unique[OF w(1)] + defer apply(rule w(2)[unfolded real_norm_def],rule z(2)) + apply safe apply(case_tac "x\s") unfolding if_P apply(rule assms(3)[rule_format]) by auto qed + +lemma integral_norm_bound_integral_component: fixes f::"real^'n \ 'a::banach" + assumes "f integrable_on s" "g integrable_on s" "\x\s. norm(f x) \ (g x)$k" + shows "norm(integral s f) \ (integral s g)$k" +proof- have "norm (integral s f) \ integral s ((\x. x $ k) o g)" + apply(rule integral_norm_bound_integral[OF assms(1)]) + apply(rule integrable_linear[OF assms(2)],rule) + unfolding o_def by(rule assms) + thus ?thesis unfolding o_def integral_component_eq[OF assms(2)] . qed + +lemma has_integral_norm_bound_integral_component: fixes f::"real^'n \ 'a::banach" + assumes "(f has_integral i) s" "(g has_integral j) s" "\x\s. norm(f x) \ (g x)$k" + shows "norm(i) \ j$k" using integral_norm_bound_integral_component[of f s g k] + unfolding integral_unique[OF assms(1)] integral_unique[OF assms(2)] + using assms by auto + +lemma absolutely_integrable_le: fixes f::"real^'n \ 'a::banach" + assumes "f absolutely_integrable_on s" + shows "norm(integral s f) \ integral s (\x. norm(f x))" + apply(rule integral_norm_bound_integral) using assms by auto + +lemma absolutely_integrable_0[intro]: "(\x. 0) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def by auto + +lemma absolutely_integrable_cmul[intro]: + "f absolutely_integrable_on s \ (\x. c *\<^sub>R f x) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def using integrable_cmul[of f s c] + using integrable_cmul[of "\x. norm (f x)" s "abs c"] by auto + +lemma absolutely_integrable_neg[intro]: + "f absolutely_integrable_on s \ (\x. -f(x)) absolutely_integrable_on s" + apply(drule absolutely_integrable_cmul[where c="-1"]) by auto + +lemma absolutely_integrable_norm[intro]: + "f absolutely_integrable_on s \ (\x. norm(f x)) absolutely_integrable_on s" + unfolding absolutely_integrable_on_def by auto + +lemma absolutely_integrable_abs[intro]: + "f absolutely_integrable_on s \ (\x. abs(f x::real)) absolutely_integrable_on s" + apply(drule absolutely_integrable_norm) unfolding real_norm_def . + +lemma absolutely_integrable_on_subinterval: fixes f::"real^'n \ 'a::banach" shows + "f absolutely_integrable_on s \ {a..b} \ s \ f absolutely_integrable_on {a..b}" + unfolding absolutely_integrable_on_def by(meson integrable_on_subinterval) + +lemma absolutely_integrable_bounded_variation: fixes f::"real^'n \ 'a::banach" + assumes "f absolutely_integrable_on UNIV" + obtains B where "\d. d division_of (\d) \ setsum (\k. norm(integral k f)) d \ B" + apply(rule that[of "integral UNIV (\x. norm (f x))"]) +proof safe case goal1 note d = division_ofD[OF this(2)] + have "(\k\d. norm (integral k f)) \ (\i\d. integral i (\x. norm (f x)))" + apply(rule setsum_mono,rule absolutely_integrable_le) apply(drule d(4),safe) + apply(rule absolutely_integrable_on_subinterval[OF assms]) by auto + also have "... \ integral (\d) (\x. norm (f x))" + apply(subst integral_combine_division_topdown[OF _ goal1(2)]) + using integrable_on_subdivision[OF goal1(2)] using assms by auto + also have "... \ integral UNIV (\x. norm (f x))" + apply(rule integral_subset_le) + using integrable_on_subdivision[OF goal1(2)] using assms by auto + finally show ?case . qed + +lemma helplemma: + assumes "setsum (\x. norm(f x - g x)) s < e" "finite s" + shows "abs(setsum (\x. norm(f x)) s - setsum (\x. norm(g x)) s) < e" + unfolding setsum_subtractf[THEN sym] apply(rule le_less_trans[OF setsum_abs]) + apply(rule le_less_trans[OF _ assms(1)]) apply(rule setsum_mono) + using norm_triangle_ineq3 . + +lemma bounded_variation_absolutely_integrable_interval: + fixes f::"real^'n \ real^'m" assumes "f integrable_on {a..b}" + "\d. d division_of {a..b} \ setsum (\k. norm(integral k f)) d \ B" + shows "f absolutely_integrable_on {a..b}" +proof- let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of {a..b} }" def i \ "Sup ?S" + have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) + apply(rule elementary_interval) defer apply(rule_tac x=B in exI) + apply(rule setleI) using assms(2) by auto + show ?thesis apply(rule,rule assms) apply rule apply(subst has_integral[of _ i]) + proof safe case goal1 hence "i - e / 2 \ Collect (isUb UNIV (setsum (\k. norm (integral k f)) ` + {d. d division_of {a..b}}))" using isLub_ubs[OF i,rule_format] + unfolding setge_def ubs_def by auto + hence " \y. y division_of {a..b} \ i - e / 2 < (\k\y. norm (integral k f))" + unfolding mem_Collect_eq isUb_def setle_def by simp then guess d .. note d=conjunctD2[OF this] + note d' = division_ofD[OF this(1)] + + have "\x. \e>0. \i\d. x \ i \ ball x e \ i = {}" + proof case goal1 have "\da>0. \xa\\{i \ d. x \ i}. da \ dist x xa" + apply(rule separate_point_closed) apply(rule closed_Union) + apply(rule finite_subset[OF _ d'(1)]) apply safe apply(drule d'(4)) by auto + thus ?case apply safe apply(rule_tac x=da in exI,safe) + apply(erule_tac x=xa in ballE) by auto + qed from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format] + + have "e/2 > 0" using goal1 by auto + from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format] + let ?g = "\x. g x \ ball x (k x)" + show ?case apply(rule_tac x="?g" in exI) apply safe + proof- show "gauge ?g" using g(1) unfolding gauge_def using k(1) by auto + fix p assume "p tagged_division_of {a..b}" "?g fine p" + note p = this(1) conjunctD2[OF this(2)[unfolded fine_inter]] + note p' = tagged_division_ofD[OF p(1)] + def p' \ "{(x,k) | x k. \i l. x \ i \ i \ d \ (x,l) \ p \ k = i \ l}" + have gp':"g fine p'" using p(2) unfolding p'_def fine_def by auto + have p'':"p' tagged_division_of {a..b}" apply(rule tagged_division_ofI) + proof- show "finite p'" apply(rule finite_subset[of _ "(\(k,(x,l)). (x,k \ l)) + ` {(k,xl) | k xl. k \ d \ xl \ p}"]) unfolding p'_def + defer apply(rule finite_imageI,rule finite_product_dependent[OF d'(1) p'(1)]) + apply safe unfolding image_iff apply(rule_tac x="(i,x,l)" in bexI) by auto + fix x k assume "(x,k)\p'" + hence "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" unfolding p'_def by auto + then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] + show "x\k" "k\{a..b}" using p'(2-3)[OF il(3)] il by auto + show "\a b. k = {a..b}" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] + apply safe unfolding inter_interval by auto + next fix x1 k1 assume "(x1,k1)\p'" + hence "\i l. x1 \ i \ i \ d \ (x1, l) \ p \ k1 = i \ l" unfolding p'_def by auto + then guess i1 l1 apply-by(erule exE)+ note il1=conjunctD4[OF this] + fix x2 k2 assume "(x2,k2)\p'" + hence "\i l. x2 \ i \ i \ d \ (x2, l) \ p \ k2 = i \ l" unfolding p'_def by auto + then guess i2 l2 apply-by(erule exE)+ note il2=conjunctD4[OF this] + assume "(x1, k1) \ (x2, k2)" + hence "interior(i1) \ interior(i2) = {} \ interior(l1) \ interior(l2) = {}" + using d'(5)[OF il1(2) il2(2)] p'(5)[OF il1(3) il2(3)] unfolding il1 il2 by auto + thus "interior k1 \ interior k2 = {}" unfolding il1 il2 by auto + next have *:"\(x, X) \ p'. X \ {a..b}" unfolding p'_def using d' by auto + show "\{k. \x. (x, k) \ p'} = {a..b}" apply rule apply(rule Union_least) + unfolding mem_Collect_eq apply(erule exE) apply(drule *[rule_format]) apply safe + proof- fix y assume y:"y\{a..b}" + hence "\x l. (x, l) \ p \ y\l" unfolding p'(6)[THEN sym] by auto + then guess x l apply-by(erule exE)+ note xl=conjunctD2[OF this] + hence "\k. k\d \ y\k" using y unfolding d'(6)[THEN sym] by auto + then guess i .. note i = conjunctD2[OF this] + have "x\i" using fineD[OF p(3) xl(1)] using k(2)[OF i(1), of x] using i(2) xl(2) by auto + thus "y\\{k. \x. (x, k) \ p'}" unfolding p'_def Union_iff apply(rule_tac x="i \ l" in bexI) + defer unfolding mem_Collect_eq apply(rule_tac x=x in exI)+ apply(rule_tac x="i\l" in exI) + apply safe apply(rule_tac x=i in exI) apply(rule_tac x=l in exI) using i xl by auto + qed qed + + hence "(\(x, k)\p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2" + apply-apply(rule g(2)[rule_format]) unfolding tagged_division_of_def apply safe using gp' . + hence **:" \(\(x,k)\p'. norm (content k *\<^sub>R f x)) - (\(x,k)\p'. norm (integral k f))\ < e / 2" + unfolding split_def apply(rule helplemma) using p'' by auto + + have p'alt:"p' = {(x,(i \ l)) | x i l. (x,l) \ p \ i \ d \ ~(i \ l = {})}" + proof safe case goal2 + have "x\i" using fineD[OF p(3) goal2(1)] k(2)[OF goal2(2), of x] goal2(4-) by auto + hence "(x, i \ l) \ p'" unfolding p'_def apply safe + apply(rule_tac x=x in exI,rule_tac x="i\l" in exI) apply safe using goal2 by auto + thus ?case using goal2(3) by auto + next fix x k assume "(x,k)\p'" + hence "\i l. x \ i \ i \ d \ (x, l) \ p \ k = i \ l" unfolding p'_def by auto + then guess i l apply-by(erule exE)+ note il=conjunctD4[OF this] + thus "\y i l. (x, k) = (y, i \ l) \ (y, l) \ p \ i \ d \ i \ l \ {}" + apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) + using p'(2)[OF il(3)] by auto + qed + have sum_p':"(\(x, k)\p'. norm (integral k f)) = (\k\snd ` p'. norm (integral k f))" + apply(subst setsum_over_tagged_division_lemma[OF p'',of "\k. norm (integral k f)"]) + unfolding norm_eq_zero apply(rule integral_null,assumption) .. + note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]] + + have *:"\sni sni' sf sf'. abs(sf' - sni') < e / 2 \ i - e / 2 < sni \ sni' \ i \ + sni \ sni' \ sf' = sf \ abs(sf - i) < e" by arith + show "norm ((\(x, k)\p. content k *\<^sub>R norm (f x)) - i) < e" + unfolding real_norm_def apply(rule *[rule_format,OF **],safe) apply(rule d(2)) + proof- case goal1 show ?case unfolding sum_p' + apply(rule isLubD2[OF i]) using division_of_tagged_division[OF p''] by auto + next case goal2 have *:"{k \ l | k l. k \ d \ l \ snd ` p} = + (\(k,l). k \ l) ` {(k,l)|k l. k \ d \ l \ snd ` p}" by auto + have "(\k\d. norm (integral k f)) \ (\i\d. \l\snd ` p. norm (integral (i \ l) f))" + proof(rule setsum_mono) case goal1 note k=this + from d'(4)[OF this] guess u v apply-by(erule exE)+ note uv=this + def d' \ "{{u..v} \ l |l. l \ snd ` p \ ~({u..v} \ l = {})}" note uvab = d'(2)[OF k[unfolded uv]] + have "d' division_of {u..v}" apply(subst d'_def) apply(rule division_inter_1) + apply(rule division_of_tagged_division[OF p(1)]) using uvab . + hence "norm (integral k f) \ setsum (\k. norm (integral k f)) d'" + unfolding uv apply(subst integral_combine_division_topdown[of _ _ d']) + apply(rule integrable_on_subinterval[OF assms(1) uvab]) apply assumption + apply(rule setsum_norm_le) by auto + also have "... = (\k\{k \ l |l. l \ snd ` p}. norm (integral k f))" + apply(rule setsum_mono_zero_left) apply(subst simple_image) + apply(rule finite_imageI)+ apply fact unfolding d'_def uv apply blast + proof case goal1 hence "i \ {{u..v} \ l |l. l \ snd ` p}" by auto + from this[unfolded mem_Collect_eq] guess l .. note l=this + hence "{u..v} \ l = {}" using goal1 by auto thus ?case using l by auto + qed also have "... = (\l\snd ` p. norm (integral (k \ l) f))" unfolding simple_image + apply(rule setsum_reindex_nonzero[unfolded o_def])apply(rule finite_imageI,rule p') + proof- case goal1 have "interior (k \ l) \ interior (l \ y)" apply(subst(2) interior_inter) + apply(rule Int_greatest) defer apply(subst goal1(4)) by auto + hence *:"interior (k \ l) = {}" using snd_p(5)[OF goal1(1-3)] by auto + from d'(4)[OF k] snd_p(4)[OF goal1(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this + show ?case using * unfolding uv inter_interval content_eq_0_interior[THEN sym] by auto + qed finally show ?case . + qed also have "... = (\(i,l)\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (i\l) f))" + apply(subst sum_sum_product[THEN sym],fact) using p'(1) by auto + also have "... = (\x\{(i, l) |i l. i \ d \ l \ snd ` p}. norm (integral (split op \ x) f))" + unfolding split_def .. + also have "... = (\k\{i \ l |i l. i \ d \ l \ snd ` p}. norm (integral k f))" + unfolding * apply(rule setsum_reindex_nonzero[THEN sym,unfolded o_def]) + apply(rule finite_product_dependent) apply(fact,rule finite_imageI,rule p') + unfolding split_paired_all mem_Collect_eq split_conv o_def + proof- note * = division_ofD(4,5)[OF division_of_tagged_division,OF p(1)] + fix l1 l2 k1 k2 assume as:"(l1, k1) \ (l2, k2)" "l1 \ k1 = l2 \ k2" + "\i l. (l1, k1) = (i, l) \ i \ d \ l \ snd ` p" + "\i l. (l2, k2) = (i, l) \ i \ d \ l \ snd ` p" + hence "l1 \ d" "k1 \ snd ` p" by auto from d'(4)[OF this(1)] *(1)[OF this(2)] + guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this + have "l1 \ l2 \ k1 \ k2" using as by auto + hence "(interior(k1) \ interior(k2) = {} \ interior(l1) \ interior(l2) = {})" apply- + apply(erule disjE) apply(rule disjI2) apply(rule d'(5)) prefer 4 apply(rule disjI1) + apply(rule *) using as by auto + moreover have "interior(l1 \ k1) = interior(l2 \ k2)" using as(2) by auto + ultimately have "interior(l1 \ k1) = {}" by auto + thus "norm (integral (l1 \ k1) f) = 0" unfolding uv inter_interval + unfolding content_eq_0_interior[THEN sym] by auto + qed also have "... = (\(x, k)\p'. norm (integral k f))" unfolding sum_p' + apply(rule setsum_mono_zero_right) apply(subst *) + apply(rule finite_imageI[OF finite_product_dependent]) apply fact + apply(rule finite_imageI[OF p'(1)]) apply safe + proof- case goal2 have "ia \ b = {}" using goal2 unfolding p'alt image_iff Bex_def not_ex + apply(erule_tac x="(a,ia\b)" in allE) by auto thus ?case by auto + next case goal1 thus ?case unfolding p'_def apply safe + apply(rule_tac x=i in exI,rule_tac x=l in exI) unfolding snd_conv image_iff + apply safe apply(rule_tac x="(a,l)" in bexI) by auto + qed finally show ?case . + + next case goal3 + let ?S = "{(x, i \ l) |x i l. (x, l) \ p \ i \ d}" + have Sigma_alt:"\s t. s \ t = {(i, j) |i j. i \ s \ j \ t}" by auto + have *:"?S = (\(xl,i). (fst xl, snd xl \ i)) ` (p \ d)" (*{(xl,i)|xl i. xl\p \ i\d}"**) + apply safe unfolding image_iff apply(rule_tac x="((x,l),i)" in bexI) by auto + note pdfin = finite_cartesian_product[OF p'(1) d'(1)] + have "(\(x, k)\p'. norm (content k *\<^sub>R f x)) = (\(x, k)\?S. \content k\ * norm (f x))" + unfolding norm_scaleR apply(rule setsum_mono_zero_left) + apply(subst *, rule finite_imageI) apply fact unfolding p'alt apply blast + apply safe apply(rule_tac x=x in exI,rule_tac x=i in exI,rule_tac x=l in exI) by auto + also have "... = (\((x,l),i)\p \ d. \content (l \ i)\ * norm (f x))" unfolding * + apply(subst setsum_reindex_nonzero,fact) unfolding split_paired_all + unfolding o_def split_def snd_conv fst_conv mem_Sigma_iff Pair_eq apply(erule_tac conjE)+ + proof- fix x1 l1 k1 x2 l2 k2 assume as:"(x1,l1)\p" "(x2,l2)\p" "k1\d" "k2\d" + "x1 = x2" "l1 \ k1 = l2 \ k2" "\ ((x1 = x2 \ l1 = l2) \ k1 = k2)" + from d'(4)[OF as(3)] p'(4)[OF as(1)] guess u1 v1 u2 v2 apply-by(erule exE)+ note uv=this + from as have "l1 \ l2 \ k1 \ k2" by auto + hence "(interior(k1) \ interior(k2) = {} \ interior(l1) \ interior(l2) = {})" + apply-apply(erule disjE) apply(rule disjI2) defer apply(rule disjI1) + apply(rule d'(5)[OF as(3-4)],assumption) apply(rule p'(5)[OF as(1-2)]) by auto + moreover have "interior(l1 \ k1) = interior(l2 \ k2)" unfolding as .. + ultimately have "interior (l1 \ k1) = {}" by auto + thus "\content (l1 \ k1)\ * norm (f x1) = 0" unfolding uv inter_interval + unfolding content_eq_0_interior[THEN sym] by auto + qed safe also have "... = (\(x, k)\p. content k *\<^sub>R norm (f x))" unfolding Sigma_alt + apply(subst sum_sum_product[THEN sym]) apply(rule p', rule,rule d') + apply(rule setsum_cong2) unfolding split_paired_all split_conv + proof- fix x l assume as:"(x,l)\p" + note xl = p'(2-4)[OF this] from this(3) guess u v apply-by(erule exE)+ note uv=this + have "(\i\d. \content (l \ i)\) = (\k\d. content (k \ {u..v}))" + apply(rule setsum_cong2) apply(drule d'(4),safe) apply(subst Int_commute) + unfolding inter_interval uv apply(subst abs_of_nonneg) by auto + also have "... = setsum content {k\{u..v}| k. k\d}" unfolding simple_image + apply(rule setsum_reindex_nonzero[unfolded o_def,THEN sym]) apply(rule d') + proof- case goal1 from d'(4)[OF this(1)] d'(4)[OF this(2)] + guess u1 v1 u2 v2 apply- by(erule exE)+ note uv=this + have "{} = interior ((k \ y) \ {u..v})" apply(subst interior_inter) + using d'(5)[OF goal1(1-3)] by auto + also have "... = interior (y \ (k \ {u..v}))" by auto + also have "... = interior (k \ {u..v})" unfolding goal1(4) by auto + finally show ?case unfolding uv inter_interval content_eq_0_interior .. + qed also have "... = setsum content {{u..v} \ k |k. k \ d \ ~({u..v} \ k = {})}" + apply(rule setsum_mono_zero_right) unfolding simple_image + apply(rule finite_imageI,rule d') apply blast apply safe + apply(rule_tac x=k in exI) + proof- case goal1 from d'(4)[OF this(1)] guess a b apply-by(erule exE)+ note ab=this + have "interior (k \ {u..v}) \ {}" using goal1(2) + unfolding ab inter_interval content_eq_0_interior by auto + thus ?case using goal1(1) using interior_subset[of "k \ {u..v}"] by auto + qed finally show "(\i\d. \content (l \ i)\ * norm (f x)) = content l *\<^sub>R norm (f x)" + unfolding setsum_left_distrib[THEN sym] real_scaleR_def apply - + apply(subst(asm) additive_content_division[OF division_inter_1[OF d(1)]]) + using xl(2)[unfolded uv] unfolding uv by auto + qed finally show ?case . + qed qed qed qed + +lemma bounded_variation_absolutely_integrable: fixes f::"real^'n \ real^'m" + assumes "f integrable_on UNIV" "\d. d division_of (\d) \ setsum (\k. norm(integral k f)) d \ B" + shows "f absolutely_integrable_on UNIV" +proof(rule absolutely_integrable_onI,fact,rule) + let ?S = "(\d. setsum (\k. norm(integral k f)) d) ` {d. d division_of (\d)}" def i \ "Sup ?S" + have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) + apply(rule elementary_interval) defer apply(rule_tac x=B in exI) + apply(rule setleI) using assms(2) by auto + have f_int:"\a b. f absolutely_integrable_on {a..b}" + apply(rule bounded_variation_absolutely_integrable_interval[where B=B]) + apply(rule integrable_on_subinterval[OF assms(1)]) defer apply safe + apply(rule assms(2)[rule_format]) by auto + show "((\x. norm (f x)) has_integral i) UNIV" apply(subst has_integral_alt',safe) + proof- case goal1 show ?case using f_int[of a b] by auto + next case goal2 have "\y\setsum (\k. norm (integral k f)) ` {d. d division_of \d}. \ y \ i - e" + proof(rule ccontr) case goal1 hence "i \ i - e" apply- + apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by auto + thus False using goal2 by auto + qed then guess K .. note * = this[unfolded image_iff not_le] + from this(1) guess d .. note this[unfolded mem_Collect_eq] + note d = this(1) *(2)[unfolded this(2)] note d'=division_ofD[OF this(1)] + have "bounded (\d)" by(rule elementary_bounded,fact) + from this[unfolded bounded_pos] guess K .. note K=conjunctD2[OF this] + show ?case apply(rule_tac x="K + 1" in exI,safe) + proof- fix a b assume ab:"ball 0 (K + 1) \ {a..b::real^'n}" + have *:"\s s1. i - e < s1 \ s1 \ s \ s < i + e \ abs(s - i) < (e::real)" by arith + show "norm (integral {a..b} (\x. if x \ UNIV then norm (f x) else 0) - i) < e" + unfolding real_norm_def apply(rule *[rule_format],safe) apply(rule d(2)) + proof- case goal1 have "(\k\d. norm (integral k f)) \ setsum (\k. integral k (\x. norm (f x))) d" + apply(rule setsum_mono) apply(rule absolutely_integrable_le) + apply(drule d'(4),safe) by(rule f_int) + also have "... = integral (\d) (\x. norm(f x))" + apply(rule integral_combine_division_bottomup[THEN sym]) + apply(rule d) unfolding forall_in_division[OF d(1)] using f_int by auto + also have "... \ integral {a..b} (\x. if x \ UNIV then norm (f x) else 0)" + proof- case goal1 have "\d \ {a..b}" apply rule apply(drule K(2)[rule_format]) + apply(rule ab[unfolded subset_eq,rule_format]) by(auto simp add:dist_norm) + thus ?case apply- apply(subst if_P,rule) apply(rule integral_subset_le) defer + apply(rule integrable_on_subdivision[of _ _ _ "{a..b}"]) + apply(rule d) using f_int[of a b] by auto + qed finally show ?case . + + next note f = absolutely_integrable_onD[OF f_int[of a b]] + note * = this(2)[unfolded has_integral_integral has_integral[of "\x. norm (f x)"],rule_format] + have "e/2>0" using `e>0` by auto from *[OF this] guess d1 .. note d1=conjunctD2[OF this] + from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this + from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p . + note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]] + have *:"\sf sf' si di. sf' = sf \ si \ i \ abs(sf - si) < e / 2 + \ abs(sf' - di) < e / 2 \ di < i + e" by arith + show "integral {a..b} (\x. if x \ UNIV then norm (f x) else 0) < i + e" apply(subst if_P,rule) + proof(rule *[rule_format]) + show "\(\(x,k)\p. norm (content k *\<^sub>R f x)) - (\(x,k)\p. norm (integral k f))\ < e / 2" + unfolding split_def apply(rule helplemma) using d2(2)[rule_format,of p] + using p(1,3) unfolding tagged_division_of_def split_def by auto + show "abs ((\(x, k)\p. content k *\<^sub>R norm (f x)) - integral {a..b} (\x. norm(f x))) < e / 2" + using d1(2)[rule_format,OF conjI[OF p(1,2)]] unfolding real_norm_def . + show "(\(x, k)\p. content k *\<^sub>R norm (f x)) = (\(x, k)\p. norm (content k *\<^sub>R f x))" + apply(rule setsum_cong2) unfolding split_paired_all split_conv + apply(drule tagged_division_ofD(4)[OF p(1)]) unfolding norm_scaleR + apply(subst abs_of_nonneg) by auto + show "(\(x, k)\p. norm (integral k f)) \ i" + apply(subst setsum_over_tagged_division_lemma[OF p(1)]) defer apply(rule isLubD2[OF i]) + unfolding image_iff apply(rule_tac x="snd ` p" in bexI) unfolding mem_Collect_eq defer + apply(rule partial_division_of_tagged_division[of _ "{a..b}"]) + using p(1) unfolding tagged_division_of_def by auto + qed qed qed(insert K,auto) qed qed + +lemma absolutely_integrable_restrict_univ: + "(\x. if x \ s then f x else (0::'a::banach)) absolutely_integrable_on UNIV \ f absolutely_integrable_on s" + unfolding absolutely_integrable_on_def if_distrib norm_zero integrable_restrict_univ .. + +lemma absolutely_integrable_add[intro]: fixes f g::"real^'n \ real^'m" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. f(x) + g(x)) absolutely_integrable_on s" +proof- let ?P = "\f g::real^'n \ real^'m. f absolutely_integrable_on UNIV \ + g absolutely_integrable_on UNIV \ (\x. f(x) + g(x)) absolutely_integrable_on UNIV" + { presume as:"PROP ?P" note a = absolutely_integrable_restrict_univ[THEN sym] + have *:"\x. (if x \ s then f x else 0) + (if x \ s then g x else 0) + = (if x \ s then f x + g x else 0)" by auto + show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] unfolding * . } + fix f g::"real^'n \ real^'m" assume assms:"f absolutely_integrable_on UNIV" + "g absolutely_integrable_on UNIV" + note absolutely_integrable_bounded_variation + from this[OF assms(1)] this[OF assms(2)] guess B1 B2 . note B=this[rule_format] + show "(\x. f(x) + g(x)) absolutely_integrable_on UNIV" + apply(rule bounded_variation_absolutely_integrable[of _ "B1+B2"]) + apply(rule integrable_add) prefer 3 + proof safe case goal1 have "\k. k \ d \ f integrable_on k \ g integrable_on k" + apply(drule division_ofD(4)[OF goal1]) apply safe + apply(rule_tac[!] integrable_on_subinterval[of _ UNIV]) using assms by auto + hence "(\k\d. norm (integral k (\x. f x + g x))) \ + (\k\d. norm (integral k f)) + (\k\d. norm (integral k g))" apply- + unfolding setsum_addf[THEN sym] apply(rule setsum_mono) + apply(subst integral_add) prefer 3 apply(rule norm_triangle_ineq) by auto + also have "... \ B1 + B2" using B(1)[OF goal1] B(2)[OF goal1] by auto + finally show ?case . + qed(insert assms,auto) qed + +lemma absolutely_integrable_sub[intro]: fixes f g::"real^'n \ real^'m" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. f(x) - g(x)) absolutely_integrable_on s" + using absolutely_integrable_add[OF assms(1) absolutely_integrable_neg[OF assms(2)]] + unfolding group_simps . + +lemma absolutely_integrable_linear: fixes f::"real^'m \ real^'n" and h::"real^'n \ real^'p" + assumes "f absolutely_integrable_on s" "bounded_linear h" + shows "(h o f) absolutely_integrable_on s" +proof- { presume as:"\f::real^'m \ real^'n. \h::real^'n \ real^'p. + f absolutely_integrable_on UNIV \ bounded_linear h \ + (h o f) absolutely_integrable_on UNIV" note a = absolutely_integrable_restrict_univ[THEN sym] + show ?thesis apply(subst a) using as[OF assms[unfolded a[of f] a[of g]]] + unfolding o_def if_distrib linear_simps[OF assms(2)] . } + fix f::"real^'m \ real^'n" and h::"real^'n \ real^'p" + assume assms:"f absolutely_integrable_on UNIV" "bounded_linear h" + from absolutely_integrable_bounded_variation[OF assms(1)] guess B . note B=this + from bounded_linear.pos_bounded[OF assms(2)] guess b .. note b=conjunctD2[OF this] + show "(h o f) absolutely_integrable_on UNIV" + apply(rule bounded_variation_absolutely_integrable[of _ "B * b"]) + apply(rule integrable_linear[OF _ assms(2)]) + proof safe case goal2 + have "(\k\d. norm (integral k (h \ f))) \ setsum (\k. norm(integral k f)) d * b" + unfolding setsum_left_distrib apply(rule setsum_mono) + proof- case goal1 from division_ofD(4)[OF goal2 this] + guess u v apply-by(erule exE)+ note uv=this + have *:"f integrable_on k" unfolding uv apply(rule integrable_on_subinterval[of _ UNIV]) + using assms by auto note this[unfolded has_integral_integral] + note has_integral_linear[OF this assms(2)] integrable_linear[OF * assms(2)] + note * = has_integral_unique[OF this(2)[unfolded has_integral_integral] this(1)] + show ?case unfolding * using b by auto + qed also have "... \ B * b" apply(rule mult_right_mono) using B goal2 b by auto + finally show ?case . + qed(insert assms,auto) qed + +lemma absolutely_integrable_setsum: fixes f::"'a \ real^'n \ real^'m" + assumes "finite t" "\a. a \ t \ (f a) absolutely_integrable_on s" + shows "(\x. setsum (\a. f a x) t) absolutely_integrable_on s" + using assms(1,2) apply induct defer apply(subst setsum.insert) apply assumption+ by(rule,auto) + +lemma absolutely_integrable_vector_abs: + assumes "f absolutely_integrable_on s" + shows "(\x. (\ i. abs(f x$i))::real^'n) absolutely_integrable_on s" +proof- have *:"\x. ((\ i. abs(f x$i))::real^'n) = (setsum (\i. + (((\y. (\ j. if j = i then y$1 else 0)) o + (vec1 o ((\x. (norm((\ j. if j = i then x$i else 0)::real^'n))) o f))) x)) UNIV)" + unfolding Cart_eq setsum_component Cart_lambda_beta + proof case goal1 have *:"\i xa. ((if i = xa then f x $ xa else 0) \ (if i = xa then f x $ xa else 0)) = + (if i = xa then (f x $ xa) * (f x $ xa) else 0)" by auto + have "\f x $ i\ = (setsum (\k. if k = i then abs ((f x)$i) else 0) UNIV)" + unfolding setsum_delta[OF finite_UNIV] by auto + also have "... = (\xa\UNIV. ((\y. \ j. if j = xa then dest_vec1 y else 0) \ + (\x. vec1 (norm (\ j. if j = xa then x $ xa else 0))) \ f) x $ i)" + unfolding norm_eq_sqrt_inner inner_vector_def Cart_lambda_beta o_def * + apply(rule setsum_cong2) unfolding setsum_delta[OF finite_UNIV] by auto + finally show ?case unfolding o_def . qed + show ?thesis unfolding * apply(rule absolutely_integrable_setsum) apply(rule finite_UNIV) + apply(rule absolutely_integrable_linear) + unfolding absolutely_integrable_on_trans unfolding o_def apply(rule absolutely_integrable_norm) + apply(rule absolutely_integrable_linear[OF assms,unfolded o_def]) unfolding linear_linear + apply(rule_tac[!] linearI) unfolding Cart_eq by auto +qed + +lemma absolutely_integrable_max: fixes f::"real^'m \ real^'n" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. (\ i. max (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s" +proof- have *:"\x. (1 / 2) *\<^sub>R ((\ i. \(f x - g x) $ i\) + (f x + g x)) = (\ i. max (f(x)$i) (g(x)$i))" + unfolding Cart_eq by auto + note absolutely_integrable_sub[OF assms] absolutely_integrable_add[OF assms] + note absolutely_integrable_vector_abs[OF this(1)] this(2) + note absolutely_integrable_add[OF this] note absolutely_integrable_cmul[OF this,of "1/2"] + thus ?thesis unfolding * . qed + +lemma absolutely_integrable_max_real: fixes f::"real^'m \ real" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. max (f x) (g x)) absolutely_integrable_on s" +proof- have *:"(\x. \ i. max ((vec1 \ f) x $ i) ((vec1 \ g) x $ i)) = vec1 o (\x. max (f x) (g x))" + apply rule unfolding Cart_eq by auto note absolutely_integrable_max[of "vec1 o f" s "vec1 o g"] + note this[unfolded absolutely_integrable_on_trans,OF assms] + thus ?thesis unfolding * by auto qed + +lemma absolutely_integrable_min: fixes f::"real^'m \ real^'n" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. (\ i. min (f(x)$i) (g(x)$i))::real^'n) absolutely_integrable_on s" +proof- have *:"\x. (1 / 2) *\<^sub>R ((f x + g x) - (\ i. \(f x - g x) $ i\)) = (\ i. min (f(x)$i) (g(x)$i))" + unfolding Cart_eq by auto + note absolutely_integrable_add[OF assms] absolutely_integrable_sub[OF assms] + note this(1) absolutely_integrable_vector_abs[OF this(2)] + note absolutely_integrable_sub[OF this] note absolutely_integrable_cmul[OF this,of "1/2"] + thus ?thesis unfolding * . qed + +lemma absolutely_integrable_min_real: fixes f::"real^'m \ real" + assumes "f absolutely_integrable_on s" "g absolutely_integrable_on s" + shows "(\x. min (f x) (g x)) absolutely_integrable_on s" +proof- have *:"(\x. \ i. min ((vec1 \ f) x $ i) ((vec1 \ g) x $ i)) = vec1 o (\x. min (f x) (g x))" + apply rule unfolding Cart_eq by auto note absolutely_integrable_min[of "vec1 o f" s "vec1 o g"] + note this[unfolded absolutely_integrable_on_trans,OF assms] + thus ?thesis unfolding * by auto qed + +lemma absolutely_integrable_abs_eq: fixes f::"real^'n \ real^'m" + shows "f absolutely_integrable_on s \ f integrable_on s \ + (\x. (\ i. abs(f x$i))::real^'m) integrable_on s" (is "?l = ?r") +proof assume ?l thus ?r apply-apply rule defer + apply(drule absolutely_integrable_vector_abs) by auto +next assume ?r { presume lem:"\f::real^'n \ real^'m. f integrable_on UNIV \ + (\x. (\ i. abs(f(x)$i))::real^'m) integrable_on UNIV \ f absolutely_integrable_on UNIV" + have *:"\x. (\ i. \(if x \ s then f x else 0) $ i\) = (if x\s then (\ i. \f x $ i\) else 0)" + unfolding Cart_eq by auto + show ?l apply(subst absolutely_integrable_restrict_univ[THEN sym]) apply(rule lem) + unfolding integrable_restrict_univ * using `?r` by auto } + fix f::"real^'n \ real^'m" assume assms:"f integrable_on UNIV" + "(\x. (\ i. abs(f(x)$i))::real^'m) integrable_on UNIV" + let ?B = "setsum (\i. integral UNIV (\x. (\ j. abs(f x$j)) ::real^'m) $ i) UNIV" + show "f absolutely_integrable_on UNIV" + apply(rule bounded_variation_absolutely_integrable[OF assms(1), where B="?B"],safe) + proof- case goal1 note d=this and d'=division_ofD[OF this] + have "(\k\d. norm (integral k f)) \ + (\k\d. setsum (op $ (integral k (\x. \ j. \f x $ j\))) UNIV)" apply(rule setsum_mono) + apply(rule order_trans[OF norm_le_l1],rule setsum_mono) + proof- fix k and i::'m assume "k\d" + from d'(4)[OF this] guess a b apply-by(erule exE)+ note ab=this + show "\integral k f $ i\ \ integral k (\x. \ j. \f x $ j\) $ i" apply(rule abs_leI) + unfolding vector_uminus_component[THEN sym] defer apply(subst integral_neg[THEN sym]) + defer apply(rule_tac[1-2] integral_component_le) apply(rule integrable_neg) + using integrable_on_subinterval[OF assms(1),of a b] + integrable_on_subinterval[OF assms(2),of a b] unfolding ab by auto + qed also have "... \ setsum (op $ (integral UNIV (\x. \ j. \f x $ j\))) UNIV" + apply(subst setsum_commute,rule setsum_mono) + proof- case goal1 have *:"(\x. \ j. \f x $ j\) integrable_on \d" + using integrable_on_subdivision[OF d assms(2)] by auto + have "(\i\d. integral i (\x. \ j. \f x $ j\) $ j) + = integral (\d) (\x. (\ j. abs(f x$j)) ::real^'m) $ j" + unfolding setsum_component[THEN sym] + apply(subst integral_combine_division_topdown[THEN sym,OF * d]) by auto + also have "... \ integral UNIV (\x. \ j. \f x $ j\) $ j" + apply(rule integral_subset_component_le) using assms * by auto + finally show ?case . + qed finally show ?case . qed qed + +lemma nonnegative_absolutely_integrable: fixes f::"real^'n \ real^'m" + assumes "\x\s. \i. 0 \ f(x)$i" "f integrable_on s" + shows "f absolutely_integrable_on s" + unfolding absolutely_integrable_abs_eq apply rule defer + apply(rule integrable_eq[of _ f]) unfolding Cart_eq using assms by auto + +lemma absolutely_integrable_integrable_bound: fixes f::"real^'n \ real^'m" + assumes "\x\s. norm(f x) \ g x" "f integrable_on s" "g integrable_on s" + shows "f absolutely_integrable_on s" +proof- { presume *:"\f::real^'n \ real^'m. \ g. \x. norm(f x) \ g x \ f integrable_on UNIV + \ g integrable_on UNIV \ f absolutely_integrable_on UNIV" + show ?thesis apply(subst absolutely_integrable_restrict_univ[THEN sym]) + apply(rule *[of _ "\x. if x\s then g x else 0"]) + using assms unfolding integrable_restrict_univ by auto } + fix g and f :: "real^'n \ real^'m" + assume assms:"\x. norm(f x) \ g x" "f integrable_on UNIV" "g integrable_on UNIV" + show "f absolutely_integrable_on UNIV" + apply(rule bounded_variation_absolutely_integrable[OF assms(2),where B="integral UNIV g"]) + proof safe case goal1 note d=this and d'=division_ofD[OF this] + have "(\k\d. norm (integral k f)) \ (\k\d. integral k g)" + apply(rule setsum_mono) apply(rule integral_norm_bound_integral) apply(drule_tac[!] d'(4),safe) + apply(rule_tac[1-2] integrable_on_subinterval) using assms by auto + also have "... = integral (\d) g" apply(rule integral_combine_division_bottomup[THEN sym]) + apply(rule d,safe) apply(drule d'(4),safe) + apply(rule integrable_on_subinterval[OF assms(3)]) by auto + also have "... \ integral UNIV g" apply(rule integral_subset_le) defer + apply(rule integrable_on_subdivision[OF d,of _ UNIV]) prefer 4 + apply(rule,rule_tac y="norm (f x)" in order_trans) using assms by auto + finally show ?case . qed qed + +lemma absolutely_integrable_integrable_bound_real: fixes f::"real^'n \ real" + assumes "\x\s. norm(f x) \ g x" "f integrable_on s" "g integrable_on s" + shows "f absolutely_integrable_on s" + apply(subst absolutely_integrable_on_trans[THEN sym]) + apply(rule absolutely_integrable_integrable_bound[where g=g]) + using assms unfolding o_def by auto + +lemma absolutely_integrable_absolutely_integrable_bound: + fixes f::"real^'n \ real^'m" and g::"real^'n \ real^'p" + assumes "\x\s. norm(f x) \ norm(g x)" "f integrable_on s" "g absolutely_integrable_on s" + shows "f absolutely_integrable_on s" + apply(rule absolutely_integrable_integrable_bound[of s f "\x. norm (g x)"]) + using assms by auto + +lemma absolutely_integrable_inf_real: + assumes "finite k" "k \ {}" + "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" + shows "(\x. (Inf ((fs x) ` k))) absolutely_integrable_on s" using assms +proof induct case (insert a k) let ?P = " (\x. if fs x ` k = {} then fs x a + else min (fs x a) (Inf (fs x ` k))) absolutely_integrable_on s" + show ?case unfolding image_insert + apply(subst Inf_insert_finite) apply(rule finite_imageI[OF insert(1)]) + proof(cases "k={}") case True + thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto + next case False thus ?P apply(subst if_not_P) defer + apply(rule absolutely_integrable_min_real) + defer apply(rule insert(3)[OF False]) using insert(5) by auto + qed qed auto + +lemma absolutely_integrable_sup_real: + assumes "finite k" "k \ {}" + "\i\k. (\x. (fs x i)::real) absolutely_integrable_on s" + shows "(\x. (Sup ((fs x) ` k))) absolutely_integrable_on s" using assms +proof induct case (insert a k) let ?P = " (\x. if fs x ` k = {} then fs x a + else max (fs x a) (Sup (fs x ` k))) absolutely_integrable_on s" + show ?case unfolding image_insert + apply(subst Sup_insert_finite) apply(rule finite_imageI[OF insert(1)]) + proof(cases "k={}") case True + thus ?P apply(subst if_P) defer apply(rule insert(5)[rule_format]) by auto + next case False thus ?P apply(subst if_not_P) defer + apply(rule absolutely_integrable_max_real) + defer apply(rule insert(3)[OF False]) using insert(5) by auto + qed qed auto + +subsection {* Dominated convergence. *} + +lemma dominated_convergence: fixes f::"nat \ real^'n \ real" + assumes "\k. (f k) integrable_on s" "h integrable_on s" + "\k. \x \ s. norm(f k x) \ (h x)" + "\x \ s. ((\k. f k x) ---> g x) sequentially" + shows "g integrable_on s" "((\k. integral s (f k)) ---> integral s g) sequentially" +proof- have "\m. (\x. Inf {f j x |j. m \ j}) integrable_on s \ + ((\k. integral s (\x. Inf {f j x |j. j \ {m..m + k}})) ---> + integral s (\x. Inf {f j x |j. m \ j}))sequentially" + proof(rule monotone_convergence_decreasing_real,safe) fix m::nat + show "bounded {integral s (\x. Inf {f j x |j. j \ {m..m + k}}) |k. True}" + unfolding bounded_iff apply(rule_tac x="integral s h" in exI) + proof safe fix k::nat + show "norm (integral s (\x. Inf {f j x |j. j \ {m..m + k}})) \ integral s h" + apply(rule integral_norm_bound_integral) unfolding simple_image + apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_inf_real) + prefer 5 unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) + prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real) + using assms unfolding real_norm_def by auto + qed fix k::nat show "(\x. Inf {f j x |j. j \ {m..m + k}}) integrable_on s" + unfolding simple_image apply(rule absolutely_integrable_onD) + apply(rule absolutely_integrable_inf_real) prefer 3 + using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto + fix x assume x:"x\s" show "Inf {f j x |j. j \ {m..m + Suc k}} + \ Inf {f j x |j. j \ {m..m + k}}" apply(rule Inf_ge) unfolding setge_def + defer apply rule apply(subst Inf_finite_le_iff) prefer 3 + apply(rule_tac x=xa in bexI) by auto + let ?S = "{f j x| j. m \ j}" def i \ "Inf ?S" + show "((\k. Inf {f j x |j. j \ {m..m + k}}) ---> i) sequentially" + unfolding Lim_sequentially + proof safe case goal1 note e=this have i:"isGlb UNIV ?S i" unfolding i_def apply(rule Inf) + defer apply(rule_tac x="- h x - 1" in exI) unfolding setge_def + proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto + qed auto + + have "\y\?S. \ y \ i + e" + proof(rule ccontr) case goal1 hence "i \ i + e" apply- + apply(rule isGlb_le_isLb[OF i]) apply(rule isLbI) unfolding setge_def by fastsimp+ + thus False using e by auto + qed then guess y .. note y=this[unfolded not_le] + from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] + + show ?case apply(rule_tac x=N in exI) + proof safe case goal1 + have *:"\y ix. y < i + e \ i \ ix \ ix \ y \ abs(ix - i) < e" by arith + show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)]) + unfolding i_def apply(rule real_le_inf_subset) prefer 3 + apply(rule,rule isGlbD1[OF i]) prefer 3 apply(subst Inf_finite_le_iff) + prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto + qed qed qed note dec1 = conjunctD2[OF this] + + have "\m. (\x. Sup {f j x |j. m \ j}) integrable_on s \ + ((\k. integral s (\x. Sup {f j x |j. j \ {m..m + k}})) ---> + integral s (\x. Sup {f j x |j. m \ j})) sequentially" + proof(rule monotone_convergence_increasing_real,safe) fix m::nat + show "bounded {integral s (\x. Sup {f j x |j. j \ {m..m + k}}) |k. True}" + unfolding bounded_iff apply(rule_tac x="integral s h" in exI) + proof safe fix k::nat + show "norm (integral s (\x. Sup {f j x |j. j \ {m..m + k}})) \ integral s h" + apply(rule integral_norm_bound_integral) unfolding simple_image + apply(rule absolutely_integrable_onD) apply(rule absolutely_integrable_sup_real) + prefer 5 unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) + prefer 5 apply rule apply(rule_tac g=h in absolutely_integrable_integrable_bound_real) + using assms unfolding real_norm_def by auto + qed fix k::nat show "(\x. Sup {f j x |j. j \ {m..m + k}}) integrable_on s" + unfolding simple_image apply(rule absolutely_integrable_onD) + apply(rule absolutely_integrable_sup_real) prefer 3 + using absolutely_integrable_integrable_bound_real[OF assms(3,1,2)] by auto + fix x assume x:"x\s" show "Sup {f j x |j. j \ {m..m + Suc k}} + \ Sup {f j x |j. j \ {m..m + k}}" apply(rule Sup_le) unfolding setle_def + defer apply rule apply(subst Sup_finite_ge_iff) prefer 3 apply(rule_tac x=y in bexI) by auto + let ?S = "{f j x| j. m \ j}" def i \ "Sup ?S" + show "((\k. Sup {f j x |j. j \ {m..m + k}}) ---> i) sequentially" + unfolding Lim_sequentially + proof safe case goal1 note e=this have i:"isLub UNIV ?S i" unfolding i_def apply(rule Sup) + defer apply(rule_tac x="h x" in exI) unfolding setle_def + proof safe case goal1 thus ?case using assms(3)[rule_format,OF x, of j] by auto + qed auto + + have "\y\?S. \ y \ i - e" + proof(rule ccontr) case goal1 hence "i \ i - e" apply- + apply(rule isLub_le_isUb[OF i]) apply(rule isUbI) unfolding setle_def by fastsimp+ + thus False using e by auto + qed then guess y .. note y=this[unfolded not_le] + from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this] + + show ?case apply(rule_tac x=N in exI) + proof safe case goal1 + have *:"\y ix. i - e < y \ ix \ i \ y \ ix \ abs(ix - i) < e" by arith + show ?case unfolding dist_real_def apply(rule *[rule_format,OF y(2)]) + unfolding i_def apply(rule real_ge_sup_subset) prefer 3 + apply(rule,rule isLubD1[OF i]) prefer 3 apply(subst Sup_finite_ge_iff) + prefer 3 apply(rule_tac x=y in bexI) using N goal1 by auto + qed qed qed note inc1 = conjunctD2[OF this] + + have "g integrable_on s \ ((\k. integral s (\x. Inf {f j x |j. k \ j})) ---> integral s g) sequentially" + apply(rule monotone_convergence_increasing_real,safe) apply fact + proof- show "bounded {integral s (\x. Inf {f j x |j. k \ j}) |k. True}" + unfolding bounded_iff apply(rule_tac x="integral s h" in exI) + proof safe fix k::nat + show "norm (integral s (\x. Inf {f j x |j. k \ j})) \ integral s h" + apply(rule integral_norm_bound_integral) apply fact+ + unfolding real_norm_def apply(rule) apply(rule Inf_abs_ge) using assms(3) by auto + qed fix k::nat and x assume x:"x\s" + + have *:"\x y::real. x \ - y \ - x \ y" by auto + show "Inf {f j x |j. k \ j} \ Inf {f j x |j. Suc k \ j}" apply- + apply(rule real_le_inf_subset) prefer 3 unfolding setge_def + apply(rule_tac x="- h x" in exI) apply safe apply(rule *) + using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto + show "((\k. Inf {f j x |j. k \ j}) ---> g x) sequentially" unfolding Lim_sequentially + proof safe case goal1 hence "0 ((\k. integral s (\x. Sup {f j x |j. k \ j})) ---> integral s g) sequentially" + apply(rule monotone_convergence_decreasing_real,safe) apply fact + proof- show "bounded {integral s (\x. Sup {f j x |j. k \ j}) |k. True}" + unfolding bounded_iff apply(rule_tac x="integral s h" in exI) + proof safe fix k::nat + show "norm (integral s (\x. Sup {f j x |j. k \ j})) \ integral s h" + apply(rule integral_norm_bound_integral) apply fact+ + unfolding real_norm_def apply(rule) apply(rule Sup_abs_le) using assms(3) by auto + qed fix k::nat and x assume x:"x\s" + + show "Sup {f j x |j. k \ j} \ Sup {f j x |j. Suc k \ j}" apply- + apply(rule real_ge_sup_subset) prefer 3 unfolding setle_def + apply(rule_tac x="h x" in exI) apply safe + using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto + show "((\k. Sup {f j x |j. k \ j}) ---> g x) sequentially" unfolding Lim_sequentially + proof safe case goal1 hence "0k. integral s (f k)) ---> integral s g) sequentially" unfolding Lim_sequentially + proof safe case goal1 + from inc2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N1 .. note N1=this[unfolded dist_real_def] + from dec2(2)[unfolded Lim_sequentially,rule_format,OF goal1] guess N2 .. note N2=this[unfolded dist_real_def] + show ?case apply(rule_tac x="N1+N2" in exI,safe) + proof- fix n assume n:"n \ N1 + N2" + have *:"\i0 i i1 g. \i0 - g\ < e \ \i1 - g\ < e \ i0 \ i \ i \ i1 \ \i - g\ < e" by arith + show "dist (integral s (f n)) (integral s g) < e" unfolding dist_real_def + apply(rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n]) + proof- show "integral s (\x. Inf {f j x |j. n \ j}) \ integral s (f n)" + proof(rule integral_le[OF dec1(1) assms(1)],safe) + fix x assume x:"x \ s" have *:"\x y::real. x \ - y \ - x \ y" by auto + show "Inf {f j x |j. n \ j} \ f n x" apply(rule Inf_lower[where z="- h x"]) defer + apply(rule *) using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto + qed show "integral s (f n) \ integral s (\x. Sup {f j x |j. n \ j})" + proof(rule integral_le[OF assms(1) inc1(1)],safe) + fix x assume x:"x \ s" + show "f n x \ Sup {f j x |j. n \ j}" apply(rule Sup_upper[where z="h x"]) defer + using assms(3)[rule_format,OF x] unfolding real_norm_def abs_le_iff by auto + qed qed(insert n,auto) qed qed qed declare [[smt_certificates=""]]