src/HOL/Analysis/Improper_Integral.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago) changeset 69981 3dced198b9ec parent 69722 b5163b2132c5 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
 ak2110@69722 ` 1` ```section \Continuity of the indefinite integral; improper integral theorem\ ``` lp15@66296 ` 2` lp15@66296 ` 3` ```theory "Improper_Integral" ``` lp15@66296 ` 4` ``` imports Equivalence_Lebesgue_Henstock_Integration ``` lp15@66296 ` 5` ```begin ``` lp15@66296 ` 6` immler@69683 ` 7` ```subsection \Equiintegrability\ ``` lp15@66296 ` 8` lp15@66296 ` 9` ```text\The definition here only really makes sense for an elementary set. ``` lp15@66296 ` 10` ``` We just use compact intervals in applications below.\ ``` lp15@66296 ` 11` ak2110@69173 ` 12` ```definition%important equiintegrable_on (infixr "equiintegrable'_on" 46) ``` lp15@66296 ` 13` ``` where "F equiintegrable_on I \ ``` lp15@66296 ` 14` ``` (\f \ F. f integrable_on I) \ ``` lp15@66296 ` 15` ``` (\e > 0. \\. gauge \ \ ``` lp15@66296 ` 16` ``` (\f \. f \ F \ \ tagged_division_of I \ \ fine \ ``` lp15@66296 ` 17` ``` \ norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral I f) < e))" ``` lp15@66296 ` 18` lp15@66296 ` 19` ```lemma equiintegrable_on_integrable: ``` lp15@66296 ` 20` ``` "\F equiintegrable_on I; f \ F\ \ f integrable_on I" ``` lp15@66296 ` 21` ``` using equiintegrable_on_def by metis ``` lp15@66296 ` 22` lp15@66296 ` 23` ```lemma equiintegrable_on_sing [simp]: ``` lp15@66296 ` 24` ``` "{f} equiintegrable_on cbox a b \ f integrable_on cbox a b" ``` lp15@66296 ` 25` ``` by (simp add: equiintegrable_on_def has_integral_integral has_integral integrable_on_def) ``` lp15@66296 ` 26` ``` ``` lp15@66296 ` 27` ```lemma equiintegrable_on_subset: "\F equiintegrable_on I; G \ F\ \ G equiintegrable_on I" ``` lp15@66296 ` 28` ``` unfolding equiintegrable_on_def Ball_def ``` lp15@66296 ` 29` ``` by (erule conj_forward imp_forward all_forward ex_forward | blast)+ ``` lp15@66296 ` 30` immler@69681 ` 31` ```lemma equiintegrable_on_Un: ``` lp15@66296 ` 32` ``` assumes "F equiintegrable_on I" "G equiintegrable_on I" ``` lp15@66296 ` 33` ``` shows "(F \ G) equiintegrable_on I" ``` lp15@66296 ` 34` ``` unfolding equiintegrable_on_def ``` immler@69681 ` 35` ```proof (intro conjI impI allI) ``` lp15@66296 ` 36` ``` show "\f\F \ G. f integrable_on I" ``` lp15@66296 ` 37` ``` using assms unfolding equiintegrable_on_def by blast ``` lp15@66296 ` 38` ``` show "\\. gauge \ \ ``` lp15@66296 ` 39` ``` (\f \. f \ F \ G \ ``` lp15@66296 ` 40` ``` \ tagged_division_of I \ \ fine \ \ ``` lp15@66296 ` 41` ``` norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral I f) < \)" ``` lp15@66296 ` 42` ``` if "\ > 0" for \ ``` lp15@66296 ` 43` ``` proof - ``` lp15@66296 ` 44` ``` obtain \1 where "gauge \1" ``` lp15@66296 ` 45` ``` and \1: "\f \. f \ F \ \ tagged_division_of I \ \1 fine \ ``` lp15@66296 ` 46` ``` \ norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral I f) < \" ``` lp15@66296 ` 47` ``` using assms \\ > 0\ unfolding equiintegrable_on_def by auto ``` lp15@66296 ` 48` ``` obtain \2 where "gauge \2" ``` lp15@66296 ` 49` ``` and \2: "\f \. f \ G \ \ tagged_division_of I \ \2 fine \ ``` lp15@66296 ` 50` ``` \ norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral I f) < \" ``` lp15@66296 ` 51` ``` using assms \\ > 0\ unfolding equiintegrable_on_def by auto ``` lp15@66296 ` 52` ``` have "gauge (\x. \1 x \ \2 x)" ``` lp15@66296 ` 53` ``` using \gauge \1\ \gauge \2\ by blast ``` lp15@66296 ` 54` ``` moreover have "\f \. f \ F \ G \ \ tagged_division_of I \ (\x. \1 x \ \2 x) fine \ \ ``` lp15@66296 ` 55` ``` norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral I f) < \" ``` lp15@66296 ` 56` ``` using \1 \2 by (auto simp: fine_Int) ``` lp15@66296 ` 57` ``` ultimately show ?thesis ``` lp15@66296 ` 58` ``` by (intro exI conjI) assumption+ ``` lp15@66296 ` 59` ``` qed ``` lp15@66296 ` 60` ```qed ``` lp15@66296 ` 61` lp15@66296 ` 62` lp15@66296 ` 63` ```lemma equiintegrable_on_insert: ``` lp15@66296 ` 64` ``` assumes "f integrable_on cbox a b" "F equiintegrable_on cbox a b" ``` lp15@66296 ` 65` ``` shows "(insert f F) equiintegrable_on cbox a b" ``` lp15@66296 ` 66` ``` by (metis assms equiintegrable_on_Un equiintegrable_on_sing insert_is_Un) ``` lp15@66296 ` 67` lp15@66296 ` 68` lp15@66296 ` 69` ```text\ Basic combining theorems for the interval of integration.\ ``` lp15@66296 ` 70` lp15@66296 ` 71` ```lemma equiintegrable_on_null [simp]: ``` lp15@66296 ` 72` ``` "content(cbox a b) = 0 \ F equiintegrable_on cbox a b" ``` lp15@66296 ` 73` ``` apply (auto simp: equiintegrable_on_def) ``` lp15@66296 ` 74` ``` by (metis gauge_trivial norm_eq_zero sum_content_null) ``` lp15@66296 ` 75` lp15@66296 ` 76` lp15@66296 ` 77` ```text\ Main limit theorem for an equiintegrable sequence.\ ``` lp15@66296 ` 78` immler@69681 ` 79` ```theorem equiintegrable_limit: ``` lp15@66296 ` 80` ``` fixes g :: "'a :: euclidean_space \ 'b :: banach" ``` lp15@66296 ` 81` ``` assumes feq: "range f equiintegrable_on cbox a b" ``` lp15@66296 ` 82` ``` and to_g: "\x. x \ cbox a b \ (\n. f n x) \ g x" ``` lp15@66296 ` 83` ``` shows "g integrable_on cbox a b \ (\n. integral (cbox a b) (f n)) \ integral (cbox a b) g" ``` immler@69681 ` 84` ```proof - ``` lp15@66296 ` 85` ``` have "Cauchy (\n. integral(cbox a b) (f n))" ``` lp15@66296 ` 86` ``` proof (clarsimp simp add: Cauchy_def) ``` lp15@66296 ` 87` ``` fix e::real ``` lp15@66296 ` 88` ``` assume "0 < e" ``` lp15@66296 ` 89` ``` then have e3: "0 < e/3" ``` lp15@66296 ` 90` ``` by simp ``` lp15@66296 ` 91` ``` then obtain \ where "gauge \" ``` lp15@66296 ` 92` ``` and \: "\n \. \\ tagged_division_of cbox a b; \ fine \\ ``` lp15@66296 ` 93` ``` \ norm((\(x,K) \ \. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) < e/3" ``` lp15@66296 ` 94` ``` using feq unfolding equiintegrable_on_def ``` lp15@66296 ` 95` ``` by (meson image_eqI iso_tuple_UNIV_I) ``` lp15@66296 ` 96` ``` obtain \ where \: "\ tagged_division_of (cbox a b)" and "\ fine \" "finite \" ``` lp15@66296 ` 97` ``` by (meson \gauge \\ fine_division_exists tagged_division_of_finite) ``` lp15@66296 ` 98` ``` with \ have \T: "\n. dist ((\(x,K)\\. content K *\<^sub>R f n x)) (integral (cbox a b) (f n)) < e/3" ``` lp15@66296 ` 99` ``` by (force simp: dist_norm) ``` lp15@66296 ` 100` ``` have "(\n. \(x,K)\\. content K *\<^sub>R f n x) \ (\(x,K)\\. content K *\<^sub>R g x)" ``` lp15@66296 ` 101` ``` using \ to_g by (auto intro!: tendsto_sum tendsto_scaleR) ``` lp15@66296 ` 102` ``` then have "Cauchy (\n. \(x,K)\\. content K *\<^sub>R f n x)" ``` lp15@66296 ` 103` ``` by (meson convergent_eq_Cauchy) ``` lp15@66296 ` 104` ``` with e3 obtain M where ``` lp15@66296 ` 105` ``` M: "\m n. \m\M; n\M\ \ dist (\(x,K)\\. content K *\<^sub>R f m x) (\(x,K)\\. content K *\<^sub>R f n x) ``` lp15@66296 ` 106` ``` < e/3" ``` lp15@66296 ` 107` ``` unfolding Cauchy_def by blast ``` lp15@66296 ` 108` ``` have "\m n. \m\M; n\M; ``` lp15@66296 ` 109` ``` dist (\(x,K)\\. content K *\<^sub>R f m x) (\(x,K)\\. content K *\<^sub>R f n x) < e/3\ ``` lp15@66296 ` 110` ``` \ dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e" ``` lp15@66296 ` 111` ``` by (metis \T dist_commute dist_triangle_third [OF _ _ \T]) ``` lp15@66296 ` 112` ``` then show "\M. \m\M. \n\M. dist (integral (cbox a b) (f m)) (integral (cbox a b) (f n)) < e" ``` lp15@66296 ` 113` ``` using M by auto ``` lp15@66296 ` 114` ``` qed ``` lp15@66296 ` 115` ``` then obtain L where L: "(\n. integral (cbox a b) (f n)) \ L" ``` lp15@66296 ` 116` ``` by (meson convergent_eq_Cauchy) ``` lp15@66296 ` 117` ``` have "(g has_integral L) (cbox a b)" ``` lp15@66296 ` 118` ``` proof (clarsimp simp: has_integral) ``` lp15@66296 ` 119` ``` fix e::real assume "0 < e" ``` lp15@66296 ` 120` ``` then have e2: "0 < e/2" ``` lp15@66296 ` 121` ``` by simp ``` lp15@66296 ` 122` ``` then obtain \ where "gauge \" ``` lp15@66296 ` 123` ``` and \: "\n \. \\ tagged_division_of cbox a b; \ fine \\ ``` lp15@66296 ` 124` ``` \ norm((\(x,K)\\. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) < e/2" ``` lp15@66296 ` 125` ``` using feq unfolding equiintegrable_on_def ``` lp15@66296 ` 126` ``` by (meson image_eqI iso_tuple_UNIV_I) ``` lp15@66296 ` 127` ``` moreover ``` lp15@66296 ` 128` ``` have "norm ((\(x,K)\\. content K *\<^sub>R g x) - L) < e" ``` lp15@66296 ` 129` ``` if "\ tagged_division_of cbox a b" "\ fine \" for \ ``` lp15@66296 ` 130` ``` proof - ``` lp15@66296 ` 131` ``` have "norm ((\(x,K)\\. content K *\<^sub>R g x) - L) \ e/2" ``` lp15@66296 ` 132` ``` proof (rule Lim_norm_ubound) ``` lp15@66296 ` 133` ``` show "(\n. (\(x,K)\\. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) \ (\(x,K)\\. content K *\<^sub>R g x) - L" ``` lp15@66296 ` 134` ``` using to_g that L ``` lp15@66296 ` 135` ``` by (intro tendsto_diff tendsto_sum) (auto simp: tag_in_interval tendsto_scaleR) ``` lp15@66296 ` 136` ``` show "\\<^sub>F n in sequentially. ``` lp15@66296 ` 137` ``` norm ((\(x,K) \ \. content K *\<^sub>R f n x) - integral (cbox a b) (f n)) \ e/2" ``` lp15@66296 ` 138` ``` by (intro eventuallyI less_imp_le \ that) ``` lp15@66296 ` 139` ``` qed auto ``` lp15@66296 ` 140` ``` with \0 < e\ show ?thesis ``` lp15@66296 ` 141` ``` by linarith ``` lp15@66296 ` 142` ``` qed ``` lp15@66296 ` 143` ``` ultimately ``` lp15@66296 ` 144` ``` show "\\. gauge \ \ ``` lp15@66296 ` 145` ``` (\\. \ tagged_division_of cbox a b \ \ fine \ \ ``` lp15@66296 ` 146` ``` norm ((\(x,K)\\. content K *\<^sub>R g x) - L) < e)" ``` lp15@66296 ` 147` ``` by meson ``` lp15@66296 ` 148` ``` qed ``` lp15@66296 ` 149` ``` with L show ?thesis ``` lp15@66296 ` 150` ``` by (simp add: \(\n. integral (cbox a b) (f n)) \ L\ has_integral_integrable_integral) ``` lp15@66296 ` 151` ```qed ``` lp15@66296 ` 152` lp15@66296 ` 153` immler@69681 ` 154` ```lemma equiintegrable_reflect: ``` lp15@66296 ` 155` ``` assumes "F equiintegrable_on cbox a b" ``` lp15@66296 ` 156` ``` shows "(\f. f \ uminus) ` F equiintegrable_on cbox (-b) (-a)" ``` immler@69681 ` 157` ```proof - ``` lp15@66296 ` 158` ``` have "\\. gauge \ \ ``` lp15@66296 ` 159` ``` (\f \. f \ (\f. f \ uminus) ` F \ \ tagged_division_of cbox (- b) (- a) \ \ fine \ \ ``` lp15@66296 ` 160` ``` norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral (cbox (- b) (- a)) f) < e)" ``` lp15@66296 ` 161` ``` if "gauge \" and ``` lp15@66296 ` 162` ``` \: "\f \. \f \ F; \ tagged_division_of cbox a b; \ fine \\ \ ``` lp15@66296 ` 163` ``` norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral (cbox a b) f) < e" for e \ ``` lp15@66296 ` 164` ``` proof (intro exI, safe) ``` lp15@66296 ` 165` ``` show "gauge (\x. uminus ` \ (-x))" ``` lp15@66296 ` 166` ``` by (metis \gauge \\ gauge_reflect) ``` lp15@66296 ` 167` ``` show "norm ((\(x,K) \ \. content K *\<^sub>R (f \ uminus) x) - integral (cbox (- b) (- a)) (f \ uminus)) < e" ``` lp15@66296 ` 168` ``` if "f \ F" and tag: "\ tagged_division_of cbox (- b) (- a)" ``` lp15@66296 ` 169` ``` and fine: "(\x. uminus ` \ (- x)) fine \" for f \ ``` lp15@66296 ` 170` ``` proof - ``` lp15@66296 ` 171` ``` have 1: "(\(x,K). (- x, uminus ` K)) ` \ tagged_partial_division_of cbox a b" ``` lp15@66296 ` 172` ``` if "\ tagged_partial_division_of cbox (- b) (- a)" ``` lp15@66296 ` 173` ``` proof - ``` lp15@66296 ` 174` ``` have "- y \ cbox a b" ``` lp15@66296 ` 175` ``` if "\x K. (x,K) \ \ \ x \ K \ K \ cbox (- b) (- a) \ (\a b. K = cbox a b)" ``` lp15@66296 ` 176` ``` "(x, Y) \ \" "y \ Y" for x Y y ``` lp15@66296 ` 177` ``` proof - ``` lp15@66296 ` 178` ``` have "y \ uminus ` cbox a b" ``` lp15@66296 ` 179` ``` using that by auto ``` lp15@66296 ` 180` ``` then show "- y \ cbox a b" ``` lp15@66296 ` 181` ``` by force ``` lp15@66296 ` 182` ``` qed ``` lp15@66296 ` 183` ``` with that show ?thesis ``` lp15@66296 ` 184` ``` by (fastforce simp: tagged_partial_division_of_def interior_negations image_iff) ``` lp15@66296 ` 185` ``` qed ``` lp15@66296 ` 186` ``` have 2: "\K. (\x. (x,K) \ (\(x,K). (- x, uminus ` K)) ` \) \ x \ K" ``` lp15@66296 ` 187` ``` if "\{K. \x. (x,K) \ \} = cbox (- b) (- a)" "x \ cbox a b" for x ``` lp15@66296 ` 188` ``` proof - ``` lp15@66296 ` 189` ``` have xm: "x \ uminus ` \{A. \a. (a, A) \ \}" ``` lp15@66296 ` 190` ``` by (simp add: that) ``` lp15@66296 ` 191` ``` then obtain a X where "-x \ X" "(a, X) \ \" ``` lp15@66296 ` 192` ``` by auto ``` lp15@66296 ` 193` ``` then show ?thesis ``` lp15@66296 ` 194` ``` by (metis (no_types, lifting) add.inverse_inverse image_iff pair_imageI) ``` lp15@66296 ` 195` ``` qed ``` lp15@66296 ` 196` ``` have 3: "\x X y. \\ tagged_partial_division_of cbox (- b) (- a); (x, X) \ \; y \ X\ \ - y \ cbox a b" ``` lp15@66296 ` 197` ``` by (metis (no_types, lifting) equation_minus_iff imageE subsetD tagged_partial_division_ofD(3) uminus_interval_vector) ``` lp15@66296 ` 198` ``` have tag': "(\(x,K). (- x, uminus ` K)) ` \ tagged_division_of cbox a b" ``` lp15@66296 ` 199` ``` using tag by (auto simp: tagged_division_of_def dest: 1 2 3) ``` lp15@66296 ` 200` ``` have fine': "\ fine (\(x,K). (- x, uminus ` K)) ` \" ``` lp15@66296 ` 201` ``` using fine by (fastforce simp: fine_def) ``` lp15@66296 ` 202` ``` have inj: "inj_on (\(x,K). (- x, uminus ` K)) \" ``` lp15@66296 ` 203` ``` unfolding inj_on_def by force ``` lp15@66296 ` 204` ``` have eq: "content (uminus ` I) = content I" ``` lp15@66296 ` 205` ``` if I: "(x, I) \ \" and fnz: "f (- x) \ 0" for x I ``` lp15@66296 ` 206` ``` proof - ``` lp15@66296 ` 207` ``` obtain a b where "I = cbox a b" ``` lp15@66296 ` 208` ``` using tag I that by (force simp: tagged_division_of_def tagged_partial_division_of_def) ``` lp15@66296 ` 209` ``` then show ?thesis ``` lp15@66296 ` 210` ``` using content_image_affinity_cbox [of "-1" 0] by auto ``` lp15@66296 ` 211` ``` qed ``` lp15@66296 ` 212` ``` have "(\(x,K) \ (\(x,K). (- x, uminus ` K)) ` \. content K *\<^sub>R f x) = ``` lp15@66296 ` 213` ``` (\(x,K) \ \. content K *\<^sub>R f (- x))" ``` lp15@66296 ` 214` ``` apply (simp add: sum.reindex [OF inj]) ``` lp15@66296 ` 215` ``` apply (auto simp: eq intro!: sum.cong) ``` lp15@66296 ` 216` ``` done ``` lp15@66296 ` 217` ``` then show ?thesis ``` lp15@66296 ` 218` ``` using \ [OF \f \ F\ tag' fine'] integral_reflect ``` lp15@66296 ` 219` ``` by (metis (mono_tags, lifting) Henstock_Kurzweil_Integration.integral_cong comp_apply split_def sum.cong) ``` lp15@66296 ` 220` ``` qed ``` lp15@66296 ` 221` ``` qed ``` lp15@66296 ` 222` ``` then show ?thesis ``` lp15@66552 ` 223` ``` using assms ``` lp15@66552 ` 224` ``` apply (auto simp: equiintegrable_on_def) ``` lp15@66552 ` 225` ``` apply (rule integrable_eq) ``` lp15@66552 ` 226` ``` by auto ``` lp15@66296 ` 227` ```qed ``` lp15@66296 ` 228` immler@69683 ` 229` ```subsection\Subinterval restrictions for equiintegrable families\ ``` lp15@66296 ` 230` lp15@66296 ` 231` ```text\First, some technical lemmas about minimizing a "flat" part of a sum over a division.\ ``` lp15@66296 ` 232` lp15@66296 ` 233` ```lemma lemma0: ``` lp15@66296 ` 234` ``` assumes "i \ Basis" ``` lp15@66296 ` 235` ``` shows "content (cbox u v) / (interval_upperbound (cbox u v) \ i - interval_lowerbound (cbox u v) \ i) = ``` lp15@66296 ` 236` ``` (if content (cbox u v) = 0 then 0 ``` lp15@66296 ` 237` ``` else \j \ Basis - {i}. interval_upperbound (cbox u v) \ j - interval_lowerbound (cbox u v) \ j)" ``` lp15@66296 ` 238` ```proof (cases "content (cbox u v) = 0") ``` lp15@66296 ` 239` ``` case True ``` lp15@66296 ` 240` ``` then show ?thesis by simp ``` lp15@66296 ` 241` ```next ``` lp15@66296 ` 242` ``` case False ``` lp15@66296 ` 243` ``` then show ?thesis ``` lp15@66296 ` 244` ``` using prod.subset_diff [of "{i}" Basis] assms ``` lp15@66296 ` 245` ``` by (force simp: content_cbox_if divide_simps split: if_split_asm) ``` lp15@66296 ` 246` ```qed ``` lp15@66296 ` 247` lp15@66296 ` 248` immler@69681 ` 249` ```lemma content_division_lemma1: ``` lp15@66296 ` 250` ``` assumes div: "\ division_of S" and S: "S \ cbox a b" and i: "i \ Basis" ``` lp15@66296 ` 251` ``` and mt: "\K. K \ \ \ content K \ 0" ``` lp15@66296 ` 252` ``` and disj: "(\K \ \. K \ {x. x \ i = a \ i} \ {}) \ (\K \ \. K \ {x. x \ i = b \ i} \ {})" ``` lp15@66296 ` 253` ``` shows "(b \ i - a \ i) * (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) ``` lp15@66296 ` 254` ``` \ content(cbox a b)" (is "?lhs \ ?rhs") ``` immler@69681 ` 255` ```proof - ``` lp15@66296 ` 256` ``` have "finite \" ``` lp15@66296 ` 257` ``` using div by blast ``` lp15@66296 ` 258` ``` define extend where ``` lp15@66296 ` 259` ``` "extend \ \K. cbox (\j \ Basis. if j = i then (a \ i) *\<^sub>R i else (interval_lowerbound K \ j) *\<^sub>R j) ``` lp15@66296 ` 260` ``` (\j \ Basis. if j = i then (b \ i) *\<^sub>R i else (interval_upperbound K \ j) *\<^sub>R j)" ``` lp15@66296 ` 261` ``` have div_subset_cbox: "\K. K \ \ \ K \ cbox a b" ``` lp15@66296 ` 262` ``` using S div by auto ``` lp15@66296 ` 263` ``` have "\K. K \ \ \ K \ {}" ``` lp15@66296 ` 264` ``` using div by blast ``` lp15@66296 ` 265` ``` have extend: "extend K \ {}" "extend K \ cbox a b" if K: "K \ \" for K ``` lp15@66296 ` 266` ``` proof - ``` lp15@66296 ` 267` ``` obtain u v where K: "K = cbox u v" "K \ {}" "K \ cbox a b" ``` lp15@66296 ` 268` ``` using K cbox_division_memE [OF _ div] by (meson div_subset_cbox) ``` lp15@66296 ` 269` ``` with i show "extend K \ {}" "extend K \ cbox a b" ``` lp15@66296 ` 270` ``` apply (auto simp: extend_def subset_box box_ne_empty sum_if_inner) ``` lp15@66296 ` 271` ``` by fastforce ``` lp15@66296 ` 272` ``` qed ``` lp15@66296 ` 273` ``` have int_extend_disjoint: ``` lp15@66296 ` 274` ``` "interior(extend K1) \ interior(extend K2) = {}" if K: "K1 \ \" "K2 \ \" "K1 \ K2" for K1 K2 ``` lp15@66296 ` 275` ``` proof - ``` lp15@66296 ` 276` ``` obtain u v where K1: "K1 = cbox u v" "K1 \ {}" "K1 \ cbox a b" ``` lp15@66296 ` 277` ``` using K cbox_division_memE [OF _ div] by (meson div_subset_cbox) ``` lp15@66296 ` 278` ``` obtain w z where K2: "K2 = cbox w z" "K2 \ {}" "K2 \ cbox a b" ``` lp15@66296 ` 279` ``` using K cbox_division_memE [OF _ div] by (meson div_subset_cbox) ``` lp15@66296 ` 280` ``` have cboxes: "cbox u v \ \" "cbox w z \ \" "cbox u v \ cbox w z" ``` lp15@66296 ` 281` ``` using K1 K2 that by auto ``` lp15@66296 ` 282` ``` with div have "interior (cbox u v) \ interior (cbox w z) = {}" ``` lp15@66296 ` 283` ``` by blast ``` lp15@66296 ` 284` ``` moreover ``` lp15@66296 ` 285` ``` have "\x. x \ box u v \ x \ box w z" ``` lp15@66296 ` 286` ``` if "x \ interior (extend K1)" "x \ interior (extend K2)" for x ``` lp15@66296 ` 287` ``` proof - ``` lp15@66296 ` 288` ``` have "a \ i < x \ i" "x \ i < b \ i" ``` lp15@66296 ` 289` ``` and ux: "\k. k \ Basis - {i} \ u \ k < x \ k" ``` lp15@66296 ` 290` ``` and xv: "\k. k \ Basis - {i} \ x \ k < v \ k" ``` lp15@66296 ` 291` ``` and wx: "\k. k \ Basis - {i} \ w \ k < x \ k" ``` lp15@66296 ` 292` ``` and xz: "\k. k \ Basis - {i} \ x \ k < z \ k" ``` lp15@66296 ` 293` ``` using that K1 K2 i by (auto simp: extend_def box_ne_empty sum_if_inner mem_box) ``` lp15@66296 ` 294` ``` have "box u v \ {}" "box w z \ {}" ``` lp15@66296 ` 295` ``` using cboxes interior_cbox by (auto simp: content_eq_0_interior dest: mt) ``` lp15@66296 ` 296` ``` then obtain q s ``` lp15@66296 ` 297` ``` where q: "\k. k \ Basis \ w \ k < q \ k \ q \ k < z \ k" ``` lp15@66296 ` 298` ``` and s: "\k. k \ Basis \ u \ k < s \ k \ s \ k < v \ k" ``` lp15@66296 ` 299` ``` by (meson all_not_in_conv mem_box(1)) ``` lp15@66296 ` 300` ``` show ?thesis using disj ``` lp15@66296 ` 301` ``` proof ``` lp15@66296 ` 302` ``` assume "\K\\. K \ {x. x \ i = a \ i} \ {}" ``` lp15@66296 ` 303` ``` then have uva: "(cbox u v) \ {x. x \ i = a \ i} \ {}" ``` lp15@66296 ` 304` ``` and wza: "(cbox w z) \ {x. x \ i = a \ i} \ {}" ``` lp15@66296 ` 305` ``` using cboxes by (auto simp: content_eq_0_interior) ``` lp15@66296 ` 306` ``` then obtain r t where "r \ i = a \ i" and r: "\k. k \ Basis \ w \ k \ r \ k \ r \ k \ z \ k" ``` lp15@66296 ` 307` ``` and "t \ i = a \ i" and t: "\k. k \ Basis \ u \ k \ t \ k \ t \ k \ v \ k" ``` lp15@66296 ` 308` ``` by (fastforce simp: mem_box) ``` lp15@66296 ` 309` ``` have u: "u \ i < q \ i" ``` lp15@66296 ` 310` ``` using i K2(1) K2(3) \t \ i = a \ i\ q s t [OF i] by (force simp: subset_box) ``` lp15@66296 ` 311` ``` have w: "w \ i < s \ i" ``` lp15@66296 ` 312` ``` using i K1(1) K1(3) \r \ i = a \ i\ s r [OF i] by (force simp: subset_box) ``` lp15@66296 ` 313` ``` let ?x = "(\j \ Basis. if j = i then min (q \ i) (s \ i) *\<^sub>R i else (x \ j) *\<^sub>R j)" ``` lp15@66296 ` 314` ``` show ?thesis ``` lp15@66296 ` 315` ``` proof (intro exI conjI) ``` lp15@66296 ` 316` ``` show "?x \ box u v" ``` lp15@66296 ` 317` ``` using \i \ Basis\ s apply (clarsimp simp: mem_box) ``` lp15@66296 ` 318` ``` apply (subst sum_if_inner; simp)+ ``` lp15@66296 ` 319` ``` apply (fastforce simp: u ux xv) ``` lp15@66296 ` 320` ``` done ``` lp15@66296 ` 321` ``` show "?x \ box w z" ``` lp15@66296 ` 322` ``` using \i \ Basis\ q apply (clarsimp simp: mem_box) ``` lp15@66296 ` 323` ``` apply (subst sum_if_inner; simp)+ ``` lp15@66296 ` 324` ``` apply (fastforce simp: w wx xz) ``` lp15@66296 ` 325` ``` done ``` lp15@66296 ` 326` ``` qed ``` lp15@66296 ` 327` ``` next ``` lp15@66296 ` 328` ``` assume "\K\\. K \ {x. x \ i = b \ i} \ {}" ``` lp15@66296 ` 329` ``` then have uva: "(cbox u v) \ {x. x \ i = b \ i} \ {}" ``` lp15@66296 ` 330` ``` and wza: "(cbox w z) \ {x. x \ i = b \ i} \ {}" ``` lp15@66296 ` 331` ``` using cboxes by (auto simp: content_eq_0_interior) ``` lp15@66296 ` 332` ``` then obtain r t where "r \ i = b \ i" and r: "\k. k \ Basis \ w \ k \ r \ k \ r \ k \ z \ k" ``` lp15@66296 ` 333` ``` and "t \ i = b \ i" and t: "\k. k \ Basis \ u \ k \ t \ k \ t \ k \ v \ k" ``` lp15@66296 ` 334` ``` by (fastforce simp: mem_box) ``` lp15@66296 ` 335` ``` have z: "s \ i < z \ i" ``` lp15@66296 ` 336` ``` using K1(1) K1(3) \r \ i = b \ i\ r [OF i] i s by (force simp: subset_box) ``` lp15@66296 ` 337` ``` have v: "q \ i < v \ i" ``` lp15@66296 ` 338` ``` using K2(1) K2(3) \t \ i = b \ i\ t [OF i] i q by (force simp: subset_box) ``` lp15@66296 ` 339` ``` let ?x = "(\j \ Basis. if j = i then max (q \ i) (s \ i) *\<^sub>R i else (x \ j) *\<^sub>R j)" ``` lp15@66296 ` 340` ``` show ?thesis ``` lp15@66296 ` 341` ``` proof (intro exI conjI) ``` lp15@66296 ` 342` ``` show "?x \ box u v" ``` lp15@66296 ` 343` ``` using \i \ Basis\ s apply (clarsimp simp: mem_box) ``` lp15@66296 ` 344` ``` apply (subst sum_if_inner; simp)+ ``` lp15@66296 ` 345` ``` apply (fastforce simp: v ux xv) ``` lp15@66296 ` 346` ``` done ``` lp15@66296 ` 347` ``` show "?x \ box w z" ``` lp15@66296 ` 348` ``` using \i \ Basis\ q apply (clarsimp simp: mem_box) ``` lp15@66296 ` 349` ``` apply (subst sum_if_inner; simp)+ ``` lp15@66296 ` 350` ``` apply (fastforce simp: z wx xz) ``` lp15@66296 ` 351` ``` done ``` lp15@66296 ` 352` ``` qed ``` lp15@66296 ` 353` ``` qed ``` lp15@66296 ` 354` ``` qed ``` lp15@66296 ` 355` ``` ultimately show ?thesis by auto ``` lp15@66296 ` 356` ``` qed ``` lp15@66296 ` 357` ``` have "?lhs = (\K\\. (b \ i - a \ i) * content K / (interval_upperbound K \ i - interval_lowerbound K \ i))" ``` lp15@66296 ` 358` ``` by (simp add: sum_distrib_left) ``` lp15@66296 ` 359` ``` also have "\ = sum (content \ extend) \" ``` lp15@66296 ` 360` ``` proof (rule sum.cong [OF refl]) ``` lp15@66296 ` 361` ``` fix K assume "K \ \" ``` lp15@66296 ` 362` ``` then obtain u v where K: "K = cbox u v" "cbox u v \ {}" "K \ cbox a b" ``` lp15@66296 ` 363` ``` using cbox_division_memE [OF _ div] div_subset_cbox by metis ``` lp15@66296 ` 364` ``` then have uv: "u \ i < v \ i" ``` lp15@66296 ` 365` ``` using mt [OF \K \ \\] \i \ Basis\ content_eq_0 by fastforce ``` lp15@66296 ` 366` ``` have "insert i (Basis \ -{i}) = Basis" ``` lp15@66296 ` 367` ``` using \i \ Basis\ by auto ``` lp15@66296 ` 368` ``` then have "(b \ i - a \ i) * content K / (interval_upperbound K \ i - interval_lowerbound K \ i) ``` lp15@66296 ` 369` ``` = (b \ i - a \ i) * (\i \ insert i (Basis \ -{i}). v \ i - u \ i) / (interval_upperbound (cbox u v) \ i - interval_lowerbound (cbox u v) \ i)" ``` lp15@66296 ` 370` ``` using K box_ne_empty(1) content_cbox by fastforce ``` lp15@66296 ` 371` ``` also have "... = (\x\Basis. if x = i then b \ x - a \ x ``` lp15@66296 ` 372` ``` else (interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) \ x)" ``` lp15@66296 ` 373` ``` using \i \ Basis\ K uv by (simp add: prod.If_cases) (simp add: algebra_simps) ``` lp15@66296 ` 374` ``` also have "... = (\k\Basis. ``` lp15@66296 ` 375` ``` (\j\Basis. if j = i then (b \ i - a \ i) *\<^sub>R i else ((interval_upperbound (cbox u v) - interval_lowerbound (cbox u v)) \ j) *\<^sub>R j) \ k)" ``` lp15@66296 ` 376` ``` using \i \ Basis\ by (subst prod.cong [OF refl sum_if_inner]; simp) ``` lp15@66296 ` 377` ``` also have "... = (\k\Basis. ``` lp15@66296 ` 378` ``` (\j\Basis. if j = i then (b \ i) *\<^sub>R i else (interval_upperbound (cbox u v) \ j) *\<^sub>R j) \ k - ``` lp15@66296 ` 379` ``` (\j\Basis. if j = i then (a \ i) *\<^sub>R i else (interval_lowerbound (cbox u v) \ j) *\<^sub>R j) \ k)" ``` lp15@66296 ` 380` ``` apply (rule prod.cong [OF refl]) ``` lp15@66296 ` 381` ``` using \i \ Basis\ ``` lp15@66296 ` 382` ``` apply (subst sum_if_inner; simp add: algebra_simps)+ ``` lp15@66296 ` 383` ``` done ``` lp15@66296 ` 384` ``` also have "... = (content \ extend) K" ``` lp15@66296 ` 385` ``` using \i \ Basis\ K box_ne_empty ``` lp15@66296 ` 386` ``` apply (simp add: extend_def) ``` lp15@66296 ` 387` ``` apply (subst content_cbox, auto) ``` lp15@66296 ` 388` ``` done ``` lp15@66296 ` 389` ``` finally show "(b \ i - a \ i) * content K / (interval_upperbound K \ i - interval_lowerbound K \ i) ``` lp15@66296 ` 390` ``` = (content \ extend) K" . ``` lp15@66296 ` 391` ``` qed ``` lp15@66296 ` 392` ``` also have "... = sum content (extend ` \)" ``` lp15@66296 ` 393` ``` proof - ``` lp15@66296 ` 394` ``` have "\K1 \ \; K2 \ \; K1 \ K2; extend K1 = extend K2\ \ content (extend K1) = 0" for K1 K2 ``` lp15@66296 ` 395` ``` using int_extend_disjoint [of K1 K2] extend_def by (simp add: content_eq_0_interior) ``` lp15@66296 ` 396` ``` then show ?thesis ``` lp15@66296 ` 397` ``` by (simp add: comm_monoid_add_class.sum.reindex_nontrivial [OF \finite \\]) ``` lp15@66296 ` 398` ``` qed ``` lp15@66296 ` 399` ``` also have "... \ ?rhs" ``` lp15@66296 ` 400` ``` proof (rule subadditive_content_division) ``` haftmann@69325 ` 401` ``` show "extend ` \ division_of \ (extend ` \)" ``` lp15@66296 ` 402` ``` using int_extend_disjoint apply (auto simp: division_of_def \finite \\ extend) ``` lp15@66296 ` 403` ``` using extend_def apply blast ``` lp15@66296 ` 404` ``` done ``` haftmann@69325 ` 405` ``` show "\ (extend ` \) \ cbox a b" ``` lp15@66296 ` 406` ``` using extend by fastforce ``` lp15@66296 ` 407` ``` qed ``` lp15@66296 ` 408` ``` finally show ?thesis . ``` lp15@66296 ` 409` ```qed ``` lp15@66296 ` 410` lp15@66296 ` 411` immler@69681 ` 412` ```proposition sum_content_area_over_thin_division: ``` lp15@66296 ` 413` ``` assumes div: "\ division_of S" and S: "S \ cbox a b" and i: "i \ Basis" ``` lp15@66296 ` 414` ``` and "a \ i \ c" "c \ b \ i" ``` lp15@66296 ` 415` ``` and nonmt: "\K. K \ \ \ K \ {x. x \ i = c} \ {}" ``` lp15@66296 ` 416` ``` shows "(b \ i - a \ i) * (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) ``` lp15@66296 ` 417` ``` \ 2 * content(cbox a b)" ``` immler@69681 ` 418` ```proof (cases "content(cbox a b) = 0") ``` lp15@66296 ` 419` ``` case True ``` lp15@66296 ` 420` ``` have "(\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) = 0" ``` lp15@66296 ` 421` ``` using S div by (force intro!: sum.neutral content_0_subset [OF True]) ``` lp15@66296 ` 422` ``` then show ?thesis ``` lp15@66296 ` 423` ``` by (auto simp: True) ``` lp15@66296 ` 424` ```next ``` lp15@66296 ` 425` ``` case False ``` lp15@66296 ` 426` ``` then have "content(cbox a b) > 0" ``` lp15@66296 ` 427` ``` using zero_less_measure_iff by blast ``` lp15@66296 ` 428` ``` then have "a \ i < b \ i" if "i \ Basis" for i ``` lp15@66296 ` 429` ``` using content_pos_lt_eq that by blast ``` lp15@66296 ` 430` ``` have "finite \" ``` lp15@66296 ` 431` ``` using div by blast ``` lp15@66296 ` 432` ``` define Dlec where "Dlec \ {L \ (\L. L \ {x. x \ i \ c}) ` \. content L \ 0}" ``` lp15@66296 ` 433` ``` define Dgec where "Dgec \ {L \ (\L. L \ {x. x \ i \ c}) ` \. content L \ 0}" ``` lp15@66296 ` 434` ``` define a' where "a' \ (\j\Basis. (if j = i then c else a \ j) *\<^sub>R j)" ``` lp15@66296 ` 435` ``` define b' where "b' \ (\j\Basis. (if j = i then c else b \ j) *\<^sub>R j)" ``` lp15@66296 ` 436` ``` have Dlec_cbox: "\K. K \ Dlec \ \a b. K = cbox a b" ``` lp15@66296 ` 437` ``` using interval_split [OF i] div by (fastforce simp: Dlec_def division_of_def) ``` lp15@66296 ` 438` ``` then have lec_is_cbox: "\content (L \ {x. x \ i \ c}) \ 0; L \ \\ \ \a b. L \ {x. x \ i \ c} = cbox a b" for L ``` lp15@66296 ` 439` ``` using Dlec_def by blast ``` lp15@66296 ` 440` ``` have Dgec_cbox: "\K. K \ Dgec \ \a b. K = cbox a b" ``` lp15@66296 ` 441` ``` using interval_split [OF i] div by (fastforce simp: Dgec_def division_of_def) ``` lp15@66296 ` 442` ``` then have gec_is_cbox: "\content (L \ {x. x \ i \ c}) \ 0; L \ \\ \ \a b. L \ {x. x \ i \ c} = cbox a b" for L ``` lp15@66296 ` 443` ``` using Dgec_def by blast ``` lp15@66296 ` 444` ``` have "(b' \ i - a \ i) * (\K\Dlec. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ content(cbox a b')" ``` lp15@66296 ` 445` ``` proof (rule content_division_lemma1) ``` lp15@66296 ` 446` ``` show "Dlec division_of \Dlec" ``` lp15@66296 ` 447` ``` unfolding division_of_def ``` lp15@66296 ` 448` ``` proof (intro conjI ballI Dlec_cbox) ``` lp15@66296 ` 449` ``` show "\K1 K2. \K1 \ Dlec; K2 \ Dlec\ \ K1 \ K2 \ interior K1 \ interior K2 = {}" ``` lp15@66296 ` 450` ``` by (clarsimp simp: Dlec_def) (use div in auto) ``` lp15@66296 ` 451` ``` qed (use \finite \\ Dlec_def in auto) ``` lp15@66296 ` 452` ``` show "\Dlec \ cbox a b'" ``` lp15@66296 ` 453` ``` using Dlec_def div S by (auto simp: b'_def division_of_def mem_box) ``` lp15@66296 ` 454` ``` show "(\K\Dlec. K \ {x. x \ i = a \ i} \ {}) \ (\K\Dlec. K \ {x. x \ i = b' \ i} \ {})" ``` lp15@66296 ` 455` ``` using nonmt by (fastforce simp: Dlec_def b'_def sum_if_inner i) ``` lp15@66296 ` 456` ``` qed (use i Dlec_def in auto) ``` lp15@66296 ` 457` ``` moreover ``` lp15@66296 ` 458` ``` have "(\K\Dlec. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) = ``` lp15@66296 ` 459` ``` (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K)" ``` lp15@66296 ` 460` ``` apply (subst sum.reindex_nontrivial [OF \finite \\, symmetric], simp) ``` lp15@66296 ` 461` ``` apply (metis division_split_left_inj [OF div] lec_is_cbox content_eq_0_interior) ``` lp15@66296 ` 462` ``` unfolding Dlec_def using \finite \\ apply (auto simp: sum.mono_neutral_left) ``` lp15@66296 ` 463` ``` done ``` lp15@66296 ` 464` ``` moreover have "(b' \ i - a \ i) = (c - a \ i)" ``` lp15@66296 ` 465` ``` by (simp add: b'_def sum_if_inner i) ``` lp15@66296 ` 466` ``` ultimately ``` lp15@66296 ` 467` ``` have lec: "(c - a \ i) * (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) ``` lp15@66296 ` 468` ``` \ content(cbox a b')" ``` lp15@66296 ` 469` ``` by simp ``` lp15@66296 ` 470` lp15@66296 ` 471` ``` have "(b \ i - a' \ i) * (\K\Dgec. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ content(cbox a' b)" ``` lp15@66296 ` 472` ``` proof (rule content_division_lemma1) ``` lp15@66296 ` 473` ``` show "Dgec division_of \Dgec" ``` lp15@66296 ` 474` ``` unfolding division_of_def ``` lp15@66296 ` 475` ``` proof (intro conjI ballI Dgec_cbox) ``` lp15@66296 ` 476` ``` show "\K1 K2. \K1 \ Dgec; K2 \ Dgec\ \ K1 \ K2 \ interior K1 \ interior K2 = {}" ``` lp15@66296 ` 477` ``` by (clarsimp simp: Dgec_def) (use div in auto) ``` lp15@66296 ` 478` ``` qed (use \finite \\ Dgec_def in auto) ``` lp15@66296 ` 479` ``` show "\Dgec \ cbox a' b" ``` lp15@66296 ` 480` ``` using Dgec_def div S by (auto simp: a'_def division_of_def mem_box) ``` lp15@66296 ` 481` ``` show "(\K\Dgec. K \ {x. x \ i = a' \ i} \ {}) \ (\K\Dgec. K \ {x. x \ i = b \ i} \ {})" ``` lp15@66296 ` 482` ``` using nonmt by (fastforce simp: Dgec_def a'_def sum_if_inner i) ``` lp15@66296 ` 483` ``` qed (use i Dgec_def in auto) ``` lp15@66296 ` 484` ``` moreover ``` lp15@66296 ` 485` ``` have "(\K\Dgec. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) = ``` lp15@66296 ` 486` ``` (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K)" ``` lp15@66296 ` 487` ``` apply (subst sum.reindex_nontrivial [OF \finite \\, symmetric], simp) ``` lp15@66296 ` 488` ``` apply (metis division_split_right_inj [OF div] gec_is_cbox content_eq_0_interior) ``` lp15@66296 ` 489` ``` unfolding Dgec_def using \finite \\ apply (auto simp: sum.mono_neutral_left) ``` lp15@66296 ` 490` ``` done ``` lp15@66296 ` 491` ``` moreover have "(b \ i - a' \ i) = (b \ i - c)" ``` lp15@66296 ` 492` ``` by (simp add: a'_def sum_if_inner i) ``` lp15@66296 ` 493` ``` ultimately ``` lp15@66296 ` 494` ``` have gec: "(b \ i - c) * (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) ``` lp15@66296 ` 495` ``` \ content(cbox a' b)" ``` lp15@66296 ` 496` ``` by simp ``` lp15@66296 ` 497` ``` show ?thesis ``` lp15@66296 ` 498` ``` proof (cases "c = a \ i \ c = b \ i") ``` lp15@66296 ` 499` ``` case True ``` lp15@66296 ` 500` ``` then show ?thesis ``` lp15@66296 ` 501` ``` proof ``` lp15@66296 ` 502` ``` assume c: "c = a \ i" ``` lp15@66296 ` 503` ``` then have "a' = a" ``` lp15@66296 ` 504` ``` apply (simp add: sum_if_inner i a'_def cong: if_cong) ``` lp15@66296 ` 505` ``` using euclidean_representation [of a] sum.cong [OF refl, of Basis "\i. (a \ i) *\<^sub>R i"] by presburger ``` lp15@66296 ` 506` ``` then have "content (cbox a' b) \ 2 * content (cbox a b)" by simp ``` lp15@66296 ` 507` ``` moreover ``` lp15@66296 ` 508` ``` have eq: "(\K\\. content (K \ {x. a \ i \ x \ i}) / ``` lp15@66296 ` 509` ``` (interval_upperbound (K \ {x. a \ i \ x \ i}) \ i - interval_lowerbound (K \ {x. a \ i \ x \ i}) \ i)) ``` lp15@66296 ` 510` ``` = (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i))" ``` lp15@66296 ` 511` ``` (is "sum ?f _ = sum ?g _") ``` lp15@66296 ` 512` ``` proof (rule sum.cong [OF refl]) ``` lp15@66296 ` 513` ``` fix K assume "K \ \" ``` lp15@66296 ` 514` ``` then have "a \ i \ x \ i" if "x \ K" for x ``` lp15@66296 ` 515` ``` by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that) ``` lp15@66296 ` 516` ``` then have "K \ {x. a \ i \ x \ i} = K" ``` lp15@66296 ` 517` ``` by blast ``` lp15@66296 ` 518` ``` then show "?f K = ?g K" ``` lp15@66296 ` 519` ``` by simp ``` lp15@66296 ` 520` ``` qed ``` lp15@66296 ` 521` ``` ultimately show ?thesis ``` lp15@66296 ` 522` ``` using gec c eq by auto ``` lp15@66296 ` 523` ``` next ``` lp15@66296 ` 524` ``` assume c: "c = b \ i" ``` lp15@66296 ` 525` ``` then have "b' = b" ``` lp15@66296 ` 526` ``` apply (simp add: sum_if_inner i b'_def cong: if_cong) ``` lp15@66296 ` 527` ``` using euclidean_representation [of b] sum.cong [OF refl, of Basis "\i. (b \ i) *\<^sub>R i"] by presburger ``` lp15@66296 ` 528` ``` then have "content (cbox a b') \ 2 * content (cbox a b)" by simp ``` lp15@66296 ` 529` ``` moreover ``` lp15@66296 ` 530` ``` have eq: "(\K\\. content (K \ {x. x \ i \ b \ i}) / ``` lp15@66296 ` 531` ``` (interval_upperbound (K \ {x. x \ i \ b \ i}) \ i - interval_lowerbound (K \ {x. x \ i \ b \ i}) \ i)) ``` lp15@66296 ` 532` ``` = (\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i))" ``` lp15@66296 ` 533` ``` (is "sum ?f _ = sum ?g _") ``` lp15@66296 ` 534` ``` proof (rule sum.cong [OF refl]) ``` lp15@66296 ` 535` ``` fix K assume "K \ \" ``` lp15@66296 ` 536` ``` then have "x \ i \ b \ i" if "x \ K" for x ``` lp15@66296 ` 537` ``` by (metis S UnionI div division_ofD(6) i mem_box(2) subsetCE that) ``` lp15@66296 ` 538` ``` then have "K \ {x. x \ i \ b \ i} = K" ``` lp15@66296 ` 539` ``` by blast ``` lp15@66296 ` 540` ``` then show "?f K = ?g K" ``` lp15@66296 ` 541` ``` by simp ``` lp15@66296 ` 542` ``` qed ``` lp15@66296 ` 543` ``` ultimately show ?thesis ``` lp15@66296 ` 544` ``` using lec c eq by auto ``` lp15@66296 ` 545` ``` qed ``` lp15@66296 ` 546` ``` next ``` lp15@66296 ` 547` ``` case False ``` lp15@66296 ` 548` ``` have prod_if: "(\k\Basis \ - {i}. f k) = (\k\Basis. f k) / f i" if "f i \ (0::real)" for f ``` lp15@66296 ` 549` ``` using that mk_disjoint_insert [OF i] ``` lp15@66296 ` 550` ``` apply (clarsimp simp add: divide_simps) ``` lp15@66296 ` 551` ``` by (metis Int_insert_left_if0 finite_Basis finite_insert le_iff_inf mult.commute order_refl prod.insert subset_Compl_singleton) ``` lp15@66296 ` 552` ``` have abc: "a \ i < c" "c < b \ i" ``` lp15@66296 ` 553` ``` using False assms by auto ``` lp15@66296 ` 554` ``` then have "(\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) ``` lp15@66296 ` 555` ``` \ content(cbox a b') / (c - a \ i)" ``` lp15@66296 ` 556` ``` "(\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) ``` lp15@66296 ` 557` ``` \ content(cbox a' b) / (b \ i - c)" ``` lp15@66296 ` 558` ``` using lec gec by (simp_all add: divide_simps mult.commute) ``` lp15@66296 ` 559` ``` moreover ``` lp15@66296 ` 560` ``` have "(\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) ``` lp15@66296 ` 561` ``` \ (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K) + ``` lp15@66296 ` 562` ``` (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K)" ``` lp15@66296 ` 563` ``` (is "?lhs \ ?rhs") ``` lp15@66296 ` 564` ``` proof - ``` lp15@66296 ` 565` ``` have "?lhs \ ``` lp15@66296 ` 566` ``` (\K\\. ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K + ``` lp15@66296 ` 567` ``` ((\K. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ ((\K. K \ {x. x \ i \ c}))) K)" ``` lp15@66296 ` 568` ``` (is "sum ?f _ \ sum ?g _") ``` lp15@66296 ` 569` ``` proof (rule sum_mono) ``` lp15@66296 ` 570` ``` fix K assume "K \ \" ``` lp15@66296 ` 571` ``` then obtain u v where uv: "K = cbox u v" ``` lp15@66296 ` 572` ``` using div by blast ``` lp15@66296 ` 573` ``` obtain u' v' where uv': "cbox u v \ {x. x \ i \ c} = cbox u v'" ``` lp15@66296 ` 574` ``` "cbox u v \ {x. c \ x \ i} = cbox u' v" ``` lp15@66296 ` 575` ``` "\k. k \ Basis \ u' \ k = (if k = i then max (u \ i) c else u \ k)" ``` lp15@66296 ` 576` ``` "\k. k \ Basis \ v' \ k = (if k = i then min (v \ i) c else v \ k)" ``` lp15@66296 ` 577` ``` using i by (auto simp: interval_split) ``` lp15@66296 ` 578` ``` have *: "\content (cbox u v') = 0; content (cbox u' v) = 0\ \ content (cbox u v) = 0" ``` lp15@66296 ` 579` ``` "content (cbox u' v) \ 0 \ content (cbox u v) \ 0" ``` lp15@66296 ` 580` ``` "content (cbox u v') \ 0 \ content (cbox u v) \ 0" ``` lp15@66296 ` 581` ``` using i uv uv' by (auto simp: content_eq_0 le_max_iff_disj min_le_iff_disj split: if_split_asm intro: order_trans) ``` lp15@66296 ` 582` ``` show "?f K \ ?g K" ``` lp15@66296 ` 583` ``` using i uv uv' apply (clarsimp simp add: lemma0 * intro!: prod_nonneg) ``` lp15@66296 ` 584` ``` by (metis content_eq_0 le_less_linear order.strict_implies_order) ``` lp15@66296 ` 585` ``` qed ``` lp15@66296 ` 586` ``` also have "... = ?rhs" ``` lp15@66296 ` 587` ``` by (simp add: sum.distrib) ``` lp15@66296 ` 588` ``` finally show ?thesis . ``` lp15@66296 ` 589` ``` qed ``` lp15@66296 ` 590` ``` moreover have "content (cbox a b') / (c - a \ i) = content (cbox a b) / (b \ i - a \ i)" ``` lp15@66296 ` 591` ``` using i abc ``` lp15@66296 ` 592` ``` apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff) ``` lp15@66296 ` 593` ``` apply (auto simp: if_distrib if_distrib [of "\f. f x" for x] prod.If_cases [of Basis "\x. x = i", simplified] prod_if field_simps) ``` lp15@66296 ` 594` ``` done ``` lp15@66296 ` 595` ``` moreover have "content (cbox a' b) / (b \ i - c) = content (cbox a b) / (b \ i - a \ i)" ``` lp15@66296 ` 596` ``` using i abc ``` lp15@66296 ` 597` ``` apply (simp add: field_simps a'_def b'_def measure_lborel_cbox_eq inner_diff) ``` lp15@66296 ` 598` ``` apply (auto simp: if_distrib prod.If_cases [of Basis "\x. x = i", simplified] prod_if field_simps) ``` lp15@66296 ` 599` ``` done ``` lp15@66296 ` 600` ``` ultimately ``` lp15@66296 ` 601` ``` have "(\K\\. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) ``` lp15@66296 ` 602` ``` \ 2 * content (cbox a b) / (b \ i - a \ i)" ``` lp15@66296 ` 603` ``` by linarith ``` lp15@66296 ` 604` ``` then show ?thesis ``` lp15@66296 ` 605` ``` using abc by (simp add: divide_simps mult.commute) ``` lp15@66296 ` 606` ``` qed ``` lp15@66296 ` 607` ```qed ``` lp15@66296 ` 608` lp15@66296 ` 609` lp15@66296 ` 610` lp15@66296 ` 611` immler@69681 ` 612` ```proposition bounded_equiintegral_over_thin_tagged_partial_division: ``` lp15@66296 ` 613` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@66296 ` 614` ``` assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" and "0 < \" ``` lp15@66296 ` 615` ``` and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" ``` lp15@66296 ` 616` ``` obtains \ where "gauge \" ``` lp15@66296 ` 617` ``` "\c i S h. \c \ cbox a b; i \ Basis; S tagged_partial_division_of cbox a b; ``` lp15@66296 ` 618` ``` \ fine S; h \ F; \x K. (x,K) \ S \ (K \ {x. x \ i = c \ i} \ {})\ ``` lp15@66296 ` 619` ``` \ (\(x,K) \ S. norm (integral K h)) < \" ``` immler@69681 ` 620` ```proof (cases "content(cbox a b) = 0") ``` lp15@66296 ` 621` ``` case True ``` lp15@66296 ` 622` ``` show ?thesis ``` lp15@66296 ` 623` ``` proof ``` lp15@66296 ` 624` ``` show "gauge (\x. ball x 1)" ``` lp15@66296 ` 625` ``` by (simp add: gauge_trivial) ``` lp15@66296 ` 626` ``` show "(\(x,K) \ S. norm (integral K h)) < \" ``` lp15@66296 ` 627` ``` if "S tagged_partial_division_of cbox a b" "(\x. ball x 1) fine S" for S and h:: "'a \ 'b" ``` lp15@66296 ` 628` ``` proof - ``` lp15@66296 ` 629` ``` have "(\(x,K) \ S. norm (integral K h)) = 0" ``` lp15@66296 ` 630` ``` using that True content_0_subset ``` lp15@66296 ` 631` ``` by (fastforce simp: tagged_partial_division_of_def intro: sum.neutral) ``` lp15@66296 ` 632` ``` with \0 < \\ show ?thesis ``` lp15@66296 ` 633` ``` by simp ``` lp15@66296 ` 634` ``` qed ``` lp15@66296 ` 635` ``` qed ``` lp15@66296 ` 636` ```next ``` lp15@66296 ` 637` ``` case False ``` lp15@66296 ` 638` ``` then have contab_gt0: "content(cbox a b) > 0" ``` lp15@66296 ` 639` ``` by (simp add: zero_less_measure_iff) ``` lp15@66296 ` 640` ``` then have a_less_b: "\i. i \ Basis \ a\i < b\i" ``` lp15@66296 ` 641` ``` by (auto simp: content_pos_lt_eq) ``` lp15@66296 ` 642` ``` obtain \0 where "gauge \0" ``` lp15@66296 ` 643` ``` and \0: "\S h. \S tagged_partial_division_of cbox a b; \0 fine S; h \ F\ ``` lp15@66296 ` 644` ``` \ (\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) < \/2" ``` lp15@66296 ` 645` ``` proof - ``` lp15@66296 ` 646` ``` obtain \ where "gauge \" ``` lp15@66296 ` 647` ``` and \: "\f \. \f \ F; \ tagged_division_of cbox a b; \ fine \\ ``` lp15@66296 ` 648` ``` \ norm ((\(x,K) \ \. content K *\<^sub>R f x) - integral (cbox a b) f) ``` lp15@66296 ` 649` ``` < \/(5 * (Suc DIM('b)))" ``` lp15@66296 ` 650` ``` proof - ``` lp15@66296 ` 651` ``` have e5: "\/(5 * (Suc DIM('b))) > 0" ``` lp15@66296 ` 652` ``` using \\ > 0\ by auto ``` lp15@66296 ` 653` ``` then show ?thesis ``` lp15@66296 ` 654` ``` using F that by (auto simp: equiintegrable_on_def) ``` lp15@66296 ` 655` ``` qed ``` lp15@66296 ` 656` ``` show ?thesis ``` lp15@66296 ` 657` ``` proof ``` lp15@66296 ` 658` ``` show "gauge \" ``` lp15@66296 ` 659` ``` by (rule \gauge \\) ``` lp15@66296 ` 660` ``` show "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) < \/2" ``` lp15@66296 ` 661` ``` if "S tagged_partial_division_of cbox a b" "\ fine S" "h \ F" for S h ``` lp15@66296 ` 662` ``` proof - ``` lp15@66296 ` 663` ``` have "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) \ 2 * real DIM('b) * (\/(5 * Suc DIM('b)))" ``` lp15@66497 ` 664` ``` proof (rule Henstock_lemma_part2 [of h a b]) ``` lp15@66296 ` 665` ``` show "h integrable_on cbox a b" ``` lp15@66296 ` 666` ``` using that F equiintegrable_on_def by metis ``` lp15@66296 ` 667` ``` show "gauge \" ``` lp15@66296 ` 668` ``` by (rule \gauge \\) ``` lp15@66296 ` 669` ``` qed (use that \\ > 0\ \ in auto) ``` lp15@66296 ` 670` ``` also have "... < \/2" ``` lp15@66296 ` 671` ``` using \\ > 0\ by (simp add: divide_simps) ``` lp15@66296 ` 672` ``` finally show ?thesis . ``` lp15@66296 ` 673` ``` qed ``` lp15@66296 ` 674` ``` qed ``` lp15@66296 ` 675` ``` qed ``` lp15@66296 ` 676` ``` define \ where "\ \ \x. \0 x \ ``` haftmann@69260 ` 677` ``` ball x ((\/8 / (norm(f x) + 1)) * (INF m\Basis. b \ m - a \ m) / content(cbox a b))" ``` lp15@66296 ` 678` ``` have "gauge (\x. ball x ``` haftmann@69260 ` 679` ``` (\ * (INF m\Basis. b \ m - a \ m) / ((8 * norm (f x) + 8) * content (cbox a b))))" ``` lp15@66296 ` 680` ``` using \0 < content (cbox a b)\ \0 < \\ a_less_b ``` lp15@66296 ` 681` ``` apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff) ``` lp15@66296 ` 682` ``` apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral) ``` lp15@66296 ` 683` ``` done ``` lp15@66296 ` 684` ``` then have "gauge \" ``` lp15@66296 ` 685` ``` unfolding \_def using \gauge \0\ gauge_Int by auto ``` lp15@66296 ` 686` ``` moreover ``` lp15@66296 ` 687` ``` have "(\(x,K) \ S. norm (integral K h)) < \" ``` lp15@66296 ` 688` ``` if "c \ cbox a b" "i \ Basis" and S: "S tagged_partial_division_of cbox a b" ``` lp15@66296 ` 689` ``` and "\ fine S" "h \ F" and ne: "\x K. (x,K) \ S \ K \ {x. x \ i = c \ i} \ {}" for c i S h ``` lp15@66296 ` 690` ``` proof - ``` lp15@66296 ` 691` ``` have "cbox c b \ cbox a b" ``` lp15@66296 ` 692` ``` by (meson mem_box(2) order_refl subset_box(1) that(1)) ``` lp15@66296 ` 693` ``` have "finite S" ``` lp15@66296 ` 694` ``` using S by blast ``` lp15@66296 ` 695` ``` have "\0 fine S" and fineS: ``` haftmann@69260 ` 696` ``` "(\x. ball x (\ * (INF m\Basis. b \ m - a \ m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S" ``` lp15@66296 ` 697` ``` using \\ fine S\ by (auto simp: \_def fine_Int) ``` lp15@66296 ` 698` ``` then have "(\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) < \/2" ``` lp15@66296 ` 699` ``` by (intro \0 that fineS) ``` lp15@66296 ` 700` ``` moreover have "(\(x,K) \ S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h)) \ \/2" ``` lp15@66296 ` 701` ``` proof - ``` lp15@66296 ` 702` ``` have "(\(x,K) \ S. norm (integral K h) - norm (content K *\<^sub>R h x - integral K h)) ``` lp15@66296 ` 703` ``` \ (\(x,K) \ S. norm (content K *\<^sub>R h x))" ``` lp15@66296 ` 704` ``` proof (clarify intro!: sum_mono) ``` lp15@66296 ` 705` ``` fix x K ``` lp15@66296 ` 706` ``` assume xK: "(x,K) \ S" ``` lp15@66296 ` 707` ``` have "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \ norm (integral K h - (integral K h - content K *\<^sub>R h x))" ``` lp15@66296 ` 708` ``` by (metis norm_minus_commute norm_triangle_ineq2) ``` lp15@66296 ` 709` ``` also have "... \ norm (content K *\<^sub>R h x)" ``` lp15@66296 ` 710` ``` by simp ``` lp15@66296 ` 711` ``` finally show "norm (integral K h) - norm (content K *\<^sub>R h x - integral K h) \ norm (content K *\<^sub>R h x)" . ``` lp15@66296 ` 712` ``` qed ``` lp15@66296 ` 713` ``` also have "... \ (\(x,K) \ S. \/4 * (b \ i - a \ i) / content (cbox a b) * ``` lp15@66296 ` 714` ``` content K / (interval_upperbound K \ i - interval_lowerbound K \ i))" ``` lp15@66296 ` 715` ``` proof (clarify intro!: sum_mono) ``` lp15@66296 ` 716` ``` fix x K ``` lp15@66296 ` 717` ``` assume xK: "(x,K) \ S" ``` lp15@66296 ` 718` ``` then have x: "x \ cbox a b" ``` lp15@66296 ` 719` ``` using S unfolding tagged_partial_division_of_def by (meson subset_iff) ``` lp15@66296 ` 720` ``` let ?\ = "interval_upperbound K \ i - interval_lowerbound K \ i" ``` lp15@66296 ` 721` ``` show "norm (content K *\<^sub>R h x) \ \/4 * (b \ i - a \ i) / content (cbox a b) * content K / ?\" ``` lp15@66296 ` 722` ``` proof (cases "content K = 0") ``` lp15@66296 ` 723` ``` case True ``` lp15@66296 ` 724` ``` then show ?thesis by simp ``` lp15@66296 ` 725` ``` next ``` lp15@66296 ` 726` ``` case False ``` lp15@66296 ` 727` ``` then have Kgt0: "content K > 0" ``` lp15@66296 ` 728` ``` using zero_less_measure_iff by blast ``` lp15@66296 ` 729` ``` moreover ``` lp15@66296 ` 730` ``` obtain u v where uv: "K = cbox u v" ``` lp15@66296 ` 731` ``` using S \(x,K) \ S\ by blast ``` lp15@66296 ` 732` ``` then have u_less_v: "\i. i \ Basis \ u \ i < v \ i" ``` lp15@66296 ` 733` ``` using content_pos_lt_eq uv Kgt0 by blast ``` lp15@66296 ` 734` ``` then have dist_uv: "dist u v > 0" ``` lp15@66296 ` 735` ``` using that by auto ``` lp15@66296 ` 736` ``` ultimately have "norm (h x) \ (\ * (b \ i - a \ i)) / (4 * content (cbox a b) * ?\)" ``` lp15@66296 ` 737` ``` proof - ``` haftmann@69260 ` 738` ``` have "dist x u < \ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2" ``` haftmann@69260 ` 739` ``` "dist x v < \ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2" ``` lp15@66296 ` 740` ``` using fineS u_less_v uv xK ``` lp15@66296 ` 741` ``` by (force simp: fine_def mem_box field_simps dest!: bspec)+ ``` haftmann@69260 ` 742` ``` moreover have "\ * (INF m\Basis. b \ m - a \ m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2 ``` lp15@66296 ` 743` ``` \ \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2" ``` lp15@66296 ` 744` ``` apply (intro mult_left_mono divide_right_mono) ``` lp15@66296 ` 745` ``` using \i \ Basis\ \0 < \\ apply (auto simp: intro!: cInf_le_finite) ``` lp15@66296 ` 746` ``` done ``` lp15@66296 ` 747` ``` ultimately ``` lp15@66296 ` 748` ``` have "dist x u < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2" ``` lp15@66296 ` 749` ``` "dist x v < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2" ``` lp15@66296 ` 750` ``` by linarith+ ``` lp15@66296 ` 751` ``` then have duv: "dist u v < \ * (b \ i - a \ i) / (4 * (norm (f x) + 1) * content (cbox a b))" ``` lp15@66296 ` 752` ``` using dist_triangle_half_r by blast ``` lp15@66296 ` 753` ``` have uvi: "\v \ i - u \ i\ \ norm (v - u)" ``` lp15@66296 ` 754` ``` by (metis inner_commute inner_diff_right \i \ Basis\ Basis_le_norm) ``` lp15@66296 ` 755` ``` have "norm (h x) \ norm (f x)" ``` lp15@66296 ` 756` ``` using x that by (auto simp: norm_f) ``` lp15@66296 ` 757` ``` also have "... < (norm (f x) + 1)" ``` lp15@66296 ` 758` ``` by simp ``` lp15@66296 ` 759` ``` also have "... < \ * (b \ i - a \ i) / dist u v / (4 * content (cbox a b))" ``` lp15@66296 ` 760` ``` using duv dist_uv contab_gt0 ``` lp15@66296 ` 761` ``` apply (simp add: divide_simps algebra_simps mult_less_0_iff zero_less_mult_iff split: if_split_asm) ``` lp15@66296 ` 762` ``` by (meson add_nonneg_nonneg linorder_not_le measure_nonneg mult_nonneg_nonneg norm_ge_zero zero_le_numeral) ``` lp15@66296 ` 763` ``` also have "... = \ * (b \ i - a \ i) / norm (v - u) / (4 * content (cbox a b))" ``` lp15@66296 ` 764` ``` by (simp add: dist_norm norm_minus_commute) ``` lp15@66296 ` 765` ``` also have "... \ \ * (b \ i - a \ i) / \v \ i - u \ i\ / (4 * content (cbox a b))" ``` lp15@66296 ` 766` ``` apply (intro mult_right_mono divide_left_mono divide_right_mono uvi) ``` lp15@66296 ` 767` ``` using \0 < \\ a_less_b [OF \i \ Basis\] u_less_v [OF \i \ Basis\] contab_gt0 ``` lp15@66296 ` 768` ``` by (auto simp: less_eq_real_def zero_less_mult_iff that) ``` lp15@66296 ` 769` ``` also have "... = \ * (b \ i - a \ i) ``` lp15@66296 ` 770` ``` / (4 * content (cbox a b) * ?\)" ``` lp15@66296 ` 771` ``` using uv False that(2) u_less_v by fastforce ``` lp15@66296 ` 772` ``` finally show ?thesis by simp ``` lp15@66296 ` 773` ``` qed ``` lp15@66296 ` 774` ``` with Kgt0 have "norm (content K *\<^sub>R h x) \ content K * ((\/4 * (b \ i - a \ i) / content (cbox a b)) / ?\)" ``` lp15@66296 ` 775` ``` using mult_left_mono by fastforce ``` lp15@66296 ` 776` ``` also have "... = \/4 * (b \ i - a \ i) / content (cbox a b) * ``` lp15@66296 ` 777` ``` content K / ?\" ``` lp15@66296 ` 778` ``` by (simp add: divide_simps) ``` lp15@66296 ` 779` ``` finally show ?thesis . ``` lp15@66296 ` 780` ``` qed ``` lp15@66296 ` 781` ``` qed ``` lp15@66296 ` 782` ``` also have "... = (\K\snd ` S. \/4 * (b \ i - a \ i) / content (cbox a b) * content K ``` lp15@66296 ` 783` ``` / (interval_upperbound K \ i - interval_lowerbound K \ i))" ``` lp15@66497 ` 784` ``` apply (rule sum.over_tagged_division_lemma [OF tagged_partial_division_of_Union_self [OF S]]) ``` lp15@66296 ` 785` ``` apply (simp add: box_eq_empty(1) content_eq_0) ``` lp15@66296 ` 786` ``` done ``` lp15@66296 ` 787` ``` also have "... = \/2 * ((b \ i - a \ i) / (2 * content (cbox a b)) * (\K\snd ` S. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)))" ``` lp15@66296 ` 788` ``` by (simp add: sum_distrib_left mult.assoc) ``` lp15@66296 ` 789` ``` also have "... \ (\/2) * 1" ``` lp15@66296 ` 790` ``` proof (rule mult_left_mono) ``` lp15@66296 ` 791` ``` have "(b \ i - a \ i) * (\K\snd ` S. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) ``` lp15@66296 ` 792` ``` \ 2 * content (cbox a b)" ``` lp15@66296 ` 793` ``` proof (rule sum_content_area_over_thin_division) ``` lp15@66296 ` 794` ``` show "snd ` S division_of \(snd ` S)" ``` lp15@66497 ` 795` ``` by (auto intro: S tagged_partial_division_of_Union_self division_of_tagged_division) ``` haftmann@69313 ` 796` ``` show "\(snd ` S) \ cbox a b" ``` lp15@66296 ` 797` ``` using S by force ``` lp15@66296 ` 798` ``` show "a \ i \ c \ i" "c \ i \ b \ i" ``` lp15@66296 ` 799` ``` using mem_box(2) that by blast+ ``` lp15@66296 ` 800` ``` qed (use that in auto) ``` lp15@66296 ` 801` ``` then show "(b \ i - a \ i) / (2 * content (cbox a b)) * (\K\snd ` S. content K / (interval_upperbound K \ i - interval_lowerbound K \ i)) \ 1" ``` lp15@66296 ` 802` ``` by (simp add: contab_gt0) ``` lp15@66296 ` 803` ``` qed (use \0 < \\ in auto) ``` lp15@66296 ` 804` ``` finally show ?thesis by simp ``` lp15@66296 ` 805` ``` qed ``` lp15@66296 ` 806` ``` then have "(\(x,K) \ S. norm (integral K h)) - (\(x,K) \ S. norm (content K *\<^sub>R h x - integral K h)) \ \/2" ``` lp15@66296 ` 807` ``` by (simp add: Groups_Big.sum_subtractf [symmetric]) ``` lp15@66296 ` 808` ``` ultimately show "(\(x,K) \ S. norm (integral K h)) < \" ``` lp15@66296 ` 809` ``` by linarith ``` lp15@66296 ` 810` ``` qed ``` lp15@66296 ` 811` ``` ultimately show ?thesis using that by auto ``` lp15@66296 ` 812` ```qed ``` lp15@66296 ` 813` lp15@66296 ` 814` lp15@66296 ` 815` immler@69681 ` 816` ```proposition equiintegrable_halfspace_restrictions_le: ``` lp15@66296 ` 817` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@66296 ` 818` ``` assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" ``` lp15@66296 ` 819` ``` and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" ``` lp15@66296 ` 820` ``` shows "(\i \ Basis. \c. \h \ F. {(\x. if x \ i \ c then h x else 0)}) ``` lp15@66296 ` 821` ``` equiintegrable_on cbox a b" ``` immler@69681 ` 822` ```proof (cases "content(cbox a b) = 0") ``` lp15@66296 ` 823` ``` case True ``` lp15@66296 ` 824` ``` then show ?thesis by simp ``` lp15@66296 ` 825` ```next ``` lp15@66296 ` 826` ``` case False ``` lp15@66296 ` 827` ``` then have "content(cbox a b) > 0" ``` lp15@66296 ` 828` ``` using zero_less_measure_iff by blast ``` lp15@66296 ` 829` ``` then have "a \ i < b \ i" if "i \ Basis" for i ``` lp15@66296 ` 830` ``` using content_pos_lt_eq that by blast ``` lp15@66296 ` 831` ``` have int_F: "f integrable_on cbox a b" if "f \ F" for f ``` lp15@66296 ` 832` ``` using F that by (simp add: equiintegrable_on_def) ``` lp15@66296 ` 833` ``` let ?CI = "\K h x. content K *\<^sub>R h x - integral K h" ``` lp15@66296 ` 834` ``` show ?thesis ``` lp15@66296 ` 835` ``` unfolding equiintegrable_on_def ``` lp15@66296 ` 836` ``` proof (intro conjI; clarify) ``` lp15@66296 ` 837` ``` show int_lec: "\i \ Basis; h \ F\ \ (\x. if x \ i \ c then h x else 0) integrable_on cbox a b" for i c h ``` lp15@66296 ` 838` ``` using integrable_restrict_Int [of "{x. x \ i \ c}" h] ``` lp15@66296 ` 839` ``` apply (auto simp: interval_split Int_commute mem_box intro!: integrable_on_subcbox int_F) ``` lp15@66296 ` 840` ``` by (metis (full_types, hide_lams) min.bounded_iff) ``` lp15@66296 ` 841` ``` show "\\. gauge \ \ ``` lp15@66296 ` 842` ``` (\f T. f \ (\i\Basis. \c. \h\F. {\x. if x \ i \ c then h x else 0}) \ ``` lp15@66296 ` 843` ``` T tagged_division_of cbox a b \ \ fine T \ ``` lp15@66296 ` 844` ``` norm ((\(x,K) \ T. content K *\<^sub>R f x) - integral (cbox a b) f) < \)" ``` lp15@66296 ` 845` ``` if "\ > 0" for \ ``` lp15@66296 ` 846` ``` proof - ``` lp15@66296 ` 847` ``` obtain \0 where "gauge \0" and \0: ``` lp15@66296 ` 848` ``` "\c i S h. \c \ cbox a b; i \ Basis; S tagged_partial_division_of cbox a b; ``` lp15@66296 ` 849` ``` \0 fine S; h \ F; \x K. (x,K) \ S \ (K \ {x. x \ i = c \ i} \ {})\ ``` lp15@66296 ` 850` ``` \ (\(x,K) \ S. norm (integral K h)) < \/12" ``` lp15@66296 ` 851` ``` apply (rule bounded_equiintegral_over_thin_tagged_partial_division [OF F f, of \\/12\]) ``` lp15@66296 ` 852` ``` using \\ > 0\ by (auto simp: norm_f) ``` lp15@66296 ` 853` ``` obtain \1 where "gauge \1" ``` lp15@66296 ` 854` ``` and \1: "\h T. \h \ F; T tagged_division_of cbox a b; \1 fine T\ ``` lp15@66296 ` 855` ``` \ norm ((\(x,K) \ T. content K *\<^sub>R h x) - integral (cbox a b) h) ``` lp15@66296 ` 856` ``` < \/(7 * (Suc DIM('b)))" ``` lp15@66296 ` 857` ``` proof - ``` lp15@66296 ` 858` ``` have e5: "\/(7 * (Suc DIM('b))) > 0" ``` lp15@66296 ` 859` ``` using \\ > 0\ by auto ``` lp15@66296 ` 860` ``` then show ?thesis ``` lp15@66296 ` 861` ``` using F that by (auto simp: equiintegrable_on_def) ``` lp15@66296 ` 862` ``` qed ``` lp15@66296 ` 863` ``` have h_less3: "(\(x,K) \ T. norm (?CI K h x)) < \/3" ``` lp15@66296 ` 864` ``` if "T tagged_partial_division_of cbox a b" "\1 fine T" "h \ F" for T h ``` lp15@66296 ` 865` ``` proof - ``` lp15@66296 ` 866` ``` have "(\(x,K) \ T. norm (?CI K h x)) \ 2 * real DIM('b) * (\/(7 * Suc DIM('b)))" ``` lp15@66497 ` 867` ``` proof (rule Henstock_lemma_part2 [of h a b]) ``` lp15@66296 ` 868` ``` show "h integrable_on cbox a b" ``` lp15@66296 ` 869` ``` using that F equiintegrable_on_def by metis ``` lp15@66296 ` 870` ``` show "gauge \1" ``` lp15@66296 ` 871` ``` by (rule \gauge \1\) ``` lp15@66296 ` 872` ``` qed (use that \\ > 0\ \1 in auto) ``` lp15@66296 ` 873` ``` also have "... < \/3" ``` lp15@66296 ` 874` ``` using \\ > 0\ by (simp add: divide_simps) ``` lp15@66296 ` 875` ``` finally show ?thesis . ``` lp15@66296 ` 876` ``` qed ``` lp15@66296 ` 877` ``` have *: "norm ((\(x,K) \ T. content K *\<^sub>R f x) - integral (cbox a b) f) < \" ``` lp15@66296 ` 878` ``` if f: "f = (\x. if x \ i \ c then h x else 0)" ``` lp15@66296 ` 879` ``` and T: "T tagged_division_of cbox a b" ``` lp15@66296 ` 880` ``` and fine: "(\x. \0 x \ \1 x) fine T" and "i \ Basis" "h \ F" for f T i c h ``` lp15@66296 ` 881` ``` proof (cases "a \ i \ c \ c \ b \ i") ``` lp15@66296 ` 882` ``` case True ``` lp15@66296 ` 883` ``` have "finite T" ``` lp15@66296 ` 884` ``` using T by blast ``` lp15@66296 ` 885` ``` define T' where "T' \ {(x,K) \ T. K \ {x. x \ i \ c} \ {}}" ``` lp15@66296 ` 886` ``` then have "T' \ T" ``` lp15@66296 ` 887` ``` by auto ``` lp15@66296 ` 888` ``` then have "finite T'" ``` lp15@66296 ` 889` ``` using \finite T\ infinite_super by blast ``` lp15@66296 ` 890` ``` have T'_tagged: "T' tagged_partial_division_of cbox a b" ``` lp15@66296 ` 891` ``` by (meson T \T' \ T\ tagged_division_of_def tagged_partial_division_subset) ``` lp15@66296 ` 892` ``` have fine': "\0 fine T'" "\1 fine T'" ``` lp15@66296 ` 893` ``` using \T' \ T\ fine_Int fine_subset fine by blast+ ``` lp15@66296 ` 894` ``` have int_KK': "(\(x,K) \ T. integral K f) = (\(x,K) \ T'. integral K f)" ``` lp15@66296 ` 895` ``` apply (rule sum.mono_neutral_right [OF \finite T\ \T' \ T\]) ``` lp15@66296 ` 896` ``` using f \finite T\ \T' \ T\ ``` lp15@66296 ` 897` ``` using integral_restrict_Int [of _ "{x. x \ i \ c}" h] ``` lp15@66296 ` 898` ``` apply (auto simp: T'_def Int_commute) ``` lp15@66296 ` 899` ``` done ``` lp15@66296 ` 900` ``` have "(\(x,K) \ T. content K *\<^sub>R f x) = (\(x,K) \ T'. content K *\<^sub>R f x)" ``` lp15@66296 ` 901` ``` apply (rule sum.mono_neutral_right [OF \finite T\ \T' \ T\]) ``` lp15@66296 ` 902` ``` using T f \finite T\ \T' \ T\ apply (force simp: T'_def) ``` lp15@66296 ` 903` ``` done ``` lp15@66296 ` 904` ``` moreover have "norm ((\(x,K) \ T'. content K *\<^sub>R f x) - integral (cbox a b) f) < \" ``` lp15@66296 ` 905` ``` proof - ``` lp15@66296 ` 906` ``` have *: "norm y < \" if "norm x < \/3" "norm(x - y) \ 2 * \/3" for x y::'b ``` lp15@66296 ` 907` ``` proof - ``` lp15@66296 ` 908` ``` have "norm y \ norm x + norm(x - y)" ``` lp15@66296 ` 909` ``` by (metis norm_minus_commute norm_triangle_sub) ``` lp15@66296 ` 910` ``` also have "\ < \/3 + 2*\/3" ``` lp15@66296 ` 911` ``` using that by linarith ``` lp15@66296 ` 912` ``` also have "... = \" ``` lp15@66296 ` 913` ``` by simp ``` lp15@66296 ` 914` ``` finally show ?thesis . ``` lp15@66296 ` 915` ``` qed ``` lp15@66296 ` 916` ``` have "norm (\(x,K) \ T'. ?CI K h x) ``` lp15@66296 ` 917` ``` \ (\(x,K) \ T'. norm (?CI K h x))" ``` lp15@66296 ` 918` ``` by (simp add: norm_sum split_def) ``` lp15@66296 ` 919` ``` also have "... < \/3" ``` lp15@66296 ` 920` ``` by (intro h_less3 T'_tagged fine' that) ``` lp15@66296 ` 921` ``` finally have "norm (\(x,K) \ T'. ?CI K h x) < \/3" . ``` lp15@66296 ` 922` ``` moreover have "integral (cbox a b) f = (\(x,K) \ T. integral K f)" ``` lp15@66296 ` 923` ``` using int_lec that by (auto simp: integral_combine_tagged_division_topdown) ``` lp15@66296 ` 924` ``` moreover have "norm (\(x,K) \ T'. ?CI K h x - ?CI K f x) ``` lp15@66296 ` 925` ``` \ 2*\/3" ``` lp15@66296 ` 926` ``` proof - ``` nipkow@69508 ` 927` ``` define T'' where "T'' \ {(x,K) \ T'. \ (K \ {x. x \ i \ c})}" ``` lp15@66296 ` 928` ``` then have "T'' \ T'" ``` lp15@66296 ` 929` ``` by auto ``` lp15@66296 ` 930` ``` then have "finite T''" ``` lp15@66296 ` 931` ``` using \finite T'\ infinite_super by blast ``` lp15@66296 ` 932` ``` have T''_tagged: "T'' tagged_partial_division_of cbox a b" ``` lp15@66296 ` 933` ``` using T'_tagged \T'' \ T'\ tagged_partial_division_subset by blast ``` lp15@66296 ` 934` ``` have fine'': "\0 fine T''" "\1 fine T''" ``` lp15@66296 ` 935` ``` using \T'' \ T'\ fine' by (blast intro: fine_subset)+ ``` lp15@66296 ` 936` ``` have "(\(x,K) \ T'. ?CI K h x - ?CI K f x) ``` lp15@66296 ` 937` ``` = (\(x,K) \ T''. ?CI K h x - ?CI K f x)" ``` lp15@66296 ` 938` ``` proof (clarify intro!: sum.mono_neutral_right [OF \finite T'\ \T'' \ T'\]) ``` lp15@66296 ` 939` ``` fix x K ``` lp15@66296 ` 940` ``` assume "(x,K) \ T'" "(x,K) \ T''" ``` lp15@66296 ` 941` ``` then have "x \ K" "x \ i \ c" "{x. x \ i \ c} \ K = K" ``` lp15@66296 ` 942` ``` using T''_def T'_tagged by blast+ ``` lp15@66296 ` 943` ``` then show "?CI K h x - ?CI K f x = 0" ``` lp15@66296 ` 944` ``` using integral_restrict_Int [of _ "{x. x \ i \ c}" h] by (auto simp: f) ``` lp15@66296 ` 945` ``` qed ``` lp15@66296 ` 946` ``` moreover have "norm (\(x,K) \ T''. ?CI K h x - ?CI K f x) \ 2*\/3" ``` lp15@66296 ` 947` ``` proof - ``` lp15@66296 ` 948` ``` define A where "A \ {(x,K) \ T''. x \ i \ c}" ``` lp15@66296 ` 949` ``` define B where "B \ {(x,K) \ T''. x \ i > c}" ``` lp15@66296 ` 950` ``` then have "A \ T''" "B \ T''" and disj: "A \ B = {}" and T''_eq: "T'' = A \ B" ``` lp15@66296 ` 951` ``` by (auto simp: A_def B_def) ``` lp15@66296 ` 952` ``` then have "finite A" "finite B" ``` lp15@66296 ` 953` ``` using \finite T''\ by (auto intro: finite_subset) ``` lp15@66296 ` 954` ``` have A_tagged: "A tagged_partial_division_of cbox a b" ``` lp15@66296 ` 955` ``` using T''_tagged \A \ T''\ tagged_partial_division_subset by blast ``` lp15@66296 ` 956` ``` have fineA: "\0 fine A" "\1 fine A" ``` lp15@66296 ` 957` ``` using \A \ T''\ fine'' by (blast intro: fine_subset)+ ``` lp15@66296 ` 958` ``` have B_tagged: "B tagged_partial_division_of cbox a b" ``` lp15@66296 ` 959` ``` using T''_tagged \B \ T''\ tagged_partial_division_subset by blast ``` lp15@66296 ` 960` ``` have fineB: "\0 fine B" "\1 fine B" ``` lp15@66296 ` 961` ``` using \B \ T''\ fine'' by (blast intro: fine_subset)+ ``` lp15@66296 ` 962` ``` have "norm (\(x,K) \ T''. ?CI K h x - ?CI K f x) ``` lp15@66296 ` 963` ``` \ (\(x,K) \ T''. norm (?CI K h x - ?CI K f x))" ``` lp15@66296 ` 964` ``` by (simp add: norm_sum split_def) ``` lp15@66296 ` 965` ``` also have "... = (\(x,K) \ A. norm (?CI K h x - ?CI K f x)) + ``` lp15@66296 ` 966` ``` (\(x,K) \ B. norm (?CI K h x - ?CI K f x))" ``` lp15@66296 ` 967` ``` by (simp add: sum.union_disjoint T''_eq disj \finite A\ \finite B\) ``` lp15@66296 ` 968` ``` also have "... = (\(x,K) \ A. norm (integral K h - integral K f)) + ``` lp15@66296 ` 969` ``` (\(x,K) \ B. norm (?CI K h x + integral K f))" ``` nipkow@67399 ` 970` ``` by (auto simp: A_def B_def f norm_minus_commute intro!: sum.cong arg_cong2 [where f= "(+)"]) ``` lp15@66296 ` 971` ``` also have "... \ (\(x,K)\A. norm (integral K h)) + ``` lp15@66296 ` 972` ``` (\(x,K)\(\(x,K). (x,K \ {x. x \ i \ c})) ` A. norm (integral K h)) ``` lp15@66296 ` 973` ``` + ((\(x,K)\B. norm (?CI K h x)) + ``` lp15@66296 ` 974` ``` (\(x,K)\B. norm (integral K h)) + ``` lp15@66296 ` 975` ``` (\(x,K)\(\(x,K). (x,K \ {x. c \ x \ i})) ` B. norm (integral K h)))" ``` lp15@66296 ` 976` ``` proof (rule add_mono) ``` lp15@66296 ` 977` ``` show "(\(x,K)\A. norm (integral K h - integral K f)) ``` lp15@66296 ` 978` ``` \ (\(x,K)\A. norm (integral K h)) + ``` lp15@66296 ` 979` ``` (\(x,K)\(\(x,K). (x,K \ {x. x \ i \ c})) ` A. ``` lp15@66296 ` 980` ``` norm (integral K h))" ``` lp15@66296 ` 981` ``` proof (subst sum.reindex_nontrivial [OF \finite A\], clarsimp) ``` lp15@66296 ` 982` ``` fix x K L ``` lp15@66296 ` 983` ``` assume "(x,K) \ A" "(x,L) \ A" ``` lp15@66296 ` 984` ``` and int_ne0: "integral (L \ {x. x \ i \ c}) h \ 0" ``` lp15@66296 ` 985` ``` and eq: "K \ {x. x \ i \ c} = L \ {x. x \ i \ c}" ``` lp15@66296 ` 986` ``` have False if "K \ L" ``` lp15@66296 ` 987` ``` proof - ``` lp15@66296 ` 988` ``` obtain u v where uv: "L = cbox u v" ``` lp15@66296 ` 989` ``` using T'_tagged \(x, L) \ A\ \A \ T''\ \T'' \ T'\ by blast ``` haftmann@69313 ` 990` ``` have "A tagged_division_of \(snd ` A)" ``` lp15@66497 ` 991` ``` using A_tagged tagged_partial_division_of_Union_self by auto ``` lp15@66296 ` 992` ``` then have "interior (K \ {x. x \ i \ c}) = {}" ``` lp15@66296 ` 993` ``` apply (rule tagged_division_split_left_inj [OF _ \(x,K) \ A\ \(x,L) \ A\]) ``` lp15@66296 ` 994` ``` using that eq \i \ Basis\ by auto ``` lp15@66296 ` 995` ``` then show False ``` lp15@66296 ` 996` ``` using interval_split [OF \i \ Basis\] int_ne0 content_eq_0_interior eq uv by fastforce ``` lp15@66296 ` 997` ``` qed ``` lp15@66296 ` 998` ``` then show "K = L" by blast ``` lp15@66296 ` 999` ``` next ``` lp15@66296 ` 1000` ``` show "(\(x,K) \ A. norm (integral K h - integral K f)) ``` lp15@66296 ` 1001` ``` \ (\(x,K) \ A. norm (integral K h)) + ``` lp15@66296 ` 1002` ``` sum ((\(x,K). norm (integral K h)) \ (\(x,K). (x,K \ {x. x \ i \ c}))) A" ``` lp15@66296 ` 1003` ``` using integral_restrict_Int [of _ "{x. x \ i \ c}" h] f ``` lp15@66296 ` 1004` ``` by (auto simp: Int_commute A_def [symmetric] sum.distrib [symmetric] intro!: sum_mono norm_triangle_ineq4) ``` lp15@66296 ` 1005` ``` qed ``` lp15@66296 ` 1006` ``` next ``` lp15@66296 ` 1007` ``` show "(\(x,K)\B. norm (?CI K h x + integral K f)) ``` lp15@66296 ` 1008` ``` \ (\(x,K)\B. norm (?CI K h x)) + (\(x,K)\B. norm (integral K h)) + ``` lp15@66296 ` 1009` ``` (\(x,K)\(\(x,K). (x,K \ {x. c \ x \ i})) ` B. norm (integral K h))" ``` lp15@66296 ` 1010` ``` proof (subst sum.reindex_nontrivial [OF \finite B\], clarsimp) ``` lp15@66296 ` 1011` ``` fix x K L ``` lp15@66296 ` 1012` ``` assume "(x,K) \ B" "(x,L) \ B" ``` lp15@66296 ` 1013` ``` and int_ne0: "integral (L \ {x. c \ x \ i}) h \ 0" ``` lp15@66296 ` 1014` ``` and eq: "K \ {x. c \ x \ i} = L \ {x. c \ x \ i}" ``` lp15@66296 ` 1015` ``` have False if "K \ L" ``` lp15@66296 ` 1016` ``` proof - ``` lp15@66296 ` 1017` ``` obtain u v where uv: "L = cbox u v" ``` lp15@66296 ` 1018` ``` using T'_tagged \(x, L) \ B\ \B \ T''\ \T'' \ T'\ by blast ``` haftmann@69313 ` 1019` ``` have "B tagged_division_of \(snd ` B)" ``` lp15@66497 ` 1020` ``` using B_tagged tagged_partial_division_of_Union_self by auto ``` lp15@66296 ` 1021` ``` then have "interior (K \ {x. c \ x \ i}) = {}" ``` lp15@66296 ` 1022` ``` apply (rule tagged_division_split_right_inj [OF _ \(x,K) \ B\ \(x,L) \ B\]) ``` lp15@66296 ` 1023` ``` using that eq \i \ Basis\ by auto ``` lp15@66296 ` 1024` ``` then show False ``` lp15@66296 ` 1025` ``` using interval_split [OF \i \ Basis\] int_ne0 ``` lp15@66296 ` 1026` ``` content_eq_0_interior eq uv by fastforce ``` lp15@66296 ` 1027` ``` qed ``` lp15@66296 ` 1028` ``` then show "K = L" by blast ``` lp15@66296 ` 1029` ``` next ``` lp15@66296 ` 1030` ``` show "(\(x,K) \ B. norm (?CI K h x + integral K f)) ``` lp15@66296 ` 1031` ``` \ (\(x,K) \ B. norm (?CI K h x)) + ``` lp15@66296 ` 1032` ``` (\(x,K) \ B. norm (integral K h)) + sum ((\(x,K). norm (integral K h)) \ (\(x,K). (x,K \ {x. c \ x \ i}))) B" ``` lp15@66296 ` 1033` ``` proof (clarsimp simp: B_def [symmetric] sum.distrib [symmetric] intro!: sum_mono) ``` lp15@66296 ` 1034` ``` fix x K ``` lp15@66296 ` 1035` ``` assume "(x,K) \ B" ``` lp15@66296 ` 1036` ``` have *: "i = i1 + i2 \ norm(c + i1) \ norm c + norm i + norm(i2)" ``` lp15@66296 ` 1037` ``` for i::'b and c i1 i2 ``` lp15@66296 ` 1038` ``` by (metis add.commute add.left_commute add_diff_cancel_right' dual_order.refl norm_add_rule_thm norm_triangle_ineq4) ``` lp15@66296 ` 1039` ``` obtain u v where uv: "K = cbox u v" ``` lp15@66296 ` 1040` ``` using T'_tagged \(x,K) \ B\ \B \ T''\ \T'' \ T'\ by blast ``` lp15@66296 ` 1041` ``` have "h integrable_on cbox a b" ``` lp15@66296 ` 1042` ``` by (simp add: int_F \h \ F\) ``` lp15@66296 ` 1043` ``` then have huv: "h integrable_on cbox u v" ``` lp15@66296 ` 1044` ``` apply (rule integrable_on_subcbox) ``` lp15@66296 ` 1045` ``` using B_tagged \(x,K) \ B\ uv by blast ``` lp15@66296 ` 1046` ``` have "integral K h = integral K f + integral (K \ {x. c \ x \ i}) h" ``` lp15@66296 ` 1047` ``` using integral_restrict_Int [of _ "{x. x \ i \ c}" h] f uv \i \ Basis\ ``` lp15@66296 ` 1048` ``` by (simp add: Int_commute integral_split [OF huv \i \ Basis\]) ``` lp15@66296 ` 1049` ``` then show "norm (?CI K h x + integral K f) ``` lp15@66296 ` 1050` ``` \ norm (?CI K h x) + norm (integral K h) + norm (integral (K \ {x. c \ x \ i}) h)" ``` lp15@66296 ` 1051` ``` by (rule *) ``` lp15@66296 ` 1052` ``` qed ``` lp15@66296 ` 1053` ``` qed ``` lp15@66296 ` 1054` ``` qed ``` lp15@66296 ` 1055` ``` also have "... \ 2*\/3" ``` lp15@66296 ` 1056` ``` proof - ``` lp15@66296 ` 1057` ``` have overlap: "K \ {x. x \ i = c} \ {}" if "(x,K) \ T''" for x K ``` lp15@66296 ` 1058` ``` proof - ``` lp15@66296 ` 1059` ``` obtain y y' where y: "y' \ K" "c < y' \ i" "y \ K" "y \ i \ c" ``` lp15@66296 ` 1060` ``` using that T''_def T'_def \(x,K) \ T''\ by fastforce ``` lp15@66296 ` 1061` ``` obtain u v where uv: "K = cbox u v" ``` lp15@66296 ` 1062` ``` using T''_tagged \(x,K) \ T''\ by blast ``` lp15@66296 ` 1063` ``` then have "connected K" ``` lp15@66296 ` 1064` ``` by (simp add: is_interval_cbox is_interval_connected) ``` lp15@66296 ` 1065` ``` then have "(\z \ K. z \ i = c)" ``` lp15@66296 ` 1066` ``` using y connected_ivt_component by fastforce ``` lp15@66296 ` 1067` ``` then show ?thesis ``` lp15@66296 ` 1068` ``` by fastforce ``` lp15@66296 ` 1069` ``` qed ``` lp15@66296 ` 1070` ``` have **: "\x < \/12; y < \/12; z \ \/2\ \ x + y + z \ 2 * \/3" for x y z ``` lp15@66296 ` 1071` ``` by auto ``` lp15@66296 ` 1072` ``` show ?thesis ``` lp15@66296 ` 1073` ``` proof (rule **) ``` lp15@66296 ` 1074` ``` have cb_ab: "(\j \ Basis. if j = i then c *\<^sub>R i else (a \ j) *\<^sub>R j) \ cbox a b" ``` lp15@66296 ` 1075` ``` using \i \ Basis\ True \\i. i \ Basis \ a \ i < b \ i\ ``` lp15@66296 ` 1076` ``` apply (clarsimp simp add: mem_box) ``` lp15@66296 ` 1077` ``` apply (subst sum_if_inner | force)+ ``` lp15@66296 ` 1078` ``` done ``` lp15@66296 ` 1079` ``` show "(\(x,K) \ A. norm (integral K h)) < \/12" ``` lp15@66296 ` 1080` ``` apply (rule \0 [OF cb_ab \i \ Basis\ A_tagged fineA(1) \h \ F\]) ``` lp15@66296 ` 1081` ``` using \i \ Basis\ \A \ T''\ overlap ``` lp15@66296 ` 1082` ``` apply (subst sum_if_inner | force)+ ``` lp15@66296 ` 1083` ``` done ``` lp15@66296 ` 1084` ``` have 1: "(\(x,K). (x,K \ {x. x \ i \ c})) ` A tagged_partial_division_of cbox a b" ``` lp15@66296 ` 1085` ``` using \finite A\ \i \ Basis\ ``` lp15@66296 ` 1086` ``` apply (auto simp: tagged_partial_division_of_def) ``` lp15@66296 ` 1087` ``` using A_tagged apply (auto simp: A_def) ``` lp15@66296 ` 1088` ``` using interval_split(1) by blast ``` lp15@66296 ` 1089` ``` have 2: "\0 fine (\(x,K). (x,K \ {x. x \ i \ c})) ` A" ``` lp15@66296 ` 1090` ``` using fineA(1) fine_def by fastforce ``` lp15@66296 ` 1091` ``` show "(\(x,K) \ (\(x,K). (x,K \ {x. x \ i \ c})) ` A. norm (integral K h)) < \/12" ``` lp15@66296 ` 1092` ``` apply (rule \0 [OF cb_ab \i \ Basis\ 1 2 \h \ F\]) ``` lp15@66296 ` 1093` ``` using \i \ Basis\ apply (subst sum_if_inner | force)+ ``` lp15@66296 ` 1094` ``` using overlap apply (auto simp: A_def) ``` lp15@66296 ` 1095` ``` done ``` lp15@66296 ` 1096` ``` have *: "\x < \/3; y < \/12; z < \/12\ \ x + y + z \ \/2" for x y z ``` lp15@66296 ` 1097` ``` by auto ``` lp15@66296 ` 1098` ``` show "(\(x,K) \ B. norm (?CI K h x)) + ``` lp15@66296 ` 1099` ``` (\(x,K) \ B. norm (integral K h)) + ``` lp15@66296 ` 1100` ``` (\(x,K) \ (\(x,K). (x,K \ {x. c \ x \ i})) ` B. norm (integral K h)) ``` lp15@66296 ` 1101` ``` \ \/2" ``` lp15@66296 ` 1102` ``` proof (rule *) ``` lp15@66296 ` 1103` ``` show "(\(x,K) \ B. norm (?CI K h x)) < \/3" ``` lp15@66296 ` 1104` ``` by (intro h_less3 B_tagged fineB that) ``` lp15@66296 ` 1105` ``` show "(\(x,K) \ B. norm (integral K h)) < \/12" ``` lp15@66296 ` 1106` ``` apply (rule \0 [OF cb_ab \i \ Basis\ B_tagged fineB(1) \h \ F\]) ``` lp15@66296 ` 1107` ``` using \i \ Basis\ \B \ T''\ overlap by (subst sum_if_inner | force)+ ``` lp15@66296 ` 1108` ``` have 1: "(\(x,K). (x,K \ {x. c \ x \ i})) ` B tagged_partial_division_of cbox a b" ``` lp15@66296 ` 1109` ``` using \finite B\ \i \ Basis\ ``` lp15@66296 ` 1110` ``` apply (auto simp: tagged_partial_division_of_def) ``` lp15@66296 ` 1111` ``` using B_tagged apply (auto simp: B_def) ``` lp15@66296 ` 1112` ``` using interval_split(2) by blast ``` lp15@66296 ` 1113` ``` have 2: "\0 fine (\(x,K). (x,K \ {x. c \ x \ i})) ` B" ``` lp15@66296 ` 1114` ``` using fineB(1) fine_def by fastforce ``` lp15@66296 ` 1115` ``` show "(\(x,K) \ (\(x,K). (x,K \ {x. c \ x \ i})) ` B. norm (integral K h)) < \/12" ``` lp15@66296 ` 1116` ``` apply (rule \0 [OF cb_ab \i \ Basis\ 1 2 \h \ F\]) ``` lp15@66296 ` 1117` ``` using \i \ Basis\ apply (subst sum_if_inner | force)+ ``` lp15@66296 ` 1118` ``` using overlap apply (auto simp: B_def) ``` lp15@66296 ` 1119` ``` done ``` lp15@66296 ` 1120` ``` qed ``` lp15@66296 ` 1121` ``` qed ``` lp15@66296 ` 1122` ``` qed ``` lp15@66296 ` 1123` ``` finally show ?thesis . ``` lp15@66296 ` 1124` ``` qed ``` lp15@66296 ` 1125` ``` ultimately show ?thesis by metis ``` lp15@66296 ` 1126` ``` qed ``` lp15@66296 ` 1127` ``` ultimately show ?thesis ``` lp15@66296 ` 1128` ``` by (simp add: sum_subtractf [symmetric] int_KK' *) ``` lp15@66296 ` 1129` ``` qed ``` lp15@66296 ` 1130` ``` ultimately show ?thesis by metis ``` lp15@66296 ` 1131` ``` next ``` lp15@66296 ` 1132` ``` case False ``` lp15@66296 ` 1133` ``` then consider "c < a \ i" | "b \ i < c" ``` lp15@66296 ` 1134` ``` by auto ``` lp15@66296 ` 1135` ``` then show ?thesis ``` lp15@66296 ` 1136` ``` proof cases ``` lp15@66296 ` 1137` ``` case 1 ``` lp15@66296 ` 1138` ``` then have f0: "f x = 0" if "x \ cbox a b" for x ``` lp15@66296 ` 1139` ``` using that f \i \ Basis\ mem_box(2) by force ``` lp15@66296 ` 1140` ``` then have int_f0: "integral (cbox a b) f = 0" ``` lp15@66296 ` 1141` ``` by (simp add: integral_cong) ``` lp15@66296 ` 1142` ``` have f0_tag: "f x = 0" if "(x,K) \ T" for x K ``` lp15@66296 ` 1143` ``` using T f0 that by (force simp: tagged_division_of_def) ``` lp15@66296 ` 1144` ``` then have "(\(x,K) \ T. content K *\<^sub>R f x) = 0" ``` lp15@66296 ` 1145` ``` by (metis (mono_tags, lifting) real_vector.scale_eq_0_iff split_conv sum.neutral surj_pair) ``` lp15@66296 ` 1146` ``` then show ?thesis ``` lp15@66296 ` 1147` ``` using \0 < \\ by (simp add: int_f0) ``` lp15@66296 ` 1148` ``` next ``` lp15@66296 ` 1149` ``` case 2 ``` lp15@66296 ` 1150` ``` then have fh: "f x = h x" if "x \ cbox a b" for x ``` lp15@66296 ` 1151` ``` using that f \i \ Basis\ mem_box(2) by force ``` lp15@66296 ` 1152` ``` then have int_f: "integral (cbox a b) f = integral (cbox a b) h" ``` lp15@66296 ` 1153` ``` using integral_cong by blast ``` lp15@66296 ` 1154` ``` have fh_tag: "f x = h x" if "(x,K) \ T" for x K ``` lp15@66296 ` 1155` ``` using T fh that by (force simp: tagged_division_of_def) ``` lp15@66296 ` 1156` ``` then have "(\(x,K) \ T. content K *\<^sub>R f x) = (\(x,K) \ T. content K *\<^sub>R h x)" ``` lp15@66296 ` 1157` ``` by (metis (mono_tags, lifting) split_cong sum.cong) ``` lp15@66296 ` 1158` ``` with \0 < \\ show ?thesis ``` lp15@66296 ` 1159` ``` apply (simp add: int_f) ``` lp15@66296 ` 1160` ``` apply (rule less_trans [OF \1]) ``` lp15@66296 ` 1161` ``` using that fine_Int apply (force simp: divide_simps)+ ``` lp15@66296 ` 1162` ``` done ``` lp15@66296 ` 1163` ``` qed ``` lp15@66296 ` 1164` ``` qed ``` lp15@66296 ` 1165` ``` have "gauge (\x. \0 x \ \1 x)" ``` lp15@66296 ` 1166` ``` by (simp add: \gauge \0\ \gauge \1\ gauge_Int) ``` lp15@66296 ` 1167` ``` then show ?thesis ``` lp15@66296 ` 1168` ``` by (auto intro: *) ``` lp15@66296 ` 1169` ``` qed ``` lp15@66296 ` 1170` ``` qed ``` lp15@66296 ` 1171` ```qed ``` lp15@66296 ` 1172` lp15@66296 ` 1173` lp15@66296 ` 1174` immler@69681 ` 1175` ```corollary equiintegrable_halfspace_restrictions_ge: ``` lp15@66296 ` 1176` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@66296 ` 1177` ``` assumes F: "F equiintegrable_on cbox a b" and f: "f \ F" ``` lp15@66296 ` 1178` ``` and norm_f: "\h x. \h \ F; x \ cbox a b\ \ norm(h x) \ norm(f x)" ``` lp15@66296 ` 1179` ``` shows "(\i \ Basis. \c. \h \ F. {(\x. if x \ i \ c then h x else 0)}) ``` lp15@66296 ` 1180` ``` equiintegrable_on cbox a b" ``` immler@69681 ` 1181` ```proof - ``` lp15@66296 ` 1182` ``` have *: "(\i\Basis. \c. \h\(\f. f \ uminus) ` F. {\x. if x \ i \ c then h x else 0}) ``` lp15@66296 ` 1183` ``` equiintegrable_on cbox (- b) (- a)" ``` lp15@66296 ` 1184` ``` proof (rule equiintegrable_halfspace_restrictions_le) ``` lp15@66296 ` 1185` ``` show "(\f. f \ uminus) ` F equiintegrable_on cbox (- b) (- a)" ``` lp15@66296 ` 1186` ``` using F equiintegrable_reflect by blast ``` lp15@66296 ` 1187` ``` show "f \ uminus \ (\f. f \ uminus) ` F" ``` lp15@66296 ` 1188` ``` using f by auto ``` lp15@66296 ` 1189` ``` show "\h x. \h \ (\f. f \ uminus) ` F; x \ cbox (- b) (- a)\ \ norm (h x) \ norm ((f \ uminus) x)" ``` lp15@66296 ` 1190` ``` using f apply (clarsimp simp:) ``` lp15@66296 ` 1191` ``` by (metis add.inverse_inverse image_eqI norm_f uminus_interval_vector) ``` lp15@66296 ` 1192` ``` qed ``` lp15@66296 ` 1193` ``` have eq: "(\f. f \ uminus) ` ``` lp15@66296 ` 1194` ``` (\i\Basis. \c. \h\F. {\x. if x \ i \ c then (h \ uminus) x else 0}) = ``` lp15@66296 ` 1195` ``` (\i\Basis. \c. \h\F. {\x. if c \ x \ i then h x else 0})" ``` lp15@66296 ` 1196` ``` apply (auto simp: o_def cong: if_cong) ``` lp15@66296 ` 1197` ``` using minus_le_iff apply fastforce ``` lp15@66296 ` 1198` ``` apply (rule_tac x="\x. if c \ (-x) \ i then h(-x) else 0" in image_eqI) ``` lp15@66296 ` 1199` ``` using le_minus_iff apply fastforce+ ``` lp15@66296 ` 1200` ``` done ``` lp15@66296 ` 1201` ``` show ?thesis ``` lp15@66296 ` 1202` ``` using equiintegrable_reflect [OF *] by (auto simp: eq) ``` lp15@66296 ` 1203` ```qed ``` lp15@66296 ` 1204` lp15@66296 ` 1205` immler@69681 ` 1206` ```proposition equiintegrable_closed_interval_restrictions: ``` lp15@66296 ` 1207` ``` fixes f :: "'a::euclidean_space \ 'b::euclidean_space" ``` lp15@66296 ` 1208` ``` assumes f: "f integrable_on cbox a b" ``` lp15@66296 ` 1209` ``` shows "(\c d. {(\x. if x \ cbox c d then f x else 0)}) equiintegrable_on cbox a b" ``` immler@69681 ` 1210` ```proof - ``` lp15@66296 ` 1211` ``` let ?g = "\B c d x. if \i\B. c \ i \ x \ i \ x \ i \ d \ i then f x else 0" ``` lp15@66296 ` 1212` ``` have *: "insert f (\c d. {?g B c d}) equiintegrable_on cbox a b" if "B \ Basis" for B ``` lp15@66296 ` 1213` ``` proof - ``` lp15@66296 ` 1214` ``` have "finite B" ``` lp15@66296 ` 1215` ``` using finite_Basis finite_subset \B \ Basis\ by blast ``` lp15@66296 ` 1216` ``` then show ?thesis using \B \ Basis\ ``` lp15@66296 ` 1217` ``` proof (induction B) ``` lp15@66296 ` 1218` ``` case empty ``` lp15@66296 ` 1219` ``` with f show ?case by auto ``` lp15@66296 ` 1220` ``` next ``` lp15@66296 ` 1221` ``` case (insert i B) ``` lp15@66296 ` 1222` ``` then have "i \ Basis" ``` lp15@66296 ` 1223` ``` by auto ``` lp15@66296 ` 1224` ``` have *: "norm (h x) \ norm (f x)" ``` lp15@66296 ` 1225` ``` if "h \ insert f (\c d. {?g B c d})" "x \ cbox a b" for h x ``` lp15@66296 ` 1226` ``` using that by auto ``` lp15@66296 ` 1227` ``` have "(\i\Basis. ``` lp15@66296 ` 1228` ``` \\. \h\insert f (\i\Basis. \\. \h\insert f (\c d. {?g B c d}). {\x. if x \ i \ \ then h x else 0}). ``` lp15@66296 ` 1229` ``` {\x. if \ \ x \ i then h x else 0}) ``` lp15@66296 ` 1230` ``` equiintegrable_on cbox a b" ``` lp15@66296 ` 1231` ``` proof (rule equiintegrable_halfspace_restrictions_ge [where f=f]) ``` lp15@66296 ` 1232` ``` show "insert f (\i\Basis. \\. \h\insert f (\c d. {?g B c d}). ``` lp15@66296 ` 1233` ``` {\x. if x \ i \ \ then h x else 0}) equiintegrable_on cbox a b" ``` lp15@66296 ` 1234` ``` apply (intro * f equiintegrable_on_insert equiintegrable_halfspace_restrictions_le [OF insert.IH insertI1]) ``` lp15@66296 ` 1235` ``` using insert.prems apply auto ``` lp15@66296 ` 1236` ``` done ``` lp15@66296 ` 1237` ``` show"norm(h x) \ norm(f x)" ``` lp15@66296 ` 1238` ``` if "h \ insert f (\i\Basis. \\. \h\insert f (\c d. {?g B c d}). {\x. if x \ i \ \ then h x else 0})" ``` lp15@66296 ` 1239` ``` "x \ cbox a b" for h x ``` lp15@66296 ` 1240` ``` using that by auto ``` lp15@66296 ` 1241` ``` qed auto ``` lp15@66296 ` 1242` ``` then have "insert f (\i\Basis. ``` lp15@66296 ` 1243` ``` \\. \h\insert f (\i\Basis. \\. \h\insert f (\c d. {?g B c d}). {\x. if x \ i \ \ then h x else 0}). ``` lp15@66296 ` 1244` ``` {\x. if \ \ x \ i then h x else 0}) ``` lp15@66296 ` 1245` ``` equiintegrable_on cbox a b" ``` lp15@66296 ` 1246` ``` by (blast intro: f equiintegrable_on_insert) ``` lp15@66296 ` 1247` ``` then show ?case ``` lp15@66296 ` 1248` ``` apply (rule equiintegrable_on_subset, clarify) ``` lp15@66296 ` 1249` ``` using \i \ Basis\ apply simp ``` lp15@66296 ` 1250` ``` apply (drule_tac x=i in bspec, assumption) ``` lp15@66296 ` 1251` ``` apply (drule_tac x="c \ i" in spec, clarify) ``` lp15@66296 ` 1252` ``` apply (drule_tac x=i in bspec, assumption) ``` lp15@66296 ` 1253` ``` apply (drule_tac x="d \ i" in spec) ``` lp15@66296 ` 1254` ``` apply (clarsimp simp add: fun_eq_iff) ``` lp15@66296 ` 1255` ``` apply (drule_tac x=c in spec) ``` lp15@66296 ` 1256` ``` apply (drule_tac x=d in spec) ``` lp15@66296 ` 1257` ``` apply (simp add: split: if_split_asm) ``` lp15@66296 ` 1258` ``` done ``` lp15@66296 ` 1259` ``` qed ``` lp15@66296 ` 1260` ``` qed ``` lp15@66296 ` 1261` ``` show ?thesis ``` lp15@66296 ` 1262` ``` by (rule equiintegrable_on_subset [OF * [OF subset_refl]]) (auto simp: mem_box) ``` lp15@66296 ` 1263` ```qed ``` lp15@66296 ` 1264` ``` ``` lp15@66296 ` 1265` lp15@66296 ` 1266` immler@69683 ` 1267` ```subsection\Continuity of the indefinite integral\ ``` lp15@66296 ` 1268` immler@69681 ` 1269` ```proposition indefinite_integral_continuous: ``` lp15@66296 ` 1270` ``` fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" ``` lp15@66296 ` 1271` ``` assumes int_f: "f integrable_on cbox a b" ``` lp15@66296 ` 1272` ``` and c: "c \ cbox a b" and d: "d \ cbox a b" "0 < \" ``` lp15@66296 ` 1273` ``` obtains \ where "0 < \" ``` lp15@66296 ` 1274` ``` "\c' d'. \c' \ cbox a b; d' \ cbox a b; norm(c' - c) \ \; norm(d' - d) \ \\ ``` lp15@66296 ` 1275` ``` \ norm(integral(cbox c' d') f - integral(cbox c d) f) < \" ``` immler@69681 ` 1276` ```proof - ``` lp15@66296 ` 1277` ``` { assume "\c' d'. c' \ cbox a b \ d' \ cbox a b \ norm(c' - c) \ \ \ norm(d' - d) \ \ \ ``` lp15@66296 ` 1278` ``` norm(integral(cbox c' d') f - integral(cbox c d) f) \ \" ``` lp15@66296 ` 1279` ``` (is "\c' d'. ?\ c' d' \") if "0 < \" for \ ``` lp15@66296 ` 1280` ``` then have "\c' d'. ?\ c' d' (1 / Suc n)" for n ``` lp15@66296 ` 1281` ``` by simp ``` lp15@66296 ` 1282` ``` then obtain u v where "\n. ?\ (u n) (v n) (1 / Suc n)" ``` lp15@66296 ` 1283` ``` by metis ``` lp15@66296 ` 1284` ``` then have u: "u n \ cbox a b" and norm_u: "norm(u n - c) \ 1 / Suc n" ``` lp15@66296 ` 1285` ``` and v: "v n \ cbox a b" and norm_v: "norm(v n - d) \ 1 / Suc n" ``` lp15@66296 ` 1286` ``` and \: "\ \ norm (integral (cbox (u n) (v n)) f - integral (cbox c d) f)" for n ``` lp15@66296 ` 1287` ``` by blast+ ``` lp15@66296 ` 1288` ``` then have False ``` lp15@66296 ` 1289` ``` proof - ``` lp15@66296 ` 1290` ``` have uvn: "cbox (u n) (v n) \ cbox a b" for n ``` lp15@66296 ` 1291` ``` by (meson u v mem_box(2) subset_box(1)) ``` lp15@66296 ` 1292` ``` define S where "S \ \i \ Basis. {x. x \ i = c \ i} \ {x. x \ i = d \ i}" ``` lp15@66296 ` 1293` ``` have "negligible S" ``` lp15@66296 ` 1294` ``` unfolding S_def by force ``` lp15@66296 ` 1295` ``` then have int_f': "(\x. if x \ S then 0 else f x) integrable_on cbox a b" ``` lp15@67980 ` 1296` ``` by (force intro: integrable_spike assms) ``` lp15@66296 ` 1297` ``` have get_n: "\n. \m\n. x \ cbox (u m) (v m) \ x \ cbox c d" if x: "x \ S" for x ``` lp15@66296 ` 1298` ``` proof - ``` lp15@66296 ` 1299` ``` define \ where "\ \ Min ((\i. min \x \ i - c \ i\ \x \ i - d \ i\) ` Basis)" ``` lp15@66296 ` 1300` ``` have "\ > 0" ``` lp15@66296 ` 1301` ``` using \x \ S\ by (auto simp: S_def \_def) ``` lp15@66296 ` 1302` ``` then obtain n where "n \ 0" and n: "1 / (real n) < \" ``` lp15@66296 ` 1303` ``` by (metis inverse_eq_divide real_arch_inverse) ``` lp15@66296 ` 1304` ``` have emin: "\ \ min \x \ i - c \ i\ \x \ i - d \ i\" if "i \ Basis" for i ``` lp15@66296 ` 1305` ``` unfolding \_def ``` lp15@66296 ` 1306` ``` apply (rule Min.coboundedI) ``` lp15@66296 ` 1307` ``` using that by force+ ``` lp15@66296 ` 1308` ``` have "1 / real (Suc n) < \" ``` lp15@66296 ` 1309` ``` using n \n \ 0\ \\ > 0\ by (simp add: field_simps) ``` lp15@66296 ` 1310` ``` have "x \ cbox (u m) (v m) \ x \ cbox c d" if "m \ n" for m ``` lp15@66296 ` 1311` ``` proof - ``` lp15@66296 ` 1312` ``` have *: "\\u - c\ \ n; \v - d\ \ n; N < \x - c\; N < \x - d\; n \ N\ ``` lp15@66296 ` 1313` ``` \ u \ x \ x \ v \ c \ x \ x \ d" for N n u v c d and x::real ``` lp15@66296 ` 1314` ``` by linarith ``` lp15@66296 ` 1315` ``` have "(u m \ i \ x \ i \ x \ i \ v m \ i) = (c \ i \ x \ i \ x \ i \ d \ i)" ``` lp15@66296 ` 1316` ``` if "i \ Basis" for i ``` lp15@66296 ` 1317` ``` proof (rule *) ``` lp15@66296 ` 1318` ``` show "\u m \ i - c \ i\ \ 1 / Suc m" ``` lp15@66296 ` 1319` ``` using norm_u [of m] ``` lp15@66296 ` 1320` ``` by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that) ``` lp15@66296 ` 1321` ``` show "\v m \ i - d \ i\ \ 1 / real (Suc m)" ``` lp15@66296 ` 1322` ``` using norm_v [of m] ``` lp15@66296 ` 1323` ``` by (metis (full_types) order_trans Basis_le_norm inner_commute inner_diff_right that) ``` lp15@66296 ` 1324` ``` show "1/n < \x \ i - c \ i\" "1/n < \x \ i - d \ i\" ``` lp15@66296 ` 1325` ``` using n \n \ 0\ emin [OF \i \ Basis\] ``` lp15@66296 ` 1326` ``` by (simp_all add: inverse_eq_divide) ``` lp15@66296 ` 1327` ``` show "1 / real (Suc m) \ 1 / real n" ``` lp15@66296 ` 1328` ``` using \n \ 0\ \m \ n\ by (simp add: divide_simps) ``` lp15@66296 ` 1329` ``` qed ``` lp15@66296 ` 1330` ``` then show ?thesis by (simp add: mem_box) ``` lp15@66296 ` 1331` ``` qed ``` lp15@66296 ` 1332` ``` then show ?thesis by blast ``` lp15@66296 ` 1333` ``` qed ``` lp15@66296 ` 1334` ``` have 1: "range (\n x. if x \ cbox (u n) (v n) then if x \ S then 0 else f x else 0) equiintegrable_on cbox a b" ``` lp15@66296 ` 1335` ``` by (blast intro: equiintegrable_on_subset [OF equiintegrable_closed_interval_restrictions [OF int_f']]) ``` lp15@66296 ` 1336` ``` have 2: "(\n. if x \ cbox (u n) (v n) then if x \ S then 0 else f x else 0) ``` lp15@66296 ` 1337` ``` \ (if x \ cbox c d then if x \ S then 0 else f x else 0)" for x ``` lp15@66296 ` 1338` ``` by (fastforce simp: dest: get_n intro: Lim_eventually eventually_sequentiallyI) ``` lp15@66296 ` 1339` ``` have [simp]: "cbox c d \ cbox a b = cbox c d" ``` lp15@66296 ` 1340` ``` using c d by (force simp: mem_box) ``` lp15@66296 ` 1341` ``` have [simp]: "cbox (u n) (v n) \ cbox a b = cbox (u n) (v n)" for n ``` lp15@66296 ` 1342` ``` using u v by (fastforce simp: mem_box intro: order.trans) ``` lp15@66296 ` 1343` ``` have "\y A. y \ A - S \ f y = (\x. if x \ S then 0 else f x) y" ``` lp15@66296 ` 1344` ``` by simp ``` lp15@66296 ` 1345` ``` then have "\A. integral A (\x. if x \ S then 0 else f (x)) = integral A (\x. f (x))" ``` lp15@66296 ` 1346` ``` by (blast intro: integral_spike [OF \negligible S\]) ``` lp15@66296 ` 1347` ``` moreover ``` lp15@66296 ` 1348` ``` obtain N where "dist (integral (cbox (u N) (v N)) (\x. if x \ S then 0 else f x)) ``` lp15@66296 ` 1349` ``` (integral (cbox c d) (\x. if x \ S then 0 else f x)) < \" ``` lp15@66296 ` 1350` ``` using equiintegrable_limit [OF 1 2] \0 < \\ by (force simp: integral_restrict_Int lim_sequentially) ``` lp15@66296 ` 1351` ``` ultimately have "dist (integral (cbox (u N) (v N)) f) (integral (cbox c d) f) < \" ``` lp15@66296 ` 1352` ``` by simp ``` lp15@66296 ` 1353` ``` then show False ``` lp15@66296 ` 1354` ``` by (metis dist_norm not_le \) ``` lp15@66296 ` 1355` ``` qed ``` lp15@66296 ` 1356` ``` } ``` lp15@66296 ` 1357` ``` then show ?thesis ``` lp15@66296 ` 1358` ``` by (meson not_le that) ``` lp15@66296 ` 1359` ```qed ``` lp15@66296 ` 1360` immler@69681 ` 1361` ```corollary indefinite_integral_uniformly_continuous: ``` lp15@66296 ` 1362` ``` fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" ``` lp15@66296 ` 1363` ``` assumes "f integrable_on cbox a b" ``` lp15@66296 ` 1364` ``` shows "uniformly_continuous_on (cbox (Pair a a) (Pair b b)) (\y. integral (cbox (fst y) (snd y)) f)" ``` immler@69681 ` 1365` ```proof - ``` lp15@66296 ` 1366` ``` show ?thesis ``` lp15@66296 ` 1367` ``` proof (rule compact_uniformly_continuous, clarsimp simp add: continuous_on_iff) ``` lp15@66296 ` 1368` ``` fix c d and \::real ``` lp15@66296 ` 1369` ``` assume c: "c \ cbox a b" and d: "d \ cbox a b" and "0 < \" ``` lp15@66296 ` 1370` ``` obtain \ where "0 < \" and \: ``` lp15@66296 ` 1371` ``` "\c' d'. \c' \ cbox a b; d' \ cbox a b; norm(c' - c) \ \; norm(d' - d) \ \\ ``` lp15@66296 ` 1372` ``` \ norm(integral(cbox c' d') f - ``` lp15@66296 ` 1373` ``` integral(cbox c d) f) < \" ``` lp15@66296 ` 1374` ``` using indefinite_integral_continuous \0 < \\ assms c d by blast ``` lp15@66296 ` 1375` ``` show "\\ > 0. \x' \ cbox (a, a) (b, b). ``` lp15@66296 ` 1376` ``` dist x' (c, d) < \ \ ``` lp15@66296 ` 1377` ``` dist (integral (cbox (fst x') (snd x')) f) ``` lp15@66296 ` 1378` ``` (integral (cbox c d) f) ``` lp15@66296 ` 1379` ``` < \" ``` lp15@66296 ` 1380` ``` using \0 < \\ ``` lp15@66296 ` 1381` ``` by (force simp: dist_norm intro: \ order_trans [OF norm_fst_le] order_trans [OF norm_snd_le] less_imp_le) ``` lp15@66296 ` 1382` ``` qed auto ``` lp15@66296 ` 1383` ```qed ``` lp15@66296 ` 1384` lp15@66296 ` 1385` immler@69681 ` 1386` ```corollary bounded_integrals_over_subintervals: ``` lp15@66296 ` 1387` ``` fixes f :: "'a :: euclidean_space \ 'b :: euclidean_space" ``` lp15@66296 ` 1388` ``` assumes "f integrable_on cbox a b" ``` lp15@66296 ` 1389` ``` shows "bounded {integral (cbox c d) f |c d. cbox c d \ cbox a b}" ``` immler@69681 ` 1390` ```proof - ``` lp15@66296 ` 1391` ``` have "bounded ((\y. integral (cbox (fst y) (snd y)) f) ` cbox (a, a) (b, b))" ``` lp15@66296 ` 1392` ``` (is "bounded ?I") ``` lp15@66296 ` 1393` ``` by (blast intro: bounded_cbox bounded_uniformly_continuous_image indefinite_integral_uniformly_continuous [OF assms]) ``` lp15@66296 ` 1394` ``` then obtain B where "B > 0" and B: "\x. x \ ?I \ norm x \ B" ``` lp15@66296 ` 1395` ``` by (auto simp: bounded_pos) ``` lp15@66296 ` 1396` ``` have "norm x \ B" if "x = integral (cbox c d) f" "cbox c d \ cbox a b" for x c d ``` lp15@66296 ` 1397` ``` proof (cases "cbox c d = {}") ``` lp15@66296 ` 1398` ``` case True ``` lp15@66296 ` 1399` ``` with \0 < B\ that show ?thesis by auto ``` lp15@66296 ` 1400` ``` next ``` lp15@66296 ` 1401` ``` case False ``` lp15@66296 ` 1402` ``` show ?thesis ``` lp15@66296 ` 1403` ``` apply (rule B) ``` lp15@66296 ` 1404` ``` using that \B > 0\ False apply (clarsimp simp: image_def) ``` lp15@66296 ` 1405` ``` by (metis cbox_Pair_iff interval_subset_is_interval is_interval_cbox prod.sel) ``` lp15@66296 ` 1406` ``` qed ``` lp15@66296 ` 1407` ``` then show ?thesis ``` lp15@66296 ` 1408` ``` by (blast intro: boundedI) ``` lp15@66296 ` 1409` ```qed ``` lp15@66296 ` 1410` lp15@66296 ` 1411` lp15@66296 ` 1412` ```text\An existence theorem for "improper" integrals. ``` lp15@66296 ` 1413` ```Hake's theorem implies that if the integrals over subintervals have a limit, the integral exists. ``` lp15@66296 ` 1414` ```We only need to assume that the integrals are bounded, and we get absolute integrability, ``` lp15@66296 ` 1415` ```but we also need a (rather weak) bound assumption on the function.\ ``` lp15@66296 ` 1416` immler@69681 ` 1417` ```theorem absolutely_integrable_improper: ``` lp15@66296 ` 1418` ``` fixes f :: "'M::euclidean_space \ 'N::euclidean_space" ``` lp15@66296 ` 1419` ``` assumes int_f: "\c d. cbox c d \ box a b \ f integrable_on cbox c d" ``` lp15@66296 ` 1420` ``` and bo: "bounded {integral (cbox c d) f |c d. cbox c d \ box a b}" ``` lp15@66296 ` 1421` ``` and absi: "\i. i \ Basis ``` lp15@66296 ` 1422` ``` \ \g. g absolutely_integrable_on cbox a b \ ``` lp15@66296 ` 1423` ``` ((\x \ cbox a b. f x \ i \ g x) \ (\x \ cbox a b. f x \ i \ g x))" ``` lp15@66296 ` 1424` ``` shows "f absolutely_integrable_on cbox a b" ``` immler@69681 ` 1425` ```proof (cases "content(cbox a b) = 0") ``` lp15@66296 ` 1426` ``` case True ``` lp15@66296 ` 1427` ``` then show ?thesis ``` lp15@66296 ` 1428` ``` by auto ``` lp15@66296 ` 1429` ```next ``` lp15@66296 ` 1430` ``` case False ``` lp15@66296 ` 1431` ``` then have pos: "content(cbox a b) > 0" ``` lp15@66296 ` 1432` ``` using zero_less_measure_iff by blast ``` lp15@66296 ` 1433` ``` show ?thesis ``` lp15@66296 ` 1434` ``` unfolding absolutely_integrable_componentwise_iff [where f = f] ``` lp15@66296 ` 1435` ``` proof ``` lp15@66296 ` 1436` ``` fix j::'N ``` lp15@66296 ` 1437` ``` assume "j \ Basis" ``` lp15@66296 ` 1438` ``` then obtain g where absint_g: "g absolutely_integrable_on cbox a b" ``` lp15@66296 ` 1439` ``` and g: "(\x \ cbox a b. f x \ j \ g x) \ (\x \ cbox a b. f x \ j \ g x)" ``` lp15@66296 ` 1440` ``` using absi by blast ``` lp15@66296 ` 1441` ``` have int_gab: "g integrable_on cbox a b" ``` lp15@66296 ` 1442` ``` using absint_g set_lebesgue_integral_eq_integral(1) by blast ``` lp15@66296 ` 1443` ``` have 1: "cbox (a + (b - a) /\<^sub>R real (Suc n)) (b - (b - a) /\<^sub>R real (Suc n)) \ box a b" for n ``` lp15@66296 ` 1444` ``` apply (rule subset_box_imp) ``` lp15@66296 ` 1445` ``` using pos apply (auto simp: content_pos_lt_eq algebra_simps) ``` lp15@66296 ` 1446` ``` done ``` lp15@66296 ` 1447` ``` have 2: "cbox (a + (b - a) /\<^sub>R real (Suc n)) (b - (b - a) /\<^sub>R real (Suc n)) \ ``` lp15@66296 ` 1448` ``` cbox (a + (b - a) /\<^sub>R real (Suc n + 1)) (b - (b - a) /\<^sub>R real (Suc n + 1))" for n ``` lp15@66296 ` 1449` ``` apply (rule subset_box_imp) ``` lp15@66296 ` 1450` ``` using pos apply (simp add: content_pos_lt_eq algebra_simps) ``` lp15@66296 ` 1451` ``` apply (simp add: divide_simps) ``` lp15@66296 ` 1452` ``` apply (auto simp: field_simps) ``` lp15@66296 ` 1453` ``` done ``` lp15@66296 ` 1454` ``` have getN: "\N::nat. \k. k \ N \ x \ cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)" ``` lp15@66296 ` 1455` ``` if x: "x \ box a b" for x ``` lp15@66296 ` 1456` ``` proof - ``` lp15@66296 ` 1457` ``` let ?\ = "(\i \ Basis. {((x - a) \ i) / ((b - a) \ i), (b - x) \ i / ((b - a) \ i)})" ``` lp15@66296 ` 1458` ``` obtain N where N: "real N > 1 / Inf ?\" ``` lp15@66296 ` 1459` ``` using reals_Archimedean2 by blast ``` lp15@66296 ` 1460` ``` moreover have \: "Inf ?\ > 0" ``` lp15@66296 ` 1461` ``` using that by (auto simp: finite_less_Inf_iff mem_box algebra_simps divide_simps) ``` lp15@66296 ` 1462` ``` ultimately have "N > 0" ``` lp15@66296 ` 1463` ``` using of_nat_0_less_iff by fastforce ``` lp15@66296 ` 1464` ``` show ?thesis ``` lp15@66296 ` 1465` ``` proof (intro exI impI allI) ``` lp15@66296 ` 1466` ``` fix k assume "N \ k" ``` lp15@66296 ` 1467` ``` with \0 < N\ have "k > 0" ``` lp15@66296 ` 1468` ``` by linarith ``` lp15@66296 ` 1469` ``` have xa_gt: "(x - a) \ i > ((b - a) \ i) / (real k)" if "i \ Basis" for i ``` lp15@66296 ` 1470` ``` proof - ``` lp15@66296 ` 1471` ``` have *: "Inf ?\ \ ((x - a) \ i) / ((b - a) \ i)" ``` lp15@66296 ` 1472` ``` using that by (force intro: cInf_le_finite) ``` lp15@66296 ` 1473` ``` have "1 / Inf ?\ \ ((b - a) \ i) / ((x - a) \ i)" ``` lp15@66296 ` 1474` ``` using le_imp_inverse_le [OF * \] ``` lp15@66296 ` 1475` ``` by (simp add: field_simps) ``` lp15@66296 ` 1476` ``` with N have "k > ((b - a) \ i) / ((x - a) \ i)" ``` lp15@66296 ` 1477` ``` using \N \ k\ by linarith ``` lp15@66296 ` 1478` ``` with x that show ?thesis ``` lp15@66296 ` 1479` ``` by (auto simp: mem_box algebra_simps divide_simps) ``` lp15@66296 ` 1480` ``` qed ``` lp15@66296 ` 1481` ``` have bx_gt: "(b - x) \ i > ((b - a) \ i) / k" if "i \ Basis" for i ``` lp15@66296 ` 1482` ``` proof - ``` lp15@66296 ` 1483` ``` have *: "Inf ?\ \ ((b - x) \ i) / ((b - a) \ i)" ``` lp15@66296 ` 1484` ``` using that by (force intro: cInf_le_finite) ``` lp15@66296 ` 1485` ``` have "1 / Inf ?\ \ ((b - a) \ i) / ((b - x) \ i)" ``` lp15@66296 ` 1486` ``` using le_imp_inverse_le [OF * \] ``` lp15@66296 ` 1487` ``` by (simp add: field_simps) ``` lp15@66296 ` 1488` ``` with N have "k > ((b - a) \ i) / ((b - x) \ i)" ``` lp15@66296 ` 1489` ``` using \N \ k\ by linarith ``` lp15@66296 ` 1490` ``` with x that show ?thesis ``` lp15@66296 ` 1491` ``` by (auto simp: mem_box algebra_simps divide_simps) ``` lp15@66296 ` 1492` ``` qed ``` lp15@66296 ` 1493` ``` show "x \ cbox (a + (b - a) /\<^sub>R k) (b - (b - a) /\<^sub>R k)" ``` lp15@66296 ` 1494` ``` using that \ \k > 0\ ``` lp15@66296 ` 1495` ``` by (auto simp: mem_box algebra_simps divide_inverse dest: xa_gt bx_gt) ``` lp15@66296 ` 1496` ``` qed ``` lp15@66296 ` 1497` ``` qed ``` lp15@66296 ` 1498` ``` obtain Bf where "Bf > 0" and Bf: "\c d. cbox c d \ box a b \ norm (integral (cbox c d) f) \ Bf" ``` lp15@66296 ` 1499` ``` using bo unfolding bounded_pos by blast ``` lp15@66296 ` 1500` ``` obtain Bg where "Bg > 0" and Bg:"\c d. cbox c d \ cbox a b \ \integral (cbox c d) g\ \ Bg" ``` lp15@66296 ` 1501` ``` using bounded_integrals_over_subintervals [OF int_gab] unfolding bounded_pos real_norm_def by blast ``` lp15@66296 ` 1502` ``` show "(\x. f x \ j) absolutely_integrable_on cbox a b" ``` lp15@66296 ` 1503` ``` using g ``` wenzelm@67443 ` 1504` ``` proof \ \A lot of duplication in the two proofs\ ``` lp15@66296 ` 1505` ``` assume fg [rule_format]: "\x\cbox a b. f x \ j \ g x" ``` lp15@66296 ` 1506` ``` have "(\x. (f x \ j)) = (\x. g x - (g x - (f x \ j)))" ``` lp15@66296 ` 1507` ``` by simp ``` lp15@66296 ` 1508` ``` moreover have "(\x. g x - (g x - (f x \ j))) integrable_on cbox a b" ``` lp15@66296 ` 1509` ``` proof (rule Henstock_Kurzweil_Integration.integrable_diff [OF int_gab]) ``` lp15@66296 ` 1510` ``` let ?\ = "\k x. if x \ cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k)) ``` lp15@66296 ` 1511` ``` then g x - f x \ j else 0" ``` lp15@66296 ` 1512` ``` have "(\x. g x - f x \ j) integrable_on box a b" ``` lp15@66408 ` 1513` ``` proof (rule monotone_convergence_increasing [of ?\, THEN conjunct1]) ``` lp15@66296 ` 1514` ``` have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \ box a b ``` lp15@66296 ` 1515` ``` = cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k ``` lp15@66296 ` 1516` ``` using box_subset_cbox "1" by fastforce ``` lp15@66296 ` 1517` ``` show "?\ k integrable_on box a b" for k ``` lp15@66296 ` 1518` ``` apply (simp add: integrable_restrict_Int integral_restrict_Int *) ``` lp15@66296 ` 1519` ``` apply (rule integrable_diff [OF integrable_on_subcbox [OF int_gab]]) ``` lp15@66296 ` 1520` ``` using "*" box_subset_cbox apply blast ``` lp15@66296 ` 1521` ``` by (metis "1" int_f integrable_component of_nat_Suc) ``` lp15@66296 ` 1522` ``` have cb12: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) ``` lp15@66296 ` 1523` ``` \ cbox (a + (b - a) /\<^sub>R (2 + real k)) (b - (b - a) /\<^sub>R (2 + real k))" for k ``` lp15@66296 ` 1524` ``` using False content_eq_0 ``` lp15@66296 ` 1525` ``` apply (simp add: subset_box algebra_simps) ``` lp15@66296 ` 1526` ``` apply (simp add: divide_simps) ``` lp15@66296 ` 1527` ``` apply (fastforce simp: field_simps) ``` lp15@66296 ` 1528` ``` done ``` lp15@66296 ` 1529` ``` show "?\ k x \ ?\ (Suc k) x" if "x \ box a b" for k x ``` lp15@66296 ` 1530` ``` using cb12 box_subset_cbox that by (force simp: intro!: fg) ``` lp15@66296 ` 1531` ``` show "(\k. ?\ k x) \ g x - f x \ j" if x: "x \ box a b" for x ``` lp15@66296 ` 1532` ``` proof (rule Lim_eventually) ``` lp15@66296 ` 1533` ``` obtain N::nat where N: "\k. k \ N \ x \ cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)" ``` lp15@66296 ` 1534` ``` using getN [OF x] by blast ``` lp15@66296 ` 1535` ``` show "\\<^sub>F k in sequentially. ?\ k x = g x - f x \ j" ``` lp15@66296 ` 1536` ``` proof ``` lp15@66296 ` 1537` ``` fix k::nat assume "N \ k" ``` lp15@66296 ` 1538` ``` have "x \ cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))" ``` lp15@66296 ` 1539` ``` by (metis \N \ k\ le_Suc_eq N) ``` lp15@66296 ` 1540` ``` then show "?\ k x = g x - f x \ j" ``` lp15@66296 ` 1541` ``` by simp ``` lp15@66296 ` 1542` ``` qed ``` lp15@66296 ` 1543` ``` qed ``` lp15@66296 ` 1544` ``` have "\integral (box a b) ``` lp15@66296 ` 1545` ``` (\x. if x \ cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) ``` lp15@66296 ` 1546` ``` then g x - f x \ j else 0)\ \ Bg + Bf" for k ``` lp15@66296 ` 1547` ``` proof - ``` lp15@66296 ` 1548` ``` let ?I = "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" ``` lp15@66296 ` 1549` ``` have I_int [simp]: "?I \ box a b = ?I" ``` lp15@66296 ` 1550` ``` using 1 by (simp add: Int_absorb2) ``` lp15@66296 ` 1551` ``` have int_fI: "f integrable_on ?I" ``` lp15@66296 ` 1552` ``` apply (rule integrable_subinterval [OF int_f order_refl]) ``` lp15@66296 ` 1553` ``` using "*" box_subset_cbox by blast ``` lp15@66296 ` 1554` ``` then have "(\x. f x \ j) integrable_on ?I" ``` lp15@66296 ` 1555` ``` by (simp add: integrable_component) ``` lp15@66296 ` 1556` ``` moreover have "g integrable_on ?I" ``` lp15@66296 ` 1557` ``` apply (rule integrable_subinterval [OF int_gab]) ``` lp15@66296 ` 1558` ``` using "*" box_subset_cbox by blast ``` lp15@66296 ` 1559` ``` moreover ``` lp15@66296 ` 1560` ``` have "\integral ?I (\x. f x \ j)\ \ norm (integral ?I f)" ``` lp15@66296 ` 1561` ``` by (simp add: Basis_le_norm int_fI \j \ Basis\) ``` lp15@66296 ` 1562` ``` with 1 I_int have "\integral ?I (\x. f x \ j)\ \ Bf" ``` lp15@66296 ` 1563` ``` by (blast intro: order_trans [OF _ Bf]) ``` lp15@66296 ` 1564` ``` ultimately show ?thesis ``` lp15@66296 ` 1565` ``` apply (simp add: integral_restrict_Int integral_diff) ``` lp15@66296 ` 1566` ``` using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4]) ``` lp15@66296 ` 1567` ``` qed ``` lp15@66408 ` 1568` ``` then show "bounded (range (\k. integral (box a b) (?\ k)))" ``` lp15@66296 ` 1569` ``` apply (simp add: bounded_pos) ``` lp15@66296 ` 1570` ``` apply (rule_tac x="Bg+Bf" in exI) ``` lp15@66296 ` 1571` ``` using \0 < Bf\ \0 < Bg\ apply auto ``` lp15@66296 ` 1572` ``` done ``` lp15@66296 ` 1573` ``` qed ``` lp15@66296 ` 1574` ``` then show "(\x. g x - f x \ j) integrable_on cbox a b" ``` lp15@66296 ` 1575` ``` by (simp add: integrable_on_open_interval) ``` lp15@66296 ` 1576` ``` qed ``` lp15@66296 ` 1577` ``` ultimately have "(\x. f x \ j) integrable_on cbox a b" ``` lp15@66296 ` 1578` ``` by auto ``` lp15@66296 ` 1579` ``` then show ?thesis ``` lp15@66296 ` 1580` ``` apply (rule absolutely_integrable_component_ubound [OF _ absint_g]) ``` lp15@66296 ` 1581` ``` by (simp add: fg) ``` lp15@66296 ` 1582` ``` next ``` lp15@66296 ` 1583` ``` assume gf [rule_format]: "\x\cbox a b. g x \ f x \ j" ``` lp15@66296 ` 1584` ``` have "(\x. (f x \ j)) = (\x. ((f x \ j) - g x) + g x)" ``` lp15@66296 ` 1585` ``` by simp ``` lp15@66296 ` 1586` ``` moreover have "(\x. (f x \ j - g x) + g x) integrable_on cbox a b" ``` lp15@66296 ` 1587` ``` proof (rule Henstock_Kurzweil_Integration.integrable_add [OF _ int_gab]) ``` lp15@66296 ` 1588` ``` let ?\ = "\k x. if x \ cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k)) ``` lp15@66296 ` 1589` ``` then f x \ j - g x else 0" ``` lp15@66296 ` 1590` ``` have "(\x. f x \ j - g x) integrable_on box a b" ``` lp15@66408 ` 1591` ``` proof (rule monotone_convergence_increasing [of ?\, THEN conjunct1]) ``` lp15@66296 ` 1592` ``` have *: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) \ box a b ``` lp15@66296 ` 1593` ``` = cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" for k ``` lp15@66296 ` 1594` ``` using box_subset_cbox "1" by fastforce ``` lp15@66296 ` 1595` ``` show "?\ k integrable_on box a b" for k ``` lp15@66296 ` 1596` ``` apply (simp add: integrable_restrict_Int integral_restrict_Int *) ``` lp15@66296 ` 1597` ``` apply (rule integrable_diff) ``` lp15@66296 ` 1598` ``` apply (metis "1" int_f integrable_component of_nat_Suc) ``` lp15@66296 ` 1599` ``` apply (rule integrable_on_subcbox [OF int_gab]) ``` lp15@66296 ` 1600` ``` using "*" box_subset_cbox apply blast ``` lp15@66296 ` 1601` ``` done ``` lp15@66296 ` 1602` ``` have cb12: "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) ``` lp15@66296 ` 1603` ``` \ cbox (a + (b - a) /\<^sub>R (2 + real k)) (b - (b - a) /\<^sub>R (2 + real k))" for k ``` lp15@66296 ` 1604` ``` using False content_eq_0 ``` lp15@66296 ` 1605` ``` apply (simp add: subset_box algebra_simps) ``` lp15@66296 ` 1606` ``` apply (simp add: divide_simps) ``` lp15@66296 ` 1607` ``` apply (fastforce simp: field_simps) ``` lp15@66296 ` 1608` ``` done ``` lp15@66296 ` 1609` ``` show "?\ k x \ ?\ (Suc k) x" if "x \ box a b" for k x ``` lp15@66296 ` 1610` ``` using cb12 box_subset_cbox that by (force simp: intro!: gf) ``` lp15@66296 ` 1611` ``` show "(\k. ?\ k x) \ f x \ j - g x" if x: "x \ box a b" for x ``` lp15@66296 ` 1612` ``` proof (rule Lim_eventually) ``` lp15@66296 ` 1613` ``` obtain N::nat where N: "\k. k \ N \ x \ cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)" ``` lp15@66296 ` 1614` ``` using getN [OF x] by blast ``` lp15@66296 ` 1615` ``` show "\\<^sub>F k in sequentially. ?\ k x = f x \ j - g x" ``` lp15@66296 ` 1616` ``` proof ``` lp15@66296 ` 1617` ``` fix k::nat assume "N \ k" ``` lp15@66296 ` 1618` ``` have "x \ cbox (a + (b - a) /\<^sub>R (Suc k)) (b - (b - a) /\<^sub>R (Suc k))" ``` lp15@66296 ` 1619` ``` by (metis \N \ k\ le_Suc_eq N) ``` lp15@66296 ` 1620` ``` then show "?\ k x = f x \ j - g x" ``` lp15@66296 ` 1621` ``` by simp ``` lp15@66296 ` 1622` ``` qed ``` lp15@66296 ` 1623` ``` qed ``` lp15@66296 ` 1624` ``` have "\integral (box a b) ``` lp15@66296 ` 1625` ``` (\x. if x \ cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k)) ``` lp15@66296 ` 1626` ``` then f x \ j - g x else 0)\ \ Bf + Bg" for k ``` lp15@66296 ` 1627` ``` proof - ``` lp15@66296 ` 1628` ``` let ?I = "cbox (a + (b - a) /\<^sub>R (1 + real k)) (b - (b - a) /\<^sub>R (1 + real k))" ``` lp15@66296 ` 1629` ``` have I_int [simp]: "?I \ box a b = ?I" ``` lp15@66296 ` 1630` ``` using 1 by (simp add: Int_absorb2) ``` lp15@66296 ` 1631` ``` have int_fI: "f integrable_on ?I" ``` lp15@66296 ` 1632` ``` apply (rule integrable_subinterval [OF int_f order_refl]) ``` lp15@66296 ` 1633` ``` using "*" box_subset_cbox by blast ``` lp15@66296 ` 1634` ``` then have "(\x. f x \ j) integrable_on ?I" ``` lp15@66296 ` 1635` ``` by (simp add: integrable_component) ``` lp15@66296 ` 1636` ``` moreover have "g integrable_on ?I" ``` lp15@66296 ` 1637` ``` apply (rule integrable_subinterval [OF int_gab]) ``` lp15@66296 ` 1638` ``` using "*" box_subset_cbox by blast ``` lp15@66296 ` 1639` ``` moreover ``` lp15@66296 ` 1640` ``` have "\integral ?I (\x. f x \ j)\ \ norm (integral ?I f)" ``` lp15@66296 ` 1641` ``` by (simp add: Basis_le_norm int_fI \j \ Basis\) ``` lp15@66296 ` 1642` ``` with 1 I_int have "\integral ?I (\x. f x \ j)\ \ Bf" ``` lp15@66296 ` 1643` ``` by (blast intro: order_trans [OF _ Bf]) ``` lp15@66296 ` 1644` ``` ultimately show ?thesis ``` lp15@66296 ` 1645` ``` apply (simp add: integral_restrict_Int integral_diff) ``` lp15@66296 ` 1646` ``` using "*" box_subset_cbox by (blast intro: Bg add_mono order_trans [OF abs_triangle_ineq4]) ``` lp15@66296 ` 1647` ``` qed ``` lp15@66408 ` 1648` ``` then show "bounded (range (\k. integral (box a b) (?\ k)))" ``` lp15@66296 ` 1649` ``` apply (simp add: bounded_pos) ``` lp15@66296 ` 1650` ``` apply (rule_tac x="Bf+Bg" in exI) ``` lp15@66296 ` 1651` ``` using \0 < Bf\ \0 < Bg\ by auto ``` lp15@66296 ` 1652` ``` qed ``` lp15@66296 ` 1653` ``` then show "(\x. f x \ j - g x) integrable_on cbox a b" ``` lp15@66296 ` 1654` ``` by (simp add: integrable_on_open_interval) ``` lp15@66296 ` 1655` ``` qed ``` lp15@66296 ` 1656` ``` ultimately have "(\x. f x \ j) integrable_on cbox a b" ``` lp15@66296 ` 1657` ``` by auto ``` lp15@66296 ` 1658` ``` then show ?thesis ``` lp15@66296 ` 1659` ``` apply (rule absolutely_integrable_component_lbound [OF absint_g]) ``` lp15@66296 ` 1660` ``` by (simp add: gf) ``` lp15@66296 ` 1661` ``` qed ``` lp15@66296 ` 1662` ``` qed ``` lp15@66296 ` 1663` ```qed ``` lp15@66296 ` 1664` lp15@66296 ` 1665` ```end ``` nipkow@67399 ` 1666` ``` ```