author wenzelm Fri Aug 18 20:47:47 2017 +0200 (2017-08-18) changeset 66453 cc19f7ca2ed6 parent 64320 ba194424b895 child 67226 ec32cdaab97b permissions -rw-r--r--
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
1 (*  Title:      HOL/Probability/Giry_Monad.thy
2     Author:     Johannes Hölzl, TU München
3     Author:     Manuel Eberl, TU München
5 Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability
6 spaces.
7 *)
10   imports Probability_Measure "HOL-Library.Monad_Syntax"
11 begin
13 section \<open>Sub-probability spaces\<close>
15 locale subprob_space = finite_measure +
16   assumes emeasure_space_le_1: "emeasure M (space M) \<le> 1"
17   assumes subprob_not_empty: "space M \<noteq> {}"
19 lemma subprob_spaceI[Pure.intro!]:
20   assumes *: "emeasure M (space M) \<le> 1"
21   assumes "space M \<noteq> {}"
22   shows "subprob_space M"
23 proof -
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+
29 qed
31 lemma (in subprob_space) emeasure_subprob_space_less_top: "emeasure M A \<noteq> top"
32   using emeasure_finite[of A] .
34 lemma 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)
38 lemma subprob_space_imp_sigma_finite: "subprob_space M \<Longrightarrow> sigma_finite_measure M"
39   unfolding subprob_space_def finite_measure_def by simp
41 sublocale prob_space \<subseteq> subprob_space
42   by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)
44 lemma subprob_space_sigma [simp]: "\<Omega> \<noteq> {} \<Longrightarrow> subprob_space (sigma \<Omega> X)"
45 by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)
47 lemma subprob_space_null_measure: "space M \<noteq> {} \<Longrightarrow> subprob_space (null_measure M)"
48 by(simp add: null_measure_def)
50 lemma (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)"
52 proof (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)
57 qed
59 lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \<le> 1"
60   by (rule order.trans[OF emeasure_space emeasure_space_le_1])
62 lemma (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)
65 lemma (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"
68 proof -
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
75 qed
77 lemma 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}"
92 proof (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>)
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
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 .
129 next
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])
134 qed
136 locale pair_subprob_space =
137   pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2
139 sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
140 proof
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)
146 qed
148 lemma 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)
152 lemma 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)"
156 proof(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" .
161 next
162   show "space (restrict_space M A) \<noteq> {}"
163     using A by(simp add: space_restrict_space)
164 qed
166 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
167   "subprob_algebra K =
168     (SUP A : sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
170 lemma 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)
173 lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"
174   by (simp add: subprob_algebra_def)
176 lemma 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)
180 lemma 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
184 lemma 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)
193 ML \<open>
195 fun subprob_cong thm ctxt = (
196   let
197     val thm' = Thm.transfer (Proof_Context.theory_of 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))
206 \<close>
208 setup \<open>
209   Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
210 \<close>
212 context
213   fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
214 begin
216 lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"
217   using measurable_space[OF K] by (simp add: space_subprob_algebra)
219 lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"
220   using measurable_space[OF K] by (simp add: space_subprob_algebra)
222 lemma 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] .
226 end
228 lemma 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)
235 lemma 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)"
239 proof
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
244 next
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)
249 qed
251 lemma 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)"
258 proof (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+
260 next
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
286 qed
288 lemma space_subprob_algebra_empty_iff:
289   "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"
290 proof
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
295 next
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)
301 qed
303 lemma 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
307 proof 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
313 next
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)
319 next
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
325 next
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)
331 next
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)
338 qed
340 lemma 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)"
343 proof (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="op \<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)
357 qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
359 lemma emeasure_space_subprob_algebra[measurable]:
360   "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"
361 proof-
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 .
367 qed
369 lemma 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)"
373 proof (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)
376 qed measurable
378 lemma 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"
382 proof -
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
389   have [measurable]: "F i \<in> N \<rightarrow>\<^sub>M count_space UNIV" for i
390     using F(1) by (rule measurable_simple_function)
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
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)
420 qed
422 (* TODO: Rename. This name is too general -- Manuel *)
423 lemma 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))"
427 proof (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)
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)
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)
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
484 qed
486 lemma 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))"
490 proof (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
506 next
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
522 qed
524 section \<open>Properties of return\<close>
526 definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where
527   "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"
529 lemma space_return[simp]: "space (return M x) = space M"
530   by (simp add: return_def)
532 lemma sets_return[simp]: "sets (return M x) = sets M"
533   by (simp add: return_def)
535 lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
536   by (simp cong: measurable_cong_sets)
538 lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
539   by (simp cong: measurable_cong_sets)
541 lemma 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)
544 lemma 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)
547 lemma emeasure_return[simp]:
548   assumes "A \<in> sets M"
549   shows "emeasure (return M x) A = indicator A x"
550 proof (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)
556 qed
558 lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"
559   by rule simp
561 lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"
562   by (intro prob_space_return prob_space_imp_subprob_space)
564 lemma subprob_space_return_ne:
565   assumes "space M \<noteq> {}" shows "subprob_space (return M x)"
566 proof
567   show "emeasure (return M x) (space (return M x)) \<le> 1"
568     by (subst emeasure_return) (auto split: split_indicator)
569 qed (simp, fact)
571 lemma 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)
574 lemma 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"
577 proof -
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 .
583 qed
585 lemma 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"
588 proof-
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 .
595 qed
597 lemma 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"
601 proof-
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
607 qed
609 lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"
610   by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)
612 lemma 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)
617 lemma 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)
621 lemma 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)"
625 proof -
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 .
674 qed
676 lemma 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"
680 proof -
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)
688 qed
690 lemma 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"
694 proof -
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
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
717 qed
719 lemma 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])
726 definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"
728 lemma 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)
732 lemma 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
736 proof (rule someI2)
737   show "sets M = sets (subprob_algebra N)"
738     by fact
739 next
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
754 qed
756 lemma 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)
760 section \<open>Join\<close>
762 definition 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)"
765 lemma
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)
770 lemma 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)"
773 proof (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
787 qed (auto simp: A sets.space_closed positive_def)
789 lemma measurable_join:
790   "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
791 proof (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))" .
804 next
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)
815 next
816   assume "\<not>(space N \<noteq> {})"
817   thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
818 qed (auto simp: space_subprob_algebra)
820 lemma 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
825 proof 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
834 next
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)
841 next
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
854 next
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)]
863   also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
865   also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
867   finally show ?case by (simp add: ac_simps)
868 next
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)
884 qed
886 lemma measurable_join1:
887   "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>
888   \<Longrightarrow> f \<in> measurable (join M) K"
889 by(simp add: measurable_def)
891 lemma
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)
900 proof(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)
914 next
915   assume *: "space N \<noteq> {}"
917   from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)
919   have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M
920     by(rule measurable_join1)
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
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)
964   show ?integrable using f_pos f_neg by(simp add: real_integrable_def)
966   note [measurable] = nn_integral_measurable_subprob_algebra
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])
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)
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)
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)
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
1027 qed
1029 lemma 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)"
1032 proof (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)
1040 qed (simp add: M)
1042 lemma 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)
1049 lemma join_return':
1050   assumes "sets N = sets M"
1051   shows "join (distr M (subprob_algebra N) (return N)) = M"
1052 apply (rule measure_eqI)
1053 apply (simp add: assms)
1054 apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")
1055 apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
1056 apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)
1057 done
1059 lemma 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")
1063 proof (rule measure_eqI)
1064   fix A assume "A \<in> sets ?r"
1065   hence A_in_N: "A \<in> sets N" by simp
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)
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
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" ..
1091 qed simp
1093 definition 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))"
1099 lemma bind_empty:
1100   "space M = {} \<Longrightarrow> bind M f = count_space {}"
1101   by (simp add: bind_def)
1103 lemma 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)
1107 lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"
1108   by (auto simp: bind_def)
1110 lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
1111   by (simp add: bind_def)
1113 lemma 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)
1118 lemma 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)
1123 lemma bind_cong_All:
1124   assumes "\<forall>x \<in> space M. f x = g x"
1125   shows "bind M f = bind M g"
1126 proof (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)
1131 qed (simp add: bind_empty)
1133 lemma 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
1137 lemma 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
1146 lemma 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')
1151 lemma 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)
1156 lemma 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)"
1160 proof 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)
1165 qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
1167 lemma 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)"
1171 proof 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)
1174 next
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)
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 .
1192 qed
1194 lemma 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)"
1198 proof (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'')
1207 next
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
1212 qed
1214 lemma 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)
1220 lemma 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
1225 lemma subprob_space_bind:
1226   assumes "subprob_space M" "f \<in> measurable M (subprob_algebra N)"
1227   shows "subprob_space (M \<bind> f)"
1228 proof (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)
1234 qed
1236 lemma
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)
1245 proof(case_tac [!] "space M = {}")
1246   assume [simp]: "space M \<noteq> {}"
1247   interpret finite_measure M by(rule fin)
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])
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])
1260 qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)
1262 lemma (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)"
1266 proof
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)
1274 qed
1276 lemma (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
1281 lemma (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"
1284 proof -
1285   interpret Mf: subprob_space "M \<bind> f"
1286     by (rule subprob_space_bind[OF _ f]) unfold_locales
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]
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)
1305 qed
1307 lemma 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)
1313 lemma 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)"
1316 using assms
1317 proof (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)
1322 next
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)
1327 qed
1329 lemma 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)
1335 lemma 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)
1342 lemma 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)
1348 lemma 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
1360 lemma 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)))"
1364 proof -
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)
1369 qed
1371 lemma bind_count_space_singleton:
1372   assumes "subprob_space (f x)"
1373   shows "count_space {x} \<bind> f = f x"
1374 proof-
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 .
1381 qed
1383 lemma 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)"
1388 proof (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
1404 qed
1406 lemma 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")
1411 proof -
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)
1428   from A have [simp]: "space M \<noteq> {}" by blast
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 .
1436 qed
1438 lemma 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)
1442 lemma 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
1451 lemma 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)
1455 lemma 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)"
1459 proof (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)]
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 ..
1486 qed (simp add: bind_empty)
1488 lemma 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"
1493 proof-
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 ..
1511 qed
1513 lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)"
1514   by (simp add: space_subprob_algebra) unfold_locales
1516 lemma (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))))"
1518 proof (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)
1527 qed
1529 lemma (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)))"
1532 proof -
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 .
1549 qed
1551 lemma 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)
1556 lemma (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)
1560 lemma 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)
1565 lemma null_measure_in_space_subprob_algebra [simp]:
1566   "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"
1567 by(simp add: space_subprob_algebra subprob_space_null_measure_iff)
1569 subsection \<open>Giry monad on probability spaces\<close>
1571 definition prob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
1572   "prob_algebra K = restrict_space (subprob_algebra K) {M. prob_space M}"
1574 lemma 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)
1577 lemma 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)
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
1585 lemma 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)
1590 lemma 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
1594 lemma 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
1598 proof (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)
1601 qed
1603 lemma 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)
1606 lemma 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
1610 proof (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)
1615 qed
1617 lemma 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
1621 proof (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)
1626 qed
1628 lemma 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
1632 proof (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)
1638 qed (insert g, simp)
1641 lemma 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
1648 proof
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
1660 qed (insert subsp, auto)
1662 lemma 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)
1667 lemma prob_space_pair:
1668   assumes "prob_space M" "prob_space N" shows "prob_space (M \<Otimes>\<^sub>M N)"
1669 proof -
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
1675 qed
1677 lemma 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)
1682 lemma 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)
1691 lemma 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)
1696 lemma 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)
1701 lemma 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"
1706 proof (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)
1713 qed
1715 lemma 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)
1720 lemma 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"
1728 proof (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}" .
1739 qed (insert assms, auto)
1741 lemma 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"
1747 proof cases
1748   assume "space N = {}" then show ?thesis
1749     using `M = N` by (simp add: bind_empty)
1750 next
1751   assume "space N \<noteq> {}"
1752   show ?thesis unfolding `M = N`
1753   proof (rule measure_eqI)
1754     have *: "sets (N \<bind> f) = sets B"
1755       using sets_bind[OF sets_kernel[OF f] `space N \<noteq> {}`] by simp
1756     then show "sets (N \<bind> f) = sets (N \<bind> g)"
1757       using sets_bind[OF sets_kernel[OF g] `space N \<noteq> {}`] 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 `space N \<noteq> {}` 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
1764 qed
1766 lemma bind_cong_strong: "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)
1769 lemma 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
1775 lemma 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
1781 lemma 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')
1787 end