# HG changeset patch # User hoelzl # Date 1412670864 -7200 # Node ID 9c66f7c541fb716275c8afe07023b73b56ad1058 # Parent 9d5013661ac6f86efd016ada3373caacc7f30372 add Giry monad diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Library/FuncSet.thy Tue Oct 07 10:34:24 2014 +0200 @@ -199,6 +199,9 @@ "(\x. x \ A \ f x = g x) \ (\x\A. f x) = (\x\A. g x)" by (simp add: fun_eq_iff Pi_def restrict_def) +lemma restrict_UNIV: "restrict f UNIV = f" + by (simp add: restrict_def) + lemma inj_on_restrict_eq [simp]: "inj_on (restrict f A) A = inj_on f A" by (simp add: inj_on_def restrict_def) diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Oct 07 10:34:24 2014 +0200 @@ -34,6 +34,12 @@ unfolding pair_measure_def using pair_measure_closed[of A B] by (rule sets_measure_of) +lemma sets_pair_in_sets: + assumes N: "space A \ space B = space N" + assumes "\a b. a \ sets A \ b \ sets B \ a \ b \ sets N" + shows "sets (A \\<^sub>M B) \ sets N" + using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N) + lemma sets_pair_measure_cong[cong]: "sets M1 = sets M1' \ sets M2 = sets M2' \ sets (M1 \\<^sub>M M2) = sets (M1' \\<^sub>M M2')" unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) @@ -42,6 +48,9 @@ "x \ sets A \ y \ sets B \ x \ y \ sets (A \\<^sub>M B)" by (auto simp: sets_pair_measure) +lemma sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)" + using pair_measureI[of "{x}" M1 "{y}" M2] by simp + lemma measurable_pair_measureI: assumes 1: "f \ space M \ space M1 \ space M2" assumes 2: "\A B. A \ sets M1 \ B \ sets M2 \ f -` (A \ B) \ space M \ sets M" @@ -98,6 +107,25 @@ and measurable_snd'': "(\x. f (snd x)) \ measurable (P \\<^sub>M M) N" by simp_all +lemma sets_pair_eq_sets_fst_snd: + "sets (A \\<^sub>M B) = sets (Sup_sigma {vimage_algebra (space A \ space B) fst A, vimage_algebra (space A \ space B) snd B})" + (is "?P = sets (Sup_sigma {?fst, ?snd})") +proof - + { fix a b assume ab: "a \ sets A" "b \ sets B" + then have "a \ b = (fst -` a \ (space A \ space B)) \ (snd -` b \ (space A \ space B))" + by (auto dest: sets.sets_into_space) + also have "\ \ sets (Sup_sigma {?fst, ?snd})" + using ab by (auto intro: in_Sup_sigma in_vimage_algebra) + finally have "a \ b \ sets (Sup_sigma {?fst, ?snd})" . } + moreover have "sets ?fst \ sets (A \\<^sub>M B)" + by (rule sets_image_in_sets) (auto simp: space_pair_measure[symmetric]) + moreover have "sets ?snd \ sets (A \\<^sub>M B)" + by (rule sets_image_in_sets) (auto simp: space_pair_measure) + ultimately show ?thesis + by (intro antisym[of "sets A" for A] sets_Sup_in_sets sets_pair_in_sets ) + (auto simp add: space_Sup_sigma space_pair_measure) +qed + lemma measurable_pair_iff: "f \ measurable M (M1 \\<^sub>M M2) \ (fst \ f) \ measurable M M1 \ (snd \ f) \ measurable M M2" by (auto intro: measurable_pair[of f M M1 M2]) diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Oct 07 10:34:24 2014 +0200 @@ -353,6 +353,25 @@ finally show "A \ sigma_sets ?\ (prod_algebra I M)" . qed +lemma sets_PiM_eq_proj: + "I \ {} \ sets (PiM I M) = sets (\\<^sub>\ i\I. vimage_algebra (\\<^sub>E i\I. space (M i)) (\x. x i) (M i))" + apply (simp add: sets_PiM_single sets_Sup_sigma) + apply (subst SUP_cong[OF refl]) + apply (rule sets_vimage_algebra2) + apply auto [] + apply (auto intro!: arg_cong2[where f=sigma_sets]) + done + +lemma sets_PiM_in_sets: + assumes space: "space N = (\\<^sub>E i\I. space (M i))" + assumes sets: "\i A. i \ I \ A \ sets (M i) \ {x\space N. x i \ A} \ sets N" + shows "sets (\\<^sub>M i \ I. M i) \ sets N" + unfolding sets_PiM_single space[symmetric] + by (intro sets.sigma_sets_subset subsetI) (auto intro: sets) + +lemma sets_PiM_cong: assumes "I = J" "\i. i \ J \ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" + using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) + lemma sets_PiM_I: assumes "finite J" "J \ I" "\i\J. E i \ sets (M i)" shows "prod_emb I M J (PIE j:J. E j) \ sets (PIM i:I. M i)" diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Giry_Monad.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Probability/Giry_Monad.thy Tue Oct 07 10:34:24 2014 +0200 @@ -0,0 +1,868 @@ +(* Title: HOL/Probability/Giry_Monad.thy + Author: Johannes Hölzl, TU München + Author: Manuel Eberl, TU München + +Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability +spaces. +*) + +theory Giry_Monad + imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax" +begin + +section {* Sub-probability spaces *} + +locale subprob_space = finite_measure + + assumes emeasure_space_le_1: "emeasure M (space M) \ 1" + assumes subprob_not_empty: "space M \ {}" + +lemma subprob_spaceI[Pure.intro!]: + assumes *: "emeasure M (space M) \ 1" + assumes "space M \ {}" + shows "subprob_space M" +proof - + interpret finite_measure M + proof + show "emeasure M (space M) \ \" using * by auto + qed + show "subprob_space M" by default fact+ +qed + +lemma prob_space_imp_subprob_space: + "prob_space M \ subprob_space M" + by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty) + +sublocale prob_space \ subprob_space + by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) + +lemma (in subprob_space) subprob_space_distr: + assumes f: "f \ measurable M M'" and "space M' \ {}" shows "subprob_space (distr M M' f)" +proof (rule subprob_spaceI) + have "f -` space M' \ space M = space M" using f by (auto dest: measurable_space) + with f show "emeasure (distr M M' f) (space (distr M M' f)) \ 1" + by (auto simp: emeasure_distr emeasure_space_le_1) + show "space (distr M M' f) \ {}" by (simp add: assms) +qed + +lemma (in subprob_space) subprob_measure_le_1: "emeasure M X \ 1" + by (rule order.trans[OF emeasure_space emeasure_space_le_1]) + +locale pair_subprob_space = + pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2 + +sublocale pair_subprob_space \ P: subprob_space "M1 \\<^sub>M M2" +proof + have "\a b. \a \ 0; b \ 0; a \ 1; b \ 1\ \ a * b \ (1::ereal)" + by (metis comm_monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono) + from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1] + show "emeasure (M1 \\<^sub>M M2) (space (M1 \\<^sub>M M2)) \ 1" + by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg) + from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \\<^sub>M M2) \ {}" + by (simp add: space_pair_measure) +qed + +definition subprob_algebra :: "'a measure \ 'a measure measure" where + "subprob_algebra K = + (\\<^sub>\ A\sets K. vimage_algebra {M. subprob_space M \ sets M = sets K} (\M. emeasure M A) borel)" + +lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \ sets M = sets A}" + by (auto simp add: subprob_algebra_def space_Sup_sigma) + +lemma subprob_algebra_cong: "sets M = sets N \ subprob_algebra M = subprob_algebra N" + by (simp add: subprob_algebra_def) + +lemma measurable_emeasure_subprob_algebra[measurable]: + "a \ sets A \ (\M. emeasure M a) \ borel_measurable (subprob_algebra A)" + by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def) + +context + fixes K M N assumes K: "K \ measurable M (subprob_algebra N)" +begin + +lemma subprob_space_kernel: "a \ space M \ subprob_space (K a)" + using measurable_space[OF K] by (simp add: space_subprob_algebra) + +lemma sets_kernel: "a \ space M \ sets (K a) = sets N" + using measurable_space[OF K] by (simp add: space_subprob_algebra) + +lemma measurable_emeasure_kernel[measurable]: + "A \ sets N \ (\a. emeasure (K a) A) \ borel_measurable M" + using measurable_compose[OF K measurable_emeasure_subprob_algebra] . + +end + +lemma measurable_subprob_algebra: + "(\a. a \ space M \ subprob_space (K a)) \ + (\a. a \ space M \ sets (K a) = sets N) \ + (\A. A \ sets N \ (\a. emeasure (K a) A) \ borel_measurable M) \ + K \ measurable M (subprob_algebra N)" + by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def) + +lemma space_subprob_algebra_empty_iff: + "space (subprob_algebra N) = {} \ space N = {}" +proof + have "\x. x \ space N \ density N (\_. 0) \ space (subprob_algebra N)" + by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI) + then show "space (subprob_algebra N) = {} \ space N = {}" + by auto +next + assume "space N = {}" + hence "sets N = {{}}" by (simp add: space_empty_iff) + moreover have "\M. subprob_space M \ sets M \ {{}}" + by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric]) + ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra) +qed + +lemma measurable_distr: + assumes [measurable]: "f \ measurable M N" + shows "(\M'. distr M' N f) \ measurable (subprob_algebra M) (subprob_algebra N)" +proof (cases "space N = {}") + assume not_empty: "space N \ {}" + show ?thesis + proof (rule measurable_subprob_algebra) + fix A assume A: "A \ sets N" + then have "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M) \ + (\M'. emeasure M' (f -` A \ space M)) \ borel_measurable (subprob_algebra M)" + by (intro measurable_cong) + (auto simp: emeasure_distr space_subprob_algebra dest: sets_eq_imp_space_eq cong: measurable_cong) + also have "\" + using A by (intro measurable_emeasure_subprob_algebra) simp + finally show "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M)" . + qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty) +qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) + +section {* Properties of return *} + +definition return :: "'a measure \ 'a \ 'a measure" where + "return R x = measure_of (space R) (sets R) (\A. indicator A x)" + +lemma space_return[simp]: "space (return M x) = space M" + by (simp add: return_def) + +lemma sets_return[simp]: "sets (return M x) = sets M" + by (simp add: return_def) + +lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L" + by (simp cong: measurable_cong_sets) + +lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N" + by (simp cong: measurable_cong_sets) + +lemma emeasure_return[simp]: + assumes "A \ sets M" + shows "emeasure (return M x) A = indicator A x" +proof (rule emeasure_measure_of[OF return_def]) + show "sets M \ Pow (space M)" by (rule sets.space_closed) + show "positive (sets (return M x)) (\A. indicator A x)" by (simp add: positive_def) + from assms show "A \ sets (return M x)" unfolding return_def by simp + show "countably_additive (sets (return M x)) (\A. indicator A x)" + by (auto intro: countably_additiveI simp: suminf_indicator) +qed + +lemma prob_space_return: "x \ space M \ prob_space (return M x)" + by rule simp + +lemma subprob_space_return: "x \ space M \ subprob_space (return M x)" + by (intro prob_space_return prob_space_imp_subprob_space) + +lemma AE_return: + assumes [simp]: "x \ space M" and [measurable]: "Measurable.pred M P" + shows "(AE y in return M x. P y) \ P x" +proof - + have "(AE y in return M x. y \ {x\space M. \ P x}) \ P x" + by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator) + also have "(AE y in return M x. y \ {x\space M. \ P x}) \ (AE y in return M x. P y)" + by (rule AE_cong) auto + finally show ?thesis . +qed + +lemma nn_integral_return: + assumes "g x \ 0" "x \ space M" "g \ borel_measurable M" + shows "(\\<^sup>+ a. g a \return M x) = g x" +proof- + interpret prob_space "return M x" by (rule prob_space_return[OF `x \ space M`]) + have "(\\<^sup>+ a. g a \return M x) = (\\<^sup>+ a. g x \return M x)" using assms + by (intro nn_integral_cong_AE) (auto simp: AE_return) + also have "... = g x" + using nn_integral_const[OF `g x \ 0`, of "return M x"] emeasure_space_1 by simp + finally show ?thesis . +qed + +lemma return_measurable: "return N \ measurable N (subprob_algebra N)" + by (rule measurable_subprob_algebra) (auto simp: subprob_space_return) + +lemma distr_return: + assumes "f \ measurable M N" and "x \ space M" + shows "distr (return M x) N f = return N (f x)" + using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr) + +definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))" + +lemma select_sets1: + "sets M = sets (subprob_algebra N) \ sets M = sets (subprob_algebra (select_sets M))" + unfolding select_sets_def by (rule someI) + +lemma sets_select_sets[simp]: + assumes sets: "sets M = sets (subprob_algebra N)" + shows "sets (select_sets M) = sets N" + unfolding select_sets_def +proof (rule someI2) + show "sets M = sets (subprob_algebra N)" + by fact +next + fix L assume "sets M = sets (subprob_algebra L)" + with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)" + by (intro sets_eq_imp_space_eq) simp + show "sets L = sets N" + proof cases + assume "space (subprob_algebra N) = {}" + with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L] + show ?thesis + by (simp add: eq space_empty_iff) + next + assume "space (subprob_algebra N) \ {}" + with eq show ?thesis + by (fastforce simp add: space_subprob_algebra) + qed +qed + +lemma space_select_sets[simp]: + "sets M = sets (subprob_algebra N) \ space (select_sets M) = space N" + by (intro sets_eq_imp_space_eq sets_select_sets) + +section {* Join *} + +definition join :: "'a measure measure \ 'a measure" where + "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\B. \\<^sup>+ M'. emeasure M' B \M)" + +lemma + shows space_join[simp]: "space (join M) = space (select_sets M)" + and sets_join[simp]: "sets (join M) = sets (select_sets M)" + by (simp_all add: join_def) + +lemma emeasure_join: + assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \ sets N" + shows "emeasure (join M) A = (\\<^sup>+ M'. emeasure M' A \M)" +proof (rule emeasure_measure_of[OF join_def]) + have eq: "borel_measurable M = borel_measurable (subprob_algebra N)" + by auto + show "countably_additive (sets (join M)) (\B. \\<^sup>+ M'. emeasure M' B \M)" + proof (rule countably_additiveI) + fix A :: "nat \ 'a set" assume A: "range A \ sets (join M)" "disjoint_family A" + have "(\i. \\<^sup>+ M'. emeasure M' (A i) \M) = (\\<^sup>+M'. (\i. emeasure M' (A i)) \M)" + using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq) + also have "\ = (\\<^sup>+M'. emeasure M' (\i. A i) \M)" + proof (rule nn_integral_cong) + fix M' assume "M' \ space M" + then show "(\i. emeasure M' (A i)) = emeasure M' (\i. A i)" + using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra) + qed + finally show "(\i. \\<^sup>+M'. emeasure M' (A i) \M) = (\\<^sup>+M'. emeasure M' (\i. A i) \M)" . + qed +qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg) + +lemma nn_integral_measurable_subprob_algebra: + assumes f: "f \ borel_measurable N" "\x. 0 \ f x" + shows "(\M. integral\<^sup>N M f) \ borel_measurable (subprob_algebra N)" (is "_ \ ?B") + using f +proof induct + case (cong f g) + moreover have "(\M'. \\<^sup>+M''. f M'' \M') \ ?B \ (\M'. \\<^sup>+M''. g M'' \M') \ ?B" + by (intro measurable_cong nn_integral_cong cong) + (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) + ultimately show ?case by simp +next + case (set B) + moreover then have "(\M'. \\<^sup>+M''. indicator B M'' \M') \ ?B \ (\M'. emeasure M' B) \ ?B" + by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra) + ultimately show ?case + by (simp add: measurable_emeasure_subprob_algebra) +next + case (mult f c) + moreover then have "(\M'. \\<^sup>+M''. c * f M'' \M') \ ?B \ (\M'. c * \\<^sup>+M''. f M'' \M') \ ?B" + by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra) + ultimately show ?case + by simp +next + case (add f g) + moreover then have "(\M'. \\<^sup>+M''. f M'' + g M'' \M') \ ?B \ (\M'. (\\<^sup>+M''. f M'' \M') + (\\<^sup>+M''. g M'' \M')) \ ?B" + by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra) + ultimately show ?case + by (simp add: ac_simps) +next + case (seq F) + moreover then have "(\M'. \\<^sup>+M''. (SUP i. F i) M'' \M') \ ?B \ (\M'. SUP i. (\\<^sup>+M''. F i M'' \M')) \ ?B" + unfolding SUP_apply + by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra) + ultimately show ?case + by (simp add: ac_simps) +qed + + +lemma measurable_join: + "join \ measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)" +proof (cases "space N \ {}", rule measurable_subprob_algebra) + fix A assume "A \ sets N" + let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))" + have "(\M'. emeasure (join M') A) \ ?B \ (\M'. (\\<^sup>+ M''. emeasure M'' A \M')) \ ?B" + proof (rule measurable_cong) + fix M' assume "M' \ space (subprob_algebra (subprob_algebra N))" + then show "emeasure (join M') A = (\\<^sup>+ M''. emeasure M'' A \M')" + by (intro emeasure_join) (auto simp: space_subprob_algebra `A\sets N`) + qed + also have "(\M'. \\<^sup>+M''. emeasure M'' A \M') \ ?B" + using measurable_emeasure_subprob_algebra[OF `A\sets N`] emeasure_nonneg[of _ A] + by (rule nn_integral_measurable_subprob_algebra) + finally show "(\M'. emeasure (join M') A) \ borel_measurable (subprob_algebra (subprob_algebra N))" . +next + assume [simp]: "space N \ {}" + fix M assume M: "M \ space (subprob_algebra (subprob_algebra N))" + then have "(\\<^sup>+M'. emeasure M' (space N) \M) \ (\\<^sup>+M'. 1 \M)" + apply (intro nn_integral_mono) + apply (auto simp: space_subprob_algebra + dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) + done + with M show "subprob_space (join M)" + by (intro subprob_spaceI) + (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1) +next + assume "\(space N \ {})" + thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff) +qed (auto simp: space_subprob_algebra) + +lemma nn_integral_join: + assumes f: "f \ borel_measurable N" "\x. 0 \ f x" and M: "sets M = sets (subprob_algebra N)" + shows "(\\<^sup>+x. f x \join M) = (\\<^sup>+M'. \\<^sup>+x. f x \M' \M)" + using f +proof induct + case (cong f g) + moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g" + by (intro nn_integral_cong cong) (simp add: M) + moreover from M have "(\\<^sup>+ M'. integral\<^sup>N M' f \M) = (\\<^sup>+ M'. integral\<^sup>N M' g \M)" + by (intro nn_integral_cong cong) + (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) + ultimately show ?case + by simp +next + case (set A) + moreover with M have "(\\<^sup>+ M'. integral\<^sup>N M' (indicator A) \M) = (\\<^sup>+ M'. emeasure M' A \M)" + by (intro nn_integral_cong nn_integral_indicator) + (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) + ultimately show ?case + using M by (simp add: emeasure_join) +next + case (mult f c) + have "(\\<^sup>+ M'. \\<^sup>+ x. c * f x \M' \M) = (\\<^sup>+ M'. c * \\<^sup>+ x. f x \M' \M)" + using mult M + by (intro nn_integral_cong nn_integral_cmult) + (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq) + also have "\ = c * (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)" + using nn_integral_measurable_subprob_algebra[OF mult(3,4)] + by (intro nn_integral_cmult mult) (simp add: M) + also have "\ = c * (integral\<^sup>N (join M) f)" + by (simp add: mult) + also have "\ = (\\<^sup>+ x. c * f x \join M)" + using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M) + finally show ?case by simp +next + case (add f g) + have "(\\<^sup>+ M'. \\<^sup>+ x. f x + g x \M' \M) = (\\<^sup>+ M'. (\\<^sup>+ x. f x \M') + (\\<^sup>+ x. g x \M') \M)" + using add M + by (intro nn_integral_cong nn_integral_add) + (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq) + also have "\ = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) + (\\<^sup>+ M'. \\<^sup>+ x. g x \M' \M)" + using nn_integral_measurable_subprob_algebra[OF add(1,2)] + using nn_integral_measurable_subprob_algebra[OF add(5,6)] + by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg) + also have "\ = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)" + by (simp add: add) + also have "\ = (\\<^sup>+ x. f x + g x \join M)" + using add by (intro nn_integral_add[symmetric] add) (simp_all add: M) + finally show ?case by (simp add: ac_simps) +next + case (seq F) + have "(\\<^sup>+ M'. \\<^sup>+ x. (SUP i. F i) x \M' \M) = (\\<^sup>+ M'. (SUP i. \\<^sup>+ x. F i x \M') \M)" + using seq M unfolding SUP_apply + by (intro nn_integral_cong nn_integral_monotone_convergence_SUP) + (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq) + also have "\ = (SUP i. \\<^sup>+ M'. \\<^sup>+ x. F i x \M' \M)" + using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq + by (intro nn_integral_monotone_convergence_SUP) + (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono ) + also have "\ = (SUP i. integral\<^sup>N (join M) (F i))" + by (simp add: seq) + also have "\ = (\\<^sup>+ x. (SUP i. F i x) \join M)" + using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M) + finally show ?case by (simp add: ac_simps) +qed + +lemma join_assoc: + assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))" + shows "join (distr M (subprob_algebra N) join) = join (join M)" +proof (rule measure_eqI) + fix A assume "A \ sets (join (distr M (subprob_algebra N) join))" + then have A: "A \ sets N" by simp + show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A" + using measurable_join[of N] + by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg + sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M] + intro!: nn_integral_cong emeasure_join cong: measurable_cong) +qed (simp add: M) + +lemma join_return: + assumes "sets M = sets N" and "subprob_space M" + shows "join (return (subprob_algebra N) M) = M" + by (rule measure_eqI) + (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra + measurable_emeasure_subprob_algebra nn_integral_return assms) + +lemma join_return': + assumes "sets N = sets M" + shows "join (distr M (subprob_algebra N) (return N)) = M" +apply (rule measure_eqI) +apply (simp add: assms) +apply (subgoal_tac "return N \ measurable M (subprob_algebra N)") +apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) +apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable) +done + +lemma join_distr_distr: + fixes f :: "'a \ 'b" and M :: "'a measure measure" and N :: "'b measure" + assumes "sets M = sets (subprob_algebra R)" and "f \ measurable R N" + shows "join (distr M (subprob_algebra N) (\M. distr M N f)) = distr (join M) N f" (is "?r = ?l") +proof (rule measure_eqI) + fix A assume "A \ sets ?r" + hence A_in_N: "A \ sets N" by simp + + from assms have "f \ measurable (join M) N" + by (simp cong: measurable_cong_sets) + moreover from assms and A_in_N have "f-`A \ space R \ sets R" + by (intro measurable_sets) simp_all + ultimately have "emeasure (distr (join M) N f) A = \\<^sup>+M'. emeasure M' (f-`A \ space R) \M" + by (simp_all add: A_in_N emeasure_distr emeasure_join assms) + + also have "... = \\<^sup>+ x. emeasure (distr x N f) A \M" using A_in_N + proof (intro nn_integral_cong, subst emeasure_distr) + fix M' assume "M' \ space M" + from assms have "space M = space (subprob_algebra R)" + using sets_eq_imp_space_eq by blast + with `M' \ space M` have [simp]: "sets M' = sets R" using space_subprob_algebra by blast + show "f \ measurable M' N" by (simp cong: measurable_cong_sets add: assms) + have "space M' = space R" by (rule sets_eq_imp_space_eq) simp + thus "emeasure M' (f -` A \ space R) = emeasure M' (f -` A \ space M')" by simp + qed + + also have "(\M. distr M N f) \ measurable M (subprob_algebra N)" + by (simp cong: measurable_cong_sets add: assms measurable_distr) + hence "(\\<^sup>+ x. emeasure (distr x N f) A \M) = + emeasure (join (distr M (subprob_algebra N) (\M. distr M N f))) A" + by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra) + finally show "emeasure ?r A = emeasure ?l A" .. +qed simp + +definition bind :: "'a measure \ ('a \ 'b measure) \ 'b measure" where + "bind M f = (if space M = {} then count_space {} else + join (distr M (subprob_algebra (f (SOME x. x \ space M))) f))" + +adhoc_overloading Monad_Syntax.bind bind + +lemma bind_empty: + "space M = {} \ bind M f = count_space {}" + by (simp add: bind_def) + +lemma bind_nonempty: + "space M \ {} \ bind M f = join (distr M (subprob_algebra (f (SOME x. x \ space M))) f)" + by (simp add: bind_def) + +lemma sets_bind_empty: "sets M = {} \ sets (bind M f) = {{}}" + by (auto simp: bind_def) + +lemma space_bind_empty: "space M = {} \ space (bind M f) = {}" + by (simp add: bind_def) + +lemma sets_bind[simp]: + assumes "f \ measurable M (subprob_algebra N)" and "space M \ {}" + shows "sets (bind M f) = sets N" + using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex]) + +lemma space_bind[simp]: + assumes "f \ measurable M (subprob_algebra N)" and "space M \ {}" + shows "space (bind M f) = space N" + using assms by (intro sets_eq_imp_space_eq sets_bind) + +lemma bind_cong: + assumes "\x \ space M. f x = g x" + shows "bind M f = bind M g" +proof (cases "space M = {}") + assume "space M \ {}" + hence "(SOME x. x \ space M) \ space M" by (rule_tac someI_ex) blast + with assms have "f (SOME x. x \ space M) = g (SOME x. x \ space M)" by blast + with `space M \ {}` and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong) +qed (simp add: bind_empty) + +lemma bind_nonempty': + assumes "f \ measurable M (subprob_algebra N)" "x \ space M" + shows "bind M f = join (distr M (subprob_algebra N) f)" + using assms + apply (subst bind_nonempty, blast) + apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast) + apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]]) + done + +lemma bind_nonempty'': + assumes "f \ measurable M (subprob_algebra N)" "space M \ {}" + shows "bind M f = join (distr M (subprob_algebra N) f)" + using assms by (auto intro: bind_nonempty') + +lemma emeasure_bind: + "\space M \ {}; f \ measurable M (subprob_algebra N);X \ sets N\ + \ emeasure (M \= f) X = \\<^sup>+x. emeasure (f x) X \M" + by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra) + +lemma bind_return: + assumes "f \ measurable M (subprob_algebra N)" and "x \ space M" + shows "bind (return M x) f = f x" + using sets_kernel[OF assms] assms + by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty' + cong: subprob_algebra_cong) + +lemma bind_return': + shows "bind M (return M) = M" + by (cases "space M = {}") + (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' + cong: subprob_algebra_cong) + +lemma bind_count_space_singleton: + assumes "subprob_space (f x)" + shows "count_space {x} \= f = f x" +proof- + have A: "\A. A \ {x} \ A = {} \ A = {x}" by auto + have "count_space {x} = return (count_space {x}) x" + by (intro measure_eqI) (auto dest: A) + also have "... \= f = f x" + by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms) + finally show ?thesis . +qed + +lemma emeasure_bind_const: + "space M \ {} \ X \ sets N \ subprob_space N \ + emeasure (M \= (\x. N)) X = emeasure N X * emeasure M (space M)" + by (simp add: bind_nonempty emeasure_join nn_integral_distr + space_subprob_algebra measurable_emeasure_subprob_algebra emeasure_nonneg) + +lemma emeasure_bind_const': + assumes "subprob_space M" "subprob_space N" + shows "emeasure (M \= (\x. N)) X = emeasure N X * emeasure M (space M)" +using assms +proof (case_tac "X \ sets N") + fix X assume "X \ sets N" + thus "emeasure (M \= (\x. N)) X = emeasure N X * emeasure M (space M)" using assms + by (subst emeasure_bind_const) + (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1) +next + fix X assume "X \ sets N" + with assms show "emeasure (M \= (\x. N)) X = emeasure N X * emeasure M (space M)" + by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty + space_subprob_algebra emeasure_notin_sets) +qed + +lemma emeasure_bind_const_prob_space: + assumes "prob_space M" "subprob_space N" + shows "emeasure (M \= (\x. N)) X = emeasure N X" + using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space + prob_space.emeasure_space_1) + +lemma bind_const': "\prob_space M; subprob_space N\ \ M \= (\x. N) = N" + by (intro measure_eqI) + (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space) + +lemma bind_return_distr: + "space M \ {} \ f \ measurable M N \ bind M (return N \ f) = distr M N f" + apply (simp add: bind_nonempty) + apply (subst subprob_algebra_cong) + apply (rule sets_return) + apply (subst distr_distr[symmetric]) + apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') + done + +lemma bind_assoc: + fixes f :: "'a \ 'b measure" and g :: "'b \ 'c measure" + assumes M1: "f \ measurable M (subprob_algebra N)" and M2: "g \ measurable N (subprob_algebra R)" + shows "bind (bind M f) g = bind M (\x. bind (f x) g)" +proof (cases "space M = {}") + assume [simp]: "space M \ {}" + from assms have [simp]: "space N \ {}" "space R \ {}" + by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) + from assms have sets_fx[simp]: "\x. x \ space M \ sets (f x) = sets N" + by (simp add: sets_kernel) + have ex_in: "\A. A \ {} \ \x. x \ A" by blast + note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF `space M \ {}`]]] + sets_kernel[OF M2 someI_ex[OF ex_in[OF `space N \ {}`]]] + note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)] + + have "bind M (\x. bind (f x) g) = + join (distr M (subprob_algebra R) (join \ (\x. (distr x (subprob_algebra R) g)) \ f))" + by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def + cong: subprob_algebra_cong distr_cong) + also have "distr M (subprob_algebra R) (join \ (\x. (distr x (subprob_algebra R) g)) \ f) = + distr (distr (distr M (subprob_algebra N) f) + (subprob_algebra (subprob_algebra R)) + (\x. distr x (subprob_algebra R) g)) + (subprob_algebra R) join" + apply (subst distr_distr, + (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+ + apply (simp add: o_assoc) + done + also have "join ... = bind (bind M f) g" + by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong) + finally show ?thesis .. +qed (simp add: bind_empty) + +lemma emeasure_space_subprob_algebra[measurable]: + "(\a. emeasure a (space a)) \ borel_measurable (subprob_algebra N)" +proof- + have "(\a. emeasure a (space N)) \ borel_measurable (subprob_algebra N)" (is "?f \ ?M") + by (rule measurable_emeasure_subprob_algebra) simp + also have "?f \ ?M \ (\a. emeasure a (space a)) \ ?M" + by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) + finally show ?thesis . +qed + +(* TODO: Rename. This name is too general – Manuel *) +lemma measurable_pair_measure: + assumes f: "f \ measurable M (subprob_algebra N)" + assumes g: "g \ measurable M (subprob_algebra L)" + shows "(\x. f x \\<^sub>M g x) \ measurable M (subprob_algebra (N \\<^sub>M L))" +proof (rule measurable_subprob_algebra) + { fix x assume "x \ space M" + with measurable_space[OF f] measurable_space[OF g] + have fx: "f x \ space (subprob_algebra N)" and gx: "g x \ space (subprob_algebra L)" + by auto + interpret F: subprob_space "f x" + using fx by (simp add: space_subprob_algebra) + interpret G: subprob_space "g x" + using gx by (simp add: space_subprob_algebra) + + interpret pair_subprob_space "f x" "g x" .. + show "subprob_space (f x \\<^sub>M g x)" by unfold_locales + show sets_eq: "sets (f x \\<^sub>M g x) = sets (N \\<^sub>M L)" + using fx gx by (simp add: space_subprob_algebra) + + have 1: "\A B. A \ sets N \ B \ sets L \ emeasure (f x \\<^sub>M g x) (A \ B) = emeasure (f x) A * emeasure (g x) B" + using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) + have "emeasure (f x \\<^sub>M g x) (space (f x \\<^sub>M g x)) = + emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))" + by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure) + hence 2: "\A. A \ sets (N \\<^sub>M L) \ emeasure (f x \\<^sub>M g x) (space N \ space L - A) = + ... - emeasure (f x \\<^sub>M g x) A" + using emeasure_compl[OF _ P.emeasure_finite] + unfolding sets_eq + unfolding sets_eq_imp_space_eq[OF sets_eq] + by (simp add: space_pair_measure G.emeasure_pair_measure_Times) + note 1 2 sets_eq } + note Times = this(1) and Compl = this(2) and sets_eq = this(3) + + fix A assume A: "A \ sets (N \\<^sub>M L)" + show "(\a. emeasure (f a \\<^sub>M g a) A) \ borel_measurable M" + using Int_stable_pair_measure_generator pair_measure_closed A + unfolding sets_pair_measure + proof (induct A rule: sigma_sets_induct_disjoint) + case (basic A) then show ?case + by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong) + (auto intro!: measurable_emeasure_kernel f g) + next + case (compl A) + then have A: "A \ sets (N \\<^sub>M L)" + by (auto simp: sets_pair_measure) + have "(\x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - + emeasure (f x \\<^sub>M g x) A) \ borel_measurable M" (is "?f \ ?M") + using compl(2) f g by measurable + thus ?case by (simp add: Compl A cong: measurable_cong) + next + case (union A) + then have "range A \ sets (N \\<^sub>M L)" "disjoint_family A" + by (auto simp: sets_pair_measure) + then have "(\a. emeasure (f a \\<^sub>M g a) (\i. A i)) \ borel_measurable M \ + (\a. \i. emeasure (f a \\<^sub>M g a) (A i)) \ borel_measurable M" + by (intro measurable_cong suminf_emeasure[symmetric]) + (auto simp: sets_eq) + also have "\" + using union by auto + finally show ?case . + qed simp +qed + +(* TODO: Move *) +lemma measurable_distr2: + assumes f[measurable]: "split f \ measurable (L \\<^sub>M M) N" + assumes g[measurable]: "g \ measurable L (subprob_algebra M)" + shows "(\x. distr (g x) N (f x)) \ measurable L (subprob_algebra N)" +proof - + have "(\x. distr (g x) N (f x)) \ measurable L (subprob_algebra N) + \ (\x. distr (return L x \\<^sub>M g x) N (split f)) \ measurable L (subprob_algebra N)" + proof (rule measurable_cong) + fix x assume x: "x \ space L" + have gx: "g x \ space (subprob_algebra M)" + using measurable_space[OF g x] . + then have [simp]: "sets (g x) = sets M" + by (simp add: space_subprob_algebra) + then have [simp]: "space (g x) = space M" + by (rule sets_eq_imp_space_eq) + let ?R = "return L x" + from measurable_compose_Pair1[OF x f] have f_M': "f x \ measurable M N" + by simp + interpret subprob_space "g x" + using gx by (simp add: space_subprob_algebra) + have space_pair_M'[simp]: "\X. space (X \\<^sub>M g x) = space (X \\<^sub>M M)" + by (simp add: space_pair_measure) + show "distr (g x) N (f x) = distr (?R \\<^sub>M g x) N (split f)" (is "?l = ?r") + proof (rule measure_eqI) + show "sets ?l = sets ?r" + by simp + next + fix A assume "A \ sets ?l" + then have A[measurable]: "A \ sets N" + by simp + then have "emeasure ?r A = emeasure (?R \\<^sub>M g x) ((\(x, y). f x y) -` A \ space (?R \\<^sub>M g x))" + by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets) + also have "\ = (\\<^sup>+M''. emeasure (g x) (f M'' -` A \ space M) \?R)" + apply (subst emeasure_pair_measure_alt) + apply (rule measurable_sets[OF _ A]) + apply (auto simp add: f_M' cong: measurable_cong_sets) + apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"]) + apply (auto simp: space_subprob_algebra space_pair_measure) + done + also have "\ = emeasure (g x) (f x -` A \ space M)" + by (subst nn_integral_return) + (auto simp: x intro!: measurable_emeasure) + also have "\ = emeasure ?l A" + by (simp add: emeasure_distr f_M' cong: measurable_cong_sets) + finally show "emeasure ?l A = emeasure ?r A" .. + qed + qed + also have "\" + apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) + apply (rule return_measurable) + apply measurable + done + finally show ?thesis . +qed + +(* END TODO *) + +lemma measurable_bind': + assumes M1: "f \ measurable M (subprob_algebra N)" and + M2: "split g \ measurable (M \\<^sub>M N) (subprob_algebra R)" + shows "(\x. bind (f x) (g x)) \ measurable M (subprob_algebra R)" +proof (subst measurable_cong) + fix x assume x_in_M: "x \ space M" + with assms have "space (f x) \ {}" + by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty) + moreover from M2 x_in_M have "g x \ measurable (f x) (subprob_algebra R)" + by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl]) + (auto dest: measurable_Pair2) + ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" + by (simp_all add: bind_nonempty'') +next + show "(\w. join (distr (f w) (subprob_algebra R) (g w))) \ measurable M (subprob_algebra R)" + apply (rule measurable_compose[OF _ measurable_join]) + apply (rule measurable_distr2[OF M2 M1]) + done +qed + +lemma measurable_bind: + assumes M1: "f \ measurable M (subprob_algebra N)" and + M2: "(\x. g (fst x) (snd x)) \ measurable (M \\<^sub>M N) (subprob_algebra R)" + shows "(\x. bind (f x) (g x)) \ measurable M (subprob_algebra R)" + using assms by (auto intro: measurable_bind' simp: measurable_split_conv) + +lemma measurable_bind2: + assumes "f \ measurable M (subprob_algebra N)" and "g \ measurable N (subprob_algebra R)" + shows "(\x. bind (f x) g) \ measurable M (subprob_algebra R)" + using assms by (intro measurable_bind' measurable_const) auto + +lemma subprob_space_bind: + assumes "subprob_space M" "f \ measurable M (subprob_algebra N)" + shows "subprob_space (M \= f)" +proof (rule subprob_space_kernel[of "\x. x \= f"]) + show "(\x. x \= f) \ measurable (subprob_algebra M) (subprob_algebra N)" + by (rule measurable_bind, rule measurable_ident_sets, rule refl, + rule measurable_compose[OF measurable_snd assms(2)]) + from assms(1) show "M \ space (subprob_algebra M)" + by (simp add: space_subprob_algebra) +qed + +lemma double_bind_assoc: + assumes Mg: "g \ measurable N (subprob_algebra N')" + assumes Mf: "f \ measurable M (subprob_algebra M')" + assumes Mh: "split h \ measurable (M \\<^sub>M M') N" + shows "do {x \ M; y \ f x; g (h x y)} = do {x \ M; y \ f x; return N (h x y)} \= g" +proof- + have "do {x \ M; y \ f x; return N (h x y)} \= g = + do {x \ M; do {y \ f x; return N (h x y)} \= g}" + using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg + measurable_compose[OF _ return_measurable] simp: measurable_split_conv) + also from Mh have "\x. x \ space M \ h x \ measurable M' N" by measurable + hence "do {x \ M; do {y \ f x; return N (h x y)} \= g} = + do {x \ M; y \ f x; return N (h x y) \= g}" + apply (intro ballI bind_cong bind_assoc) + apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp) + apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg) + done + also have "\x. x \ space M \ space (f x) = space M'" + by (intro sets_eq_imp_space_eq sets_kernel[OF Mf]) + with measurable_space[OF Mh] + have "do {x \ M; y \ f x; return N (h x y) \= g} = do {x \ M; y \ f x; g (h x y)}" + by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure) + finally show ?thesis .. +qed + +section {* Measures are \omega-chain complete partial orders *} + +definition SUP_measure :: "(nat \ 'a measure) \ 'a measure" where + "SUP_measure M = measure_of (\i. space (M i)) (\i. sets (M i)) (\A. SUP i. emeasure (M i) A)" + +lemma + assumes const: "\i j. sets (M i) = sets (M j)" + shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp) + and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st) +proof - + have "(\i. sets (M i)) = sets (M i)" + using const by auto + moreover have "(\i. space (M i)) = space (M i)" + using const[THEN sets_eq_imp_space_eq] by auto + moreover have "\i. sets (M i) \ Pow (space (M i))" + by (auto dest: sets.sets_into_space) + ultimately show ?sp ?st + by (simp_all add: SUP_measure_def) +qed + +lemma emeasure_SUP_measure: + assumes const: "\i j. sets (M i) = sets (M j)" + and mono: "mono (\i. emeasure (M i))" + shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)" +proof cases + assume "A \ sets (SUP_measure M)" + show ?thesis + proof (rule emeasure_measure_of[OF SUP_measure_def]) + show "countably_additive (sets (SUP_measure M)) (\A. SUP i. emeasure (M i) A)" + proof (rule countably_additiveI) + fix A :: "nat \ 'a set" assume "range A \ sets (SUP_measure M)" + then have "\i j. A i \ sets (M j)" + using sets_SUP_measure[of M, OF const] by simp + moreover assume "disjoint_family A" + ultimately show "(\i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\i. A i))" + using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure) + qed + show "positive (sets (SUP_measure M)) (\A. SUP i. emeasure (M i) A)" + by (auto simp: positive_def intro: SUP_upper2) + show "(\i. sets (M i)) \ Pow (\i. space (M i))" + using sets.sets_into_space by auto + qed fact +next + assume "A \ sets (SUP_measure M)" + with sets_SUP_measure[of M, OF const] show ?thesis + by (simp add: emeasure_notin_sets) +qed + +end diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Measure_Space.thy Tue Oct 07 10:34:24 2014 +0200 @@ -1643,6 +1643,10 @@ "X \ A \ infinite X \ emeasure (count_space A) X = \" using emeasure_count_space[of X A] by simp +lemma measure_count_space: "measure (count_space A) X = (if X \ A then card X else 0)" + unfolding measure_def + by (cases "finite X") (simp_all add: emeasure_notin_sets) + lemma emeasure_count_space_eq_0: "emeasure (count_space A) X = 0 \ (X \ A \ X = {})" proof cases @@ -1655,6 +1659,9 @@ qed simp qed (simp add: emeasure_notin_sets) +lemma space_empty: "space M = {} \ M = count_space {}" + by (rule measure_eqI) (simp_all add: space_empty_iff) + lemma null_sets_count_space: "null_sets (count_space A) = { {} }" unfolding null_sets_def by (auto simp add: emeasure_count_space_eq_0) diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Tue Oct 07 10:34:24 2014 +0200 @@ -748,6 +748,9 @@ lemma nn_integral_nonneg: "0 \ integral\<^sup>N M f" by (auto intro!: SUP_upper2[of "\x. 0"] simp: nn_integral_def le_fun_def) +lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \ 0 \ integral\<^sup>N M f = 0" + using nn_integral_nonneg[of M f] by auto + lemma nn_integral_not_MInfty[simp]: "integral\<^sup>N M f \ -\" using nn_integral_nonneg[of M f] by auto @@ -2187,6 +2190,10 @@ using emeasure_uniform_measure[OF emeasure_neq_0_sets[OF A(1)] B] A by (cases "emeasure M A" "emeasure M (A \ B)" rule: ereal2_cases) (simp_all add: measure_def) +lemma AE_uniform_measureI: + "A \ sets M \ (AE x in M. x \ A \ P x) \ (AE x in uniform_measure M A. P x)" + unfolding uniform_measure_def by (auto simp: AE_density) + subsubsection {* Uniform count measure *} definition "uniform_count_measure A = point_measure A (\x. 1 / card A)" diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Probability.thy --- a/src/HOL/Probability/Probability.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Probability.thy Tue Oct 07 10:34:24 2014 +0200 @@ -7,6 +7,7 @@ Distributions Probability_Mass_Function Stream_Space + Giry_Monad begin end diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Tue Oct 07 10:34:24 2014 +0200 @@ -1,20 +1,10 @@ +(* Title: HOL/Probability/Probability_Mass_Function.thy + Author: Johannes Hölzl, TU München *) + theory Probability_Mass_Function imports Probability_Measure begin -lemma sets_Pair: "{x} \ sets M1 \ {y} \ sets M2 \ {(x, y)} \ sets (M1 \\<^sub>M M2)" - using pair_measureI[of "{x}" M1 "{y}" M2] by simp - -lemma finite_subset_card: - assumes X: "infinite X" shows "\A\X. finite A \ card A = n" -proof (induct n) - case (Suc n) then guess A .. note A = this - with X obtain x where "x \ X" "x \ A" - by (metis subset_antisym subset_eq) - with A show ?case - by (intro exI[of _ "insert x A"]) auto -qed (simp cong: conj_cong) - lemma (in prob_space) countable_support: "countable {x. measure M {x} \ 0}" proof - @@ -25,7 +15,7 @@ proof (rule ccontr) fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X") then obtain X where "finite X" "card X = Suc (Suc n)" "X \ ?X" - by (metis finite_subset_card) + by (metis infinite_arbitrarily_large) from this(3) have *: "\x. x \ X \ 1 / Suc n \ ?m x" by (auto simp: inverse_eq_divide) { fix x assume "x \ X" @@ -46,17 +36,10 @@ unfolding * by (intro countable_UN countableI_type countable_finite[OF **]) qed -lemma measure_count_space: "measure (count_space A) X = (if X \ A then card X else 0)" - unfolding measure_def - by (cases "finite X") (simp_all add: emeasure_notin_sets) - typedef 'a pmf = "{M :: 'a measure. prob_space M \ sets M = UNIV \ (AE x in M. measure M {x} \ 0)}" morphisms measure_pmf Abs_pmf - apply (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) - apply (auto intro!: prob_space_uniform_measure simp: measure_count_space) - apply (subst uniform_measure_def) - apply (simp add: AE_density AE_count_space split: split_indicator) - done + by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"]) + (auto intro!: prob_space_uniform_measure AE_uniform_measureI) declare [[coercion measure_pmf]] diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Sigma_Algebra.thy --- a/src/HOL/Probability/Sigma_Algebra.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Oct 07 10:34:24 2014 +0200 @@ -1759,6 +1759,10 @@ lemma in_measure_of[intro, simp]: "M \ Pow \ \ A \ M \ A \ sets (measure_of \ M \)" by auto +lemma space_empty_iff: "space N = {} \ sets N = {{}}" + by (metis Pow_empty Sup_bot_conv(1) cSup_singleton empty_iff + sets.sigma_sets_eq sets.space_closed sigma_sets_top subset_singletonD) + subsubsection {* Constructing simple @{typ "'a measure"} *} lemma emeasure_measure_of: @@ -2154,6 +2158,10 @@ unfolding measurable_def by auto qed +lemma measurable_empty_iff: + "space N = {} \ f \ measurable M N \ space M = {}" + by (auto simp add: measurable_def Pi_iff) + subsubsection {* Extend measure *} definition "extend_measure \ I G \ = diff -r 9d5013661ac6 -r 9c66f7c541fb src/HOL/Probability/Stream_Space.thy --- a/src/HOL/Probability/Stream_Space.thy Mon Oct 06 21:21:46 2014 +0200 +++ b/src/HOL/Probability/Stream_Space.thy Tue Oct 07 10:34:24 2014 +0200 @@ -1,3 +1,6 @@ +(* Title: HOL/Probability/Stream_Space.thy + Author: Johannes Hölzl, TU München *) + theory Stream_Space imports Infinite_Product_Measure @@ -10,15 +13,6 @@ lemma Stream_snth: "(x ## s) !! n = (case n of 0 \ x | Suc n \ s !! n)" by (cases n) simp_all -lemma sets_PiM_cong: assumes "I = J" "\i. i \ J \ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" - using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong) - -lemma nn_integral_le_0[simp]: "integral\<^sup>N M f \ 0 \ integral\<^sup>N M f = 0" - using nn_integral_nonneg[of M f] by auto - -lemma restrict_UNIV: "restrict f UNIV = f" - by (simp add: restrict_def) - definition to_stream :: "(nat \ 'a) \ 'a stream" where "to_stream X = smap X nats"