# HG changeset patch
# User hoelzl
# Date 1282902546 -7200
# Node ID 8b7c009da23ce490b78c97dfcb9c398935f1d986
# Parent  7a6ecce976611bde0701348329a23b388e315b72
added definition of conditional expectation

diff -r 7a6ecce97661 -r 8b7c009da23c src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 11:33:37 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 11:49:06 2010 +0200
@@ -512,7 +512,9 @@
   show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
 qed
 
-lemma (in prob_space)
+section "Conditional Expectation and Probability"
+
+lemma (in prob_space) conditional_expectation_exists:
   fixes X :: "'a \<Rightarrow> pinfreal"
   assumes borel: "X \<in> borel_measurable M"
   and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
@@ -552,4 +554,30 @@
     by (auto intro!: bexI[OF _ Y(1)])
 qed
 
+definition (in prob_space)
+  "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable (M\<lparr>sets:=N\<rparr>)
+    \<and> (\<forall>C\<in>N. positive_integral (\<lambda>x. Y x * indicator C x) = positive_integral (\<lambda>x. X x * indicator C x)))"
+
+abbreviation (in prob_space)
+  "conditional_probabiltiy N A \<equiv> conditional_expectation N (indicator A)"
+
+lemma (in prob_space)
+  fixes X :: "'a \<Rightarrow> pinfreal"
+  assumes borel: "X \<in> borel_measurable M"
+  and N_subalgebra: "N \<subseteq> sets M" "sigma_algebra (M\<lparr> sets := N \<rparr>)"
+  shows borel_measurable_conditional_expectation:
+    "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+  and conditional_expectation: "\<And>C. C \<in> N \<Longrightarrow>
+      positive_integral (\<lambda>x. conditional_expectation N X x * indicator C x) =
+      positive_integral (\<lambda>x. X x * indicator C x)"
+   (is "\<And>C. C \<in> N \<Longrightarrow> ?eq C")
+proof -
+  note CE = conditional_expectation_exists[OF assms, unfolded Bex_def]
+  then show "conditional_expectation N X \<in> borel_measurable (M\<lparr> sets := N \<rparr>)"
+    unfolding conditional_expectation_def by (rule someI2_ex) blast
+
+  from CE show "\<And>C. C\<in>N \<Longrightarrow> ?eq C"
+    unfolding conditional_expectation_def by (rule someI2_ex) blast
+qed
+
 end