src/HOL/Probability/Borel_Space.thy
changeset 57036 22568fb89165
parent 56994 8d5e5ec1cac3
child 57137 f174712d0a84
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed May 21 12:49:27 2014 +0200
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed May 21 13:52:46 2014 +0200
     1.3 @@ -1187,13 +1187,13 @@
     1.4  qed auto
     1.5  
     1.6  lemma sets_Collect_Cauchy[measurable]: 
     1.7 -  fixes f :: "nat \<Rightarrow> 'a => real"
     1.8 +  fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
     1.9    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
    1.10    shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
    1.11 -  unfolding Cauchy_iff2 using f by auto
    1.12 +  unfolding metric_Cauchy_iff2 using f by auto
    1.13  
    1.14  lemma borel_measurable_lim[measurable (raw)]:
    1.15 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
    1.16 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.17    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
    1.18    shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
    1.19  proof -
    1.20 @@ -1201,7 +1201,7 @@
    1.21    then have *: "\<And>x. lim (\<lambda>i. f i x) = (if Cauchy (\<lambda>i. f i x) then u' x else (THE x. False))"
    1.22      by (auto simp: lim_def convergent_eq_cauchy[symmetric])
    1.23    have "u' \<in> borel_measurable M"
    1.24 -  proof (rule borel_measurable_LIMSEQ)
    1.25 +  proof (rule borel_measurable_LIMSEQ_metric)
    1.26      fix x
    1.27      have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
    1.28        by (cases "Cauchy (\<lambda>i. f i x)")
    1.29 @@ -1215,7 +1215,7 @@
    1.30  qed
    1.31  
    1.32  lemma borel_measurable_suminf[measurable (raw)]:
    1.33 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
    1.34 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
    1.35    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
    1.36    shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
    1.37    unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp