src/HOL/Probability/Conditional_Probability.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46731 5302e932d1e5 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 hoelzl@43556 ` 1` ```(* Title: HOL/Probability/Conditional_Probability.thy ``` hoelzl@43556 ` 2` ``` Author: Johannes Hölzl, TU München ``` hoelzl@43556 ` 3` ```*) ``` hoelzl@43556 ` 4` hoelzl@43556 ` 5` ```header {*Conditional probability*} ``` hoelzl@43556 ` 6` hoelzl@43556 ` 7` ```theory Conditional_Probability ``` hoelzl@43556 ` 8` ```imports Probability_Measure Radon_Nikodym ``` hoelzl@43556 ` 9` ```begin ``` hoelzl@43556 ` 10` hoelzl@43556 ` 11` ```section "Conditional Expectation and Probability" ``` hoelzl@43556 ` 12` hoelzl@43556 ` 13` ```definition (in prob_space) ``` hoelzl@43556 ` 14` ``` "conditional_expectation N X = (SOME Y. Y\borel_measurable N \ (\x. 0 \ Y x) ``` hoelzl@43556 ` 15` ``` \ (\C\sets N. (\\<^isup>+x. Y x * indicator C x\M) = (\\<^isup>+x. X x * indicator C x\M)))" ``` hoelzl@43556 ` 16` hoelzl@43556 ` 17` ```lemma (in prob_space) conditional_expectation_exists: ``` hoelzl@43920 ` 18` ``` fixes X :: "'a \ ereal" and N :: "('a, 'b) measure_space_scheme" ``` hoelzl@43556 ` 19` ``` assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" ``` hoelzl@43556 ` 20` ``` and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" ``` hoelzl@43556 ` 21` ``` shows "\Y\borel_measurable N. (\x. 0 \ Y x) \ (\C\sets N. ``` hoelzl@43556 ` 22` ``` (\\<^isup>+x. Y x * indicator C x \M) = (\\<^isup>+x. X x * indicator C x \M))" ``` hoelzl@43556 ` 23` ```proof - ``` hoelzl@43556 ` 24` ``` note N(4)[simp] ``` hoelzl@43556 ` 25` ``` interpret P: prob_space N ``` hoelzl@43556 ` 26` ``` using prob_space_subalgebra[OF N] . ``` hoelzl@43556 ` 27` wenzelm@46731 ` 28` ``` let ?f = "\A x. X x * indicator A x" ``` wenzelm@46731 ` 29` ``` let ?Q = "\A. integral\<^isup>P M (?f A)" ``` hoelzl@43556 ` 30` hoelzl@43556 ` 31` ``` from measure_space_density[OF borel] ``` hoelzl@43556 ` 32` ``` have Q: "measure_space (N\ measure := ?Q \)" ``` hoelzl@43556 ` 33` ``` apply (rule measure_space.measure_space_subalgebra[of "M\ measure := ?Q \"]) ``` hoelzl@43556 ` 34` ``` using N by (auto intro!: P.sigma_algebra_cong) ``` hoelzl@43556 ` 35` ``` then interpret Q: measure_space "N\ measure := ?Q \" . ``` hoelzl@43556 ` 36` hoelzl@43556 ` 37` ``` have "P.absolutely_continuous ?Q" ``` hoelzl@43556 ` 38` ``` unfolding P.absolutely_continuous_def ``` hoelzl@43556 ` 39` ``` proof safe ``` hoelzl@43556 ` 40` ``` fix A assume "A \ sets N" "P.\ A = 0" ``` hoelzl@43556 ` 41` ``` then have f_borel: "?f A \ borel_measurable M" "AE x. x \ A" ``` hoelzl@43556 ` 42` ``` using borel N by (auto intro!: borel_measurable_indicator AE_not_in) ``` hoelzl@43556 ` 43` ``` then show "?Q A = 0" ``` hoelzl@43556 ` 44` ``` by (auto simp add: positive_integral_0_iff_AE) ``` hoelzl@43556 ` 45` ``` qed ``` hoelzl@43556 ` 46` ``` from P.Radon_Nikodym[OF Q this] ``` hoelzl@43556 ` 47` ``` obtain Y where Y: "Y \ borel_measurable N" "\x. 0 \ Y x" ``` hoelzl@43556 ` 48` ``` "\A. A \ sets N \ ?Q A =(\\<^isup>+x. Y x * indicator A x \N)" ``` hoelzl@43556 ` 49` ``` by blast ``` hoelzl@43556 ` 50` ``` with N(2) show ?thesis ``` hoelzl@43556 ` 51` ``` by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ _ N(2,3,4,1)]) ``` hoelzl@43556 ` 52` ```qed ``` hoelzl@43556 ` 53` hoelzl@43556 ` 54` ```lemma (in prob_space) ``` hoelzl@43920 ` 55` ``` fixes X :: "'a \ ereal" and N :: "('a, 'b) measure_space_scheme" ``` hoelzl@43556 ` 56` ``` assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" ``` hoelzl@43556 ` 57` ``` and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" ``` hoelzl@43556 ` 58` ``` shows borel_measurable_conditional_expectation: ``` hoelzl@43556 ` 59` ``` "conditional_expectation N X \ borel_measurable N" ``` hoelzl@43556 ` 60` ``` and conditional_expectation: "\C. C \ sets N \ ``` hoelzl@43556 ` 61` ``` (\\<^isup>+x. conditional_expectation N X x * indicator C x \M) = ``` hoelzl@43556 ` 62` ``` (\\<^isup>+x. X x * indicator C x \M)" ``` hoelzl@43556 ` 63` ``` (is "\C. C \ sets N \ ?eq C") ``` hoelzl@43556 ` 64` ```proof - ``` hoelzl@43556 ` 65` ``` note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] ``` hoelzl@43556 ` 66` ``` then show "conditional_expectation N X \ borel_measurable N" ``` hoelzl@43556 ` 67` ``` unfolding conditional_expectation_def by (rule someI2_ex) blast ``` hoelzl@43556 ` 68` hoelzl@43556 ` 69` ``` from CE show "\C. C \ sets N \ ?eq C" ``` hoelzl@43556 ` 70` ``` unfolding conditional_expectation_def by (rule someI2_ex) blast ``` hoelzl@43556 ` 71` ```qed ``` hoelzl@43556 ` 72` hoelzl@43556 ` 73` ```lemma (in sigma_algebra) factorize_measurable_function_pos: ``` hoelzl@43920 ` 74` ``` fixes Z :: "'a \ ereal" and Y :: "'a \ 'c" ``` hoelzl@43556 ` 75` ``` assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" ``` hoelzl@43556 ` 76` ``` assumes Z: "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)" ``` hoelzl@43556 ` 77` ``` shows "\g\borel_measurable M'. \x\space M. max 0 (Z x) = g (Y x)" ``` hoelzl@43556 ` 78` ```proof - ``` hoelzl@43556 ` 79` ``` interpret M': sigma_algebra M' by fact ``` hoelzl@43556 ` 80` ``` have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto ``` hoelzl@43556 ` 81` ``` from M'.sigma_algebra_vimage[OF this] ``` hoelzl@43556 ` 82` ``` interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . ``` hoelzl@43556 ` 83` hoelzl@43556 ` 84` ``` from va.borel_measurable_implies_simple_function_sequence'[OF Z] guess f . note f = this ``` hoelzl@43556 ` 85` hoelzl@43556 ` 86` ``` have "\i. \g. simple_function M' g \ (\x\space M. f i x = g (Y x))" ``` hoelzl@43556 ` 87` ``` proof ``` hoelzl@43556 ` 88` ``` fix i ``` hoelzl@43556 ` 89` ``` from f(1)[of i] have "finite (f i`space M)" and B_ex: ``` hoelzl@43556 ` 90` ``` "\z\(f i)`space M. \B. B \ sets M' \ (f i) -` {z} \ space M = Y -` B \ space M" ``` hoelzl@43556 ` 91` ``` unfolding simple_function_def by auto ``` hoelzl@43556 ` 92` ``` from B_ex[THEN bchoice] guess B .. note B = this ``` hoelzl@43556 ` 93` hoelzl@43556 ` 94` ``` let ?g = "\x. \z\f i`space M. z * indicator (B z) x" ``` hoelzl@43556 ` 95` hoelzl@43556 ` 96` ``` show "\g. simple_function M' g \ (\x\space M. f i x = g (Y x))" ``` hoelzl@43556 ` 97` ``` proof (intro exI[of _ ?g] conjI ballI) ``` hoelzl@43556 ` 98` ``` show "simple_function M' ?g" using B by auto ``` hoelzl@43556 ` 99` hoelzl@43556 ` 100` ``` fix x assume "x \ space M" ``` hoelzl@43920 ` 101` ``` then have "\z. z \ f i`space M \ indicator (B z) (Y x) = (indicator (f i -` {z} \ space M) x::ereal)" ``` hoelzl@43556 ` 102` ``` unfolding indicator_def using B by auto ``` hoelzl@43556 ` 103` ``` then show "f i x = ?g (Y x)" using `x \ space M` f(1)[of i] ``` hoelzl@43556 ` 104` ``` by (subst va.simple_function_indicator_representation) auto ``` hoelzl@43556 ` 105` ``` qed ``` hoelzl@43556 ` 106` ``` qed ``` hoelzl@43556 ` 107` ``` from choice[OF this] guess g .. note g = this ``` hoelzl@43556 ` 108` hoelzl@43556 ` 109` ``` show ?thesis ``` hoelzl@43556 ` 110` ``` proof (intro ballI bexI) ``` hoelzl@43556 ` 111` ``` show "(\x. SUP i. g i x) \ borel_measurable M'" ``` hoelzl@43556 ` 112` ``` using g by (auto intro: M'.borel_measurable_simple_function) ``` hoelzl@43556 ` 113` ``` fix x assume "x \ space M" ``` hoelzl@43556 ` 114` ``` have "max 0 (Z x) = (SUP i. f i x)" using f by simp ``` hoelzl@43556 ` 115` ``` also have "\ = (SUP i. g i (Y x))" ``` hoelzl@43556 ` 116` ``` using g `x \ space M` by simp ``` hoelzl@43556 ` 117` ``` finally show "max 0 (Z x) = (SUP i. g i (Y x))" . ``` hoelzl@43556 ` 118` ``` qed ``` hoelzl@43556 ` 119` ```qed ``` hoelzl@43556 ` 120` hoelzl@43556 ` 121` ```lemma (in sigma_algebra) factorize_measurable_function: ``` hoelzl@43920 ` 122` ``` fixes Z :: "'a \ ereal" and Y :: "'a \ 'c" ``` hoelzl@43556 ` 123` ``` assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" ``` hoelzl@43556 ` 124` ``` shows "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) ``` hoelzl@43556 ` 125` ``` \ (\g\borel_measurable M'. \x\space M. Z x = g (Y x))" ``` hoelzl@43556 ` 126` ```proof safe ``` hoelzl@43556 ` 127` ``` interpret M': sigma_algebra M' by fact ``` hoelzl@43556 ` 128` ``` have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto ``` hoelzl@43556 ` 129` ``` from M'.sigma_algebra_vimage[OF this] ``` hoelzl@43556 ` 130` ``` interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . ``` hoelzl@43556 ` 131` hoelzl@43920 ` 132` ``` { fix g :: "'c \ ereal" assume "g \ borel_measurable M'" ``` hoelzl@43556 ` 133` ``` with M'.measurable_vimage_algebra[OF Y] ``` hoelzl@43556 ` 134` ``` have "g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` hoelzl@43556 ` 135` ``` by (rule measurable_comp) ``` hoelzl@43556 ` 136` ``` moreover assume "\x\space M. Z x = g (Y x)" ``` hoelzl@43556 ` 137` ``` then have "Z \ borel_measurable (M'.vimage_algebra (space M) Y) \ ``` hoelzl@43556 ` 138` ``` g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` hoelzl@43556 ` 139` ``` by (auto intro!: measurable_cong) ``` hoelzl@43556 ` 140` ``` ultimately show "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` hoelzl@43556 ` 141` ``` by simp } ``` hoelzl@43556 ` 142` hoelzl@43556 ` 143` ``` assume Z: "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` hoelzl@43556 ` 144` ``` with assms have "(\x. - Z x) \ borel_measurable M" ``` hoelzl@43556 ` 145` ``` "(\x. - Z x) \ borel_measurable (M'.vimage_algebra (space M) Y)" ``` hoelzl@43556 ` 146` ``` by auto ``` hoelzl@43556 ` 147` ``` from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this ``` hoelzl@43556 ` 148` ``` from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this ``` wenzelm@46731 ` 149` ``` let ?g = "\x. p x - n x" ``` hoelzl@43556 ` 150` ``` show "\g\borel_measurable M'. \x\space M. Z x = g (Y x)" ``` hoelzl@43556 ` 151` ``` proof (intro bexI ballI) ``` hoelzl@43556 ` 152` ``` show "?g \ borel_measurable M'" using p n by auto ``` hoelzl@43556 ` 153` ``` fix x assume "x \ space M" ``` hoelzl@43556 ` 154` ``` then have "p (Y x) = max 0 (Z x)" "n (Y x) = max 0 (- Z x)" ``` hoelzl@43556 ` 155` ``` using p n by auto ``` hoelzl@43556 ` 156` ``` then show "Z x = ?g (Y x)" ``` hoelzl@43556 ` 157` ``` by (auto split: split_max) ``` hoelzl@43556 ` 158` ``` qed ``` hoelzl@43556 ` 159` ```qed ``` hoelzl@43556 ` 160` hoelzl@43556 ` 161` `end`