Theory Binary_CoProduct_QuasiBorel
subsection ‹Coproduct Spaces›
theory Binary_CoProduct_QuasiBorel
imports "Measure_QuasiBorel_Adjunction"
begin
subsubsection ‹ Binary Coproduct Spaces ›
definition copair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel] ⇒ (real => 'a + 'b) set" where
"copair_qbs_Mx X Y ≡
{g. ∃ S ∈ sets real_borel.
(S = {} ⟶ (∃ α1∈ qbs_Mx X. g = (λr. Inl (α1 r)))) ∧
(S = UNIV ⟶ (∃ α2∈ qbs_Mx Y. g = (λr. Inr (α2 r)))) ∧
((S ≠ {} ∧ S ≠ UNIV) ⟶
(∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))))}"
definition copair_qbs :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a + 'b) quasi_borel" (infixr ‹<+>⇩Q› 65) where
"copair_qbs X Y ≡ Abs_quasi_borel (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)"
text ‹ The followin is an equivalent definition of @{term copair_qbs_Mx}. ›
definition copair_qbs_Mx2 :: "['a quasi_borel, 'b quasi_borel] ⇒ (real => 'a + 'b) set" where
"copair_qbs_Mx2 X Y ≡
{g. (if qbs_space X = {} ∧ qbs_space Y = {} then False
else if qbs_space X ≠ {} ∧ qbs_space Y = {} then
(∃α1∈ qbs_Mx X. g = (λr. Inl (α1 r)))
else if qbs_space X = {} ∧ qbs_space Y ≠ {} then
(∃α2∈ qbs_Mx Y. g = (λr. Inr (α2 r)))
else
(∃S ∈ sets real_borel. ∃α1∈ qbs_Mx X. ∃α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r))))) }"
lemma copair_qbs_Mx_equiv :"copair_qbs_Mx (X :: 'a quasi_borel) (Y :: 'b quasi_borel) = copair_qbs_Mx2 X Y"
proof(auto)
fix g :: "real ⇒ 'a + 'b"
assume "g ∈ copair_qbs_Mx X Y"
then obtain S where hs:"S∈ sets real_borel ∧
(S = {} ⟶ (∃ α1∈ qbs_Mx X. g = (λr. Inl (α1 r)))) ∧
(S = UNIV ⟶ (∃ α2∈ qbs_Mx Y. g = (λr. Inr (α2 r)))) ∧
((S ≠ {} ∧ S ≠ UNIV) ⟶
(∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))))"
by (auto simp add: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
then show "g ∈ copair_qbs_Mx2 X Y"
proof cases
assume "S = {}"
from hs this have "∃ α1∈ qbs_Mx X. g = (λr. Inl (α1 r))" by simp
then obtain α1 where h1:"α1∈ qbs_Mx X ∧ g = (λr. Inl (α1 r))" by auto
have "qbs_space X ≠ {}"
using qbs_empty_equiv h1
by auto
then have "(qbs_space X ≠ {} ∧ qbs_space Y = {}) ∨ (qbs_space X ≠ {} ∧ qbs_space Y ≠ {})"
by simp
then show "g ∈ copair_qbs_Mx2 X Y"
proof
assume "qbs_space X ≠ {} ∧ qbs_space Y = {}"
then show "g ∈ copair_qbs_Mx2 X Y"
by(simp add: copair_qbs_Mx2_def ‹∃ α1∈ qbs_Mx X. g = (λr. Inl (α1 r))›)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
then obtain α2 where "α2 ∈ qbs_Mx Y" using qbs_empty_equiv by force
define S' :: "real set"
where "S' ≡ UNIV"
define g' :: "real ⇒ 'a + 'b"
where "g' ≡ (λr::real. (if (r ∈ S') then Inl (α1 r) else Inr (α2 r)))"
from ‹qbs_space X ≠ {} ∧ qbs_space Y ≠ {}› h1 ‹α2 ∈ qbs_Mx Y›
have "g' ∈ copair_qbs_Mx2 X Y"
by(force simp add: S'_def g'_def copair_qbs_Mx2_def)
moreover have "g = g'"
using h1 by(simp add: g'_def S'_def)
ultimately show ?thesis
by simp
qed
next
assume "S = UNIV"
from hs this have "∃ α2∈ qbs_Mx Y. g = (λr. Inr (α2 r))" by simp
then obtain α2 where h2:"α2∈ qbs_Mx Y ∧ g = (λr. Inr (α2 r))" by auto
have "qbs_space Y ≠ {}"
using qbs_empty_equiv h2
by auto
then have "(qbs_space X = {} ∧ qbs_space Y ≠ {}) ∨ (qbs_space X ≠ {} ∧ qbs_space Y ≠ {})"
by simp
then show "g ∈ copair_qbs_Mx2 X Y"
proof
assume "qbs_space X = {} ∧ qbs_space Y ≠ {}"
then show ?thesis
by(simp add: copair_qbs_Mx2_def ‹∃ α2∈ qbs_Mx Y. g = (λr. Inr (α2 r))›)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
then obtain α1 where "α1 ∈ qbs_Mx X" using qbs_empty_equiv by force
define S' :: "real set"
where "S' ≡ {}"
define g' :: "real ⇒ 'a + 'b"
where "g' ≡ (λr::real. (if (r ∈ S') then Inl (α1 r) else Inr (α2 r)))"
from ‹qbs_space X ≠ {} ∧ qbs_space Y ≠ {}› h2 ‹α1 ∈ qbs_Mx X›
have "g' ∈ copair_qbs_Mx2 X Y"
by(force simp add: S'_def g'_def copair_qbs_Mx2_def)
moreover have "g = g'"
using h2 by(simp add: g'_def S'_def)
ultimately show ?thesis
by simp
qed
next
assume "S ≠ {} ∧ S ≠ UNIV"
then have
h: "∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))"
using hs by simp
then have "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
by (metis empty_iff qbs_empty_equiv)
thus ?thesis
using hs h by(auto simp add: copair_qbs_Mx2_def)
qed
next
fix g :: "real ⇒ 'a + 'b"
assume "g ∈ copair_qbs_Mx2 X Y"
then have
h: "if qbs_space X = {} ∧ qbs_space Y = {} then False
else if qbs_space X ≠ {} ∧ qbs_space Y = {} then
(∃α1∈ qbs_Mx X. g = (λr. Inl (α1 r)))
else if qbs_space X = {} ∧ qbs_space Y ≠ {} then
(∃α2∈ qbs_Mx Y. g = (λr. Inr (α2 r)))
else
(∃S ∈ sets real_borel. ∃α1∈ qbs_Mx X. ∃α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r))))"
by(simp add: copair_qbs_Mx2_def)
consider "(qbs_space X = {} ∧ qbs_space Y = {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y = {})" |
"(qbs_space X = {} ∧ qbs_space Y ≠ {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y ≠ {})" by auto
then show "g ∈ copair_qbs_Mx X Y"
proof cases
assume "qbs_space X = {} ∧ qbs_space Y = {}"
then show ?thesis
using ‹g ∈ copair_qbs_Mx2 X Y› by(simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y = {}"
from h this have "∃α1∈ qbs_Mx X. g = (λr. Inl (α1 r))" by simp
thus ?thesis
by(auto simp add: copair_qbs_Mx_def)
next
assume "qbs_space X = {} ∧ qbs_space Y ≠ {}"
from h this have "∃α2∈ qbs_Mx Y. g = (λr. Inr (α2 r))" by simp
thus ?thesis
unfolding copair_qbs_Mx_def
by(force simp add: copair_qbs_Mx_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
from h this have
"∃S ∈ sets real_borel. ∃α1∈ qbs_Mx X. ∃α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))" by simp
then show ?thesis
proof(auto simp add: exE)
fix S
fix α1
fix α2
assume "S ∈ sets real_borel"
"α1 ∈ qbs_Mx X"
"α2 ∈ qbs_Mx Y"
"g = (λr. if r ∈ S then Inl (α1 r)
else Inr (α2 r))"
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
then show "(λr. if r ∈ S then Inl (α1 r) else Inr (α2 r)) ∈ copair_qbs_Mx X Y"
proof cases
assume "S = {}"
then have [simp]: "(λr. if r ∈ S then Inl (α1 r) else Inr (α2 r)) = (λr. Inr (α2 r))"
by simp
have "UNIV ∈ sets real_borel" by simp
then show ?thesis
using ‹α2 ∈ qbs_Mx Y› unfolding copair_qbs_Mx_def
by(auto intro! : bexI[where x=UNIV])
next
assume "S = UNIV"
then have "(λr. if r ∈ S then Inl (α1 r) else Inr (α2 r)) = (λr. Inl (α1 r))"
by simp
then show ?thesis
using ‹α1 ∈ qbs_Mx X›
by(auto simp add: copair_qbs_Mx_def)
next
assume "S ≠ {} ∧ S ≠ UNIV"
then show ?thesis
using ‹S ∈ sets real_borel› ‹α1 ∈ qbs_Mx X› ‹α2 ∈ qbs_Mx Y›
by(auto simp add: copair_qbs_Mx_def)
qed
qed
qed
qed
lemma copair_qbs_f[simp]: "copair_qbs_Mx X Y ⊆ UNIV → qbs_space X <+> qbs_space Y"
proof
fix g
assume "g ∈ copair_qbs_Mx X Y"
then obtain S where hs:"S∈ sets real_borel ∧
(S = {} ⟶ (∃ α1∈ qbs_Mx X. g = (λr. Inl (α1 r)))) ∧
(S = UNIV ⟶ (∃ α2∈ qbs_Mx Y. g = (λr. Inr (α2 r)))) ∧
((S ≠ {} ∧ S ≠ UNIV) ⟶
(∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))))"
by (auto simp add: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
then show "g ∈ UNIV → qbs_space X <+> qbs_space Y"
proof cases
assume "S = {}"
then show ?thesis
using hs by auto
next
assume "S = UNIV"
then show ?thesis
using hs by auto
next
assume "S ≠ {} ∧ S ≠ UNIV"
then have "∃ α1∈ qbs_Mx X. ∃ α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))" using hs by simp
then show ?thesis
by(auto simp add: exE)
qed
qed
lemma copair_qbs_closed1: "qbs_closed1 (copair_qbs_Mx X Y)"
proof(auto simp add: qbs_closed1_def)
fix g
fix f
assume "g ∈ copair_qbs_Mx X Y"
"f ∈ real_borel →⇩M real_borel"
then have "g ∈ copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by auto
consider "(qbs_space X = {} ∧ qbs_space Y = {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y = {})" |
"(qbs_space X = {} ∧ qbs_space Y ≠ {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y ≠ {})" by auto
then have "g ∘ f ∈ copair_qbs_Mx2 X Y"
proof cases
assume "qbs_space X = {} ∧ qbs_space Y = {}"
then show ?thesis
using ‹g ∈ copair_qbs_Mx2 X Y› qbs_empty_equiv by(simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y = {}"
then obtain α1 where h1:"α1∈ qbs_Mx X ∧ g = (λr. Inl (α1 r))"
using ‹g ∈ copair_qbs_Mx2 X Y› by(auto simp add: copair_qbs_Mx2_def)
then have "α1 ∘ f ∈ qbs_Mx X"
using ‹f ∈ real_borel →⇩M real_borel› by auto
moreover have "g ∘ f = (λr. Inl ((α1 ∘ f) r))"
using h1 by auto
ultimately show ?thesis
using ‹qbs_space X ≠ {} ∧ qbs_space Y = {}› by(force simp add: copair_qbs_Mx2_def)
next
assume "(qbs_space X = {} ∧ qbs_space Y ≠ {})"
then obtain α2 where h2:"α2∈ qbs_Mx Y ∧ g = (λr. Inr (α2 r))"
using ‹g ∈ copair_qbs_Mx2 X Y› by(auto simp add: copair_qbs_Mx2_def)
then have "α2 ∘ f ∈ qbs_Mx Y"
using ‹f ∈ real_borel →⇩M real_borel› by auto
moreover have "g ∘ f = (λr. Inr ((α2 ∘ f) r))"
using h2 by auto
ultimately show ?thesis
using ‹(qbs_space X = {} ∧ qbs_space Y ≠ {})› by(force simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
then have "∃S ∈ sets real_borel. ∃α1∈ qbs_Mx X. ∃α2∈ qbs_Mx Y.
g = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))"
using ‹g ∈ copair_qbs_Mx2 X Y› by(simp add: copair_qbs_Mx2_def)
then show ?thesis
proof(auto simp add: exE)
fix S
fix α1
fix α2
assume "S ∈ sets real_borel"
"α1∈ qbs_Mx X"
"α2 ∈ qbs_Mx Y"
"g = (λr. if r ∈ S then Inl (α1 r) else Inr (α2 r))"
have "f -` S ∈ sets real_borel"
using ‹f ∈ real_borel →⇩M real_borel› ‹S ∈ sets real_borel›
by (simp add: measurable_sets_borel)
moreover have "α1 ∘ f ∈ qbs_Mx X"
using ‹α1∈ qbs_Mx X› ‹f ∈ real_borel →⇩M real_borel› qbs_decomp
by(auto simp add: qbs_closed1_def)
moreover have "α2 ∘ f ∈ qbs_Mx Y"
using ‹α2∈ qbs_Mx Y› ‹f ∈ real_borel →⇩M real_borel› qbs_decomp
by(auto simp add: qbs_closed1_def)
moreover have
"(λr. if r ∈ S then Inl (α1 r) else Inr (α2 r)) ∘ f = (λr. if r ∈ f -` S then Inl ((α1 ∘ f) r) else Inr ((α2 ∘ f) r))"
by auto
ultimately show "(λr. if r ∈ S then Inl (α1 r) else Inr (α2 r)) ∘ f ∈ copair_qbs_Mx2 X Y"
using ‹qbs_space X ≠ {} ∧ qbs_space Y ≠ {}› by(force simp add: copair_qbs_Mx2_def)
qed
qed
thus "g ∘ f ∈ copair_qbs_Mx X Y"
using copair_qbs_Mx_equiv by auto
qed
lemma copair_qbs_closed2: "qbs_closed2 (qbs_space X <+> qbs_space Y) (copair_qbs_Mx X Y)"
proof(auto simp add: qbs_closed2_def)
fix x
assume "x ∈ qbs_space X"
define α1 :: "real ⇒ _" where "α1 ≡ (λr. x)"
have "α1 ∈ qbs_Mx X" using ‹x ∈ qbs_space X› qbs_decomp
by(force simp add: qbs_closed2_def α1_def )
moreover have "(λr. Inl x) = (λl. Inl (α1 l))" by (simp add: α1_def)
moreover have "{} ∈ sets real_borel" by auto
ultimately show "(λr. Inl x) ∈ copair_qbs_Mx X Y"
by(auto simp add: copair_qbs_Mx_def)
next
fix y
assume "y ∈ qbs_space Y"
define α2 :: "real ⇒ _" where "α2 ≡ (λr. y)"
have "α2 ∈ qbs_Mx Y" using ‹y ∈ qbs_space Y› qbs_decomp
by(force simp add: qbs_closed2_def α2_def )
moreover have "(λr. Inr y) = (λl. Inr (α2 l))" by (simp add: α2_def)
moreover have "UNIV ∈ sets real_borel" by auto
ultimately show "(λr. Inr y) ∈ copair_qbs_Mx X Y"
unfolding copair_qbs_Mx_def
by(auto intro!: bexI[where x=UNIV])
qed
lemma copair_qbs_closed3: "qbs_closed3 (copair_qbs_Mx X Y)"
proof(auto simp add: qbs_closed3_def)
fix P :: "real ⇒ nat"
fix Fi :: "nat ⇒ real ⇒_ + _"
assume "∀i. P -` {i} ∈ sets real_borel"
"∀i. Fi i ∈ copair_qbs_Mx X Y"
then have "∀i. Fi i ∈ copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by blast
consider "(qbs_space X = {} ∧ qbs_space Y = {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y = {})" |
"(qbs_space X = {} ∧ qbs_space Y ≠ {})" |
"(qbs_space X ≠ {} ∧ qbs_space Y ≠ {})" by auto
then have "(λr. Fi (P r) r) ∈ copair_qbs_Mx2 X Y"
proof cases
assume "qbs_space X = {} ∧ qbs_space Y = {}"
then show ?thesis
using ‹∀i. Fi i ∈ copair_qbs_Mx2 X Y› qbs_empty_equiv
by(simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y = {}"
then have "∀i. ∃αi. αi ∈ qbs_Mx X ∧ Fi i = (λr. Inl (αi r))"
using ‹∀i. Fi i ∈ copair_qbs_Mx2 X Y› by(auto simp add: copair_qbs_Mx2_def)
then have "∃α1. ∀i. α1 i ∈ qbs_Mx X ∧ Fi i = (λr. Inl (α1 i r))"
by(rule choice)
then obtain α1 :: "nat ⇒ real ⇒ _"
where h1: "∀i. α1 i ∈ qbs_Mx X ∧ Fi i = (λr. Inl (α1 i r))" by auto
define β :: "real ⇒ _"
where "β ≡ (λr. α1 (P r) r)"
from ‹∀i. P -` {i} ∈ sets real_borel› h1
have "β ∈ qbs_Mx X"
by (simp add: β_def)
moreover have "(λr. Fi (P r) r) = (λr. Inl (β r))"
using h1 by(simp add: β_def)
ultimately show ?thesis
using ‹qbs_space X ≠ {} ∧ qbs_space Y = {}› by (auto simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X = {} ∧ qbs_space Y ≠ {}"
then have "∀i. ∃αi. αi ∈ qbs_Mx Y ∧ Fi i = (λr. Inr (αi r))"
using ‹∀i. Fi i ∈ copair_qbs_Mx2 X Y› by(auto simp add: copair_qbs_Mx2_def)
then have "∃α2. ∀i. α2 i ∈ qbs_Mx Y ∧ Fi i = (λr. Inr (α2 i r))"
by(rule choice)
then obtain α2 :: "nat ⇒ real ⇒ _"
where h2: "∀i. α2 i ∈ qbs_Mx Y ∧ Fi i = (λr. Inr (α2 i r))" by auto
define β :: "real ⇒ _"
where "β ≡ (λr. α2 (P r) r)"
from ‹∀i. P -` {i} ∈ sets real_borel› h2 qbs_decomp
have "β ∈ qbs_Mx Y"
by(simp add: β_def)
moreover have "(λr. Fi (P r) r) = (λr. Inr (β r))"
using h2 by(simp add: β_def)
ultimately show ?thesis
using ‹qbs_space X = {} ∧ qbs_space Y ≠ {}› by (auto simp add: copair_qbs_Mx2_def)
next
assume "qbs_space X ≠ {} ∧ qbs_space Y ≠ {}"
then have "∀i. ∃Si. Si ∈ sets real_borel ∧ (∃α1i∈ qbs_Mx X. ∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ Si) then Inl (α1i r) else Inr (α2i r))))"
using ‹∀i. Fi i ∈ copair_qbs_Mx2 X Y› by (auto simp add: copair_qbs_Mx2_def)
then have "∃S. ∀i. S i ∈ sets real_borel ∧ (∃α1i∈ qbs_Mx X. ∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1i r) else Inr (α2i r))))"
by(rule choice)
then obtain S :: "nat ⇒ real set"
where hs :"∀i. S i ∈ sets real_borel ∧ (∃α1i∈ qbs_Mx X. ∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1i r) else Inr (α2i r))))"
by auto
then have "∀i. ∃α1i. α1i ∈ qbs_Mx X ∧ (∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1i r) else Inr (α2i r))))"
by blast
then have "∃α1. ∀i. α1 i ∈ qbs_Mx X ∧ (∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1 i r) else Inr (α2i r))))"
by(rule choice)
then obtain α1
where h1: "∀i. α1 i ∈ qbs_Mx X ∧ (∃α2i∈ qbs_Mx Y.
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1 i r) else Inr (α2i r))))"
by auto
define β1 :: "real ⇒ _"
where "β1 ≡ (λr. α1 (P r) r)"
from ‹∀i. P -` {i} ∈ sets real_borel› h1 qbs_decomp
have "β1 ∈ qbs_Mx X"
by(simp add: β1_def)
from h1 have "∀i. ∃α2i. α2i∈ qbs_Mx Y ∧
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1 i r) else Inr (α2i r)))"
by auto
then have "∃α2. ∀i. α2 i∈ qbs_Mx Y ∧
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1 i r) else Inr (α2 i r)))"
by(rule choice)
then obtain α2
where h2: "∀i. α2 i∈ qbs_Mx Y ∧
Fi i = (λr::real. (if (r ∈ S i) then Inl (α1 i r) else Inr (α2 i r)))"
by auto
define β2 :: "real ⇒ _"
where "β2 ≡ (λr. α2 (P r) r)"
from ‹∀i. P -` {i} ∈ sets real_borel› h2 qbs_decomp
have "β2 ∈ qbs_Mx Y"
by(simp add: β2_def)
define A :: "nat ⇒ real set"
where "A ≡ (λi. S i ∩ P -` {i})"
have "∀i. A i ∈ sets real_borel"
using A_def ‹∀i. P -` {i} ∈ sets real_borel› hs by blast
define S' :: "real set"
where "S' ≡ {r. r ∈ S (P r)}"
have "S' = (⋃i::nat. A i)"
by(auto simp add: S'_def A_def)
hence "S' ∈ sets real_borel"
using ‹∀i. A i ∈ sets real_borel› by auto
from h2 have "(λr. Fi (P r) r) = (λr. (if r ∈ S' then Inl (β1 r)
else Inr (β2 r)))"
by(auto simp add: β1_def β2_def S'_def)
thus "(λr. Fi (P r) r) ∈ copair_qbs_Mx2 X Y"
using ‹qbs_space X ≠ {} ∧ qbs_space Y ≠ {}› ‹S' ∈ sets real_borel› ‹β1 ∈ qbs_Mx X› ‹β2 ∈ qbs_Mx Y›
by(auto simp add: copair_qbs_Mx2_def)
qed
thus "(λr. Fi (P r) r) ∈ copair_qbs_Mx X Y"
using copair_qbs_Mx_equiv by auto
qed
lemma copair_qbs_correct: "Rep_quasi_borel (copair_qbs X Y) = (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)"
unfolding copair_qbs_def
by(auto intro!: Abs_quasi_borel_inverse copair_qbs_f simp: copair_qbs_closed2 copair_qbs_closed1 copair_qbs_closed3)
lemma copair_qbs_space[simp]: "qbs_space (copair_qbs X Y) = qbs_space X <+> qbs_space Y"
by(simp add: qbs_space_def copair_qbs_correct)
lemma copair_qbs_Mx[simp]: "qbs_Mx (copair_qbs X Y) = copair_qbs_Mx X Y"
by(simp add: qbs_Mx_def copair_qbs_correct)
lemma Inl_qbs_morphism:
"Inl ∈ X →⇩Q X <+>⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx X"
moreover have "Inl ∘ α = (λr. Inl (α r))" by auto
ultimately show "Inl ∘ α ∈ qbs_Mx (X <+>⇩Q Y)"
by(auto simp add: copair_qbs_Mx_def)
qed
lemma Inr_qbs_morphism:
"Inr ∈ Y →⇩Q X <+>⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx Y"
moreover have "Inr ∘ α = (λr. Inr (α r))" by auto
ultimately show "Inr ∘ α ∈ qbs_Mx (X <+>⇩Q Y)"
by(auto intro!: bexI[where x=UNIV] simp add: copair_qbs_Mx_def)
qed
lemma case_sum_preserves_morphisms:
assumes "f ∈ X →⇩Q Z"
and "g ∈ Y →⇩Q Z"
shows "case_sum f g ∈ X <+>⇩Q Y →⇩Q Z"
proof(rule qbs_morphismI;auto)
fix α
assume "α ∈ copair_qbs_Mx X Y"
then obtain S where hs:"S∈ sets real_borel ∧
(S = {} ⟶ (∃ α1∈ qbs_Mx X. α = (λr. Inl (α1 r)))) ∧
(S = UNIV ⟶ (∃ α2∈ qbs_Mx Y. α = (λr. Inr (α2 r)))) ∧
((S ≠ {} ∧ S ≠ UNIV) ⟶
(∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx Y.
α = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))))"
by (auto simp add: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
then show "case_sum f g ∘ α ∈ qbs_Mx Z"
proof cases
assume "S = {}"
then obtain α1 where h1: "α1∈ qbs_Mx X ∧ α = (λr. Inl (α1 r))"
using hs by auto
then have "f ∘ α1 ∈ qbs_Mx Z"
using assms by(auto simp add: qbs_morphism_def)
moreover have "case_sum f g ∘ α = f ∘ α1"
using h1 by auto
ultimately show ?thesis by simp
next
assume "S = UNIV"
then obtain α2 where h2: "α2∈ qbs_Mx Y ∧ α = (λr. Inr (α2 r))"
using hs by auto
then have "g ∘ α2 ∈ qbs_Mx Z"
using assms by(auto simp add: qbs_morphism_def)
moreover have "case_sum f g ∘ α = g ∘ α2"
using h2 by auto
ultimately show ?thesis by simp
next
assume "S ≠ {} ∧ S ≠ UNIV"
then obtain α1 α2 where h: "α1∈ qbs_Mx X ∧ α2∈ qbs_Mx Y ∧
α = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))"
using hs by auto
define F :: "nat ⇒ real ⇒ _"
where "F ≡ (λi r. (if i = 0 then (f ∘ α1) r
else (g ∘ α2) r))"
define P :: "real ⇒ nat"
where "P ≡ (λr. if r ∈ S then 0 else 1)"
have "f ∘ α1 ∈ qbs_Mx Z"
using assms h by(simp add: qbs_morphism_def)
have "g ∘ α2 ∈ qbs_Mx Z"
using assms h by(simp add: qbs_morphism_def)
have "∀i. F i ∈ qbs_Mx Z"
proof(auto simp add: F_def)
fix i :: nat
consider "i = 0" | "i ≠ 0" by auto
then show "(λr. if i = 0 then (f ∘ α1) r else (g ∘ α2) r) ∈ qbs_Mx Z"
proof cases
assume "i = 0"
then have "(λr. if i = 0 then (f ∘ α1) r else (g ∘ α2) r) = f ∘ α1" by auto
then show ?thesis
using ‹f ∘ α1 ∈ qbs_Mx Z› by simp
next
assume "i ≠ 0"
then have "(λr. if i = 0 then (f ∘ α1) r else (g ∘ α2) r) = g ∘ α2" by auto
then show ?thesis
using ‹g ∘ α2 ∈ qbs_Mx Z› by simp
qed
qed
moreover have "∀i. P -`{i} ∈ sets real_borel"
proof
fix i :: nat
consider "i = 0" | "i = 1" | "i ≠ 0 ∧ i ≠ 1" by auto
then show "P -`{i} ∈ sets real_borel"
proof cases
assume "i = 0"
then show ?thesis
using hs by(simp add: P_def)
next
assume "i = 1"
then show ?thesis
using hs by (simp add: P_def borel_comp)
next
assume "i ≠ 0 ∧ i ≠ 1"
then show ?thesis by(simp add: P_def)
qed
qed
ultimately have "(λr. F (P r) r) ∈ qbs_Mx Z"
by simp
moreover have "case_sum f g ∘ α = (λr. F (P r) r)"
using h by(auto simp add: F_def P_def)
ultimately show "case_sum f g ∘ α ∈ qbs_Mx Z" by simp
qed
qed
lemma map_sum_preserves_morphisms:
assumes "f ∈ X →⇩Q Y"
and "g ∈ X' →⇩Q Y'"
shows "map_sum f g ∈ X <+>⇩Q X' →⇩Q Y <+>⇩Q Y'"
proof(rule qbs_morphismI,simp)
fix α
assume "α ∈ copair_qbs_Mx X X'"
then obtain S where hs:"S∈ sets real_borel ∧
(S = {} ⟶ (∃ α1∈ qbs_Mx X. α = (λr. Inl (α1 r)))) ∧
(S = UNIV ⟶ (∃ α2∈ qbs_Mx X'. α = (λr. Inr (α2 r)))) ∧
((S ≠ {} ∧ S ≠ UNIV) ⟶
(∃ α1∈ qbs_Mx X.
∃ α2∈ qbs_Mx X'.
α = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))))"
by (auto simp add: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
then show "map_sum f g ∘ α ∈ copair_qbs_Mx Y Y'"
proof cases
assume "S = {}"
then obtain α1 where h1: "α1∈ qbs_Mx X ∧ α = (λr. Inl (α1 r))"
using hs by auto
define f' :: "real ⇒ _" where "f' ≡ f ∘ α1"
then have "f' ∈ qbs_Mx Y"
using assms h1 by(simp add: qbs_morphism_def)
moreover have "map_sum f g ∘ α = (λr. Inl (f' r))"
using h1 by (auto simp add: f'_def)
moreover have "{} ∈ sets real_borel" by simp
ultimately show ?thesis
by(auto simp add: copair_qbs_Mx_def)
next
assume "S = UNIV"
then obtain α2 where h2: "α2∈ qbs_Mx X' ∧ α = (λr. Inr (α2 r))"
using hs by auto
define g' :: "real ⇒ _" where "g' ≡ g ∘ α2"
then have "g' ∈ qbs_Mx Y'"
using assms h2 by(simp add: qbs_morphism_def)
moreover have "map_sum f g ∘ α = (λr. Inr (g' r))"
using h2 by (auto simp add: g'_def)
ultimately show ?thesis
by(auto intro!: bexI[where x=UNIV] simp add: copair_qbs_Mx_def)
next
assume "S ≠ {} ∧ S ≠ UNIV"
then obtain α1 α2 where h: "α1∈ qbs_Mx X ∧ α2∈ qbs_Mx X' ∧
α = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))"
using hs by auto
define f' :: "real ⇒ _" where "f' ≡ f ∘ α1"
define g' :: "real ⇒ _" where "g' ≡ g ∘ α2"
have "f' ∈ qbs_Mx Y"
using assms h by(auto simp: f'_def)
moreover have "g' ∈ qbs_Mx Y'"
using assms h by(auto simp: g'_def)
moreover have "map_sum f g ∘ α = (λr::real. (if (r ∈ S) then Inl (f' r) else Inr (g' r)))"
using h by(auto simp add: f'_def g'_def)
moreover have "S ∈ sets real_borel" using hs by simp
ultimately show ?thesis
using ‹S ≠ {} ∧ S ≠ UNIV› by(auto simp add: copair_qbs_Mx_def)
qed
qed
end