author hoelzl Fri Feb 19 13:40:50 2016 +0100 (2016-02-19) changeset 62378 85ed00c1fe7c parent 62026 ea3b1b0413b4 child 62975 1d066f6ab25d permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     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 Lebesgue_Integral_Substitution "~~/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

    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 add: nn_integral_const_If)

    70   also have "\<dots> \<le> c * 1" using emeasure_space_le_1 \<open>0 \<le> c\<close> by(rule ereal_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

   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   have "\<And>a b. \<lbrakk>a \<ge> 0; b \<ge> 0; a \<le> 1; b \<le> 1\<rbrakk> \<Longrightarrow> a * b \<le> (1::ereal)"

   139     by (metis monoid_mult_class.mult.left_neutral dual_order.trans ereal_mult_right_mono)

   140   from this[OF _ _ M1.emeasure_space_le_1 M2.emeasure_space_le_1]

   141     show "emeasure (M1 \<Otimes>\<^sub>M M2) (space (M1 \<Otimes>\<^sub>M M2)) \<le> 1"

   142     by (simp add: M2.emeasure_pair_measure_Times space_pair_measure emeasure_nonneg)

   143   from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \<Otimes>\<^sub>M M2) \<noteq> {}"

   144     by (simp add: space_pair_measure)

   145 qed

   146

   147 lemma subprob_space_null_measure_iff:

   148     "subprob_space (null_measure M) \<longleftrightarrow> space M \<noteq> {}"

   149   by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)

   150

   151 lemma subprob_space_restrict_space:

   152   assumes M: "subprob_space M"

   153   and A: "A \<inter> space M \<in> sets M" "A \<inter> space M \<noteq> {}"

   154   shows "subprob_space (restrict_space M A)"

   155 proof(rule subprob_spaceI)

   156   have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \<inter> space M)"

   157     using A by(simp add: emeasure_restrict_space space_restrict_space)

   158   also have "\<dots> \<le> 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)

   159   finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \<le> 1" .

   160 next

   161   show "space (restrict_space M A) \<noteq> {}"

   162     using A by(simp add: space_restrict_space)

   163 qed

   164

   165 definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where

   166   "subprob_algebra K =

   167     (\<Squnion>\<^sub>\<sigma> A\<in>sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"

   168

   169 lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"

   170   by (auto simp add: subprob_algebra_def space_Sup_sigma)

   171

   172 lemma subprob_algebra_cong: "sets M = sets N \<Longrightarrow> subprob_algebra M = subprob_algebra N"

   173   by (simp add: subprob_algebra_def)

   174

   175 lemma measurable_emeasure_subprob_algebra[measurable]:

   176   "a \<in> sets A \<Longrightarrow> (\<lambda>M. emeasure M a) \<in> borel_measurable (subprob_algebra A)"

   177   by (auto intro!: measurable_Sup_sigma1 measurable_vimage_algebra1 simp: subprob_algebra_def)

   178

   179 lemma subprob_measurableD:

   180   assumes N: "N \<in> measurable M (subprob_algebra S)" and x: "x \<in> space M"

   181   shows "space (N x) = space S"

   182     and "sets (N x) = sets S"

   183     and "measurable (N x) K = measurable S K"

   184     and "measurable K (N x) = measurable K S"

   185   using measurable_space[OF N x]

   186   by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)

   187

   188 ML \<open>

   189

   190 fun subprob_cong thm ctxt = (

   191   let

   192     val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm

   193     val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>

   194       dest_comb |> snd |> strip_abs_body |> head_of |> is_Free

   195   in

   196     if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)

   197             else ([], ctxt)

   198   end

   199   handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))

   200

   201 \<close>

   202

   203 setup \<open>

   204   Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)

   205 \<close>

   206

   207 context

   208   fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"

   209 begin

   210

   211 lemma subprob_space_kernel: "a \<in> space M \<Longrightarrow> subprob_space (K a)"

   212   using measurable_space[OF K] by (simp add: space_subprob_algebra)

   213

   214 lemma sets_kernel: "a \<in> space M \<Longrightarrow> sets (K a) = sets N"

   215   using measurable_space[OF K] by (simp add: space_subprob_algebra)

   216

   217 lemma measurable_emeasure_kernel[measurable]:

   218     "A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M"

   219   using measurable_compose[OF K measurable_emeasure_subprob_algebra] .

   220

   221 end

   222

   223 lemma measurable_subprob_algebra:

   224   "(\<And>a. a \<in> space M \<Longrightarrow> subprob_space (K a)) \<Longrightarrow>

   225   (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>

   226   (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>

   227   K \<in> measurable M (subprob_algebra N)"

   228   by (auto intro!: measurable_Sup_sigma2 measurable_vimage_algebra2 simp: subprob_algebra_def)

   229

   230 lemma measurable_submarkov:

   231   "K \<in> measurable M (subprob_algebra M) \<longleftrightarrow>

   232     (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>

   233     (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"

   234 proof

   235   assume "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>

   236     (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"

   237   then show "K \<in> measurable M (subprob_algebra M)"

   238     by (intro measurable_subprob_algebra) auto

   239 next

   240   assume "K \<in> measurable M (subprob_algebra M)"

   241   then show "(\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>

   242     (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"

   243     by (auto dest: subprob_space_kernel sets_kernel)

   244 qed

   245

   246 lemma space_subprob_algebra_empty_iff:

   247   "space (subprob_algebra N) = {} \<longleftrightarrow> space N = {}"

   248 proof

   249   have "\<And>x. x \<in> space N \<Longrightarrow> density N (\<lambda>_. 0) \<in> space (subprob_algebra N)"

   250     by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)

   251   then show "space (subprob_algebra N) = {} \<Longrightarrow> space N = {}"

   252     by auto

   253 next

   254   assume "space N = {}"

   255   hence "sets N = {{}}" by (simp add: space_empty_iff)

   256   moreover have "\<And>M. subprob_space M \<Longrightarrow> sets M \<noteq> {{}}"

   257     by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])

   258   ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)

   259 qed

   260

   261 lemma nn_integral_measurable_subprob_algebra':

   262   assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"

   263   shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")

   264   using f

   265 proof induct

   266   case (cong f g)

   267   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"

   268     by (intro measurable_cong nn_integral_cong cong)

   269        (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)

   270   ultimately show ?case by simp

   271 next

   272   case (set B)

   273   moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. indicator B M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. emeasure M' B) \<in> ?B"

   274     by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)

   275   ultimately show ?case

   276     by (simp add: measurable_emeasure_subprob_algebra)

   277 next

   278   case (mult f c)

   279   moreover 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"

   280     by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)

   281   ultimately show ?case

   282     by simp

   283 next

   284   case (add f g)

   285   moreover 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"

   286     by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)

   287   ultimately show ?case

   288     by (simp add: ac_simps)

   289 next

   290   case (seq F)

   291   moreover 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"

   292     unfolding SUP_apply

   293     by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)

   294   ultimately show ?case

   295     by (simp add: ac_simps)

   296 qed

   297

   298 lemma nn_integral_measurable_subprob_algebra:

   299   "f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)"

   300   by (subst nn_integral_max_0[symmetric])

   301      (auto intro!: nn_integral_measurable_subprob_algebra')

   302

   303 lemma measurable_distr:

   304   assumes [measurable]: "f \<in> measurable M N"

   305   shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"

   306 proof (cases "space N = {}")

   307   assume not_empty: "space N \<noteq> {}"

   308   show ?thesis

   309   proof (rule measurable_subprob_algebra)

   310     fix A assume A: "A \<in> sets N"

   311     then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>

   312       (\<lambda>M'. emeasure M' (f - A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"

   313       by (intro measurable_cong)

   314          (auto simp: emeasure_distr space_subprob_algebra

   315                intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])

   316     also have "\<dots>"

   317       using A by (intro measurable_emeasure_subprob_algebra) simp

   318     finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .

   319   qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)

   320 qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)

   321

   322 lemma emeasure_space_subprob_algebra[measurable]:

   323   "(\<lambda>a. emeasure a (space a)) \<in> borel_measurable (subprob_algebra N)"

   324 proof-

   325   have "(\<lambda>a. emeasure a (space N)) \<in> borel_measurable (subprob_algebra N)" (is "?f \<in> ?M")

   326     by (rule measurable_emeasure_subprob_algebra) simp

   327   also have "?f \<in> ?M \<longleftrightarrow> (\<lambda>a. emeasure a (space a)) \<in> ?M"

   328     by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)

   329   finally show ?thesis .

   330 qed

   331

   332 lemma integral_measurable_subprob_algebra:

   333   fixes f :: "_ \<Rightarrow> real"

   334   assumes f_measurable [measurable]: "f \<in> borel_measurable N"

   335   and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"

   336   shows "(\<lambda>M. integral\<^sup>L M f) \<in> borel_measurable (subprob_algebra N)"

   337 proof -

   338   note [measurable] = nn_integral_measurable_subprob_algebra

   339   have "?thesis \<longleftrightarrow> (\<lambda>M. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M) - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M)) \<in> borel_measurable (subprob_algebra N)"

   340   proof(rule measurable_cong)

   341     fix M

   342     assume "M \<in> space (subprob_algebra N)"

   343     hence "subprob_space M" and M [measurable_cong]: "sets M = sets N"

   344       by(simp_all add: space_subprob_algebra)

   345     interpret subprob_space M by fact

   346     have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M)"

   347       by(rule nn_integral_mono)(simp add: sets_eq_imp_space_eq[OF M] f_bounded)

   348     also have "\<dots> = max B 0 * emeasure M (space M)" by(simp add: nn_integral_const_If max_def)

   349     also have "\<dots> \<le> ereal (max B 0) * 1"

   350       by(rule ereal_mult_left_mono)(simp_all add: emeasure_space_le_1 zero_ereal_def)

   351     finally have "(\<integral>\<^sup>+ x. ereal \<bar>f x\<bar> \<partial>M) \<noteq> \<infinity>" by(auto simp add: max_def)

   352     then have "integrable M f" using f_measurable

   353       by(auto intro: integrableI_bounded)

   354     thus "(\<integral> x. f x \<partial>M) = real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M) - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M)"

   355       by(simp add: real_lebesgue_integral_def)

   356   qed

   357   also have "\<dots>" by measurable

   358   finally show ?thesis .

   359 qed

   360

   361 (* TODO: Rename. This name is too general -- Manuel *)

   362 lemma measurable_pair_measure:

   363   assumes f: "f \<in> measurable M (subprob_algebra N)"

   364   assumes g: "g \<in> measurable M (subprob_algebra L)"

   365   shows "(\<lambda>x. f x \<Otimes>\<^sub>M g x) \<in> measurable M (subprob_algebra (N \<Otimes>\<^sub>M L))"

   366 proof (rule measurable_subprob_algebra)

   367   { fix x assume "x \<in> space M"

   368     with measurable_space[OF f] measurable_space[OF g]

   369     have fx: "f x \<in> space (subprob_algebra N)" and gx: "g x \<in> space (subprob_algebra L)"

   370       by auto

   371     interpret F: subprob_space "f x"

   372       using fx by (simp add: space_subprob_algebra)

   373     interpret G: subprob_space "g x"

   374       using gx by (simp add: space_subprob_algebra)

   375

   376     interpret pair_subprob_space "f x" "g x" ..

   377     show "subprob_space (f x \<Otimes>\<^sub>M g x)" by unfold_locales

   378     show sets_eq: "sets (f x \<Otimes>\<^sub>M g x) = sets (N \<Otimes>\<^sub>M L)"

   379       using fx gx by (simp add: space_subprob_algebra)

   380

   381     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"

   382       using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra)

   383     have "emeasure (f x \<Otimes>\<^sub>M g x) (space (f x \<Otimes>\<^sub>M g x)) =

   384               emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"

   385       by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)

   386     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) =

   387                                              ... - emeasure (f x \<Otimes>\<^sub>M g x) A"

   388       using emeasure_compl[OF _ P.emeasure_finite]

   389       unfolding sets_eq

   390       unfolding sets_eq_imp_space_eq[OF sets_eq]

   391       by (simp add: space_pair_measure G.emeasure_pair_measure_Times)

   392     note 1 2 sets_eq }

   393   note Times = this(1) and Compl = this(2) and sets_eq = this(3)

   394

   395   fix A assume A: "A \<in> sets (N \<Otimes>\<^sub>M L)"

   396   show "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) A) \<in> borel_measurable M"

   397     using Int_stable_pair_measure_generator pair_measure_closed A

   398     unfolding sets_pair_measure

   399   proof (induct A rule: sigma_sets_induct_disjoint)

   400     case (basic A) then show ?case

   401       by (auto intro!: borel_measurable_ereal_times simp: Times cong: measurable_cong)

   402          (auto intro!: measurable_emeasure_kernel f g)

   403   next

   404     case (compl A)

   405     then have A: "A \<in> sets (N \<Otimes>\<^sub>M L)"

   406       by (auto simp: sets_pair_measure)

   407     have "(\<lambda>x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) -

   408                    emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")

   409       using compl(2) f g by measurable

   410     thus ?case by (simp add: Compl A cong: measurable_cong)

   411   next

   412     case (union A)

   413     then have "range A \<subseteq> sets (N \<Otimes>\<^sub>M L)" "disjoint_family A"

   414       by (auto simp: sets_pair_measure)

   415     then have "(\<lambda>a. emeasure (f a \<Otimes>\<^sub>M g a) (\<Union>i. A i)) \<in> borel_measurable M \<longleftrightarrow>

   416       (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"

   417       by (intro measurable_cong suminf_emeasure[symmetric])

   418          (auto simp: sets_eq)

   419     also have "\<dots>"

   420       using union by auto

   421     finally show ?case .

   422   qed simp

   423 qed

   424

   425 lemma restrict_space_measurable:

   426   assumes X: "X \<noteq> {}" "X \<in> sets K"

   427   assumes N: "N \<in> measurable M (subprob_algebra K)"

   428   shows "(\<lambda>x. restrict_space (N x) X) \<in> measurable M (subprob_algebra (restrict_space K X))"

   429 proof (rule measurable_subprob_algebra)

   430   fix a assume a: "a \<in> space M"

   431   from N[THEN measurable_space, OF this]

   432   have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"

   433     by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)

   434   then interpret subprob_space "N a"

   435     by simp

   436   show "subprob_space (restrict_space (N a) X)"

   437   proof

   438     show "space (restrict_space (N a) X) \<noteq> {}"

   439       using X by (auto simp add: space_restrict_space)

   440     show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \<le> 1"

   441       using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)

   442   qed

   443   show "sets (restrict_space (N a) X) = sets (restrict_space K X)"

   444     by (intro sets_restrict_space_cong) fact

   445 next

   446   fix A assume A: "A \<in> sets (restrict_space K X)"

   447   show "(\<lambda>a. emeasure (restrict_space (N a) X) A) \<in> borel_measurable M"

   448   proof (subst measurable_cong)

   449     fix a assume "a \<in> space M"

   450     from N[THEN measurable_space, OF this]

   451     have [simp]: "sets (N a) = sets K" "space (N a) = space K"

   452       by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)

   453     show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \<inter> X)"

   454       using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)

   455   next

   456     show "(\<lambda>w. emeasure (N w) (A \<inter> X)) \<in> borel_measurable M"

   457       using A X

   458       by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])

   459          (auto simp: sets_restrict_space)

   460   qed

   461 qed

   462

   463 section \<open>Properties of return\<close>

   464

   465 definition return :: "'a measure \<Rightarrow> 'a \<Rightarrow> 'a measure" where

   466   "return R x = measure_of (space R) (sets R) (\<lambda>A. indicator A x)"

   467

   468 lemma space_return[simp]: "space (return M x) = space M"

   469   by (simp add: return_def)

   470

   471 lemma sets_return[simp]: "sets (return M x) = sets M"

   472   by (simp add: return_def)

   473

   474 lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"

   475   by (simp cong: measurable_cong_sets)

   476

   477 lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"

   478   by (simp cong: measurable_cong_sets)

   479

   480 lemma return_sets_cong: "sets M = sets N \<Longrightarrow> return M = return N"

   481   by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)

   482

   483 lemma return_cong: "sets A = sets B \<Longrightarrow> return A x = return B x"

   484   by (auto simp add: return_def dest: sets_eq_imp_space_eq)

   485

   486 lemma emeasure_return[simp]:

   487   assumes "A \<in> sets M"

   488   shows "emeasure (return M x) A = indicator A x"

   489 proof (rule emeasure_measure_of[OF return_def])

   490   show "sets M \<subseteq> Pow (space M)" by (rule sets.space_closed)

   491   show "positive (sets (return M x)) (\<lambda>A. indicator A x)" by (simp add: positive_def)

   492   from assms show "A \<in> sets (return M x)" unfolding return_def by simp

   493   show "countably_additive (sets (return M x)) (\<lambda>A. indicator A x)"

   494     by (auto intro: countably_additiveI simp: suminf_indicator)

   495 qed

   496

   497 lemma prob_space_return: "x \<in> space M \<Longrightarrow> prob_space (return M x)"

   498   by rule simp

   499

   500 lemma subprob_space_return: "x \<in> space M \<Longrightarrow> subprob_space (return M x)"

   501   by (intro prob_space_return prob_space_imp_subprob_space)

   502

   503 lemma subprob_space_return_ne:

   504   assumes "space M \<noteq> {}" shows "subprob_space (return M x)"

   505 proof

   506   show "emeasure (return M x) (space (return M x)) \<le> 1"

   507     by (subst emeasure_return) (auto split: split_indicator)

   508 qed (simp, fact)

   509

   510 lemma measure_return: assumes X: "X \<in> sets M" shows "measure (return M x) X = indicator X x"

   511   unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)

   512

   513 lemma AE_return:

   514   assumes [simp]: "x \<in> space M" and [measurable]: "Measurable.pred M P"

   515   shows "(AE y in return M x. P y) \<longleftrightarrow> P x"

   516 proof -

   517   have "(AE y in return M x. y \<notin> {x\<in>space M. \<not> P x}) \<longleftrightarrow> P x"

   518     by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)

   519   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)"

   520     by (rule AE_cong) auto

   521   finally show ?thesis .

   522 qed

   523

   524 lemma nn_integral_return:

   525   assumes "g x \<ge> 0" "x \<in> space M" "g \<in> borel_measurable M"

   526   shows "(\<integral>\<^sup>+ a. g a \<partial>return M x) = g x"

   527 proof-

   528   interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>])

   529   have "(\<integral>\<^sup>+ a. g a \<partial>return M x) = (\<integral>\<^sup>+ a. g x \<partial>return M x)" using assms

   530     by (intro nn_integral_cong_AE) (auto simp: AE_return)

   531   also have "... = g x"

   532     using nn_integral_const[OF \<open>g x \<ge> 0\<close>, of "return M x"] emeasure_space_1 by simp

   533   finally show ?thesis .

   534 qed

   535

   536 lemma integral_return:

   537   fixes g :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"

   538   assumes "x \<in> space M" "g \<in> borel_measurable M"

   539   shows "(\<integral>a. g a \<partial>return M x) = g x"

   540 proof-

   541   interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>])

   542   have "(\<integral>a. g a \<partial>return M x) = (\<integral>a. g x \<partial>return M x)" using assms

   543     by (intro integral_cong_AE) (auto simp: AE_return)

   544   then show ?thesis

   545     using prob_space by simp

   546 qed

   547

   548 lemma return_measurable[measurable]: "return N \<in> measurable N (subprob_algebra N)"

   549   by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)

   550

   551 lemma distr_return:

   552   assumes "f \<in> measurable M N" and "x \<in> space M"

   553   shows "distr (return M x) N f = return N (f x)"

   554   using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)

   555

   556 lemma return_restrict_space:

   557   "\<Omega> \<in> sets M \<Longrightarrow> return (restrict_space M \<Omega>) x = restrict_space (return M x) \<Omega>"

   558   by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)

   559

   560 lemma measurable_distr2:

   561   assumes f[measurable]: "case_prod f \<in> measurable (L \<Otimes>\<^sub>M M) N"

   562   assumes g[measurable]: "g \<in> measurable L (subprob_algebra M)"

   563   shows "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)"

   564 proof -

   565   have "(\<lambda>x. distr (g x) N (f x)) \<in> measurable L (subprob_algebra N)

   566     \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"

   567   proof (rule measurable_cong)

   568     fix x assume x: "x \<in> space L"

   569     have gx: "g x \<in> space (subprob_algebra M)"

   570       using measurable_space[OF g x] .

   571     then have [simp]: "sets (g x) = sets M"

   572       by (simp add: space_subprob_algebra)

   573     then have [simp]: "space (g x) = space M"

   574       by (rule sets_eq_imp_space_eq)

   575     let ?R = "return L x"

   576     from measurable_compose_Pair1[OF x f] have f_M': "f x \<in> measurable M N"

   577       by simp

   578     interpret subprob_space "g x"

   579       using gx by (simp add: space_subprob_algebra)

   580     have space_pair_M'[simp]: "\<And>X. space (X \<Otimes>\<^sub>M g x) = space (X \<Otimes>\<^sub>M M)"

   581       by (simp add: space_pair_measure)

   582     show "distr (g x) N (f x) = distr (?R \<Otimes>\<^sub>M g x) N (case_prod f)" (is "?l = ?r")

   583     proof (rule measure_eqI)

   584       show "sets ?l = sets ?r"

   585         by simp

   586     next

   587       fix A assume "A \<in> sets ?l"

   588       then have A[measurable]: "A \<in> sets N"

   589         by simp

   590       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))"

   591         by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)

   592       also have "\<dots> = (\<integral>\<^sup>+M''. emeasure (g x) (f M'' - A \<inter> space M) \<partial>?R)"

   593         apply (subst emeasure_pair_measure_alt)

   594         apply (rule measurable_sets[OF _ A])

   595         apply (auto simp add: f_M' cong: measurable_cong_sets)

   596         apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])

   597         apply (auto simp: space_subprob_algebra space_pair_measure)

   598         done

   599       also have "\<dots> = emeasure (g x) (f x - A \<inter> space M)"

   600         by (subst nn_integral_return)

   601            (auto simp: x intro!: measurable_emeasure)

   602       also have "\<dots> = emeasure ?l A"

   603         by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)

   604       finally show "emeasure ?l A = emeasure ?r A" ..

   605     qed

   606   qed

   607   also have "\<dots>"

   608     apply (intro measurable_compose[OF measurable_pair_measure measurable_distr])

   609     apply (rule return_measurable)

   610     apply measurable

   611     done

   612   finally show ?thesis .

   613 qed

   614

   615 lemma nn_integral_measurable_subprob_algebra2:

   616   assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"

   617   assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"

   618   shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"

   619 proof -

   620   note nn_integral_measurable_subprob_algebra[measurable]

   621   note measurable_distr2[measurable]

   622   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"

   623     by measurable

   624   then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"

   625     by (rule measurable_cong[THEN iffD1, rotated])

   626        (simp add: nn_integral_distr)

   627 qed

   628

   629 lemma emeasure_measurable_subprob_algebra2:

   630   assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"

   631   assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"

   632   shows "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"

   633 proof -

   634   { fix x assume "x \<in> space M"

   635     then have "Pair x - Sigma (space M) A = A x"

   636       by auto

   637     with sets_Pair1[OF A, of x] have "A x \<in> sets N"

   638       by auto }

   639   note ** = this

   640

   641   have *: "\<And>x. fst x \<in> space M \<Longrightarrow> snd x \<in> A (fst x) \<longleftrightarrow> x \<in> (SIGMA x:space M. A x)"

   642     by (auto simp: fun_eq_iff)

   643   have "(\<lambda>(x, y). indicator (A x) y::ereal) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"

   644     apply measurable

   645     apply (subst measurable_cong)

   646     apply (rule *)

   647     apply (auto simp: space_pair_measure)

   648     done

   649   then have "(\<lambda>x. integral\<^sup>N (L x) (indicator (A x))) \<in> borel_measurable M"

   650     by (intro nn_integral_measurable_subprob_algebra2[where N=N] ereal_indicator_nonneg L)

   651   then show "(\<lambda>x. emeasure (L x) (A x)) \<in> borel_measurable M"

   652     apply (rule measurable_cong[THEN iffD1, rotated])

   653     apply (rule nn_integral_indicator)

   654     apply (simp add: subprob_measurableD[OF L] **)

   655     done

   656 qed

   657

   658 lemma measure_measurable_subprob_algebra2:

   659   assumes A[measurable]: "(SIGMA x:space M. A x) \<in> sets (M \<Otimes>\<^sub>M N)"

   660   assumes L[measurable]: "L \<in> measurable M (subprob_algebra N)"

   661   shows "(\<lambda>x. measure (L x) (A x)) \<in> borel_measurable M"

   662   unfolding measure_def

   663   by (intro borel_measurable_real_of_ereal emeasure_measurable_subprob_algebra2[OF assms])

   664

   665 definition "select_sets M = (SOME N. sets M = sets (subprob_algebra N))"

   666

   667 lemma select_sets1:

   668   "sets M = sets (subprob_algebra N) \<Longrightarrow> sets M = sets (subprob_algebra (select_sets M))"

   669   unfolding select_sets_def by (rule someI)

   670

   671 lemma sets_select_sets[simp]:

   672   assumes sets: "sets M = sets (subprob_algebra N)"

   673   shows "sets (select_sets M) = sets N"

   674   unfolding select_sets_def

   675 proof (rule someI2)

   676   show "sets M = sets (subprob_algebra N)"

   677     by fact

   678 next

   679   fix L assume "sets M = sets (subprob_algebra L)"

   680   with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"

   681     by (intro sets_eq_imp_space_eq) simp

   682   show "sets L = sets N"

   683   proof cases

   684     assume "space (subprob_algebra N) = {}"

   685     with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]

   686     show ?thesis

   687       by (simp add: eq space_empty_iff)

   688   next

   689     assume "space (subprob_algebra N) \<noteq> {}"

   690     with eq show ?thesis

   691       by (fastforce simp add: space_subprob_algebra)

   692   qed

   693 qed

   694

   695 lemma space_select_sets[simp]:

   696   "sets M = sets (subprob_algebra N) \<Longrightarrow> space (select_sets M) = space N"

   697   by (intro sets_eq_imp_space_eq sets_select_sets)

   698

   699 section \<open>Join\<close>

   700

   701 definition join :: "'a measure measure \<Rightarrow> 'a measure" where

   702   "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"

   703

   704 lemma

   705   shows space_join[simp]: "space (join M) = space (select_sets M)"

   706     and sets_join[simp]: "sets (join M) = sets (select_sets M)"

   707   by (simp_all add: join_def)

   708

   709 lemma emeasure_join:

   710   assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"

   711   shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"

   712 proof (rule emeasure_measure_of[OF join_def])

   713   show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"

   714   proof (rule countably_additiveI)

   715     fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"

   716     have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"

   717       using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)

   718     also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"

   719     proof (rule nn_integral_cong)

   720       fix M' assume "M' \<in> space M"

   721       then show "(\<Sum>i. emeasure M' (A i)) = emeasure M' (\<Union>i. A i)"

   722         using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)

   723     qed

   724     finally show "(\<Sum>i. \<integral>\<^sup>+M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)" .

   725   qed

   726 qed (auto simp: A sets.space_closed positive_def nn_integral_nonneg)

   727

   728 lemma measurable_join:

   729   "join \<in> measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"

   730 proof (cases "space N \<noteq> {}", rule measurable_subprob_algebra)

   731   fix A assume "A \<in> sets N"

   732   let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"

   733   have "(\<lambda>M'. emeasure (join M') A) \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')) \<in> ?B"

   734   proof (rule measurable_cong)

   735     fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"

   736     then show "emeasure (join M') A = (\<integral>\<^sup>+ M''. emeasure M'' A \<partial>M')"

   737       by (intro emeasure_join) (auto simp: space_subprob_algebra \<open>A\<in>sets N\<close>)

   738   qed

   739   also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"

   740     using measurable_emeasure_subprob_algebra[OF \<open>A\<in>sets N\<close>]

   741     by (rule nn_integral_measurable_subprob_algebra)

   742   finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .

   743 next

   744   assume [simp]: "space N \<noteq> {}"

   745   fix M assume M: "M \<in> space (subprob_algebra (subprob_algebra N))"

   746   then have "(\<integral>\<^sup>+M'. emeasure M' (space N) \<partial>M) \<le> (\<integral>\<^sup>+M'. 1 \<partial>M)"

   747     apply (intro nn_integral_mono)

   748     apply (auto simp: space_subprob_algebra

   749                  dest!: sets_eq_imp_space_eq subprob_space.emeasure_space_le_1)

   750     done

   751   with M show "subprob_space (join M)"

   752     by (intro subprob_spaceI)

   753        (auto simp: emeasure_join space_subprob_algebra M assms dest: subprob_space.emeasure_space_le_1)

   754 next

   755   assume "\<not>(space N \<noteq> {})"

   756   thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)

   757 qed (auto simp: space_subprob_algebra)

   758

   759 lemma nn_integral_join':

   760   assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"

   761     and M[measurable_cong]: "sets M = sets (subprob_algebra N)"

   762   shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"

   763   using f

   764 proof induct

   765   case (cong f g)

   766   moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"

   767     by (intro nn_integral_cong cong) (simp add: M)

   768   moreover from M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' f \<partial>M) = (\<integral>\<^sup>+ M'. integral\<^sup>N M' g \<partial>M)"

   769     by (intro nn_integral_cong cong)

   770        (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)

   771   ultimately show ?case

   772     by simp

   773 next

   774   case (set A)

   775   moreover with M have "(\<integral>\<^sup>+ M'. integral\<^sup>N M' (indicator A) \<partial>M) = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"

   776     by (intro nn_integral_cong nn_integral_indicator)

   777        (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)

   778   ultimately show ?case

   779     using M by (simp add: emeasure_join)

   780 next

   781   case (mult f c)

   782   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)"

   783     using mult M M[THEN sets_eq_imp_space_eq]

   784     by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)

   785   also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"

   786     using nn_integral_measurable_subprob_algebra[OF mult(3)]

   787     by (intro nn_integral_cmult mult) (simp add: M)

   788   also have "\<dots> = c * (integral\<^sup>N (join M) f)"

   789     by (simp add: mult)

   790   also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"

   791     using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)

   792   finally show ?case by simp

   793 next

   794   case (add f g)

   795   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)"

   796     using add M M[THEN sets_eq_imp_space_eq]

   797     by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)

   798   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)"

   799     using nn_integral_measurable_subprob_algebra[OF add(1)]

   800     using nn_integral_measurable_subprob_algebra[OF add(5)]

   801     by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)

   802   also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"

   803     by (simp add: add)

   804   also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"

   805     using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)

   806   finally show ?case by (simp add: ac_simps)

   807 next

   808   case (seq F)

   809   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)"

   810     using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply

   811     by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)

   812        (auto simp add: space_subprob_algebra)

   813   also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"

   814     using nn_integral_measurable_subprob_algebra[OF seq(1)] seq

   815     by (intro nn_integral_monotone_convergence_SUP)

   816        (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )

   817   also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"

   818     by (simp add: seq)

   819   also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"

   820     using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)

   821                  (simp_all add: M cong: measurable_cong_sets)

   822   finally show ?case by (simp add: ac_simps)

   823 qed

   824

   825 lemma nn_integral_join:

   826   assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)"

   827   shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"

   828   apply (subst (1 3) nn_integral_max_0[symmetric])

   829   apply (rule nn_integral_join')

   830   apply (auto simp: f)

   831   done

   832

   833 lemma measurable_join1:

   834   "\<lbrakk> f \<in> measurable N K; sets M = sets (subprob_algebra N) \<rbrakk>

   835   \<Longrightarrow> f \<in> measurable (join M) K"

   836 by(simp add: measurable_def)

   837

   838 lemma

   839   fixes f :: "_ \<Rightarrow> real"

   840   assumes f_measurable [measurable]: "f \<in> borel_measurable N"

   841   and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> \<bar>f x\<bar> \<le> B"

   842   and M [measurable_cong]: "sets M = sets (subprob_algebra N)"

   843   and fin: "finite_measure M"

   844   and M_bounded: "AE M' in M. emeasure M' (space M') \<le> ereal B'"

   845   shows integrable_join: "integrable (join M) f" (is ?integrable)

   846   and integral_join: "integral\<^sup>L (join M) f = \<integral> M'. integral\<^sup>L M' f \<partial>M" (is ?integral)

   847 proof(case_tac [!] "space N = {}")

   848   assume *: "space N = {}"

   849   show ?integrable

   850     using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)

   851   have "(\<integral> M'. integral\<^sup>L M' f \<partial>M) = (\<integral> M'. 0 \<partial>M)"

   852   proof(rule integral_cong)

   853     fix M'

   854     assume "M' \<in> space M"

   855     with sets_eq_imp_space_eq[OF M] have "space M' = space N"

   856       by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)

   857     with * show "(\<integral> x. f x \<partial>M') = 0" by(simp add: integral_empty)

   858   qed simp

   859   then show ?integral

   860     using M * by(simp add: integral_empty)

   861 next

   862   assume *: "space N \<noteq> {}"

   863

   864   from * have B [simp]: "0 \<le> B" by(auto dest: f_bounded)

   865

   866   have [measurable]: "f \<in> borel_measurable (join M)" using f_measurable M

   867     by(rule measurable_join1)

   868

   869   { fix f M'

   870     assume [measurable]: "f \<in> borel_measurable N"

   871       and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"

   872       and "M' \<in> space M" "emeasure M' (space M') \<le> ereal B'"

   873     have "AE x in M'. ereal (f x) \<le> ereal B"

   874     proof(rule AE_I2)

   875       fix x

   876       assume "x \<in> space M'"

   877       with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]

   878       have "x \<in> space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)

   879       from f_bounded[OF this] show "ereal (f x) \<le> ereal B" by simp

   880     qed

   881     then have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> (\<integral>\<^sup>+ x. ereal B \<partial>M')"

   882       by(rule nn_integral_mono_AE)

   883     also have "\<dots> = ereal B * emeasure M' (space M')" by(simp)

   884     also have "\<dots> \<le> ereal B * ereal B'" by(rule ereal_mult_left_mono)(fact, simp)

   885     also have "\<dots> \<le> ereal B * ereal \<bar>B'\<bar>" by(rule ereal_mult_left_mono)(simp_all)

   886     finally have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)" by simp }

   887   note bounded1 = this

   888

   889   have bounded:

   890     "\<And>f. \<lbrakk> f \<in> borel_measurable N; \<And>x. x \<in> space N \<Longrightarrow> f x \<le> B \<rbrakk>

   891     \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"

   892   proof -

   893     fix f

   894     assume [measurable]: "f \<in> borel_measurable N"

   895       and f_bounded: "\<And>x. x \<in> space N \<Longrightarrow> f x \<le> B"

   896     have "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. ereal (f x) \<partial>M' \<partial>M)"

   897       by(rule nn_integral_join[OF _ M]) simp

   898     also have "\<dots> \<le> \<integral>\<^sup>+ M'. B * \<bar>B'\<bar> \<partial>M"

   899       using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]

   900       by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])

   901     also have "\<dots> = B * \<bar>B'\<bar> * emeasure M (space M)" by simp

   902     also have "\<dots> < \<infinity>" by(simp add: finite_measure.finite_emeasure_space[OF fin])

   903     finally show "?thesis f" by simp

   904   qed

   905   have f_pos: "(\<integral>\<^sup>+ x. ereal (f x) \<partial>join M) \<noteq> \<infinity>"

   906     and f_neg: "(\<integral>\<^sup>+ x. ereal (- f x) \<partial>join M) \<noteq> \<infinity>"

   907     using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)

   908

   909   show ?integrable using f_pos f_neg by(simp add: real_integrable_def)

   910

   911   note [measurable] = nn_integral_measurable_subprob_algebra

   912

   913   have "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (f x) \<partial>join M)"

   914     by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)

   915   also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (f x) \<partial>M' \<partial>M"

   916     by(simp add: nn_integral_join[OF _ M])

   917   also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M"

   918     by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)

   919   finally have int_f: "(\<integral>\<^sup>+ x. f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)" .

   920

   921   have "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ x. max 0 (- f x) \<partial>join M)"

   922     by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)

   923   also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. max 0 (- f x) \<partial>M' \<partial>M"

   924     by(simp add: nn_integral_join[OF _ M])

   925   also have "\<dots> = \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M"

   926     by(subst nn_integral_max_0[symmetric])(simp add: zero_ereal_def)

   927   finally have int_mf: "(\<integral>\<^sup>+ x. - f x \<partial>join M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)" .

   928

   929   have f_pos1:

   930     "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>

   931     \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"

   932     using f_measurable by(auto intro!: bounded1 dest: f_bounded)

   933   have "AE M' in M. (\<integral>\<^sup>+ x. f x \<partial>M') \<noteq> \<infinity>"

   934     using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_pos1)

   935   hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"

   936     by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)

   937   from f_pos have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M'))"

   938     by(simp add: int_f real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)

   939

   940   have f_neg1:

   941     "\<And>M'. \<lbrakk> M' \<in> space M; emeasure M' (space M') \<le> ereal B' \<rbrakk>

   942     \<Longrightarrow> (\<integral>\<^sup>+ x. ereal (- f x) \<partial>M') \<le> ereal (B * \<bar>B'\<bar>)"

   943     using f_measurable by(auto intro!: bounded1 dest: f_bounded)

   944   have "AE M' in M. (\<integral>\<^sup>+ x. - f x \<partial>M') \<noteq> \<infinity>"

   945     using M_bounded by(rule AE_mp[OF _ AE_I2])(auto dest: f_neg1)

   946   hence [simp]: "(\<integral>\<^sup>+ M'. ereal (real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M')) \<partial>M) = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M)"

   947     by(rule nn_integral_cong_AE[OF AE_mp])(simp add: ereal_real nn_integral_nonneg)

   948   from f_neg have [simp]: "integrable M (\<lambda>M'. real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M'))"

   949     by(simp add: int_mf real_integrable_def nn_integral_nonneg real_of_ereal[symmetric] nn_integral_0_iff_AE[THEN iffD2] del: real_of_ereal)

   950

   951   from \<open>?integrable\<close>

   952   have "ereal (\<integral> x. f x \<partial>join M) = (\<integral>\<^sup>+ x. f x \<partial>join M) - (\<integral>\<^sup>+ x. - f x \<partial>join M)"

   953     by(simp add: real_lebesgue_integral_def ereal_minus(1)[symmetric] ereal_real nn_integral_nonneg f_pos f_neg del: ereal_minus(1))

   954   also note int_f

   955   also note int_mf

   956   also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) =

   957     ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)) -

   958     ((\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M))"

   959     by(subst (7 11) nn_integral_0_iff_AE[THEN iffD2])(simp_all add: nn_integral_nonneg)

   960   also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) = \<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M"

   961     using f_pos

   962     by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_f nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])

   963   also have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) - (\<integral>\<^sup>+ M'. - \<integral>\<^sup>+ x. - f x \<partial>M' \<partial>M) = \<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"

   964     using f_neg

   965     by(simp add: real_lebesgue_integral_def)(simp add: ereal_minus(1)[symmetric] ereal_real int_mf nn_integral_nonneg nn_integral_0_iff_AE[THEN iffD2] real_of_ereal_pos zero_ereal_def[symmetric])

   966   also note ereal_minus(1)

   967   also have "(\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') \<partial>M) - (\<integral> M'. real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M) =

   968     \<integral>M'. real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') \<partial>M"

   969     by simp

   970   also have "\<dots> = \<integral>M'. \<integral> x. f x \<partial>M' \<partial>M" using _ _ M_bounded

   971   proof(rule integral_cong_AE[OF _ _ AE_mp[OF _ AE_I2], rule_format])

   972     show "(\<lambda>M'. integral\<^sup>L M' f) \<in> borel_measurable M"

   973       by measurable(simp add: integral_measurable_subprob_algebra[OF _ f_bounded])

   974

   975     fix M'

   976     assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"

   977     then interpret finite_measure M' by(auto intro: finite_measureI)

   978

   979     from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]

   980     have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)

   981     hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)

   982     have "integrable M' f"

   983       by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)

   984     then show "real_of_ereal (\<integral>\<^sup>+ x. f x \<partial>M') - real_of_ereal (\<integral>\<^sup>+ x. - f x \<partial>M') = \<integral> x. f x \<partial>M'"

   985       by(simp add: real_lebesgue_integral_def)

   986   qed simp_all

   987   finally show ?integral by simp

   988 qed

   989

   990 lemma join_assoc:

   991   assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"

   992   shows "join (distr M (subprob_algebra N) join) = join (join M)"

   993 proof (rule measure_eqI)

   994   fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"

   995   then have A: "A \<in> sets N" by simp

   996   show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"

   997     using measurable_join[of N]

   998     by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg

   999                    sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]

  1000              intro!: nn_integral_cong emeasure_join)

  1001 qed (simp add: M)

  1002

  1003 lemma join_return:

  1004   assumes "sets M = sets N" and "subprob_space M"

  1005   shows "join (return (subprob_algebra N) M) = M"

  1006   by (rule measure_eqI)

  1007      (simp_all add: emeasure_join emeasure_nonneg space_subprob_algebra

  1008                     measurable_emeasure_subprob_algebra nn_integral_return assms)

  1009

  1010 lemma join_return':

  1011   assumes "sets N = sets M"

  1012   shows "join (distr M (subprob_algebra N) (return N)) = M"

  1013 apply (rule measure_eqI)

  1014 apply (simp add: assms)

  1015 apply (subgoal_tac "return N \<in> measurable M (subprob_algebra N)")

  1016 apply (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)

  1017 apply (subst measurable_cong_sets, rule assms[symmetric], rule refl, rule return_measurable)

  1018 done

  1019

  1020 lemma join_distr_distr:

  1021   fixes f :: "'a \<Rightarrow> 'b" and M :: "'a measure measure" and N :: "'b measure"

  1022   assumes "sets M = sets (subprob_algebra R)" and "f \<in> measurable R N"

  1023   shows "join (distr M (subprob_algebra N) (\<lambda>M. distr M N f)) = distr (join M) N f" (is "?r = ?l")

  1024 proof (rule measure_eqI)

  1025   fix A assume "A \<in> sets ?r"

  1026   hence A_in_N: "A \<in> sets N" by simp

  1027

  1028   from assms have "f \<in> measurable (join M) N"

  1029       by (simp cong: measurable_cong_sets)

  1030   moreover from assms and A_in_N have "f-A \<inter> space R \<in> sets R"

  1031       by (intro measurable_sets) simp_all

  1032   ultimately have "emeasure (distr (join M) N f) A = \<integral>\<^sup>+M'. emeasure M' (f-A \<inter> space R) \<partial>M"

  1033       by (simp_all add: A_in_N emeasure_distr emeasure_join assms)

  1034

  1035   also have "... = \<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M" using A_in_N

  1036   proof (intro nn_integral_cong, subst emeasure_distr)

  1037     fix M' assume "M' \<in> space M"

  1038     from assms have "space M = space (subprob_algebra R)"

  1039         using sets_eq_imp_space_eq by blast

  1040     with \<open>M' \<in> space M\<close> have [simp]: "sets M' = sets R" using space_subprob_algebra by blast

  1041     show "f \<in> measurable M' N" by (simp cong: measurable_cong_sets add: assms)

  1042     have "space M' = space R" by (rule sets_eq_imp_space_eq) simp

  1043     thus "emeasure M' (f - A \<inter> space R) = emeasure M' (f - A \<inter> space M')" by simp

  1044   qed

  1045

  1046   also have "(\<lambda>M. distr M N f) \<in> measurable M (subprob_algebra N)"

  1047       by (simp cong: measurable_cong_sets add: assms measurable_distr)

  1048   hence "(\<integral>\<^sup>+ x. emeasure (distr x N f) A \<partial>M) =

  1049              emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"

  1050       by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)

  1051   finally show "emeasure ?r A = emeasure ?l A" ..

  1052 qed simp

  1053

  1054 definition bind :: "'a measure \<Rightarrow> ('a \<Rightarrow> 'b measure) \<Rightarrow> 'b measure" where

  1055   "bind M f = (if space M = {} then count_space {} else

  1056     join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"

  1057

  1058 adhoc_overloading Monad_Syntax.bind bind

  1059

  1060 lemma bind_empty:

  1061   "space M = {} \<Longrightarrow> bind M f = count_space {}"

  1062   by (simp add: bind_def)

  1063

  1064 lemma bind_nonempty:

  1065   "space M \<noteq> {} \<Longrightarrow> bind M f = join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f)"

  1066   by (simp add: bind_def)

  1067

  1068 lemma sets_bind_empty: "sets M = {} \<Longrightarrow> sets (bind M f) = {{}}"

  1069   by (auto simp: bind_def)

  1070

  1071 lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"

  1072   by (simp add: bind_def)

  1073

  1074 lemma sets_bind[simp, measurable_cong]:

  1075   assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}"

  1076   shows "sets (bind M f) = sets N"

  1077   using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq)

  1078

  1079 lemma space_bind[simp]:

  1080   assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}"

  1081   shows "space (bind M f) = space N"

  1082   using assms by (intro sets_eq_imp_space_eq sets_bind)

  1083

  1084 lemma bind_cong:

  1085   assumes "\<forall>x \<in> space M. f x = g x"

  1086   shows "bind M f = bind M g"

  1087 proof (cases "space M = {}")

  1088   assume "space M \<noteq> {}"

  1089   hence "(SOME x. x \<in> space M) \<in> space M" by (rule_tac someI_ex) blast

  1090   with assms have "f (SOME x. x \<in> space M) = g (SOME x. x \<in> space M)" by blast

  1091   with \<open>space M \<noteq> {}\<close> and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)

  1092 qed (simp add: bind_empty)

  1093

  1094 lemma bind_nonempty':

  1095   assumes "f \<in> measurable M (subprob_algebra N)" "x \<in> space M"

  1096   shows "bind M f = join (distr M (subprob_algebra N) f)"

  1097   using assms

  1098   apply (subst bind_nonempty, blast)

  1099   apply (subst subprob_algebra_cong[OF sets_kernel[OF assms(1) someI_ex]], blast)

  1100   apply (simp add: subprob_algebra_cong[OF sets_kernel[OF assms]])

  1101   done

  1102

  1103 lemma bind_nonempty'':

  1104   assumes "f \<in> measurable M (subprob_algebra N)" "space M \<noteq> {}"

  1105   shows "bind M f = join (distr M (subprob_algebra N) f)"

  1106   using assms by (auto intro: bind_nonempty')

  1107

  1108 lemma emeasure_bind:

  1109     "\<lbrakk>space M \<noteq> {}; f \<in> measurable M (subprob_algebra N);X \<in> sets N\<rbrakk>

  1110       \<Longrightarrow> emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"

  1111   by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)

  1112

  1113 lemma nn_integral_bind:

  1114   assumes f: "f \<in> borel_measurable B"

  1115   assumes N: "N \<in> measurable M (subprob_algebra B)"

  1116   shows "(\<integral>\<^sup>+x. f x \<partial>(M \<bind> N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"

  1117 proof cases

  1118   assume M: "space M \<noteq> {}" show ?thesis

  1119     unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]

  1120     by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])

  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: emeasure_le_0_iff 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> ereal 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 _ f_bounded])

  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 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 = ereal (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. ereal (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)

  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 emeasure_nonneg)

  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 section \<open>Measures form a $\omega$-chain complete partial order\<close>

  1508

  1509 definition SUP_measure :: "(nat \<Rightarrow> 'a measure) \<Rightarrow> 'a measure" where

  1510   "SUP_measure M = measure_of (\<Union>i. space (M i)) (\<Union>i. sets (M i)) (\<lambda>A. SUP i. emeasure (M i) A)"

  1511

  1512 lemma

  1513   assumes const: "\<And>i j. sets (M i) = sets (M j)"

  1514   shows space_SUP_measure: "space (SUP_measure M) = space (M i)" (is ?sp)

  1515     and sets_SUP_measure: "sets (SUP_measure M) = sets (M i)" (is ?st)

  1516 proof -

  1517   have "(\<Union>i. sets (M i)) = sets (M i)"

  1518     using const by auto

  1519   moreover have "(\<Union>i. space (M i)) = space (M i)"

  1520     using const[THEN sets_eq_imp_space_eq] by auto

  1521   moreover have "\<And>i. sets (M i) \<subseteq> Pow (space (M i))"

  1522     by (auto dest: sets.sets_into_space)

  1523   ultimately show ?sp ?st

  1524     by (simp_all add: SUP_measure_def)

  1525 qed

  1526

  1527 lemma emeasure_SUP_measure:

  1528   assumes const: "\<And>i j. sets (M i) = sets (M j)"

  1529     and mono: "mono (\<lambda>i. emeasure (M i))"

  1530   shows "emeasure (SUP_measure M) A = (SUP i. emeasure (M i) A)"

  1531 proof cases

  1532   assume "A \<in> sets (SUP_measure M)"

  1533   show ?thesis

  1534   proof (rule emeasure_measure_of[OF SUP_measure_def])

  1535     show "countably_additive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"

  1536     proof (rule countably_additiveI)

  1537       fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (SUP_measure M)"

  1538       then have "\<And>i j. A i \<in> sets (M j)"

  1539         using sets_SUP_measure[of M, OF const] by simp

  1540       moreover assume "disjoint_family A"

  1541       ultimately show "(\<Sum>i. SUP ia. emeasure (M ia) (A i)) = (SUP i. emeasure (M i) (\<Union>i. A i))"

  1542         using mono by (subst suminf_SUP_eq) (auto simp: mono_def le_fun_def intro!: SUP_cong suminf_emeasure)

  1543     qed

  1544     show "positive (sets (SUP_measure M)) (\<lambda>A. SUP i. emeasure (M i) A)"

  1545       by (auto simp: positive_def intro: SUP_upper2)

  1546     show "(\<Union>i. sets (M i)) \<subseteq> Pow (\<Union>i. space (M i))"

  1547       using sets.sets_into_space by auto

  1548   qed fact

  1549 next

  1550   assume "A \<notin> sets (SUP_measure M)"

  1551   with sets_SUP_measure[of M, OF const] show ?thesis

  1552     by (simp add: emeasure_notin_sets)

  1553 qed

  1554

  1555 lemma bind_return'': "sets M = sets N \<Longrightarrow> M \<bind> return N = M"

  1556    by (cases "space M = {}")

  1557       (simp_all add: bind_empty space_empty[symmetric] bind_nonempty join_return'

  1558                 cong: subprob_algebra_cong)

  1559

  1560 lemma (in prob_space) distr_const[simp]:

  1561   "c \<in> space N \<Longrightarrow> distr M N (\<lambda>x. c) = return N c"

  1562   by (rule measure_eqI) (auto simp: emeasure_distr emeasure_space_1)

  1563

  1564 lemma return_count_space_eq_density:

  1565     "return (count_space M) x = density (count_space M) (indicator {x})"

  1566   by (rule measure_eqI)

  1567      (auto simp: indicator_inter_arith_ereal emeasure_density split: split_indicator)

  1568

  1569 lemma null_measure_in_space_subprob_algebra [simp]:

  1570   "null_measure M \<in> space (subprob_algebra M) \<longleftrightarrow> space M \<noteq> {}"

  1571 by(simp add: space_subprob_algebra subprob_space_null_measure_iff)

  1572

  1573 end
`