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