1(* Title: HOL/Probability/Giry_Monad.thy 2 Author: Johannes H��lzl, TU M��nchen 3 Author: Manuel Eberl, TU M��nchen 4 5Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability 6spaces. 7*) 8 9theory Giry_Monad 10 imports Probability_Measure "HOL-Library.Monad_Syntax" 11begin 12 13section \<open>Sub-probability spaces\<close> 14 15locale subprob_space = finite_measure + 16 assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1" 17 assumes subprob_not_empty: "space M \<noteq> {}" 18 19lemma subprob_spaceI[Pure.intro!]: 20 assumes *: "emeasure M (space M) \<le> 1" 21 assumes "space M \<noteq> {}" 22 shows "subprob_space M" 23proof - 24 interpret finite_measure M 25 proof 26 show "emeasure M (space M) \<noteq> \<infinity>" using * by (auto simp: top_unique) 27 qed 28 show "subprob_space M" by standard fact+ 29qed 30 31lemma (in subprob_space) emeasure_subprob_space_less_top: "emeasure M A \<noteq> top" 32 using emeasure_finite[of A] . 33 34lemma prob_space_imp_subprob_space: 35 "prob_space M \<Longrightarrow> subprob_space M" 36 by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty) 37 38lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M" 39 unfolding subprob_space_def finite_measure_def by simp 40 41sublocale prob_space \<subseteq> subprob_space 42 by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty) 43 44lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)" 45by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv) 46 47lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)" 48by(simp add: null_measure_def) 49 50lemma (in subprob_space) subprob_space_distr: 51 assumes f: "f \<in> measurable M M'" and "space M' \<noteq> {}" shows "subprob_space (distr M M' f)" 52proof (rule subprob_spaceI) 53 have "f -` space M' \<inter> space M = space M" using f by (auto dest: measurable_space) 54 with f show "emeasure (distr M M' f) (space (distr M M' f)) \<le> 1" 55 by (auto simp: emeasure_distr emeasure_space_le_1) 56 show "space (distr M M' f) \<noteq> {}" by (simp add: assms) 57qed 58 59lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1" 60 by (rule order.trans[OF emeasure_space emeasure_space_le_1]) 61 62lemma (in subprob_space) subprob_measure_le_1: "measure M X \<le> 1" 63 using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure) 64 65lemma (in subprob_space) nn_integral_le_const: 66 assumes "0 \<le> c" "AE x in M. f x \<le> c" 67 shows "(\<integral>\<^sup>+x. f x \<partial>M) \<le> c" 68proof - 69 have "(\<integral>\<^sup>+ x. f x \<partial>M) \<le> (\<integral>\<^sup>+ x. c \<partial>M)" 70 by(rule nn_integral_mono_AE) fact 71 also have "\<dots> \<le> c * emeasure M (space M)" 72 using \<open>0 \<le> c\<close> by simp 73 also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule mult_left_mono) 74 finally show ?thesis by simp 75qed 76 77lemma emeasure_density_distr_interval: 78 fixes h :: "real \<Rightarrow> real" and g :: "real \<Rightarrow> real" and g' :: "real \<Rightarrow> real" 79 assumes [simp]: "a \<le> b" 80 assumes Mf[measurable]: "f \<in> borel_measurable borel" 81 assumes Mg[measurable]: "g \<in> borel_measurable borel" 82 assumes Mg'[measurable]: "g' \<in> borel_measurable borel" 83 assumes Mh[measurable]: "h \<in> borel_measurable borel" 84 assumes prob: "subprob_space (density lborel f)" 85 assumes nonnegf: "\<And>x. f x \<ge> 0" 86 assumes derivg: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)" 87 assumes contg': "continuous_on {a..b} g'" 88 assumes mono: "strict_mono_on g {a..b}" and inv: "\<And>x. h x \<in> {a..b} \<Longrightarrow> g (h x) = x" 89 assumes range: "{a..b} \<subseteq> range h" 90 shows "emeasure (distr (density lborel f) lborel h) {a..b} = 91 emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 92proof (cases "a < b") 93 assume "a < b" 94 from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on) 95 from mono have mono': "mono_on g {a..b}" by (rule strict_mono_on_imp_mono_on) 96 from mono' derivg have "\<And>x. x \<in> {a<..<b} \<Longrightarrow> g' x \<ge> 0" 97 by (rule mono_on_imp_deriv_nonneg) auto 98 from contg' this have derivg_nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0" 99 by (rule continuous_ge_on_Ioo) (simp_all add: \<open>a < b\<close>) 100 101 from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on) 102 have A: "h -` {a..b} = {g a..g b}" 103 proof (intro equalityI subsetI) 104 fix x assume x: "x \<in> h -` {a..b}" 105 hence "g (h x) \<in> {g a..g b}" by (auto intro: mono_onD[OF mono']) 106 with inv and x show "x \<in> {g a..g b}" by simp 107 next 108 fix y assume y: "y \<in> {g a..g b}" 109 with IVT'[OF _ _ _ contg, of y] obtain x where "x \<in> {a..b}" "y = g x" by auto 110 with range and inv show "y \<in> h -` {a..b}" by auto 111 qed 112 113 have prob': "subprob_space (distr (density lborel f) lborel h)" 114 by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh) 115 have B: "emeasure (distr (density lborel f) lborel h) {a..b} = 116 \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel" 117 by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh]) 118 also note A 119 also have "emeasure (distr (density lborel f) lborel h) {a..b} \<le> 1" 120 by (rule subprob_space.subprob_emeasure_le_1) (rule prob') 121 hence "emeasure (distr (density lborel f) lborel h) {a..b} \<noteq> \<infinity>" by (auto simp: top_unique) 122 with assms have "(\<integral>\<^sup>+x. f x * indicator {g a..g b} x \<partial>lborel) = 123 (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)" 124 by (intro nn_integral_substitution_aux) 125 (auto simp: derivg_nonneg A B emeasure_density mult.commute \<open>a < b\<close>) 126 also have "... = emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}" 127 by (simp add: emeasure_density) 128 finally show ?thesis . 129next 130 assume "\<not>a < b" 131 with \<open>a \<le> b\<close> have [simp]: "b = a" by (simp add: not_less del: \<open>a \<le> b\<close>) 132 from inv and range have "h -` {a} = {g a}" by auto 133 thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh]) 134qed 135 136locale pair_subprob_space = 137 pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2 138 139sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2" 140proof 141 from mult_le_one[OF M1.emeasure_space_le_1 _ M2.emeasure_space_le_1] 142 show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1" 143 by (simp add: M2.emeasure_pair_measure_Times space_pair_measure) 144 from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}" 145 by (simp add: space_pair_measure) 146qed 147 148lemma subprob_space_null_measure_iff: 149 "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}" 150 by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty) 151 152lemma subprob_space_restrict_space: 153 assumes M: "subprob_space M" 154 and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}" 155 shows "subprob_space (restrict_space M A)" 156proof(rule subprob_spaceI) 157 have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)" 158 using A by(simp add: emeasure_restrict_space space_restrict_space) 159 also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M) 160 finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" . 161next 162 show "space (restrict_space M A) \<noteq> {}" 163 using A by(simp add: space_restrict_space) 164qed 165 166definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where 167 "subprob_algebra K = 168 (SUP A \<in> sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)" 169 170lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}" 171 by (auto simp add: subprob_algebra_def space_Sup_eq_UN) 172 173lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N" 174 by (simp add: subprob_algebra_def) 175 176lemma measurable_emeasure_subprob_algebra[measurable]: 177 "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)" 178 by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: subprob_algebra_def) 179 180lemma measurable_measure_subprob_algebra[measurable]: 181 "a \<in> sets A \<Longrightarrow> (\<lambda>M. measure M a) \<in> borel_measurable (subprob_algebra A)" 182 unfolding measure_def by measurable 183 184lemma subprob_measurableD: 185 assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M" 186 shows "space (N x) = space S" 187 and "sets (N x) = sets S" 188 and "measurable (N x) K = measurable S K" 189 and "measurable K (N x) = measurable K S" 190 using measurable_space[OF N x] 191 by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq) 192 193ML \<open> 194 195fun subprob_cong thm ctxt = ( 196 let 197 val thm' = Thm.transfer' ctxt thm 198 val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |> 199 dest_comb |> snd |> strip_abs_body |> head_of |> is_Free 200 in 201 if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt) 202 else ([], ctxt) 203 end 204 handle THM _ => ([], ctxt) | TERM _ => ([], ctxt)) 205 206\<close> 207 208setup \<open> 209 Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong) 210\<close> 211 212context 213 fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)" 214begin 215 216lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)" 217 using measurable_space[OF K] by (simp add: space_subprob_algebra) 218 219lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N" 220 using measurable_space[OF K] by (simp add: space_subprob_algebra) 221 222lemma measurable_emeasure_kernel[measurable]: 223 "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M" 224 using measurable_compose[OF K measurable_emeasure_subprob_algebra] . 225 226end 227 228lemma measurable_subprob_algebra: 229 "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow> 230 (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow> 231 (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow> 232 K \<in> measurable M (subprob_algebra N)" 233 by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: subprob_algebra_def) 234 235lemma measurable_submarkov: 236 "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow> 237 (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 238 (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)" 239proof 240 assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 241 (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)" 242 then show "K \<in> measurable M (subprob_algebra M)" 243 by (intro measurable_subprob_algebra) auto 244next 245 assume "K \<in> measurable M (subprob_algebra M)" 246 then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and> 247 (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)" 248 by (auto dest: subprob_space_kernel sets_kernel) 249qed 250 251lemma measurable_subprob_algebra_generated: 252 assumes eq: "sets N = sigma_sets \<Omega> G" and "Int_stable G" "G \<subseteq> Pow \<Omega>" 253 assumes subsp: "\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)" 254 assumes sets: "\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N" 255 assumes "\<And>A. A \<in> G \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M" 256 assumes \<Omega>: "(\<lambda>a. emeasure (K a) \<Omega>) \<in> borel_measurable M" 257 shows "K \<in> measurable M (subprob_algebra N)" 258proof (rule measurable_subprob_algebra) 259 fix a assume "a \<in> space M" then show "subprob_space (K a)" "sets (K a) = sets N" by fact+ 260next 261 interpret G: sigma_algebra \<Omega> "sigma_sets \<Omega> G" 262 using \<open>G \<subseteq> Pow \<Omega>\<close> by (rule sigma_algebra_sigma_sets) 263 fix A assume "A \<in> sets N" with assms(2,3) show "(\<lambda>a. emeasure (K a) A) \<in> borel_measurable M" 264 unfolding \<open>sets N = sigma_sets \<Omega> G\<close> 265 proof (induction rule: sigma_sets_induct_disjoint) 266 case (basic A) then show ?case by fact 267 next 268 case empty then show ?case by simp 269 next 270 case (compl A) 271 have "(\<lambda>a. emeasure (K a) (\<Omega> - A)) \<in> borel_measurable M \<longleftrightarrow> 272 (\<lambda>a. emeasure (K a) \<Omega> - emeasure (K a) A) \<in> borel_measurable M" 273 using G.top G.sets_into_space sets eq compl subprob_space.emeasure_subprob_space_less_top[OF subsp] 274 by (intro measurable_cong emeasure_Diff) auto 275 with compl \<Omega> show ?case 276 by simp 277 next 278 case (union F) 279 moreover have "(\<lambda>a. emeasure (K a) (\<Union>i. F i)) \<in> borel_measurable M \<longleftrightarrow> 280 (\<lambda>a. \<Sum>i. emeasure (K a) (F i)) \<in> borel_measurable M" 281 using sets union eq 282 by (intro measurable_cong suminf_emeasure[symmetric]) auto 283 ultimately show ?case 284 by auto 285 qed 286qed 287 288lemma space_subprob_algebra_empty_iff: 289 "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}" 290proof 291 have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)" 292 by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI) 293 then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}" 294 by auto 295next 296 assume "space N = {}" 297 hence "sets N = {{}}" by (simp add: space_empty_iff) 298 moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}" 299 by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric]) 300 ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra) 301qed 302 303lemma nn_integral_measurable_subprob_algebra[measurable]: 304 assumes f: "f \<in> borel_measurable N" 305 shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B") 306 using f 307proof induct 308 case (cong f g) 309 moreover have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. \<integral>\<^sup>+M''. g M'' \<partial>M') \<in> ?B" 310 by (intro measurable_cong nn_integral_cong cong) 311 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 312 ultimately show ?case by simp 313next 314 case (set B) 315 then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B" 316 by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra) 317 with set show ?case 318 by (simp add: measurable_emeasure_subprob_algebra) 319next 320 case (mult f c) 321 then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B" 322 by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 323 with mult show ?case 324 by simp 325next 326 case (add f g) 327 then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B" 328 by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra) 329 with add show ?case 330 by (simp add: ac_simps) 331next 332 case (seq F) 333 then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B" 334 unfolding SUP_apply 335 by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra) 336 with seq show ?case 337 by (simp add: ac_simps) 338qed 339 340lemma measurable_distr: 341 assumes [measurable]: "f \<in> measurable M N" 342 shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" 343proof (cases "space N = {}") 344 assume not_empty: "space N \<noteq> {}" 345 show ?thesis 346 proof (rule measurable_subprob_algebra) 347 fix A assume A: "A \<in> sets N" 348 then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow> 349 (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)" 350 by (intro measurable_cong) 351 (auto simp: emeasure_distr space_subprob_algebra 352 intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="(\<inter>)"]) 353 also have "\<dots>" 354 using A by (intro measurable_emeasure_subprob_algebra) simp 355 finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" . 356 qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets) 357qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) 358 359lemma emeasure_space_subprob_algebra[measurable]: 360 "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)" 361proof- 362 have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M") 363 by (rule measurable_emeasure_subprob_algebra) simp 364 also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M" 365 by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq) 366 finally show ?thesis . 367qed 368 369lemma integrable_measurable_subprob_algebra[measurable]: 370 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 371 assumes [measurable]: "f \<in> borel_measurable N" 372 shows "Measurable.pred (subprob_algebra N) (\<lambda>M. integrable M f)" 373proof (rule measurable_cong[THEN iffD2]) 374 show "M \<in> space (subprob_algebra N) \<Longrightarrow> integrable M f \<longleftrightarrow> (\<integral>\<^sup>+x. norm (f x) \<partial>M) < \<infinity>" for M 375 by (auto simp: space_subprob_algebra integrable_iff_bounded) 376qed measurable 377 378lemma integral_measurable_subprob_algebra[measurable]: 379 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 380 assumes f [measurable]: "f \<in> borel_measurable N" 381 shows "(\<lambda>M. integral\<^sup>L M f) \<in> subprob_algebra N \<rightarrow>\<^sub>M borel" 382proof - 383 from borel_measurable_implies_sequence_metric[OF f, of 0] 384 obtain F where F: "\<And>i. simple_function N (F i)" 385 "\<And>x. x \<in> space N \<Longrightarrow> (\<lambda>i. F i x) \<longlonglongrightarrow> f x" 386 "\<And>i x. x \<in> space N \<Longrightarrow> norm (F i x) \<le> 2 * norm (f x)" 387 unfolding norm_conv_dist by blast 388 389 have [measurable]: "F i \<in> N \<rightarrow>\<^sub>M count_space UNIV" for i 390 using F(1) by (rule measurable_simple_function) 391 392 define F' where [abs_def]: 393 "F' M i = (if integrable M f then integral\<^sup>L M (F i) else 0)" for M i 394 395 have "(\<lambda>M. F' M i) \<in> subprob_algebra N \<rightarrow>\<^sub>M borel" for i 396 proof (rule measurable_cong[THEN iffD2]) 397 fix M assume "M \<in> space (subprob_algebra N)" 398 then have [simp]: "sets M = sets N" "space M = space N" "subprob_space M" 399 by (auto simp: space_subprob_algebra intro!: sets_eq_imp_space_eq) 400 interpret subprob_space M by fact 401 have "F' M i = (if integrable M f then Bochner_Integration.simple_bochner_integral M (F i) else 0)" 402 using F(1) 403 by (subst simple_bochner_integrable_eq_integral) 404 (auto simp: simple_bochner_integrable.simps simple_function_def F'_def) 405 then show "F' M i = (if integrable M f then \<Sum>y\<in>F i ` space N. measure M {x\<in>space N. F i x = y} *\<^sub>R y else 0)" 406 unfolding simple_bochner_integral_def by simp 407 qed measurable 408 moreover 409 have "F' M \<longlonglongrightarrow> integral\<^sup>L M f" if M: "M \<in> space (subprob_algebra N)" for M 410 proof cases 411 from M have [simp]: "sets M = sets N" "space M = space N" 412 by (auto simp: space_subprob_algebra intro!: sets_eq_imp_space_eq) 413 assume "integrable M f" then show ?thesis 414 unfolding F'_def using F(1)[THEN borel_measurable_simple_function] F 415 by (auto intro!: integral_dominated_convergence[where w="\<lambda>x. 2 * norm (f x)"] 416 cong: measurable_cong_sets) 417 qed (auto simp: F'_def not_integrable_integral_eq) 418 ultimately show ?thesis 419 by (rule borel_measurable_LIMSEQ_metric) 420qed 421 422(* TODO: Rename. This name is too general -- Manuel *) 423lemma measurable_pair_measure: 424 assumes f: "f \<in> measurable M (subprob_algebra N)" 425 assumes g: "g \<in> measurable M (subprob_algebra L)" 426 shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))" 427proof (rule measurable_subprob_algebra) 428 { fix x assume "x \<in> space M" 429 with measurable_space[OF f] measurable_space[OF g] 430 have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)" 431 by auto 432 interpret F: subprob_space "f x" 433 using fx by (simp add: space_subprob_algebra) 434 interpret G: subprob_space "g x" 435 using gx by (simp add: space_subprob_algebra) 436 437 interpret pair_subprob_space "f x" "g x" .. 438 show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales 439 show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)" 440 using fx gx by (simp add: space_subprob_algebra) 441 442 have 1: "\<And>A B. A \<in> sets N \<Longrightarrow> B \<in> sets L \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (A \<times> B) = emeasure (f x) A * emeasure (g x) B" 443 using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra) 444 have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) = 445 emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))" 446 by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure) 447 hence 2: "\<And>A. A \<in> sets (N \<Otimes>\<^sub>M L) \<Longrightarrow> emeasure (f x \<Otimes>\<^sub>M g x) (space N \<times> space L - A) = 448 ... - emeasure (f x \<Otimes>\<^sub>M g x) A" 449 using emeasure_compl[simplified, OF _ P.emeasure_finite] 450 unfolding sets_eq 451 unfolding sets_eq_imp_space_eq[OF sets_eq] 452 by (simp add: space_pair_measure G.emeasure_pair_measure_Times) 453 note 1 2 sets_eq } 454 note Times = this(1) and Compl = this(2) and sets_eq = this(3) 455 456 fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)" 457 show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M" 458 using Int_stable_pair_measure_generator pair_measure_closed A 459 unfolding sets_pair_measure 460 proof (induct A rule: sigma_sets_induct_disjoint) 461 case (basic A) then show ?case 462 by (auto intro!: borel_measurable_times_ennreal simp: Times cong: measurable_cong) 463 (auto intro!: measurable_emeasure_kernel f g) 464 next 465 case (compl A) 466 then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)" 467 by (auto simp: sets_pair_measure) 468 have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) - 469 emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M") 470 using compl(2) f g by measurable 471 thus ?case by (simp add: Compl A cong: measurable_cong) 472 next 473 case (union A) 474 then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A" 475 by (auto simp: sets_pair_measure) 476 then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow> 477 (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M" 478 by (intro measurable_cong suminf_emeasure[symmetric]) 479 (auto simp: sets_eq) 480 also have "\<dots>" 481 using union by auto 482 finally show ?case . 483 qed simp 484qed 485 486lemma restrict_space_measurable: 487 assumes X: "X \<noteq> {}" "X \<in> sets K" 488 assumes N: "N \<in> measurable M (subprob_algebra K)" 489 shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))" 490proof (rule measurable_subprob_algebra) 491 fix a assume a: "a \<in> space M" 492 from N[THEN measurable_space, OF this] 493 have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K" 494 by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 495 then interpret subprob_space "N a" 496 by simp 497 show "subprob_space (restrict_space (N a) X)" 498 proof 499 show "space (restrict_space (N a) X) \<noteq> {}" 500 using X by (auto simp add: space_restrict_space) 501 show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1" 502 using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1) 503 qed 504 show "sets (restrict_space (N a) X) = sets (restrict_space K X)" 505 by (intro sets_restrict_space_cong) fact 506next 507 fix A assume A: "A \<in> sets (restrict_space K X)" 508 show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M" 509 proof (subst measurable_cong) 510 fix a assume "a \<in> space M" 511 from N[THEN measurable_space, OF this] 512 have [simp]: "sets (N a) = sets K" "space (N a) = space K" 513 by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 514 show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)" 515 using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps) 516 next 517 show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M" 518 using A X 519 by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra]) 520 (auto simp: sets_restrict_space) 521 qed 522qed 523 524section \<open>Properties of return\<close> 525 526definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where 527 "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)" 528 529lemma space_return[simp]: "space (return M x) = space M" 530 by (simp add: return_def) 531 532lemma sets_return[simp]: "sets (return M x) = sets M" 533 by (simp add: return_def) 534 535lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L" 536 by (simp cong: measurable_cong_sets) 537 538lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N" 539 by (simp cong: measurable_cong_sets) 540 541lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N" 542 by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def) 543 544lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x" 545 by (auto simp add: return_def dest: sets_eq_imp_space_eq) 546 547lemma emeasure_return[simp]: 548 assumes "A \<in> sets M" 549 shows "emeasure (return M x) A = indicator A x" 550proof (rule emeasure_measure_of[OF return_def]) 551 show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed) 552 show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def) 553 from assms show "A \<in> sets (return M x)" unfolding return_def by simp 554 show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)" 555 by (auto intro!: countably_additiveI suminf_indicator) 556qed 557 558lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)" 559 by rule simp 560 561lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)" 562 by (intro prob_space_return prob_space_imp_subprob_space) 563 564lemma subprob_space_return_ne: 565 assumes "space M \<noteq> {}" shows "subprob_space (return M x)" 566proof 567 show "emeasure (return M x) (space (return M x)) \<le> 1" 568 by (subst emeasure_return) (auto split: split_indicator) 569qed (simp, fact) 570 571lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x" 572 unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator) 573 574lemma AE_return: 575 assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P" 576 shows "(AE y in return M x. P y) \<longleftrightarrow> P x" 577proof - 578 have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x" 579 by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator) 580 also have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> (AE y in return M x. P y)" 581 by (rule AE_cong) auto 582 finally show ?thesis . 583qed 584 585lemma nn_integral_return: 586 assumes "x \<in> space M" "g \<in> borel_measurable M" 587 shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x" 588proof- 589 interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>]) 590 have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms 591 by (intro nn_integral_cong_AE) (auto simp: AE_return) 592 also have "... = g x" 593 using nn_integral_const[of "return M x"] emeasure_space_1 by simp 594 finally show ?thesis . 595qed 596 597lemma integral_return: 598 fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}" 599 assumes "x \<in> space M" "g \<in> borel_measurable M" 600 shows "(\<integral>a. g a \<partial>return M x) = g x" 601proof- 602 interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>]) 603 have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms 604 by (intro integral_cong_AE) (auto simp: AE_return) 605 then show ?thesis 606 using prob_space by simp 607qed 608 609lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)" 610 by (rule measurable_subprob_algebra) (auto simp: subprob_space_return) 611 612lemma distr_return: 613 assumes "f \<in> measurable M N" and "x \<in> space M" 614 shows "distr (return M x) N f = return N (f x)" 615 using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr) 616 617lemma return_restrict_space: 618 "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>" 619 by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space) 620 621lemma measurable_distr2: 622 assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N" 623 assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)" 624 shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)" 625proof - 626 have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N) 627 \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)" 628 proof (rule measurable_cong) 629 fix x assume x: "x \<in> space L" 630 have gx: "g x \<in> space (subprob_algebra M)" 631 using measurable_space[OF g x] . 632 then have [simp]: "sets (g x) = sets M" 633 by (simp add: space_subprob_algebra) 634 then have [simp]: "space (g x) = space M" 635 by (rule sets_eq_imp_space_eq) 636 let ?R = "return L x" 637 from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N" 638 by simp 639 interpret subprob_space "g x" 640 using gx by (simp add: space_subprob_algebra) 641 have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)" 642 by (simp add: space_pair_measure) 643 show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r") 644 proof (rule measure_eqI) 645 show "sets ?l = sets ?r" 646 by simp 647 next 648 fix A assume "A \<in> sets ?l" 649 then have A[measurable]: "A \<in> sets N" 650 by simp 651 then have "emeasure ?r A = emeasure (?R \<Otimes>\<^sub>M g x) ((\<lambda>(x, y). f x y) -` A \<inter> space (?R \<Otimes>\<^sub>M g x))" 652 by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets) 653 also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' -` A \<inter> space M) \<partial>?R)" 654 apply (subst emeasure_pair_measure_alt) 655 apply (rule measurable_sets[OF _ A]) 656 apply (auto simp add: f_M' cong: measurable_cong_sets) 657 apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"]) 658 apply (auto simp: space_subprob_algebra space_pair_measure) 659 done 660 also have "\<dots> = emeasure (g x) (f x -` A \<inter> space M)" 661 by (subst nn_integral_return) 662 (auto simp: x intro!: measurable_emeasure) 663 also have "\<dots> = emeasure ?l A" 664 by (simp add: emeasure_distr f_M' cong: measurable_cong_sets) 665 finally show "emeasure ?l A = emeasure ?r A" .. 666 qed 667 qed 668 also have "\<dots>" 669 apply (intro measurable_compose[OF measurable_pair_measure measurable_distr]) 670 apply (rule return_measurable) 671 apply measurable 672 done 673 finally show ?thesis . 674qed 675 676lemma nn_integral_measurable_subprob_algebra2: 677 assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" 678 assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)" 679 shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" 680proof - 681 note nn_integral_measurable_subprob_algebra[measurable] 682 note measurable_distr2[measurable] 683 have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M" 684 by measurable 685 then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M" 686 by (rule measurable_cong[THEN iffD1, rotated]) 687 (simp add: nn_integral_distr) 688qed 689 690lemma emeasure_measurable_subprob_algebra2: 691 assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" 692 assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" 693 shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" 694proof - 695 { fix x assume "x \<in> space M" 696 then have "Pair x -` Sigma (space M) A = A x" 697 by auto 698 with sets_Pair1[OF A, of x] have "A x \<in> sets N" 699 by auto } 700 note ** = this 701 702 have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)" 703 by (auto simp: fun_eq_iff) 704 have "(\<lambda>(x, y). indicator (A x) y::ennreal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" 705 apply measurable 706 apply (subst measurable_cong) 707 apply (rule *) 708 apply (auto simp: space_pair_measure) 709 done 710 then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M" 711 by (intro nn_integral_measurable_subprob_algebra2[where N=N] L) 712 then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M" 713 apply (rule measurable_cong[THEN iffD1, rotated]) 714 apply (rule nn_integral_indicator) 715 apply (simp add: subprob_measurableD[OF L] **) 716 done 717qed 718 719lemma measure_measurable_subprob_algebra2: 720 assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)" 721 assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)" 722 shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M" 723 unfolding measure_def 724 by (intro borel_measurable_enn2real emeasure_measurable_subprob_algebra2[OF assms]) 725 726definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))" 727 728lemma select_sets1: 729 "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))" 730 unfolding select_sets_def by (rule someI) 731 732lemma sets_select_sets[simp]: 733 assumes sets: "sets M = sets (subprob_algebra N)" 734 shows "sets (select_sets M) = sets N" 735 unfolding select_sets_def 736proof (rule someI2) 737 show "sets M = sets (subprob_algebra N)" 738 by fact 739next 740 fix L assume "sets M = sets (subprob_algebra L)" 741 with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)" 742 by (intro sets_eq_imp_space_eq) simp 743 show "sets L = sets N" 744 proof cases 745 assume "space (subprob_algebra N) = {}" 746 with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L] 747 show ?thesis 748 by (simp add: eq space_empty_iff) 749 next 750 assume "space (subprob_algebra N) \<noteq> {}" 751 with eq show ?thesis 752 by (fastforce simp add: space_subprob_algebra) 753 qed 754qed 755 756lemma space_select_sets[simp]: 757 "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N" 758 by (intro sets_eq_imp_space_eq sets_select_sets) 759 760section \<open>Join\<close> 761 762definition join :: "'a measure measure \<Rightarrow> 'a measure" where 763 "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" 764 765lemma 766 shows space_join[simp]: "space (join M) = space (select_sets M)" 767 and sets_join[simp]: "sets (join M) = sets (select_sets M)" 768 by (simp_all add: join_def) 769 770lemma emeasure_join: 771 assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N" 772 shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 773proof (rule emeasure_measure_of[OF join_def]) 774 show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)" 775 proof (rule countably_additiveI) 776 fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A" 777 have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)" 778 using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra) 779 also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" 780 proof (rule nn_integral_cong) 781 fix M' assume "M' \<in> space M" 782 then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)" 783 using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra) 784 qed 785 finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" . 786 qed 787qed (auto simp: A sets.space_closed positive_def) 788 789lemma measurable_join: 790 "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)" 791proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra) 792 fix A assume "A \<in> sets N" 793 let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))" 794 have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B" 795 proof (rule measurable_cong) 796 fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))" 797 then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')" 798 by (intro emeasure_join) (auto simp: space_subprob_algebra \<open>A\<in>sets N\<close>) 799 qed 800 also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B" 801 using measurable_emeasure_subprob_algebra[OF \<open>A\<in>sets N\<close>] 802 by (rule nn_integral_measurable_subprob_algebra) 803 finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" . 804next 805 assume [simp]: "space N \<noteq> {}" 806 fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))" 807 then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)" 808 apply (intro nn_integral_mono) 809 apply (auto simp: space_subprob_algebra 810 dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1) 811 done 812 with M show "subprob_space (join M)" 813 by (intro subprob_spaceI) 814 (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1) 815next 816 assume "\<not>(space N \<noteq> {})" 817 thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff) 818qed (auto simp: space_subprob_algebra) 819 820lemma nn_integral_join: 821 assumes f: "f \<in> borel_measurable N" 822 and M[measurable_cong]: "sets M = sets (subprob_algebra N)" 823 shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)" 824 using f 825proof induct 826 case (cong f g) 827 moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g" 828 by (intro nn_integral_cong cong) (simp add: M) 829 moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)" 830 by (intro nn_integral_cong cong) 831 (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq) 832 ultimately show ?case 833 by simp 834next 835 case (set A) 836 with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)" 837 by (intro nn_integral_cong nn_integral_indicator) 838 (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq) 839 with set show ?case 840 using M by (simp add: emeasure_join) 841next 842 case (mult f c) 843 have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 844 using mult M M[THEN sets_eq_imp_space_eq] 845 by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra) 846 also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 847 using nn_integral_measurable_subprob_algebra[OF mult(2)] 848 by (intro nn_integral_cmult mult) (simp add: M) 849 also have "\<dots> = c * (integral\<^sup>N (join M) f)" 850 by (simp add: mult) 851 also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)" 852 using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets) 853 finally show ?case by simp 854next 855 case (add f g) 856 have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)" 857 using add M M[THEN sets_eq_imp_space_eq] 858 by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra) 859 also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)" 860 using nn_integral_measurable_subprob_algebra[OF add(1)] 861 using nn_integral_measurable_subprob_algebra[OF add(4)] 862 by (intro nn_integral_add add) (simp_all add: M) 863 also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)" 864 by (simp add: add) 865 also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)" 866 using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets) 867 finally show ?case by (simp add: ac_simps) 868next 869 case (seq F) 870 have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)" 871 using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply 872 by (intro nn_integral_cong nn_integral_monotone_convergence_SUP) 873 (auto simp add: space_subprob_algebra) 874 also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)" 875 using nn_integral_measurable_subprob_algebra[OF seq(1)] seq 876 by (intro nn_integral_monotone_convergence_SUP) 877 (simp_all add: M incseq_nn_integral incseq_def le_fun_def nn_integral_mono ) 878 also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))" 879 by (simp add: seq) 880 also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)" 881 using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) 882 (simp_all add: M cong: measurable_cong_sets) 883 finally show ?case by (simp add: ac_simps image_comp) 884qed 885 886lemma measurable_join1: 887 "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk> 888 \<Longrightarrow> f \<in> measurable (join M) K" 889by(simp add: measurable_def) 890 891lemma 892 fixes f :: "_ \<Rightarrow> real" 893 assumes f_measurable [measurable]: "f \<in> borel_measurable N" 894 and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B" 895 and M [measurable_cong]: "sets M = sets (subprob_algebra N)" 896 and fin: "finite_measure M" 897 and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ennreal B'" 898 shows integrable_join: "integrable (join M) f" (is ?integrable) 899 and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral) 900proof(case_tac [!] "space N = {}") 901 assume *: "space N = {}" 902 show ?integrable 903 using M * by(simp add: real_integrable_def measurable_def nn_integral_empty) 904 have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)" 905 proof(rule Bochner_Integration.integral_cong) 906 fix M' 907 assume "M' \<in> space M" 908 with sets_eq_imp_space_eq[OF M] have "space M' = space N" 909 by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 910 with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: Bochner_Integration.integral_empty) 911 qed simp 912 then show ?integral 913 using M * by(simp add: Bochner_Integration.integral_empty) 914next 915 assume *: "space N \<noteq> {}" 916 917 from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded) 918 919 have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M 920 by(rule measurable_join1) 921 922 { fix f M' 923 assume [measurable]: "f \<in> borel_measurable N" 924 and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B" 925 and "M' \<in> space M" "emeasure M' (space M') \<le> ennreal B'" 926 have "AE x in M'. ennreal (f x) \<le> ennreal B" 927 proof(rule AE_I2) 928 fix x 929 assume "x \<in> space M'" 930 with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M] 931 have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq) 932 from f_bounded[OF this] show "ennreal (f x) \<le> ennreal B" by simp 933 qed 934 then have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ennreal B \<partial>M')" 935 by(rule nn_integral_mono_AE) 936 also have "\<dots> = ennreal B * emeasure M' (space M')" by(simp) 937 also have "\<dots> \<le> ennreal B * ennreal B'" by(rule mult_left_mono)(fact, simp) 938 also have "\<dots> \<le> ennreal B * ennreal \<bar>B'\<bar>" by(rule mult_left_mono)(simp_all) 939 finally have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M') \<le> ennreal (B * \<bar>B'\<bar>)" by (simp add: ennreal_mult) } 940 note bounded1 = this 941 942 have bounded: 943 "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk> 944 \<Longrightarrow> (\<integral>\<^sup>+ x. ennreal (f x) \<partial>join M) \<noteq> top" 945 proof - 946 fix f 947 assume [measurable]: "f \<in> borel_measurable N" 948 and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B" 949 have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ennreal (f x) \<partial>M' \<partial>M)" 950 by(rule nn_integral_join[OF _ M]) simp 951 also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M" 952 using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded] 953 by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format]) 954 also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp 955 also have "\<dots> < \<infinity>" 956 using finite_measure.finite_emeasure_space[OF fin] 957 by(simp add: ennreal_mult_less_top less_top) 958 finally show "?thesis f" by simp 959 qed 960 have f_pos: "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>join M) \<noteq> \<infinity>" 961 and f_neg: "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>join M) \<noteq> \<infinity>" 962 using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff) 963 964 show ?integrable using f_pos f_neg by(simp add: real_integrable_def) 965 966 note [measurable] = nn_integral_measurable_subprob_algebra 967 968 have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M" 969 by(simp add: nn_integral_join[OF _ M]) 970 have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" 971 by(simp add: nn_integral_join[OF _ M]) 972 973 have pos_finite: "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>" 974 using AE_space M_bounded 975 proof eventually_elim 976 fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> ennreal B'" 977 then have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M') \<le> ennreal (B * \<bar>B'\<bar>)" 978 using f_measurable by(auto intro!: bounded1 dest: f_bounded) 979 then show "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>M') \<noteq> \<infinity>" 980 by (auto simp: top_unique) 981 qed 982 hence [simp]: "(\<integral>\<^sup>+ M'. ennreal (enn2real (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" 983 by (rule nn_integral_cong_AE[OF AE_mp]) (simp add: less_top) 984 from f_pos have [simp]: "integrable M (\<lambda>M'. enn2real (\<integral>\<^sup>+ x. f x \<partial>M'))" 985 by(simp add: int_f real_integrable_def nn_integral_0_iff_AE[THEN iffD2] ennreal_neg enn2real_nonneg) 986 987 have neg_finite: "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>" 988 using AE_space M_bounded 989 proof eventually_elim 990 fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> ennreal B'" 991 then have "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M') \<le> ennreal (B * \<bar>B'\<bar>)" 992 using f_measurable by(auto intro!: bounded1 dest: f_bounded) 993 then show "(\<integral>\<^sup>+ x. ennreal (- f x) \<partial>M') \<noteq> \<infinity>" 994 by (auto simp: top_unique) 995 qed 996 hence [simp]: "(\<integral>\<^sup>+ M'. ennreal (enn2real (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" 997 by (rule nn_integral_cong_AE[OF AE_mp]) (simp add: less_top) 998 from f_neg have [simp]: "integrable M (\<lambda>M'. enn2real (\<integral>\<^sup>+ x. - f x \<partial>M'))" 999 by(simp add: int_mf real_integrable_def nn_integral_0_iff_AE[THEN iffD2] ennreal_neg enn2real_nonneg) 1000 1001 have "(\<integral> x. f x \<partial>join M) = enn2real (\<integral>\<^sup>+ N. \<integral>\<^sup>+x. f x \<partial>N \<partial>M) - enn2real (\<integral>\<^sup>+ N. \<integral>\<^sup>+x. - f x \<partial>N \<partial>M)" 1002 unfolding real_lebesgue_integral_def[OF \<open>?integrable\<close>] by (simp add: nn_integral_join[OF _ M]) 1003 also have "\<dots> = (\<integral>N. enn2real (\<integral>\<^sup>+x. f x \<partial>N) \<partial>M) - (\<integral>N. enn2real (\<integral>\<^sup>+x. - f x \<partial>N) \<partial>M)" 1004 using pos_finite neg_finite by (subst (1 2) integral_eq_nn_integral) (auto simp: enn2real_nonneg) 1005 also have "\<dots> = (\<integral>N. enn2real (\<integral>\<^sup>+x. f x \<partial>N) - enn2real (\<integral>\<^sup>+x. - f x \<partial>N) \<partial>M)" 1006 by simp 1007 also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" 1008 proof (rule integral_cong_AE) 1009 show "AE x in M. 1010 enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>x) - enn2real (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>x) = integral\<^sup>L x f" 1011 using AE_space M_bounded 1012 proof eventually_elim 1013 fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> B'" 1014 then interpret subprob_space M' 1015 by (auto simp: M[THEN sets_eq_imp_space_eq] space_subprob_algebra) 1016 1017 from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M] 1018 have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra) 1019 hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq) 1020 have "integrable M' f" 1021 by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded) 1022 then show "enn2real (\<integral>\<^sup>+ x. f x \<partial>M') - enn2real (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'" 1023 by(simp add: real_lebesgue_integral_def) 1024 qed 1025 qed simp_all 1026 finally show ?integral by simp 1027qed 1028 1029lemma join_assoc: 1030 assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))" 1031 shows "join (distr M (subprob_algebra N) join) = join (join M)" 1032proof (rule measure_eqI) 1033 fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))" 1034 then have A: "A \<in> sets N" by simp 1035 show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A" 1036 using measurable_join[of N] 1037 by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra 1038 sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M] 1039 intro!: nn_integral_cong emeasure_join) 1040qed (simp add: M) 1041 1042lemma join_return: 1043 assumes "sets M = sets N" and "subprob_space M" 1044 shows "join (return (subprob_algebra N) M) = M" 1045 by (rule measure_eqI) 1046 (simp_all add: emeasure_join space_subprob_algebra 1047 measurable_emeasure_subprob_algebra nn_integral_return assms) 1048 1049lemma join_return': 1050 assumes "sets N = sets M" 1051 shows "join (distr M (subprob_algebra N) (return N)) = M" 1052apply (rule measure_eqI) 1053apply (simp add: assms) 1054apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)") 1055apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms) 1056apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable) 1057done 1058 1059lemma join_distr_distr: 1060 fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure" 1061 assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N" 1062 shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l") 1063proof (rule measure_eqI) 1064 fix A assume "A \<in> sets ?r" 1065 hence A_in_N: "A \<in> sets N" by simp 1066 1067 from assms have "f \<in> measurable (join M) N" 1068 by (simp cong: measurable_cong_sets) 1069 moreover from assms and A_in_N have "f-`A \<inter> space R \<in> sets R" 1070 by (intro measurable_sets) simp_all 1071 ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-`A \<inter> space R) \<partial>M" 1072 by (simp_all add: A_in_N emeasure_distr emeasure_join assms) 1073 1074 also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N 1075 proof (intro nn_integral_cong, subst emeasure_distr) 1076 fix M' assume "M' \<in> space M" 1077 from assms have "space M = space (subprob_algebra R)" 1078 using sets_eq_imp_space_eq by blast 1079 with \<open>M' \<in> space M\<close> have [simp]: "sets M' = sets R" using space_subprob_algebra by blast 1080 show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms) 1081 have "space M' = space R" by (rule sets_eq_imp_space_eq) simp 1082 thus "emeasure M' (f -` A \<inter> space R) = emeasure M' (f -` A \<inter> space M')" by simp 1083 qed 1084 1085 also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)" 1086 by (simp cong: measurable_cong_sets add: assms measurable_distr) 1087 hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) = 1088 emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A" 1089 by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra) 1090 finally show "emeasure ?r A = emeasure ?l A" .. 1091qed simp 1092 1093definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where 1094 "bind M f = (if space M = {} then count_space {} else 1095 join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))" 1096 1097adhoc_overloading Monad_Syntax.bind bind 1098 1099lemma bind_empty: 1100 "space M = {} \<Longrightarrow> bind M f = count_space {}" 1101 by (simp add: bind_def) 1102 1103lemma bind_nonempty: 1104 "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)" 1105 by (simp add: bind_def) 1106 1107lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}" 1108 by (auto simp: bind_def) 1109 1110lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}" 1111 by (simp add: bind_def) 1112 1113lemma sets_bind[simp, measurable_cong]: 1114 assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}" 1115 shows "sets (bind M f) = sets N" 1116 using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq) 1117 1118lemma space_bind[simp]: 1119 assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}" 1120 shows "space (bind M f) = space N" 1121 using assms by (intro sets_eq_imp_space_eq sets_bind) 1122 1123lemma bind_cong_All: 1124 assumes "\<forall>x \<in> space M. f x = g x" 1125 shows "bind M f = bind M g" 1126proof (cases "space M = {}") 1127 assume "space M \<noteq> {}" 1128 hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast 1129 with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast 1130 with \<open>space M \<noteq> {}\<close> and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong) 1131qed (simp add: bind_empty) 1132 1133lemma bind_cong: 1134 "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> f x = g x) \<Longrightarrow> bind M f = bind N g" 1135 using bind_cong_All[of M f g] by auto 1136 1137lemma bind_nonempty': 1138 assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M" 1139 shows "bind M f = join (distr M (subprob_algebra N) f)" 1140 using assms 1141 apply (subst bind_nonempty, blast) 1142 apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast) 1143 apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]]) 1144 done 1145 1146lemma bind_nonempty'': 1147 assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}" 1148 shows "bind M f = join (distr M (subprob_algebra N) f)" 1149 using assms by (auto intro: bind_nonempty') 1150 1151lemma emeasure_bind: 1152 "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk> 1153 \<Longrightarrow> emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" 1154 by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra) 1155 1156lemma nn_integral_bind: 1157 assumes f: "f \<in> borel_measurable B" 1158 assumes N: "N \<in> measurable M (subprob_algebra B)" 1159 shows "(\<integral>\<^sup>+x. f x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)" 1160proof cases 1161 assume M: "space M \<noteq> {}" show ?thesis 1162 unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr] 1163 by (rule nn_integral_distr[OF N]) 1164 (simp add: f nn_integral_measurable_subprob_algebra) 1165qed (simp add: bind_empty space_empty[of M] nn_integral_count_space) 1166 1167lemma AE_bind: 1168 assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)" 1169 assumes P[measurable]: "Measurable.pred B P" 1170 shows "(AE x in M \<bind> N. P x) \<longleftrightarrow> (AE x in M. AE y in N x. P y)" 1171proof cases 1172 assume M: "space M = {}" show ?thesis 1173 unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space) 1174next 1175 assume M: "space M \<noteq> {}" 1176 note sets_kernel[OF N, simp] 1177 have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<bind> N))" 1178 by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator) 1179 1180 have "(AE x in M \<bind> N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0" 1181 by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B] 1182 del: nn_integral_indicator) 1183 also have "\<dots> = (AE x in M. AE y in N x. P y)" 1184 apply (subst nn_integral_0_iff_AE) 1185 apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra]) 1186 apply measurable 1187 apply (intro eventually_subst AE_I2) 1188 apply (auto simp add: subprob_measurableD(1)[OF N] 1189 intro!: AE_iff_measurable[symmetric]) 1190 done 1191 finally show ?thesis . 1192qed 1193 1194lemma measurable_bind': 1195 assumes M1: "f \<in> measurable M (subprob_algebra N)" and 1196 M2: "case_prod g \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" 1197 shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" 1198proof (subst measurable_cong) 1199 fix x assume x_in_M: "x \<in> space M" 1200 with assms have "space (f x) \<noteq> {}" 1201 by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty) 1202 moreover from M2 x_in_M have "g x \<in> measurable (f x) (subprob_algebra R)" 1203 by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl]) 1204 (auto dest: measurable_Pair2) 1205 ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))" 1206 by (simp_all add: bind_nonempty'') 1207next 1208 show "(\<lambda>w. join (distr (f w) (subprob_algebra R) (g w))) \<in> measurable M (subprob_algebra R)" 1209 apply (rule measurable_compose[OF _ measurable_join]) 1210 apply (rule measurable_distr2[OF M2 M1]) 1211 done 1212qed 1213 1214lemma measurable_bind[measurable (raw)]: 1215 assumes M1: "f \<in> measurable M (subprob_algebra N)" and 1216 M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)" 1217 shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)" 1218 using assms by (auto intro: measurable_bind' simp: measurable_split_conv) 1219 1220lemma measurable_bind2: 1221 assumes "f \<in> measurable M (subprob_algebra N)" and "g \<in> measurable N (subprob_algebra R)" 1222 shows "(\<lambda>x. bind (f x) g) \<in> measurable M (subprob_algebra R)" 1223 using assms by (intro measurable_bind' measurable_const) auto 1224 1225lemma subprob_space_bind: 1226 assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)" 1227 shows "subprob_space (M \<bind> f)" 1228proof (rule subprob_space_kernel[of "\<lambda>x. x \<bind> f"]) 1229 show "(\<lambda>x. x \<bind> f) \<in> measurable (subprob_algebra M) (subprob_algebra N)" 1230 by (rule measurable_bind, rule measurable_ident_sets, rule refl, 1231 rule measurable_compose[OF measurable_snd assms(2)]) 1232 from assms(1) show "M \<in> space (subprob_algebra M)" 1233 by (simp add: space_subprob_algebra) 1234qed 1235 1236lemma 1237 fixes f :: "_ \<Rightarrow> real" 1238 assumes f_measurable [measurable]: "f \<in> borel_measurable K" 1239 and f_bounded: "\<And>x. x \<in> space K \<Longrightarrow> \<bar>f x\<bar> \<le> B" 1240 and N [measurable]: "N \<in> measurable M (subprob_algebra K)" 1241 and fin: "finite_measure M" 1242 and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \<le> ennreal B'" 1243 shows integrable_bind: "integrable (bind M N) f" (is ?integrable) 1244 and integral_bind: "integral\<^sup>L (bind M N) f = \<integral> x. integral\<^sup>L (N x) f \<partial>M" (is ?integral) 1245proof(case_tac [!] "space M = {}") 1246 assume [simp]: "space M \<noteq> {}" 1247 interpret finite_measure M by(rule fin) 1248 1249 have "integrable (join (distr M (subprob_algebra K) N)) f" 1250 using f_measurable f_bounded 1251 by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) 1252 then show ?integrable by(simp add: bind_nonempty''[where N=K]) 1253 1254 have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \<integral> M'. integral\<^sup>L M' f \<partial>distr M (subprob_algebra K) N" 1255 using f_measurable f_bounded 1256 by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded) 1257 also have "\<dots> = \<integral> x. integral\<^sup>L (N x) f \<partial>M" 1258 by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _]) 1259 finally show ?integral by(simp add: bind_nonempty''[where N=K]) 1260qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty) 1261 1262lemma (in prob_space) prob_space_bind: 1263 assumes ae: "AE x in M. prob_space (N x)" 1264 and N[measurable]: "N \<in> measurable M (subprob_algebra S)" 1265 shows "prob_space (M \<bind> N)" 1266proof 1267 have "emeasure (M \<bind> N) (space (M \<bind> N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)" 1268 by (subst emeasure_bind[where N=S]) 1269 (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong) 1270 also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)" 1271 using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1) 1272 finally show "emeasure (M \<bind> N) (space (M \<bind> N)) = 1" 1273 by (simp add: emeasure_space_1) 1274qed 1275 1276lemma (in subprob_space) bind_in_space: 1277 "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<bind> A) \<in> space (subprob_algebra N)" 1278 by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind) 1279 unfold_locales 1280 1281lemma (in subprob_space) measure_bind: 1282 assumes f: "f \<in> measurable M (subprob_algebra N)" and X: "X \<in> sets N" 1283 shows "measure (M \<bind> f) X = \<integral>x. measure (f x) X \<partial>M" 1284proof - 1285 interpret Mf: subprob_space "M \<bind> f" 1286 by (rule subprob_space_bind[OF _ f]) unfold_locales 1287 1288 { fix x assume "x \<in> space M" 1289 from f[THEN measurable_space, OF this] interpret subprob_space "f x" 1290 by (simp add: space_subprob_algebra) 1291 have "emeasure (f x) X = ennreal (measure (f x) X)" "measure (f x) X \<le> 1" 1292 by (auto simp: emeasure_eq_measure subprob_measure_le_1) } 1293 note this[simp] 1294 1295 have "emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M" 1296 using subprob_not_empty f X by (rule emeasure_bind) 1297 also have "\<dots> = \<integral>\<^sup>+x. ennreal (measure (f x) X) \<partial>M" 1298 by (intro nn_integral_cong) simp 1299 also have "\<dots> = \<integral>x. measure (f x) X \<partial>M" 1300 by (intro nn_integral_eq_integral integrable_const_bound[where B=1] 1301 measure_measurable_subprob_algebra2[OF _ f] pair_measureI X) 1302 (auto simp: measure_nonneg) 1303 finally show ?thesis 1304 by (simp add: Mf.emeasure_eq_measure measure_nonneg integral_nonneg) 1305qed 1306 1307lemma emeasure_bind_const: 1308 "space M \<noteq> {} \<Longrightarrow> X \<in> sets N \<Longrightarrow> subprob_space N \<Longrightarrow> 1309 emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 1310 by (simp add: bind_nonempty emeasure_join nn_integral_distr 1311 space_subprob_algebra measurable_emeasure_subprob_algebra) 1312 1313lemma emeasure_bind_const': 1314 assumes "subprob_space M" "subprob_space N" 1315 shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 1316using assms 1317proof (case_tac "X \<in> sets N") 1318 fix X assume "X \<in> sets N" 1319 thus "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" using assms 1320 by (subst emeasure_bind_const) 1321 (simp_all add: subprob_space.subprob_not_empty subprob_space.emeasure_space_le_1) 1322next 1323 fix X assume "X \<notin> sets N" 1324 with assms show "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X * emeasure M (space M)" 1325 by (simp add: sets_bind[of _ _ N] subprob_space.subprob_not_empty 1326 space_subprob_algebra emeasure_notin_sets) 1327qed 1328 1329lemma emeasure_bind_const_prob_space: 1330 assumes "prob_space M" "subprob_space N" 1331 shows "emeasure (M \<bind> (\<lambda>x. N)) X = emeasure N X" 1332 using assms by (simp add: emeasure_bind_const' prob_space_imp_subprob_space 1333 prob_space.emeasure_space_1) 1334 1335lemma bind_return: 1336 assumes "f \<in> measurable M (subprob_algebra N)" and "x \<in> space M" 1337 shows "bind (return M x) f = f x" 1338 using sets_kernel[OF assms] assms 1339 by (simp_all add: distr_return join_return subprob_space_kernel bind_nonempty' 1340 cong: subprob_algebra_cong) 1341 1342lemma bind_return': 1343 shows "bind M (return M) = M" 1344 by (cases "space M = {}") 1345 (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 1346 cong: subprob_algebra_cong) 1347 1348lemma distr_bind: 1349 assumes N: "N \<in> measurable M (subprob_algebra K)" "space M \<noteq> {}" 1350 assumes f: "f \<in> measurable K R" 1351 shows "distr (M \<bind> N) R f = (M \<bind> (\<lambda>x. distr (N x) R f))" 1352 unfolding bind_nonempty''[OF N] 1353 apply (subst bind_nonempty''[OF measurable_compose[OF N(1) measurable_distr] N(2)]) 1354 apply (rule f) 1355 apply (simp add: join_distr_distr[OF _ f, symmetric]) 1356 apply (subst distr_distr[OF measurable_distr, OF f N(1)]) 1357 apply (simp add: comp_def) 1358 done 1359 1360lemma bind_distr: 1361 assumes f[measurable]: "f \<in> measurable M X" 1362 assumes N[measurable]: "N \<in> measurable X (subprob_algebra K)" and "space M \<noteq> {}" 1363 shows "(distr M X f \<bind> N) = (M \<bind> (\<lambda>x. N (f x)))" 1364proof - 1365 have "space X \<noteq> {}" "space M \<noteq> {}" 1366 using \<open>space M \<noteq> {}\<close> f[THEN measurable_space] by auto 1367 then show ?thesis 1368 by (simp add: bind_nonempty''[where N=K] distr_distr comp_def) 1369qed 1370 1371lemma bind_count_space_singleton: 1372 assumes "subprob_space (f x)" 1373 shows "count_space {x} \<bind> f = f x" 1374proof- 1375 have A: "\<And>A. A \<subseteq> {x} \<Longrightarrow> A = {} \<or> A = {x}" by auto 1376 have "count_space {x} = return (count_space {x}) x" 1377 by (intro measure_eqI) (auto dest: A) 1378 also have "... \<bind> f = f x" 1379 by (subst bind_return[of _ _ "f x"]) (auto simp: space_subprob_algebra assms) 1380 finally show ?thesis . 1381qed 1382 1383lemma restrict_space_bind: 1384 assumes N: "N \<in> measurable M (subprob_algebra K)" 1385 assumes "space M \<noteq> {}" 1386 assumes X[simp]: "X \<in> sets K" "X \<noteq> {}" 1387 shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)" 1388proof (rule measure_eqI) 1389 note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp] 1390 note N_space = sets_eq_imp_space_eq[OF N_sets, simp] 1391 show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))" 1392 by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]]) 1393 fix A assume "A \<in> sets (restrict_space (M \<bind> N) X)" 1394 with X have "A \<in> sets K" "A \<subseteq> X" 1395 by (auto simp: sets_restrict_space) 1396 then show "emeasure (restrict_space (M \<bind> N) X) A = emeasure (M \<bind> (\<lambda>x. restrict_space (N x) X)) A" 1397 using assms 1398 apply (subst emeasure_restrict_space) 1399 apply (simp_all add: emeasure_bind[OF assms(2,1)]) 1400 apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]]) 1401 apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra 1402 intro!: nn_integral_cong dest!: measurable_space) 1403 done 1404qed 1405 1406lemma bind_restrict_space: 1407 assumes A: "A \<inter> space M \<noteq> {}" "A \<inter> space M \<in> sets M" 1408 and f: "f \<in> measurable (restrict_space M A) (subprob_algebra N)" 1409 shows "restrict_space M A \<bind> f = M \<bind> (\<lambda>x. if x \<in> A then f x else null_measure (f (SOME x. x \<in> A \<and> x \<in> space M)))" 1410 (is "?lhs = ?rhs" is "_ = M \<bind> ?f") 1411proof - 1412 let ?P = "\<lambda>x. x \<in> A \<and> x \<in> space M" 1413 let ?x = "Eps ?P" 1414 let ?c = "null_measure (f ?x)" 1415 from A have "?P ?x" by-(rule someI_ex, blast) 1416 hence "?x \<in> space (restrict_space M A)" by(simp add: space_restrict_space) 1417 with f have "f ?x \<in> space (subprob_algebra N)" by(rule measurable_space) 1418 hence sps: "subprob_space (f ?x)" 1419 and sets: "sets (f ?x) = sets N" 1420 by(simp_all add: space_subprob_algebra) 1421 have "space (f ?x) \<noteq> {}" using sps by(rule subprob_space.subprob_not_empty) 1422 moreover have "sets ?c = sets N" by(simp add: null_measure_def)(simp add: sets) 1423 ultimately have c: "?c \<in> space (subprob_algebra N)" 1424 by(simp add: space_subprob_algebra subprob_space_null_measure) 1425 from f A c have f': "?f \<in> measurable M (subprob_algebra N)" 1426 by(simp add: measurable_restrict_space_iff) 1427 1428 from A have [simp]: "space M \<noteq> {}" by blast 1429 1430 have "?lhs = join (distr (restrict_space M A) (subprob_algebra N) f)" 1431 using assms by(simp add: space_restrict_space bind_nonempty'') 1432 also have "\<dots> = join (distr M (subprob_algebra N) ?f)" 1433 by(rule measure_eqI)(auto simp add: emeasure_join nn_integral_distr nn_integral_restrict_space f f' A intro: nn_integral_cong) 1434 also have "\<dots> = ?rhs" using f' by(simp add: bind_nonempty'') 1435 finally show ?thesis . 1436qed 1437 1438lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<bind> (\<lambda>x. N) = N" 1439 by (intro measure_eqI) 1440 (simp_all add: space_subprob_algebra prob_space.not_empty emeasure_bind_const_prob_space) 1441 1442lemma bind_return_distr: 1443 "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (return N \<circ> f) = distr M N f" 1444 apply (simp add: bind_nonempty) 1445 apply (subst subprob_algebra_cong) 1446 apply (rule sets_return) 1447 apply (subst distr_distr[symmetric]) 1448 apply (auto intro!: return_measurable simp: distr_distr[symmetric] join_return') 1449 done 1450 1451lemma bind_return_distr': 1452 "space M \<noteq> {} \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> bind M (\<lambda>x. return N (f x)) = distr M N f" 1453 using bind_return_distr[of M f N] by (simp add: comp_def) 1454 1455lemma bind_assoc: 1456 fixes f :: "'a \<Rightarrow> 'b measure" and g :: "'b \<Rightarrow> 'c measure" 1457 assumes M1: "f \<in> measurable M (subprob_algebra N)" and M2: "g \<in> measurable N (subprob_algebra R)" 1458 shows "bind (bind M f) g = bind M (\<lambda>x. bind (f x) g)" 1459proof (cases "space M = {}") 1460 assume [simp]: "space M \<noteq> {}" 1461 from assms have [simp]: "space N \<noteq> {}" "space R \<noteq> {}" 1462 by (auto simp: measurable_empty_iff space_subprob_algebra_empty_iff) 1463 from assms have sets_fx[simp]: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" 1464 by (simp add: sets_kernel) 1465 have ex_in: "\<And>A. A \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A" by blast 1466 note sets_some[simp] = sets_kernel[OF M1 someI_ex[OF ex_in[OF \<open>space M \<noteq> {}\<close>]]] 1467 sets_kernel[OF M2 someI_ex[OF ex_in[OF \<open>space N \<noteq> {}\<close>]]] 1468 note space_some[simp] = sets_eq_imp_space_eq[OF this(1)] sets_eq_imp_space_eq[OF this(2)] 1469 1470 have "bind M (\<lambda>x. bind (f x) g) = 1471 join (distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f))" 1472 by (simp add: sets_eq_imp_space_eq[OF sets_fx] bind_nonempty o_def 1473 cong: subprob_algebra_cong distr_cong) 1474 also have "distr M (subprob_algebra R) (join \<circ> (\<lambda>x. (distr x (subprob_algebra R) g)) \<circ> f) = 1475 distr (distr (distr M (subprob_algebra N) f) 1476 (subprob_algebra (subprob_algebra R)) 1477 (\<lambda>x. distr x (subprob_algebra R) g)) 1478 (subprob_algebra R) join" 1479 apply (subst distr_distr, 1480 (blast intro: measurable_comp measurable_distr measurable_join M1 M2)+)+ 1481 apply (simp add: o_assoc) 1482 done 1483 also have "join ... = bind (bind M f) g" 1484 by (simp add: join_assoc join_distr_distr M2 bind_nonempty cong: subprob_algebra_cong) 1485 finally show ?thesis .. 1486qed (simp add: bind_empty) 1487 1488lemma double_bind_assoc: 1489 assumes Mg: "g \<in> measurable N (subprob_algebra N')" 1490 assumes Mf: "f \<in> measurable M (subprob_algebra M')" 1491 assumes Mh: "case_prod h \<in> measurable (M \<Otimes>\<^sub>M M') N" 1492 shows "do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)} = do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g" 1493proof- 1494 have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y)} \<bind> g = 1495 do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g}" 1496 using Mh by (auto intro!: bind_assoc measurable_bind'[OF Mf] Mf Mg 1497 measurable_compose[OF _ return_measurable] simp: measurable_split_conv) 1498 also from Mh have "\<And>x. x \<in> space M \<Longrightarrow> h x \<in> measurable M' N" by measurable 1499 hence "do {x \<leftarrow> M; do {y \<leftarrow> f x; return N (h x y)} \<bind> g} = 1500 do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g}" 1501 apply (intro ballI bind_cong refl bind_assoc) 1502 apply (subst measurable_cong_sets[OF sets_kernel[OF Mf] refl], simp) 1503 apply (rule measurable_compose[OF _ return_measurable], auto intro: Mg) 1504 done 1505 also have "\<And>x. x \<in> space M \<Longrightarrow> space (f x) = space M'" 1506 by (intro sets_eq_imp_space_eq sets_kernel[OF Mf]) 1507 with measurable_space[OF Mh] 1508 have "do {x \<leftarrow> M; y \<leftarrow> f x; return N (h x y) \<bind> g} = do {x \<leftarrow> M; y \<leftarrow> f x; g (h x y)}" 1509 by (intro ballI bind_cong bind_return[OF Mg]) (auto simp: space_pair_measure) 1510 finally show ?thesis .. 1511qed 1512 1513lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)" 1514 by (simp add: space_subprob_algebra) unfold_locales 1515 1516lemma (in pair_prob_space) pair_measure_eq_bind: 1517 "(M1 \<Otimes>\<^sub>M M2) = (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" 1518proof (rule measure_eqI) 1519 have ps_M2: "prob_space M2" by unfold_locales 1520 note return_measurable[measurable] 1521 show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))" 1522 by (simp_all add: M1.not_empty M2.not_empty) 1523 fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)" 1524 show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A" 1525 by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] 1526 intro!: nn_integral_cong) 1527qed 1528 1529lemma (in pair_prob_space) bind_rotate: 1530 assumes C[measurable]: "(\<lambda>(x, y). C x y) \<in> measurable (M1 \<Otimes>\<^sub>M M2) (subprob_algebra N)" 1531 shows "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))" 1532proof - 1533 interpret swap: pair_prob_space M2 M1 by unfold_locales 1534 note measurable_bind[where N="M2", measurable] 1535 note measurable_bind[where N="M1", measurable] 1536 have [simp]: "M1 \<in> space (subprob_algebra M1)" "M2 \<in> space (subprob_algebra M2)" 1537 by (auto simp: space_subprob_algebra) unfold_locales 1538 have "(M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. C x y))) = 1539 (M1 \<bind> (\<lambda>x. M2 \<bind> (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) \<bind> (\<lambda>(x, y). C x y)" 1540 by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M1 \<Otimes>\<^sub>M M2" and R=N]) 1541 also have "\<dots> = (distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))) \<bind> (\<lambda>(x, y). C x y)" 1542 unfolding pair_measure_eq_bind[symmetric] distr_pair_swap[symmetric] .. 1543 also have "\<dots> = (M2 \<bind> (\<lambda>x. M1 \<bind> (\<lambda>y. return (M2 \<Otimes>\<^sub>M M1) (x, y)))) \<bind> (\<lambda>(y, x). C x y)" 1544 unfolding swap.pair_measure_eq_bind[symmetric] 1545 by (auto simp add: space_pair_measure M1.not_empty M2.not_empty bind_distr[OF _ C] intro!: bind_cong) 1546 also have "\<dots> = (M2 \<bind> (\<lambda>y. M1 \<bind> (\<lambda>x. C x y)))" 1547 by (auto intro!: bind_cong simp: bind_return[where N=N] space_pair_measure bind_assoc[where N="M2 \<Otimes>\<^sub>M M1" and R=N]) 1548 finally show ?thesis . 1549qed 1550 1551lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<bind> return N = M" 1552 by (cases "space M = {}") 1553 (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return' 1554 cong: subprob_algebra_cong) 1555 1556lemma (in prob_space) distr_const[simp]: 1557 "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c" 1558 by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1) 1559 1560lemma return_count_space_eq_density: 1561 "return (count_space M) x = density (count_space M) (indicator {x})" 1562 by (rule measure_eqI) 1563 (auto simp: indicator_inter_arith[symmetric] emeasure_density split: split_indicator) 1564 1565lemma null_measure_in_space_subprob_algebra [simp]: 1566 "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}" 1567by(simp add: space_subprob_algebra subprob_space_null_measure_iff) 1568 1569subsection \<open>Giry monad on probability spaces\<close> 1570 1571definition prob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where 1572 "prob_algebra K = restrict_space (subprob_algebra K) {M. prob_space M}" 1573 1574lemma space_prob_algebra: "space (prob_algebra M) = {N. sets N = sets M \<and> prob_space N}" 1575 unfolding prob_algebra_def by (auto simp: space_subprob_algebra space_restrict_space prob_space_imp_subprob_space) 1576 1577lemma measurable_measure_prob_algebra[measurable]: 1578 "a \<in> sets A \<Longrightarrow> (\<lambda>M. Sigma_Algebra.measure M a) \<in> prob_algebra A \<rightarrow>\<^sub>M borel" 1579 unfolding prob_algebra_def by (intro measurable_restrict_space1 measurable_measure_subprob_algebra) 1580 1581lemma measurable_prob_algebraD: 1582 "f \<in> N \<rightarrow>\<^sub>M prob_algebra M \<Longrightarrow> f \<in> N \<rightarrow>\<^sub>M subprob_algebra M" 1583 unfolding prob_algebra_def measurable_restrict_space2_iff by auto 1584 1585lemma measure_measurable_prob_algebra2: 1586 "Sigma (space M) A \<in> sets (M \<Otimes>\<^sub>M N) \<Longrightarrow> L \<in> M \<rightarrow>\<^sub>M prob_algebra N \<Longrightarrow> 1587 (\<lambda>x. Sigma_Algebra.measure (L x) (A x)) \<in> borel_measurable M" 1588 using measure_measurable_subprob_algebra2[of M A N L] by (auto intro: measurable_prob_algebraD) 1589 1590lemma measurable_prob_algebraI: 1591 "(\<And>x. x \<in> space N \<Longrightarrow> prob_space (f x)) \<Longrightarrow> f \<in> N \<rightarrow>\<^sub>M subprob_algebra M \<Longrightarrow> f \<in> N \<rightarrow>\<^sub>M prob_algebra M" 1592 unfolding prob_algebra_def by (intro measurable_restrict_space2) auto 1593 1594lemma measurable_distr_prob_space: 1595 assumes f: "f \<in> M \<rightarrow>\<^sub>M N" 1596 shows "(\<lambda>M'. distr M' N f) \<in> prob_algebra M \<rightarrow>\<^sub>M prob_algebra N" 1597 unfolding prob_algebra_def measurable_restrict_space2_iff 1598proof (intro conjI measurable_restrict_space1 measurable_distr f) 1599 show "(\<lambda>M'. distr M' N f) \<in> space (restrict_space (subprob_algebra M) (Collect prob_space)) \<rightarrow> Collect prob_space" 1600 using f by (auto simp: space_restrict_space space_subprob_algebra intro!: prob_space.prob_space_distr) 1601qed 1602 1603lemma measurable_return_prob_space[measurable]: "return N \<in> N \<rightarrow>\<^sub>M prob_algebra N" 1604 by (rule measurable_prob_algebraI) (auto simp: prob_space_return) 1605 1606lemma measurable_distr_prob_space2[measurable (raw)]: 1607 assumes f: "g \<in> L \<rightarrow>\<^sub>M prob_algebra M" "(\<lambda>(x, y). f x y) \<in> L \<Otimes>\<^sub>M M \<rightarrow>\<^sub>M N" 1608 shows "(\<lambda>x. distr (g x) N (f x)) \<in> L \<rightarrow>\<^sub>M prob_algebra N" 1609 unfolding prob_algebra_def measurable_restrict_space2_iff 1610proof (intro conjI measurable_restrict_space1 measurable_distr2[where M=M] f measurable_prob_algebraD) 1611 show "(\<lambda>x. distr (g x) N (f x)) \<in> space L \<rightarrow> Collect prob_space" 1612 using f subprob_measurableD[OF measurable_prob_algebraD[OF f(1)]] 1613 by (auto simp: measurable_restrict_space2_iff prob_algebra_def 1614 intro!: prob_space.prob_space_distr) 1615qed 1616 1617lemma measurable_bind_prob_space: 1618 assumes f: "f \<in> M \<rightarrow>\<^sub>M prob_algebra N" and g: "g \<in> N \<rightarrow>\<^sub>M prob_algebra R" 1619 shows "(\<lambda>x. bind (f x) g) \<in> M \<rightarrow>\<^sub>M prob_algebra R" 1620 unfolding prob_algebra_def measurable_restrict_space2_iff 1621proof (intro conjI measurable_restrict_space1 measurable_bind2[where N=N] f g measurable_prob_algebraD) 1622 show "(\<lambda>x. f x \<bind> g) \<in> space M \<rightarrow> Collect prob_space" 1623 using g f subprob_measurableD[OF measurable_prob_algebraD[OF f]] 1624 by (auto simp: measurable_restrict_space2_iff prob_algebra_def 1625 intro!: prob_space.prob_space_bind[where S=R] AE_I2) 1626qed 1627 1628lemma measurable_bind_prob_space2[measurable (raw)]: 1629 assumes f: "f \<in> M \<rightarrow>\<^sub>M prob_algebra N" and g: "(\<lambda>(x, y). g x y) \<in> (M \<Otimes>\<^sub>M N) \<rightarrow>\<^sub>M prob_algebra R" 1630 shows "(\<lambda>x. bind (f x) (g x)) \<in> M \<rightarrow>\<^sub>M prob_algebra R" 1631 unfolding prob_algebra_def measurable_restrict_space2_iff 1632proof (intro conjI measurable_restrict_space1 measurable_bind[where N=N] f g measurable_prob_algebraD) 1633 show "(\<lambda>x. f x \<bind> g x) \<in> space M \<rightarrow> Collect prob_space" 1634 using g f subprob_measurableD[OF measurable_prob_algebraD[OF f]] 1635 using measurable_space[OF g] 1636 by (auto simp: measurable_restrict_space2_iff prob_algebra_def space_pair_measure Pi_iff 1637 intro!: prob_space.prob_space_bind[where S=R] AE_I2) 1638qed (insert g, simp) 1639 1640 1641lemma measurable_prob_algebra_generated: 1642 assumes eq: "sets N = sigma_sets \<Omega> G" and "Int_stable G" "G \<subseteq> Pow \<Omega>" 1643 assumes subsp: "\<And>a. a \<in> space M \<Longrightarrow> prob_space (K a)" 1644 assumes sets: "\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N" 1645 assumes "\<And>A. A \<in> G \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M" 1646 shows "K \<in> measurable M (prob_algebra N)" 1647 unfolding measurable_restrict_space2_iff prob_algebra_def 1648proof 1649 show "K \<in> M \<rightarrow>\<^sub>M subprob_algebra N" 1650 proof (rule measurable_subprob_algebra_generated[OF assms(1,2,3) _ assms(5,6)]) 1651 fix a assume "a \<in> space M" then show "subprob_space (K a)" 1652 using subsp[of a] by (intro prob_space_imp_subprob_space) 1653 next 1654 have "(\<lambda>a. emeasure (K a) \<Omega>) \<in> borel_measurable M \<longleftrightarrow> (\<lambda>a. 1::ennreal) \<in> borel_measurable M" 1655 using sets_eq_imp_space_eq[of "sigma \<Omega> G" N] \<open>G \<subseteq> Pow \<Omega>\<close> eq sets_eq_imp_space_eq[OF sets] 1656 prob_space.emeasure_space_1[OF subsp] 1657 by (intro measurable_cong) auto 1658 then show "(\<lambda>a. emeasure (K a) \<Omega>) \<in> borel_measurable M" by simp 1659 qed 1660qed (insert subsp, auto) 1661 1662lemma in_space_prob_algebra: 1663 "x \<in> space (prob_algebra M) \<Longrightarrow> emeasure x (space M) = 1" 1664 unfolding prob_algebra_def space_restrict_space space_subprob_algebra 1665 by (auto dest!: prob_space.emeasure_space_1 sets_eq_imp_space_eq) 1666 1667lemma prob_space_pair: 1668 assumes "prob_space M" "prob_space N" shows "prob_space (M \<Otimes>\<^sub>M N)" 1669proof - 1670 interpret M: prob_space M by fact 1671 interpret N: prob_space N by fact 1672 interpret P: pair_prob_space M N proof qed 1673 show ?thesis 1674 by unfold_locales 1675qed 1676 1677lemma measurable_pair_prob[measurable]: 1678 "f \<in> M \<rightarrow>\<^sub>M prob_algebra N \<Longrightarrow> g \<in> M \<rightarrow>\<^sub>M prob_algebra L \<Longrightarrow> (\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> M \<rightarrow>\<^sub>M prob_algebra (N \<Otimes>\<^sub>M L)" 1679 unfolding prob_algebra_def measurable_restrict_space2_iff 1680 by (auto intro!: measurable_pair_measure prob_space_pair) 1681 1682lemma emeasure_bind_prob_algebra: 1683 assumes A: "A \<in> space (prob_algebra N)" 1684 assumes B: "B \<in> N \<rightarrow>\<^sub>M prob_algebra L" 1685 assumes X: "X \<in> sets L" 1686 shows "emeasure (bind A B) X = (\<integral>\<^sup>+x. emeasure (B x) X \<partial>A)" 1687 using A B 1688 by (intro emeasure_bind[OF _ _ X]) 1689 (auto simp: space_prob_algebra measurable_prob_algebraD cong: measurable_cong_sets intro!: prob_space.not_empty) 1690 1691lemma prob_space_bind': 1692 assumes A: "A \<in> space (prob_algebra M)" and B: "B \<in> M \<rightarrow>\<^sub>M prob_algebra N" shows "prob_space (A \<bind> B)" 1693 using measurable_bind_prob_space[OF measurable_const, OF A B, THEN measurable_space, of undefined "count_space UNIV"] 1694 by (simp add: space_prob_algebra) 1695 1696lemma sets_bind': 1697 assumes A: "A \<in> space (prob_algebra M)" and B: "B \<in> M \<rightarrow>\<^sub>M prob_algebra N" shows "sets (A \<bind> B) = sets N" 1698 using measurable_bind_prob_space[OF measurable_const, OF A B, THEN measurable_space, of undefined "count_space UNIV"] 1699 by (simp add: space_prob_algebra) 1700 1701lemma bind_cong_AE': 1702 assumes M: "M \<in> space (prob_algebra L)" 1703 and f: "f \<in> L \<rightarrow>\<^sub>M prob_algebra N" and g: "g \<in> L \<rightarrow>\<^sub>M prob_algebra N" 1704 and ae: "AE x in M. f x = g x" 1705 shows "bind M f = bind M g" 1706proof (rule measure_eqI) 1707 show "sets (M \<bind> f) = sets (M \<bind> g)" 1708 unfolding sets_bind'[OF M f] sets_bind'[OF M g] .. 1709 show "A \<in> sets (M \<bind> f) \<Longrightarrow> emeasure (M \<bind> f) A = emeasure (M \<bind> g) A" for A 1710 unfolding sets_bind'[OF M f] 1711 using emeasure_bind_prob_algebra[OF M f, of A] emeasure_bind_prob_algebra[OF M g, of A] ae 1712 by (auto intro: nn_integral_cong_AE) 1713qed 1714 1715lemma density_discrete: 1716 "countable A \<Longrightarrow> sets N = Set.Pow A \<Longrightarrow> (\<And>x. f x \<ge> 0) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x = emeasure N {x}) \<Longrightarrow> 1717 density (count_space A) f = N" 1718 by (rule measure_eqI_countable[of _ A]) (auto simp: emeasure_density) 1719 1720lemma distr_density_discrete: 1721 fixes f' 1722 assumes "countable A" 1723 assumes "f' \<in> borel_measurable M" 1724 assumes "g \<in> measurable M (count_space A)" 1725 defines "f \<equiv> \<lambda>x. \<integral>\<^sup>+t. (if g t = x then 1 else 0) * f' t \<partial>M" 1726 assumes "\<And>x. x \<in> space M \<Longrightarrow> g x \<in> A" 1727 shows "density (count_space A) (\<lambda>x. f x) = distr (density M f') (count_space A) g" 1728proof (rule density_discrete) 1729 fix x assume x: "x \<in> A" 1730 have "f x = \<integral>\<^sup>+t. indicator (g -` {x} \<inter> space M) t * f' t \<partial>M" (is "_ = ?I") unfolding f_def 1731 by (intro nn_integral_cong) (simp split: split_indicator) 1732 also from x have in_sets: "g -` {x} \<inter> space M \<in> sets M" 1733 by (intro measurable_sets[OF assms(3)]) simp 1734 have "?I = emeasure (density M f') (g -` {x} \<inter> space M)" unfolding f_def 1735 by (subst emeasure_density[OF assms(2) in_sets], subst mult.commute) (rule refl) 1736 also from assms(3) x have "... = emeasure (distr (density M f') (count_space A) g) {x}" 1737 by (subst emeasure_distr) simp_all 1738 finally show "f x = emeasure (distr (density M f') (count_space A) g) {x}" . 1739qed (insert assms, auto) 1740 1741lemma bind_cong_AE: 1742 assumes "M = N" 1743 assumes f: "f \<in> measurable N (subprob_algebra B)" 1744 assumes g: "g \<in> measurable N (subprob_algebra B)" 1745 assumes ae: "AE x in N. f x = g x" 1746 shows "bind M f = bind N g" 1747proof cases 1748 assume "space N = {}" then show ?thesis 1749 using \<open>M = N\<close> by (simp add: bind_empty) 1750next 1751 assume "space N \<noteq> {}" 1752 show ?thesis unfolding \<open>M = N\<close> 1753 proof (rule measure_eqI) 1754 have *: "sets (N \<bind> f) = sets B" 1755 using sets_bind[OF sets_kernel[OF f] \<open>space N \<noteq> {}\<close>] by simp 1756 then show "sets (N \<bind> f) = sets (N \<bind> g)" 1757 using sets_bind[OF sets_kernel[OF g] \<open>space N \<noteq> {}\<close>] by auto 1758 fix A assume "A \<in> sets (N \<bind> f)" 1759 then have "A \<in> sets B" 1760 unfolding * . 1761 with ae f g \<open>space N \<noteq> {}\<close> show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A" 1762 by (subst (1 2) emeasure_bind[where N=B]) (auto intro!: nn_integral_cong_AE) 1763 qed 1764qed 1765 1766lemma bind_cong_simp: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g" 1767 by (auto simp: simp_implies_def intro!: bind_cong) 1768 1769lemma sets_bind_measurable: 1770 assumes f: "f \<in> measurable M (subprob_algebra B)" 1771 assumes M: "space M \<noteq> {}" 1772 shows "sets (M \<bind> f) = sets B" 1773 using M by (intro sets_bind[OF sets_kernel[OF f]]) auto 1774 1775lemma space_bind_measurable: 1776 assumes f: "f \<in> measurable M (subprob_algebra B)" 1777 assumes M: "space M \<noteq> {}" 1778 shows "space (M \<bind> f) = space B" 1779 using M by (intro space_bind[OF sets_kernel[OF f]]) auto 1780 1781lemma bind_distr_return: 1782 "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> g \<in> N \<rightarrow>\<^sub>M L \<Longrightarrow> space M \<noteq> {} \<Longrightarrow> 1783 distr M N f \<bind> (\<lambda>x. return L (g x)) = distr M L (\<lambda>x. g (f x))" 1784 by (subst bind_distr[OF _ measurable_compose[OF _ return_measurable]]) 1785 (auto intro!: bind_return_distr') 1786 1787end 1788