diff -r 6e83d94760c4 -r 37588fbe39f9 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Sun Jun 28 14:30:53 2015 +0200 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Wed Jun 17 18:44:23 2015 +0200 @@ -1381,20 +1381,25 @@ subsubsection \ Geometric Distribution \ -lift_definition geometric_pmf :: "nat pmf" is "\n. 1 / 2^Suc n" +context + fixes p :: real assumes p[arith]: "0 < p" "p \ 1" +begin + +lift_definition geometric_pmf :: "nat pmf" is "\n. (1 - p)^n * p" proof - note geometric_sums[of "1 / 2"] - note sums_mult[OF this, of "1 / 2"] - from sums_suminf_ereal[OF this] - show "(\\<^sup>+ x. ereal (1 / 2 ^ Suc x) \count_space UNIV) = 1" + have "(\i. ereal (p * (1 - p) ^ i)) = ereal (p * (1 / (1 - (1 - p))))" + by (intro sums_suminf_ereal sums_mult geometric_sums) auto + then show "(\\<^sup>+ x. ereal ((1 - p)^x * p) \count_space UNIV) = 1" by (simp add: nn_integral_count_space_nat field_simps) qed simp -lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n" +lemma pmf_geometric[simp]: "pmf geometric_pmf n = (1 - p)^n * p" by transfer rule -lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV" - by (auto simp: set_pmf_iff) +end + +lemma set_pmf_geometric: "0 < p \ p < 1 \ set_pmf (geometric_pmf p) = UNIV" + by (auto simp: set_pmf_iff) subsubsection \ Uniform Multiset Distribution \