src/HOL/Probability/Probability_Space.thy
 author hoelzl Mon, 23 Aug 2010 19:35:57 +0200 changeset 38656 d5d342611edb parent 36624 25153c08655e child 39083 e46acc0ea1fe permissions -rw-r--r--
Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 1` ```theory Probability_Space ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 2` ```imports Lebesgue_Integration ``` 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` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 5` ```lemma (in measure_space) measure_inter_full_set: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 6` ``` assumes "S \ sets M" "T \ sets M" and not_\: "\ (T - S) \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 7` ``` assumes T: "\ T = \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 8` ``` shows "\ (S \ T) = \ S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 9` ```proof (rule antisym) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 10` ``` show " \ (S \ T) \ \ S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 11` ``` using assms by (auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 12` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 13` ``` show "\ S \ \ (S \ T)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 14` ``` proof (rule ccontr) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 15` ``` assume contr: "\ ?thesis" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 16` ``` have "\ (space M) = \ ((T - S) \ (S \ T))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 17` ``` unfolding T[symmetric] by (auto intro!: arg_cong[where f="\"]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 18` ``` also have "\ \ \ (T - S) + \ (S \ T)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 19` ``` using assms by (auto intro!: measure_subadditive) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 20` ``` also have "\ < \ (T - S) + \ S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 21` ``` by (rule pinfreal_less_add[OF not_\]) (insert contr, auto) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 22` ``` also have "\ = \ (T \ S)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 23` ``` using assms by (subst measure_additive) auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 24` ``` also have "\ \ \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 25` ``` using assms sets_into_space by (auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 26` ``` finally show False .. ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 27` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 28` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 29` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 30` ```lemma (in finite_measure) finite_measure_inter_full_set: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 31` ``` assumes "S \ sets M" "T \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 32` ``` assumes T: "\ T = \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 33` ``` shows "\ (S \ T) = \ S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 34` ``` using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 35` ``` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 36` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 37` ```locale prob_space = measure_space + ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 38` ``` assumes measure_space_1: "\ (space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 39` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 40` ```sublocale prob_space < finite_measure ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 41` ```proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 42` ``` from measure_space_1 show "\ (space M) \ \" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 43` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 44` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 45` ```context prob_space ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 46` ```begin ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 47` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 48` ```abbreviation "events \ sets M" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 49` ```abbreviation "prob \ \A. real (\ A)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 50` ```abbreviation "prob_preserving \ measure_preserving" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 51` ```abbreviation "random_variable \ \ s X. X \ measurable M s" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 52` ```abbreviation "expectation \ integral" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 53` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 54` ```definition ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 55` ``` "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 ` 56` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 57` ```definition ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 58` ``` "indep_families F G \ (\ A \ F. \ B \ G. indep A B)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 59` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 60` ```definition ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 61` ``` "distribution X = (\s. \ ((X -` s) \ (space M)))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 62` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 63` ```abbreviation ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 64` ``` "joint_distribution X Y \ distribution (\x. (X x, Y x))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 65` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 66` ```lemma prob_space: "prob (space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 67` ``` unfolding measure_space_1 by simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 68` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 69` ```lemma measure_le_1[simp, intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 70` ``` assumes "A \ events" shows "\ A \ 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 71` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 72` ``` have "\ A \ \ (space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 73` ``` using assms sets_into_space by(auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 74` ``` also note measure_space_1 ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 75` ``` finally show ?thesis . ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 76` ```qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 77` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 78` ```lemma measure_finite[simp, intro]: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 79` ``` assumes "A \ events" shows "\ A \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 80` ``` using measure_le_1[OF assms] by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 81` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 82` ```lemma prob_compl: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 83` ``` assumes "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 84` ``` shows "prob (space M - A) = 1 - prob A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 85` ``` using `A \ events`[THEN sets_into_space] `A \ events` measure_space_1 ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 86` ``` by (subst real_finite_measure_Diff) auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 87` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 88` ```lemma indep_space: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 89` ``` assumes "s \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 90` ``` shows "indep (space M) s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 91` ``` using assms prob_space by (simp add: indep_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 92` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 93` ```lemma prob_space_increasing: "increasing M prob" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 94` ``` by (auto intro!: real_measure_mono simp: increasing_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 95` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 96` ```lemma prob_zero_union: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 97` ``` assumes "s \ events" "t \ events" "prob t = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 98` ``` shows "prob (s \ t) = prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 99` ```using assms ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 100` ```proof - ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 101` ``` have "prob (s \ t) \ prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 102` ``` using real_finite_measure_subadditive[of s t] assms by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 103` ``` moreover have "prob (s \ t) \ prob s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 104` ``` using assms by (blast intro: real_measure_mono) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 105` ``` ultimately show ?thesis by simp ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 106` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 107` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 108` ```lemma prob_eq_compl: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 109` ``` assumes "s \ events" "t \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 110` ``` assumes "prob (space M - s) = prob (space M - t)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 111` ``` shows "prob s = prob t" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 112` ``` using assms prob_compl by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 113` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 114` ```lemma prob_one_inter: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 115` ``` assumes events:"s \ events" "t \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 116` ``` assumes "prob t = 1" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 117` ``` shows "prob (s \ t) = prob s" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 118` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 119` ``` have "prob ((space M - s) \ (space M - t)) = prob (space M - s)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 120` ``` using events assms prob_compl[of "t"] by (auto intro!: prob_zero_union) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 121` ``` also have "(space M - s) \ (space M - t) = space M - (s \ t)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 122` ``` by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 123` ``` finally show "prob (s \ t) = prob s" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 124` ``` using events by (auto intro!: prob_eq_compl[of "s \ t" s]) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 125` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 126` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 127` ```lemma prob_eq_bigunion_image: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 128` ``` assumes "range f \ events" "range g \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 129` ``` assumes "disjoint_family f" "disjoint_family g" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 130` ``` assumes "\ n :: nat. prob (f n) = prob (g n)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 131` ``` shows "(prob (\ i. f i) = prob (\ i. g i))" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 132` ```using assms ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 133` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 134` ``` have a: "(\ i. prob (f i)) sums (prob (\ i. f i))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 135` ``` by (rule real_finite_measure_UNION[OF assms(1,3)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 136` ``` have b: "(\ i. prob (g i)) sums (prob (\ i. g i))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 137` ``` by (rule real_finite_measure_UNION[OF assms(2,4)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 138` ``` 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 ` 139` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 140` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 141` ```lemma prob_countably_zero: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 142` ``` assumes "range c \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 143` ``` assumes "\ i. prob (c i) = 0" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 144` ``` shows "prob (\ i :: nat. c i) = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 145` ```proof (rule antisym) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 146` ``` show "prob (\ i :: nat. c i) \ 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 147` ``` using real_finite_measurable_countably_subadditive[OF assms(1)] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 148` ``` by (simp add: assms(2) suminf_zero summable_zero) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 149` ``` show "0 \ prob (\ i :: nat. c i)" by (rule real_pinfreal_nonneg) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 150` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 151` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 152` ```lemma indep_sym: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 153` ``` "indep a b \ indep b a" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 154` ```unfolding indep_def using Int_commute[of a b] by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 155` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 156` ```lemma indep_refl: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 157` ``` assumes "a \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 158` ``` shows "indep a a = (prob a = 0) \ (prob a = 1)" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 159` ```using assms unfolding indep_def by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 160` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 161` ```lemma prob_equiprobable_finite_unions: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 162` ``` assumes "s \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 163` ``` assumes s_finite: "finite s" "\x. x \ s \ {x} \ events" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 164` ``` assumes "\ x y. \x \ s; y \ s\ \ (prob {x} = prob {y})" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 165` ``` shows "prob s = real (card s) * prob {SOME x. x \ s}" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 166` ```proof (cases "s = {}") ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 167` ``` case False hence "\ x. x \ s" by blast ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 168` ``` from someI_ex[OF this] assms ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 169` ``` 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 ` 170` ``` have "prob s = (\ x \ s. prob {x})" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 171` ``` using real_finite_measure_finite_singelton[OF s_finite] by simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 172` ``` 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 ` 173` ``` also have "\ = real (card s) * prob {(SOME x. x \ s)}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 174` ``` using setsum_constant assms by (simp add: real_eq_of_nat) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 175` ``` finally show ?thesis by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 176` ```qed simp ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 177` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 178` ```lemma prob_real_sum_image_fn: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 179` ``` assumes "e \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 180` ``` assumes "\ x. x \ s \ e \ f x \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 181` ``` assumes "finite s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 182` ``` assumes disjoint: "\ x y. \x \ s ; y \ s ; x \ y\ \ f x \ f y = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 183` ``` assumes upper: "space M \ (\ i \ s. f i)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 184` ``` shows "prob e = (\ x \ s. prob (e \ f x))" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 185` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 186` ``` have e: "e = (\ i \ s. e \ f i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 187` ``` using `e \ events` sets_into_space upper by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 188` ``` hence "prob e = prob (\ i \ s. e \ f i)" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 189` ``` also have "\ = (\ x \ s. prob (e \ f x))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 190` ``` proof (rule real_finite_measure_finite_Union) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 191` ``` show "finite s" by fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 192` ``` show "\i. i \ s \ e \ f i \ events" by fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 193` ``` show "disjoint_family_on (\i. e \ f i) s" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 194` ``` using disjoint by (auto simp: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 195` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 196` ``` finally show ?thesis . ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 197` ```qed ``` 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_prob_space: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 200` ``` fixes S :: "('c, 'd) algebra_scheme" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 201` ``` assumes "sigma_algebra S" "random_variable S X" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 202` ``` shows "prob_space S (distribution X)" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 203` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 204` ``` interpret S: sigma_algebra S by fact ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 205` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 206` ``` proof ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 207` ``` show "distribution X {} = 0" unfolding distribution_def by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 208` ``` have "X -` space S \ space M = space M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 209` ``` using `random_variable S X` by (auto simp: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 210` ``` then show "distribution X (space S) = 1" using measure_space_1 by (simp add: distribution_def) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 211` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 212` ``` show "countably_additive S (distribution X)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 213` ``` proof (unfold countably_additive_def, safe) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 214` ``` fix A :: "nat \ 'c set" assume "range A \ sets S" "disjoint_family A" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 215` ``` hence *: "\i. X -` A i \ space M \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 216` ``` using `random_variable S X` by (auto simp: measurable_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 217` ``` moreover hence "\i. \ (X -` A i \ space M) \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 218` ``` using finite_measure by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 219` ``` moreover have "(\i. X -` A i \ space M) \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 220` ``` using * by blast ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 221` ``` moreover hence "\ (\i. X -` A i \ space M) \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 222` ``` using finite_measure by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 223` ``` moreover have **: "disjoint_family (\i. X -` A i \ space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 224` ``` using `disjoint_family A` by (auto simp: disjoint_family_on_def) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 225` ``` ultimately show "(\\<^isub>\ i. distribution X (A i)) = distribution X (\i. A i)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 226` ``` using measure_countably_additive[OF _ **] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 227` ``` by (auto simp: distribution_def Real_real comp_def vimage_UN) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 228` ``` qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 229` ``` qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 230` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 231` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 232` ```lemma distribution_lebesgue_thm1: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 233` ``` assumes "random_variable s X" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 234` ``` assumes "A \ sets s" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 235` ``` shows "real (distribution X A) = expectation (indicator (X -` A \ space M))" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 236` ```unfolding distribution_def ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 237` ```using assms unfolding measurable_def ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 238` ```using integral_indicator by auto ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 239` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 240` ```lemma distribution_lebesgue_thm2: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 241` ``` assumes "sigma_algebra S" "random_variable S X" and "A \ sets S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 242` ``` shows "distribution X A = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 243` ``` measure_space.positive_integral S (distribution X) (indicator A)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 244` ``` (is "_ = measure_space.positive_integral _ ?D _") ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 245` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 246` ``` 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 ` 247` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 248` ``` show ?thesis ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 249` ``` using S.positive_integral_indicator(1) ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 250` ``` using assms unfolding distribution_def by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 251` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 252` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 253` ```lemma finite_expectation1: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 254` ``` assumes "finite (X`space M)" and rv: "random_variable borel_space X" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 255` ``` shows "expectation X = (\ r \ X ` space M. r * prob (X -` {r} \ space M))" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 256` ```proof (rule integral_on_finite(2)[OF assms(2,1)]) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 257` ``` fix x have "X -` {x} \ space M \ sets M" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 258` ``` using rv unfolding measurable_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 259` ``` thus "\ (X -` {x} \ space M) \ \" using finite_measure by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 260` ```qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 261` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 262` ```lemma finite_expectation: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 263` ``` assumes "finite (space M)" "random_variable borel_space X" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 264` ``` shows "expectation X = (\ r \ X ` (space M). r * real (distribution X {r}))" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 265` ``` using assms unfolding distribution_def using finite_expectation1 by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 266` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 267` ```lemma prob_x_eq_1_imp_prob_y_eq_0: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 268` ``` assumes "{x} \ events" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 269` ``` assumes "prob {x} = 1" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 270` ``` assumes "{y} \ events" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 271` ``` assumes "y \ x" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 272` ``` shows "prob {y} = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 273` ``` using prob_one_inter[of "{y}" "{x}"] assms by auto ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 274` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 275` ```lemma distribution_empty[simp]: "distribution X {} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 276` ``` unfolding distribution_def by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 277` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 278` ```lemma distribution_space[simp]: "distribution X (X ` space M) = 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 279` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 280` ``` have "X -` X ` space M \ space M = space M" by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 281` ``` thus ?thesis unfolding distribution_def by (simp add: measure_space_1) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 282` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 283` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 284` ```lemma distribution_one: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 285` ``` assumes "random_variable M X" and "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 286` ``` shows "distribution X A \ 1" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 287` ```proof - ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 288` ``` have "distribution X A \ \ (space M)" unfolding distribution_def ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 289` ``` using assms[unfolded measurable_def] by (auto intro!: measure_mono) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 290` ``` thus ?thesis by (simp add: measure_space_1) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 291` ```qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 292` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 293` ```lemma distribution_finite: ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 294` ``` assumes "random_variable M X" and "A \ events" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 295` ``` shows "distribution X A \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 296` ``` using distribution_one[OF assms] by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 297` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 298` ```lemma distribution_x_eq_1_imp_distribution_y_eq_0: ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 299` ``` 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 ` 300` ``` (is "random_variable ?S X") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 301` ``` assumes "distribution X {x} = 1" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 302` ``` assumes "y \ x" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 303` ``` shows "distribution X {y} = 0" ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 304` ```proof - ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 305` ``` have "sigma_algebra ?S" by (rule sigma_algebra_Pow) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 306` ``` from distribution_prob_space[OF this X] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 307` ``` interpret S: prob_space ?S "distribution X" by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 308` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 309` ``` have x: "{x} \ sets ?S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 310` ``` proof (rule ccontr) ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 311` ``` assume "{x} \ sets ?S" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 312` ``` hence "X -` {x} \ space M = {}" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 313` ``` thus "False" using assms unfolding distribution_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 314` ``` qed ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 315` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 316` ``` have [simp]: "{y} \ {x} = {}" "{x} - {y} = {x}" using `y \ x` by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 317` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 318` ``` show ?thesis ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 319` ``` proof cases ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 320` ``` assume "{y} \ sets ?S" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 321` ``` with `{x} \ sets ?S` assms show "distribution X {y} = 0" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 322` ``` using S.measure_inter_full_set[of "{y}" "{x}"] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 323` ``` by simp ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 324` ``` next ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 325` ``` assume "{y} \ sets ?S" ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 326` ``` hence "X -` {y} \ space M = {}" by auto ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 327` ``` thus "distribution X {y} = 0" unfolding distribution_def by auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 328` ``` qed ``` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 329` ```qed ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 330` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 331` ```end ``` b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 332` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 333` ```locale finite_prob_space = prob_space + finite_measure_space ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 334` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 335` ```lemma finite_prob_space_eq: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 336` ``` "finite_prob_space M \ \ finite_measure_space M \ \ \ (space M) = 1" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 337` ``` 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 ` 338` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 339` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 340` ```lemma (in prob_space) not_empty: "space M \ {}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 341` ``` using prob_space empty_measure by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 342` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 343` ```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 ` 344` ``` using measure_space_1 sum_over_space by simp ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 345` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 346` ```lemma (in finite_prob_space) positive_distribution: "0 \ distribution X x" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 347` ``` unfolding distribution_def by simp ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 348` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 349` ```lemma (in finite_prob_space) joint_distribution_restriction_fst: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 350` ``` "joint_distribution X Y A \ distribution X (fst ` A)" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 351` ``` unfolding distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 352` ```proof (safe intro!: measure_mono) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 353` ``` fix x assume "x \ space M" and *: "(X x, Y x) \ A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 354` ``` show "x \ X -` fst ` A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 355` ``` by (auto intro!: image_eqI[OF _ *]) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 356` ```qed (simp_all add: sets_eq_Pow) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 357` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 358` ```lemma (in finite_prob_space) joint_distribution_restriction_snd: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 359` ``` "joint_distribution X Y A \ distribution Y (snd ` A)" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 360` ``` unfolding distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 361` ```proof (safe intro!: measure_mono) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 362` ``` fix x assume "x \ space M" and *: "(X x, Y x) \ A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 363` ``` show "x \ Y -` snd ` A" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 364` ``` by (auto intro!: image_eqI[OF _ *]) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 365` ```qed (simp_all add: sets_eq_Pow) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 366` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 367` ```lemma (in finite_prob_space) distribution_order: ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 368` ``` shows "0 \ distribution X x'" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 369` ``` and "(distribution X x' \ 0) \ (0 < distribution X x')" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 370` ``` and "r \ joint_distribution X Y {(x, y)} \ r \ distribution X {x}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 371` ``` and "r \ joint_distribution X Y {(x, y)} \ r \ distribution Y {y}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 372` ``` and "r < joint_distribution X Y {(x, y)} \ r < distribution X {x}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 373` ``` and "r < joint_distribution X Y {(x, y)} \ r < distribution Y {y}" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 374` ``` and "distribution X {x} = 0 \ joint_distribution X Y {(x, y)} = 0" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 375` ``` and "distribution Y {y} = 0 \ joint_distribution X Y {(x, y)} = 0" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 376` ``` using positive_distribution[of X x'] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 377` ``` positive_distribution[of "\x. (X x, Y x)" "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 378` ``` joint_distribution_restriction_fst[of X Y "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 379` ``` joint_distribution_restriction_snd[of X Y "{(x, y)}"] ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 380` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 381` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 382` ```lemma (in finite_prob_space) finite_product_measure_space: ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 383` ``` assumes "finite s1" "finite s2" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 384` ``` shows "finite_measure_space \ space = s1 \ s2, sets = Pow (s1 \ s2)\ (joint_distribution X Y)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 385` ``` (is "finite_measure_space ?M ?D") ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 386` ```proof (rule finite_Pow_additivity_sufficient) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 387` ``` show "positive ?D" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 388` ``` unfolding positive_def using assms sets_eq_Pow ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 389` ``` by (simp add: distribution_def) ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 390` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 391` ``` show "additive ?M ?D" unfolding additive_def ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 392` ``` proof safe ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 393` ``` fix x y ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 394` ``` have A: "((\x. (X x, Y x)) -` x) \ space M \ sets M" using assms sets_eq_Pow by auto ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 395` ``` have B: "((\x. (X x, Y x)) -` y) \ space M \ sets M" using assms sets_eq_Pow by auto ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 396` ``` assume "x \ y = {}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 397` ``` hence "(\x. (X x, Y x)) -` x \ space M \ ((\x. (X x, Y x)) -` y \ space M) = {}" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 398` ``` by auto ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 399` ``` from additive[unfolded additive_def, rule_format, OF A B] this ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 400` ``` finite_measure[OF A] finite_measure[OF B] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 401` ``` show "?D (x \ y) = ?D x + ?D y" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 402` ``` apply (simp add: distribution_def) ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 403` ``` apply (subst Int_Un_distrib2) ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 404` ``` by (auto simp: real_of_pinfreal_add) ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 405` ``` qed ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 406` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 407` ``` show "finite (space ?M)" ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 408` ``` using assms by auto ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 409` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 410` ``` show "sets ?M = Pow (space ?M)" ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 411` ``` by simp ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 412` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 413` ``` { fix x assume "x \ space ?M" thus "?D {x} \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 414` ``` unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) } ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 415` ```qed ``` 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 416` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 417` ```lemma (in finite_prob_space) finite_product_measure_space_of_images: ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 418` ``` shows "finite_measure_space \ space = X ` space M \ Y ` space M, ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 419` ``` sets = Pow (X ` space M \ Y ` space M) \ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 420` ``` (joint_distribution X Y)" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 421` ``` using finite_space by (auto intro!: finite_product_measure_space) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 422` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 423` ```lemma (in finite_prob_space) finite_measure_space: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 424` ``` 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 ` 425` ``` (is "finite_measure_space ?S _") ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 426` ```proof (rule finite_Pow_additivity_sufficient, simp_all) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 427` ``` show "finite (X ` space M)" using finite_space by simp ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 428` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 429` ``` show "positive (distribution X)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 430` ``` unfolding distribution_def positive_def using sets_eq_Pow by auto ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 431` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 432` ``` show "additive ?S (distribution X)" unfolding additive_def distribution_def ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 433` ``` proof (simp, safe) ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 434` ``` fix x y ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 435` ``` have x: "(X -` x) \ space M \ sets M" ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 436` ``` and y: "(X -` y) \ space M \ sets M" using sets_eq_Pow by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 437` ``` assume "x \ y = {}" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 438` ``` hence "X -` x \ space M \ (X -` y \ space M) = {}" by auto ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 439` ``` from additive[unfolded additive_def, rule_format, OF x y] this ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 440` ``` finite_measure[OF x] finite_measure[OF y] ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 441` ``` have "\ (((X -` x) \ (X -` y)) \ space M) = ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 442` ``` \ ((X -` x) \ space M) + \ ((X -` y) \ space M)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 443` ``` by (subst Int_Un_distrib2) auto ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 444` ``` thus "\ ((X -` x \ X -` y) \ space M) = \ (X -` x \ space M) + \ (X -` y \ space M)" ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 445` ``` by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 446` ``` qed ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 447` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 448` ``` { fix x assume "x \ X ` space M" thus "distribution X {x} \ \" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 449` ``` unfolding distribution_def by (auto intro!: finite_measure simp: sets_eq_Pow) } ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 450` ```qed ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 451` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 452` ```lemma (in finite_prob_space) finite_prob_space_of_images: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 453` ``` "finite_prob_space \ space = X ` space M, sets = Pow (X ` space M)\ (distribution X)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 454` ``` by (simp add: finite_prob_space_eq finite_measure_space) ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 455` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 456` ```lemma (in finite_prob_space) finite_product_prob_space_of_images: ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 457` ``` "finite_prob_space \ space = X ` space M \ Y ` space M, sets = Pow (X ` space M \ Y ` space M)\ ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 458` ``` (joint_distribution X Y)" ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 459` ``` (is "finite_prob_space ?S _") ``` d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 460` ```proof (simp add: finite_prob_space_eq finite_product_measure_space_of_images) ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 461` ``` have "X -` X ` space M \ Y -` Y ` space M \ space M = space M" by auto ``` 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 462` ``` thus "joint_distribution X Y (X ` space M \ Y ` space M) = 1" ``` 38656 d5d342611edb Rewrite the Probability theory. hoelzl parents: 36624 diff changeset ` 463` ``` by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) ``` 36624 25153c08655e Cleanup information theory hoelzl parents: 35977 diff changeset ` 464` ```qed ``` 35977 30d42bfd0174 Added finite measure space. hoelzl parents: 35929 diff changeset ` 465` 35582 b16d99a72dc9 Add Lebesgue integral and probability space. hoelzl parents: diff changeset ` 466` ```end ```