Theory Source_and_Sink_Algebras_Constructions
theory Source_and_Sink_Algebras_Constructions
imports
"HOL-Analysis.Finite_Product_Measure"
"Source_and_Sink_Algebras"
"Measurable_Isomorphism"
begin
section ‹ Basic measurable sapces defined with initial and final lifts ›
subsection ‹ Another form of product ‹σ›-algebra ›
text ‹ We here introduce another form of product ‹σ›-algebra. The initial lift induced by projections has the same ‹σ›-algebra as @{term PiM} in the standard library, but ours are more suitable for categorical semantics of probabilistic programs. ›
definition prod_initial_source :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i ⇒ 'a) measure"where
"prod_initial_source I M = initial_source (Π⇩E i∈I. space (M i)) ({((λ f. f i),M i) |i. i ∈ I})"
syntax
"_prod_initial_source":: "pttrn ⇒'i set ⇒ ('i ⇒ 'a set) ⇒ ('i × 'a) set"("(3Π⇩S _∈_./ _)"10)
translations
"Π⇩S x∈A. B"⇌"CONST prod_initial_source A (λx. B)"
lemma space_prod_initial_source:
"space (Π⇩S i∈I. (M i)) = (Π⇩E i∈I. space (M i))"
by (auto simp: prod_initial_source_def)
lemma PiM_is_initial_source_nonempty_sets:
assumes "I ≠ {}"
shows "sets (PiM I M) = sets(prod_initial_source I M)"
unfolding prod_initial_source_def initial_source_def
proof(subst sets_PiM_eq_proj, unfold vimage_algebra_def)
show "sets (SUP i∈I. sigma (Π⇩E i∈I. space (M i)) {(λx. x i) -` A ∩ (Π⇩E i∈I. space (M i)) |A. A ∈ sets (M i)}) =
sets
(sigma (Π⇩E i∈I. space (M i))
{B. ∃A f N. B = f -` A ∩ (Π⇩E i∈I. space (M i)) ∧ (f, N) ∈ {(λf. f i, M i) |i. i ∈ I} ∧ A ∈ sets N})"
proof(subst SUP_sigma_sigma)
show "sets (sigma (Π⇩E i∈I. space (M i)) (⋃m∈I. {(λx. x m) -` A ∩ (Π⇩E i∈I. space (M i)) |A. A ∈ sets (M m)}))
= sets (sigma (Π⇩E i∈I. space (M i)) {B. ∃A f N. B = f -` A ∩ (Π⇩E i∈I. space (M i)) ∧ (f, N) ∈ {(λf. f i, M i) |i. i ∈ I} ∧ A ∈ sets N})"
proof(subst sets_measure_of)
show "sigma_sets (Π⇩E i∈I. space (M i)) (⋃m∈I. {(λx. x m) -` A ∩ (Π⇩E i∈I. space (M i)) |A. A ∈ sets (M m)})
= sets (sigma (Π⇩E i∈I. space (M i)) {B. ∃A f N. B = f -` A ∩ (Π⇩E i∈I. space (M i)) ∧ (f, N) ∈ {(λf. f i, M i) |i. i ∈ I} ∧ A ∈ sets N})"
proof(subst sets_measure_of)
show "sigma_sets (Π⇩E i∈I. space (M i)) (⋃m∈I. {(λx. x m) -` A ∩ (Π⇩E i∈I. space (M i)) |A. A ∈ sets (M m)})
= sigma_sets (Π⇩E i∈I. space (M i)) {B. ∃A f N. B = f -` A ∩ (Π⇩E i∈I. space (M i)) ∧ (f, N) ∈ {(λf. f i, M i) |i. i ∈ I} ∧ A ∈ sets N}"
by(rule sigma_sets_eqI,blast,blast)
qed(auto)
qed(auto)
qed(auto simp add: assms)
qed(auto simp add: assms)
lemma PiM_is_initial_source_nonempty_space:
assumes "I ≠ {}"
shows "space (PiM I M) = space(prod_initial_source I M)"
by (meson assms PiM_is_initial_source_nonempty_sets sets_eq_imp_space_eq)
lemma
shows PiM_is_initial_source_empty_space: "space(prod_initial_source {} M) = {λk. undefined}"
and PiM_is_initial_source_empty_sets: "sets(prod_initial_source {} M) = {{}, {λk. undefined}}"
proof
show s1: "space (prod_initial_source {} M) ⊆ {λk. undefined}"
by (auto simp add: prod_initial_source_def)
show s2: "{λk. undefined} ⊆ space (prod_initial_source {} M)"
by (auto simp add: prod_initial_source_def)
show "sets (prod_initial_source {} M) = {{}, {λk. undefined}}"
proof
show "sets (prod_initial_source {} M) ⊆ {{}, {λk. undefined}}"
by (metis s1 s2 insertCI sets.sets_into_space subsetI subset_antisym subset_singletonD)
show "sets (prod_initial_source {} M) ⊇ {{}, {λk. undefined}}"
by (metis empty_subsetI insert_subsetI s1 s2 sets.empty_sets sets.top subset_antisym)
qed
qed
proposition PiM_is_initial_source:
shows "space (PiM I M) = space (prod_initial_source I M)"
and "sets (PiM I M) = sets (prod_initial_source I M)"
proof-
show "sets (PiM I M) = sets (prod_initial_source I M)"
proof(cases"I={}")
case True
thus ?thesis using PiM_is_initial_source_empty_sets sets_PiM_empty by metis
next
case False
thus ?thesis using PiM_is_initial_source_nonempty_sets by metis
qed
thus "space (PiM I M) = space (prod_initial_source I M)"
using sets_eq_imp_space_eq by auto
qed
lemma measurable_prod_initial_sourceI:
assumes space: "f ∈ space N → (Π⇩E i∈I. space (M i))"
and measurability: "⋀ i. i ∈ I ⟹ (λ x . f x i) ∈ N →⇩M M i"
shows "f ∈ N →⇩M prod_initial_source I M"
by(unfold prod_initial_source_def, rule measurable_initial_source2, auto simp add: space intro: measurability)
lemma measurable_prod_initial_source_projections [measurable(raw)]:
assumes "i ∈ I"
shows "(λf. f i) ∈ (Π⇩S i∈I. (M i)) →⇩M (M i)"
by(unfold prod_initial_source_def PiE_def, intro measurable_initial_source1,auto intro: assms)
subsubsection‹decomposition of countable product›
lemma measurable_projection_shift:
shows "(λx n. x (Suc n)) ∈ (Π⇩S i∈{..<Suc n}. M) →⇩M (Π⇩S i∈{..<n}. M)"
by(induction n)(rule measurable_prod_initial_sourceI,auto simp:space_prod_initial_source)+
lemma measurable_decompose_prod_initial_source_Suc_n:
shows "(λ f. (f 0, (λ n. f (Suc n)))) ∈ (Π⇩S i∈{..<Suc n}. M) →⇩M (M ⨂⇩M (Π⇩S i∈{..< n}. M))"
by(rule measurable_Pair,auto simp: measurable_projection_shift)
lemma measurable_integrate_prod_initial_source_Suc_n:
shows "(λp. (λ n. if n = 0 then (fst p) else (snd p)(n - 1))) ∈ (M ⨂⇩M (Π⇩S i∈{..< n}. M)) →⇩M (Π⇩S i∈{..<Suc n}. M)"
proof(rule measurable_prod_initial_sourceI)
show "(λp n. if n = 0 then fst p else snd p (n - 1)) ∈ space (M ⨂⇩M (Π⇩S i∈{..<n}. M)) → {..<Suc n} →⇩E space M"
unfolding space_pair_measure space_prod_initial_source PiE_def extensional_def Pi_def by auto
fix i assume i: "i ∈ {..<Suc n}"
show "(λx. if i = 0 then fst x else snd x (i - 1)) ∈ M ⨂⇩M (Π⇩S i∈{..<n}. M) →⇩M M"
proof(cases"i = 0")
case True
thus ?thesis by auto
next
case False
from i False have 1: "(i - 1) ∈ {..<n}"
by auto
from False have "(λx. if i = 0 then fst x else snd x (i - 1)) = (λf. f(i - 1)) o snd"
by auto
also have "... ∈ M ⨂⇩M (Π⇩S i∈{..<n}. M) →⇩M M"
using 1 by measurable
finally show ?thesis .
qed
qed
proposition measurable_iff_prod_initial_source:
shows integrate_prod_initial_source_iff:
"⋀ f . (f ∈ (M ⨂⇩M (Π⇩S i∈{..< n}. M)) →⇩M N) ⟷ (f o (λ f. (f 0, (λ n. f (Suc n))))) ∈ ((Π⇩S i∈{..<Suc n}. M) →⇩M N)"
and decompose_prod_initial_source_iff:
"⋀ f . (f ∈ (Π⇩S i∈{..<Suc n}. M) →⇩M N) ⟷ (f o (λp. (λ n. if n = 0 then (fst p) else (snd p)(n - 1))) ∈ (M ⨂⇩M (Π⇩S i∈{..< n}. M)) →⇩M N)"
proof-
have A: "∀x∈space (Π⇩S i∈{..<Suc n}. M). (λn. if n = 0 then fst (x 0, λn. x (Suc n)) else snd (x 0, λn. x (Suc n)) (n - 1)) = x"
and B: "∀y∈space (M ⨂⇩M (Π⇩S i∈{..<n}. M)). (if 0 = 0 then fst y else snd y (0 - 1), λn. if Suc n = 0 then fst y else snd y (Suc n - 1)) = y"
by auto
show "⋀ f . (f ∈ (M ⨂⇩M (Π⇩S i∈{..< n}. M)) →⇩M N) ⟷ (f o (λ f. (f 0, (λ n. f (Suc n))))) ∈ ((Π⇩S i∈{..<Suc n}. M) →⇩M N)"
and "⋀ f . (f ∈ (Π⇩S i∈{..<Suc n}. M) →⇩M N) ⟷ (f o (λp. (λ n. if n = 0 then (fst p) else (snd p)(n - 1))) ∈ (M ⨂⇩M (Π⇩S i∈{..< n}. M)) →⇩M N)"
using
measurable_isomorphism_iff(1,2)[of"(λ f. (f 0, (λ n. f (Suc n))))"_ _"(λp. (λ n. if n = 0 then (fst p) else (snd p)(n - 1)))"_ N , OF measurable_decompose_prod_initial_source_Suc_n measurable_integrate_prod_initial_source_Suc_n A B]
by auto
qed
subsection ‹ (Infinite) coproduct (disjoint union, direct sum) space ›
text ‹ We here introduce coproduct ‹σ›-algebra as the final lift induced by coprojections. We first recall coprojections and copairs, and then we define coproduct space. ›
subsubsection ‹ Coprojections and Cotuples ›
text ‹ We want to distinguish the usage of @{term "Pair"} for the coprojections from the pairing for binary product. ›
definition
"coProj ≡ Pair"
lemma coProj_function:
assumes "i ∈ I"
shows "coProj i ∈ A i → (SIGMA i:I. A i)"
by (auto simp: assms Sigma_def coProj_def)
definition coTuple :: "'i set ⇒ ('i ⇒ 'a set) ⇒ ('i ⇒ ('a ⇒ 'b)) ⇒ ('i × 'a ⇒ 'b)"where
"coTuple I A F = (λ (i,a). F i a)"
lemma coTuple_function:
assumes "∀ i ∈ I. F i ∈ A i → B"
shows "coTuple I A F ∈ (SIGMA i:I. A i) → B"
unfolding coTuple_def Sigma_def using assms by auto
lemma coTuple_eqI:
assumes "∀ i ∈ I. F i ∈ A i → C"
and "∀ i ∈ I. (∀a ∈ (A i). F i a = G i a)"
shows "∀(i,a) ∈ (SIGMA i:I. A i). coTuple I A F (i,a) = coTuple I A G (i,a)"
unfolding coTuple_def Sigma_def using assms by auto
lemma coProj_coTuple:
assumes "i ∈ I"
shows "coTuple I A F o coProj i = F i"
unfolding coTuple_def coProj_def by auto
lemma coTuple_unique:
assumes "g ∈ (SIGMA i:I. A i) → B"
shows "∀ (i,a) ∈ (SIGMA i:I. A i). g(i,a) = (coTuple I A (λ j ∈ I. (g o coProj j)))(i,a)"
by (auto simp: coTuple_def coProj_def Sigma_def)
subsubsection ‹ Coproduct ‹σ›-algebra defined as the final lift ›
definition coprod_final_sink :: "'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i × 'a) measure"where
"coprod_final_sink I M = final_sink (SIGMA i:I. space (M i)) ({(coProj i,M i) |i. i ∈ I})"
syntax
"_coprod_final_sink":: "pttrn ⇒'i set ⇒ ('i ⇒ 'a measure) ⇒ ('i × 'a) measure"("(3⨿⇩M _∈_./ _)"10)
translations
"⨿⇩M i∈I. M"⇌"CONST coprod_final_sink I (λi. M)"
lemma coProj_measurable[measurable]:
assumes "i ∈ I"
shows "coProj i ∈ M i →⇩M (⨿⇩M i∈I. M i)"
unfolding coprod_final_sink_def
proof(rule measurable_final_sink1)
show "∀(g, N)∈{(coProj i, M i) |i. i ∈ I}. g ∈ space N → (SIGMA i:I. space (M i))"
using coProj_function by force
show "(coProj i, M i) ∈ {(coProj i, M i) |i. i ∈ I}"
using assms by auto
qed
lemma coTuple_measurable [measurable(raw)]:
assumes "∀ i ∈ I. F i ∈ (M i) →⇩M N"
shows "coTuple I (λ i. space (M i)) F ∈ (⨿⇩M i∈I. M i) →⇩M N"
unfolding coprod_final_sink_def
proof(rule measurable_final_sink2)
show "coTuple I (λi. space (M i)) F ∈ (SIGMA i:I. space (M i)) → space N"
using assms by(auto simp: coTuple_function measurable_iff_sets)
show "∀(g, N)∈{(coProj i, M i) |i. i ∈ I}. g ∈ space N → (SIGMA i:I. space (M i))"
using coProj_function by (auto simp add: Sigma_def coProj_def)
show "∀(g, K)∈{(coProj i, M i) |i. i ∈ I}. (λx. coTuple I (λi. space (M i)) F (g x)) ∈ K →⇩M N"
using assms by (auto simp add: coTuple_def coProj_def)
qed
proposition coprod_measurable_iff:
shows "⋀ f. (f ∈ (⨿⇩M i∈I. M i) →⇩M N) ⟷ (∀ i∈ I. (f o coProj i) ∈ M i →⇩M N)"
proof
fix f assume f1: "f ∈ coprod_final_sink I M →⇩M N"
thus"∀i∈I. f ∘ coProj i ∈ M i →⇩M N"
using f1 coProj_measurable by auto
next fix f assume f2: "∀i∈I. f ∘ coProj i ∈ M i →⇩M N"
hence *: "(coTuple I (λ i. space (M i)) (λ i ∈ I. (f ∘ coProj i))) ∈ coprod_final_sink I M →⇩M N"
by auto
have "∀ (n,h) ∈ space (⨿⇩M i∈I. M i). f (n,h) = coTuple I (λ i. space (M i)) (λ i ∈ I. (f ∘ coProj i)) (n,h)"
unfolding coprod_final_sink_def space_final_sink
by(rule coTuple_unique, auto)
with * show "f ∈ coprod_final_sink I M →⇩M N"
using measurable_cong_simp by fastforce
qed
lemma space_coprod_final_sink:
shows "space (coprod_final_sink I M) = (SIGMA i:I. space (M i))"
by(auto simp: coprod_final_sink_def)
lemma sets_coprod_final_sink_gen:
shows "i ∈ I ⟹ A ∈ sets (M i) ⟹ j ∈ I ⟹coProj j -` ({i} × A) ∩ space (M j) ∈ sets (M j)"
by(cases"j = i",auto simp: coProj_def)
lemma sets_coprod_final_sink_section[measurable(raw)]:
shows "i ∈ I ⟹ A ∈ sets (M i) ⟹({i} × A) ∈ sets (coprod_final_sink I M)"
proof
fix i A assume i: "i ∈ I"and Ai: "A ∈ sets (M i)"
hence "A ⊆ space (M i)"
by (auto simp: sets.sets_into_space)
hence cond1: "{i} × A ∈ Pow (SIGMA i:I. space (M i))"
unfolding Sigma_def using i by auto
from sets_coprod_final_sink_gen[of i I A M,OF i,OF Ai] have
cond2: "(∀(g, N)∈{(coProj i, M i) |i. i ∈ I}. g -` ({i} × A) ∩ space N ∈ sets N)"
by blast
from cond1 cond2 show "{i} × A ∈ sets (coprod_final_sink I M)"
unfolding coprod_final_sink_def sets_final_sink by auto
qed(auto)
lemma sets_coprod_final_sink_partition:
assumes A: "A ∈ sets (coprod_final_sink I M)"
shows "(∀ i ∈ I. {c | c. (i,c) ∈ A ∧ c ∈ space (M i)} ∈ sets (M i))"
and "A = ⋃ ((λ i. {i} × {c | c. (i,c) ∈ A ∧ c ∈ space (M i)}) ` I)"
proof
fix i assume i: "i ∈ I"
have "{c |c. (i, c) ∈ A ∧ c ∈ space (M i)} = coProj i -` A ∩ space (M i)"
by (auto simp: Collect_conj_eq vimage_def coProj_def)
also have "...∈ sets (M i)"
by (meson assms coProj_measurable i measurable_sets)
finally show "{c |c. (i, c) ∈ A ∧ c ∈ space (M i)} ∈ sets (M i)".
next
have "A ⊆ space (coprod_final_sink I M)"
using A sets.sets_into_space by blast
also have "... = {(i,c) |i c. i ∈ I ∧ c ∈ space (M i)}"
unfolding coprod_final_sink_def space_final_sink
by (auto simp add: Sigma_def)
finally have "A ⊆ {(i,c) |i c. i ∈ I ∧ c ∈ space (M i)}".
thus"A = ⋃ ((λ i. {i} × {c | c. (i,c) ∈ A ∧ c ∈ space (M i)}) ` I)"
by auto
qed
proposition sets_coprod_final_sink:
assumes I: "countable I"
shows "sets (coprod_final_sink I M) = sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
proof
show "sets (coprod_final_sink I M) ⊆ sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
proof
fix A assume "A ∈ sets (coprod_final_sink I M)"
hence measAi: "(∀ i ∈ I. {c | c. (i,c) ∈ A ∧ c ∈ space (M i)} ∈ sets (M i))"
and UnionAi: "A = ⋃ ((λ i. {i} × {c | c. (i,c) ∈ A ∧ c ∈ space (M i)}) ` I)"
using sets_coprod_final_sink_partition [of A I M] by auto
have measUnionAi: "⋃ ((λ i. {i} × {c | c. (i,c) ∈ A ∧ c ∈ space (M i)}) ` I) ∈ sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
proof(intro sigma_sets_UNION)
show "countable ((λi. {i} × {c |c. (i, c) ∈ A ∧ c ∈ space (M i)}) ` I)"
using I by blast
fix B assume "B ∈ (λi. {i} × {c |c. (i, c) ∈ A ∧ c ∈ space (M i)}) ` I"
then obtain i where Bi: "i ∈ I ∧ B = {i} × {c |c. (i, c) ∈ A ∧ c ∈ space (M i)}"
by auto
with measAi have "{i} × {c |c. (i, c) ∈ A ∧ c ∈ space (M i)} ∈ {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
by auto
with Bi have "B ∈ {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
by auto
thus"B ∈ sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
by (meson sigma_sets.Basic)
qed
with UnionAi show "A ∈ sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)}"
by auto
qed
show "sigma_sets (SIGMA i:I. space (M i)) {{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)} ⊆ sets (coprod_final_sink I M)"
proof(intro sigma_algebra.sigma_sets_subset)
show "sigma_algebra (SIGMA i:I. space (M i)) (sets (coprod_final_sink I M))"
unfolding coprod_final_sink_def sets_final_sink
by (auto simp: sigma_algebra_sigma_sets subset_iff)
{
fix i A assume i: "i ∈ I"and Ai: "A ∈ sets(M i)"
note sets_coprod_final_sink_section[of i I A M, OF i Ai]
}
thus"{{i} × A |i A. i ∈ I ∧ A ∈ sets (M i)} ⊆ sets (coprod_final_sink I M)"
by auto
qed
qed
subsubsection ‹ Distributive laws between binary products and countable coproducts›
text‹ We here formalize the distributive laws between binary products and countable coproducts, that is, the measurable isomorphisms between @{term"(⨿⇩M i∈I. (M ⨂⇩M N i))"} and @{term"M ⨂⇩M (⨿⇩M i∈I. N i)"}›
definition dist_law_A :: "'i set ⇒ ('i ⇒ 'b measure) ⇒ 'a measure ⇒ 'i × 'a × 'b ⇒ 'a × 'i × 'b"where
"dist_law_A I N M =
(coTuple I (λi. space M × space (N i)) (λi. λ p. ((fst p), coProj i (snd p))))"
proposition dist_law_A_measurable[measurable]:
shows "dist_law_A I N M ∈ (⨿⇩M i∈I. M ⨂⇩M N i) →⇩M (M ⨂⇩M (⨿⇩M i∈I. N i))"
unfolding dist_law_A_def space_pair_measure[THEN sym]
by auto
lemma dist_law_A_def2:
shows "dist_law_A I N M = (λ p. ((fst (snd p)), ((fst p) ,(snd (snd p)))))"
unfolding coTuple_def dist_law_A_def coProj_def
by auto
lemma dist_law_A_vimage:
shows "dist_law_A I N M -` space (M ⨂⇩M (⨿⇩M i∈I. N i)) = (space (⨿⇩M i∈I. (M ⨂⇩M N i)))"
unfolding dist_law_A_def2 coprod_final_sink_def space_pair_measure space_final_sink Sigma_def
by auto
definition dist_law_B :: "'i set ⇒ ('i ⇒ 'b measure) ⇒ 'a measure ⇒ 'a × 'i × 'b ⇒ 'i × 'a × 'b"where
"dist_law_B I N M = (λ p. ((fst (snd p)), ((fst p) ,(snd (snd p)))))"
lemma dist_law_B_function:
shows "dist_law_B I N M ∈ space (M ⨂⇩M (⨿⇩M i∈I. N i)) → space (⨿⇩M i∈I. (M ⨂⇩M N i))"
unfolding space_pair_measure coprod_final_sink_def space_final_sink Sigma_def dist_law_B_def
by auto
lemma dist_law_B_vimage:
shows "dist_law_B I N M -` (space (⨿⇩M i∈I. (M ⨂⇩M N i))) = space (M ⨂⇩M (⨿⇩M i∈I. N i))"
unfolding space_pair_measure coprod_final_sink_def space_final_sink Sigma_def dist_law_B_def
by auto
lemma dist_laws_mutually_inverse:
shows "⋀x. (dist_law_A I N M o dist_law_B I N M) x = x"
and "⋀y. (dist_law_B I N M o dist_law_A I N M) y = y"
unfolding dist_law_B_def
by(auto simp add:dist_law_A_def2)
lemma sets_generator_product_of_M_and_coprodNi:
assumes I: "countable I"
shows "sets (M ⨂⇩M (⨿⇩M i∈I. N i)) = sigma_sets (space (M ⨂⇩M (⨿⇩M i∈I. N i))) {A × ({i} × B) | A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)}"
proof
have "{A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)} ⊆ sets (M ⨂⇩M coprod_final_sink I N)"
proof(clarify)
fix A i B assume "A ∈ sets M""i ∈ I""B ∈ sets (N i)"
hence "A ∈ sets M""{i} × B ∈ sets (coprod_final_sink I N)"
using sets_coprod_final_sink_section by auto
thus"A × {i} × B ∈ sets (M ⨂⇩M coprod_final_sink I N)"
by auto
qed
thus"sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)} ⊆ sets (M ⨂⇩M coprod_final_sink I N)"
by (auto simp: sets.sigma_sets_subset)
show "sets (M ⨂⇩M coprod_final_sink I N) ⊆ sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof
{
fix C assume "C ∈ sigma_sets (space M × space (coprod_final_sink I N)){A × D | A D . A ∈ sets M ∧ D ∈ sets (coprod_final_sink I N)}"
hence "C ∈ sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof(induction C)
case (Basic a)
then obtain A D where *: "a = A × D ∧ A ∈ sets M ∧ D ∈ sets (coprod_final_sink I N)"
by auto
hence measDi: "(∀ i ∈ I. {c | c. (i,c) ∈ D ∧ c ∈ space (N i)} ∈ sets (N i))"
using sets_coprod_final_sink_partition(1) by force
from * have unionDi: "D = ⋃ ((λ i. {i} × {c | c. (i,c) ∈ D ∧ c ∈ space (N i)}) ` I)"
using sets_coprod_final_sink_partition(2) by force
with * have "a = ⋃ ((λ i. A × ({i} × {c | c. (i,c) ∈ D ∧ c ∈ space (N i)}))` I)"
by(auto intro: set_eqI)
also have "... ∈ sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof(intro sigma_sets_UNION)
show "countable ((λi. A × {i} × {c |c. (i, c) ∈ D ∧ c ∈ space (N i)}) ` I)"
using I by blast
show "⋀C. C ∈ (λi. A × {i} × {c |c. (i, c) ∈ D ∧ c ∈ space (N i)}) ` I ⟹ C ∈ sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
using measDi * by blast
qed
finally show ?case.
next
case Empty
thus ?case
using sigma_sets.Empty by auto
next
case (Compl a)
thus ?case
unfolding space_pair_measure
using sigma_sets.Compl by blast
next
case (Union a)
thus ?case
unfolding space_pair_measure
using sigma_sets.Union by blast
qed
}
thus "⋀x. x ∈ sets (M ⨂⇩M coprod_final_sink I N) ⟹ x ∈ sigma_sets (space (M ⨂⇩M coprod_final_sink I N)) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
unfolding sets_pair_measure by auto
qed
qed
lemma sets_generator_coproduct_of_prod_M_Ni:
assumes I: "countable I"
shows "sets (⨿⇩M i∈I. (M ⨂⇩M N i)) = sigma_sets (space (⨿⇩M i∈I. (M ⨂⇩M N i))) {{i} × (A × B) | A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)}"
proof
have "{{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)} ⊆ sets (⨿⇩M i∈I. M ⨂⇩M N i)"
proof(clarify)
fix A i B assume "A ∈ sets M""i ∈ I""B ∈ sets (N i)"
thus"{i} × A × B ∈ sets (⨿⇩M i∈I. M ⨂⇩M N i)"
by (auto simp: sets_coprod_final_sink_section)
qed
thus"sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)} ⊆ sets (⨿⇩M i∈I. M ⨂⇩M N i)"
by (meson sets.sigma_sets_subset)
{
fix i assume i: "i ∈ I"
fix D assume Di: "D ∈ sigma_sets (space (M ⨂⇩M N i)) {A × B | A B. A ∈ sets M ∧ B ∈ sets (N i)}"
hence "{i} × D ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof(induction D)
case (Basic a)
thus ?case
using i by auto
next
case Empty
thus ?case
using sigma_sets.Empty by auto
next
case (Compl a)
hence "{i} × (space (M ⨂⇩M N i) - a) = ({i} × (space (M ⨂⇩M N i))) - ({i} × a)"
by blast
also have "... ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof(intro ring_of_sets.Diff)
have "sigma_algebra (space (⨿⇩M i∈I. M ⨂⇩M N i)) (sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)})"
unfolding space_pair_measure coprod_final_sink_def space_final_sink
proof(intro sigma_algebra_sigma_sets subsetI)
fix W assume "W ∈ {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
then obtain A i B where *: "W = {i} × A × B ∧A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)"
by blast
hence "W ⊆ {(i, a) |i a. i ∈ I ∧ a ∈ space M × space (N i)}"
proof(intro subsetI)
{
fix i a b assume W: "(i,a,b) ∈ W"
hence "(a ∈ A) ∧ (i ∈ I) ∧ (b ∈ B)"
using * by auto
hence "(a ∈ space M) ∧ (i ∈ I) ∧ (b ∈ space (N i))"
using * by (metis SigmaD1 W sets.sets_into_space singletonD subsetD)
hence "(i,a,b) ∈{(i, a) |i a. i ∈ I ∧ a ∈ space M × space (N i)}"
by auto
}
thus"⋀x. x ∈ W ⟹ x ∈ {(i, a) |i a. i ∈ I ∧ a ∈ space M × space (N i)}"
by auto
qed
thus"W ∈ Pow (SIGMA i:I. space M × space (N i))"
by auto
qed
thus"ring_of_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) (sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)})"
using algebra.axioms(1) sigma_algebra_def by blast
show "{i} × space (M ⨂⇩M N i) ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
unfolding space_pair_measure using i by blast
show "{i} × a ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
using local.Compl by blast
qed
finally show ?case.
next
case (Union a)
have "{i} × ⋃ (range a) = ⋃ (range (λ n :: nat. {i} × (a n)))"
by auto
also have "... ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
using sigma_sets.Union local.Union
by (auto simp: sigma_sets.Union local.Union)
finally show ?case .
qed
}
hence "∀ i ∈ I. ∀ D ∈ sigma_sets (space (M ⨂⇩M N i)) {A × B |A B. A ∈ sets M ∧ B ∈ sets (N i)}. {i} × D
∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
by auto
hence "{{i} × D |i D. i ∈ I ∧ D ∈ sets (M ⨂⇩M N i)} ⊆ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
unfolding sets_pair_measure space_pair_measure by auto
hence eq: "sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × D |i D. i ∈ I ∧ D ∈ sets (M ⨂⇩M N i)} ⊆ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
by (auto simp: sigma_sets_mono)
have eq2: "sets (⨿⇩M i∈I. M ⨂⇩M N i) = sigma_sets (SIGMA i:I. space (M ⨂⇩M N i)) {{i} × D |i D. i ∈ I ∧ D ∈ sets (M ⨂⇩M N i)}"
by(intro sets_coprod_final_sink I)
from eq eq2 show "sets (⨿⇩M i∈I. M ⨂⇩M N i) ⊆ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
unfolding coprod_final_sink_def space_final_sink by auto
qed
proposition dist_law_B_measurable [measurable(raw)]:
assumes I: "countable I"
shows "dist_law_B I N M ∈ (M ⨂⇩M (⨿⇩M i∈I. N i)) →⇩M (⨿⇩M i∈I. (M ⨂⇩M N i))"
proof(rule measurableI)
show "⋀x. x ∈ space (M ⨂⇩M coprod_final_sink I N) ⟹ dist_law_B I N M x ∈ space (⨿⇩M i∈I. M ⨂⇩M N i)"
unfolding space_pair_measure coprod_final_sink_def space_final_sink Sigma_def dist_law_B_def
by auto
show "⋀A. A ∈ sets (⨿⇩M i∈I. M ⨂⇩M N i) ⟹ dist_law_B I N M -` A ∩ space (M ⨂⇩M coprod_final_sink I N) ∈ sets (M ⨂⇩M coprod_final_sink I N)"
proof
have "⋀ A i B. (A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)) ⟹ dist_law_B I N M -` ({i} × (A × B)) = A × {i} × B"
unfolding dist_law_B_def by auto
hence "⋀D. D ∈ {{i} × (A × B) | A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)} ⟹ dist_law_B I N M -` D ∈ {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
by blast
hence baseD: "⋀D. D ∈ {{i} × (A × B) | A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)} ⟹ dist_law_B I N M -` D ∈ sigma_sets (space (M ⨂⇩M (⨿⇩M i∈I. N i))) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
by auto
have Dgen: "⋀D. D ∈ sigma_sets (space ((⨿⇩M i∈I. M ⨂⇩M N i))) {{i} × (A × B) | A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets(N i)} ⟹ (dist_law_B I N M -` D) ∈ sigma_sets (space (M ⨂⇩M (⨿⇩M i∈I. N i))) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof-
fix D assume D: "D ∈ sigma_sets (space (⨿⇩M i∈I. M ⨂⇩M N i)) {{i} × A × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
thus"dist_law_B I N M -` D ∈ sigma_sets (space (M ⨂⇩M (⨿⇩M i∈I. N i))) {A × {i} × B |A i B. A ∈ sets M ∧ i ∈ I ∧ B ∈ sets (N i)}"
proof(induct)
case (Basic a)
thus ?case using baseD by auto
next
case Empty
thus ?case using sigma_sets.Empty by auto
next
case (Compl a)
have "dist_law_B I N M -` (space (⨿⇩M i∈I. M ⨂⇩M N i) - a) = (space (M ⨂⇩M (⨿⇩M i∈I. N i)))- (dist_law_B I N M -` a)"
using dist_law_B_vimage by blast
thus ?case
by (metis (mono_tags, lifting) Compl.hyps(2) sigma_sets.Compl)
next
case (Union a)
have "(dist_law_B I N M -` ⋃ (range a)) = (⋃ i :: nat. (dist_law_B I N M -` (a i)))"
by auto
thus ?case
by (metis (mono_tags, lifting) sigma_sets.Union local.Union(2))
qed
qed
show "⋀A. A ∈ sets (⨿⇩M i∈I. M ⨂⇩M N i) ⟹ dist_law_B I N M -` A ∈ sets (M ⨂⇩M coprod_final_sink I N)"
using sets_generator_product_of_M_and_coprodNi[of I M N, OF I] sets_generator_coproduct_of_prod_M_Ni[of I M N, OF I] Dgen
by blast
qed(auto)
qed
proposition measurable_iff_dist_laws:
assumes I: "countable I"
shows measurable_iff_dist_law_A: "⋀f. (f ∈ (M ⨂⇩M (⨿⇩M i∈I. N i)) →⇩M K) ⟷ ((f o dist_law_A I N M) ∈ (⨿⇩M i∈I. (M ⨂⇩M N i)) →⇩M K)"
and measurable_iff_dist_law_B: "⋀f. (f ∈ (⨿⇩M i∈I. (M ⨂⇩M N i)) →⇩M K) ⟷ ((f o dist_law_B I N M) ∈ (M ⨂⇩M (⨿⇩M i∈I. N i)) →⇩M K)"
proof-
have A: "∀x∈space (⨿⇩M i∈I. M ⨂⇩M N i). dist_law_B I N M (dist_law_A I N M x) = x"
and B: "∀y∈space (M ⨂⇩M coprod_final_sink I N). dist_law_A I N M (dist_law_B I N M y) = y"
using dist_laws_mutually_inverse by auto
show "⋀f. (f ∈ (M ⨂⇩M (⨿⇩M i∈I. N i)) →⇩M K) ⟷ ((f o dist_law_A I N M) ∈ (⨿⇩M i∈I. (M ⨂⇩M N i)) →⇩M K)"
and "⋀f. (f ∈ (⨿⇩M i∈I. (M ⨂⇩M N i)) →⇩M K) ⟷ ((f o dist_law_B I N M) ∈ (M ⨂⇩M (⨿⇩M i∈I. N i)) →⇩M K)"
using measurable_isomorphism_iff(1,2)[OF dist_law_A_measurable dist_law_B_measurable[OF I] A B ]
by auto
qed
subsection ‹ Binary coproduct (disjoint union, direct sum) space defined with final lifts ›
text ‹We can define binary coproduct of measurable space, but it is rather ugly. It might be better to formalize them directly.›
subsubsection ‹ The "union"of two ‹σ›-algebras ›
definition union_final_sink :: "'a measure ⇒ 'a measure ⇒ 'a measure"where
"union_final_sink M1 M2 = final_sink ((space M1) ∪ (space M2)) {(id,M1),(id,M2)}"
lemma space_union_final_sink[simp]:
shows "space(union_final_sink M1 M2) = (space M1) ∪ (space M2)"
unfolding union_final_sink_def by auto
lemma union_final_sink_sym:
shows "union_final_sink M1 M2 = union_final_sink M2 M1"
unfolding union_final_sink_def by(intro final_sink_cong,auto)
paragraph ‹ The "union"of two disjoint ‹σ›-algebras ›
lemma restrict_space_sets_cong2:
shows "(A ∩ space M) = (B ∩ space N) ⟹ sets M = sets N ⟹ sets (restrict_space M A) = sets (restrict_space N B)"
proof-
have eq1: "sets (restrict_space M A) = sets (restrict_space M (A ∩ space M))"
by (metis image_cong inf_assoc sets.Int_space_eq1 sets_restrict_space)
have eq2: "sets (restrict_space N B) = sets (restrict_space N (B ∩ space N))"
by (metis image_cong inf_assoc sets.Int_space_eq1 sets_restrict_space)
show "(A ∩ space M) = (B ∩ space N) ⟹ sets M = sets N ⟹ sets (restrict_space M A) = sets (restrict_space N B)"
unfolding eq1 eq2 by (rule restrict_space_sets_cong)
qed
context
fixes M1 M2::"'a measure"
assumes disj: "(space M1) ∩ (space M2) = {}"
begin
lemma sets_union_final_sink_disjoint:
shows "sets (union_final_sink M1 M2) = {A ∪ B | A B. A ∈ sets M1 ∧ B ∈ sets M2}"
unfolding union_final_sink_def
proof(subst sets_final_sink')
show "∀(g, N)∈{(id, M1), (id, M2)}. g ∈ space N → space M1 ∪ space M2"by auto
show "{A |A. A ∈ Pow (space M1 ∪ space M2) ∧ (∀(g, N)∈{(id, M1), (id, M2)}. g -` A ∩ space N ∈ sets N)} = {A ∪ B |A B. A ∈ sets M1 ∧ B ∈ sets M2}"
proof(intro equalityI subsetI)
fix x assume "x ∈ {A |A. A ∈ Pow (space M1 ∪ space M2) ∧ (∀(g, N)∈{(id, M1), (id, M2)}. g -` A ∩ space N ∈ sets N)}"
then have "x ∩ space M1 ∈ sets M1" and "x ∩ space M2 ∈ sets M2"and "x = (x ∩ space M1) ∪ (x ∩ space M2)"by auto
thus "x ∈ {A ∪ B |A B. A ∈ sets M1 ∧ B ∈ sets M2}"by auto
next fix x assume "x ∈ {A ∪ B |A B. A ∈ sets M1 ∧ B ∈ sets M2}"
then obtain A B where x: "x = A ∪ B"and A: "A ∈ sets M1"and B: "B ∈ sets M2"by auto
hence x2: "x ∈ Pow (space M1 ∪ space M2)"
by (metis PowI sets.sets_into_space sup_mono)
from x A B disj have "(x ∩ space M1) = A"
by (metis (full_types) inf_assoc inf_bot_right inf_commute inf_sup_distrib2 sets.Int_space_eq2 sup_bot_right)
with A have A2: "x ∩ space M1 ∈ sets M1"by auto
from x A B disj have "(x ∩ space M2) = B"
by (metis Int_assoc Un_empty_left boolean_algebra.conj_disj_distrib2 boolean_algebra.conj_zero_right sets.Int_space_eq2)
with B have B2: "x ∩ space M2 ∈ sets M2"by auto
from x2 A2 B2
show "x ∈ {A |A. A ∈ Pow (space M1 ∪ space M2) ∧ (∀(g, N)∈{(id, M1), (id, M2)}. g -` A ∩ space N ∈ sets N)}"
by auto
qed
qed
lemma union_final_sink_restricted_space_disjoint:
shows "sets(restrict_space (union_final_sink M1 M2) {x. x ∈ space M1} ) = (sets M1)"
proof(subst sets_restrict_space,subst sets_union_final_sink_disjoint )
have "(∩) {x. x ∈ space M1} ` {A ∪ B |A B. A ∈ sets M1 ∧ B ∈ sets M2} = {(space M1) ∩ (A ∪ B) |A B. A ∈ sets M1 ∧ B ∈ sets M2}"by auto
also have "... = (sets M1)"
proof(intro equalityI subsetI)
fix x assume "x ∈ {space M1 ∩ (A ∪ B) |A B. A ∈ sets M1 ∧ B ∈ sets M2}"
then obtain A B where x: "x = space M1 ∩ (A ∪ B)"and A: "A ∈ sets M1" and "B ∈ sets M2"
by auto
with disj have B2: "(space M1) ∩ B = {}"
by (metis Int_empty_right Int_left_commute sets.Int_space_eq2)
with x A have "x = A"
by (auto simp: Int_Un_distrib)
with A show "x ∈ (sets M1)"by auto
next show "⋀x. x ∈ (sets M1) ⟹ x ∈ {space M1 ∩ (A ∪ B) |A B. A ∈ sets M1 ∧ B ∈ sets M2}"
by (metis (mono_tags, lifting) Un_empty_right mem_Collect_eq sets.Int_space_eq1 sets.empty_sets)
qed
finally show "(∩) {x. x ∈ space M1} ` {A ∪ B |A B. A ∈ sets M1 ∧ B ∈ sets M2} = sets M1".
qed
lemma union_final_sink_restricted_space_disjoint':
shows "sets(restrict_space (union_final_sink M1 M2) {x. x ∈ space M2}) = (sets M2)"
using union_final_sink_sym[of"M1""M2"] union_final_sink_restricted_space_disjoint
by (metis Int_commute Source_and_Sink_Algebras_Constructions.union_final_sink_restricted_space_disjoint disj)
lemma measurable_inclusion_union_final_sink_restricted_space_disjoint:
shows "id ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M1} →⇩M M1"
using union_final_sink_restricted_space_disjoint measurable_cong_sets measurable_ident
by blast
lemma measurable_inclusion_union_final_sink_restricted_space_disjoint2:
shows "id ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M2} →⇩M M2"
using union_final_sink_restricted_space_disjoint' measurable_cong_sets measurable_ident
by blast
lemma measurable_if_union_final_sink_disjoint:
assumes "f ∈ M1 →⇩M N"
and "g ∈ M2 →⇩M N"
shows "(λx. if (x ∈ space M1) then f x else g x) ∈ (union_final_sink M1 M2) →⇩M N"
using assms
proof(subst measurable_If_restrict_space_iff)
have eq1: "{x ∈ space (union_final_sink M1 M2). x ∈ space M1} = space M1"
unfolding space_union_final_sink by auto
have in1: "{x. (x ∈ space M1 ∨ x ∈ space M2) ∧ x ∈ space M1} ∩ space M1 ∈ sets M1"
using eq1 by auto
have in2: "{x. (x ∈ space M1 ∨ x ∈ space M2) ∧ x ∈ space M1} ∩ space M2 ∈ sets M2"
using disj eq1 by auto
show "{x ∈ space (union_final_sink M1 M2). x ∈ space M1} ∈ sets (union_final_sink M1 M2)"
unfolding union_final_sink_def
by(subst sets_final_sink',auto simp add: in1 in2)
show "f ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M1} →⇩M N ∧ g ∈ restrict_space (union_final_sink M1 M2) {x. x ∉ space M1} →⇩M N"
proof(rule conjI)
show "f ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M1} →⇩M N"
proof(subst measurable_cong')
show "f o id ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M1} →⇩M N"
by(rule measurable_comp[OF measurable_inclusion_union_final_sink_restricted_space_disjoint assms(1)])
qed(auto)
show "g ∈ restrict_space (union_final_sink M1 M2) {x. x ∉ space M1} →⇩M N"
proof(subst measurable_cong_simp)
have eq1: "sets (restrict_space (union_final_sink M1 M2) {x. x ∉ space M1}) = sets (restrict_space (union_final_sink M1 M2) {x. x ∈ space M2})"
using disj by(intro restrict_space_sets_cong2,auto)
thus"restrict_space (union_final_sink M1 M2) {x. x ∉ space M1} = (restrict_space (union_final_sink M1 M2) {x. x ∈ space M2})"
unfolding restrict_space_def using eq1 by (metis sets_eq_imp_space_eq sets_restrict_space space_restrict_space)
show "g ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M2} →⇩M N"
proof(subst measurable_cong')
show "g o id ∈ restrict_space (union_final_sink M1 M2) {x. x ∈ space M2} →⇩M N"
by(rule measurable_comp[OF measurable_inclusion_union_final_sink_restricted_space_disjoint2 assms(2)])
qed(auto)
qed(auto)
qed
qed
end
subsubsection ‹ Binary coproduct space ›
text ‹ To construct the coproduct of @{term M} and @{term N}. We first embed them to the common @{typ"('a + 'b) measure"} ›
lemma
shows Plus_inter: "(A <+> B) ∩ (C <+> D) = ((A ∩ C) <+> (B ∩ D))"
and Plus_union: "(A <+> B) ∪ (C <+> D) = ((A ∪ C) <+> (B ∪ D))"
unfolding Plus_def by auto
lemma
shows Plus_mono: "⋀A B C D. A ⊆ B ⟹ C ⊆ D ⟹ A <+> C ⊆ B <+> D"
and Plus_decompose: "⋀A. A = Inl -` A <+> Inr -` A"
and Plus_subset_decompose: "⋀A C D. A ⊆ C <+> D ⟹ (Inl -` A) ⊆ C ∧ (Inr -` A) ⊆ D"
and vimage_inl: "⋀A B. Inl -` (A <+> B) = A"
and vimage_inr: "⋀A B. Inr -` (A <+> B) = B"
unfolding Plus_def using UNIV_sum by auto
definition Inl_final_sink :: "'a measure ⇒ 'b measure ⇒ ('a + 'b) measure"where
"Inl_final_sink M N = final_sink ((space M) <+> ({} :: 'b set)) {(Inl,M)}"
lemma space_Inl_final_sink:
"space (Inl_final_sink M N) = (space M) <+> {}"
by(auto simp: Inl_final_sink_def)
lemma sets_Inl_final_sink:
fixes M :: "'a measure"and N :: "'b measure"
shows "sets (Inl_final_sink M N) = {A <+> ({} :: 'b set) | A. A ∈ sets M}"
unfolding Inl_final_sink_def
proof(subst sets_final_sink')
have imp: "⋀A x. A ∈ sets M ⟹ x ∈ A ⟹ x ∈ space M"
using sets.sets_into_space by auto
show "{A |A. A ∈ Pow (space M <+> {}) ∧ (∀(g, N)∈{(Inl, M)}. g -` A ∩ space N ∈ sets N)} = {A <+> {} |A. A ∈ sets M}"
by(intro set_eqI iffI)(clarify,intro exI conjI sets.sets_into_space,auto simp:imp vimage_inl vimage_inr)
qed(auto)
definition Inr_final_sink :: "'a measure ⇒ 'b measure ⇒ ('a + 'b) measure"where
"Inr_final_sink M N = final_sink (({} :: 'a set) <+> (space N)) {(Inr,N)}"
lemma space_Inr_final_sink:
shows "space (Inr_final_sink M N) = {} <+> (space N)"
by(auto simp: Inr_final_sink_def)
lemma sets_Inr_final_sink:
fixes M :: "'a measure"and N :: "'b measure"
shows "sets (Inr_final_sink M N) = {({} :: 'a set) <+> A | A. A ∈ sets N}"
unfolding Inr_final_sink_def
proof(subst sets_final_sink')
have imp: "⋀A y. A ∈ sets N ⟹ y ∈ A ⟹ y ∈ space N"
using sets.sets_into_space by auto
show "{A |A. A ∈ Pow ({} <+> space N) ∧ (∀(g, N)∈{(Inr, N)}. g -` A ∩ space N ∈ sets N)} = {{} <+> A |A. A ∈ sets N}"
by(intro set_eqI iffI)(clarify,intro exI conjI sets.sets_into_space,auto simp:imp vimage_inl vimage_inr)
qed(auto)
definition Plus_algebra :: "'a measure ⇒ 'b measure ⇒ ('a + 'b) measure"where
"Plus_algebra M N = union_final_sink (Inl_final_sink M N) (Inr_final_sink M N)"
lemma space_Plus_algebra[simp]:
shows "space (Plus_algebra M N) = ((space M) <+> (space N))"
unfolding Plus_algebra_def union_final_sink_def space_final_sink Inl_final_sink_def Inr_final_sink_def by auto
lemma measurable_Inl': "Inl ∈ M →⇩M (Inl_final_sink M N)"
unfolding Inl_final_sink_def
by(rule measurable_final_sink1,auto)
lemma measurable_projl':
shows "projl ∈ (Inl_final_sink M N) →⇩M M"
unfolding Inl_final_sink_def
by(auto intro!: measurable_final_sink2)
lemma measurable_Inr': "Inr ∈ N →⇩M (Inr_final_sink M N)"
unfolding Inr_final_sink_def
by(rule measurable_final_sink1,auto)
lemma measurable_projr':
shows "projr ∈ (Inr_final_sink M N) →⇩M N"
unfolding Inr_final_sink_def
by(auto intro!: measurable_final_sink2)
lemma measurable_Inl[measurable]:
shows "Inl ∈ M →⇩M (Plus_algebra M N)"
proof-
have "Inl = id o Inl"
by auto
also have "... ∈ M →⇩M (Plus_algebra M N)"
by(rule measurable_comp,auto intro: measurable_Inl' measurable_final_sink1 simp: Plus_algebra_def union_final_sink_def)
finally show "Inl ∈ M →⇩M Plus_algebra M N".
qed
lemma measurable_Inr[measurable]:
shows "Inr ∈ N →⇩M (Plus_algebra M N)"
proof-
have "Inr = id o Inr"
by auto
also have "... ∈ N →⇩M (Plus_algebra M N)"
by(rule measurable_comp,auto intro: measurable_Inr' measurable_final_sink1 simp: Plus_algebra_def union_final_sink_def)
finally show "Inr ∈ N →⇩M Plus_algebra M N".
qed
lemma measurable_case_sum [measurable(raw)]:
assumes [measurable]: "f ∈ M →⇩M K"
and [measurable]: "g ∈ N →⇩M K"
shows "case_sum f g ∈ (Plus_algebra M N) →⇩M K"
proof-
note [measurable] = measurable_Inl' measurable_Inr' measurable_projl' measurable_projr'
{
fix w assume "w ∈ space (Plus_algebra M N)"
then consider"(∃ x. x ∈ space M ∧ w = Inl x)"|"(∃ y. y ∈ space N ∧ w = Inr y)"
by auto
hence "case_sum f g w = (λx. if (x ∈ space (Inl_final_sink M N)) then (f o projl) x else (g o projr) x) w"
by(cases,auto simp: space_Inl_final_sink)
}note eq1 = this
show ?thesis
proof(subst measurable_cong[OF eq1],clarify)
show "(λw. if w ∈ space (Inl_final_sink M N) then (f ∘ projl) w else (g ∘ projr) w) ∈ Plus_algebra M N →⇩M K"
unfolding Plus_algebra_def
by(rule measurable_if_union_final_sink_disjoint,auto simp: space_Inl_final_sink space_Inr_final_sink)
qed
qed
lemma measurable_from_plus_algebra_iff:
shows "(h o Inl ∈ M →⇩M K) ∧ (h o Inr ∈ N →⇩M K) ⟷ h ∈ (Plus_algebra M N) →⇩M K"
proof(rule iffI)
assume A: "(h o Inl ∈ M →⇩M K) ∧ (h o Inr ∈ N →⇩M K)"
have "h = case_sum (h o Inl) (h o Inr)"
by (auto simp: case_sum_expand_Inr_pointfree)
also have "... ∈ (Plus_algebra M N) →⇩M K"
by (auto simp: A measurable_case_sum)
finally show "h ∈ Plus_algebra M N →⇩M K".
next
note [measurable] = measurable_Inl measurable_Inr
assume A2: "h ∈ Plus_algebra M N →⇩M K"
thus"h ∘ Inl ∈ M →⇩M K ∧ h ∘ Inr ∈ N →⇩M K"
by(intro conjI, measurable)
qed
text ‹ It might be better to use the following ‹σ›-algebra directly. ›
lemma sets_Plus_algebra:
fixes M :: "'a measure"and N :: "'b measure"
shows "sets (Plus_algebra M N) = {A <+> B | A B. A ∈ sets M ∧ B ∈ sets N}"
unfolding Plus_algebra_def space_Inl_final_sink space_Inr_final_sink
proof(subst sets_union_final_sink_disjoint)
show "space (Inl_final_sink M N) ∩ space (Inr_final_sink M N) = {}"
by(auto simp: space_Inl_final_sink space_Inr_final_sink)
show "{A ∪ B |A B. A ∈ sets (Inl_final_sink M N) ∧ B ∈ sets (Inr_final_sink M N)} = {A <+> B |A B. A ∈ sets M ∧ B ∈ sets N}"
by(rule equalityI subsetI)(auto simp: sets_Inl_final_sink sets_Inr_final_sink Plus_def)
qed
paragraph ‹ Distributive laws between binary products and binary coproducts ›
lemma measurable_Plus_pair_pair_to_pair_Plus:
shows "case_sum (λ(a,b). (Inl a,b)) (λ(a,b). (Inr a,b)) ∈ (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)) →⇩M ((Plus_algebra M N) ⨂⇩M L) "
by measurable
lemma sets_Plus_pair_basis:
"sets (Plus_algebra M N ⨂⇩M L) = sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E | C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"
unfolding sets_pair_measure sets_Plus_algebra space_Plus_algebra space_pair_measure
by(rule subset_antisym)(intro sigma_sets_mono,clarify,blast)+
lemma sets_pair_Plus_basis:
"sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)) = sigma_sets (space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))) {(C × E) <+> (D × F) | C D E F. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L ∧ F ∈ sets L} "
unfolding space_Plus_algebra space_pair_measure
proof(rule subset_antisym)
let ?Ω = "sigma_sets (space M × space L <+> space N × space L) {(C × E) <+> (D × F) | C D E F. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L ∧ F ∈ sets L} "
have 1: "ring_of_sets (space M × space L <+> space N × space L) ?Ω"
proof(intro algebra.axioms(1) sigma_algebra.axioms(1) sigma_algebra_sigma_sets subsetI)
fix x assume "x ∈ {C × E <+> D × F |C D E F. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L ∧ F ∈ sets L}"
then obtain C D E F where "C ∈ sets M""D ∈ sets N""E ∈ sets L""F ∈ sets L "and x :"x = C × E <+> D × F"
by auto
hence "C ⊆ space M" "D ⊆ space N" "E ⊆ space L" "F ⊆ space L"
using sets.sets_into_space by blast+
thus "x ∈ Pow (space M × space L <+> space N × space L)"unfolding x by auto
qed
show "sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)) ⊆ ?Ω"
unfolding sets_Plus_algebra space_Plus_algebra space_pair_measure sets_pair_measure
proof(intro subsetI,clarify)
fix A B assume A: "A ∈ sigma_sets (space M × space L) {C × D |C D. C ∈ sets M ∧ D ∈ sets L}"and B: "B ∈ sigma_sets (space N × space L) {C × D |C D. C ∈ sets N ∧ D ∈ sets L}"
from A have A2: "A <+> {} ∈ ?Ω"
proof(induct A rule: sigma_sets.induct)
case (Basic a)
then show ?case
by (blast intro: Sigma_empty1)
next
case Empty
then show ?case
by (auto simp: Plus_def sigma_sets.Empty)
next
case (Compl a)
have "(space M × space L - a) <+> {} = ((space M × space L ) <+> {}) -(a <+> {}) "
by auto
also have "... ∈ ?Ω"
proof(intro ring_of_sets.Diff)
show "space M × space L <+> {} ∈ ?Ω"
by blast
qed(fact+)
finally show ?case .
next
case (Union a)
have "⋃ (range a) <+> {} = ⋃ { a i <+> {} | i::nat. i ∈ UNIV} "by auto
also have "... ∈ ?Ω"
proof(rule sigma_sets_UNION)
show "countable {a i <+> {} |i. i ∈ UNIV}"
by (metis Setcompr_eq_image uncountable_def)
qed(auto simp: Union)
finally show ?case .
qed
from B have B2: "{} <+> B ∈ ?Ω"
proof(induct B rule: sigma_sets.induct)
case (Basic a)
then show ?case
by (blast intro: Sigma_empty1)
next
case Empty
then show ?case unfolding Plus_def
by (auto simp: sigma_sets.Empty)
next
case (Compl a)
have "{} <+> (space N × space L - a) = ({} <+> (space N × space L )) -({} <+> a) "
by auto
also have "... ∈ ?Ω"
proof(rule ring_of_sets.Diff)
show "{} <+> space N × space L ∈ ?Ω"
by blast
qed(fact+)
finally show ?case .
next
case (Union a)
have "{} <+> ⋃ (range a) = ⋃ {{} <+> a i | i::nat. i ∈ UNIV} "by auto
also have "... ∈ ?Ω"
proof(rule sigma_sets_UNION)
show "countable {{} <+> a i |i. i ∈ UNIV}"
by (metis Setcompr_eq_image uncountable_def)
qed (auto simp: Union)
finally show ?case .
qed
from A2 B2
have "A <+> B = (A <+> {}) ∪ ({} <+> B)"by auto
also have "... ∈ ?Ω"
by(rule sigma_sets_Un, auto simp: A2 B2)
finally show "A <+> B ∈ ?Ω".
qed
show "?Ω ⊆ sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
proof(intro subsetI)
fix x assume "x ∈ ?Ω"
then show "x ∈ sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
proof (induct x rule: sigma_sets.induct)
case (Basic a)
then obtain C E D F where a: "a = C × E <+> D × F"and "C ∈ sets M""D ∈ sets N""E ∈ sets L""F ∈ sets L"
by auto
hence "C × E ∈ sigma_sets (space M × space L) {a × b |a b. a ∈ sets M ∧ b ∈ sets L}""D × F∈ sigma_sets (space N × space L) {a × b |a b. a ∈ sets N ∧ b ∈ sets L}"
by auto
then show ?case unfolding a sets_Plus_algebra sets_pair_measure space_Plus_algebra space_pair_measure by auto
next
case Empty
then show ?case by blast
next
case (Compl a)
then show ?case
proof(intro ring_of_sets.Diff)
show "space M × space L <+> space N × space L ∈ sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
unfolding sets_Plus_algebra sets_pair_measure space_Plus_algebra space_pair_measure by blast
show "ring_of_sets (space M × space L <+> space N × space L) (sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)))"
by(intro algebra.axioms(1) sigma_algebra.axioms(1)) (metis sets.sigma_algebra_axioms space_Plus_algebra space_pair_measure)
qed(auto)
next
case (Union a)
then show ?case by auto
qed
qed
qed
lemma vimage_map_sum:
shows "(map_sum f g) -` (A <+> B) = (f -` A) <+> (g -` B)"
proof
let ?f = "(map_sum f g)"
show "?f -` (A <+> B) ⊆ f -` A <+> g -` B"
proof(rule subsetI,unfold vimage_eq)
fix x::"('a + 'b)"assume xin: "?f x ∈ A <+> B"
then have P: "(∃ a::'a. x = (Inl a)) ∨ (∃ a::'b. x = (Inr a))"
using sum.exhaust_sel by blast
consider "(∃ a::'a. x = (Inl a))"| "(∃ a::'b. x = (Inr a))"
using P by auto
then show "x ∈ f -` A <+> g -` B"
using xin by(cases, force+)
qed
show "f -` A <+> g -` B ⊆ map_sum f g -` (A <+> B)"
by auto
qed
lemma measurable_pair_Plus_to_Plus_pair_pair:
shows "(λ(a::'a +'b, b::'c). case a of Inl x ⇒ Inl (x, b) | Inr x ⇒ Inr (x, b)) ∈ ((Plus_algebra M N) ⨂⇩M L) →⇩M (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
(is "?f ∈ ((Plus_algebra M N) ⨂⇩M L) →⇩M (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))")
proof(rule measurableI)
have feq: "?f -` space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)) = space (Plus_algebra M N ⨂⇩M L)"
unfolding space_Plus_algebra space_pair_measure
proof(intro set_eqI iffI;unfold vimage_eq)
fix x::"('a + 'b) × 'c"assume xin: "?f x ∈ space M × space L <+> space N × space L"
then have P: "(∃ a::'a. ∃ b::'c. x = (Inl a, b)) ∨ (∃ a::'b. ∃ b::'c. x = (Inr a, b)) "
by (metis prod.exhaust_sel sum.exhaust_sel)
consider "(∃ a::'a. ∃ b::'c. x = (Inl a, b))"| "(∃ a::'b. ∃ b::'c. x = (Inr a, b))"
using P by auto
then show "x ∈ (space M <+> space N) × space L"
using xin by(cases,force+)
next fix x assume xin: "x ∈ (space M <+> space N) × space L"
then have P: "(∃ a::'a. ∃ b::'c. x = (Inl a, b)) ∨ (∃ a::'b. ∃ b::'c. x = (Inr a, b)) "
by (metis prod.exhaust_sel sum.exhaust_sel)
consider "(∃ a::'a. ∃ b::'c. x = (Inl a, b))"| "(∃ a::'b. ∃ b::'c. x = (Inr a, b))"
using P by auto
then show "?f x ∈ space M × space L <+> space N × space L"
using xin by(cases,force+)
qed
show "⋀x. x ∈ space (Plus_algebra M N ⨂⇩M L) ⟹ ?f x ∈ space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
by (auto simp: space_pair_measure)
fix A assume A: "A ∈ sets (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
have "?f -` A ∩ space (Plus_algebra M N ⨂⇩M L) = ?f -` A"
proof
show "?f -` A ∩ space (Plus_algebra M N ⨂⇩M L) ⊆ ?f -` A"
by auto
have "?f -` A ⊆ space (Plus_algebra M N ⨂⇩M L) "
using A sets.sets_into_space feq by blast
thus "?f -` A ⊆ ?f -` A ∩ space (Plus_algebra M N ⨂⇩M L)"
by auto
qed
also have "... ∈ sets (Plus_algebra M N ⨂⇩M L)"
using A
unfolding sets_Plus_pair_basis sets_pair_Plus_basis comp_def
proof(induct rule: sigma_sets.induct)
case (Basic a)
then obtain C D E F where C: "C ∈ sets M"and D: "D ∈ sets N"and E: "E ∈ sets L"and F: "F ∈ sets L "and a :"a = C × E <+> D × F"
by auto
have finva: "?f -` a = ((C <+> {}) × E) ∪ (({} <+> D) × F) "
unfolding a
proof(intro set_eqI iffI; unfold vimage_eq)
fix x::"('a + 'b) × 'c"assume xin: "?f x ∈ C × E <+> D × F"
then have P: "(∃ a::'a. ∃ b::'c. x = (Inl a, b)) ∨ (∃ a::'b. ∃ b::'c. x = (Inr a, b)) "
by (metis old.sum.exhaust surj_pair)
consider "(∃ a::'a. ∃ b::'c. x = (Inl a, b))"| "(∃ a::'b. ∃ b::'c. x = (Inr a, b))"
using P by auto
then show "x ∈ (C <+> {}) × E ∪ ({} <+> D) × F"
using xin by(cases,force+)
next
fix x::"('a + 'b) × 'c"assume xin: "x ∈ (C <+> {}) × E ∪ ({} <+> D) × F"
then have P: "(∃ a::'a. ∃ b::'c. x = (Inl a, b)) ∨ (∃ a::'b. ∃ b::'c. x = (Inr a, b)) "
by (metis old.sum.exhaust surj_pair)
consider "(∃ a::'a. ∃ b::'c. x = (Inl a, b))"| "(∃ a::'b. ∃ b::'c. x = (Inr a, b))"
using P by auto
then show "?f x ∈ C × E <+> D × F"
using xin by(cases,force+)
qed
show ?case unfolding finva
by(intro sigma_sets_Un sigma_sets.Basic, auto intro!: C D E F)
next
case Empty
then show ?case
by (auto simp: sigma_sets.Empty)
next
case (Compl a)
have "?f -` (space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)) - a) = ?f -` (space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))) - ?f -` a"
by auto
also have "... ∈ sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"
proof(rule ring_of_sets.Diff)
show "?f -` (space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))) ∈ sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"
using feq unfolding space_Plus_algebra space_pair_measure by auto
show "?f -` a ∈ sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"
by fact
show "ring_of_sets (space (Plus_algebra M N ⨂⇩M L)) (sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L})"
by(intro algebra.axioms(1) sigma_algebra.axioms(1) sigma_algebra_sigma_sets, auto simp: space_pair_measure dest!: sets.sets_into_space)
qed
finally show ?case .
next
case (Union a)
{fix i
have incl: "a i ⊆ space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L))"
proof(rule sigma_sets_into_sp)
show "{C × E <+> D × F |C D E F. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L ∧ F ∈ sets L} ⊆ Pow (space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)))"
unfolding space_pair_measure space_Plus_algebra using sets.sets_into_space[of _ M] sets.sets_into_space[of _ N] sets.sets_into_space[of _ L]
by fastforce
qed (fact)
hence "(λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -` a i ⊆ (λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -`( space (Plus_algebra (M ⨂⇩M L) (N ⨂⇩M L)))"
by blast
also have "... ⊆ space (Plus_algebra M N ⨂⇩M L)"
unfolding space_pair_measure space_Plus_algebra
proof(rule subsetI,unfold vimage_eq)
fix x::"('a + 'b) × 'c"assume A: "(case x of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) ∈ space M × space L <+> space N × space L "
then have P: "(∃ a::'a. ∃ b::'c. x = (Inl a, b)) ∨ (∃ a::'b. ∃ b::'c. x = (Inr a, b)) "
by (metis prod.exhaust_sel sum.exhaust_sel)
consider "(∃ a::'a. ∃ b::'c. x = (Inl a, b))"| "(∃ a::'b. ∃ b::'c. x = (Inr a, b))"
using P by auto
then show "x ∈ (space M <+> space N) × space L"
proof(cases)
case 1
then obtain a b where x: "x = (Inl a, b)"
by auto
then have "(case x of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) = Inl (a,b)"
by auto
then have "a ∈ space M"and "b ∈ space L"
using A by auto
then show ?thesis using x by auto
next
case 2
then obtain a b where x: "x = (Inr a, b)"
by auto
then have "(case x of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) = Inr (a,b)"
by auto
then have "a ∈ space N"and "b ∈ space L"
using A by auto
then show ?thesis using x by auto
qed
qed
finally have incl: "(λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -` a i ⊆ space (Plus_algebra M N ⨂⇩M L)".
hence meas:"(λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -` a i ∈ sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"using Union(2) by auto
note * = incl meas
}note * = this
then have "(λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -` ⋃ (range a) = ⋃ (range (λ i. (λa. case a of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b)) -` a i))"
by blast
also have "... ∈ sigma_sets (space (Plus_algebra M N ⨂⇩M L)) {(C <+> D) × E |C D E. C ∈ sets M ∧ D ∈ sets N ∧ E ∈ sets L}"
using sigma_sets.Union *(2)
by (metis (no_types, lifting))
finally show ?case by blast
qed
finally show "?f -` A ∩ space (Plus_algebra M N ⨂⇩M L) ∈ sets (Plus_algebra M N ⨂⇩M L)".
qed
lemma pair_Plus_o_Plus_pair_pair_id:
"( (λ(a::'a +'b, b::'c). case a of Inl x ⇒ Inl (x, b) | Inr x ⇒ Inr (x, b)) o case_sum (λ(a,b). (Inl a,b)) (λ(a,b). (Inr a,b)) ) = id"
unfolding comp_def
proof
fix x::"('a ×'c) + ('b ×'c)"
consider "(∃ a c. x = Inl(a,c)) "|"(∃ b c. x = Inr(b,c))"
by (metis obj_sumE surj_pair)
thus "(case case x of Inl (a, xa) ⇒ (Inl a, xa) | Inr (a, xa) ⇒ (Inr a, xa) of (Inl x, b) ⇒ Inl (x, b) | (Inr x, b) ⇒ Inr (x, b))= id x"
by (cases,auto)
qed
lemma Plus_pair_pair_o_pair_Plus_id:
"(case_sum (λ(a,b). (Inl a,b)) (λ(a,b). (Inr a,b)) o (λ(a::'a +'b, b::'c). case a of Inl x ⇒ Inl (x, b) | Inr x ⇒ Inr (x, b))) = id"
proof
fix x::"('a +'b) ×'c"
consider "(∃ a c. x = (Inl a,c)) "|"(∃ b c. x = (Inr b,c))"
by (metis obj_sumE surj_pair)
thus "(case_sum (λ(a, b). (Inl a, b)) (λ(a, b). (Inr a, b)) ∘ (λ(a, b). case a of Inl x ⇒ Inl (x, b) | Inr x ⇒ Inr (x, b))) x = id x"
by (cases,auto)
qed
subsection ‹ Option spaces ›
definition None_algebra :: "('a option) measure"where
"None_algebra = sigma {None} {{None}}"
definition Some_final_sink :: "'a measure ⇒ ('a option) measure"where
"Some_final_sink M = final_sink (Some` (space M)) {(Some,M)}"
lemma sets_Some_final_sink:
shows "sets (Some_final_sink M) = {Some `A | A. A ∈ (sets M)}"
unfolding Some_final_sink_def
proof(subst sets_final_sink')
show "∀(g, N)∈{(Some, M)}. g ∈ space N → Some ` space M"by auto
show "{A |A. A ∈ Pow (Some ` space M) ∧ (∀(g, N)∈{(Some, M)}. g -` A ∩ space N ∈ sets N)} = {Some ` A |A. A ∈ sets M}"
proof(intro equalityI subsetI)
fix x assume "x ∈ {A |A. A ∈ Pow (Some ` space M) ∧ (∀(g, N)∈{(Some, M)}. g -` A ∩ space N ∈ sets N)}"
then have "x = Some ` (Some -` x)"and "Some -` x = Some -` x ∩ space M"and 2: "Some -` x ∩ space M ∈ sets M"
by auto
thus "x ∈ {Some ` A |A. A ∈ sets M}"
by (metis (mono_tags, lifting) mem_Collect_eq)
next fix x assume "x ∈ {Some ` A |A. A ∈ sets M}"
then obtain A where "A ⊆ space M"and A: "A ∈ sets M"and "x = Some ` A"
using sets.sets_into_space by force
hence "x ∈ Pow (Some ` space M)"and "Some -` x ∩ space M = A"
by blast+
with A show "x ∈ {A |A. A ∈ Pow (Some ` space M) ∧ (∀(g, N)∈{(Some, M)}. g -` A ∩ space N ∈ sets N)}"
by blast
qed
qed
definition option_final_sink:: "'a measure ⇒ ('a option) measure"where
"option_final_sink M = union_final_sink (Some_final_sink M) (None_algebra)"
lemma space_option_final_sink[simp]:
shows "space (option_final_sink M) = (Some` (space M)) ∪ {None}"
by(auto simp:option_final_sink_def Some_final_sink_def None_algebra_def union_final_sink_def)
lemma measurable_Some[measurable]:
shows "Some ∈ M →⇩M option_final_sink M"
proof-
have "Some = id o Some"
by auto
also have "... ∈ M →⇩M option_final_sink M"
by(rule measurable_comp[of _ _ "Some_final_sink M"],auto simp:Some_final_sink_def option_final_sink_def union_final_sink_def)
finally show ?thesis .
qed
lemma sets_option_final_sink:
shows "sets (option_final_sink M) = { (Some `A ) ∪ {None} | A. A ∈ sets M} ∪ { (Some `A ) | A. A ∈ sets M}"
unfolding option_final_sink_def
proof(subst sets_union_final_sink_disjoint)
show "space (Some_final_sink M) ∩ space None_algebra = {}"
unfolding Some_final_sink_def None_algebra_def
by auto
show "{A ∪ B |A B. A ∈ sets (Some_final_sink M) ∧ B ∈ sets None_algebra} = {Some ` A ∪ {None} |A. A ∈ sets M} ∪ {Some ` A |A. A ∈ sets M}"
proof(intro equalityI subsetI)
fix x assume "x ∈ {A ∪ B |A B. A ∈ sets (Some_final_sink M) ∧ B ∈ sets None_algebra}"
then obtain A B where x: "x = A ∪ B"and "A ∈ sets (Some_final_sink M)"and B: "B ∈ sets None_algebra"by auto
then obtain C where A: "A = Some `C "and C: "C ∈ (sets M)"
by (auto simp:sets_Some_final_sink)
from B have B: "B = {} ∨ B = {None}"
unfolding None_algebra_def by auto
from x A C B show "x ∈ {Some ` A ∪ {None} |A. A ∈ sets M} ∪ {Some ` A |A. A ∈ sets M}"by auto
next fix x assume "x ∈ {Some ` A ∪ {None} |A. A ∈ sets M} ∪ {Some ` A |A. A ∈ sets M}"
then have "x ∈ {Some ` A ∪ {None} |A. A ∈ sets M} ∨ x ∈ {Some ` A |A. A ∈ sets M}"by auto
thus "x ∈ {A ∪ B |A B. A ∈ sets (Some_final_sink M) ∧ B ∈ sets None_algebra} "
by (auto simp:sets_Some_final_sink None_algebra_def)
qed
qed
end