author | haftmann |
Thu, 03 Mar 2016 08:33:55 +0100 | |
changeset 62499 | 4a5b81ff5992 |
parent 62397 | 5ae24f33d343 |
child 62975 | 1d066f6ab25d |
permissions | -rw-r--r-- |
62083 | 1 |
(* Theory: Levy.thy |
2 |
Author: Jeremy Avigad |
|
3 |
*) |
|
4 |
||
5 |
section \<open>The Levy inversion theorem, and the Levy continuity theorem.\<close> |
|
6 |
||
7 |
theory Levy |
|
8 |
imports Characteristic_Functions Helly_Selection Sinc_Integral |
|
9 |
begin |
|
10 |
||
11 |
lemma LIM_zero_cancel: |
|
12 |
fixes f :: "_ \<Rightarrow> 'b::real_normed_vector" |
|
13 |
shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F" |
|
14 |
unfolding tendsto_iff dist_norm by simp |
|
15 |
||
16 |
subsection \<open>The Levy inversion theorem\<close> |
|
17 |
||
18 |
(* Actually, this is not needed for us -- but it is useful for other purposes. (See Billingsley.) *) |
|
19 |
lemma Levy_Inversion_aux1: |
|
20 |
fixes a b :: real |
|
21 |
assumes "a \<le> b" |
|
22 |
shows "((\<lambda>t. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t)) \<longlongrightarrow> b - a) (at 0)" |
|
23 |
(is "(?F \<longlongrightarrow> _) (at _)") |
|
24 |
proof - |
|
25 |
have 1: "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \<noteq> 0" for t |
|
26 |
proof - |
|
27 |
have "cmod (?F t - (b - a)) = cmod ( |
|
28 |
(iexp (-(t * a)) - (1 + ii * -(t * a))) / (ii * t) - |
|
29 |
(iexp (-(t * b)) - (1 + ii * -(t * b))) / (ii * t))" |
|
30 |
(is "_ = cmod (?one / (ii * t) - ?two / (ii * t))") |
|
31 |
using `t \<noteq> 0` by (intro arg_cong[where f=norm]) (simp add: field_simps) |
|
32 |
also have "\<dots> \<le> cmod (?one / (ii * t)) + cmod (?two / (ii * t))" |
|
33 |
by (rule norm_triangle_ineq4) |
|
34 |
also have "cmod (?one / (ii * t)) = cmod ?one / abs t" |
|
35 |
by (simp add: norm_divide norm_mult) |
|
36 |
also have "cmod (?two / (ii * t)) = cmod ?two / abs t" |
|
37 |
by (simp add: norm_divide norm_mult) |
|
38 |
also have "cmod ?one / abs t + cmod ?two / abs t \<le> |
|
39 |
((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t" |
|
40 |
apply (rule add_mono) |
|
41 |
apply (rule divide_right_mono) |
|
42 |
using iexp_approx1 [of "-(t * a)" 1] apply (simp add: field_simps eval_nat_numeral) |
|
43 |
apply force |
|
44 |
apply (rule divide_right_mono) |
|
45 |
using iexp_approx1 [of "-(t * b)" 1] apply (simp add: field_simps eval_nat_numeral) |
|
46 |
by force |
|
47 |
also have "\<dots> = a^2 / 2 * abs t + b^2 / 2 * abs t" |
|
48 |
using `t \<noteq> 0` apply (case_tac "t \<ge> 0", simp add: field_simps power2_eq_square) |
|
49 |
using `t \<noteq> 0` by (subst (1 2) abs_of_neg, auto simp add: field_simps power2_eq_square) |
|
50 |
finally show "cmod (?F t - (b - a)) \<le> a^2 / 2 * abs t + b^2 / 2 * abs t" . |
|
51 |
qed |
|
52 |
show ?thesis |
|
53 |
apply (rule LIM_zero_cancel) |
|
54 |
apply (rule tendsto_norm_zero_cancel) |
|
55 |
apply (rule real_LIM_sandwich_zero [OF _ _ 1]) |
|
56 |
apply (auto intro!: tendsto_eq_intros) |
|
57 |
done |
|
58 |
qed |
|
59 |
||
60 |
lemma Levy_Inversion_aux2: |
|
61 |
fixes a b t :: real |
|
62 |
assumes "a \<le> b" and "t \<noteq> 0" |
|
63 |
shows "cmod ((iexp (t * b) - iexp (t * a)) / (ii * t)) \<le> b - a" (is "?F \<le> _") |
|
64 |
proof - |
|
65 |
have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (ii * t))" |
|
66 |
using `t \<noteq> 0` by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus) |
|
67 |
also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t" |
|
68 |
unfolding norm_divide norm_mult norm_exp_ii_times using `t \<noteq> 0` |
|
69 |
by (simp add: complex_eq_iff norm_mult) |
|
70 |
also have "\<dots> \<le> abs (t * (b - a)) / abs t" |
|
71 |
using iexp_approx1 [of "t * (b - a)" 0] |
|
72 |
by (intro divide_right_mono) (auto simp add: field_simps eval_nat_numeral) |
|
73 |
also have "\<dots> = b - a" |
|
74 |
using assms by (auto simp add: abs_mult) |
|
75 |
finally show ?thesis . |
|
76 |
qed |
|
77 |
||
78 |
(* TODO: refactor! *) |
|
79 |
theorem (in real_distribution) Levy_Inversion: |
|
80 |
fixes a b :: real |
|
81 |
assumes "a \<le> b" |
|
82 |
defines "\<mu> \<equiv> measure M" and "\<phi> \<equiv> char M" |
|
83 |
assumes "\<mu> {a} = 0" and "\<mu> {b} = 0" |
|
84 |
shows "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t) * \<phi> t)) |
|
85 |
\<longlonglongrightarrow> \<mu> {a<..b}" |
|
86 |
(is "(\<lambda>T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \<phi> t)) \<longlonglongrightarrow> of_real (\<mu> {a<..b})") |
|
87 |
proof - |
|
88 |
interpret P: pair_sigma_finite lborel M .. |
|
89 |
from bounded_Si obtain B where Bprop: "\<And>T. abs (Si T) \<le> B" by auto |
|
90 |
from Bprop [of 0] have [simp]: "B \<ge> 0" by auto |
|
91 |
let ?f = "\<lambda>t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (ii * t)" |
|
92 |
{ fix T :: real |
|
93 |
assume "T \<ge> 0" |
|
94 |
let ?f' = "\<lambda>(t, x). indicator {-T<..<T} t *\<^sub>R ?f t x" |
|
95 |
{ fix x |
|
96 |
have 1: "complex_interval_lebesgue_integrable lborel u v (\<lambda>t. ?f t x)" for u v :: real |
|
97 |
using Levy_Inversion_aux2[of "x - b" "x - a"] |
|
98 |
apply (simp add: interval_lebesgue_integrable_def del: times_divide_eq_left) |
|
99 |
apply (intro integrableI_bounded_set_indicator[where B="b - a"] conjI impI) |
|
100 |
apply (auto intro!: AE_I [of _ _ "{0}"] simp: assms) |
|
101 |
done |
|
102 |
have "(CLBINT t. ?f' (t, x)) = (CLBINT t=-T..T. ?f t x)" |
|
103 |
using `T \<ge> 0` by (simp add: interval_lebesgue_integral_def) |
|
104 |
also have "\<dots> = (CLBINT t=-T..(0 :: real). ?f t x) + (CLBINT t=(0 :: real)..T. ?f t x)" |
|
105 |
(is "_ = _ + ?t") |
|
106 |
using 1 by (intro interval_integral_sum[symmetric]) (simp add: min_absorb1 max_absorb2 \<open>T \<ge> 0\<close>) |
|
107 |
also have "(CLBINT t=-T..(0 :: real). ?f t x) = (CLBINT t=(0::real)..T. ?f (-t) x)" |
|
108 |
by (subst interval_integral_reflect) auto |
|
109 |
also have "\<dots> + ?t = (CLBINT t=(0::real)..T. ?f (-t) x + ?f t x)" |
|
110 |
using 1 |
|
111 |
by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all |
|
112 |
also have "\<dots> = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) - |
|
113 |
(iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (ii * t))" |
|
114 |
using `T \<ge> 0` by (intro interval_integral_cong) (auto simp add: divide_simps) |
|
115 |
also have "\<dots> = (CLBINT t=(0::real)..T. complex_of_real( |
|
116 |
2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))" |
|
117 |
using `T \<ge> 0` |
|
118 |
apply (intro interval_integral_cong) |
|
119 |
apply (simp add: field_simps cis.ctr Im_divide Re_divide Im_exp Re_exp complex_eq_iff) |
|
120 |
unfolding minus_diff_eq[symmetric, of "y * x" "y * a" for y a] sin_minus cos_minus |
|
121 |
apply (simp add: field_simps power2_eq_square) |
|
122 |
done |
|
123 |
also have "\<dots> = complex_of_real (LBINT t=(0::real)..T. |
|
124 |
2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t))" |
|
125 |
by (rule interval_lebesgue_integral_of_real) |
|
126 |
also have "\<dots> = complex_of_real (2 * (sgn (x - a) * Si (T * abs (x - a)) - |
|
127 |
sgn (x - b) * Si (T * abs (x - b))))" |
|
128 |
apply (subst interval_lebesgue_integral_diff) |
|
129 |
apply (rule interval_lebesgue_integrable_mult_right, rule integrable_sinc')+ |
|
130 |
apply (subst interval_lebesgue_integral_mult_right)+ |
|
131 |
apply (simp add: zero_ereal_def[symmetric] LBINT_I0c_sin_scale_divide[OF `T \<ge> 0`]) |
|
132 |
done |
|
133 |
finally have "(CLBINT t. ?f' (t, x)) = |
|
134 |
2 * (sgn (x - a) * Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))" . |
|
135 |
} note main_eq = this |
|
136 |
have "(CLBINT t=-T..T. ?F t * \<phi> t) = |
|
137 |
(CLBINT t. (CLINT x | M. ?F t * iexp (t * x) * indicator {-T<..<T} t))" |
|
138 |
using `T \<ge> 0` unfolding \<phi>_def char_def interval_lebesgue_integral_def |
|
139 |
by (auto split: split_indicator intro!: integral_cong) |
|
140 |
also have "\<dots> = (CLBINT t. (CLINT x | M. ?f' (t, x)))" |
|
141 |
by (auto intro!: integral_cong simp: field_simps exp_diff exp_minus split: split_indicator) |
|
142 |
also have "\<dots> = (CLINT x | M. (CLBINT t. ?f' (t, x)))" |
|
143 |
proof (intro P.Fubini_integral [symmetric] integrableI_bounded_set [where B="b - a"]) |
|
144 |
show "emeasure (lborel \<Otimes>\<^sub>M M) ({- T<..<T} \<times> space M) < \<infinity>" |
|
145 |
using \<open>T \<ge> 0\<close> by (subst emeasure_pair_measure_Times) auto |
|
146 |
show "AE x\<in>{- T<..<T} \<times> space M in lborel \<Otimes>\<^sub>M M. cmod (case x of (t, x) \<Rightarrow> ?f' (t, x)) \<le> b - a" |
|
147 |
using Levy_Inversion_aux2[of "x - b" "x - a" for x] `a \<le> b` |
|
148 |
by (intro AE_I [of _ _ "{0} \<times> UNIV"]) (force simp: emeasure_pair_measure_Times)+ |
|
149 |
qed (auto split: split_indicator split_indicator_asm) |
|
150 |
also have "\<dots> = (CLINT x | M. (complex_of_real (2 * (sgn (x - a) * |
|
151 |
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))))" |
|
152 |
using main_eq by (intro integral_cong, auto) |
|
153 |
also have "\<dots> = complex_of_real (LINT x | M. (2 * (sgn (x - a) * |
|
154 |
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" |
|
155 |
by (rule integral_complex_of_real) |
|
156 |
finally have "(CLBINT t=-T..T. ?F t * \<phi> t) = |
|
157 |
complex_of_real (LINT x | M. (2 * (sgn (x - a) * |
|
158 |
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b)))))" . |
|
159 |
} note main_eq2 = this |
|
160 |
||
161 |
have "(\<lambda>T :: nat. LINT x | M. (2 * (sgn (x - a) * |
|
162 |
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow> |
|
163 |
(LINT x | M. 2 * pi * indicator {a<..b} x)" |
|
164 |
proof (rule integral_dominated_convergence [where w="\<lambda>x. 4 * B"]) |
|
165 |
show "integrable M (\<lambda>x. 4 * B)" |
|
166 |
by (rule integrable_const_bound [of _ "4 * B"]) auto |
|
167 |
next |
|
168 |
let ?S = "\<lambda>n::nat. \<lambda>x. sgn (x - a) * Si (n * \<bar>x - a\<bar>) - sgn (x - b) * Si (n * \<bar>x - b\<bar>)" |
|
169 |
{ fix n x |
|
170 |
have "norm (?S n x) \<le> norm (sgn (x - a) * Si (n * \<bar>x - a\<bar>)) + norm (sgn (x - b) * Si (n * \<bar>x - b\<bar>))" |
|
171 |
by (rule norm_triangle_ineq4) |
|
172 |
also have "\<dots> \<le> B + B" |
|
173 |
using Bprop by (intro add_mono) (auto simp: abs_mult abs_sgn_eq) |
|
174 |
finally have "norm (2 * ?S n x) \<le> 4 * B" |
|
175 |
by simp } |
|
176 |
then show "\<And>n. AE x in M. norm (2 * ?S n x) \<le> 4 * B" |
|
177 |
by auto |
|
178 |
have "AE x in M. x \<noteq> a" "AE x in M. x \<noteq> b" |
|
179 |
using prob_eq_0[of "{a}"] prob_eq_0[of "{b}"] `\<mu> {a} = 0` `\<mu> {b} = 0` by (auto simp: \<mu>_def) |
|
180 |
then show "AE x in M. (\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x" |
|
181 |
proof eventually_elim |
|
182 |
fix x assume x: "x \<noteq> a" "x \<noteq> b" |
|
183 |
then have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n))) |
|
184 |
\<longlonglongrightarrow> 2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2))" |
|
185 |
by (intro tendsto_intros filterlim_compose[OF Si_at_top] |
|
186 |
filterlim_tendsto_pos_mult_at_top[OF tendsto_const] filterlim_real_sequentially) |
|
187 |
auto |
|
188 |
also have "(\<lambda>n. 2 * (sgn (x - a) * Si (\<bar>x - a\<bar> * n) - sgn (x - b) * Si (\<bar>x - b\<bar> * n))) = (\<lambda>n. 2 * ?S n x)" |
|
189 |
by (auto simp: ac_simps) |
|
190 |
also have "2 * (sgn (x - a) * (pi / 2) - sgn (x - b) * (pi / 2)) = 2 * pi * indicator {a<..b} x" |
|
191 |
using x `a \<le> b` by (auto split: split_indicator) |
|
192 |
finally show "(\<lambda>n. 2 * ?S n x) \<longlonglongrightarrow> 2 * pi * indicator {a<..b} x" . |
|
193 |
qed |
|
194 |
qed simp_all |
|
195 |
also have "(LINT x | M. 2 * pi * indicator {a<..b} x) = 2 * pi * \<mu> {a<..b}" |
|
196 |
by (simp add: \<mu>_def) |
|
197 |
finally have "(\<lambda>T. LINT x | M. (2 * (sgn (x - a) * |
|
198 |
Si (T * abs (x - a)) - sgn (x - b) * Si (T * abs (x - b))))) \<longlonglongrightarrow> |
|
199 |
2 * pi * \<mu> {a<..b}" . |
|
200 |
with main_eq2 show ?thesis |
|
201 |
by (auto intro!: tendsto_eq_intros) |
|
202 |
qed |
|
203 |
||
204 |
theorem Levy_uniqueness: |
|
205 |
fixes M1 M2 :: "real measure" |
|
206 |
assumes "real_distribution M1" "real_distribution M2" and |
|
207 |
"char M1 = char M2" |
|
208 |
shows "M1 = M2" |
|
209 |
proof - |
|
210 |
interpret M1: real_distribution M1 by (rule assms) |
|
211 |
interpret M2: real_distribution M2 by (rule assms) |
|
212 |
have "countable ({x. measure M1 {x} \<noteq> 0} \<union> {x. measure M2 {x} \<noteq> 0})" |
|
213 |
by (intro countable_Un M2.countable_support M1.countable_support) |
|
214 |
then have count: "countable {x. measure M1 {x} \<noteq> 0 \<or> measure M2 {x} \<noteq> 0}" |
|
215 |
by (simp add: Un_def) |
|
216 |
||
217 |
have "cdf M1 = cdf M2" |
|
218 |
proof (rule ext) |
|
219 |
fix x |
|
220 |
from M1.cdf_is_right_cont [of x] have "(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)" |
|
221 |
by (simp add: continuous_within) |
|
222 |
from M2.cdf_is_right_cont [of x] have "(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)" |
|
223 |
by (simp add: continuous_within) |
|
224 |
||
225 |
{ fix \<epsilon> :: real |
|
226 |
assume "\<epsilon> > 0" |
|
227 |
from `\<epsilon> > 0` `(cdf M1 \<longlongrightarrow> 0) at_bot` `(cdf M2 \<longlongrightarrow> 0) at_bot` |
|
228 |
have "eventually (\<lambda>y. \<bar>cdf M1 y\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y\<bar> < \<epsilon> / 4 \<and> y \<le> x) at_bot" |
|
229 |
by (simp only: tendsto_iff dist_real_def diff_0_right eventually_conj eventually_le_at_bot) |
|
230 |
then obtain M where "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M1 y\<bar> < \<epsilon> / 4" "\<And>y. y \<le> M \<Longrightarrow> \<bar>cdf M2 y\<bar> < \<epsilon> / 4" "M \<le> x" |
|
231 |
unfolding eventually_at_bot_linorder by auto |
|
232 |
with open_minus_countable[OF count, of "{..< M}"] obtain a where |
|
233 |
"measure M1 {a} = 0" "measure M2 {a} = 0" "a < M" "a \<le> x" "\<bar>cdf M1 a\<bar> < \<epsilon> / 4" "\<bar>cdf M2 a\<bar> < \<epsilon> / 4" |
|
234 |
by auto |
|
235 |
||
236 |
from `\<epsilon> > 0` `(cdf M1 \<longlongrightarrow> cdf M1 x) (at_right x)` `(cdf M2 \<longlongrightarrow> cdf M2 x) (at_right x)` |
|
237 |
have "eventually (\<lambda>y. \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4 \<and> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4 \<and> x < y) (at_right x)" |
|
238 |
by (simp only: tendsto_iff dist_real_def eventually_conj eventually_at_right_less) |
|
239 |
then obtain N where "N > x" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M1 y - cdf M1 x\<bar> < \<epsilon> / 4" |
|
240 |
"\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> \<bar>cdf M2 y - cdf M2 x\<bar> < \<epsilon> / 4" "\<And>y. x < y \<Longrightarrow> y < N \<Longrightarrow> x < y" |
|
241 |
by (auto simp add: eventually_at_right[OF less_add_one]) |
|
242 |
with open_minus_countable[OF count, of "{x <..< N}"] obtain b where "x < b" "b < N" |
|
243 |
"measure M1 {b} = 0" "measure M2 {b} = 0" "\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4" "\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4" |
|
244 |
by (auto simp: abs_minus_commute) |
|
245 |
from `a \<le> x` `x < b` have "a < b" "a \<le> b" by auto |
|
246 |
||
247 |
from `char M1 = char M2` |
|
248 |
M1.Levy_Inversion [OF `a \<le> b` `measure M1 {a} = 0` `measure M1 {b} = 0`] |
|
249 |
M2.Levy_Inversion [OF `a \<le> b` `measure M2 {a} = 0` `measure M2 {b} = 0`] |
|
250 |
have "complex_of_real (measure M1 {a<..b}) = complex_of_real (measure M2 {a<..b})" |
|
251 |
by (intro LIMSEQ_unique) auto |
|
252 |
then have "measure M1 {a<..b} = measure M2 {a<..b}" by auto |
|
253 |
then have *: "cdf M1 b - cdf M1 a = cdf M2 b - cdf M2 a" |
|
254 |
unfolding M1.cdf_diff_eq [OF `a < b`] M2.cdf_diff_eq [OF `a < b`] . |
|
255 |
||
256 |
have "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) = abs (cdf M1 x - cdf M1 b + cdf M1 a)" |
|
257 |
by simp |
|
258 |
also have "\<dots> \<le> abs (cdf M1 x - cdf M1 b) + abs (cdf M1 a)" |
|
259 |
by (rule abs_triangle_ineq) |
|
260 |
also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4" |
|
261 |
by (intro add_mono less_imp_le \<open>\<bar>cdf M1 a\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M1 x - cdf M1 b\<bar> < \<epsilon> / 4\<close>) |
|
262 |
finally have 1: "abs (cdf M1 x - (cdf M1 b - cdf M1 a)) \<le> \<epsilon> / 2" by simp |
|
263 |
||
264 |
have "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) = abs (cdf M2 x - cdf M2 b + cdf M2 a)" |
|
265 |
by simp |
|
266 |
also have "\<dots> \<le> abs (cdf M2 x - cdf M2 b) + abs (cdf M2 a)" |
|
267 |
by (rule abs_triangle_ineq) |
|
268 |
also have "\<dots> \<le> \<epsilon> / 4 + \<epsilon> / 4" |
|
269 |
by (intro add_mono less_imp_le \<open>\<bar>cdf M2 x - cdf M2 b\<bar> < \<epsilon> / 4\<close> \<open>\<bar>cdf M2 a\<bar> < \<epsilon> / 4\<close>) |
|
270 |
finally have 2: "abs (cdf M2 x - (cdf M2 b - cdf M2 a)) \<le> \<epsilon> / 2" by simp |
|
271 |
||
272 |
have "abs (cdf M1 x - cdf M2 x) = abs ((cdf M1 x - (cdf M1 b - cdf M1 a)) - |
|
273 |
(cdf M2 x - (cdf M2 b - cdf M2 a)))" by (subst *, simp) |
|
274 |
also have "\<dots> \<le> abs (cdf M1 x - (cdf M1 b - cdf M1 a)) + |
|
275 |
abs (cdf M2 x - (cdf M2 b - cdf M2 a))" by (rule abs_triangle_ineq4) |
|
276 |
also have "\<dots> \<le> \<epsilon> / 2 + \<epsilon> / 2" by (rule add_mono [OF 1 2]) |
|
277 |
finally have "abs (cdf M1 x - cdf M2 x) \<le> \<epsilon>" by simp } |
|
278 |
then show "cdf M1 x = cdf M2 x" |
|
279 |
by (metis abs_le_zero_iff dense_ge eq_iff_diff_eq_0) |
|
280 |
qed |
|
281 |
thus ?thesis |
|
282 |
by (rule cdf_unique [OF `real_distribution M1` `real_distribution M2`]) |
|
283 |
qed |
|
284 |
||
285 |
||
286 |
subsection \<open>The Levy continuity theorem\<close> |
|
287 |
||
288 |
theorem levy_continuity1: |
|
289 |
fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure" |
|
290 |
assumes "\<And>n. real_distribution (M n)" "real_distribution M'" "weak_conv_m M M'" |
|
291 |
shows "(\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t" |
|
292 |
unfolding char_def using assms by (rule weak_conv_imp_integral_bdd_continuous_conv) auto |
|
293 |
||
294 |
theorem levy_continuity: |
|
295 |
fixes M :: "nat \<Rightarrow> real measure" and M' :: "real measure" |
|
296 |
assumes real_distr_M : "\<And>n. real_distribution (M n)" |
|
297 |
and real_distr_M': "real_distribution M'" |
|
298 |
and char_conv: "\<And>t. (\<lambda>n. char (M n) t) \<longlonglongrightarrow> char M' t" |
|
299 |
shows "weak_conv_m M M'" |
|
300 |
proof - |
|
301 |
interpret Mn: real_distribution "M n" for n by fact |
|
302 |
interpret M': real_distribution M' by fact |
|
303 |
||
304 |
have *: "\<And>u x. u > 0 \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (CLBINT t:{-u..u}. 1 - iexp (t * x)) = |
|
305 |
2 * (u - sin (u * x) / x)" |
|
306 |
proof - |
|
307 |
fix u :: real and x :: real |
|
308 |
assume "u > 0" and "x \<noteq> 0" |
|
309 |
hence "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = (CLBINT t=-u..u. 1 - iexp (t * x))" |
|
310 |
by (subst interval_integral_Icc, auto) |
|
311 |
also have "\<dots> = (CLBINT t=-u..0. 1 - iexp (t * x)) + (CLBINT t=0..u. 1 - iexp (t * x))" |
|
312 |
using `u > 0` |
|
313 |
apply (subst interval_integral_sum) |
|
314 |
apply (simp add: min_absorb1 min_absorb2 max_absorb1 max_absorb2) |
|
315 |
apply (rule interval_integrable_isCont) |
|
316 |
apply auto |
|
317 |
done |
|
318 |
also have "\<dots> = (CLBINT t=ereal 0..u. 1 - iexp (t * -x)) + (CLBINT t=ereal 0..u. 1 - iexp (t * x))" |
|
319 |
apply (subgoal_tac "0 = ereal 0", erule ssubst) |
|
320 |
by (subst interval_integral_reflect, auto) |
|
321 |
also have "\<dots> = (LBINT t=ereal 0..u. 2 - 2 * cos (t * x))" |
|
322 |
apply (subst interval_lebesgue_integral_add (2) [symmetric]) |
|
323 |
apply ((rule interval_integrable_isCont, auto)+) [2] |
|
324 |
unfolding exp_Euler cos_of_real |
|
325 |
apply (simp add: of_real_mult interval_lebesgue_integral_of_real[symmetric]) |
|
326 |
done |
|
327 |
also have "\<dots> = 2 * u - 2 * sin (u * x) / x" |
|
328 |
by (subst interval_lebesgue_integral_diff) |
|
329 |
(auto intro!: interval_integrable_isCont |
|
330 |
simp: interval_lebesgue_integral_of_real integral_cos [OF `x \<noteq> 0`] mult.commute[of _ x]) |
|
331 |
finally show "(CLBINT t:{-u..u}. 1 - iexp (t * x)) = 2 * (u - sin (u * x) / x)" |
|
332 |
by (simp add: field_simps) |
|
333 |
qed |
|
334 |
have main_bound: "\<And>u n. u > 0 \<Longrightarrow> Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> |
|
335 |
u * measure (M n) {x. abs x \<ge> 2 / u}" |
|
336 |
proof - |
|
337 |
fix u :: real and n |
|
338 |
assume "u > 0" |
|
339 |
interpret P: pair_sigma_finite "M n" lborel .. |
|
340 |
(* TODO: put this in the real_distribution locale as a simp rule? *) |
|
341 |
have Mn1 [simp]: "measure (M n) UNIV = 1" by (metis Mn.prob_space Mn.space_eq_univ) |
|
342 |
(* TODO: make this automatic somehow? *) |
|
343 |
have Mn2 [simp]: "\<And>x. complex_integrable (M n) (\<lambda>t. exp (\<i> * complex_of_real (x * t)))" |
|
344 |
by (rule Mn.integrable_const_bound [where B = 1], auto) |
|
345 |
have Mn3: "set_integrable (M n \<Otimes>\<^sub>M lborel) (UNIV \<times> {- u..u}) (\<lambda>a. 1 - exp (\<i> * complex_of_real (snd a * fst a)))" |
|
346 |
using `0 < u` |
|
347 |
by (intro integrableI_bounded_set_indicator [where B="2"]) |
|
348 |
(auto simp: lborel.emeasure_pair_measure_Times split: split_indicator |
|
349 |
intro!: order_trans [OF norm_triangle_ineq4]) |
|
350 |
have "(CLBINT t:{-u..u}. 1 - char (M n) t) = |
|
351 |
(CLBINT t:{-u..u}. (CLINT x | M n. 1 - iexp (t * x)))" |
|
352 |
unfolding char_def by (rule set_lebesgue_integral_cong, auto simp del: of_real_mult) |
|
353 |
also have "\<dots> = (CLBINT t. (CLINT x | M n. indicator {-u..u} t *\<^sub>R (1 - iexp (t * x))))" |
|
354 |
by (rule integral_cong) (auto split: split_indicator) |
|
355 |
also have "\<dots> = (CLINT x | M n. (CLBINT t:{-u..u}. 1 - iexp (t * x)))" |
|
356 |
using Mn3 by (subst P.Fubini_integral) (auto simp: indicator_times split_beta') |
|
357 |
also have "\<dots> = (CLINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" |
|
358 |
using `u > 0` by (intro integral_cong, auto simp add: * simp del: of_real_mult) |
|
359 |
also have "\<dots> = (LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" |
|
360 |
by (rule integral_complex_of_real) |
|
361 |
finally have "Re (CLBINT t:{-u..u}. 1 - char (M n) t) = |
|
362 |
(LINT x | M n. (if x = 0 then 0 else 2 * (u - sin (u * x) / x)))" by simp |
|
363 |
also have "\<dots> \<ge> (LINT x : {x. abs x \<ge> 2 / u} | M n. u)" |
|
364 |
proof - |
|
365 |
have "complex_integrable (M n) (\<lambda>x. CLBINT t:{-u..u}. 1 - iexp (snd (x, t) * fst (x, t)))" |
|
366 |
using Mn3 by (intro P.integrable_fst) (simp add: indicator_times split_beta') |
|
367 |
hence "complex_integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))" |
|
368 |
using `u > 0` by (subst integrable_cong) (auto simp add: * simp del: of_real_mult) |
|
369 |
hence **: "integrable (M n) (\<lambda>x. if x = 0 then 0 else 2 * (u - sin (u * x) / x))" |
|
370 |
unfolding complex_of_real_integrable_eq . |
|
371 |
have "2 * sin x \<le> x" if "2 \<le> x" for x :: real |
|
372 |
by (rule order_trans[OF _ \<open>2 \<le> x\<close>]) auto |
|
373 |
moreover have "x \<le> 2 * sin x" if "x \<le> - 2" for x :: real |
|
374 |
by (rule order_trans[OF \<open>x \<le> - 2\<close>]) auto |
|
375 |
moreover have "x < 0 \<Longrightarrow> x \<le> sin x" for x :: real |
|
376 |
using sin_x_le_x[of "-x"] by simp |
|
377 |
ultimately show ?thesis |
|
378 |
using `u > 0` |
|
379 |
by (intro integral_mono [OF _ **]) |
|
380 |
(auto simp: divide_simps sin_x_le_x mult.commute[of u] mult_neg_pos split: split_indicator) |
|
381 |
qed |
|
382 |
also (xtrans) have "(LINT x : {x. abs x \<ge> 2 / u} | M n. u) = |
|
383 |
u * measure (M n) {x. abs x \<ge> 2 / u}" |
|
384 |
by (simp add: Mn.emeasure_eq_measure) |
|
385 |
finally show "Re (CLBINT t:{-u..u}. 1 - char (M n) t) \<ge> u * measure (M n) {x. abs x \<ge> 2 / u}" . |
|
386 |
qed |
|
387 |
||
388 |
have tight_aux: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})" |
|
389 |
proof - |
|
390 |
fix \<epsilon> :: real |
|
391 |
assume "\<epsilon> > 0" |
|
392 |
note M'.isCont_char [of 0] |
|
393 |
hence "\<exists>d>0. \<forall>t. abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4" |
|
394 |
apply (subst (asm) continuous_at_eps_delta) |
|
395 |
apply (drule_tac x = "\<epsilon> / 4" in spec) |
|
396 |
using `\<epsilon> > 0` by (auto simp add: dist_real_def dist_complex_def M'.char_zero) |
|
397 |
then obtain d where "d > 0 \<and> (\<forall>t. (abs t < d \<longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4))" .. |
|
398 |
hence d0: "d > 0" and d1: "\<And>t. abs t < d \<Longrightarrow> cmod (char M' t - 1) < \<epsilon> / 4" by auto |
|
399 |
have 1: "\<And>x. cmod (1 - char M' x) \<le> 2" |
|
400 |
by (rule order_trans [OF norm_triangle_ineq4], auto simp add: M'.cmod_char_le_1) |
|
401 |
then have 2: "\<And>u v. complex_set_integrable lborel {u..v} (\<lambda>x. 1 - char M' x)" |
|
402 |
by (intro integrableI_bounded_set_indicator[where B=2]) (auto simp: emeasure_lborel_Icc_eq) |
|
403 |
have 3: "\<And>u v. set_integrable lborel {u..v} (\<lambda>x. cmod (1 - char M' x))" |
|
404 |
by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on |
|
405 |
continuous_intros ballI M'.isCont_char continuous_intros) |
|
406 |
have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)" |
|
407 |
using integral_norm_bound[OF 2] by simp |
|
408 |
also have "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4" |
|
409 |
apply (rule integral_mono [OF 3]) |
|
410 |
apply (simp add: emeasure_lborel_Icc_eq) |
|
411 |
apply (case_tac "x \<in> {-d/2..d/2}", auto) |
|
412 |
apply (subst norm_minus_commute) |
|
413 |
apply (rule less_imp_le) |
|
414 |
apply (rule d1 [simplified]) |
|
415 |
using d0 by auto |
|
416 |
also with d0 have "\<dots> = d * \<epsilon> / 4" |
|
417 |
by simp |
|
418 |
finally have bound: "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> d * \<epsilon> / 4" . |
|
419 |
{ fix n x |
|
420 |
have "cmod (1 - char (M n) x) \<le> 2" |
|
421 |
by (rule order_trans [OF norm_triangle_ineq4], auto simp add: Mn.cmod_char_le_1) |
|
422 |
} note bd1 = this |
|
423 |
have "(\<lambda>n. CLBINT t:{-d/2..d/2}. 1 - char (M n) t) \<longlonglongrightarrow> (CLBINT t:{-d/2..d/2}. 1 - char M' t)" |
|
424 |
using bd1 |
|
425 |
apply (intro integral_dominated_convergence[where w="\<lambda>x. indicator {-d/2..d/2} x *\<^sub>R 2"]) |
|
426 |
apply (auto intro!: char_conv tendsto_intros |
|
427 |
simp: emeasure_lborel_Icc_eq |
|
428 |
split: split_indicator) |
|
429 |
done |
|
430 |
hence "eventually (\<lambda>n. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - |
|
431 |
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4) sequentially" |
|
432 |
using d0 `\<epsilon> > 0` apply (subst (asm) tendsto_iff) |
|
433 |
by (subst (asm) dist_complex_def, drule spec, erule mp, auto) |
|
434 |
hence "\<exists>N. \<forall>n \<ge> N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - |
|
435 |
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by (simp add: eventually_sequentially) |
|
436 |
then guess N .. |
|
437 |
hence N: "\<And>n. n \<ge> N \<Longrightarrow> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - |
|
438 |
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by auto |
|
439 |
{ fix n |
|
440 |
assume "n \<ge> N" |
|
441 |
have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) = |
|
442 |
cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - (CLBINT t:{-d/2..d/2}. 1 - char M' t) |
|
443 |
+ (CLBINT t:{-d/2..d/2}. 1 - char M' t))" by simp |
|
444 |
also have "\<dots> \<le> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) - |
|
445 |
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) + cmod(CLBINT t:{-d/2..d/2}. 1 - char M' t)" |
|
446 |
by (rule norm_triangle_ineq) |
|
447 |
also have "\<dots> < d * \<epsilon> / 4 + d * \<epsilon> / 4" |
|
448 |
by (rule add_less_le_mono [OF N [OF `n \<ge> N`] bound]) |
|
449 |
also have "\<dots> = d * \<epsilon> / 2" by auto |
|
450 |
finally have "cmod (CLBINT t:{-d/2..d/2}. 1 - char (M n) t) < d * \<epsilon> / 2" . |
|
451 |
hence "d * \<epsilon> / 2 > Re (CLBINT t:{-d/2..d/2}. 1 - char (M n) t)" |
|
452 |
by (rule order_le_less_trans [OF complex_Re_le_cmod]) |
|
453 |
hence "d * \<epsilon> / 2 > Re (CLBINT t:{-(d/2)..d/2}. 1 - char (M n) t)" (is "_ > ?lhs") by simp |
|
454 |
also have "?lhs \<ge> (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}" |
|
455 |
using d0 by (intro main_bound, simp) |
|
456 |
finally (xtrans) have "d * \<epsilon> / 2 > (d / 2) * measure (M n) {x. abs x \<ge> 2 / (d / 2)}" . |
|
457 |
with d0 `\<epsilon> > 0` have "\<epsilon> > measure (M n) {x. abs x \<ge> 2 / (d / 2)}" by (simp add: field_simps) |
|
458 |
hence "\<epsilon> > 1 - measure (M n) (UNIV - {x. abs x \<ge> 2 / (d / 2)})" |
|
459 |
apply (subst Mn.borel_UNIV [symmetric]) |
|
460 |
by (subst Mn.prob_compl, auto) |
|
461 |
also have "UNIV - {x. abs x \<ge> 2 / (d / 2)} = {x. -(4 / d) < x \<and> x < (4 / d)}" |
|
462 |
using d0 apply (auto simp add: field_simps) |
|
463 |
(* very annoying -- this should be automatic *) |
|
464 |
apply (case_tac "x \<ge> 0", auto simp add: field_simps) |
|
465 |
apply (subgoal_tac "0 \<le> x * d", arith, rule mult_nonneg_nonneg, auto) |
|
466 |
apply (case_tac "x \<ge> 0", auto simp add: field_simps) |
|
467 |
apply (subgoal_tac "x * d \<le> 0", arith) |
|
468 |
apply (rule mult_nonpos_nonneg, auto) |
|
469 |
by (case_tac "x \<ge> 0", auto simp add: field_simps) |
|
470 |
finally have "measure (M n) {x. -(4 / d) < x \<and> x < (4 / d)} > 1 - \<epsilon>" |
|
471 |
by auto |
|
472 |
} note 6 = this |
|
473 |
{ fix n :: nat |
|
474 |
have *: "(UN (k :: nat). {- real k<..real k}) = UNIV" |
|
475 |
by (auto, metis leI le_less_trans less_imp_le minus_less_iff reals_Archimedean2) |
|
476 |
have "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow> |
|
477 |
measure (M n) (UN (k :: nat). {- real k<..real k})" |
|
478 |
by (rule Mn.finite_Lim_measure_incseq, auto simp add: incseq_def) |
|
479 |
hence "(\<lambda>k. measure (M n) {- real k<..real k}) \<longlonglongrightarrow> 1" |
|
480 |
using Mn.prob_space unfolding * Mn.borel_UNIV by simp |
|
481 |
hence "eventually (\<lambda>k. measure (M n) {- real k<..real k} > 1 - \<epsilon>) sequentially" |
|
482 |
apply (elim order_tendstoD (1)) |
|
483 |
using `\<epsilon> > 0` by auto |
|
484 |
} note 7 = this |
|
485 |
{ fix n :: nat |
|
486 |
have "eventually (\<lambda>k. \<forall>m < n. measure (M m) {- real k<..real k} > 1 - \<epsilon>) sequentially" |
|
487 |
(is "?P n") |
|
488 |
proof (induct n) |
|
489 |
case (Suc n) with 7[of n] show ?case |
|
490 |
by eventually_elim (auto simp add: less_Suc_eq) |
|
491 |
qed simp |
|
492 |
} note 8 = this |
|
493 |
from 8 [of N] have "\<exists>K :: nat. \<forall>k \<ge> K. \<forall>m<N. 1 - \<epsilon> < |
|
494 |
Sigma_Algebra.measure (M m) {- real k<..real k}" |
|
495 |
by (auto simp add: eventually_sequentially) |
|
496 |
hence "\<exists>K :: nat. \<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" by auto |
|
497 |
then obtain K :: nat where |
|
498 |
"\<forall>m<N. 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" .. |
|
499 |
hence K: "\<And>m. m < N \<Longrightarrow> 1 - \<epsilon> < Sigma_Algebra.measure (M m) {- real K<..real K}" |
|
500 |
by auto |
|
501 |
let ?K' = "max K (4 / d)" |
|
502 |
have "-?K' < ?K' \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {-?K'<..?K'})" |
|
503 |
using d0 apply auto |
|
504 |
apply (rule max.strict_coboundedI2, auto) |
|
505 |
proof - |
|
506 |
fix n |
|
507 |
show " 1 - \<epsilon> < measure (M n) {- max (real K) (4 / d)<..max (real K) (4 / d)}" |
|
508 |
apply (case_tac "n < N") |
|
509 |
apply (rule order_less_le_trans) |
|
510 |
apply (erule K) |
|
511 |
apply (rule Mn.finite_measure_mono, auto) |
|
512 |
apply (rule order_less_le_trans) |
|
513 |
apply (rule 6, erule leI) |
|
514 |
by (rule Mn.finite_measure_mono, auto) |
|
515 |
qed |
|
516 |
thus "\<exists>a b. a < b \<and> (\<forall>n. 1 - \<epsilon> < measure (M n) {a<..b})" by (intro exI) |
|
517 |
qed |
|
518 |
have tight: "tight M" |
|
519 |
by (auto simp: tight_def intro: assms tight_aux) |
|
520 |
show ?thesis |
|
521 |
proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight]) |
|
522 |
fix s \<nu> |
|
523 |
assume s: "subseq s" |
|
524 |
assume nu: "weak_conv_m (M \<circ> s) \<nu>" |
|
525 |
assume *: "real_distribution \<nu>" |
|
526 |
have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms) |
|
527 |
have 3: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char \<nu> t" by (intro levy_continuity1 [OF 2 * nu]) |
|
528 |
have 4: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) = ((\<lambda>n. char (M n) t) \<circ> s)" by (rule ext, simp) |
|
529 |
have 5: "\<And>t. (\<lambda>n. char ((M \<circ> s) n) t) \<longlonglongrightarrow> char M' t" |
|
62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62083
diff
changeset
|
530 |
by (subst 4, rule LIMSEQ_subseq_LIMSEQ [OF _ s], rule assms) |
62083 | 531 |
hence "char \<nu> = char M'" by (intro ext, intro LIMSEQ_unique [OF 3 5]) |
532 |
hence "\<nu> = M'" by (rule Levy_uniqueness [OF * `real_distribution M'`]) |
|
533 |
thus "weak_conv_m (M \<circ> s) M'" |
|
62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62083
diff
changeset
|
534 |
by (elim subst) (rule nu) |
62083 | 535 |
qed |
536 |
qed |
|
537 |
||
538 |
end |