# HG changeset patch # User Andreas Lochbihler # Date 1429013683 -7200 # Node ID f1a5bcf5658f79d1c879f39b701736eb51db2570 # Parent 14efa7f4ee7b440fdb166d84e77431e1c83788f5 lemmas about integrals over bind and join on measures diff -r 14efa7f4ee7b -r f1a5bcf5658f src/HOL/Probability/Giry_Monad.thy --- a/src/HOL/Probability/Giry_Monad.thy Tue Apr 14 14:13:51 2015 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Tue Apr 14 14:14:43 2015 +0200 @@ -38,6 +38,12 @@ sublocale prob_space \ subprob_space by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) +lemma subprob_space_sigma [simp]: "\ \ {} \ subprob_space (sigma \ X)" +by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) + +lemma subprob_space_null_measure: "space M \ {} \ subprob_space (null_measure M)" +by(simp add: null_measure_def) + 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) @@ -324,6 +330,35 @@ finally show ?thesis . qed +lemma integral_measurable_subprob_algebra: + fixes f :: "_ \ real" + assumes f_measurable [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ \f x\ \ B" + shows "(\M. integral\<^sup>L M f) \ borel_measurable (subprob_algebra N)" +proof - + note [measurable] = nn_integral_measurable_subprob_algebra + have "?thesis \ (\M. real (\\<^sup>+ x. f x \M) - real (\\<^sup>+ x. - f x \M)) \ borel_measurable (subprob_algebra N)" + proof(rule measurable_cong) + fix M + assume "M \ space (subprob_algebra N)" + hence "subprob_space M" and M [measurable_cong]: "sets M = sets N" + by(simp_all add: space_subprob_algebra) + interpret subprob_space M by fact + have "(\\<^sup>+ x. ereal \f x\ \M) \ (\\<^sup>+ x. ereal B \M)" + by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded) + also have "\ = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def) + also have "\ \ ereal (max B 0) * 1" + by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def) + finally have "(\\<^sup>+ x. ereal \f x\ \M) \ \" by(auto simp add: max_def) + then have "integrable M f" using f_measurable + by(auto intro: integrableI_bounded) + thus "(\ x. f x \M) = real (\\<^sup>+ x. f x \M) - real (\\<^sup>+ x. - f x \M)" + by(simp add: real_lebesgue_integral_def) + qed + also have "\" by measurable + finally show ?thesis . +qed + (* TODO: Rename. This name is too general -- Manuel *) lemma measurable_pair_measure: assumes f: "f \ measurable M (subprob_algebra N)" @@ -796,6 +831,163 @@ apply (auto simp: f) done +lemma measurable_join1: + "\ f \ measurable N K; sets M = sets (subprob_algebra N) \ + \ f \ measurable (join M) K" +by(simp add: measurable_def) + +lemma + fixes f :: "_ \ real" + assumes f_measurable [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ \f x\ \ B" + and M [measurable_cong]: "sets M = sets (subprob_algebra N)" + and fin: "finite_measure M" + and M_bounded: "AE M' in M. emeasure M' (space M') \ ereal B'" + shows integrable_join: "integrable (join M) f" (is ?integrable) + and integral_join: "integral\<^sup>L (join M) f = \ M'. integral\<^sup>L M' f \M" (is ?integral) +proof(case_tac [!] "space N = {}") + assume *: "space N = {}" + show ?integrable + using M * by(simp add: real_integrable_def measurable_def nn_integral_empty) + have "(\ M'. integral\<^sup>L M' f \M) = (\ M'. 0 \M)" + proof(rule integral_cong) + fix M' + assume "M' \ space M" + with sets_eq_imp_space_eq[OF M] have "space M' = space N" + by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) + with * show "(\ x. f x \M') = 0" by(simp add: integral_empty) + qed simp + then show ?integral + using M * by(simp add: integral_empty) +next + assume *: "space N \ {}" + + from * have B [simp]: "0 \ B" by(auto dest: f_bounded) + + have [measurable]: "f \ borel_measurable (join M)" using f_measurable M + by(rule measurable_join1) + + { fix f M' + assume [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ f x \ B" + and "M' \ space M" "emeasure M' (space M') \ ereal B'" + have "AE x in M'. ereal (f x) \ ereal B" + proof(rule AE_I2) + fix x + assume "x \ space M'" + with \M' \ space M\ sets_eq_imp_space_eq[OF M] + have "x \ space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) + from f_bounded[OF this] show "ereal (f x) \ ereal B" by simp + qed + then have "(\\<^sup>+ x. ereal (f x) \M') \ (\\<^sup>+ x. ereal B \M')" + by(rule nn_integral_mono_AE) + also have "\ = ereal B * emeasure M' (space M')" by(simp) + also have "\ \ ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp) + also have "\ \ ereal B * ereal \B'\" by(rule ereal_mult_left_mono)(simp_all) + finally have "(\\<^sup>+ x. ereal (f x) \M') \ ereal (B * \B'\)" by simp } + note bounded1 = this + + have bounded: + "\f. \ f \ borel_measurable N; \x. x \ space N \ f x \ B \ + \ (\\<^sup>+ x. ereal (f x) \join M) \ \" + proof - + fix f + assume [measurable]: "f \ borel_measurable N" + and f_bounded: "\x. x \ space N \ f x \ B" + have "(\\<^sup>+ x. ereal (f x) \join M) = (\\<^sup>+ M'. \\<^sup>+ x. ereal (f x) \M' \M)" + by(rule nn_integral_join[OF _ M]) simp + also have "\ \ \\<^sup>+ M'. B * \B'\ \M" + using bounded1[OF \f \ borel_measurable N\ f_bounded] + by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format]) + also have "\ = B * \B'\ * emeasure M (space M)" by simp + also have "\ < \" by(simp add: finite_measure.finite_emeasure_space[OF fin]) + finally show "?thesis f" by simp + qed + have f_pos: "(\\<^sup>+ x. ereal (f x) \join M) \ \" + and f_neg: "(\\<^sup>+ x. ereal (- f x) \join M) \ \" + using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff) + + show ?integrable using f_pos f_neg by(simp add: real_integrable_def) + + note [measurable] = nn_integral_measurable_subprob_algebra + + have "(\\<^sup>+ x. f x \join M) = (\\<^sup>+ x. max 0 (f x) \join M)" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. max 0 (f x) \M' \M" + by(simp add: nn_integral_join[OF _ M]) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. f x \M' \M" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + finally have int_f: "(\\<^sup>+ x. f x \join M) = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)" . + + have "(\\<^sup>+ x. - f x \join M) = (\\<^sup>+ x. max 0 (- f x) \join M)" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. max 0 (- f x) \M' \M" + by(simp add: nn_integral_join[OF _ M]) + also have "\ = \\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M" + by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def) + finally have int_mf: "(\\<^sup>+ x. - f x \join M) = (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M)" . + + have f_pos1: + "\M'. \ M' \ space M; emeasure M' (space M') \ ereal B' \ + \ (\\<^sup>+ x. ereal (f x) \M') \ ereal (B * \B'\)" + using f_measurable by(auto intro!: bounded1 dest: f_bounded) + have "AE M' in M. (\\<^sup>+ x. f x \M') \ \" + using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1) + hence [simp]: "(\\<^sup>+ M'. ereal (real (\\<^sup>+ x. f x \M')) \M) = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)" + by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg) + from f_pos have [simp]: "integrable M (\M'. real (\\<^sup>+ x. f x \M'))" + by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal) + + have f_neg1: + "\M'. \ M' \ space M; emeasure M' (space M') \ ereal B' \ + \ (\\<^sup>+ x. ereal (- f x) \M') \ ereal (B * \B'\)" + using f_measurable by(auto intro!: bounded1 dest: f_bounded) + have "AE M' in M. (\\<^sup>+ x. - f x \M') \ \" + using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1) + hence [simp]: "(\\<^sup>+ M'. ereal (real (\\<^sup>+ x. - f x \M')) \M) = (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M)" + by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg) + from f_neg have [simp]: "integrable M (\M'. real (\\<^sup>+ x. - f x \M'))" + by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal) + + from \?integrable\ + have "ereal (\ x. f x \join M) = (\\<^sup>+ x. f x \join M) - (\\<^sup>+ x. - f x \join M)" + by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1)) + also note int_f + also note int_mf + also have "(\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) - (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M) = + ((\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) - (\\<^sup>+ M'. - \\<^sup>+ x. f x \M' \M)) - + ((\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M) - (\\<^sup>+ M'. - \\<^sup>+ x. - f x \M' \M))" + by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg) + also have "(\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) - (\\<^sup>+ M'. - \\<^sup>+ x. f x \M' \M) = \ M'. real (\\<^sup>+ x. f x \M') \M" + using f_pos + by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric]) + also have "(\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M) - (\\<^sup>+ M'. - \\<^sup>+ x. - f x \M' \M) = \ M'. real (\\<^sup>+ x. - f x \M') \M" + using f_neg + by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric]) + also note ereal_minus(1) + also have "(\ M'. real (\\<^sup>+ x. f x \M') \M) - (\ M'. real (\\<^sup>+ x. - f x \M') \M) = + \M'. real (\\<^sup>+ x. f x \M') - real (\\<^sup>+ x. - f x \M') \M" + by simp + also have "\ = \M'. \ x. f x \M' \M" using _ _ M_bounded + proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format]) + show "(\M'. integral\<^sup>L M' f) \ borel_measurable M" + by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded]) + + fix M' + assume "M' \ space M" "emeasure M' (space M') \ B'" + then interpret finite_measure M' by(auto intro: finite_measureI) + + from \M' \ space M\ sets_eq_imp_space_eq[OF M] + have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra) + hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq) + have "integrable M' f" + by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded) + then show "real (\\<^sup>+ x. f x \M') - real (\\<^sup>+ x. - f x \M') = \ x. f x \M'" + by(simp add: real_lebesgue_integral_def) + qed simp_all + finally show ?integral by simp +qed + lemma join_assoc: assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))" shows "join (distr M (subprob_algebra N) join) = join (join M)" @@ -998,6 +1190,32 @@ by (simp add: space_subprob_algebra) qed +lemma + fixes f :: "_ \ real" + assumes f_measurable [measurable]: "f \ borel_measurable K" + and f_bounded: "\x. x \ space K \ \f x\ \ B" + and N [measurable]: "N \ measurable M (subprob_algebra K)" + and fin: "finite_measure M" + and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \ ereal B'" + shows integrable_bind: "integrable (bind M N) f" (is ?integrable) + and integral_bind: "integral\<^sup>L (bind M N) f = \ x. integral\<^sup>L (N x) f \M" (is ?integral) +proof(case_tac [!] "space M = {}") + assume [simp]: "space M \ {}" + interpret finite_measure M by(rule fin) + + have "integrable (join (distr M (subprob_algebra K) N)) f" + using f_measurable f_bounded + by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) + then show ?integrable by(simp add: bind_nonempty''[where N=K]) + + have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \ M'. integral\<^sup>L M' f \distr M (subprob_algebra K) N" + using f_measurable f_bounded + by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) + also have "\ = \ x. integral\<^sup>L (N x) f \M" + by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _ f_bounded]) + finally show ?integral by(simp add: bind_nonempty''[where N=K]) +qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite integral_empty) + lemma (in prob_space) prob_space_bind: assumes ae: "AE x in M. prob_space (N x)" and N[measurable]: "N \ measurable M (subprob_algebra S)" @@ -1142,6 +1360,38 @@ done qed +lemma bind_restrict_space: + assumes A: "A \ space M \ {}" "A \ space M \ sets M" + and f: "f \ measurable (restrict_space M A) (subprob_algebra N)" + shows "restrict_space M A \= f = M \= (\x. if x \ A then f x else null_measure (f (SOME x. x \ A \ x \ space M)))" + (is "?lhs = ?rhs" is "_ = M \= ?f") +proof - + let ?P = "\x. x \ A \ x \ space M" + let ?x = "Eps ?P" + let ?c = "null_measure (f ?x)" + from A have "?P ?x" by-(rule someI_ex, blast) + hence "?x \ space (restrict_space M A)" by(simp add: space_restrict_space) + with f have "f ?x \ space (subprob_algebra N)" by(rule measurable_space) + hence sps: "subprob_space (f ?x)" + and sets: "sets (f ?x) = sets N" + by(simp_all add: space_subprob_algebra) + have "space (f ?x) \ {}" using sps by(rule subprob_space.subprob_not_empty) + moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets) + ultimately have c: "?c \ space (subprob_algebra N)" + by(simp add: space_subprob_algebra subprob_space_null_measure) + from f A c have f': "?f \ measurable M (subprob_algebra N)" + by(simp add: measurable_restrict_space_iff) + + from A have [simp]: "space M \ {}" by blast + + have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)" + using assms by(simp add: space_restrict_space bind_nonempty'') + also have "\ = join (distr M (subprob_algebra N) ?f)" + by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong) + also have "\ = ?rhs" using f' by(simp add: bind_nonempty'') + finally show ?thesis . +qed + 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)