# 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 \ f` sf] N.positive_integral_isoton_simple[OF `fs \ f` Nsf] show ?thesis unfolding simple_integral_subalgebra[OF msN] isoton_def by simp qed -(* + lemma (in prob_space) fixes X :: "'a \ pinfreal" assumes borel: "X \ borel_measurable M" @@ -548,16 +548,8 @@ obtain Y where Y: "Y \ borel_measurable (M\sets := N\)" "\A. A \ sets (M\sets:=N\) \ ?Q A = P.positive_integral (\x. Y x * indicator A x)" by blast - show ?thesis - proof (intro bexI[OF _ Y(1)] ballI) - fix A assume "A \ N" - have "positive_integral (\x. Y x * indicator A x) = P.positive_integral (\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 (\x. Y x * indicator A x) = ?Q A" - qed + with N_subalgebra show ?thesis + by (auto intro!: bexI[OF _ Y(1)]) qed -*) end