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
```