src/HOL/Probability/Probability_Space.thy
 author hoelzl Thu, 02 Sep 2010 17:28:00 +0200 changeset 39096 111756225292 parent 39092 98de40859858 child 39097 943c7b348524 permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 1` ```theory Probability_Space ``` 39083 e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 2` ```imports Lebesgue_Integration Radon_Nikodym ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 3` ```begin ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 4` 39096 111756225292 merged hoelzl parents: 39092 diff changeset ` 5` 111756225292 merged hoelzl parents: 39092 diff changeset ` 6` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 7` ```locale prob_space = measure_space + ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 8` ``` assumes measure_space_1: "\ (space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 9` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 10` ```sublocale prob_space < finite_measure ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 11` ```proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 12` ``` from measure_space_1 show "\ (space M) \ \" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 13` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 14` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 15` ```context prob_space ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 16` ```begin ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 17` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 18` ```abbreviation "events \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 19` ```abbreviation "prob \ \A. real (\ A)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 20` ```abbreviation "prob_preserving \ measure_preserving" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 21` ```abbreviation "random_variable \ \ s X. X \ measurable M s" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 22` ```abbreviation "expectation \ integral" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 23` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 24` ```definition ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 25` ``` "indep A B \ A \ events \ B \ events \ prob (A \ B) = prob A * prob B" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 26` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 27` ```definition ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 28` ``` "indep_families F G \ (\ A \ F. \ B \ G. indep A B)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 29` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 30` ```definition ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 31` ``` "distribution X = (\s. \ ((X -` s) \ (space M)))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 32` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 33` ```abbreviation ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 34` ``` "joint_distribution X Y \ distribution (\x. (X x, Y x))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 35` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 36` ```lemma prob_space: "prob (space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 37` ``` unfolding measure_space_1 by simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 38` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 39` ```lemma measure_le_1[simp, intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 40` ``` assumes "A \ events" shows "\ A \ 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 41` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 42` ``` have "\ A \ \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 43` ``` using assms sets_into_space by(auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 44` ``` also note measure_space_1 ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 45` ``` finally show ?thesis . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 46` ```qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 47` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 48` ```lemma prob_compl: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 49` ``` assumes "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 50` ``` shows "prob (space M - A) = 1 - prob A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 51` ``` using `A \ events`[THEN sets_into_space] `A \ events` measure_space_1 ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 52` ``` by (subst real_finite_measure_Diff) auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 53` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 54` ```lemma indep_space: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 55` ``` assumes "s \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 56` ``` shows "indep (space M) s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 57` ``` using assms prob_space by (simp add: indep_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 58` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 59` ```lemma prob_space_increasing: "increasing M prob" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 60` ``` by (auto intro!: real_measure_mono simp: increasing_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 61` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 62` ```lemma prob_zero_union: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 63` ``` assumes "s \ events" "t \ events" "prob t = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 64` ``` shows "prob (s \ t) = prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 65` ```using assms ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 66` ```proof - ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 67` ``` have "prob (s \ t) \ prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 68` ``` using real_finite_measure_subadditive[of s t] assms by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 69` ``` moreover have "prob (s \ t) \ prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 70` ``` using assms by (blast intro: real_measure_mono) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 71` ``` ultimately show ?thesis by simp ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 72` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 73` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 74` ```lemma prob_eq_compl: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 75` ``` assumes "s \ events" "t \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 76` ``` assumes "prob (space M - s) = prob (space M - t)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 77` ``` shows "prob s = prob t" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 78` ``` using assms prob_compl by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 79` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 80` ```lemma prob_one_inter: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 81` ``` assumes events:"s \ events" "t \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 82` ``` assumes "prob t = 1" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 83` ``` shows "prob (s \ t) = prob s" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 84` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 85` ``` have "prob ((space M - s) \ (space M - t)) = prob (space M - s)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 86` ``` using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 87` ``` also have "(space M - s) \ (space M - t) = space M - (s \ t)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 88` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 89` ``` finally show "prob (s \ t) = prob s" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 90` ``` using events by (auto intro!: prob_eq_compl[of "s \ t" s]) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 91` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 92` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 93` ```lemma prob_eq_bigunion_image: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 94` ``` assumes "range f \ events" "range g \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 95` ``` assumes "disjoint_family f" "disjoint_family g" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 96` ``` assumes "\ n :: nat. prob (f n) = prob (g n)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 97` ``` shows "(prob (\ i. f i) = prob (\ i. g i))" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 98` ```using assms ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 99` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 100` ``` have a: "(\ i. prob (f i)) sums (prob (\ i. f i))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 101` ``` by (rule real_finite_measure_UNION[OF assms(1,3)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 102` ``` have b: "(\ i. prob (g i)) sums (prob (\ i. g i))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 103` ``` by (rule real_finite_measure_UNION[OF assms(2,4)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 104` ``` show ?thesis using sums_unique[OF b] sums_unique[OF a] assms by simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 105` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 106` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 107` ```lemma prob_countably_zero: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 108` ``` assumes "range c \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 109` ``` assumes "\ i. prob (c i) = 0" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 110` ``` shows "prob (\ i :: nat. c i) = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 111` ```proof (rule antisym) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 112` ``` show "prob (\ i :: nat. c i) \ 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 113` ``` using real_finite_measurable_countably_subadditive[OF assms(1)] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 114` ``` by (simp add: assms(2) suminf_zero summable_zero) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 115` ``` show "0 \ prob (\ i :: nat. c i)" by (rule real_pinfreal_nonneg) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 116` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 117` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 118` ```lemma indep_sym: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 119` ``` "indep a b \ indep b a" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 120` ```unfolding indep_def using Int_commute[of a b] by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 121` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 122` ```lemma indep_refl: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 123` ``` assumes "a \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 124` ``` shows "indep a a = (prob a = 0) \ (prob a = 1)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 125` ```using assms unfolding indep_def by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 126` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 127` ```lemma prob_equiprobable_finite_unions: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 128` ``` assumes "s \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 129` ``` assumes s_finite: "finite s" "\x. x \ s \ {x} \ events" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 130` ``` assumes "\ x y. \x \ s; y \ s\ \ (prob {x} = prob {y})" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 131` ``` shows "prob s = real (card s) * prob {SOME x. x \ s}" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 132` ```proof (cases "s = {}") ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 133` ``` case False hence "\ x. x \ s" by blast ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 134` ``` from someI_ex[OF this] assms ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 135` ``` have prob_some: "\ x. x \ s \ prob {x} = prob {SOME y. y \ s}" by blast ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 136` ``` have "prob s = (\ x \ s. prob {x})" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 137` ``` using real_finite_measure_finite_singelton[OF s_finite] by simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 138` ``` also have "\ = (\ x \ s. prob {SOME y. y \ s})" using prob_some by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 139` ``` also have "\ = real (card s) * prob {(SOME x. x \ s)}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 140` ``` using setsum_constant assms by (simp add: real_eq_of_nat) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 141` ``` finally show ?thesis by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 142` ```qed simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 143` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 144` ```lemma prob_real_sum_image_fn: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 145` ``` assumes "e \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 146` ``` assumes "\ x. x \ s \ e \ f x \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 147` ``` assumes "finite s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 148` ``` assumes disjoint: "\ x y. \x \ s ; y \ s ; x \ y\ \ f x \ f y = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 149` ``` assumes upper: "space M \ (\ i \ s. f i)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 150` ``` shows "prob e = (\ x \ s. prob (e \ f x))" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 151` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 152` ``` have e: "e = (\ i \ s. e \ f i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 153` ``` using `e \ events` sets_into_space upper by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 154` ``` hence "prob e = prob (\ i \ s. e \ f i)" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 155` ``` also have "\ = (\ x \ s. prob (e \ f x))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 156` ``` proof (rule real_finite_measure_finite_Union) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 157` ``` show "finite s" by fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 158` ``` show "\i. i \ s \ e \ f i \ events" by fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 159` ``` show "disjoint_family_on (\i. e \ f i) s" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 160` ``` using disjoint by (auto simp: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 161` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 162` ``` finally show ?thesis . ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 163` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 164` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 165` ```lemma distribution_prob_space: ``` 39089 df379a447753 vimage of measurable function is a measure space hoelzl parents: 39085 diff changeset ` 166` ``` assumes S: "sigma_algebra S" "random_variable S X" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 167` ``` shows "prob_space S (distribution X)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 168` ```proof - ``` 39089 df379a447753 vimage of measurable function is a measure space hoelzl parents: 39085 diff changeset ` 169` ``` interpret S: measure_space S "distribution X" ``` df379a447753 vimage of measurable function is a measure space hoelzl parents: 39085 diff changeset ` 170` ``` using measure_space_vimage[OF S(2,1)] unfolding distribution_def . ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 171` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 172` ``` proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 173` ``` have "X -` space S \ space M = space M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 174` ``` using `random_variable S X` by (auto simp: measurable_def) ``` 39089 df379a447753 vimage of measurable function is a measure space hoelzl parents: 39085 diff changeset ` 175` ``` then show "distribution X (space S) = 1" ``` df379a447753 vimage of measurable function is a measure space hoelzl parents: 39085 diff changeset ` 176` ``` using measure_space_1 by (simp add: distribution_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 177` ``` qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 178` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 179` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 180` ```lemma distribution_lebesgue_thm1: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 181` ``` assumes "random_variable s X" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 182` ``` assumes "A \ sets s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 183` ``` shows "real (distribution X A) = expectation (indicator (X -` A \ space M))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 184` ```unfolding distribution_def ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 185` ```using assms unfolding measurable_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 186` ```using integral_indicator by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 187` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 188` ```lemma distribution_lebesgue_thm2: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 189` ``` assumes "sigma_algebra S" "random_variable S X" and "A \ sets S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 190` ``` shows "distribution X A = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 191` ``` measure_space.positive_integral S (distribution X) (indicator A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 192` ``` (is "_ = measure_space.positive_integral _ ?D _") ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 193` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 194` ``` interpret S: prob_space S "distribution X" using assms(1,2) by (rule distribution_prob_space) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 195` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 196` ``` show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 197` ``` using S.positive_integral_indicator(1) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 198` ``` using assms unfolding distribution_def by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 199` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 200` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 201` ```lemma finite_expectation1: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 202` ``` assumes "finite (X`space M)" and rv: "random_variable borel_space X" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 203` ``` shows "expectation X = (\ r \ X ` space M. r * prob (X -` {r} \ space M))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 204` ```proof (rule integral_on_finite(2)[OF assms(2,1)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 205` ``` fix x have "X -` {x} \ space M \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 206` ``` using rv unfolding measurable_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 207` ``` thus "\ (X -` {x} \ space M) \ \" using finite_measure by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 208` ```qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 209` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 210` ```lemma finite_expectation: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 211` ``` assumes "finite (space M)" "random_variable borel_space X" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 212` ``` shows "expectation X = (\ r \ X ` (space M). r * real (distribution X {r}))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 213` ``` using assms unfolding distribution_def using finite_expectation1 by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 214` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 215` ```lemma prob_x_eq_1_imp_prob_y_eq_0: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 216` ``` assumes "{x} \ events" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 217` ``` assumes "prob {x} = 1" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 218` ``` assumes "{y} \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 219` ``` assumes "y \ x" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 220` ``` shows "prob {y} = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 221` ``` using prob_one_inter[of "{y}" "{x}"] assms by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 222` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 223` ```lemma distribution_empty[simp]: "distribution X {} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 224` ``` unfolding distribution_def by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 225` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 226` ```lemma distribution_space[simp]: "distribution X (X ` space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 227` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 228` ``` have "X -` X ` space M \ space M = space M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 229` ``` thus ?thesis unfolding distribution_def by (simp add: measure_space_1) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 230` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 231` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 232` ```lemma distribution_one: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 233` ``` assumes "random_variable M X" and "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 234` ``` shows "distribution X A \ 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 235` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 236` ``` have "distribution X A \ \ (space M)" unfolding distribution_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 237` ``` using assms[unfolded measurable_def] by (auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 238` ``` thus ?thesis by (simp add: measure_space_1) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 239` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 240` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 241` ```lemma distribution_finite: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 242` ``` assumes "random_variable M X" and "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 243` ``` shows "distribution X A \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 244` ``` using distribution_one[OF assms] by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 245` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 246` ```lemma distribution_x_eq_1_imp_distribution_y_eq_0: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 247` ``` assumes X: "random_variable \space = X ` (space M), sets = Pow (X ` (space M))\ X" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 248` ``` (is "random_variable ?S X") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 249` ``` assumes "distribution X {x} = 1" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 250` ``` assumes "y \ x" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 251` ``` shows "distribution X {y} = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 252` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 253` ``` have "sigma_algebra ?S" by (rule sigma_algebra_Pow) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 254` ``` from distribution_prob_space[OF this X] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 255` ``` interpret S: prob_space ?S "distribution X" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 256` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 257` ``` have x: "{x} \ sets ?S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 258` ``` proof (rule ccontr) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 259` ``` assume "{x} \ sets ?S" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 260` ``` hence "X -` {x} \ space M = {}" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 261` ``` thus "False" using assms unfolding distribution_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 262` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 263` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 264` ``` have [simp]: "{y} \ {x} = {}" "{x} - {y} = {x}" using `y \ x` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 265` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 266` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 267` ``` proof cases ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 268` ``` assume "{y} \ sets ?S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 269` ``` with `{x} \ sets ?S` assms show "distribution X {y} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 270` ``` using S.measure_inter_full_set[of "{y}" "{x}"] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 271` ``` by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 272` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 273` ``` assume "{y} \ sets ?S" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 274` ``` hence "X -` {y} \ space M = {}" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 275` ``` thus "distribution X {y} = 0" unfolding distribution_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 276` ``` qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 277` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 278` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 279` ```end ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 280` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 281` ```locale finite_prob_space = prob_space + finite_measure_space ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 282` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 283` ```lemma finite_prob_space_eq: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 284` ``` "finite_prob_space M \ \ finite_measure_space M \ \ \ (space M) = 1" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 285` ``` unfolding finite_prob_space_def finite_measure_space_def prob_space_def prob_space_axioms_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 286` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 287` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 288` ```lemma (in prob_space) not_empty: "space M \ {}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 289` ``` using prob_space empty_measure by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 290` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 291` ```lemma (in finite_prob_space) sum_over_space_eq_1: "(\x\space M. \ {x}) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 292` ``` using measure_space_1 sum_over_space by simp ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 293` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 294` ```lemma (in finite_prob_space) positive_distribution: "0 \ distribution X x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 295` ``` unfolding distribution_def by simp ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 296` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 297` ```lemma (in finite_prob_space) joint_distribution_restriction_fst: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 298` ``` "joint_distribution X Y A \ distribution X (fst ` A)" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 299` ``` unfolding distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 300` ```proof (safe intro!: measure_mono) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 301` ``` fix x assume "x \ space M" and *: "(X x, Y x) \ A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 302` ``` show "x \ X -` fst ` A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 303` ``` by (auto intro!: image_eqI[OF _ *]) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 304` ```qed (simp_all add: sets_eq_Pow) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 305` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 306` ```lemma (in finite_prob_space) joint_distribution_restriction_snd: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 307` ``` "joint_distribution X Y A \ distribution Y (snd ` A)" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 308` ``` unfolding distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 309` ```proof (safe intro!: measure_mono) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 310` ``` fix x assume "x \ space M" and *: "(X x, Y x) \ A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 311` ``` show "x \ Y -` snd ` A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 312` ``` by (auto intro!: image_eqI[OF _ *]) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 313` ```qed (simp_all add: sets_eq_Pow) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 314` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 315` ```lemma (in finite_prob_space) distribution_order: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 316` ``` shows "0 \ distribution X x'" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 317` ``` and "(distribution X x' \ 0) \ (0 < distribution X x')" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 318` ``` and "r \ joint_distribution X Y {(x, y)} \ r \ distribution X {x}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 319` ``` and "r \ joint_distribution X Y {(x, y)} \ r \ distribution Y {y}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 320` ``` and "r < joint_distribution X Y {(x, y)} \ r < distribution X {x}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 321` ``` and "r < joint_distribution X Y {(x, y)} \ r < distribution Y {y}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 322` ``` and "distribution X {x} = 0 \ joint_distribution X Y {(x, y)} = 0" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 323` ``` and "distribution Y {y} = 0 \ joint_distribution X Y {(x, y)} = 0" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 324` ``` using positive_distribution[of X x'] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 325` ``` positive_distribution[of "\x. (X x, Y x)" "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 326` ``` joint_distribution_restriction_fst[of X Y "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 327` ``` joint_distribution_restriction_snd[of X Y "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 328` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 329` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 330` ```lemma (in finite_prob_space) finite_prob_space_of_images: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 331` ``` "finite_prob_space \ space = X ` space M, sets = Pow (X ` space M)\ (distribution X)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 332` ``` by (simp add: finite_prob_space_eq finite_measure_space) ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 333` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 334` ```lemma (in finite_prob_space) finite_product_prob_space_of_images: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 335` ``` "finite_prob_space \ space = X ` space M \ Y ` space M, sets = Pow (X ` space M \ Y ` space M)\ ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 336` ``` (joint_distribution X Y)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 337` ``` (is "finite_prob_space ?S _") ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 338` ```proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 339` ``` have "X -` X ` space M \ Y -` Y ` space M \ space M = space M" by auto ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 340` ``` thus "joint_distribution X Y (X ` space M \ Y ` space M) = 1" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 341` ``` by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 342` ```qed ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 343` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 344` ```lemma (in prob_space) prob_space_subalgebra: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 345` ``` assumes "N \ sets M" "sigma_algebra (M\ sets := N \)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 346` ``` shows "prob_space (M\ sets := N \) \" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 347` ```proof - ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 348` ``` interpret N: measure_space "M\ sets := N \" \ ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 349` ``` using measure_space_subalgebra[OF assms] . ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 350` ``` show ?thesis ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 351` ``` proof qed (simp add: measure_space_1) ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 352` ```qed ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 353` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 354` ```lemma (in prob_space) prob_space_of_restricted_space: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 355` ``` assumes "\ A \ 0" "\ A \ \" "A \ sets M" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 356` ``` shows "prob_space (restricted_space A) (\S. \ S / \ A)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 357` ``` unfolding prob_space_def prob_space_axioms_def ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 358` ```proof ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 359` ``` show "\ (space (restricted_space A)) / \ A = 1" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 360` ``` using `\ A \ 0` `\ A \ \` by (auto simp: pinfreal_noteq_omega_Ex) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 361` ``` have *: "\S. \ S / \ A = inverse (\ A) * \ S" by (simp add: mult_commute) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 362` ``` interpret A: measure_space "restricted_space A" \ ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 363` ``` using `A \ sets M` by (rule restricted_measure_space) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 364` ``` show "measure_space (restricted_space A) (\S. \ S / \ A)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 365` ``` proof ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 366` ``` show "\ {} / \ A = 0" by auto ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 367` ``` show "countably_additive (restricted_space A) (\S. \ S / \ A)" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 368` ``` unfolding countably_additive_def psuminf_cmult_right * ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 369` ``` using A.measure_countably_additive by auto ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 370` ``` qed ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 371` ```qed ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 372` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 373` ```lemma finite_prob_spaceI: ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 374` ``` assumes "finite (space M)" "sets M = Pow(space M)" "\ (space M) = 1" "\ {} = 0" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 375` ``` and "\A B. A\space M \ B\space M \ A \ B = {} \ \ (A \ B) = \ A + \ B" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 376` ``` shows "finite_prob_space M \" ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 377` ``` unfolding finite_prob_space_eq ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 378` ```proof ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 379` ``` show "finite_measure_space M \" using assms ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 380` ``` by (auto intro!: finite_measure_spaceI) ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 381` ``` show "\ (space M) = 1" by fact ``` 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 382` ```qed ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 383` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 384` ```lemma (in finite_prob_space) finite_measure_space: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 385` ``` shows "finite_measure_space \space = X ` space M, sets = Pow (X ` space M)\ (distribution X)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 386` ``` (is "finite_measure_space ?S _") ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 387` ```proof (rule finite_measure_spaceI, simp_all) ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 388` ``` show "finite (X ` space M)" using finite_space by simp ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 389` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 390` ``` show "positive (distribution X)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 391` ``` unfolding distribution_def positive_def using sets_eq_Pow by auto ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 392` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 393` ``` show "additive ?S (distribution X)" unfolding additive_def distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 394` ``` proof (simp, safe) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 395` ``` fix x y ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 396` ``` have x: "(X -` x) \ space M \ sets M" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 397` ``` and y: "(X -` y) \ space M \ sets M" using sets_eq_Pow by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 398` ``` assume "x \ y = {}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 399` ``` hence "X -` x \ space M \ (X -` y \ space M) = {}" by auto ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 400` ``` from additive[unfolded additive_def, rule_format, OF x y] this ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 401` ``` finite_measure[OF x] finite_measure[OF y] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 402` ``` have "\ (((X -` x) \ (X -` y)) \ space M) = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 403` ``` \ ((X -` x) \ space M) + \ ((X -` y) \ space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 404` ``` by (subst Int_Un_distrib2) auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 405` ``` thus "\ ((X -` x \ X -` y) \ space M) = \ (X -` x \ space M) + \ (X -` y \ space M)" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 406` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 407` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 408` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 409` ``` { fix x assume "x \ X ` space M" thus "distribution X {x} \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 410` ``` unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) } ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 411` ```qed ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 412` 39096 111756225292 merged hoelzl parents: 39092 diff changeset ` 413` ```lemma (in finite_prob_space) finite_product_measure_space: ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 414` ``` assumes "finite s1" "finite s2" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 415` ``` shows "finite_measure_space \ space = s1 \ s2, sets = Pow (s1 \ s2)\ (joint_distribution X Y)" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 416` ``` (is "finite_measure_space ?M ?D") ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 417` ```proof (rule finite_Pow_additivity_sufficient) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 418` ``` show "positive ?D" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 419` ``` unfolding positive_def using assms sets_eq_Pow ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 420` ``` by (simp add: distribution_def) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 421` 111756225292 merged hoelzl parents: 39092 diff changeset ` 422` ``` show "additive ?M ?D" unfolding additive_def ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 423` ``` proof safe ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 424` ``` fix x y ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 425` ``` have A: "((\x. (X x, Y x)) -` x) \ space M \ sets M" using assms sets_eq_Pow by auto ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 426` ``` have B: "((\x. (X x, Y x)) -` y) \ space M \ sets M" using assms sets_eq_Pow by auto ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 427` ``` assume "x \ y = {}" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 428` ``` hence "(\x. (X x, Y x)) -` x \ space M \ ((\x. (X x, Y x)) -` y \ space M) = {}" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 429` ``` by auto ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 430` ``` from additive[unfolded additive_def, rule_format, OF A B] this ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 431` ``` finite_measure[OF A] finite_measure[OF B] ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 432` ``` show "?D (x \ y) = ?D x + ?D y" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 433` ``` apply (simp add: distribution_def) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 434` ``` apply (subst Int_Un_distrib2) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 435` ``` by (auto simp: real_of_pinfreal_add) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 436` ``` qed ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 437` 111756225292 merged hoelzl parents: 39092 diff changeset ` 438` ``` show "finite (space ?M)" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 439` ``` using assms by auto ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 440` 111756225292 merged hoelzl parents: 39092 diff changeset ` 441` ``` show "sets ?M = Pow (space ?M)" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 442` ``` by simp ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 443` 111756225292 merged hoelzl parents: 39092 diff changeset ` 444` ``` { fix x assume "x \ space ?M" thus "?D {x} \ \" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 445` ``` unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) } ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 446` ```qed ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 447` 111756225292 merged hoelzl parents: 39092 diff changeset ` 448` ```lemma (in finite_measure_space) finite_product_measure_space_of_images: ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 449` ``` shows "finite_measure_space \ space = X ` space M \ Y ` space M, ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 450` ``` sets = Pow (X ` space M \ Y ` space M) \ ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 451` ``` (joint_distribution X Y)" ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 452` ``` using finite_space by (auto intro!: finite_product_measure_space) ``` 111756225292 merged hoelzl parents: 39092 diff changeset ` 453` 39085 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 454` ```section "Conditional Expectation and Probability" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 455` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 456` ```lemma (in prob_space) conditional_expectation_exists: ``` 39083 e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 457` ``` fixes X :: "'a \ pinfreal" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 458` ``` assumes borel: "X \ borel_measurable M" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 459` ``` and N_subalgebra: "N \ sets M" "sigma_algebra (M\ sets := N \)" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 460` ``` shows "\Y\borel_measurable (M\ sets := N \). \C\N. ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 461` ``` positive_integral (\x. Y x * indicator C x) = positive_integral (\x. X x * indicator C x)" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 462` ```proof - ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 463` ``` interpret P: prob_space "M\ sets := N \" \ ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 464` ``` using prob_space_subalgebra[OF N_subalgebra] . ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 465` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 466` ``` let "?f A" = "\x. X x * indicator A x" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 467` ``` let "?Q A" = "positive_integral (?f A)" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 468` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 469` ``` from measure_space_density[OF borel] ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 470` ``` have Q: "measure_space (M\ sets := N \) ?Q" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 471` ``` by (rule measure_space.measure_space_subalgebra[OF _ N_subalgebra]) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 472` ``` then interpret Q: measure_space "M\ sets := N \" ?Q . ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 473` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 474` ``` have "P.absolutely_continuous ?Q" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 475` ``` unfolding P.absolutely_continuous_def ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 476` ``` proof (safe, simp) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 477` ``` fix A assume "A \ N" "\ A = 0" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 478` ``` moreover then have f_borel: "?f A \ borel_measurable M" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 479` ``` using borel N_subalgebra by (auto intro: borel_measurable_indicator) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 480` ``` moreover have "{x\space M. ?f A x \ 0} = (?f A -` {0<..} \ space M) \ A" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 481` ``` by (auto simp: indicator_def) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 482` ``` moreover have "\ \ \ \ A" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 483` ``` using `A \ N` N_subalgebra f_borel ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 484` ``` by (auto intro!: measure_mono Int[of _ A] measurable_sets) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 485` ``` ultimately show "?Q A = 0" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 486` ``` by (simp add: positive_integral_0_iff) ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 487` ``` qed ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 488` ``` from P.Radon_Nikodym[OF Q this] ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 489` ``` obtain Y where Y: "Y \ borel_measurable (M\sets := N\)" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 490` ``` "\A. A \ sets (M\sets:=N\) \ ?Q A = P.positive_integral (\x. Y x * indicator A x)" ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 491` ``` by blast ``` 39084 7a6ecce97661 proved existence of conditional expectation hoelzl parents: 39083 diff changeset ` 492` ``` with N_subalgebra show ?thesis ``` 7a6ecce97661 proved existence of conditional expectation hoelzl parents: 39083 diff changeset ` 493` ``` by (auto intro!: bexI[OF _ Y(1)]) ``` 39083 e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 494` ```qed ``` e46acc0ea1fe introduced integration on subalgebras hoelzl parents: 38656 diff changeset ` 495` 39085 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 496` ```definition (in prob_space) ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 497` ``` "conditional_expectation N X = (SOME Y. Y\borel_measurable (M\sets:=N\) ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 498` ``` \ (\C\N. positive_integral (\x. Y x * indicator C x) = positive_integral (\x. X x * indicator C x)))" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 499` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 500` ```abbreviation (in prob_space) ``` 39092 98de40859858 move lemmas to correct theory files hoelzl parents: 39091 diff changeset ` 501` ``` "conditional_prob N A \ conditional_expectation N (indicator A)" ``` 39085 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 502` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 503` ```lemma (in prob_space) ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 504` ``` fixes X :: "'a \ pinfreal" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 505` ``` assumes borel: "X \ borel_measurable M" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 506` ``` and N_subalgebra: "N \ sets M" "sigma_algebra (M\ sets := N \)" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 507` ``` shows borel_measurable_conditional_expectation: ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 508` ``` "conditional_expectation N X \ borel_measurable (M\ sets := N \)" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 509` ``` and conditional_expectation: "\C. C \ N \ ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 510` ``` positive_integral (\x. conditional_expectation N X x * indicator C x) = ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 511` ``` positive_integral (\x. X x * indicator C x)" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 512` ``` (is "\C. C \ N \ ?eq C") ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 513` ```proof - ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 514` ``` note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 515` ``` then show "conditional_expectation N X \ borel_measurable (M\ sets := N \)" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 516` ``` unfolding conditional_expectation_def by (rule someI2_ex) blast ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 517` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 518` ``` from CE show "\C. C\N \ ?eq C" ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 519` ``` unfolding conditional_expectation_def by (rule someI2_ex) blast ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 520` ```qed ``` 8b7c009da23c added definition of conditional expectation hoelzl parents: 39084 diff changeset ` 521` 39091 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 522` ```lemma (in sigma_algebra) factorize_measurable_function: ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 523` ``` fixes Z :: "'a \ pinfreal" and Y :: "'a \ 'c" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 524` ``` assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 525` ``` shows "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 526` ``` \ (\g\borel_measurable M'. \x\space M. Z x = g (Y x))" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 527` ```proof safe ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 528` ``` interpret M': sigma_algebra M' by fact ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 529` ``` have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 530` ``` from M'.sigma_algebra_vimage[OF this] ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 531` ``` interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 532` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 533` ``` { fix g :: "'c \ pinfreal" assume "g \ borel_measurable M'" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 534` ``` with M'.measurable_vimage_algebra[OF Y] ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 535` ``` have "g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 536` ``` by (rule measurable_comp) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 537` ``` moreover assume "\x\space M. Z x = g (Y x)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 538` ``` then have "Z \ borel_measurable (M'.vimage_algebra (space M) Y) \ ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 539` ``` g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 540` ``` by (auto intro!: measurable_cong) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 541` ``` ultimately show "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 542` ``` by simp } ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 543` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 544` ``` assume "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 545` ``` from va.borel_measurable_implies_simple_function_sequence[OF this] ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 546` ``` obtain f where f: "\i. va.simple_function (f i)" and "f \ Z" by blast ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 547` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 548` ``` have "\i. \g. M'.simple_function g \ (\x\space M. f i x = g (Y x))" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 549` ``` proof ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 550` ``` fix i ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 551` ``` from f[of i] have "finite (f i`space M)" and B_ex: ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 552` ``` "\z\(f i)`space M. \B. B \ sets M' \ (f i) -` {z} \ space M = Y -` B \ space M" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 553` ``` unfolding va.simple_function_def by auto ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 554` ``` from B_ex[THEN bchoice] guess B .. note B = this ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 555` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 556` ``` let ?g = "\x. \z\f i`space M. z * indicator (B z) x" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 557` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 558` ``` show "\g. M'.simple_function g \ (\x\space M. f i x = g (Y x))" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 559` ``` proof (intro exI[of _ ?g] conjI ballI) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 560` ``` show "M'.simple_function ?g" using B by auto ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 561` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 562` ``` fix x assume "x \ space M" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 563` ``` then have "\z. z \ f i`space M \ indicator (B z) (Y x) = (indicator (f i -` {z} \ space M) x::pinfreal)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 564` ``` unfolding indicator_def using B by auto ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 565` ``` then show "f i x = ?g (Y x)" using `x \ space M` f[of i] ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 566` ``` by (subst va.simple_function_indicator_representation) auto ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 567` ``` qed ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 568` ``` qed ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 569` ``` from choice[OF this] guess g .. note g = this ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 570` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 571` ``` show "\g\borel_measurable M'. \x\space M. Z x = g (Y x)" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 572` ``` proof (intro ballI bexI) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 573` ``` show "(SUP i. g i) \ borel_measurable M'" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 574` ``` using g by (auto intro: M'.borel_measurable_simple_function) ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 575` ``` fix x assume "x \ space M" ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 576` ``` have "Z x = (SUP i. f i) x" using `f \ Z` unfolding isoton_def by simp ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 577` ``` also have "\ = (SUP i. g i) (Y x)" unfolding SUPR_fun_expand ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 578` ``` using g `x \ space M` by simp ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 579` ``` finally show "Z x = (SUP i. g i) (Y x)" . ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 580` ``` qed ``` 11314c196e11 factorizable measurable functions hoelzl parents: 39090 diff changeset ` 581` ```qed ``` 39090 a2d38b8b693e Introduced sigma algebra generated by function preimages. hoelzl parents: 39089 diff changeset ` 582` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 583` ```end ```