add various lemmas about pmfs
authorAndreas Lochbihler
Tue Apr 14 14:15:10 2015 +0200 (2015-04-14)
changeset 60068ef2123db900c
parent 60067 f1a5bcf5658f
child 60069 d76f9047121c
add various lemmas about pmfs
src/HOL/Probability/Probability_Mass_Function.thy
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Apr 14 14:14:43 2015 +0200
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Apr 14 14:15:10 2015 +0200
     1.3 @@ -224,6 +224,9 @@
     1.4    shows "emeasure M {x} = pmf M x"
     1.5    by transfer (simp add: finite_measure.emeasure_eq_measure[OF prob_space.finite_measure])
     1.6  
     1.7 +lemma measure_pmf_single: "measure (measure_pmf M) {x} = pmf M x"
     1.8 +using emeasure_pmf_single[of M x] by(simp add: measure_pmf.emeasure_eq_measure)
     1.9 +
    1.10  lemma emeasure_measure_pmf_finite: "finite S \<Longrightarrow> emeasure (measure_pmf M) S = (\<Sum>s\<in>S. pmf M s)"
    1.11    by (subst emeasure_eq_setsum_singleton) (auto simp: emeasure_pmf_single)
    1.12  
    1.13 @@ -510,13 +513,13 @@
    1.14    finally show ?thesis .
    1.15  qed
    1.16  
    1.17 -lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
    1.18 +lemma map_return_pmf [simp]: "map_pmf f (return_pmf x) = return_pmf (f x)"
    1.19    by transfer (simp add: distr_return)
    1.20  
    1.21  lemma map_pmf_const[simp]: "map_pmf (\<lambda>_. c) M = return_pmf c"
    1.22    by transfer (auto simp: prob_space.distr_const)
    1.23  
    1.24 -lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
    1.25 +lemma pmf_return [simp]: "pmf (return_pmf x) y = indicator {y} x"
    1.26    by transfer (simp add: measure_return)
    1.27  
    1.28  lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
    1.29 @@ -592,7 +595,7 @@
    1.30    then show "emeasure ?L X = emeasure ?R X"
    1.31      apply (simp add: emeasure_bind[OF _ M' X])
    1.32      apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
    1.33 -                     nn_integral_measure_pmf_finite emeasure_nonneg pmf_return one_ereal_def[symmetric])
    1.34 +                     nn_integral_measure_pmf_finite emeasure_nonneg one_ereal_def[symmetric])
    1.35      apply (subst emeasure_bind[OF _ _ X])
    1.36      apply measurable
    1.37      apply (subst emeasure_bind[OF _ _ X])
    1.38 @@ -624,6 +627,16 @@
    1.39    by (auto simp: pmf.rep_eq map_pmf_rep_eq measure_distr AE_measure_pmf_iff inj_onD
    1.40             intro!: measure_pmf.finite_measure_eq_AE)
    1.41  
    1.42 +lemma pmf_map_inj': "inj f \<Longrightarrow> pmf (map_pmf f M) (f x) = pmf M x"
    1.43 +apply(cases "x \<in> set_pmf M")
    1.44 + apply(simp add: pmf_map_inj[OF subset_inj_on])
    1.45 +apply(simp add: pmf_eq_0_set_pmf[symmetric])
    1.46 +apply(auto simp add: pmf_eq_0_set_pmf dest: injD)
    1.47 +done
    1.48 +
    1.49 +lemma pmf_map_outside: "x \<notin> f ` set_pmf M \<Longrightarrow> pmf (map_pmf f M) x = 0"
    1.50 +unfolding pmf_eq_0_set_pmf by simp
    1.51 +
    1.52  subsection \<open> PMFs as function \<close>
    1.53  
    1.54  context
    1.55 @@ -651,6 +664,9 @@
    1.56      by transfer (simp add: measure_def emeasure_density nonneg max_def)
    1.57  qed
    1.58  
    1.59 +lemma set_embed_pmf: "set_pmf embed_pmf = {x. f x \<noteq> 0}"
    1.60 +by(auto simp add: set_pmf_eq assms pmf_embed_pmf)
    1.61 +
    1.62  end
    1.63  
    1.64  lemma embed_pmf_transfer:
    1.65 @@ -700,6 +716,9 @@
    1.66  
    1.67  end
    1.68  
    1.69 +lemma nn_integral_measure_pmf: "(\<integral>\<^sup>+ x. f x \<partial>measure_pmf p) = \<integral>\<^sup>+ x. ereal (pmf p x) * f x \<partial>count_space UNIV"
    1.70 +by(simp add: measure_pmf_eq_density nn_integral_density pmf_nonneg)
    1.71 +
    1.72  locale pmf_as_function
    1.73  begin
    1.74  
    1.75 @@ -896,11 +915,11 @@
    1.76    then show "\<And>x y. (x, y) \<in> set_pmf ?pq \<Longrightarrow> R x y"
    1.77      by auto
    1.78    show "map_pmf fst ?pq = p"
    1.79 -    by (simp add: map_bind_pmf map_return_pmf bind_return_pmf')
    1.80 +    by (simp add: map_bind_pmf bind_return_pmf')
    1.81  
    1.82    show "map_pmf snd ?pq = q"
    1.83      using R eq
    1.84 -    apply (simp add: bind_cond_pmf_cancel map_bind_pmf map_return_pmf bind_return_pmf')
    1.85 +    apply (simp add: bind_cond_pmf_cancel map_bind_pmf bind_return_pmf')
    1.86      apply (rule bind_cond_pmf_cancel)
    1.87      apply (auto simp: rel_set_def)
    1.88      done
    1.89 @@ -1064,10 +1083,10 @@
    1.90          by blast
    1.91      next
    1.92        have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    1.93 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_return_pmf map_pmf_comp)
    1.94 +        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
    1.95        then show "map_pmf snd pr = r"
    1.96          unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    1.97 -    qed (simp add: pr_def map_bind_pmf split_beta map_return_pmf map_pmf_def[symmetric] p map_pmf_comp) }
    1.98 +    qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
    1.99    then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
   1.100      by(auto simp add: le_fun_def)
   1.101  qed (fact natLeq_card_order natLeq_cinfinite)+
   1.102 @@ -1420,8 +1439,59 @@
   1.103  lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
   1.104    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
   1.105  
   1.106 +lemma nn_integral_pmf_of_set': 
   1.107 +  "(\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> nn_integral (measure_pmf pmf_of_set) f = setsum f S / card S"
   1.108 +apply(subst nn_integral_measure_pmf_finite, simp_all add: S_finite)
   1.109 +apply(simp add: setsum_ereal_left_distrib[symmetric])
   1.110 +apply(subst ereal_divide', simp add: S_not_empty S_finite)
   1.111 +apply(simp add: ereal_times_divide_eq one_ereal_def[symmetric])
   1.112 +done
   1.113 +
   1.114 +lemma nn_integral_pmf_of_set: 
   1.115 +  "nn_integral (measure_pmf pmf_of_set) f = setsum (max 0 \<circ> f) S / card S"
   1.116 +apply(subst nn_integral_max_0[symmetric])
   1.117 +apply(subst nn_integral_pmf_of_set')
   1.118 +apply simp_all
   1.119 +done
   1.120 +
   1.121 +lemma integral_pmf_of_set:
   1.122 +  "integral\<^sup>L (measure_pmf pmf_of_set) f = setsum f S / card S"
   1.123 +apply(simp add: real_lebesgue_integral_def integrable_measure_pmf_finite nn_integral_pmf_of_set S_finite)
   1.124 +apply(subst real_of_ereal_minus')
   1.125 + apply(simp add: ereal_max_0 S_finite del: ereal_max)
   1.126 +apply(simp add: ereal_max_0 S_finite S_not_empty del: ereal_max)
   1.127 +apply(simp add: field_simps S_finite S_not_empty)
   1.128 +apply(subst setsum.distrib[symmetric])
   1.129 +apply(rule setsum.cong; simp_all)
   1.130 +done
   1.131 +
   1.132  end
   1.133  
   1.134 +lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
   1.135 +by(rule pmf_eqI)(simp add: indicator_def)
   1.136 +
   1.137 +lemma map_pmf_of_set_inj: 
   1.138 +  assumes f: "inj_on f A"
   1.139 +  and [simp]: "A \<noteq> {}" "finite A"
   1.140 +  shows "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" (is "?lhs = ?rhs")
   1.141 +proof(rule pmf_eqI)
   1.142 +  fix i
   1.143 +  show "pmf ?lhs i = pmf ?rhs i"
   1.144 +  proof(cases "i \<in> f ` A")
   1.145 +    case True
   1.146 +    then obtain i' where "i = f i'" "i' \<in> A" by auto
   1.147 +    thus ?thesis using f by(simp add: card_image pmf_map_inj)
   1.148 +  next
   1.149 +    case False
   1.150 +    hence "pmf ?lhs i = 0" by(simp add: pmf_eq_0_set_pmf set_map_pmf)
   1.151 +    moreover have "pmf ?rhs i = 0" using False by simp
   1.152 +    ultimately show ?thesis by simp
   1.153 +  qed
   1.154 +qed
   1.155 +
   1.156 +lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
   1.157 +by(rule pmf_eqI) simp_all
   1.158 +
   1.159  subsubsection \<open> Poisson Distribution \<close>
   1.160  
   1.161  context