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