# HG changeset patch
# User hoelzl
# Date 1282901617 -7200
# Node ID 7a6ecce976611bde0701348329a23b388e315b72
# Parent  e46acc0ea1fe92fa677480b63bdce40cb1cf9eb9
proved existence of conditional expectation

diff -r e46acc0ea1fe -r 7a6ecce97661 src/HOL/Probability/Probability_Space.thy
--- a/src/HOL/Probability/Probability_Space.thy	Thu Aug 26 18:41:54 2010 +0200
+++ b/src/HOL/Probability/Probability_Space.thy	Fri Aug 27 11:33:37 2010 +0200
@@ -511,7 +511,7 @@
   from positive_integral_isoton_simple[OF `fs \<up> f` sf] N.positive_integral_isoton_simple[OF `fs \<up> f` Nsf]
   show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp
 qed
-(*
+
 lemma (in prob_space)
   fixes X :: "'a \<Rightarrow> pinfreal"
   assumes borel: "X \<in> borel_measurable M"
@@ -548,16 +548,8 @@
   obtain Y where Y: "Y \<in> borel_measurable (M\<lparr>sets := N\<rparr>)"
     "\<And>A. A \<in> sets (M\<lparr>sets:=N\<rparr>) \<Longrightarrow> ?Q A = P.positive_integral (\<lambda>x. Y x * indicator A x)"
     by blast
-  show ?thesis
-  proof (intro bexI[OF _ Y(1)] ballI)
-    fix A assume "A \<in> N"
-    have "positive_integral (\<lambda>x. Y x * indicator A x) = P.positive_integral (\<lambda>x. Y x * indicator A x)"
-      unfolding P.positive_integral_def positive_integral_def
-      unfolding P.simple_integral_def_raw simple_integral_def_raw
-      apply simp
-    show "positive_integral (\<lambda>x. Y x * indicator A x) = ?Q A"
-  qed
+  with N_subalgebra show ?thesis
+    by (auto intro!: bexI[OF _ Y(1)])
 qed
-*)
 
 end