src/HOL/Probability/Borel_Space.thy
changeset 43923 ab93d0190a5d
parent 43920 cedb5cb948fd
child 44282 f0de18b62d63
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Jul 19 14:37:49 2011 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Jul 19 14:38:29 2011 +0200
     1.3 @@ -1122,7 +1122,7 @@
     1.4    show "(real -` B \<inter> space borel :: ereal set) \<in> sets borel"
     1.5    proof cases
     1.6      assume "0 \<in> B"
     1.7 -    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0}"
     1.8 +    then have *: "real -` B = real -` (B - {0}) \<union> {-\<infinity>, \<infinity>, 0::ereal}"
     1.9        by (auto simp add: real_of_ereal_eq_0)
    1.10      then show "(real -` B :: ereal set) \<inter> space borel \<in> sets borel"
    1.11        using open_real by auto
    1.12 @@ -1148,7 +1148,8 @@
    1.13  qed auto
    1.14  
    1.15  lemma (in sigma_algebra) borel_measurable_ereal_iff_real:
    1.16 -  "f \<in> borel_measurable M \<longleftrightarrow>
    1.17 +  fixes f :: "'a \<Rightarrow> ereal"
    1.18 +  shows "f \<in> borel_measurable M \<longleftrightarrow>
    1.19      ((\<lambda>x. real (f x)) \<in> borel_measurable M \<and> f -` {\<infinity>} \<inter> space M \<in> sets M \<and> f -` {-\<infinity>} \<inter> space M \<in> sets M)"
    1.20  proof safe
    1.21    assume *: "(\<lambda>x. real (f x)) \<in> borel_measurable M" "f -` {\<infinity>} \<inter> space M \<in> sets M" "f -` {-\<infinity>} \<inter> space M \<in> sets M"
    1.22 @@ -1208,7 +1209,8 @@
    1.23  qed auto
    1.24  
    1.25  lemma (in sigma_algebra) borel_measurable_eq_atMost_ereal:
    1.26 -  "(f::'a \<Rightarrow> ereal) \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
    1.27 +  fixes f :: "'a \<Rightarrow> ereal"
    1.28 +  shows "f \<in> borel_measurable M \<longleftrightarrow> (\<forall>a. f -` {..a} \<inter> space M \<in> sets M)"
    1.29  proof (intro iffI allI)
    1.30    assume pos[rule_format]: "\<forall>a. f -` {..a} \<inter> space M \<in> sets M"
    1.31    show "f \<in> borel_measurable M"
    1.32 @@ -1226,7 +1228,7 @@
    1.33        by (auto simp: not_le)
    1.34      then show "f -` {\<infinity>} \<inter> space M \<in> sets M" using pos by (auto simp del: UN_simps intro!: Diff)
    1.35      moreover
    1.36 -    have "{-\<infinity>} = {..-\<infinity>}" by auto
    1.37 +    have "{-\<infinity>::ereal} = {..-\<infinity>}" by auto
    1.38      then show "f -` {-\<infinity>} \<inter> space M \<in> sets M" using pos by auto
    1.39      moreover have "{x\<in>space M. f x \<le> ereal a} \<in> sets M"
    1.40        using pos[of "ereal a"] by (simp add: vimage_def Int_def conj_commute)