1(* Title: HOL/Probability/Characteristic_Functions.thy 2 Authors: Jeremy Avigad (CMU), Luke Serafin (CMU), Johannes H��lzl (TUM) 3*) 4 5section \<open>Characteristic Functions\<close> 6 7theory Characteristic_Functions 8 imports Weak_Convergence Independent_Family Distributions 9begin 10 11lemma 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 14lemma 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" 17proof - 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 29qed 30 31lemma 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 37subsection \<open>Application of the FTC: integrating $e^ix$\<close> 38 39abbreviation iexp :: "real \<Rightarrow> complex" where 40 "iexp \<equiv> (\<lambda>x. exp (\<i> * complex_of_real x))" 41 42lemma isCont_iexp [simp]: "isCont iexp x" 43 by (intro continuous_intros) 44 45lemma 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 49lemma 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 55subsection \<open>The Characteristic Function of a Real Measure.\<close> 56 57definition 58 char :: "real measure \<Rightarrow> real \<Rightarrow> complex" 59where 60 "char M t = CLINT x|M. iexp (t * x)" 61 62lemma (in real_distribution) char_zero: "char M 0 = 1" 63 unfolding char_def by (simp del: space_eq_univ add: prob_space) 64 65lemma (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)))" 68proof (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_i_times[of "Re (f x)" for x] by simp 73qed (insert f, simp) 74 75lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1" 76proof - 77 have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)" 78 unfolding char_def by (intro integral_norm_bound) 79 also have "\<dots> \<le> 1" 80 by (simp del: of_real_mult) 81 finally show ?thesis . 82qed 83 84lemma (in real_distribution) isCont_char: "isCont (char M) t" 85 unfolding continuous_at_sequentially 86proof 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) 91qed 92 93lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel" 94 by (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on isCont_char) 95 96subsection \<open>Independence\<close> 97 98(* the automation can probably be improved *) 99lemma (in prob_space) char_distr_add: 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" 104proof - 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 . 118qed 119 120lemma (in prob_space) char_distr_sum: 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)" 123proof (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_add indep_vars_sum) 126qed (simp_all add: char_def integral_distr prob_space del: distr_const) 127 128subsection \<open>Approximations to $e^{ix}$\<close> 129 130text \<open>Proofs from Billingsley, page 343.\<close> 131 132lemma 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)" 137proof - 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) 162qed 163 164lemma 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") 169proof (induction n) 170 show "?P 0" 171 by (auto simp add: field_simps interval_integral_iexp f_def zero_ereal_def) 172next 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 sum.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) 182qed 183 184lemma 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))" 188proof - 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 213qed 214 215lemma 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>" 217proof - 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 . 247qed 248 249lemma iexp_approx1: "cmod (iexp x - (\<Sum>k \<le> n. (\<i> * x)^k / fact k)) \<le> \<bar>x\<bar>^(Suc n) / fact (Suc n)" 250proof - 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 . 269qed 270 271lemma iexp_approx2: "cmod (iexp x - (\<Sum>k \<le> n. (\<i> * x)^k / fact k)) \<le> 2 * \<bar>x\<bar>^n / fact n" 272proof (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 278 unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def set_lebesgue_integral_def set_integrable_def 279 by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono) 280 281 have "iexp x - (\<Sum>k \<le> Suc n. (\<i> * x)^k / fact k) = 282 ((\<i> ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2") 283 unfolding iexp_eq2 [of x n] by (simp add: field_simps) 284 then have "cmod (?t1) = cmod (?t2)" 285 by simp 286 also have "\<dots> = (1 / (fact n)) * cmod (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" 287 by (simp add: norm_mult norm_divide norm_power) 288 also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. cmod ((x - s)^n * (iexp s - 1))\<bar>" 289 by (intro mult_left_mono interval_integral_norm2) 290 (auto intro!: interval_integrable_isCont simp: zero_ereal_def) 291 also have "\<dots> = (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * cmod((iexp s - 1))\<bar>" 292 by (simp add: norm_mult del: of_real_diff of_real_power) 293 also have "\<dots> \<le> (1 / (fact n)) * \<bar>LBINT s=0..x. abs ((x - s)^n) * 2\<bar>" 294 by (intro mult_left_mono * order_trans [OF norm_triangle_ineq4]) 295 (auto simp: mult_ac zero_ereal_def intro!: interval_integrable_isCont) 296 also have "\<dots> = (2 / (fact n)) * \<bar>x ^ (Suc n) / (Suc n)\<bar>" 297 by (simp add: abs_LBINT_I0c_abs_power_diff abs_mult) 298 also have "2 / fact n * \<bar>x ^ Suc n / real (Suc n)\<bar> = 2 * \<bar>x\<bar> ^ Suc n / (fact (Suc n))" 299 by (simp add: abs_mult power_abs) 300 finally show ?case . 301qed (insert norm_triangle_ineq4[of "iexp x" 1], simp) 302 303lemma (in real_distribution) char_approx1: 304 assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x^k)" 305 shows "cmod (char M t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le> 306 (2*\<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>x\<bar>^n)" (is "cmod (char M t - ?t1) \<le> _") 307proof - 308 have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))" 309 by (intro integrable_const_bound) auto 310 311 define c where [abs_def]: "c k x = (\<i> * t)^k / fact k * complex_of_real (x^k)" for k x 312 have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)" 313 unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) 314 315 have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k 316 unfolding c_def integral_mult_right_zero integral_complex_of_real by simp 317 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" 318 by (simp add: integ_c) 319 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" 320 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) 321 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" 322 by (intro integral_norm_bound) 323 also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" 324 proof (rule integral_mono) 325 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" 326 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp 327 show "integrable M (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)" 328 unfolding power_abs[symmetric] 329 by (intro integrable_mult_right integrable_abs integrable_moments) simp 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 331 using iexp_approx2[of "t * x" n] by (auto simp add: abs_mult field_simps c_def) 332 qed 333 finally show ?thesis 334 unfolding integral_mult_right_zero . 335qed 336 337lemma (in real_distribution) char_approx2: 338 assumes integrable_moments: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. x ^ k)" 339 shows "cmod (char M t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. x^k))) \<le> 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))" 341 (is "cmod (char M t - ?t1) \<le> _") 342proof - 343 have integ_iexp: "integrable M (\<lambda>x. iexp (t * x))" 344 by (intro integrable_const_bound) auto 345 346 define c where [abs_def]: "c k x = (\<i> * t)^k / fact k * complex_of_real (x^k)" for k x 347 have integ_c: "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. c k x)" 348 unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) 349 350 have *: "min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^Suc n / fact (Suc n)) = 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 352 apply (subst mult_min_right) 353 apply simp 354 apply (rule arg_cong2[where f=min]) 355 apply (simp_all add: field_simps abs_mult del: fact_Suc) 356 apply (simp_all add: field_simps) 357 done 358 359 have "k \<le> n \<Longrightarrow> expectation (c k) = (\<i>*t) ^ k * (expectation (\<lambda>x. x ^ k)) / fact k" for k 360 unfolding c_def integral_mult_right_zero integral_complex_of_real by simp 361 then have "norm (char M t - ?t1) = norm (char M t - (CLINT x | M. (\<Sum>k \<le> n. c k x)))" 362 by (simp add: integ_c) 363 also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))" 364 unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c) 365 also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))" 366 by (rule integral_norm_bound) 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)))" 368 (is "_ \<le> expectation ?f") 369 proof (rule integral_mono) 370 show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))" 371 by (intro integrable_norm Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp 372 show "integrable M ?f" 373 by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>t * x\<bar> ^ n / fact n"]) 374 (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib) 375 show "cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)) \<le> ?f x" for x 376 using iexp_approx1[of "t * x" n] iexp_approx2[of "t * x" n] 377 by (auto simp add: abs_mult field_simps c_def intro!: min.boundedI) 378 qed 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))" 380 unfolding * 381 proof (rule Bochner_Integration.integral_mult_right) 382 show "integrable M (\<lambda>x. min (2 * \<bar>x\<bar> ^ n * real (Suc n)) (\<bar>t\<bar> * \<bar>x\<bar> ^ Suc n))" 383 by (rule Bochner_Integration.integrable_bound[where f="\<lambda>x. 2 * \<bar>x\<bar> ^ n * real (Suc n)"]) 384 (auto simp: integrable_moments power_abs[symmetric] power_mult_distrib) 385 qed 386 finally show ?thesis 387 unfolding integral_mult_right_zero . 388qed 389 390lemma (in real_distribution) char_approx3: 391 fixes t 392 assumes 393 integrable_1: "integrable M (\<lambda>x. x)" and 394 integral_1: "expectation (\<lambda>x. x) = 0" and 395 integrable_2: "integrable M (\<lambda>x. x^2)" and 396 integral_2: "variance (\<lambda>x. x) = \<sigma>2" 397 shows "cmod (char M t - (1 - t^2 * \<sigma>2 / 2)) \<le> 398 (t^2 / 6) * expectation (\<lambda>x. min (6 * x^2) (abs t * (abs x)^3) )" 399proof - 400 note real_distribution.char_approx2 [of M 2 t, simplified] 401 have [simp]: "prob UNIV = 1" by (metis prob_space space_eq_univ) 402 from integral_2 have [simp]: "expectation (\<lambda>x. x * x) = \<sigma>2" 403 by (simp add: integral_1 numeral_eq_Suc) 404 have 1: "k \<le> 2 \<Longrightarrow> integrable M (\<lambda>x. x^k)" for k 405 using assms by (auto simp: eval_nat_numeral le_Suc_eq) 406 note char_approx1 407 note 2 = char_approx1 [of 2 t, OF 1, simplified] 408 have "cmod (char M t - (\<Sum>k\<le>2. (\<i> * t) ^ k * (expectation (\<lambda>x. x ^ k)) / (fact k))) \<le> 409 t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / fact (3::nat)" 410 using char_approx2 [of 2 t, OF 1] by simp 411 also have "(\<Sum>k\<le>2. (\<i> * t) ^ k * expectation (\<lambda>x. x ^ k) / (fact k)) = 1 - t^2 * \<sigma>2 / 2" 412 by (simp add: complex_eq_iff numeral_eq_Suc integral_1 Re_divide Im_divide) 413 also have "fact 3 = 6" by (simp add: eval_nat_numeral) 414 also have "t\<^sup>2 * expectation (\<lambda>x. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3)) / 6 = 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) 416 finally show ?thesis . 417qed 418 419text \<open> 420 This is a more familiar textbook formulation in terms of random variables, but 421 we will use the previous version for the CLT. 422\<close> 423 424lemma (in prob_space) char_approx3': 425 fixes \<mu> :: "real measure" and X 426 assumes rv_X [simp]: "random_variable borel X" 427 and [simp]: "integrable M X" "integrable M (\<lambda>x. (X x)^2)" "expectation X = 0" 428 and var_X: "variance X = \<sigma>2" 429 and \<mu>_def: "\<mu> = distr M borel X" 430 shows "cmod (char \<mu> t - (1 - t^2 * \<sigma>2 / 2)) \<le> 431 (t^2 / 6) * expectation (\<lambda>x. min (6 * (X x)^2) (\<bar>t\<bar> * \<bar>X x\<bar>^3))" 432 using var_X unfolding \<mu>_def 433 apply (subst integral_distr [symmetric, OF rv_X], simp) 434 apply (intro real_distribution.char_approx3) 435 apply (auto simp add: integrable_distr_eq integral_distr) 436 done 437 438text \<open> 439 this is the formulation in the book -- in terms of a random variable *with* the distribution, 440 rather the distribution itself. I don't know which is more useful, though in principal we can 441 go back and forth between them. 442\<close> 443 444lemma (in prob_space) char_approx1': 445 fixes \<mu> :: "real measure" and X 446 assumes integrable_moments : "\<And>k. k \<le> n \<Longrightarrow> integrable M (\<lambda>x. X x ^ k)" 447 and rv_X[measurable]: "random_variable borel X" 448 and \<mu>_distr : "distr M borel X = \<mu>" 449 shows "cmod (char \<mu> t - (\<Sum>k \<le> n. ((\<i> * t)^k / fact k) * expectation (\<lambda>x. (X x)^k))) \<le> 450 (2 * \<bar>t\<bar>^n / fact n) * expectation (\<lambda>x. \<bar>X x\<bar>^n)" 451 unfolding \<mu>_distr[symmetric] 452 apply (subst (1 2) integral_distr [symmetric, OF rv_X], simp, simp) 453 apply (intro real_distribution.char_approx1[of "distr M borel X" n t] real_distribution_distr rv_X) 454 apply (auto simp: integrable_distr_eq integrable_moments) 455 done 456 457subsection \<open>Calculation of the Characteristic Function of the Standard Distribution\<close> 458 459abbreviation 460 "std_normal_distribution \<equiv> density lborel std_normal_density" 461 462(* TODO: should this be an instance statement? *) 463lemma real_dist_normal_dist: "real_distribution std_normal_distribution" 464 using prob_space_normal_density by (auto simp: real_distribution_def real_distribution_axioms_def) 465 466lemma std_normal_distribution_even_moments: 467 fixes k :: nat 468 shows "(LINT x|std_normal_distribution. x^(2 * k)) = fact (2 * k) / (2^k * fact k)" 469 and "integrable std_normal_distribution (\<lambda>x. x^(2 * k))" 470 using integral_std_normal_moment_even[of k] 471 by (subst integral_density) 472 (auto simp: normal_density_nonneg integrable_density 473 intro: integrable.intros std_normal_moment_even) 474 475lemma integrable_std_normal_distribution_moment: "integrable std_normal_distribution (\<lambda>x. x^k)" 476 by (auto simp: normal_density_nonneg integrable_std_normal_moment integrable_density) 477 478lemma integral_std_normal_distribution_moment_odd: 479 "odd k \<Longrightarrow> integral\<^sup>L std_normal_distribution (\<lambda>x. x^k) = 0" 480 using integral_std_normal_moment_odd[of "(k - 1) div 2"] 481 by (auto simp: integral_density normal_density_nonneg elim: oddE) 482 483lemma std_normal_distribution_even_moments_abs: 484 fixes k :: nat 485 shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k)) = fact (2 * k) / (2^k * fact k)" 486 using integral_std_normal_moment_even[of k] 487 by (subst integral_density) (auto simp: normal_density_nonneg power_even_abs) 488 489lemma std_normal_distribution_odd_moments_abs: 490 fixes k :: nat 491 shows "(LINT x|std_normal_distribution. \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2 ^ k * fact k" 492 using integral_std_normal_moment_abs_odd[of k] 493 by (subst integral_density) (auto simp: normal_density_nonneg) 494 495theorem char_std_normal_distribution: 496 "char std_normal_distribution = (\<lambda>t. complex_of_real (exp (- (t^2) / 2)))" 497proof (intro ext LIMSEQ_unique) 498 fix t :: real 499 let ?f' = "\<lambda>k. (\<i> * t)^k / fact k * (LINT x | std_normal_distribution. x^k)" 500 let ?f = "\<lambda>n. (\<Sum>k \<le> n. ?f' k)" 501 show "?f \<longlonglongrightarrow> exp (-(t^2) / 2)" 502 proof (rule limseq_even_odd) 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 504 by (subst power_mult) (simp add: field_simps uminus_power_if power_mult) 505 then have *: "?f (2 * n) = complex_of_real (\<Sum>k < Suc n. (1 / fact k) * (- (t^2) / 2)^k)" for n :: nat 506 unfolding of_real_sum 507 by (intro sum.reindex_bij_witness_not_neutral[symmetric, where 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'="{}"]) 509 (auto simp: integral_std_normal_distribution_moment_odd std_normal_distribution_even_moments) 510 show "(\<lambda>n. ?f (2 * n)) \<longlonglongrightarrow> exp (-(t^2) / 2)" 511 unfolding * using exp_converges[where 'a=real] 512 by (intro tendsto_of_real LIMSEQ_Suc) (auto simp: inverse_eq_divide sums_def [symmetric]) 513 have **: "?f (2 * n + 1) = ?f (2 * n)" for n 514 proof - 515 have "?f (2 * n + 1) = ?f (2 * n) + ?f' (2 * n + 1)" 516 by simp 517 also have "?f' (2 * n + 1) = 0" 518 by (subst integral_std_normal_distribution_moment_odd) simp_all 519 finally show "?f (2 * n + 1) = ?f (2 * n)" 520 by simp 521 qed 522 show "(\<lambda>n. ?f (2 * n + 1)) \<longlonglongrightarrow> exp (-(t^2) / 2)" 523 unfolding ** by fact 524 qed 525 526 have **: "(\<lambda>n. x ^ n / fact n) \<longlonglongrightarrow> 0" for x :: real 527 using summable_LIMSEQ_zero [OF summable_exp] by (auto simp add: inverse_eq_divide) 528 529 let ?F = "\<lambda>n. 2 * \<bar>t\<bar> ^ n / fact n * (LINT x|std_normal_distribution. \<bar>x\<bar> ^ n)" 530 531 show "?f \<longlonglongrightarrow> char std_normal_distribution t" 532 proof (rule metric_tendsto_imp_tendsto[OF limseq_even_odd]) 533 show "(\<lambda>n. ?F (2 * n)) \<longlonglongrightarrow> 0" 534 proof (rule Lim_transform_eventually) 535 show "\<forall>\<^sub>F n in sequentially. 2 * ((t^2 / 2)^n / fact n) = ?F (2 * n)" 536 unfolding std_normal_distribution_even_moments_abs by (simp add: power_mult power_divide) 537 qed (intro tendsto_mult_right_zero **) 538 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 540 unfolding std_normal_distribution_odd_moments_abs 541 by (simp add: field_simps power_mult[symmetric] power_even_abs) 542 have "norm ((2 * t\<^sup>2) ^ n * fact n / fact (2 * n + 1)) \<le> (2 * t\<^sup>2) ^ n / fact n" for n 543 using mult_mono[OF _ square_fact_le_2_fact, of 1 "1 + 2 * real n" n] 544 by (auto simp add: divide_simps intro!: mult_left_mono) 545 then show "(\<lambda>n. ?F (2 * n + 1)) \<longlonglongrightarrow> 0" 546 unfolding * by (intro tendsto_mult_right_zero Lim_null_comparison [OF _ ** [of "2 * t\<^sup>2"]]) auto 547 548 show "\<forall>\<^sub>F n in sequentially. dist (?f n) (char std_normal_distribution t) \<le> dist (?F n) 0" 549 using real_distribution.char_approx1[OF real_dist_normal_dist integrable_std_normal_distribution_moment] 550 by (auto simp: dist_norm integral_nonneg_AE norm_minus_commute) 551 qed 552qed 553 554end 555