# HG changeset patch # User hoelzl # Date 1309160566 -7200 # Node ID 0d78c8d31d0d4c6269b79f45747c783228962560 # Parent 93c1fc6ac52791bdb5402b216d2dd2282055e710 move conditional expectation to its own theory file diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/IsaMakefile Mon Jun 27 09:42:46 2011 +0200 @@ -1203,6 +1203,7 @@ $(OUT)/HOL-Probability: $(OUT)/HOL-Multivariate_Analysis \ Probability/Binary_Product_Measure.thy Probability/Borel_Space.thy \ Probability/Caratheodory.thy Probability/Complete_Measure.thy \ + Probability/Conditional_Probability.thy \ Probability/ex/Dining_Cryptographers.thy \ Probability/ex/Koepf_Duermuth_Countermeasure.thy \ Probability/Finite_Product_Measure.thy \ diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Conditional_Probability.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Conditional_Probability.thy Mon Jun 27 09:42:46 2011 +0200 @@ -0,0 +1,161 @@ +(* Title: HOL/Probability/Conditional_Probability.thy + Author: Johannes Hölzl, TU München +*) + +header {*Conditional probability*} + +theory Conditional_Probability +imports Probability_Measure Radon_Nikodym +begin + +section "Conditional Expectation and Probability" + +definition (in prob_space) + "conditional_expectation N X = (SOME Y. Y\borel_measurable N \ (\x. 0 \ Y x) + \ (\C\sets N. (\\<^isup>+x. Y x * indicator C x\M) = (\\<^isup>+x. X x * indicator C x\M)))" + +lemma (in prob_space) conditional_expectation_exists: + fixes X :: "'a \ extreal" and N :: "('a, 'b) measure_space_scheme" + assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" + and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" + shows "\Y\borel_measurable N. (\x. 0 \ Y x) \ (\C\sets N. + (\\<^isup>+x. Y x * indicator C x \M) = (\\<^isup>+x. X x * indicator C x \M))" +proof - + note N(4)[simp] + interpret P: prob_space N + using prob_space_subalgebra[OF N] . + + let "?f A" = "\x. X x * indicator A x" + let "?Q A" = "integral\<^isup>P M (?f A)" + + from measure_space_density[OF borel] + have Q: "measure_space (N\ measure := ?Q \)" + apply (rule measure_space.measure_space_subalgebra[of "M\ measure := ?Q \"]) + using N by (auto intro!: P.sigma_algebra_cong) + then interpret Q: measure_space "N\ measure := ?Q \" . + + have "P.absolutely_continuous ?Q" + unfolding P.absolutely_continuous_def + proof safe + fix A assume "A \ sets N" "P.\ A = 0" + then have f_borel: "?f A \ borel_measurable M" "AE x. x \ A" + using borel N by (auto intro!: borel_measurable_indicator AE_not_in) + then show "?Q A = 0" + by (auto simp add: positive_integral_0_iff_AE) + qed + from P.Radon_Nikodym[OF Q this] + obtain Y where Y: "Y \ borel_measurable N" "\x. 0 \ Y x" + "\A. A \ sets N \ ?Q A =(\\<^isup>+x. Y x * indicator A x \N)" + by blast + with N(2) show ?thesis + by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ _ N(2,3,4,1)]) +qed + +lemma (in prob_space) + fixes X :: "'a \ extreal" and N :: "('a, 'b) measure_space_scheme" + assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" + and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" + shows borel_measurable_conditional_expectation: + "conditional_expectation N X \ borel_measurable N" + and conditional_expectation: "\C. C \ sets N \ + (\\<^isup>+x. conditional_expectation N X x * indicator C x \M) = + (\\<^isup>+x. X x * indicator C x \M)" + (is "\C. C \ sets N \ ?eq C") +proof - + note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] + then show "conditional_expectation N X \ borel_measurable N" + unfolding conditional_expectation_def by (rule someI2_ex) blast + + from CE show "\C. C \ sets N \ ?eq C" + unfolding conditional_expectation_def by (rule someI2_ex) blast +qed + +lemma (in sigma_algebra) factorize_measurable_function_pos: + fixes Z :: "'a \ extreal" and Y :: "'a \ 'c" + assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" + assumes Z: "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)" + shows "\g\borel_measurable M'. \x\space M. max 0 (Z x) = g (Y x)" +proof - + interpret M': sigma_algebra M' by fact + have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto + from M'.sigma_algebra_vimage[OF this] + interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . + + from va.borel_measurable_implies_simple_function_sequence'[OF Z] guess f . note f = this + + have "\i. \g. simple_function M' g \ (\x\space M. f i x = g (Y x))" + proof + fix i + from f(1)[of i] have "finite (f i`space M)" and B_ex: + "\z\(f i)`space M. \B. B \ sets M' \ (f i) -` {z} \ space M = Y -` B \ space M" + unfolding simple_function_def by auto + from B_ex[THEN bchoice] guess B .. note B = this + + let ?g = "\x. \z\f i`space M. z * indicator (B z) x" + + show "\g. simple_function M' g \ (\x\space M. f i x = g (Y x))" + proof (intro exI[of _ ?g] conjI ballI) + show "simple_function M' ?g" using B by auto + + fix x assume "x \ space M" + then have "\z. z \ f i`space M \ indicator (B z) (Y x) = (indicator (f i -` {z} \ space M) x::extreal)" + unfolding indicator_def using B by auto + then show "f i x = ?g (Y x)" using `x \ space M` f(1)[of i] + by (subst va.simple_function_indicator_representation) auto + qed + qed + from choice[OF this] guess g .. note g = this + + show ?thesis + proof (intro ballI bexI) + show "(\x. SUP i. g i x) \ borel_measurable M'" + using g by (auto intro: M'.borel_measurable_simple_function) + fix x assume "x \ space M" + have "max 0 (Z x) = (SUP i. f i x)" using f by simp + also have "\ = (SUP i. g i (Y x))" + using g `x \ space M` by simp + finally show "max 0 (Z x) = (SUP i. g i (Y x))" . + qed +qed + +lemma (in sigma_algebra) factorize_measurable_function: + fixes Z :: "'a \ extreal" and Y :: "'a \ 'c" + assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" + shows "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) + \ (\g\borel_measurable M'. \x\space M. Z x = g (Y x))" +proof safe + interpret M': sigma_algebra M' by fact + have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto + from M'.sigma_algebra_vimage[OF this] + interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . + + { fix g :: "'c \ extreal" assume "g \ borel_measurable M'" + with M'.measurable_vimage_algebra[OF Y] + have "g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" + by (rule measurable_comp) + moreover assume "\x\space M. Z x = g (Y x)" + then have "Z \ borel_measurable (M'.vimage_algebra (space M) Y) \ + g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" + by (auto intro!: measurable_cong) + ultimately show "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" + by simp } + + assume Z: "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" + with assms have "(\x. - Z x) \ borel_measurable M" + "(\x. - Z x) \ borel_measurable (M'.vimage_algebra (space M) Y)" + by auto + from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this + from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this + let "?g x" = "p x - n x" + show "\g\borel_measurable M'. \x\space M. Z x = g (Y x)" + proof (intro bexI ballI) + show "?g \ borel_measurable M'" using p n by auto + fix x assume "x \ space M" + then have "p (Y x) = max 0 (Z x)" "n (Y x) = max 0 (- Z x)" + using p n by auto + then show "Z x = ?g (Y x)" + by (auto split: split_max) + qed +qed + +end \ No newline at end of file diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/Probability/Information.thy Mon Jun 27 09:42:46 2011 +0200 @@ -8,6 +8,7 @@ theory Information imports Independent_Family + Radon_Nikodym "~~/src/HOL/Library/Convex" begin diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Measure.thy --- a/src/HOL/Probability/Measure.thy Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/Probability/Measure.thy Mon Jun 27 09:42:46 2011 +0200 @@ -1205,6 +1205,10 @@ lemma (in finite_measure) positive_measure'[simp, intro]: "0 \ \' A" unfolding \'_def by (auto simp: real_of_extreal_pos) +lemma (in finite_measure) real_measure: + assumes A: "A \ sets M" shows "\r. 0 \ r \ \ A = extreal r" + using finite_measure[OF A] positive_measure[OF A] by (cases "\ A") auto + lemma (in finite_measure) bounded_measure: "\' A \ \' (space M)" proof cases assume "A \ sets M" diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/Probability/Probability.thy Mon Jun 27 09:42:46 2011 +0200 @@ -4,6 +4,7 @@ Probability_Measure Infinite_Product_Measure Independent_Family + Conditional_Probability Information "ex/Dining_Cryptographers" "ex/Koepf_Duermuth_Countermeasure" diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/Probability/Probability_Measure.thy Mon Jun 27 09:42:46 2011 +0200 @@ -6,7 +6,7 @@ header {*Probability measure*} theory Probability_Measure -imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure Lebesgue_Measure +imports Lebesgue_Measure begin locale prob_space = measure_space + @@ -1107,159 +1107,6 @@ by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1) qed -section "Conditional Expectation and Probability" - -lemma (in prob_space) conditional_expectation_exists: - fixes X :: "'a \ extreal" and N :: "('a, 'b) measure_space_scheme" - assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" - and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" - shows "\Y\borel_measurable N. (\x. 0 \ Y x) \ (\C\sets N. - (\\<^isup>+x. Y x * indicator C x \M) = (\\<^isup>+x. X x * indicator C x \M))" -proof - - note N(4)[simp] - interpret P: prob_space N - using prob_space_subalgebra[OF N] . - - let "?f A" = "\x. X x * indicator A x" - let "?Q A" = "integral\<^isup>P M (?f A)" - - from measure_space_density[OF borel] - have Q: "measure_space (N\ measure := ?Q \)" - apply (rule measure_space.measure_space_subalgebra[of "M\ measure := ?Q \"]) - using N by (auto intro!: P.sigma_algebra_cong) - then interpret Q: measure_space "N\ measure := ?Q \" . - - have "P.absolutely_continuous ?Q" - unfolding P.absolutely_continuous_def - proof safe - fix A assume "A \ sets N" "P.\ A = 0" - then have f_borel: "?f A \ borel_measurable M" "AE x. x \ A" - using borel N by (auto intro!: borel_measurable_indicator AE_not_in) - then show "?Q A = 0" - by (auto simp add: positive_integral_0_iff_AE) - qed - from P.Radon_Nikodym[OF Q this] - obtain Y where Y: "Y \ borel_measurable N" "\x. 0 \ Y x" - "\A. A \ sets N \ ?Q A =(\\<^isup>+x. Y x * indicator A x \N)" - by blast - with N(2) show ?thesis - by (auto intro!: bexI[OF _ Y(1)] simp: positive_integral_subalgebra[OF _ _ N(2,3,4,1)]) -qed - -definition (in prob_space) - "conditional_expectation N X = (SOME Y. Y\borel_measurable N \ (\x. 0 \ Y x) - \ (\C\sets N. (\\<^isup>+x. Y x * indicator C x\M) = (\\<^isup>+x. X x * indicator C x\M)))" - -abbreviation (in prob_space) - "conditional_prob N A \ conditional_expectation N (indicator A)" - -lemma (in prob_space) - fixes X :: "'a \ extreal" and N :: "('a, 'b) measure_space_scheme" - assumes borel: "X \ borel_measurable M" "AE x. 0 \ X x" - and N: "sigma_algebra N" "sets N \ sets M" "space N = space M" "\A. measure N A = \ A" - shows borel_measurable_conditional_expectation: - "conditional_expectation N X \ borel_measurable N" - and conditional_expectation: "\C. C \ sets N \ - (\\<^isup>+x. conditional_expectation N X x * indicator C x \M) = - (\\<^isup>+x. X x * indicator C x \M)" - (is "\C. C \ sets N \ ?eq C") -proof - - note CE = conditional_expectation_exists[OF assms, unfolded Bex_def] - then show "conditional_expectation N X \ borel_measurable N" - unfolding conditional_expectation_def by (rule someI2_ex) blast - - from CE show "\C. C \ sets N \ ?eq C" - unfolding conditional_expectation_def by (rule someI2_ex) blast -qed - -lemma (in sigma_algebra) factorize_measurable_function_pos: - fixes Z :: "'a \ extreal" and Y :: "'a \ 'c" - assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" - assumes Z: "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)" - shows "\g\borel_measurable M'. \x\space M. max 0 (Z x) = g (Y x)" -proof - - interpret M': sigma_algebra M' by fact - have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto - from M'.sigma_algebra_vimage[OF this] - interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . - - from va.borel_measurable_implies_simple_function_sequence'[OF Z] guess f . note f = this - - have "\i. \g. simple_function M' g \ (\x\space M. f i x = g (Y x))" - proof - fix i - from f(1)[of i] have "finite (f i`space M)" and B_ex: - "\z\(f i)`space M. \B. B \ sets M' \ (f i) -` {z} \ space M = Y -` B \ space M" - unfolding simple_function_def by auto - from B_ex[THEN bchoice] guess B .. note B = this - - let ?g = "\x. \z\f i`space M. z * indicator (B z) x" - - show "\g. simple_function M' g \ (\x\space M. f i x = g (Y x))" - proof (intro exI[of _ ?g] conjI ballI) - show "simple_function M' ?g" using B by auto - - fix x assume "x \ space M" - then have "\z. z \ f i`space M \ indicator (B z) (Y x) = (indicator (f i -` {z} \ space M) x::extreal)" - unfolding indicator_def using B by auto - then show "f i x = ?g (Y x)" using `x \ space M` f(1)[of i] - by (subst va.simple_function_indicator_representation) auto - qed - qed - from choice[OF this] guess g .. note g = this - - show ?thesis - proof (intro ballI bexI) - show "(\x. SUP i. g i x) \ borel_measurable M'" - using g by (auto intro: M'.borel_measurable_simple_function) - fix x assume "x \ space M" - have "max 0 (Z x) = (SUP i. f i x)" using f by simp - also have "\ = (SUP i. g i (Y x))" - using g `x \ space M` by simp - finally show "max 0 (Z x) = (SUP i. g i (Y x))" . - qed -qed - -lemma (in sigma_algebra) factorize_measurable_function: - fixes Z :: "'a \ extreal" and Y :: "'a \ 'c" - assumes "sigma_algebra M'" and "Y \ measurable M M'" "Z \ borel_measurable M" - shows "Z \ borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y) - \ (\g\borel_measurable M'. \x\space M. Z x = g (Y x))" -proof safe - interpret M': sigma_algebra M' by fact - have Y: "Y \ space M \ space M'" using assms unfolding measurable_def by auto - from M'.sigma_algebra_vimage[OF this] - interpret va: sigma_algebra "M'.vimage_algebra (space M) Y" . - - { fix g :: "'c \ extreal" assume "g \ borel_measurable M'" - with M'.measurable_vimage_algebra[OF Y] - have "g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" - by (rule measurable_comp) - moreover assume "\x\space M. Z x = g (Y x)" - then have "Z \ borel_measurable (M'.vimage_algebra (space M) Y) \ - g \ Y \ borel_measurable (M'.vimage_algebra (space M) Y)" - by (auto intro!: measurable_cong) - ultimately show "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" - by simp } - - assume Z: "Z \ borel_measurable (M'.vimage_algebra (space M) Y)" - with assms have "(\x. - Z x) \ borel_measurable M" - "(\x. - Z x) \ borel_measurable (M'.vimage_algebra (space M) Y)" - by auto - from factorize_measurable_function_pos[OF assms(1,2) this] guess n .. note n = this - from factorize_measurable_function_pos[OF assms Z] guess p .. note p = this - let "?g x" = "p x - n x" - show "\g\borel_measurable M'. \x\space M. Z x = g (Y x)" - proof (intro bexI ballI) - show "?g \ borel_measurable M'" using p n by auto - fix x assume "x \ space M" - then have "p (Y x) = max 0 (Z x)" "n (Y x) = max 0 (- Z x)" - using p n by auto - then show "Z x = ?g (Y x)" - by (auto split: split_max) - qed -qed - subsection "Borel Measure on {0 .. 1}" definition pborel :: "real measure_space" where diff -r 93c1fc6ac527 -r 0d78c8d31d0d src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Sun Jun 26 19:10:03 2011 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Jun 27 09:42:46 2011 +0200 @@ -314,10 +314,6 @@ qed qed -lemma (in finite_measure) real_measure: - assumes A: "A \ sets M" shows "\r. 0 \ r \ \ A = extreal r" - using finite_measure[OF A] positive_measure[OF A] by (cases "\ A") auto - lemma (in finite_measure) Radon_Nikodym_finite_measure: assumes "finite_measure (M\ measure := \\)" (is "finite_measure ?M'") assumes "absolutely_continuous \"