Theory Kernels

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

section ‹ Kernels ›
theory Kernels
  imports Lemmas_S_Finite_Measure_Monad
begin

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

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

lemmas(in finite_measure) s_finite_measure_finite_measure = s_finite_measure

lemmas(in subprob_space) s_finite_measure_subprob = s_finite_measure

lemmas(in prob_space) s_finite_measure_prob = s_finite_measure

sublocale sigma_finite_measure  s_finite_measure
  by(rule s_finite_measure)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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