isabelle: src/HOL/Probability/Central_Limit_Theorem.thy@d3996d5873dd (annotated)

62083 7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	1	(* Theory: Central_Limit_Theorem.thy
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	2	Authors: Jeremy Avigad, Luke Serafin
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>The Central Limit Theorem\<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 Central_Limit_Theorem
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	8	imports Levy
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	theorem (in prob_space) central_limit_theorem:
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	12	fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	13	and \<mu> :: "real measure"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	14	and \<sigma> :: real
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	15	and S :: "nat \<Rightarrow> 'a \<Rightarrow> real"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	16	assumes X_indep: "indep_vars (\<lambda>i. borel) X UNIV"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	17	and X_integrable: "\<And>n. integrable M (X n)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	18	and X_mean_0: "\<And>n. expectation (X n) = 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	19	and \<sigma>_pos: "\<sigma> > 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	20	and X_square_integrable: "\<And>n. integrable M (\<lambda>x. (X n x)\<^sup>2)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	21	and X_variance: "\<And>n. variance (X n) = \<sigma>\<^sup>2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	22	and X_distrib: "\<And>n. distr M borel (X n) = \<mu>"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	23	defines "S n \<equiv> \<lambda>x. \<Sum>i<n. X i x"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	24	shows "weak_conv_m (\<lambda>n. distr M borel (\<lambda>x. S n x / sqrt (n * \<sigma>\<^sup>2))) std_normal_distribution"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	25	proof -
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	26	let ?S' = "\<lambda>n x. S n x / sqrt (real n * \<sigma>\<^sup>2)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	27	def \<phi> \<equiv> "\<lambda>n. char (distr M borel (?S' n))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	28	def \<psi> \<equiv> "\<lambda>n t. char \<mu> (t / sqrt (\<sigma>\<^sup>2 * n))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	29
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	30	have X_rv [simp, measurable]: "\<And>n. random_variable borel (X n)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	31	using X_indep unfolding indep_vars_def2 by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	32	interpret \<mu>: real_distribution \<mu>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	33	by (subst X_distrib [symmetric, of 0], rule real_distribution_distr, simp)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	34
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	35	(* these are equivalent to the hypotheses on X, given X_distr *)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	36	have \<mu>_integrable [simp]: "integrable \<mu> (\<lambda>x. x)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	37	and \<mu>_mean_integrable [simp]: "\<mu>.expectation (\<lambda>x. x) = 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	38	and \<mu>_square_integrable [simp]: "integrable \<mu> (\<lambda>x. x^2)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	39	and \<mu>_variance [simp]: "\<mu>.expectation (\<lambda>x. x^2) = \<sigma>\<^sup>2"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	40	using assms by (simp_all add: X_distrib [symmetric, of 0] integrable_distr_eq integral_distr)
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	have main: "\<forall>\<^sub>F n in sequentially.
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	43	cmod (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	44	t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>t / sqrt (\<sigma>\<^sup>2 * n)\<bar> * \<bar>x\<bar> ^ 3))" for t
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	45	proof (rule eventually_sequentiallyI)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	46	fix n :: nat
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	47	assume "n \<ge> nat (ceiling (t^2 / 4))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	48	hence n: "n \<ge> t^2 / 4" by (subst nat_ceiling_le_eq [symmetric])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	49	let ?t = "t / sqrt (\<sigma>\<^sup>2 * n)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	50
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	51	def \<psi>' \<equiv> "\<lambda>n i. char (distr M borel (\<lambda>x. X i x / sqrt (\<sigma>\<^sup>2 * n)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	52	have *: "\<And>n i t. \<psi>' n i t = \<psi> n t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	53	unfolding \<psi>_def \<psi>'_def char_def
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	54	by (subst X_distrib [symmetric]) (auto simp: integral_distr)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	55
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	56	have "\<phi> n t = char (distr M borel (\<lambda>x. \<Sum>i<n. X i x / sqrt (\<sigma>\<^sup>2 * real n))) t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	57	by (auto simp: \<phi>_def S_def setsum_divide_distrib ac_simps)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	58	also have "\<dots> = (\<Prod> i < n. \<psi>' n i t)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	59	unfolding \<psi>'_def
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	60	apply (rule char_distr_setsum)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	61	apply (rule indep_vars_compose2[where X=X])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	62	apply (rule indep_vars_subset)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	63	apply (rule X_indep)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	64	apply auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	65	done
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	66	also have "\<dots> = (\<psi> n t)^n"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	67	by (auto simp add: * setprod_constant)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	68	finally have \<phi>_eq: "\<phi> n t =(\<psi> n t)^n" .
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	69
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	70	have "norm (\<psi> n t - (1 - ?t^2 * \<sigma>\<^sup>2 / 2)) \<le> ?t\<^sup>2 / 6 * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	71	unfolding \<psi>_def by (rule \<mu>.char_approx3, auto)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	72	also have "?t^2 * \<sigma>\<^sup>2 = t^2 / n"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	73	using \<sigma>_pos by (simp add: power_divide)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	74	also have "t^2 / n / 2 = (t^2 / 2) / n"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	75	by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	76	finally have **: "norm (\<psi> n t - (1 + (-(t^2) / 2) / n)) \<le>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	77	?t\<^sup>2 / 6 * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))" by simp
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	78
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	79	have "norm (\<phi> n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \<le>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	80	n * norm (\<psi> n t - (complex_of_real (1 + (-(t^2) / 2) / n)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	81	using n
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	82	by (auto intro!: norm_power_diff \<mu>.cmod_char_le_1 abs_leI
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	83	simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \<phi>_eq \<psi>_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	84	also have "\<dots> \<le> n * (?t\<^sup>2 / 6 * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	85	by (rule mult_left_mono [OF **], simp)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	86	also have "\<dots> = (t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	87	using \<sigma>_pos by (simp add: field_simps min_absorb2)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	88	finally show "norm (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	89	(t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	90	by simp
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	show ?thesis
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	94	proof (rule levy_continuity)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	95	fix t
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	96	let ?t = "\<lambda>n. t / sqrt (\<sigma>\<^sup>2 * n)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	97	have "\<And>x. (\<lambda>n. min (6 * x\<^sup>2) (\<bar>t\<bar> * \<bar>x\<bar> ^ 3 / \<bar>sqrt (\<sigma>\<^sup>2 * real n)\<bar>)) \<longlonglongrightarrow> 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	98	using \<sigma>_pos
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	99	by (auto simp: real_sqrt_mult min_absorb2
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	100	intro!: tendsto_min[THEN tendsto_eq_rhs] sqrt_at_top[THEN filterlim_compose]
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	101	filterlim_tendsto_pos_mult_at_top filterlim_at_top_imp_at_infinity
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	102	tendsto_divide_0 filterlim_real_sequentially)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	103	then have "(\<lambda>n. LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t n\<bar> * \<bar>x\<bar> ^ 3)) \<longlonglongrightarrow> (LINT x\|\<mu>. 0)"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	104	by (intro integral_dominated_convergence [where w = "\<lambda>x. 6 * x^2"]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	105	then have : "(\<lambda>n. t\<^sup>2 / (6 \<sigma>\<^sup>2) * (LINT x\|\<mu>. min (6 * x\<^sup>2) (\<bar>?t n\<bar> * \<bar>x\<bar> ^ 3))) \<longlonglongrightarrow> 0"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	106	by (simp only: integral_zero tendsto_mult_right_zero)
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 "(\<lambda>n. complex_of_real ((1 + (-(t^2) / 2) / n)^n)) \<longlonglongrightarrow> complex_of_real (exp (-(t^2) / 2))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	109	by (rule isCont_tendsto_compose [OF _ tendsto_exp_limit_sequentially]) auto
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	110	then have "(\<lambda>n. \<phi> n t) \<longlonglongrightarrow> complex_of_real (exp (-(t^2) / 2))"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	111	by (rule Lim_transform) (rule Lim_null_comparison [OF main *])
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	112	then show "(\<lambda>n. char (distr M borel (?S' n)) t) \<longlonglongrightarrow> char std_normal_distribution t"
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	113	by (simp add: \<phi>_def char_std_normal_distribution)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	114	qed (auto intro!: real_dist_normal_dist simp: S_def)
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	115	qed
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	116
7582b39f51ed add the proof of the central limit theorem hoelzl parents: diff changeset	117	end

author	wenzelm
	Mon, 15 Feb 2016 14:55:44 +0100
changeset 62337	d3996d5873dd
parent 62083	7582b39f51ed
child 63040	eb4ddd18d635
permissions	-rw-r--r--