add various lemmas
authorAndreas Lochbihler
Wed Nov 11 10:28:22 2015 +0100 (2015-11-11)
changeset 6163448e2de1b1df5
parent 61633 64e6d712af16
child 61635 c657ee4f59b7
add various lemmas
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
     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.9 +by(simp add: space_subprob_algebra subprob_space_null_measure_iff)
    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.13 +by(simp add: scale_measure_def)
    2.14 +
    2.15 +lemma sets_scale_measure [simp, measurable_cong]: "sets (scale_measure r M) = sets M"
    2.16 +by(simp add: scale_measure_def)
    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.28 +    proof (rule countably_additiveI)
    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.36 +qed(simp add: emeasure_notin_sets)
    2.37 +
    2.38 +lemma measure_scale_measure [simp]: "measure (scale_measure r M) A = max 0 r * measure M A"
    2.39 +by(simp add: measure_def max_def)
    2.40 +
    2.41 +lemma scale_measure_1 [simp]: "scale_measure 1 M = M"
    2.42 +by(rule measure_eqI)(simp_all add: max_def)
    2.43 +
    2.44 +lemma scale_measure_le_0: "r \<le> 0 \<Longrightarrow> scale_measure r M = null_measure M"
    2.45 +by(rule measure_eqI)(simp_all add: max_def)
    2.46 +
    2.47 +lemma scale_measure_0 [simp]: "scale_measure 0 M = null_measure M"
    2.48 +by(simp add: scale_measure_le_0)
    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.5  by(simp_all add: sets_uniform_count_measure)
     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.24 +    by(simp add: nn_integral_add ereal_right_distrib nn_integral_nonneg)
    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.18 +by(simp add: AE_measure_pmf_iff)
    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.88 +    by(simp add: measure_pmf_single)
    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.96 +by(simp add: pmf_False_conv_True)
    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.206    by (simp add: set_pmf_binomial_eq)
   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