src/HOL/Probability/Lebesgue_Measure.thy
 author hoelzl Wed Dec 01 19:20:30 2010 +0100 (2010-12-01) changeset 40859 de0b30e6c2d2 parent 38656 d5d342611edb child 40871 688f6ff859e1 permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
 hoelzl@40859 ` 1` ```(* Author: Robert Himmelmann, TU Muenchen *) ``` hoelzl@38656 ` 2` ```header {* Lebsegue measure *} ``` hoelzl@38656 ` 3` ```theory Lebesgue_Measure ``` hoelzl@40859 ` 4` ``` imports Product_Measure Gauge_Measure Complete_Measure ``` hoelzl@38656 ` 5` ```begin ``` hoelzl@38656 ` 6` hoelzl@40859 ` 7` ```lemma (in complete_lattice) SUP_pair: ``` hoelzl@40859 ` 8` ``` "(SUP i:A. SUP j:B. f i j) = (SUP p:A\B. (\ (i, j). f i j) p)" (is "?l = ?r") ``` hoelzl@40859 ` 9` ```proof (intro antisym SUP_leI) ``` hoelzl@40859 ` 10` ``` fix i j assume "i \ A" "j \ B" ``` hoelzl@40859 ` 11` ``` then have "(case (i,j) of (i,j) \ f i j) \ ?r" ``` hoelzl@40859 ` 12` ``` by (intro SUPR_upper) auto ``` hoelzl@40859 ` 13` ``` then show "f i j \ ?r" by auto ``` hoelzl@40859 ` 14` ```next ``` hoelzl@40859 ` 15` ``` fix p assume "p \ A \ B" ``` hoelzl@40859 ` 16` ``` then obtain i j where "p = (i,j)" "i \ A" "j \ B" by auto ``` hoelzl@40859 ` 17` ``` have "f i j \ (SUP j:B. f i j)" using `j \ B` by (intro SUPR_upper) ``` hoelzl@40859 ` 18` ``` also have "(SUP j:B. f i j) \ ?l" using `i \ A` by (intro SUPR_upper) ``` hoelzl@40859 ` 19` ``` finally show "(case p of (i, j) \ f i j) \ ?l" using `p = (i,j)` by simp ``` hoelzl@40859 ` 20` ```qed ``` hoelzl@38656 ` 21` hoelzl@40859 ` 22` ```lemma (in complete_lattice) SUP_surj_compose: ``` hoelzl@40859 ` 23` ``` assumes *: "f`A = B" shows "SUPR A (g \ f) = SUPR B g" ``` hoelzl@40859 ` 24` ``` unfolding SUPR_def unfolding *[symmetric] ``` hoelzl@40859 ` 25` ``` by (simp add: image_compose) ``` hoelzl@40859 ` 26` hoelzl@40859 ` 27` ```lemma (in complete_lattice) SUP_swap: ``` hoelzl@40859 ` 28` ``` "(SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)" ``` hoelzl@40859 ` 29` ```proof - ``` hoelzl@40859 ` 30` ``` have *: "(\(i,j). (j,i)) ` (B \ A) = A \ B" by auto ``` hoelzl@40859 ` 31` ``` show ?thesis ``` hoelzl@40859 ` 32` ``` unfolding SUP_pair SUP_surj_compose[symmetric, OF *] ``` hoelzl@40859 ` 33` ``` by (auto intro!: arg_cong[where f=Sup] image_eqI simp: comp_def SUPR_def) ``` hoelzl@40859 ` 34` ```qed ``` hoelzl@38656 ` 35` hoelzl@40859 ` 36` ```lemma SUP_\: "(SUP i:A. f i) = \ \ (\x<\. \i\A. x < f i)" ``` hoelzl@40859 ` 37` ```proof ``` hoelzl@40859 ` 38` ``` assume *: "(SUP i:A. f i) = \" ``` hoelzl@40859 ` 39` ``` show "(\x<\. \i\A. x < f i)" unfolding *[symmetric] ``` hoelzl@40859 ` 40` ``` proof (intro allI impI) ``` hoelzl@40859 ` 41` ``` fix x assume "x < SUPR A f" then show "\i\A. x < f i" ``` hoelzl@40859 ` 42` ``` unfolding less_SUP_iff by auto ``` hoelzl@40859 ` 43` ``` qed ``` hoelzl@40859 ` 44` ```next ``` hoelzl@40859 ` 45` ``` assume *: "\x<\. \i\A. x < f i" ``` hoelzl@40859 ` 46` ``` show "(SUP i:A. f i) = \" ``` hoelzl@40859 ` 47` ``` proof (rule pinfreal_SUPI) ``` hoelzl@40859 ` 48` ``` fix y assume **: "\i. i \ A \ f i \ y" ``` hoelzl@40859 ` 49` ``` show "\ \ y" ``` hoelzl@40859 ` 50` ``` proof cases ``` hoelzl@40859 ` 51` ``` assume "y < \" ``` hoelzl@40859 ` 52` ``` from *[THEN spec, THEN mp, OF this] ``` hoelzl@40859 ` 53` ``` obtain i where "i \ A" "\ (f i \ y)" by auto ``` hoelzl@40859 ` 54` ``` with ** show ?thesis by auto ``` hoelzl@40859 ` 55` ``` qed auto ``` hoelzl@40859 ` 56` ``` qed auto ``` hoelzl@40859 ` 57` ```qed ``` hoelzl@38656 ` 58` hoelzl@40859 ` 59` ```lemma psuminf_commute: ``` hoelzl@40859 ` 60` ``` shows "(\\<^isub>\ i j. f i j) = (\\<^isub>\ j i. f i j)" ``` hoelzl@40859 ` 61` ```proof - ``` hoelzl@40859 ` 62` ``` have "(SUP n. \ i < n. SUP m. \ j < m. f i j) = (SUP n. SUP m. \ i < n. \ j < m. f i j)" ``` hoelzl@40859 ` 63` ``` apply (subst SUPR_pinfreal_setsum) ``` hoelzl@40859 ` 64` ``` by auto ``` hoelzl@40859 ` 65` ``` also have "\ = (SUP m n. \ j < m. \ i < n. f i j)" ``` hoelzl@40859 ` 66` ``` apply (subst SUP_swap) ``` hoelzl@40859 ` 67` ``` apply (subst setsum_commute) ``` hoelzl@40859 ` 68` ``` by auto ``` hoelzl@40859 ` 69` ``` also have "\ = (SUP m. \ j < m. SUP n. \ i < n. f i j)" ``` hoelzl@40859 ` 70` ``` apply (subst SUPR_pinfreal_setsum) ``` hoelzl@40859 ` 71` ``` by auto ``` hoelzl@40859 ` 72` ``` finally show ?thesis ``` hoelzl@40859 ` 73` ``` unfolding psuminf_def by auto ``` hoelzl@40859 ` 74` ```qed ``` hoelzl@40859 ` 75` hoelzl@40859 ` 76` ```lemma psuminf_SUP_eq: ``` hoelzl@40859 ` 77` ``` assumes "\n i. f n i \ f (Suc n) i" ``` hoelzl@40859 ` 78` ``` shows "(\\<^isub>\ i. SUP n::nat. f n i) = (SUP n::nat. \\<^isub>\ i. f n i)" ``` hoelzl@40859 ` 79` ```proof - ``` hoelzl@40859 ` 80` ``` { fix n :: nat ``` hoelzl@40859 ` 81` ``` have "(\ii 'a::ordered_euclidean_space set" where ``` hoelzl@40859 ` 93` ``` "cube n \ {\\ i. - real n .. \\ i. real n}" ``` hoelzl@40859 ` 94` hoelzl@40859 ` 95` ```lemma cube_closed[intro]: "closed (cube n)" ``` hoelzl@40859 ` 96` ``` unfolding cube_def by auto ``` hoelzl@40859 ` 97` hoelzl@40859 ` 98` ```lemma cube_subset[intro]: "n \ N \ cube n \ cube N" ``` hoelzl@40859 ` 99` ``` by (fastsimp simp: eucl_le[where 'a='a] cube_def) ``` hoelzl@38656 ` 100` hoelzl@40859 ` 101` ```lemma cube_subset_iff: ``` hoelzl@40859 ` 102` ``` "cube n \ cube N \ n \ N" ``` hoelzl@40859 ` 103` ```proof ``` hoelzl@40859 ` 104` ``` assume subset: "cube n \ (cube N::'a set)" ``` hoelzl@40859 ` 105` ``` then have "((\\ i. real n)::'a) \ cube N" ``` hoelzl@40859 ` 106` ``` using DIM_positive[where 'a='a] ``` hoelzl@40859 ` 107` ``` by (fastsimp simp: cube_def eucl_le[where 'a='a]) ``` hoelzl@40859 ` 108` ``` then show "n \ N" ``` hoelzl@40859 ` 109` ``` by (fastsimp simp: cube_def eucl_le[where 'a='a]) ``` hoelzl@40859 ` 110` ```next ``` hoelzl@40859 ` 111` ``` assume "n \ N" then show "cube n \ (cube N::'a set)" by (rule cube_subset) ``` hoelzl@40859 ` 112` ```qed ``` hoelzl@38656 ` 113` hoelzl@38656 ` 114` ```lemma ball_subset_cube:"ball (0::'a::ordered_euclidean_space) (real n) \ cube n" ``` hoelzl@38656 ` 115` ``` unfolding cube_def subset_eq mem_interval apply safe unfolding euclidean_lambda_beta' ``` hoelzl@38656 ` 116` ```proof- fix x::'a and i assume as:"x\ball 0 (real n)" "i x \$\$ i" "real n \ x \$\$ i" ``` hoelzl@38656 ` 118` ``` using component_le_norm[of x i] by(auto simp: dist_norm) ``` hoelzl@38656 ` 119` ```qed ``` hoelzl@38656 ` 120` hoelzl@38656 ` 121` ```lemma mem_big_cube: obtains n where "x \ cube n" ``` hoelzl@38656 ` 122` ```proof- from real_arch_lt[of "norm x"] guess n .. ``` hoelzl@38656 ` 123` ``` thus ?thesis apply-apply(rule that[where n=n]) ``` hoelzl@38656 ` 124` ``` apply(rule ball_subset_cube[unfolded subset_eq,rule_format]) ``` hoelzl@38656 ` 125` ``` by (auto simp add:dist_norm) ``` hoelzl@38656 ` 126` ```qed ``` hoelzl@38656 ` 127` hoelzl@38656 ` 128` ```lemma Union_inter_cube:"\{s \ cube n |n. n \ UNIV} = s" ``` hoelzl@38656 ` 129` ```proof safe case goal1 ``` hoelzl@38656 ` 130` ``` from mem_big_cube[of x] guess n . note n=this ``` hoelzl@38656 ` 131` ``` show ?case unfolding Union_iff apply(rule_tac x="s \ cube n" in bexI) ``` hoelzl@38656 ` 132` ``` using n goal1 by auto ``` hoelzl@38656 ` 133` ```qed ``` hoelzl@38656 ` 134` hoelzl@38656 ` 135` ```lemma gmeasurable_cube[intro]:"gmeasurable (cube n)" ``` hoelzl@38656 ` 136` ``` unfolding cube_def by auto ``` hoelzl@38656 ` 137` hoelzl@38656 ` 138` ```lemma gmeasure_le_inter_cube[intro]: fixes s::"'a::ordered_euclidean_space set" ``` hoelzl@38656 ` 139` ``` assumes "gmeasurable (s \ cube n)" shows "gmeasure (s \ cube n) \ gmeasure (cube n::'a set)" ``` hoelzl@38656 ` 140` ``` apply(rule has_gmeasure_subset[of "s\cube n" _ "cube n"]) ``` hoelzl@38656 ` 141` ``` unfolding has_gmeasure_measure[THEN sym] using assms by auto ``` hoelzl@38656 ` 142` hoelzl@40859 ` 143` ```lemma has_gmeasure_cube[intro]: "(cube n::('a::ordered_euclidean_space) set) ``` hoelzl@40859 ` 144` ``` has_gmeasure ((2 * real n) ^ (DIM('a)))" ``` hoelzl@40859 ` 145` ```proof- ``` hoelzl@40859 ` 146` ``` have "content {\\ i. - real n..(\\ i. real n)::'a} = (2 * real n) ^ (DIM('a))" ``` hoelzl@40859 ` 147` ``` apply(subst content_closed_interval) defer ``` hoelzl@40859 ` 148` ``` by (auto simp add:setprod_constant) ``` hoelzl@40859 ` 149` ``` thus ?thesis unfolding cube_def ``` hoelzl@40859 ` 150` ``` using has_gmeasure_interval(1)[of "(\\ i. - real n)::'a" "(\\ i. real n)::'a"] ``` hoelzl@40859 ` 151` ``` by auto ``` hoelzl@40859 ` 152` ```qed ``` hoelzl@40859 ` 153` hoelzl@40859 ` 154` ```lemma gmeasure_cube_eq[simp]: ``` hoelzl@40859 ` 155` ``` "gmeasure (cube n::('a::ordered_euclidean_space) set) = (2 * real n) ^ DIM('a)" ``` hoelzl@40859 ` 156` ``` by (intro measure_unique) auto ``` hoelzl@40859 ` 157` hoelzl@40859 ` 158` ```lemma gmeasure_cube_ge_n: "gmeasure (cube n::('a::ordered_euclidean_space) set) \ real n" ``` hoelzl@40859 ` 159` ```proof cases ``` hoelzl@40859 ` 160` ``` assume "n = 0" then show ?thesis by simp ``` hoelzl@40859 ` 161` ```next ``` hoelzl@40859 ` 162` ``` assume "n \ 0" ``` hoelzl@40859 ` 163` ``` have "real n \ (2 * real n)^1" by simp ``` hoelzl@40859 ` 164` ``` also have "\ \ (2 * real n)^DIM('a)" ``` hoelzl@40859 ` 165` ``` using DIM_positive[where 'a='a] `n \ 0` ``` hoelzl@40859 ` 166` ``` by (intro power_increasing) auto ``` hoelzl@40859 ` 167` ``` also have "\ = gmeasure (cube n::'a set)" by simp ``` hoelzl@40859 ` 168` ``` finally show ?thesis . ``` hoelzl@40859 ` 169` ```qed ``` hoelzl@40859 ` 170` hoelzl@40859 ` 171` ```lemma gmeasure_setsum: ``` hoelzl@40859 ` 172` ``` assumes "finite A" and "\s t. s \ A \ t \ A \ s \ t \ f s \ f t = {}" ``` hoelzl@40859 ` 173` ``` and "\i. i \ A \ gmeasurable (f i)" ``` hoelzl@40859 ` 174` ``` shows "gmeasure (\i\A. f i) = (\i\A. gmeasure (f i))" ``` hoelzl@40859 ` 175` ```proof - ``` hoelzl@40859 ` 176` ``` have "gmeasure (\i\A. f i) = gmeasure (\f ` A)" by auto ``` hoelzl@40859 ` 177` ``` also have "\ = setsum gmeasure (f ` A)" using assms ``` hoelzl@40859 ` 178` ``` proof (intro measure_negligible_unions) ``` hoelzl@40859 ` 179` ``` fix X Y assume "X \ f`A" "Y \ f`A" "X \ Y" ``` hoelzl@40859 ` 180` ``` then have "X \ Y = {}" using assms by auto ``` hoelzl@40859 ` 181` ``` then show "negligible (X \ Y)" by auto ``` hoelzl@40859 ` 182` ``` qed auto ``` hoelzl@40859 ` 183` ``` also have "\ = setsum gmeasure (f ` A - {{}})" ``` hoelzl@40859 ` 184` ``` using assms by (intro setsum_mono_zero_cong_right) auto ``` hoelzl@40859 ` 185` ``` also have "\ = (\i\A - {i. f i = {}}. gmeasure (f i))" ``` hoelzl@40859 ` 186` ``` proof (intro setsum_reindex_cong inj_onI) ``` hoelzl@40859 ` 187` ``` fix s t assume *: "s \ A - {i. f i = {}}" "t \ A - {i. f i = {}}" "f s = f t" ``` hoelzl@40859 ` 188` ``` show "s = t" ``` hoelzl@40859 ` 189` ``` proof (rule ccontr) ``` hoelzl@40859 ` 190` ``` assume "s \ t" with assms(2)[of s t] * show False by auto ``` hoelzl@40859 ` 191` ``` qed ``` hoelzl@40859 ` 192` ``` qed auto ``` hoelzl@40859 ` 193` ``` also have "\ = (\i\A. gmeasure (f i))" ``` hoelzl@40859 ` 194` ``` using assms by (intro setsum_mono_zero_cong_left) auto ``` hoelzl@40859 ` 195` ``` finally show ?thesis . ``` hoelzl@40859 ` 196` ```qed ``` hoelzl@40859 ` 197` hoelzl@40859 ` 198` ```lemma gmeasurable_finite_UNION[intro]: ``` hoelzl@40859 ` 199` ``` assumes "\i. i \ S \ gmeasurable (A i)" "finite S" ``` hoelzl@40859 ` 200` ``` shows "gmeasurable (\i\S. A i)" ``` hoelzl@40859 ` 201` ``` unfolding UNION_eq_Union_image using assms ``` hoelzl@40859 ` 202` ``` by (intro gmeasurable_finite_unions) auto ``` hoelzl@40859 ` 203` hoelzl@40859 ` 204` ```lemma gmeasurable_countable_UNION[intro]: ``` hoelzl@40859 ` 205` ``` fixes A :: "nat \ ('a::ordered_euclidean_space) set" ``` hoelzl@40859 ` 206` ``` assumes measurable: "\i. gmeasurable (A i)" ``` hoelzl@40859 ` 207` ``` and finite: "\n. gmeasure (UNION {.. n} A) \ B" ``` hoelzl@40859 ` 208` ``` shows "gmeasurable (\i. A i)" ``` hoelzl@40859 ` 209` ```proof - ``` hoelzl@40859 ` 210` ``` have *: "\n. \{A k |k. k \ n} = (\i\n. A i)" ``` hoelzl@40859 ` 211` ``` "(\{A n |n. n \ UNIV}) = (\i. A i)" by auto ``` hoelzl@40859 ` 212` ``` show ?thesis ``` hoelzl@40859 ` 213` ``` by (rule gmeasurable_countable_unions_strong[of A B, unfolded *, OF assms]) ``` hoelzl@40859 ` 214` ```qed ``` hoelzl@38656 ` 215` hoelzl@38656 ` 216` ```subsection {* Measurability *} ``` hoelzl@38656 ` 217` hoelzl@40859 ` 218` ```definition lebesgue :: "'a::ordered_euclidean_space algebra" where ``` hoelzl@40859 ` 219` ``` "lebesgue = \ space = UNIV, sets = {A. \n. gmeasurable (A \ cube n)} \" ``` hoelzl@40859 ` 220` hoelzl@40859 ` 221` ```lemma space_lebesgue[simp]:"space lebesgue = UNIV" ``` hoelzl@40859 ` 222` ``` unfolding lebesgue_def by auto ``` hoelzl@38656 ` 223` hoelzl@40859 ` 224` ```lemma lebesgueD[dest]: assumes "S \ sets lebesgue" ``` hoelzl@40859 ` 225` ``` shows "\n. gmeasurable (S \ cube n)" ``` hoelzl@40859 ` 226` ``` using assms unfolding lebesgue_def by auto ``` hoelzl@38656 ` 227` hoelzl@40859 ` 228` ```lemma lebesgueI[intro]: assumes "gmeasurable S" ``` hoelzl@40859 ` 229` ``` shows "S \ sets lebesgue" unfolding lebesgue_def cube_def ``` hoelzl@38656 ` 230` ``` using assms gmeasurable_interval by auto ``` hoelzl@38656 ` 231` hoelzl@40859 ` 232` ```lemma lebesgueI2: "(\n. gmeasurable (S \ cube n)) \ S \ sets lebesgue" ``` hoelzl@40859 ` 233` ``` using assms unfolding lebesgue_def by auto ``` hoelzl@38656 ` 234` hoelzl@40859 ` 235` ```interpretation lebesgue: sigma_algebra lebesgue ``` hoelzl@40859 ` 236` ```proof ``` hoelzl@40859 ` 237` ``` show "sets lebesgue \ Pow (space lebesgue)" ``` hoelzl@40859 ` 238` ``` unfolding lebesgue_def by auto ``` hoelzl@40859 ` 239` ``` show "{} \ sets lebesgue" ``` hoelzl@40859 ` 240` ``` using gmeasurable_empty by auto ``` hoelzl@40859 ` 241` ``` { fix A B :: "'a set" assume "A \ sets lebesgue" "B \ sets lebesgue" ``` hoelzl@40859 ` 242` ``` then show "A \ B \ sets lebesgue" ``` hoelzl@40859 ` 243` ``` by (auto intro: gmeasurable_union simp: lebesgue_def Int_Un_distrib2) } ``` hoelzl@40859 ` 244` ``` { fix A :: "nat \ 'a set" assume A: "range A \ sets lebesgue" ``` hoelzl@40859 ` 245` ``` show "(\i. A i) \ sets lebesgue" ``` hoelzl@40859 ` 246` ``` proof (rule lebesgueI2) ``` hoelzl@40859 ` 247` ``` fix n show "gmeasurable ((\i. A i) \ cube n)" unfolding UN_extend_simps ``` hoelzl@40859 ` 248` ``` using A ``` hoelzl@40859 ` 249` ``` by (intro gmeasurable_countable_UNION[where B="gmeasure (cube n::'a set)"]) ``` hoelzl@40859 ` 250` ``` (auto intro!: measure_subset gmeasure_setsum simp: UN_extend_simps simp del: gmeasure_cube_eq UN_simps) ``` hoelzl@40859 ` 251` ``` qed } ``` hoelzl@40859 ` 252` ``` { fix A assume A: "A \ sets lebesgue" show "space lebesgue - A \ sets lebesgue" ``` hoelzl@40859 ` 253` ``` proof (rule lebesgueI2) ``` hoelzl@40859 ` 254` ``` fix n ``` hoelzl@40859 ` 255` ``` have *: "(space lebesgue - A) \ cube n = cube n - (A \ cube n)" ``` hoelzl@40859 ` 256` ``` unfolding lebesgue_def by auto ``` hoelzl@40859 ` 257` ``` show "gmeasurable ((space lebesgue - A) \ cube n)" unfolding * ``` hoelzl@40859 ` 258` ``` using A by (auto intro!: gmeasurable_diff) ``` hoelzl@40859 ` 259` ``` qed } ``` hoelzl@38656 ` 260` ```qed ``` hoelzl@38656 ` 261` hoelzl@40859 ` 262` ```lemma lebesgueI_borel[intro, simp]: fixes s::"'a::ordered_euclidean_space set" ``` hoelzl@40859 ` 263` ``` assumes "s \ sets borel" shows "s \ sets lebesgue" ``` hoelzl@40859 ` 264` ```proof- let ?S = "range (\(a, b). {a .. (b :: 'a\ordered_euclidean_space)})" ``` hoelzl@40859 ` 265` ``` have *:"?S \ sets lebesgue" by auto ``` hoelzl@40859 ` 266` ``` have "s \ sigma_sets UNIV ?S" using assms ``` hoelzl@40859 ` 267` ``` unfolding borel_eq_atLeastAtMost by (simp add: sigma_def) ``` hoelzl@40859 ` 268` ``` thus ?thesis ``` hoelzl@40859 ` 269` ``` using lebesgue.sigma_subset[of "\ space = UNIV, sets = ?S\", simplified, OF *] ``` hoelzl@40859 ` 270` ``` by (auto simp: sigma_def) ``` hoelzl@38656 ` 271` ```qed ``` hoelzl@38656 ` 272` hoelzl@40859 ` 273` ```lemma lebesgueI_negligible[dest]: fixes s::"'a::ordered_euclidean_space set" ``` hoelzl@40859 ` 274` ``` assumes "negligible s" shows "s \ sets lebesgue" ``` hoelzl@40859 ` 275` ```proof (rule lebesgueI2) ``` hoelzl@40859 ` 276` ``` fix n ``` hoelzl@38656 ` 277` ``` have *:"\x. (if x \ cube n then indicator s x else 0) = (if x \ s \ cube n then 1 else 0)" ``` hoelzl@38656 ` 278` ``` unfolding indicator_def_raw by auto ``` hoelzl@38656 ` 279` ``` note assms[unfolded negligible_def,rule_format,of "(\\ i. - real n)::'a" "\\ i. real n"] ``` hoelzl@40859 ` 280` ``` thus "gmeasurable (s \ cube n)" apply-apply(rule gmeasurableI[of _ 0]) unfolding has_gmeasure_def ``` hoelzl@38656 ` 281` ``` apply(subst(asm) has_integral_restrict_univ[THEN sym]) unfolding cube_def[symmetric] ``` hoelzl@38656 ` 282` ``` apply(subst has_integral_restrict_univ[THEN sym]) unfolding * . ``` hoelzl@38656 ` 283` ```qed ``` hoelzl@38656 ` 284` hoelzl@38656 ` 285` ```section {* The Lebesgue Measure *} ``` hoelzl@38656 ` 286` hoelzl@40859 ` 287` ```definition "lmeasure A = (SUP n. Real (gmeasure (A \ cube n)))" ``` hoelzl@38656 ` 288` hoelzl@40859 ` 289` ```lemma lmeasure_eq_0: assumes "negligible S" shows "lmeasure S = 0" ``` hoelzl@40859 ` 290` ```proof - ``` hoelzl@40859 ` 291` ``` from lebesgueI_negligible[OF assms] ``` hoelzl@40859 ` 292` ``` have "\n. gmeasurable (S \ cube n)" by auto ``` hoelzl@40859 ` 293` ``` from gmeasurable_measure_eq_0[OF this] ``` hoelzl@40859 ` 294` ``` have "\n. gmeasure (S \ cube n) = 0" using assms by auto ``` hoelzl@40859 ` 295` ``` then show ?thesis unfolding lmeasure_def by simp ``` hoelzl@40859 ` 296` ```qed ``` hoelzl@40859 ` 297` hoelzl@40859 ` 298` ```lemma lmeasure_iff_LIMSEQ: ``` hoelzl@40859 ` 299` ``` assumes "A \ sets lebesgue" "0 \ m" ``` hoelzl@40859 ` 300` ``` shows "lmeasure A = Real m \ (\n. (gmeasure (A \ cube n))) ----> m" ``` hoelzl@40859 ` 301` ``` unfolding lmeasure_def using assms cube_subset[where 'a='a] ``` hoelzl@40859 ` 302` ``` by (intro SUP_eq_LIMSEQ monoI measure_subset) force+ ``` hoelzl@38656 ` 303` hoelzl@40859 ` 304` ```interpretation lebesgue: measure_space lebesgue lmeasure ``` hoelzl@40859 ` 305` ```proof ``` hoelzl@40859 ` 306` ``` show "lmeasure {} = 0" ``` hoelzl@40859 ` 307` ``` by (auto intro!: lmeasure_eq_0) ``` hoelzl@40859 ` 308` ``` show "countably_additive lebesgue lmeasure" ``` hoelzl@40859 ` 309` ``` proof (unfold countably_additive_def, intro allI impI conjI) ``` hoelzl@40859 ` 310` ``` fix A :: "nat \ 'b set" assume "range A \ sets lebesgue" "disjoint_family A" ``` hoelzl@40859 ` 311` ``` then have A: "\i. A i \ sets lebesgue" by auto ``` hoelzl@40859 ` 312` ``` show "(\\<^isub>\n. lmeasure (A n)) = lmeasure (\i. A i)" unfolding lmeasure_def ``` hoelzl@40859 ` 313` ``` proof (subst psuminf_SUP_eq) ``` hoelzl@40859 ` 314` ``` { fix i n ``` hoelzl@40859 ` 315` ``` have "gmeasure (A i \ cube n) \ gmeasure (A i \ cube (Suc n))" ``` hoelzl@40859 ` 316` ``` using A cube_subset[of n "Suc n"] by (auto intro!: measure_subset) ``` hoelzl@40859 ` 317` ``` then show "Real (gmeasure (A i \ cube n)) \ Real (gmeasure (A i \ cube (Suc n)))" ``` hoelzl@40859 ` 318` ``` by auto } ``` hoelzl@40859 ` 319` ``` show "(SUP n. \\<^isub>\i. Real (gmeasure (A i \ cube n))) = (SUP n. Real (gmeasure ((\i. A i) \ cube n)))" ``` hoelzl@40859 ` 320` ``` proof (intro arg_cong[where f="SUPR UNIV"] ext) ``` hoelzl@40859 ` 321` ``` fix n ``` hoelzl@40859 ` 322` ``` have sums: "(\i. gmeasure (A i \ cube n)) sums gmeasure (\{A i \ cube n |i. i \ UNIV})" ``` hoelzl@40859 ` 323` ``` proof (rule has_gmeasure_countable_negligible_unions(2)) ``` hoelzl@40859 ` 324` ``` fix i show "gmeasurable (A i \ cube n)" using A by auto ``` hoelzl@40859 ` 325` ``` next ``` hoelzl@40859 ` 326` ``` fix i m :: nat assume "m \ i" ``` hoelzl@40859 ` 327` ``` then have "A m \ cube n \ (A i \ cube n) = {}" ``` hoelzl@40859 ` 328` ``` using `disjoint_family A` unfolding disjoint_family_on_def by auto ``` hoelzl@40859 ` 329` ``` then show "negligible (A m \ cube n \ (A i \ cube n))" by auto ``` hoelzl@40859 ` 330` ``` next ``` hoelzl@40859 ` 331` ``` fix i ``` hoelzl@40859 ` 332` ``` have "(\k = 0..i. gmeasure (A k \ cube n)) = gmeasure (\k\i . A k \ cube n)" ``` hoelzl@40859 ` 333` ``` unfolding atLeast0AtMost using A ``` hoelzl@40859 ` 334` ``` proof (intro gmeasure_setsum[symmetric]) ``` hoelzl@40859 ` 335` ``` fix s t :: nat assume "s \ t" then have "A t \ A s = {}" ``` hoelzl@40859 ` 336` ``` using `disjoint_family A` unfolding disjoint_family_on_def by auto ``` hoelzl@40859 ` 337` ``` then show "A s \ cube n \ (A t \ cube n) = {}" by auto ``` hoelzl@40859 ` 338` ``` qed auto ``` hoelzl@40859 ` 339` ``` also have "\ \ gmeasure (cube n :: 'b set)" using A ``` hoelzl@40859 ` 340` ``` by (intro measure_subset gmeasurable_finite_UNION) auto ``` hoelzl@40859 ` 341` ``` finally show "(\k = 0..i. gmeasure (A k \ cube n)) \ gmeasure (cube n :: 'b set)" . ``` hoelzl@40859 ` 342` ``` qed ``` hoelzl@40859 ` 343` ``` show "(\\<^isub>\i. Real (gmeasure (A i \ cube n))) = Real (gmeasure ((\i. A i) \ cube n))" ``` hoelzl@40859 ` 344` ``` unfolding psuminf_def ``` hoelzl@40859 ` 345` ``` apply (subst setsum_Real) ``` hoelzl@40859 ` 346` ``` apply (simp add: measure_pos_le) ``` hoelzl@40859 ` 347` ``` proof (rule SUP_eq_LIMSEQ[THEN iffD2]) ``` hoelzl@40859 ` 348` ``` have "(\{A i \ cube n |i. i \ UNIV}) = (\i. A i) \ cube n" by auto ``` hoelzl@40859 ` 349` ``` with sums show "(\i. \k cube n)) ----> gmeasure ((\i. A i) \ cube n)" ``` hoelzl@40859 ` 350` ``` unfolding sums_def atLeast0LessThan by simp ``` hoelzl@40859 ` 351` ``` qed (auto intro!: monoI setsum_nonneg setsum_mono2) ``` hoelzl@40859 ` 352` ``` qed ``` hoelzl@40859 ` 353` ``` qed ``` hoelzl@40859 ` 354` ``` qed ``` hoelzl@40859 ` 355` ```qed ``` hoelzl@38656 ` 356` hoelzl@40859 ` 357` ```lemma lmeasure_finite_has_gmeasure: assumes "s \ sets lebesgue" "lmeasure s = Real m" "0 \ m" ``` hoelzl@38656 ` 358` ``` shows "s has_gmeasure m" ``` hoelzl@40859 ` 359` ```proof- ``` hoelzl@38656 ` 360` ``` have *:"(\n. (gmeasure (s \ cube n))) ----> m" ``` hoelzl@40859 ` 361` ``` using `lmeasure s = Real m` unfolding lmeasure_iff_LIMSEQ[OF `s \ sets lebesgue` `0 \ m`] . ``` hoelzl@40859 ` 362` ``` have s: "\n. gmeasurable (s \ cube n)" using assms by auto ``` hoelzl@38656 ` 363` ``` have "(\x. if x \ s then 1 else (0::real)) integrable_on UNIV \ ``` hoelzl@38656 ` 364` ``` (\k. integral UNIV (\x. if x \ s \ cube k then 1 else (0::real))) ``` hoelzl@38656 ` 365` ``` ----> integral UNIV (\x. if x \ s then 1 else 0)" ``` hoelzl@38656 ` 366` ``` proof(rule monotone_convergence_increasing) ``` hoelzl@40859 ` 367` ``` have "lmeasure s \ Real m" using `lmeasure s = Real m` by simp ``` hoelzl@40859 ` 368` ``` then have "\n. gmeasure (s \ cube n) \ m" ``` hoelzl@40859 ` 369` ``` unfolding lmeasure_def complete_lattice_class.SUP_le_iff ``` hoelzl@40859 ` 370` ``` using `0 \ m` by (auto simp: measure_pos_le) ``` hoelzl@40859 ` 371` ``` thus *:"bounded {integral UNIV (\x. if x \ s \ cube k then 1 else (0::real)) |k. True}" ``` hoelzl@40859 ` 372` ``` unfolding integral_measure_univ[OF s] bounded_def apply- ``` hoelzl@38656 ` 373` ``` apply(rule_tac x=0 in exI,rule_tac x=m in exI) unfolding dist_real_def ``` hoelzl@38656 ` 374` ``` by (auto simp: measure_pos_le) ``` hoelzl@38656 ` 375` ``` show "\k. (\x. if x \ s \ cube k then (1::real) else 0) integrable_on UNIV" ``` hoelzl@38656 ` 376` ``` unfolding integrable_restrict_univ ``` hoelzl@40859 ` 377` ``` using s unfolding gmeasurable_def has_gmeasure_def by auto ``` hoelzl@38656 ` 378` ``` have *:"\n. n \ Suc n" by auto ``` hoelzl@38656 ` 379` ``` show "\k. \x\UNIV. (if x \ s \ cube k then 1 else 0) \ (if x \ s \ cube (Suc k) then 1 else (0::real))" ``` hoelzl@38656 ` 380` ``` using cube_subset[OF *] by fastsimp ``` hoelzl@38656 ` 381` ``` show "\x\UNIV. (\k. if x \ s \ cube k then 1 else 0) ----> (if x \ s then 1 else (0::real))" ``` hoelzl@40859 ` 382` ``` unfolding Lim_sequentially ``` hoelzl@38656 ` 383` ``` proof safe case goal1 from real_arch_lt[of "norm x"] guess N .. note N = this ``` hoelzl@38656 ` 384` ``` show ?case apply(rule_tac x=N in exI) ``` hoelzl@38656 ` 385` ``` proof safe case goal1 ``` hoelzl@38656 ` 386` ``` have "x \ cube n" using cube_subset[OF goal1] N ``` hoelzl@40859 ` 387` ``` using ball_subset_cube[of N] by(auto simp: dist_norm) ``` hoelzl@38656 ` 388` ``` thus ?case using `e>0` by auto ``` hoelzl@38656 ` 389` ``` qed ``` hoelzl@38656 ` 390` ``` qed ``` hoelzl@38656 ` 391` ``` qed note ** = conjunctD2[OF this] ``` hoelzl@38656 ` 392` ``` hence *:"m = integral UNIV (\x. if x \ s then 1 else 0)" apply- ``` hoelzl@40859 ` 393` ``` apply(rule LIMSEQ_unique[OF _ **(2)]) unfolding measure_integral_univ[THEN sym,OF s] using * . ``` hoelzl@38656 ` 394` ``` show ?thesis unfolding has_gmeasure * apply(rule integrable_integral) using ** by auto ``` hoelzl@38656 ` 395` ```qed ``` hoelzl@38656 ` 396` hoelzl@40859 ` 397` ```lemma lmeasure_finite_gmeasurable: assumes "s \ sets lebesgue" "lmeasure s \ \" ``` hoelzl@38656 ` 398` ``` shows "gmeasurable s" ``` hoelzl@40859 ` 399` ```proof (cases "lmeasure s") ``` hoelzl@40859 ` 400` ``` case (preal m) from lmeasure_finite_has_gmeasure[OF `s \ sets lebesgue` this] ``` hoelzl@40859 ` 401` ``` show ?thesis unfolding gmeasurable_def by auto ``` hoelzl@40859 ` 402` ```qed (insert assms, auto) ``` hoelzl@38656 ` 403` hoelzl@40859 ` 404` ```lemma has_gmeasure_lmeasure: assumes "s has_gmeasure m" ``` hoelzl@40859 ` 405` ``` shows "lmeasure s = Real m" ``` hoelzl@40859 ` 406` ```proof- ``` hoelzl@40859 ` 407` ``` have gmea:"gmeasurable s" using assms by auto ``` hoelzl@40859 ` 408` ``` then have s: "s \ sets lebesgue" by auto ``` hoelzl@38656 ` 409` ``` have m:"m \ 0" using assms by auto ``` hoelzl@38656 ` 410` ``` have *:"m = gmeasure (\{s \ cube n |n. n \ UNIV})" unfolding Union_inter_cube ``` hoelzl@38656 ` 411` ``` using assms by(rule measure_unique[THEN sym]) ``` hoelzl@40859 ` 412` ``` show ?thesis ``` hoelzl@40859 ` 413` ``` unfolding lmeasure_iff_LIMSEQ[OF s `0 \ m`] unfolding * ``` hoelzl@38656 ` 414` ``` apply(rule gmeasurable_nested_unions[THEN conjunct2, where B1="gmeasure s"]) ``` hoelzl@38656 ` 415` ``` proof- fix n::nat show *:"gmeasurable (s \ cube n)" ``` hoelzl@38656 ` 416` ``` using gmeasurable_inter[OF gmea gmeasurable_cube] . ``` hoelzl@38656 ` 417` ``` show "gmeasure (s \ cube n) \ gmeasure s" apply(rule measure_subset) ``` hoelzl@38656 ` 418` ``` apply(rule * gmea)+ by auto ``` hoelzl@38656 ` 419` ``` show "s \ cube n \ s \ cube (Suc n)" using cube_subset[of n "Suc n"] by auto ``` hoelzl@38656 ` 420` ``` qed ``` hoelzl@38656 ` 421` ```qed ``` hoelzl@38656 ` 422` hoelzl@40859 ` 423` ```lemma has_gmeasure_iff_lmeasure: ``` hoelzl@40859 ` 424` ``` "A has_gmeasure m \ (A \ sets lebesgue \ 0 \ m \ lmeasure A = Real m)" ``` hoelzl@40859 ` 425` ```proof ``` hoelzl@40859 ` 426` ``` assume "A has_gmeasure m" ``` hoelzl@40859 ` 427` ``` with has_gmeasure_lmeasure[OF this] ``` hoelzl@40859 ` 428` ``` have "gmeasurable A" "0 \ m" "lmeasure A = Real m" by auto ``` hoelzl@40859 ` 429` ``` then show "A \ sets lebesgue \ 0 \ m \ lmeasure A = Real m" by auto ``` hoelzl@40859 ` 430` ```next ``` hoelzl@40859 ` 431` ``` assume "A \ sets lebesgue \ 0 \ m \ lmeasure A = Real m" ``` hoelzl@40859 ` 432` ``` then show "A has_gmeasure m" by (intro lmeasure_finite_has_gmeasure) auto ``` hoelzl@38656 ` 433` ```qed ``` hoelzl@38656 ` 434` hoelzl@40859 ` 435` ```lemma gmeasure_lmeasure: assumes "gmeasurable s" shows "lmeasure s = Real (gmeasure s)" ``` hoelzl@40859 ` 436` ```proof - ``` hoelzl@40859 ` 437` ``` note has_gmeasure_measureI[OF assms] ``` hoelzl@40859 ` 438` ``` note has_gmeasure_lmeasure[OF this] ``` hoelzl@40859 ` 439` ``` thus ?thesis . ``` hoelzl@40859 ` 440` ```qed ``` hoelzl@38656 ` 441` hoelzl@38656 ` 442` ```lemma lebesgue_simple_function_indicator: ``` hoelzl@38656 ` 443` ``` fixes f::"'a::ordered_euclidean_space \ pinfreal" ``` hoelzl@38656 ` 444` ``` assumes f:"lebesgue.simple_function f" ``` hoelzl@38656 ` 445` ``` shows "f = (\x. (\y \ f ` UNIV. y * indicator (f -` {y}) x))" ``` hoelzl@38656 ` 446` ``` apply(rule,subst lebesgue.simple_function_indicator_representation[OF f]) by auto ``` hoelzl@38656 ` 447` hoelzl@38656 ` 448` ```lemma lmeasure_gmeasure: ``` hoelzl@38656 ` 449` ``` "gmeasurable s \ gmeasure s = real (lmeasure s)" ``` hoelzl@40859 ` 450` ``` by (subst gmeasure_lmeasure) auto ``` hoelzl@38656 ` 451` hoelzl@38656 ` 452` ```lemma lmeasure_finite: assumes "gmeasurable s" shows "lmeasure s \ \" ``` hoelzl@38656 ` 453` ``` using gmeasure_lmeasure[OF assms] by auto ``` hoelzl@38656 ` 454` hoelzl@40859 ` 455` ```lemma negligible_iff_lebesgue_null_sets: ``` hoelzl@40859 ` 456` ``` "negligible A \ A \ lebesgue.null_sets" ``` hoelzl@40859 ` 457` ```proof ``` hoelzl@40859 ` 458` ``` assume "negligible A" ``` hoelzl@40859 ` 459` ``` from this[THEN lebesgueI_negligible] this[THEN lmeasure_eq_0] ``` hoelzl@40859 ` 460` ``` show "A \ lebesgue.null_sets" by auto ``` hoelzl@40859 ` 461` ```next ``` hoelzl@40859 ` 462` ``` assume A: "A \ lebesgue.null_sets" ``` hoelzl@40859 ` 463` ``` then have *:"gmeasurable A" using lmeasure_finite_gmeasurable[of A] by auto ``` hoelzl@40859 ` 464` ``` show "negligible A" ``` hoelzl@40859 ` 465` ``` unfolding gmeasurable_measure_eq_0[OF *, symmetric] ``` hoelzl@40859 ` 466` ``` unfolding lmeasure_gmeasure[OF *] using A by auto ``` hoelzl@40859 ` 467` ```qed ``` hoelzl@40859 ` 468` hoelzl@40859 ` 469` ```lemma ``` hoelzl@40859 ` 470` ``` fixes a b ::"'a::ordered_euclidean_space" ``` hoelzl@40859 ` 471` ``` shows lmeasure_atLeastAtMost[simp]: "lmeasure {a..b} = Real (content {a..b})" ``` hoelzl@40859 ` 472` ``` and lmeasure_greaterThanLessThan[simp]: "lmeasure {a <..< b} = Real (content {a..b})" ``` hoelzl@40859 ` 473` ``` using has_gmeasure_interval[of a b] by (auto intro!: has_gmeasure_lmeasure) ``` hoelzl@40859 ` 474` hoelzl@40859 ` 475` ```lemma lmeasure_cube: ``` hoelzl@40859 ` 476` ``` "lmeasure (cube n::('a::ordered_euclidean_space) set) = (Real ((2 * real n) ^ (DIM('a))))" ``` hoelzl@40859 ` 477` ``` by (intro has_gmeasure_lmeasure) auto ``` hoelzl@40859 ` 478` hoelzl@40859 ` 479` ```lemma lmeasure_UNIV[intro]: "lmeasure UNIV = \" ``` hoelzl@40859 ` 480` ``` unfolding lmeasure_def SUP_\ ``` hoelzl@40859 ` 481` ```proof (intro allI impI) ``` hoelzl@40859 ` 482` ``` fix x assume "x < \" ``` hoelzl@40859 ` 483` ``` then obtain r where r: "x = Real r" "0 \ r" by (cases x) auto ``` hoelzl@40859 ` 484` ``` then obtain n where n: "r < of_nat n" using ex_less_of_nat by auto ``` hoelzl@40859 ` 485` ``` show "\i\UNIV. x < Real (gmeasure (UNIV \ cube i))" ``` hoelzl@40859 ` 486` ``` proof (intro bexI[of _ n]) ``` hoelzl@40859 ` 487` ``` have "x < Real (of_nat n)" using n r by auto ``` hoelzl@40859 ` 488` ``` also have "Real (of_nat n) \ Real (gmeasure (UNIV \ cube n))" ``` hoelzl@40859 ` 489` ``` using gmeasure_cube_ge_n[of n] by (auto simp: real_eq_of_nat[symmetric]) ``` hoelzl@40859 ` 490` ``` finally show "x < Real (gmeasure (UNIV \ cube n))" . ``` hoelzl@40859 ` 491` ``` qed auto ``` hoelzl@40859 ` 492` ```qed ``` hoelzl@40859 ` 493` hoelzl@40859 ` 494` ```lemma atLeastAtMost_singleton_euclidean[simp]: ``` hoelzl@40859 ` 495` ``` fixes a :: "'a::ordered_euclidean_space" shows "{a .. a} = {a}" ``` hoelzl@40859 ` 496` ``` by (force simp: eucl_le[where 'a='a] euclidean_eq[where 'a='a]) ``` hoelzl@40859 ` 497` hoelzl@40859 ` 498` ```lemma content_singleton[simp]: "content {a} = 0" ``` hoelzl@40859 ` 499` ```proof - ``` hoelzl@40859 ` 500` ``` have "content {a .. a} = 0" ``` hoelzl@40859 ` 501` ``` by (subst content_closed_interval) auto ``` hoelzl@40859 ` 502` ``` then show ?thesis by simp ``` hoelzl@40859 ` 503` ```qed ``` hoelzl@40859 ` 504` hoelzl@40859 ` 505` ```lemma lmeasure_singleton[simp]: ``` hoelzl@40859 ` 506` ``` fixes a :: "'a::ordered_euclidean_space" shows "lmeasure {a} = 0" ``` hoelzl@40859 ` 507` ``` using has_gmeasure_interval[of a a] unfolding zero_pinfreal_def ``` hoelzl@40859 ` 508` ``` by (intro has_gmeasure_lmeasure) ``` hoelzl@40859 ` 509` ``` (simp add: content_closed_interval DIM_positive) ``` hoelzl@40859 ` 510` hoelzl@40859 ` 511` ```declare content_real[simp] ``` hoelzl@40859 ` 512` hoelzl@40859 ` 513` ```lemma ``` hoelzl@40859 ` 514` ``` fixes a b :: real ``` hoelzl@40859 ` 515` ``` shows lmeasure_real_greaterThanAtMost[simp]: ``` hoelzl@40859 ` 516` ``` "lmeasure {a <.. b} = Real (if a \ b then b - a else 0)" ``` hoelzl@40859 ` 517` ```proof cases ``` hoelzl@40859 ` 518` ``` assume "a < b" ``` hoelzl@40859 ` 519` ``` then have "lmeasure {a <.. b} = lmeasure {a <..< b} + lmeasure {b}" ``` hoelzl@40859 ` 520` ``` by (subst lebesgue.measure_additive) ``` hoelzl@40859 ` 521` ``` (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure]) ``` hoelzl@40859 ` 522` ``` then show ?thesis by auto ``` hoelzl@40859 ` 523` ```qed auto ``` hoelzl@40859 ` 524` hoelzl@40859 ` 525` ```lemma ``` hoelzl@40859 ` 526` ``` fixes a b :: real ``` hoelzl@40859 ` 527` ``` shows lmeasure_real_atLeastLessThan[simp]: ``` hoelzl@40859 ` 528` ``` "lmeasure {a ..< b} = Real (if a \ b then b - a else 0)" (is ?eqlt) ``` hoelzl@40859 ` 529` ```proof cases ``` hoelzl@40859 ` 530` ``` assume "a < b" ``` hoelzl@40859 ` 531` ``` then have "lmeasure {a ..< b} = lmeasure {a} + lmeasure {a <..< b}" ``` hoelzl@40859 ` 532` ``` by (subst lebesgue.measure_additive) ``` hoelzl@40859 ` 533` ``` (auto intro!: lebesgueI_borel arg_cong[where f=lmeasure]) ``` hoelzl@40859 ` 534` ``` then show ?thesis by auto ``` hoelzl@40859 ` 535` ```qed auto ``` hoelzl@40859 ` 536` hoelzl@40859 ` 537` ```interpretation borel: measure_space borel lmeasure ``` hoelzl@40859 ` 538` ```proof ``` hoelzl@40859 ` 539` ``` show "countably_additive borel lmeasure" ``` hoelzl@40859 ` 540` ``` using lebesgue.ca unfolding countably_additive_def ``` hoelzl@40859 ` 541` ``` apply safe apply (erule_tac x=A in allE) by auto ``` hoelzl@40859 ` 542` ```qed auto ``` hoelzl@40859 ` 543` hoelzl@40859 ` 544` ```interpretation borel: sigma_finite_measure borel lmeasure ``` hoelzl@40859 ` 545` ```proof (default, intro conjI exI[of _ "\n. cube n"]) ``` hoelzl@40859 ` 546` ``` show "range cube \ sets borel" by (auto intro: borel_closed) ``` hoelzl@40859 ` 547` ``` { fix x have "\n. x\cube n" using mem_big_cube by auto } ``` hoelzl@40859 ` 548` ``` thus "(\i. cube i) = space borel" by auto ``` hoelzl@40859 ` 549` ``` show "\i. lmeasure (cube i) \ \" unfolding lmeasure_cube by auto ``` hoelzl@40859 ` 550` ```qed ``` hoelzl@40859 ` 551` hoelzl@40859 ` 552` ```interpretation lebesgue: sigma_finite_measure lebesgue lmeasure ``` hoelzl@40859 ` 553` ```proof ``` hoelzl@40859 ` 554` ``` from borel.sigma_finite guess A .. ``` hoelzl@40859 ` 555` ``` moreover then have "range A \ sets lebesgue" using lebesgueI_borel by blast ``` hoelzl@40859 ` 556` ``` ultimately show "\A::nat \ 'b set. range A \ sets lebesgue \ (\i. A i) = space lebesgue \ (\i. lmeasure (A i) \ \)" ``` hoelzl@40859 ` 557` ``` by auto ``` hoelzl@40859 ` 558` ```qed ``` hoelzl@40859 ` 559` hoelzl@40859 ` 560` ```lemma simple_function_has_integral: ``` hoelzl@40859 ` 561` ``` fixes f::"'a::ordered_euclidean_space \ pinfreal" ``` hoelzl@40859 ` 562` ``` assumes f:"lebesgue.simple_function f" ``` hoelzl@40859 ` 563` ``` and f':"\x. f x \ \" ``` hoelzl@40859 ` 564` ``` and om:"\x\range f. lmeasure (f -` {x} \ UNIV) = \ \ x = 0" ``` hoelzl@40859 ` 565` ``` shows "((\x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV" ``` hoelzl@40859 ` 566` ``` unfolding lebesgue.simple_integral_def ``` hoelzl@40859 ` 567` ``` apply(subst lebesgue_simple_function_indicator[OF f]) ``` hoelzl@40859 ` 568` ```proof- case goal1 ``` hoelzl@40859 ` 569` ``` have *:"\x. \y\range f. y * indicator (f -` {y}) x \ \" ``` hoelzl@40859 ` 570` ``` "\x\range f. x * lmeasure (f -` {x} \ UNIV) \ \" ``` hoelzl@40859 ` 571` ``` using f' om unfolding indicator_def by auto ``` hoelzl@40859 ` 572` ``` show ?case unfolding space_lebesgue real_of_pinfreal_setsum'[OF *(1),THEN sym] ``` hoelzl@40859 ` 573` ``` unfolding real_of_pinfreal_setsum'[OF *(2),THEN sym] ``` hoelzl@40859 ` 574` ``` unfolding real_of_pinfreal_setsum space_lebesgue ``` hoelzl@40859 ` 575` ``` apply(rule has_integral_setsum) ``` hoelzl@40859 ` 576` ``` proof safe show "finite (range f)" using f by (auto dest: lebesgue.simple_functionD) ``` hoelzl@40859 ` 577` ``` fix y::'a show "((\x. real (f y * indicator (f -` {f y}) x)) has_integral ``` hoelzl@40859 ` 578` ``` real (f y * lmeasure (f -` {f y} \ UNIV))) UNIV" ``` hoelzl@40859 ` 579` ``` proof(cases "f y = 0") case False ``` hoelzl@40859 ` 580` ``` have mea:"gmeasurable (f -` {f y})" apply(rule lmeasure_finite_gmeasurable) ``` hoelzl@40859 ` 581` ``` using assms unfolding lebesgue.simple_function_def using False by auto ``` hoelzl@40859 ` 582` ``` have *:"\x. real (indicator (f -` {f y}) x::pinfreal) = (if x \ f -` {f y} then 1 else 0)" by auto ``` hoelzl@40859 ` 583` ``` show ?thesis unfolding real_of_pinfreal_mult[THEN sym] ``` hoelzl@40859 ` 584` ``` apply(rule has_integral_cmul[where 'b=real, unfolded real_scaleR_def]) ``` hoelzl@40859 ` 585` ``` unfolding Int_UNIV_right lmeasure_gmeasure[OF mea,THEN sym] ``` hoelzl@40859 ` 586` ``` unfolding measure_integral_univ[OF mea] * apply(rule integrable_integral) ``` hoelzl@40859 ` 587` ``` unfolding gmeasurable_integrable[THEN sym] using mea . ``` hoelzl@40859 ` 588` ``` qed auto ``` hoelzl@40859 ` 589` ``` qed qed ``` hoelzl@40859 ` 590` hoelzl@40859 ` 591` ```lemma bounded_realI: assumes "\x\s. abs (x::real) \ B" shows "bounded s" ``` hoelzl@40859 ` 592` ``` unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) ``` hoelzl@40859 ` 593` ``` using assms by auto ``` hoelzl@40859 ` 594` hoelzl@40859 ` 595` ```lemma simple_function_has_integral': ``` hoelzl@40859 ` 596` ``` fixes f::"'a::ordered_euclidean_space \ pinfreal" ``` hoelzl@40859 ` 597` ``` assumes f:"lebesgue.simple_function f" ``` hoelzl@40859 ` 598` ``` and i: "lebesgue.simple_integral f \ \" ``` hoelzl@40859 ` 599` ``` shows "((\x. real (f x)) has_integral (real (lebesgue.simple_integral f))) UNIV" ``` hoelzl@40859 ` 600` ```proof- let ?f = "\x. if f x = \ then 0 else f x" ``` hoelzl@40859 ` 601` ``` { fix x have "real (f x) = real (?f x)" by (cases "f x") auto } note * = this ``` hoelzl@40859 ` 602` ``` have **:"{x. f x \ ?f x} = f -` {\}" by auto ``` hoelzl@40859 ` 603` ``` have **:"lmeasure {x\space lebesgue. f x \ ?f x} = 0" ``` hoelzl@40859 ` 604` ``` using lebesgue.simple_integral_omega[OF assms] by(auto simp add:**) ``` hoelzl@40859 ` 605` ``` show ?thesis apply(subst lebesgue.simple_integral_cong'[OF f _ **]) ``` hoelzl@40859 ` 606` ``` apply(rule lebesgue.simple_function_compose1[OF f]) ``` hoelzl@40859 ` 607` ``` unfolding * defer apply(rule simple_function_has_integral) ``` hoelzl@40859 ` 608` ``` proof- ``` hoelzl@40859 ` 609` ``` show "lebesgue.simple_function ?f" ``` hoelzl@40859 ` 610` ``` using lebesgue.simple_function_compose1[OF f] . ``` hoelzl@40859 ` 611` ``` show "\x. ?f x \ \" by auto ``` hoelzl@40859 ` 612` ``` show "\x\range ?f. lmeasure (?f -` {x} \ UNIV) = \ \ x = 0" ``` hoelzl@40859 ` 613` ``` proof (safe, simp, safe, rule ccontr) ``` hoelzl@40859 ` 614` ``` fix y assume "f y \ \" "f y \ 0" ``` hoelzl@40859 ` 615` ``` hence "(\x. if f x = \ then 0 else f x) -` {if f y = \ then 0 else f y} = f -` {f y}" ``` hoelzl@40859 ` 616` ``` by (auto split: split_if_asm) ``` hoelzl@40859 ` 617` ``` moreover assume "lmeasure ((\x. if f x = \ then 0 else f x) -` {if f y = \ then 0 else f y}) = \" ``` hoelzl@40859 ` 618` ``` ultimately have "lmeasure (f -` {f y}) = \" by simp ``` hoelzl@40859 ` 619` ``` moreover ``` hoelzl@40859 ` 620` ``` have "f y * lmeasure (f -` {f y}) \ \" using i f ``` hoelzl@40859 ` 621` ``` unfolding lebesgue.simple_integral_def setsum_\ lebesgue.simple_function_def ``` hoelzl@40859 ` 622` ``` by auto ``` hoelzl@40859 ` 623` ``` ultimately have "f y = 0" by (auto split: split_if_asm) ``` hoelzl@40859 ` 624` ``` then show False using `f y \ 0` by simp ``` hoelzl@40859 ` 625` ``` qed ``` hoelzl@40859 ` 626` ``` qed ``` hoelzl@40859 ` 627` ```qed ``` hoelzl@40859 ` 628` hoelzl@40859 ` 629` ```lemma (in measure_space) positive_integral_monotone_convergence: ``` hoelzl@40859 ` 630` ``` fixes f::"nat \ 'a \ pinfreal" ``` hoelzl@40859 ` 631` ``` assumes i: "\i. f i \ borel_measurable M" and mono: "\x. mono (\n. f n x)" ``` hoelzl@40859 ` 632` ``` and lim: "\x. (\i. f i x) ----> u x" ``` hoelzl@40859 ` 633` ``` shows "u \ borel_measurable M" ``` hoelzl@40859 ` 634` ``` and "(\i. positive_integral (f i)) ----> positive_integral u" (is ?ilim) ``` hoelzl@40859 ` 635` ```proof - ``` hoelzl@40859 ` 636` ``` from positive_integral_isoton[unfolded isoton_fun_expand isoton_iff_Lim_mono, of f u] ``` hoelzl@40859 ` 637` ``` show ?ilim using mono lim i by auto ``` hoelzl@40859 ` 638` ``` have "(SUP i. f i) = u" using mono lim SUP_Lim_pinfreal ``` hoelzl@40859 ` 639` ``` unfolding fun_eq_iff SUPR_fun_expand mono_def by auto ``` hoelzl@40859 ` 640` ``` moreover have "(SUP i. f i) \ borel_measurable M" ``` hoelzl@40859 ` 641` ``` using i by (rule borel_measurable_SUP) ``` hoelzl@40859 ` 642` ``` ultimately show "u \ borel_measurable M" by simp ``` hoelzl@40859 ` 643` ```qed ``` hoelzl@40859 ` 644` hoelzl@40859 ` 645` ```lemma positive_integral_has_integral: ``` hoelzl@40859 ` 646` ``` fixes f::"'a::ordered_euclidean_space => pinfreal" ``` hoelzl@40859 ` 647` ``` assumes f:"f \ borel_measurable lebesgue" ``` hoelzl@40859 ` 648` ``` and int_om:"lebesgue.positive_integral f \ \" ``` hoelzl@40859 ` 649` ``` and f_om:"\x. f x \ \" (* TODO: remove this *) ``` hoelzl@40859 ` 650` ``` shows "((\x. real (f x)) has_integral (real (lebesgue.positive_integral f))) UNIV" ``` hoelzl@40859 ` 651` ```proof- let ?i = "lebesgue.positive_integral f" ``` hoelzl@40859 ` 652` ``` from lebesgue.borel_measurable_implies_simple_function_sequence[OF f] ``` hoelzl@40859 ` 653` ``` guess u .. note conjunctD2[OF this,rule_format] note u = conjunctD2[OF this(1)] this(2) ``` hoelzl@40859 ` 654` ``` let ?u = "\i x. real (u i x)" and ?f = "\x. real (f x)" ``` hoelzl@40859 ` 655` ``` have u_simple:"\k. lebesgue.simple_integral (u k) = lebesgue.positive_integral (u k)" ``` hoelzl@40859 ` 656` ``` apply(subst lebesgue.positive_integral_eq_simple_integral[THEN sym,OF u(1)]) .. ``` hoelzl@40859 ` 657` ``` have int_u_le:"\k. lebesgue.simple_integral (u k) \ lebesgue.positive_integral f" ``` hoelzl@40859 ` 658` ``` unfolding u_simple apply(rule lebesgue.positive_integral_mono) ``` hoelzl@40859 ` 659` ``` using isoton_Sup[OF u(3)] unfolding le_fun_def by auto ``` hoelzl@40859 ` 660` ``` have u_int_om:"\i. lebesgue.simple_integral (u i) \ \" ``` hoelzl@40859 ` 661` ``` proof- case goal1 thus ?case using int_u_le[of i] int_om by auto qed ``` hoelzl@40859 ` 662` hoelzl@40859 ` 663` ``` note u_int = simple_function_has_integral'[OF u(1) this] ``` hoelzl@40859 ` 664` ``` have "(\x. real (f x)) integrable_on UNIV \ ``` hoelzl@40859 ` 665` ``` (\k. Integration.integral UNIV (\x. real (u k x))) ----> Integration.integral UNIV (\x. real (f x))" ``` hoelzl@40859 ` 666` ``` apply(rule monotone_convergence_increasing) apply(rule,rule,rule u_int) ``` hoelzl@40859 ` 667` ``` proof safe case goal1 show ?case apply(rule real_of_pinfreal_mono) using u(2,3) by auto ``` hoelzl@40859 ` 668` ``` next case goal2 show ?case using u(3) apply(subst lim_Real[THEN sym]) ``` hoelzl@40859 ` 669` ``` prefer 3 apply(subst Real_real') defer apply(subst Real_real') ``` hoelzl@40859 ` 670` ``` using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] using f_om u by auto ``` hoelzl@40859 ` 671` ``` next case goal3 ``` hoelzl@40859 ` 672` ``` show ?case apply(rule bounded_realI[where B="real (lebesgue.positive_integral f)"]) ``` hoelzl@40859 ` 673` ``` apply safe apply(subst abs_of_nonneg) apply(rule integral_nonneg,rule) apply(rule u_int) ``` hoelzl@40859 ` 674` ``` unfolding integral_unique[OF u_int] defer apply(rule real_of_pinfreal_mono[OF _ int_u_le]) ``` hoelzl@40859 ` 675` ``` using u int_om by auto ``` hoelzl@40859 ` 676` ``` qed note int = conjunctD2[OF this] ``` hoelzl@40859 ` 677` hoelzl@40859 ` 678` ``` have "(\i. lebesgue.simple_integral (u i)) ----> ?i" unfolding u_simple ``` hoelzl@40859 ` 679` ``` apply(rule lebesgue.positive_integral_monotone_convergence(2)) ``` hoelzl@40859 ` 680` ``` apply(rule lebesgue.borel_measurable_simple_function[OF u(1)]) ``` hoelzl@40859 ` 681` ``` using isotone_Lim[OF u(3)[unfolded isoton_fun_expand, THEN spec]] by auto ``` hoelzl@40859 ` 682` ``` hence "(\i. real (lebesgue.simple_integral (u i))) ----> real ?i" apply- ``` hoelzl@40859 ` 683` ``` apply(subst lim_Real[THEN sym]) prefer 3 ``` hoelzl@40859 ` 684` ``` apply(subst Real_real') defer apply(subst Real_real') ``` hoelzl@40859 ` 685` ``` using u f_om int_om u_int_om by auto ``` hoelzl@40859 ` 686` ``` note * = LIMSEQ_unique[OF this int(2)[unfolded integral_unique[OF u_int]]] ``` hoelzl@40859 ` 687` ``` show ?thesis unfolding * by(rule integrable_integral[OF int(1)]) ``` hoelzl@40859 ` 688` ```qed ``` hoelzl@40859 ` 689` hoelzl@40859 ` 690` ```lemma lebesgue_integral_has_integral: ``` hoelzl@40859 ` 691` ``` fixes f::"'a::ordered_euclidean_space => real" ``` hoelzl@40859 ` 692` ``` assumes f:"lebesgue.integrable f" ``` hoelzl@40859 ` 693` ``` shows "(f has_integral (lebesgue.integral f)) UNIV" ``` hoelzl@40859 ` 694` ```proof- let ?n = "\x. - min (f x) 0" and ?p = "\x. max (f x) 0" ``` hoelzl@40859 ` 695` ``` have *:"f = (\x. ?p x - ?n x)" apply rule by auto ``` hoelzl@40859 ` 696` ``` note f = lebesgue.integrableD[OF f] ``` hoelzl@40859 ` 697` ``` show ?thesis unfolding lebesgue.integral_def apply(subst *) ``` hoelzl@40859 ` 698` ``` proof(rule has_integral_sub) case goal1 ``` hoelzl@40859 ` 699` ``` have *:"\x. Real (f x) \ \" by auto ``` hoelzl@40859 ` 700` ``` note lebesgue.borel_measurable_Real[OF f(1)] ``` hoelzl@40859 ` 701` ``` from positive_integral_has_integral[OF this f(2) *] ``` hoelzl@40859 ` 702` ``` show ?case unfolding real_Real_max . ``` hoelzl@40859 ` 703` ``` next case goal2 ``` hoelzl@40859 ` 704` ``` have *:"\x. Real (- f x) \ \" by auto ``` hoelzl@40859 ` 705` ``` note lebesgue.borel_measurable_uminus[OF f(1)] ``` hoelzl@40859 ` 706` ``` note lebesgue.borel_measurable_Real[OF this] ``` hoelzl@40859 ` 707` ``` from positive_integral_has_integral[OF this f(3) *] ``` hoelzl@40859 ` 708` ``` show ?case unfolding real_Real_max minus_min_eq_max by auto ``` hoelzl@40859 ` 709` ``` qed ``` hoelzl@40859 ` 710` ```qed ``` hoelzl@40859 ` 711` hoelzl@40859 ` 712` ```lemma continuous_on_imp_borel_measurable: ``` hoelzl@40859 ` 713` ``` fixes f::"'a::ordered_euclidean_space \ 'b::ordered_euclidean_space" ``` hoelzl@40859 ` 714` ``` assumes "continuous_on UNIV f" ``` hoelzl@40859 ` 715` ``` shows "f \ borel_measurable lebesgue" ``` hoelzl@40859 ` 716` ``` apply(rule lebesgue.borel_measurableI) ``` hoelzl@40859 ` 717` ``` using continuous_open_preimage[OF assms] unfolding vimage_def by auto ``` hoelzl@40859 ` 718` hoelzl@40859 ` 719` ```lemma (in measure_space) integral_monotone_convergence_pos': ``` hoelzl@40859 ` 720` ``` assumes i: "\i. integrable (f i)" and mono: "\x. mono (\n. f n x)" ``` hoelzl@40859 ` 721` ``` and pos: "\x i. 0 \ f i x" ``` hoelzl@40859 ` 722` ``` and lim: "\x. (\i. f i x) ----> u x" ``` hoelzl@40859 ` 723` ``` and ilim: "(\i. integral (f i)) ----> x" ``` hoelzl@40859 ` 724` ``` shows "integrable u \ integral u = x" ``` hoelzl@40859 ` 725` ``` using integral_monotone_convergence_pos[OF assms] by auto ``` hoelzl@40859 ` 726` hoelzl@40859 ` 727` ```definition e2p :: "'a::ordered_euclidean_space \ (nat \ real)" where ``` hoelzl@40859 ` 728` ``` "e2p x = (\i\{.. real) \ 'a::ordered_euclidean_space" where ``` hoelzl@40859 ` 731` ``` "p2e x = (\\ i. x i)" ``` hoelzl@40859 ` 732` hoelzl@40859 ` 733` ```lemma bij_euclidean_component: ``` hoelzl@40859 ` 734` ``` "bij_betw (e2p::'a::ordered_euclidean_space \ _) (UNIV :: 'a set) ``` hoelzl@40859 ` 735` ``` ({..\<^isub>E (UNIV :: real set))" ``` hoelzl@40859 ` 736` ``` unfolding bij_betw_def e2p_def_raw ``` hoelzl@40859 ` 737` ```proof let ?e = "\x.\i\{.. real" assume x:"\i. i \ {.. x i = undefined" ``` hoelzl@40859 ` 741` ``` hence "x = ?e (\\ i. x i)" apply-apply(rule,case_tac "xa range ?e" by fastsimp ``` hoelzl@40859 ` 743` ``` } thus "range ?e = ({.. UNIV) \ extensional {.. 'a::ordered_euclidean_space) ({..\<^isub>E (UNIV :: real set)) ``` hoelzl@40859 ` 749` ``` (UNIV :: 'a set)" (is "bij_betw ?p ?U _") ``` hoelzl@40859 ` 750` ``` unfolding bij_betw_def ``` hoelzl@40859 ` 751` ```proof show "inj_on ?p ?U" unfolding inj_on_def p2e_def ``` hoelzl@40859 ` 752` ``` apply(subst euclidean_eq) apply(safe,rule) unfolding extensional_def ``` hoelzl@40859 ` 753` ``` apply(case_tac "xa ?p ` extensional {.. extensional {..x. borel::real algebra" "\x. lmeasure" ``` hoelzl@40859 ` 773` ``` by default ``` hoelzl@40859 ` 774` hoelzl@40859 ` 775` ```lemma cube_subset_Suc[intro]: "cube n \ cube (Suc n)" ``` hoelzl@40859 ` 776` ``` unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto ``` hoelzl@40859 ` 777` hoelzl@40859 ` 778` ```lemma borel_vimage_algebra_eq: ``` hoelzl@40859 ` 779` ``` "sigma_algebra.vimage_algebra ``` hoelzl@40859 ` 780` ``` (borel :: ('a::ordered_euclidean_space) algebra) ({..\<^isub>E UNIV) p2e = ``` hoelzl@40859 ` 781` ``` sigma (product_algebra (\x. \ space = UNIV::real set, sets = range (\a. {..) {.. "product_algebra (\x. \ space = UNIV::real set, sets = range (\a. {..) {.. "\space = (UNIV::'a set), sets = range lessThan\" ``` hoelzl@40859 ` 785` ``` have *:"(({.. UNIV) \ extensional {.. Pow (space E)" "p2e \ space F \ space E" unfolding E_def by auto ``` hoelzl@40859 ` 789` ``` next fix A assume "A \ sets F" ``` hoelzl@40859 ` 790` ``` hence A:"A \ (Pi\<^isub>E {.. range lessThan)" ``` hoelzl@40859 ` 791` ``` unfolding F_def product_algebra_def algebra.simps . ``` hoelzl@40859 ` 792` ``` then guess B unfolding image_iff .. note B=this ``` hoelzl@40859 ` 793` ``` hence "\x range lessThan" by auto ``` hoelzl@40859 ` 794` ``` hence "\x. \xa. x B x = {..i (\X. p2e -` X \ space F) ` sets E" unfolding image_iff B ``` hoelzl@40859 ` 799` ``` proof(rule_tac x="{..< \\ i. Sup (B i)}" in bexI) ``` hoelzl@40859 ` 800` ``` show "Pi\<^isub>E {..\ i. Sup (B i))::'a} \ space F" ``` hoelzl@40859 ` 801` ``` unfolding F_def E_def product_algebra_def algebra.simps ``` hoelzl@40859 ` 802` ``` proof(rule,unfold subset_eq,rule_tac[!] ballI) ``` hoelzl@40859 ` 803` ``` fix x assume "x \ Pi\<^isub>E {..ii\DIM('a). x i = undefined" ``` hoelzl@40859 ` 805` ``` unfolding Pi_def extensional_def using b by auto ``` hoelzl@40859 ` 806` ``` have "(p2e x::'a) < (\\ i. Sup (B i))" unfolding less_prod_def eucl_less[of "p2e x"] ``` hoelzl@40859 ` 807` ``` apply safe unfolding euclidean_lambda_beta b'[rule_format] p2e_def using * by auto ``` hoelzl@40859 ` 808` ``` moreover have "x \ extensional {.. p2e -` {..<(\\ i. Sup (B i)) ::'a} \ ``` hoelzl@40859 ` 811` ``` (({.. UNIV) \ extensional {.. p2e -` {..<(\\ i. Sup (B i))::'a} \ ``` hoelzl@40859 ` 813` ``` (({.. UNIV) \ extensional {..\ i. Sup (B i))::'a)" by auto ``` hoelzl@40859 ` 815` ``` hence "\i B i" apply-apply(subst(asm) eucl_less) ``` hoelzl@40859 ` 816` ``` unfolding p2e_def using b b' by auto ``` hoelzl@40859 ` 817` ``` thus "x \ Pi\<^isub>E {..\ i. Sup (B i))::'a} \ sets E" unfolding E_def algebra.simps by auto ``` hoelzl@40859 ` 820` ``` qed ``` hoelzl@40859 ` 821` ``` next fix A assume "A \ sets E" ``` hoelzl@40859 ` 822` ``` then guess a unfolding E_def algebra.simps image_iff .. note a = this(2) ``` hoelzl@40859 ` 823` ``` def B \ "\i. {.. space F \ sets F" unfolding F_def ``` hoelzl@40859 ` 825` ``` unfolding product_algebra_def algebra.simps image_iff ``` hoelzl@40859 ` 826` ``` apply(rule_tac x=B in bexI) apply rule unfolding subset_eq apply(rule_tac[1-2] ballI) ``` hoelzl@40859 ` 827` ``` proof- show "B \ {.. range lessThan" unfolding B_def by auto ``` hoelzl@40859 ` 828` ``` fix x assume as:"x \ p2e -` A \ (({.. UNIV) \ extensional {.. A" by auto ``` hoelzl@40859 ` 830` ``` hence "\i B i" unfolding B_def a lessThan_iff ``` hoelzl@40859 ` 831` ``` apply-apply(subst (asm) eucl_less) unfolding p2e_def by auto ``` hoelzl@40859 ` 832` ``` thus "x \ Pi\<^isub>E {.. Pi\<^isub>E {.. A" unfolding a lessThan_iff p2e_def apply(subst eucl_less) ``` hoelzl@40859 ` 835` ``` using x unfolding Pi_def extensional_def B_def by auto ``` hoelzl@40859 ` 836` ``` ultimately show "x \ p2e -` A \ (({.. UNIV) \ extensional {.. 0" "y \ 0" ``` hoelzl@40859 ` 842` ``` shows "Real (x * y) = Real x * Real y" using assms by auto ``` hoelzl@40859 ` 843` hoelzl@40859 ` 844` ```lemma Real_setprod: assumes "\x\A. f x \ 0" shows "Real (setprod f A) = setprod (\x. Real (f x)) A" ``` hoelzl@40859 ` 845` ```proof(cases "finite A") ``` hoelzl@40859 ` 846` ``` case True thus ?thesis using assms ``` hoelzl@40859 ` 847` ``` proof(induct A) case (insert x A) ``` hoelzl@40859 ` 848` ``` have "0 \ setprod f A" apply(rule setprod_nonneg) using insert by auto ``` hoelzl@40859 ` 849` ``` thus ?case unfolding setprod_insert[OF insert(1-2)] apply- ``` hoelzl@40859 ` 850` ``` apply(subst Real_mult_nonneg) prefer 3 apply(subst insert(3)[THEN sym]) ``` hoelzl@40859 ` 851` ``` using insert by auto ``` hoelzl@40859 ` 852` ``` qed auto ``` hoelzl@40859 ` 853` ```qed auto ``` hoelzl@40859 ` 854` hoelzl@40859 ` 855` ```lemma e2p_Int:"e2p ` A \ e2p ` B = e2p ` (A \ B)" (is "?L = ?R") ``` hoelzl@40859 ` 856` ``` apply(rule image_Int[THEN sym]) using bij_euclidean_component ``` hoelzl@40859 ` 857` ``` unfolding bij_betw_def by auto ``` hoelzl@40859 ` 858` hoelzl@40859 ` 859` ```lemma Int_stable_cuboids: fixes x::"'a::ordered_euclidean_space" ``` hoelzl@40859 ` 860` ``` shows "Int_stable \space = UNIV, sets = range (\(a, b::'a). e2p ` {a..b})\" ``` hoelzl@40859 ` 861` ``` unfolding Int_stable_def algebra.select_convs ``` hoelzl@40859 ` 862` ```proof safe fix a b x y::'a ``` hoelzl@40859 ` 863` ``` have *:"e2p ` {a..b} \ e2p ` {x..y} = ``` hoelzl@40859 ` 864` ``` (\(a, b). e2p ` {a..b}) (\\ i. max (a \$\$ i) (x \$\$ i), \\ i. min (b \$\$ i) (y \$\$ i)::'a)" ``` hoelzl@40859 ` 865` ``` unfolding e2p_Int inter_interval by auto ``` hoelzl@40859 ` 866` ``` show "e2p ` {a..b} \ e2p ` {x..y} \ range (\(a, b). e2p ` {a..b::'a})" unfolding * ``` hoelzl@40859 ` 867` ``` apply(rule range_eqI) .. ``` hoelzl@40859 ` 868` ```qed ``` hoelzl@40859 ` 869` hoelzl@40859 ` 870` ```lemma Int_stable_cuboids': fixes x::"'a::ordered_euclidean_space" ``` hoelzl@40859 ` 871` ``` shows "Int_stable \space = UNIV, sets = range (\(a, b::'a). {a..b})\" ``` hoelzl@40859 ` 872` ``` unfolding Int_stable_def algebra.select_convs ``` hoelzl@40859 ` 873` ``` apply safe unfolding inter_interval by auto ``` hoelzl@40859 ` 874` hoelzl@40859 ` 875` ```lemma product_borel_eq_vimage: ``` hoelzl@40859 ` 876` ``` "sigma (product_algebra (\x. borel) {.. UNIV) \ extensional {.. 'a::ordered_euclidean_space)" ``` hoelzl@40859 ` 879` ``` unfolding borel_vimage_algebra_eq unfolding borel_eq_lessThan ``` hoelzl@40859 ` 880` ``` apply(subst sigma_product_algebra_sigma_eq[where S="\i. \n. lessThan (real n)"]) ``` hoelzl@40859 ` 881` ``` unfolding lessThan_iff ``` hoelzl@40859 ` 882` ```proof- fix i assume i:"in. {.. space \space = UNIV, sets = range lessThan\" ``` hoelzl@40859 ` 884` ``` by(auto intro!:real_arch_lt isotoneI) ``` hoelzl@40859 ` 885` ```qed auto ``` hoelzl@40859 ` 886` hoelzl@40859 ` 887` ```lemma inj_on_disjoint_family_on: assumes "disjoint_family_on A S" "inj f" ``` hoelzl@40859 ` 888` ``` shows "disjoint_family_on (\x. f ` A x) S" ``` hoelzl@40859 ` 889` ``` unfolding disjoint_family_on_def ``` hoelzl@40859 ` 890` ```proof(rule,rule,rule) ``` hoelzl@40859 ` 891` ``` fix x1 x2 assume x:"x1 \ S" "x2 \ S" "x1 \ x2" ``` hoelzl@40859 ` 892` ``` show "f ` A x1 \ f ` A x2 = {}" ``` hoelzl@40859 ` 893` ``` proof(rule ccontr) case goal1 ``` hoelzl@40859 ` 894` ``` then obtain z where z:"z \ f ` A x1 \ f ` A x2" by auto ``` hoelzl@40859 ` 895` ``` then obtain z1 z2 where z12:"z1 \ A x1" "z2 \ A x2" "f z1 = z" "f z2 = z" by auto ``` hoelzl@40859 ` 896` ``` hence "z1 = z2" using assms(2) unfolding inj_on_def by blast ``` hoelzl@40859 ` 897` ``` hence "x1 = x2" using z12(1-2) using assms[unfolded disjoint_family_on_def] using x by auto ``` hoelzl@40859 ` 898` ``` thus False using x(3) by auto ``` hoelzl@40859 ` 899` ``` qed ``` hoelzl@40859 ` 900` ```qed ``` hoelzl@40859 ` 901` hoelzl@40859 ` 902` ```declare restrict_extensional[intro] ``` hoelzl@40859 ` 903` hoelzl@40859 ` 904` ```lemma e2p_extensional[intro]:"e2p (y::'a::ordered_euclidean_space) \ extensional {.. (({.. UNIV) \ extensional {.. e2p ` A" then guess y unfolding image_iff .. note y=this ``` hoelzl@40859 ` 911` ``` show "x \ p2e -` A \ (({.. UNIV) \ extensional {.. p2e -` A \ (({.. UNIV) \ extensional {.. e2p ` A" unfolding image_iff apply(rule_tac x="p2e x" in bexI) apply(subst e2p_p2e) by auto ``` hoelzl@40859 ` 915` ```qed ``` hoelzl@40859 ` 916` hoelzl@40859 ` 917` ```lemma lmeasure_measure_eq_borel_prod: ``` hoelzl@40859 ` 918` ``` fixes A :: "('a::ordered_euclidean_space) set" ``` hoelzl@40859 ` 919` ``` assumes "A \ sets borel" ``` hoelzl@40859 ` 920` ``` shows "lmeasure A = borel_product.product_measure {.. real) set)" ``` hoelzl@40859 ` 921` ```proof (rule measure_unique_Int_stable[where X=A and A=cube]) ``` hoelzl@40859 ` 922` ``` interpret fprod: finite_product_sigma_finite "\x. borel" "\x. lmeasure" "{.. space = UNIV :: 'a set, sets = range (\(a,b). {a..b}) \" ``` hoelzl@40859 ` 924` ``` (is "Int_stable ?E" ) using Int_stable_cuboids' . ``` hoelzl@40859 ` 925` ``` show "borel = sigma ?E" using borel_eq_atLeastAtMost . ``` hoelzl@40859 ` 926` ``` show "\i. lmeasure (cube i) \ \" unfolding lmeasure_cube by auto ``` hoelzl@40859 ` 927` ``` show "\X. X \ sets ?E \ ``` hoelzl@40859 ` 928` ``` lmeasure X = borel_product.product_measure {.. real) set)" ``` hoelzl@40859 ` 929` ``` proof- case goal1 then obtain a b where X:"X = {a..b}" by auto ``` hoelzl@40859 ` 930` ``` { presume *:"X \ {} \ ?case" ``` hoelzl@40859 ` 931` ``` show ?case apply(cases,rule *,assumption) by auto } ``` hoelzl@40859 ` 932` ``` def XX \ "\i. {a \$\$ i .. b \$\$ i}" assume "X \ {}" note X' = this[unfolded X interval_ne_empty] ``` hoelzl@40859 ` 933` ``` have *:"Pi\<^isub>E {.. Pi\<^isub>E {.. e2p ` X" unfolding image_iff apply(rule_tac x="\\ i. x i" in bexI) ``` hoelzl@40859 ` 936` ``` unfolding Pi_def extensional_def e2p_def restrict_def X mem_interval XX_def by rule auto ``` hoelzl@40859 ` 937` ``` next fix x assume "x \ e2p ` X" then guess y unfolding image_iff .. note y = this ``` hoelzl@40859 ` 938` ``` show "x \ Pi\<^isub>E {..xi sets \space = UNIV, sets = range (\(a, b). {a..b})\" ``` hoelzl@40859 ` 951` ``` unfolding cube_def_raw by auto ``` hoelzl@40859 ` 952` ``` have "\x. \xa. x \ cube xa" apply(rule_tac x=x in mem_big_cube) by fastsimp ``` hoelzl@40859 ` 953` ``` thus "cube \ space \space = UNIV, sets = range (\(a, b). {a..b})\" ``` hoelzl@40859 ` 954` ``` apply-apply(rule isotoneI) apply(rule cube_subset_Suc) by auto ``` hoelzl@40859 ` 955` ``` show "A \ sets borel " by fact ``` hoelzl@40859 ` 956` ``` show "measure_space borel lmeasure" by default ``` hoelzl@40859 ` 957` ``` show "measure_space borel ``` hoelzl@40859 ` 958` ``` (\a::'a set. finite_product_sigma_finite.measure (\x. borel) (\x. lmeasure) {.. 'a set" assume A:"range A \ sets borel" "disjoint_family A" ``` hoelzl@40859 ` 961` ``` "(\i. A i) \ sets borel" ``` hoelzl@40859 ` 962` ``` note fprod.ca[unfolded countably_additive_def,rule_format] ``` hoelzl@40859 ` 963` ``` note ca = this[of "\ n. e2p ` (A n)"] ``` hoelzl@40859 ` 964` ``` show "(\\<^isub>\n. finite_product_sigma_finite.measure ``` hoelzl@40859 ` 965` ``` (\x. borel) (\x. lmeasure) {..x. borel) ``` hoelzl@40859 ` 967` ``` (\x. lmeasure) {..i. A i))" unfolding image_UN ``` hoelzl@40859 ` 968` ``` proof(rule ca) show "range (\n. e2p ` A n) \ sets ``` hoelzl@40859 ` 969` ``` (sigma (product_algebra (\x. borel) {..n. e2p ` A n)" apply(rule inj_on_disjoint_family_on) ``` hoelzl@40859 ` 979` ``` using bij_euclidean_component using A(2) unfolding bij_betw_def by auto ``` hoelzl@40859 ` 980` ``` show "(\n. e2p ` A n) \ sets (sigma (product_algebra (\x. borel) {.. (\n. e2p ` A n)" hence "p2e x \ (\i. A i)" by auto ``` hoelzl@40859 ` 984` ``` moreover have "x \ extensional {.. p2e -` (\i. A i) \ (({.. UNIV) \ ``` hoelzl@40859 ` 987` ``` extensional {.. p2e -` (\i. A i) \ (({.. UNIV) \ ``` hoelzl@40859 ` 989` ``` extensional {.. (\i. A i)" by auto ``` hoelzl@40859 ` 991` ``` hence "\n. x \ e2p ` A n" apply safe apply(rule_tac x=i in exI) ``` hoelzl@40859 ` 992` ``` unfolding image_iff apply(rule_tac x="p2e x" in bexI) ``` hoelzl@40859 ` 993` ``` apply(subst e2p_p2e) using x by auto ``` hoelzl@40859 ` 994` ``` thus "x \ (\n. e2p ` A n)" by auto ``` hoelzl@40859 ` 995` ``` qed ``` hoelzl@40859 ` 996` ``` qed ``` hoelzl@40859 ` 997` ``` qed auto ``` hoelzl@40859 ` 998` ```qed ``` hoelzl@40859 ` 999` hoelzl@40859 ` 1000` ```lemma e2p_p2e'[simp]: fixes x::"'a::ordered_euclidean_space" ``` hoelzl@40859 ` 1001` ``` assumes "A \ extensional {..'a::ordered_euclidean_space) = UNIV" ``` hoelzl@40859 ` 1007` ``` apply safe defer unfolding image_iff apply(rule_tac x="\i. x \$\$ i" in bexI) ``` hoelzl@40859 ` 1008` ``` unfolding p2e_def by auto ``` hoelzl@40859 ` 1009` hoelzl@40859 ` 1010` ```lemma p2e_inv_extensional:"(A::'a::ordered_euclidean_space set) ``` hoelzl@40859 ` 1011` ``` = p2e ` (p2e -` A \ extensional {..A" ``` hoelzl@40859 ` 1014` ``` let ?y = "\i. if ixa\Chi -` A \ extensional {..A` by(auto simp: *) ``` hoelzl@40859 ` 1018` ```qed ``` hoelzl@40859 ` 1019` hoelzl@40859 ` 1020` ```lemma borel_fubini_positiv_integral: ``` hoelzl@40859 ` 1021` ``` fixes f :: "'a::ordered_euclidean_space \ pinfreal" ``` hoelzl@40859 ` 1022` ``` assumes f: "f \ borel_measurable borel" ``` hoelzl@40859 ` 1023` ``` shows "borel.positive_integral f = ``` hoelzl@40859 ` 1024` ``` borel_product.product_positive_integral {.. p2e)" ``` hoelzl@40859 ` 1025` ```proof- def U \ "(({.. UNIV) \ extensional {.. real) set" ``` hoelzl@40859 ` 1026` ``` interpret fprod: finite_product_sigma_finite "\x. borel" "\x. lmeasure" "{..x. \i::nat. x < real i" by (metis real_arch_lt) ``` hoelzl@408