src/HOL/Probability/Distributions.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59734 f41a2f77ab1b
child 61359 e985b52c3eb3
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     1 (*  Title:      HOL/Probability/Distributions.thy
     2     Author:     Sudeep Kanav, TU München
     3     Author:     Johannes Hölzl, TU München
     4     Author:     Jeremy Avigad, CMU *)
     5 
     6 section {* Properties of Various Distributions *}
     7 
     8 theory Distributions
     9   imports Convolution Information
    10 begin
    11 
    12 lemma (in prob_space) distributed_affine:
    13   fixes f :: "real \<Rightarrow> ereal"
    14   assumes f: "distributed M lborel X f"
    15   assumes c: "c \<noteq> 0"
    16   shows "distributed M lborel (\<lambda>x. t + c * X x) (\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>)"
    17   unfolding distributed_def
    18 proof safe
    19   have [measurable]: "f \<in> borel_measurable borel"
    20     using f by (simp add: distributed_def)
    21   have [measurable]: "X \<in> borel_measurable M"
    22     using f by (simp add: distributed_def)
    23 
    24   show "(\<lambda>x. f ((x - t) / c) / \<bar>c\<bar>) \<in> borel_measurable lborel"
    25     by simp
    26   show "random_variable lborel (\<lambda>x. t + c * X x)"
    27     by simp
    28   
    29   have "AE x in lborel. 0 \<le> f x"
    30     using f by (simp add: distributed_def)
    31   from AE_borel_affine[OF _ _ this, where c="1/c" and t="- t / c"] c
    32   show "AE x in lborel. 0 \<le> f ((x - t) / c) / ereal \<bar>c\<bar>"
    33     by (auto simp add: field_simps)
    34 
    35   have eq: "\<And>x. ereal \<bar>c\<bar> * (f x / ereal \<bar>c\<bar>) = f x"
    36     using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
    37     
    38   have "density lborel f = distr M lborel X"
    39     using f by (simp add: distributed_def)
    40   with c show "distr M lborel (\<lambda>x. t + c * X x) = density lborel (\<lambda>x. f ((x - t) / c) / ereal \<bar>c\<bar>)"
    41     by (subst (2) lborel_real_affine[where c="c" and t="t"])
    42        (simp_all add: density_density_eq density_distr distr_distr field_simps eq cong: distr_cong)
    43 qed
    44 
    45 lemma (in prob_space) distributed_affineI:
    46   fixes f :: "real \<Rightarrow> ereal"
    47   assumes f: "distributed M lborel (\<lambda>x. (X x - t) / c) (\<lambda>x. \<bar>c\<bar> * f (x * c + t))"
    48   assumes c: "c \<noteq> 0"
    49   shows "distributed M lborel X f"
    50 proof -
    51   have eq: "\<And>x. f x * ereal \<bar>c\<bar> / ereal \<bar>c\<bar> = f x"
    52     using c by (simp add: divide_ereal_def ac_simps one_ereal_def[symmetric])
    53 
    54   show ?thesis
    55     using distributed_affine[OF f c, where t=t] c
    56     by (simp add: field_simps eq)
    57 qed
    58 
    59 lemma (in prob_space) distributed_AE2:
    60   assumes [measurable]: "distributed M N X f" "Measurable.pred N P"
    61   shows "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in N. 0 < f x \<longrightarrow> P x)"
    62 proof -
    63   have "(AE x in M. P (X x)) \<longleftrightarrow> (AE x in distr M N X. P x)"
    64     by (simp add: AE_distr_iff)
    65   also have "\<dots> \<longleftrightarrow> (AE x in density N f. P x)"
    66     unfolding distributed_distr_eq_density[OF assms(1)] ..
    67   also have "\<dots> \<longleftrightarrow>  (AE x in N. 0 < f x \<longrightarrow> P x)"
    68     by (rule AE_density) simp
    69   finally show ?thesis .
    70 qed
    71 
    72 subsection {* Erlang *}
    73 
    74 lemma nn_intergal_power_times_exp_Icc:
    75   assumes [arith]: "0 \<le> a"
    76   shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x \<partial>lborel) =
    77     (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n)) * fact k" (is "?I = _")
    78 proof -
    79   let ?f = "\<lambda>k x. x^k * exp (-x) / fact k"
    80   let ?F = "\<lambda>k x. - (\<Sum>n\<le>k. (x^n * exp (-x)) / fact n)"
    81   have "?I * (inverse (real_of_nat (fact k))) = 
    82       (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 .. a} x * (inverse (real_of_nat (fact k))) \<partial>lborel)"
    83     by (intro nn_integral_multc[symmetric]) auto
    84   also have "\<dots> = (\<integral>\<^sup>+x. ereal (?f k x) * indicator {0 .. a} x \<partial>lborel)"
    85     apply (intro nn_integral_cong)
    86     apply (simp add: field_simps)
    87     by (metis (no_types) divide_inverse mult.commute mult.left_commute mult.left_neutral times_ereal.simps(1))
    88   also have "\<dots> = ereal (?F k a - ?F k 0)"
    89   proof (rule nn_integral_FTC_Icc)
    90     fix x assume "x \<in> {0..a}"
    91     show "DERIV (?F k) x :> ?f k x"
    92     proof(induction k)
    93       case 0 show ?case by (auto intro!: derivative_eq_intros)
    94     next
    95       case (Suc k)
    96       have "DERIV (\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) x :>
    97         ?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k))"
    98         by (intro DERIV_diff Suc)
    99            (auto intro!: derivative_eq_intros simp del: fact_Suc power_Suc
   100                  simp add: field_simps power_Suc[symmetric] real_of_nat_def[symmetric])
   101       also have "(\<lambda>x. ?F k x - (x^Suc k * exp (-x)) / fact (Suc k)) = ?F (Suc k)"
   102         by simp
   103       also have "?f k x - ((real (Suc k) - x) * x ^ k * exp (- x)) / (fact (Suc k)) = ?f (Suc k) x"
   104         by (auto simp: field_simps simp del: fact_Suc)
   105            (simp_all add: real_of_nat_Suc field_simps)
   106       finally show ?case .
   107     qed
   108   qed auto
   109   also have "\<dots> = ereal (1 - (\<Sum>n\<le>k. (a^n * exp (-a)) / fact n))"
   110     by (auto simp: power_0_left if_distrib[where f="\<lambda>x. x / a" for a] setsum.If_cases)
   111   finally show ?thesis
   112     by (cases "?I") (auto simp: field_simps)
   113 qed
   114 
   115 lemma nn_intergal_power_times_exp_Ici:
   116   shows "(\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel) = real_of_nat (fact k)"
   117 proof (rule LIMSEQ_unique)
   118   let ?X = "\<lambda>n. \<integral>\<^sup>+ x. ereal (x^k * exp (-x)) * indicator {0 .. real n} x \<partial>lborel"
   119   show "?X ----> (\<integral>\<^sup>+x. ereal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
   120     apply (intro nn_integral_LIMSEQ)
   121     apply (auto simp: incseq_def le_fun_def eventually_sequentially
   122                 split: split_indicator intro!: Lim_eventually)
   123     apply (metis nat_ceiling_le_eq)
   124     done
   125 
   126   have "((\<lambda>x::real. (1 - (\<Sum>n\<le>k. (x ^ n / exp x) / (fact n))) * fact k) --->
   127         (1 - (\<Sum>n\<le>k. 0 / (fact n))) * fact k) at_top"
   128     by (intro tendsto_intros tendsto_power_div_exp_0) simp
   129   then show "?X ----> real_of_nat (fact k)"
   130     by (subst nn_intergal_power_times_exp_Icc)
   131        (auto simp: exp_minus field_simps intro!: filterlim_compose[OF _ filterlim_real_sequentially])
   132 qed
   133 
   134 definition erlang_density :: "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   135   "erlang_density k l x = (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k)"
   136 
   137 definition erlang_CDF ::  "nat \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   138   "erlang_CDF k l x = (if x < 0 then 0 else 1 - (\<Sum>n\<le>k. ((l * x)^n * exp (- l * x) / fact n)))"
   139 
   140 lemma erlang_density_nonneg: "0 \<le> l \<Longrightarrow> 0 \<le> erlang_density k l x"
   141   by (simp add: erlang_density_def)
   142 
   143 lemma borel_measurable_erlang_density[measurable]: "erlang_density k l \<in> borel_measurable borel"
   144   by (auto simp add: erlang_density_def[abs_def])
   145 
   146 lemma erlang_CDF_transform: "0 < l \<Longrightarrow> erlang_CDF k l a = erlang_CDF k 1 (l * a)"
   147   by (auto simp add: erlang_CDF_def mult_less_0_iff)
   148 
   149 lemma nn_integral_erlang_density:
   150   assumes [arith]: "0 < l"
   151   shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = erlang_CDF k l a"
   152 proof cases
   153   assume [arith]: "0 \<le> a"
   154   have eq: "\<And>x. indicator {0..a} (x / l) = indicator {0..a*l} x"
   155     by (simp add: field_simps split: split_indicator)
   156   have "(\<integral>\<^sup>+x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) =
   157     (\<integral>\<^sup>+x. (l/fact k) * (ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x) \<partial>lborel)"
   158     by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib split: split_indicator)
   159   also have "\<dots> = (l/fact k) * (\<integral>\<^sup>+x. ereal ((l*x)^k * exp (- (l*x))) * indicator {0 .. a} x \<partial>lborel)"
   160     by (intro nn_integral_cmult) auto
   161   also have "\<dots> = ereal (l/fact k) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^k * exp (- x)) * indicator {0 .. l * a} x \<partial>lborel))"
   162     by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
   163   also have "\<dots> = (1 - (\<Sum>n\<le>k. ((l * a)^n * exp (-(l * a))) / fact n))"
   164     by (subst nn_intergal_power_times_exp_Icc) auto
   165   also have "\<dots> = erlang_CDF k l a"
   166     by (auto simp: erlang_CDF_def)
   167   finally show ?thesis .
   168 next
   169   assume "\<not> 0 \<le> a" 
   170   moreover then have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x) * indicator {.. a} x \<partial>lborel) = (\<integral>\<^sup>+x. 0 \<partial>(lborel::real measure))"
   171     by (intro nn_integral_cong) (auto simp: erlang_density_def)
   172   ultimately show ?thesis
   173     by (simp add: erlang_CDF_def)
   174 qed
   175 
   176 lemma emeasure_erlang_density: 
   177   "0 < l \<Longrightarrow> emeasure (density lborel (erlang_density k l)) {.. a} = erlang_CDF k l a"
   178   by (simp add: emeasure_density nn_integral_erlang_density)
   179 
   180 lemma nn_integral_erlang_ith_moment: 
   181   fixes k i :: nat and l :: real
   182   assumes [arith]: "0 < l" 
   183   shows "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x ^ i) \<partial>lborel) = fact (k + i) / (fact k * l ^ i)"
   184 proof -
   185   have eq: "\<And>x. indicator {0..} (x / l) = indicator {0..} x"
   186     by (simp add: field_simps split: split_indicator)
   187   have "(\<integral>\<^sup>+ x. ereal (erlang_density k l x * x^i) \<partial>lborel) =
   188     (\<integral>\<^sup>+x. (l/(fact k * l^i)) * (ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x) \<partial>lborel)"
   189     by (intro nn_integral_cong) (auto simp: erlang_density_def power_mult_distrib power_add split: split_indicator)
   190   also have "\<dots> = (l/(fact k * l^i)) * (\<integral>\<^sup>+x. ereal ((l*x)^(k+i) * exp (- (l*x))) * indicator {0 ..} x \<partial>lborel)"
   191     by (intro nn_integral_cmult) auto
   192   also have "\<dots> = ereal (l/(fact k * l^i)) * ((1/l) * (\<integral>\<^sup>+x. ereal (x^(k+i) * exp (- x)) * indicator {0 ..} x \<partial>lborel))"
   193     by (subst nn_integral_real_affine[where c="1 / l" and t=0]) (auto simp: field_simps eq)
   194   also have "\<dots> = fact (k + i) / (fact k * l ^ i)"
   195     by (subst nn_intergal_power_times_exp_Ici) auto
   196   finally show ?thesis .
   197 qed
   198 
   199 lemma prob_space_erlang_density:
   200   assumes l[arith]: "0 < l"
   201   shows "prob_space (density lborel (erlang_density k l))" (is "prob_space ?D")
   202 proof
   203   show "emeasure ?D (space ?D) = 1"
   204     using nn_integral_erlang_ith_moment[OF l, where k=k and i=0] by (simp add: emeasure_density)
   205 qed
   206 
   207 lemma (in prob_space) erlang_distributed_le:
   208   assumes D: "distributed M lborel X (erlang_density k l)"
   209   assumes [simp, arith]: "0 < l" "0 \<le> a"
   210   shows "\<P>(x in M. X x \<le> a) = erlang_CDF k l a"
   211 proof -
   212   have "emeasure M {x \<in> space M. X x \<le> a } = emeasure (distr M lborel X) {.. a}"
   213     using distributed_measurable[OF D]
   214     by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
   215   also have "\<dots> = emeasure (density lborel (erlang_density k l)) {.. a}"
   216     unfolding distributed_distr_eq_density[OF D] ..
   217   also have "\<dots> = erlang_CDF k l a"
   218     by (auto intro!: emeasure_erlang_density)
   219   finally show ?thesis
   220     by (auto simp: measure_def)
   221 qed
   222 
   223 lemma (in prob_space) erlang_distributed_gt:
   224   assumes D[simp]: "distributed M lborel X (erlang_density k l)"
   225   assumes [arith]: "0 < l" "0 \<le> a"
   226   shows "\<P>(x in M. a < X x ) = 1 - (erlang_CDF k l a)"
   227 proof -
   228   have " 1 - (erlang_CDF k l a) = 1 - \<P>(x in M. X x \<le> a)" by (subst erlang_distributed_le) auto
   229   also have "\<dots> = prob (space M - {x \<in> space M. X x \<le> a })"
   230     using distributed_measurable[OF D] by (auto simp: prob_compl)
   231   also have "\<dots> = \<P>(x in M. a < X x )" by (auto intro!: arg_cong[where f=prob] simp: not_le)
   232   finally show ?thesis by simp
   233 qed
   234 
   235 lemma erlang_CDF_at0: "erlang_CDF k l 0 = 0"
   236   by (induction k) (auto simp: erlang_CDF_def)
   237 
   238 lemma erlang_distributedI:
   239   assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
   240     and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = erlang_CDF k l a"
   241   shows "distributed M lborel X (erlang_density k l)"
   242 proof (rule distributedI_borel_atMost)
   243   fix a :: real
   244   { assume "a \<le> 0"  
   245     with X have "emeasure M {x\<in>space M. X x \<le> a} \<le> emeasure M {x\<in>space M. X x \<le> 0}"
   246       by (intro emeasure_mono) auto
   247     also have "... = 0"  by (auto intro!: erlang_CDF_at0 simp: X_distr[of 0])
   248     finally have "emeasure M {x\<in>space M. X x \<le> a} \<le> 0" by simp
   249     then have "emeasure M {x\<in>space M. X x \<le> a} = 0" by (simp add:emeasure_le_0_iff)
   250   }
   251   note eq_0 = this
   252 
   253   show "(\<integral>\<^sup>+ x. erlang_density k l x * indicator {..a} x \<partial>lborel) = ereal (erlang_CDF k l a)"
   254     using nn_integral_erlang_density[of l k a]
   255     by (simp add: times_ereal.simps(1)[symmetric] ereal_indicator del: times_ereal.simps)
   256 
   257   show "emeasure M {x\<in>space M. X x \<le> a} = ereal (erlang_CDF k l a)"
   258     using X_distr[of a] eq_0 by (auto simp: one_ereal_def erlang_CDF_def)
   259 qed (simp_all add: erlang_density_nonneg)
   260 
   261 lemma (in prob_space) erlang_distributed_iff:
   262   assumes [arith]: "0<l"
   263   shows "distributed M lborel X (erlang_density k l) \<longleftrightarrow>
   264     (X \<in> borel_measurable M \<and> 0 < l \<and>  (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = erlang_CDF k l a ))"
   265   using
   266     distributed_measurable[of M lborel X "erlang_density k l"]
   267     emeasure_erlang_density[of l]
   268     erlang_distributed_le[of X k l]
   269   by (auto intro!: erlang_distributedI simp: one_ereal_def emeasure_eq_measure) 
   270 
   271 lemma (in prob_space) erlang_distributed_mult_const:
   272   assumes erlX: "distributed M lborel X (erlang_density k l)"
   273   assumes a_pos[arith]: "0 < \<alpha>"  "0 < l"
   274   shows  "distributed M lborel (\<lambda>x. \<alpha> * X x) (erlang_density k (l / \<alpha>))"
   275 proof (subst erlang_distributed_iff, safe)
   276   have [measurable]: "random_variable borel X"  and  [arith]: "0 < l " 
   277   and  [simp]: "\<And>a. 0 \<le> a \<Longrightarrow> prob {x \<in> space M. X x \<le> a} = erlang_CDF k l a"
   278     by(insert erlX, auto simp: erlang_distributed_iff)
   279 
   280   show "random_variable borel (\<lambda>x. \<alpha> * X x)" "0 < l / \<alpha>"  "0 < l / \<alpha>" 
   281     by (auto simp:field_simps)
   282   
   283   fix a:: real assume [arith]: "0 \<le> a"
   284   obtain b:: real  where [simp, arith]: "b = a/ \<alpha>" by blast 
   285 
   286   have [arith]: "0 \<le> b" by (auto simp: divide_nonneg_pos)
   287  
   288   have "prob {x \<in> space M. \<alpha> * X x \<le> a}  = prob {x \<in> space M.  X x \<le> b}"
   289     by (rule arg_cong[where f= prob]) (auto simp:field_simps)
   290   
   291   moreover have "prob {x \<in> space M. X x \<le> b} = erlang_CDF k l b" by auto
   292   moreover have "erlang_CDF k (l / \<alpha>) a = erlang_CDF k l b" unfolding erlang_CDF_def by auto
   293   ultimately show "prob {x \<in> space M. \<alpha> * X x \<le> a} = erlang_CDF k (l / \<alpha>) a" by fastforce  
   294 qed
   295 
   296 lemma (in prob_space) has_bochner_integral_erlang_ith_moment:
   297   fixes k i :: nat and l :: real
   298   assumes [arith]: "0 < l" and D: "distributed M lborel X (erlang_density k l)"
   299   shows "has_bochner_integral M (\<lambda>x. X x ^ i) (fact (k + i) / (fact k * l ^ i))"
   300 proof (rule has_bochner_integral_nn_integral)
   301   show "AE x in M. 0 \<le> X x ^ i"
   302     by (subst distributed_AE2[OF D]) (auto simp: erlang_density_def)
   303   show "(\<integral>\<^sup>+ x. ereal (X x ^ i) \<partial>M) = ereal (fact (k + i) / (fact k * l ^ i))"
   304     using nn_integral_erlang_ith_moment[of l k i]
   305     by (subst distributed_nn_integral[symmetric, OF D]) auto
   306 qed (insert distributed_measurable[OF D], simp)
   307 
   308 lemma (in prob_space) erlang_ith_moment_integrable:
   309   "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow> integrable M (\<lambda>x. X x ^ i)"
   310   by rule (rule has_bochner_integral_erlang_ith_moment)
   311 
   312 lemma (in prob_space) erlang_ith_moment:
   313   "0 < l \<Longrightarrow> distributed M lborel X (erlang_density k l) \<Longrightarrow>
   314     expectation (\<lambda>x. X x ^ i) = fact (k + i) / (fact k * l ^ i)"
   315   by (rule has_bochner_integral_integral_eq) (rule has_bochner_integral_erlang_ith_moment)
   316 
   317 lemma (in prob_space) erlang_distributed_variance:
   318   assumes [arith]: "0 < l" and "distributed M lborel X (erlang_density k l)"
   319   shows "variance X = (k + 1) / l\<^sup>2"
   320 proof (subst variance_eq)
   321   show "integrable M X" "integrable M (\<lambda>x. (X x)\<^sup>2)"
   322     using erlang_ith_moment_integrable[OF assms, of 1] erlang_ith_moment_integrable[OF assms, of 2]
   323     by auto
   324 
   325   show "expectation (\<lambda>x. (X x)\<^sup>2) - (expectation X)\<^sup>2 = real (k + 1) / l\<^sup>2"
   326     using erlang_ith_moment[OF assms, of 1] erlang_ith_moment[OF assms, of 2]
   327     by simp (auto simp: power2_eq_square field_simps real_of_nat_Suc)
   328 qed
   329 
   330 subsection {* Exponential distribution *}
   331 
   332 abbreviation exponential_density :: "real \<Rightarrow> real \<Rightarrow> real" where
   333   "exponential_density \<equiv> erlang_density 0"
   334 
   335 lemma exponential_density_def:
   336   "exponential_density l x = (if x < 0 then 0 else l * exp (- x * l))"
   337   by (simp add: fun_eq_iff erlang_density_def)
   338 
   339 lemma erlang_CDF_0: "erlang_CDF 0 l a = (if 0 \<le> a then 1 - exp (- l * a) else 0)"
   340   by (simp add: erlang_CDF_def)
   341 
   342 lemma (in prob_space) exponential_distributed_params:
   343   assumes D: "distributed M lborel X (exponential_density l)"
   344   shows "0 < l"
   345 proof (cases l "0 :: real" rule: linorder_cases)
   346   assume "l < 0"
   347   have "emeasure lborel {0 <.. 1::real} \<le>
   348     emeasure lborel {x :: real \<in> space lborel. 0 < x}"
   349     by (rule emeasure_mono) (auto simp: greaterThan_def[symmetric])
   350   also have "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
   351   proof -
   352     have "AE x in lborel. 0 \<le> exponential_density l x"
   353       using assms by (auto simp: distributed_real_AE)
   354     then have "AE x in lborel. x \<le> (0::real)"
   355       apply eventually_elim 
   356       using `l < 0`
   357       apply (auto simp: exponential_density_def zero_le_mult_iff split: split_if_asm)
   358       done
   359     then show "emeasure lborel {x :: real \<in> space lborel. 0 < x} = 0"
   360       by (subst (asm) AE_iff_measurable[OF _ refl]) (auto simp: not_le greaterThan_def[symmetric])
   361   qed
   362   finally show "0 < l" by simp
   363 next
   364   assume "l = 0"
   365   then have [simp]: "\<And>x. ereal (exponential_density l x) = 0"
   366     by (simp add: exponential_density_def)
   367   interpret X: prob_space "distr M lborel X"
   368     using distributed_measurable[OF D] by (rule prob_space_distr)
   369   from X.emeasure_space_1
   370   show "0 < l"
   371     by (simp add: emeasure_density distributed_distr_eq_density[OF D])
   372 qed assumption
   373 
   374 lemma prob_space_exponential_density: "0 < l \<Longrightarrow> prob_space (density lborel (exponential_density l))"
   375   by (rule prob_space_erlang_density)
   376 
   377 lemma (in prob_space) exponential_distributedD_le:
   378   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   379   shows "\<P>(x in M. X x \<le> a) = 1 - exp (- a * l)"
   380   using erlang_distributed_le[OF D exponential_distributed_params[OF D] a] a
   381   by (simp add: erlang_CDF_def)
   382 
   383 lemma (in prob_space) exponential_distributedD_gt:
   384   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"
   385   shows "\<P>(x in M. a < X x ) = exp (- a * l)"
   386   using erlang_distributed_gt[OF D exponential_distributed_params[OF D] a] a
   387   by (simp add: erlang_CDF_def)
   388 
   389 lemma (in prob_space) exponential_distributed_memoryless:
   390   assumes D: "distributed M lborel X (exponential_density l)" and a: "0 \<le> a"and t: "0 \<le> t"
   391   shows "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. t < X x)"
   392 proof -
   393   have "\<P>(x in M. a + t < X x \<bar> a < X x) = \<P>(x in M. a + t < X x) / \<P>(x in M. a < X x)"
   394     using `0 \<le> t` by (auto simp: cond_prob_def intro!: arg_cong[where f=prob] arg_cong2[where f="op /"])
   395   also have "\<dots> = exp (- (a + t) * l) / exp (- a * l)"
   396     using a t by (simp add: exponential_distributedD_gt[OF D])
   397   also have "\<dots> = exp (- t * l)"
   398     using exponential_distributed_params[OF D] by (auto simp: field_simps exp_add[symmetric])
   399   finally show ?thesis
   400     using t by (simp add: exponential_distributedD_gt[OF D])
   401 qed
   402 
   403 lemma exponential_distributedI:
   404   assumes X[measurable]: "X \<in> borel_measurable M" and [arith]: "0 < l"
   405     and X_distr: "\<And>a. 0 \<le> a \<Longrightarrow> emeasure M {x\<in>space M. X x \<le> a} = 1 - exp (- a * l)"
   406   shows "distributed M lborel X (exponential_density l)"
   407 proof (rule erlang_distributedI)
   408   fix a :: real assume "0 \<le> a" then show "emeasure M {x \<in> space M. X x \<le> a} = ereal (erlang_CDF 0 l a)"
   409     using X_distr[of a] by (simp add: erlang_CDF_def one_ereal_def)
   410 qed fact+
   411 
   412 lemma (in prob_space) exponential_distributed_iff:
   413   "distributed M lborel X (exponential_density l) \<longleftrightarrow>
   414     (X \<in> borel_measurable M \<and> 0 < l \<and> (\<forall>a\<ge>0. \<P>(x in M. X x \<le> a) = 1 - exp (- a * l)))"
   415   using exponential_distributed_params[of X l] erlang_distributed_iff[of l X 0] by (auto simp: erlang_CDF_0)
   416 
   417 
   418 lemma (in prob_space) exponential_distributed_expectation:
   419   "distributed M lborel X (exponential_density l) \<Longrightarrow> expectation X = 1 / l"
   420   using erlang_ith_moment[OF exponential_distributed_params, of X l X 0 1] by simp
   421 
   422 lemma exponential_density_nonneg: "0 < l \<Longrightarrow> 0 \<le> exponential_density l x"
   423   by (auto simp: exponential_density_def)
   424 
   425 lemma (in prob_space) exponential_distributed_min:
   426   assumes expX: "distributed M lborel X (exponential_density l)"
   427   assumes expY: "distributed M lborel Y (exponential_density u)"
   428   assumes ind: "indep_var borel X borel Y"
   429   shows "distributed M lborel (\<lambda>x. min (X x) (Y x)) (exponential_density (l + u))"
   430 proof (subst exponential_distributed_iff, safe)
   431   have randX: "random_variable borel X" using expX by (simp add: exponential_distributed_iff)
   432   moreover have randY: "random_variable borel Y" using expY by (simp add: exponential_distributed_iff)
   433   ultimately show "random_variable borel (\<lambda>x. min (X x) (Y x))" by auto
   434   
   435   have "0 < l" by (rule exponential_distributed_params) fact
   436   moreover have "0 < u" by (rule exponential_distributed_params) fact
   437   ultimately  show " 0 < l + u" by force
   438 
   439   fix a::real assume a[arith]: "0 \<le> a"
   440   have gt1[simp]: "\<P>(x in M. a < X x ) = exp (- a * l)" by (rule exponential_distributedD_gt[OF expX a]) 
   441   have gt2[simp]: "\<P>(x in M. a < Y x ) = exp (- a * u)" by (rule exponential_distributedD_gt[OF expY a]) 
   442 
   443   have "\<P>(x in M. a < (min (X x) (Y x)) ) =  \<P>(x in M. a < (X x) \<and> a < (Y x))" by (auto intro!:arg_cong[where f=prob])
   444 
   445   also have " ... =  \<P>(x in M. a < (X x)) *  \<P>(x in M. a< (Y x) )"
   446     using prob_indep_random_variable[OF ind, of "{a <..}" "{a <..}"] by simp
   447   also have " ... = exp (- a * (l + u))" by (auto simp:field_simps mult_exp_exp)
   448   finally have indep_prob: "\<P>(x in M. a < (min (X x) (Y x)) ) = exp (- a * (l + u))" .
   449 
   450   have "{x \<in> space M. (min (X x) (Y x)) \<le>a } = (space M - {x \<in> space M. a<(min (X x) (Y x)) })"
   451     by auto
   452   then have "1 - prob {x \<in> space M. a < (min (X x) (Y x))} = prob {x \<in> space M. (min (X x) (Y x)) \<le> a}"
   453     using randX randY by (auto simp: prob_compl) 
   454   then show "prob {x \<in> space M. (min (X x) (Y x)) \<le> a} = 1 - exp (- a * (l + u))"
   455     using indep_prob by auto
   456 qed
   457  
   458 lemma (in prob_space) exponential_distributed_Min:
   459   assumes finI: "finite I"
   460   assumes A: "I \<noteq> {}"
   461   assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density (l i))"
   462   assumes ind: "indep_vars (\<lambda>i. borel) X I" 
   463   shows "distributed M lborel (\<lambda>x. Min ((\<lambda>i. X i x)`I)) (exponential_density (\<Sum>i\<in>I. l i))"
   464 using assms
   465 proof (induct rule: finite_ne_induct)
   466   case (singleton i) then show ?case by simp
   467 next
   468   case (insert i I)
   469   then have "distributed M lborel (\<lambda>x. min (X i x) (Min ((\<lambda>i. X i x)`I))) (exponential_density (l i + (\<Sum>i\<in>I. l i)))"
   470       by (intro exponential_distributed_min indep_vars_Min insert)
   471          (auto intro: indep_vars_subset) 
   472   then show ?case
   473     using insert by simp
   474 qed
   475 
   476 lemma (in prob_space) exponential_distributed_variance:
   477   "distributed M lborel X (exponential_density l) \<Longrightarrow> variance X = 1 / l\<^sup>2"
   478   using erlang_distributed_variance[OF exponential_distributed_params, of X l X 0] by simp
   479 
   480 lemma nn_integral_zero': "AE x in M. f x = 0 \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) = 0"
   481   by (simp cong: nn_integral_cong_AE)
   482 
   483 lemma convolution_erlang_density:
   484   fixes k\<^sub>1 k\<^sub>2 :: nat
   485   assumes [simp, arith]: "0 < l"
   486   shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y)) * ereal (erlang_density k\<^sub>2 l y) \<partial>lborel) =
   487     (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
   488       (is "?LHS = ?RHS")
   489 proof
   490   fix x :: real
   491   have "x \<le> 0 \<or> 0 < x"
   492     by arith
   493   then show "?LHS x = ?RHS x"
   494   proof
   495     assume "x \<le> 0" then show ?thesis
   496       apply (subst nn_integral_zero')
   497       apply (rule AE_I[where N="{0}"])
   498       apply (auto simp add: erlang_density_def not_less)
   499       done
   500   next
   501     note zero_le_mult_iff[simp] zero_le_divide_iff[simp]
   502   
   503     have I_eq1: "integral\<^sup>N lborel (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l) = 1"
   504       using nn_integral_erlang_ith_moment[of l "Suc k\<^sub>1 + Suc k\<^sub>2 - 1" 0] by (simp del: fact_Suc)
   505   
   506     have 1: "(\<integral>\<^sup>+ x. ereal (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l x * indicator {0<..} x) \<partial>lborel) = 1"
   507       apply (subst I_eq1[symmetric])
   508       unfolding erlang_density_def
   509       by (auto intro!: nn_integral_cong split:split_indicator)
   510   
   511     have "prob_space (density lborel ?LHS)"
   512       unfolding times_ereal.simps[symmetric]
   513       by (intro prob_space_convolution_density) 
   514          (auto intro!: prob_space_erlang_density erlang_density_nonneg)
   515     then have 2: "integral\<^sup>N lborel ?LHS = 1"
   516       by (auto dest!: prob_space.emeasure_space_1 simp: emeasure_density)
   517   
   518     let ?I = "(integral\<^sup>N lborel (\<lambda>y. ereal ((1 - y)^ k\<^sub>1 * y^k\<^sub>2 * indicator {0..1} y)))"
   519     let ?C = "(fact (Suc (k\<^sub>1 + k\<^sub>2))) / ((fact k\<^sub>1) * (fact k\<^sub>2))"
   520     let ?s = "Suc k\<^sub>1 + Suc k\<^sub>2 - 1"
   521     let ?L = "(\<lambda>x. \<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x- y) * erlang_density k\<^sub>2 l y * indicator {0..x} y) \<partial>lborel)"
   522 
   523     { fix x :: real assume [arith]: "0 < x"
   524       have *: "\<And>x y n. (x - y * x::real)^n = x^n * (1 - y)^n"
   525         unfolding power_mult_distrib[symmetric] by (simp add: field_simps)
   526     
   527       have "?LHS x = ?L x"
   528         unfolding erlang_density_def
   529         by (auto intro!: nn_integral_cong split:split_indicator)
   530       also have "... = (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
   531         apply (subst nn_integral_real_affine[where c=x and t = 0])
   532         apply (simp_all add: nn_integral_cmult[symmetric] nn_integral_multc[symmetric] erlang_density_nonneg del: fact_Suc)
   533         apply (intro nn_integral_cong)
   534         apply (auto simp add: erlang_density_def mult_less_0_iff exp_minus field_simps exp_diff power_add *
   535                     simp del: fact_Suc split: split_indicator)
   536         done
   537       finally have "(\<integral>\<^sup>+y. ereal (erlang_density k\<^sub>1 l (x - y) * erlang_density k\<^sub>2 l y) \<partial>lborel) = 
   538         (\<lambda>x. ereal ?C * ?I * erlang_density ?s l x) x"
   539         by simp }
   540     note * = this
   541 
   542     assume [arith]: "0 < x"
   543     have 3: "1 = integral\<^sup>N lborel (\<lambda>xa. ?LHS xa * indicator {0<..} xa)"
   544       by (subst 2[symmetric])
   545          (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"]
   546                simp: erlang_density_def  nn_integral_multc[symmetric] indicator_def split: split_if_asm)
   547     also have "... = integral\<^sup>N lborel (\<lambda>x. (ereal (?C) * ?I) * ((erlang_density ?s l x) * indicator {0<..} x))"
   548       by (auto intro!: nn_integral_cong simp: * split: split_indicator)
   549     also have "... = ereal (?C) * ?I"
   550       using 1
   551       by (auto simp: nn_integral_nonneg nn_integral_cmult)  
   552     finally have " ereal (?C) * ?I = 1" by presburger
   553   
   554     then show ?thesis
   555       using * by simp
   556   qed
   557 qed
   558 
   559 lemma (in prob_space) sum_indep_erlang:
   560   assumes indep: "indep_var borel X borel Y"
   561   assumes [simp, arith]: "0 < l"
   562   assumes erlX: "distributed M lborel X (erlang_density k\<^sub>1 l)"
   563   assumes erlY: "distributed M lborel Y (erlang_density k\<^sub>2 l)"
   564   shows "distributed M lborel (\<lambda>x. X x + Y x) (erlang_density (Suc k\<^sub>1 + Suc k\<^sub>2 - 1) l)"
   565   using assms
   566   apply (subst convolution_erlang_density[symmetric, OF `0<l`])
   567   apply (intro distributed_convolution)
   568   apply auto
   569   done
   570 
   571 lemma (in prob_space) erlang_distributed_setsum:
   572   assumes finI : "finite I"
   573   assumes A: "I \<noteq> {}"
   574   assumes [simp, arith]: "0 < l"
   575   assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (erlang_density (k i) l)"
   576   assumes ind: "indep_vars (\<lambda>i. borel) X I"
   577   shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((\<Sum>i\<in>I. Suc (k i)) - 1) l)"
   578 using assms
   579 proof (induct rule: finite_ne_induct)
   580   case (singleton i) then show ?case by auto
   581 next
   582   case (insert i I)
   583     then have "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) (erlang_density (Suc (k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1) l)"
   584       by(intro sum_indep_erlang indep_vars_setsum) (auto intro!: indep_vars_subset)
   585     also have "(\<lambda>x. (X i x) + (\<Sum>i\<in> I. X i x)) = (\<lambda>x. \<Sum>i\<in>insert i I. X i x)"
   586       using insert by auto
   587     also have "Suc(k i) + Suc ((\<Sum>i\<in>I. Suc (k i)) - 1) - 1 = (\<Sum>i\<in>insert i I. Suc (k i)) - 1"
   588       using insert by (auto intro!: Suc_pred simp: ac_simps)    
   589     finally show ?case by fast
   590 qed
   591 
   592 lemma (in prob_space) exponential_distributed_setsum:
   593   assumes finI: "finite I"
   594   assumes A: "I \<noteq> {}"
   595   assumes expX: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (exponential_density l)"
   596   assumes ind: "indep_vars (\<lambda>i. borel) X I" 
   597   shows "distributed M lborel (\<lambda>x. \<Sum>i\<in>I. X i x) (erlang_density ((card I) - 1) l)"
   598 proof -
   599   obtain i where "i \<in> I" using assms by auto
   600   note exponential_distributed_params[OF expX[OF this]]
   601   from erlang_distributed_setsum[OF assms(1,2) this assms(3,4)] show ?thesis by simp
   602 qed
   603 
   604 lemma (in information_space) entropy_exponential:
   605   assumes D: "distributed M lborel X (exponential_density l)"
   606   shows "entropy b lborel X = log b (exp 1 / l)"
   607 proof -
   608   have l[simp, arith]: "0 < l" by (rule exponential_distributed_params[OF D])
   609  
   610   have [simp]: "integrable lborel (exponential_density l)"
   611     using distributed_integrable[OF D, of "\<lambda>_. 1"] by simp
   612 
   613   have [simp]: "integral\<^sup>L lborel (exponential_density l) = 1"
   614     using distributed_integral[OF D, of "\<lambda>_. 1"] by (simp add: prob_space)
   615     
   616   have [simp]: "integrable lborel (\<lambda>x. exponential_density l x * x)"
   617     using erlang_ith_moment_integrable[OF l D, of 1] distributed_integrable[OF D, of "\<lambda>x. x"] by simp
   618 
   619   have [simp]: "integral\<^sup>L lborel (\<lambda>x. exponential_density l x * x) = 1 / l"
   620     using erlang_ith_moment[OF l D, of 1] distributed_integral[OF D, of "\<lambda>x. x"] by simp
   621     
   622   have "entropy b lborel X = - (\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel)"
   623     using D by (rule entropy_distr)
   624   also have "(\<integral> x. exponential_density l x * log b (exponential_density l x) \<partial>lborel) = 
   625     (\<integral> x. (ln l * exponential_density l x - l * (exponential_density l x * x)) / ln b \<partial>lborel)"
   626     by (intro integral_cong) (auto simp: log_def ln_mult exponential_density_def field_simps)
   627   also have "\<dots> = (ln l - 1) / ln b"
   628     by simp
   629   finally show ?thesis
   630     by (simp add: log_def divide_simps ln_div)
   631 qed
   632 
   633 subsection {* Uniform distribution *}
   634 
   635 lemma uniform_distrI:
   636   assumes X: "X \<in> measurable M M'"
   637     and A: "A \<in> sets M'" "emeasure M' A \<noteq> \<infinity>" "emeasure M' A \<noteq> 0"
   638   assumes distr: "\<And>B. B \<in> sets M' \<Longrightarrow> emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A"
   639   shows "distr M M' X = uniform_measure M' A"
   640   unfolding uniform_measure_def
   641 proof (intro measure_eqI)
   642   let ?f = "\<lambda>x. indicator A x / emeasure M' A"
   643   fix B assume B: "B \<in> sets (distr M M' X)"
   644   with X have "emeasure M (X -` B \<inter> space M) = emeasure M' (A \<inter> B) / emeasure M' A"
   645     by (simp add: distr[of B] measurable_sets)
   646   also have "\<dots> = (1 / emeasure M' A) * emeasure M' (A \<inter> B)"
   647      by simp
   648   also have "\<dots> = (\<integral>\<^sup>+ x. (1 / emeasure M' A) * indicator (A \<inter> B) x \<partial>M')"
   649     using A B
   650     by (intro nn_integral_cmult_indicator[symmetric]) (auto intro!: zero_le_divide_ereal)
   651   also have "\<dots> = (\<integral>\<^sup>+ x. ?f x * indicator B x \<partial>M')"
   652     by (rule nn_integral_cong) (auto split: split_indicator)
   653   finally show "emeasure (distr M M' X) B = emeasure (density M' ?f) B"
   654     using A B X by (auto simp add: emeasure_distr emeasure_density)
   655 qed simp
   656 
   657 lemma uniform_distrI_borel:
   658   fixes A :: "real set"
   659   assumes X[measurable]: "X \<in> borel_measurable M" and A: "emeasure lborel A = ereal r" "0 < r"
   660     and [measurable]: "A \<in> sets borel"
   661   assumes distr: "\<And>a. emeasure M {x\<in>space M. X x \<le> a} = emeasure lborel (A \<inter> {.. a}) / r"
   662   shows "distributed M lborel X (\<lambda>x. indicator A x / measure lborel A)"
   663 proof (rule distributedI_borel_atMost)
   664   let ?f = "\<lambda>x. 1 / r * indicator A x"
   665   fix a
   666   have "emeasure lborel (A \<inter> {..a}) \<le> emeasure lborel A"
   667     using A by (intro emeasure_mono) auto
   668   also have "\<dots> < \<infinity>"
   669     using A by simp
   670   finally have fin: "emeasure lborel (A \<inter> {..a}) \<noteq> \<infinity>"
   671     by simp
   672   from emeasure_eq_ereal_measure[OF this]
   673   have fin_eq: "emeasure lborel (A \<inter> {..a}) / r = ereal (measure lborel (A \<inter> {..a}) / r)"
   674     using A by simp
   675   then show "emeasure M {x\<in>space M. X x \<le> a} = ereal (measure lborel (A \<inter> {..a}) / r)"
   676     using distr by simp
   677  
   678   have "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
   679     (\<integral>\<^sup>+ x. ereal (1 / measure lborel A) * indicator (A \<inter> {..a}) x \<partial>lborel)"
   680     by (auto intro!: nn_integral_cong split: split_indicator)
   681   also have "\<dots> = ereal (1 / measure lborel A) * emeasure lborel (A \<inter> {..a})"
   682     using `A \<in> sets borel`
   683     by (intro nn_integral_cmult_indicator) (auto simp: measure_nonneg)
   684   also have "\<dots> = ereal (measure lborel (A \<inter> {..a}) / r)"
   685     unfolding emeasure_eq_ereal_measure[OF fin] using A by (simp add: measure_def)
   686   finally show "(\<integral>\<^sup>+ x. ereal (indicator A x / measure lborel A * indicator {..a} x) \<partial>lborel) =
   687     ereal (measure lborel (A \<inter> {..a}) / r)" .
   688 qed (auto simp: measure_nonneg)
   689 
   690 lemma (in prob_space) uniform_distrI_borel_atLeastAtMost:
   691   fixes a b :: real
   692   assumes X: "X \<in> borel_measurable M" and "a < b"
   693   assumes distr: "\<And>t. a \<le> t \<Longrightarrow> t \<le> b \<Longrightarrow> \<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
   694   shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b})"
   695 proof (rule uniform_distrI_borel)
   696   fix t
   697   have "t < a \<or> (a \<le> t \<and> t \<le> b) \<or> b < t"
   698     by auto
   699   then show "emeasure M {x\<in>space M. X x \<le> t} = emeasure lborel ({a .. b} \<inter> {..t}) / (b - a)"
   700   proof (elim disjE conjE)
   701     assume "t < a" 
   702     then have "emeasure M {x\<in>space M. X x \<le> t} \<le> emeasure M {x\<in>space M. X x \<le> a}"
   703       using X by (auto intro!: emeasure_mono measurable_sets)
   704     also have "\<dots> = 0"
   705       using distr[of a] `a < b` by (simp add: emeasure_eq_measure)
   706     finally have "emeasure M {x\<in>space M. X x \<le> t} = 0"
   707       by (simp add: antisym measure_nonneg emeasure_le_0_iff)
   708     with `t < a` show ?thesis by simp
   709   next
   710     assume bnds: "a \<le> t" "t \<le> b"
   711     have "{a..b} \<inter> {..t} = {a..t}"
   712       using bnds by auto
   713     then show ?thesis using `a \<le> t` `a < b`
   714       using distr[OF bnds] by (simp add: emeasure_eq_measure)
   715   next
   716     assume "b < t" 
   717     have "1 = emeasure M {x\<in>space M. X x \<le> b}"
   718       using distr[of b] `a < b` by (simp add: one_ereal_def emeasure_eq_measure)
   719     also have "\<dots> \<le> emeasure M {x\<in>space M. X x \<le> t}"
   720       using X `b < t` by (auto intro!: emeasure_mono measurable_sets)
   721     finally have "emeasure M {x\<in>space M. X x \<le> t} = 1"
   722        by (simp add: antisym emeasure_eq_measure one_ereal_def)
   723     with `b < t` `a < b` show ?thesis by (simp add: measure_def one_ereal_def)
   724   qed
   725 qed (insert X `a < b`, auto)
   726 
   727 lemma (in prob_space) uniform_distributed_measure:
   728   fixes a b :: real
   729   assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
   730   assumes " a \<le> t" "t \<le> b"
   731   shows "\<P>(x in M. X x \<le> t) = (t - a) / (b - a)"
   732 proof -
   733   have "emeasure M {x \<in> space M. X x \<le> t} = emeasure (distr M lborel X) {.. t}"
   734     using distributed_measurable[OF D]
   735     by (subst emeasure_distr) (auto intro!: arg_cong2[where f=emeasure])
   736   also have "\<dots> = (\<integral>\<^sup>+x. ereal (1 / (b - a)) * indicator {a .. t} x \<partial>lborel)"
   737     using distributed_borel_measurable[OF D] `a \<le> t` `t \<le> b`
   738     unfolding distributed_distr_eq_density[OF D]
   739     by (subst emeasure_density)
   740        (auto intro!: nn_integral_cong simp: measure_def split: split_indicator)
   741   also have "\<dots> = ereal (1 / (b - a)) * (t - a)"
   742     using `a \<le> t` `t \<le> b`
   743     by (subst nn_integral_cmult_indicator) auto
   744   finally show ?thesis
   745     by (simp add: measure_def)
   746 qed
   747 
   748 lemma (in prob_space) uniform_distributed_bounds:
   749   fixes a b :: real
   750   assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
   751   shows "a < b"
   752 proof (rule ccontr)
   753   assume "\<not> a < b"
   754   then have "{a .. b} = {} \<or> {a .. b} = {a .. a}" by simp
   755   with uniform_distributed_params[OF D] show False 
   756     by (auto simp: measure_def)
   757 qed
   758 
   759 lemma (in prob_space) uniform_distributed_iff:
   760   fixes a b :: real
   761   shows "distributed M lborel X (\<lambda>x. indicator {a..b} x / measure lborel {a..b}) \<longleftrightarrow> 
   762     (X \<in> borel_measurable M \<and> a < b \<and> (\<forall>t\<in>{a .. b}. \<P>(x in M. X x \<le> t)= (t - a) / (b - a)))"
   763   using
   764     uniform_distributed_bounds[of X a b]
   765     uniform_distributed_measure[of X a b]
   766     distributed_measurable[of M lborel X]
   767   by (auto intro!: uniform_distrI_borel_atLeastAtMost)
   768 
   769 lemma (in prob_space) uniform_distributed_expectation:
   770   fixes a b :: real
   771   assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
   772   shows "expectation X = (a + b) / 2"
   773 proof (subst distributed_integral[OF D, of "\<lambda>x. x", symmetric])
   774   have "a < b"
   775     using uniform_distributed_bounds[OF D] .
   776 
   777   have "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = 
   778     (\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel)"
   779     by (intro integral_cong) auto
   780   also have "(\<integral> x. (x / measure lborel {a .. b}) * indicator {a .. b} x \<partial>lborel) = (a + b) / 2"
   781   proof (subst integral_FTC_Icc_real)
   782     fix x
   783     show "DERIV (\<lambda>x. x\<^sup>2 / (2 * measure lborel {a..b})) x :> x / measure lborel {a..b}"
   784       using uniform_distributed_params[OF D]
   785       by (auto intro!: derivative_eq_intros)
   786     show "isCont (\<lambda>x. x / Sigma_Algebra.measure lborel {a..b}) x"
   787       using uniform_distributed_params[OF D]
   788       by (auto intro!: isCont_divide)
   789     have *: "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) =
   790       (b*b - a * a) / (2 * (b - a))"
   791       using `a < b`
   792       by (auto simp: measure_def power2_eq_square diff_divide_distrib[symmetric])
   793     show "b\<^sup>2 / (2 * measure lborel {a..b}) - a\<^sup>2 / (2 * measure lborel {a..b}) = (a + b) / 2"
   794       using `a < b`
   795       unfolding * square_diff_square_factored by (auto simp: field_simps)
   796   qed (insert `a < b`, simp)
   797   finally show "(\<integral> x. indicator {a .. b} x / measure lborel {a .. b} * x \<partial>lborel) = (a + b) / 2" .
   798 qed auto
   799 
   800 lemma (in prob_space) uniform_distributed_variance:
   801   fixes a b :: real
   802   assumes D: "distributed M lborel X (\<lambda>x. indicator {a .. b} x / measure lborel {a .. b})"
   803   shows "variance X = (b - a)\<^sup>2 / 12"
   804 proof (subst distributed_variance)
   805   have [arith]: "a < b" using uniform_distributed_bounds[OF D] .
   806   let ?\<mu> = "expectation X" let ?D = "\<lambda>x. indicator {a..b} (x + ?\<mu>) / measure lborel {a..b}"
   807   have "(\<integral>x. x\<^sup>2 * (?D x) \<partial>lborel) = (\<integral>x. x\<^sup>2 * (indicator {a - ?\<mu> .. b - ?\<mu>} x) / measure lborel {a .. b} \<partial>lborel)"
   808     by (intro integral_cong) (auto split: split_indicator)
   809   also have "\<dots> = (b - a)\<^sup>2 / 12"
   810     by (simp add: integral_power uniform_distributed_expectation[OF D])
   811        (simp add: eval_nat_numeral field_simps )
   812   finally show "(\<integral>x. x\<^sup>2 * ?D x \<partial>lborel) = (b - a)\<^sup>2 / 12" .
   813 qed fact
   814 
   815 subsection {* Normal distribution *}
   816 
   817 
   818 definition normal_density :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
   819   "normal_density \<mu> \<sigma> x = 1 / sqrt (2 * pi * \<sigma>\<^sup>2) * exp (-(x - \<mu>)\<^sup>2/ (2 * \<sigma>\<^sup>2))"
   820 
   821 abbreviation std_normal_density :: "real \<Rightarrow> real" where
   822   "std_normal_density \<equiv> normal_density 0 1"
   823 
   824 lemma std_normal_density_def: "std_normal_density x = (1 / sqrt (2 * pi)) * exp (- x\<^sup>2 / 2)"
   825   unfolding normal_density_def by simp
   826 
   827 lemma normal_density_nonneg: "0 \<le> normal_density \<mu> \<sigma> x"
   828   by (auto simp: normal_density_def)
   829 
   830 lemma normal_density_pos: "0 < \<sigma> \<Longrightarrow> 0 < normal_density \<mu> \<sigma> x"
   831   by (auto simp: normal_density_def)
   832 
   833 lemma borel_measurable_normal_density[measurable]: "normal_density \<mu> \<sigma> \<in> borel_measurable borel"
   834   by (auto simp: normal_density_def[abs_def])
   835 
   836 lemma gaussian_moment_0:
   837   "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2)) (sqrt pi / 2)"
   838 proof -
   839   let ?pI = "\<lambda>f. (\<integral>\<^sup>+s. f (s::real) * indicator {0..} s \<partial>lborel)"
   840   let ?gauss = "\<lambda>x. exp (- x\<^sup>2)"
   841 
   842   let ?I = "indicator {0<..} :: real \<Rightarrow> real"
   843   let ?ff= "\<lambda>x s. x * exp (- x\<^sup>2 * (1 + s\<^sup>2)) :: real"
   844 
   845   have *: "?pI ?gauss = (\<integral>\<^sup>+x. ?gauss x * ?I x \<partial>lborel)"
   846     by (intro nn_integral_cong_AE AE_I[where N="{0}"]) (auto split: split_indicator)
   847 
   848   have "?pI ?gauss * ?pI ?gauss = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel \<partial>lborel)"
   849     by (auto simp: nn_integral_nonneg nn_integral_cmult[symmetric] nn_integral_multc[symmetric] *
   850              intro!: nn_integral_cong split: split_indicator)
   851   also have "\<dots> = (\<integral>\<^sup>+x. \<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel)"
   852   proof (rule nn_integral_cong, cases)
   853     fix x :: real assume "x \<noteq> 0"
   854     then show "(\<integral>\<^sup>+s. ?gauss x * ?gauss s * ?I s * ?I x \<partial>lborel) = (\<integral>\<^sup>+s. ?ff x s * ?I s * ?I x \<partial>lborel)"
   855       by (subst nn_integral_real_affine[where t="0" and c="x"])
   856          (auto simp: mult_exp_exp nn_integral_cmult[symmetric] field_simps zero_less_mult_iff
   857                intro!: nn_integral_cong split: split_indicator)
   858   qed simp
   859   also have "... = \<integral>\<^sup>+s. \<integral>\<^sup>+x. ?ff x s * ?I s * ?I x \<partial>lborel \<partial>lborel"
   860     by (rule lborel_pair.Fubini'[symmetric]) auto
   861   also have "... = ?pI (\<lambda>s. ?pI (\<lambda>x. ?ff x s))"
   862     by (rule nn_integral_cong_AE)
   863        (auto intro!: nn_integral_cong_AE AE_I[where N="{0}"] split: split_indicator_asm)
   864   also have "\<dots> = ?pI (\<lambda>s. ereal (1 / (2 * (1 + s\<^sup>2))))"
   865   proof (intro nn_integral_cong ereal_right_mult_cong)
   866     fix s :: real show "?pI (\<lambda>x. ?ff x s) = ereal (1 / (2 * (1 + s\<^sup>2)))"
   867     proof (subst nn_integral_FTC_atLeast)
   868       have "((\<lambda>a. - (exp (- (a\<^sup>2 * (1 + s\<^sup>2))) / (2 + 2 * s\<^sup>2))) ---> (- (0 / (2 + 2 * s\<^sup>2)))) at_top"
   869         apply (intro tendsto_intros filterlim_compose[OF exp_at_bot] filterlim_compose[OF filterlim_uminus_at_bot_at_top])
   870         apply (subst mult.commute)         
   871         apply (auto intro!: filterlim_tendsto_pos_mult_at_top
   872                             filterlim_at_top_mult_at_top[OF filterlim_ident filterlim_ident] 
   873                     simp: add_pos_nonneg  power2_eq_square add_nonneg_eq_0_iff)
   874         done
   875       then show "((\<lambda>a. - (exp (- a\<^sup>2 - s\<^sup>2 * a\<^sup>2) / (2 + 2 * s\<^sup>2))) ---> 0) at_top"
   876         by (simp add: field_simps)
   877     qed (auto intro!: derivative_eq_intros simp: field_simps add_nonneg_eq_0_iff)
   878   qed rule
   879   also have "... = ereal (pi / 4)"
   880   proof (subst nn_integral_FTC_atLeast)
   881     show "((\<lambda>a. arctan a / 2) ---> (pi / 2) / 2 ) at_top"
   882       by (intro tendsto_intros) (simp_all add: tendsto_arctan_at_top)
   883   qed (auto intro!: derivative_eq_intros simp: add_nonneg_eq_0_iff field_simps power2_eq_square)
   884   finally have "?pI ?gauss^2 = pi / 4"
   885     by (simp add: power2_eq_square)
   886   then have "?pI ?gauss = sqrt (pi / 4)"
   887     using power_eq_iff_eq_base[of 2 "real (?pI ?gauss)" "sqrt (pi / 4)"]
   888           nn_integral_nonneg[of lborel "\<lambda>x. ?gauss x * indicator {0..} x"]
   889     by (cases "?pI ?gauss") auto
   890   also have "?pI ?gauss = (\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R exp (- x\<^sup>2) \<partial>lborel)"
   891     by (intro nn_integral_cong) (simp split: split_indicator)
   892   also have "sqrt (pi / 4) = sqrt pi / 2"
   893     by (simp add: real_sqrt_divide)
   894   finally show ?thesis
   895     by (rule has_bochner_integral_nn_integral[rotated 2]) auto
   896 qed
   897 
   898 lemma gaussian_moment_1:
   899   "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x)) (1 / 2)" 
   900 proof - 
   901   have "(\<integral>\<^sup>+x. indicator {0..} x *\<^sub>R (exp (- x\<^sup>2) * x) \<partial>lborel) =
   902     (\<integral>\<^sup>+x. ereal (x * exp (- x\<^sup>2)) * indicator {0..} x \<partial>lborel)"
   903     by (intro nn_integral_cong)
   904        (auto simp: ac_simps times_ereal.simps(1)[symmetric] ereal_indicator simp del: times_ereal.simps)
   905   also have "\<dots> = ereal (0 - (- exp (- 0\<^sup>2) / 2))"
   906   proof (rule nn_integral_FTC_atLeast)
   907     have "((\<lambda>x::real. - exp (- x\<^sup>2) / 2) ---> - 0 / 2) at_top"
   908       by (intro tendsto_divide tendsto_minus filterlim_compose[OF exp_at_bot]
   909                    filterlim_compose[OF filterlim_uminus_at_bot_at_top]
   910                    filterlim_pow_at_top filterlim_ident)
   911          auto
   912     then show "((\<lambda>a::real. - exp (- a\<^sup>2) / 2) ---> 0) at_top"
   913       by simp
   914   qed (auto intro!: derivative_eq_intros)
   915   also have "\<dots> = ereal (1 / 2)"
   916     by simp
   917   finally show ?thesis
   918     by (rule has_bochner_integral_nn_integral[rotated 2]) (auto split: split_indicator)
   919 qed
   920 
   921 lemma
   922   fixes k :: nat
   923   shows gaussian_moment_even_pos:
   924     "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k)))
   925        ((sqrt pi / 2) * (fact (2 * k) / (2 ^ (2 * k) * fact k)))" 
   926        (is "?even")
   927     and gaussian_moment_odd_pos:
   928       "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*x^(2 * k + 1))) (fact k / 2)" 
   929       (is "?odd")
   930 proof -
   931   let ?M = "\<lambda>k x. exp (- x\<^sup>2) * x^k :: real"
   932 
   933   { fix k I assume Mk: "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M k x) I"
   934     have "2 \<noteq> (0::real)"
   935       by linarith
   936     let ?f = "\<lambda>b. \<integral>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..b} x \<partial>lborel"
   937     have "((\<lambda>b. (k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x) \<partial>lborel) - ?M (k + 1) b / 2) --->
   938         (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top" (is ?tendsto)
   939     proof (intro tendsto_intros `2 \<noteq> 0` tendsto_integral_at_top sets_lborel Mk[THEN integrable.intros])
   940       show "(?M (k + 1) ---> 0) at_top"
   941       proof cases
   942         assume "even k"
   943         have "((\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) ---> 0 * 0) at_top"
   944           by (intro tendsto_intros tendsto_divide_0[OF tendsto_const] filterlim_compose[OF tendsto_power_div_exp_0]
   945                    filterlim_at_top_imp_at_infinity filterlim_ident filterlim_pow_at_top filterlim_ident)
   946              auto
   947         also have "(\<lambda>x. ((x\<^sup>2)^(k div 2 + 1) / exp (x\<^sup>2)) * (1 / x) :: real) = ?M (k + 1)"
   948           using `even k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: evenE)
   949         finally show ?thesis by simp
   950       next
   951         assume "odd k"
   952         have "((\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) ---> 0) at_top"
   953           by (intro filterlim_compose[OF tendsto_power_div_exp_0] filterlim_at_top_imp_at_infinity
   954                     filterlim_ident filterlim_pow_at_top)
   955              auto
   956         also have "(\<lambda>x. ((x\<^sup>2)^((k - 1) div 2 + 1) / exp (x\<^sup>2)) :: real) = ?M (k + 1)"
   957           using `odd k` by (auto simp: fun_eq_iff exp_minus field_simps power2_eq_square power_mult elim: oddE)
   958         finally show ?thesis by simp
   959       qed
   960     qed
   961     also have "?tendsto \<longleftrightarrow> ((?f ---> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel) - 0 / 2) at_top)"
   962     proof (intro filterlim_cong refl eventually_at_top_linorder[THEN iffD2] exI[of _ 0] allI impI)
   963       fix b :: real assume b: "0 \<le> b"
   964       have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) = (\<integral>x. indicator {0..b} x *\<^sub>R (exp (- x\<^sup>2) * ((Suc k) * x ^ k)) \<partial>lborel)"
   965         unfolding integral_mult_right_zero[symmetric] by (intro integral_cong) auto
   966       also have "\<dots> = exp (- b\<^sup>2) * b ^ (Suc k) - exp (- 0\<^sup>2) * 0 ^ (Suc k) -
   967           (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel)"
   968         by (rule integral_by_parts')
   969            (auto intro!: derivative_eq_intros b
   970                  simp: real_of_nat_def[symmetric] diff_Suc real_of_nat_Suc field_simps split: nat.split)
   971       also have "(\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * x * exp (- x\<^sup>2) * x ^ (Suc k)) \<partial>lborel) =
   972         (\<integral>x. indicator {0..b} x *\<^sub>R (- 2 * (exp (- x\<^sup>2) * x ^ (k + 2))) \<partial>lborel)"
   973         by (intro integral_cong) auto
   974       finally have "Suc k * (\<integral>x. indicator {0..b} x *\<^sub>R ?M k x \<partial>lborel) =
   975         exp (- b\<^sup>2) * b ^ (Suc k) + 2 * (\<integral>x. indicator {0..b} x *\<^sub>R ?M (k + 2) x \<partial>lborel)"
   976         apply (simp del: real_scaleR_def integral_mult_right add: integral_mult_right[symmetric])
   977         apply (subst integral_mult_right_zero[symmetric])
   978         apply (intro integral_cong)
   979         apply simp_all
   980         done
   981       then show "(k + 1) / 2 * (\<integral>x. indicator {..b} x *\<^sub>R (indicator {0..} x *\<^sub>R ?M k x)\<partial>lborel) - exp (- b\<^sup>2) * b ^ (k + 1) / 2 = ?f b"
   982         by (simp add: field_simps atLeastAtMost_def indicator_inter_arith)
   983     qed
   984     finally have int_M_at_top: "((?f ---> (k + 1) / 2 * (\<integral>x. indicator {0..} x *\<^sub>R ?M k x \<partial>lborel)) at_top)"
   985       by simp
   986     
   987     have "has_bochner_integral lborel (\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x) ((k + 1) / 2 * I)"
   988     proof (rule has_bochner_integral_monotone_convergence_at_top)
   989       fix y :: real
   990       have *: "(\<lambda>x. indicator {0..} x *\<^sub>R ?M (k + 2) x * indicator {..y} x::real) =
   991             (\<lambda>x. indicator {0..y} x *\<^sub>R ?M (k + 2) x)"
   992         by rule (simp split: split_indicator)
   993       show "integrable lborel (\<lambda>x. indicator {0..} x *\<^sub>R (?M (k + 2) x) * indicator {..y} x::real)"
   994         unfolding * by (rule borel_integrable_compact) (auto intro!: continuous_intros)
   995       show "((?f ---> (k + 1) / 2 * I) at_top)"
   996         using int_M_at_top has_bochner_integral_integral_eq[OF Mk] by simp
   997     qed (auto split: split_indicator) }
   998   note step = this
   999 
  1000   show ?even
  1001   proof (induct k)
  1002     case (Suc k)
  1003     note step[OF this]
  1004     also have "(real (2 * k + 1) / 2 * (sqrt pi / 2 * ((fact (2 * k)) / ((2::real)^(2*k) * fact k)))) =
  1005       sqrt pi / 2 * ((fact (2 * Suc k)) / ((2::real)^(2 * Suc k) * fact (Suc k)))"
  1006       apply (simp add: field_simps del: fact_Suc)
  1007       apply (simp add: real_of_nat_def of_nat_mult field_simps)
  1008       done
  1009     finally show ?case
  1010       by simp
  1011   qed (insert gaussian_moment_0, simp)
  1012 
  1013   show ?odd
  1014   proof (induct k)
  1015     case (Suc k)
  1016     note step[OF this]
  1017     also have "(real (2 * k + 1 + 1) / (2::real) * ((fact k) / 2)) = (fact (Suc k)) / 2"
  1018       by (simp add: field_simps real_of_nat_Suc divide_simps del: fact_Suc) (simp add: field_simps)
  1019     finally show ?case
  1020       by simp
  1021   qed (insert gaussian_moment_1, simp)
  1022 qed
  1023 
  1024 context
  1025   fixes k :: nat and \<mu> \<sigma> :: real assumes [arith]: "0 < \<sigma>"
  1026 begin
  1027 
  1028 lemma normal_moment_even:
  1029   "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>) ^ (2 * k)) (fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k))"
  1030 proof -
  1031   have eq: "\<And>x::real. x\<^sup>2^k = (x^k)\<^sup>2"
  1032     by (simp add: power_mult[symmetric] ac_simps)
  1033 
  1034   have "has_bochner_integral lborel (\<lambda>x. exp (-x\<^sup>2)*x^(2 * k))
  1035       (sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k)))"
  1036     using has_bochner_integral_even_function[OF gaussian_moment_even_pos[where k=k]] by simp
  1037   then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2)))
  1038       ((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2)))"
  1039     by (rule has_bochner_integral_mult_left)
  1040   also have "(\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k)) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) =
  1041     (\<lambda>x. exp (- ((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2*\<sigma>\<^sup>2)) * ((sqrt 2 * \<sigma>) * x) ^ (2 * k) / sqrt (2 * pi * \<sigma>\<^sup>2))"
  1042     by (auto simp: fun_eq_iff field_simps real_sqrt_power[symmetric] real_sqrt_mult
  1043                    real_sqrt_divide power_mult eq)
  1044   also have "((sqrt pi * (fact (2 * k) / (2 ^ (2 * k) * fact k))) * ((2*\<sigma>\<^sup>2)^k / sqrt (2 * pi * \<sigma>\<^sup>2))) = 
  1045     (inverse (sqrt 2 * \<sigma>) * ((fact (2 * k))) / ((2/\<sigma>\<^sup>2) ^ k * (fact k)))"
  1046     by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_mult
  1047                    power2_eq_square)
  1048   finally show ?thesis
  1049     unfolding normal_density_def
  1050     by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all
  1051 qed
  1052 
  1053 lemma normal_moment_abs_odd:
  1054   "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) (2^k * \<sigma>^(2 * k + 1) * fact k * sqrt (2 / pi))"
  1055 proof -
  1056   have "has_bochner_integral lborel (\<lambda>x::real. indicator {0..} x *\<^sub>R (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1))) (fact k / 2)"
  1057     by (rule has_bochner_integral_cong[THEN iffD1, OF _ _ _ gaussian_moment_odd_pos[of k]]) auto
  1058   from has_bochner_integral_even_function[OF this]
  1059   have "has_bochner_integral lborel (\<lambda>x::real. exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) (fact k)"
  1060     by simp
  1061   then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))
  1062       (fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2)))"
  1063     by (rule has_bochner_integral_mult_left)
  1064   also have "(\<lambda>x. (exp (-x\<^sup>2)*\<bar>x\<bar>^(2 * k + 1)) * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) =
  1065     (\<lambda>x. exp (- (((sqrt 2 * \<sigma>) * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) * \<bar>sqrt 2 * \<sigma> * x\<bar> ^ (2 * k + 1) / sqrt (2 * pi * \<sigma>\<^sup>2))"
  1066     by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult real_sqrt_mult)
  1067   also have "(fact k * (2^k * \<sigma>^(2 * k + 1) / sqrt (pi * \<sigma>\<^sup>2))) = 
  1068     (inverse (sqrt 2) * inverse \<sigma> * (2 ^ k * (\<sigma> * \<sigma> ^ (2 * k)) * (fact k) * sqrt (2 / pi)))"
  1069     by (auto simp: fun_eq_iff power_mult field_simps real_sqrt_power[symmetric] real_sqrt_divide
  1070                    real_sqrt_mult)
  1071   finally show ?thesis
  1072     unfolding normal_density_def
  1073     by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>])
  1074        simp_all
  1075 qed
  1076 
  1077 lemma normal_moment_odd:
  1078   "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k + 1)) 0"
  1079 proof -
  1080   have "has_bochner_integral lborel (\<lambda>x. exp (- x\<^sup>2) * x^(2 * k + 1)::real) 0"
  1081     using gaussian_moment_odd_pos by (rule has_bochner_integral_odd_function) simp
  1082   then have "has_bochner_integral lborel (\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi))
  1083       (0 * (2^k*\<sigma>^(2*k)/sqrt pi))"
  1084     by (rule has_bochner_integral_mult_left)
  1085   also have "(\<lambda>x. (exp (-x\<^sup>2)*x^(2 * k + 1)) * (2^k*\<sigma>^(2*k)/sqrt pi)) =
  1086     (\<lambda>x. exp (- ((sqrt 2 * \<sigma> * x)\<^sup>2 / (2 * \<sigma>\<^sup>2))) *
  1087           (sqrt 2 * \<sigma> * x * (sqrt 2 * \<sigma> * x) ^ (2 * k)) /
  1088           sqrt (2 * pi * \<sigma>\<^sup>2))"
  1089     unfolding real_sqrt_mult
  1090     by (simp add: field_simps abs_mult real_sqrt_power[symmetric] power_mult fun_eq_iff)
  1091   finally show ?thesis
  1092     unfolding normal_density_def
  1093     by (subst lborel_has_bochner_integral_real_affine_iff[where c="sqrt 2 * \<sigma>" and t=\<mu>]) simp_all
  1094 qed
  1095 
  1096 lemma integral_normal_moment_even:
  1097   "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k)) = fact (2 * k) / ((2 / \<sigma>\<^sup>2)^k * fact k)"
  1098   using normal_moment_even by (rule has_bochner_integral_integral_eq)
  1099 
  1100 lemma integral_normal_moment_abs_odd:
  1101   "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^(2 * k + 1)) = 2 ^ k * \<sigma> ^ (2 * k + 1) * fact k * sqrt (2 / pi)"
  1102   using normal_moment_abs_odd by (rule has_bochner_integral_integral_eq)
  1103 
  1104 lemma integral_normal_moment_odd:
  1105   "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^(2 * k + 1)) = 0"
  1106   using normal_moment_odd by (rule has_bochner_integral_integral_eq)
  1107 
  1108 end
  1109 
  1110 
  1111 context
  1112   fixes \<sigma> :: real
  1113   assumes \<sigma>_pos[arith]: "0 < \<sigma>"
  1114 begin
  1115 
  1116 lemma normal_moment_nz_1: "has_bochner_integral lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) \<mu>"
  1117 proof -
  1118   note normal_moment_even[OF \<sigma>_pos, of \<mu> 0]
  1119   note normal_moment_odd[OF \<sigma>_pos, of \<mu> 0] has_bochner_integral_mult_left[of \<mu>, OF this]
  1120   note has_bochner_integral_add[OF this]
  1121   then show ?thesis
  1122     by (simp add: power2_eq_square field_simps)  
  1123 qed
  1124 
  1125 lemma integral_normal_moment_nz_1:
  1126   "integral\<^sup>L lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x) = \<mu>"
  1127   using normal_moment_nz_1 by (rule has_bochner_integral_integral_eq)
  1128 
  1129 lemma integrable_normal_moment_nz_1: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * x)"
  1130   using normal_moment_nz_1 by rule
  1131 
  1132 lemma integrable_normal_moment: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * (x - \<mu>)^k)"
  1133 proof cases
  1134   assume "even k" then show ?thesis
  1135     using integrable.intros[OF normal_moment_even] by (auto elim: evenE)
  1136 next
  1137   assume "odd k" then show ?thesis
  1138     using integrable.intros[OF normal_moment_odd] by (auto elim: oddE)
  1139 qed
  1140 
  1141 lemma integrable_normal_moment_abs: "integrable lborel (\<lambda>x. normal_density \<mu> \<sigma> x * \<bar>x - \<mu>\<bar>^k)"
  1142 proof cases
  1143   assume "even k" then show ?thesis
  1144     using integrable.intros[OF normal_moment_even] by (auto simp add: power_even_abs elim: evenE)
  1145 next
  1146   assume "odd k" then show ?thesis
  1147     using integrable.intros[OF normal_moment_abs_odd] by (auto elim: oddE)
  1148 qed
  1149 
  1150 lemma integrable_normal_density[simp, intro]: "integrable lborel (normal_density \<mu> \<sigma>)"
  1151   using integrable_normal_moment[of \<mu> 0] by simp
  1152 
  1153 lemma integral_normal_density[simp]: "(\<integral>x. normal_density \<mu> \<sigma> x \<partial>lborel) = 1"
  1154   using integral_normal_moment_even[of \<sigma> \<mu> 0] by simp
  1155 
  1156 lemma prob_space_normal_density:
  1157   "prob_space (density lborel (normal_density \<mu> \<sigma>))"
  1158   proof qed (simp add: emeasure_density nn_integral_eq_integral normal_density_nonneg)
  1159 
  1160 end
  1161 
  1162 
  1163 
  1164 context
  1165   fixes k :: nat
  1166 begin
  1167 
  1168 lemma std_normal_moment_even:
  1169   "has_bochner_integral lborel (\<lambda>x. std_normal_density x * x ^ (2 * k)) (fact (2 * k) / (2^k * fact k))"
  1170   using normal_moment_even[of 1 0 k] by simp
  1171 
  1172 lemma std_normal_moment_abs_odd:
  1173   "has_bochner_integral lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) (sqrt (2/pi) * 2^k * fact k)"
  1174   using normal_moment_abs_odd[of 1 0 k] by (simp add: ac_simps)
  1175 
  1176 lemma std_normal_moment_odd:
  1177   "has_bochner_integral lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) 0"
  1178   using normal_moment_odd[of 1 0 k] by simp
  1179 
  1180 lemma integral_std_normal_moment_even:
  1181   "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2*k)) = fact (2 * k) / (2^k * fact k)"
  1182   using std_normal_moment_even by (rule has_bochner_integral_integral_eq)
  1183 
  1184 lemma integral_std_normal_moment_abs_odd:
  1185   "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^(2 * k + 1)) = sqrt (2 / pi) * 2^k * fact k"
  1186   using std_normal_moment_abs_odd by (rule has_bochner_integral_integral_eq)
  1187 
  1188 lemma integral_std_normal_moment_odd:
  1189   "integral\<^sup>L lborel (\<lambda>x. std_normal_density x * x^(2 * k + 1)) = 0"
  1190   using std_normal_moment_odd by (rule has_bochner_integral_integral_eq)
  1191 
  1192 lemma integrable_std_normal_moment_abs: "integrable lborel (\<lambda>x. std_normal_density x * \<bar>x\<bar>^k)"
  1193   using integrable_normal_moment_abs[of 1 0 k] by simp
  1194 
  1195 lemma integrable_std_normal_moment: "integrable lborel (\<lambda>x. std_normal_density x * x^k)"
  1196   using integrable_normal_moment[of 1 0 k] by simp
  1197 
  1198 end
  1199 
  1200 lemma (in prob_space) normal_density_affine:
  1201   assumes X: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1202   assumes [simp, arith]: "0 < \<sigma>" "\<alpha> \<noteq> 0"
  1203   shows "distributed M lborel (\<lambda>x. \<beta> + \<alpha> * X x) (normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>))"
  1204 proof -
  1205   have eq: "\<And>x. \<bar>\<alpha>\<bar> * normal_density (\<beta> + \<alpha> * \<mu>) (\<bar>\<alpha>\<bar> * \<sigma>) (x * \<alpha> + \<beta>) =
  1206     normal_density \<mu> \<sigma> x"
  1207     by (simp add: normal_density_def real_sqrt_mult field_simps)
  1208        (simp add: power2_eq_square field_simps)
  1209   show ?thesis
  1210     by (rule distributed_affineI[OF _ `\<alpha> \<noteq> 0`, where t=\<beta>]) (simp_all add: eq X)
  1211 qed
  1212 
  1213 lemma (in prob_space) normal_standard_normal_convert:
  1214   assumes pos_var[simp, arith]: "0 < \<sigma>"
  1215   shows "distributed M lborel X (normal_density  \<mu> \<sigma>) = distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) std_normal_density"
  1216 proof auto
  1217   assume "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))"
  1218   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))"
  1219     by(rule normal_density_affine) auto
  1220   
  1221   then show "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
  1222     by (simp add: diff_divide_distrib[symmetric] field_simps)
  1223 next
  1224   assume *: "distributed M lborel (\<lambda>x. (X x - \<mu>) / \<sigma>) (\<lambda>x. ereal (std_normal_density x))"
  1225   have "distributed M lborel (\<lambda>x. \<mu> + \<sigma> * ((X x - \<mu>) / \<sigma>)) (\<lambda>x. ereal (normal_density \<mu> \<bar>\<sigma>\<bar> x))"
  1226     using normal_density_affine[OF *, of \<sigma> \<mu>] by simp  
  1227   then show "distributed M lborel X (\<lambda>x. ereal (normal_density \<mu> \<sigma> x))" by simp
  1228 qed
  1229 
  1230 lemma conv_normal_density_zero_mean:
  1231   assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
  1232   shows "(\<lambda>x. \<integral>\<^sup>+y. ereal (normal_density 0 \<sigma> (x - y) * normal_density 0 \<tau> y) \<partial>lborel) =
  1233     normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2))"  (is "?LHS = ?RHS")
  1234 proof -
  1235   def \<sigma>' \<equiv> "\<sigma>\<^sup>2" and \<tau>' \<equiv> "\<tau>\<^sup>2"
  1236   then have [simp, arith]: "0 < \<sigma>'" "0 < \<tau>'"
  1237     by simp_all
  1238   let ?\<sigma> = "sqrt ((\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))"  
  1239   have sqrt: "(sqrt (2 * pi * (\<sigma>' + \<tau>')) * sqrt (2 * pi * (\<sigma>' * \<tau>') / (\<sigma>' + \<tau>'))) = 
  1240     (sqrt (2 * pi * \<sigma>') * sqrt (2 * pi * \<tau>'))"
  1241     by (subst power_eq_iff_eq_base[symmetric, where n=2])
  1242        (simp_all add: real_sqrt_mult[symmetric] power2_eq_square)
  1243   have "?LHS =
  1244     (\<lambda>x. \<integral>\<^sup>+y. ereal((normal_density 0 (sqrt (\<sigma>' + \<tau>')) x) * normal_density (\<tau>' * x / (\<sigma>' + \<tau>')) ?\<sigma> y) \<partial>lborel)"
  1245     apply (intro ext nn_integral_cong)
  1246     apply (simp add: normal_density_def \<sigma>'_def[symmetric] \<tau>'_def[symmetric] sqrt mult_exp_exp)
  1247     apply (simp add: divide_simps power2_eq_square)
  1248     apply (simp add: field_simps)
  1249     done
  1250 
  1251   also have "... =
  1252     (\<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)"
  1253     by (subst nn_integral_cmult[symmetric]) (auto simp: \<sigma>'_def \<tau>'_def normal_density_def)
  1254 
  1255   also have "... = (\<lambda>x. (normal_density 0 (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
  1256     by (subst nn_integral_eq_integral) (auto simp: normal_density_nonneg)
  1257 
  1258   finally show ?thesis by fast
  1259 qed
  1260 
  1261 lemma conv_std_normal_density:
  1262   "(\<lambda>x. \<integral>\<^sup>+y. ereal (std_normal_density (x - y) * std_normal_density y) \<partial>lborel) =
  1263   (normal_density 0 (sqrt 2))"
  1264   by (subst conv_normal_density_zero_mean) simp_all
  1265 
  1266 lemma (in prob_space) sum_indep_normal:
  1267   assumes indep: "indep_var borel X borel Y"
  1268   assumes pos_var[arith]: "0 < \<sigma>" "0 < \<tau>"
  1269   assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1270   assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
  1271   shows "distributed M lborel (\<lambda>x. X x + Y x) (normal_density (\<mu> + \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
  1272 proof -
  1273   have ind[simp]: "indep_var borel (\<lambda>x. - \<mu> + X x) borel (\<lambda>x. - \<nu> + Y x)"
  1274   proof -
  1275     have "indep_var borel ( (\<lambda>x. -\<mu> + x) o X) borel ((\<lambda>x. - \<nu> + x) o Y)"
  1276       by (auto intro!: indep_var_compose assms) 
  1277     then show ?thesis by (simp add: o_def)
  1278   qed
  1279   
  1280   have "distributed M lborel (\<lambda>x. -\<mu> + 1 * X x) (normal_density (- \<mu> + 1 * \<mu>) (\<bar>1\<bar> * \<sigma>))"
  1281     by(rule normal_density_affine[OF normalX pos_var(1), of 1 "-\<mu>"]) simp
  1282   then have 1[simp]: "distributed M lborel (\<lambda>x. - \<mu> +  X x) (normal_density 0 \<sigma>)" by simp
  1283 
  1284   have "distributed M lborel (\<lambda>x. -\<nu> + 1 * Y x) (normal_density (- \<nu> + 1 * \<nu>) (\<bar>1\<bar> * \<tau>))"
  1285     by(rule normal_density_affine[OF normalY pos_var(2), of 1 "-\<nu>"]) simp
  1286   then have 2[simp]: "distributed M lborel (\<lambda>x. - \<nu> +  Y x) (normal_density 0 \<tau>)" by simp
  1287   
  1288   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))"
  1289     using distributed_convolution[OF ind 1 2] conv_normal_density_zero_mean[OF pos_var] by simp
  1290   
  1291   have "distributed M lborel (\<lambda>x. \<mu> + \<nu> + 1 * (- \<mu> + X x + (- \<nu> + Y x)))
  1292         (\<lambda>x. ereal (normal_density (\<mu> + \<nu> + 1 * 0) (\<bar>1\<bar> * sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)) x))"
  1293     by (rule normal_density_affine[OF *, of 1 "\<mu> + \<nu>"]) (auto simp: add_pos_pos)
  1294 
  1295   then show ?thesis by auto
  1296 qed
  1297 
  1298 lemma (in prob_space) diff_indep_normal:
  1299   assumes indep[simp]: "indep_var borel X borel Y"
  1300   assumes [simp, arith]: "0 < \<sigma>" "0 < \<tau>"
  1301   assumes normalX[simp]: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1302   assumes normalY[simp]: "distributed M lborel Y (normal_density \<nu> \<tau>)"
  1303   shows "distributed M lborel (\<lambda>x. X x - Y x) (normal_density (\<mu> - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
  1304 proof -
  1305   have "distributed M lborel (\<lambda>x. 0 + - 1 * Y x) (\<lambda>x. ereal (normal_density (0 + - 1 * \<nu>) (\<bar>- 1\<bar> * \<tau>) x))" 
  1306     by(rule normal_density_affine, auto)
  1307   then have [simp]:"distributed M lborel (\<lambda>x. - Y x) (\<lambda>x. ereal (normal_density (- \<nu>) \<tau> x))" by simp
  1308 
  1309   have "distributed M lborel (\<lambda>x. X x + (- Y x)) (normal_density (\<mu> + - \<nu>) (sqrt (\<sigma>\<^sup>2 + \<tau>\<^sup>2)))"
  1310     apply (rule sum_indep_normal)
  1311     apply (rule indep_var_compose[unfolded comp_def, of borel _ borel _ "\<lambda>x. x" _ "\<lambda>x. - x"])
  1312     apply simp_all
  1313     done
  1314   then show ?thesis by simp
  1315 qed
  1316 
  1317 lemma (in prob_space) setsum_indep_normal:
  1318   assumes "finite I" "I \<noteq> {}" "indep_vars (\<lambda>i. borel) X I"
  1319   assumes "\<And>i. i \<in> I \<Longrightarrow> 0 < \<sigma> i"
  1320   assumes normal: "\<And>i. i \<in> I \<Longrightarrow> distributed M lborel (X i) (normal_density (\<mu> i) (\<sigma> i))"
  1321   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)))"
  1322   using assms 
  1323 proof (induct I rule: finite_ne_induct)
  1324   case (singleton i) then show ?case by (simp add : abs_of_pos)
  1325 next
  1326   case (insert i I)
  1327     then have 1: "distributed M lborel (\<lambda>x. (X i x) + (\<Sum>i\<in>I. X i x)) 
  1328                 (normal_density (\<mu> i  + setsum \<mu> I)  (sqrt ((\<sigma> i)\<^sup>2 + (sqrt (\<Sum>i\<in>I. (\<sigma> i)\<^sup>2))\<^sup>2)))"
  1329       apply (intro sum_indep_normal indep_vars_setsum insert real_sqrt_gt_zero)  
  1330       apply (auto intro: indep_vars_subset intro!: setsum_pos)
  1331       apply fastforce
  1332       done
  1333     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))"
  1334           "\<mu> i + setsum \<mu> I = setsum \<mu> (insert i I)"
  1335       using insert by auto
  1336   
  1337     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))"
  1338       using insert by (simp add: setsum_nonneg)
  1339   
  1340     show ?case using 1 2 3 by simp  
  1341 qed
  1342 
  1343 lemma (in prob_space) standard_normal_distributed_expectation:
  1344   assumes D: "distributed M lborel X std_normal_density"
  1345   shows "expectation X = 0"
  1346   using integral_std_normal_moment_odd[of 0]
  1347   by (auto simp: distributed_integral[OF D, of "\<lambda>x. x", symmetric])
  1348 
  1349 lemma (in prob_space) normal_distributed_expectation:
  1350   assumes \<sigma>[arith]: "0 < \<sigma>"
  1351   assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1352   shows "expectation X = \<mu>"
  1353   using integral_normal_moment_nz_1[OF \<sigma>, of \<mu>] distributed_integral[OF D, of "\<lambda>x. x", symmetric]
  1354   by (auto simp: field_simps)
  1355 
  1356 lemma (in prob_space) normal_distributed_variance:
  1357   fixes a b :: real
  1358   assumes [simp, arith]: "0 < \<sigma>"
  1359   assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1360   shows "variance X = \<sigma>\<^sup>2"
  1361   using integral_normal_moment_even[of \<sigma> \<mu> 1]
  1362   by (subst distributed_integral[OF D, symmetric])
  1363      (simp_all add: eval_nat_numeral normal_distributed_expectation[OF assms])
  1364 
  1365 lemma (in prob_space) standard_normal_distributed_variance:
  1366   "distributed M lborel X std_normal_density \<Longrightarrow> variance X = 1"
  1367   using normal_distributed_variance[of 1 X 0] by simp
  1368 
  1369 lemma (in information_space) entropy_normal_density:
  1370   assumes [arith]: "0 < \<sigma>"
  1371   assumes D: "distributed M lborel X (normal_density \<mu> \<sigma>)"
  1372   shows "entropy b lborel X = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
  1373 proof -
  1374   have "entropy b lborel X = - (\<integral> x. normal_density \<mu> \<sigma> x * log b (normal_density \<mu> \<sigma> x) \<partial>lborel)"
  1375     using D by (rule entropy_distr)
  1376   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)"
  1377     by (intro arg_cong[where f="uminus"] integral_cong)
  1378        (auto simp: normal_density_def field_simps ln_mult log_def ln_div ln_sqrt)
  1379   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)"
  1380     by (intro arg_cong[where f="uminus"] integral_cong) (auto simp: divide_simps field_simps)
  1381   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)"
  1382     by (simp del: minus_add_distrib)
  1383   also have "\<dots> = (ln (2 * pi * \<sigma>\<^sup>2) + 1) / (2 * ln b)"
  1384     using integral_normal_moment_even[of \<sigma> \<mu> 1] by (simp add: integrable_normal_moment fact_numeral)
  1385   also have "\<dots> = log b (2 * pi * exp 1 * \<sigma>\<^sup>2) / 2"
  1386     by (simp add: log_def field_simps ln_mult)
  1387   finally show ?thesis .
  1388 qed
  1389 
  1390 end