isabelle: src/HOL/Probability/Characteristic_Functions.thy@8d93f9ca6518 (annotated)

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

author	blanchet
	Tue, 13 Jul 2021 10:57:15 +0200
changeset 73975	8d93f9ca6518
parent 70365	4df0628e8545
child 75462	7448423e5dba
permissions	-rw-r--r--