src/HOL/Probability/Probability_Mass_Function.thy
changeset 59093 2b106e58a177
parent 59092 d469103c0737
child 59134 a71f2e256ee2
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 05 12:06:18 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Dec 05 13:39:59 2014 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  theory Probability_Mass_Function
     1.5  imports
     1.6    Giry_Monad
     1.7 +  "~~/src/HOL/Number_Theory/Binomial"
     1.8    "~~/src/HOL/Library/Multiset"
     1.9  begin
    1.10  
    1.11 @@ -479,6 +480,8 @@
    1.12  
    1.13  interpretation pmf_as_function .
    1.14  
    1.15 +subsubsection \<open> Bernoulli Distribution \<close>
    1.16 +
    1.17  lift_definition bernoulli_pmf :: "real \<Rightarrow> bool pmf" is
    1.18    "\<lambda>p b. ((\<lambda>p. if b then p else 1 - p) \<circ> min 1 \<circ> max 0) p"
    1.19    by (auto simp: nn_integral_count_space_finite[where A="{False, True}"] UNIV_bool
    1.20 @@ -504,6 +507,8 @@
    1.21    shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
    1.22    by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
    1.23  
    1.24 +subsubsection \<open> Geometric Distribution \<close>
    1.25 +
    1.26  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
    1.27  proof
    1.28    note geometric_sums[of "1 / 2"]
    1.29 @@ -519,6 +524,8 @@
    1.30  lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
    1.31    by (auto simp: set_pmf_iff)
    1.32  
    1.33 +subsubsection \<open> Uniform Multiset Distribution \<close>
    1.34 +
    1.35  context
    1.36    fixes M :: "'a multiset" assumes M_not_empty: "M \<noteq> {#}"
    1.37  begin
    1.38 @@ -540,6 +547,8 @@
    1.39  
    1.40  end
    1.41  
    1.42 +subsubsection \<open> Uniform Distribution \<close>
    1.43 +
    1.44  context
    1.45    fixes S :: "'a set" assumes S_not_empty: "S \<noteq> {}" and S_finite: "finite S"
    1.46  begin
    1.47 @@ -561,9 +570,75 @@
    1.48  
    1.49  end
    1.50  
    1.51 +subsubsection \<open> Poisson Distribution \<close>
    1.52 +
    1.53 +context
    1.54 +  fixes rate :: real assumes rate_pos: "0 < rate"
    1.55 +begin
    1.56 +
    1.57 +lift_definition poisson_pmf :: "nat pmf" is "\<lambda>k. rate ^ k / fact k * exp (-rate)"
    1.58 +proof
    1.59 +  (* Proof by Manuel Eberl *)
    1.60 +
    1.61 +  have summable: "summable (\<lambda>x::nat. rate ^ x / fact x)" using summable_exp
    1.62 +    by (simp add: field_simps field_divide_inverse[symmetric])
    1.63 +  have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x * exp (-rate) \<partial>count_space UNIV) =
    1.64 +          exp (-rate) * (\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV)"
    1.65 +    by (simp add: field_simps nn_integral_cmult[symmetric])
    1.66 +  also from rate_pos have "(\<integral>\<^sup>+(x::nat). rate ^ x / fact x \<partial>count_space UNIV) = (\<Sum>x. rate ^ x / fact x)"
    1.67 +    by (simp_all add: nn_integral_count_space_nat suminf_ereal summable suminf_ereal_finite)
    1.68 +  also have "... = exp rate" unfolding exp_def
    1.69 +    by (simp add: field_simps field_divide_inverse[symmetric] transfer_int_nat_factorial)
    1.70 +  also have "ereal (exp (-rate)) * ereal (exp rate) = 1"
    1.71 +    by (simp add: mult_exp_exp)
    1.72 +  finally show "(\<integral>\<^sup>+ x. ereal (rate ^ x / real (fact x) * exp (- rate)) \<partial>count_space UNIV) = 1" .
    1.73 +qed (simp add: rate_pos[THEN less_imp_le])
    1.74 +
    1.75 +lemma pmf_poisson[simp]: "pmf poisson_pmf k = rate ^ k / fact k * exp (-rate)"
    1.76 +  by transfer rule
    1.77 +
    1.78 +lemma set_pmf_poisson[simp]: "set_pmf poisson_pmf = UNIV"
    1.79 +  using rate_pos by (auto simp: set_pmf_iff)
    1.80 +
    1.81  end
    1.82  
    1.83 -subsection {* Monad interpretation *}
    1.84 +subsubsection \<open> Binomial Distribution \<close>
    1.85 +
    1.86 +context
    1.87 +  fixes n :: nat and p :: real assumes p_nonneg: "0 \<le> p" and p_le_1: "p \<le> 1"
    1.88 +begin
    1.89 +
    1.90 +lift_definition binomial_pmf :: "nat pmf" is "\<lambda>k. (n choose k) * p^k * (1 - p)^(n - k)"
    1.91 +proof
    1.92 +  have "(\<integral>\<^sup>+k. ereal (real (n choose k) * p ^ k * (1 - p) ^ (n - k)) \<partial>count_space UNIV) =
    1.93 +    ereal (\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k))"
    1.94 +    using p_le_1 p_nonneg by (subst nn_integral_count_space') auto
    1.95 +  also have "(\<Sum>k\<le>n. real (n choose k) * p ^ k * (1 - p) ^ (n - k)) = (p + (1 - p)) ^ n"
    1.96 +    by (subst binomial_ring) (simp add: atLeast0AtMost real_of_nat_def)
    1.97 +  finally show "(\<integral>\<^sup>+ x. ereal (real (n choose x) * p ^ x * (1 - p) ^ (n - x)) \<partial>count_space UNIV) = 1"
    1.98 +    by simp
    1.99 +qed (insert p_nonneg p_le_1, simp)
   1.100 +
   1.101 +lemma pmf_binomial[simp]: "pmf binomial_pmf k = (n choose k) * p^k * (1 - p)^(n - k)"
   1.102 +  by transfer rule
   1.103 +
   1.104 +lemma set_pmf_binomial_eq: "set_pmf binomial_pmf = (if p = 0 then {0} else if p = 1 then {n} else {.. n})"
   1.105 +  using p_nonneg p_le_1 unfolding set_eq_iff set_pmf_iff pmf_binomial by (auto simp: set_pmf_iff)
   1.106 +
   1.107 +end
   1.108 +
   1.109 +end
   1.110 +
   1.111 +lemma set_pmf_binomial_0[simp]: "set_pmf (binomial_pmf n 0) = {0}"
   1.112 +  by (simp add: set_pmf_binomial_eq)
   1.113 +
   1.114 +lemma set_pmf_binomial_1[simp]: "set_pmf (binomial_pmf n 1) = {n}"
   1.115 +  by (simp add: set_pmf_binomial_eq)
   1.116 +
   1.117 +lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
   1.118 +  by (simp add: set_pmf_binomial_eq)
   1.119 +
   1.120 +subsection \<open> Monad Interpretation \<close>
   1.121  
   1.122  lemma measurable_measure_pmf[measurable]:
   1.123    "(\<lambda>x. measure_pmf (M x)) \<in> measurable (count_space UNIV) (subprob_algebra (count_space UNIV))"