# avigad/isabelle

Switch branches/tags
Nothing to show
Fetching contributors…
Cannot retrieve contributors at this time
118 lines (104 sloc) 6.32 KB
 (* Theory: Central_Limit_Theorem.thy Authors: Jeremy Avigad, Luke Serafin *) section \The Central Limit Theorem\ theory Central_Limit_Theorem imports Levy begin theorem (in prob_space) central_limit_theorem: fixes X :: "nat \ 'a \ real" and \ :: "real measure" and \ :: 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 \_pos: "\ > 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. \in. 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)" def \ \ "\n. char (distr M borel (?S' n))" def \ \ "\n t. char \ (t / sqrt (\\<^sup>2 * n))" have X_rv [simp, measurable]: "\n. random_variable borel (X n)" using X_indep unfolding indep_vars_def2 by simp interpret \: real_distribution \ by (subst X_distrib [symmetric, of 0], rule real_distribution_distr, simp) (* these are equivalent to the hypotheses on X, given X_distr *) have \_integrable [simp]: "integrable \ (\x. x)" and \_mean_integrable [simp]: "\.expectation (\x. x) = 0" and \_square_integrable [simp]: "integrable \ (\x. x^2)" and \_variance [simp]: "\.expectation (\x. x^2) = \\<^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 (\ n t - (1 + (-(t^2) / 2) / n)^n) \ t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\t / sqrt (\\<^sup>2 * n)\ * \x\ ^ 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)" def \' \ "\n i. char (distr M borel (\x. X i x / sqrt (\\<^sup>2 * n)))" have *: "\n i t. \' n i t = \ n t" unfolding \_def \'_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: \_def S_def setsum_divide_distrib ac_simps) also have "\ = (\ i < n. \' n i t)" unfolding \'_def apply (rule char_distr_setsum) 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: * setprod_constant) finally have \_eq: "\ n t =(\ 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 \_def by (rule \.char_approx3, auto) also have "?t^2 * \\<^sup>2 = t^2 / n" using \_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|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 3))" by simp have "norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n))^n) \ n * norm (\ n t - (complex_of_real (1 + (-(t^2) / 2) / n)))" using n by (auto intro!: norm_power_diff \.cmod_char_le_1 abs_leI simp del: of_real_diff simp: of_real_diff[symmetric] divide_le_eq \_eq \_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 \_pos by (simp add: field_simps min_absorb2) finally show "norm (\ n t - (1 + (-(t^2) / 2) / n)^n) \ (t\<^sup>2 / (6 * \\<^sup>2) * (LINT x|\. min (6 * x\<^sup>2) (\?t\ * \x\ ^ 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 \_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: \_def char_std_normal_distribution) qed (auto intro!: real_dist_normal_dist simp: S_def) qed end