author hoelzl Fri, 27 Aug 2010 11:49:06 +0200 changeset 39085 8b7c009da23c parent 39084 7a6ecce97661 child 39086 c4b809e57fe0
```--- 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```