properties of normal distributed random variables (by Sudeep Kanav)
authorhoelzl
Fri Jun 13 14:08:20 2014 +0200 (2014-06-13)
changeset 5725219b7ace1c5da
parent 57251 f51985ebd152
child 57253 6515cf25de13
properties of normal distributed random variables (by Sudeep Kanav)
CONTRIBUTORS
NEWS
src/HOL/Probability/Distributions.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Probability.thy
     1.1 --- a/CONTRIBUTORS	Fri Jun 13 07:05:01 2014 +0200
     1.2 +++ b/CONTRIBUTORS	Fri Jun 13 14:08:20 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    Waldmeister, etc.).
     1.5  
     1.6  * June 2014: Sudeep Kanav, TUM, and Johannes Hölzl, TUM
     1.7 -  Various properties of Erlang and exponentially distributed random variables.
     1.8 +  Various properties of exponentially, Erlang, and normal distributed random variables.
     1.9  
    1.10  * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM
    1.11    SML-based engines for MaSh.
     2.1 --- a/NEWS	Fri Jun 13 07:05:01 2014 +0200
     2.2 +++ b/NEWS	Fri Jun 13 14:08:20 2014 +0200
     2.3 @@ -757,6 +757,9 @@
     2.4  
     2.5      * Renamed abbreviation integral\<^sup>P to integral\<^sup>N.
     2.6  
     2.7 +  - Formalized properties about exponentially, Erlang, and normal distributed
     2.8 +    random variables.
     2.9 +
    2.10  * Library/Kleene-Algebra was removed because AFP/Kleene_Algebra subsumes it.
    2.11  
    2.12  *** Scala ***
     3.1 --- a/src/HOL/Probability/Distributions.thy	Fri Jun 13 07:05:01 2014 +0200
     3.2 +++ b/src/HOL/Probability/Distributions.thy	Fri Jun 13 14:08:20 2014 +0200
     3.3 @@ -5,9 +5,120 @@
     3.4  header {* Properties of Various Distributions *}
     3.5  
     3.6  theory Distributions
     3.7 -  imports Probability_Measure Convolution
     3.8 +  imports Convolution Information
     3.9  begin
    3.10  
    3.11 +lemma nn_integral_even_function:
    3.12 +  fixes f :: "real \<Rightarrow> ereal"
    3.13 +  assumes [measurable]: "f \<in> borel_measurable borel"
    3.14 +  assumes even: "\<And>x. f x = f (- x)"
    3.15 +  shows "(\<integral>\<^sup>+x. f x \<partial>lborel) = 2 * (\<integral>\<^sup>+x. f x * indicator {0 ..} x \<partial>lborel)"
    3.16 +proof -
    3.17 +  def f' \<equiv> "\<lambda>x. max 0 (f x)"
    3.18 +  have [measurable]: "f' \<in> borel_measurable borel"
    3.19 +    by (simp add: f'_def)
    3.20 +  
    3.21 +  { fix x :: ereal have "2 * x = x + x"
    3.22 +      by (cases x) auto }
    3.23 +  note two_mult = this
    3.24 +
    3.25 +  have "(\<integral>\<^sup>+x. f x \<partial>lborel) = (\<integral>\<^sup>+x. f' x \<partial>lborel)"
    3.26 +    unfolding f'_def nn_integral_max_0 ..
    3.27 +  also have "\<dots> = (\<integral>\<^sup>+x. f' x * indicator {0 ..} x + f' x * indicator {.. 0} x \<partial>lborel)"
    3.28 +    by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator_asm)
    3.29 +  also have "\<dots> = (\<integral>\<^sup>+x. f' x * indicator {0 ..} x \<partial>lborel) + (\<integral>\<^sup>+x. f' x * indicator {.. 0} x \<partial>lborel)"
    3.30 +    by (intro nn_integral_add) (auto simp: f'_def)
    3.31 +  also have "(\<integral>\<^sup>+x. f' x * indicator {.. 0} x \<partial>lborel) = (\<integral>\<^sup>+x. f' x * indicator {0 ..} x \<partial>lborel)"
    3.32 +    using even
    3.33 +    by (subst nn_integral_real_affine[where c="-1" and t=0])
    3.34 +       (auto simp: f'_def one_ereal_def[symmetric] split: split_indicator intro!: nn_integral_cong)
    3.35 +  also have "(\<integral>\<^sup>+x. f' x * indicator {0 ..} x \<partial>lborel) = (\<integral>\<^sup>+x. f x * indicator {0 ..} x \<partial>lborel)"
    3.36 +    unfolding f'_def by (subst (2) nn_integral_max_0[symmetric]) (auto intro!: nn_integral_cong split: split_indicator split_max)
    3.37 +  finally show ?thesis
    3.38 +    unfolding two_mult by simp
    3.39 +qed
    3.40 +
    3.41 +lemma filterlim_power2_at_top[intro]: "filterlim (\<lambda>(x::real). x\<^sup>2) at_top at_top"
    3.42 +  by (auto intro!: filterlim_at_top_mult_at_top filterlim_ident simp: power2_eq_square)
    3.43 +
    3.44 +lemma distributed_integrable_var:
    3.45 +  fixes X :: "'a \<Rightarrow> real"
    3.46 +  shows "distributed M lborel X (\<lambda>x. ereal (f x)) \<Longrightarrow> integrable lborel (\<lambda>x. f x * x) \<Longrightarrow> integrable M X"
    3.47 +  using distributed_integrable[of M lborel X f "\<lambda>x. x"] by simp
    3.48 +
    3.49 +lemma (in ordered_comm_monoid_add) setsum_pos: 
    3.50 +  "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 < f i) \<Longrightarrow> 0 < setsum f I"
    3.51 +  by (induct I rule: finite_ne_induct) (auto intro: add_pos_pos)
    3.52 +
    3.53 +lemma ln_sqrt: "0 < x \<Longrightarrow> ln (sqrt x) = ln x / 2"
    3.54 +  by (simp add: ln_powr powr_numeral ln_powr[symmetric] mult_commute)
    3.55 +
    3.56 +lemma distr_cong: "M = K \<Longrightarrow> sets N = sets L \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> distr M N f = distr K L g"
    3.57 +  using sets_eq_imp_space_eq[of N L] by (simp add: distr_def Int_def cong: rev_conj_cong)
    3.58 +
    3.59 +lemma AE_borel_affine: 
    3.60 +  fixes P :: "real \<Rightarrow> bool"
    3.61 +  shows "c \<noteq> 0 \<Longrightarrow> Measurable.pred borel P \<Longrightarrow> AE x in lborel. P x \<Longrightarrow> AE x in lborel. P (t + c * x)"
    3.62 +  by (subst lborel_real_affine[where t="- t / c" and c="1 / c"])
    3.63 +     (simp_all add: AE_density AE_distr_iff field_simps)
    3.64 +
    3.65 +lemma density_distr:
    3.66 +  assumes [measurable]: "f \<in> borel_measurable N" "X \<in> measurable M N"
    3.67 +  shows "density (distr M N X) f = distr (density M (\<lambda>x. f (X x))) N X"
    3.68 +  by (intro measure_eqI)
    3.69 +     (auto simp add: emeasure_density nn_integral_distr emeasure_distr
    3.70 +           split: split_indicator intro!: nn_integral_cong)
    3.71 +
    3.72 +lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
    3.73 +  by (simp split: split_indicator)
    3.74 +
    3.75 +lemma (in prob_space) distributed_affine:
    3.76 +  fixes f :: "real \<Rightarrow> ereal"
    3.77 +  assumes f: "distributed M lborel X f"
    3.78 +  assumes c: "c \<noteq> 0"
    3.79 +  shows "distributed M lborel (\<lambda>x. t + c * X x) (\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>)"
    3.80 +  unfolding distributed_def
    3.81 +proof safe
    3.82 +  have [measurable]: "f \<in> borel_measurable borel"
    3.83 +    using f by (simp add: distributed_def)
    3.84 +  have [measurable]: "X \<in> borel_measurable M"
    3.85 +    using f by (simp add: distributed_def)
    3.86 +
    3.87 +  show "(\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>) \<in> borel_measurable lborel"
    3.88 +    by simp
    3.89 +  show "random_variable lborel (\<lambda>x. t + c * X x)"
    3.90 +    by simp
    3.91 +  
    3.92 +  have "AE x in lborel. 0 \<le> f x"
    3.93 +    using f by (simp add: distributed_def)
    3.94 +  from AE_borel_affine[OF _ _ this, where c="1/c" and t="- t / c"] c
    3.95 +  show "AE x in lborel. 0 \<le> f ((x - t) / c) / ereal \<bar>c\<bar>"
    3.96 +    by (auto simp add: field_simps)
    3.97 +
    3.98 +  have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
    3.99 +    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
   3.100 +    
   3.101 +  have "density lborel f = distr M lborel X"
   3.102 +    using f by (simp add: distributed_def)
   3.103 +  with c show "distr M lborel (\<lambda>x. t + c * X x) = density lborel (\<lambda>x. f ((x - t) / c) / ereal \<bar>c\<bar>)"
   3.104 +    by (subst (2) lborel_real_affine[where c="c" and t="t"])
   3.105 +       (simp_all add: density_density_eq density_distr distr_distr field_simps eq cong: distr_cong)
   3.106 +qed
   3.107 +
   3.108 +lemma (in prob_space) distributed_affineI:
   3.109 +  fixes f :: "real \<Rightarrow> ereal"
   3.110 +  assumes f: "distributed M lborel (\<lambda>x. (X x - t) / c) (\<lambda>x. \<bar>c\<bar> * f (x * c + t))"
   3.111 +  assumes c: "c \<noteq> 0"
   3.112 +  shows "distributed M lborel X f"
   3.113 +proof -
   3.114 +  have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
   3.115 +    using c by (simp add: divide_ereal_def mult_ac one_ereal_def[symmetric])
   3.116 +
   3.117 +  show ?thesis
   3.118 +    using distributed_affine[OF f c, where t=t] c
   3.119 +    by (simp add: field_simps eq)
   3.120 +qed
   3.121 +
   3.122  lemma measure_lebesgue_Icc: "measure lebesgue {a .. b} = (if a \<le> b then b - a else 0)"
   3.123    by (auto simp: measure_def)
   3.124  
   3.125 @@ -571,6 +682,35 @@
   3.126    from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp
   3.127  qed
   3.128  
   3.129 +lemma (in information_space) entropy_exponential:
   3.130 +  assumes D: "distributed M lborel X (exponential_density l)"
   3.131 +  shows "entropy b lborel X = log b (exp 1 / l)"
   3.132 +proof -
   3.133 +  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
   3.134 + 
   3.135 +  have [simp]: "integrable lborel (exponential_density l)"
   3.136 +    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
   3.137 +
   3.138 +  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
   3.139 +    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
   3.140 +    
   3.141 +  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
   3.142 +    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
   3.143 +
   3.144 +  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
   3.145 +    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
   3.146 +    
   3.147 +  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
   3.148 +    using D by (rule entropy_distr)
   3.149 +  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
   3.150 +    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
   3.151 +    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
   3.152 +  also have "\<dots> = (ln l - 1) / ln b"
   3.153 +    by simp
   3.154 +  finally show ?thesis
   3.155 +    by (simp add: log_def divide_simps ln_div)
   3.156 +qed
   3.157 +
   3.158  subsection {* Uniform distribution *}
   3.159  
   3.160  lemma uniform_distrI:
   3.161 @@ -755,4 +895,561 @@
   3.162    finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
   3.163  qed fact
   3.164  
   3.165 +subsection {* Normal distribution *}
   3.166 +
   3.167 +definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   3.168 +  "normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp (-(x - \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))"
   3.169 +
   3.170 +abbreviation std_normal_density :: "real \<Rightarrow> real" where
   3.171 +  "std_normal_density \<equiv> normal_density 0 1"
   3.172 +
   3.173 +lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp (- x\<^sup>2 / 2)"
   3.174 +  unfolding normal_density_def by simp
   3.175 +
   3.176 +lemma borel_measurable_normal_density[measurable]: "normal_density \<mu> \<sigma> \<in> borel_measurable borel"
   3.177 +  by (auto simp: normal_density_def[abs_def])
   3.178 +
   3.179 +lemma nn_integral_gaussian: "(\<integral>\<^sup>+x. (exp (- x\<^sup>2)) \<partial>lborel) = sqrt pi"
   3.180 +proof -
   3.181 +  let ?pI = "\<lambda>f. (\<integral>\<^sup>+s. f (s::real) * indicator {0..} s \<partial>lborel)"
   3.182 +  let ?gauss = "\<lambda>x. exp (- x\<^sup>2)"
   3.183 +
   3.184 +  have "?pI ?gauss * ?pI ?gauss = ?pI (\<lambda>s. ?pI (\<lambda>x. ereal (x * exp (-x\<^sup>2 * (1 + s\<^sup>2)))))"
   3.185 +  proof-
   3.186 +    let ?ff= "\<lambda>(x, s). ((x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) * indicator {0<..} s * indicator {0<..} x)) :: real"
   3.187 +  
   3.188 +    have *: "?pI ?gauss = (\<integral>\<^sup>+x. ?gauss x * indicator {0<..} x \<partial>lborel)"
   3.189 +      by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator)
   3.190 +  
   3.191 +    have "?pI ?gauss * ?pI ?gauss = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?ff (x, s) \<partial>lborel \<partial>lborel)"
   3.192 +      unfolding *
   3.193 +      apply (auto simp: nn_integral_nonneg nn_integral_cmult[symmetric])
   3.194 +      apply (auto intro!: nn_integral_cong split:split_indicator)
   3.195 +      apply (auto simp: nn_integral_multc[symmetric])
   3.196 +      apply (subst nn_integral_real_affine[where t="0" and c="x"])
   3.197 +      by (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff
   3.198 +          intro!: nn_integral_cong split:split_indicator)
   3.199 +    also have "... = \<integral>\<^sup>+ (s::real). \<integral>\<^sup>+ (x::real). ?ff (x, s) \<partial>lborel \<partial>lborel"
   3.200 +      by (rule lborel_pair.Fubini[symmetric]) auto
   3.201 +    also have "... = ?pI (\<lambda>s. ?pI (\<lambda>x. ereal (x * exp (-x\<^sup>2 * (1 + s\<^sup>2)))))"
   3.202 +      by (rule nn_integral_cong_AE) (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm)
   3.203 +    finally show ?thesis
   3.204 +      by simp
   3.205 +  qed
   3.206 +  also have "\<dots> = ?pI (\<lambda>s. ereal (1 / (2 * (1 + s\<^sup>2))))"
   3.207 +  proof (intro nn_integral_cong ereal_right_mult_cong)
   3.208 +    fix s :: real show "?pI (\<lambda>x. ereal (x * exp (-x\<^sup>2 * (1 + s\<^sup>2)))) = ereal (1 / (2 * (1 + s\<^sup>2)))"
   3.209 +    proof (subst nn_integral_FTC_atLeast)
   3.210 +      have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top"
   3.211 +        apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   3.212 +        apply (subst mult_commute)         
   3.213 +        by (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] 
   3.214 +          simp: add_pos_nonneg  power2_eq_square add_nonneg_eq_0_iff)
   3.215 +      then show "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top"
   3.216 +        by (simp add: field_simps)
   3.217 +    qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff)
   3.218 +  qed
   3.219 +  also have "... = ereal (pi / 4)"
   3.220 +  proof (subst nn_integral_FTC_atLeast)
   3.221 +    show "((\<lambda>a. arctan a / 2) ---> (pi / 2) / 2 ) at_top"
   3.222 +      by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top)
   3.223 +  qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square)
   3.224 +  finally have "?pI ?gauss^2 = pi / 4"
   3.225 +    by (simp add: power2_eq_square)
   3.226 +  then have "?pI ?gauss = sqrt (pi / 4)"
   3.227 +    using power_eq_iff_eq_base[of 2 "real (?pI ?gauss)" "sqrt (pi / 4)"]
   3.228 +      nn_integral_nonneg[of lborel "\<lambda>x. ?gauss x * indicator {0..} x"]
   3.229 +    by (cases "?pI ?gauss") auto
   3.230 +  then show ?thesis
   3.231 +    by (subst nn_integral_even_function) (auto simp add: real_sqrt_divide)
   3.232 +qed
   3.233 +
   3.234 +lemma has_bochner_integral_gaussian: "has_bochner_integral lborel (\<lambda>x. exp (- x\<^sup>2)) (sqrt pi)"
   3.235 +  by (auto intro!: nn_integral_gaussian has_bochner_integral_nn_integral)
   3.236 +
   3.237 +lemma integral_gaussian: "(\<integral>x. (exp (- x\<^sup>2)) \<partial>lborel) = sqrt pi"
   3.238 +  using has_bochner_integral_gaussian by (rule has_bochner_integral_integral_eq)
   3.239 +
   3.240 +lemma integrable_gaussian[intro]: "integrable lborel (\<lambda>x. exp (- x\<^sup>2)::real)"
   3.241 +  using has_bochner_integral_gaussian by rule
   3.242 +
   3.243 +context
   3.244 +  fixes \<sigma> :: real
   3.245 +  assumes \<sigma>_pos[arith]: "0 < \<sigma>"
   3.246 +begin
   3.247 +
   3.248 +lemma nn_integral_normal_density: "(\<integral>\<^sup>+x. normal_density \<mu> \<sigma> x \<partial>lborel) = 1"
   3.249 +  unfolding normal_density_def
   3.250 +  apply (subst times_ereal.simps(1)[symmetric],subst nn_integral_cmult)
   3.251 +  apply auto
   3.252 +  apply (subst nn_integral_real_affine[where t=\<mu> and  c="(sqrt 2) * \<sigma>"])
   3.253 +  by (auto simp: power_mult_distrib nn_integral_gaussian real_sqrt_mult one_ereal_def)
   3.254 +
   3.255 +lemma 
   3.256 +  shows normal_density_pos: "\<And>x. 0 < normal_density \<mu> \<sigma> x"
   3.257 +  and normal_density_nonneg: "\<And>x. 0 \<le> normal_density \<mu> \<sigma> x" 
   3.258 +  by (auto simp: normal_density_def)
   3.259 +
   3.260 +lemma integrable_normal[intro]: "integrable lborel (normal_density \<mu> \<sigma>)"
   3.261 +  by (auto intro!: integrableI_nn_integral_finite simp: nn_integral_normal_density normal_density_nonneg)
   3.262 +
   3.263 +lemma integral_normal_density[simp]: "(\<integral>x. normal_density \<mu> \<sigma> x \<partial>lborel) = 1"
   3.264 +  by (simp add: integral_eq_nn_integral normal_density_nonneg nn_integral_normal_density)
   3.265 +
   3.266 +lemma prob_space_normal_density:
   3.267 +  "prob_space (density lborel (normal_density \<mu> \<sigma>))" (is "prob_space ?D")
   3.268 +  proof qed (simp add: emeasure_density nn_integral_normal_density)
   3.269 +
   3.270  end
   3.271 +
   3.272 +lemma (in prob_space) normal_density_affine:
   3.273 +  assumes X: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.274 +  assumes [simp, arith]: "0 < \<sigma>" "\<alpha> \<noteq> 0"
   3.275 +  shows "distributed M lborel (\<lambda>x. \<beta> + \<alpha> * X x) (normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>))"
   3.276 +proof -
   3.277 +  have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) =
   3.278 +    normal_density \<mu> \<sigma> x"
   3.279 +    by (simp add: normal_density_def real_sqrt_mult field_simps)
   3.280 +       (simp add: power2_eq_square field_simps)
   3.281 +  show ?thesis
   3.282 +    by (rule distributed_affineI[OF _ `\<alpha> \<noteq> 0`, where t=\<beta>]) (simp_all add: eq X)
   3.283 +qed
   3.284 +
   3.285 +lemma (in prob_space) normal_standard_normal_convert:
   3.286 +  assumes pos_var[simp, arith]: "0 < \<sigma>"
   3.287 +  shows "distributed M lborel X (normal_density  \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density"
   3.288 +proof auto
   3.289 +  assume "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))"
   3.290 +  then have "distributed M lborel (\<lambda>x. -\<mu> / \<sigma> + (1/\<sigma>) * X x) (\<lambda>x. ereal (normal_density (-\<mu> / \<sigma> + (1/\<sigma>)* \<mu>) (\<bar>1/\<sigma>\<bar> * \<sigma>) x))"
   3.291 +    by(rule normal_density_affine) auto
   3.292 +  
   3.293 +  then show "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
   3.294 +    by (simp add: diff_divide_distrib[symmetric] field_simps)
   3.295 +next
   3.296 +  assume *: "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
   3.297 +  have "distributed M lborel (\<lambda>x. \<mu> + \<sigma> * ((X x - \<mu>) / \<sigma>)) (\<lambda>x. ereal (normal_density \<mu> \<bar>\<sigma>\<bar> x))"
   3.298 +    using normal_density_affine[OF *, of \<sigma> \<mu>] by simp  
   3.299 +  then show "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))" by simp
   3.300 +qed
   3.301 +
   3.302 +lemma conv_normal_density_zero_mean:
   3.303 +  assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
   3.304 +  shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (normal_density 0 \<sigma> (x - y) * normal_density 0 \<tau> y) \<partial>lborel) =
   3.305 +    normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))"  (is "?LHS = ?RHS")
   3.306 +proof -
   3.307 +  def \<sigma>' \<equiv> "\<sigma>\<^sup>2" and \<tau>' \<equiv> "\<tau>\<^sup>2"
   3.308 +  then have [simp, arith]: "0 < \<sigma>'" "0 < \<tau>'"
   3.309 +    by simp_all
   3.310 +  let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))"  
   3.311 +  have sqrt: "(sqrt (2 * pi * (\<sigma>' + \<tau>')) * sqrt (2 * pi * (\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))) = 
   3.312 +    (sqrt (2 * pi * \<sigma>') * sqrt (2 * pi * \<tau>'))"
   3.313 +    by (subst power_eq_iff_eq_base[symmetric, where n=2])
   3.314 +       (simp_all add: real_sqrt_mult[symmetric] power2_eq_square)
   3.315 +  have "?LHS =
   3.316 +    (\<lambda>x. \<integral>\<^sup>+y. ereal((normal_density 0 (sqrt (\<sigma>' + \<tau>')) x) * normal_density (\<tau>' * x / (\<sigma>' + \<tau>')) ?\<sigma> y) \<partial>lborel)"
   3.317 +    apply (intro ext nn_integral_cong)
   3.318 +    apply (simp add: normal_density_def \<sigma>'_def[symmetric] \<tau>'_def[symmetric] sqrt mult_exp_exp)
   3.319 +    apply (simp add: divide_simps power2_eq_square)
   3.320 +    apply (simp add: field_simps)
   3.321 +    done
   3.322 +
   3.323 +  also have "... =
   3.324 +    (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x) * \<integral>\<^sup>+y. ereal( normal_density (\<tau>\<^sup>2* x / (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) ?\<sigma> y) \<partial>lborel)"
   3.325 +    by (subst nn_integral_cmult[symmetric]) (auto simp: \<sigma>'_def \<tau>'_def normal_density_def)
   3.326 +
   3.327 +  also have "... = (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
   3.328 +    by (subst nn_integral_normal_density) (auto simp: sum_power2_gt_zero_iff)
   3.329 +
   3.330 +  finally show ?thesis by fast
   3.331 +qed
   3.332 +
   3.333 +lemma conv_std_normal_density:
   3.334 +  "(\<lambda>x. \<integral>\<^sup>+y. ereal (std_normal_density (x - y) * std_normal_density y) \<partial>lborel) =
   3.335 +  (normal_density 0 (sqrt 2))"
   3.336 +  by (subst conv_normal_density_zero_mean) simp_all
   3.337 +
   3.338 +lemma (in prob_space) sum_indep_normal:
   3.339 +  assumes indep: "indep_var borel X borel Y"
   3.340 +  assumes pos_var[arith]: "0 < \<sigma>" "0 < \<tau>"
   3.341 +  assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.342 +  assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
   3.343 +  shows "distributed M lborel (\<lambda>x. X x + Y x) (normal_density (\<mu> + \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
   3.344 +proof -
   3.345 +  have ind[simp]: "indep_var borel (\<lambda>x. - \<mu> + X x) borel (\<lambda>x. - \<nu> + Y x)"
   3.346 +  proof -
   3.347 +    have "indep_var borel ( (\<lambda>x. -\<mu> + x) o X) borel ((\<lambda>x. - \<nu> + x) o Y)"
   3.348 +      by (auto intro!: indep_var_compose assms) 
   3.349 +    then show ?thesis by (simp add: o_def)
   3.350 +  qed
   3.351 +  
   3.352 +  have "distributed M lborel (\<lambda>x. -\<mu> + 1 * X x) (normal_density (- \<mu> + 1 * \<mu>) (\<bar>1\<bar> * \<sigma>))"
   3.353 +    by(rule normal_density_affine[OF normalX pos_var(1), of 1 "-\<mu>"]) simp
   3.354 +  then have 1[simp]: "distributed M lborel (\<lambda>x. - \<mu> +  X x) (normal_density 0 \<sigma>)" by simp
   3.355 +
   3.356 +  have "distributed M lborel (\<lambda>x. -\<nu> + 1 * Y x) (normal_density (- \<nu> + 1 * \<nu>) (\<bar>1\<bar> * \<tau>))"
   3.357 +    by(rule normal_density_affine[OF normalY pos_var(2), of 1 "-\<nu>"]) simp
   3.358 +  then have 2[simp]: "distributed M lborel (\<lambda>x. - \<nu> +  Y x) (normal_density 0 \<tau>)" by simp
   3.359 +  
   3.360 +  have *: "distributed M lborel (\<lambda>x. (- \<mu> + X x) + (- \<nu> + Y x)) (\<lambda>x. ereal (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
   3.361 +    using distributed_convolution[OF ind 1 2] conv_normal_density_zero_mean[OF pos_var] by simp
   3.362 +  
   3.363 +  have "distributed M lborel (\<lambda>x. \<mu> + \<nu> + 1 * (- \<mu> + X x + (- \<nu> + Y x)))
   3.364 +        (\<lambda>x. ereal (normal_density (\<mu> + \<nu> + 1 * 0) (\<bar>1\<bar> * sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
   3.365 +    by (rule normal_density_affine[OF *, of 1 "\<mu> + \<nu>"]) (auto simp: add_pos_pos)
   3.366 +
   3.367 +  then show ?thesis by auto
   3.368 +qed
   3.369 +
   3.370 +lemma (in prob_space) diff_indep_normal:
   3.371 +  assumes indep[simp]: "indep_var borel X borel Y"
   3.372 +  assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
   3.373 +  assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.374 +  assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
   3.375 +  shows "distributed M lborel (\<lambda>x. X x - Y x) (normal_density (\<mu> - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
   3.376 +proof -
   3.377 +  have "distributed M lborel (\<lambda>x. 0 + - 1 * Y x) (\<lambda>x. ereal (normal_density (0 + - 1 * \<nu>) (\<bar>- 1\<bar> * \<tau>) x))" 
   3.378 +    by(rule normal_density_affine, auto)
   3.379 +  then have [simp]:"distributed M lborel (\<lambda>x. - Y x) (\<lambda>x. ereal (normal_density (- \<nu>) \<tau> x))" by simp
   3.380 +
   3.381 +  have "distributed M lborel (\<lambda>x. X x + (- Y x)) (normal_density (\<mu> + - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
   3.382 +    apply (rule sum_indep_normal)
   3.383 +    apply (rule indep_var_compose[unfolded comp_def, of borel _ borel _ "\<lambda>x. x" _ "\<lambda>x. - x"])
   3.384 +    apply simp_all
   3.385 +    done
   3.386 +  then show ?thesis by simp
   3.387 +qed
   3.388 +
   3.389 +lemma (in prob_space) setsum_indep_normal:
   3.390 +  assumes "finite I" "I \<noteq> {}" "indep_vars (\<lambda>i. borel) X I"
   3.391 +  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 < \<sigma> i"
   3.392 +  assumes normal: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (normal_density (\<mu> i) (\<sigma> i))"
   3.393 +  shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (normal_density (\<Sum>i\<in>I. \<mu> i) (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2)))"
   3.394 +  using assms 
   3.395 +proof (induct I rule: finite_ne_induct)
   3.396 +  case (singleton i) then show ?case by (simp add : abs_of_pos)
   3.397 +next
   3.398 +  case (insert i I)
   3.399 +    then have 1: "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in>I. X i x)) 
   3.400 +                (normal_density (\<mu> i  + setsum \<mu> I)  (sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)))"
   3.401 +      apply (intro sum_indep_normal indep_vars_setsum insert real_sqrt_gt_zero)  
   3.402 +      apply (auto intro: indep_vars_subset intro!: setsum_pos)
   3.403 +      apply fastforce
   3.404 +      done
   3.405 +    have 2: "(\<lambda>x. (X i x)+ (\<Sum>i\<in>I. X i x)) = (\<lambda>x. (\<Sum>j\<in>insert i I. X j x))"
   3.406 +          "\<mu> i + setsum \<mu> I = setsum \<mu> (insert i I)"
   3.407 +      using insert by auto
   3.408 +  
   3.409 +    have 3: "(sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)) = (sqrt (\<Sum>i\<in>insert i I. (\<sigma> i)\<^sup>2))"
   3.410 +      using insert by (simp add: setsum_nonneg)
   3.411 +  
   3.412 +    show ?case using 1 2 3 by simp  
   3.413 +qed
   3.414 +
   3.415 +lemma nn_integral_x_exp_x_square: "(\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2 )) \<partial>lborel) = ereal 1 / 2" 
   3.416 +  and nn_integral_x_exp_x_square_indicator: "(\<integral>\<^sup>+x. ereal( x * exp (-x\<^sup>2 )) * indicator {0..} x \<partial>lborel) = ereal 1 / 2"
   3.417 +proof - 
   3.418 +  let ?F = "\<lambda>x. - exp (-x\<^sup>2 ) / 2"
   3.419 +
   3.420 +  have 1: "(\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel) =ereal( 0 - ?F 0)"
   3.421 +  apply (rule nn_integral_FTC_atLeast)
   3.422 +  apply (auto intro!: derivative_eq_intros)
   3.423 +  apply (rule tendsto_minus_cancel)
   3.424 +  apply (simp add: field_simps)
   3.425 +  proof - 
   3.426 +    have "((\<lambda>(x::real). exp (- x\<^sup>2) / 2) ---> 0 / 2) at_top"
   3.427 +    apply (intro tendsto_divide filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   3.428 +    apply auto
   3.429 +    done
   3.430 +    then show "((\<lambda>(x::real). exp (- x\<^sup>2) / 2) ---> 0) at_top" by simp
   3.431 +  qed
   3.432 +
   3.433 +  also have 2: "(\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel) = integral\<^sup>N lborel (\<lambda>x. ereal (x * exp (- x\<^sup>2)))"
   3.434 +    by (subst(2) nn_integral_max_0[symmetric])
   3.435 +       (auto intro!: nn_integral_cong split: split_indicator simp: max_def zero_le_mult_iff)
   3.436 +  finally show "(\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2)) \<partial>lborel) = ereal 1 / 2" by auto
   3.437 +
   3.438 +  show "(\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel) = ereal 1 / 2" using 1 by auto
   3.439 +qed
   3.440 +
   3.441 +lemma borel_integral_x_times_standard_normal[intro]: "(\<integral>x. std_normal_density x * x \<partial>lborel) = 0" 
   3.442 +  and borel_integrable_x_times_standard_normal[intro]: "integrable lborel (\<lambda>x. std_normal_density x * x)"
   3.443 +  and borel_integral_x_times_standard_normal'[intro]: "(\<integral>x. x * std_normal_density x \<partial>lborel) = 0" 
   3.444 +  and borel_integrable_x_times_standard_normal'[intro]: "integrable lborel (\<lambda>x. x * std_normal_density x)"
   3.445 +proof -    
   3.446 +  have 0: "(\<integral>\<^sup>+x. ereal (x * std_normal_density x) \<partial>lborel) = \<integral>\<^sup>+x. ereal (x * std_normal_density x) * indicator {0..} x \<partial>lborel"
   3.447 +    apply (subst nn_integral_max_0[symmetric]) 
   3.448 +    unfolding max_def std_normal_density_def
   3.449 +    apply (auto intro!: nn_integral_cong split:split_indicator simp: zero_le_divide_iff zero_le_mult_iff)
   3.450 +    apply (metis not_le pi_gt_zero)
   3.451 +    done
   3.452 +
   3.453 +  have 1: "(\<integral>\<^sup>+x. ereal (- (x * std_normal_density x)) \<partial>lborel) = \<integral>\<^sup>+x. ereal (x * std_normal_density x) * indicator {0..} x \<partial>lborel"
   3.454 +    apply (subst(2) nn_integral_real_affine[where c = "-1" and t = 0])
   3.455 +    apply(auto simp: std_normal_density_def split: split_indicator)
   3.456 +    apply(subst nn_integral_max_0[symmetric]) 
   3.457 +    unfolding max_def std_normal_density_def
   3.458 +    apply (auto intro!: nn_integral_cong split: split_indicator
   3.459 +                simp: divide_le_0_iff mult_le_0_iff one_ereal_def[symmetric])
   3.460 +    apply (metis not_le pi_gt_zero)
   3.461 +    done
   3.462 +
   3.463 +  have 2: "sqrt pi / sqrt 2 * (\<integral>\<^sup>+x. ereal (x * std_normal_density x) * indicator {0..} x \<partial>lborel) = integral\<^sup>N lborel (\<lambda>x. ereal (x * exp (- x\<^sup>2)))"
   3.464 +    unfolding std_normal_density_def
   3.465 +    apply (subst nn_integral_real_affine[where c = "sqrt 2" and t = 0])
   3.466 +    apply (auto simp: power_mult_distrib split: split_indicator)
   3.467 +    apply (subst mult_assoc[symmetric])
   3.468 +    apply (subst nn_integral_cmult[symmetric])
   3.469 +    apply auto
   3.470 +    apply (subst(2) nn_integral_max_0[symmetric])
   3.471 +    apply (auto intro!: nn_integral_cong split: split_indicator simp: max_def zero_le_mult_iff real_sqrt_mult)
   3.472 +    done
   3.473 +
   3.474 +  have *: "(\<integral>\<^sup>+x. ereal (x * std_normal_density x) * indicator {0..} x \<partial>lborel) = sqrt 2 / sqrt pi *(integral\<^sup>N lborel (\<lambda>x. ereal (x * exp (- x\<^sup>2))))"
   3.475 +    apply (subst 2[symmetric])
   3.476 +    apply (subst mult_assoc[symmetric])
   3.477 +    apply (auto simp: field_simps one_ereal_def[symmetric])
   3.478 +    done
   3.479 +    
   3.480 +  show "(\<integral> x. x * std_normal_density x \<partial>lborel) = 0" "integrable lborel (\<lambda>x. x * std_normal_density x)"
   3.481 +    by (subst real_lebesgue_integral_def)
   3.482 +       (auto simp: 0 1 * nn_integral_x_exp_x_square real_integrable_def)
   3.483 +
   3.484 +  then show "(\<integral> x. std_normal_density x * x \<partial>lborel) = 0" "integrable lborel (\<lambda>x. std_normal_density x * x)"
   3.485 +    by (simp_all add:mult_commute)
   3.486 +qed
   3.487 +
   3.488 +lemma (in prob_space) standard_normal_distributed_expectation:
   3.489 +  assumes D: "distributed M lborel X std_normal_density "
   3.490 +  shows "expectation X = 0"
   3.491 +  by (auto simp: distributed_integral[OF D, of "\<lambda>x. x", symmetric])
   3.492 +
   3.493 +lemma (in prob_space) normal_distributed_expectation:
   3.494 +  assumes pos_var[arith]: "0 < \<sigma>"
   3.495 +  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.496 +  shows "expectation X = \<mu>"
   3.497 +proof -
   3.498 +  def X' \<equiv> "\<lambda>x. (X x - \<mu>) / \<sigma>"
   3.499 +  then have D1: "distributed M lborel X' std_normal_density"
   3.500 +    by (simp add: normal_standard_normal_convert[OF pos_var, of X \<mu>, symmetric] D)
   3.501 +  then have [simp]: "integrable M X'"
   3.502 +    by (rule distributed_integrable_var) auto
   3.503 +
   3.504 +  have "expectation X = expectation (\<lambda>x. \<mu> + \<sigma> * X' x)"
   3.505 +    by (simp add: X'_def)
   3.506 +  then show ?thesis
   3.507 +    by (simp add: prob_space standard_normal_distributed_expectation[OF D1])
   3.508 +qed
   3.509 +
   3.510 +lemma integral_xsquare_exp_xsquare: "(\<integral> x. (x\<^sup>2 * exp (-x\<^sup>2 )) \<partial>lborel) =  sqrt pi / 2"
   3.511 +  and integrable_xsquare_exp_xsquare: "integrable lborel (\<lambda>x. x\<^sup>2 * exp (- x\<^sup>2)::real)"
   3.512 +proof- 
   3.513 +  note filterlim_compose[OF exp_at_top, intro] filterlim_ident[intro]
   3.514 +
   3.515 +  let ?f = "(\<lambda>x. x * - exp (- x\<^sup>2) / 2 - 0 * - exp (- 0\<^sup>2) / 2 -
   3.516 +                 \<integral> xa. 1 * (- exp (- xa\<^sup>2) / 2) * indicator {0..x} xa \<partial>lborel)::real\<Rightarrow>real"
   3.517 +  let ?IFunc = "(\<lambda>z. \<integral>x. (x\<^sup>2 * exp (- x\<^sup>2)) * indicator {0 .. z} x \<partial>lborel)::real\<Rightarrow>real"
   3.518 +
   3.519 +
   3.520 +  from nn_integral_gaussian  
   3.521 +  have 1: "(\<integral>\<^sup>+xa. ereal (exp (- xa\<^sup>2)) * indicator {0..} xa \<partial>lborel) = ereal (sqrt pi) / ereal 2"
   3.522 +    apply (subst (asm) nn_integral_even_function)
   3.523 +    apply simp
   3.524 +    apply simp
   3.525 +    apply (cases "\<integral>\<^sup>+ xa. ereal (exp (- xa\<^sup>2)) * indicator {0..} xa \<partial>lborel")
   3.526 +    apply auto
   3.527 +    done
   3.528 +
   3.529 +  then have I: "(\<integral>xa. exp (- xa\<^sup>2) * indicator {0..} xa \<partial>lborel) = sqrt pi / 2"
   3.530 +    by (subst integral_eq_nn_integral) (auto simp: ereal_mult_indicator)
   3.531 +  
   3.532 +  have byparts: "?IFunc = (\<lambda>z. (if z < 0 then 0 else ?f z))"
   3.533 +    proof (intro HOL.ext, subst split_ifs, safe)
   3.534 +      fix z::real assume [arith]:" \<not> z < 0 "
   3.535 +  
   3.536 +      have "?IFunc z =  \<integral>x. (x * (x * exp (- x\<^sup>2))) * indicator {0 .. z} x \<partial>lborel"
   3.537 +        by(auto intro!: integral_cong split: split_indicator simp: power2_eq_square)
   3.538 +  
   3.539 +      also have "... = (\<lambda>x. x) z * (\<lambda>x. - exp (- x\<^sup>2 ) / 2) z - (\<lambda>x. x) 0 * (\<lambda>x. - exp (- x\<^sup>2) / 2) 0 
   3.540 +          -  \<integral>x. 1 * ( - exp (- x\<^sup>2) / 2) * indicator {0 .. z} x \<partial>lborel"
   3.541 +        by(rule integral_by_parts, auto intro!: derivative_eq_intros)  
   3.542 +      finally have "?IFunc z = ..." .
   3.543 +
   3.544 +      then show "?IFunc z = ?f z" by simp
   3.545 +    qed simp    
   3.546 +
   3.547 +  have [simp]: "(\<lambda>y. \<integral> x. x\<^sup>2 * exp (- x\<^sup>2) * indicator {0..} x * indicator {..y} x \<partial>lborel) = ?IFunc"
   3.548 +    by(auto intro!: integral_cong split:split_indicator)
   3.549 +
   3.550 +  have [intro]: "((\<lambda>(x::real). x * exp (- x\<^sup>2) / 2) ---> 0) at_top"
   3.551 +  proof -
   3.552 +    have "((\<lambda>(x::real). x * exp (- x\<^sup>2) / 2) ---> 0 / 2) at_top"
   3.553 +      apply (intro tendsto_divide filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   3.554 +      apply (auto simp: exp_minus inverse_eq_divide)
   3.555 +      apply (rule lhospital_at_top_at_top[where f' = "\<lambda>x. 1" and g' = "\<lambda>x. 2 * x * exp (x\<^sup>2)"])
   3.556 +      apply (auto intro!: derivative_eq_intros eventually_elim1[OF eventually_gt_at_top, of 1])
   3.557 +      apply (subst inverse_eq_divide[symmetric])
   3.558 +      apply (rule  tendsto_inverse_0_at_top)
   3.559 +      apply (subst mult_assoc)
   3.560 +      by (auto intro!: filterlim_tendsto_pos_mult_at_top[of "\<lambda>x. 2" 2] filterlim_at_top_mult_at_top[OF filterlim_ident])
   3.561 +    
   3.562 +    then show ?thesis by simp
   3.563 +  qed
   3.564 +
   3.565 +  have "((\<lambda>x. (\<integral>y. (exp (- y\<^sup>2) * indicator {0..} y) * indicator {.. x} y \<partial>lborel) :: real) ---> \<integral>y. exp (- y\<^sup>2) * indicator {0..} y \<partial>lborel) at_top"
   3.566 +    by (intro tendsto_integral_at_top integrable_mult_indicator) auto
   3.567 +  also have "(\<lambda>x. (\<integral>y. (exp (- y\<^sup>2) * indicator {0..} y) * indicator {.. x} y \<partial>lborel) :: real) = 
   3.568 +    (\<lambda>x. (\<integral>y. exp (- y\<^sup>2) * indicator {0..x} y \<partial>lborel) :: real)"
   3.569 +    by (auto simp: fun_eq_iff split: split_indicator intro!: integral_cong)
   3.570 +  finally have *: "((\<lambda>x. (\<integral>y. exp (- y\<^sup>2) * indicator {0..x} y \<partial>lborel) :: real) ---> \<integral>y. exp (- y\<^sup>2) * indicator {0..} y \<partial>lborel) at_top"
   3.571 +    .
   3.572 +
   3.573 +  have tends: "((\<lambda>x. (\<integral> xa. exp (- xa\<^sup>2) * indicator {0..x} xa \<partial>lborel) / 2) ---> (sqrt pi / 2) / 2) at_top"
   3.574 +    apply (rule tendsto_divide)
   3.575 +    apply (subst I[symmetric])
   3.576 +    apply (auto intro: *)
   3.577 +    done
   3.578 +
   3.579 +  have [intro]: "(?IFunc ---> sqrt pi / 4) at_top"
   3.580 +    apply (simp add: byparts)
   3.581 +    apply (subst filterlim_cong[where g = ?f])
   3.582 +    apply (auto simp: eventually_ge_at_top linorder_not_less)
   3.583 +  proof -
   3.584 +    have "((\<lambda>x. (\<integral> xa. exp (- xa\<^sup>2) * indicator {0..x} xa / 2 \<partial>lborel) - x * exp (- x\<^sup>2) / 2::real) --->
   3.585 +        (0 + sqrt pi / 4 - 0)) at_top"
   3.586 +      apply (intro tendsto_diff)
   3.587 +      apply auto
   3.588 +      apply (subst divide_real_def)
   3.589 +      using tends
   3.590 +      by (auto intro!: integrable_mult_indicator)
   3.591 +    then show "((\<lambda>x. (\<integral> xa. exp (- xa\<^sup>2) * indicator {0..x} xa \<partial>lborel) / 2 - x * exp (- x\<^sup>2) / 2) ---> sqrt pi / 4) at_top" by  simp
   3.592 +  qed
   3.593 +    
   3.594 +  have [intro]:"\<And>y. integrable lborel (\<lambda>x. x\<^sup>2 * exp (- x\<^sup>2) * indicator {0..} x * indicator {..y} x::real)"
   3.595 +    apply (subst integrable_cong[where g = "\<lambda>x. x\<^sup>2 * exp (- x\<^sup>2) * indicator {0..y} x" for y])
   3.596 +    by (auto intro!: borel_integrable_atLeastAtMost split:split_indicator)
   3.597 +    
   3.598 +  have **[intro]: "integrable lborel (\<lambda>x. x\<^sup>2 * exp (- x\<^sup>2) * indicator {0..} x::real)"
   3.599 +    by (rule integrable_monotone_convergence_at_top) auto
   3.600 +
   3.601 +  have "(\<integral>x. x\<^sup>2 * exp (- x\<^sup>2) * indicator {0..} x \<partial>lborel) = sqrt pi / 4"
   3.602 +    by (rule integral_monotone_convergence_at_top) auto
   3.603 +  
   3.604 +  then have "(\<integral>\<^sup>+x. ereal (x\<^sup>2 * exp (- x\<^sup>2)* indicator {0..} x) \<partial>lborel) = sqrt pi / 4"
   3.605 +    by (subst nn_integral_eq_integral) auto
   3.606 +
   3.607 +  then have ***: "(\<integral>\<^sup>+ x. ereal (x\<^sup>2 * exp (- x\<^sup>2)) \<partial>lborel) = sqrt pi / 2"
   3.608 +    by (subst nn_integral_even_function)
   3.609 +       (auto simp: real_sqrt_mult real_sqrt_divide ereal_mult_indicator)
   3.610 +  
   3.611 +  then show "(\<integral> x. x\<^sup>2 * exp (- x\<^sup>2) \<partial>lborel) = sqrt pi / 2"
   3.612 +    by (subst integral_eq_nn_integral) auto
   3.613 +
   3.614 +  show "integrable lborel (\<lambda>x. x\<^sup>2 * exp (- x\<^sup>2)::real)"
   3.615 +    by (intro integrableI_nn_integral_finite[OF _ _ ***]) auto
   3.616 +qed
   3.617 +
   3.618 +lemma integral_xsquare_times_standard_normal[intro]: "(\<integral> x. std_normal_density x * x\<^sup>2 \<partial>lborel) = 1"
   3.619 +  and integrable_xsquare_times_standard_normal[intro]: "integrable lborel (\<lambda>x. std_normal_density x * x\<^sup>2)"
   3.620 +proof -
   3.621 +  have [intro]:"integrable lborel (\<lambda>x. exp (- x\<^sup>2) * (2 * x\<^sup>2) / (sqrt 2 * sqrt pi))"
   3.622 +    apply (subst integrable_cong[where g ="(\<lambda>x. (2 * inverse (sqrt 2 * sqrt pi)) * (exp (- x\<^sup>2) * x\<^sup>2))"])
   3.623 +    by (auto intro!: integrable_xsquare_exp_xsquare simp: field_simps)
   3.624 +
   3.625 +  have "(\<integral> x. std_normal_density x * x\<^sup>2 \<partial>lborel) = (2 / sqrt pi) * \<integral> x. x\<^sup>2 * exp (- x\<^sup>2) \<partial>lborel"
   3.626 +    apply (subst integral_mult_right[symmetric])
   3.627 +    apply (rule integrable_xsquare_exp_xsquare)
   3.628 +    unfolding std_normal_density_def
   3.629 +    apply (subst lborel_integral_real_affine[where c = "sqrt 2" and t=0], simp_all)
   3.630 +    unfolding integral_mult_right_zero[symmetric] integral_divide_zero[symmetric]
   3.631 +    apply (intro integral_cong)
   3.632 +    by (auto simp: power_mult_distrib real_sqrt_mult)
   3.633 +  also have "... = 1"
   3.634 +    by (subst integral_xsquare_exp_xsquare, auto)
   3.635 +  finally show "(\<integral> x. std_normal_density x * x\<^sup>2 \<partial>lborel) = 1" .
   3.636 +
   3.637 +  show "integrable lborel (\<lambda>x. std_normal_density x * x\<^sup>2)"
   3.638 +    unfolding std_normal_density_def
   3.639 +    apply (subst lborel_integrable_real_affine_iff[where c = "sqrt 2" and t=0, symmetric])
   3.640 +    by (auto simp: power_mult_distrib real_sqrt_mult)
   3.641 +qed
   3.642 +
   3.643 +lemma 
   3.644 +  assumes [arith]: "0 < \<sigma>"
   3.645 +  shows integral_xsquare_times_normal: "(\<integral> x. normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2 \<partial>lborel) = \<sigma>\<^sup>2"
   3.646 +  and integrable_xsquare_times_normal: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2)"
   3.647 +proof -
   3.648 +  have "(\<integral> x. normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2 \<partial>lborel) = \<sigma> * \<sigma> * \<integral> x. std_normal_density x * x\<^sup>2 \<partial>lborel"
   3.649 +    unfolding normal_density_def
   3.650 +    apply (subst lborel_integral_real_affine[ where c = \<sigma> and t = \<mu>])
   3.651 +    apply (auto simp: power_mult_distrib)
   3.652 +    unfolding integral_mult_right_zero[symmetric] integral_divide_zero[symmetric]
   3.653 +    apply (intro integral_cong)
   3.654 +    apply auto
   3.655 +    unfolding normal_density_def
   3.656 +    by (auto simp: real_sqrt_mult field_simps power2_eq_square[symmetric])
   3.657 +    
   3.658 +  also have "... = \<sigma>\<^sup>2" 
   3.659 +    by(auto simp: power2_eq_square[symmetric])
   3.660 +
   3.661 +  finally show "(\<integral> x. normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2 \<partial>lborel) = \<sigma>\<^sup>2" .
   3.662 + 
   3.663 +  show "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2)"
   3.664 +    unfolding normal_density_def
   3.665 +    apply (subst lborel_integrable_real_affine_iff[ where c = \<sigma> and t = \<mu>, symmetric])
   3.666 +    apply auto
   3.667 +    apply (auto simp: power_mult_distrib)
   3.668 +    apply (subst integrable_cong[where g ="(\<lambda>x. \<sigma> * (std_normal_density x * x\<^sup>2))"], auto)
   3.669 +    unfolding std_normal_density_def
   3.670 +    by (auto simp: field_simps real_sqrt_mult power2_eq_square[symmetric])
   3.671 +qed
   3.672 +  
   3.673 +lemma (in prob_space) standard_normal_distributed_variance:
   3.674 +  fixes a b :: real
   3.675 +  assumes D: "distributed M lborel X std_normal_density"
   3.676 +  shows "variance X = 1"
   3.677 +  apply (subst distributed_integral[OF D, of "(\<lambda>x. (x - expectation X)\<^sup>2)", symmetric])
   3.678 +  by (auto simp: standard_normal_distributed_expectation[OF D])
   3.679 +
   3.680 +lemma (in prob_space) normal_distributed_variance:
   3.681 +  fixes a b :: real
   3.682 +  assumes [simp, arith]: " 0 < \<sigma>"
   3.683 +  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.684 +  shows "variance X = \<sigma>\<^sup>2"
   3.685 +proof-  
   3.686 +  have *[intro]: "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
   3.687 +    by (subst normal_standard_normal_convert[OF assms(1) , symmetric]) fact
   3.688 +
   3.689 +  have "variance X = variance  (\<lambda>x. \<mu> + \<sigma> * ((X x - \<mu>) / \<sigma>) )" by simp
   3.690 +  also have "... = \<sigma>\<^sup>2 * 1"
   3.691 +    apply (subst variance_affine)
   3.692 +    apply (auto intro!: standard_normal_distributed_variance prob_space_normal_density
   3.693 +      simp: distributed_integrable[OF *,of "\<lambda>x. x", symmetric]
   3.694 +      distributed_integrable[OF *,of "\<lambda>x. x\<^sup>2", symmetric] variance_affine
   3.695 +      simp del: integral_divide_zero)
   3.696 +    done
   3.697 +
   3.698 +  finally show ?thesis by simp
   3.699 +qed
   3.700 +
   3.701 +lemma (in information_space) entropy_normal_density:
   3.702 +  assumes [arith]: "0 < \<sigma>"
   3.703 +  assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
   3.704 +  shows "entropy b lborel X = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
   3.705 +proof -
   3.706 +  have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
   3.707 +    using D by (rule entropy_distr)
   3.708 +  also have "\<dots> = - (\<integral> x. normal_density \<mu> \<sigma> x * (- ln (2 * pi * \<sigma>\<^sup>2) - (x - \<mu>)\<^sup>2 / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
   3.709 +    by (intro arg_cong[where f="uminus"] integral_cong)
   3.710 +       (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
   3.711 +  also have "\<dots> = - (\<integral>x. - (normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2) / (2 * ln b) \<partial>lborel)"
   3.712 +    by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
   3.713 +  also have "\<dots> = (\<integral>x. normal_density \<mu> \<sigma> x * (ln (2 * pi * \<sigma>\<^sup>2)) + (normal_density \<mu> \<sigma> x * (x - \<mu>)\<^sup>2) / \<sigma>\<^sup>2 \<partial>lborel) / (2 * ln b)"
   3.714 +    by (simp del: minus_add_distrib)
   3.715 +  also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
   3.716 +    by (simp add: integrable_xsquare_times_normal integrable_normal integral_xsquare_times_normal)
   3.717 +  also have "\<dots> = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
   3.718 +    by (simp add: log_def field_simps ln_mult)
   3.719 +  finally show ?thesis .
   3.720 +qed
   3.721 +
   3.722 +end
     4.1 --- a/src/HOL/Probability/Information.thy	Fri Jun 13 07:05:01 2014 +0200
     4.2 +++ b/src/HOL/Probability/Information.thy	Fri Jun 13 14:08:20 2014 +0200
     4.3 @@ -8,7 +8,6 @@
     4.4  theory Information
     4.5  imports
     4.6    Independent_Family
     4.7 -  Distributions
     4.8    "~~/src/HOL/Library/Convex"
     4.9  begin
    4.10  
    4.11 @@ -916,35 +915,6 @@
    4.12      by (subst integral_mult_right) (auto simp: measure_def)
    4.13  qed
    4.14  
    4.15 -lemma (in information_space) entropy_exponential:
    4.16 -  assumes D: "distributed M lborel X (exponential_density l)"
    4.17 -  shows "entropy b lborel X = log b (exp 1 / l)"
    4.18 -proof -
    4.19 -  have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
    4.20 - 
    4.21 -  have [simp]: "integrable lborel (exponential_density l)"
    4.22 -    using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
    4.23 -
    4.24 -  have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
    4.25 -    using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
    4.26 -    
    4.27 -  have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
    4.28 -    using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
    4.29 -
    4.30 -  have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
    4.31 -    using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
    4.32 -    
    4.33 -  have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
    4.34 -    using D by (rule entropy_distr)
    4.35 -  also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
    4.36 -    (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
    4.37 -    by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
    4.38 -  also have "\<dots> = (ln l - 1) / ln b"
    4.39 -    by simp
    4.40 -  finally show ?thesis
    4.41 -    by (simp add: log_def divide_simps ln_div)
    4.42 -qed
    4.43 -
    4.44  lemma (in information_space) entropy_simple_distributed:
    4.45    "simple_distributed M X f \<Longrightarrow> \<H>(X) = - (\<Sum>x\<in>X`space M. f x * log b (f x))"
    4.46    by (subst entropy_distr[OF simple_distributed])
     5.1 --- a/src/HOL/Probability/Probability.thy	Fri Jun 13 07:05:01 2014 +0200
     5.2 +++ b/src/HOL/Probability/Probability.thy	Fri Jun 13 14:08:20 2014 +0200
     5.3 @@ -6,7 +6,6 @@
     5.4    Infinite_Product_Measure
     5.5    Projective_Limit
     5.6    Independent_Family
     5.7 -  Information
     5.8    Distributions
     5.9  begin
    5.10