Theory Kernels

(*  Title:   Kernels.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

section ‹ Kernels ›
theory Kernels
  imports Lemmas_S_Finite_Measure_Monad
begin

subsection ‹S-Finite Measures›
locale s_finite_measure =
  fixes M :: "'a measure"
  assumes s_finite_sum: "Mi :: nat  'a measure. (i. sets (Mi i) = sets M)  (i. finite_measure (Mi i))  (Asets M. M A = (i. Mi i A))"

lemma(in sigma_finite_measure) s_finite_measure: "s_finite_measure M"
proof
  obtain A :: "nat  _" where A: "range A  sets M" " (range A) = space M" "i. emeasure M (A i)  " "disjoint_family A"
    by(metis sigma_finite_disjoint)
  define Mi where "Mi  (λi. measure_of (space M) (sets M) (λa. M (a  A i)))"
  have emeasure_Mi:"Mi i a = M (a  A i)" if "a  sets M" for i a
  proof -
    have "positive (sets (Mi i)) (λa. M (a  A i))" "countably_additive (sets (Mi i)) (λa. M (a  A i))"
      unfolding positive_def countably_additive_def
    proof safe
      fix B :: "nat  _"
      assume "range B  sets (Mi i)" "disjoint_family B"
      with A(1) have "range (λj. B j  A i)  sets M" "disjoint_family (λj. B j  A i)"
        by(fastforce simp: Mi_def disjoint_family_on_def)+
      thus "(j. M (B j  A i)) = M ( (range B)  A i)"
        by (metis UN_extend_simps(4) suminf_emeasure)
    qed simp
    from emeasure_measure_of[OF _ _ this] that show ?thesis
      by(auto simp add: Mi_def sets.space_closed)
  qed
  have sets_Mi:"sets (Mi i) = sets M" for i by(simp add: Mi_def)
  show "Mi. (i. sets (Mi i) = sets M)  (i. finite_measure (Mi i))  (Asets M. emeasure M A = (i. emeasure (Mi i) A))"
  proof(safe intro!: exI[where x=Mi])
    fix i
    show "finite_measure (Mi i)"
      using A by(auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_Mi] emeasure_Mi)
  next
    fix B
    assume B:"B  sets M"
    with A(1,4) have "range (λi. B  A i)  sets M" "disjoint_family (λi. B  A i)"
      by(auto simp: disjoint_family_on_def)
    then show "M B = (i. (Mi i) B)"
      by(simp add: emeasure_Mi[OF B] suminf_emeasure A(2) B)
  qed(simp_all add: sets_Mi)
qed

lemmas(in finite_measure) s_finite_measure_finite_measure = s_finite_measure

lemmas(in subprob_space) s_finite_measure_subprob = s_finite_measure

lemmas(in prob_space) s_finite_measure_prob = s_finite_measure

sublocale sigma_finite_measure  s_finite_measure
  by(rule s_finite_measure)

lemma s_finite_measureI:
  assumes "i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. Asets M  M A = (i. Mi i A)"
  shows "s_finite_measure M"
  by standard (use assms in blast)

lemma s_finite_measure_prodI:
  assumes "i j. sets (Mij i j) = sets M" "i j. Mij i j (space M) < " "A. A  sets M  M A = (i. (j. Mij i j A))"
  shows "s_finite_measure M"
proof -
  define Mi' where "Mi'  (λn. case_prod Mij (prod_decode n))"
  have sets_Mi'[measurable_cong]:"i. sets (Mi' i) = sets M"
    using assms(1) by(simp add: Mi'_def split_beta')
  have Mi'_finite:"i. finite_measure (Mi' i)"
    using assms(2) sets_eq_imp_space_eq[OF sets_Mi'[symmetric]] top.not_eq_extremum
    by(fastforce intro!: finite_measureI simp: Mi'_def split_beta')
  show ?thesis
  proof(safe intro!: s_finite_measureI[where Mi=Mi'] sets_Mi' Mi'_finite)
    fix A
    show "A  sets M  M A = (i. Mi' i A)"
      by(simp add: assms(3) suminf_ennreal_2dimen[where f="λ(x,y). Mij x y A", simplified,OF refl,symmetric] Mi'_def split_beta')
  qed
qed

corollary s_finite_measure_s_finite_sumI:
  assumes "i. sets (Mi i) = sets M" "i. s_finite_measure (Mi i)" "A. A  sets M  M A = (i. Mi i A)"
  shows "s_finite_measure M"
proof -
  from s_finite_measure.s_finite_sum[OF assms(2)]
  obtain Mij where Mij[measurable]: "i j. sets (Mij i j) = sets M" "i j. finite_measure (Mij i j)" "i j A. A  sets M  Mi i A = (j. Mij i j A)"
    by (metis assms(1))
  show ?thesis
    using finite_measure.emeasure_finite[OF Mij(2)]
    by(auto intro!: s_finite_measure_prodI[where Mij = Mij] simp: assms(3) Mij top.not_eq_extremum)
qed

lemma s_finite_measure_finite_sumI:
  assumes "finite I" "i. i  I  s_finite_measure (Mi i)" "i. i  I  sets (Mi i) = sets M"
    and "A. A  sets M  M A = (iI. Mi i A)"
  shows "s_finite_measure M"
proof -
  let ?Mi = "λn. if n < card I then Mi (from_nat_into I n) else null_measure M"
  show ?thesis
  proof(rule s_finite_measure_s_finite_sumI[of ?Mi])
    show "i. s_finite_measure (?Mi i)"
      by (metis  (full_types) assms(2) bot_nat_0.extremum_strict card.empty emeasure_null_measure ennreal_top_neq_zero finite_measure.s_finite_measure_finite_measure finite_measureI from_nat_into infinity_ennreal_def)
  next
    show "i. sets (?Mi i) = sets M"
      by (metis (full_types) assms(3) card_gt_0_iff dual_order.strict_trans2 from_nat_into less_zeroE linorder_le_less_linear sets_null_measure)
  next
    fix A
    assume "A  sets M"
    then have "M A = (iI. Mi i A)"
      by fact
    also have "... = (n<card I. Mi (from_nat_into I n) A)"
      by(rule sum.card_from_nat_into[symmetric])
    also have "... = (n<card I. ?Mi n A)"
      by simp
    also have "... =  (n. ?Mi n A)"
      by(rule suminf_finite[symmetric]) auto
    finally show "M A = (n. ?Mi n A)" .
  qed
qed

lemma countable_space_s_finite_measure:
  assumes "countable (space M)" "sets M = Pow (space M)"
  shows "s_finite_measure M"
proof -
  define Mi where "Mi  (λi. measure_of (space M) (sets M) (λA. emeasure M (A  {from_nat_into (space M) i})))"
  have sets_Mi[measurable_cong,simp]: "sets (Mi i) = sets M" for i
    by(auto simp: Mi_def)
  have emeasure_Mi: "emeasure (Mi i) A = emeasure M (A  {from_nat_into (space M) i})" if [measurable]: "A  sets M" and i:"i  to_nat_on (space M) ` (space M)" for i A
  proof -
    have "from_nat_into (space M) i  space M"
      by (simp add: from_nat_into_def i inv_into_into)
    hence [measurable]: "{from_nat_into (space M) i}  sets M"
      using assms(2) by auto
    have 1:"countably_additive (sets M) (λA. emeasure M (A  {from_nat_into (space M) i}))"
      unfolding countably_additive_def
    proof safe
      fix B :: "nat  _"
      assume "range B  sets M" "disjoint_family B"
      then have [measurable]:"i. B i  sets M" and "disjoint_family (λj. B j  {from_nat_into (space M) i})"
        by(auto simp: disjoint_family_on_def)
      then have "(j. emeasure M (B j  {from_nat_into (space M) i})) = emeasure M ( (range (λj. B j  {from_nat_into (space M) i})))"
        by(intro suminf_emeasure) auto
      thus "(j. emeasure M (B j  {from_nat_into (space M) i})) = emeasure M ( (range B)  {from_nat_into (space M) i})"
        by simp
    qed
    have 2:"positive (sets M) (λA. emeasure M (A  {from_nat_into (space M) i}))"
      by(auto simp: positive_def)
    show ?thesis
      by(simp add: Mi_def emeasure_measure_of_sigma[OF sets.sigma_algebra_axioms 2 1])
  qed
  define Mi' where "Mi'  (λi. if i  to_nat_on (space M) ` (space M) then Mi i else null_measure M)"
  have [measurable_cong, simp]: "sets (Mi' i) = sets M" for i
    by(auto simp: Mi'_def)
  show ?thesis
  proof(rule s_finite_measure_s_finite_sumI[where Mi=Mi'])
    fix A
    assume A[measurable]: "A  sets M"
    show "emeasure M A = (i. emeasure (Mi' i) A)" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (+ x. emeasure M {x} count_space A)"
        using sets.sets_into_space[OF A] by(auto intro!: emeasure_countable_singleton simp: assms(2) countable_subset[OF _ assms(1)])
      also have "... = (+ x. emeasure (Mi (to_nat_on (space M) x)) A count_space A)"
      proof(safe intro!: nn_integral_cong)
        fix x
        assume "x  space (count_space A)"
        then have 1:"x  A" by simp
        hence 2:"to_nat_on (space M) x  to_nat_on (space M) ` (space M)"
          using A assms(2) by auto
        have [simp]: "from_nat_into (space M) (to_nat_on (space M) x) = x"
          by (metis 1 2 A assms(1) eq_from_nat_into_iff in_mono sets.sets_into_space)
        show "emeasure M {x} = emeasure (Mi (to_nat_on (space M) x)) A"
          using 1 by(simp add: emeasure_Mi[OF A 2])
      qed
      also have "... = (+ xA. emeasure (Mi (to_nat_on (space M) x)) A count_space UNIV)"
        by (simp add: nn_integral_count_space_indicator)
      also have "... = (+ ito_nat_on (space M) ` A. emeasure (Mi i) A count_space UNIV)"
        by(rule nn_integral_count_compose_inj[OF inj_on_subset[OF inj_on_to_nat_on[OF assms(1)] sets.sets_into_space[OF A]]])
      also have "... = (+ ito_nat_on (space M) ` A. emeasure (Mi' i) A count_space UNIV)"
      proof -
        {
          fix x
          assume "x  A"
          then have "to_nat_on (space M) x  to_nat_on (space M) ` (space M)"
            using sets.sets_into_space[OF A] by auto
          hence "emeasure (Mi (to_nat_on (space M) x)) A = emeasure (Mi' (to_nat_on (space M) x)) A"
            by(auto simp: Mi'_def)
        }
        thus ?thesis
          by(auto intro!: nn_integral_cong simp: indicator_def)
      qed
      also have "... = (+ i. emeasure (Mi' i) A count_space UNIV)"
      proof -
        { 
          fix i
          assume i:"i  to_nat_on (space M) ` A"
          have "from_nat_into (space M) i  A" if "i  to_nat_on (space M) ` (space M)"
            by (metis i image_eqI that to_nat_on_from_nat_into)
          with emeasure_Mi have "emeasure (Mi' i) A = 0"
            by(auto simp: Mi'_def)
        }
        thus ?thesis
          by(auto intro!: nn_integral_cong simp: indicator_def)
      qed
      also have "... = ?rhs"
        by(rule nn_integral_count_space_nat)
      finally show ?thesis .
    qed
  next
    fix i
    show "s_finite_measure (Mi' i)"
    proof -
      {
        fix x
        assume h:"x  space M" "i = to_nat_on (space M) x"
        then have i:"i  to_nat_on (space M) ` space M"
          by blast
        have x: "from_nat_into (space M) i = x"
          using h by (simp add: assms(1))
        consider "M {x} = 0" | "M {x}  0" "M {x} < " | "M {x} = "
          using top.not_eq_extremum by fastforce
        hence "s_finite_measure (Mi (to_nat_on (space M) x))"
        proof cases
          case 1
          then have [simp]:"Mi i = null_measure M"
            by(auto intro!: measure_eqI simp: emeasure_Mi[OF _ i] x Int_insert_right)
          show ?thesis
            by(auto simp: h(2)[symmetric] intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
        next
          case 2
          then show ?thesis
            unfolding h(2)[symmetric]
            by(auto intro!: finite_measure.s_finite_measure_finite_measure finite_measureI simp: sets_eq_imp_space_eq[OF sets_Mi] emeasure_Mi[OF _ i] x h(1))
        next
          case 3
          show ?thesis
            unfolding h(2)[symmetric] s_finite_measure_def
          proof(safe intro!: exI[where x="λj. return M x"] prob_space.finite_measure prob_space_return h(1))
            fix A
            assume "A  sets (Mi i)"
            then have [measurable]: "A  sets M"
              by(simp add: Mi_def)
            thus "emeasure (Mi i) A = (i. emeasure (return M x) A)"
              by(simp add: emeasure_Mi[OF _ i] x) (cases "x  A",auto simp: 3 nn_integral_count_space_nat[symmetric])
          qed(auto simp: Mi_def)
        qed
      }
      thus ?thesis
        by(auto simp: Mi'_def) (auto intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
    qed
  qed simp
qed

lemma s_finite_measure_subprob_space:
 "s_finite_measure M  (Mi :: nat  'a measure. (i. sets (Mi i) = sets M)  (i. (Mi i) (space M)  1)  (Asets M. M A = (i. Mi i A)))"
proof
  assume "Mi. (i. sets (Mi i) = sets M)  (i. emeasure (Mi i) (space M)  1)  (Asets M. M A = (i. (Mi i) A))"
  then obtain Mi where 1:"i. sets (Mi i) = sets M" "i. emeasure (Mi i) (space M)  1" "(Asets M. M A = (i. (Mi i) A))"
    by auto
  thus "s_finite_measure M"
    by(auto simp: s_finite_measure_def sets_eq_imp_space_eq[OF 1(1)] intro!: finite_measureI exI[where x=Mi])  (metis ennreal_one_less_top linorder_not_le)
next
  assume "s_finite_measure M"
  then obtain Mi' where Mi': "i. sets (Mi' i) = sets M" "i. finite_measure (Mi' i)" "A. Asets M  M A = (i. Mi' i A)"
    by (metis s_finite_measure.s_finite_sum)
  obtain u where u:"i. u i < " "i. Mi' i (space M) = u i"
    using Mi'(2) finite_measure.emeasure_finite top.not_eq_extremum by fastforce
  define Mmn where "Mmn  (λ(m,n). if n < nat enn2real (u m) then scale_measure (1 / ennreal (real_of_int enn2real (u m))) (Mi' m) else (sigma (space M) (sets M)))"
  have sets_Mmn : "sets (Mmn k) = sets M" for k by(simp add: Mmn_def split_beta Mi')
  have emeasure_Mmn: "(Mmn (m, n)) A = (Mi' m A) / ennreal (real_of_int enn2real (u m))" if "n < nat enn2real (u m)" "A  sets M" for n m A
    by(auto simp: Mmn_def that ennreal_divide_times)
  have emeasure_Mmn_less1: "(Mmn (m, n)) A  1" for m n A
  proof (cases "n < nat enn2real (u m)  A  sets M")
    case h:True
    have "(Mi' m) A  ennreal (real_of_int enn2real (u m))"
      by(rule order.trans[OF emeasure_mono[OF sets.sets_into_space sets.top]]) (insert u(1) h, auto simp: u(2)[symmetric] enn2real_le top.not_eq_extremum sets_eq_imp_space_eq[OF Mi'(1)] Mi'(1))
    with h show ?thesis
      by(simp add: emeasure_Mmn) (metis divide_le_posI_ennreal dual_order.eq_iff ennreal_zero_divide mult.right_neutral not_gr_zero zero_le)
  qed(auto simp: Mmn_def emeasure_sigma emeasure_notin_sets  Mi')
  have Mi'_sum:"Mi' m A = (n. Mmn (m, n) A)" if "A  sets M" for m A
  proof -
    have "(n. Mmn (m, n) A) = (n. Mmn (m, n + nat enn2real (u m)) A) + (n< nat enn2real (u m). Mmn (m, n) A)"
      by(simp add: suminf_offset[where f="λn. Mmn (m, n) A"])
    also have "... = (n< nat enn2real (u m). Mmn (m, n) A)"
      by(simp add: emeasure_sigma Mmn_def)
    also have "... = (n< nat enn2real (u m). (Mi' m A) / ennreal (real_of_int enn2real (u m)))"
      by(rule Finite_Cartesian_Product.sum_cong_aux) (auto simp: emeasure_Mmn that)
    also have "... = Mi' m A"
    proof (cases "nat enn2real (u m)")
      case 0
      with u[of m] show ?thesis
        by simp (metis Mi'(1) emeasure_mono enn2real_positive_iff less_le_not_le linorder_less_linear not_less_zero sets.sets_into_space sets.top that)
    next
      case (Suc n')
      then have "ennreal (real_of_int enn2real (u m)) > 0"
        using ennreal_less_zero_iff by fastforce
      with u(1)[of m] have "of_nat (nat enn2real (u m)) / ennreal (real_of_int enn2real (u m)) = 1"
        by (simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
      thus ?thesis
        by (simp add: ennreal_divide_times[symmetric])
    qed
    finally show ?thesis ..
  qed
  define Mi where "Mi  (λi. Mmn (prod_decode i))"
  show "Mi. (i. sets (Mi i) = sets M)  (i. emeasure (Mi i) (space M)  1)  (Asets M. M A = (i. (Mi i) A))"
   by(auto intro!: exI[where x=Mi] simp: Mi_def sets_Mmn suminf_ennreal_2dimen[OF Mi'_sum] Mi'(3)) (metis emeasure_Mmn_less1 prod_decode_aux.cases)
qed

lemma(in s_finite_measure) finite_measures:
  obtains Mi where "i. sets (Mi i) = sets M" "i. (Mi i) (space M)  1" "A. M A = (i. Mi i A)"
proof -
  obtain Mi where Mi:"i. sets (Mi i) = sets M" "i. (Mi i) (space M)  1" "A. A  sets M  M A = (i. Mi i A)"
    using s_finite_measure_axioms by(metis s_finite_measure_subprob_space)
  hence "M A = (i. Mi i A)" for A
    by(cases "A  sets M") (auto simp: emeasure_notin_sets)
  with Mi(1,2) show ?thesis
    using that by blast
qed

lemma(in s_finite_measure) finite_measures_ne:
  assumes "space M  {}"
  obtains Mi where "i. sets (Mi i) = sets M" "i. subprob_space (Mi i)" "A. M A = (i. Mi i A)"
  by (metis assms finite_measures sets_eq_imp_space_eq subprob_spaceI)

lemma(in s_finite_measure) finite_measures':
  obtains Mi where "i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
  by (metis ennreal_top_neq_one finite_measureI finite_measures infinity_ennreal_def sets_eq_imp_space_eq top.extremum_uniqueI)

lemma(in s_finite_measure) s_finite_measure_distr:
  assumes f[measurable]:"f  M M N"
  shows "s_finite_measure (distr M N f)"
proof -
  obtain Mi where Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
    by(metis finite_measures')
  show ?thesis
    by(auto intro!: s_finite_measureI[where Mi="(λi. distr (Mi i) N f)"] finite_measure.finite_measure_distr[OF Mi(2)] simp: emeasure_distr Mi(3) sets_eq_imp_space_eq[OF Mi(1)])
qed

lemma nn_integral_measure_suminf:
  assumes [measurable_cong]:"i. sets (Mi i) = sets M" and "A. Asets M  M A = (i. Mi i A)" "f  borel_measurable M"
  shows "(i. +x. f x (Mi i)) = (+x. f x M)"
  using assms(3)
proof induction
  case (cong f g)
  then show ?case
    by (metis (no_types, lifting) assms(1) nn_integral_cong sets_eq_imp_space_eq suminf_cong)
next
  case (set A)
  then show ?case
    using assms(1,2) by simp
next
  case (mult u c)
  then show ?case
    by(simp add: nn_integral_cmult)
next
  case (add u v)
  then show ?case
    by(simp add: nn_integral_add suminf_add[symmetric])
next
  case ih:(seq U)
  have "(i. integralN (Mi i) ( range U)) = (i. + x. (j. U j x)  (Mi i))"
    by(auto intro!: suminf_cong) (metis SUP_apply)
  also have "... = (i. j. + x. U j x (Mi i))"
    using ih by(auto intro!: suminf_cong nn_integral_monotone_convergence_SUP)
  also have "... = (j. (i. + x. U j x (Mi i)))"
    using ih(3) by(auto intro!: ennreal_suminf_SUP_eq incseq_nn_integral)
  also have "... = (j. integralN M (U j))"
    by(simp add: ih)
  also have "... = (+ x. (j. U j x) M)"
    using ih by(auto intro!: nn_integral_monotone_convergence_SUP[symmetric])
  also have "... = integralN M ( range U)"
    by(metis SUP_apply)
  finally show ?case .
qed

text ‹ A @{term density M f} of $s$-finite measure @{term M} and @{term f  borel_measurable M} is again s-finite.
       We do not require additional assumption, unlike $\sigma$-finite measures.›
lemma(in s_finite_measure) s_finite_measure_density:
  assumes f[measurable]:"f  borel_measurable M"
    shows "s_finite_measure (density M f)"
proof -
  obtain Mi where Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
    by(metis finite_measures')
  show ?thesis
  proof(rule s_finite_measure_s_finite_sumI[where Mi="λi. density (Mi i) f"])
    show "s_finite_measure (density (Mi i) f)" for i
    proof -
      define Mij where "Mij = (λj::nat. if j = 0 then density (Mi i) (λx.  * indicator {xspace M. f x = } x)
                                   else if j = 1 then density (Mi i) (λx. f x * indicator {xspace M. f x < } x)
                                   else null_measure M)"
      have sets_Mij[measurable_cong]: "sets (Mij j) = sets M" for j
        by(auto simp: Mij_def Mi)
      have emeasure_Mi:"density (Mi i) f A = (j. Mij j A)" (is "?lhs = ?rhs") if A[measurable]: "A  sets M" for A
      proof -
        have "?lhs = (+x  A. f x Mi i)"
          by(simp add: emeasure_density)
        also have "... = (+x.  * indicator {xspace M. f x = } x * indicator A x + f x * indicator {xspace M. f x < } x * indicator A x Mi i)"
          by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF Mi(1)] indicator_def) (simp add: top.not_eq_extremum)
        also have "... = density (Mi i) (λx.  * indicator {xspace M. f x = } x) A + density (Mi i) (λx. f x * indicator {xspace M. f x < } x) A"
          by(simp add: nn_integral_add emeasure_density)
        also have "... = ?rhs"
          using suminf_finite[of "{..<Suc (Suc 0)}" "λj. Mij j A"] by(auto simp: Mij_def)
        finally show ?thesis .
      qed
      show ?thesis
      proof(rule s_finite_measure_s_finite_sumI[OF _ _ emeasure_Mi])
        fix j :: nat
        consider "j = 0" | "j = 1" | "j  0" "j  1" by auto
        then show "s_finite_measure (Mij j)"
        proof cases
          case 1
          have 2:"Mij j A = (k. density (Mi i) (indicator {xspace M. f x = }) A)" if A[measurable]:"A  sets M" for A
            by(auto simp: Mij_def 1 emeasure_density nn_integral_suminf[symmetric] sets_eq_imp_space_eq[OF Mi(1)] indicator_def  intro!: nn_integral_cong) (simp add: nn_integral_count_space_nat[symmetric])
          show ?thesis
            by(auto simp: s_finite_measure_def 2 Mi(1)[of i] sets_Mij[of j] intro!: exI[where x="λk. density (Mi i) (indicator {xspace M. f x = })"] finite_measure.finite_measure_restricted Mi(2))
        next
          case 2
          show ?thesis
            by(auto intro!: sigma_finite_measure.s_finite_measure AE_mono_measure[OF Mi(1)] sum_le_suminf[where I="{i}" and f="λi. Mi i _",simplified] simp: sigma_finite_measure.sigma_finite_iff_density_finite[OF finite_measure.sigma_finite_measure[OF Mi(2)[of i]]] le_measure[OF Mi(1)] Mi indicator_def 2 Mij_def) auto
        next
          case 3
          then show ?thesis
            by(auto simp: Mij_def intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
        qed
      qed(auto simp: sets_Mij Mi)
    qed 
  qed(auto simp: emeasure_density nn_integral_measure_suminf[OF Mi(1,3)] Mi(1))
qed

lemma
  fixes f :: "'a  'b::{banach, second_countable_topology}"
  assumes [measurable_cong]:"i. sets (Mi i) = sets M" and "A. Asets M  M A = (i. Mi i A)" "integrable M f"
  shows lebesgue_integral_measure_suminf:"(i. x. f x (Mi i)) = (x. f x M)" (is "?suminf")
    and lebesgue_integral_measure_suminf_summable_norm: "summable (λi. norm (x. f x (Mi i)))" (is "?summable2")
    and lebesgue_integral_measure_suminf_summable_norm_in: "summable (λi. x. norm (f x) (Mi i))" (is "?summable")
proof -
  have Mi:"Mi i  M" for i
    using assms(2) ennreal_suminf_lessD linorder_not_le by(fastforce simp: assms(1) le_measure[OF assms(1)])
  have sum2: "summable (λi. norm (x. g x (Mi i)))" if "summable (λi. x. norm (g x) (Mi i))" for g :: "'a  'b"
  proof(rule summable_suminf_not_top)
    have "(i. ennreal (norm (x. g x (Mi i))))  (i. ennreal (x. norm (g x) (Mi i)))"
      by(auto intro!: suminf_le)
    thus "(i. ennreal (norm (x. g x (Mi i))))  "
      by (metis ennreal_suminf_neq_top[OF that] Bochner_Integration.integral_nonneg neq_top_trans norm_ge_zero)
  qed simp    
  have "?suminf  ?summable"
    using assms(3)
  proof induction
    case h[measurable]:(base A c)
    have Mi_fin:"Mi i A < " for i
      by(rule order.strict_trans1[OF _ h(2)], auto simp: le_measureD3[OF Mi assms(1)])
    have 1: "(x. (indicat_real A x *R c) Mi i) = measure (Mi i) A *R c" for i
      using Mi_fin by simp
    have 2:"summable (λi. x. norm (indicat_real A x *R c) Mi i)"
    proof(rule summable_suminf_not_top)
      show "(i. ennreal (x. norm (indicat_real A x *R c) Mi i))  " (is "?l  _")
      proof -
        have "?l = (i. Mi i A ) * norm c"
          using Mi_fin by(auto intro!: suminf_cong simp: measure_def enn2real_mult ennreal_mult)
        also have "... = M A * norm c"
          by(simp add: assms(2))
        also have "...  "
          using h(2) by (simp add: ennreal_mult_less_top top.not_eq_extremum)
        finally show ?thesis .
      qed
    qed simp
    have 3: "(i. x. indicat_real A x *R c Mi i) = (x. indicat_real A x *R c M)" (is "?l = ?r")
    proof -
      have [simp]: "summable (λi. enn2real (Mi i A))"
        using Mi_fin h by(auto intro!: summable_suminf_not_top simp: assms(2)[symmetric])
      have "?l = (i. measure (Mi i) A) *R c"
        by(auto intro!: suminf_cong simp: 1 measure_def suminf_scaleR_left)
      also have "... = ?r"
        using h(2) Mi_fin by(simp add: ennreal_inj[where a="(i. measure (Mi i) A)" and b="measure M A",OF suminf_nonneg measure_nonneg,symmetric,simplified measure_def] measure_def suminf_ennreal2[symmetric] assms(2)[symmetric])
      finally show ?thesis .
    qed
    from 2 3 show ?case by simp
  next
    case ih[measurable]:(add f g)
    have 1:"summable (λi. x. norm (f x + g x) Mi i)"
    proof(rule summable_suminf_not_top)
      show "(i. ennreal (x. norm (f x + g x) Mi i))  " (is "?l  _")
      proof -
        have "?l = (i. (+x. ennreal (norm (f x + g x)) Mi i))"
          using ih by(auto intro!: suminf_cong nn_integral_eq_integral[symmetric] integrable_mono_measure[OF assms(1) Mi])
        also have "...  (i. (+x. ennreal (norm (f x) + norm (g x)) Mi i))"
          by(auto intro!: suminf_le nn_integral_mono norm_triangle_ineq simp del: ennreal_plus)
        also have "... = (i. (+x. ennreal (norm (f x)) Mi i)) + (i. (+x. ennreal (norm (g x)) Mi i))"
          by(auto intro!: suminf_cong simp: nn_integral_add suminf_add)
        also have "... = (i. ennreal (x. norm (f x) Mi i)) + (i. ennreal (x. norm (g x) Mi i))"
          using ih by(simp add: nn_integral_eq_integral integrable_mono_measure[OF assms(1) Mi])
        also have "... < "
          using ennreal_suminf_neq_top[OF conjunct2[OF ih(3)]] ennreal_suminf_neq_top[OF conjunct2[OF ih(4)]]
          by (meson Bochner_Integration.integral_nonneg ennreal_add_eq_top norm_ge_zero top.not_eq_extremum)
        finally show ?thesis
          using order.strict_iff_order by blast
      qed
    qed simp
    with ih show ?case
      by(auto simp: Bochner_Integration.integral_add[OF integrable_mono_measure[OF assms(1) Mi ih(1)] integrable_mono_measure[OF assms(1) Mi ih(2)]] suminf_add[symmetric,OF summable_norm_cancel[OF sum2[OF conjunct2[OF ih(3)]]] summable_norm_cancel[OF sum2[OF conjunct2[OF ih(4)]]]])
  next
    case ih[measurable]:(lim f fn)
    have 1:"summable (λi. x. norm (f x) (Mi i))"
    proof(rule summable_suminf_not_top)
      show "(i. ennreal (x. norm (f x) (Mi i)))  " (is "?lhs  _")
      proof -
        have "?lhs = (i. + x. ennreal (norm (f x)) Mi i)"
          by(auto intro!: suminf_cong nn_integral_eq_integral[symmetric] integrable_mono_measure[OF assms(1) Mi] simp: ih)
        also have "... = (+ x. ennreal (norm (f x)) M)"
          by(simp add: nn_integral_measure_suminf[OF assms(1,2)])
        also have "... = ennreal ( x. norm (f x) M)"
          by(auto intro!: nn_integral_eq_integral ih(4))
        also have "... < " by simp
        finally show "?lhs  "
          using linorder_neq_iff by blast
      qed
    qed simp
    have "(i. x. f x (Mi i)) = (i. x. f x (Mi i) (count_space UNIV))"
      by(rule integral_count_space_nat[symmetric]) (simp add: integrable_count_space_nat_iff sum2[OF 1])
    also have "... = lim (λm. i. x. fn m x (Mi i) (count_space UNIV))"
    proof(rule limI[OF integral_dominated_convergence[where w="λi. 2 * (x. norm (f x) (Mi i))"],symmetric],auto simp: AE_count_space integrable_count_space_nat_iff 1)
      show "(λm. x. fn m x (Mi i))  x. f x (Mi i)" for i
        by(rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"],insert ih) (auto intro!: integrable_mono_measure[OF assms(1) Mi] simp: sets_eq_imp_space_eq[OF assms(1)])
    next
      fix i j
      show "norm (x. fn j x (Mi i))  2 * (x. norm (f x) (Mi i))" (is "?l  ?r")
      proof -
        have "?l  (x. norm (fn j x) (Mi i))"
          by simp
        also have "...  (x. 2 * norm (f x) (Mi i))"
          by(rule integral_mono,insert ih) (auto intro!: integrable_mono_measure[OF assms(1) Mi] simp: sets_eq_imp_space_eq[OF assms(1)])
        finally show "?l  ?r" by simp
      qed
    qed
    also have "... = lim (λm. (i. x. fn m x (Mi i)))"
    proof -
      have "(i. x. fn m x (Mi i) (count_space UNIV)) = (i. x. fn m x (Mi i))" for m
        by(auto intro!: integral_count_space_nat sum2 simp: integrable_count_space_nat_iff) (use ih(5) in auto)
      thus ?thesis by simp
    qed
    also have "... = lim (λm. x. fn m x M)"
      by(simp add: ih(5))
    also have "... = (x. f x M)"
      using ih by(auto intro!: limI[OF integral_dominated_convergence[where w="λx. 2 * norm (f x)"]])
    finally show ?case
      using 1 by auto
  qed
  thus ?suminf ?summable ?summable2
    by(simp_all add: sum2)
qed

(* Ported from sigma-finite measure. 
   The following proof is easier than the sigma-finite measure version. *)
lemma (in s_finite_measure) measurable_emeasure_Pair':
  assumes "Q  sets (N M M)"
  shows "(λx. emeasure M (Pair x -` Q))  borel_measurable N" (is "?s Q  _")
proof -
  obtain Mi where Mi:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
    by(metis finite_measures')
  show ?thesis
    using Mi(1,2) assms finite_measure.finite_measure_cut_measurable[of "Mi _" Q N]
    by(simp add: Mi(3))
qed

lemma (in s_finite_measure) measurable_emeasure'[measurable (raw)]:
  assumes space: "x. x  space N  A x  space M"
  assumes A: "{xspace (N M M). snd x  A (fst x)}  sets (N M M)"
  shows "(λx. emeasure M (A x))  borel_measurable N"
proof -
  from space have "x. x  space N  Pair x -` {x  space (N M M). snd x  A (fst x)} = A x"
    by (auto simp: space_pair_measure)
  with measurable_emeasure_Pair'[OF A] show ?thesis
    by (auto cong: measurable_cong)
qed


lemma(in s_finite_measure) emeasure_pair_measure':
  assumes "X  sets (N M M)"
  shows "emeasure (N M M) X = (+ x. + y. indicator X (x, y) M N)" (is "_ =  X")
proof (rule emeasure_measure_of[OF pair_measure_def])
  show "positive (sets (N M M)) "
    by (auto simp: positive_def)
  have eq[simp]: "A x y. indicator A (x, y) = indicator (Pair x -` A) y"
    by (auto simp: indicator_def)
  show "countably_additive (sets (N M M)) "
  proof (rule countably_additiveI)
    fix F :: "nat  ('b × 'a) set" assume F: "range F  sets (N M M)" "disjoint_family F"
    from F have *: "i. F i  sets (N M M)" by auto
    moreover have "x. disjoint_family (λi. Pair x -` F i)"
      by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
    moreover have "x. range (λi. Pair x -` F i)  sets M"
      using F by (auto simp: sets_Pair1)
    ultimately show "(n.  (F n)) =  (i. F i)"
      by (auto simp add: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure
               intro!: nn_integral_cong nn_integral_indicator[symmetric]) 
  qed
  show "{a × b |a b. a  sets N  b  sets M}  Pow (space N × space M)"
    using sets.space_closed[of N] sets.space_closed[of M] by auto
qed fact

lemma (in s_finite_measure) emeasure_pair_measure_alt':
  assumes X: "X  sets (N M M)"
  shows "emeasure (N M M) X = (+x. emeasure M (Pair x -` X) N)"
proof -
  have [simp]: "x y. indicator X (x, y) = indicator (Pair x -` X) y"
    by (auto simp: indicator_def)
  show ?thesis
    using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure' sets_Pair1)
qed

proposition (in s_finite_measure) emeasure_pair_measure_Times':
  assumes A: "A  sets N" and B: "B  sets M"
  shows "emeasure (N M M) (A × B) = emeasure N A * emeasure M B"
proof -
  have "emeasure (N M M) (A × B) = (+x. emeasure M B * indicator A x N)"
    using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt')
  also have " = emeasure M B * emeasure N A"
    using A by (simp add: nn_integral_cmult_indicator)
  finally show ?thesis
    by (simp add: ac_simps)
qed

lemma(in s_finite_measure) measure_times:
  assumes[measurable]: "A  sets N" "B  sets M"
  shows "measure (N M M) (A × B) = measure N A * measure M B"
  by(auto simp: measure_def emeasure_pair_measure_Times' enn2real_mult)

lemma pair_measure_s_finite_measure_suminf:
  assumes Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
      and Ni[measurable_cong]:"i. sets (Ni i) = sets N" "i. finite_measure (Ni i)" "A. N A = (i. Ni i A)"
    shows "(M M N) A = (i j. (Mi i M Ni j) A)" (is "?lhs = ?rhs")
proof -
  interpret N: s_finite_measure N
    by(auto intro!: s_finite_measureI[where Mi=Mi] s_finite_measureI[where Mi=Ni] assms)
  show ?thesis
  proof(cases "A  sets (M M N)")
    case [measurable]:True
    show ?thesis
    proof -
      have "?lhs = (+x. N (Pair x -` A) M)"
        by(simp add: N.emeasure_pair_measure_alt')
      also have "... = (i. +x. N (Pair x -` A) Mi i)"
        using N.measurable_emeasure_Pair'[of A]
        by(auto intro!: nn_integral_measure_suminf[OF Mi(1,3),symmetric])
      also have "... = (i. +x. (j. Ni j (Pair x -` A)) Mi i)"
        by(simp add: Ni(3))
      also have "... = (i j. +x. Ni j (Pair x -` A) Mi i)"
        using  s_finite_measure.measurable_emeasure_Pair'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)],of A]
        by(auto simp: nn_integral_suminf intro!: suminf_cong)
      also have "... = ?rhs"
        by(auto intro!: suminf_cong simp: s_finite_measure.emeasure_pair_measure_alt'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)]])
      finally show ?thesis .
    qed
  next
    case False
    with Mi(1) Ni(1) show ?thesis
      by(simp add: emeasure_notin_sets)
  qed
qed

lemma pair_measure_s_finite_measure_suminf':
  assumes Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
      and Ni[measurable_cong]:"i. sets (Ni i) = sets N" "i. finite_measure (Ni i)" "A. N A = (i. Ni i A)"
    shows "(M M N) A = (i j. (Mi j M Ni i) A)" (is "?lhs = ?rhs")
proof -
  interpret N: s_finite_measure N
    by(auto intro!: s_finite_measureI[where Mi=Mi] s_finite_measureI[where Mi=Ni] assms)
  show ?thesis
  proof(cases "A  sets (M M N)")
    case [measurable]:True
    show ?thesis
    proof -
      have "?lhs = (+x. N (Pair x -` A) M)"
        by(simp add: N.emeasure_pair_measure_alt')
      also have "... = (+x. (i. Ni i (Pair x -` A)) M)"
        by(auto intro!: nn_integral_cong simp: Ni)
      also have "... = (i. (+x. Ni i (Pair x -` A) M))"
        by(auto intro!: nn_integral_suminf simp: finite_measure.finite_measure_cut_measurable[OF Ni(2)])
      also have "... = (i j. +x. Ni i (Pair x -` A) Mi j)"
        by(auto intro!: suminf_cong nn_integral_measure_suminf[symmetric] simp: finite_measure.finite_measure_cut_measurable[OF Ni(2)] Mi)
      also have "... = ?rhs"
        by(auto intro!: suminf_cong simp: s_finite_measure.emeasure_pair_measure_alt'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)]])
      finally show ?thesis .
    qed
  next
    case False
    with Mi(1) Ni(1) show ?thesis
      by(simp add: emeasure_notin_sets)
  qed
qed

lemma pair_measure_s_finite_measure:
  assumes "s_finite_measure M" and "s_finite_measure N"
  shows "s_finite_measure (M M N)"
proof -
  obtain Mi where Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
    by(metis s_finite_measure.finite_measures'[OF assms(1)])
  obtain Ni where Ni[measurable_cong]:"i. sets (Ni i) = sets N" "i. finite_measure (Ni i)" "A. N A = (i. Ni i A)"
    by(metis s_finite_measure.finite_measures'[OF assms(2)])
  show ?thesis
  proof(rule s_finite_measure_prodI[where Mij="λi j. Mi i M Ni j"])
    show "emeasure (Mi i M Ni j) (space (M M N)) < " for i j
      using finite_measure.emeasure_finite[OF Mi(2)[of i]] finite_measure.emeasure_finite[OF Ni(2)[of j]]
      by(auto simp: sets_eq_imp_space_eq[OF Mi(1)[of i],symmetric] sets_eq_imp_space_eq[OF Ni(1)[of j],symmetric] space_pair_measure s_finite_measure.emeasure_pair_measure_Times'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)[of j]]] ennreal_mult_less_top top.not_eq_extremum)
  qed(auto simp: pair_measure_s_finite_measure_suminf Mi Ni)
qed

lemma(in s_finite_measure) borel_measurable_nn_integral_fst':
  assumes [measurable]: "f  borel_measurable (N M M)"
  shows "(λx. + y. f (x, y) M)  borel_measurable N"
proof -
  obtain Mi where Mi[measurable_cong]:"i. sets (Mi i) = sets M" "i. finite_measure (Mi i)" "A. M A = (i. Mi i A)"
    by(metis finite_measures')
  show ?thesis
    by(rule measurable_cong[where g="λx. i. + y. f (x, y) Mi i",THEN iffD2])
      (auto simp: nn_integral_measure_suminf[OF Mi(1,3)] intro!: borel_measurable_suminf_order sigma_finite_measure.borel_measurable_nn_integral_fst[OF finite_measure.sigma_finite_measure[OF Mi(2)]])
qed

lemma (in s_finite_measure) nn_integral_fst':
  assumes f: "f  borel_measurable (M1 M M)"
  shows "(+ x. + y. f (x, y) M M1) = integralN (M1 M M) f" (is "?I f = _")
  using f proof induct
  case (cong u v)
  then have "?I u = ?I v"
    by (intro nn_integral_cong) (auto simp: space_pair_measure)
  with cong show ?case
    by (simp cong: nn_integral_cong)
qed (simp_all add: emeasure_pair_measure' nn_integral_cmult nn_integral_add
                   nn_integral_monotone_convergence_SUP measurable_compose_Pair1
                   borel_measurable_nn_integral_fst' nn_integral_mono incseq_def le_fun_def image_comp
              cong: nn_integral_cong)

lemma (in s_finite_measure) borel_measurable_nn_integral'[measurable (raw)]:
  "case_prod f  borel_measurable (N M M)  (λx. + y. f x y M)  borel_measurable N"
  using borel_measurable_nn_integral_fst'[of "case_prod f" N] by simp

lemma distr_pair_swap_s_finite:
  assumes "s_finite_measure M1" and "s_finite_measure M2"
  shows "M1 M M2 = distr (M2 M M1) (M1 M M2) (λ(x, y). (y, x))" (is "?P = ?D")
proof -
  {
    from s_finite_measure.finite_measures'[OF assms(1)] s_finite_measure.finite_measures'[OF assms(2)]
    obtain Mi1 Mi2
      where Mi1:"i. sets (Mi1 i) = sets M1" "i. finite_measure (Mi1 i)" "A. M1 A = (i. Mi1 i A)"
        and Mi2:"i. sets (Mi2 i) = sets M2" "i. finite_measure (Mi2 i)" "A. M2 A = (i. Mi2 i A)"
      by metis
    fix A
    assume A[measurable]:"A  sets (M1 M M2)"
    have "emeasure (M1 M M2) A = emeasure (M2 M M1) ((λ(x, y). (y, x)) -` A  space (M2 M M1))"
    proof -
      { 
        fix i j
        interpret pair_sigma_finite "Mi1 i" "Mi2 j"
          by(auto simp: pair_sigma_finite_def Mi1(2) Mi2(2) finite_measure.sigma_finite_measure)
        have "emeasure (Mi1 i M Mi2 j) A = emeasure (Mi2 j M Mi1 i) ((λ(x, y). (y, x)) -` A  space (M2 M M1))"
          using Mi1(1) Mi2(1) by(simp add: arg_cong[OF distr_pair_swap,of emeasure] emeasure_distr sets_eq_imp_space_eq[OF sets_pair_measure_cong[OF Mi2(1) Mi1(1)]])
      }
      thus ?thesis
        by(auto simp: pair_measure_s_finite_measure_suminf'[OF Mi2 Mi1] pair_measure_s_finite_measure_suminf[OF Mi1 Mi2] intro!: suminf_cong)
    qed
  }
  thus ?thesis
    by(auto intro!: measure_eqI simp: emeasure_distr)
qed

proposition nn_integral_snd':
  assumes "s_finite_measure M1" "s_finite_measure M2"
      and f[measurable]: "f  borel_measurable (M1 M M2)"
    shows "(+ y. (+ x. f (x, y) M1) M2) = integralN (M1 M M2) f"
proof -
  interpret M1: s_finite_measure M1 by fact
  interpret M2: s_finite_measure M2 by fact
  note measurable_pair_swap[OF f]
  from M1.nn_integral_fst'[OF this]
  have "(+ y. (+ x. f (x, y) M1) M2) = (+ (x, y). f (y, x) (M2 M M1))"
    by simp
  also have "(+ (x, y). f (y, x) (M2 M M1)) = integralN (M1 M M2) f"
    by (subst distr_pair_swap_s_finite[OF assms(1,2)]) (auto simp add: nn_integral_distr intro!: nn_integral_cong)
  finally show ?thesis .
qed

lemma (in s_finite_measure) borel_measurable_lebesgue_integrable'[measurable (raw)]:
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes [measurable]: "case_prod f  borel_measurable (N M M)"
  shows "Measurable.pred N (λx. integrable M (f x))"
proof -
  have [simp]: "x. x  space N  integrable M (f x)  (+y. norm (f x y) M) < "
    unfolding integrable_iff_bounded by simp
  show ?thesis
    by (simp cong: measurable_cong)
qed

lemma (in s_finite_measure) measurable_measure'[measurable (raw)]:
  "(x. x  space N  A x  space M) 
    {x  space (N M M). snd x  A (fst x)}  sets (N M M) 
    (λx. measure M (A x))  borel_measurable N"
  unfolding measure_def by (intro measurable_emeasure' borel_measurable_enn2real) auto

proposition (in s_finite_measure) borel_measurable_lebesgue_integral'[measurable (raw)]:
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes f[measurable]: "case_prod f  borel_measurable (N M M)"
  shows "(λx. y. f x y M)  borel_measurable N"
proof -
  from borel_measurable_implies_sequence_metric[OF f, of 0]
  obtain s where s: "i. simple_function (N M M) (s i)"
    and "xspace (N M M). (λi. s i x)  (case x of (x, y)  f x y)"
    and "i. xspace (N M M). dist (s i x) 0  2 * dist (case x of (x, xa)  f x xa) 0"
    by auto
  then have *:
    "x y. x  space N  y  space M  (λi. s i (x, y))  f x y"
    "i x y. x  space N  y  space M  norm (s i (x, y))  2 * norm (f x y)"
    by (auto simp: space_pair_measure)

  have [measurable]: "i. s i  borel_measurable (N M M)"
    by (rule borel_measurable_simple_function) fact

  have "i. s i  measurable (N M M) (count_space UNIV)"
    by (rule measurable_simple_function) fact

  define f' where [abs_def]: "f' i x =
    (if integrable M (f x) then Bochner_Integration.simple_bochner_integral M (λy. s i (x, y)) else 0)" for i x

  { fix i x assume "x  space N"
    then have "Bochner_Integration.simple_bochner_integral M (λy. s i (x, y)) =
      (zs i ` (space N × space M). measure M {y  space M. s i (x, y) = z} *R z)"
      using s[THEN simple_functionD(1)]
      unfolding simple_bochner_integral_def
      by (intro sum.mono_neutral_cong_left)
         (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
  note eq = this

  show ?thesis
  proof (rule borel_measurable_LIMSEQ_metric)
    fix i show "f' i  borel_measurable N"
      unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
  next
    fix x assume x: "x  space N"
    { assume int_f: "integrable M (f x)"
      have int_2f: "integrable M (λy. 2 * norm (f x y))"
        by (intro integrable_norm integrable_mult_right int_f)
      have "(λi. integralL M (λy. s i (x, y)))  integralL M (f x)"
      proof (rule integral_dominated_convergence)
        from int_f show "f x  borel_measurable M" by auto
        show "i. (λy. s i (x, y))  borel_measurable M"
          using x by simp
        show "AE xa in M. (λi. s i (x, xa))  f x xa"
          using x * by auto
        show "i. AE xa in M. norm (s i (x, xa))  2 * norm (f x xa)"
          using x * by auto
      qed fact
      moreover
      { fix i
        have "Bochner_Integration.simple_bochner_integrable M (λy. s i (x, y))"
        proof (rule simple_bochner_integrableI_bounded)
          have "(λy. s i (x, y)) ` space M  s i ` (space N × space M)"
            using x by auto
          then show "simple_function M (λy. s i (x, y))"
            using simple_functionD(1)[OF s(1), of i] x
            by (intro simple_function_borel_measurable)
               (auto simp: space_pair_measure dest: finite_subset)
          have "(+ y. ennreal (norm (s i (x, y))) M)  (+ y. 2 * norm (f x y) M)"
            using x * by (intro nn_integral_mono) auto
          also have "(+ y. 2 * norm (f x y) M) < "
            using int_2f unfolding integrable_iff_bounded by simp
          finally show "(+ xa. ennreal (norm (s i (x, xa))) M) < " .
        qed
        then have "integralL M (λy. s i (x, y)) = Bochner_Integration.simple_bochner_integral M (λy. s i (x, y))"
          by (rule simple_bochner_integrable_eq_integral[symmetric]) }
      ultimately have "(λi. Bochner_Integration.simple_bochner_integral M (λy. s i (x, y)))  integralL M (f x)"
        by simp }
    then
    show "(λi. f' i x)  integralL M (f x)"
      unfolding f'_def
      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
  qed
qed

lemma integrable_product_swap_s_finite:
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
      and "integrable (M1 M M2) f"
  shows "integrable (M2 M M1) (λ(x,y). f (y,x))"
proof -
  have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)(y,x)))" by (auto simp: fun_eq_iff)
  show ?thesis unfolding *
    by (rule integrable_distr[OF measurable_pair_swap'])
       (simp add: distr_pair_swap_s_finite[OF M1 M2,symmetric] assms)
qed

lemma integrable_product_swap_iff_s_finite:
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
  shows "integrable (M2 M M1) (λ(x,y). f (y,x))  integrable (M1 M M2) f"
proof -
  from integrable_product_swap_s_finite[OF M2 M1,of "λ(x,y). f (y,x)"] integrable_product_swap_s_finite[OF M1 M2,of f]
  show ?thesis by auto
qed

lemma integral_product_swap_s_finite:
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
      and f: "f  borel_measurable (M1 M M2)"
  shows "((x,y). f (y,x) (M2 M M1)) = integralL (M1 M M2) f"
proof -
  have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)(y,x)))" by (auto simp: fun_eq_iff)
  show ?thesis unfolding *
    by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap_s_finite[OF M1 M2,symmetric])
qed

theorem(in s_finite_measure) Fubini_integrable':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes f[measurable]: "f  borel_measurable (M1 M M)"
    and integ1: "integrable M1 (λx.  y. norm (f (x, y)) M)"
    and integ2: "AE x in M1. integrable M (λy. f (x, y))"
  shows "integrable (M1 M M) f"
proof (rule integrableI_bounded)
  have "(+ p. norm (f p) (M1 M M)) = (+ x. (+ y. norm (f (x, y)) M) M1)"
    by (simp add: nn_integral_fst'[symmetric])
  also have " = (+ x. ¦y. norm (f (x, y)) M¦ M1)"
  proof(rule nn_integral_cong_AE)
    show "AE x in M1. (+ y. ennreal (norm (f (x, y))) M) = ennreal ¦LINT y|M. norm (f (x, y))¦"
      using integ2
    proof eventually_elim
      fix x assume "integrable M (λy. f (x, y))"
      then have f: "integrable M (λy. norm (f (x, y)))"
        by simp
      then have "(+y. ennreal (norm (f (x, y))) M) = ennreal (LINT y|M. norm (f (x, y)))"
        by (rule nn_integral_eq_integral) simp
      also have " = ennreal ¦LINT y|M. norm (f (x, y))¦"
        using f by simp
      finally show "(+y. ennreal (norm (f (x, y))) M) = ennreal ¦LINT y|M. norm (f (x, y))¦" .
    qed
  qed
  also have " < "
    using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
  finally show "(+ p. norm (f p) (M1 M M)) < " .
qed fact

lemma(in s_finite_measure) emeasure_pair_measure_finite':
  assumes A: "A  sets (M1 M M)" and finite: "emeasure (M1 M M) A < "
  shows "AE x in M1. emeasure M {yspace M. (x, y)  A} < "
proof -
  from emeasure_pair_measure_alt'[OF A] finite
  have "(+ x. emeasure M (Pair x -` A) M1)  "
    by simp
  then have "AE x in M1. emeasure M (Pair x -` A)  "
    by (rule nn_integral_PInf_AE[rotated]) (intro measurable_emeasure_Pair' A)
  moreover have "x. x  space M1  Pair x -` A = {yspace M. (x, y)  A}"
    using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
  ultimately show ?thesis by (auto simp: less_top)
qed

lemma(in s_finite_measure) AE_integrable_fst''':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes f[measurable]: "integrable (M1 M M) f"
  shows "AE x in M1. integrable M (λy. f (x, y))"
proof -
  have "(+x. (+y. norm (f (x, y)) M) M1) = (+x. norm (f x) (M1 M M))"
    by (rule nn_integral_fst') simp
  also have "(+x. norm (f x) (M1 M M))  "
    using f unfolding integrable_iff_bounded by simp
  finally have "AE x in M1. (+y. norm (f (x, y)) M)  "
    by (intro nn_integral_PInf_AE borel_measurable_nn_integral')
       (auto simp: measurable_split_conv)
  with AE_space show ?thesis
    by eventually_elim
       (auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
qed

lemma(in s_finite_measure) integrable_fst_norm':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes f[measurable]: "integrable (M1 M M) f"
  shows "integrable M1 (λx. y. norm (f (x, y)) M)"
  unfolding integrable_iff_bounded
proof
  show "(λx.  y. norm (f (x, y)) M)  borel_measurable M1"
    by (rule borel_measurable_lebesgue_integral') simp
  have "(+ x. ennreal (norm (y. norm (f (x, y)) M)) M1) = (+x. (+y. norm (f (x, y)) M) M1)"
    using AE_integrable_fst'''[OF f] by (auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral)
  also have "(+x. (+y. norm (f (x, y)) M) M1) = (+x. norm (f x) (M1 M M))"
    by (rule nn_integral_fst') simp
  also have "(+x. norm (f x) (M1 M M)) < "
    using f unfolding integrable_iff_bounded by simp
  finally show "(+ x. ennreal (norm (y. norm (f (x, y)) M)) M1) < " .
qed

lemma(in s_finite_measure) integrable_fst''':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes f[measurable]: "integrable (M1 M M) f"
  shows "integrable M1 (λx. y. f (x, y) M)"
  by(auto intro!: Bochner_Integration.integrable_bound[OF integrable_fst_norm'[OF f]])

proposition(in s_finite_measure) integral_fst''':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes f: "integrable (M1 M M) f"
  shows "(x. (y. f (x, y) M) M1) = integralL (M1 M M) f"
using f proof induct
  case (base A c)
  have A[measurable]: "A  sets (M1 M M)" by fact

  have eq: "x y. x  space M1  indicator A (x, y) = indicator {yspace M. (x, y)  A} y"
    using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)

  have int_A: "integrable (M1 M M) (indicator A :: _  real)"
    using base by (rule integrable_real_indicator)
  have "( x.  y. indicator A (x, y) *R c M M1) = (x. measure M {yspace M. (x, y)  A} *R c M1)"
  proof (intro integral_cong_AE)
    from AE_integrable_fst'''[OF int_A] AE_space
    show "AE x in M1. (y. indicator A (x, y) *R c M) = measure M {yspace M. (x, y)  A} *R c"
      by eventually_elim (simp add: eq integrable_indicator_iff)
  qed simp_all
  also have " = measure (M1 M M) A *R c"
  proof (subst integral_scaleR_left)
    have "(+x. ennreal (measure M {y  space M. (x, y)  A}) M1) =
      (+x. emeasure M {y  space M. (x, y)  A} M1)"
      using emeasure_pair_measure_finite'[OF base]
      by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ennreal_measure)
    also have " = emeasure (M1 M M) A"
      using sets.sets_into_space[OF A]
      by (subst emeasure_pair_measure_alt')
         (auto intro!: nn_integral_cong arg_cong[where f="emeasure M"] simp: space_pair_measure)
    finally have *: "(+x. ennreal (measure M {y  space M. (x, y)  A}) M1) = emeasure (M1 M M) A" .

    from base * show "integrable M1 (λx. measure M {y  space M. (x, y)  A})"
      by (simp add: integrable_iff_bounded)
    then have "(x. measure M {y  space M. (x, y)  A} M1) =
      (+x. ennreal (measure M {y  space M. (x, y)  A}) M1)"
      by (rule nn_integral_eq_integral[symmetric]) simp
    also note *
    finally show "(x. measure M {y  space M. (x, y)  A} M1) *R c = measure (M1 M M) A *R c"
      using base by (simp add: emeasure_eq_ennreal_measure)
  qed
  also have " = ( a. indicator A a *R c (M1 M M))"
    using base by simp
  finally show ?case .
next
  case (add f g)
  then have [measurable]: "f  borel_measurable (M1 M M)" "g  borel_measurable (M1 M M)"
    by auto
  have "( x.  y. f (x, y) + g (x, y) M M1) =
    ( x. ( y. f (x, y) M) + ( y. g (x, y) M) M1)"
    apply (rule integral_cong_AE)
    apply simp_all
    using AE_integrable_fst'''[OF add(1)] AE_integrable_fst'''[OF add(3)]
    apply eventually_elim
    apply simp
    done
  also have " = ( x. f x (M1 M M)) + ( x. g x (M1 M M))"
    using integrable_fst'''[OF add(1)] integrable_fst'''[OF add(3)] add(2,4) by simp
  finally show ?case
    using add by simp
next
  case (lim f s)
  then have [measurable]: "f  borel_measurable (M1 M M)" "i. s i  borel_measurable (M1 M M)"
    by auto

  show ?case
  proof (rule LIMSEQ_unique)
    show "(λi. integralL (M1 M M) (s i))  integralL (M1 M M) f"
    proof (rule integral_dominated_convergence)
      show "integrable (M1 M M) (λx. 2 * norm (f x))"
        using lim(5) by auto
    qed (insert lim, auto)
    have "(λi.  x.  y. s i (x, y) M M1)   x.  y. f (x, y) M M1"
    proof (rule integral_dominated_convergence)
      have "AE x in M1. i. integrable M (λy. s i (x, y))"
        unfolding AE_all_countable using AE_integrable_fst'''[OF lim(1)] ..
      with AE_space AE_integrable_fst'''[OF lim(5)]
      show "AE x in M1. (λi.  y. s i (x, y) M)   y. f (x, y) M"
      proof eventually_elim
        fix x assume x: "x  space M1" and
          s: "i. integrable M (λy. s i (x, y))" and f: "integrable M (λy. f (x, y))"
        show "(λi.  y. s i (x, y) M)   y. f (x, y) M"
        proof (rule integral_dominated_convergence)
          show "integrable M (λy. 2 * norm (f (x, y)))"
             using f by auto
          show "AE xa in M. (λi. s i (x, xa))  f (x, xa)"
            using x lim(3) by (auto simp: space_pair_measure)
          show "i. AE xa in M. norm (s i (x, xa))  2 * norm (f (x, xa))"
            using x lim(4) by (auto simp: space_pair_measure)
        qed (insert x, measurable)
      qed
      show "integrable M1 (λx. ( y. 2 * norm (f (x, y)) M))"
        by (intro integrable_mult_right integrable_norm integrable_fst''' lim)
      fix i show "AE x in M1. norm ( y. s i (x, y) M)  ( y. 2 * norm (f (x, y)) M)"
        using AE_space AE_integrable_fst'''[OF lim(1), of i] AE_integrable_fst'''[OF lim(5)]
      proof eventually_elim
        fix x assume x: "x  space M1"
          and s: "integrable M (λy. s i (x, y))" and f: "integrable M (λy. f (x, y))"
        from s have "norm ( y. s i (x, y) M)  (+y. norm (s i (x, y)) M)"
          by (rule integral_norm_bound_ennreal)
        also have "  (+y. 2 * norm (f (x, y)) M)"
          using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
        also have " = (y. 2 * norm (f (x, y)) M)"
          using f by (intro nn_integral_eq_integral) auto
        finally show "norm ( y. s i (x, y) M)  ( y. 2 * norm (f (x, y)) M)"
          by simp
      qed
    qed simp_all
    then show "(λi. integralL (M1 M M) (s i))   x.  y. f (x, y) M M1"
      using lim by simp
  qed
qed

lemma (in s_finite_measure)
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes f: "integrable (M1 M M) (case_prod f)"
  shows AE_integrable_fst'': "AE x in M1. integrable M (λy. f x y)"
    and integrable_fst'': "integrable M1 (λx. y. f x y M)"
    and integrable_fst_norm: "integrable M1 (λx. y. norm (f x y) M)"
    and integral_fst'': "(x. (y. f x y M) M1) = integralL (M1 M M) (λ(x, y). f x y)"
  using AE_integrable_fst'''[OF f] integrable_fst'''[OF f] integral_fst'''[OF f] integrable_fst_norm'[OF f] by auto

lemma
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
      and f[measurable]: "integrable (M1 M M2) (case_prod f)"
  shows AE_integrable_snd_s_finite: "AE y in M2. integrable M1 (λx. f x y)" (is "?AE")
    and integrable_snd_s_finite: "integrable M2 (λy. x. f x y M1)" (is "?INT")
    and integrable_snd_norm_s_finite: "integrable M2 (λy. x. norm (f x y) M1)" (is "?INT2")
    and integral_snd_s_finite: "(y. (x. f x y M1) M2) = integralL (M1 M M2) (case_prod f)" (is "?EQ")
proof -
  interpret Q: s_finite_measure M1 by fact
  have Q_int: "integrable (M2 M M1) (λ(x, y). f y x)"
    using f unfolding integrable_product_swap_iff_s_finite[OF M1 M2,symmetric] by simp
  show ?AE  using Q.AE_integrable_fst'''[OF Q_int] by simp
  show ?INT using Q.integrable_fst'''[OF Q_int] by simp
  show ?INT2 using Q.integrable_fst_norm[OF Q_int] by simp
  show ?EQ using Q.integral_fst'''[OF Q_int]
    using integral_product_swap_s_finite[OF M1 M2,of "case_prod f"] by simp
qed

proposition Fubini_integral':
  fixes f :: "_  _  _ :: {banach, second_countable_topology}"
  assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
      and f: "integrable (M1 M M2) (case_prod f)"
  shows "(y. (x. f x y M1) M2) = (x. (y. f x y M2) M1)"
  unfolding integral_snd_s_finite[OF assms] s_finite_measure.integral_fst''[OF assms(2,3)] ..

locale product_s_finite =
  fixes M :: "'i  'a measure"
  assumes s_finite_measures: "i. s_finite_measure (M i)"

sublocale product_s_finite  M?: s_finite_measure "M i" for i
  by (rule s_finite_measures)

locale finite_product_s_finite = product_s_finite M for M :: "'i  'a measure" +
  fixes I :: "'i set"
  assumes finite_index: "finite I"

lemma (in product_s_finite) emeasure_PiM:
  "finite I  (i. iI  A i  sets (M i))  emeasure (PiM I M) (PiE I A) = (iI. emeasure (M i) (A i))"
proof (induct I arbitrary: A rule: finite_induct)
  case (insert i I)
  interpret finite_product_s_finite M I by standard fact
  have "finite (insert i I)" using finite I by auto
  interpret I': finite_product_s_finite M "insert i I" by standard fact
  let ?h = "(λ(f, y). f(i := y))"

  let ?P = "distr (PiM I M M M i) (PiM (insert i I) M) ?h"
  let  = "emeasure ?P"
  let ?I = "{j  insert i I. emeasure (M j) (space (M j))  1}"
  let ?f = "λJ E j. if j  J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"

  have "emeasure (PiM (insert i I) M) (prod_emb (insert i I) M (insert i I) (PiE (insert i I) A)) =
    (iinsert i I. emeasure (M i) (A i))"
  proof (subst emeasure_extend_measure_Pair[OF PiM_def])
    fix J E assume "(J  {}  insert i I = {})  finite J  J  insert i I  E  (Π jJ. sets (M j))"
    then have J: "J  {}" "finite J" "J  insert i I" and E: "jJ. E j  sets (M j)" by auto
    let ?p = "prod_emb (insert i I) M J (PiE J E)"
    let ?p' = "prod_emb I M (J - {i}) (ΠE jJ-{i}. E j)"
    have " ?p =
      emeasure (PiM I M M (M i)) (?h -` ?p  space (PiM I M M M i))"
      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
    also have "?h -` ?p  space (PiM I M M M i) = ?p' × (if i  J then E i else space (M i))"
      using J E[rule_format, THEN sets.sets_into_space]
      by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
    also have "emeasure (PiM I M M (M i)) (?p' × (if i  J then E i else space (M i))) =
      emeasure (PiM I M) ?p' * emeasure (M i) (if i  J then (E i) else space (M i))"
      using J E by (intro M.emeasure_pair_measure_Times' sets_PiM_I) auto
    also have "?p' = (ΠE jI. if j  J-{i} then E j else space (M j))"
      using J E[rule_format, THEN sets.sets_into_space]
      by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
    also have "emeasure (PiM I M) (ΠE jI. if j  J-{i} then E j else space (M j)) =
      ( jI. if j  J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
      using E by (subst insert) (auto intro!: prod.cong)
    also have "(jI. if j  J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
       emeasure (M i) (if i  J then E i else space (M i)) = (jinsert i I. ?f J E j)"
      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
    also have " = (jJ  ?I. ?f J E j)"
      using insert(1,2) J E by (intro prod.mono_neutral_right) auto
    finally show " ?p = " .

    show "prod_emb (insert i I) M J (PiE J E)  Pow (ΠE iinsert i I. space (M i))"
      using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
  next
    show "positive (sets (PiM (insert i I) M)) " "countably_additive (sets (PiM (insert i I) M)) "
      using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
  next
    show "(insert i I  {}  insert i I = {})  finite (insert i I) 
      insert i I  insert i I  A  (Π jinsert i I. sets (M j))"
      using insert by auto
  qed (auto intro!: prod.cong)
  with insert show ?case
    by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
qed simp


lemma (in finite_product_s_finite) measure_times:
  "(i. i  I  A i  sets (M i))  emeasure (PiM I M) (PiE I A) = (iI. emeasure (M i) (A i))"
  using emeasure_PiM[OF finite_index] by auto

lemma (in product_s_finite) nn_integral_empty:
  "0  f (λk. undefined)  integralN (PiM {} M) f = f (λk. undefined)"
  by (simp add: PiM_empty nn_integral_count_space_finite)

text ‹ Every s-finite measure is represented as the push-forward measure of a $\sigma$-finite measure.›
definition Mi_to_NM :: "(nat  'a measure)  'a measure  (nat × 'a) measure" where
"Mi_to_NM Mi M  measure_of (space (count_space UNIV M M)) (sets (count_space UNIV M M)) (λA. i. distr (Mi i) (count_space UNIV M M) (λx. (i,x)) A)"

lemma
  shows sets_Mi_to_NM[measurable_cong,simp]: "sets (Mi_to_NM Mi M) = sets (count_space UNIV M M)"
    and space_Mi_to_NM[simp]: "space (Mi_to_NM Mi M) = space (count_space UNIV M M)"
  by(simp_all add: Mi_to_NM_def)

context
  fixes M :: "'a measure" and Mi :: "nat  'a measure"
  assumes sets_Mi[measurable_cong,simp]: "i. sets (Mi i) = sets M"
      and emeasure_Mi: "A. A  sets M  M A = (i. Mi i A)"
begin

lemma emeasure_Mi_to_NM:
  assumes [measurable]: "A  sets (count_space UNIV M M)"
  shows "emeasure (Mi_to_NM Mi M) A = (i. distr (Mi i) (count_space UNIV M M) (λx. (i,x)) A)"
proof(rule emeasure_measure_of[where Ω="space (count_space UNIV M M)" and A="sets (count_space UNIV M M)"])
  show "countably_additive (sets (Mi_to_NM Mi M)) (λA. i. emeasure (distr (Mi i) (count_space UNIV M M) (Pair i)) A)"
    unfolding countably_additive_def
  proof safe
    fix A :: "nat  (nat × _) set"
    assume "range A  sets (Mi_to_NM Mi M)" and dA:"disjoint_family A"
    hence [measurable]: "i. A i  sets (count_space UNIV M M)"
      by auto
    show "(j i. emeasure (distr (Mi i) (count_space UNIV M M) (Pair i)) (A j)) = (i. emeasure (distr (Mi i) (count_space UNIV M M) (Pair i)) ( (range A)))" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (i j. emeasure (distr (Mi i) (count_space UNIV M M) (Pair i)) (A j))"
        by(auto simp: nn_integral_count_space_nat[symmetric] pair_sigma_finite_def sigma_finite_measure_count_space intro!: pair_sigma_finite.Fubini')
      also have "... = ?rhs"
      proof(rule suminf_cong)
        fix n
        have [simp]:"Pair n -`  (range A) = ( (range (λj. Pair n -` A j)))"
          by auto
        show " (j. emeasure (distr (Mi n) (count_space UNIV M M) (Pair n)) (A j)) = emeasure (distr (Mi n) (count_space UNIV M M) (Pair n)) ( (range A))"
          using dA by(fastforce intro!: suminf_emeasure simp: disjoint_family_on_def emeasure_distr)
      qed
      finally show ?thesis .
    qed
  qed
qed(auto simp: positive_def sets.space_closed Mi_to_NM_def)

lemma sigma_finite_Mi_to_NM_measure:
  assumes "i. finite_measure (Mi i)"
  shows "sigma_finite_measure (Mi_to_NM Mi M)"
proof -
  {
    fix n
    assume "emeasure (Mi_to_NM Mi M) ({n} × space M) = "
    moreover have "emeasure (Mi_to_NM Mi M) ({n} × space M) = emeasure (Mi n) (space M)"
      by(simp add:  emeasure_Mi_to_NM emeasure_distr suminf_offset[of _ "Suc n"])
    ultimately have False
      using finite_measure.finite_emeasure_space[OF assms[of n]] by(auto simp: sets_eq_imp_space_eq[OF sets_Mi])
  }
  thus ?thesis
    by(auto intro!: exI[where x="i. {{i} × space M}"] simp: space_pair_measure sigma_finite_measure_def)
qed


lemma distr_Mi_to_NM_M: "distr (Mi_to_NM Mi M) M snd = M"
proof -
  have [simp]:"Pair i -` snd -` A  Pair i -` space (count_space UNIV M M) = A" if "A  sets M" for A and i :: nat
    using sets.sets_into_space[OF that] by(auto simp: space_pair_measure)
  show ?thesis
    by(auto intro!: measure_eqI simp: emeasure_distr emeasure_Mi_to_NM emeasure_Mi)
qed

end

context
  fixes μ :: "'a measure"
  assumes standard_borel_ne: "standard_borel_ne μ"
      and s_finite: "s_finite_measure μ"
begin

interpretation μ : s_finite_measure μ by fact

interpretation n_μ: standard_borel_ne "count_space (UNIV :: nat set) M μ"
  by (simp add: pair_standard_borel_ne standard_borel_ne)

lemma exists_push_forward:
 "(μ' :: real measure) f. f  borel M μ  sets μ' = sets borel  sigma_finite_measure μ'
                            distr μ' μ f = μ"
proof -
  obtain μi where μi: "i. sets (μi i) = sets μ" "i. finite_measure (μi i)" "A. μ A = (i. μi i A)"
    by(metis μ.finite_measures')
  show ?thesis
  proof(safe intro!: exI[where x="distr (Mi_to_NM μi μ) borel n_μ.to_real"] exI[where x="snd  n_μ.from_real"])
    have [simp]:"distr (distr (Mi_to_NM μi μ) borel n_μ.to_real) (count_space UNIV M μ) n_μ.from_real = Mi_to_NM μi μ"
      by(auto simp: distr_distr comp_def intro!:distr_id')
    show "sigma_finite_measure (distr (Mi_to_NM μi μ) borel n_μ.to_real)"
      by(rule sigma_finite_measure_distr[where N="count_space UNIV M μ" and f=n_μ.from_real]) (auto intro!: sigma_finite_Mi_to_NM_measure μi)
  next
    have [simp]: "distr (Mi_to_NM μi μ) μ (snd  n_μ.from_real  n_μ.to_real) =  distr (Mi_to_NM μi μ) μ snd"
      by(auto intro!: distr_cong[OF refl])
    show "distr (distr (Mi_to_NM μi μ) borel n_μ.to_real) μ (snd  n_μ.from_real) = μ"
      by(auto simp: distr_distr distr_Mi_to_NM_M[OF μi(1,3)])
  qed auto
qed

abbreviation "μ'_and_f  (SOME (μ'::real measure,f). f  borel M μ  sets μ' = sets borel  sigma_finite_measure μ'  distr μ' μ f = μ)"

definition "sigma_pair_μ  fst μ'_and_f"
definition "sigma_pair_f  snd μ'_and_f"

lemma
  shows sigma_pair_f_measurable : "sigma_pair_f  borel M μ" (is ?g1)
    and sets_sigma_pair_μ: "sets sigma_pair_μ = sets borel" (is ?g2)
    and sigma_finite_sigma_pair_μ: "sigma_finite_measure sigma_pair_μ" (is ?g3)
    and distr_sigma_pair: "distr sigma_pair_μ μ sigma_pair_f = μ" (is ?g4)
proof -
  have "case μ'_and_f of (μ',f)  f  borel M μ  sets μ' = sets borel  sigma_finite_measure μ'  distr μ' μ f = μ"
    by(rule someI_ex) (use exists_push_forward in auto)
  then show ?g1 ?g2 ?g3 ?g4
    by(auto simp: sigma_pair_μ_def sigma_pair_f_def split_beta)
qed

end

definition s_finite_measure_algebra :: "'a measure  'a measure measure" where
  "s_finite_measure_algebra K =
    (SUP A  sets K. vimage_algebra {M. s_finite_measure M  sets M = sets K} (λM. emeasure M A) borel)"

lemma space_s_finite_measure_algebra:
 "space (s_finite_measure_algebra K) = {M. s_finite_measure M  sets M = sets K}"
  by (auto simp add: s_finite_measure_algebra_def space_Sup_eq_UN)

lemma s_finite_measure_algebra_cong: "sets M = sets N  s_finite_measure_algebra M = s_finite_measure_algebra N"
  by (simp add: s_finite_measure_algebra_def)

lemma measurable_emeasure_s_finite_measure_algebra[measurable]:
  "a  sets A  (λM. emeasure M a)  borel_measurable (s_finite_measure_algebra A)"
  by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: s_finite_measure_algebra_def)

lemma measurable_measure_s_finite_measure_algebra[measurable]:
  "a  sets A  (λM. measure M a)  borel_measurable (s_finite_measure_algebra A)"
  unfolding measure_def by measurable

lemma s_finite_measure_algebra_measurableD:
  assumes N: "N  measurable M (s_finite_measure_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_s_finite_measure_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)

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

lemma s_finite_measure_algebra_kernel: "a  space M  s_finite_measure (K a)"
  using measurable_space[OF K] by (simp add: space_s_finite_measure_algebra)

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

lemma measurable_emeasure_kernel_s_finite_measure_algebra[measurable]:
    "A  sets N  (λa. emeasure (K a) A)  borel_measurable M"
  using measurable_compose[OF K measurable_emeasure_s_finite_measure_algebra] .

end

lemma measurable_s_finite_measure_algebra:
  "(a. a  space M  s_finite_measure (K a)) 
  (a. a  space M  sets (K a) = sets N) 
  (A. A  sets N  (λa. emeasure (K a) A)  borel_measurable M) 
  K  measurable M (s_finite_measure_algebra N)"
  by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: s_finite_measure_algebra_def)

definition bind_kernel :: "'a measure  ('a  'b measure)  'b measure" (infixl k 54) where
"bind_kernel M k = (if space M = {} then count_space {} else
    let Y = k (SOME x. x  space M) in
     measure_of (space Y) (sets Y) (λB. +x. (k x B) M))"

lemma bind_kernel_cong_All:
  assumes "x. x  space M  f x = g x"
  shows "M k f = M k g"
proof(cases "space M = {}")
  case 1:False
  have "(SOME x. x  space M)  space M"
    by (rule someI_ex) (use 1 in blast)
  with assms have [simp]:"f (SOME x. x  space M) = g (SOME x. x  space M)" by simp
  have "(λB. + x. emeasure (f x) B M) = (λB. + x. emeasure (g x) B M)"
    by standard (auto intro!: nn_integral_cong simp: assms)
  thus ?thesis
    by(auto simp: bind_kernel_def 1)
qed(simp add: bind_kernel_def)

lemma sets_bind_kernel:
  assumes "x. x  space M  sets (k x) = sets N" "space M  {}"
  shows "sets (M k k) = sets N"
proof -
  have "sets (k (SOME x. x  space M)) = sets N"
    by(rule someI2_ex) (use assms in auto)
  with sets_eq_imp_space_eq[OF this] show ?thesis
    by(simp add: bind_kernel_def assms(2))
qed

subsection ‹ Measure Kernel ›
locale measure_kernel =
  fixes X :: "'a measure" and Y :: "'b measure" and κ :: "'a  'b measure"
  assumes kernel_sets[measurable_cong]: "x. x  space X  sets (κ x) = sets Y"
      and emeasure_measurable[measurable]: "B. B  sets Y  (λx. emeasure (κ x) B)  borel_measurable X"
      and Y_not_empty: "space X  {}  space Y  {}"
begin

lemma kernel_space :"x. x  space X  space (κ x) = space Y"
  by (meson kernel_sets sets_eq_imp_space_eq)

lemma measure_measurable:
  assumes "B  sets Y"
  shows "(λx. measure (κ x) B)  borel_measurable X"
  using emeasure_measurable[OF assms] by (simp add: Sigma_Algebra.measure_def)

lemma set_nn_integral_measure:
  assumes [measurable_cong]: "sets μ = sets X" and [measurable]: "A  sets X" "B  sets Y"
  defines "ν  measure_of (space Y) (sets Y) (λB. +xA. (κ x B) μ)"
  shows "ν B = (+xA. (κ x B) μ)"
proof -
  have nu_sets[measurable_cong]: "sets ν = sets Y"
    by(simp add: ν_def)
  have "positive (sets Y) (λB. +xA. (κ x B) μ)"
    by(simp add: positive_def)
  moreover have "countably_additive (sets Y) (λB. +xA. (κ x B) μ)"
    unfolding countably_additive_def
  proof safe
    fix C :: "nat  _"
    assume h:"range C  sets Y" "disjoint_family C"
    thus "(i. +xA. (κ x) (C i)μ) = (+xA. (κ x) ( (range C))μ)"
      by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF assms(1)] kernel_sets suminf_emeasure nn_integral_suminf[symmetric])
  qed
  ultimately show ?thesis
    using ν_def assms(3) emeasure_measure_of_sigma sets.sigma_algebra_axioms by blast
qed

corollary nn_integral_measure:
  assumes "sets μ = sets X" "B  sets Y"
  defines "ν  measure_of (space Y) (sets Y) (λB. +x. (κ x B) μ)"
  shows "ν B = (+x. (κ x B) μ)"
  using set_nn_integral_measure[OF assms(1) sets.top assms(2)]
  by(simp add: ν_def sets_eq_imp_space_eq[OF assms(1),symmetric])

lemma distr_measure_kernel:
  assumes [measurable]:"f  Y M Z"
  shows "measure_kernel X Z (λx. distr (κ x) Z f)"
  unfolding measure_kernel_def
proof safe
  fix B
  assume B[measurable]: "B  sets Z"
  show "(λx. emeasure (distr (κ x) Z f) B)  borel_measurable X"
    by(rule measurable_cong[where g= "(λx. κ x (f -` B  space Y))",THEN iffD2]) (auto simp: emeasure_distr sets_eq_imp_space_eq[OF kernel_sets])
next
  show "x. space Z = {}  x  space X  x  {}"
    by (metis Y_not_empty assms measurable_empty_iff)
qed auto

lemma measure_kernel_comp:
  assumes [measurable]: "f  W M X"
  shows "measure_kernel W Y (λx. κ (f x))"
  using measurable_space[OF assms] kernel_sets Y_not_empty
  by(auto simp: measure_kernel_def)

lemma emeasure_bind_kernel:
  assumes "sets μ = sets X" "B  sets Y" "space X  {}"
  shows "(μ k κ) B = (+x. (κ x B) μ)"
proof -
  have "sets (κ (SOME x. x  space μ)) = sets Y"
    by(rule someI2_ex) (use assms(3) kernel_sets sets_eq_imp_space_eq[OF assms(1)] in auto)
  with sets_eq_imp_space_eq[OF this] show ?thesis
    by(simp add: bind_kernel_def sets_eq_imp_space_eq[OF assms(1) ]assms(3) nn_integral_measure[OF assms(1,2)])
qed

lemma measure_bind_kernel:
  assumes [measurable_cong]:"sets μ = sets X" and [measurable]:"B  sets Y" "space X  {}" "AE x in μ. κ x B < "
  shows "measure (μ k κ) B = (x. measure (κ x) B μ)"
  using assms(4) by(auto simp: emeasure_bind_kernel[OF assms(1-3)] measure_def integral_eq_nn_integral intro!: arg_cong[of _ _ enn2real] nn_integral_cong_AE)

lemma sets_bind_kernel:
  assumes "space X  {}" "sets μ = sets X"
  shows "sets (μ k κ) = sets Y"
  using sets_bind_kernel[of μ κ, OF kernel_sets,simplified sets_eq_imp_space_eq[OF assms(2)]]
  by(auto simp: assms(1))

lemma distr_bind_kernel:
  assumes "space X  {}" and [measurable_cong]:"sets μ = sets X" and [measurable]: "f  Y M Z"
  shows "distr (μ k κ) Z f = μ k (λx. distr (κ x) Z f)"
proof -
  {
    fix A
    assume A[measurable]:"A  sets Z"
    have sets[measurable_cong]:"sets (μ k κ) = sets Y"
      by(rule sets_bind_kernel[OF assms(1,2)])
    have "emeasure (distr (μ k κ) Z f) A = emeasure (μ k (λx. distr (κ x) Z f)) A" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (+ x. emeasure (κ x) (f -` A  space Y) μ)"
        by(simp add: emeasure_distr sets_eq_imp_space_eq[OF sets] emeasure_bind_kernel[OF assms(2) _ assms(1)])
      also have "... = (+ x. emeasure (distr (κ x) Z f) A μ)"
        by(auto simp: emeasure_distr sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] intro!: nn_integral_cong)
      also have "... = ?rhs"
        by(simp add: measure_kernel.emeasure_bind_kernel[OF distr_measure_kernel[OF assms(3)] assms(2) _ assms(1)])
      finally show ?thesis .
    qed
  }
  thus ?thesis
    by(auto intro!: measure_eqI simp: measure_kernel.sets_bind_kernel[OF distr_measure_kernel[OF assms(3)] assms(1,2)])
qed

lemma bind_kernel_distr:
  assumes [measurable]: "f  W M X" and "space W  {}"
  shows "distr W X f k κ = W k (λx. κ (f x))"
proof -
  have X: "space X  {}"
    using measurable_space[OF assms(1)] assms(2) by auto
  show ?thesis
    by(rule measure_eqI, insert X) (auto simp: sets_bind_kernel[OF X] measure_kernel.sets_bind_kernel[OF measure_kernel_comp[OF assms(1)] assms(2) refl] emeasure_bind_kernel nn_integral_distr measure_kernel.emeasure_bind_kernel[OF  measure_kernel_comp[OF assms(1)] refl _ assms(2)])
qed

lemma bind_kernel_return:
  assumes "x  space X"
  shows "return X x k κ = κ x"
proof -
  have X: "space X  {}"
    using assms by auto
  show ?thesis
    by(rule measure_eqI) (auto simp: sets_bind_kernel[OF X sets_return] kernel_sets[OF assms] emeasure_bind_kernel[OF sets_return,simplified,OF _ X] nn_integral_return[OF assms])
qed

lemma kernel_nn_integral_measurable:
  assumes "f  borel_measurable Y"
  shows "(λx. + y. f y (κ x))  borel_measurable X"
  using assms
proof induction
  case (cong f g)
  then show ?case
    by(auto intro!: measurable_cong[where f="λx. + y. f y (κ x)" and g= "λx. + y. g y (κ x)",THEN iffD2] nn_integral_cong simp: sets_eq_imp_space_eq[OF kernel_sets])
next
  case (set A)
  then show ?case
    by(auto intro!: measurable_cong[where f="λx. integralN (κ x) (indicator A)" and g="λx. κ x A",THEN iffD2])
next
  case (mult u c)
  then show ?case
    by(auto intro!: measurable_cong[where f="λx. + y. c * u y κ x" and g="λx. c * + y. u y κ x",THEN iffD2] simp: nn_integral_cmult)
next
  case (add u v)
  then show ?case
    by(auto intro!: measurable_cong[where f="λx. + y. v y + u y κ x" and g="λx. (+ y. v y κ x) + (+ y. u y κ x)",THEN iffD2] simp: nn_integral_add)
next
  case (seq U)
  then show ?case
    by(intro measurable_cong[where f="λx. integralN (κ x) ( range U)" and g="λx. i. integralN (κ x) (U i)",THEN iffD2])
      (auto simp: nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[symmetric]])
qed

lemma bind_kernel_measure_kernel:
  assumes "measure_kernel Y Z k'"
  shows "measure_kernel X Z (λx. κ x k k')"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by(auto simp: measure_kernel_def measurable_def)
next
  case X:False
  then have Y: "space Y  {}"
    by(simp add: Y_not_empty)
  interpret k': measure_kernel Y Z k' by fact
  show ?thesis
  proof
    fix B
    assume "B  sets Z"
    with k'.emeasure_bind_kernel[OF kernel_sets,of _ B] show "(λx. emeasure (κ x k k') B)  borel_measurable X"
      by(auto intro!: measurable_cong[where f="λx. emeasure (κ x k k') B" and g="λx. + y. emeasure (k' y) B κ x",THEN iffD2] kernel_nn_integral_measurable simp: sets_eq_imp_space_eq[OF kernel_sets] Y)
  qed(use k'.Y_not_empty Y  k'.sets_bind_kernel[OF Y kernel_sets] in auto)
qed

lemma restrict_measure_kernel: "measure_kernel (restrict_space X A) Y κ"
proof
  fix B
  assume "B  sets Y"
  from emeasure_measurable[OF this] show "(λx. emeasure (κ x) B)  borel_measurable (restrict_space X A)"
    using measurable_restrict_space1 by blast
qed(insert Y_not_empty,auto simp add: space_restrict_space kernel_sets)

end

lemma measure_kernel_cong_sets:
  assumes "sets X = sets X'" "sets Y = sets Y'"
  shows "measure_kernel X Y = measure_kernel X' Y'"
  by standard (simp add: measure_kernel_def measurable_cong_sets[OF assms(1) refl] sets_eq_imp_space_eq[OF assms(1)] assms(2) sets_eq_imp_space_eq[OF assms(2)])

lemma measure_kernel_pair_countble1:
  assumes "countable A" "i. i  A  measure_kernel X Y (λx. k (i,x))"
  shows "measure_kernel (count_space A M X) Y k"
  using assms by(auto simp: measure_kernel_def space_pair_measure intro!: measurable_pair_measure_countable1)

lemma measure_kernel_empty_trivial:
  assumes "space X = {}"
  shows "measure_kernel X Y k"
  using assms by(auto simp: measure_kernel_def measurable_def)

subsection ‹ Finite Kernel ›
locale finite_kernel = measure_kernel +
  assumes finite_measure_spaces: "r<. x space X. κ x (space Y) < r"
begin

lemma finite_measures:
  assumes "x  space X"
  shows "finite_measure (κ x)"
proof-
  obtain r where "κ x (space Y) < r"
    using finite_measure_spaces assms by metis
  then show ?thesis
    by(auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF kernel_sets[OF assms]])
qed

end

lemma finite_kernel_empty_trivial: "space X = {}  finite_kernel X Y f"
  by(auto simp: finite_kernel_def finite_kernel_axioms_def measure_kernel_empty_trivial intro!: exI[where x=1])

lemma finite_kernel_cong_sets:
  assumes "sets X = sets X'" "sets Y = sets Y'"
  shows "finite_kernel X Y = finite_kernel X' Y'"
  by standard (auto simp: measure_kernel_cong_sets[OF assms] finite_kernel_def finite_kernel_axioms_def sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF assms(2)])

subsection ‹ Sub-Probability Kernel›
locale subprob_kernel = measure_kernel +
  assumes subprob_spaces: "x. x  space X  subprob_space (κ x)"
begin
lemma subprob_space:
 "x. x  space X  κ x (space Y)  1"
  by (simp add: subprob_space.subprob_emeasure_le_1 subprob_spaces)

lemma subprob_measurable[measurable]:
 "κ  X M subprob_algebra Y"
  by(auto intro!: measurable_subprob_algebra_generated[OF sets.sigma_sets_eq[symmetric] sets.Int_stable sets.space_closed] simp: subprob_spaces kernel_sets emeasure_measurable)

lemma finite_kernel: "finite_kernel X Y κ"
  by(auto simp: finite_kernel_def finite_kernel_axioms_def intro!: measure_kernel_axioms exI[where x=2] order.strict_trans1[OF subprob_space.subprob_emeasure_le_1[OF subprob_spaces]])

sublocale finite_kernel
  by (rule finite_kernel)

end

lemma subprob_kernel_def':
 "subprob_kernel X Y κ  κ  X M subprob_algebra Y"
  by(auto simp: subprob_kernel.subprob_measurable subprob_kernel_def subprob_kernel_axioms_def measure_kernel_def measurable_subprob_algebra measurable_empty_iff space_subprob_algebra_empty_iff)
    (auto simp: subprob_measurableD(2) subprob_space_kernel)

lemmas subprob_kernelI = measurable_subprob_algebra[simplified subprob_kernel_def'[symmetric]]

lemma subprob_kernel_cong_sets:
  assumes "sets X = sets X'" "sets Y = sets Y'"
  shows "subprob_kernel X Y = subprob_kernel X' Y'"
  by standard (auto simp: subprob_kernel_def' subprob_algebra_cong[OF assms(2)] measurable_cong_sets[OF assms(1) refl])

lemma subprob_kernel_empty_trivial:
  assumes "space X = {}"
  shows "subprob_kernel X Y k"
  using assms by(auto simp: subprob_kernel_def subprob_kernel_axioms_def intro!: measure_kernel_empty_trivial)

lemma bind_kernel_bind:
  assumes "f  M M subprob_algebra N"
  shows "M k f = M  f"
proof(cases "space M = {}")
  case True
  then show ?thesis
    by(simp add: bind_kernel_def bind_def)
next
  case h:False
  interpret subprob_kernel M N f
    using assms(1) by(simp add: subprob_kernel_def')
  show ?thesis
    by(rule measure_eqI,insert sets_kernel[OF assms]) (auto simp: h sets_bind_kernel emeasure_bind_kernel[OF refl _ h] emeasure_bind[OF h assms])
qed

lemma(in measure_kernel) subprob_kernel_sum:
  assumes "x. x  space X  finite_measure (κ x)"
  obtains ki where "i. subprob_kernel X Y (ki i)" "A x. x  space X  κ x A = (i. ki i x A)"
proof -
  obtain u where u: "x. x  space X  u x < " "x. x  space X  u x = κ x (space Y)"
    using finite_measure.emeasure_finite[OF assms]
    by (simp add: top.not_eq_extremum)  
  have [measurable]: "u  borel_measurable X"
    by(simp cong: measurable_cong add: u(2))
  define ki where "ki  (λi x. if i < nat enn2real (u x) then scale_measure  (1 / ennreal (real_of_int enn2real (u x))) (κ x) else (sigma (space Y) (sets Y)))"
  have 1:"i x. x  space X  sets (ki i x) = sets Y"
    by(auto simp: ki_def kernel_sets)
  have "subprob_kernel X Y (ki i)" for i
  proof -
    {
      fix i B
      assume [measurable]: "B  sets Y"
      have "(λx. emeasure (ki i x) B) = (λx. if i < nat enn2real (u x) then (1 / ennreal (real_of_int enn2real (u x))) * emeasure (κ x) B else 0)"
        by(auto simp: ki_def emeasure_sigma)
      also have "...  borel_measurable X"
        by simp
      finally have "(λx. emeasure (ki i x) B)  borel_measurable X" .
    }
    moreover {
      fix i x
      assume x:"x  space X"
      have "emeasure (ki i x) (space Y)  1"
        by(cases "u x = 0",auto simp: ki_def emeasure_sigma u(2)[OF x,symmetric]) (metis u(1)[OF x,simplified] divide_ennreal_def divide_le_posI_ennreal enn2real_le le_of_int_ceiling mult.commute mult.right_neutral not_gr_zero order.strict_iff_not)
      hence "subprob_space (ki i x)"
        using x Y_not_empty by(fastforce intro!: subprob_spaceI simp: sets_eq_imp_space_eq[OF 1[OF x]])
    }
    ultimately show ?thesis
      by(auto simp: subprob_kernel_def measure_kernel_def 1 Y_not_empty subprob_kernel_axioms_def)
  qed
  moreover have "κ x A = (i. ki i x A)" if x:"x  space X" for x A
  proof (cases "A  sets Y")
    case A[measurable]:True
    have "emeasure (κ x) A = (i<nat enn2real (u x). emeasure (ki i x) A)"
    proof(cases "u x = 0")
      case True
      then show ?thesis
        using u(2)[OF that] by simp (metis A emeasure_eq_0 kernel_sets sets.sets_into_space sets.top x)
    next
      case u0:False
      hence "real_of_int enn2real (u x) > 0"
        by (metis enn2real_nonneg ennreal_0 ennreal_enn2real_if infinity_ennreal_def linorder_not_le nat_0_iff nle_le of_int_le_0_iff of_nat_eq_0_iff real_nat_ceiling_ge u(1) x)
      with u(1)[OF x] have "of_nat (nat enn2real (u x)) / ennreal (real_of_int enn2real (u x)) = 1"
        by(simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
      thus ?thesis
        by(simp add: ki_def ennreal_divide_times[symmetric]  mult.assoc[symmetric])
    qed
    then show ?thesis
      by(auto simp: suminf_offset[of "λi. emeasure (ki i x) A" "nat enn2real (u x)"]) (simp add: ki_def emeasure_sigma)
  next
    case False
    then show ?thesis
      using kernel_sets[OF x] 1[OF x]
      by(simp add: emeasure_notin_sets)
  qed
  ultimately show ?thesis
    using that by blast
qed

subsection ‹ Probability Kernel ›
locale prob_kernel = measure_kernel +
  assumes prob_spaces: "x. x  space X  prob_space (κ x)"
begin

lemma prob_space:
 "x. x  space X  κ x (space Y) = 1"
  using kernel_space prob_space.emeasure_space_1 prob_spaces by fastforce

lemma prob_measurable[measurable]:
 "κ  X M prob_algebra Y"
  by(auto intro!: measurable_prob_algebra_generated[OF sets.sigma_sets_eq[symmetric] sets.Int_stable sets.space_closed] simp: prob_spaces kernel_sets emeasure_measurable)

lemma subprob_kernel: "subprob_kernel X Y κ"
  by (simp add: measurable_prob_algebraD subprob_kernel_def')

sublocale subprob_kernel
  by (simp add: subprob_kernel)

lemma restrict_probability_kernel:
  "prob_kernel (restrict_space X A) Y κ"
  by(auto simp: prob_kernel_def restrict_measure_kernel prob_kernel_axioms_def space_restrict_space prob_spaces)

end

lemma prob_kernel_def':
 "prob_kernel X Y κ  κ  X M prob_algebra Y"
proof
  assume h:"κ  X M prob_algebra Y"
  show "prob_kernel X Y κ"
    using subprob_measurableD(2)[OF measurable_prob_algebraD[OF h]] measurable_space[OF h] measurable_emeasure_kernel[OF  measurable_prob_algebraD[OF h]]
    by(auto simp: prob_kernel_def measure_kernel_def prob_kernel_axioms_def space_prob_algebra ) (metis prob_space.not_empty sets_eq_imp_space_eq)
qed(auto simp: prob_kernel.prob_measurable prob_kernel_def prob_kernel_axioms_def measure_kernel_def)


lemma bind_kernel_return'':
  assumes "sets M = sets N"
  shows "M k return N = M"
proof(cases "space M = {}")
  case True
  then show ?thesis
    by(simp add: bind_kernel_def space_empty[symmetric])
next
  case False
  then have 1: "space N  {}"
    by(simp add: sets_eq_imp_space_eq[OF assms])
  interpret prob_kernel N N "return N"
    by(simp add: prob_kernel_def')
  show ?thesis
    by(rule measure_eqI) (auto simp: emeasure_bind_kernel[OF assms _ 1] sets_bind_kernel[OF 1 assms] assms)
qed

subsection‹ S-Finite Kernel ›
locale s_finite_kernel = measure_kernel +
  assumes s_finite_kernel_sum: "ki. (i. finite_kernel X Y (ki i)  (xspace X. Asets Y. κ x A = (i. ki i x A)))"

lemma s_finite_kernel_subI:
  assumes "x. x  space X  sets (κ x) = sets Y" "i. subprob_kernel X Y (ki i)" "x A. x  space X  A  sets Y  emeasure (κ x) A = (i. ki i x A)"
  shows "s_finite_kernel X Y κ"
proof -
  interpret measure_kernel X Y κ
  proof
    show "B  sets Y  (λx. emeasure (κ x) B)  borel_measurable X" for B
      using assms(2) by(simp add: assms(3) subprob_kernel_def' cong: measurable_cong)
  next
    show "space X  {}  space Y  {}"
      using assms(2)[of 0] by(auto simp: subprob_kernel_def measure_kernel_def)
  qed fact
  show ?thesis
    by (auto simp: s_finite_kernel_def measure_kernel_axioms s_finite_kernel_axioms_def assms(2,3) intro!: exI[where x=ki] subprob_kernel.finite_kernel)
qed

context s_finite_kernel
begin

lemma s_finite_kernels_fin:
  obtains ki where "i. finite_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
proof -
  obtain ki where ki:"i. finite_kernel X Y (ki i)" "x A. x  space X  A  sets Y  κ x A = (i. ki i x A)"
    by(metis s_finite_kernel_sum)
  hence "κ x A = (i. ki i x A)" if "x  space X " for x A
    by(cases "A  sets Y", insert that kernel_sets[OF that]) (auto simp: finite_kernel_def measure_kernel_def emeasure_notin_sets)
  with ki show ?thesis
    using that by auto
qed

lemma s_finite_kernels:
  obtains ki where "i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
proof -
  obtain ki where ki:"i. finite_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by(metis s_finite_kernels_fin)
  have "kij. (j. subprob_kernel X Y (kij j))  (x A. x  space X  ki i x A = (j. kij j x A))" for i
    using measure_kernel.subprob_kernel_sum[of X Y "ki i", OF _ finite_kernel.finite_measures[OF ki(1)[of i]]] ki(1)[of i] by(metis finite_kernel_def)
  then obtain kij where kij: "i j. subprob_kernel X Y (kij i j)" "x A i. x  space X  ki i x A = (j. kij i j x A)"
    by metis
  have "i. subprob_kernel X Y (case_prod kij (prod_decode i))"
    using kij(1) by(auto simp: split_beta)
  moreover have "x  space X  κ x A = (i. case_prod kij (prod_decode i) x A)" for x A
    using suminf_ennreal_2dimen[of "λi. ki i x A" "λ(i,j). kij i j x A"]
    by(auto simp: ki(2) kij(2) split_beta')
  ultimately show ?thesis
    using that by fastforce
qed

lemma image_s_finite_measure:
  assumes "x  space X"
  shows "s_finite_measure (κ x)"
proof -
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by(metis s_finite_kernels)
  show ?thesis
    using ki(1)[simplified subprob_kernel_def'] measurable_space[OF ki(1)[simplified subprob_kernel_def'] assms]
    by(auto intro!: s_finite_measureI[where Mi="λi. ki i x"] subprob_space.axioms(1) simp: kernel_sets[OF assms] space_subprob_algebra ki(2)[OF assms])
qed

corollary kernel_measurable_s_finite[measurable]:"κ  X M s_finite_measure_algebra Y"
  by(auto intro!: measurable_s_finite_measure_algebra simp: kernel_sets image_s_finite_measure)

lemma comp_measurable:
  assumes f[measurable]:"f  M M X"
  shows "s_finite_kernel M Y (λx. κ (f x))"
proof -
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by(metis s_finite_kernels)
  show ?thesis
    using ki(1) measurable_space[OF f] by(auto intro!: s_finite_kernel_subI[where ki="λi x. ki i (f x)"] simp: subprob_kernel_def' ki(2) kernel_sets)
qed

lemma distr_s_finite_kernel:
  assumes f[measurable]: "f  Y M Z"
  shows "s_finite_kernel X Z (λx. distr (κ x) Z f)"
proof -
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by(metis s_finite_kernels)
  hence 1:"x  space X  space (ki i x) = space Y" for x i
    by(auto simp: subprob_kernel_def' intro!: subprob_measurableD(1)[of _ X Y])
  have [measurable]:"B  sets Z  (λx. emeasure (distr (κ x) Z f) B)  borel_measurable X" for B
    by(rule measurable_cong[where g="λx. κ x (f -` B  space Y)", THEN iffD2]) (auto simp: emeasure_distr sets_eq_imp_space_eq[OF kernel_sets])
  show ?thesis
    using ki(1) measurable_distr[OF f] by(auto intro!: s_finite_kernel_subI[where ki="λi x. distr (ki i x) Z f"] simp: subprob_kernel_def' emeasure_distr ki(2) sets_eq_imp_space_eq[OF kernel_sets] 1)
qed

lemma comp_s_finite_measure:
  assumes "s_finite_measure μ" and [measurable_cong]: "sets μ = sets X"
  shows "s_finite_measure (μ k κ)"
proof(cases "space X = {}")
  case 1:True
  show ?thesis
    by(auto simp: sets_eq_imp_space_eq[OF assms(2)] 1 bind_kernel_def intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
next
  case 0:False
  then have 1: "space μ  {}"
    by(simp add: sets_eq_imp_space_eq[OF assms(2)])
  have 2: "sets (κ (SOME x. x  space μ)) = sets Y"
    by(rule someI2_ex, insert 1 kernel_sets) (auto simp: sets_eq_imp_space_eq[OF assms(2)])
  have sets_bind[measurable_cong]: "sets (μ k κ) = sets Y"
    by(simp add: bind_kernel_def 1 sets_eq_imp_space_eq[OF 2] 2)
  obtain μi where mui[measurable_cong]: "i. sets (μi i) = sets X" "i. (μi i) (space X)  1" "A. μ A = (i. μi i A)"
    using s_finite_measure.finite_measures[OF assms(1)] assms(2) sets_eq_imp_space_eq[OF assms(2)] by metis
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by(metis s_finite_kernels)
  define Mi where "Mi  (λn. (λ(i,j). measure_of (space Y) (sets Y) (λA. +x. (ki i x A) (μi j))) (prod_decode n))"
  have emeasure:"(μ k κ) A = (i. (Mi i) A)" (is "?lhs = ?rhs") if "A  sets Y" for A
  proof -
    have "?lhs = (+x. (κ x A) μ)"
      by(simp add: emeasure_bind_kernel[OF assms(2) that 0])
    also have "... = (+x. (i. (ki i x A)) μ)"
      by(auto intro!: nn_integral_cong simp: ki sets_eq_imp_space_eq[OF assms(2)])
    also have "... = (i. +x. (ki i x A) μ)"
      by(auto intro!: nn_integral_suminf) (metis ki(1) assms(2) measurable_cong_sets measure_kernel.emeasure_measurable subprob_kernel_def that)
    also have "... = ?rhs"
      unfolding Mi_def
    proof(rule suminf_ennreal_2dimen[symmetric])
      fix m
      interpret kim: subprob_kernel X Y "ki m"
        by(simp add: ki)
      show "(+ x. (ki m x) A μ) = (n. emeasure (case (m, n) of (i, j)  measure_of (space Y) (sets Y) (λA. + x. emeasure (ki i x) A μi j)) A)"
        using kim.emeasure_measurable[OF that] by(simp add: kim.nn_integral_measure[OF mui(1) that] nn_integral_measure_suminf[OF mui(1)[simplified assms(2)[symmetric]] mui(3)])
    qed
    finally show ?thesis .
  qed
  have fin:"finite_measure (Mi i)" for i
  proof(rule prod.exhaust[where y="prod_decode i"])
    fix j1 j2
      interpret kij: subprob_kernel X Y "ki j1"
        by(simp add: ki)
    assume pd:"prod_decode i = (j1, j2)"
    have "Mi i (space (Mi i)) = (+x. (ki j1 x (space Y)) μi j2)"
      by(auto simp: Mi_def pd kij.nn_integral_measure[OF mui(1) sets.top])
    also have "...  (+x. 1 μi j2)"
      by(intro nn_integral_mono) (metis kij.subprob_space mui(1) sets_eq_imp_space_eq)
    also have "...  1"
      using mui by (simp add: sets_eq_imp_space_eq[OF mui(1)])
    finally show "finite_measure (Mi i)"
      by (metis ennreal_one_less_top finite_measureI infinity_ennreal_def less_le_not_le)
  qed
  have 3: "sets (Mi i) = sets (μ k κ)" for i
    by(simp add: Mi_def split_beta sets_bind)
  show "s_finite_measure (μ k κ)"
    using emeasure fin 3 by (auto intro!: exI[where x=Mi] simp: s_finite_measure_def sets_bind)
qed

end

lemma s_finite_kernel_empty_trivial:
  assumes "space X = {}"
  shows "s_finite_kernel X Y k"
  using assms by(auto simp: s_finite_kernel_def s_finite_kernel_axioms_def intro!: measure_kernel_empty_trivial finite_kernel_empty_trivial)

lemma s_finite_kernel_def': "s_finite_kernel X Y κ  ((x. x  space X  sets (κ x) = sets Y)  (ki. (i. subprob_kernel X Y (ki i))  (x A. x  space X  A  sets Y  emeasure (κ x) A = (i. ki i x A))))" (is "?l  ?r")
proof
  assume ?l
  then interpret s_finite_kernel X Y κ .
  from s_finite_kernels obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  emeasure (κ x) A = (i. emeasure (ki i x) A)"
    by metis
  thus ?r
    by(auto simp: kernel_sets)
qed(auto intro!: s_finite_kernel_subI)

lemma(in finite_kernel) s_finite_kernel_finite_kernel: "s_finite_kernel X Y κ"
proof
  consider "space X = {}" | "space X  {}" by auto
  then show "ki. i. finite_kernel X Y (ki i)  (xspace X. Asets Y. (κ x) A = (i. (ki i x) A))"
  proof cases
    case 1
    then show ?thesis
      by(auto simp: finite_kernel_def measure_kernel_def finite_kernel_axioms_def measurable_def intro!: exI[where x=0])
  next
    case 2
    then have y:"space Y  {}" by(simp add: Y_not_empty)
    define ki where "ki i  case i of 0  κ | Suc _  (λ_. sigma (space Y) (sets Y))" for i
    have "finite_kernel X Y (ki i)" for i
      by (cases i, auto simp: ki_def finite_kernel_axioms) (auto simp: emeasure_sigma finite_kernel_def measure_kernel_def finite_kernel_axioms_def y intro!: finite_measureI exI[where x=1])
    moreover have "(κ x) A = (i. (ki i x) A)" for x A
      by(simp add: suminf_offset[where i="Suc 0" and f="λi. ki i x A",simplified],simp add: ki_def emeasure_sigma)
    ultimately show ?thesis by auto
  qed
qed

lemmas(in subprob_kernel) s_finite_kernel_subprob_kernel = s_finite_kernel_finite_kernel
lemmas(in prob_kernel) s_finite_kernel_prob_kernel = s_finite_kernel_subprob_kernel

sublocale finite_kernel  s_finite_kernel
  by(rule s_finite_kernel_finite_kernel)

lemma s_finite_kernel_cong_sets:
  assumes "sets X = sets X'" "sets Y = sets Y'"
  shows "s_finite_kernel X Y = s_finite_kernel X' Y'"
  by standard (simp add: s_finite_kernel_def measurable_cong_sets[OF assms(1) refl] sets_eq_imp_space_eq[OF assms(1)] assms(2) measure_kernel_cong_sets[OF assms] s_finite_kernel_axioms_def finite_kernel_cong_sets[OF assms])

lemma(in s_finite_kernel) s_finite_kernel_cong:
  assumes "x. x  space X  κ x = g x"
  shows "s_finite_kernel X Y g"
  using assms s_finite_kernel_axioms by(auto simp: s_finite_kernel_def s_finite_kernel_axioms_def measure_kernel_def cong: measurable_cong)

lemma(in s_finite_measure) s_finite_kernel_const:
  assumes "space M  {}"
  shows "s_finite_kernel X M (λx. M)"
proof
  obtain Mi where Mi:"i. sets (Mi i) = sets M" "i. (Mi i) (space M)  1" "A. M A = (i. Mi i A)"
    by(metis finite_measures)
  hence "i. subprob_kernel X M (λx. Mi i)"
    by(auto simp: subprob_kernel_def' space_subprob_algebra sets_eq_imp_space_eq[OF Mi(1)] assms intro!:measurable_const subprob_spaceI)
  thus "ki. i. finite_kernel X M (ki i)  (xspace X. Asets M. M A = (i. (ki i x) A))"
    by(auto intro!: exI[where x="λi x. Mi i"] Mi(3) subprob_kernel.finite_kernel)
qed (auto simp: assms)

lemma s_finite_kernel_pair_countble1:
  assumes "countable A" "i. i  A  s_finite_kernel X Y (λx. k (i,x))"
  shows "s_finite_kernel (count_space A M X) Y k"
proof -
  have "ki. (j. subprob_kernel X Y (ki j))  (x B. x  space X  B  sets Y  k (i,x) B = (j. ki j x B))" if "i  A" for i
    using s_finite_kernel.s_finite_kernels[OF assms(2)[OF that]] by metis
  then obtain ki where ki:"i j. i  A  subprob_kernel X Y (ki i j)" "i x B. i  A  x  space X  B  sets Y  k (i,x) B = (j. ki i j x B)"
     by metis
  then show ?thesis
    using assms(2) by(auto simp: s_finite_kernel_def' measure_kernel_pair_countble1[OF assms(1)] subprob_kernel_def' space_pair_measure intro!: exI[where x="λj (i,x). ki i j x"] measurable_pair_measure_countable1 assms(1))
qed

lemma s_finite_kernel_s_finite_kernel:
  assumes "i. s_finite_kernel X Y (ki i)" "x. x  space X  sets (k x) = sets Y" "x A. x  space X  A  sets Y  emeasure (k x) A = (i. (ki i) x A)"
  shows "s_finite_kernel X Y k"
proof -
  have "kij. (j. subprob_kernel X Y (kij j))  (x A. x  space X  ki i x A = (j. kij j x A))" for i
    using s_finite_kernel.s_finite_kernels[OF assms(1)[of i]] by metis
  then obtain kij where kij:"i j. subprob_kernel X Y (kij i j)" "i x A. x  space X  ki i x A = (j. kij i j x A)"
    by metis
  define ki' where "ki'  (λn. case_prod kij (prod_decode n))"
  have emeasure_sumk':"emeasure (k x) A = (i. emeasure (ki' i x) A)" if x:"x  space X" and A: "A  sets Y" for x A
    by(auto simp: assms(3)[OF that] kij(2)[OF x] ki'_def intro!: suminf_ennreal_2dimen[symmetric])
  have "subprob_kernel X Y (ki' i)" for i
    using kij(1) by(auto simp: ki'_def split_beta')
  thus ?thesis
    by(auto simp: s_finite_kernel_def' measure_kernel_def assms(2) s_finite_kernel_axioms_def emeasure_sumk' intro!: exI[where x=ki'])
qed

lemma s_finite_kernel_finite_sumI:
  assumes [measurable_cong]: "x. x  space X  sets (κ x) = sets Y"
      and "i. i  I  subprob_kernel X Y (ki i)" "x A. x  space X  A  sets Y  emeasure (κ x) A = (iI. ki i x A)" "finite I" "I  {}"
    shows "s_finite_kernel X Y κ"
proof -
  consider "space X = {}" | "space X  {}" by auto
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by(rule s_finite_kernel_empty_trivial)
  next
    case 2
    then have Y:"space Y  {}"
      using assms measure_kernel.Y_not_empty by (fastforce simp: subprob_kernel_def)
    define ki' where "ki'  (λi x. if i < card I then ki (from_nat_into I i) x else null_measure Y)"
    have [simp]:"subprob_kernel X Y (ki' i)" for i
      by(cases "i < card I") (simp add: ki'_def from_nat_into assms, auto simp: ki'_def subprob_kernel_def measure_kernel_def subprob_kernel_axioms_def Y intro!: subprob_spaceI)
    have [simp]: "(i. emeasure (ki' i x) A) = (iI. ki i x A)" for x A
      using suminf_finite[of "{..<card I}" "λi. (if i < card I then ki (from_nat_into I i) x else null_measure Y) A"]
      by(auto simp: sum.reindex_bij_betw[OF bij_betw_from_nat_into_finite[OF assms(4)],symmetric] ki'_def)
    have [measurable]:"B  sets Y  (λx. emeasure (κ x) B)  borel_measurable X" for B
      using assms(2) by(auto simp: assms(3) subprob_kernel_def' cong: measurable_cong)
    show ?thesis
      by (auto simp: s_finite_kernel_def' intro!: exI[where x=ki'] assms)
  qed
qed

text ‹ Each kernel does not need to be bounded by a uniform upper-bound in the definition of @{term s_finite_kernel}
lemma s_finite_kernel_finite_bounded_sum:
  assumes [measurable_cong]: "x. x  space X  sets (κ x) = sets Y"
      and "i. measure_kernel X Y (ki i)" "x A. x  space X  A  sets Y  κ x A = (i. ki i x A)" "i x. x  space X  ki i x (space Y) < "
    shows "s_finite_kernel X Y κ"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by(simp add: s_finite_kernel_empty_trivial)
next
  case X:False
  then have Y: "space Y  {}"
    using assms(2)[of 0] by(simp add: measure_kernel_def)
  show ?thesis
  proof(rule s_finite_kernel_s_finite_kernel[where ki=ki,OF _ assms(1) assms(3)])
    fix i
    interpret m: measure_kernel X Y "ki i" by fact
    define kij where "kij  (λ(j :: nat) x. if j < nat enn2real (ki i x (space Y)) then scale_measure (1 / ennreal enn2real (ki i x (space Y))) (ki i x) else sigma (space Y) (sets Y))"
    have sets_kij: "sets (kij j x) = sets Y" if "x  space X" for j x
      by(auto simp: m.kernel_sets[OF that] kij_def)
    have emeasure_kij: "ki i x A = (j. kij j x A)" if "x  space X" "A  sets Y" for x A
    proof -
      have "(j. kij j x A) = (j< nat enn2real (ki i x (space Y)). scale_measure (1 / ennreal enn2real (ki i x (space Y))) (ki i x) A)"
        by(simp add: suminf_offset[where i="nat enn2real (ki i x (space Y))" and f="λj. kij j x A"], simp add: kij_def emeasure_sigma)
      also have "... = ki i x A"
      proof(cases "nat enn2real (ki i x (space Y))")
        case 0
        then show ?thesis
          by simp (metis assms(4) emeasure_eq_0 enn2real_le ennreal_0 infinity_ennreal_def le_zero_eq linorder_not_le m.kernel_space nle_le sets.sets_into_space sets.top that)
      next
        case (Suc n')
        then have "ennreal (real_of_int enn2real (emeasure (ki i x) (space Y))) > 0"
          using ennreal_less_zero_iff by fastforce
        with assms(4)[OF that(1),of i] have [simp]: "of_nat (nat enn2real (emeasure (ki i x) (space Y))) / ennreal (real_of_int enn2real (emeasure (ki i x) (space Y))) = 1"
          by (simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
        show ?thesis
          by(simp add: mult.assoc[symmetric] ennreal_times_divide)
      qed
      finally show ?thesis by simp
    qed
    have sk: "subprob_kernel X Y (kij j)" for j
    proof -
      {
        fix B
        assume [measurable]:"B  sets Y"
        have "emeasure (kij j x) B = (if j < nat enn2real (ki i x (space Y)) then (ki i x) B / ennreal (real_of_int enn2real (ki i x (space Y))) else 0)" if "x  space X" for x
          by(auto simp: kij_def emeasure_sigma divide_ennreal_def mult.commute)
        hence " (λx. emeasure (kij j x) B)  borel_measurable X"
          by(auto simp: kij_def cong: measurable_cong)
      }
      moreover {
        fix x
        assume x:"x  space X"
        have "subprob_space (kij j x)"
        proof -
          have "emeasure (kij j x) (space Y)  1"
          proof -
            {
              assume 1:"j < nat enn2real (emeasure (ki i x) (space Y))"
              then have "emeasure (ki i x) (space Y) > 0"
                by (metis ceiling_zero enn2real_0 nat_zero_as_int not_gr_zero not_less_zero)
              with assms(4)[OF x] have [simp]:"emeasure (ki i x) (space Y) / emeasure (ki i x) (space Y) = 1"
                by simp
              have [simp]:"emeasure (ki i x) (space Y) / ennreal (real_of_int enn2real (ki i x (space Y)))  1"
              proof(rule order.trans[where b="emeasure (ki i x) (space Y) / ki i x (space Y)",OF divide_le_posI_ennreal])
                show "0 < ennreal (real_of_int enn2real (ki i x (space Y)))"
                  using 1 assms(4)[OF x] enn2real_positive_iff top.not_eq_extremum by fastforce
              next
                have 1:"ennreal (real_of_int enn2real (ki i x (space Y)))  ki i x (space Y)"
                  using assms(4)[OF x] enn2real_le by (simp add: linorder_neq_iff)
                have "ennreal (real_of_int enn2real (ki i x (space Y))) / ki i x (space Y)  1"
                  by(rule order.trans[OF _ divide_right_mono_ennreal[OF 1,of "ki i x (space Y)"]]) simp
                thus "emeasure (ki i x) (space Y)  ennreal (real_of_int enn2real (ki i x (space Y))) * (emeasure (ki i x) (space Y) / ki i x (space Y))"
                  by (simp add: "1")
              qed simp
              have "1 / ennreal (real_of_int enn2real (emeasure (ki i x) (space Y))) * emeasure (ki i x) (space Y)  1"
                by (simp add: ennreal_divide_times)
            }
            thus ?thesis
              by(auto simp: kij_def emeasure_sigma)
          qed
          thus ?thesis
            by(auto intro!: subprob_spaceI simp: sets_eq_imp_space_eq[OF sets_kij[OF x,of j]] Y)
        qed
      }
      ultimately show ?thesis
        by(auto simp: subprob_kernel_def measure_kernel_def sets_kij m.Y_not_empty subprob_kernel_axioms_def)
    qed
    show "s_finite_kernel X Y (ki i)"
      by(auto intro!: s_finite_kernel_subI simp: emeasure_kij sk m.kernel_sets)
  qed simp_all
qed

lemma(in measure_kernel) s_finite_kernel_finite_bounded:
  assumes "x. x  space X  κ x (space Y) < "
  shows "s_finite_kernel X Y κ"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by(simp add: s_finite_kernel_empty_trivial)
next
  case False
  then have Y:"space Y  {}" by(simp add: Y_not_empty)
  have "measure_kernel X Y (case i of 0  κ | Suc x  λx. null_measure Y)" for i
    by(cases i,auto simp: measure_kernel_axioms) (auto simp: measure_kernel_def Y)
  moreover have "κ x A = (i. emeasure ((case i of 0  κ | Suc x  λx. null_measure Y) x) A)" for x A
    by(simp add: suminf_offset[where i="Suc 0"])
  moreover have "x  space X  emeasure ((case i of 0  κ | Suc x  λx. null_measure Y) x) (space Y) < " for x i
    by(cases i) (use assms in auto)
  ultimately show ?thesis
    by(auto intro!: s_finite_kernel_finite_bounded_sum[where ki="λi. case i of 0  κ | Suc _  (λx. null_measure Y)" and X=X and Y=Y] simp: kernel_sets)
qed

lemma(in s_finite_kernel) density_s_finite_kernel:
  assumes f[measurable]: "case_prod f  X M Y M borel"
  shows "s_finite_kernel X Y (λx. density (κ x) (f x))"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by(simp add: s_finite_kernel_empty_trivial)
next
  case False
  note Y = Y_not_empty[OF this]
  obtain ki' where ki': "i. subprob_kernel X Y (ki' i)" "x A. x  space X  κ x A = (i. ki' i x A)"
    by(metis s_finite_kernels)
  hence sets_ki'[measurable_cong]:"x i. x  space X  sets (ki' i x) = sets Y"
    by(auto simp: subprob_kernel_def measure_kernel_def)
  define ki where "ki  (λi x. density (ki' i x) (f x))"
  have sets_ki: "x  space X  sets (ki i x) = sets Y" for i x
    using ki'(1) by(auto simp: subprob_kernel_def measure_kernel_def ki_def)
  have emeasure_k:"density (κ x) (f x) A = (i. ki i x A)" if x:"x  space X" and A[measurable]:"A  sets Y" for x A
    using kernel_sets[OF x] x ki'(1) sets_ki'[OF x] by(auto simp: emeasure_density nn_integral_measure_suminf[OF _ ki'(2),of x] ki_def)
  show ?thesis
  proof(rule s_finite_kernel_s_finite_kernel[where ki="ki",OF _ _ emeasure_k])
    fix i
    note nn_integral_measurable_subprob_algebra2[OF _ ki'(1)[of i,simplified subprob_kernel_def'],measurable]
    define kij where "kij  (λj x. if j = 0 then density (ki' i x) (λy.  * indicator {yspace Y. f x y = } y)
                                    else if j = (Suc 0) then density (ki' i x) (λy. f x y * indicator {yspace Y. f x y < } y)
                                    else null_measure Y)"
    have emeasure_kij: "ki i x A = (j. kij j x A)" (is "?lhs = ?rhs") if x:"x  space X" and [measurable]: "A  sets Y" for x A
    proof -
      have "?lhs = (+yA. f x y ki' i x)"
        using sets_ki[OF x,of i] x by(auto simp: ki_def emeasure_density)
      also have "... = (+y. ( * indicator {y  space Y. f x y = } y * indicator A y + f x y * indicator {y  space Y. f x y < } y * indicator A y) ki' i x)"
        by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF sets_ki'[OF x]] indicator_def) (simp add: top.not_eq_extremum)
      also have "... = density (ki' i x) (λy.  * indicator {yspace Y. f x y = } y) A + density (ki' i x) (λy. f x y * indicator {yspace Y. f x y < } y) A"
        using sets_ki[OF x,of i] x by(auto simp: ki_def emeasure_density nn_integral_add)
      also have "... = ?rhs"
        using suminf_finite[of "{..<Suc (Suc 0)}" "λj. kij j x A"] by(simp add: kij_def)
      finally show ?thesis .
    qed
    have sets_kij[measurable_cong]:"x  space X  sets (kij j x) = sets Y" for j x
      by(auto simp: kij_def sets_ki')
    show "s_finite_kernel X Y (ki i)"
    proof(rule s_finite_kernel_s_finite_kernel[where ki=kij,OF _ _ emeasure_kij])
      fix j
      consider "j = 0" | "j = Suc 0" | "j  0" "j  Suc 0" by auto
      then show "s_finite_kernel X Y (kij j)"
      proof cases
        case 1
        have emeasure_ki: "emeasure (kij j x) A = (j. emeasure (density (ki' i x) (indicator {y  space Y. f x y = })) A)" if x:"x  space X" and [measurable]: "A  sets Y" for x A
          using sets_ki'[OF x] x by(auto simp: 1 kij_def emeasure_density nn_integral_suminf[symmetric] indicator_def intro!: nn_integral_cong) (simp add: nn_integral_count_space_nat[symmetric])
        have [simp]:"subprob_kernel X Y (λx. density (ki' i x) (indicator {y  space Y. f x y = }))"
        proof -
          have [simp]:"x  space X  set_nn_integral (ki' i x) (space Y) (indicator {y  space Y. f x y = })  1" for x
            by(rule order.trans[OF nn_integral_mono[where v="λx. 1"]],insert ki'(1)[of i]) (auto simp: indicator_def subprob_kernel_def subprob_kernel_axioms_def intro!: subprob_space.emeasure_space_le_1)
          show ?thesis
            by(auto simp: subprob_kernel_def measure_kernel_def emeasure_density subprob_kernel_axioms_def sets_ki' sets_eq_imp_space_eq[OF sets_ki'] Y cong: measurable_cong intro!: subprob_spaceI)
        qed
        show ?thesis
          by (auto simp: s_finite_kernel_def' sets_kij intro!: exI[where x="λk x. density (ki' i x) (indicator {y  space Y. f x y = })"] simp: emeasure_ki )
      next
        case j:2
        have emeasure_ki: "emeasure (kij j x) A = (k. density (ki' i x) (λy. f x y * indicator {y  space Y. of_nat k  f x y  f x y < 1 + of_nat k} y) A)" if x:"x  space X" and [measurable]:"A  sets Y" for x A
        proof -
          have [simp]: "f x y * indicator {y  space Y. f x y < } y * indicator A y = f x y * (k. indicator {y  space Y. of_nat k  f x y  f x y < 1 + of_nat k} y) * indicator A y" if y:"y  space Y" for y
          proof(cases "f x y < ")
            case f:True
            define l where "l  floor (enn2real (f x y))"
            have "nat l  enn2real (f x y)" "enn2real (f x y) < 1 + nat l"
              by (simp_all add: l_def) linarith
            with y have l:"of_nat (nat l)  f x y" "f x y < 1 + of_nat (nat l)"
              using Orderings.order_eq_iff enn2real_positive_iff ennreal_enn2real_if ennreal_of_nat_eq_real_of_nat linorder_not_le of_nat_0_le_iff f by fastforce+
            then have "(j. indicator {y  space Y. of_nat j  f x y  f x y < 1 + of_nat j} y :: ennreal) = (j. if j = nat l then 1 else 0)"
              by(auto intro!: suminf_cong simp: indicator_def y) (metis Suc_leI linorder_neqE_nat linorder_not_less of_nat_Suc of_nat_le_iff order_trans)
            also have "... = 1"
              using suminf_finite[where N="{nat l}" and f="λj. if j = nat l then 1 else (0 :: ennreal)"] by simp
            finally show ?thesis
              by(auto, insert f) (auto simp: indicator_def)
          qed(use top.not_eq_extremum in fastforce)
          show ?thesis
            using sets_ki[OF x] sets_ki'[OF x] x by(auto simp: kij_def j emeasure_density nn_integral_suminf[symmetric] sets_eq_imp_space_eq[OF sets_ki'[OF x]] intro!: nn_integral_cong)
        qed
        show ?thesis
        proof(rule s_finite_kernel_finite_bounded_sum[OF sets_kij _ emeasure_ki])
          fix k
          show "measure_kernel X Y (λx. density (ki' i x) (λy. f x y * indicator {y  space Y. of_nat k  f x y  f x y < 1 + of_nat k} y))"
            using sets_ki'[of _ i] by(auto simp: measure_kernel_def emeasure_density Y cong: measurable_cong)
        next
          fix k x
          assume x:"x space X"
          have "emeasure (density (ki' i x) (λy. f x y * indicator {y  space Y. of_nat k  f x y  f x y < 1 + of_nat k} y)) (space Y)  1 + of_nat k"
            by(auto simp: emeasure_density x,rule order.trans[OF nn_integral_mono[where v="λx. 1 + of_nat k"]]) (insert subprob_kernel.subprob_space[OF ki'(1)[of i] x], auto simp: indicator_def subprob_kernel_def subprob_kernel_axioms_def  sets_eq_imp_space_eq[OF sets_ki'[OF x]] intro!: mult_mono[where d="1 :: ennreal",OF order.refl,simplified])
          also have "... < "
            by (simp add: of_nat_less_top)
          finally show "emeasure (density (ki' i x) (λy. f x y * indicator {y  space Y. of_nat k  f x y  f x y < 1 + of_nat k} y)) (space Y) < " .
        qed auto
      next
        case 3
        then show ?thesis
          by(auto simp: kij_def s_finite_kernel_cong_sets[of X X Y,OF _ sets_null_measure[symmetric]] Y intro!: s_finite_measure.s_finite_kernel_const finite_measure.s_finite_measure_finite_measure finite_measureI)
      qed
    qed(auto simp: sets_ki)
  qed(auto simp: kernel_sets)
qed

lemma(in s_finite_kernel) nn_integral_measurable_f:
  assumes [measurable]:"(λ(x,y). f x y)  borel_measurable (X M Y)"
  shows "(λx. +y. f x y (κ x))  borel_measurable X"
proof -
  obtain κi where κi:"i. subprob_kernel X Y (κi i)" "x A. x  space X  κ x A = (i. κi i x A)"
    by(metis s_finite_kernels)
  show ?thesis
  proof(rule measurable_cong[THEN iffD2])
    fix x
    assume "x  space X"
    with κi show "(+ y. f x y κ x) = (i. + y. f x y κi i x)"
      by(auto intro!: nn_integral_measure_suminf[symmetric] simp: subprob_kernel_def kernel_sets measure_kernel_def)
  next
    show "(λx. i. + y. f x y κi i x)  borel_measurable X"
      using κi(1) nn_integral_measurable_subprob_algebra2[OF assms] by(simp add: subprob_kernel_def' )
  qed
qed

lemma(in s_finite_kernel) nn_integral_measurable_f':
  assumes "f  borel_measurable (X M Y)"
  shows "(λx. +y. f (x, y) (κ x))  borel_measurable X"
  using nn_integral_measurable_f[where f="curry f",simplified,OF assms] by simp

lemma(in s_finite_kernel) bind_kernel_s_finite_kernel':
  assumes "s_finite_kernel (X M Y) Z (case_prod g)"
  shows "s_finite_kernel X Z (λx. κ x k g x)"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by (simp add: s_finite_kernel_empty_trivial)
next
  case X:False
  then have Y:"space Y  {}"
    by(simp add: Y_not_empty)
  from s_finite_kernels obtain ki where ki:
  "i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    by metis
  interpret g:s_finite_kernel "X M Y" Z "case_prod g" by fact
  from g.s_finite_kernels[simplified space_pair_measure] obtain gi where gi:
  "i. subprob_kernel (X M Y) Z (gi i)" "x y A. x  space X  y  space Y  g x y A = (i. gi i (x,y) A)"
    by auto metis
  define kgi where "kgi = (λi x. case prod_decode i of (i,j)  (ki j x  curry (gi i) x))"
  have emeasure:"emeasure (κ x k g x) A = (i. emeasure (kgi i x) A)" (is "?lhs = ?rhs") if x:"x  space X" and A:"A  sets Z" for x A
  proof -
    interpret gx: s_finite_kernel Y Z "g x"
      using g.comp_measurable[OF measurable_Pair1'[OF x]] by auto
    have "?lhs = (+ y. g x y A κ x)"
      using gx.emeasure_bind_kernel[OF kernel_sets[OF x] A]
      by(auto simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] Y)
    also have "... = (+ y. (i. gi i (x, y) A) κ x)"
      by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] gi(2)[OF x])
    also have "... = (i. + y. gi i (x, y) A κ x)"
      using gi(1) x A by(auto intro!: nn_integral_suminf simp: subprob_kernel_def')
    also have "... = (i. (j. + y. gi i (x, y) A ki j x))"
      by(rule suminf_cong, rule nn_integral_measure_suminf[symmetric], insert kernel_sets[OF x] ki gi(1) x A)
        (auto simp: subprob_kernel_def measure_kernel_def measurable_cong_sets[OF sets_pair_measure_cong[OF refl kernel_sets[OF x]]] intro!: measurable_Pair2[OF _ x])
    also have "... = (i. (j. emeasure (ki j x  (curry (gi i) x)) A))"
      using sets_eq_imp_space_eq[of "ki _ x" Y] ki(1) x gi(1) measurable_cong_sets[of _ _ "subprob_algebra Z" "subprob_algebra Z", OF sets_pair_measure_cong[of X X Y "ki _ x"]]
      by(auto intro!: suminf_cong emeasure_bind[OF _ _ A,symmetric] measurable_Pair2[OF _ x] simp: curry_def subprob_kernel_def[of X] subprob_kernel_def'[of "X M Y"]  measure_kernel_def Y)
    also have "... = ?rhs"
      unfolding kgi_def by(rule suminf_ennreal_2dimen[symmetric]) (simp add: curry_def)
    finally show ?thesis .
  qed
  have sets: "sets (κ x k g x) = sets Z" if x:"x  space X" for x
  proof -
    interpret gx: s_finite_kernel Y Z "g x"
      using g.comp_measurable[OF measurable_Pair1'[OF x]] by auto
    show ?thesis
      by(simp add: gx.sets_bind_kernel[OF _ kernel_sets[OF x]] Y)
  qed
  have sk:"subprob_kernel X Z (kgi i)" for i
    using ki(1)[of "snd (prod_decode i)"] gi(1)[of "fst (prod_decode i)"]
    by(auto simp: subprob_kernel_def' kgi_def split_beta' curry_def)
  show ?thesis
    using sk by(auto simp: s_finite_kernel_def' emeasure sets subprob_kernel_def' intro!: exI[where x=kgi] measurable_cong[where g="λx. i. emeasure (kgi i x) _" and f="λx. emeasure (κ x k g x) _",THEN iffD2])
qed

corollary(in s_finite_kernel) bind_kernel_s_finite_kernel:
  assumes "s_finite_kernel Y Z k'"
  shows "s_finite_kernel X Z (λx. κ x k k')"
  by(auto intro!: bind_kernel_s_finite_kernel' s_finite_kernel.comp_measurable[OF assms measurable_snd] simp: split_beta')

lemma(in s_finite_kernel) nn_integral_bind_kernel:
  assumes "f  borel_measurable Y" "sets μ = sets X"
  shows "(+ y. f y (μ k κ)) = (+x. (+ y. f y (κ x)) μ)"
proof(cases "space X = {}")
  case True
  then show ?thesis
    by(simp add: sets_eq_imp_space_eq[OF assms(2)] bind_kernel_def nn_integral_empty)
next
  case X:False
  then have μ:"space μ  {}" by(simp add: sets_eq_imp_space_eq[OF assms(2)])
  note 1[measurable_cong] = assms(2) sets_bind_kernel[OF X assms(2)]
  from assms(1) show ?thesis
  proof induction
    case ih:(cong f g)
    have "(+ y. f y (μ k κ)) = (+ y. g y (μ k κ))" "(+ x. integralN (κ x) f μ) = (+ x. integralN (κ x) g μ)"
      by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF 1(2)] sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] ih(3))
    then show ?case
      by(simp add: ih)
  next
    case (set A)
    then show ?case
      by(auto simp: emeasure_bind_kernel[OF 1(1) _ X] sets_eq_imp_space_eq[OF 1(1)] intro!: nn_integral_cong)
  next
    case ih:(mult u c)
    then have "(+ x. + y. c * u y κ x μ) = (+ x. c * + y. u y κ x μ)"
      by(auto intro!: nn_integral_cong nn_integral_cmult simp: sets_eq_imp_space_eq[OF 1(1)])
    with ih nn_integral_measurable_f[of "λ_ y. u y"] show ?case
      by(auto simp: nn_integral_cmult intro!: nn_integral_cong)
  next
    case ih:(add u v)
    then have "(+ x. + y. v y + u y κ x μ) = (+ x. (+ y. v y κ x) + (+ y. u y κ x) μ)"
      by(auto intro!: nn_integral_cong simp: nn_integral_add sets_eq_imp_space_eq[OF 1(1)])
    with ih nn_integral_measurable_f[of "λ_ y. u y"] nn_integral_measurable_f[of "λ_ y. v y"] show ?case
      by(simp add: nn_integral_add)
  next
    case ih[measurable]:(seq U)
    show ?case (is "?lhs = ?rhs")
    proof -
      have "?lhs = ((i. integralN (μ k κ) (U i)))"
        by(rule nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[of U UNIV,symmetric]]) (use ih in auto)
      also have "... = (i. + x. (+ y. U i y κ x) μ)"
        by(simp add: ih)
      also have "... = (+ x. (i. (+ y. U i y κ x)) μ)"
      proof(rule nn_integral_monotone_convergence_SUP[symmetric])
        show "incseq (λi x. + y. U i y κ x)"
          by standard+ (auto intro!: le_funI nn_integral_mono simp:le_funD[OF incseqD[OF ih(3)]])
      qed(use nn_integral_measurable_f[of "λ_ y. U _ y"] in simp)
      also have "... = ?rhs"
        by(rule nn_integral_cong, rule nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[of U UNIV,symmetric],OF ih(3),symmetric]) (auto simp: sets_eq_imp_space_eq[OF 1(1)])
      finally show ?thesis .
    qed
  qed
qed

lemma(in s_finite_kernel) bind_kernel_assoc:
  assumes "s_finite_kernel Y Z k'" "sets μ = sets X"
  shows "μ k (λx. κ x k k') = μ k κ k k'"
proof(cases "space X = {}")
  case X:False
  then have μ: "space μ  {}" and Y:"space Y  {}"
    by(simp_all add: Y_not_empty sets_eq_imp_space_eq[OF assms(2)])
  interpret k':s_finite_kernel Y Z k' by fact
  interpret k'': s_finite_kernel X Z "λx. κ x k k'"
    by(rule bind_kernel_s_finite_kernel[OF assms(1)])
  show ?thesis
  proof(rule measure_eqI)
    fix A
    assume "A  sets (μ k (λx. κ x k k'))"
    then have A[measurable]: "A  sets Z"
      by(simp add: k''.sets_bind_kernel[OF X assms(2)])
    show "emeasure (μ k (λx. κ x k k')) A = emeasure (μ k κ k k') A" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (+ x. emeasure (κ x k k') A μ)"
        by(rule k''.emeasure_bind_kernel[OF assms(2) A X])
      also have "... = (+ x. + y. k' y A κ x μ)"
        using k'.emeasure_bind_kernel[OF kernel_sets A]
        by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] Y)
      also have "... = (+ y. k' y A (μ k κ))"
        by(simp add: nn_integral_bind_kernel[OF k'.emeasure_measurable[OF A] assms(2)])
      also have "... = ?rhs"
        by(simp add: k'.emeasure_bind_kernel[OF sets_bind_kernel[OF X assms(2)] A] sets_eq_imp_space_eq[OF sets_bind_kernel[OF X assms(2)]] Y)
      finally show ?thesis .
    qed
  qed(auto simp: k'.sets_bind_kernel[OF Y sets_bind_kernel[OF X assms(2)]] k''.sets_bind_kernel[OF X assms(2)]) 
qed(simp add: bind_kernel_def sets_eq_imp_space_eq[OF assms(2)])

lemma s_finite_kernel_pair_measure:
  assumes "s_finite_kernel X Y k" and "s_finite_kernel X Z k'"
  shows "s_finite_kernel X (Y M Z) (λx. k x M k' x)"
proof -
  interpret k: s_finite_kernel X Y k by fact
  interpret k': s_finite_kernel X Z k' by fact
  from k.s_finite_kernels k'.s_finite_kernels obtain ki ki'
    where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  k x A = (i. ki i x A)"
      and ki':"i. subprob_kernel X Z (ki' i)" "x A. x  space X  k' x A = (i. ki' i x A)"
    by metis
  then have 1[measurable_cong]: "x i. x  space X  sets (ki i x) = sets Y" "x i. x  space X  sets (ki' i x) = sets Z"
    by(auto simp: subprob_kernel_def measure_kernel_def)
  define kki where "kki  (λi x. (λ(j,i). ki i x M ki' j x) (prod_decode i))"
  have kki1: "i. subprob_kernel X (Y M Z) (kki i)"
    using ki(1) ki'(1) by(auto simp: subprob_kernel_def' kki_def split_beta intro!: measurable_pair_measure)
  have kki2: "(k x M k' x) A = (i. (kki i x) A)" (is "?lhs = ?rhs") if x:"x  space X" and A[measurable]: "A  sets (Y M Z)" for x A
  proof -
    have "?lhs = (+ y. + z. indicator A (y, z) k' x k x)"
      using x by(simp add: s_finite_measure.emeasure_pair_measure'[OF k'.image_s_finite_measure])
    also have "... = (+ y. (j. + z. indicator A (y, z) ki' j x) k x)"
      using ki' x by(auto intro!: nn_integral_cong nn_integral_measure_suminf[symmetric] simp: sets_eq_imp_space_eq[OF k.kernel_sets[OF x]] subprob_kernel_def measure_kernel_def k'.kernel_sets)
    also have "... = (j. + y. + z. indicator A (y, z) ki' j x k x)"
      using x by(auto intro!: nn_integral_suminf s_finite_measure.borel_measurable_nn_integral_fst' s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]])
    also have "... = (j. (i. (+ y. + z. indicator A (y, z) ki' j x ki i x)))"
      using x ki by(auto intro!: suminf_cong nn_integral_measure_suminf[symmetric] s_finite_measure.borel_measurable_nn_integral_fst' simp: k.kernel_sets[OF x] subprob_kernel_def measure_kernel_def s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]])
    also have "... =  (j. (i. (ki i x M ki' j x) A))"
      using x by(auto simp: s_finite_measure.emeasure_pair_measure'[OF s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]]])
    also have "... = ?rhs"
      unfolding kki_def by(rule suminf_ennreal_2dimen[symmetric]) auto
    finally show ?thesis .
  qed
  show ?thesis
  proof
    fix B
    assume [measurable]:"B  sets (Y M Z)"
    show "(λx. emeasure (k x M k' x) B)  borel_measurable X"
      by(rule measurable_cong[where g="λx. i. (kki i x) B",THEN iffD2], insert kki1) (auto simp: subprob_kernel_def' kki2)
  qed(auto intro!: exI[where x=kki] simp: subprob_kernel.finite_kernel kki1 kki2 k.kernel_sets k'.kernel_sets space_pair_measure k.Y_not_empty k'.Y_not_empty)
qed

lemma pair_measure_eq_bind_s_finite:
  assumes "s_finite_measure μ" "s_finite_measure ν"
  shows "μ M ν = μ k (λx. ν k (λy. return (μ M ν) (x,y)))"
proof -
  consider "space μ = {}" | "space ν = {}" | "space μ  {}" "space ν  {}"
    by auto
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by(auto simp: bind_kernel_def space_pair_measure intro!: space_empty)
  next
    case 2
    then have "μ k (λx. ν k (λy. return (μ M ν) (x, y))) = count_space {}"
      by(auto simp: bind_kernel_def space_empty)
    with 2 show ?thesis
      by(auto simp: space_pair_measure intro!: space_empty)
  next
    case 3
    show ?thesis
    proof(intro measure_eqI sets_bind_kernel[OF _ 3(1),symmetric] sets_bind_kernel[OF _ 3(2)])
      fix A
      assume A[measurable]: "A  sets (μ M ν)"
      show "emeasure (μ M ν) A = emeasure (μ k (λx. ν k (λy. return (μ M ν) (x, y)))) A" (is "?lhs = ?rhs")
      proof -
        have "?lhs = (+ x. + y. return (μ M ν) (x, y) A ν μ)"
          by(simp add: s_finite_measure.emeasure_pair_measure'[OF assms(2)])
        also have "... = (+ x. (ν k (λy. return (μ M ν) (x,y))) A μ)"
          by(auto intro!: nn_integral_cong measure_kernel.emeasure_bind_kernel[OF _ _ A 3(2),symmetric] prob_kernel.axioms(1) simp: prob_kernel_def' simp del: emeasure_return)
        also have "... = ?rhs"
          by(auto intro!: measure_kernel.emeasure_bind_kernel[OF _ _ A 3(1),symmetric] s_finite_kernel.axioms(1) s_finite_kernel.bind_kernel_s_finite_kernel'[where Y=ν] s_finite_measure.s_finite_kernel_const[OF assms(2) 3(2)] prob_kernel.s_finite_kernel_prob_kernel[of "μ M ν"] simp: prob_kernel_def')
        finally show ?thesis .
      qed
    qed simp
  qed
qed

lemma bind_kernel_rotate_return:
  assumes "s_finite_measure μ" "s_finite_measure ν"
  shows "μ k (λx. ν k (λy. return (μ M ν) (x,y))) = ν k (λy. μ k (λx. return (μ M ν) (x,y)))"
proof -
  consider "space μ = {}" | "space ν = {}" | "space μ  {}" "space ν  {}"
    by auto
  then show ?thesis
  proof cases
    case 1
    then have "ν k (λy. μ k (λx. return (μ M ν) (x,y))) = count_space {}"
      by(auto simp: bind_kernel_def space_empty)
    then show ?thesis
      by(auto simp: bind_kernel_def space_pair_measure 1 intro!: space_empty)
  next
    case 2
    then have "μ k (λx. ν k (λy. return (μ M ν) (x, y))) = count_space {}"
      by(auto simp: bind_kernel_def space_empty)
    with 2 show ?thesis
      by(auto simp: space_pair_measure bind_kernel_def intro!: space_empty)
  next
    case 3
    show ?thesis
      unfolding pair_measure_eq_bind_s_finite[OF assms,symmetric]
    proof(intro measure_eqI)
      fix A
      assume A[measurable]:"A  sets (μ M ν)"
      show "emeasure (μ M ν) A = emeasure (ν k (λy. μ k (λx. return (μ M ν) (x, y)))) A" (is "?lhs = ?rhs")
      proof -
        have "?lhs = (+ x. + y. indicator A (x, y) ν μ)"
          by(rule s_finite_measure.emeasure_pair_measure'[OF assms(2) A])
        also have "... = (+ y. + x. return (μ M ν) (x, y) A μ ν)"
          by(simp add: nn_integral_snd'[OF assms] s_finite_measure.nn_integral_fst'[OF assms(2)])
        also have "... = (+ y. (μ k (λx. return (μ M ν) (x, y))) A ν)"
          by(auto intro!: nn_integral_cong measure_kernel.emeasure_bind_kernel[OF _ _  A 3(1),symmetric] prob_kernel.axioms(1) simp add: prob_kernel_def' simp del: emeasure_return)
        also have "... = ?rhs"
          by(auto intro!: measure_kernel.emeasure_bind_kernel[OF _ _  A 3(2),symmetric] s_finite_kernel.axioms(1) s_finite_kernel.bind_kernel_s_finite_kernel'[where Y=μ] s_finite_measure.s_finite_kernel_const[OF assms(1) 3(1)] prob_kernel.s_finite_kernel_prob_kernel[of "ν M μ"] simp: prob_kernel_def')
        finally show ?thesis .
      qed
    qed(auto intro!: sets_bind_kernel[OF _ 3(2),symmetric] sets_bind_kernel[OF _ 3(1)])
  qed
qed

lemma bind_kernel_rotate':
  assumes "s_finite_measure μ" "s_finite_measure ν" "s_finite_kernel (μ M ν) Z (case_prod f)"
  shows "μ k (λx. ν k (λy. f x y)) = ν k (λy. μ k (λx. f x y))" (is "?lhs = ?rhs")
proof -
  interpret sk: s_finite_kernel "μ M ν" Z "case_prod f" by fact
  consider "space μ = {}" | "space ν = {}" | "space μ  {}" "space ν  {}"
    by auto
  then show ?thesis
  proof cases
    case 1
    then have "?rhs = count_space {}"
      by(auto simp: bind_kernel_def space_empty)
    then show ?thesis
      by(auto simp: bind_kernel_def space_pair_measure 1 intro!: space_empty)
  next
    case 2
    then show ?thesis
      by(auto simp: space_pair_measure bind_kernel_def intro!: space_empty)
  next
    case 3
    show ?thesis
    proof -
      have "?lhs = μ k (λx. ν k (λy. return (μ M ν) (x, y)) k case_prod f)"
        by(auto intro!: bind_kernel_cong_All simp: s_finite_kernel.bind_kernel_assoc[OF prob_kernel.s_finite_kernel_prob_kernel assms(3) refl,of ν "λy. return (μ M ν) (_, y)",simplified prob_kernel_def',symmetric] sk.bind_kernel_return space_pair_measure)
      also have "... = μ k (λx. ν k (λy. return (μ M ν) (x,y))) k (case_prod f)"
        by(auto simp: s_finite_kernel.bind_kernel_assoc[OF s_finite_kernel.bind_kernel_s_finite_kernel'[OF s_finite_measure.s_finite_kernel_const[OF assms(2) 3(2),of μ] prob_kernel.s_finite_kernel_prob_kernel,of "μ M ν" "λx y. return (μ M ν) (x,y)",simplified] assms(3) refl, simplified prob_kernel_def',symmetric])
      also have "... = ν k (λy. μ k (λx. return (μ M ν) (x,y))) k (case_prod f)"
        by(simp add: bind_kernel_rotate_return assms)
      also have "... = ν k (λy. μ k (λx. return (μ M ν) (x, y)) k case_prod f)"
        by(auto intro!: s_finite_kernel.bind_kernel_assoc[OF _ assms(3),symmetric] s_finite_kernel.bind_kernel_s_finite_kernel'[OF s_finite_measure.s_finite_kernel_const[OF assms(1) 3(1)]] prob_kernel.s_finite_kernel_prob_kernel[of "ν M μ"] simp: prob_kernel_def')
      also have "... = ?rhs"
        by(auto intro!: bind_kernel_cong_All simp: s_finite_kernel.bind_kernel_assoc[OF prob_kernel.s_finite_kernel_prob_kernel assms(3) refl,of μ "λx. return (μ M ν) (x, _)",simplified prob_kernel_def',symmetric] sk.bind_kernel_return space_pair_measure)
      finally show ?thesis .
    qed
  qed
qed

lemma bind_kernel_rotate:
  assumes "sets μ = sets X" and "sets ν = sets Y"
      and "s_finite_measure μ" "s_finite_measure ν" "s_finite_kernel (X M Y) Z (λ(x,y). f x y)"
    shows "μ k (λx. ν k (λy. f x y)) = ν k (λy. μ k (λx. f x y))"
  by(auto intro!: bind_kernel_rotate' assms simp: s_finite_kernel_cong_sets[OF sets_pair_measure_cong[OF assms(1,2)]])

lemma(in s_finite_kernel) emeasure_measurable':
  assumes A[measurable]: "(SIGMA x:space X. A x)  sets (X M Y)"
  shows "(λx. emeasure (κ x) (A x))  borel_measurable X"
proof -
  have **: "A x  sets Y" if "x  space X" for x
  proof -
    have "Pair x -` Sigma (space X) A = A x"
      using that by auto
    with sets_Pair1[OF A, of x] show "A x  sets Y"
      by auto
  qed

  have *: "x. fst x  space X  snd x  A (fst x)  x  (SIGMA x:space X. A x)"
    by (auto simp: fun_eq_iff)
  have "(λ(x, y). indicator (A x) y::ennreal)  borel_measurable (X M Y)"
    by (measurable,subst measurable_cong[OF *]) (auto simp: space_pair_measure)
  then have "(λx. integralN (κ x) (indicator (A x)))  borel_measurable X"
    by(rule nn_integral_measurable_f)
  moreover have "integralN (κ x) (indicator (A x)) = emeasure (κ x) (A x)" if "x  space X" for x
    using **[OF that] kernel_sets[OF that] by(auto intro!: nn_integral_indicator)
  ultimately show "(λx. emeasure (κ x) (A x))  borel_measurable X"
    by(auto cong: measurable_cong)
qed

lemma(in s_finite_kernel) measure_measurable':
  assumes "(SIGMA x:space X. A x)  sets (X M Y)"
  shows "(λx. measure (κ x) (A x))  borel_measurable X"
  using emeasure_measurable'[OF assms] by(simp add: measure_def)

lemma(in s_finite_kernel) AE_pred:
  assumes P[measurable]:"Measurable.pred (X M Y) (case_prod P)"
  shows "Measurable.pred X (λx. AE y in κ x. P x y)"
proof -
  have [measurable]:"Measurable.pred X (λx. emeasure (κ x) {y  space Y. ¬ P x y} = 0)"
  proof(rule pred_eq_const1[where N=borel],rule emeasure_measurable')
   have "(SIGMA x:space X. {y  space Y. ¬ P x y}) = {xyspace (X M Y). ¬ P (fst xy) (snd xy)}"
      by (auto simp: space_pair_measure)
    also have "...  sets (X M Y)"
      by simp
    finally show "(SIGMA x:space X. {y  space Y. ¬ P x y})  sets (X M Y)" .
  qed simp
  have "{x  space X. almost_everywhere (κ x) (P x)} = {x  space X. emeasure (κ x) {yspace Y. ¬ P x y} = 0}"
  proof safe
    fix x
    assume x:"x  space X"
    show "(AE y in κ x. P x y)  emeasure (κ x) {y  space Y. ¬ P x y} = 0"
      using emeasure_eq_0_AE[of "λy. ¬ P x y" "κ x"]
      by(simp add: sets_eq_imp_space_eq[OF kernel_sets[OF x]])
    show "emeasure (κ x) {y  space Y. ¬ P x y} = 0  almost_everywhere (κ x) (P x)"
      using x by(auto intro!: AE_I[where N="{y  space Y. ¬ P x y}"] simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] kernel_sets[OF x])
  qed
  also have "...  sets X"
    by(simp add: pred_def)
  finally show ?thesis
    by(simp add: pred_def)
qed

lemma(in subprob_kernel) integrable_probability_kernel_pred:
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes [measurable]:"(λ(x,y). f x y)  borel_measurable (X M Y)"
    shows "Measurable.pred X (λx. integrable (κ x) (f x))"
proof(rule measurable_cong[THEN iffD2])
  show "x  space X  integrable (κ x) (f x)  (+y. norm (f x y) (κ x)) < " for x
    by(auto simp: integrable_iff_bounded)
next
  have "(λ(x,y). ennreal (norm (f x y)))  borel_measurable (X M Y)"
    by measurable
  from nn_integral_measurable_f[OF this]
  show "Measurable.pred X (λx. (+ y. ennreal (norm (f x y)) κ x) < )"
    by simp
qed

corollary integrable_measurable_subprob':
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes [measurable]:"(λ(x,y). f x y)  borel_measurable (X M Y)" "k  X M subprob_algebra Y"
  shows "Measurable.pred X (λx. integrable (k x) (f x))"
  by(auto intro!: subprob_kernel.integrable_probability_kernel_pred[where Y=Y] simp: subprob_kernel_def')

lemma(in subprob_kernel) integrable_probability_kernel_pred':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes "f  borel_measurable (X M Y)"
  shows "Measurable.pred X (λx. integrable (κ x) (curry f x))"
  using integrable_probability_kernel_pred[of "curry f"] assms by auto

lemma(in subprob_kernel) lebesgue_integral_measurable_f_subprob:
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes [measurable]:"f  borel_measurable (X M Y)"
  shows "(λx. y. f (x,y) (κ x))  borel_measurable X"
proof -
  from borel_measurable_implies_sequence_metric[OF assms, of 0]
  obtain s where s: "i. simple_function (X M Y) (s i)"
    and "xspace (X M Y). (λi. s i x)  f x"
    and "i. xspace (X M Y). dist (s i x) 0  2 * dist (f x) 0"
    by auto
  then have *:
    "x y. x  space X  y  space Y  (λi. s i (x, y))  f (x,y)"
    "i x y. x  space X  y  space Y  norm (s i (x, y))  2 * norm (f (x, y))"
    by (auto simp: space_pair_measure)

  have [measurable]: "i. s i  borel_measurable (X M Y)"
    by (rule borel_measurable_simple_function) fact

  have s':"i. s i  X M Y M count_space UNIV"
    by (rule measurable_simple_function) fact

  define f' where [abs_def]: "f' i x =
    (if integrable (κ x) (curry f x) then Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y)) else 0)" for i x

  have eq: "Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y)) =
      (zs i ` (space X × space Y). measure (κ x) {y  space (κ x). s i (x, y) = z} *R z)" if "x  space X" for x i
  proof -
    have [measurable_cong]: "sets (κ x) = sets Y" and [simp]: "space (κ x) = space Y"
      using that  by (simp_all add: kernel_sets kernel_space)
    with that show ?thesis
      using s[THEN simple_functionD(1)]
      unfolding simple_bochner_integral_def
      by (intro sum.mono_neutral_cong_left)
         (auto simp: eq_commute space_pair_measure image_iff cong: conj_cong)
  qed

  show ?thesis
  proof (rule borel_measurable_LIMSEQ_metric)
    fix i
    note [measurable] = integrable_probability_kernel_pred'[OF assms]
    have [measurable]:"(SIGMA x:space X. {y  space Y. s i (x, y) = s i (a, b)})  sets (X M Y)" for a b
    proof -
      have "(SIGMA x:space X. {y  space Y. s i (x, y) = s i (a, b)}) = space (X M Y)  s i -` {s i (a,b)}"
        by(auto simp: space_pair_measure)
      thus ?thesis
        using s'[of i] by simp
    qed
    show "f' i  borel_measurable X"
      by (auto simp : eq kernel_space f'_def cong: measurable_cong if_cong intro!: borel_measurable_sum measurable_If borel_measurable_scaleR measure_measurable')
  next
    fix x
    assume x:"x  space X"
    have "(λi. Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y)))  (y. f (x,y) (κ x))" if int_f:"integrable (κ x) (curry f x)"
    proof -
      have int_2f: "integrable (κ x) (λy. 2 * norm (f (x,y)))"
        using int_f by(auto simp: curry_def)
      have "(λi. integralL (κ x) (λy. s i (x, y)))  integralL (κ x) (curry f x)"
      proof (rule integral_dominated_convergence)
        show "curry f x  borel_measurable (κ x)"
          using int_f by auto
      next
        show "i. (λy. s i (x, y))  borel_measurable (κ x)"
          using x kernel_sets by auto
      next
        show "AE xa in κ x. (λi. s i (x, xa))  curry f x xa"
          using x *(1) kernel_space by(auto simp: curry_def)
      next
        show "i. AE xa in κ x. norm (s i (x, xa))  2 * norm (f (x,xa))"
          using x * (2) kernel_space by auto
      qed fact
      moreover have "integralL (κ x) (λy. s i (x, y)) = Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y))" for i
      proof -
        have "Bochner_Integration.simple_bochner_integrable (κ x) (λy. s i (x, y))"
        proof (rule simple_bochner_integrableI_bounded)
         have "(λy. s i (x, y)) ` space Y  s i ` (space X × space Y)"
            using x by auto
          then show "simple_function (κ x) (λy. s i (x, y))"
            using simple_functionD(1)[OF s(1), of i] x kernel_space
            by (intro simple_function_borel_measurable) (auto simp: space_pair_measure dest: finite_subset)
        next
          have "(+ y. ennreal (norm (s i (x, y))) κ x)  (+ y. 2 * norm (f (x,y)) κ x)"
            using x *(2) kernel_space by (intro nn_integral_mono) auto
          also have "... < "
            using int_2f unfolding integrable_iff_bounded by simp
          finally show "(+ y. ennreal (norm (s i (x, y))) κ x) < " .
        qed
        then show ?thesis
          by (rule simple_bochner_integrable_eq_integral[symmetric])
      qed
      ultimately show ?thesis
        by(simp add: curry_def)
    qed
    thus "(λi. f' i x)  (y. f (x,y) (κ x))"
      by (cases "integrable (κ x) (curry f x)") (simp_all add: f'_def not_integrable_integral_eq curry_def)
  qed
qed

lemma(in s_finite_kernel) integrable_measurable_pred[measurable (raw)]:
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes [measurable]:"case_prod f  borel_measurable (X M Y)"
  shows "Measurable.pred X (λx. integrable (κ x) (f x))"
proof(cases "space X = {}")
  case True
  from space_empty[OF this] show ?thesis
    by simp
next
  case h:False
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    using s_finite_kernels by metis
  have [simp]:"integrable (κ x) (f x) = ((i. + y. ennreal (norm (f x y)) ki i x) < )" if "x  space X" for x
    using ki(1) nn_integral_measure_suminf[of "λi. ki i x" "κ x",OF _ ki(2)] that kernel_sets
    by(auto simp: integrable_iff_bounded  subprob_kernel_def measure_kernel_def)
  note [measurable] = nn_integral_measurable_subprob_algebra2
  show ?thesis
    by(rule measurable_cong[where g="λx. (i. +y. ennreal (norm (f x y)) (ki i x)) < ",THEN iffD2]) (insert ki(1), auto simp: subprob_kernel_def')
qed

lemma(in s_finite_kernel) integral_measurable_f:
  fixes f :: "_  _  _::{banach, second_countable_topology}"
  assumes [measurable]:"case_prod f  borel_measurable (X M Y)"
  shows "(λx. y. f x y (κ x))  borel_measurable X"
proof -
  obtain ki where ki:"i. subprob_kernel X Y (ki i)" "x A. x  space X  κ x A = (i. ki i x A)"
    using s_finite_kernels by metis
  note [measurable] = integral_measurable_subprob_algebra2

  show ?thesis
  proof(rule measurable_cong[where f="(λx. if integrable (κ x) (f x) then (i. y. f x y (ki i x)) else 0)",THEN iffD1])
    fix x
    assume h:"x  space X"
    {
      assume h':"integrable (κ x) (f x)"
      have "(i. y. f x y (ki i x)) = (y. f x y (κ x))"
        using lebesgue_integral_measure_suminf[of "λi. ki i x" "κ x",OF _ ki(2) h'] ki(1) kernel_sets[OF h] h
        by(auto simp: subprob_kernel_def measure_kernel_def)
    }
    thus "(if integrable (κ x) (f x) then (i. y. f x y (ki i x)) else 0) = (y. f x y (κ x))"
      using not_integrable_integral_eq by auto
  qed(insert ki(1), auto simp: subprob_kernel_def')
qed

lemma(in s_finite_kernel) integral_measurable_f':
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes [measurable]:"f  borel_measurable (X M Y)"
  shows "(λx. y. f (x,y) (κ x))  borel_measurable X"
  using integral_measurable_f[of "curry f"] by simp

lemma(in s_finite_kernel)
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes [measurable_cong]: "sets μ = sets X"
      and "integrable (μ k κ) f"
    shows integrable_bind_kernelD1: "integrable μ (λx. y. norm (f y) κ x)" (is ?g1)
      and integrable_bind_kernelD1': "integrable μ (λx. y. f y κ x)" (is ?g1')
      and integrable_bind_kernelD2: "AE x in μ. integrable (κ x) f" (is ?g2)
      and integrable_bind_kernelD3: "space X  {}  f  borel_measurable Y" (is "_  ?g3")
proof -
  show 1:"space X  {}  ?g3"
    using assms(2) sets_bind_kernel[OF _ assms(1)] by(simp add: integrable_iff_bounded cong: measurable_cong_sets)
  have "integrable μ (λx. y. norm (f y) κ x)  integrable μ (λx. y. f y κ x)  (AE x in μ. integrable (κ x) f)"
  proof(cases "space X = {}")
    assume ne: "space X  {}"
    then have "space μ  {}" by(simp add: sets_eq_imp_space_eq[OF assms(1)])
    note h = integral_measurable_f[measurable] sets_bind_kernel[OF ne assms(1),measurable_cong]
    have g2: ?g2
      unfolding integrable_iff_bounded AE_conj_iff
    proof safe
      show "AE x in μ. f  borel_measurable (κ x)"
        using assms(2) by(auto simp: sets_eq_imp_space_eq[OF assms(1)] measurable_cong_sets[OF kernel_sets])
    next
      note nn_integral_measurable_f[measurable]
      have "AE x in μ. (+ x. ennreal (norm (f x)) κ x)  "
        by(rule nn_integral_PInf_AE,insert assms(2)) (auto simp: integrable_iff_bounded nn_integral_bind_kernel[OF _ assms(1)] intro!: )
      thus "AE x in μ. (+ x. ennreal (norm (f x)) κ x) < "
        by (simp add: top.not_eq_extremum)
    qed
    have [simp]:"(+ x. + x. ennreal (norm (f x)) κ x μ) =  (+ x. ennreal (y. norm (f y) κ x)μ)"
      using g2 by(auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral)
    have g1: ?g1
      using assms(2) by(auto simp: integrable_iff_bounded measurable_cong_sets[OF h(2)] measurable_cong_sets[OF assms(1)] nn_integral_bind_kernel[OF _ assms(1)])
    have ?g1'
      using assms(2) by(auto intro!: Bochner_Integration.integrable_bound[OF g1])
    with g2 g1 show ?thesis
      by auto
  qed(auto simp: space_empty[of μ] sets_eq_imp_space_eq[OF assms(1)] integrable_iff_bounded nn_integral_empty)
  thus ?g1 ?g1' ?g2
    by auto
qed

lemma(in s_finite_kernel)
  fixes f :: "_  _::{banach, second_countable_topology}"
  assumes [measurable_cong]: "sets μ = sets X"
      and [measurable]:"AE x in μ. integrable (κ x) f" "integrable μ (λx. y. norm (f y) κ x)" "f  borel_measurable Y"
    shows integrable_bind_kernel: "integrable (μ k κ) f"
      and integral_bind_kernel: "(y. f y (μ k κ)) = (x. (y. f yκ x) μ)" (is ?eq)
proof -
  have "integrable (μ k κ) f  (y. f y (μ k κ)) = (x. (y. f yκ x) μ)"
  proof(cases "space X = {}")
    assume ne: "space X  {}"
    note sets_bind[measurable_cong] = sets_bind_kernel[OF ne assms(1)]
    note h = integral_measurable_f[measurable]
    have 1:"integrable (μ k κ) f"
      unfolding integrable_iff_bounded
    proof
      show "(+ x. ennreal (norm (f x)) (μ k κ)) < " (is "?l < _")
      proof -
        have "?l = (+ x. ennreal (y. norm (f y) κ x)μ)"
          using assms(2) by(auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral simp: nn_integral_bind_kernel[OF _ assms(1)])
        also have "... < "
          using assms(3) by(auto simp: integrable_iff_bounded)
        finally show ?thesis .
      qed
    qed simp
    then have ?eq
    proof induction
      case h[measurable]:(base A c)
      hence 1:"integrable (μ k κ) (indicat_real A)"
        by simp
      have 2:"integrable μ (λx. measure (κ x) A)"
        by(rule Bochner_Integration.integrable_cong[where f="λx. Sigma_Algebra.measure (κ x) (A  space (κ x))",THEN iffD1,OF refl])
        (insert h integrable_bind_kernelD1[OF assms(1) 1] sets_eq_imp_space_eq[OF kernel_sets], auto simp: sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF kernel_sets] sets_bind)
      have "AE x in μ. emeasure (κ x) A  "
        by(rule nn_integral_PInf_AE,insert h) (auto simp: emeasure_bind_kernel[OF assms(1) _ ne] sets_bind)
      hence 0:"AE x in μ. emeasure (κ x) A < "
        by (simp add: top.not_eq_extremum)
      have "(x. (y. indicat_real A y *R c κ x) μ) = (x. measure (κ x) A *R cμ)"
        using h integrable_bind_kernelD2[OF assms(1) integrable_real_indicator,of A]
        by(auto intro!: integral_cong_AE simp: sets_eq_imp_space_eq[OF kernel_sets] sets_bind sets_eq_imp_space_eq[OF assms(1)])
      also have "... = (x. measure (κ x) A μ) *R c"
        using 2 by(auto intro!: integral_scaleR_left)
      finally show ?case
        using h by(auto simp: measure_bind_kernel[OF assms(1) _ ne 0] sets_bind)
    next
      case ih:(add f g)
      show ?case
        using ih(1,2) integrable_bind_kernelD2[OF assms(1) ih(1)] integrable_bind_kernelD2[OF assms(1) ih(2)]
        by(auto simp: ih(3,4) Bochner_Integration.integral_add[OF integrable_bind_kernelD1'[OF assms(1) ih(1)] integrable_bind_kernelD1'[OF assms(1) ih(2)],symmetric] intro!: integral_cong_AE)
    next
      case ih:(lim f fn)
      show ?case (is "?lhs = ?rhs")
      proof -
        have conv: "AE x in μ. (λn. y. fn n yκ x)  (y. f y κ x)"
        proof -
          have conv:"AE x in μ. integrable (κ x) f  (λn. y. fn n yκ x)  (y. f y κ x)"
          proof
            fix x
            assume h:"x  space μ"
            then show "integrable (κ x) f  (λn. y. fn n yκ x)  (y. f y κ x)"
              using ih by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f x)"]  simp: sets_eq_imp_space_eq[OF sets_bind] sets_eq_imp_space_eq[OF kernel_sets[OF h[simplified sets_eq_imp_space_eq[OF assms(1)]]]] sets_eq_imp_space_eq[OF assms(1)])
          qed
          with conv integrable_bind_kernelD2[OF assms(1) ih(4)]
          show ?thesis by fastforce
        qed
        have "?lhs = lim (λn. y. fn n y (μ k κ))"
          by(rule limI[OF integral_dominated_convergence[where w="λx. 2 * norm (f x)"],symmetric]) (use ih in auto)
        also have "... = lim (λn. (x. (y. fn n yκ x) μ))"
          by(simp add: ih)
        also have "... = (x. lim (λn. y. fn n yκ x) μ)"
        proof(rule limI[OF integral_dominated_convergence[where w="λx. y. 2 * norm (f y) κ x"]])
          fix n
          show "AE x in μ. norm (y. fn n yκ x)  (y. 2 * norm (f y) κ x)"
            by(rule AE_mp[OF integrable_bind_kernelD2[OF assms(1) ih(1),of n] AE_mp[OF integrable_bind_kernelD2[OF assms(1) ih(4)]]],standard+,rule order.trans[OF integral_norm_bound integral_mono[of "κ _" "λy. norm (fn n y)" _,OF _ _ ih(3)[simplified sets_eq_imp_space_eq[OF sets_bind]]]])
              (auto simp: sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF kernel_sets])
        qed(use ih integrable_bind_kernelD1[OF assms(1) ih(4)] conv limI in auto,fastforce)
        also have "... = ?rhs"
          using ih conv limI by(auto intro!: integral_cong_AE, blast)
        finally show ?thesis .
      qed
    qed
    with 1 show ?thesis
      by auto
  qed(auto simp: bind_kernel_def space_empty[of μ] sets_eq_imp_space_eq[OF assms(1)] integrable_iff_bounded nn_integral_empty Bochner_Integration.integral_empty)
  thus "integrable (μ k κ) f" ?eq
    by auto
qed

end