Quelle Central_Limit_Theorem.thy Sprache: Isabelle

(*  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_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]: "random_variable borel (X n)" for n
    using X_indep unfolding indep_vars_def2 by simp
  have X_integrable [simp, intro]: "integrable M (X n)" for n
    by (rule square_integrable_imp_integrable[OF _ X_square_integrable]) simp_all
  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_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
  have X_rv [simp, measurable]: "random_variable borel (X n)" for n
    using X_indep unfolding indep_vars_def2 by simp
  have X_integrable [simp, intro]: "integrable M (X n)" for n
    by (rule square_integrable_imp_integrable[OF _ X_square_integrable]) simp_all
  show "expectation (X' n) = 0" for n
    using 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

quality98%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.