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