Quellcode-Bibliothek Giry_Monad.thy Sprache: Isabelle

(*  Title:      HOL/Probability/Giry_Monad.thy
    Author:     Johannes Hölzl, TU München
    Author:     Manuel Eberl, TU München

Defines subprobability spaces, the subprobability functor and the Giry monad on subprobability
spaces.
*)

section \<open>The Giry monad\<close>

theory Giry_Monad
  imports Probability_Measure "HOL-Library.Monad_Syntax"
begin

subsection \<open>Sub-probability spaces\<close>

locale subprob_space = finite_measure +
  assumes emeasure_space_le_1: "emeasure M (space M) \ 1"
  assumes subprob_not_empty: "space M \ {}"

lemma subprob_spaceI[Pure.intro!]:
  assumes *: "emeasure M (space M) \ 1"
  assumes "space M \ {}"
  shows "subprob_space M"
proof -
  interpret finite_measure M
  proof
    show "emeasure M (space M) \ \" using * by (auto simp: top_unique)
  qed
  show "subprob_space M" by standard fact+
qed

lemma (in subprob_space) emeasure_subprob_space_less_top: "emeasure M A \ top"
  by simp

lemma prob_space_imp_subprob_space:
  "prob_space M \ subprob_space M"
  by (rule subprob_spaceI) (simp_all add: prob_space.emeasure_space_1 prob_space.not_empty)

lemma subprob_space_imp_sigma_finite: "subprob_space M \ sigma_finite_measure M"
  unfolding subprob_space_def finite_measure_def by simp

sublocale prob_space \<subseteq> subprob_space
  by (rule subprob_spaceI) (simp_all add: emeasure_space_1 not_empty)

lemma subprob_space_sigma [simp]: "\ \ {} \ subprob_space (sigma \ X)"
  by(rule subprob_spaceI)(simp_all add: emeasure_sigma space_measure_of_conv)

lemma subprob_space_null_measure: "space M \ {} \ subprob_space (null_measure M)"
  by(simp add: null_measure_def)

lemma (in subprob_space) subprob_space_distr:
  assumes f: "f \ measurable M M'" and "space M' \ {}" shows "subprob_space (distr M M' f)"
proof (rule subprob_spaceI)
  have "f -` space M' \ space M = space M" using f by (auto dest: measurable_space)
  with f show "emeasure (distr M M' f) (space (distr M M' f)) \ 1"
    by (auto simp: emeasure_distr emeasure_space_le_1)
  show "space (distr M M' f) \ {}" by (simp add: assms)
qed

lemma (in subprob_space) subprob_emeasure_le_1: "emeasure M X \ 1"
  by (rule order.trans[OF emeasure_space emeasure_space_le_1])

lemma (in subprob_space) subprob_measure_le_1: "measure M X \ 1"
  using subprob_emeasure_le_1[of X] by (simp add: emeasure_eq_measure)

lemma (in subprob_space) nn_integral_le_const:
  assumes "0 \ c" "AE x in M. f x \ c"
  shows "(\\<^sup>+x. f x \M) \ c"
proof -
  have "(\\<^sup>+ x. f x \M) \ (\\<^sup>+ x. c \M)"
    by(rule nn_integral_mono_AE) fact
  also have "\ \ c * emeasure M (space M)"
    using \<open>0 \<le> c\<close> by simp
  also have "\ \ c * 1" using emeasure_space_le_1 \0 \ c\ by(rule mult_left_mono)
  finally show ?thesis by simp
qed

lemma emeasure_density_distr_interval:
  fixes h :: "real \ real" and g :: "real \ real" and g' :: "real \ real"
  assumes [simp]: "a \ b"
  assumes Mf[measurable]: "f \ borel_measurable borel"
  assumes Mg[measurable]: "g \ borel_measurable borel"
  assumes Mg'[measurable]: "g' \<in> borel_measurable borel"
  assumes Mh[measurable]: "h \ borel_measurable borel"
  assumes prob: "subprob_space (density lborel f)"
  assumes nonnegf: "\x. f x \ 0"
  assumes derivg: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)"
  assumes contg': "continuous_on {a..b} g'"
  assumes mono: "strict_mono_on {a..b} g" and inv: "\x. h x \ {a..b} \ g (h x) = x"
  assumes range: "{a..b} \ range h"
  shows "emeasure (distr (density lborel f) lborel h) {a..b} =
             emeasure (density lborel (\<lambda>x. f (g x) * g' x)) {a..b}"
proof (cases "a < b")
  assume "a < b"
  from mono have inj: "inj_on g {a..b}" by (rule strict_mono_on_imp_inj_on)
  from mono have mono': "mono_on {a..b} g" by (rule strict_mono_on_imp_mono_on)
  from mono' derivg have "\x. x \ {a<.. g' x \ 0"
    by (rule mono_on_imp_deriv_nonneg) auto
  from contg' this have derivg_nonneg: "\x. x \ {a..b} \ g' x \ 0"
    by (rule continuous_ge_on_Ioo) (simp_all add: \<open>a < b\<close>)

  from derivg have contg: "continuous_on {a..b} g" by (rule has_real_derivative_imp_continuous_on)
  have A: "h -` {a..b} = {g a..g b}"
  proof (intro equalityI subsetI)
    fix x assume x: "x \ h -` {a..b}"
    hence "g (h x) \ {g a..g b}" by (auto intro: mono_onD[OF mono'])
    with inv and x show "x \ {g a..g b}" by simp
  next
    fix y assume y: "y \ {g a..g b}"
    with IVT'[OF _ _ _ contg, of y] obtain x where "x \ {a..b}" "y = g x" by auto
    with range and inv show "y \ h -` {a..b}" by auto
  qed

  have prob': "subprob_space (distr (density lborel f) lborel h)"
    by (rule subprob_space.subprob_space_distr[OF prob]) (simp_all add: Mh)
  have B: "emeasure (distr (density lborel f) lborel h) {a..b} =
            \<integral>\<^sup>+x. f x * indicator (h -` {a..b}) x \<partial>lborel"
    by (subst emeasure_distr) (simp_all add: emeasure_density Mf Mh measurable_sets_borel[OF Mh])
  also note A
  also have "emeasure (distr (density lborel f) lborel h) {a..b} \ 1"
    by (rule subprob_space.subprob_emeasure_le_1) (rule prob')
  hence "emeasure (distr (density lborel f) lborel h) {a..b} \ \" by (auto simp: top_unique)
  with assms have "(\\<^sup>+x. f x * indicator {g a..g b} x \lborel) =
                      (\<integral>\<^sup>+x. f (g x) * g' x * indicator {a..b} x \<partial>lborel)"
    by (intro nn_integral_substitution_aux)
       (auto simp: derivg_nonneg A B emeasure_density mult.commute \<open>a < b\<close>)
  also have "... = emeasure (density lborel (\x. f (g x) * g' x)) {a..b}"
    by (simp add: emeasure_density)
  finally show ?thesis .
next
  assume "\a < b"
  with \<open>a \<le> b\<close> have [simp]: "b = a" by (simp add: not_less del: \<open>a \<le> b\<close>)
  from inv and range have "h -` {a} = {g a}" by auto
  thus ?thesis by (simp_all add: emeasure_distr emeasure_density measurable_sets_borel[OF Mh])
qed

locale pair_subprob_space =
  pair_sigma_finite M1 M2 + M1: subprob_space M1 + M2: subprob_space M2 for M1 M2

sublocale pair_subprob_space \<subseteq> P?: subprob_space "M1 \<Otimes>\<^sub>M M2"
proof
  from mult_le_one[OF M1.emeasure_space_le_1 _ M2.emeasure_space_le_1]
  show "emeasure (M1 \\<^sub>M M2) (space (M1 \\<^sub>M M2)) \ 1"
    by (simp add: M2.emeasure_pair_measure_Times space_pair_measure)
  from M1.subprob_not_empty and M2.subprob_not_empty show "space (M1 \\<^sub>M M2) \ {}"
    by (simp add: space_pair_measure)
qed

lemma subprob_space_null_measure_iff:
    "subprob_space (null_measure M) \ space M \ {}"
  by (auto intro!: subprob_spaceI dest: subprob_space.subprob_not_empty)

lemma subprob_space_restrict_space:
  assumes M: "subprob_space M"
  and A: "A \ space M \ sets M" "A \ space M \ {}"
  shows "subprob_space (restrict_space M A)"
proof(rule subprob_spaceI)
  have "emeasure (restrict_space M A) (space (restrict_space M A)) = emeasure M (A \ space M)"
    using A by(simp add: emeasure_restrict_space space_restrict_space)
  also have "\ \ 1" by(rule subprob_space.subprob_emeasure_le_1)(rule M)
  finally show "emeasure (restrict_space M A) (space (restrict_space M A)) \ 1" .
next
  show "space (restrict_space M A) \ {}"
    using A by(simp add: space_restrict_space)
qed

definition subprob_algebra :: "'a measure \ 'a measure measure" where
  "subprob_algebra K =
    (SUP A \<in> sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"

lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \ sets M = sets A}"
  by (auto simp add: subprob_algebra_def space_Sup_eq_UN)

lemma subprob_algebra_cong: "sets M = sets N \ subprob_algebra M = subprob_algebra N"
  by (simp add: subprob_algebra_def)

lemma measurable_emeasure_subprob_algebra[measurable]:
  "a \ sets A \ (\M. emeasure M a) \ borel_measurable (subprob_algebra A)"
  by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: subprob_algebra_def)

lemma measurable_measure_subprob_algebra[measurable]:
  "a \ sets A \ (\M. measure M a) \ borel_measurable (subprob_algebra A)"
  unfolding measure_def by measurable

lemma subprob_measurableD:
  assumes N: "N \ measurable M (subprob_algebra S)" and x: "x \ space M"
  shows "space (N x) = space S"
    and "sets (N x) = sets S"
    and "measurable (N x) K = measurable S K"
    and "measurable K (N x) = measurable K S"
  using measurable_space[OF N x]
  by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)

ML \<open>

fun subprob_cong thm ctxt = (
  let
    val thm' = Thm.transfer' ctxt thm
    val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
      dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
  in
    if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)
            else ([], ctxt)
  end
  handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))

\<close>

setup \<open>
  Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
\<close>

context
  fixes K M N assumes K: "K \ measurable M (subprob_algebra N)"
begin

lemma subprob_space_kernel: "a \ space M \ subprob_space (K a)"
  using measurable_space[OF K] by (simp add: space_subprob_algebra)

lemma sets_kernel: "a \ space M \ sets (K a) = sets N"
  using measurable_space[OF K] by (simp add: space_subprob_algebra)

lemma measurable_emeasure_kernel[measurable]:
    "A \ sets N \ (\a. emeasure (K a) A) \ borel_measurable M"
  using measurable_compose[OF K measurable_emeasure_subprob_algebra] .

end

lemma measurable_subprob_algebra:
  "(\a. a \ space M \ subprob_space (K a)) \
  (\<And>a. a \<in> space M \<Longrightarrow> sets (K a) = sets N) \<Longrightarrow>
  (\<And>A. A \<in> sets N \<Longrightarrow> (\<lambda>a. emeasure (K a) A) \<in> borel_measurable M) \<Longrightarrow>
  K \<in> measurable M (subprob_algebra N)"
  by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: subprob_algebra_def)

lemma measurable_submarkov:
  "K \ measurable M (subprob_algebra M) \
    (\<forall>x\<in>space M. subprob_space (K x) \<and> sets (K x) = sets M) \<and>
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> measurable M borel)"
proof
  assume "(\x\space M. subprob_space (K x) \ sets (K x) = sets M) \
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
  then show "K \ measurable M (subprob_algebra M)"
    by (intro measurable_subprob_algebra) auto
next
  assume "K \ measurable M (subprob_algebra M)"
  then show "(\x\space M. subprob_space (K x) \ sets (K x) = sets M) \
    (\<forall>A\<in>sets M. (\<lambda>x. emeasure (K x) A) \<in> borel_measurable M)"
    by (auto dest: subprob_space_kernel sets_kernel)
qed

lemma measurable_subprob_algebra_generated:
  assumes eq: "sets N = sigma_sets \ G" and "Int_stable G" "G \ Pow \"
  assumes subsp: "\a. a \ space M \ subprob_space (K a)"
  assumes sets: "\a. a \ space M \ sets (K a) = sets N"
  assumes "\A. A \ G \ (\a. emeasure (K a) A) \ borel_measurable M"
  assumes \<Omega>: "(\<lambda>a. emeasure (K a) \<Omega>) \<in> borel_measurable M"
  shows "K \ measurable M (subprob_algebra N)"
proof (rule measurable_subprob_algebra)
  fix a assume "a \ space M" then show "subprob_space (K a)" "sets (K a) = sets N" by fact+
next
  interpret G: sigma_algebra \<Omega> "sigma_sets \<Omega> G"
    using \<open>G \<subseteq> Pow \<Omega>\<close> by (rule sigma_algebra_sigma_sets)
  fix A assume "A \ sets N" with assms(2,3) show "(\a. emeasure (K a) A) \ borel_measurable M"
    unfolding \<open>sets N = sigma_sets \<Omega> G\<close>
  proof (induction rule: sigma_sets_induct_disjoint)
    case (basic A) then show ?case by fact
  next
    case empty then show ?case by simp
  next
    case (compl A)
    have "(\a. emeasure (K a) (\ - A)) \ borel_measurable M \
      (\<lambda>a. emeasure (K a) \<Omega> - emeasure (K a) A) \<in> borel_measurable M"
      using G.top G.sets_into_space sets eq compl subprob_space.emeasure_subprob_space_less_top[OF subsp]
      by (intro measurable_cong emeasure_Diff) auto
    with compl \<Omega> show ?case
      by simp
  next
    case (union F)
    moreover have "(\a. emeasure (K a) (\i. F i)) \ borel_measurable M \
        (\<lambda>a. \<Sum>i. emeasure (K a) (F i)) \<in> borel_measurable M"
      using sets union eq
      by (intro measurable_cong suminf_emeasure[symmetric]) auto
    ultimately show ?case
      by auto
  qed
qed

lemma space_subprob_algebra_empty_iff:
  "space (subprob_algebra N) = {} \ space N = {}"
proof
  have "\x. x \ space N \ density N (\_. 0) \ space (subprob_algebra N)"
    by (auto simp: space_subprob_algebra emeasure_density intro!: subprob_spaceI)
  then show "space (subprob_algebra N) = {} \ space N = {}"
    by auto
next
  assume "space N = {}"
  hence "sets N = {{}}" by (simp add: space_empty_iff)
  moreover have "\M. subprob_space M \ sets M \ {{}}"
    by (simp add: subprob_space.subprob_not_empty space_empty_iff[symmetric])
  ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
qed

lemma nn_integral_measurable_subprob_algebra[measurable]:
  assumes f: "f \ borel_measurable N"
  shows "(\M. integral\<^sup>N M f) \ borel_measurable (subprob_algebra N)" (is "_ \ ?B")
  using f
proof induct
  case (cong f g)
  moreover have "(\M'. \\<^sup>+M''. f M'' \M') \ ?B \ (\M'. \\<^sup>+M''. g M'' \M') \ ?B"
    by (intro measurable_cong nn_integral_cong cong)
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
  ultimately show ?case by simp
next
  case (set B)
  then have "(\M'. \\<^sup>+M''. indicator B M'' \M') \ ?B \ (\M'. emeasure M' B) \ ?B"
    by (intro measurable_cong nn_integral_indicator) (simp add: space_subprob_algebra)
  with set show ?case
    by (simp add: measurable_emeasure_subprob_algebra)
next
  case (mult f c)
  then have "(\M'. \\<^sup>+M''. c * f M'' \M') \ ?B \ (\M'. c * \\<^sup>+M''. f M'' \M') \ ?B"
    by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
  with mult show ?case
    by simp
next
  case (add f g)
  then have "(\M'. \\<^sup>+M''. f M'' + g M'' \M') \ ?B \ (\M'. (\\<^sup>+M''. f M'' \M') + (\\<^sup>+M''. g M'' \M')) \ ?B"
    by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
  with add show ?case
    by (simp add: ac_simps)
next
  case (seq F)
  then have "(\M'. \\<^sup>+M''. (SUP i. F i) M'' \M') \ ?B \ (\M'. SUP i. (\\<^sup>+M''. F i M'' \M')) \ ?B"
    unfolding SUP_apply
    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
  with seq show ?case
    by (simp add: ac_simps)
qed

lemma measurable_distr:
  assumes [measurable]: "f \ measurable M N"
  shows "(\M'. distr M' N f) \ measurable (subprob_algebra M) (subprob_algebra N)"
proof (cases "space N = {}")
  case False
  show ?thesis
  proof (rule measurable_subprob_algebra)
    fix A assume A: "A \ sets N"
    then have "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M) \
      (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
      by (intro measurable_cong)
         (auto simp: emeasure_distr space_subprob_algebra
               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="(\)"])
    also have "\"
      using A by (intro measurable_emeasure_subprob_algebra) simp
    finally show "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M)" .
  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra False cong: measurable_cong_sets)
qed (use assms in \<open>auto simp: measurable_empty_iff space_subprob_algebra_empty_iff\<close>)

lemma emeasure_space_subprob_algebra[measurable]:
  "(\a. emeasure a (space a)) \ borel_measurable (subprob_algebra N)"
proof-
  have "(\a. emeasure a (space N)) \ borel_measurable (subprob_algebra N)" (is "?f \ ?M")
    by (rule measurable_emeasure_subprob_algebra) simp
  also have "?f \ ?M \ (\a. emeasure a (space a)) \ ?M"
    by (rule measurable_cong) (auto simp: space_subprob_algebra dest: sets_eq_imp_space_eq)
  finally show ?thesis .
qed

lemma integrable_measurable_subprob_algebra[measurable]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes [measurable]: "f \ borel_measurable N"
  shows "Measurable.pred (subprob_algebra N) (\M. integrable M f)"
proof (rule measurable_cong[THEN iffD2])
  show "M \ space (subprob_algebra N) \ integrable M f \ (\\<^sup>+x. norm (f x) \M) < \" for M
    by (auto simp: space_subprob_algebra integrable_iff_bounded)
qed measurable

lemma integral_measurable_subprob_algebra[measurable]:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes f [measurable]: "f \ borel_measurable N"
  shows "(\M. integral\<^sup>L M f) \ subprob_algebra N \\<^sub>M borel"
proof -
  from borel_measurable_implies_sequence_metric[OF f, of 0]
  obtain F where F: "\i. simple_function N (F i)"
    "\x. x \ space N \ (\i. F i x) \ f x"
    "\i x. x \ space N \ norm (F i x) \ 2 * norm (f x)"
    unfolding norm_conv_dist by blast

  have [measurable]: "F i \ N \\<^sub>M count_space UNIV" for i
    using F(1) by (rule measurable_simple_function)

  define F' where [abs_def]:
    "F' M i = (if integrable M f then integral\<^sup>L M (F i) else 0)" for M i

  have "(\M. F' M i) \ subprob_algebra N \\<^sub>M borel" for i
  proof (rule measurable_cong[THEN iffD2])
    fix M assume "M \ space (subprob_algebra N)"
    then have [simp]: "sets M = sets N" "space M = space N" "subprob_space M"
      by (auto simp: space_subprob_algebra intro!: sets_eq_imp_space_eq)
    interpret subprob_space M by fact
    have "F' M i = (if integrable M f then Bochner_Integration.simple_bochner_integral M (F i) else 0)"
      using F(1)
      by (subst simple_bochner_integrable_eq_integral)
         (auto simp: simple_bochner_integrable.simps simple_function_def F'_def)
    then show "F' M i = (if integrable M f then \y\F i ` space N. measure M {x\space N. F i x = y} *\<^sub>R y else 0)"
      unfolding simple_bochner_integral_def by simp
  qed measurable
  moreover
  have "F' M \ integral\<^sup>L M f" if M: "M \ space (subprob_algebra N)" for M
  proof cases
    from M have [simp]: "sets M = sets N" "space M = space N"
      by (auto simp: space_subprob_algebra intro!: sets_eq_imp_space_eq)
    assume "integrable M f" then show ?thesis
      unfolding F'_def using F(1)[THEN borel_measurable_simple_function] F
      by (auto intro!: integral_dominated_convergence[where w="\x. 2 * norm (f x)"]
               cong: measurable_cong_sets)
  qed (auto simp: F'_def not_integrable_integral_eq)
  ultimately show ?thesis
    by (rule borel_measurable_LIMSEQ_metric)
qed

(* TODO: Rename. This name is too general -- Manuel *)
lemma measurable_pair_measure:
  assumes f: "f \ measurable M (subprob_algebra N)"
  assumes g: "g \ measurable M (subprob_algebra L)"
  shows "(\x. f x \\<^sub>M g x) \ measurable M (subprob_algebra (N \\<^sub>M L))"
proof (rule measurable_subprob_algebra)
  { fix x assume "x \ space M"
    with measurable_space[OF f] measurable_space[OF g]
    have fx: "f x \ space (subprob_algebra N)" and gx: "g x \ space (subprob_algebra L)"
      by auto
    interpret F: subprob_space "f x"
      using fx by (simp add: space_subprob_algebra)
    interpret G: subprob_space "g x"
      using gx by (simp add: space_subprob_algebra)

    interpret pair_subprob_space "f x" "g x" ..
    show "subprob_space (f x \\<^sub>M g x)" by unfold_locales
    show sets_eq: "sets (f x \\<^sub>M g x) = sets (N \\<^sub>M L)"
      using fx gx by (simp add: space_subprob_algebra)

    have 1: "\A B. A \ sets N \ B \ sets L \ emeasure (f x \\<^sub>M g x) (A \ B) = emeasure (f x) A * emeasure (g x) B"
      using fx gx by (intro G.emeasure_pair_measure_Times) (auto simp: space_subprob_algebra)
    have "emeasure (f x \\<^sub>M g x) (space (f x \\<^sub>M g x)) =
              emeasure (f x) (space (f x)) * emeasure (g x) (space (g x))"
      by (subst G.emeasure_pair_measure_Times[symmetric]) (simp_all add: space_pair_measure)
    hence 2: "\A. A \ sets (N \\<^sub>M L) \ emeasure (f x \\<^sub>M g x) (space N \ space L - A) =
                                             ... - emeasure (f x \<Otimes>\<^sub>M g x) A"
      using emeasure_compl[simplified, OF _ P.emeasure_finite]
      unfolding sets_eq
      unfolding sets_eq_imp_space_eq[OF sets_eq]
      by (simp add: space_pair_measure G.emeasure_pair_measure_Times)
    note 1 2 sets_eq }
  note Times = this(1) and Compl = this(2) and sets_eq = this(3)

  fix A assume A: "A \ sets (N \\<^sub>M L)"
  show "(\a. emeasure (f a \\<^sub>M g a) A) \ borel_measurable M"
    using Int_stable_pair_measure_generator pair_measure_closed A
    unfolding sets_pair_measure
  proof (induct A rule: sigma_sets_induct_disjoint)
    case (basic A) then show ?case
      by (auto intro!: borel_measurable_times_ennreal simp: Times cong: measurable_cong)
         (auto intro!: measurable_emeasure_kernel f g)
  next
    case (compl A)
    then have A: "A \ sets (N \\<^sub>M L)"
      by (auto simp: sets_pair_measure)
    have "(\x. emeasure (f x) (space (f x)) * emeasure (g x) (space (g x)) -
                   emeasure (f x \<Otimes>\<^sub>M g x) A) \<in> borel_measurable M" (is "?f \<in> ?M")
      using compl(2) f g by measurable
    thus ?case by (simp add: Compl A cong: measurable_cong)
  next
    case (union A)
    then have "range A \ sets (N \\<^sub>M L)" "disjoint_family A"
      by (auto simp: sets_pair_measure)
    then have "(\a. emeasure (f a \\<^sub>M g a) (\i. A i)) \ borel_measurable M \
      (\<lambda>a. \<Sum>i. emeasure (f a \<Otimes>\<^sub>M g a) (A i)) \<in> borel_measurable M"
      by (intro measurable_cong suminf_emeasure[symmetric])
         (auto simp: sets_eq)
    also have "\"
      using union by auto
    finally show ?case .
  qed simp
qed

lemma restrict_space_measurable:
  assumes X: "X \ {}" "X \ sets K"
  assumes N: "N \ measurable M (subprob_algebra K)"
  shows "(\x. restrict_space (N x) X) \ measurable M (subprob_algebra (restrict_space K X))"
proof (rule measurable_subprob_algebra)
  fix a assume a: "a \ space M"
  from N[THEN measurable_space, OF this]
  have "subprob_space (N a)" and [simp]: "sets (N a) = sets K" "space (N a) = space K"
    by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
  then interpret subprob_space "N a"
    by simp
  show "subprob_space (restrict_space (N a) X)"
  proof
    show "space (restrict_space (N a) X) \ {}"
      using X by (auto simp add: space_restrict_space)
    show "emeasure (restrict_space (N a) X) (space (restrict_space (N a) X)) \ 1"
      using X by (simp add: emeasure_restrict_space space_restrict_space subprob_emeasure_le_1)
  qed
  show "sets (restrict_space (N a) X) = sets (restrict_space K X)"
    by (intro sets_restrict_space_cong) fact
next
  fix A assume A: "A \ sets (restrict_space K X)"
  show "(\a. emeasure (restrict_space (N a) X) A) \ borel_measurable M"
  proof (subst measurable_cong)
    fix a assume "a \ space M"
    from N[THEN measurable_space, OF this]
    have [simp]: "sets (N a) = sets K" "space (N a) = space K"
      by (auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
    show "emeasure (restrict_space (N a) X) A = emeasure (N a) (A \ X)"
      using X A by (subst emeasure_restrict_space) (auto simp add: sets_restrict_space ac_simps)
  next
    show "(\w. emeasure (N w) (A \ X)) \ borel_measurable M"
      using A X
      by (intro measurable_compose[OF N measurable_emeasure_subprob_algebra])
         (auto simp: sets_restrict_space)
  qed
qed

subsection \<open>Properties of ``return''\<close>

definition return :: "'a measure \ 'a \ 'a measure" where
  "return R x = measure_of (space R) (sets R) (\A. indicator A x)"

lemma space_return[simp]: "space (return M x) = space M"
  by (simp add: return_def)

lemma sets_return[simp]: "sets (return M x) = sets M"
  by (simp add: return_def)

lemma measurable_return1[simp]: "measurable (return N x) L = measurable N L"
  by (simp cong: measurable_cong_sets)

lemma measurable_return2[simp]: "measurable L (return N x) = measurable L N"
  by (simp cong: measurable_cong_sets)

lemma return_sets_cong: "sets M = sets N \ return M = return N"
  by (auto dest: sets_eq_imp_space_eq simp: fun_eq_iff return_def)

lemma return_cong: "sets A = sets B \ return A x = return B x"
  by (auto simp add: return_def dest: sets_eq_imp_space_eq)

lemma emeasure_return[simp]:
  assumes "A \ sets M"
  shows "emeasure (return M x) A = indicator A x"
proof (rule emeasure_measure_of[OF return_def])
  show "sets M \ Pow (space M)" by (rule sets.space_closed)
  show "positive (sets (return M x)) (\A. indicator A x)" by (simp add: positive_def)
  from assms show "A \ sets (return M x)" unfolding return_def by simp
  show "countably_additive (sets (return M x)) (\A. indicator A x)"
    by (auto intro!: countably_additiveI suminf_indicator)
qed

lemma prob_space_return: "x \ space M \ prob_space (return M x)"
  by rule simp

lemma subprob_space_return: "x \ space M \ subprob_space (return M x)"
  by (intro prob_space_return prob_space_imp_subprob_space)

lemma subprob_space_return_ne:
  assumes "space M \ {}" shows "subprob_space (return M x)"
  by (metis assms emeasure_return indicator_simps(2) sets.top space_return subprob_spaceI subprob_space_return zero_le)

lemma measure_return: assumes X: "X \ sets M" shows "measure (return M x) X = indicator X x"
  unfolding measure_def emeasure_return[OF X, of x] by (simp split: split_indicator)

lemma AE_return:
  assumes [simp]: "x \ space M" and [measurable]: "Measurable.pred M P"
  shows "(AE y in return M x. P y) \ P x"
proof -
  have "(AE y in return M x. y \ {x\space M. \ P x}) \ P x"
    by (subst AE_iff_null_sets[symmetric]) (simp_all add: null_sets_def split: split_indicator)
  also have "(AE y in return M x. y \ {x\space M. \ P x}) \ (AE y in return M x. P y)"
    by (rule AE_cong) auto
  finally show ?thesis .
qed

lemma nn_integral_return:
  assumes "x \ space M" "g \ borel_measurable M"
  shows "(\\<^sup>+ a. g a \return M x) = g x"
proof-
  interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>])
  have "(\\<^sup>+ a. g a \return M x) = (\\<^sup>+ a. g x \return M x)" using assms
    by (intro nn_integral_cong_AE) (auto simp: AE_return)
  also have "... = g x"
    using nn_integral_const[of "return M x"] emeasure_space_1 by simp
  finally show ?thesis .
qed

lemma integral_return:
  fixes g :: "_ \ 'a :: {banach, second_countable_topology}"
  assumes "x \ space M" "g \ borel_measurable M"
  shows "(\a. g a \return M x) = g x"
proof-
  interpret prob_space "return M x" by (rule prob_space_return[OF \<open>x \<in> space M\<close>])
  have "(\a. g a \return M x) = (\a. g x \return M x)" using assms
    by (intro integral_cong_AE) (auto simp: AE_return)
  then show ?thesis
    using prob_space by simp
qed

lemma return_measurable[measurable]: "return N \ measurable N (subprob_algebra N)"
  by (rule measurable_subprob_algebra) (auto simp: subprob_space_return)

lemma distr_return:
  assumes "f \ measurable M N" and "x \ space M"
  shows "distr (return M x) N f = return N (f x)"
  using assms by (intro measure_eqI) (simp_all add: indicator_def emeasure_distr)

lemma return_restrict_space:
  "\ \ sets M \ return (restrict_space M \) x = restrict_space (return M x) \"
  by (auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space)

lemma measurable_distr2:
  assumes f[measurable]: "case_prod f \ measurable (L \\<^sub>M M) N"
  assumes g[measurable]: "g \ measurable L (subprob_algebra M)"
  shows "(\x. distr (g x) N (f x)) \ measurable L (subprob_algebra N)"
proof -
  have "(\x. distr (g x) N (f x)) \ measurable L (subprob_algebra N)
    \<longleftrightarrow> (\<lambda>x. distr (return L x \<Otimes>\<^sub>M g x) N (case_prod f)) \<in> measurable L (subprob_algebra N)"
  proof (rule measurable_cong)
    fix x assume x: "x \ space L"
    have gx: "g x \ space (subprob_algebra M)"
      using measurable_space[OF g x] .
    then have [simp]: "sets (g x) = sets M"
      by (simp add: space_subprob_algebra)
    then have [simp]: "space (g x) = space M"
      by (rule sets_eq_imp_space_eq)
    let ?R = "return L x"
    from measurable_compose_Pair1[OF x f] have f_M': "f x \ measurable M N"
      by simp
    interpret subprob_space "g x"
      using gx by (simp add: space_subprob_algebra)
    have space_pair_M'[simp]: "\X. space (X \\<^sub>M g x) = space (X \\<^sub>M M)"
      by (simp add: space_pair_measure)
    show "distr (g x) N (f x) = distr (?R \\<^sub>M g x) N (case_prod f)" (is "?l = ?r")
    proof (rule measure_eqI)
      show "sets ?l = sets ?r"
        by simp
    next
      fix A assume "A \ sets ?l"
      then have A[measurable]: "A \ sets N"
        by simp
      then have "emeasure ?r A = emeasure (?R \\<^sub>M g x) ((\(x, y). f x y) -` A \ space (?R \\<^sub>M g x))"
        by (auto simp add: emeasure_distr f_M' cong: measurable_cong_sets)
      also have "\ = (\\<^sup>+M''. emeasure (g x) (f M'' -` A \ space M) \?R)"
        apply (subst emeasure_pair_measure_alt)
        apply (force simp add: f_M' cong: measurable_cong_sets intro!: measurable_sets[OF _ A])
        apply (intro nn_integral_cong arg_cong[where f="emeasure (g x)"])
        apply (auto simp: space_subprob_algebra space_pair_measure)
        done
      also have "\ = emeasure (g x) (f x -` A \ space M)"
        by (subst nn_integral_return)
           (auto simp: x intro!: measurable_emeasure)
      also have "\ = emeasure ?l A"
        by (simp add: emeasure_distr f_M' cong: measurable_cong_sets)
      finally show "emeasure ?l A = emeasure ?r A" ..
    qed
  qed
  also have "\"
  proof (intro measurable_compose[OF measurable_pair_measure measurable_distr])
    show "return L \ L \\<^sub>M subprob_algebra L"
      by (rule return_measurable)
  qed measurable
  finally show ?thesis .
qed

lemma nn_integral_measurable_subprob_algebra2:
  assumes f[measurable]: "(\(x, y). f x y) \ borel_measurable (M \\<^sub>M N)"
  assumes N[measurable]: "L \ measurable M (subprob_algebra N)"
  shows "(\x. integral\<^sup>N (L x) (f x)) \ borel_measurable M"
proof -
  note nn_integral_measurable_subprob_algebra[measurable]
  note measurable_distr2[measurable]
  have "(\x. integral\<^sup>N (distr (L x) (M \\<^sub>M N) (\y. (x, y))) (\(x, y). f x y)) \ borel_measurable M"
    by measurable
  then show "(\x. integral\<^sup>N (L x) (f x)) \ borel_measurable M"
    by (rule measurable_cong[THEN iffD1, rotated])
       (simp add: nn_integral_distr)
qed

lemma emeasure_measurable_subprob_algebra2:
  assumes A[measurable]: "(SIGMA x:space M. A x) \ sets (M \\<^sub>M N)"
  assumes L[measurable]: "L \ measurable M (subprob_algebra N)"
  shows "(\x. emeasure (L x) (A x)) \ borel_measurable M"
proof -
  { fix x assume "x \ space M"
    then have "Pair x -` Sigma (space M) A = A x"
      by auto
    with sets_Pair1[OF A, of x] have "A x \ sets N"
      by auto }
  note ** = this

  have *: "\x. fst x \ space M \ snd x \ A (fst x) \ x \ (SIGMA x:space M. A x)"
    by (auto simp: fun_eq_iff)
  have MN: "Measurable.pred (M \\<^sub>M N) (\w. w \ Sigma (space M) A)"
    by auto
  then have "(\(x, y). indicator (A x) y::ennreal) \ borel_measurable (M \\<^sub>M N)"
    apply measurable
    by (smt (verit, best) MN measurable_cong mem_Sigma_iff prod.collapse space_pair_measure)
  then have "(\x. integral\<^sup>N (L x) (indicator (A x))) \ borel_measurable M"
    by (intro nn_integral_measurable_subprob_algebra2[where N=N] L)
  then show "(\x. emeasure (L x) (A x)) \ borel_measurable M"
    by (smt (verit) "**" L measurable_cong_simp nn_integral_indicator sets_kernel)
qed

lemma measure_measurable_subprob_algebra2:
  assumes A[measurable]: "(SIGMA x:space M. A x) \ sets (M \\<^sub>M N)"
  assumes L[measurable]: "L \ measurable M (subprob_algebra N)"
  shows "(\x. measure (L x) (A x)) \ borel_measurable M"
  unfolding measure_def
  by (intro borel_measurable_enn2real emeasure_measurable_subprob_algebra2[OF assms])

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

lemma select_sets1:
  "sets M = sets (subprob_algebra N) \ sets M = sets (subprob_algebra (select_sets M))"
  unfolding select_sets_def by (rule someI)

lemma sets_select_sets[simp]:
  assumes sets: "sets M = sets (subprob_algebra N)"
  shows "sets (select_sets M) = sets N"
  unfolding select_sets_def
proof (rule someI2)
  show "sets M = sets (subprob_algebra N)"
    by fact
next
  fix L assume "sets M = sets (subprob_algebra L)"
  with sets have eq: "space (subprob_algebra N) = space (subprob_algebra L)"
    by (intro sets_eq_imp_space_eq) simp
  show "sets L = sets N"
  proof cases
    assume "space (subprob_algebra N) = {}"
    with space_subprob_algebra_empty_iff[of N] space_subprob_algebra_empty_iff[of L]
    show ?thesis
      by (simp add: eq space_empty_iff)
  next
    assume "space (subprob_algebra N) \ {}"
    with eq show ?thesis
      by (smt (verit) equals0I mem_Collect_eq space_subprob_algebra)
  qed
qed

lemma space_select_sets[simp]:
  "sets M = sets (subprob_algebra N) \ space (select_sets M) = space N"
  by (intro sets_eq_imp_space_eq sets_select_sets)

subsection \<open>Join\<close>

definition join :: "'a measure measure \ 'a measure" where
  "join M = measure_of (space (select_sets M)) (sets (select_sets M)) (\B. \\<^sup>+ M'. emeasure M' B \M)"

lemma
  shows space_join[simp]: "space (join M) = space (select_sets M)"
    and sets_join[simp]: "sets (join M) = sets (select_sets M)"
  by (simp_all add: join_def)

lemma emeasure_join:
  assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \ sets N"
  shows "emeasure (join M) A = (\\<^sup>+ M'. emeasure M' A \M)"
proof (rule emeasure_measure_of[OF join_def])
  show "countably_additive (sets (join M)) (\B. \\<^sup>+ M'. emeasure M' B \M)"
  proof (rule countably_additiveI)
    fix A :: "nat \ 'a set" assume A: "range A \ sets (join M)" "disjoint_family A"
    have "(\i. \\<^sup>+ M'. emeasure M' (A i) \M) = (\\<^sup>+M'. (\i. emeasure M' (A i)) \M)"
      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)
    also have "\ = (\\<^sup>+M'. emeasure M' (\i. A i) \M)"
    proof (rule nn_integral_cong)
      fix M' assume "M' \<in> space M"
      then show "(\i. emeasure M' (A i)) = emeasure M' (\i. A i)"
        using A sets_eq_imp_space_eq[OF M] by (simp add: suminf_emeasure space_subprob_algebra)
    qed
    finally show "(\i. \\<^sup>+M'. emeasure M' (A i) \M) = (\\<^sup>+M'. emeasure M' (\i. A i) \M)" .
  qed
qed (auto simp: A sets.space_closed positive_def)

lemma measurable_join:
  "join \ measurable (subprob_algebra (subprob_algebra N)) (subprob_algebra N)"
proof (cases "space N \ {}", rule measurable_subprob_algebra)
  fix A assume "A \ sets N"
  let ?B = "borel_measurable (subprob_algebra (subprob_algebra N))"
  have "(\M'. emeasure (join M') A) \ ?B \ (\M'. (\\<^sup>+ M''. emeasure M'' A \M')) \ ?B"
  proof (rule measurable_cong)
    fix M' assume "M' \<in> space (subprob_algebra (subprob_algebra N))"
    then show "emeasure (join M') A = (\\<^sup>+ M''. emeasure M'' A \M')"
      by (intro emeasure_join) (auto simp: space_subprob_algebra \<open>A\<in>sets N\<close>)
  qed
  also have "(\M'. \\<^sup>+M''. emeasure M'' A \M') \ ?B"
    using measurable_emeasure_subprob_algebra[OF \<open>A\<in>sets N\<close>]
    by (rule nn_integral_measurable_subprob_algebra)
  finally show "(\M'. emeasure (join M') A) \ borel_measurable (subprob_algebra (subprob_algebra N))" .
next
  assume [simp]: "space N \ {}"
  fix M assume M: "M \ space (subprob_algebra (subprob_algebra N))"
  then have "(\\<^sup>+M'. emeasure M' (space N) \M) \ (\\<^sup>+M'. 1 \M)"
  proof (intro nn_integral_mono)
    show "\x. \M \ space (subprob_algebra (subprob_algebra N)); x \ space M\
         \<Longrightarrow> emeasure x (space N) \<le> 1"
      by (smt (verit) mem_Collect_eq sets_eq_imp_space_eq space_subprob_algebra subprob_space.subprob_emeasure_le_1)
  qed
  with M show "subprob_space (join M)"
    by (intro subprob_spaceI)
       (auto simp: emeasure_join space_subprob_algebra M dest: subprob_space.emeasure_space_le_1)
next
  assume "\(space N \ {})"
  thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
qed (auto simp: space_subprob_algebra)

lemma nn_integral_join:
  assumes f: "f \ borel_measurable N"
    and M[measurable_cong]: "sets M = sets (subprob_algebra N)"
  shows "(\\<^sup>+x. f x \join M) = (\\<^sup>+M'. \\<^sup>+x. f x \M' \M)"
  using f
proof induct
  case (cong f g)
  moreover have "integral\<^sup>N (join M) f = integral\<^sup>N (join M) g"
    by (intro nn_integral_cong cong) (simp add: M)
  moreover from M have "(\\<^sup>+ M'. integral\<^sup>N M' f \M) = (\\<^sup>+ M'. integral\<^sup>N M' g \M)"
    by (intro nn_integral_cong cong)
       (auto simp add: space_subprob_algebra dest!: sets_eq_imp_space_eq)
  ultimately show ?case
    by simp
next
  case (set A)
  with M have "(\\<^sup>+ M'. integral\<^sup>N M' (indicator A) \M) = (\\<^sup>+ M'. emeasure M' A \M)"
    by (intro nn_integral_cong nn_integral_indicator)
       (auto simp: space_subprob_algebra dest!: sets_eq_imp_space_eq)
  with set show ?case
    using M by (simp add: emeasure_join)
next
  case (mult f c)
  have "(\\<^sup>+ M'. \\<^sup>+ x. c * f x \M' \M) = (\\<^sup>+ M'. c * \\<^sup>+ x. f x \M' \M)"
    using mult M M[THEN sets_eq_imp_space_eq]
    by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
  also have "\ = c * (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)"
    using nn_integral_measurable_subprob_algebra[OF mult(2)]
    by (intro nn_integral_cmult mult) (simp add: M)
  also have "\ = c * (integral\<^sup>N (join M) f)"
    by (simp add: mult)
  also have "\ = (\\<^sup>+ x. c * f x \join M)"
    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)
  finally show ?case by simp
next
  case (add f g)
  have "(\\<^sup>+ M'. \\<^sup>+ x. f x + g x \M' \M) = (\\<^sup>+ M'. (\\<^sup>+ x. f x \M') + (\\<^sup>+ x. g x \M') \M)"
    using add M M[THEN sets_eq_imp_space_eq]
    by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)
  also have "\ = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) + (\\<^sup>+ M'. \\<^sup>+ x. g x \M' \M)"
    using nn_integral_measurable_subprob_algebra[OF add(1)]
    using nn_integral_measurable_subprob_algebra[OF add(4)]
    by (intro nn_integral_add add) (simp_all add: M)
  also have "\ = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
    by (simp add: add)
  also have "\ = (\\<^sup>+ x. f x + g x \join M)"
    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)
  finally show ?case by (simp add: ac_simps)
next
  case (seq F)
  have "(\\<^sup>+ M'. \\<^sup>+ x. (SUP i. F i) x \M' \M) = (\\<^sup>+ M'. (SUP i. \\<^sup>+ x. F i x \M') \M)"
    using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply
    by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
       (auto simp add: space_subprob_algebra)
  also have "\ = (SUP i. \\<^sup>+ M'. \\<^sup>+ x. F i x \M' \M)"
    using nn_integral_measurable_subprob_algebra[OF seq(1)] seq
    by (intro nn_integral_monotone_convergence_SUP)
       (simp_all add: M incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
  also have "\ = (SUP i. integral\<^sup>N (join M) (F i))"
    by (simp add: seq)
  also have "\ = (\\<^sup>+ x. (SUP i. F i x) \join M)"
    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
                 (simp_all add: M cong: measurable_cong_sets)
  finally show ?case by (simp add: ac_simps image_comp)
qed

lemma measurable_join1:
  "\ f \ measurable N K; sets M = sets (subprob_algebra N) \
  \<Longrightarrow> f \<in> measurable (join M) K"
  by(simp add: measurable_def)

lemma
  fixes f :: "_ \ real"
  assumes f_measurable [measurable]: "f \ borel_measurable N"
  and f_bounded: "\x. x \ space N \ \f x\ \ B"
  and M [measurable_cong]: "sets M = sets (subprob_algebra N)"
  and fin: "finite_measure M"
  and M_bounded: "AE M' in M. emeasure M' (space M') \ ennreal B'"
  shows integrable_join: "integrable (join M) f" (is ?integrable)
  and integral_join: "integral\<^sup>L (join M) f = \ M'. integral\<^sup>L M' f \M" (is ?integral)
proof(case_tac [!] "space N = {}")
  assume *: "space N = {}"
  show ?integrable
    using M * by(simp add: real_integrable_def measurable_def nn_integral_empty)
  have "(\ M'. integral\<^sup>L M' f \M) = (\ M'. 0 \M)"
  proof(rule Bochner_Integration.integral_cong)
    fix M'
    assume "M' \ space M"
    with sets_eq_imp_space_eq[OF M] have "space M' = space N"
      by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
    with * show "(\ x. f x \M') = 0" by(simp add: Bochner_Integration.integral_empty)
  qed simp
  then show ?integral
    using M * by(simp add: Bochner_Integration.integral_empty)
next
  assume *: "space N \ {}"

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

  have [measurable]: "f \ borel_measurable (join M)" using f_measurable M
    by(rule measurable_join1)

  { fix f M'
    assume [measurable]: "f \ borel_measurable N"
      and f_bounded: "\x. x \ space N \ f x \ B"
      and "M' \ space M" "emeasure M' (space M') \ ennreal B'"
    have "AE x in M'. ennreal (f x) \ ennreal B"
    proof(rule AE_I2)
      fix x
      assume "x \ space M'"
      with \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
      have "x \ space N" by(auto simp add: space_subprob_algebra dest: sets_eq_imp_space_eq)
      from f_bounded[OF this] show "ennreal (f x) \ ennreal B" by simp
    qed
    then have "(\\<^sup>+ x. ennreal (f x) \M') \ (\\<^sup>+ x. ennreal B \M')"
      by(rule nn_integral_mono_AE)
    also have "\ = ennreal B * emeasure M' (space M')" by(simp)
    also have "\ \ ennreal B * ennreal B'" by(rule mult_left_mono)(fact, simp)
    also have "\ \ ennreal B * ennreal \B'\" by(rule mult_left_mono)(simp_all)
    finally have "(\\<^sup>+ x. ennreal (f x) \M') \ ennreal (B * \B'\)" by (simp add: ennreal_mult) }
  note bounded1 = this

  have bounded:
    "\f. \ f \ borel_measurable N; \x. x \ space N \ f x \ B \
    \<Longrightarrow> (\<integral>\<^sup>+ x. ennreal (f x) \<partial>join M) \<noteq> top"
  proof -
    fix f
    assume [measurable]: "f \ borel_measurable N"
      and f_bounded: "\x. x \ space N \ f x \ B"
    have "(\\<^sup>+ x. ennreal (f x) \join M) = (\\<^sup>+ M'. \\<^sup>+ x. ennreal (f x) \M' \M)"
      by(rule nn_integral_join[OF _ M]) simp
    also have "\ \ \\<^sup>+ M'. B * \B'\ \M"
      using bounded1[OF \<open>f \<in> borel_measurable N\<close> f_bounded]
      by(rule nn_integral_mono_AE[OF AE_mp[OF M_bounded AE_I2], rule_format])
    also have "\ = B * \B'\ * emeasure M (space M)" by simp
    also have "\ < \"
      using finite_measure.finite_emeasure_space[OF fin]
      by(simp add: ennreal_mult_less_top less_top)
    finally show "?thesis f" by simp
  qed
  have f_pos: "(\\<^sup>+ x. ennreal (f x) \join M) \ \"
    and f_neg: "(\\<^sup>+ x. ennreal (- f x) \join M) \ \"
    using f_bounded by(auto del: notI intro!: bounded simp add: abs_le_iff)

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

  note [measurable] = nn_integral_measurable_subprob_algebra

  have int_f: "(\\<^sup>+ x. f x \join M) = \\<^sup>+ M'. \\<^sup>+ x. f x \M' \M"
    by(simp add: nn_integral_join[OF _ M])
  have int_mf: "(\\<^sup>+ x. - f x \join M) = (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M)"
    by(simp add: nn_integral_join[OF _ M])

  have pos_finite: "AE M' in M. (\\<^sup>+ x. f x \M') \ \"
    using AE_space M_bounded
  proof eventually_elim
    fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> ennreal B'"
    then have "(\\<^sup>+ x. ennreal (f x) \M') \ ennreal (B * \B'\)"
      using f_measurable by(auto intro!: bounded1 dest: f_bounded)
    then show "(\\<^sup>+ x. ennreal (f x) \M') \ \"
      by (auto simp: top_unique)
  qed
  hence [simp]: "(\\<^sup>+ M'. ennreal (enn2real (\\<^sup>+ x. f x \M')) \M) = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M)"
    by (rule nn_integral_cong_AE[OF AE_mp]) (simp add: less_top)
  from f_pos have [simp]: "integrable M (\M'. enn2real (\\<^sup>+ x. f x \M'))"
    by(simp add: int_f real_integrable_def nn_integral_0_iff_AE[THEN iffD2] ennreal_neg enn2real_nonneg)

  have neg_finite: "AE M' in M. (\\<^sup>+ x. - f x \M') \ \"
    using AE_space M_bounded
  proof eventually_elim
    fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> ennreal B'"
    then have "(\\<^sup>+ x. ennreal (- f x) \M') \ ennreal (B * \B'\)"
      using f_measurable by(auto intro!: bounded1 dest: f_bounded)
    then show "(\\<^sup>+ x. ennreal (- f x) \M') \ \"
      by (auto simp: top_unique)
  qed
  hence [simp]: "(\\<^sup>+ M'. ennreal (enn2real (\\<^sup>+ x. - f x \M')) \M) = (\\<^sup>+ M'. \\<^sup>+ x. - f x \M' \M)"
    by (rule nn_integral_cong_AE[OF AE_mp]) (simp add: less_top)
  from f_neg have [simp]: "integrable M (\M'. enn2real (\\<^sup>+ x. - f x \M'))"
    by(simp add: int_mf real_integrable_def nn_integral_0_iff_AE[THEN iffD2] ennreal_neg enn2real_nonneg)

  have "(\ x. f x \join M) = enn2real (\\<^sup>+ N. \\<^sup>+x. f x \N \M) - enn2real (\\<^sup>+ N. \\<^sup>+x. - f x \N \M)"
    unfolding real_lebesgue_integral_def[OF \<open>?integrable\<close>] by (simp add: nn_integral_join[OF _ M])
  also have "\ = (\N. enn2real (\\<^sup>+x. f x \N) \M) - (\N. enn2real (\\<^sup>+x. - f x \N) \M)"
    using pos_finite neg_finite by (subst (1 2) integral_eq_nn_integral) (auto simp: enn2real_nonneg)
  also have "\ = (\N. enn2real (\\<^sup>+x. f x \N) - enn2real (\\<^sup>+x. - f x \N) \M)"
    by simp
  also have "\ = \M'. \ x. f x \M' \M"
  proof (rule integral_cong_AE)
    show "AE x in M.
        enn2real (\<integral>\<^sup>+ x. ennreal (f x) \<partial>x) - enn2real (\<integral>\<^sup>+ x. ennreal (- f x) \<partial>x) = integral\<^sup>L x f"
      using AE_space M_bounded
    proof eventually_elim
      fix M' assume "M' \<in> space M" "emeasure M' (space M') \<le> B'"
      then interpret subprob_space M'
        by (auto simp: M[THEN sets_eq_imp_space_eq] space_subprob_algebra)

      from \<open>M' \<in> space M\<close> sets_eq_imp_space_eq[OF M]
      have [measurable_cong]: "sets M' = sets N" by(simp add: space_subprob_algebra)
      hence [simp]: "space M' = space N" by(rule sets_eq_imp_space_eq)
      have "integrable M' f"
        by(rule integrable_const_bound[where B=B])(auto simp add: f_bounded)
      then show "enn2real (\\<^sup>+ x. f x \M') - enn2real (\\<^sup>+ x. - f x \M') = \ x. f x \M'"
        by(simp add: real_lebesgue_integral_def)
    qed
  qed simp_all
  finally show ?integral by simp
qed

lemma join_assoc:
  assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
  shows "join (distr M (subprob_algebra N) join) = join (join M)"
proof (rule measure_eqI)
  fix A assume "A \ sets (join (distr M (subprob_algebra N) join))"
  then have A: "A \ sets N" by simp
  show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
    using measurable_join[of N]
    by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra
                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]
             intro!: nn_integral_cong emeasure_join)
qed (simp add: M)

lemma join_return:
  assumes "sets M = sets N" and "subprob_space M"
  shows "join (return (subprob_algebra N) M) = M"
  by (rule measure_eqI)
     (simp_all add: emeasure_join space_subprob_algebra
                    measurable_emeasure_subprob_algebra nn_integral_return assms)

lemma join_return':
  assumes "sets N = sets M"
  shows "join (distr M (subprob_algebra N) (return N)) = M"
proof (rule measure_eqI)
  fix A
  have "return N \ measurable M (subprob_algebra N)"
    using assms by auto
  moreover
  assume "A \ sets (join (distr M (subprob_algebra N) (return N)))"
  ultimately show "emeasure (join (distr M (subprob_algebra N) (return N))) A = emeasure M A"
    by (simp add: emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra assms)
qed (simp add: assms)

lemma join_distr_distr:
  fixes f :: "'a \ 'b" and M :: "'a measure measure" and N :: "'b measure"
  assumes "sets M = sets (subprob_algebra R)" and "f \ measurable R N"
  shows "join (distr M (subprob_algebra N) (\M. distr M N f)) = distr (join M) N f" (is "?r = ?l")
proof (rule measure_eqI)
  fix A assume "A \ sets ?r"
  hence A_in_N: "A \ sets N" by simp

  from assms have "f \ measurable (join M) N"
      by (simp cong: measurable_cong_sets)
  moreover from assms and A_in_N have "f-`A \ space R \ sets R"
      by (intro measurable_sets) simp_all
  ultimately have "emeasure (distr (join M) N f) A = \\<^sup>+M'. emeasure M' (f-`A \ space R) \M"
      by (simp_all add: A_in_N emeasure_distr emeasure_join assms)

  also have "... = \\<^sup>+ x. emeasure (distr x N f) A \M" using A_in_N
  proof (intro nn_integral_cong, subst emeasure_distr)
    fix M' assume "M' \<in> space M"
    from assms have "space M = space (subprob_algebra R)"
        using sets_eq_imp_space_eq by blast
    with \<open>M' \<in> space M\<close> have [simp]: "sets M' = sets R" using space_subprob_algebra by blast
    show "f \ measurable M' N" by (simp cong: measurable_cong_sets add: assms)
    have "space M' = space R" by (rule sets_eq_imp_space_eq) simp
    thus "emeasure M' (f -` A \ space R) = emeasure M' (f -` A \ space M')" by simp
  qed

  also have "(\M. distr M N f) \ measurable M (subprob_algebra N)"
      by (simp cong: measurable_cong_sets add: assms measurable_distr)
  hence "(\\<^sup>+ x. emeasure (distr x N f) A \M) =
             emeasure (join (distr M (subprob_algebra N) (\<lambda>M. distr M N f))) A"
      by (simp_all add: emeasure_join assms A_in_N nn_integral_distr measurable_emeasure_subprob_algebra)
  finally show "emeasure ?r A = emeasure ?l A" ..
qed simp

definition bind :: "'a measure \ ('a \ 'b measure) \ 'b measure" where
  "bind M f = (if space M = {} then count_space {} else
    join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"

adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind

lemma bind_empty:
  "space M = {} \ bind M f = count_space {}"
  by (simp add: bind_def)

lemma bind_nonempty:
  "space M \ {} \ bind M f = join (distr M (subprob_algebra (f (SOME x. x \ space M))) f)"
  by (simp add: bind_def)

lemma sets_bind_empty: "sets M = {} \ sets (bind M f) = {{}}"
  by auto

lemma space_bind_empty: "space M = {} \ space (bind M f) = {}"
  by (simp add: bind_def)

lemma sets_bind[simp, measurable_cong]:
  assumes f: "\x. x \ space M \ sets (f x) = sets N" and M: "space M \ {}"
  shows "sets (bind M f) = sets N"
  using f [of "SOME x. x \ space M"] by (simp add: bind_nonempty M some_in_eq)

lemma space_bind[simp]:
  assumes "\x. x \ space M \ sets (f x) = sets N" and "space M \ {}"
  shows "space (bind M f) = space N"
  using assms by (intro sets_eq_imp_space_eq sets_bind)

lemma bind_cong_All:
  assumes "\x \ space M. f x = g x"
  shows "bind M f = bind M g"
proof (cases "space M = {}")
  assume "space M \ {}"
  hence "(SOME x. x \ space M) \ space M" by (rule_tac someI_ex) blast
  with assms have "f (SOME x. x \ space M) = g (SOME x. x \ space M)" by blast
  with \<open>space M \<noteq> {}\<close> and assms show ?thesis by (simp add: bind_nonempty cong: distr_cong)
qed (simp add: bind_empty)

lemma bind_cong:
  "M = N \ (\x. x \ space M \ f x = g x) \ bind M f = bind N g"
  using bind_cong_All[of M f g] by auto

lemma bind_nonempty':
  assumes "f \ measurable M (subprob_algebra N)" "x \ space M"
  shows "bind M f = join (distr M (subprob_algebra N) f)"
proof -
  have "join (distr M (subprob_algebra (f (SOME x. x \ space M))) f) = join (distr M (subprob_algebra N) f)"
    by (metis assms someI_ex subprob_algebra_cong subprob_measurableD(2))
  with assms show ?thesis
    by (metis bind_nonempty empty_iff)
qed

lemma bind_nonempty'':
  assumes "f \ measurable M (subprob_algebra N)" "space M \ {}"
  shows "bind M f = join (distr M (subprob_algebra N) f)"
  using assms by (auto intro: bind_nonempty')

lemma emeasure_bind:
    "\space M \ {}; f \ measurable M (subprob_algebra N);X \ sets N\
      \<Longrightarrow> emeasure (M \<bind> f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
  by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)

lemma nn_integral_bind:
  assumes f: "f \ borel_measurable B"
  assumes N: "N \ measurable M (subprob_algebra B)"
  shows "(\\<^sup>+x. f x \(M \ N)) = (\\<^sup>+x. \\<^sup>+y. f y \N x \M)"
proof cases
  assume M: "space M \ {}" show ?thesis
    unfolding bind_nonempty''[OF N M] nn_integral_join[OF f sets_distr]
    by (rule nn_integral_distr[OF N])
       (simp add: f nn_integral_measurable_subprob_algebra)
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)

lemma AE_bind:
  assumes N[measurable]: "N \ measurable M (subprob_algebra B)"
  assumes P[measurable]: "Measurable.pred B P"
  shows "(AE x in M \ N. P x) \ (AE x in M. AE y in N x. P y)"
proof cases
  assume M: "space M = {}" show ?thesis
    unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
next
  assume M: "space M \ {}"
  note sets_kernel[OF N, simp]
  have *: "(\\<^sup>+x. indicator {x. \ P x} x \(M \ N)) = (\\<^sup>+x. indicator {x\space B. \ P x} x \(M \ N))"
    by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)

  have "(AE x in M \ N. P x) \ (\\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \ space B. \ P x}) \M) = 0"
    by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
             del: nn_integral_indicator)
  also have "... = (AE x in M. integral\<^sup>N (N x) (indicator {x \ space B. \ P x}) = 0)"
  proof (rule nn_integral_0_iff_AE)
    show "(\x. integral\<^sup>N (N x) (indicator {x \ space B. \ P x})) \ borel_measurable M"
    apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
      by measurable
  qed
  also have "\ = (AE x in M. AE y in N x. P y)"
    apply (intro eventually_subst AE_I2)
    by (auto simp add: subprob_measurableD(1)[OF N] intro!: AE_iff_measurable[symmetric])
  finally show ?thesis .
qed

lemma measurable_bind':
  assumes M1: "f \ measurable M (subprob_algebra N)" and
          M2: "case_prod g \ measurable (M \\<^sub>M N) (subprob_algebra R)"
  shows "(\x. bind (f x) (g x)) \ measurable M (subprob_algebra R)"
proof (subst measurable_cong)
  fix x assume x_in_M: "x \ space M"
  with assms have "space (f x) \ {}"
      by (blast dest: subprob_space_kernel subprob_space.subprob_not_empty)
  moreover from M2 x_in_M have "g x \ measurable (f x) (subprob_algebra R)"
      by (subst measurable_cong_sets[OF sets_kernel[OF M1 x_in_M] refl])
         (auto dest: measurable_Pair2)
  ultimately show "bind (f x) (g x) = join (distr (f x) (subprob_algebra R) (g x))"
      by (simp_all add: bind_nonempty'')
next
  show "(\w. join (distr (f w) (subprob_algebra R) (g w))) \ measurable M (subprob_algebra R)"
    apply (rule measurable_compose[OF _ measurable_join])
    apply (rule measurable_distr2[OF M2 M1])
    done
qed

lemma measurable_bind[measurable (raw)]:
  assumes M1: "f \ measurable M (subprob_algebra N)" and
          M2: "(\x. g (fst x) (snd x)) \ measurable (M \\<^sub>M N) (subprob_algebra R)"
  shows "(\x. bind (f x) (g x)) \ measurable M (subprob_algebra R)"
  using assms by (auto intro: measurable_bind' simp: measurable_split_conv)

lemma measurable_bind2:
  assumes "f \ measurable M (subprob_algebra N)" and "g \ measurable N (subprob_algebra R)"
  shows "(\x. bind (f x) g) \ measurable M (subprob_algebra R)"
    using assms by (intro measurable_bind' measurable_const) auto

lemma subprob_space_bind:
  assumes "subprob_space M" "f \ measurable M (subprob_algebra N)"
  shows "subprob_space (M \ f)"
proof (rule subprob_space_kernel[of "\x. x \ f"])
  show "(\x. x \ f) \ measurable (subprob_algebra M) (subprob_algebra N)"
    by (rule measurable_bind, rule measurable_ident_sets, rule refl,
        rule measurable_compose[OF measurable_snd assms(2)])
  from assms(1) show "M \ space (subprob_algebra M)"
    by (simp add: space_subprob_algebra)
qed

lemma
  fixes f :: "_ \ real"
  assumes f_measurable [measurable]: "f \ borel_measurable K"
  and f_bounded: "\x. x \ space K \ \f x\ \ B"
  and N [measurable]: "N \ measurable M (subprob_algebra K)"
  and fin: "finite_measure M"
  and M_bounded: "AE x in M. emeasure (N x) (space (N x)) \ ennreal B'"
  shows integrable_bind: "integrable (bind M N) f" (is ?integrable)
  and integral_bind: "integral\<^sup>L (bind M N) f = \ x. integral\<^sup>L (N x) f \M" (is ?integral)
proof(case_tac [!] "space M = {}")
  assume [simp]: "space M \ {}"
  interpret finite_measure M by(rule fin)

  have "integrable (join (distr M (subprob_algebra K) N)) f"
    using f_measurable f_bounded
    by(rule integrable_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
  then show ?integrable by(simp add: bind_nonempty''[where N=K])

  have "integral\<^sup>L (join (distr M (subprob_algebra K) N)) f = \ M'. integral\<^sup>L M' f \distr M (subprob_algebra K) N"
    using f_measurable f_bounded
    by(rule integral_join[where B'=B'])(simp_all add: finite_measure_distr AE_distr_iff M_bounded)
  also have "\ = \ x. integral\<^sup>L (N x) f \M"
    by(rule integral_distr)(simp_all add: integral_measurable_subprob_algebra[OF _])
  finally show ?integral by(simp add: bind_nonempty''[where N=K])
qed(simp_all add: bind_def integrable_count_space lebesgue_integral_count_space_finite Bochner_Integration.integral_empty)

lemma (in prob_space) prob_space_bind:
  assumes ae: "AE x in M. prob_space (N x)"
    and N[measurable]: "N \ measurable M (subprob_algebra S)"
  shows "prob_space (M \ N)"
proof
  have "emeasure (M \ N) (space (M \ N)) = (\\<^sup>+x. emeasure (N x) (space (N x)) \M)"
    by (subst emeasure_bind[where N=S])
--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.8Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.