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.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))"
```