1(* Title: HOL/Probability/Weak_Convergence.thy 2 Authors: Jeremy Avigad (CMU), Johannes H��lzl (TUM) 3*) 4 5section \<open>Weak Convergence of Functions and Distributions\<close> 6 7text \<open>Properties of weak convergence of functions and measures, including the portmanteau theorem.\<close> 8 9theory Weak_Convergence 10 imports Distribution_Functions 11begin 12 13section \<open>Weak Convergence of Functions\<close> 14 15definition 16 weak_conv :: "(nat \<Rightarrow> (real \<Rightarrow> real)) \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool" 17where 18 "weak_conv F_seq F \<equiv> \<forall>x. isCont F x \<longrightarrow> (\<lambda>n. F_seq n x) \<longlonglongrightarrow> F x" 19 20section \<open>Weak Convergence of Distributions\<close> 21 22definition 23 weak_conv_m :: "(nat \<Rightarrow> real measure) \<Rightarrow> real measure \<Rightarrow> bool" 24where 25 "weak_conv_m M_seq M \<equiv> weak_conv (\<lambda>n. cdf (M_seq n)) (cdf M)" 26 27section \<open>Skorohod's theorem\<close> 28 29locale right_continuous_mono = 30 fixes f :: "real \<Rightarrow> real" and a b :: real 31 assumes cont: "\<And>x. continuous (at_right x) f" 32 assumes mono: "mono f" 33 assumes bot: "(f \<longlongrightarrow> a) at_bot" 34 assumes top: "(f \<longlongrightarrow> b) at_top" 35begin 36 37abbreviation I :: "real \<Rightarrow> real" where 38 "I \<omega> \<equiv> Inf {x. \<omega> \<le> f x}" 39 40lemma pseudoinverse: assumes "a < \<omega>" "\<omega> < b" shows "\<omega> \<le> f x \<longleftrightarrow> I \<omega> \<le> x" 41proof 42 let ?F = "{x. \<omega> \<le> f x}" 43 obtain y where "f y < \<omega>" 44 by (metis eventually_happens' trivial_limit_at_bot_linorder order_tendstoD(2) bot \<open>a < \<omega>\<close>) 45 with mono have bdd: "bdd_below ?F" 46 by (auto intro!: bdd_belowI[of _ y] elim: mono_invE[OF _ less_le_trans]) 47 48 have ne: "?F \<noteq> {}" 49 using order_tendstoD(1)[OF top \<open>\<omega> < b\<close>] 50 by (auto dest!: eventually_happens'[OF trivial_limit_at_top_linorder] intro: less_imp_le) 51 52 show "\<omega> \<le> f x \<Longrightarrow> I \<omega> \<le> x" 53 by (auto intro!: cInf_lower bdd) 54 55 { assume *: "I \<omega> \<le> x" 56 have "\<omega> \<le> (INF s\<in>{x. \<omega> \<le> f x}. f s)" 57 by (rule cINF_greatest[OF ne]) auto 58 also have "\<dots> = f (I \<omega>)" 59 using continuous_at_Inf_mono[OF mono cont ne bdd] .. 60 also have "\<dots> \<le> f x" 61 using * by (rule monoD[OF \<open>mono f\<close>]) 62 finally show "\<omega> \<le> f x" . } 63qed 64 65lemma pseudoinverse': "\<forall>\<omega>\<in>{a<..<b}. \<forall>x. \<omega> \<le> f x \<longleftrightarrow> I \<omega> \<le> x" 66 by (intro ballI allI impI pseudoinverse) auto 67 68lemma mono_I: "mono_on I {a <..< b}" 69 unfolding mono_on_def by (metis order.trans order.refl pseudoinverse') 70 71end 72 73locale cdf_distribution = real_distribution 74begin 75 76abbreviation "C \<equiv> cdf M" 77 78sublocale right_continuous_mono C 0 1 79 by standard 80 (auto intro: cdf_nondecreasing cdf_is_right_cont cdf_lim_at_top_prob cdf_lim_at_bot monoI) 81 82lemma measurable_C[measurable]: "C \<in> borel_measurable borel" 83 by (intro borel_measurable_mono mono) 84 85lemma measurable_CI[measurable]: "I \<in> borel_measurable (restrict_space borel {0<..<1})" 86 by (intro borel_measurable_mono_on_fnc mono_I) 87 88lemma emeasure_distr_I: "emeasure (distr (restrict_space lborel {0<..<1::real}) borel I) UNIV = 1" 89 by (simp add: emeasure_distr space_restrict_space emeasure_restrict_space ) 90 91lemma distr_I_eq_M: "distr (restrict_space lborel {0<..<1::real}) borel I = M" (is "?I = _") 92proof (intro cdf_unique ext) 93 let ?\<Omega> = "restrict_space lborel {0<..<1}::real measure" 94 interpret \<Omega>: prob_space ?\<Omega> 95 by (auto simp add: emeasure_restrict_space space_restrict_space intro!: prob_spaceI) 96 show "real_distribution ?I" 97 by auto 98 99 fix x 100 have "cdf ?I x = measure lborel {\<omega>\<in>{0<..<1}. \<omega> \<le> C x}" 101 by (subst cdf_def) 102 (auto simp: pseudoinverse[symmetric] measure_distr space_restrict_space measure_restrict_space 103 intro!: arg_cong2[where f="measure"]) 104 also have "\<dots> = measure lborel {0 <..< C x}" 105 using cdf_bounded_prob[of x] AE_lborel_singleton[of "C x"] 106 by (auto intro!: arg_cong[where f=enn2real] emeasure_eq_AE simp: measure_def) 107 also have "\<dots> = C x" 108 by (simp add: cdf_nonneg) 109 finally show "cdf (distr ?\<Omega> borel I) x = C x" . 110qed standard 111 112end 113 114context 115 fixes \<mu> :: "nat \<Rightarrow> real measure" 116 and M :: "real measure" 117 assumes \<mu>: "\<And>n. real_distribution (\<mu> n)" 118 assumes M: "real_distribution M" 119 assumes \<mu>_to_M: "weak_conv_m \<mu> M" 120begin 121 122(* state using obtains? *) 123theorem Skorohod: 124 "\<exists> (\<Omega> :: real measure) (Y_seq :: nat \<Rightarrow> real \<Rightarrow> real) (Y :: real \<Rightarrow> real). 125 prob_space \<Omega> \<and> 126 (\<forall>n. Y_seq n \<in> measurable \<Omega> borel) \<and> 127 (\<forall>n. distr \<Omega> borel (Y_seq n) = \<mu> n) \<and> 128 Y \<in> measurable \<Omega> lborel \<and> 129 distr \<Omega> borel Y = M \<and> 130 (\<forall>x \<in> space \<Omega>. (\<lambda>n. Y_seq n x) \<longlonglongrightarrow> Y x)" 131proof - 132 interpret \<mu>: cdf_distribution "\<mu> n" for n 133 unfolding cdf_distribution_def by (rule \<mu>) 134 interpret M: cdf_distribution M 135 unfolding cdf_distribution_def by (rule M) 136 137 have conv: "measure M {x} = 0 \<Longrightarrow> (\<lambda>n. \<mu>.C n x) \<longlonglongrightarrow> M.C x" for x 138 using \<mu>_to_M M.isCont_cdf by (auto simp: weak_conv_m_def weak_conv_def) 139 140 let ?\<Omega> = "restrict_space lborel {0<..<1} :: real measure" 141 have "prob_space ?\<Omega>" 142 by (auto simp: space_restrict_space emeasure_restrict_space intro!: prob_spaceI) 143 interpret \<Omega>: prob_space ?\<Omega> 144 by fact 145 146 have Y_distr: "distr ?\<Omega> borel M.I = M" 147 by (rule M.distr_I_eq_M) 148 149 have Y_cts_cnv: "(\<lambda>n. \<mu>.I n \<omega>) \<longlonglongrightarrow> M.I \<omega>" 150 if \<omega>: "\<omega> \<in> {0<..<1}" "isCont M.I \<omega>" for \<omega> :: real 151 proof (intro limsup_le_liminf_real) 152 show "liminf (\<lambda>n. \<mu>.I n \<omega>) \<ge> M.I \<omega>" 153 unfolding le_Liminf_iff 154 proof safe 155 fix B :: ereal assume B: "B < M.I \<omega>" 156 then show "\<forall>\<^sub>F n in sequentially. B < \<mu>.I n \<omega>" 157 proof (cases B) 158 case (real r) 159 with B have r: "r < M.I \<omega>" 160 by simp 161 then obtain x where x: "r < x" "x < M.I \<omega>" "measure M {x} = 0" 162 using open_minus_countable[OF M.countable_support, of "{r<..<M.I \<omega>}"] by auto 163 then have Fx_less: "M.C x < \<omega>" 164 using M.pseudoinverse' \<omega> not_less by blast 165 166 have "\<forall>\<^sub>F n in sequentially. \<mu>.C n x < \<omega>" 167 using order_tendstoD(2)[OF conv[OF x(3)] Fx_less] . 168 then have "\<forall>\<^sub>F n in sequentially. x < \<mu>.I n \<omega>" 169 by eventually_elim (insert \<omega> \<mu>.pseudoinverse[symmetric], simp add: not_le[symmetric]) 170 then show ?thesis 171 by eventually_elim (insert x(1), simp add: real) 172 qed auto 173 qed 174 175 have *: "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>'" 176 if \<omega>': "0 < \<omega>'" "\<omega>' < 1" "\<omega> < \<omega>'" for \<omega>' :: real 177 proof (rule dense_ge_bounded) 178 fix B' assume "ereal (M.I \<omega>') < B'" "B' < ereal (M.I \<omega>' + 1)" 179 then obtain B where "M.I \<omega>' < B" and [simp]: "B' = ereal B" 180 by (cases B') auto 181 then obtain y where y: "M.I \<omega>' < y" "y < B" "measure M {y} = 0" 182 using open_minus_countable[OF M.countable_support, of "{M.I \<omega>'<..<B}"] by auto 183 then have "\<omega>' \<le> M.C (M.I \<omega>')" 184 using M.pseudoinverse' \<omega>' by (metis greaterThanLessThan_iff order_refl) 185 also have "... \<le> M.C y" 186 using M.mono y unfolding mono_def by auto 187 finally have Fy_gt: "\<omega> < M.C y" 188 using \<omega>'(3) by simp 189 190 have "\<forall>\<^sub>F n in sequentially. \<omega> \<le> \<mu>.C n y" 191 using order_tendstoD(1)[OF conv[OF y(3)] Fy_gt] by eventually_elim (rule less_imp_le) 192 then have 2: "\<forall>\<^sub>F n in sequentially. \<mu>.I n \<omega> \<le> ereal y" 193 by simp (subst \<mu>.pseudoinverse'[rule_format, OF \<omega>(1), symmetric]) 194 then show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> B'" 195 using \<open>y < B\<close> 196 by (intro Limsup_bounded[rotated]) (auto intro: le_less_trans elim: eventually_mono) 197 qed simp 198 199 have **: "(M.I \<longlongrightarrow> ereal (M.I \<omega>)) (at_right \<omega>)" 200 using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at) 201 show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>" 202 using \<omega> 203 by (intro tendsto_lowerbound[OF **]) 204 (auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1]) 205 qed 206 207 let ?D = "{\<omega>\<in>{0<..<1}. \<not> isCont M.I \<omega>}" 208 have D_countable: "countable ?D" 209 using mono_on_ctble_discont[OF M.mono_I] by (simp add: at_within_open[of _ "{0 <..< 1}"] cong: conj_cong) 210 hence D: "emeasure ?\<Omega> ?D = 0" 211 using emeasure_lborel_countable[OF D_countable] 212 by (subst emeasure_restrict_space) auto 213 214 define Y' where "Y' \<omega> = (if \<omega> \<in> ?D then 0 else M.I \<omega>)" for \<omega> 215 have Y'_AE: "AE \<omega> in ?\<Omega>. Y' \<omega> = M.I \<omega>" 216 by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y'_def) 217 218 define Y_seq' where "Y_seq' n \<omega> = (if \<omega> \<in> ?D then 0 else \<mu>.I n \<omega>)" for n \<omega> 219 have Y_seq'_AE: "\<And>n. AE \<omega> in ?\<Omega>. Y_seq' n \<omega> = \<mu>.I n \<omega>" 220 by (rule AE_I [OF _ D]) (auto simp: space_restrict_space sets_restrict_space_iff Y_seq'_def) 221 222 have Y'_cnv: "\<forall>\<omega>\<in>{0<..<1}. (\<lambda>n. Y_seq' n \<omega>) \<longlonglongrightarrow> Y' \<omega>" 223 by (auto simp: Y'_def Y_seq'_def Y_cts_cnv) 224 225 have [simp]: "Y_seq' n \<in> borel_measurable ?\<Omega>" for n 226 by (rule measurable_discrete_difference[of "\<mu>.I n" _ _ ?D]) 227 (insert \<mu>.measurable_CI[of n] D_countable, auto simp: sets_restrict_space Y_seq'_def) 228 moreover have "distr ?\<Omega> borel (Y_seq' n) = \<mu> n" for n 229 using \<mu>.distr_I_eq_M [of n] Y_seq'_AE [of n] 230 by (subst distr_cong_AE[where f = "Y_seq' n" and g = "\<mu>.I n"], auto) 231 moreover have [simp]: "Y' \<in> borel_measurable ?\<Omega>" 232 by (rule measurable_discrete_difference[of M.I _ _ ?D]) 233 (insert M.measurable_CI D_countable, auto simp: sets_restrict_space Y'_def) 234 moreover have "distr ?\<Omega> borel Y' = M" 235 using M.distr_I_eq_M Y'_AE 236 by (subst distr_cong_AE[where f = Y' and g = M.I], auto) 237 ultimately have "prob_space ?\<Omega> \<and> (\<forall>n. Y_seq' n \<in> borel_measurable ?\<Omega>) \<and> 238 (\<forall>n. distr ?\<Omega> borel (Y_seq' n) = \<mu> n) \<and> Y' \<in> measurable ?\<Omega> lborel \<and> distr ?\<Omega> borel Y' = M \<and> 239 (\<forall>x\<in>space ?\<Omega>. (\<lambda>n. Y_seq' n x) \<longlonglongrightarrow> Y' x)" 240 using Y'_cnv \<open>prob_space ?\<Omega>\<close> by (auto simp: space_restrict_space) 241 thus ?thesis by metis 242qed 243 244text \<open> 245 The Portmanteau theorem, that is, the equivalence of various definitions of weak convergence. 246\<close> 247 248theorem weak_conv_imp_bdd_ae_continuous_conv: 249 fixes 250 f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" 251 assumes 252 discont_null: "M ({x. \<not> isCont f x}) = 0" and 253 f_bdd: "\<And>x. norm (f x) \<le> B" and 254 [measurable]: "f \<in> borel_measurable borel" 255 shows 256 "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f" 257proof - 258 have "0 \<le> B" 259 using norm_ge_zero f_bdd by (rule order_trans) 260 note Skorohod 261 then obtain Omega Y_seq Y where 262 ps_Omega [simp]: "prob_space Omega" and 263 Y_seq_measurable [measurable]: "\<And>n. Y_seq n \<in> borel_measurable Omega" and 264 distr_Y_seq: "\<And>n. distr Omega borel (Y_seq n) = \<mu> n" and 265 Y_measurable [measurable]: "Y \<in> borel_measurable Omega" and 266 distr_Y: "distr Omega borel Y = M" and 267 YnY: "\<And>x :: real. x \<in> space Omega \<Longrightarrow> (\<lambda>n. Y_seq n x) \<longlonglongrightarrow> Y x" by force 268 interpret prob_space Omega by fact 269 have *: "emeasure Omega (Y -` {x. \<not> isCont f x} \<inter> space Omega) = 0" 270 by (subst emeasure_distr [symmetric, where N=borel]) (auto simp: distr_Y discont_null) 271 have *: "AE x in Omega. (\<lambda>n. f (Y_seq n x)) \<longlonglongrightarrow> f (Y x)" 272 by (rule AE_I [OF _ *]) (auto intro: isCont_tendsto_compose YnY) 273 show ?thesis 274 by (auto intro!: integral_dominated_convergence[where w="\<lambda>x. B"] 275 simp: f_bdd * integral_distr distr_Y_seq [symmetric] distr_Y [symmetric]) 276qed 277 278theorem weak_conv_imp_integral_bdd_continuous_conv: 279 fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}" 280 assumes 281 "\<And>x. isCont f x" and 282 "\<And>x. norm (f x) \<le> B" 283 shows 284 "(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f" 285 using assms 286 by (intro weak_conv_imp_bdd_ae_continuous_conv) 287 (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on) 288 289theorem weak_conv_imp_continuity_set_conv: 290 fixes f :: "real \<Rightarrow> real" 291 assumes [measurable]: "A \<in> sets borel" and "M (frontier A) = 0" 292 shows "(\<lambda>n. measure (\<mu> n) A) \<longlonglongrightarrow> measure M A" 293proof - 294 interpret M: real_distribution M by fact 295 interpret \<mu>: real_distribution "\<mu> n" for n by fact 296 297 have "(\<lambda>n. (\<integral>x. indicator A x \<partial>\<mu> n) :: real) \<longlonglongrightarrow> (\<integral>x. indicator A x \<partial>M)" 298 by (intro weak_conv_imp_bdd_ae_continuous_conv[where B=1]) 299 (auto intro: assms simp: isCont_indicator) 300 then show ?thesis 301 by simp 302qed 303 304end 305 306definition 307 cts_step :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" 308where 309 "cts_step a b x \<equiv> if x \<le> a then 1 else if x \<ge> b then 0 else (b - x) / (b - a)" 310 311lemma cts_step_uniformly_continuous: 312 assumes [arith]: "a < b" 313 shows "uniformly_continuous_on UNIV (cts_step a b)" 314 unfolding uniformly_continuous_on_def 315proof clarsimp 316 fix e :: real assume [arith]: "0 < e" 317 let ?d = "min (e * (b - a)) (b - a)" 318 have "?d > 0" 319 by (auto simp add: field_simps) 320 moreover have "dist x' x < ?d \<Longrightarrow> dist (cts_step a b x') (cts_step a b x) < e" for x x' 321 by (auto simp: dist_real_def divide_simps cts_step_def) 322 ultimately show "\<exists>d > 0. \<forall>x x'. dist x' x < d \<longrightarrow> dist (cts_step a b x') (cts_step a b x) < e" 323 by blast 324qed 325 326lemma (in real_distribution) integrable_cts_step: "a < b \<Longrightarrow> integrable M (cts_step a b)" 327 by (rule integrable_const_bound [of _ 1]) (auto simp: cts_step_def[abs_def]) 328 329lemma (in real_distribution) cdf_cts_step: 330 assumes [arith]: "x < y" 331 shows "cdf M x \<le> integral\<^sup>L M (cts_step x y)" and "integral\<^sup>L M (cts_step x y) \<le> cdf M y" 332proof - 333 have "cdf M x = integral\<^sup>L M (indicator {..x})" 334 by (simp add: cdf_def) 335 also have "\<dots> \<le> expectation (cts_step x y)" 336 by (intro integral_mono integrable_cts_step) 337 (auto simp: cts_step_def less_top[symmetric] split: split_indicator) 338 finally show "cdf M x \<le> expectation (cts_step x y)" . 339next 340 have "expectation (cts_step x y) \<le> integral\<^sup>L M (indicator {..y})" 341 by (intro integral_mono integrable_cts_step) 342 (auto simp: cts_step_def less_top[symmetric] split: split_indicator) 343 also have "\<dots> = cdf M y" 344 by (simp add: cdf_def) 345 finally show "expectation (cts_step x y) \<le> cdf M y" . 346qed 347 348context 349 fixes M_seq :: "nat \<Rightarrow> real measure" 350 and M :: "real measure" 351 assumes distr_M_seq [simp]: "\<And>n. real_distribution (M_seq n)" 352 assumes distr_M [simp]: "real_distribution M" 353begin 354 355theorem continuity_set_conv_imp_weak_conv: 356 fixes f :: "real \<Rightarrow> real" 357 assumes *: "\<And>A. A \<in> sets borel \<Longrightarrow> M (frontier A) = 0 \<Longrightarrow> (\<lambda> n. (measure (M_seq n) A)) \<longlonglongrightarrow> measure M A" 358 shows "weak_conv_m M_seq M" 359proof - 360 interpret real_distribution M by simp 361 show ?thesis 362 by (auto intro!: * simp: frontier_real_atMost isCont_cdf emeasure_eq_measure weak_conv_m_def weak_conv_def cdf_def2) 363qed 364 365theorem integral_cts_step_conv_imp_weak_conv: 366 assumes integral_conv: "\<And>x y. x < y \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step x y)) \<longlonglongrightarrow> integral\<^sup>L M (cts_step x y)" 367 shows "weak_conv_m M_seq M" 368 unfolding weak_conv_m_def weak_conv_def 369proof (clarsimp) 370 interpret real_distribution M by (rule distr_M) 371 fix x assume "isCont (cdf M) x" 372 hence left_cont: "continuous (at_left x) (cdf M)" 373 unfolding continuous_at_split .. 374 { fix y :: real assume [arith]: "x < y" 375 have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> limsup (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step x y))" 376 by (auto intro!: Limsup_mono always_eventually real_distribution.cdf_cts_step) 377 also have "\<dots> = integral\<^sup>L M (cts_step x y)" 378 by (intro lim_imp_Limsup) (auto intro: integral_conv) 379 also have "\<dots> \<le> cdf M y" 380 by (simp add: cdf_cts_step) 381 finally have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M y" . 382 } note * = this 383 { fix y :: real assume [arith]: "x > y" 384 have "cdf M y \<le> ereal (integral\<^sup>L M (cts_step y x))" 385 by (simp add: cdf_cts_step) 386 also have "\<dots> = liminf (\<lambda>n. integral\<^sup>L (M_seq n) (cts_step y x))" 387 by (intro lim_imp_Liminf[symmetric]) (auto intro: integral_conv) 388 also have "\<dots> \<le> liminf (\<lambda>n. cdf (M_seq n) x)" 389 by (auto intro!: Liminf_mono always_eventually real_distribution.cdf_cts_step) 390 finally have "liminf (\<lambda>n. cdf (M_seq n) x) \<ge> cdf M y" . 391 } note ** = this 392 393 have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M x" 394 proof (rule tendsto_lowerbound) 395 show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>xa. ereal (cdf (M_seq xa) x)) \<le> ereal (cdf M i)" 396 by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"]) 397 qed (insert cdf_is_right_cont, auto simp: continuous_within) 398 moreover have "cdf M x \<le> liminf (\<lambda>n. cdf (M_seq n) x)" 399 proof (rule tendsto_upperbound) 400 show "\<forall>\<^sub>F i in at_left x. ereal (cdf M i) \<le> liminf (\<lambda>xa. ereal (cdf (M_seq xa) x))" 401 by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"]) 402 qed (insert left_cont, auto simp: continuous_within) 403 ultimately show "(\<lambda>n. cdf (M_seq n) x) \<longlonglongrightarrow> cdf M x" 404 by (elim limsup_le_liminf_real) 405qed 406 407theorem integral_bdd_continuous_conv_imp_weak_conv: 408 assumes 409 "\<And>f. (\<And>x. isCont f x) \<Longrightarrow> (\<And>x. abs (f x) \<le> 1) \<Longrightarrow> (\<lambda>n. integral\<^sup>L (M_seq n) f::real) \<longlonglongrightarrow> integral\<^sup>L M f" 410 shows 411 "weak_conv_m M_seq M" 412 apply (rule integral_cts_step_conv_imp_weak_conv [OF assms]) 413 apply (rule continuous_on_interior) 414 apply (rule uniformly_continuous_imp_continuous) 415 apply (rule cts_step_uniformly_continuous) 416 apply (auto simp: cts_step_def) 417 done 418 419end 420 421end 422