src/HOL/Probability/Characteristic_Functions.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62083 7582b39f51ed
child 63040 eb4ddd18d635
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
hoelzl@62083
     1
(*
hoelzl@62083
     2
  Theory: Characteristic_Functions.thy
hoelzl@62083
     3
  Authors: Jeremy Avigad, Luke Serafin
hoelzl@62083
     4
*)
hoelzl@62083
     5
hoelzl@62083
     6
section \<open>Characteristic Functions\<close>
hoelzl@62083
     7
hoelzl@62083
     8
theory Characteristic_Functions
hoelzl@62083
     9
  imports Weak_Convergence Interval_Integral Independent_Family Distributions
hoelzl@62083
    10
begin
hoelzl@62083
    11
hoelzl@62083
    12
lemma mult_min_right: "a \<ge> 0 \<Longrightarrow> (a :: real) * min b c = min (a * b) (a * c)"
hoelzl@62083
    13
  by (metis min.absorb_iff2 min_def mult_left_mono)
hoelzl@62083
    14
hoelzl@62083
    15
lemma sequentially_even_odd:
hoelzl@62083
    16
  assumes E: "eventually (\<lambda>n. P (2 * n)) sequentially" and O: "eventually (\<lambda>n. P (2 * n + 1)) sequentially"
hoelzl@62083
    17
  shows "eventually P sequentially"
hoelzl@62083
    18
proof -
hoelzl@62083
    19
  from E obtain n_e where [intro]: "\<And>n. n \<ge> n_e \<Longrightarrow> P (2 * n)"
hoelzl@62083
    20
    by (auto simp: eventually_sequentially)
hoelzl@62083
    21
  moreover
hoelzl@62083
    22
  from O obtain n_o where [intro]: "\<And>n. n \<ge> n_o \<Longrightarrow> P (Suc (2 * n))"
hoelzl@62083
    23
    by (auto simp: eventually_sequentially)
hoelzl@62083
    24
  show ?thesis
hoelzl@62083
    25
    unfolding eventually_sequentially
hoelzl@62083
    26
  proof (intro exI allI impI)
hoelzl@62083
    27
    fix n assume "max (2 * n_e) (2 * n_o + 1) \<le> n" then show "P n"
hoelzl@62083
    28
      by (cases "even n") (auto elim!: evenE oddE )
hoelzl@62083
    29
  qed
hoelzl@62083
    30
qed
hoelzl@62083
    31
hoelzl@62083
    32
lemma limseq_even_odd: 
hoelzl@62083
    33
  assumes "(\<lambda>n. f (2 * n)) \<longlonglongrightarrow> (l :: 'a :: topological_space)"
hoelzl@62083
    34
      and "(\<lambda>n. f (2 * n + 1)) \<longlonglongrightarrow> l"
hoelzl@62083
    35
  shows "f \<longlonglongrightarrow> l"
hoelzl@62083
    36
  using assms by (auto simp: filterlim_iff intro: sequentially_even_odd)
hoelzl@62083
    37
hoelzl@62083
    38
subsection \<open>Application of the FTC: integrating $e^ix$\<close>
hoelzl@62083
    39
hoelzl@62083
    40
abbreviation iexp :: "real \<Rightarrow> complex" where
hoelzl@62083
    41
  "iexp \<equiv> (\<lambda>x. exp (\<i> * complex_of_real x))"
hoelzl@62083
    42
hoelzl@62083
    43
lemma isCont_iexp [simp]: "isCont iexp x"
hoelzl@62083
    44
  by (intro continuous_intros)
hoelzl@62083
    45
hoelzl@62083
    46
lemma has_vector_derivative_iexp[derivative_intros]:
hoelzl@62083
    47
  "(iexp has_vector_derivative \<i> * iexp x) (at x within s)"
hoelzl@62083
    48
  by (auto intro!: derivative_eq_intros simp: Re_exp Im_exp has_vector_derivative_complex_iff)
hoelzl@62083
    49
hoelzl@62083
    50
lemma interval_integral_iexp:
hoelzl@62083
    51
  fixes a b :: real
hoelzl@62083
    52
  shows "(CLBINT x=a..b. iexp x) = ii * iexp a - ii * iexp b"
hoelzl@62083
    53
  by (subst interval_integral_FTC_finite [where F = "\<lambda>x. -ii * iexp x"])
hoelzl@62083
    54
     (auto intro!: derivative_eq_intros continuous_intros)
hoelzl@62083
    55
hoelzl@62083
    56
subsection \<open>The Characteristic Function of a Real Measure.\<close>
hoelzl@62083
    57
hoelzl@62083
    58
definition
hoelzl@62083
    59
  char :: "real measure \<Rightarrow> real \<Rightarrow> complex"
hoelzl@62083
    60
where
hoelzl@62083
    61
  "char M t = CLINT x|M. iexp (t * x)"
hoelzl@62083
    62
hoelzl@62083
    63
lemma (in real_distribution) char_zero: "char M 0 = 1"
hoelzl@62083
    64
  unfolding char_def by (simp del: space_eq_univ add: prob_space)
hoelzl@62083
    65
hoelzl@62083
    66
lemma (in prob_space) integrable_iexp: 
hoelzl@62083
    67
  assumes f: "f \<in> borel_measurable M" "\<And>x. Im (f x) = 0"
hoelzl@62083
    68
  shows "integrable M (\<lambda>x. exp (ii * (f x)))"
hoelzl@62083
    69
proof (intro integrable_const_bound [of _ 1])
hoelzl@62083
    70
  from f have "\<And>x. of_real (Re (f x)) = f x"
hoelzl@62083
    71
    by (simp add: complex_eq_iff)
hoelzl@62083
    72
  then show "AE x in M. cmod (exp (\<i> * f x)) \<le> 1"
hoelzl@62083
    73
    using norm_exp_ii_times[of "Re (f x)" for x] by simp
hoelzl@62083
    74
qed (insert f, simp)
hoelzl@62083
    75
hoelzl@62083
    76
lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
hoelzl@62083
    77
proof -
hoelzl@62083
    78
  have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)"
hoelzl@62083
    79
    unfolding char_def by (intro integral_norm_bound integrable_iexp) auto
hoelzl@62083
    80
  also have "\<dots> \<le> 1"
hoelzl@62083
    81
    by (simp del: of_real_mult)
hoelzl@62083
    82
  finally show ?thesis .
hoelzl@62083
    83
qed
hoelzl@62083
    84
hoelzl@62083
    85
lemma (in real_distribution) isCont_char: "isCont (char M) t"
hoelzl@62083
    86
  unfolding continuous_at_sequentially
hoelzl@62083
    87
proof safe
hoelzl@62083
    88
  fix X assume X: "X \<longlonglongrightarrow> t"
hoelzl@62083
    89
  show "(char M \<circ> X) \<longlonglongrightarrow> char M t"
hoelzl@62083
    90
    unfolding comp_def char_def
hoelzl@62083
    91
    by (rule integral_dominated_convergence[where w="\<lambda>_. 1"]) (auto intro!: tendsto_intros X)
hoelzl@62083
    92
qed
hoelzl@62083
    93
hoelzl@62083
    94
lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel"
hoelzl@62083
    95
  by (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on isCont_char)
hoelzl@62083
    96
hoelzl@62083
    97
subsection \<open>Independence\<close>
hoelzl@62083
    98
hoelzl@62083
    99
(* the automation can probably be improved *)  
hoelzl@62083
   100
lemma (in prob_space) char_distr_sum:
hoelzl@62083
   101
  fixes X1 X2 :: "'a \<Rightarrow> real" and t :: real
hoelzl@62083
   102
  assumes "indep_var borel X1 borel X2"
hoelzl@62083
   103
  shows "char (distr M borel (\<lambda>\<omega>. X1 \<omega> + X2 \<omega>)) t =
hoelzl@62083
   104
    char (distr M borel X1) t * char (distr M borel X2) t"
hoelzl@62083
   105
proof -
hoelzl@62083
   106
  from assms have [measurable]: "random_variable borel X1" by (elim indep_var_rv1)
hoelzl@62083
   107
  from assms have [measurable]: "random_variable borel X2" by (elim indep_var_rv2)
hoelzl@62083
   108
hoelzl@62083
   109
  have "char (distr M borel (\<lambda>\<omega>. X1 \<omega> + X2 \<omega>)) t = (CLINT x|M. iexp (t * (X1 x + X2 x)))"
hoelzl@62083
   110
    by (simp add: char_def integral_distr)
hoelzl@62083
   111
  also have "\<dots> = (CLINT x|M. iexp (t * (X1 x)) * iexp (t * (X2 x))) "
hoelzl@62083
   112
    by (simp add: field_simps exp_add)
hoelzl@62083
   113
  also have "\<dots> = (CLINT x|M. iexp (t * (X1 x))) * (CLINT x|M. iexp (t * (X2 x)))"
hoelzl@62083
   114
    by (intro indep_var_lebesgue_integral indep_var_compose[unfolded comp_def, OF assms])
hoelzl@62083
   115
       (auto intro!: integrable_iexp)
hoelzl@62083
   116
  also have "\<dots> = char (distr M borel X1) t * char (distr M borel X2) t"
hoelzl@62083
   117
    by (simp add: char_def integral_distr)
hoelzl@62083
   118
  finally show ?thesis .
hoelzl@62083
   119
qed
hoelzl@62083
   120
hoelzl@62083
   121
lemma (in prob_space) char_distr_setsum:
hoelzl@62083
   122
  "indep_vars (\<lambda>i. borel) X A \<Longrightarrow>
hoelzl@62083
   123
    char (distr M borel (\<lambda>\<omega>. \<Sum>i\<in>A. X i \<omega>)) t = (\<Prod>i\<in>A. char (distr M borel (X i)) t)"
hoelzl@62083
   124
proof (induct A rule: infinite_finite_induct)
hoelzl@62083
   125
  case (insert x F) with indep_vars_subset[of "\<lambda>_. borel" X "insert x F" F] show ?case
hoelzl@62083
   126
    by (auto simp add: char_distr_sum indep_vars_setsum)
hoelzl@62083
   127
qed (simp_all add: char_def integral_distr prob_space del: distr_const)
hoelzl@62083
   128
hoelzl@62083
   129
subsection \<open>Approximations to $e^{ix}$\<close>
hoelzl@62083
   130
hoelzl@62083
   131
text \<open>Proofs from Billingsley, page 343.\<close>
hoelzl@62083
   132
hoelzl@62083
   133
lemma CLBINT_I0c_power_mirror_iexp:
hoelzl@62083
   134
  fixes x :: real and n :: nat
hoelzl@62083
   135
  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
hoelzl@62083
   136
  shows "(CLBINT s=0..x. f s n * iexp s) =
hoelzl@62083
   137
    x^Suc n / Suc n + (ii / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)"
hoelzl@62083
   138
proof -
hoelzl@62083
   139
  have 1:
hoelzl@62083
   140
    "((\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s)
hoelzl@62083
   141
      has_vector_derivative complex_of_real((x - s)^n) * iexp s + (ii * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n))))
hoelzl@62083
   142
      (at s within A)" for s A
hoelzl@62083
   143
    by (intro derivative_eq_intros) auto
hoelzl@62083
   144
hoelzl@62083
   145
  let ?F = "\<lambda>s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s"
hoelzl@62083
   146
  have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS")
hoelzl@62083
   147
  proof -
hoelzl@62083
   148
    have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * 
hoelzl@62083
   149
      complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))"
hoelzl@62083
   150
      by (cases "0 \<le> x") (auto intro!: simp: f_def[abs_def])
hoelzl@62083
   151
    also have "... = ?F x - ?F 0"
hoelzl@62083
   152
      unfolding zero_ereal_def using 1
hoelzl@62083
   153
      by (intro interval_integral_FTC_finite)
hoelzl@62083
   154
         (auto simp: f_def add_nonneg_eq_0_iff complex_eq_iff 
hoelzl@62083
   155
               intro!: continuous_at_imp_continuous_on continuous_intros)
hoelzl@62083
   156
    finally show ?thesis
hoelzl@62083
   157
      by auto
hoelzl@62083
   158
  qed
hoelzl@62083
   159
  show ?thesis
hoelzl@62083
   160
    unfolding \<open>?LHS = ?RHS\<close> f_def interval_lebesgue_integral_mult_right [symmetric]
hoelzl@62083
   161
    by (subst interval_lebesgue_integral_add(2) [symmetric])
hoelzl@62083
   162
       (auto intro!: interval_integrable_isCont continuous_intros simp: zero_ereal_def complex_eq_iff)
hoelzl@62083
   163
qed
hoelzl@62083
   164
hoelzl@62083
   165
lemma iexp_eq1:
hoelzl@62083
   166
  fixes x :: real
hoelzl@62083
   167
  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)"
hoelzl@62083
   168
  shows "iexp x =
hoelzl@62083
   169
    (\<Sum>k \<le> n. (ii * x)^k / (fact k)) + ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n")
hoelzl@62083
   170
proof (induction n)
hoelzl@62083
   171
  show "?P 0"
hoelzl@62083
   172
    by (auto simp add: field_simps interval_integral_iexp f_def zero_ereal_def)
hoelzl@62083
   173
next
hoelzl@62083
   174
  fix n assume ih: "?P n"
hoelzl@62083
   175
  have **: "\<And>a b :: real. a = -b \<longleftrightarrow> a + b = 0"
hoelzl@62083
   176
    by linarith
hoelzl@62083
   177
  have *: "of_nat n * of_nat (fact n) \<noteq> - (of_nat (fact n)::complex)"
hoelzl@62083
   178
    unfolding of_nat_mult[symmetric]
hoelzl@62083
   179
    by (simp add: complex_eq_iff ** of_nat_add[symmetric] del: of_nat_mult of_nat_fact of_nat_add)
hoelzl@62083
   180
  show "?P (Suc n)"
hoelzl@62083
   181
    unfolding setsum_atMost_Suc ih f_def CLBINT_I0c_power_mirror_iexp[of _ n]
hoelzl@62083
   182
    by (simp add: divide_simps add_eq_0_iff *) (simp add: field_simps)
hoelzl@62083
   183
qed
hoelzl@62083
   184
hoelzl@62083
   185
lemma iexp_eq2:
hoelzl@62083
   186
  fixes x :: real
hoelzl@62083
   187
  defines "f s m \<equiv> complex_of_real ((x - s) ^ m)" 
hoelzl@62083
   188
  shows "iexp x = (\<Sum>k\<le>Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))"
hoelzl@62083
   189
proof -
hoelzl@62083
   190
  have isCont_f: "isCont (\<lambda>s. f s n) x" for n x
hoelzl@62083
   191
    by (auto simp: f_def)
hoelzl@62083
   192
  let ?F = "\<lambda>s. complex_of_real (-((x - s) ^ (Suc n) / real (Suc n)))"
hoelzl@62083
   193
  have calc1: "(CLBINT s=0..x. f s n * (iexp s - 1)) =
hoelzl@62083
   194
    (CLBINT s=0..x. f s n * iexp s) - (CLBINT s=0..x. f s n)"
hoelzl@62083
   195
    unfolding zero_ereal_def
hoelzl@62083
   196
    by (subst interval_lebesgue_integral_diff(2) [symmetric])
hoelzl@62083
   197
       (simp_all add: interval_integrable_isCont isCont_f field_simps)
hoelzl@62083
   198
hoelzl@62083
   199
  have calc2: "(CLBINT s=0..x. f s n) = x^Suc n / Suc n"
hoelzl@62083
   200
    unfolding zero_ereal_def
hoelzl@62083
   201
  proof (subst interval_integral_FTC_finite [where a = 0 and b = x and f = "\<lambda>s. f s n" and F = ?F])
hoelzl@62083
   202
    show "(?F has_vector_derivative f y n) (at y within {min 0 x..max 0 x})" for y
hoelzl@62083
   203
      unfolding f_def
hoelzl@62083
   204
      by (intro has_vector_derivative_of_real)
hoelzl@62083
   205
         (auto intro!: derivative_eq_intros simp del: power_Suc simp add: add_nonneg_eq_0_iff)
hoelzl@62083
   206
  qed (auto intro: continuous_at_imp_continuous_on isCont_f)
hoelzl@62083
   207
hoelzl@62083
   208
  have calc3: "ii ^ (Suc (Suc n)) / (fact (Suc n)) = (ii ^ (Suc n) / (fact n)) * (ii / (Suc n))"
hoelzl@62083
   209
    by (simp add: field_simps)
hoelzl@62083
   210
hoelzl@62083
   211
  show ?thesis
hoelzl@62083
   212
    unfolding iexp_eq1 [where n = "Suc n" and x=x] calc1 calc2 calc3 unfolding f_def
hoelzl@62083
   213
    by (subst CLBINT_I0c_power_mirror_iexp [where n = n]) auto
hoelzl@62083
   214
qed
hoelzl@62083
   215
hoelzl@62083
   216
lemma abs_LBINT_I0c_abs_power_diff:
hoelzl@62083
   217
  "\<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar> = \<bar>x ^ (Suc n) / (Suc n)\<bar>"
hoelzl@62083
   218
proof -
hoelzl@62083
   219
 have "\<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar> = \<bar>LBINT s=0..x. (x - s)^n\<bar>"
hoelzl@62083
   220
  proof cases
hoelzl@62083
   221
    assume "0 \<le> x \<or> even n"
hoelzl@62083
   222
    then have "(LBINT s=0..x. \<bar>(x - s)^n\<bar>) = LBINT s=0..x. (x - s)^n"
hoelzl@62083
   223
      by (auto simp add: zero_ereal_def power_even_abs power_abs min_absorb1 max_absorb2
hoelzl@62083
   224
               intro!: interval_integral_cong)
hoelzl@62083
   225
    then show ?thesis by simp
hoelzl@62083
   226
  next
hoelzl@62083
   227
    assume "\<not> (0 \<le> x \<or> even n)" 
hoelzl@62083
   228
    then have "(LBINT s=0..x. \<bar>(x - s)^n\<bar>) = LBINT s=0..x. -((x - s)^n)"
hoelzl@62083
   229
      by (auto simp add: zero_ereal_def power_abs min_absorb1 max_absorb2
hoelzl@62083
   230
                         ereal_min[symmetric] ereal_max[symmetric] power_minus_odd[symmetric]
hoelzl@62083
   231
               simp del: ereal_min ereal_max intro!: interval_integral_cong)
hoelzl@62083
   232
    also have "\<dots> = - (LBINT s=0..x. (x - s)^n)"
hoelzl@62083
   233
      by (subst interval_lebesgue_integral_uminus, rule refl)
hoelzl@62083
   234
    finally show ?thesis by simp
hoelzl@62083
   235
  qed
hoelzl@62083
   236
  also have "LBINT s=0..x. (x - s)^n = x^Suc n / Suc n"
hoelzl@62083
   237
  proof -
hoelzl@62083
   238
    let ?F = "\<lambda>t. - ((x - t)^(Suc n) / Suc n)"
hoelzl@62083
   239
    have "LBINT s=0..x. (x - s)^n = ?F x - ?F 0"
hoelzl@62083
   240
      unfolding zero_ereal_def
hoelzl@62083
   241
      by (intro interval_integral_FTC_finite continuous_at_imp_continuous_on
hoelzl@62083
   242
                has_field_derivative_iff_has_vector_derivative[THEN iffD1])
hoelzl@62083
   243
         (auto simp del: power_Suc intro!: derivative_eq_intros simp add: add_nonneg_eq_0_iff)
hoelzl@62083
   244
    also have "\<dots> = x ^ (Suc n) / (Suc n)" by simp
hoelzl@62083
   245
    finally show ?thesis .
hoelzl@62083
   246
  qed
hoelzl@62083
   247
  finally show ?thesis .
hoelzl@62083
   248
qed
hoelzl@62083
   249
hoelzl@62083
   250
lemma iexp_approx1: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> \<bar>x\<bar>^(Suc n) / fact (Suc n)"
hoelzl@62083
   251
proof -
hoelzl@62083
   252
  have "iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k) =
hoelzl@62083
   253
      ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2")
hoelzl@62083
   254
    by (subst iexp_eq1 [of _ n], simp add: field_simps)
hoelzl@62083
   255
  then have "cmod (?t1) = cmod (?t2)"
hoelzl@62083
   256
    by simp
hoelzl@62083
   257
  also have "\<dots> =  (1 / of_nat (fact n)) * cmod (CLBINT s=0..x. (x - s)^n * (iexp s))"
hoelzl@62083
   258
    by (simp add: norm_mult norm_divide norm_power)
hoelzl@62083
   259
  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>LBINT s=0..x. cmod ((x - s)^n * (iexp s))\<bar>"
hoelzl@62083
   260
    by (intro mult_left_mono interval_integral_norm2)
hoelzl@62083
   261
       (auto simp: zero_ereal_def intro: interval_integrable_isCont)
hoelzl@62083
   262
  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>LBINT s=0..x. \<bar>(x - s)^n\<bar>\<bar>"
hoelzl@62083
   263
    by (simp add: norm_mult del: of_real_diff of_real_power)
hoelzl@62083
   264
  also have "\<dots> \<le> (1 / of_nat (fact n)) * \<bar>x ^ (Suc n) / (Suc n)\<bar>"
hoelzl@62083
   265
    by (simp add: abs_LBINT_I0c_abs_power_diff)
hoelzl@62083
   266
  also have "1 / real_of_nat (fact n::nat) * \<bar>x ^ Suc n / real (Suc n)\<bar> =
hoelzl@62083
   267
      \<bar>x\<bar> ^ Suc n / fact (Suc n)"
hoelzl@62083
   268
    by (simp add: abs_mult power_abs)
hoelzl@62083
   269
  finally show ?thesis .
hoelzl@62083
   270
qed
hoelzl@62083
   271
hoelzl@62083
   272
lemma iexp_approx2: "cmod (iexp x - (\<Sum>k \<le> n. (ii * x)^k / fact k)) \<le> 2 * \<bar>x\<bar>^n / fact n"
hoelzl@62083
   273
proof (induction n) -- \<open>really cases\<close>
hoelzl@62083
   274
  case (Suc n)
hoelzl@62083
   275
  have *: "\<And>a b. interval_lebesgue_integrable lborel a b f \<Longrightarrow> interval_lebesgue_integrable lborel a b g \<Longrightarrow>
hoelzl@62083
   276
      \<bar>LBINT s=a..b. f s\<bar> \<le> \<bar>LBINT s=a..b. g s\<bar>"
hoelzl@62083
   277
    if f: "\<And>s. 0 \<le> f s" and g: "\<And>s. f s \<le> g s" for f g :: "_ \<Rightarrow> real"
hoelzl@62083
   278
    using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def
hoelzl@62083
   279
    by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono)
hoelzl@62083
   280
hoelzl@62083
   281
  have "iexp x - (\<Sum>k \<le> Suc n. (ii * x)^k / fact k) =
hoelzl@62083
   282
      ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2")
hoelzl@62083
   283
    unfolding iexp_eq2 [of x n] by (simp add: field_simps)
hoelzl@62083
   284
  then have "cmod (?t1) = cmod (?t2)"
hoelzl@62083
   285
    by simp
hoelzl@62083
   286
  also have "\<dots> =  (1 / (fact n)) * cmod (CLBINT s=0..x. (x - s)^n * (iexp s - 1))"
hoelzl@62083
   287
    by (simp add: norm_mult norm_divide norm_power)
hoelzl@62083
   288
  also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. cmod ((x - s)^n * (iexp s - 1))\<bar>"
hoelzl@62083
   289
    by (intro mult_left_mono interval_integral_norm2)
hoelzl@62083
   290
       (auto intro!: interval_integrable_isCont simp: zero_ereal_def)
hoelzl@62083
   291
  also have "\<dots> = (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * cmod((iexp s - 1))\<bar>"
hoelzl@62083
   292
    by (simp add: norm_mult del: of_real_diff of_real_power)
hoelzl@62083
   293
  also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * 2\<bar>"
hoelzl@62083
   294
    by (intro mult_left_mono * order_trans [OF norm_triangle_ineq4])
hoelzl@62083
   295
       (auto simp: mult_ac zero_ereal_def intro!: interval_integrable_isCont)
hoelzl@62083
   296
  also have "\<dots> = (2 / (fact n)) * \<bar>x ^ (Suc n) / (Suc n)\<bar>"
hoelzl@62083
   297
   by (simp add: abs_LBINT_I0c_abs_power_diff abs_mult)
hoelzl@62083
   298
  also have "2 / fact n * \<bar>x ^ Suc n / real (Suc n)\<bar> = 2 * \<bar>x\<bar> ^ Suc n / (fact (Suc n))"
hoelzl@62083
   299
    by (simp add: abs_mult power_abs)
hoelzl@62083
   300
  finally show ?case .
hoelzl@62083
   301
qed (insert norm_triangle_ineq4[of "iexp x" 1], simp)
hoelzl@62083
   302
hoelzl@62083
   303
lemma (in real_distribution) char_approx1:
hoelzl@62083
   304
  assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x^k)"
hoelzl@62083
   305
  shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
hoelzl@62083
   306
    (2*\<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>x\<bar>^n)" (is "cmod (char M t - ?t1) \<le> _")
hoelzl@62083
   307
proof -
hoelzl@62083
   308
  have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
hoelzl@62083
   309
    by (intro integrable_const_bound) auto
hoelzl@62083
   310
  
hoelzl@62083
   311
  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
hoelzl@62083
   312
  have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
hoelzl@62083
   313
    unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
hoelzl@62083
   314
  
hoelzl@62083
   315
  have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
hoelzl@62083
   316
    unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
hoelzl@62083
   317
  then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   318
    by (simp add: integ_c)
hoelzl@62083
   319
  also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   320
    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
hoelzl@62083
   321
  also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   322
    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
hoelzl@62083
   323
  also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
hoelzl@62083
   324
  proof (rule integral_mono)
hoelzl@62083
   325
    show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
hoelzl@62083
   326
      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
hoelzl@62083
   327
    show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
hoelzl@62083
   328
      unfolding power_abs[symmetric]
hoelzl@62083
   329
      by (intro integrable_mult_right integrable_abs integrable_moments) simp
hoelzl@62083
   330
    show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n" for x
hoelzl@62083
   331
      using iexp_approx2[of "t * x" n] by (auto simp add: abs_mult field_simps c_def)
hoelzl@62083
   332
  qed
hoelzl@62083
   333
  finally show ?thesis
hoelzl@62083
   334
    unfolding integral_mult_right_zero .
hoelzl@62083
   335
qed
hoelzl@62083
   336
hoelzl@62083
   337
lemma (in real_distribution) char_approx2:
hoelzl@62083
   338
  assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x ^ k)"
hoelzl@62083
   339
  shows "cmod (char M t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le>
hoelzl@62083
   340
    (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
hoelzl@62083
   341
    (is "cmod (char M t - ?t1) \<le> _")
hoelzl@62083
   342
proof -
hoelzl@62083
   343
  have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))"
hoelzl@62083
   344
    by (intro integrable_const_bound) auto
hoelzl@62083
   345
  
hoelzl@62083
   346
  def c \<equiv> "\<lambda>k x. (ii * t)^k / fact k * complex_of_real (x^k)"
hoelzl@62083
   347
  have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)"
hoelzl@62083
   348
    unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments)
hoelzl@62083
   349
hoelzl@62083
   350
  have *: "min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^Suc n / fact (Suc n)) =
hoelzl@62083
   351
      \<bar>t\<bar>^n / fact (Suc n) * min (2 * \<bar>x\<bar>^n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar>^(Suc n))" for x
hoelzl@62083
   352
    apply (subst mult_min_right)
hoelzl@62083
   353
    apply simp
hoelzl@62083
   354
    apply (rule arg_cong2[where f=min])
hoelzl@62083
   355
    apply (simp_all add: field_simps abs_mult del: fact_Suc)
hoelzl@62083
   356
    apply (simp_all add: field_simps)
hoelzl@62083
   357
    done
hoelzl@62083
   358
  
hoelzl@62083
   359
  have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k
hoelzl@62083
   360
    unfolding c_def integral_mult_right_zero integral_complex_of_real by simp
hoelzl@62083
   361
  then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   362
    by (simp add: integ_c)
hoelzl@62083
   363
  also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   364
    unfolding char_def by (subst integral_diff[OF integ_iexp]) (auto intro!: integ_c)
hoelzl@62083
   365
  also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
hoelzl@62083
   366
    by (intro integral_norm_bound integrable_diff integ_iexp integrable_setsum integ_c) simp
hoelzl@62083
   367
  also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
hoelzl@62083
   368
    (is "_ \<le> expectation ?f")
hoelzl@62083
   369
  proof (rule integral_mono)
hoelzl@62083
   370
    show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
hoelzl@62083
   371
      by (intro integrable_norm integrable_diff integ_iexp integrable_setsum integ_c) simp
hoelzl@62083
   372
    show "integrable M ?f"
hoelzl@62083
   373
      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"])
hoelzl@62083
   374
         (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
hoelzl@62083
   375
    show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x
hoelzl@62083
   376
      using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n]
hoelzl@62083
   377
      by (auto simp add: abs_mult field_simps c_def intro!: min.boundedI)
hoelzl@62083
   378
  qed
hoelzl@62083
   379
  also have "\<dots> = (\<bar>t\<bar>^n / fact (Suc n)) * expectation (\<lambda>x. min (2 * \<bar>x\<bar>^n * Suc n) (\<bar>t\<bar> * \<bar>x\<bar>^Suc n))"
hoelzl@62083
   380
    unfolding *
hoelzl@62083
   381
  proof (rule integral_mult_right)
hoelzl@62083
   382
    show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))"
hoelzl@62083
   383
      by (rule integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"])
hoelzl@62083
   384
         (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib)
hoelzl@62083
   385
  qed
hoelzl@62083
   386
  finally show ?thesis
hoelzl@62083
   387
    unfolding integral_mult_right_zero .
hoelzl@62083
   388
qed
hoelzl@62083
   389
hoelzl@62083
   390
lemma (in real_distribution) char_approx3:
hoelzl@62083
   391
  fixes t
hoelzl@62083
   392
  assumes
hoelzl@62083
   393
    integrable_1: "integrable M (\<lambda>x. x)" and
hoelzl@62083
   394
    integral_1: "expectation (\<lambda>x. x) = 0" and
hoelzl@62083
   395
    integrable_2: "integrable M (\<lambda>x. x^2)" and
hoelzl@62083
   396
    integral_2: "variance (\<lambda>x. x) = \<sigma>2"
hoelzl@62083
   397
  shows "cmod (char M t - (1 - t^2 * \<sigma>2 / 2)) \<le>
hoelzl@62083
   398
    (t^2 / 6) * expectation (\<lambda>x. min (6 * x^2) (abs t * (abs x)^3) )"
hoelzl@62083
   399
proof -
hoelzl@62083
   400
  note real_distribution.char_approx2 [of M 2 t, simplified]
hoelzl@62083
   401
  have [simp]: "prob UNIV = 1" by (metis prob_space space_eq_univ)
hoelzl@62083
   402
  from integral_2 have [simp]: "expectation (\<lambda>x. x * x) = \<sigma>2" 
hoelzl@62083
   403
    by (simp add: integral_1 numeral_eq_Suc)
hoelzl@62083
   404
  have 1: "k \<le> 2 \<Longrightarrow> integrable M (\<lambda>x. x^k)" for k 
hoelzl@62083
   405
    using assms by (auto simp: eval_nat_numeral le_Suc_eq)
hoelzl@62083
   406
  note char_approx1
hoelzl@62083
   407
  note 2 = char_approx1 [of 2 t, OF 1, simplified]
hoelzl@62083
   408
  have "cmod (char M t - (\<Sum>k\<le>2. (\<i> * t) ^ k * (expectation (\<lambda>x. x ^ k)) / (fact k))) \<le>
hoelzl@62083
   409
      t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / fact (3::nat)"
hoelzl@62083
   410
    using char_approx2 [of 2 t, OF 1] by simp
hoelzl@62083
   411
  also have "(\<Sum>k\<le>2. (\<i> * t) ^ k * expectation (\<lambda>x. x ^ k) / (fact k)) = 1 - t^2 * \<sigma>2 / 2"
hoelzl@62083
   412
    by (simp add: complex_eq_iff numeral_eq_Suc integral_1 Re_divide Im_divide)
hoelzl@62083
   413
  also have "fact 3 = 6" by (simp add: eval_nat_numeral)
hoelzl@62083
   414
  also have "t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / 6 =
hoelzl@62083
   415
     t\<^sup>2 / 6 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3))" by (simp add: field_simps)
hoelzl@62083
   416
  finally show ?thesis .
hoelzl@62083
   417
qed
hoelzl@62083
   418
hoelzl@62083
   419
text \<open>
hoelzl@62083
   420
  This is a more familiar textbook formulation in terms of random variables, but 
hoelzl@62083
   421
  we will use the previous version for the CLT.
hoelzl@62083
   422
\<close>
hoelzl@62083
   423
hoelzl@62083
   424
lemma (in prob_space) char_approx3':
hoelzl@62083
   425
  fixes \<mu> :: "real measure" and X
hoelzl@62083
   426
  assumes rv_X [simp]: "random_variable borel X"
hoelzl@62083
   427
    and [simp]: "integrable M X" "integrable M (\<lambda>x. (X x)^2)" "expectation X = 0"
hoelzl@62083
   428
    and var_X: "variance X = \<sigma>2"
hoelzl@62083
   429
    and \<mu>_def: "\<mu> = distr M borel X"
hoelzl@62083
   430
  shows "cmod (char \<mu> t - (1 - t^2 * \<sigma>2 / 2)) \<le>
hoelzl@62083
   431
    (t^2 / 6) * expectation (\<lambda>x. min (6 * (X x)^2) (\<bar>t\<bar> * \<bar>X x\<bar>^3))"
hoelzl@62083
   432
  using var_X unfolding \<mu>_def
hoelzl@62083
   433
  apply (subst integral_distr [symmetric, OF rv_X], simp)
hoelzl@62083
   434
  apply (intro real_distribution.char_approx3)
hoelzl@62083
   435
  apply (auto simp add: integrable_distr_eq integral_distr)
hoelzl@62083
   436
  done
hoelzl@62083
   437
hoelzl@62083
   438
text \<open>
hoelzl@62083
   439
  this is the formulation in the book -- in terms of a random variable *with* the distribution,
hoelzl@62083
   440
  rather the distribution itself. I don't know which is more useful, though in principal we can
hoelzl@62083
   441
  go back and forth between them.
hoelzl@62083
   442
\<close>
hoelzl@62083
   443
hoelzl@62083
   444
lemma (in prob_space) char_approx1':
hoelzl@62083
   445
  fixes \<mu> :: "real measure" and X
hoelzl@62083
   446
  assumes integrable_moments : "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. X x ^ k)"
hoelzl@62083
   447
    and rv_X[measurable]: "random_variable borel X"
hoelzl@62083
   448
    and \<mu>_distr : "distr M borel X = \<mu>"
hoelzl@62083
   449
  shows "cmod (char \<mu> t - (\<Sum>k \<le> n. ((ii * t)^k / fact k) * expectation (\<lambda>x. (X x)^k))) \<le>
hoelzl@62083
   450
    (2 * \<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>X x\<bar>^n)"
hoelzl@62083
   451
  unfolding \<mu>_distr[symmetric]
hoelzl@62083
   452
  apply (subst (1 2) integral_distr [symmetric, OF rv_X], simp, simp)
hoelzl@62083
   453
  apply (intro real_distribution.char_approx1[of "distr M borel X" n t] real_distribution_distr rv_X)
hoelzl@62083
   454
  apply (auto simp: integrable_distr_eq integrable_moments)
hoelzl@62083
   455
  done
hoelzl@62083
   456
hoelzl@62083
   457
subsection \<open>Calculation of the Characteristic Function of the Standard Distribution\<close>
hoelzl@62083
   458
hoelzl@62083
   459
abbreviation
hoelzl@62083
   460
  "std_normal_distribution \<equiv> density lborel std_normal_density"
hoelzl@62083
   461
hoelzl@62083
   462
(* TODO: should this be an instance statement? *)
hoelzl@62083
   463
lemma real_dist_normal_dist: "real_distribution std_normal_distribution"
hoelzl@62083
   464
  using prob_space_normal_density by (auto simp: real_distribution_def real_distribution_axioms_def)
hoelzl@62083
   465
hoelzl@62083
   466
lemma std_normal_distribution_even_moments:
hoelzl@62083
   467
  fixes k :: nat
hoelzl@62083
   468
  shows "(LINT x|std_normal_distribution. x^(2 * k)) = fact (2 * k) / (2^k * fact k)"
hoelzl@62083
   469
    and "integrable std_normal_distribution (\<lambda>x. x^(2 * k))"
hoelzl@62083
   470
  using integral_std_normal_moment_even[of k]
hoelzl@62083
   471
  by (subst integral_density)
hoelzl@62083
   472
     (auto simp: normal_density_nonneg integrable_density
hoelzl@62083
   473
           intro: integrable.intros std_normal_moment_even)
hoelzl@62083
   474
hoelzl@62083
   475
lemma integrable_std_normal_distribution_moment: "integrable std_normal_distribution (\<lambda>x. x^k)"
hoelzl@62083
   476
  by (auto simp: normal_density_nonneg integrable_std_normal_moment integrable_density)
hoelzl@62083
   477
hoelzl@62083
   478
lemma integral_std_normal_distribution_moment_odd:
hoelzl@62083
   479
  "odd k \<Longrightarrow> integral\<^sup>L std_normal_distribution (\<lambda>x. x^k) = 0"
hoelzl@62083
   480
  using integral_std_normal_moment_odd[of "(k - 1) div 2"]
hoelzl@62083
   481
  by (auto simp: integral_density normal_density_nonneg elim: oddE)
hoelzl@62083
   482
hoelzl@62083
   483
lemma std_normal_distribution_even_moments_abs:
hoelzl@62083
   484
  fixes k :: nat
hoelzl@62083
   485
  shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k)) = fact (2 * k) / (2^k * fact k)"
hoelzl@62083
   486
  using integral_std_normal_moment_even[of k]
hoelzl@62083
   487
  by (subst integral_density) (auto simp: normal_density_nonneg power_even_abs)
hoelzl@62083
   488
hoelzl@62083
   489
lemma std_normal_distribution_odd_moments_abs:
hoelzl@62083
   490
  fixes k :: nat
hoelzl@62083
   491
  shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2 ^ k * fact k"
hoelzl@62083
   492
  using integral_std_normal_moment_abs_odd[of k]
hoelzl@62083
   493
  by (subst integral_density) (auto simp: normal_density_nonneg)
hoelzl@62083
   494
hoelzl@62083
   495
theorem char_std_normal_distribution:
hoelzl@62083
   496
  "char std_normal_distribution = (\<lambda>t. complex_of_real (exp (- (t^2) / 2)))"
hoelzl@62083
   497
proof (intro ext LIMSEQ_unique)
hoelzl@62083
   498
  fix t :: real
hoelzl@62083
   499
  let ?f' = "\<lambda>k. (ii * t)^k / fact k * (LINT x | std_normal_distribution. x^k)"
hoelzl@62083
   500
  let ?f = "\<lambda>n. (\<Sum>k \<le> n. ?f' k)"
hoelzl@62083
   501
  show "?f \<longlonglongrightarrow> exp (-(t^2) / 2)"
hoelzl@62083
   502
  proof (rule limseq_even_odd)
hoelzl@62083
   503
    have "(\<i> * complex_of_real t) ^ (2 * a) / (2 ^ a * fact a) = (- ((complex_of_real t)\<^sup>2 / 2)) ^ a / fact a" for a
hoelzl@62083
   504
      by (subst power_mult) (simp add: field_simps uminus_power_if power_mult)
hoelzl@62083
   505
    then have *: "?f (2 * n) = complex_of_real (\<Sum>k < Suc n. (1 / fact k) * (- (t^2) / 2)^k)" for n :: nat
hoelzl@62083
   506
      unfolding of_real_setsum
hoelzl@62083
   507
      by (intro setsum.reindex_bij_witness_not_neutral[symmetric, where
hoelzl@62083
   508
           i="\<lambda>n. n div 2" and j="\<lambda>n. 2 * n" and T'="{i. i \<le> 2 * n \<and> odd i}" and S'="{}"])
hoelzl@62083
   509
         (auto simp: integral_std_normal_distribution_moment_odd std_normal_distribution_even_moments)
hoelzl@62083
   510
    show "(\<lambda>n. ?f (2 * n)) \<longlonglongrightarrow> exp (-(t^2) / 2)"
hoelzl@62083
   511
      unfolding * using exp_converges[where 'a=real]
hoelzl@62083
   512
      by (intro tendsto_of_real LIMSEQ_Suc) (auto simp: inverse_eq_divide sums_def [symmetric])
hoelzl@62083
   513
    have **: "?f (2 * n + 1) = ?f (2 * n)" for n
hoelzl@62083
   514
    proof -
hoelzl@62083
   515
      have "?f (2 * n + 1) = ?f (2 * n) + ?f' (2 * n + 1)"
hoelzl@62083
   516
        by simp
hoelzl@62083
   517
      also have "?f' (2 * n + 1) = 0"
hoelzl@62083
   518
        by (subst integral_std_normal_distribution_moment_odd) simp_all
hoelzl@62083
   519
      finally show "?f (2 * n + 1) = ?f (2 * n)"
hoelzl@62083
   520
        by simp
hoelzl@62083
   521
    qed
hoelzl@62083
   522
    show "(\<lambda>n. ?f (2 * n + 1)) \<longlonglongrightarrow> exp (-(t^2) / 2)"
hoelzl@62083
   523
      unfolding ** by fact
hoelzl@62083
   524
  qed
hoelzl@62083
   525
hoelzl@62083
   526
  have **: "(\<lambda>n. x ^ n / fact n) \<longlonglongrightarrow> 0" for x :: real
hoelzl@62083
   527
    using summable_LIMSEQ_zero [OF summable_exp] by (auto simp add: inverse_eq_divide)
hoelzl@62083
   528
hoelzl@62083
   529
  let ?F = "\<lambda>n. 2 * \<bar>t\<bar> ^ n / fact n * (LINT x|std_normal_distribution. \<bar>x\<bar> ^ n)"
hoelzl@62083
   530
hoelzl@62083
   531
  show "?f \<longlonglongrightarrow> char std_normal_distribution t"
hoelzl@62083
   532
  proof (rule metric_tendsto_imp_tendsto[OF limseq_even_odd])
hoelzl@62083
   533
    show "(\<lambda>n. ?F (2 * n)) \<longlonglongrightarrow> 0"
hoelzl@62083
   534
    proof (rule Lim_transform_eventually)
hoelzl@62083
   535
      show "\<forall>\<^sub>F n in sequentially. 2 * ((t^2 / 2)^n / fact n) = ?F (2 * n)"
hoelzl@62083
   536
        unfolding std_normal_distribution_even_moments_abs by (simp add: power_mult power_divide)
hoelzl@62083
   537
    qed (intro tendsto_mult_right_zero **)
hoelzl@62083
   538
hoelzl@62083
   539
    have *: "?F (2 * n + 1) = (2 * \<bar>t\<bar> * sqrt (2 / pi)) * ((2 * t^2)^n * fact n / fact (2 * n + 1))" for n
hoelzl@62083
   540
      unfolding std_normal_distribution_odd_moments_abs
hoelzl@62083
   541
      by (simp add: field_simps power_mult[symmetric] power_even_abs)
hoelzl@62083
   542
    have "norm ((2 * t\<^sup>2) ^ n * fact n / fact (2 * n + 1)) \<le> (2 * t\<^sup>2) ^ n / fact n" for n
hoelzl@62083
   543
      using mult_mono[OF _ square_fact_le_2_fact, of 1 "1 + 2 * real n" n]
hoelzl@62083
   544
      by (auto simp add: divide_simps intro!: mult_left_mono)
hoelzl@62083
   545
    then show "(\<lambda>n. ?F (2 * n + 1)) \<longlonglongrightarrow> 0"
hoelzl@62083
   546
      unfolding * by (intro tendsto_mult_right_zero Lim_null_comparison [OF _ ** [of "2 * t\<^sup>2"]]) auto
hoelzl@62083
   547
hoelzl@62083
   548
    show "\<forall>\<^sub>F n in sequentially. dist (?f n) (char std_normal_distribution t) \<le> dist (?F n) 0"
hoelzl@62083
   549
      using real_distribution.char_approx1[OF real_dist_normal_dist integrable_std_normal_distribution_moment]
hoelzl@62083
   550
      by (auto simp: dist_norm integral_nonneg_AE norm_minus_commute)
hoelzl@62083
   551
  qed
hoelzl@62083
   552
qed
hoelzl@62083
   553
hoelzl@62083
   554
end