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