src/HOL/Probability/Probability_Mass_Function.thy
changeset 59002 2c8b2fb54b88
parent 59000 6eb0725503fc
child 59023 4999a616336c
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 08:18:58 2014 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Fri Nov 14 13:18:33 2014 +0100
     1.3 @@ -281,6 +281,12 @@
     1.4    unfolding `p = q`[symmetric] measure_pmf_inject[symmetric] map_pmf.rep_eq
     1.5    by (auto simp add: emeasure_distr AE_measure_pmf_iff intro!: emeasure_eq_AE measure_eqI)
     1.6  
     1.7 +lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
     1.8 +  unfolding map_pmf.rep_eq by (subst emeasure_distr) auto
     1.9 +
    1.10 +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.11 +  unfolding map_pmf.rep_eq by (intro nn_integral_distr) auto
    1.12 +
    1.13  lemma pmf_set_map: 
    1.14    fixes f :: "'a \<Rightarrow> 'b"
    1.15    shows "set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
    1.16 @@ -433,6 +439,17 @@
    1.17  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
    1.18    by (auto simp add: set_pmf_iff UNIV_bool)
    1.19  
    1.20 +lemma nn_integral_bernoulli_pmf[simp]: 
    1.21 +  assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
    1.22 +  shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
    1.23 +  by (subst nn_integral_measure_pmf_support[of UNIV])
    1.24 +     (auto simp: UNIV_bool field_simps)
    1.25 +
    1.26 +lemma integral_bernoulli_pmf[simp]: 
    1.27 +  assumes [simp]: "0 \<le> p" "p \<le> 1"
    1.28 +  shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
    1.29 +  by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
    1.30 +
    1.31  lift_definition geometric_pmf :: "nat pmf" is "\<lambda>n. 1 / 2^Suc n"
    1.32  proof
    1.33    note geometric_sums[of "1 / 2"]
    1.34 @@ -445,7 +462,7 @@
    1.35  lemma pmf_geometric[simp]: "pmf geometric_pmf n = 1 / 2^Suc n"
    1.36    by transfer rule
    1.37  
    1.38 -lemma set_pmf_geometric: "set_pmf geometric_pmf = UNIV"
    1.39 +lemma set_pmf_geometric[simp]: "set_pmf geometric_pmf = UNIV"
    1.40    by (auto simp: set_pmf_iff)
    1.41  
    1.42  context
    1.43 @@ -485,6 +502,9 @@
    1.44  lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
    1.45    using S_finite S_not_empty by (auto simp: set_pmf_iff)
    1.46  
    1.47 +lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
    1.48 +  by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
    1.49 +
    1.50  end
    1.51  
    1.52  end
    1.53 @@ -558,12 +578,18 @@
    1.54  lemma map_return_pmf: "map_pmf f (return_pmf x) = return_pmf (f x)"
    1.55    by transfer (simp add: distr_return)
    1.56  
    1.57 -lemma set_pmf_return: "set_pmf (return_pmf x) = {x}"
    1.58 +lemma set_return_pmf: "set_pmf (return_pmf x) = {x}"
    1.59    by transfer (auto simp add: measure_return split: split_indicator)
    1.60  
    1.61  lemma pmf_return: "pmf (return_pmf x) y = indicator {y} x"
    1.62    by transfer (simp add: measure_return)
    1.63  
    1.64 +lemma nn_integral_return_pmf[simp]: "0 \<le> f x \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>return_pmf x) = f x"
    1.65 +  unfolding return_pmf.rep_eq by (intro nn_integral_return) auto
    1.66 +
    1.67 +lemma emeasure_return_pmf[simp]: "emeasure (return_pmf x) X = indicator X x"
    1.68 +  unfolding return_pmf.rep_eq by (intro emeasure_return) auto
    1.69 +
    1.70  end
    1.71  
    1.72  definition "bind_pmf M f = join_pmf (map_pmf f M)"
    1.73 @@ -584,6 +610,41 @@
    1.74  lemma bind_return_pmf: "bind_pmf (return_pmf x) f = f x"
    1.75    unfolding bind_pmf_def map_return_pmf join_return_pmf ..
    1.76  
    1.77 +lemma set_bind_pmf: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
    1.78 +  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
    1.79 +  apply (subst integral_nonneg_eq_0_iff_AE)
    1.80 +  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
    1.81 +              intro!: measure_pmf.integrable_const_bound[where B=1])
    1.82 +  done
    1.83 +
    1.84 +lemma measurable_pair_restrict_pmf2:
    1.85 +  assumes "countable A"
    1.86 +  assumes "\<And>y. y \<in> A \<Longrightarrow> (\<lambda>x. f (x, y)) \<in> measurable M L"
    1.87 +  shows "f \<in> measurable (M \<Otimes>\<^sub>M restrict_space (measure_pmf N) A) L"
    1.88 +  apply (subst measurable_cong_sets)
    1.89 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
    1.90 +  apply (simp_all add: restrict_count_space)
    1.91 +  apply (subst split_eta[symmetric])
    1.92 +  unfolding measurable_split_conv
    1.93 +  apply (rule measurable_compose_countable'[OF _ measurable_snd `countable A`])
    1.94 +  apply (rule measurable_compose[OF measurable_fst])
    1.95 +  apply fact
    1.96 +  done
    1.97 +
    1.98 +lemma measurable_pair_restrict_pmf1:
    1.99 +  assumes "countable A"
   1.100 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (\<lambda>y. f (x, y)) \<in> measurable N L"
   1.101 +  shows "f \<in> measurable (restrict_space (measure_pmf M) A \<Otimes>\<^sub>M N) L"
   1.102 +  apply (subst measurable_cong_sets)
   1.103 +  apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   1.104 +  apply (simp_all add: restrict_count_space)
   1.105 +  apply (subst split_eta[symmetric])
   1.106 +  unfolding measurable_split_conv
   1.107 +  apply (rule measurable_compose_countable'[OF _ measurable_fst `countable A`])
   1.108 +  apply (rule measurable_compose[OF measurable_snd])
   1.109 +  apply fact
   1.110 +  done
   1.111 +                                
   1.112  lemma bind_commute_pmf: "bind_pmf A (\<lambda>x. bind_pmf B (C x)) = bind_pmf B (\<lambda>y. bind_pmf A (\<lambda>x. C x y))"
   1.113    unfolding pmf_eq_iff pmf_bind
   1.114  proof
   1.115 @@ -601,36 +662,15 @@
   1.116    have "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>A)"
   1.117      by (rule integral_cong) (auto intro!: integral_pmf_restrict)
   1.118    also have "\<dots> = (\<integral> x. (\<integral> y. pmf (C x y) i \<partial>restrict_space B B) \<partial>restrict_space A A)"
   1.119 -    apply (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral)
   1.120 -    apply (auto simp: measurable_split_conv)
   1.121 -    apply (subst measurable_cong_sets)
   1.122 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   1.123 -    apply (simp add: restrict_count_space)
   1.124 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   1.125 -    apply (rule measurable_compose[OF measurable_fst])
   1.126 -    apply (auto intro: countable_set_pmf)
   1.127 -    done
   1.128 +    by (intro integral_pmf_restrict B.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   1.129 +              countable_set_pmf borel_measurable_count_space)
   1.130    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>restrict_space B B)"
   1.131 -    apply (rule AB.Fubini_integral[symmetric])
   1.132 -    apply (auto intro!: AB.integrable_const_bound[where B=1] simp: pmf_nonneg pmf_le_1)
   1.133 -    apply (auto simp: measurable_split_conv)
   1.134 -    apply (subst measurable_cong_sets)
   1.135 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   1.136 -    apply (simp add: restrict_count_space)
   1.137 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   1.138 -    apply (rule measurable_compose[OF measurable_fst])
   1.139 -    apply (auto intro: countable_set_pmf)
   1.140 -    done
   1.141 +    by (rule AB.Fubini_integral[symmetric])
   1.142 +       (auto intro!: AB.integrable_const_bound[where B=1] measurable_pair_restrict_pmf2
   1.143 +             simp: pmf_nonneg pmf_le_1 countable_set_pmf measurable_restrict_space1)
   1.144    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>restrict_space A A \<partial>B)"
   1.145 -    apply (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral)
   1.146 -    apply (auto simp: measurable_split_conv)
   1.147 -    apply (subst measurable_cong_sets)
   1.148 -    apply (rule sets_pair_measure_cong sets_restrict_space_cong sets_measure_pmf_count_space refl)+
   1.149 -    apply (simp add: restrict_count_space)
   1.150 -    apply (rule measurable_compose_countable'[OF _ measurable_snd])
   1.151 -    apply (rule measurable_compose[OF measurable_fst])
   1.152 -    apply (auto intro: countable_set_pmf)
   1.153 -    done
   1.154 +    by (intro integral_pmf_restrict[symmetric] A.borel_measurable_lebesgue_integral measurable_pair_restrict_pmf2
   1.155 +              countable_set_pmf borel_measurable_count_space)
   1.156    also have "\<dots> = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)"
   1.157      by (rule integral_cong) (auto intro!: integral_pmf_restrict[symmetric])
   1.158    finally show "(\<integral> x. \<integral> y. pmf (C x y) i \<partial>B \<partial>A) = (\<integral> y. \<integral> x. pmf (C x y) i \<partial>A \<partial>B)" .
   1.159 @@ -642,6 +682,22 @@
   1.160  
   1.161  interpretation pmf_as_measure .
   1.162  
   1.163 +lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
   1.164 +  by transfer simp
   1.165 +
   1.166 +lemma nn_integral_bind_pmf[simp]: "(\<integral>\<^sup>+x. f x \<partial>bind_pmf M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   1.167 +  using measurable_measure_pmf[of N]
   1.168 +  unfolding measure_pmf_bind
   1.169 +  apply (subst (1 3) nn_integral_max_0[symmetric])
   1.170 +  apply (intro nn_integral_bind[where B="count_space UNIV"])
   1.171 +  apply auto
   1.172 +  done
   1.173 +
   1.174 +lemma emeasure_bind_pmf[simp]: "emeasure (bind_pmf M N) X = (\<integral>\<^sup>+x. emeasure (N x) X \<partial>M)"
   1.175 +  using measurable_measure_pmf[of N]
   1.176 +  unfolding measure_pmf_bind
   1.177 +  by (subst emeasure_bind[where N="count_space UNIV"]) auto
   1.178 +
   1.179  lemma bind_return_pmf': "bind_pmf N return_pmf = N"
   1.180  proof (transfer, clarify)
   1.181    fix N :: "'a measure" assume "sets N = UNIV" then show "N \<guillemotright>= return (count_space UNIV) = N"
   1.182 @@ -661,9 +717,6 @@
   1.183       (auto intro!: bind_assoc[where N="count_space UNIV" and R="count_space UNIV"]
   1.184             simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space)
   1.185  
   1.186 -lemma measure_pmf_bind: "measure_pmf (bind_pmf M f) = (measure_pmf M \<guillemotright>= (\<lambda>x. measure_pmf (f x)))"
   1.187 -  by transfer simp
   1.188 -
   1.189  end
   1.190  
   1.191  definition "pair_pmf A B = bind_pmf A (\<lambda>x. bind_pmf B (\<lambda>y. return_pmf (x, y)))"
   1.192 @@ -676,6 +729,9 @@
   1.193    apply (auto simp: indicator_eq_0_iff setsum_nonneg_eq_0_iff pmf_nonneg)
   1.194    done
   1.195  
   1.196 +lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   1.197 +  unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
   1.198 +
   1.199  lemma bind_pair_pmf:
   1.200    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
   1.201    shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
   1.202 @@ -700,18 +756,18 @@
   1.203    then show "emeasure ?L X = emeasure ?R X"
   1.204      apply (simp add: emeasure_bind[OF _ M' X])
   1.205      unfolding pair_pmf_def measure_pmf_bind[of A]
   1.206 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
   1.207 +    apply (subst nn_integral_bind)
   1.208      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   1.209      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   1.210      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   1.211      apply measurable
   1.212      unfolding measure_pmf_bind
   1.213 -    apply (subst nn_integral_bind[OF _ emeasure_nonneg])
   1.214 +    apply (subst nn_integral_bind)
   1.215      apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
   1.216      apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
   1.217      apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
   1.218      apply measurable
   1.219 -    apply (simp add: nn_integral_measure_pmf_finite set_pmf_return emeasure_nonneg pmf_return one_ereal_def[symmetric])
   1.220 +    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
   1.221      apply (subst emeasure_bind[OF _ _ X])
   1.222      apply simp
   1.223      apply (rule measurable_bind[where N="count_space UNIV"])
   1.224 @@ -727,15 +783,6 @@
   1.225      done
   1.226  qed
   1.227  
   1.228 -lemma set_pmf_bind: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
   1.229 -  apply (simp add: set_eq_iff set_pmf_iff pmf_bind)
   1.230 -  apply (subst integral_nonneg_eq_0_iff_AE)
   1.231 -  apply (auto simp: pmf_nonneg pmf_le_1 AE_measure_pmf_iff
   1.232 -              intro!: measure_pmf.integrable_const_bound[where B=1])
   1.233 -  done
   1.234 -
   1.235 -lemma set_pmf_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   1.236 -  unfolding pair_pmf_def set_pmf_bind set_pmf_return by auto
   1.237  
   1.238  (*
   1.239