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