src/HOL/Probability/Conditional_Probability.thy

 definition (in prob_space)
   "conditional_expectation N X = (SOME Y. Y\<in>borel_measurable N \<and> (\<forall>x. 0 \<le> Y x)
     \<and> (\<forall>C\<in>sets N. (\<integral>\<^isup>+x. Y x * indicator C x\<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x\<partial>M)))"
 
 lemma (in prob_space) conditional_expectation_exists:
-  fixes X :: "'a \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme"
+  fixes X :: "'a \<Rightarrow> ereal" and N :: "('a, 'b) measure_space_scheme"
   assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x"
   and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A"
   shows "\<exists>Y\<in>borel_measurable N. (\<forall>x. 0 \<le> Y x) \<and> (\<forall>C\<in>sets N.
       (\<integral>\<^isup>+x. Y x * indicator C x \<partial>M) = (\<integral>\<^isup>+x. X x * indicator C x \<partial>M))"
 proof -

   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 \<Rightarrow> extreal" and N :: "('a, 'b) measure_space_scheme"
+  fixes X :: "'a \<Rightarrow> ereal" and N :: "('a, 'b) measure_space_scheme"
   assumes borel: "X \<in> borel_measurable M" "AE x. 0 \<le> X x"
   and N: "sigma_algebra N" "sets N \<subseteq> sets M" "space N = space M" "\<And>A. measure N A = \<mu> A"
   shows borel_measurable_conditional_expectation:
     "conditional_expectation N X \<in> borel_measurable N"
   and conditional_expectation: "\<And>C. C \<in> sets N \<Longrightarrow>

   from CE show "\<And>C. C \<in> sets N \<Longrightarrow> ?eq C"
     unfolding conditional_expectation_def by (rule someI2_ex) blast
 qed
 
 lemma (in sigma_algebra) factorize_measurable_function_pos:
-  fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c"
+  fixes Z :: "'a \<Rightarrow> ereal" and Y :: "'a \<Rightarrow> 'c"
   assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
   assumes Z: "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)"
   shows "\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. max 0 (Z x) = g (Y x)"
 proof -
   interpret M': sigma_algebra M' by fact

     show "\<exists>g. simple_function M' g \<and> (\<forall>x\<in>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 \<in> space M"
-      then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::extreal)"
+      then have "\<And>z. z \<in> f i`space M \<Longrightarrow> indicator (B z) (Y x) = (indicator (f i -` {z} \<inter> space M) x::ereal)"
         unfolding indicator_def using B by auto
       then show "f i x = ?g (Y x)" using `x \<in> space M` f(1)[of i]
         by (subst va.simple_function_indicator_representation) auto
     qed
   qed

     finally show "max 0 (Z x) = (SUP i. g i (Y x))" .
   qed
 qed
 
 lemma (in sigma_algebra) factorize_measurable_function:
-  fixes Z :: "'a \<Rightarrow> extreal" and Y :: "'a \<Rightarrow> 'c"
+  fixes Z :: "'a \<Rightarrow> ereal" and Y :: "'a \<Rightarrow> 'c"
   assumes "sigma_algebra M'" and "Y \<in> measurable M M'" "Z \<in> borel_measurable M"
   shows "Z \<in> borel_measurable (sigma_algebra.vimage_algebra M' (space M) Y)
     \<longleftrightarrow> (\<exists>g\<in>borel_measurable M'. \<forall>x\<in>space M. Z x = g (Y x))"
 proof safe
   interpret M': sigma_algebra M' by fact
   have Y: "Y \<in> space M \<rightarrow> 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 \<Rightarrow> extreal" assume "g \<in> borel_measurable M'"
+  { fix g :: "'c \<Rightarrow> ereal" assume "g \<in> borel_measurable M'"
     with M'.measurable_vimage_algebra[OF Y]
     have "g \<circ> Y \<in> borel_measurable (M'.vimage_algebra (space M) Y)"
       by (rule measurable_comp)
     moreover assume "\<forall>x\<in>space M. Z x = g (Y x)"
     then have "Z \<in> borel_measurable (M'.vimage_algebra (space M) Y) \<longleftrightarrow>