Theory Probability_Tools
section ‹Auxiliary Lemmas Related to Probability Theory›
theory Probability_Tools
imports "HOL-Probability.Probability"
begin
subsection ‹Tuples›
definition tuples :: ‹'a set ⇒ nat ⇒ 'a list set› where
‹tuples S n = {xs. set xs ⊆ S ∧ length xs = n}›
lemma tuplesI: ‹⟦ set xs ⊆ S; length xs = n ⟧ ⟹ xs ∈ tuples S n›
by (simp add: tuples_def)
lemma tuplesE [elim]: ‹⟦ xs ∈ tuples S n; ⟦ set xs ⊆ S; length xs = n ⟧ ⟹ P ⟧ ⟹ P›
by (simp add: tuples_def)
lemma tuples_Zero: ‹tuples S 0 = {[]}›
by (auto simp add: tuples_def)
lemma tuples_Suc: ‹tuples S (Suc n) = (λ(x, xs). x # xs) ` (S × tuples S n)›
by (fastforce simp add: tuples_def image_def Suc_length_conv dest: sym)
lemma tuples_non_empty [simp]: ‹S ≠ {} ⟹ tuples S n ≠ {}›
by (induction n) (auto simp add: tuples_Zero tuples_Suc)
lemma tuples_finite [simp]: ‹⟦ finite (S::'a set); S ≠ {} ⟧ ⟹ finite (tuples S n :: 'a list set)›
by (auto simp add: tuples_def dest: finite_lists_length_eq)
subsection ‹Congruence and monotonicity›
lemma prob_cong:
assumes ‹⋀x. x ∈ set_pmf M ⟹ x ∈ A ⟷ x ∈ B›
shows ‹measure_pmf.prob M A = measure_pmf.prob M B›
using assms
by (simp add: measure_pmf.finite_measure_eq_AE AE_measure_pmf_iff)
lemma prob_mono:
assumes ‹⋀x. x ∈ set_pmf M ⟹ x ∈ A ⟹ x ∈ B›
shows ‹measure_pmf.prob M A ≤ measure_pmf.prob M B›
using assms
by (simp add: measure_pmf.finite_measure_mono_AE AE_measure_pmf_iff)
subsection ‹Some simple derived lemmas›
lemma prob_empty:
assumes ‹A = {}›
shows ‹measure_pmf.prob M A = 0›
using assms
by (simp)
lemma prob_pmf_of_set_geq_1:
assumes "finite S" and "S ≠ {}"
shows "measure_pmf.prob (pmf_of_set S) A ≥ 1 ⟷ S ⊆ A" using assms
by (auto simp add: measure_pmf.measure_ge_1_iff measure_pmf.prob_eq_1 AE_measure_pmf_iff)
subsection ‹Intersection and union lemmas›
lemma prob_disjoint_union:
assumes ‹A ∩ B = {}›
shows ‹measure_pmf.prob M (A ∪ B) = measure_pmf.prob M A + measure_pmf.prob M B›
using assms
by (fact measure_pmf.finite_measure_Union[simplified])
lemma prob_finite_Union:
assumes ‹disjoint_family_on A I› ‹finite I›
shows ‹measure_pmf.prob M (⋃i∈I. A i) = (∑i∈I. measure_pmf.prob M (A i))›
using assms
by (intro measure_pmf.finite_measure_finite_Union) (simp_all)
lemma prob_disjoint_cases:
assumes ‹B ∪ C = A› ‹B ∩ C = {}›
shows ‹measure_pmf.prob M A = measure_pmf.prob M B + measure_pmf.prob M C›
proof -
have ‹measure_pmf.prob M A = measure_pmf.prob M (B ∪ C)› using ‹B ∪ C = A›
by (auto intro: prob_cong)
also have ‹... = measure_pmf.prob M B + measure_pmf.prob M C› using ‹B ∩ C = {}›
by (simp add: prob_disjoint_union)
finally show ?thesis .
qed
lemma prob_finite_disjoint_cases:
assumes ‹(⋃i∈I. B i) = A› ‹disjoint_family_on B I› ‹finite I›
shows ‹measure_pmf.prob M A = (∑i∈I. measure_pmf.prob M (B i))›
proof -
have ‹measure_pmf.prob M A = measure_pmf.prob M (⋃i∈I. B i)› using assms(1)
by (auto intro: prob_cong)
also have ‹... = (∑i∈I. measure_pmf.prob M (B i))› using assms(2,3)
by (intro prob_finite_Union)
finally show ?thesis .
qed
subsection ‹Independent probabilities for head and tail of a tuple›
lemma pmf_of_set_Times:
"pmf_of_set (A × B) = pair_pmf (pmf_of_set A) (pmf_of_set B)"
if "finite A" "finite B" "A ≠ {}" "B ≠ {}"
by(rule pmf_eqI)(auto simp add: that pmf_pair indicator_def)
lemma prob_tuples_hd_tl_indep:
assumes ‹S ≠ {}›
shows
‹measure_pmf.prob (pmf_of_set (tuples S (Suc n))) {(r::'a::finite) # rs | r rs. P r ∧ Q rs}
= measure_pmf.prob (pmf_of_set (S::'a set)) {r. P r} *
measure_pmf.prob (pmf_of_set (tuples S n)) {rs. Q rs}›
(is "?lhs = ?rhs")
proof -
text ‹
Step 1: Split the random variable @{term "pmf_of_set (tuples S (Suc n))"} into
two independent (@{term "pair_pmf"}) random variables, one producing the head and one
producing the tail of the list, and then @{term Cons} the two random variables using
@{term "map_pmf"}.
›
have *: "pmf_of_set (tuples S (Suc n))
= map_pmf (λ(x :: 'a, xs). x # xs) (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n)))"
unfolding tuples_Suc using ‹S ≠ {}›
by (auto simp add: map_pmf_of_set_inj[symmetric] inj_on_def pmf_of_set_Times)
text ‹
Step 2: Transform the event by move the @{term Cons} from the random variable into the event.
This corresponds to using @{term distr} on measures.
›
have "?lhs = measure_pmf.prob (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n)))
((λ(x :: 'a, xs). x # xs) -` {r # rs | r rs. P r ∧ Q rs})"
unfolding * measure_map_pmf by (rule refl)
text ‹
Step 3: Rewrite the event as a pair of events. Then we apply independence of the head
from the tail.
›
also have "((λ(x, xs). x # xs) -` {r # rs | r rs. P r ∧ Q rs}) = {r. P r} × {rs. Q rs}" by auto
also have "measure_pmf.prob (pair_pmf (pmf_of_set S) (pmf_of_set (tuples S n))) … =
measure_pmf.prob (pmf_of_set S) {r. P r}
* measure_pmf.prob (pmf_of_set (tuples S n)) {rs. Q rs}"
by(rule measure_pmf_prob_product) simp_all
finally show ?thesis .
qed
lemma prob_tuples_fixed_hd:
‹measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) {rs::'a list. P rs}
= (∑a ∈ UNIV. measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a # rs)}) / real(CARD('a::finite))›
(is "?lhs = ?rhs")
proof -
{
fix a
have ‹measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} ∩ {rs. hd rs = a})
= measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({r#rs | r rs. r = a ∧ P (a#rs)})›
by (intro prob_cong) (auto simp add: tuples_Suc)
also have ‹... = measure_pmf.prob (pmf_of_set (UNIV::'a set)) {r. r = a} *
measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)}›
by (intro prob_tuples_hd_tl_indep) simp
also have ‹... = measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)} / real (CARD ('a))›
by (simp add: measure_pmf_single)
finally
have ‹measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} ∩ {rs. hd rs = a})
= measure_pmf.prob (pmf_of_set (tuples UNIV n)) {rs. P (a#rs)} / real (CARD ('a))› .
}
note A1 = this
have ‹?lhs = (∑a ∈ UNIV. measure_pmf.prob (pmf_of_set (tuples UNIV (Suc n))) ({rs. P rs} ∩ {rs. hd rs = a}))›
by (intro prob_finite_disjoint_cases) (auto simp add: disjoint_family_on_def)
also have ‹... = ?rhs› using A1
by (simp add: sum_divide_distrib)
finally show ?thesis .
qed
end