Theory Coproduct_Measure

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

theory Coproduct_Measure
  imports "Lemmas_Coproduct_Measure"
          "HOL-Analysis.Analysis"
begin

section ‹ Binary Coproduct Measures ›
definition copair_measure :: "['a measure, 'b measure]  ('a + 'b) measure" (infixr M 65) where
"M M N = measure_of (space M <+> space N)
                      ({Inl ` A |A. A  sets M}  {Inr ` A|A. A  sets N})
                      (λA. emeasure M (Inl -` A) + emeasure N (Inr -` A))"

subsection ‹The Measurable Space and Measurability›
lemma
  shows space_copair_measure: "space (copair_measure M N) = space M <+> space N"
    and sets_copair_measure_sigma:
       "sets (copair_measure M N)
         = sigma_sets (space M <+> space N) ({Inl ` A |A. A  sets M}  {Inr ` A|A. A  sets N})"
    and Inl_measurable[measurable]: "Inl  M M M M N"
    and Inr_measurable[measurable]: "Inr  N M M M N"
proof -
  have 1:"({Inl ` A |A. A  sets M}  {Inr ` A|A. A  sets N})  Pow (space M <+> space N)"
    using sets.sets_into_space[of _ M] sets.sets_into_space[of _ N] by fastforce
  show "space (copair_measure M N) = space M <+> space N"
 and 2:"sets (copair_measure M N)
        = sigma_sets (space M <+> space N) ({Inl ` A |A. A  sets M}  {Inr ` A|A. A  sets N})"
    by(simp_all add: copair_measure_def sets_measure_of[OF 1] space_measure_of[OF 1])
  show "Inl  M M M M N" "Inr  N M M M N"
    by(auto intro!: measurable_sigma_sets[OF 2 1] simp: vimage_def image_def)
qed

lemma sets_copair_measure_cong:
  "sets M1 = sets M2  sets N1 = sets N2  sets (M1 M N1) = sets (M2 M N2)"
  by(simp cong: sets_eq_imp_space_eq add: sets_copair_measure_sigma)

lemma measurable_image_Inl[measurable]: "A  sets M  Inl ` A  sets (M M N)"
  using sets_copair_measure_sigma by fastforce

lemma measurable_image_Inr[measurable]: "A  sets N  Inr ` A  sets (M M N)"
  using sets_copair_measure_sigma by fastforce

lemma measurable_vimage_Inl:
  assumes [measurable]:"A  sets (M M N)"
  shows "Inl -` A  sets M"
proof -
  have "Inl -` A = Inl -` A  space M"
    using sets.sets_into_space[OF assms]
    by(auto simp add: space_copair_measure)
  also have "...  sets M"
    by simp
  finally show ?thesis .
qed

lemma measurable_vimage_Inr:
  assumes [measurable]:"A  sets (M M N)"
  shows "Inr -` A  sets N"
proof -
  have "Inr -` A = Inr -` A  space N"
    using sets.sets_into_space[OF assms]
    by(auto simp add: space_copair_measure)
  also have "...  sets N"
    by simp
  finally show ?thesis .
qed

lemma in_sets_copair_measure_iff:
 "A  sets (copair_measure M N)  Inl -` A  sets M  Inr -` A  sets N"
proof safe
  assume [measurable]: "Inl -` A  sets M" "Inr -` A  sets N"
  have "A = ((Inl ` Inl -` A)  (Inr ` Inr -` A))"
    by(simp add: vimage_def image_def) (safe, metis obj_sumE)
  also have "...  sets (copair_measure M N)"
    by measurable
  finally show "A   sets (copair_measure M N)" .
qed(use measurable_vimage_Inl measurable_vimage_Inr in auto)

lemma measurable_copair_Inl_Inr:
  assumes [measurable]:"(λx. f (Inl x))  M M L" "(λx. f (Inr x))  N M L"
  shows "f  M M N M L"
proof(rule measurableI)
  fix A
  assume [measurable]:"A  sets L"
  have "f -` A = Inl ` ((λx. f (Inl x)) -` A)  Inr ` ((λx. f (Inr x)) -` A)"
    by(simp add: image_def vimage_def) (safe, metis obj_sumE)
  hence "f -` A  space (M M N)
         = Inl ` ((λx. f (Inl x)) -` A  space M)  Inr ` ((λx. f (Inr x)) -` A  space N)"
    by(auto simp: space_copair_measure)
  also have "...  sets (M M N)"
    by measurable
  finally show "f -` A  space (M M N)  sets (M M N)" .
next
  show "x. x  space (M M N)  f x  space L"
    using measurable_space[OF assms(1)] measurable_space[OF assms(2)]
    by(auto simp add: space_copair_measure)
qed

corollary measurable_copair_measure_iff:
 "f  M M N M L  (λx. f (Inl x))  M M L  (λx. f (Inr x))  N M L"
  by(auto simp add: measurable_copair_Inl_Inr)

lemma measurable_copair_dest1:
  assumes [measurable]:"f  L M M M N" and "f -` (Inl ` space M)  space L = space L"
  obtains f' where "f'  L M M" "x. x  space L  f x = Inl (f' x)"
proof -
  define f' where "f'  (λx. SOME y. f x = Inl y)"
  have f':"x. x  space L  f x = Inl (f' x)"
    unfolding f'_def by(rule someI_ex) (use assms(2) in blast)
  moreover have "f'  L M M"
  proof(rule measurableI)
    show "x. x  space L  f' x  space M"
      using f' measurable_space[OF assms(1)]
      by(auto simp: space_copair_measure)
  next
    fix A
    assume A[measurable]:"A  sets M"
    have [simp]:"f' -` A  space L = f -` (Inl ` A)  space L"
      using f' sets.sets_into_space[OF A] by auto
    show "f' -` A  space L  sets L"
      by auto
  qed
  ultimately show ?thesis
    using that by blast
qed

lemma measurable_copair_dest2:
  assumes [measurable]:"f  L M M M N" and "f -` (Inr ` space N)  space L = space L"
  obtains f' where "f'  L M N" "x. x  space L  f x = Inr (f' x)"
proof -
  define f' where "f'  (λx. SOME y. f x = Inr y)"
  have f':"x. x  space L  f x = Inr (f' x)"
    unfolding f'_def by(rule someI_ex) (use assms(2) in blast)
  moreover have "f'  L M N"
  proof(rule measurableI)
    show "x. x  space L  f' x  space N"
      using f' measurable_space[OF assms(1)]
      by(auto simp: space_copair_measure)
  next
    fix A
    assume A[measurable]:"A  sets N"
    have [simp]:"f' -` A  space L = f -` (Inr ` A)  space L"
      using f' sets.sets_into_space[OF A] by auto
    show "f' -` A  space L  sets L"
      by auto
  qed
  ultimately show ?thesis
    using that by blast
qed

lemma measurable_copair_dest3:
  assumes [measurable]:"f  L M M M N"
    and "f -` (Inl ` space M)  space L  space L" "f -` (Inr ` space N)  space L  space L"
  obtains f' f'' where "f'  L M M"  "f''  L M N"
    "x. x  space L  x  f -` Inl ` space M  f x = Inl (f' x)"
    "x. x  space L  x  f -` Inl ` space M  f x = Inr (f'' x)"
proof -
  have ne:"space M  {}" "space N  {}"
    using assms(2,3) measurable_space[OF assms(1)] by(fastforce simp: space_copair_measure)+
  define m where "m  SOME y. y  space M"
  define n where "n  SOME y. y  space N"
  have m[measurable, simp]:"m  space M" and n[measurable, simp]:"n  space N"
    using ne by(auto simp: n_def m_def some_in_eq)
  define f' where "f'  (λx. if x  f -` Inl ` space M then SOME y. f x = Inl y else m)"
  have "x. x  space L  x  f -` Inl ` space M  f x = Inl (SOME y. f x = Inl y)"
    unfolding f'_def by(rule someI_ex) (use assms(2) in blast)
  hence f':"x. x  space L   x  f -` Inl ` space M  f x = Inl (f' x)"
    by(simp add: f'_def)
  hence f'_space: "x  space L  f' x  space M" for x
    using measurable_space[OF assms(1)]
    by(cases "x  f -` Inl ` space M") (auto simp: space_copair_measure f'_def)
  define f'' where "f''  (λx. if x  f -` Inl ` space M then SOME y. f x = Inr y else n)"
  have *:"x. x  space L  x  f -` Inl ` space M  x  f -` Inr ` space N"
    using measurable_space[OF assms(1)] by(fastforce simp: space_copair_measure)
  have "x. x  space L  x  f -` Inl ` space M  f x = Inr ( SOME y. f x = Inr y)"
    unfolding f''_def by(rule someI_ex) (use * in blast)
  hence f'':"x. x  space L  x  f -` Inl ` space M  f x = Inr (f'' x)"
    by(simp add: f''_def)
  hence f''_space:"x  space L   f'' x  space N" for x
    using measurable_space[OF assms(1),of x]
    by(cases "x  f -` Inl ` space M") (auto simp add: space_copair_measure f''_def)
  have "f'  L M M"
  proof -
    have "f' = (λx. if x  f -` Inl ` space M then f' x else m)"
      by(auto simp add: f'_def)
    also have "...  L M M"
    proof(intro measurable_restrict_space_iff[THEN iffD1] measurableI)
      fix A
      assume A[measurable]:"A  sets M"
      have [measurable]:"f  restrict_space L (f -` Inl ` space M) M M M N"
        by(auto intro!: measurable_restrict_space1)
      have [simp]:"f' -` A  space (restrict_space L (f -` Inl ` space M))
                   = f -` (Inl ` A)  space (restrict_space L (f -` Inl ` space M))"
        using f' sets.sets_into_space[OF A] by(fastforce simp: space_restrict_space)
      show "f' -` A  space (restrict_space L (f -` Inl ` space M))
             sets (restrict_space L (f -` Inl ` space M))"
        by simp
    next
      show "x. x  space (restrict_space L (f -` Inl ` space M))  f' x  space M"
        by(auto simp: space_restrict_space f'_space)
    qed simp_all
    finally show ?thesis .
  qed
  moreover have "f''  L M N"
  proof -
    have "f'' = (λx. if x  f -` Inl ` space M then f'' x else n)"
      by(auto simp add: f''_def)
    also have "...  L M N"
    proof(rule measurable_If_restrict_space_iff[THEN iffD2,OF _ conjI[OF measurableI]])
      fix A
      assume A[measurable]:"A  sets N"
      have f:"f  restrict_space L {x. x  f -` Inl ` space M} M M M N"
        by(auto intro!: measurable_restrict_space1)
      have 1:"f'' -` A  space (restrict_space L {x. x  f -` Inl ` space M})
               = f -` (Inr ` A)  space (restrict_space L {x. x  f -` Inl ` space M})"
        using f'' sets.sets_into_space[OF A] by(fastforce simp: space_restrict_space)
      show "f'' -` A  space (restrict_space L {x. x  f -` Inl ` space M})
             sets (restrict_space L {x. x  f -` Inl ` space M})"
        unfolding 1 using f by simp
    next
      show "x. x  space (restrict_space L {x. x  f -` Inl ` space M})  f'' x  space N"
        by(auto simp: space_restrict_space f''_space)
    qed simp_all
    finally show ?thesis .
  qed
  ultimately show ?thesis
    using that f' f'' by blast
qed      

subsection ‹ Measures ›
lemma emeasure_copair_measure:
  assumes [measurable]: "A  sets (M M N)"
  shows "emeasure (M M N) A = emeasure M (Inl -` A) + emeasure N (Inr -` A)"
proof(rule emeasure_measure_of)
  show "{Inl ` A |A. A  sets M}  {Inr ` A|A. A  sets N}  Pow (space M <+> space N)"
    using sets.sets_into_space[of _ M] sets.sets_into_space[of _ N] by fastforce
  show "A  sets (M M N)"
    by fact
  show "countably_additive (sets (M M N)) (λa. emeasure M (Inl -` a) + emeasure N (Inr -` a))"
  proof(safe intro!: countably_additiveI)
    note [measurable] =  measurable_vimage_Inl[of _ M N] measurable_vimage_Inr[of _ M N]
    fix A :: "nat  _ set"
    assume h:"range A  sets (M M N)" "disjoint_family A"
    then have [measurable]: "i. A i  sets (M M N)"
      by blast
    have disj:"disjoint_family (λi. Inl -` A i)" "disjoint_family (λi. Inr -` A i)"
      using h by(auto simp: disjoint_family_on_def)
    show "(i. emeasure M (Inl -` A i) + emeasure N (Inr -` A i))
           = emeasure M (Inl -`  (range A)) + emeasure N (Inr -`  (range A))" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (i. emeasure M (Inl -` A i)) + (i. emeasure N (Inr -` A i))"
        by(simp add: suminf_add)
      also have "... = emeasure M (i. (Inl -` A i)) + emeasure N (i. (Inr -` A i))"
      proof -
        have "(i. emeasure M (Inl -` A i)) = emeasure M (i. (Inl -` A i))"
             "(i. emeasure N (Inr -` A i)) = emeasure N (i. (Inr -` A i))"
          by(auto intro!: suminf_emeasure disj)
        thus ?thesis
          by argo
      qed
      also have "... = ?rhs"
        by(simp add: vimage_UN)
      finally show ?thesis .
    qed
  qed
qed(auto simp: positive_def copair_measure_def)

lemma emeasure_copair_measure_space:
 "emeasure (M M N) (space (M M N)) = emeasure M (space M) + emeasure N (space N)"
proof -
  have [simp]:"Inl -` space (M M N) = space M" "Inr -` space (M M N) = space N"
    by(auto simp: space_copair_measure)
  show ?thesis
    by(simp add: emeasure_copair_measure)
qed

corollary
  shows emeasure_copair_measure_Inl: "A  sets M  emeasure (M M N) (Inl ` A) = emeasure M A"
    and emeasure_copair_measure_Inr: "B  sets N  emeasure (M M N) (Inr ` B) = emeasure N B"
proof -
  have [simp]:"Inl -` Inl ` A = A" "Inr -` Inl ` A = {}" "Inl -` Inr ` B = {}" "Inr -` Inr ` B = B"
    by auto
  show "A  sets M  emeasure (M M N) (Inl ` A) = emeasure M A"
       "B  sets N  emeasure (M M N) (Inr ` B) = emeasure N B"
    by(simp_all add: emeasure_copair_measure)
qed

lemma measure_copair_measure:
  assumes [measurable]:"A  sets (M M N)" "emeasure (M M N) A < "
  shows "measure (M M N) A = measure M (Inl -` A) + measure N (Inr -` A)"
  using assms(2) by(auto simp add: emeasure_copair_measure measure_def intro!: enn2real_plus)

lemma
  shows measure_copair_measure_Inl: "A  sets M  measure (M M N) (Inl ` A) = measure M A"
    and measure_copair_measure_Inr: "B  sets N  measure (M M N) (Inr ` B) = measure N B"
  by(auto simp: emeasure_copair_measure_Inl measure_def emeasure_copair_measure_Inr)

subsection ‹ Finiteness ›
lemma finite_measure_copair_measure: "finite_measure M  finite_measure N  finite_measure (M M N)"
  by(auto intro!: finite_measureI simp: emeasure_copair_measure_space finite_measure.finite_emeasure_space)

subsection ‹ $\sigma$-Finiteness ›
lemma sigma_finite_measure_copair_measure:
  assumes "sigma_finite_measure M" "sigma_finite_measure N"
  shows "sigma_finite_measure (M M N)"
proof -
  obtain A B where AB[measurable]: "i. A i  sets M" "( (range A)) = space M" "i::nat. emeasure M (A i)  "
      "i. B i  sets N" "( (range B)) = space N" "i::nat. emeasure N (B i)  "
    by (metis range_subsetD sigma_finite_measure.sigma_finite assms)
  then have *:"( (range (λi. Inl ` (A i)  Inr ` (B i)))) = space (M M N)"
    unfolding space_copair_measure Plus_def by fastforce
  have [simp]: "i. Inl -` Inl ` A i  Inl -` Inr ` B i = A i" "i. Inr -` Inl ` A i  Inr -` Inr ` B i = B i"
    using sets.sets_into_space AB(1,4) by blast+  
  show ?thesis
    apply standard
    using AB * by(auto intro!: exI[where x="range (λi. Inl ` (A i)  Inr ` (B i))"]
                         simp: space_copair_measure emeasure_copair_measure)
qed

subsection ‹Non-Negative Integral›
lemma nn_integral_copair_measure:
  assumes "f  borel_measurable (M M N)"
  shows "(+x. f x (M M N)) = (+x. f (Inl x) M) + (+x. f (Inr x) N)"
  using assms
proof induction
  case (cong f g)
  moreover hence "x. x  space M  f (Inl x) = g (Inl x)"
                 "x. x  space N  f (Inr x) = g (Inr x)"
    by(auto simp: space_copair_measure)
  ultimately show ?case
    by(simp cong: nn_integral_cong)
next
  case [measurable]:(set A)
  note [measurable] = measurable_vimage_Inl[of _ M N] measurable_vimage_Inr[of _ M N]
  show ?case
    by (simp add: indicator_vimage[symmetric] emeasure_copair_measure)
next
  case (mult u c)
  then show ?case
    by(simp add: measurable_copair_measure_iff nn_integral_cmult distrib_left)
next
  case (add u v)
  then show ?case
    by(simp add: nn_integral_add)
next
  case h[measurable]:(seq U)
  have inc:"x. incseq (λi. U i x)"
    by (metis h(3) incseq_def le_funE)
  have lim:"(λi. U i x)  Sup (range U) x" for x
    by (metis SUP_apply LIMSEQ_SUP[OF inc[of x]])
  have "(λi. (+ x. U i x (M M N)))  (+ x. (Sup (range U)) x (M M N))"
    by(intro nn_integral_LIMSEQ[OF _ _ lim]) (auto simp: h)
  moreover have "(λi. (+ x. U i x (M M N)))  (+ x. Sup (range U) (Inl x) M) + (+ x. Sup (range U) (Inr x) N)"
  proof -
    have "(λi. (+ x. U i x (M M N))) = (λi. (+ x. U i (Inl x) M) + (+ x. U i (Inr x) N))"
      by(simp add: h)
    also have "...  (+ x. Sup (range U) (Inl x) M) + (+ x. Sup (range U) (Inr x) N)"
    proof(rule tendsto_add)
      have inc:"x. incseq (λi. U i (Inl x))"
        by (metis h(3) incseq_def le_funE)
      have lim:"(λi. U i (Inl x))  Sup (range U) (Inl x)" for x
        by (metis SUP_apply LIMSEQ_SUP[OF inc[of x]])
      show "(λi. (+ x. U i (Inl x) M))  (+ x. Sup (range U) (Inl x) M)"
        using inc by(intro nn_integral_LIMSEQ[OF _ _ lim]) (auto simp: incseq_def intro!: le_funI)
    next
      have inc:"x. incseq (λi. U i (Inr x))"
        by (metis h(3) incseq_def le_funE)
      have lim:"(λi. U i (Inr x))  Sup (range U) (Inr x)" for x
        by (metis SUP_apply LIMSEQ_SUP[OF inc[of x]])
      show "(λi. (+ x. U i (Inr x) N))  (+ x. Sup (range U) (Inr x) N)"
        using inc by(intro nn_integral_LIMSEQ[OF _ _ lim]) (auto simp: incseq_def intro!: le_funI)
    qed
    finally show ?thesis .
  qed
  ultimately show ?case
    using LIMSEQ_unique by blast 
qed

subsection ‹ Integrability ›
lemma integrable_copair_measure_iff:
  fixes f :: "'a + 'b  'c::{banach, second_countable_topology}"
  shows "integrable (M M N) f  integrable M (λx. f (Inl x))  integrable N (λx. f (Inr x))"
  by(auto simp add: measurable_copair_measure_iff nn_integral_copair_measure integrable_iff_bounded)

corollary interable_copair_measureI:
  fixes f :: "'a + 'b  'c::{banach, second_countable_topology}"
  shows "integrable M (λx. f (Inl x))  integrable N (λx. f (Inr x))  integrable (M M N) f"
  by(simp add: integrable_copair_measure_iff)

subsection ‹ The Lebesgue Integral ›
lemma integral_copair_measure:
  fixes f :: "'a + 'b  'c::{banach, second_countable_topology}"
  assumes "integrable (M M N) f"
  shows "(x. f x (M M N)) = (x. f (Inl x) M) + (x. f (Inr x) N)"
  using assms
proof induction
  case h[measurable]:(base A c)
  note [measurable] = measurable_vimage_Inl[of _ M N] measurable_vimage_Inr[of _ M N]
  have [simp]:"integrable (M M N) (indicat_real A)" "integrable M (indicat_real (Inl -` A))"
              "integrable N (indicat_real (Inr -` A))"
    using h(2) by(auto simp: emeasure_copair_measure)
  show ?case
    by(cases "c = 0")
      (simp_all add: indicator_vimage[symmetric] measure_copair_measure measure_copair_measure[OF _ h(2)] scaleR_left_distrib)
next
  case (add f g)
  then show ?case
    by(simp add: integrable_copair_measure_iff)
next
  case ih:(lim f s)
  have "(λn. (x. s n x (M M N)))  (x. f x (M M N))"
    using ih(1-4) by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
  moreover have "(λn. (x. s n x (M M N)))  (x. f (Inl x) M) + (x. f (Inr x) N)"
    using ih(1-4)
    by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f (Inl x))"]
                    integral_dominated_convergence[where w="λx. 2 * norm (f (Inr x))"] tendsto_add
              simp: ih(5) integrable_copair_measure_iff measurable_copair_measure_iff
                    borel_measurable_integrable space_copair_measure InlI InrI)
  ultimately show ?case
    using LIMSEQ_unique by blast
qed

section ‹ Coproduct Measures ›
definition coPiM :: "['i set, 'i  'a measure]  ('i × 'a) measure" where
"coPiM I Mi  measure_of
                (SIGMA i:I. space (Mi i))
                {A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}
                (λA. (iI. emeasure (Mi i) (Pair i -` A)))"

syntax
 "_coPiM" :: "pttrn  'i set  'a measure  ('i × 'a) measure" ((3⨿M __./ _)  10)
translations
 "⨿M xI. M"  "CONST coPiM I (λx. M)"

subsection ‹ The Measurable Space and Measurability ›
lemma
  shows space_coPiM: "space (coPiM I Mi) = (SIGMA i:I. space (Mi i))"
    and sets_coPiM:
    "sets (coPiM I Mi) = sigma_sets (SIGMA i:I. space (Mi i)) {A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
    and sets_coPiM_eq:"sets (coPiM I Mi) = {A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
proof -
  have 1:"{A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}  Pow (SIGMA i:I. space (Mi i))"
    using sets.sets_into_space by auto
  show "space (coPiM I Mi) = (SIGMA i:I. space (Mi i))"
 and 2:"sets (coPiM I Mi)
        = sigma_sets (SIGMA i:I. space (Mi i)) {A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
    by(auto simp: sets_measure_of[OF 1] space_measure_of[OF 1] coPiM_def)
  show "sets (coPiM I Mi) = {A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
  proof -
    have "sigma_algebra (SIGMA i:I. space (Mi i)) {A. A  (SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
    proof(subst Dynkin_system.sigma_algebra_eq_Int_stable)
      show "Dynkin_system (SIGMA i:I. space (Mi i)) {A. A  (SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}"
        by unfold_locales (auto simp: Pair_vimage_Sigma sets.Diff vimage_Diff vimage_Union 1)
    qed (auto intro!: Int_stableI)
    thus ?thesis
      by(auto simp: 2 intro!: sigma_algebra.sigma_sets_eq)
  qed
qed

lemma sets_coPiM_cong:
 "I = J  (i. i  I  sets (Mi i) = sets (Ni i))  sets (coPiM I Mi) = sets (coPiM J Ni)"
  by(simp cong: sets_eq_imp_space_eq Sigma_cong add: sets_coPiM)

lemma measurable_coPiM2:
  assumes [measurable]:"i. i  I  f i  Mi i M N"
  shows "(λ(i,x). f i x)  coPiM I Mi M N"
proof(rule measurableI)
  fix A
  assume [measurable]: "A  sets N"
  have [simp]:
    "i. i  I
     Pair i -` (λ(x, y). f x y) -` A  Pair i -` (SIGMA i:I. space (Mi i)) = f i -` A  space (Mi i)"
    by auto
  show "(λ(i, x). f i x) -` A  space (coPiM I Mi)  sets (coPiM I Mi)"
    by(auto simp: sets_coPiM space_coPiM)
qed(auto simp: space_coPiM measurable_space[OF assms])

lemma measurable_Pair_coPiM[measurable (raw)]:
  assumes "i  I"
  shows "Pair i  Mi i M coPiM I Mi"
proof(rule measurable_sigma_sets)
  show "{A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}
          Pow (SIGMA i:I. space (Mi i))"
    by blast
qed (auto simp: assms sets_coPiM)

lemma measurable_Pair_coPiM':
  assumes "i  I" "(λ(i,x). f i x)  coPiM I Mi M N"
  shows "f i  Mi i M N"
  using measurable_compose[OF measurable_Pair_coPiM assms(2)] assms(1) by fast

lemma measurable_copair_iff: "(λ(i,x). f i x)  coPiM I Mi M N  (iI. f i  Mi i M N)"
  by(auto intro!: measurable_coPiM2 simp: measurable_Pair_coPiM')

lemma measurable_copair_iff': "f  coPiM I Mi M N  (iI. (λx. f (i, x))  Mi i M N)"
  using measurable_copair_iff[of "curry f"] by(simp add: split_beta' curry_def)

lemma coPair_inverse_space_unit:
  "i  I  A  sets (coPiM I Mi)  Pair i -` A  space (Mi i) = Pair i -` A"
  using sets.sets_into_space by(fastforce simp: space_coPiM)

lemma measurable_Pair_vimage:
  assumes "i  I" "A  sets (coPiM I Mi)"
  shows "Pair i -` A  sets (Mi i)"
  using measurable_sets[OF measurable_Pair_coPiM[OF assms(1)] assms(2)]
  by (simp add: coPair_inverse_space_unit[OF assms])

lemma measurable_Sigma_singleton[measurable (raw)]:
 "i A. i  I  A  sets (Mi i)  {i} × A  sets (coPiM I Mi)"
  using sets.sets_into_space sets_coPiM by fastforce

lemma sets_coPiM_countable:
  assumes "countable I"
  shows "sets (coPiM I Mi) = sigma_sets (SIGMA i:I. space (Mi i)) (iI. (×) {i} ` (sets (Mi i)))"
  unfolding sets_coPiM
proof(safe intro!: sigma_sets_eqI)
  fix a
  assume h:"a  (SIGMA i:I. space (Mi i))" "iI. Pair i -` a  sets (Mi i)"
  then have "a = (iI. {i} × Pair i -` a)"
    by auto
  moreover have "(iI. {i} × Pair i -` a)  sigma_sets (SIGMA i:I. space (Mi i)) (iI. (×) {i} ` (sets (Mi i)))"
    using h(2) by(auto intro!: sigma_sets_UNION[OF countable_image[OF assms]])
  ultimately show "a  sigma_sets (SIGMA i:I. space (Mi i)) (iI. (×) {i} ` (sets (Mi i)))"
    by argo
qed(use sets.sets_into_space in fastforce)

lemma measurable_coPiM1':
  assumes "countable I"
    and [measurable]: "a  N M count_space I" "i. i  a ` (space N)  g i  N M Mi i"
  shows "(λx. (a x, g (a x) x))  N M coPiM I Mi"
proof(safe intro!: measurable_sigma_sets[OF sets_coPiM_countable[OF assms(1)]])
  fix i B
  assume iB[measurable]:"i  I" "B  sets (Mi i)"
  show  "(λx. (a x, g (a x) x)) -` ({i} × B)  space N  sets N"
  proof(cases "i  a ` (space N)")
    assume [measurable]:"i  a ` (space N)"
    have "(λx. (a x, g (a x) x)) -` ({i} × B)  space N = (a -` {i}  space N)  (g i -` B  space N)"
      by auto
    also have "...  sets N"
      by simp
    finally show ?thesis .
  next
    assume"i  a ` (space N)"
    then have "(λx. (a x, g (a x) x)) -` ({i} × B)  space N = {}"
      using measurable_space[OF assms(2)] by blast
    thus ?thesis
      by simp
  qed
qed(use measurable_space[OF assms(2)] measurable_space[OF assms(3)] sets.sets_into_space in fastforce)+

lemma measurable_coPiM1:
  assumes "countable I"
    and "a  N M count_space I" "i. i  I  g i  N M Mi i"
  shows "(λx. (a x, g (a x) x))  N M coPiM I Mi"
  using measurable_space[OF assms(2)] by(auto intro!: measurable_coPiM1' assms)

lemma measurable_coPiM1_elements:
  assumes "countable I" and [measurable]:"f  N M coPiM I Mi"
  obtains a g
  where "a  N M count_space I"
        "i. i  I  space (Mi i)  {}  g i  N M Mi i"
        "f = (λx. (a x, g (a x) x))"
proof -
  define a where "a  fst  f"
  have 1[measurable]:"a  N M count_space I"
  proof(safe intro!: measurable_count_space_eq_countable[THEN iffD2] assms)
    fix i
    assume i:"i  I"
    have "a -` {i}  space N = f -` ({i} × space (Mi i))  space N"
      using measurable_space[OF assms(2)] by(fastforce simp: a_def space_coPiM)
    also have "...  sets N"
      using i by auto
    finally show "a -` {i}  space N  sets N" .
  next
    show "x. x  space N  a x  I"
      using measurable_space[OF assms(2)] by(fastforce simp: space_coPiM a_def)
  qed
  define g where "g  (λi x. if a x = i then snd (f x) else (SOME y. y  space (Mi i)))"
  have 2:"g i  N M Mi i" if i:"i  I" and ne:"space (Mi i)  {}" for i
    unfolding g_def
  proof(safe intro!: measurable_If_restrict_space_iff[THEN iffD2] measurable_const some_in_eq[THEN iffD2] ne)
    show "(λx. snd (f x))   restrict_space N {x. a x = i} M Mi i"
    proof(safe intro!: measurableI)
      show "x. x  space (restrict_space N {x. a x = i})  snd (f x)  space (Mi i)"
        using measurable_space[OF assms(2)] by(fastforce simp: space_restrict_space a_def space_coPiM)
    next
      fix A
      assume [measurable]:"A  sets (Mi i)"
      have "(λx. snd (f x)) -` A  space (restrict_space N {x. a x = i}) = f -` ({i} × A)  space N"
        using i measurable_space[OF assms(2)] by(fastforce simp: space_restrict_space a_def space_coPiM)
      also have "...  sets N"
        using i by simp
      finally show "(λx. snd (f x)) -` A  space (restrict_space N {x. a x = i})
                      sets (restrict_space N {x. a x = i})"
        by(auto simp: sets_restrict_space space_restrict_space)
    qed
  qed(use i ne in auto)
  have 3:"f = (λx. (a x, g (a x) x))"
    by(auto simp: a_def g_def)
  show ?thesis
    using 1 2 3 that by blast
qed

subsection ‹ Measures ›
lemma emeasure_coPiM:
  assumes "A  sets (coPiM I Mi)"
  shows "emeasure (coPiM I Mi) A = (iI. emeasure (Mi i) (Pair i -` A))"
proof(rule emeasure_measure_of)
  show "{A. A(SIGMA i:I. space (Mi i))  (iI. Pair i -` A  sets (Mi i))}  Pow (SIGMA i:I. space (Mi i))"
    by blast
next
  note measurable_Pair_vimage[of _ I _ Mi,measurable (raw)]
  show "countably_additive (sets (coPiM I Mi)) (λa. iI. emeasure (Mi i) (Pair i -` a))"
    unfolding countably_additive_def
  proof safe
    fix A :: "nat  _"
    assume A:"range A  sets (coPiM I Mi)" "disjoint_family A"
    then have [measurable]:"n. A n  sets (coPiM I Mi)"
      by blast
    show "(n. iI. emeasure (Mi i) (Pair i -` A n))
           = (iI. emeasure (Mi i) (Pair i -`  (range A)))" (is "?lhs = ?rhs")
    proof -
      have "?lhs = (nUNIV. iI. emeasure (Mi i) (Pair i -` A n))"
        by(auto intro!: infsum_eq_suminf[symmetric] nonneg_summable_on_complete)
      also have "... = (iI. nUNIV. emeasure (Mi i) (Pair i -` A n))"
        by(rule infsum_swap_ennreal)
      also have "... = ?rhs"
      proof(rule infsum_cong)
        fix i
        assume "i  I"
        then have "(n. Mi i (Pair i -` A n)) = Mi i (n. Pair i -` A n)"
          using A(2) by(intro suminf_emeasure) (auto simp: disjoint_family_on_def)
        also have "... = Mi i (Pair i -`  (range A))"
          by (metis vimage_UN)
        finally show "(n. emeasure (Mi i) (Pair i -` A n)) = emeasure (Mi i) (Pair i -`  (range A))"
          by(auto simp: infsum_eq_suminf[OF nonneg_summable_on_complete])
      qed
      finally show ?thesis .
    qed
  qed
next
  show "A  sets (coPiM I Mi)"
    by fact
qed(auto simp: positive_def coPiM_def)

corollary emeasure_coPiM_space:
 "emeasure (coPiM I Mi) (space (coPiM I Mi)) = (iI. emeasure (Mi i) (space (Mi i)))"
proof -
  have [simp]: "i. i  I  Pair i -` space (coPiM I Mi) = space (Mi i)"
    by(auto simp: space_coPiM)
  show ?thesis
    by(auto simp: emeasure_coPiM intro!: infsum_cong)
qed

lemma emeasure_coPiM_coproj:
  assumes [measurable]: "i  I" "A  sets (Mi i)"
  shows "emeasure (coPiM I Mi) ({i} × A) = emeasure (Mi i) A"
proof -
  have "emeasure (coPiM I Mi) ({i} × A) = (jI. emeasure (Mi j) (if j = i then A else {}))"
    by(simp add: emeasure_coPiM)
  also have "... = (j(I - {i})  {i}. emeasure (Mi j) (if j = i then A else {}))"
    by(rule arg_cong[where f="infsum _"]) (use assms in auto)
  also have "... = (jI - {i}. emeasure (Mi j) (if j = i then A else {}))
                    + (j{i}. emeasure (Mi j) (if j = i then A else {}))"
    by(rule infsum_Un_disjoint) (auto intro!: nonneg_summable_on_complete)
  also have "... = emeasure (Mi i) A"
  proof -
    have "(jI - {i}. emeasure (Mi j) (if j = i then A else {})) = 0"
      by (rule infsum_0) simp
    thus ?thesis by simp
  qed
  finally show ?thesis .
qed

lemma measure_coPiM_coproj: "i  I  A  sets (Mi i)  measure (coPiM I Mi) ({i} × A) = measure (Mi i) A"
  by(simp add: emeasure_coPiM_coproj measure_def)

lemma emeasure_coPiM_less_top_summable:
  assumes [measurable]:"A  sets (coPiM I Mi)" "emeasure (coPiM I Mi) A < "
  shows"(λi. measure (Mi i) (Pair i -` A)) summable_on I"
proof -
  have *:"(iI. emeasure (Mi i) (Pair i -` A)) < top"
    using assms(2) by(simp add: emeasure_coPiM)
  from infsum_less_top_dest[OF this] have ifin:"i. i  I  emeasure (Mi i) (Pair i -` A) < top"
    by simp
  with * have "(iI. ennreal (measure (Mi i) (Pair i -` A))) < top"
    by (metis (mono_tags, lifting) emeasure_eq_ennreal_measure infsum_cong top.not_eq_extremum)
  thus ?thesis
    by(auto intro!: bounded_infsum_summable)
qed

lemma measure_coPiM:
  assumes [measurable]:"A  sets (coPiM I Mi)" "emeasure (coPiM I Mi) A < "
  shows "measure (coPiM I Mi) A = (iI. measure (Mi i) (Pair i -` A))"
proof(subst ennreal_inj[symmetric])
  have *:"(iI. emeasure (Mi i) (Pair i -` A)) < top"
    using assms(2) by(simp add: emeasure_coPiM)
  from infsum_less_top_dest[OF this] have ifin:"i. i  I  emeasure (Mi i) (Pair i -` A) < top"
    by simp
  show "ennreal (measure (coPiM I Mi) A) = ennreal (iI. measure (Mi i) (Pair i -` A))" (is "?lhs = ?rhs")
  proof -
    have "?lhs = emeasure (coPiM I Mi) A"
      using assms by(auto intro!: emeasure_eq_ennreal_measure[symmetric])
    also have "... = (iI. emeasure (Mi i) (Pair i -` A))"
      by(simp add: emeasure_coPiM)
    also have "... = (iI. ennreal (measure (Mi i) (Pair i -` A)))"
      using ifin by(fastforce intro!: infsum_cong  emeasure_eq_ennreal_measure)
    also have "... = ?rhs"
      by(simp add: infsum_ennreal_eq[OF emeasure_coPiM_less_top_summable[OF assms]])
    finally show ?thesis .
  qed
qed(auto intro!: infsum_nonneg)

subsection ‹Non-Negative Integral›
lemma nn_integral_coPiM:
  assumes "f  borel_measurable (coPiM I Mi)"
  shows "(+x. f x coPiM I Mi) = (iI. (+x. f (i, x) Mi i))"
  using assms
proof induction
  case (cong f g)
  moreover hence "i x. i  I  x  space (Mi i)  f (i, x) = g (i, x)"
    by(auto simp: space_coPiM)
  ultimately show ?case
    by(simp cong: nn_integral_cong infsum_cong)
next
  case [measurable]:(set A)
  note [measurable] = measurable_Pair_vimage[OF _ this]
  show ?case
    by(simp add: indicator_vimage[symmetric] emeasure_coPiM cong: infsum_cong)
next
  case (add u v)
  then show ?case
    by(simp add: nn_integral_add infsum_add nonneg_summable_on_complete cong: infsum_cong)
next
  case (mult u c)
  then show ?case
    by(simp add: nn_integral_cmult infsum_cmult_right_ennreal cong: infsum_cong)
next
  case ih[measurable]:(seq U)
  show ?case (is "?lhs = ?rhs")
  proof -
    have "?lhs = (+ x. (SUP j. U j x) coPiM I Mi)"
      by(auto intro!: nn_integral_cong simp: SUP_apply[symmetric])
    also have "... = (SUP j. (+ x. U j x coPiM I Mi))"
      by(auto intro!: nn_integral_monotone_convergence_SUP ih(3))
    also have "... = (SUP j. (iI. (+ x. U j (i, x) Mi i)))"
      by(simp add: ih)
    also have "... = (iI. (SUP j. (+ x. U j (i, x) Mi i)))"
      using ih(3) by(auto intro!: ennreal_infsum_Sup_eq[symmetric] incseq_nn_integral simp: mono_compose)
    also have "... = (iI. (+ x. (SUP j. U j (i, x)) Mi i))"
      using ih(3) by(auto intro!: infsum_cong nn_integral_monotone_convergence_SUP[symmetric] mono_compose)
    also have "... = ?rhs"
      by(simp add: SUP_apply[symmetric])
    finally show ?thesis .
  qed
qed

subsection ‹ Integrability ›
lemma
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "integrable (coPiM I Mi) f"
  shows integrable_coPiM_dest_sum:"(iI. (+ x. norm (f (i, x)) Mi i)) < "
    and integrable_coPiM_dest_integrable: "i. i  I  integrable (Mi i) (λx. f (i, x))"
    and integrable_coPiM_summable_norm: "(λi. (x. norm (f (i, x)) Mi i)) summable_on I"
    and integrable_coPiM_abs_summable: "Infinite_Sum.abs_summable_on (λi. (x. f (i, x) Mi i)) I"
    and integrable_coPiM_summable: "(λi. (x. f (i, x) Mi i)) summable_on I"
proof -
  show fin:"(iI. (+ x. norm (f (i, x)) Mi i)) < "
    using assms by(auto simp: integrable_iff_bounded nn_integral_coPiM)
  thus integ:"i  I  integrable (Mi i) (λx. f (i, x))" for i
    using assms by(auto simp: integrable_iff_bounded intro!: infsum_less_top_dest[of _ _ i])
  show summable:"(λi. (x. norm (f (i, x)) Mi i)) summable_on I"
    using nn_integral_eq_integral[OF integrable_norm[OF integ]] fin
    by(auto intro!: bounded_infsum_summable cong: infsum_cong)
  show "Infinite_Sum.abs_summable_on (λi. (x. f (i, x) Mi i)) I"
    by(rule summable_on_comparison_test[OF summable]) auto
  thus "(λi. (x. f (i, x) Mi i)) summable_on I"
    using abs_summable_summable by fastforce
qed

subsection ‹ The Lebesgue Integral ›
lemma integral_coPiM:
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "integrable (coPiM I Mi) f"
  shows "(x. f x coPiM I Mi) = (iI. (x. f (i, x) Mi i))"
  using assms
proof induction
  case h[measurable]:(base A c)
  note [measurable] = measurable_Pair_vimage[OF _ this(1)]
  have [simp]: "integrable (coPiM I Mi) (indicat_real A)"
    "i. i  I  integrable (Mi i) (indicat_real (Pair i -` A))"
    using h(2) by(auto simp: emeasure_coPiM dest: infsum_less_top_dest)
  show ?case
    using h(2) emeasure_coPiM_less_top_summable[OF h]
    by(cases "c = 0")
      (auto simp: measure_coPiM indicator_vimage[symmetric] infsum_scaleR_left[symmetric] cong: infsum_cong)
next
  case h:(add f g)
  show ?case (is "?lhs = ?rhs")
  proof -
    have "?lhs = (iI. (x. f (i, x) Mi i)) + (iI. (x. g (i, x) Mi i))"
      using h by simp
    also have "... = (iI. (x. f (i, x) Mi i) + (x. g (i, x) Mi i))"
      by(auto intro!: infsum_add[symmetric] integrable_coPiM_summable h)
    also have "... = ?rhs"
      using h
      by(auto intro!: infsum_cong Bochner_Integration.integral_add[symmetric] integrable_coPiM_dest_integrable)
    finally show ?thesis .
  qed
next
  case ih:(lim f fn)
  note [measurable,simp] = ih(1-4)
  show ?case (is "?lhs = ?rhs")
  proof -
    have "?lhs = lim (λn. (x. fn n x (coPiM I Mi)))"
      by(auto intro!: limI[symmetric] integral_dominated_convergence[where w="λx. 2 * norm (f x)"])
    also have "... = lim (λn. (iI.  (x. fn n (i, x) Mi i)))"
      by(simp add: ih(5))
    also have "... = lim (λn. (i. (x. fn n (i, x) Mi i)count_space I))"
      by(simp add: integrable_coPiM_abs_summable infsum_eq_integral)
    also have "... = (i. (x. f (i, x) Mi i)count_space I)"
    proof(intro limI integral_dominated_convergence[where w="λi. (x. 2 * norm (f (i, x)) Mi i)"] AE_I2 )
      show "integrable (count_space I) (λi. (x. 2 * norm (f (i, x)) Mi i))"
        by(auto simp: abs_summable_on_integrable_iff[symmetric] integrable_coPiM_summable_norm[OF ih(4)])
    next
      show "i  space (count_space I)  (λn. (x. fn n (i, x) Mi i))  (x. f (i, x) Mi i)" for i
        by(auto intro!: integral_dominated_convergence[where w="λx. 2*norm (f (i, x))"] integrable_coPiM_dest_integrable
                  simp: space_coPiM)
    next
      show "i  space (count_space I)  norm ((x. fn n (i, x) Mi i))  (x.  2 * norm (f (i, x)) Mi i)" for n i
        by(rule order.trans[where b="(x. norm (fn n (i, x)) Mi i)"])
          (auto simp: space_coPiM
            simp del: Bochner_Integration.integral_mult_right_zero Bochner_Integration.integral_mult_right
              intro!: integral_mono integrable_coPiM_dest_integrable)
    qed simp_all
    also have "... = ?rhs"
      by(simp add: infsum_eq_integral integrable_coPiM_abs_summable)
    finally show ?thesis .
  qed
qed

subsection ‹ Finite Coproduct Measures ›
lemma emeasure_coPiM_finite:
  assumes "finite I" "A  sets (coPiM I Mi)"
  shows "emeasure (coPiM I Mi) A = (iI. emeasure (Mi i) (Pair i -` A))"
  using assms by(simp add: emeasure_coPiM)

lemma emeasure_coPiM_finite_space:
 "finite I  emeasure (coPiM I Mi) (space (coPiM I Mi)) = (iI. emeasure (Mi i) (space (Mi i)))"
  by(simp add: emeasure_coPiM_space)

lemma measure_coPiM_finite:
  assumes "finite I" "A  sets (coPiM I Mi)" "emeasure (coPiM I Mi) A < "
  shows "measure (coPiM I Mi) A = (iI. measure (Mi i) (Pair i -` A))"
  using assms(3) by(simp add: emeasure_coPiM_finite[OF assms(1,2)] measure_def enn2real_sum assms(1))

lemma nn_integral_coPiM_finite:
  assumes "finite I" "f  borel_measurable (coPiM I Mi)"
  shows "(+x. f x (coPiM I Mi)) = (iI. (+x. f (i, x) (Mi i)))"
  by(simp add: nn_integral_coPiM assms)

lemma integrable_coPiM_finite_iff:
  fixes f :: "_  'c::{banach, second_countable_topology}"
  shows "finite I  integrable (coPiM I Mi) f  (iI. integrable (Mi i) (λx. f (i, x)))"
  using measurable_copair_iff'[of f I Mi borel]
  by(auto simp: integrable_iff_bounded nn_integral_coPiM_finite)

lemma integral_coPiM_finite:
  fixes f :: "_  'c::{banach, second_countable_topology}"
  assumes "finite I" "integrable (coPiM I Mi) f"
  shows "(x. f x (coPiM I Mi)) = (iI. (x. f (i, x) (Mi i)))"
  by(auto simp: assms integral_coPiM)

subsection ‹ Countable Infinite Coproduct Measures ›
lemma emeasure_coPiM_countable_infinite:
  assumes [measurable]: "bij_betw from_n (UNIV :: nat set) I" "A  sets (coPiM I Mi)"
  shows "emeasure (coPiM I Mi) A = (n. emeasure (Mi (from_n n)) (Pair (from_n n) -` A))"
proof -
  have I:"countable I"
    using assms(1) countableI_bij by blast
  have [measurable,simp]:"Pair (from_n n) -` A  sets (Mi (from_n n))" "from_n n  I" for n
    using bij_betwE[OF assms(1)] by(auto intro!: measurable_Pair_vimage[where I=I])
  have "emeasure (coPiM I Mi) A = emeasure (coPiM I Mi) (n. {from_n n} × Pair (from_n n) -` A)"
    using sets.sets_into_space[OF assms(2)] assms(1)
    by(fastforce intro!: arg_cong[where f="emeasure (coPiM I Mi)"]
                   simp: space_coPiM  bij_betw_def)
  also have "... = (n. emeasure (Mi (from_n n)) (Pair (from_n n) -` A))"
    using injD[OF bij_betw_imp_inj_on[OF assms(1)]]
    by(subst suminf_emeasure[symmetric])
      (auto simp: disjoint_family_on_def emeasure_coPiM_coproj intro!: suminf_cong)
  finally show ?thesis .
qed

lemmas emeasure_coPiM_countable_infinite' = emeasure_coPiM_countable_infinite[OF bij_betw_from_nat_into]
lemmas emeasure_coPiM_nat = emeasure_coPiM_countable_infinite[OF bij_id,simplified]

lemma measure_coPiM_countable_infinite:
  assumes [measurable,simp]: "bij_betw from_n (UNIV :: nat set) I" "A  sets (coPiM I Mi)"
    and "emeasure (coPiM I Mi) A < "
  shows "measure (coPiM I Mi) A = (n. measure (Mi (from_n n)) (Pair (from_n n) -` A))" (is "?lhs = ?rhs")
    and "summable (λn. measure (Mi (from_n n)) (Pair (from_n n) -` A))"
proof -
  have "ennreal ?lhs = emeasure (coPiM I Mi) A"
    using assms(3) by(auto intro!: emeasure_eq_ennreal_measure[symmetric])
  also have "... = (n. emeasure (Mi (from_n n)) (Pair (from_n n) -` A))"
    by(simp add: emeasure_coPiM_countable_infinite)
  also have "... = (n. ennreal (measure (Mi (from_n n)) (Pair (from_n n) -` A)))"
    using assms(3) ennreal_suminf_lessD top.not_eq_extremum
    by(auto intro!: suminf_cong emeasure_eq_ennreal_measure
              simp: emeasure_coPiM_countable_infinite[OF assms(1)])
  finally have *:"ennreal ?lhs = (n. ennreal (measure (Mi (from_n n)) (Pair (from_n n) -` A)))" .
  thus **[simp]: "summable (λn. measure (Mi (from_n n)) (Pair (from_n n) -` A))"
    by(auto intro!: summable_suminf_not_top)
  show "?lhs = ?rhs"
  proof(subst ennreal_inj[symmetric])
    have "ennreal ?lhs = (n. ennreal (measure (Mi (from_n n)) (Pair (from_n n) -` A)))"
      by fact
    also have "... = ennreal ?rhs"
      using assms(3) by(auto intro!: suminf_ennreal2)
    finally show "ennreal ?lhs = ennreal ?rhs" .
  qed(simp_all add: suminf_nonneg)
qed

lemmas measure_coPiM_countable_infinite' = measure_coPiM_countable_infinite[OF bij_betw_from_nat_into]
lemmas measure_coPiM_nat = measure_coPiM_countable_infinite[OF bij_id,simplified id_apply]

lemma nn_integral_coPiM_countable_infinite:
  assumes [measurable]:"bij_betw from_n (UNIV :: nat set) I" "f  borel_measurable (coPiM I Mi)"
  shows "(+x. f x (coPiM I Mi)) = (n. (+x. f (from_n n, x) (Mi (from_n n))))" (is "_ = ?rhs")
proof -
  have "(+x. f x (coPiM I Mi)) = (iI. (+x. f (i, x) Mi i))"
    by(simp add: nn_integral_coPiM)
  also have "... = (ifrom_n ` UNIV. (+x. f (i, x) Mi i))"
    by(rule arg_cong[where f="infsum _"]) (metis assms(1) bij_betw_def)
  also have "... = (nUNIV. (+x. f (from_n n, x) (Mi (from_n n))))"
    by(rule infsum_reindex[simplified comp_def]) (use assms(1) bij_betw_imp_inj_on in blast)
  also have "... = ?rhs"
    by(auto intro!: infsum_eq_suminf nonneg_summable_on_complete)
  finally show ?thesis .
qed
lemmas nn_integral_coPiM_countable_infinite' = nn_integral_coPiM_countable_infinite[OF bij_betw_from_nat_into]
lemmas nn_integral_coPiM_nat = nn_integral_coPiM_countable_infinite[OF bij_id,simplified]

lemma 
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "bij_betw from_n (UNIV :: nat set) I" "integrable (coPiM I Mi) f"
  shows integrable_coPiM_countable_infinite_dest_sum:"(n. (+ x. norm (f (from_n n, x)) (Mi (from_n n)))) < "
    and integrable_coPiM_countable_infinite_dest': "n. integrable (Mi (from_n n)) (λx. f (from_n n, x))"
  using ennreal_suminf_lessD assms(1,2) bij_betwE[OF assms(1)]
  by(auto simp: integrable_iff_bounded nn_integral_coPiM_countable_infinite)

lemmas integrable_coPiM_countable_infinite_dest_sum' = integrable_coPiM_countable_infinite_dest_sum[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_countable_infinite_dest'' = integrable_coPiM_countable_infinite_dest'[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_nat_dest_sum = integrable_coPiM_countable_infinite_dest_sum[OF bij_id,simplified id_apply]
lemmas integrable_coPiM_nat_dest = integrable_coPiM_countable_infinite_dest'[OF bij_id,simplified id_apply]

lemma 
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "bij_betw from_n (UNIV :: nat set) I" "integrable (coPiM I Mi) f"
  shows integrable_coPiM_countable_infinite_summable_norm: "summable (λn. (x. norm (f (from_n n, x)) (Mi (from_n n))))"
    and integrable_coPiM_countable_infinite_summable_norm': "summable (λn. norm (x. f (from_n n, x) (Mi (from_n n))))"
    and integrable_coPiM_countable_infinite_summable: "summable (λn. (x. f (from_n n, x) (Mi (from_n n))))"
proof -
  show *:"summable (λn. (x. norm (f (from_n n, x)) (Mi (from_n n))))"
    using integrable_coPiM_countable_infinite_dest_sum[OF assms]
      nn_integral_eq_integral[OF integrable_norm[OF integrable_coPiM_countable_infinite_dest'[OF assms]]]
    by (auto intro!: summable_suminf_not_top)
  show "summable (λn. norm (x. f (from_n n, x) (Mi (from_n n))))"
    by(rule summable_comparison_test_ev[OF _ *]) auto
  thus "summable (λn. (x. f (from_n n, x) (Mi (from_n n))))"
    using summable_norm_cancel by force
qed

lemmas integrable_coPiM_countable_infinite_summable_norm''
  = integrable_coPiM_countable_infinite_summable_norm[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_countable_infinite_summable_norm'''
  = integrable_coPiM_countable_infinite_summable_norm'[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_countable_infinite_summable'
  = integrable_coPiM_countable_infinite_summable[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_nat_summable_norm
  = integrable_coPiM_countable_infinite_summable_norm[OF bij_id,simplified id_apply]
lemmas integrable_coPiM_nat_summable_norm'
  = integrable_coPiM_countable_infinite_summable_norm'[OF bij_id,simplified id_apply]
lemmas integrable_coPiM_nat_summable
  = integrable_coPiM_countable_infinite_summable[OF bij_id,simplified id_apply]

lemma
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "countable I" "infinite I" "integrable (coPiM I Mi) f"
  shows integrable_coPiM_countable_infinite_dest:"i. i  I  integrable (Mi i) (λx. f (i, x))"
  using integrable_coPiM_countable_infinite_dest'[OF bij_betw_from_nat_into[OF assms(1,2)] assms(3)]
  by (meson assms(1) countable_all)

lemma integrable_coPiM_countable_infiniteI:
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "bij_betw from_n (UNIV :: nat set) I" "i. i  I  (λx. f (i,x))  borel_measurable (Mi i)"
    and "(n. (+ x. norm (f (from_n n, x)) (Mi (from_n n)))) < "
  shows "integrable (coPiM I Mi) f"
  using nn_integral_coPiM_countable_infinite[OF assms(1),of _ Mi] assms(2,3)
  by(auto simp: measurable_copair_iff' integrable_iff_bounded)

lemmas integrable_coPiM_countable_infiniteI' = integrable_coPiM_countable_infiniteI[OF bij_betw_from_nat_into]
lemmas integrable_coPiM_natI = integrable_coPiM_countable_infiniteI[OF bij_id, simplified id_apply]

lemma integral_coPiM_countable_infinite:
  fixes f :: "_  'b::{banach, second_countable_topology}"
  assumes "bij_betw from_n (UNIV :: nat set) I" "integrable (coPiM I Mi) f"
  shows "(x. f x (coPiM I Mi)) = (n. (x. f (from_n n, x) (Mi (from_n n))))" (is "?lhs = ?rhs")
proof -
  have "?lhs = (iI. (x. f (i, x) Mi i))"
    by(simp add: integral_coPiM assms)
  also have "... = (ifrom_n ` UNIV. (x. f (i, x) Mi i))"
    by(rule arg_cong[where f="infsum _"]) (metis assms(1) bij_betw_def)
  also have "... = (nUNIV. (x. f (from_n n, x) (Mi (from_n n))))"
    by(rule infsum_reindex[simplified comp_def]) (use assms(1) bij_betw_imp_inj_on in blast)
  also have "... = ?rhs"
    by(auto intro!: infsum_eq_suminf norm_summable_imp_summable_on integrable_coPiM_countable_infinite_summable_norm' assms)
  finally show ?thesis .
qed

lemmas integral_coPiM_countable_infinite' = integral_coPiM_countable_infinite[OF bij_betw_from_nat_into]
lemmas integral_coPiM_nat = integral_coPiM_countable_infinite[OF bij_id,simplified id_apply]

subsection ‹ Finiteness ›
lemma finite_measure_coPiM:
  assumes "finite I" "i. i  I  finite_measure (Mi i)"
  shows "finite_measure (coPiM I Mi)"
  by(rule finite_measureI) (auto simp: emeasure_coPiM_finite finite_measure.emeasure_finite assms)

subsection ‹ $\sigma$-Finiteness ›
lemma sigma_finite_measure_coPiM:
  assumes "countable I" "i. i  I  sigma_finite_measure (Mi i)"
  shows "sigma_finite_measure (coPiM I Mi)"
proof
  have "A. range A  sets (Mi i)  (n. A n) = space (Mi i)  (n::nat. emeasure (Mi i) (A n)  )"
       if "i  I" for i
    using sigma_finite_measure.sigma_finite[OF assms(2)[OF that]] by metis
  hence "A. iI. range (A i)  sets (Mi i)  (n. A i n) = space (Mi i)  (n::nat. emeasure (Mi i) (A i n)  )"
    by metis
  then obtain Ai
    where Ai[measurable]: "i n. i  I  Ai i n  sets (Mi i)"
      "i. i  I  (n::nat. (Ai i n)) = space (Mi i)"
      "i n. i  I  emeasure (Mi i) (Ai i n)  "
    by (metis UNIV_I sets_range) 
  show "A. countable A  A  sets (coPiM I Mi)   A = space (coPiM I Mi)  (aA. emeasure (coPiM I Mi) a  )"
  proof(intro exI[where x="n. (i  I. {{i} × Ai i n})"] conjI ballI)
    show "countable (n. (i  I. {{i} × Ai i n}))"
      using assms(1) by auto
  next
    show "(n. iI. {{i} × Ai i n})  sets (coPiM I Mi)"
      by auto
  next
    show " (n. iI. {{i} × Ai i n}) = space (coPiM I Mi)"
      using sets.sets_into_space[OF Ai(1)] Ai(2) by(fastforce simp: space_coPiM)
  next
    fix a
    assume "a  (n. iI. {{i} × Ai i n})"
    then obtain n i where a: "i  I" "a = {i} × Ai i n"
      by blast
    show "emeasure (coPiM I Mi) a  "
      using a(1) Ai(3) assms by(auto simp: a(2) emeasure_coPiM_coproj)
  qed
qed

end