(* Title: HOL/Probability/Central_Limit_Theorem.thy
Authors: Jeremy Avigad (CMU), Luke Serafin (CMU)
*)
section \<open>The Central Limit Theorem\<close>
theory Central_Limit_Theorem
imports Levy
begin
theorem (in prob_space) central_limit_theorem_zero_mean:
fixes X :: "nat \ 'a \ real"
and \<mu> :: "real measure"
and \<sigma> :: real
and S :: "nat \ 'a \ real"
assumes X_indep: "indep_vars (\i. borel) X UNIV"
and X_integrable: "\n. integrable M (X n)"
and X_mean_0: "\n. expectation (X n) = 0"
and \<sigma>_pos: "\<sigma> > 0"
and X_square_integrable: "\n. integrable M (\x. (X n x)\<^sup>2)"
and X_variance: "\n. variance (X n) = \\<^sup>2"
and X_distrib: "\n. distr M borel (X n) = \"
defines "S n \ \x. \i
shows "weak_conv_m (\n. distr M borel (\x. S n x / sqrt (n * \\<^sup>2))) std_normal_distribution"
proof -
let ?S' = "\n x. S n x / sqrt (real n * \\<^sup>2)"
define \<phi> where "\<phi> n = char (distr M borel (?S' n))" for n
define \<psi> where "\<psi> n t = char \<mu> (t / sqrt (\<sigma>\<^sup>2 * n))" for n t
have X_rv [simp, measurable]: "\n. random_variable borel (X n)"
using X_indep unfolding indep_vars_def2 by simp
interpret \<mu>: real_distribution \<mu>
by (subst X_distrib [symmetric, of 0], rule real_distribution_distr, simp)
(* these are equivalent to the hypotheses on X, given X_distr *)
have \<mu>_integrable [simp]: "integrable \<mu> (\<lambda>x. x)"
and \<mu>_mean_integrable [simp]: "\<mu>.expectation (\<lambda>x. x) = 0"
and \<mu>_square_integrable [simp]: "integrable \<mu> (\<lambda>x. x^2)"
and \<mu>_variance [simp]: "\<mu>.expectation (\<lambda>x. x^2) = \<sigma>\<^sup>2"
using assms by (simp_all add: X_distrib [symmetric, of 0] integrable_distr_eq integral_distr)
have main: "\\<^sub>F n in sequentially.
cmod (\<phi> n t - (1 + (-(t^2) / 2) / n)^n) \<le>
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
proof (rule eventually_sequentiallyI)
fix n :: nat
assume "n \ nat (ceiling (t^2 / 4))"
hence n: "n \ t^2 / 4" by (subst nat_ceiling_le_eq [symmetric])
let ?t = "t / sqrt (\\<^sup>2 * n)"
define \<psi>' where "\<psi>' n i = char (distr M borel (\<lambda>x. X i x / sqrt (\<sigma>\<^sup>2 * n)))" for n i
have *: "\n i t. \' n i t = \ n t"
unfolding \<psi>_def \<psi>'_def char_def
by (subst X_distrib [symmetric]) (auto simp: integral_distr)
have "\ n t = char (distr M borel (\x. \i\<^sup>2 * real n))) t"
by (auto simp: \<phi>_def S_def sum_divide_distrib ac_simps)
also have "\ = (\ i < n. \' n i t)"
unfolding \<psi>'_def
apply (rule char_distr_sum)
apply (rule indep_vars_compose2[where X=X])
apply (rule indep_vars_subset)
apply (rule X_indep)
apply auto
done
also have "\ = (\ n t)^n"
by (auto simp add: * prod_constant)
finally have \<phi>_eq: "\<phi> n t =(\<psi> n t)^n" .
have "norm (\ n t - (1 - ?t^2 * \\<^sup>2 / 2)) \ ?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3))"
unfolding \<psi>_def by (rule \<mu>.char_approx3, auto)
also have "?t^2 * \\<^sup>2 = t^2 / n"
using \<sigma>_pos by (simp add: power_divide)
also have "t^2 / n / 2 = (t^2 / 2) / n"
by simp
finally have **: "norm (\ n t - (1 + (-(t^2) / 2) / n)) \
?t\<^sup>2 / 6 * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3))" by simp
have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \
n * norm (\<psi> n t - (complex_of_real (1 + (-(t^2) / 2) / n)))"
using n
by (auto intro!: norm_power_diff \<mu>.cmod_char_le_1 abs_leI
simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \<phi>_eq \<psi>_def)
also have "\ \ n * (?t\<^sup>2 / 6 * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))"
by (rule mult_left_mono [OF **], simp)
also have "\ = (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3)))"
using \<sigma>_pos by (simp add: field_simps min_absorb2)
finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \
(t\<^sup>2 / (6 * \<sigma>\<^sup>2) * (LINT x|\<mu>. min (6 * x\<^sup>2) (\<bar>?t\<bar> * \<bar>x\<bar> ^ 3)))"
by simp
qed
show ?thesis
proof (rule levy_continuity)
fix t
let ?t = "\n. t / sqrt (\\<^sup>2 * n)"
have "\x. (\n. min (6 * x\<^sup>2) (\t\ * \x\ ^ 3 / \sqrt (\\<^sup>2 * real n)\)) \ 0"
using \<sigma>_pos
by (auto simp: real_sqrt_mult min_absorb2
intro!: tendsto_min[THEN tendsto_eq_rhs] sqrt_at_top[THEN filterlim_compose]
filterlim_tendsto_pos_mult_at_top filterlim_at_top_imp_at_infinity
tendsto_divide_0 filterlim_real_sequentially)
then have "(\n. LINT x|\. min (6 * x\<^sup>2) (\?t n\ * \x\ ^ 3)) \ (LINT x|\. 0)"
by (intro integral_dominated_convergence [where w = "\x. 6 * x^2"]) auto
then have *: "(\n. t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t n\ * \x\ ^ 3))) \ 0"
by (simp only: integral_zero tendsto_mult_right_zero)
have "(\n. complex_of_real ((1 + (-(t^2) / 2) / n)^n)) \ complex_of_real (exp (-(t^2) / 2))"
by (rule isCont_tendsto_compose [OF _ tendsto_exp_limit_sequentially]) auto
then have "(\n. \ n t) \ complex_of_real (exp (-(t^2) / 2))"
by (rule Lim_transform) (rule Lim_null_comparison [OF main *])
then show "(\n. char (distr M borel (?S' n)) t) \ char std_normal_distribution t"
by (simp add: \<phi>_def char_std_normal_distribution)
qed (auto intro!: real_dist_normal_dist simp: S_def)
qed
theorem (in prob_space) central_limit_theorem:
fixes X :: "nat \ 'a \ real"
and \<mu> :: "real measure"
and \<sigma> :: real
and S :: "nat \ 'a \ real"
assumes X_indep: "indep_vars (\i. borel) X UNIV"
and X_integrable: "\n. integrable M (X n)"
and X_mean: "\n. expectation (X n) = m"
and \<sigma>_pos: "\<sigma> > 0"
and X_square_integrable: "\n. integrable M (\x. (X n x)\<^sup>2)"
and X_variance: "\n. variance (X n) = \\<^sup>2"
and X_distrib: "\n. distr M borel (X n) = \"
defines "X' i x \ X i x - m"
shows "weak_conv_m (\n. distr M borel (\x. (\i\<^sup>2))) std_normal_distribution"
proof (intro central_limit_theorem_zero_mean)
show "indep_vars (\i. borel) X' UNIV"
unfolding X'_def[abs_def] using X_indep by (rule indep_vars_compose2) auto
show "integrable M (X' n)" "expectation (X' n) = 0" for n
using X_integrable X_mean by (auto simp: X'_def[abs_def] prob_space)
show "\ > 0" "integrable M (\x. (X' n x)\<^sup>2)" "variance (X' n) = \\<^sup>2" for n
using \<open>0 < \<sigma>\<close> X_integrable X_mean X_square_integrable X_variance unfolding X'_def
by (auto simp: prob_space power2_diff)
show "distr M borel (X' n) = distr \ borel (\x. x - m)" for n
unfolding X_distrib[of n, symmetric] using X_integrable
by (subst distr_distr) (auto simp: X'_def[abs_def] comp_def)
qed
end
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
