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