# HG changeset patch
# User hoelzl
# Date 1475502368 -7200
# Node ID a5d293f1af80f95707d67d749ab56da0258737c6
# Parent  17a20ca86d62037d2b31bd8f49d1673ba07a1680
Probability: variant of central limit theorem with non-zero mean

diff -r 17a20ca86d62 -r a5d293f1af80 src/HOL/Probability/Central_Limit_Theorem.thy
--- a/src/HOL/Probability/Central_Limit_Theorem.thy	Fri Sep 30 16:08:38 2016 +0200
+++ b/src/HOL/Probability/Central_Limit_Theorem.thy	Mon Oct 03 15:46:08 2016 +0200
@@ -8,7 +8,7 @@
   imports Levy
 begin
 
-theorem (in prob_space) central_limit_theorem:
+theorem (in prob_space) central_limit_theorem_zero_mean:
   fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
     and \<mu> :: "real measure"
     and \<sigma> :: real
@@ -114,4 +114,31 @@
   qed (auto intro!: real_dist_normal_dist simp: S_def)
 qed
 
+theorem (in prob_space) central_limit_theorem:
+  fixes X :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+    and \<mu> :: "real measure"
+    and \<sigma> :: real
+    and S :: "nat \<Rightarrow> 'a \<Rightarrow> real"
+  assumes X_indep: "indep_vars (\<lambda>i. borel) X UNIV"
+    and X_integrable: "\<And>n. integrable M (X n)"
+    and X_mean: "\<And>n. expectation (X n) = m"
+    and \<sigma>_pos: "\<sigma> > 0"
+    and X_square_integrable: "\<And>n. integrable M (\<lambda>x. (X n x)\<^sup>2)"
+    and X_variance: "\<And>n. variance (X n) = \<sigma>\<^sup>2"
+    and X_distrib: "\<And>n. distr M borel (X n) = \<mu>"
+  defines "X' i x \<equiv> X i x - m"
+  shows "weak_conv_m (\<lambda>n. distr M borel (\<lambda>x. (\<Sum>i<n. X' i x) / sqrt (n*\<sigma>\<^sup>2))) std_normal_distribution"
+proof (intro central_limit_theorem_zero_mean)
+  show "indep_vars (\<lambda>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 "\<sigma> > 0" "integrable M (\<lambda>x. (X' n x)\<^sup>2)" "variance (X' n) = \<sigma>\<^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 \<mu> borel (\<lambda>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