# HG changeset patch
# User hoelzl
# Date 1434559463 -7200
# Node ID 37588fbe39f9fc4028fb8f5c52660a440ab8f4f1
# Parent  6e83d94760c4204332ed50b61d356c5de655f2fc
generalized geometric distribution

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 \<open> Geometric Distribution \<close>
 
-lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
+context
+  fixes p :: real assumes p[arith]: "0 < p" "p \<le> 1"
+begin
+
+lift_definition geometric_pmf :: "nat pmf" is "\<lambda>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 "(\<integral>\<^sup>+ x. ereal (1 / 2 ^ Suc x) \<partial>count_space UNIV) = 1"
+  have "(\<Sum>i. ereal (p * (1 - p) ^ i)) = ereal (p * (1 / (1 - (1 - p))))"
+    by (intro sums_suminf_ereal sums_mult geometric_sums) auto
+  then show "(\<integral>\<^sup>+ x. ereal ((1 - p)^x * p) \<partial>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 \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (geometric_pmf p) = UNIV"
+  by (auto simp: set_pmf_iff) 
 
 subsubsection \<open> Uniform Multiset Distribution \<close>