src/HOL/Probability/Levy.thy
 author hoelzl Wed Jan 06 12:18:53 2016 +0100 (2016-01-06) changeset 62083 7582b39f51ed child 62397 5ae24f33d343 permissions -rw-r--r--
add the proof of the central limit theorem
```     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"
```
```   530       by (subst 4, rule lim_subseq [OF s], rule assms)
```
```   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'"
```
```   534       apply (elim subst)
```
```   535       by (rule nu)
```
```   536   qed
```
```   537 qed
```
```   538
```
```   539 end
```