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