src/HOL/Probability/Product_Measure.thy
 author hoelzl Tue Mar 16 16:27:28 2010 +0100 (2010-03-16) changeset 35833 7b7ae5aa396d child 35977 30d42bfd0174 permissions -rw-r--r--
 hoelzl@35833 ` 1` ```theory Product_Measure ``` hoelzl@35833 ` 2` ```imports "~~/src/HOL/Probability/Lebesgue" ``` hoelzl@35833 ` 3` ```begin ``` hoelzl@35833 ` 4` hoelzl@35833 ` 5` ```definition ``` hoelzl@35833 ` 6` ``` "prod_measure M M' = (\a. measure_space.integral M (\s0. measure M' ((\s1. (s0, s1)) -` a)))" ``` hoelzl@35833 ` 7` hoelzl@35833 ` 8` ```definition ``` hoelzl@35833 ` 9` ``` "prod_measure_space M M' \ ``` hoelzl@35833 ` 10` ``` \ space = space M \ space M', ``` hoelzl@35833 ` 11` ``` sets = sets (sigma (space M \ space M') (prod_sets (sets M) (sets M'))), ``` hoelzl@35833 ` 12` ``` measure = prod_measure M M' \" ``` hoelzl@35833 ` 13` hoelzl@35833 ` 14` ```lemma prod_measure_times: ``` hoelzl@35833 ` 15` ``` assumes "measure_space M" and "measure_space M'" and a: "a \ sets M" ``` hoelzl@35833 ` 16` ``` shows "prod_measure M M' (a \ a') = measure M a * measure M' a'" ``` hoelzl@35833 ` 17` ```proof - ``` hoelzl@35833 ` 18` ``` interpret M: measure_space M by fact ``` hoelzl@35833 ` 19` ``` interpret M': measure_space M' by fact ``` hoelzl@35833 ` 20` hoelzl@35833 ` 21` ``` { fix \ ``` hoelzl@35833 ` 22` ``` have "(\\'. (\, \')) -` (a \ a') = (if \ \ a then a' else {})" ``` hoelzl@35833 ` 23` ``` by auto ``` hoelzl@35833 ` 24` ``` hence "measure M' ((\\'. (\, \')) -` (a \ a')) = ``` hoelzl@35833 ` 25` ``` measure M' a' * indicator_fn a \" ``` hoelzl@35833 ` 26` ``` unfolding indicator_fn_def by auto } ``` hoelzl@35833 ` 27` ``` note vimage_eq_indicator = this ``` hoelzl@35833 ` 28` hoelzl@35833 ` 29` ``` show ?thesis ``` hoelzl@35833 ` 30` ``` unfolding prod_measure_def vimage_eq_indicator ``` hoelzl@35833 ` 31` ``` M.integral_cmul_indicator(1)[OF `a \ sets M`] ``` hoelzl@35833 ` 32` ``` by simp ``` hoelzl@35833 ` 33` ```qed ``` hoelzl@35833 ` 34` hoelzl@35833 ` 35` hoelzl@35833 ` 36` hoelzl@35833 ` 37` ```lemma measure_space_finite_prod_measure: ``` hoelzl@35833 ` 38` ``` fixes M :: "('a, 'b) measure_space_scheme" ``` hoelzl@35833 ` 39` ``` and M' :: "('c, 'd) measure_space_scheme" ``` hoelzl@35833 ` 40` ``` assumes "measure_space M" and "measure_space M'" ``` hoelzl@35833 ` 41` ``` and finM: "finite (space M)" "Pow (space M) = sets M" ``` hoelzl@35833 ` 42` ``` and finM': "finite (space M')" "Pow (space M') = sets M'" ``` hoelzl@35833 ` 43` ``` shows "measure_space (prod_measure_space M M')" ``` hoelzl@35833 ` 44` ```proof (rule finite_additivity_sufficient) ``` hoelzl@35833 ` 45` ``` interpret M: measure_space M by fact ``` hoelzl@35833 ` 46` ``` interpret M': measure_space M' by fact ``` hoelzl@35833 ` 47` hoelzl@35833 ` 48` ``` have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'" ``` hoelzl@35833 ` 49` ``` unfolding prod_measure_space_def by simp ``` hoelzl@35833 ` 50` hoelzl@35833 ` 51` ``` have prod_sets: "prod_sets (sets M) (sets M') \ Pow (space M \ space M')" ``` hoelzl@35833 ` 52` ``` using M.sets_into_space M'.sets_into_space unfolding prod_sets_def by auto ``` hoelzl@35833 ` 53` ``` show sigma: "sigma_algebra (prod_measure_space M M')" unfolding prod_measure_space_def ``` hoelzl@35833 ` 54` ``` by (rule sigma_algebra_sigma_sets[where a="prod_sets (sets M) (sets M')"]) ``` hoelzl@35833 ` 55` ``` (simp_all add: sigma_def prod_sets) ``` hoelzl@35833 ` 56` hoelzl@35833 ` 57` ``` then interpret sa: sigma_algebra "prod_measure_space M M'" . ``` hoelzl@35833 ` 58` hoelzl@35833 ` 59` ``` { fix x y assume "y \ sets (prod_measure_space M M')" and "x \ space M" ``` hoelzl@35833 ` 60` ``` hence "y \ space M \ space M'" ``` hoelzl@35833 ` 61` ``` using sa.sets_into_space unfolding prod_measure_space_def by simp ``` hoelzl@35833 ` 62` ``` hence "Pair x -` y \ sets M'" ``` hoelzl@35833 ` 63` ``` using `x \ space M` unfolding finM'(2)[symmetric] by auto } ``` hoelzl@35833 ` 64` ``` note Pair_in_sets = this ``` hoelzl@35833 ` 65` hoelzl@35833 ` 66` ``` show "additive (prod_measure_space M M') (measure (prod_measure_space M M'))" ``` hoelzl@35833 ` 67` ``` unfolding measure additive_def ``` hoelzl@35833 ` 68` ``` proof safe ``` hoelzl@35833 ` 69` ``` fix x y assume x: "x \ sets (prod_measure_space M M')" and y: "y \ sets (prod_measure_space M M')" ``` hoelzl@35833 ` 70` ``` and disj_x_y: "x \ y = {}" ``` hoelzl@35833 ` 71` ``` { fix z have "Pair z -` x \ Pair z -` y = {}" using disj_x_y by auto } ``` hoelzl@35833 ` 72` ``` note Pair_disj = this ``` hoelzl@35833 ` 73` hoelzl@35833 ` 74` ``` from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric] ``` hoelzl@35833 ` 75` ``` show "prod_measure M M' (x \ y) = prod_measure M M' x + prod_measure M M' y" ``` hoelzl@35833 ` 76` ``` unfolding prod_measure_def ``` hoelzl@35833 ` 77` ``` apply (subst (1 2 3) M.integral_finite_singleton[OF finM]) ``` hoelzl@35833 ` 78` ``` by (simp_all add: setsum_addf[symmetric] field_simps) ``` hoelzl@35833 ` 79` ``` qed ``` hoelzl@35833 ` 80` hoelzl@35833 ` 81` ``` show "finite (space (prod_measure_space M M'))" ``` hoelzl@35833 ` 82` ``` unfolding prod_measure_space_def using finM finM' by simp ``` hoelzl@35833 ` 83` hoelzl@35833 ` 84` ``` have singletonM: "\x. x \ space M \ {x} \ sets M" ``` hoelzl@35833 ` 85` ``` unfolding finM(2)[symmetric] by simp ``` hoelzl@35833 ` 86` hoelzl@35833 ` 87` ``` show "positive (prod_measure_space M M') (measure (prod_measure_space M M'))" ``` hoelzl@35833 ` 88` ``` unfolding positive_def ``` hoelzl@35833 ` 89` ``` proof (safe, simp add: M.integral_zero prod_measure_space_def prod_measure_def) ``` hoelzl@35833 ` 90` ``` fix Q assume "Q \ sets (prod_measure_space M M')" ``` hoelzl@35833 ` 91` ``` from Pair_in_sets[OF this] ``` hoelzl@35833 ` 92` ``` show "0 \ measure (prod_measure_space M M') Q" ``` hoelzl@35833 ` 93` ``` unfolding prod_measure_space_def prod_measure_def ``` hoelzl@35833 ` 94` ``` apply (subst M.integral_finite_singleton[OF finM]) ``` hoelzl@35833 ` 95` ``` using M.positive M'.positive singletonM ``` hoelzl@35833 ` 96` ``` by (auto intro!: setsum_nonneg mult_nonneg_nonneg) ``` hoelzl@35833 ` 97` ``` qed ``` hoelzl@35833 ` 98` ```qed ``` hoelzl@35833 ` 99` hoelzl@35833 ` 100` ```lemma measure_space_finite_prod_measure_alterantive: ``` hoelzl@35833 ` 101` ``` assumes "measure_space M" and "measure_space M'" ``` hoelzl@35833 ` 102` ``` and finM: "finite (space M)" "Pow (space M) = sets M" ``` hoelzl@35833 ` 103` ``` and finM': "finite (space M')" "Pow (space M') = sets M'" ``` hoelzl@35833 ` 104` ``` shows "measure_space \ space = space M \ space M', ``` hoelzl@35833 ` 105` ``` sets = Pow (space M \ space M'), ``` hoelzl@35833 ` 106` ``` measure = prod_measure M M' \" ``` hoelzl@35833 ` 107` ``` (is "measure_space ?space") ``` hoelzl@35833 ` 108` ```proof (rule finite_additivity_sufficient) ``` hoelzl@35833 ` 109` ``` interpret M: measure_space M by fact ``` hoelzl@35833 ` 110` ``` interpret M': measure_space M' by fact ``` hoelzl@35833 ` 111` hoelzl@35833 ` 112` ``` show "sigma_algebra ?space" ``` hoelzl@35833 ` 113` ``` using sigma_algebra.sigma_algebra_extend[where M="\ space = space M \ space M', sets = Pow (space M \ space M') \"] ``` hoelzl@35833 ` 114` ``` by (auto intro!: sigma_algebra_Pow) ``` hoelzl@35833 ` 115` ``` then interpret sa: sigma_algebra ?space . ``` hoelzl@35833 ` 116` hoelzl@35833 ` 117` ``` have measure: "measure_space.measure (prod_measure_space M M') = prod_measure M M'" ``` hoelzl@35833 ` 118` ``` unfolding prod_measure_space_def by simp ``` hoelzl@35833 ` 119` hoelzl@35833 ` 120` ``` { fix x y assume "y \ sets ?space" and "x \ space M" ``` hoelzl@35833 ` 121` ``` hence "y \ space M \ space M'" ``` hoelzl@35833 ` 122` ``` using sa.sets_into_space by simp ``` hoelzl@35833 ` 123` ``` hence "Pair x -` y \ sets M'" ``` hoelzl@35833 ` 124` ``` using `x \ space M` unfolding finM'(2)[symmetric] by auto } ``` hoelzl@35833 ` 125` ``` note Pair_in_sets = this ``` hoelzl@35833 ` 126` hoelzl@35833 ` 127` ``` show "additive ?space (measure ?space)" ``` hoelzl@35833 ` 128` ``` unfolding measure additive_def ``` hoelzl@35833 ` 129` ``` proof safe ``` hoelzl@35833 ` 130` ``` fix x y assume x: "x \ sets ?space" and y: "y \ sets ?space" ``` hoelzl@35833 ` 131` ``` and disj_x_y: "x \ y = {}" ``` hoelzl@35833 ` 132` ``` { fix z have "Pair z -` x \ Pair z -` y = {}" using disj_x_y by auto } ``` hoelzl@35833 ` 133` ``` note Pair_disj = this ``` hoelzl@35833 ` 134` hoelzl@35833 ` 135` ``` from M'.measure_additive[OF Pair_in_sets[OF x] Pair_in_sets[OF y] Pair_disj, symmetric] ``` hoelzl@35833 ` 136` ``` show "measure ?space (x \ y) = measure ?space x + measure ?space y" ``` hoelzl@35833 ` 137` ``` apply (simp add: prod_measure_def) ``` hoelzl@35833 ` 138` ``` apply (subst (1 2 3) M.integral_finite_singleton[OF finM]) ``` hoelzl@35833 ` 139` ``` by (simp_all add: setsum_addf[symmetric] field_simps) ``` hoelzl@35833 ` 140` ``` qed ``` hoelzl@35833 ` 141` hoelzl@35833 ` 142` ``` show "finite (space ?space)" using finM finM' by simp ``` hoelzl@35833 ` 143` hoelzl@35833 ` 144` ``` have singletonM: "\x. x \ space M \ {x} \ sets M" ``` hoelzl@35833 ` 145` ``` unfolding finM(2)[symmetric] by simp ``` hoelzl@35833 ` 146` hoelzl@35833 ` 147` ``` show "positive ?space (measure ?space)" ``` hoelzl@35833 ` 148` ``` unfolding positive_def ``` hoelzl@35833 ` 149` ``` proof (safe, simp add: M.integral_zero prod_measure_def) ``` hoelzl@35833 ` 150` ``` fix Q assume "Q \ sets ?space" ``` hoelzl@35833 ` 151` ``` from Pair_in_sets[OF this] ``` hoelzl@35833 ` 152` ``` show "0 \ measure ?space Q" ``` hoelzl@35833 ` 153` ``` unfolding prod_measure_space_def prod_measure_def ``` hoelzl@35833 ` 154` ``` apply (subst M.integral_finite_singleton[OF finM]) ``` hoelzl@35833 ` 155` ``` using M.positive M'.positive singletonM ``` hoelzl@35833 ` 156` ``` by (auto intro!: setsum_nonneg mult_nonneg_nonneg) ``` hoelzl@35833 ` 157` ``` qed ``` hoelzl@35833 ` 158` ```qed ``` hoelzl@35833 ` 159` hoelzl@35833 ` 160` `end`