Theory S_Finite_Measure_Monad.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)) ∧ (∀A∈sets 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)) ∧ (∀A∈sets 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. A∈sets 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 = (∑i∈I. 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 = (∑i∈I. 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 "... = (∫⇧+ x∈A. emeasure (Mi (to_nat_on (space M) x)) A ∂count_space UNIV)"
        by (simp add: nn_integral_count_space_indicator)
      also have "... = (∫⇧+ i∈to_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 "... = (∫⇧+ i∈to_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) ∧ (∀A∈sets M. M A = (∑i. Mi i A)))"
proof
  assume "∃Mi. (∀i. sets (Mi i) = sets M) ∧ (∀i. emeasure (Mi i) (space M) ≤ 1) ∧ (∀A∈sets 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" "(∀A∈sets 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. A∈sets 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) ∧ (∀A∈sets 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. A∈sets 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. integral⇧N (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. integral⇧N 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 "... = integral⇧N 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 {x∈space M. f x = ∞} x)
                                   else if j = 1 then density (Mi i) (λx. f x * indicator {x∈space 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 {x∈space M. f x = ∞} x * indicator A x + f x * indicator {x∈space 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 {x∈space M. f x = ∞} x) A + density (Mi i) (λx. f x * indicator {x∈space 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 {x∈space 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 {x∈space 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. A∈sets 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: "{x∈space (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) = integral⇧N (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) = integral⇧N (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)) = integral⇧N (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 "∀x∈space (N ⨂⇩M M). (λi. s i x) ⇢ (case x of (x, y) ⇒ f x y)"
    and "∀i. ∀x∈space (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)) =
      (∑z∈s 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. integral⇧L M (λy. s i (x, y))) ⇢ integral⇧L 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 "integral⇧L 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))) ⇢ integral⇧L M (f x)"
        by simp }
    then
    show "(λi. f' i x) ⇢ integral⇧L 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)) = integral⇧L (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 {y∈space 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 = {y∈space 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) = integral⇧L (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 {y∈space 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 {y∈space 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 {y∈space 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. integral⇧L (M1 ⨂⇩M M) (s i)) ⇢ integral⇧L (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. integral⇧L (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) = integral⇧L (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) = integral⇧L (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. i∈I ⟹ A i ∈ sets (M i)) ⟹ emeasure (PiM I M) (Pi⇩E I A) = (∏i∈I. 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 (Pi⇩M I M ⨂⇩M M i) (Pi⇩M (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 (Pi⇩M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi⇩E (insert i I) A)) =
    (∏i∈insert 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 ∈ (Π j∈J. sets (M j))"
    then have J: "J ≠ {}" "finite J" "J ⊆ insert i I" and E: "∀j∈J. E j ∈ sets (M j)" by auto
    let ?p = "prod_emb (insert i I) M J (Pi⇩E J E)"
    let ?p' = "prod_emb I M (J - {i}) (Π⇩E j∈J-{i}. E j)"
    have "?μ ?p =
      emeasure (Pi⇩M I M ⨂⇩M (M i)) (?h -` ?p ∩ space (Pi⇩M I M ⨂⇩M M i))"
      by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
    also have "?h -` ?p ∩ space (Pi⇩M 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 (Pi⇩M I M ⨂⇩M (M i)) (?p' × (if i ∈ J then E i else space (M i))) =
      emeasure (Pi⇩M 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 j∈I. 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 (Pi⇩M I M) (Π⇩E j∈I. if j ∈ J-{i} then E j else space (M j)) =
      (∏ j∈I. 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 "(∏j∈I. 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)) = (∏j∈insert i I. ?f J E j)"
      using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
    also have "… = (∏j∈J ∪ ?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 (Pi⇩E J E) ∈ Pow (Π⇩E i∈insert 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 (Pi⇩M (insert i I) M)) ?μ" "countably_additive (sets (Pi⇩M (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 ∈ (Π j∈insert 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 (Pi⇩M I M) (Pi⇩E I A) = (∏i∈I. 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) ⟹ integral⇧N (Pi⇩M {} 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. ∫⇧+x∈A. (κ x B) ∂μ)"
  shows "ν B = (∫⇧+x∈A. (κ x B) ∂μ)"
proof -
  have nu_sets[measurable_cong]: "sets ν = sets Y"
    by(simp add: ν_def)
  have "positive (sets Y) (λB. ∫⇧+x∈A. (κ x B) ∂μ)"
    by(simp add: positive_def)
  moreover have "countably_additive (sets Y) (λB. ∫⇧+x∈A. (κ x B) ∂μ)"
    unfolding countably_additive_def
  proof safe
    fix C :: "nat ⇒ _"
    assume h:"range C ⊆ sets Y" "disjoint_family C"
    thus "(∑i. ∫⇧+x∈A. (κ x) (C i)∂μ) = (∫⇧+x∈A. (κ 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. integral⇧N (κ 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. integral⇧N (κ x) (⨆ range U)" and g="λx. ⨆i. integral⇧N (κ 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) ∧ (∀x∈space X. ∀A∈sets 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) ∧ (∀x∈space X. ∀A∈sets 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) ∧ (∀x∈space X. ∀A∈sets 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 = (∑i∈I. 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) = (∑i∈I. 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 {y∈space Y. f x y = ∞} y)
                                    else if j = (Suc 0) then density (ki' i x) (λy. f x y * indicator {y∈space 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 = (∫⇧+y∈A. 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 {y∈space Y. f x y = ∞} y) A + density (ki' i x) (λy. f x y * indicator {y∈space 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. integral⇧N (κ x) f ∂μ) = (∫⇧+ x. integral⇧N (κ 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. integral⇧N (μ ⤜⇩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. integral⇧N (κ x) (indicator (A x))) ∈ borel_measurable X"
    by(rule nn_integral_measurable_f)
  moreover have "integral⇧N (κ 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}) = {xy∈space (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) {y∈space 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 "∀x∈space (X ⨂⇩M Y). (λi. s i x) ⇢ f x"
    and "∀i. ∀x∈space (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)) =
      (∑z∈s 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. integral⇧L (κ x) (λy. s i (x, y))) ⇢ integral⇧L (κ 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 "integral⇧L (κ 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