author Andreas Lochbihler Wed Nov 11 10:28:22 2015 +0100 (2015-11-11) changeset 61634 48e2de1b1df5 parent 61633 64e6d712af16 child 61635 c657ee4f59b7
```     1.1 --- a/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:13:40 2015 +0100
1.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Wed Nov 11 10:28:22 2015 +0100
1.3 @@ -1567,4 +1567,8 @@
1.4    by (rule measure_eqI)
1.5       (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)
1.6
1.7 +lemma null_measure_in_space_subprob_algebra [simp]:
1.8 +  "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"
1.10 +
1.11  end
```
```     2.1 --- a/src/HOL/Probability/Measure_Space.thy	Wed Nov 11 10:13:40 2015 +0100
2.2 +++ b/src/HOL/Probability/Measure_Space.thy	Wed Nov 11 10:28:22 2015 +0100
2.3 @@ -2106,6 +2106,56 @@
2.4  lemma null_measure_idem [simp]: "null_measure (null_measure M) = null_measure M"
2.5  by(rule measure_eqI) simp_all
2.6
2.7 +subsection \<open>Scaling a measure\<close>
2.8 +
2.9 +definition scale_measure :: "real \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
2.10 +where "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. (max 0 r) * emeasure M A)"
2.11 +
2.12 +lemma space_scale_measure: "space (scale_measure r M) = space M"
2.14 +
2.15 +lemma sets_scale_measure [simp, measurable_cong]: "sets (scale_measure r M) = sets M"
2.17 +
2.18 +lemma emeasure_scale_measure [simp]:
2.19 +  "emeasure (scale_measure r M) A = max 0 r * emeasure M A"
2.20 +  (is "_ = ?\<mu> A")
2.21 +proof(cases "A \<in> sets M")
2.22 +  case True
2.23 +  show ?thesis unfolding scale_measure_def
2.24 +  proof(rule emeasure_measure_of_sigma)
2.25 +    show "sigma_algebra (space M) (sets M)" ..
2.26 +    show "positive (sets M) ?\<mu>" by(simp add: positive_def emeasure_nonneg)
2.27 +    show "countably_additive (sets M) ?\<mu>"
2.29 +      fix A :: "nat \<Rightarrow> _"  assume *: "range A \<subseteq> sets M" "disjoint_family A"
2.30 +      have "(\<Sum>i. ?\<mu> (A i)) = max 0 (ereal r) * (\<Sum>i. emeasure M (A i))"
2.31 +        by(rule suminf_cmult_ereal)(simp_all add: emeasure_nonneg)
2.32 +      also have "\<dots> = ?\<mu> (\<Union>i. A i)" using * by(simp add: suminf_emeasure)
2.33 +      finally show "(\<Sum>i. ?\<mu> (A i)) = ?\<mu> (\<Union>i. A i)" .
2.34 +    qed
2.35 +  qed(fact True)
2.37 +
2.38 +lemma measure_scale_measure [simp]: "measure (scale_measure r M) A = max 0 r * measure M A"
2.40 +
2.41 +lemma scale_measure_1 [simp]: "scale_measure 1 M = M"
2.43 +
2.44 +lemma scale_measure_le_0: "r \<le> 0 \<Longrightarrow> scale_measure r M = null_measure M"
2.46 +
2.47 +lemma scale_measure_0 [simp]: "scale_measure 0 M = null_measure M"
2.49 +
2.50 +lemma scale_scale_measure [simp]:
2.51 +  "scale_measure r (scale_measure r' M) = scale_measure (max 0 r * max 0 r') M"
2.52 +by(rule measure_eqI)(simp_all add: max_def mult.assoc times_ereal.simps(1)[symmetric] del: times_ereal.simps(1))
2.53 +
2.54 +lemma scale_null_measure [simp]: "scale_measure r (null_measure M) = null_measure M"
2.55 +by(rule measure_eqI) simp_all
2.56 +
2.57  subsection \<open>Measures form a chain-complete partial order\<close>
2.58
2.59  instantiation measure :: (type) order_bot
```
```     3.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:13:40 2015 +0100
3.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Wed Nov 11 10:28:22 2015 +0100
3.3 @@ -2719,4 +2719,32 @@
3.4    "UNIV = sets (uniform_count_measure UNIV) \<longleftrightarrow> True"
3.6
3.7 +subsubsection \<open>Scaled measure\<close>
3.8 +
3.9 +lemma nn_integral_scale_measure':
3.10 +  assumes f: "f \<in> borel_measurable M" "\<And>x. 0 \<le> f x"
3.11 +  shows "nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
3.12 +  using f
3.13 +proof induction
3.14 +  case (cong f g)
3.15 +  thus ?case
3.16 +    by(simp add: cong.hyps space_scale_measure cong: nn_integral_cong_simp)
3.17 +next
3.18 +  case (mult f c)
3.19 +  thus ?case
3.20 +    by(simp add: nn_integral_cmult max_def mult.assoc mult.left_commute)
3.21 +next
3.22 +  case (add f g)
3.23 +  thus ?case
3.25 +next
3.26 +  case (seq U)
3.27 +  thus ?case
3.28 +    by(simp add: nn_integral_monotone_convergence_SUP SUP_ereal_mult_left nn_integral_nonneg)
3.29 +qed simp
3.30 +
3.31 +lemma nn_integral_scale_measure:
3.32 +  "f \<in> borel_measurable M \<Longrightarrow> nn_integral (scale_measure r M) f = max 0 r * nn_integral M f"
3.33 +by(subst (1 2) nn_integral_max_0[symmetric])(rule nn_integral_scale_measure', simp_all)
3.34 +
3.35  end
```
```     4.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:13:40 2015 +0100
4.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Wed Nov 11 10:28:22 2015 +0100
4.3 @@ -144,6 +144,9 @@
4.4  lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
4.5    using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
4.6
4.7 +lemma measure_pmf_UNIV [simp]: "measure (measure_pmf p) UNIV = 1"
4.8 +using measure_pmf.prob_space[of p] by simp
4.9 +
4.10  lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
4.11    by (simp add: space_subprob_algebra subprob_space_measure_pmf)
4.12
4.13 @@ -198,6 +201,9 @@
4.14    using AE_measure_singleton[of M] AE_measure_pmf[of M]
4.15    by (auto simp: set_pmf.rep_eq)
4.16
4.17 +lemma AE_pmfI: "(\<And>y. y \<in> set_pmf M \<Longrightarrow> P y) \<Longrightarrow> almost_everywhere (measure_pmf M) P"
4.19 +
4.20  lemma countable_set_pmf [simp]: "countable (set_pmf p)"
4.21    by transfer (metis prob_space.finite_measure finite_measure.countable_support)
4.22
4.23 @@ -487,6 +493,9 @@
4.24  lemma emeasure_map_pmf[simp]: "emeasure (map_pmf f M) X = emeasure M (f -` X)"
4.25    unfolding map_pmf_rep_eq by (subst emeasure_distr) auto
4.26
4.27 +lemma measure_map_pmf[simp]: "measure (map_pmf f M) X = measure M (f -` X)"
4.28 +using emeasure_map_pmf[of f M X] by(simp add: measure_pmf.emeasure_eq_measure)
4.29 +
4.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)"
4.31    unfolding map_pmf_rep_eq by (intro nn_integral_distr) auto
4.32
4.33 @@ -810,6 +819,67 @@
4.34
4.35  end
4.36
4.37 +lemma pair_return_pmf1: "pair_pmf (return_pmf x) y = map_pmf (Pair x) y"
4.38 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
4.39 +
4.40 +lemma pair_return_pmf2: "pair_pmf x (return_pmf y) = map_pmf (\<lambda>x. (x, y)) x"
4.41 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def)
4.42 +
4.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))"
4.44 +by(simp add: pair_pmf_def bind_return_pmf map_pmf_def bind_assoc_pmf)
4.45 +
4.46 +lemma pair_commute_pmf: "pair_pmf x y = map_pmf (\<lambda>(x, y). (y, x)) (pair_pmf y x)"
4.47 +unfolding pair_pmf_def by(subst bind_commute_pmf)(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)
4.48 +
4.49 +lemma set_pmf_subset_singleton: "set_pmf p \<subseteq> {x} \<longleftrightarrow> p = return_pmf x"
4.50 +proof(intro iffI pmf_eqI)
4.51 +  fix i
4.52 +  assume x: "set_pmf p \<subseteq> {x}"
4.53 +  hence *: "set_pmf p = {x}" using set_pmf_not_empty[of p] by auto
4.54 +  have "ereal (pmf p x) = \<integral>\<^sup>+ i. indicator {x} i \<partial>p" by(simp add: emeasure_pmf_single)
4.55 +  also have "\<dots> = \<integral>\<^sup>+ i. 1 \<partial>p" by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
4.56 +  also have "\<dots> = 1" by simp
4.57 +  finally show "pmf p i = pmf (return_pmf x) i" using x
4.58 +    by(auto split: split_indicator simp add: pmf_eq_0_set_pmf)
4.59 +qed auto
4.60 +
4.61 +lemma bind_eq_return_pmf:
4.62 +  "bind_pmf p f = return_pmf x \<longleftrightarrow> (\<forall>y\<in>set_pmf p. f y = return_pmf x)"
4.63 +  (is "?lhs \<longleftrightarrow> ?rhs")
4.64 +proof(intro iffI strip)
4.65 +  fix y
4.66 +  assume y: "y \<in> set_pmf p"
4.67 +  assume "?lhs"
4.68 +  hence "set_pmf (bind_pmf p f) = {x}" by simp
4.69 +  hence "(\<Union>y\<in>set_pmf p. set_pmf (f y)) = {x}" by simp
4.70 +  hence "set_pmf (f y) \<subseteq> {x}" using y by auto
4.71 +  thus "f y = return_pmf x" by(simp add: set_pmf_subset_singleton)
4.72 +next
4.73 +  assume *: ?rhs
4.74 +  show ?lhs
4.75 +  proof(rule pmf_eqI)
4.76 +    fix i
4.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)
4.78 +    also have "\<dots> = \<integral>\<^sup>+ y. ereal (pmf (return_pmf x) i) \<partial>p"
4.79 +      by(rule nn_integral_cong_AE)(simp add: AE_measure_pmf_iff * )
4.80 +    also have "\<dots> = ereal (pmf (return_pmf x) i)" by simp
4.81 +    finally show "pmf (bind_pmf p f) i = pmf (return_pmf x) i" by simp
4.82 +  qed
4.83 +qed
4.84 +
4.85 +lemma pmf_False_conv_True: "pmf p False = 1 - pmf p True"
4.86 +proof -
4.87 +  have "pmf p False + pmf p True = measure p {False} + measure p {True}"
4.89 +  also have "\<dots> = measure p ({False} \<union> {True})"
4.90 +    by(subst measure_pmf.finite_measure_Union) simp_all
4.91 +  also have "{False} \<union> {True} = space p" by auto
4.92 +  finally show ?thesis by simp
4.93 +qed
4.94 +
4.95 +lemma pmf_True_conv_False: "pmf p True = 1 - pmf p False"
4.97 +
4.98  subsection \<open> Conditional Probabilities \<close>
4.99
4.100  lemma measure_pmf_zero_iff: "measure (measure_pmf p) s = 0 \<longleftrightarrow> set_pmf p \<inter> s = {}"
4.101 @@ -946,6 +1016,22 @@
4.102    finally show "measure p {x. R x y} = measure q {y. R x y}" .
4.103  qed
4.104
4.105 +lemma rel_pmf_measureD:
4.106 +  assumes "rel_pmf R p q"
4.107 +  shows "measure (measure_pmf p) A \<le> measure (measure_pmf q) {y. \<exists>x\<in>A. R x y}" (is "?lhs \<le> ?rhs")
4.108 +using assms
4.109 +proof cases
4.110 +  fix pq
4.111 +  assume R: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
4.112 +    and p[symmetric]: "map_pmf fst pq = p"
4.113 +    and q[symmetric]: "map_pmf snd pq = q"
4.114 +  have "?lhs = measure (measure_pmf pq) (fst -` A)" by(simp add: p)
4.115 +  also have "\<dots> \<le> measure (measure_pmf pq) {y. \<exists>x\<in>A. R x (snd y)}"
4.116 +    by(rule measure_pmf.finite_measure_mono_AE)(auto 4 3 simp add: AE_measure_pmf_iff dest: R)
4.117 +  also have "\<dots> = ?rhs" by(simp add: q)
4.118 +  finally show ?thesis .
4.119 +qed
4.120 +
4.121  lemma rel_pmf_iff_measure:
4.122    assumes "symp R" "transp R"
4.123    shows "rel_pmf R p q \<longleftrightarrow>
4.124 @@ -1092,6 +1178,9 @@
4.125    qed
4.126  qed (fact natLeq_card_order natLeq_cinfinite)+
4.127
4.128 +lemma map_pmf_idI: "(\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = x) \<Longrightarrow> map_pmf f p = p"
4.129 +by(simp cong: pmf.map_cong)
4.130 +
4.131  lemma rel_pmf_conj[simp]:
4.132    "rel_pmf (\<lambda>x y. P \<and> Q x y) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
4.133    "rel_pmf (\<lambda>x y. Q x y \<and> P) x y \<longleftrightarrow> P \<and> rel_pmf Q x y"
4.134 @@ -1190,6 +1279,31 @@
4.135    by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
4.136       (auto simp add: pmf.map_comp o_def assms)
4.137
4.138 +lemma rel_pmf_bij_betw:
4.139 +  assumes f: "bij_betw f (set_pmf p) (set_pmf q)"
4.140 +  and eq: "\<And>x. x \<in> set_pmf p \<Longrightarrow> pmf p x = pmf q (f x)"
4.141 +  shows "rel_pmf (\<lambda>x y. f x = y) p q"
4.142 +proof(rule rel_pmf.intros)
4.143 +  let ?pq = "map_pmf (\<lambda>x. (x, f x)) p"
4.144 +  show "map_pmf fst ?pq = p" by(simp add: pmf.map_comp o_def)
4.145 +
4.146 +  have "map_pmf f p = q"
4.147 +  proof(rule pmf_eqI)
4.148 +    fix i
4.149 +    show "pmf (map_pmf f p) i = pmf q i"
4.150 +    proof(cases "i \<in> set_pmf q")
4.151 +      case True
4.152 +      with f obtain j where "i = f j" "j \<in> set_pmf p"
4.153 +        by(auto simp add: bij_betw_def image_iff)
4.154 +      thus ?thesis using f by(simp add: bij_betw_def pmf_map_inj eq)
4.155 +    next
4.156 +      case False thus ?thesis
4.157 +        by(subst pmf_map_outside)(auto simp add: set_pmf_iff eq[symmetric])
4.158 +    qed
4.159 +  qed
4.160 +  then show "map_pmf snd ?pq = q" by(simp add: pmf.map_comp o_def)
4.161 +qed auto
4.162 +
4.163  context
4.164  begin
4.165
4.166 @@ -1442,7 +1556,7 @@
4.167  lemma set_pmf_of_set[simp]: "set_pmf pmf_of_set = S"
4.168    using S_finite S_not_empty by (auto simp: set_pmf_iff)
4.169
4.170 -lemma emeasure_pmf_of_set[simp]: "emeasure pmf_of_set S = 1"
4.171 +lemma emeasure_pmf_of_set_space[simp]: "emeasure pmf_of_set S = 1"
4.172    by (rule measure_pmf.emeasure_eq_1_AE) (auto simp: AE_measure_pmf_iff)
4.173
4.174  lemma nn_integral_pmf_of_set':
4.175 @@ -1471,6 +1585,13 @@
4.176  apply(rule setsum.cong; simp_all)
4.177  done
4.178
4.179 +lemma emeasure_pmf_of_set:
4.180 +  "emeasure (measure_pmf pmf_of_set) A = card (S \<inter> A) / card S"
4.181 +apply(subst nn_integral_indicator[symmetric], simp)
4.182 +apply(subst nn_integral_pmf_of_set)
4.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)
4.184 +done
4.185 +
4.186  end
4.187
4.188  lemma pmf_of_set_singleton: "pmf_of_set {x} = return_pmf x"
4.189 @@ -1498,6 +1619,14 @@
4.190  lemma bernoulli_pmf_half_conv_pmf_of_set: "bernoulli_pmf (1 / 2) = pmf_of_set UNIV"
4.191  by(rule pmf_eqI) simp_all
4.192
4.193 +
4.194 +
4.195 +lemma measure_pmf_of_set:
4.196 +  assumes "S \<noteq> {}" "finite S"
4.197 +  shows "measure (measure_pmf (pmf_of_set S)) A = card (S \<inter> A) / card S"
4.198 +using emeasure_pmf_of_set[OF assms, of A]
4.199 +unfolding measure_pmf.emeasure_eq_measure by simp
4.200 +
4.201  subsubsection \<open> Poisson Distribution \<close>
4.202
4.203  context
4.204 @@ -1564,4 +1693,15 @@
4.205  lemma set_pmf_binomial[simp]: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (binomial_pmf n p) = {..n}"
4.207
4.208 +context begin interpretation lifting_syntax .
4.209 +
4.210 +lemma bind_pmf_parametric [transfer_rule]:
4.211 +  "(rel_pmf A ===> (A ===> rel_pmf B) ===> rel_pmf B) bind_pmf bind_pmf"
4.212 +by(blast intro: rel_pmf_bindI dest: rel_funD)
4.213 +
4.214 +lemma return_pmf_parametric [transfer_rule]: "(A ===> rel_pmf A) return_pmf return_pmf"
4.215 +by(rule rel_funI) simp
4.216 +
4.217  end
4.218 +
4.219 +end
```