Theory Coproduct_Measure
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)) ∧ (∀i∈I. Pair i -` A ∈ sets (Mi i))}
(λA. (∑⇩∞i∈I. emeasure (Mi i) (Pair i -` A)))"
syntax
"_coPiM" :: "pttrn ⇒ 'i set ⇒ 'a measure ⇒ ('i × 'a) measure" ("(3⨿⇩M _∈_./ _)" 10)
translations
"⨿⇩M x∈I. 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)) ∧ (∀i∈I. Pair i -` A ∈ sets (Mi i))}"
and sets_coPiM_eq:"sets (coPiM I Mi) = {A. A⊆(SIGMA i:I. space (Mi i)) ∧ (∀i∈I. Pair i -` A ∈ sets (Mi i))}"
proof -
have 1:"{A. A⊆(SIGMA i:I. space (Mi i)) ∧ (∀i∈I. 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)) ∧ (∀i∈I. 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)) ∧ (∀i∈I. Pair i -` A ∈ sets (Mi i))}"
proof -
have "sigma_algebra (SIGMA i:I. space (Mi i)) {A. A ⊆ (SIGMA i:I. space (Mi i)) ∧ (∀i∈I. 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)) ∧ (∀i∈I. 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)) ∧ (∀i∈I. 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 ⟷ (∀i∈I. 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 ⟷ (∀i∈I. (λ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)) (⋃i∈I. (×) {i} ` (sets (Mi i)))"
unfolding sets_coPiM
proof(safe intro!: sigma_sets_eqI)
fix a
assume h:"a ⊆ (SIGMA i:I. space (Mi i))" "∀i∈I. Pair i -` a ∈ sets (Mi i)"
then have "a = (⋃i∈I. {i} × Pair i -` a)"
by auto
moreover have "(⋃i∈I. {i} × Pair i -` a) ∈ sigma_sets (SIGMA i:I. space (Mi i)) (⋃i∈I. (×) {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)) (⋃i∈I. (×) {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 = (∑⇩∞i∈I. emeasure (Mi i) (Pair i -` A))"
proof(rule emeasure_measure_of)
show "{A. A⊆(SIGMA i:I. space (Mi i)) ∧ (∀i∈I. 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. ∑⇩∞i∈I. 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. ∑⇩∞i∈I. emeasure (Mi i) (Pair i -` A n))
= (∑⇩∞i∈I. emeasure (Mi i) (Pair i -` ⋃ (range A)))" (is "?lhs = ?rhs")
proof -
have "?lhs = (∑⇩∞n∈UNIV. ∑⇩∞i∈I. emeasure (Mi i) (Pair i -` A n))"
by(auto intro!: infsum_eq_suminf[symmetric] nonneg_summable_on_complete)
also have "... = (∑⇩∞i∈I. ∑⇩∞n∈UNIV. 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)) = (∑⇩∞i∈I. 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) = (∑⇩∞j∈I. 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 "... = (∑⇩∞j∈I - {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 "(∑⇩∞j∈I - {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 *:"(∑⇩∞i∈I. 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 "(∑⇩∞i∈I. 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 = (∑⇩∞i∈I. measure (Mi i) (Pair i -` A))"
proof(subst ennreal_inj[symmetric])
have *:"(∑⇩∞i∈I. 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 (∑⇩∞i∈I. 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 "... = (∑⇩∞i∈I. emeasure (Mi i) (Pair i -` A))"
by(simp add: emeasure_coPiM)
also have "... = (∑⇩∞i∈I. 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) = (∑⇩∞i∈I. (∫⇧+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. (∑⇩∞i∈I. (∫⇧+ x. U j (i, x) ∂Mi i)))"
by(simp add: ih)
also have "... = (∑⇩∞i∈I. (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 "... = (∑⇩∞i∈I. (∫⇧+ 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:"(∑⇩∞i∈I. (∫⇧+ 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:"(∑⇩∞i∈I. (∫⇧+ 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) = (∑⇩∞i∈I. (∫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 = (∑⇩∞i∈I. (∫x. f (i, x) ∂Mi i)) + (∑⇩∞i∈I. (∫x. g (i, x) ∂Mi i))"
using h by simp
also have "... = (∑⇩∞i∈I. (∫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. (∑⇩∞i∈I. (∫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 = (∑i∈I. 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)) = (∑i∈I. 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 = (∑i∈I. 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)) = (∑i∈I. (∫⇧+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 ⟷ (∀i∈I. 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)) = (∑i∈I. (∫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)) = (∑⇩∞i∈I. (∫⇧+x. f (i, x) ∂Mi i))"
by(simp add: nn_integral_coPiM)
also have "... = (∑⇩∞i∈from_n ` UNIV. (∫⇧+x. f (i, x) ∂Mi i))"
by(rule arg_cong[where f="infsum _"]) (metis assms(1) bij_betw_def)
also have "... = (∑⇩∞n∈UNIV. (∫⇧+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 = (∑⇩∞i∈I. (∫x. f (i, x) ∂Mi i))"
by(simp add: integral_coPiM assms)
also have "... = (∑⇩∞i∈from_n ` UNIV. (∫x. f (i, x) ∂Mi i))"
by(rule arg_cong[where f="infsum _"]) (metis assms(1) bij_betw_def)
also have "... = (∑⇩∞n∈UNIV. (∫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. ∀i∈I. 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) ∧ (∀a∈A. 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. ⋃i∈I. {{i} × Ai i n}) ⊆ sets (coPiM I Mi)"
by auto
next
show "⋃ (⋃n. ⋃i∈I. {{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. ⋃i∈I. {{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