src/HOL/Probability/Product_Measure.thy
 author hoelzl Mon Aug 23 19:35:57 2010 +0200 (2010-08-23) changeset 38656 d5d342611edb parent 36649 bfd8c550faa6 child 38705 aaee86c0e237 permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
 hoelzl@35833 ` 1` ```theory Product_Measure ``` hoelzl@38656 ` 2` ```imports Lebesgue_Integration ``` hoelzl@35833 ` 3` ```begin ``` hoelzl@35833 ` 4` hoelzl@38656 ` 5` ```definition prod_sets where ``` hoelzl@38656 ` 6` ``` "prod_sets A B = {z. \x \ A. \y \ B. z = x \ y}" ``` hoelzl@38656 ` 7` hoelzl@35833 ` 8` ```definition ``` hoelzl@38656 ` 9` ``` "prod_measure M \ N \ = (\A. measure_space.positive_integral M \ (\s0. \ ((\s1. (s0, s1)) -` A)))" ``` hoelzl@35833 ` 10` hoelzl@35833 ` 11` ```definition ``` hoelzl@38656 ` 12` ``` "prod_measure_space M1 M2 = sigma (space M1 \ space M2) (prod_sets (sets M1) (sets M2))" ``` hoelzl@38656 ` 13` hoelzl@38656 ` 14` ```lemma prod_setsI: "x \ A \ y \ B \ (x \ y) \ prod_sets A B" ``` hoelzl@38656 ` 15` ``` by (auto simp add: prod_sets_def) ``` hoelzl@35833 ` 16` hoelzl@38656 ` 17` ```lemma sigma_prod_sets_finite: ``` hoelzl@38656 ` 18` ``` assumes "finite A" and "finite B" ``` hoelzl@38656 ` 19` ``` shows "sigma_sets (A \ B) (prod_sets (Pow A) (Pow B)) = Pow (A \ B)" ``` hoelzl@38656 ` 20` ```proof safe ``` hoelzl@38656 ` 21` ``` have fin: "finite (A \ B)" using assms by (rule finite_cartesian_product) ``` hoelzl@35833 ` 22` hoelzl@38656 ` 23` ``` fix x assume subset: "x \ A \ B" ``` hoelzl@38656 ` 24` ``` hence "finite x" using fin by (rule finite_subset) ``` hoelzl@38656 ` 25` ``` from this subset show "x \ sigma_sets (A\B) (prod_sets (Pow A) (Pow B))" ``` hoelzl@38656 ` 26` ``` (is "x \ sigma_sets ?prod ?sets") ``` hoelzl@38656 ` 27` ``` proof (induct x) ``` hoelzl@38656 ` 28` ``` case empty show ?case by (rule sigma_sets.Empty) ``` hoelzl@38656 ` 29` ``` next ``` hoelzl@38656 ` 30` ``` case (insert a x) ``` hoelzl@38656 ` 31` ``` hence "{a} \ sigma_sets ?prod ?sets" by (auto simp: prod_sets_def intro!: sigma_sets.Basic) ``` hoelzl@38656 ` 32` ``` moreover have "x \ sigma_sets ?prod ?sets" using insert by auto ``` hoelzl@38656 ` 33` ``` ultimately show ?case unfolding insert_is_Un[of a x] by (rule sigma_sets_Un) ``` hoelzl@38656 ` 34` ``` qed ``` hoelzl@38656 ` 35` ```next ``` hoelzl@38656 ` 36` ``` fix x a b ``` hoelzl@38656 ` 37` ``` assume "x \ sigma_sets (A\B) (prod_sets (Pow A) (Pow B))" and "(a, b) \ x" ``` hoelzl@38656 ` 38` ``` from sigma_sets_into_sp[OF _ this(1)] this(2) ``` hoelzl@38656 ` 39` ``` show "a \ A" and "b \ B" ``` hoelzl@38656 ` 40` ``` by (auto simp: prod_sets_def) ``` hoelzl@35833 ` 41` ```qed ``` hoelzl@35833 ` 42` hoelzl@38656 ` 43` ```lemma (in sigma_algebra) measurable_prod_sigma: ``` hoelzl@38656 ` 44` ``` assumes sa1: "sigma_algebra a1" and sa2: "sigma_algebra a2" ``` hoelzl@38656 ` 45` ``` assumes 1: "(fst o f) \ measurable M a1" and 2: "(snd o f) \ measurable M a2" ``` hoelzl@38656 ` 46` ``` shows "f \ measurable M (sigma ((space a1) \ (space a2)) ``` hoelzl@38656 ` 47` ``` (prod_sets (sets a1) (sets a2)))" ``` hoelzl@35977 ` 48` ```proof - ``` hoelzl@38656 ` 49` ``` from 1 have fn1: "fst \ f \ space M \ space a1" ``` hoelzl@38656 ` 50` ``` and q1: "\y\sets a1. (fst \ f) -` y \ space M \ sets M" ``` hoelzl@38656 ` 51` ``` by (auto simp add: measurable_def) ``` hoelzl@38656 ` 52` ``` from 2 have fn2: "snd \ f \ space M \ space a2" ``` hoelzl@38656 ` 53` ``` and q2: "\y\sets a2. (snd \ f) -` y \ space M \ sets M" ``` hoelzl@38656 ` 54` ``` by (auto simp add: measurable_def) ``` hoelzl@38656 ` 55` ``` show ?thesis ``` hoelzl@38656 ` 56` ``` proof (rule measurable_sigma) ``` hoelzl@38656 ` 57` ``` show "prod_sets (sets a1) (sets a2) \ Pow (space a1 \ space a2)" using sa1 sa2 ``` hoelzl@38656 ` 58` ``` by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed) ``` hoelzl@38656 ` 59` ``` next ``` hoelzl@38656 ` 60` ``` show "f \ space M \ space a1 \ space a2" ``` hoelzl@38656 ` 61` ``` by (rule prod_final [OF fn1 fn2]) ``` hoelzl@38656 ` 62` ``` next ``` hoelzl@38656 ` 63` ``` fix z ``` hoelzl@38656 ` 64` ``` assume z: "z \ prod_sets (sets a1) (sets a2)" ``` hoelzl@38656 ` 65` ``` thus "f -` z \ space M \ sets M" ``` hoelzl@38656 ` 66` ``` proof (auto simp add: prod_sets_def vimage_Times) ``` hoelzl@38656 ` 67` ``` fix x y ``` hoelzl@38656 ` 68` ``` assume x: "x \ sets a1" and y: "y \ sets a2" ``` hoelzl@38656 ` 69` ``` have "(fst \ f) -` x \ (snd \ f) -` y \ space M = ``` hoelzl@38656 ` 70` ``` ((fst \ f) -` x \ space M) \ ((snd \ f) -` y \ space M)" ``` hoelzl@38656 ` 71` ``` by blast ``` hoelzl@38656 ` 72` ``` also have "... \ sets M" using x y q1 q2 ``` hoelzl@38656 ` 73` ``` by blast ``` hoelzl@38656 ` 74` ``` finally show "(fst \ f) -` x \ (snd \ f) -` y \ space M \ sets M" . ``` hoelzl@38656 ` 75` ``` qed ``` hoelzl@38656 ` 76` ``` qed ``` hoelzl@35977 ` 77` ```qed ``` hoelzl@35833 ` 78` hoelzl@38656 ` 79` ```lemma (in sigma_finite_measure) prod_measure_times: ``` hoelzl@38656 ` 80` ``` assumes "sigma_finite_measure N \" ``` hoelzl@38656 ` 81` ``` and "A1 \ sets M" "A2 \ sets N" ``` hoelzl@38656 ` 82` ``` shows "prod_measure M \ N \ (A1 \ A2) = \ A1 * \ A2" ``` hoelzl@38656 ` 83` ``` oops ``` hoelzl@35833 ` 84` hoelzl@38656 ` 85` ```lemma (in sigma_finite_measure) sigma_finite_prod_measure_space: ``` hoelzl@38656 ` 86` ``` assumes "sigma_finite_measure N \" ``` hoelzl@38656 ` 87` ``` shows "sigma_finite_measure (prod_measure_space M N) (prod_measure M \ N \)" ``` hoelzl@38656 ` 88` ``` oops ``` hoelzl@38656 ` 89` hoelzl@38656 ` 90` ```lemma (in finite_measure_space) simple_function_finite: ``` hoelzl@38656 ` 91` ``` "simple_function f" ``` hoelzl@38656 ` 92` ``` unfolding simple_function_def sets_eq_Pow using finite_space by auto ``` hoelzl@38656 ` 93` hoelzl@38656 ` 94` ```lemma (in finite_measure_space) borel_measurable_finite[intro, simp]: "f \ borel_measurable M" ``` hoelzl@38656 ` 95` ``` unfolding measurable_def sets_eq_Pow by auto ``` hoelzl@35833 ` 96` hoelzl@38656 ` 97` ```lemma (in finite_measure_space) positive_integral_finite_eq_setsum: ``` hoelzl@38656 ` 98` ``` "positive_integral f = (\x \ space M. f x * \ {x})" ``` hoelzl@38656 ` 99` ```proof - ``` hoelzl@38656 ` 100` ``` have *: "positive_integral f = positive_integral (\x. \y\space M. f y * indicator {y} x)" ``` hoelzl@38656 ` 101` ``` by (auto intro!: positive_integral_cong simp add: indicator_def if_distrib setsum_cases[OF finite_space]) ``` hoelzl@38656 ` 102` ``` show ?thesis unfolding * using borel_measurable_finite[of f] ``` hoelzl@38656 ` 103` ``` by (simp add: positive_integral_setsum positive_integral_cmult_indicator sets_eq_Pow) ``` hoelzl@38656 ` 104` ```qed ``` hoelzl@35833 ` 105` hoelzl@38656 ` 106` ```lemma (in finite_measure_space) finite_prod_measure_times: ``` hoelzl@38656 ` 107` ``` assumes "finite_measure_space N \" ``` hoelzl@38656 ` 108` ``` and "A1 \ sets M" "A2 \ sets N" ``` hoelzl@38656 ` 109` ``` shows "prod_measure M \ N \ (A1 \ A2) = \ A1 * \ A2" ``` hoelzl@38656 ` 110` ```proof - ``` hoelzl@38656 ` 111` ``` interpret N: finite_measure_space N \ by fact ``` hoelzl@38656 ` 112` ``` have *: "\x. \ (Pair x -` (A1 \ A2)) * \ {x} = (if x \ A1 then \ A2 * \ {x} else 0)" ``` hoelzl@38656 ` 113` ``` by (auto simp: vimage_Times comp_def) ``` hoelzl@38656 ` 114` ``` have "finite A1" ``` hoelzl@38656 ` 115` ``` using `A1 \ sets M` finite_space by (auto simp: sets_eq_Pow intro: finite_subset) ``` hoelzl@38656 ` 116` ``` then have "\ A1 = (\x\A1. \ {x})" using `A1 \ sets M` ``` hoelzl@38656 ` 117` ``` by (auto intro!: measure_finite_singleton simp: sets_eq_Pow) ``` hoelzl@38656 ` 118` ``` then show ?thesis using `A1 \ sets M` ``` hoelzl@38656 ` 119` ``` unfolding prod_measure_def positive_integral_finite_eq_setsum * ``` hoelzl@38656 ` 120` ``` by (auto simp add: sets_eq_Pow setsum_right_distrib[symmetric] mult_commute setsum_cases[OF finite_space]) ``` hoelzl@35833 ` 121` ```qed ``` hoelzl@35833 ` 122` hoelzl@38656 ` 123` ```lemma (in finite_measure_space) finite_prod_measure_space: ``` hoelzl@38656 ` 124` ``` assumes "finite_measure_space N \" ``` hoelzl@38656 ` 125` ``` shows "prod_measure_space M N = \ space = space M \ space N, sets = Pow (space M \ space N) \" ``` hoelzl@35977 ` 126` ```proof - ``` hoelzl@38656 ` 127` ``` interpret N: finite_measure_space N \ by fact ``` hoelzl@38656 ` 128` ``` show ?thesis using finite_space N.finite_space ``` hoelzl@38656 ` 129` ``` by (simp add: sigma_def prod_measure_space_def sigma_prod_sets_finite sets_eq_Pow N.sets_eq_Pow) ``` hoelzl@35833 ` 130` ```qed ``` hoelzl@35833 ` 131` hoelzl@38656 ` 132` ```lemma (in finite_measure_space) finite_measure_space_finite_prod_measure: ``` hoelzl@38656 ` 133` ``` assumes "finite_measure_space N \" ``` hoelzl@38656 ` 134` ``` shows "finite_measure_space (prod_measure_space M N) (prod_measure M \ N \)" ``` hoelzl@38656 ` 135` ``` unfolding finite_prod_measure_space[OF assms] ``` hoelzl@38656 ` 136` ```proof (rule finite_measure_spaceI) ``` hoelzl@38656 ` 137` ``` interpret N: finite_measure_space N \ by fact ``` hoelzl@38656 ` 138` hoelzl@38656 ` 139` ``` let ?P = "\space = space M \ space N, sets = Pow (space M \ space N)\" ``` hoelzl@38656 ` 140` ``` show "measure_space ?P (prod_measure M \ N \)" ``` hoelzl@38656 ` 141` ``` proof (rule sigma_algebra.finite_additivity_sufficient) ``` hoelzl@38656 ` 142` ``` show "sigma_algebra ?P" by (rule sigma_algebra_Pow) ``` hoelzl@38656 ` 143` ``` show "finite (space ?P)" using finite_space N.finite_space by auto ``` hoelzl@38656 ` 144` ``` from finite_prod_measure_times[OF assms, of "{}" "{}"] ``` hoelzl@38656 ` 145` ``` show "positive (prod_measure M \ N \)" ``` hoelzl@38656 ` 146` ``` unfolding positive_def by simp ``` hoelzl@38656 ` 147` hoelzl@38656 ` 148` ``` show "additive ?P (prod_measure M \ N \)" ``` hoelzl@38656 ` 149` ``` unfolding additive_def ``` hoelzl@38656 ` 150` ``` apply (auto simp add: sets_eq_Pow prod_measure_def positive_integral_add[symmetric] ``` hoelzl@38656 ` 151` ``` intro!: positive_integral_cong) ``` hoelzl@38656 ` 152` ``` apply (subst N.measure_additive[symmetric]) ``` hoelzl@38656 ` 153` ``` by (auto simp: N.sets_eq_Pow sets_eq_Pow) ``` hoelzl@38656 ` 154` ``` qed ``` hoelzl@38656 ` 155` ``` show "finite (space ?P)" using finite_space N.finite_space by auto ``` hoelzl@38656 ` 156` ``` show "sets ?P = Pow (space ?P)" by simp ``` hoelzl@38656 ` 157` hoelzl@38656 ` 158` ``` fix x assume "x \ space ?P" ``` hoelzl@38656 ` 159` ``` with finite_prod_measure_times[OF assms, of "{fst x}" "{snd x}"] ``` hoelzl@38656 ` 160` ``` finite_measure[of "{fst x}"] N.finite_measure[of "{snd x}"] ``` hoelzl@38656 ` 161` ``` show "prod_measure M \ N \ {x} \ \" ``` hoelzl@38656 ` 162` ``` by (auto simp add: sets_eq_Pow N.sets_eq_Pow elim!: SigmaE) ``` hoelzl@38656 ` 163` ```qed ``` hoelzl@38656 ` 164` hoelzl@38656 ` 165` ```lemma (in finite_measure_space) finite_measure_space_finite_prod_measure_alterantive: ``` hoelzl@38656 ` 166` ``` assumes N: "finite_measure_space N \" ``` hoelzl@38656 ` 167` ``` shows "finite_measure_space \ space = space M \ space N, sets = Pow (space M \ space N) \ (prod_measure M \ N \)" ``` hoelzl@38656 ` 168` ``` (is "finite_measure_space ?M ?m") ``` hoelzl@38656 ` 169` ``` unfolding finite_prod_measure_space[OF N, symmetric] ``` hoelzl@38656 ` 170` ``` using finite_measure_space_finite_prod_measure[OF N] . ``` hoelzl@38656 ` 171` hoelzl@35833 ` 172` `end`