Theory Geometric_PMF
section ‹Theorems about the Geometric Distribution›
theory Geometric_PMF
imports
"HOL-Probability.Probability"
Pi_pmf
"Monad_Normalisation.Monad_Normalisation"
begin
lemma nn_integral_geometric_pmf:
assumes "p ∈ {0<..1}"
shows "nn_integral (geometric_pmf p) real = (1 - p) / p"
using assms expectation_geometric_pmf integrable_real_geometric_pmf
by (subst nn_integral_eq_integral) auto
lemma geometric_pmf_prob_atMost:
assumes "p ∈ {0<..1}"
shows "measure_pmf.prob (geometric_pmf p) {..n} = (1 - (1 - p)^(n + 1))"
proof -
have "(∑x≤n. (1 - p) ^ x * p) = 1 - (1 - p) * (1 - p) ^ n"
by (induction n) (auto simp add: algebra_simps)
then show ?thesis
using assms by (auto simp add: measure_pmf_conv_infsetsum)
qed
lemma geometric_pmf_prob_lessThan:
assumes "p ∈ {0<..1}"
shows "measure_pmf.prob (geometric_pmf p) {..<n} = 1 - (1 - p) ^ n"
proof -
have "(∑x<n. (1 - p) ^ x * p) = 1 - (1 - p) ^ n"
by (induction n) (auto simp add: algebra_simps)
then show ?thesis
using assms by (auto simp add: measure_pmf_conv_infsetsum)
qed
lemma geometric_pmf_prob_greaterThan:
assumes "p ∈ {0<..1}"
shows "measure_pmf.prob (geometric_pmf p) {n<..} = (1 - p)^(n + 1)"
proof -
have "(UNIV - {..n}) = {n<..}"
by auto
moreover have "measure_pmf.prob (geometric_pmf p) (UNIV - {..n}) = (1 - p) ^ (n + 1)"
using assms by (subst measure_pmf.finite_measure_Diff)
(auto simp add: geometric_pmf_prob_atMost)
ultimately show ?thesis
by auto
qed
lemma geometric_pmf_prob_atLeast:
assumes "p ∈ {0<..1}"
shows "measure_pmf.prob (geometric_pmf p) {n..} = (1 - p)^n"
proof -
have "(UNIV - {..<n}) = {n..}"
by auto
moreover have "measure_pmf.prob (geometric_pmf p) (UNIV - {..<n}) = (1 - p) ^ n"
using assms by (subst measure_pmf.finite_measure_Diff)
(auto simp add: geometric_pmf_prob_lessThan)
ultimately show ?thesis
by auto
qed
lemma bernoulli_pmf_of_set':
assumes "finite A"
shows "map_pmf (λb. {x ∈ A. ¬ b x}) (Pi_pmf A P (λ_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)"
proof -
have *: "Pi_pmf A P (λ_. pmf_of_set (UNIV :: bool set)) = pmf_of_set (PiE_dflt A P (λ_. UNIV :: bool set))"
using assms by (intro Pi_pmf_of_set) auto
have "map_pmf (λb. {x ∈ A. ¬ b x}) (Pi_pmf A P (λ_. bernoulli_pmf (1 / 2))) =
map_pmf (λb. {x ∈ A. ¬ b x}) (Pi_pmf A P (λ_. pmf_of_set UNIV))"
using bernoulli_pmf_half_conv_pmf_of_set by auto
also have "… = map_pmf (λb. {x ∈ A. ¬ b x}) (pmf_of_set (PiE_dflt A P (λ_. UNIV)))"
using assms by (subst Pi_pmf_of_set) (auto)
also have "… = pmf_of_set (Pow A)"
proof -
have "bij_betw (λb. {x ∈ A. ¬ b x}) (PiE_dflt A P (λ_. UNIV)) (Pow A)"
by (rule bij_betwI[of _ _ _ "λB b. if b ∈ A then ¬ (b ∈ B) else P"]) (auto simp add: PiE_dflt_def)
then show ?thesis
using assms by (intro map_pmf_of_set_bij_betw) auto
qed
finally show ?thesis
by simp
qed
lemma Pi_pmf_pmf_of_set_Suc:
assumes "finite A"
shows "Pi_pmf A 0 (λ_. geometric_pmf (1/2)) =
do {
B ← pmf_of_set (Pow A);
Pi_pmf B 0 (λ_. map_pmf Suc (geometric_pmf (1/2))) }"
proof -
have "Pi_pmf A 0 (λ_. geometric_pmf (1/2)) =
Pi_pmf A 0 (λ_. bernoulli_pmf (1/2) ⤜
(λb. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
using assms by (subst geometric_bind_pmf_unfold) auto
also have "… =
Pi_pmf A False (λ_. bernoulli_pmf (1/2)) ⤜
(λb. Pi_pmf A 0 (λx. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto
also have "… =
do {b ← Pi_pmf A False (λ_. bernoulli_pmf (1/2));
Pi_pmf {x ∈ A. ~b x} 0 (λx. map_pmf Suc (geometric_pmf (1/2)))}"
using assms by (subst Pi_pmf_if_set') auto
also have "… =
do {B ← map_pmf (λb. {x ∈ A. ¬ b x}) (Pi_pmf A False (λ_. bernoulli_pmf (1/2)));
Pi_pmf B 0 (λx. map_pmf Suc (geometric_pmf (1/2)))}"
unfolding map_pmf_def apply(subst bind_assoc_pmf) apply(subst bind_return_pmf) by auto
also have "… = pmf_of_set (Pow A) ⤜ (λB. Pi_pmf B 0 (λx. map_pmf Suc (geometric_pmf (1 / 2))))"
unfolding assms using assms by (subst bernoulli_pmf_of_set') auto
finally show ?thesis
by simp
qed
lemma Pi_pmf_pmf_of_set_Suc':
assumes "finite A"
shows "Pi_pmf A 0 (λ_. geometric_pmf (1/2)) =
do {
B ← pmf_of_set (Pow A);
Pi_pmf B 0 (λ_. map_pmf Suc (geometric_pmf (1/2))) }"
proof -
have "Pi_pmf A 0 (λ_. geometric_pmf (1/2)) =
Pi_pmf A 0 (λ_. bernoulli_pmf (1/2) ⤜
(λb. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
using assms by (subst geometric_bind_pmf_unfold) auto
also have "… =
Pi_pmf A False (λ_. bernoulli_pmf (1/2)) ⤜
(λb. Pi_pmf A 0 (λx. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto
also have "… =
do {b ← Pi_pmf A False (λ_. bernoulli_pmf (1/2));
Pi_pmf {x ∈ A. ~b x} 0 (λx. map_pmf Suc (geometric_pmf (1/2)))}"
using assms by (subst Pi_pmf_if_set') auto
also have "… =
do {B ← map_pmf (λb. {x ∈ A. ¬ b x}) (Pi_pmf A False (λ_. bernoulli_pmf (1/2)));
Pi_pmf B 0 (λx. map_pmf Suc (geometric_pmf (1/2)))}"
unfolding map_pmf_def by (auto simp add: bind_assoc_pmf bind_return_pmf)
also have "… = pmf_of_set (Pow A) ⤜ (λB. Pi_pmf B 0 (λx. map_pmf Suc (geometric_pmf (1 / 2))))"
unfolding assms using assms by (subst bernoulli_pmf_of_set') auto
finally show ?thesis
by simp
qed
lemma binomial_pmf_altdef':
fixes A :: "'a set"
assumes "finite A" and "card A = n" and p: "p ∈ {0..1}"
shows "binomial_pmf n p =
map_pmf (λf. card {x∈A. f x}) (Pi_pmf A dflt (λ_. bernoulli_pmf p))" (is "?lhs = ?rhs")
proof -
from assms have "?lhs = binomial_pmf (card A) p"
by simp
also have "… = ?rhs"
using assms(1)
proof (induction rule: finite_induct)
case empty
with p show ?case by (simp add: binomial_pmf_0)
next
case (insert x A)
from insert.hyps have "card (insert x A) = Suc (card A)"
by simp
also have "binomial_pmf … p = do {
b ← bernoulli_pmf p;
f ← Pi_pmf A dflt (λ_. bernoulli_pmf p);
return_pmf ((if b then 1 else 0) + card {y ∈ A. f y})
}"
using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf)
also have "… = do {
b ← bernoulli_pmf p;
f ← Pi_pmf A dflt (λ_. bernoulli_pmf p);
return_pmf (card {y ∈ insert x A. (f(x := b)) y})
}"
proof (intro bind_pmf_cong refl, goal_cases)
case (1 b f)
have "(if b then 1 else 0) + card {y∈A. f y} = card ((if b then {x} else {}) ∪ {y∈A. f y})"
using insert.hyps by auto
also have "(if b then {x} else {}) ∪ {y∈A. f y} = {y∈insert x A. (f(x := b)) y}"
using insert.hyps by auto
finally show ?case by simp
qed
also have "… = map_pmf (λf. card {y∈insert x A. f y})
(Pi_pmf (insert x A) dflt (λ_. bernoulli_pmf p))"
using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf)
finally show ?case .
qed
finally show ?thesis .
qed
lemma bernoulli_pmf_Not:
assumes "p ∈ {0..1}"
shows "bernoulli_pmf p = map_pmf Not (bernoulli_pmf (1 - p))"
proof -
have *: "(Not -` {True}) = {False}" "(Not -` {False}) = {True}"
by blast+
have "pmf (bernoulli_pmf p) b = pmf (map_pmf Not (bernoulli_pmf (1 - p))) b" for b
using assms by (cases b) (auto simp add: pmf_map * measure_pmf_single)
then show ?thesis
by (rule pmf_eqI)
qed
lemma binomial_pmf_altdef'':
assumes p: "p ∈ {0..1}"
shows "binomial_pmf n p =
map_pmf (λf. card {x. x < n ∧ f x}) (Pi_pmf {..<n} dflt (λ_. bernoulli_pmf p))"
using assms by (subst binomial_pmf_altdef'[of "{..<n}"]) (auto)
context includes monad_normalisation
begin
lemma Pi_pmf_geometric_filter:
assumes "finite A" "p ∈ {0<..1}"
shows "Pi_pmf A 0 (λ_. geometric_pmf p) =
do {
fb ← Pi_pmf A dflt (λ_. bernoulli_pmf p);
Pi_pmf {x ∈ A. ¬ fb x} 0 (λ_. map_pmf Suc (geometric_pmf p)) }"
proof -
have "Pi_pmf A 0 (λ_. geometric_pmf p) =
Pi_pmf A 0 (λ_. bernoulli_pmf p ⤜
(λb. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)))"
using assms by (subst geometric_bind_pmf_unfold) auto
also have "… =
Pi_pmf A dflt (λ_. bernoulli_pmf p) ⤜
(λb. Pi_pmf A 0 (λx. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf p)))"
using assms by (subst Pi_pmf_bind[of _ _ _ _ dflt]) auto
also have "… =
do {b ← Pi_pmf A dflt (λ_. bernoulli_pmf p);
Pi_pmf {x ∈ A. ¬ b x} 0 (λx. map_pmf Suc (geometric_pmf p))}"
using assms by (subst Pi_pmf_if_set') (auto)
finally show ?thesis
by simp
qed
lemma Pi_pmf_geometric_filter':
assumes "finite A" "p ∈ {0<..1}"
shows "Pi_pmf A 0 (λ_. geometric_pmf p) =
do {
fb ← Pi_pmf A dflt (λ_. bernoulli_pmf (1 - p));
Pi_pmf {x ∈ A. fb x} 0 (λ_. map_pmf Suc (geometric_pmf p)) }"
using assms by (auto simp add: Pi_pmf_geometric_filter[of _ _ "¬ dflt"] bernoulli_pmf_Not[of p]
Pi_pmf_map[of _ _ dflt] map_pmf_def[of "((∘) Not)"])
end
end