src/HOL/Probability/Probability_Mass_Function.thy
changeset 61634 48e2de1b1df5
parent 61610 4f54d2759a0b
child 61808 fc1556774cfe
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:13:40 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:28:22 2015 +0100
     1.3 @@ -144,6 +144,9 @@
     1.4  lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
     1.5    using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
     1.6  
     1.7 +lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1"
     1.8 +using measure_pmf.prob_space[of p] by simp
     1.9 +
    1.10  lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
    1.11    by (simp add: space_subprob_algebra subprob_space_measure_pmf)
    1.12  
    1.13 @@ -198,6 +201,9 @@
    1.14    using AE_measure_singleton[of M] AE_measure_pmf[of M]
    1.15    by (auto simp: set_pmf.rep_eq)
    1.16  
    1.17 +lemma AE_pmfI: "(\<And>y. y \<in> set_pmf M \<Longrightarrow> P y) \<Longrightarrow> almost_everywhere (measure_pmf M) P"
    1.18 +by(simp add: AE_measure_pmf_iff)
    1.19 +
    1.20  lemma countable_set_pmf [simp]: "countable (set_pmf p)"
    1.21    by transfer (metis prob_space.finite_measure finite_measure.countable_support)
    1.22  
    1.23 @@ -487,6 +493,9 @@
    1.24  lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
    1.25    unfolding map_pmf_rep_eq by (subst emeasure_distr) auto
    1.26  
    1.27 +lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
    1.28 +using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure)
    1.29 +
    1.30  lemma nn_integral_map_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>map_pmf g M) = (\<integral>\<^sup>+x. f (g x) \<partial>M)"
    1.31    unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto
    1.32  
    1.33 @@ -810,6 +819,67 @@
    1.34  
    1.35  end
    1.36  
    1.37 +lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y"
    1.38 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
    1.39 +
    1.40 +lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\<lambda>x. (x, y)) x"
    1.41 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
    1.42 +
    1.43 +lemma pair_pair_pmf: "pair_pmf (pair_pmf u v) w = map_pmf (\<lambda>(x, (y, z)). ((x, y), z)) (pair_pmf u (pair_pmf v w))"
    1.44 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf)
    1.45 +
    1.46 +lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\<lambda>(x, y). (y, x)) (pair_pmf y x)"
    1.47 +unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)
    1.48 +
    1.49 +lemma set_pmf_subset_singleton: "set_pmf p \<subseteq> {x} \<longleftrightarrow> p = return_pmf x"
    1.50 +proof(intro iffI pmf_eqI)
    1.51 +  fix i
    1.52 +  assume x: "set_pmf p \<subseteq> {x}"
    1.53 +  hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
    1.54 +  have "ereal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
    1.55 +  also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
    1.56 +  also have "\<dots> = 1" by simp
    1.57 +  finally show "pmf p i = pmf (return_pmf x) i" using x
    1.58 +    by(auto split: split_indicator simp add: pmf_eq_0_set_pmf)
    1.59 +qed auto
    1.60 +
    1.61 +lemma bind_eq_return_pmf:
    1.62 +  "bind_pmf p f = return_pmf x \<longleftrightarrow> (\<forall>y\<in>set_pmf p. f y = return_pmf x)"
    1.63 +  (is "?lhs \<longleftrightarrow> ?rhs")
    1.64 +proof(intro iffI strip)
    1.65 +  fix y
    1.66 +  assume y: "y \<in> set_pmf p"
    1.67 +  assume "?lhs"
    1.68 +  hence "set_pmf (bind_pmf p f) = {x}" by simp
    1.69 +  hence "(\<Union>y\<in>set_pmf p. set_pmf (f y)) = {x}" by simp
    1.70 +  hence "set_pmf (f y) \<subseteq> {x}" using y by auto
    1.71 +  thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton)
    1.72 +next
    1.73 +  assume *: ?rhs
    1.74 +  show ?lhs
    1.75 +  proof(rule pmf_eqI)
    1.76 +    fix i
    1.77 +    have "ereal (pmf (bind_pmf p f) i) = \<integral>\<^sup>+ y. ereal (pmf (f y) i) \<partial>p" by(simp add: ereal_pmf_bind)
    1.78 +    also have "\<dots> = \<integral>\<^sup>+ y. ereal (pmf (return_pmf x) i) \<partial>p"
    1.79 +      by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
    1.80 +    also have "\<dots> = ereal (pmf (return_pmf x) i)" by simp
    1.81 +    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp
    1.82 +  qed
    1.83 +qed
    1.84 +
    1.85 +lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True"
    1.86 +proof -
    1.87 +  have "pmf p False + pmf p True = measure p {False} + measure p {True}"
    1.88 +    by(simp add: measure_pmf_single)
    1.89 +  also have "\<dots> = measure p ({False} \<union> {True})"
    1.90 +    by(subst measure_pmf.finite_measure_Union) simp_all
    1.91 +  also have "{False} \<union> {True} = space p" by auto
    1.92 +  finally show ?thesis by simp
    1.93 +qed
    1.94 +
    1.95 +lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False"
    1.96 +by(simp add: pmf_False_conv_True)
    1.97 +
    1.98  subsection \<open> Conditional Probabilities \<close>
    1.99  
   1.100  lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
   1.101 @@ -946,6 +1016,22 @@
   1.102    finally show "measure p {x. R x y} = measure q {y. R x y}" .
   1.103  qed
   1.104  
   1.105 +lemma rel_pmf_measureD:
   1.106 +  assumes "rel_pmf R p q"
   1.107 +  shows "measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
   1.108 +using assms
   1.109 +proof cases
   1.110 +  fix pq
   1.111 +  assume R: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
   1.112 +    and p[symmetric]: "map_pmf fst pq = p"
   1.113 +    and q[symmetric]: "map_pmf snd pq = q"
   1.114 +  have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p)
   1.115 +  also have "\<dots> \<le> measure (measure_pmf pq) {y. \<exists>x\<in>A. R x (snd y)}"
   1.116 +    by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R)
   1.117 +  also have "\<dots> = ?rhs" by(simp add: q)
   1.118 +  finally show ?thesis .
   1.119 +qed
   1.120 +
   1.121  lemma rel_pmf_iff_measure:
   1.122    assumes "symp R" "transp R"
   1.123    shows "rel_pmf R p q \<longleftrightarrow>
   1.124 @@ -1092,6 +1178,9 @@
   1.125    qed
   1.126  qed (fact natLeq_card_order natLeq_cinfinite)+
   1.127  
   1.128 +lemma map_pmf_idI: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
   1.129 +by(simp cong: pmf.map_cong)
   1.130 +
   1.131  lemma rel_pmf_conj[simp]:
   1.132    "rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
   1.133    "rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
   1.134 @@ -1190,6 +1279,31 @@
   1.135    by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
   1.136       (auto simp add: pmf.map_comp o_def assms)
   1.137  
   1.138 +lemma rel_pmf_bij_betw:
   1.139 +  assumes f: "bij_betw f (set_pmf p) (set_pmf q)"
   1.140 +  and eq: "\<And>x. x \<in> set_pmf p \<Longrightarrow> pmf p x = pmf q (f x)"
   1.141 +  shows "rel_pmf (\<lambda>x y. f x = y) p q"
   1.142 +proof(rule rel_pmf.intros)
   1.143 +  let ?pq = "map_pmf (\<lambda>x. (x, f x)) p"
   1.144 +  show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def)
   1.145 +
   1.146 +  have "map_pmf f p = q"
   1.147 +  proof(rule pmf_eqI)
   1.148 +    fix i
   1.149 +    show "pmf (map_pmf f p) i = pmf q i"
   1.150 +    proof(cases "i \<in> set_pmf q")
   1.151 +      case True
   1.152 +      with f obtain j where "i = f j" "j \<in> set_pmf p"
   1.153 +        by(auto simp add: bij_betw_def image_iff)
   1.154 +      thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq)
   1.155 +    next
   1.156 +      case False thus ?thesis
   1.157 +        by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric])
   1.158 +    qed
   1.159 +  qed
   1.160 +  then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def)
   1.161 +qed auto
   1.162 +
   1.163  context
   1.164  begin
   1.165  
   1.166 @@ -1442,7 +1556,7 @@
   1.167  lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
   1.168    using S_finite S_not_empty by (auto simp: set_pmf_iff)
   1.169  
   1.170 -lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
   1.171 +lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1"
   1.172    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
   1.173  
   1.174  lemma nn_integral_pmf_of_set':
   1.175 @@ -1471,6 +1585,13 @@
   1.176  apply(rule setsum.cong; simp_all)
   1.177  done
   1.178  
   1.179 +lemma emeasure_pmf_of_set:
   1.180 +  "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
   1.181 +apply(subst nn_integral_indicator[symmetric], simp)
   1.182 +apply(subst nn_integral_pmf_of_set)
   1.183 +apply(simp add: o_def max_def ereal_indicator[symmetric] S_not_empty S_finite real_of_nat_indicator[symmetric] of_nat_setsum[symmetric] setsum_indicator_eq_card del: of_nat_setsum)
   1.184 +done
   1.185 +
   1.186  end
   1.187  
   1.188  lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
   1.189 @@ -1498,6 +1619,14 @@
   1.190  lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
   1.191  by(rule pmf_eqI) simp_all
   1.192  
   1.193 +
   1.194 +
   1.195 +lemma measure_pmf_of_set:
   1.196 +  assumes "S \<noteq> {}" "finite S"
   1.197 +  shows "measure (measure_pmf (pmf_of_set S)) A = card (S \<inter> A) / card S"
   1.198 +using emeasure_pmf_of_set[OF assms, of A]
   1.199 +unfolding measure_pmf.emeasure_eq_measure by simp
   1.200 +
   1.201  subsubsection \<open> Poisson Distribution \<close>
   1.202  
   1.203  context
   1.204 @@ -1564,4 +1693,15 @@
   1.205  lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
   1.206    by (simp add: set_pmf_binomial_eq)
   1.207  
   1.208 +context begin interpretation lifting_syntax .
   1.209 +
   1.210 +lemma bind_pmf_parametric [transfer_rule]:
   1.211 +  "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
   1.212 +by(blast intro: rel_pmf_bindI dest: rel_funD)
   1.213 +
   1.214 +lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf"
   1.215 +by(rule rel_funI) simp
   1.216 +
   1.217  end
   1.218 +
   1.219 +end