author hoelzl Wed May 21 13:52:46 2014 +0200 (2014-05-21) changeset 57036 22568fb89165 parent 57035 e865c4d99c49 child 57037 c51132be8e16
generalized Bochner integral over infinite sums
```     1.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Wed May 21 12:49:27 2014 +0200
1.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Wed May 21 13:52:46 2014 +0200
1.3 @@ -563,7 +563,7 @@
1.4      by (metis has_bochner_integral_simple_bochner_integrable)
1.5  qed
1.6
1.9    "has_bochner_integral M f x \<Longrightarrow> has_bochner_integral M g y \<Longrightarrow>
1.10      has_bochner_integral M (\<lambda>x. f x + g x) (x + y)"
1.11  proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
1.12 @@ -713,8 +713,7 @@
1.13  lemma has_bochner_integral_setsum:
1.14    "(\<And>i. i \<in> I \<Longrightarrow> has_bochner_integral M (f i) (x i)) \<Longrightarrow>
1.15      has_bochner_integral M (\<lambda>x. \<Sum>i\<in>I. f i x) (\<Sum>i\<in>I. x i)"
1.16 -  by (induct I rule: infinite_finite_induct)
1.17 -     (auto intro: has_bochner_integral_zero has_bochner_integral_add)
1.18 +  by (induct I rule: infinite_finite_induct) auto
1.19
1.20  lemma has_bochner_integral_implies_finite_norm:
1.21    "has_bochner_integral M f x \<Longrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>"
1.22 @@ -918,7 +917,7 @@
1.23    by (intro has_bochner_integral_cong_AE arg_cong[where f=The] ext)
1.24
1.25  lemma integrable_add[simp, intro]: "integrable M f \<Longrightarrow> integrable M g \<Longrightarrow> integrable M (\<lambda>x. f x + g x)"
1.26 -  by (auto simp: integrable.simps intro: has_bochner_integral_add)
1.27 +  by (auto simp: integrable.simps)
1.28
1.29  lemma integrable_zero[simp, intro]: "integrable M (\<lambda>x. 0)"
1.30    by (metis has_bochner_integral_zero integrable.simps)
1.31 @@ -1383,6 +1382,56 @@
1.32    finally show ?thesis .
1.33  qed
1.34
1.35 +lemma
1.36 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
1.37 +  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
1.38 +  and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
1.39 +  and sums: "summable (\<lambda>i. (\<integral>x. norm (f i x) \<partial>M))"
1.40 +  shows integrable_suminf: "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
1.41 +    and sums_integral: "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is "?f sums ?x")
1.42 +    and integral_suminf: "(\<integral>x. (\<Sum>i. f i x) \<partial>M) = (\<Sum>i. integral\<^sup>L M (f i))"
1.43 +    and summable_integral: "summable (\<lambda>i. integral\<^sup>L M (f i))"
1.44 +proof -
1.45 +  have 1: "integrable M (\<lambda>x. \<Sum>i. norm (f i x))"
1.46 +  proof (rule integrableI_bounded)
1.47 +    have "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) = (\<integral>\<^sup>+ x. (\<Sum>i. ereal (norm (f i x))) \<partial>M)"
1.48 +      apply (intro nn_integral_cong_AE)
1.49 +      using summable
1.50 +      apply eventually_elim
1.51 +      apply (simp add: suminf_ereal' suminf_nonneg)
1.52 +      done
1.53 +    also have "\<dots> = (\<Sum>i. \<integral>\<^sup>+ x. norm (f i x) \<partial>M)"
1.54 +      by (intro nn_integral_suminf) auto
1.55 +    also have "\<dots> = (\<Sum>i. ereal (\<integral>x. norm (f i x) \<partial>M))"
1.56 +      by (intro arg_cong[where f=suminf] ext nn_integral_eq_integral integrable_norm integrable) auto
1.57 +    finally show "(\<integral>\<^sup>+ x. ereal (norm (\<Sum>i. norm (f i x))) \<partial>M) < \<infinity>"
1.58 +      by (simp add: suminf_ereal' sums)
1.59 +  qed simp
1.60 +
1.61 +  have 2: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
1.62 +    using summable by eventually_elim (auto intro: summable_LIMSEQ summable_norm_cancel)
1.63 +
1.64 +  have 3: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))"
1.65 +    using summable
1.66 +  proof eventually_elim
1.67 +    fix j x assume [simp]: "summable (\<lambda>i. norm (f i x))"
1.68 +    have "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i<j. norm (f i x))" by (rule norm_setsum)
1.69 +    also have "\<dots> \<le> (\<Sum>i. norm (f i x))"
1.70 +      using setsum_le_suminf[of "\<lambda>i. norm (f i x)"] unfolding sums_iff by auto
1.71 +    finally show "norm (\<Sum>i<j. f i x) \<le> (\<Sum>i. norm (f i x))" by simp
1.72 +  qed
1.73 +
1.74 +  note int = integral_dominated_convergence(1,3)[OF _ _ 1 2 3]
1.75 +
1.76 +  show "integrable M ?S"
1.77 +    by (rule int) measurable
1.78 +
1.79 +  show "?f sums ?x" unfolding sums_def
1.80 +    using int(2) by (simp add: integrable)
1.81 +  then show "?x = suminf ?f" "summable ?f"
1.82 +    unfolding sums_iff by auto
1.83 +qed
1.84 +
1.85  lemma integral_norm_bound:
1.86    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
1.87    shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
1.88 @@ -1475,8 +1524,7 @@
1.89    shows "0 \<le> integral\<^sup>L M f"
1.90  proof -
1.91    have "0 \<le> ereal (integral\<^sup>L M (\<lambda>x. max 0 (f x)))"
1.92 -    by (subst integral_eq_nn_integral)
1.93 -       (auto intro: real_of_ereal_pos nn_integral_nonneg integrable_max assms)
1.94 +    by (subst integral_eq_nn_integral) (auto intro: real_of_ereal_pos nn_integral_nonneg assms)
1.95    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = integral\<^sup>L M f"
1.96      using assms(2) by (intro integral_cong_AE assms integrable_max) auto
1.97    finally show ?thesis
1.98 @@ -1616,7 +1664,7 @@
1.99        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. g x *\<^sub>R s i x)) ----> integral\<^sup>L (density M g) f"
1.100          unfolding lim(2)[symmetric]
1.101          by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
1.102 -           (insert lim(3-5), auto intro: integrable_norm)
1.103 +           (insert lim(3-5), auto)
1.104      qed
1.105    qed
1.106  qed (simp add: f g integrable_density)
1.107 @@ -1686,7 +1734,7 @@
1.108        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L M (\<lambda>x. f (g x))"
1.109        proof (rule integral_dominated_convergence(3))
1.110          show "integrable M (\<lambda>x. 2 * norm (f (g x)))"
1.111 -          using lim by (auto intro!: integrable_norm simp: integrable_distr_eq)
1.112 +          using lim by (auto simp: integrable_distr_eq)
1.113          show "AE x in M. (\<lambda>i. s i (g x)) ----> f (g x)"
1.114            using lim(3) g[THEN measurable_space] by auto
1.115          show "\<And>i. AE x in M. norm (s i (g x)) \<le> 2 * norm (f (g x))"
1.116 @@ -1695,7 +1743,7 @@
1.117        show "(\<lambda>i. integral\<^sup>L M (\<lambda>x. s i (g x))) ----> integral\<^sup>L (distr M N g) f"
1.118          unfolding lim(2)[symmetric]
1.119          by (rule integral_dominated_convergence(3)[where w="\<lambda>x. 2 * norm (f x)"])
1.120 -           (insert lim(3-5), auto intro: integrable_norm)
1.121 +           (insert lim(3-5), auto)
1.122      qed
1.123    qed
1.124  qed (simp add: f g integrable_distr_eq)
1.125 @@ -1764,9 +1812,9 @@
1.126    also have "\<dots> = integral\<^sup>L M (\<lambda>x. max 0 (f x)) - integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
1.127      by (intro integral_diff integrable_max integrable_minus integrable_zero f)
1.128    also have "integral\<^sup>L M (\<lambda>x. max 0 (f x)) = real (\<integral>\<^sup>+x. max 0 (f x) \<partial>M)"
1.129 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
1.130 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
1.131    also have "integral\<^sup>L M (\<lambda>x. max 0 (- f x)) = real (\<integral>\<^sup>+x. max 0 (- f x) \<partial>M)"
1.132 -    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: integrable_max f)
1.133 +    by (subst integral_eq_nn_integral[symmetric]) (auto intro!: f)
1.134    also have "(\<lambda>x. ereal (max 0 (f x))) = (\<lambda>x. max 0 (ereal (f x)))"
1.135      by (auto simp: max_def)
1.136    also have "(\<lambda>x. ereal (max 0 (- f x))) = (\<lambda>x. max 0 (- ereal (f x)))"
1.137 @@ -1967,73 +2015,10 @@
1.138    shows "integral\<^sup>L M X < integral\<^sup>L M Y"
1.139    using gt by (intro integral_less_AE[OF int, where A="space M"]) auto
1.140
1.141 -(* GENERALIZE to banach, sct *)
1.142 -lemma integral_sums:
1.143 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
1.144 -  assumes integrable[measurable]: "\<And>i. integrable M (f i)"
1.145 -  and summable: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>f i x\<bar>)"
1.146 -  and sums: "summable (\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
1.147 -  shows "integrable M (\<lambda>x. (\<Sum>i. f i x))" (is "integrable M ?S")
1.148 -  and "(\<lambda>i. integral\<^sup>L M (f i)) sums (\<integral>x. (\<Sum>i. f i x) \<partial>M)" (is ?integral)
1.149 -proof -
1.150 -  have "\<forall>x\<in>space M. \<exists>w. (\<lambda>i. \<bar>f i x\<bar>) sums w"
1.151 -    using summable unfolding summable_def by auto
1.152 -  from bchoice[OF this]
1.153 -  obtain w where w: "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. \<bar>f i x\<bar>) sums w x" by auto
1.154 -  then have w_borel: "w \<in> borel_measurable M" unfolding sums_def
1.155 -    by (rule borel_measurable_LIMSEQ) auto
1.156 -
1.157 -  let ?w = "\<lambda>y. if y \<in> space M then w y else 0"
1.158 -
1.159 -  obtain x where abs_sum: "(\<lambda>i. (\<integral>x. \<bar>f i x\<bar> \<partial>M)) sums x"
1.160 -    using sums unfolding summable_def ..
1.161 -
1.162 -  have 1: "\<And>n. integrable M (\<lambda>x. \<Sum>i<n. f i x)"
1.163 -    using integrable by auto
1.164 -
1.165 -  have 2: "\<And>j. AE x in M. norm (\<Sum>i<j. f i x) \<le> ?w x"
1.166 -    using AE_space
1.167 -  proof eventually_elim
1.168 -    fix j x assume [simp]: "x \<in> space M"
1.169 -    have "\<bar>\<Sum>i<j. f i x\<bar> \<le> (\<Sum>i<j. \<bar>f i x\<bar>)" by (rule setsum_abs)
1.170 -    also have "\<dots> \<le> w x" using w[of x] setsum_le_suminf[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
1.171 -    finally show "norm (\<Sum>i<j. f i x) \<le> ?w x" by simp
1.172 -  qed
1.173 -
1.174 -  have 3: "integrable M ?w"
1.175 -  proof (rule integrable_monotone_convergence(1))
1.176 -    let ?F = "\<lambda>n y. (\<Sum>i<n. \<bar>f i y\<bar>)"
1.177 -    let ?w' = "\<lambda>n y. if y \<in> space M then ?F n y else 0"
1.178 -    have "\<And>n. integrable M (?F n)"
1.179 -      using integrable by (auto intro!: integrable_abs)
1.180 -    thus "\<And>n. integrable M (?w' n)" by (simp cong: integrable_cong)
1.181 -    show "AE x in M. mono (\<lambda>n. ?w' n x)"
1.182 -      by (auto simp: mono_def le_fun_def intro!: setsum_mono2)
1.183 -    show "AE x in M. (\<lambda>n. ?w' n x) ----> ?w x"
1.184 -        using w by (simp_all add: tendsto_const sums_def)
1.185 -    have *: "\<And>n. integral\<^sup>L M (?w' n) = (\<Sum>i< n. (\<integral>x. \<bar>f i x\<bar> \<partial>M))"
1.186 -      using integrable by (simp add: integrable_abs cong: integral_cong)
1.187 -    from abs_sum
1.188 -    show "(\<lambda>i. integral\<^sup>L M (?w' i)) ----> x" unfolding * sums_def .
1.189 -  qed (simp add: w_borel measurable_If_set)
1.190 -
1.191 -  from summable[THEN summable_rabs_cancel]
1.192 -  have 4: "AE x in M. (\<lambda>n. \<Sum>i<n. f i x) ----> (\<Sum>i. f i x)"
1.193 -    by (auto intro: summable_LIMSEQ)
1.194 -
1.195 -  note int = integral_dominated_convergence(1,3)[OF _ _ 3 4 2]
1.196 -
1.197 -  from int show "integrable M ?S" by simp
1.198 -
1.199 -  show ?integral unfolding sums_def integral_setsum(1)[symmetric, OF integrable]
1.200 -    using int(2) by simp
1.201 -qed
1.202 -
1.203  lemma integrable_mult_indicator:
1.204    fixes f :: "'a \<Rightarrow> real"
1.205    shows "A \<in> sets M \<Longrightarrow> integrable M f \<Longrightarrow> integrable M (\<lambda>x. f x * indicator A x)"
1.206 -  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"])
1.207 -     (auto intro: integrable_abs split: split_indicator)
1.208 +  by (rule integrable_bound[where f="\<lambda>x. \<bar>f x\<bar>"]) (auto split: split_indicator)
1.209
1.210  lemma tendsto_integral_at_top:
1.211    fixes f :: "real \<Rightarrow> real"
1.212 @@ -2069,15 +2054,14 @@
1.213    let ?p = "integral\<^sup>L M (\<lambda>x. max 0 (f x))"
1.214    let ?n = "integral\<^sup>L M (\<lambda>x. max 0 (- f x))"
1.215    have "(?P ---> ?p) at_top" "(?N ---> ?n) at_top"
1.216 -    by (auto intro!: nonneg integrable_max f)
1.217 +    by (auto intro!: nonneg f)
1.218    note tendsto_diff[OF this]
1.219    also have "(\<lambda>y. ?P y - ?N y) = (\<lambda>y. \<integral> x. f x * indicator {..y} x \<partial>M)"
1.220      by (subst integral_diff[symmetric])
1.221 -       (auto intro!: integrable_mult_indicator integrable_max f integral_cong
1.222 +       (auto intro!: integrable_mult_indicator f integral_cong
1.223               simp: M split: split_max)
1.224    also have "?p - ?n = integral\<^sup>L M f"
1.225 -    by (subst integral_diff[symmetric])
1.226 -       (auto intro!: integrable_max f integral_cong simp: M split: split_max)
1.227 +    by (subst integral_diff[symmetric]) (auto intro!: f integral_cong simp: M split: split_max)
1.228    finally show ?thesis .
1.229  qed
1.230
1.231 @@ -2112,67 +2096,6 @@
1.232      by (auto simp: _has_bochner_integral_iff)
1.233  qed
1.234
1.235 -
1.236 -subsection {* Lebesgue integration on countable spaces *}
1.237 -
1.238 -lemma integral_on_countable:
1.239 -  fixes f :: "real \<Rightarrow> real"
1.240 -  assumes f: "f \<in> borel_measurable M"
1.241 -  and bij: "bij_betw enum S (f ` space M)"
1.242 -  and enum_zero: "enum ` (-S) \<subseteq> {0}"
1.243 -  and fin: "\<And>x. x \<noteq> 0 \<Longrightarrow> (emeasure M) (f -` {x} \<inter> space M) \<noteq> \<infinity>"
1.244 -  and abs_summable: "summable (\<lambda>r. \<bar>enum r * real ((emeasure M) (f -` {enum r} \<inter> space M))\<bar>)"
1.245 -  shows "integrable M f"
1.246 -  and "(\<lambda>r. enum r * real ((emeasure M) (f -` {enum r} \<inter> space M))) sums integral\<^sup>L M f" (is ?sums)
1.247 -proof -
1.248 -  let ?A = "\<lambda>r. f -` {enum r} \<inter> space M"
1.249 -  let ?F = "\<lambda>r x. enum r * indicator (?A r) x"
1.250 -  have enum_eq: "\<And>r. enum r * real ((emeasure M) (?A r)) = integral\<^sup>L M (?F r)"
1.251 -    using f fin by (simp add: measure_def cong: disj_cong)
1.252 -
1.253 -  { fix x assume "x \<in> space M"
1.254 -    hence "f x \<in> enum ` S" using bij unfolding bij_betw_def by auto
1.255 -    then obtain i where "i\<in>S" "enum i = f x" by auto
1.256 -    have F: "\<And>j. ?F j x = (if j = i then f x else 0)"
1.257 -    proof cases
1.258 -      fix j assume "j = i"
1.259 -      thus "?thesis j" using `x \<in> space M` `enum i = f x` by (simp add: indicator_def)
1.260 -    next
1.261 -      fix j assume "j \<noteq> i"
1.262 -      show "?thesis j" using bij `i \<in> S` `j \<noteq> i` `enum i = f x` enum_zero
1.263 -        by (cases "j \<in> S") (auto simp add: indicator_def bij_betw_def inj_on_def)
1.264 -    qed
1.265 -    hence F_abs: "\<And>j. \<bar>if j = i then f x else 0\<bar> = (if j = i then \<bar>f x\<bar> else 0)" by auto
1.266 -    have "(\<lambda>i. ?F i x) sums f x"
1.267 -         "(\<lambda>i. \<bar>?F i x\<bar>) sums \<bar>f x\<bar>"
1.268 -      by (auto intro!: sums_single simp: F F_abs) }
1.269 -  note F_sums_f = this(1) and F_abs_sums_f = this(2)
1.270 -
1.271 -  have int_f: "integral\<^sup>L M f = (\<integral>x. (\<Sum>r. ?F r x) \<partial>M)" "integrable M f = integrable M (\<lambda>x. \<Sum>r. ?F r x)"
1.272 -    using F_sums_f by (auto intro!: integral_cong integrable_cong simp: sums_iff)
1.273 -
1.274 -  { fix r
1.275 -    have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = (\<integral>x. \<bar>enum r\<bar> * indicator (?A r) x \<partial>M)"
1.276 -      by (auto simp: indicator_def intro!: integral_cong)
1.277 -    also have "\<dots> = \<bar>enum r\<bar> * real ((emeasure M) (?A r))"
1.278 -      using f fin by (simp add: measure_def cong: disj_cong)
1.279 -    finally have "(\<integral>x. \<bar>?F r x\<bar> \<partial>M) = \<bar>enum r * real ((emeasure M) (?A r))\<bar>"
1.280 -      using f by (subst (2) abs_mult_pos[symmetric]) (auto intro!: real_of_ereal_pos measurable_sets) }
1.281 -  note int_abs_F = this
1.282 -
1.283 -  have 1: "\<And>i. integrable M (\<lambda>x. ?F i x)"
1.284 -    using f fin by auto
1.285 -
1.286 -  have 2: "\<And>x. x \<in> space M \<Longrightarrow> summable (\<lambda>i. \<bar>?F i x\<bar>)"
1.287 -    using F_abs_sums_f unfolding sums_iff by auto
1.288 -
1.289 -  from integral_sums(2)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
1.290 -  show ?sums unfolding enum_eq int_f by simp
1.291 -
1.292 -  from integral_sums(1)[OF 1 2, unfolded int_abs_F, OF _ abs_summable]
1.293 -  show "integrable M f" unfolding int_f by simp
1.294 -qed
1.295 -
1.296  subsection {* Product measure *}
1.297
1.298  lemma (in sigma_finite_measure) borel_measurable_lebesgue_integrable[measurable (raw)]:
1.299 @@ -2419,7 +2342,7 @@
1.300      show "(\<lambda>i. integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (s i)) ----> integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) f"
1.301      proof (rule integral_dominated_convergence)
1.302        show "integrable (M1 \<Otimes>\<^sub>M M2) (\<lambda>x. 2 * norm (f x))"
1.303 -        using lim(5) by (auto intro: integrable_norm)
1.304 +        using lim(5) by auto
1.305      qed (insert lim, auto)
1.306      have "(\<lambda>i. \<integral> x. \<integral> y. s i (x, y) \<partial>M2 \<partial>M1) ----> \<integral> x. \<integral> y. f (x, y) \<partial>M2 \<partial>M1"
1.307      proof (rule integral_dominated_convergence)
1.308 @@ -2433,7 +2356,7 @@
1.309          show "(\<lambda>i. \<integral> y. s i (x, y) \<partial>M2) ----> \<integral> y. f (x, y) \<partial>M2"
1.310          proof (rule integral_dominated_convergence)
1.311            show "integrable M2 (\<lambda>y. 2 * norm (f (x, y)))"
1.312 -             using f by (auto intro: integrable_norm)
1.313 +             using f by auto
1.314            show "AE xa in M2. (\<lambda>i. s i (x, xa)) ----> f (x, xa)"
1.315              using x lim(3) by (auto simp: space_pair_measure)
1.316            show "\<And>i. AE xa in M2. norm (s i (x, xa)) \<le> 2 * norm (f (x, xa))"
```
```     2.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed May 21 12:49:27 2014 +0200
2.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed May 21 13:52:46 2014 +0200
2.3 @@ -1187,13 +1187,13 @@
2.4  qed auto
2.5
2.6  lemma sets_Collect_Cauchy[measurable]:
2.7 -  fixes f :: "nat \<Rightarrow> 'a => real"
2.8 +  fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
2.9    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
2.10    shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
2.11 -  unfolding Cauchy_iff2 using f by auto
2.12 +  unfolding metric_Cauchy_iff2 using f by auto
2.13
2.14  lemma borel_measurable_lim[measurable (raw)]:
2.15 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
2.16 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
2.17    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
2.18    shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
2.19  proof -
2.20 @@ -1201,7 +1201,7 @@
2.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))"
2.22      by (auto simp: lim_def convergent_eq_cauchy[symmetric])
2.23    have "u' \<in> borel_measurable M"
2.24 -  proof (rule borel_measurable_LIMSEQ)
2.25 +  proof (rule borel_measurable_LIMSEQ_metric)
2.26      fix x
2.27      have "convergent (\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0)"
2.28        by (cases "Cauchy (\<lambda>i. f i x)")
2.29 @@ -1215,7 +1215,7 @@
2.30  qed
2.31
2.32  lemma borel_measurable_suminf[measurable (raw)]:
2.33 -  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
2.34 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
2.35    assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
2.36    shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
2.37    unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
```