src/HOL/Probability/Probability_Mass_Function.thy
changeset 59667 651ea265d568
parent 59665 37adca7fd48f
child 59670 dee043d19729
child 59730 b7c394c7a619
     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 11:56:32 2015 +0100
     1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 15:20:40 2015 +0000
     1.3 @@ -1,5 +1,5 @@
     1.4  (*  Title:      HOL/Probability/Probability_Mass_Function.thy
     1.5 -    Author:     Johannes Hölzl, TU München 
     1.6 +    Author:     Johannes Hölzl, TU München
     1.7      Author:     Andreas Lochbihler, ETH Zurich
     1.8  *)
     1.9  
    1.10 @@ -8,7 +8,6 @@
    1.11  theory Probability_Mass_Function
    1.12  imports
    1.13    Giry_Monad
    1.14 -  "~~/src/HOL/Number_Theory/Binomial"
    1.15    "~~/src/HOL/Library/Multiset"
    1.16  begin
    1.17  
    1.18 @@ -52,14 +51,14 @@
    1.19      fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
    1.20      then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
    1.21        by (metis infinite_arbitrarily_large)
    1.22 -    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x" 
    1.23 +    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
    1.24        by auto
    1.25      { fix x assume "x \<in> X"
    1.26        from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
    1.27        then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
    1.28      note singleton_sets = this
    1.29      have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
    1.30 -      using `?M \<noteq> 0` 
    1.31 +      using `?M \<noteq> 0`
    1.32        by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
    1.33      also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
    1.34        by (rule setsum_mono) fact
    1.35 @@ -82,7 +81,7 @@
    1.36    assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)"
    1.37    then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S"
    1.38      by auto
    1.39 -  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) = 
    1.40 +  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) =
    1.41      (\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)"
    1.42      by (subst emeasure_UN_countable)
    1.43         (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
    1.44 @@ -136,7 +135,7 @@
    1.45  interpretation pmf_as_measure .
    1.46  
    1.47  lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
    1.48 -  by transfer blast 
    1.49 +  by transfer blast
    1.50  
    1.51  lemma sets_measure_pmf_count_space[measurable_cong]:
    1.52    "sets (measure_pmf M) = sets (count_space UNIV)"
    1.53 @@ -353,10 +352,10 @@
    1.54  
    1.55    have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
    1.56      by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
    1.57 -    
    1.58 +
    1.59    show "prob_space (f \<guillemotright>= g)"
    1.60      using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
    1.61 -  then interpret fg: prob_space "f \<guillemotright>= g" . 
    1.62 +  then interpret fg: prob_space "f \<guillemotright>= g" .
    1.63    show [simp]: "sets (f \<guillemotright>= g) = UNIV"
    1.64      using sets_eq_imp_space_eq[OF s_f]
    1.65      by (subst sets_bind[where N="count_space UNIV"]) auto
    1.66 @@ -385,7 +384,7 @@
    1.67    by transfer (simp add: bind_const' prob_space_imp_subprob_space)
    1.68  
    1.69  lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
    1.70 -  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind  
    1.71 +  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind
    1.72    by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
    1.73  
    1.74  lemma bind_pmf_cong:
    1.75 @@ -415,7 +414,7 @@
    1.76    using measurable_measure_pmf[of N]
    1.77    unfolding measure_pmf_bind
    1.78    by (subst emeasure_bind[where N="count_space UNIV"]) auto
    1.79 -                                
    1.80 +
    1.81  lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
    1.82    by (auto intro!: prob_space_return simp: AE_return measure_return)
    1.83  
    1.84 @@ -451,7 +450,7 @@
    1.85  proof -
    1.86    have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
    1.87       (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
    1.88 -    unfolding map_pmf_def[abs_def] comp_def by transfer_prover 
    1.89 +    unfolding map_pmf_def[abs_def] comp_def by transfer_prover
    1.90    then show ?thesis
    1.91      by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
    1.92  qed
    1.93 @@ -468,7 +467,7 @@
    1.94    using map_pmf_id unfolding id_def .
    1.95  
    1.96  lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g"
    1.97 -  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def) 
    1.98 +  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def)
    1.99  
   1.100  lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M"
   1.101    using map_pmf_compose[of f g] by (simp add: comp_def)
   1.102 @@ -665,7 +664,7 @@
   1.103    show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
   1.104    proof (rule measure_eqI)
   1.105      fix A :: "'a set"
   1.106 -    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) = 
   1.107 +    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
   1.108        (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
   1.109        by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
   1.110      also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
   1.111 @@ -706,9 +705,9 @@
   1.112  
   1.113  setup_lifting td_pmf_embed_pmf
   1.114  
   1.115 -lemma set_pmf_transfer[transfer_rule]: 
   1.116 +lemma set_pmf_transfer[transfer_rule]:
   1.117    assumes "bi_total A"
   1.118 -  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"  
   1.119 +  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"
   1.120    using `bi_total A`
   1.121    by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
   1.122       metis+
   1.123 @@ -888,14 +887,14 @@
   1.124  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
   1.125  for R p q
   1.126  where
   1.127 -  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y; 
   1.128 +  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y;
   1.129       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
   1.130    \<Longrightarrow> rel_pmf R p q"
   1.131  
   1.132  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
   1.133  proof -
   1.134    show "map_pmf id = id" by (rule map_pmf_id)
   1.135 -  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose) 
   1.136 +  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
   1.137    show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p"
   1.138      by (intro map_pmf_cong refl)
   1.139  
   1.140 @@ -1042,7 +1041,7 @@
   1.141                     map_pair)
   1.142  qed
   1.143  
   1.144 -lemma rel_pmf_reflI: 
   1.145 +lemma rel_pmf_reflI:
   1.146    assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
   1.147    shows "rel_pmf P p p"
   1.148    by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
   1.149 @@ -1089,7 +1088,7 @@
   1.150      and q: "q = map_pmf snd pq"
   1.151      and P: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> rel_pmf P x y"
   1.152      by cases auto
   1.153 -  from P obtain PQ 
   1.154 +  from P obtain PQ
   1.155      where PQ: "\<And>x y a b. \<lbrakk> (x, y) \<in> set_pmf pq; (a, b) \<in> set_pmf (PQ x y) \<rbrakk> \<Longrightarrow> P a b"
   1.156      and x: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf fst (PQ x y) = x"
   1.157      and y: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf snd (PQ x y) = y"
   1.158 @@ -1112,12 +1111,12 @@
   1.159  
   1.160  text {*
   1.161    Proof that @{const rel_pmf} preserves orders.
   1.162 -  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism, 
   1.163 -  Theoretical Computer Science 12(1):19--37, 1980, 
   1.164 +  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
   1.165 +  Theoretical Computer Science 12(1):19--37, 1980,
   1.166    @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
   1.167  *}
   1.168  
   1.169 -lemma 
   1.170 +lemma
   1.171    assumes *: "rel_pmf R p q"
   1.172    and refl: "reflp R" and trans: "transp R"
   1.173    shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
   1.174 @@ -1174,7 +1173,7 @@
   1.175      hence "measure (measure_pmf p) (?E x) \<noteq> 0"
   1.176        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
   1.177      hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
   1.178 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}" 
   1.179 +    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
   1.180        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
   1.181    ultimately show "inf R R\<inverse>\<inverse> x y"
   1.182      by (auto simp add: pq_def)
   1.183 @@ -1235,13 +1234,13 @@
   1.184  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
   1.185    by (auto simp add: set_pmf_iff UNIV_bool)
   1.186  
   1.187 -lemma nn_integral_bernoulli_pmf[simp]: 
   1.188 +lemma nn_integral_bernoulli_pmf[simp]:
   1.189    assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
   1.190    shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
   1.191    by (subst nn_integral_measure_pmf_support[of UNIV])
   1.192       (auto simp: UNIV_bool field_simps)
   1.193  
   1.194 -lemma integral_bernoulli_pmf[simp]: 
   1.195 +lemma integral_bernoulli_pmf[simp]:
   1.196    assumes [simp]: "0 \<le> p" "p \<le> 1"
   1.197    shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
   1.198    by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
   1.199 @@ -1277,7 +1276,7 @@
   1.200  
   1.201  lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M"
   1.202  proof
   1.203 -  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"  
   1.204 +  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
   1.205      using M_not_empty
   1.206      by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
   1.207                    setsum_divide_distrib[symmetric])
   1.208 @@ -1300,7 +1299,7 @@
   1.209  
   1.210  lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S"
   1.211  proof
   1.212 -  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"  
   1.213 +  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
   1.214      using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto
   1.215  qed simp
   1.216