src/HOL/Probability/Probability_Mass_Function.thy
changeset 60602 37588fbe39f9
parent 60595 804dfdc82835
child 61169 4de9ff3ea29a
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Sun Jun 28 14:30:53 2015 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Jun 17 18:44:23 2015 +0200
     1.3 @@ -1381,20 +1381,25 @@
     1.4  
     1.5  subsubsection \<open> Geometric Distribution \<close>
     1.6  
     1.7 -lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
     1.8 +context
     1.9 +  fixes p :: real assumes p[arith]: "0 < p" "p \<le> 1"
    1.10 +begin
    1.11 +
    1.12 +lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. (1 - p)^n * p"
    1.13  proof
    1.14 -  note geometric_sums[of "1 / 2"]
    1.15 -  note sums_mult[OF this, of "1 / 2"]
    1.16 -  from sums_suminf_ereal[OF this]
    1.17 -  show "(\<integral>\<^sup>+ x. ereal (1 / 2 ^ Suc x) \<partial>count_space UNIV) = 1"
    1.18 +  have "(\<Sum>i. ereal (p * (1 - p) ^ i)) = ereal (p * (1 / (1 - (1 - p))))"
    1.19 +    by (intro sums_suminf_ereal sums_mult geometric_sums) auto
    1.20 +  then show "(\<integral>\<^sup>+ x. ereal ((1 - p)^x * p) \<partial>count_space UNIV) = 1"
    1.21      by (simp add: nn_integral_count_space_nat field_simps)
    1.22  qed simp
    1.23  
    1.24 -lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
    1.25 +lemma pmf_geometric[simp]: "pmf geometric_pmf n = (1 - p)^n * p"
    1.26    by transfer rule
    1.27  
    1.28 -lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
    1.29 -  by (auto simp: set_pmf_iff)
    1.30 +end
    1.31 +
    1.32 +lemma set_pmf_geometric: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (geometric_pmf p) = UNIV"
    1.33 +  by (auto simp: set_pmf_iff) 
    1.34  
    1.35  subsubsection \<open> Uniform Multiset Distribution \<close>
    1.36