Theory QuasiBorel
section ‹Quasi-Borel Spaces›
theory QuasiBorel
imports "HOL-Probability.Probability"
begin
subsection ‹ Definitions ›
subsubsection ‹ Quasi-Borel Spaces›
definition qbs_closed1 :: "(real ⇒ 'a) set ⇒ bool"
where "qbs_closed1 Mx ≡ (∀a ∈ Mx. ∀f ∈ (borel :: real measure) →⇩M (borel :: real measure). a ∘ f ∈ Mx)"
definition qbs_closed2 :: "['a set, (real ⇒ 'a) set] ⇒ bool"
where "qbs_closed2 X Mx ≡ (∀x ∈ X. (λr. x) ∈ Mx)"
definition qbs_closed3 :: "(real ⇒ 'a) set ⇒ bool"
where "qbs_closed3 Mx ≡ (∀P::real ⇒ nat. ∀Fi::nat ⇒ real ⇒ 'a.
(P ∈ borel →⇩M count_space UNIV) ⟶ (∀i. Fi i ∈ Mx) ⟶ (λr. Fi (P r) r) ∈ Mx)"
lemma separate_measurable:
fixes P :: "real ⇒ nat"
assumes "⋀i. P -` {i} ∈ sets borel"
shows "P ∈ borel →⇩M count_space UNIV"
by (auto simp add: assms measurable_count_space_eq_countable)
lemma measurable_separate:
fixes P :: "real ⇒ nat"
assumes "P ∈ borel →⇩M count_space UNIV"
shows "P -` {i} ∈ sets borel"
by (metis assms borel_singleton measurable_sets_borel sets.empty_sets sets_borel_eq_count_space)
definition "is_quasi_borel X Mx ⟷ Mx ⊆ UNIV → X ∧ qbs_closed1 Mx ∧ qbs_closed2 X Mx ∧ qbs_closed3 Mx"
lemma is_quasi_borel_intro[simp]:
assumes "Mx ⊆ UNIV → X"
and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx"
shows "is_quasi_borel X Mx"
using assms by(simp add: is_quasi_borel_def)
typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}"
proof
show "(UNIV, UNIV) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
qed
definition qbs_space :: "'a quasi_borel ⇒ 'a set" where
"qbs_space X ≡ fst (Rep_quasi_borel X)"
definition qbs_Mx :: "'a quasi_borel ⇒ (real ⇒ 'a) set" where
"qbs_Mx X ≡ snd (Rep_quasi_borel X)"
declare [[coercion qbs_space]]
lemma qbs_decomp : "(qbs_space X,qbs_Mx X) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified])
lemma qbs_Mx_to_X:
assumes "α ∈ qbs_Mx X"
shows "α r ∈ qbs_space X"
using qbs_decomp assms by(auto simp: is_quasi_borel_def)
lemma qbs_closed1I:
assumes "⋀α f. α ∈ Mx ⟹ f ∈ borel →⇩M borel ⟹ α ∘ f ∈ Mx"
shows "qbs_closed1 Mx"
using assms by(simp add: qbs_closed1_def)
lemma qbs_closed1_dest[simp]:
assumes "α ∈ qbs_Mx X"
and "f ∈ borel →⇩M borel"
shows "α ∘ f ∈ qbs_Mx X"
using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def)
lemma qbs_closed1_dest'[simp]:
assumes "α ∈ qbs_Mx X"
and "f ∈ borel →⇩M borel"
shows "(λr. α (f r)) ∈ qbs_Mx X"
using qbs_closed1_dest[OF assms] by (simp add: comp_def)
lemma qbs_closed2I:
assumes "⋀x. x ∈ X ⟹ (λr. x) ∈ Mx"
shows "qbs_closed2 X Mx"
using assms by(simp add: qbs_closed2_def)
lemma qbs_closed2_dest[simp]:
assumes "x ∈ qbs_space X"
shows "(λr. x) ∈ qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def)
lemma qbs_closed3I:
assumes "⋀(P :: real ⇒ nat) Fi. P ∈ borel →⇩M count_space UNIV ⟹ (⋀i. Fi i ∈ Mx)
⟹ (λr. Fi (P r) r) ∈ Mx"
shows "qbs_closed3 Mx"
using assms by(auto simp: qbs_closed3_def)
lemma qbs_closed3I':
assumes "⋀(P :: real ⇒ nat) Fi. (⋀i. P -` {i} ∈ sets borel) ⟹ (⋀i. Fi i ∈ Mx)
⟹ (λr. Fi (P r) r) ∈ Mx"
shows "qbs_closed3 Mx"
using assms by(auto intro!: qbs_closed3I dest: measurable_separate)
lemma qbs_closed3_dest[simp]:
fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
assumes "P ∈ borel →⇩M count_space UNIV"
and "⋀i. Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def)
lemma qbs_closed3_dest':
fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
assumes "⋀i. P -` {i} ∈ sets borel"
and "⋀i. Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
using qbs_closed3_dest[OF separate_measurable[OF assms(1)] assms(2)] .
lemma qbs_closed3_dest2:
assumes "countable I"
and [measurable]: "P ∈ borel →⇩M count_space I"
and "⋀i. i ∈ I ⟹ Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
have 0:"I ≠ {}"
using measurable_empty_iff[of "count_space I" P borel] assms(2)
by fastforce
define P' where "P' ≡ to_nat_on I ∘ P"
define Fi' where "Fi' ≡ Fi ∘ (from_nat_into I)"
have 1:"P' ∈ borel →⇩M count_space UNIV"
by(simp add: P'_def)
have 2:"⋀i. Fi' i ∈ qbs_Mx X"
using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def)
have "(λr. Fi' (P' r) r) ∈ qbs_Mx X"
using 1 2 measurable_separate by auto
thus ?thesis
using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)]
by(auto simp: Fi'_def P'_def)
qed
lemma qbs_closed3_dest2':
assumes "countable I"
and [measurable]: "P ∈ borel →⇩M count_space I"
and "⋀i. i ∈ range P ⟹ Fi i ∈ qbs_Mx X"
shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
have 0:"range P ∩ I = range P"
using measurable_space[OF assms(2)] by auto
have 1:"P ∈ borel →⇩M count_space (range P)"
using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"]
by(simp add: 0)
have 2:"countable (range P)"
using countable_Int2[OF assms(1),of "range P"]
by(simp add: 0)
show ?thesis
by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)])
qed
lemma qbs_Mx_indicat:
assumes "S ∈ sets borel" "α ∈ qbs_Mx X" "β ∈ qbs_Mx X"
shows "(λr. if r ∈ S then α r else β r) ∈ qbs_Mx X"
proof -
have "(λr::real. if r ∈ S then α r else β r) = (λr. (λb. if b then α else β) (r ∈ S) r)"
by(auto simp: indicator_def)
also have "... ∈ qbs_Mx X"
by(rule qbs_closed3_dest2[where I=UNIV and Fi="λb. if b then α else β"]) (use assms in auto)
finally show ?thesis .
qed
lemma qbs_space_Mx: "qbs_space X = {α x |x α. α ∈ qbs_Mx X}"
proof safe
fix x
assume 1:"x ∈ qbs_space X"
show "∃xa α. x = α xa ∧ α ∈ qbs_Mx X"
by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1)
qed(simp add: qbs_Mx_to_X)
lemma qbs_space_eq_Mx:
assumes "qbs_Mx X = qbs_Mx Y"
shows "qbs_space X = qbs_space Y"
by(simp add: qbs_space_Mx assms)
lemma qbs_eqI:
assumes "qbs_Mx X = qbs_Mx Y"
shows "X = Y"
by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms])
subsubsection ‹ Empty Space ›
definition empty_quasi_borel :: "'a quasi_borel" where
"empty_quasi_borel ≡ Abs_quasi_borel ({},{})"
lemma
shows eqb_space[simp]: "qbs_space empty_quasi_borel = ({} :: 'a set)"
and eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = ({} :: (real ⇒ 'a) set)"
proof -
have "Rep_quasi_borel empty_quasi_borel = ({} :: 'a set, {})"
using Abs_quasi_borel_inverse by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
thus "qbs_space empty_quasi_borel = ({} :: 'a set)" "qbs_Mx empty_quasi_borel = ({} :: (real ⇒ 'a) set)"
by(auto simp add: qbs_space_def qbs_Mx_def)
qed
lemma qbs_empty_equiv :"qbs_space X = {} ⟷ qbs_Mx X = {}"
proof safe
fix x
assume "qbs_Mx X = {}"
and h:"x ∈ qbs_space X"
have "(λr. x) ∈ qbs_Mx X"
using h by simp
thus "x ∈ {}" using ‹qbs_Mx X = {}› by simp
qed(use qbs_Mx_to_X in blast)
lemma empty_quasi_borel_iff:
"qbs_space X = {} ⟷ X = empty_quasi_borel"
by(auto intro!: qbs_eqI simp: qbs_empty_equiv)
subsubsection ‹ Unit Space ›
definition unit_quasi_borel :: "unit quasi_borel" ("1⇩Q") where
"unit_quasi_borel ≡ Abs_quasi_borel (UNIV,UNIV)"
lemma
shows unit_qbs_space[simp]: "qbs_space unit_quasi_borel = {()}"
and unit_qbs_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}"
proof -
have "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)"
using Abs_quasi_borel_inverse by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
thus "qbs_space unit_quasi_borel = {()}" "qbs_Mx unit_quasi_borel = {λr. ()}"
by(auto simp add: qbs_space_def qbs_Mx_def UNIV_unit)
qed
subsubsection ‹ Sub-Spaces ›
definition sub_qbs :: "['a quasi_borel, 'a set] ⇒ 'a quasi_borel" where
"sub_qbs X U ≡ Abs_quasi_borel (qbs_space X ∩ U,{α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)})"
lemma
shows sub_qbs_space: "qbs_space (sub_qbs X U) = qbs_space X ∩ U"
and sub_qbs_Mx: "qbs_Mx (sub_qbs X U) = {α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)}"
proof -
have "qbs_closed1 {α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)}" "qbs_closed2 (qbs_space X ∩ U) {α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)}"
"qbs_closed3 {α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)}"
unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto
hence "Rep_quasi_borel (sub_qbs X U) = (qbs_space X ∩ U,{α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)})"
by(auto simp: sub_qbs_def is_quasi_borel_def qbs_Mx_to_X intro!: Abs_quasi_borel_inverse)
thus "qbs_space (sub_qbs X U) = qbs_space X ∩ U" "qbs_Mx (sub_qbs X U) = {α. α ∈ qbs_Mx X ∧ (∀r. α r ∈ U)}"
by(simp_all add: qbs_Mx_def qbs_space_def)
qed
lemma sub_qbs:
assumes "U ⊆ qbs_space X"
shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f ∈ UNIV → U. f ∈ qbs_Mx X})"
using assms by (auto simp: sub_qbs_space sub_qbs_Mx)
lemma sub_qbs_ident: "sub_qbs X (qbs_space X) = X"
by(auto intro!: qbs_eqI simp: sub_qbs_Mx qbs_Mx_to_X)
lemma sub_qbs_sub_qbs: "sub_qbs (sub_qbs X A) B = sub_qbs X (A ∩ B)"
by(auto intro!: qbs_eqI simp: sub_qbs_Mx sub_qbs_space)
subsubsection ‹ Image Spaces ›
definition map_qbs :: "['a ⇒ 'b] ⇒ 'a quasi_borel ⇒ 'b quasi_borel" where
"map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{f ∘ α |α. α∈ qbs_Mx X})"
lemma
shows map_qbs_space: "qbs_space (map_qbs f X) = f ` (qbs_space X)"
and map_qbs_Mx: "qbs_Mx (map_qbs f X) = {f ∘ α |α. α∈ qbs_Mx X}"
proof -
have "{f ∘ α |α. α∈ qbs_Mx X} ⊆ UNIV → f ` (qbs_space X)"
using qbs_Mx_to_X by fastforce
moreover have "qbs_closed1 {f ∘ α |α. α∈ qbs_Mx X}"
unfolding qbs_closed1_def using qbs_closed1_dest by(fastforce simp: comp_def)
moreover have "qbs_closed2 (f ` (qbs_space X)) {f ∘ α |α. α∈ qbs_Mx X}"
unfolding qbs_closed2_def by fastforce
moreover have "qbs_closed3 {f ∘ α |α. α∈ qbs_Mx X}"
proof(rule qbs_closed3I')
fix P :: "real ⇒ nat" and Fi
assume h:"⋀i::nat. P -` {i} ∈ sets borel"
"⋀i::nat. Fi i ∈ {f ∘ α |α. α∈ qbs_Mx X}"
then obtain αi where ha: "⋀i::nat. αi i ∈ qbs_Mx X" "⋀i. Fi i = f ∘ (αi i)"
by auto metis
hence 1:"(λr. αi (P r) r) ∈ qbs_Mx X"
using h(1) qbs_closed3_dest' by blast
show "(λr. Fi (P r) r) ∈ {f ∘ α |α. α∈ qbs_Mx X}"
by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def)
qed
ultimately have "Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{f ∘ α |α. α∈ qbs_Mx X})"
unfolding map_qbs_def by(auto intro!: Abs_quasi_borel_inverse)
thus "qbs_space (map_qbs f X) = f ` (qbs_space X)" "qbs_Mx (map_qbs f X) = {f ∘ α |α. α∈ qbs_Mx X}"
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
subsubsection ‹ Binary Product Spaces ›
definition pair_qbs :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a × 'b) quasi_borel" (infixr "⨂⇩Q" 80) where
"pair_qbs X Y = Abs_quasi_borel (qbs_space X × qbs_space Y, {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y})"
lemma
shows pair_qbs_space: "qbs_space (X ⨂⇩Q Y) = qbs_space X × qbs_space Y"
and pair_qbs_Mx: "qbs_Mx (X ⨂⇩Q Y) = {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
proof -
have "{f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y} ⊆ UNIV → qbs_space X × qbs_space Y"
by (auto simp: mem_Times_iff[of _ "qbs_space X" "qbs_space Y"]; use qbs_Mx_to_X in fastforce)
moreover have "qbs_closed1 {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
unfolding qbs_closed1_def by (metis (no_types, lifting) comp_assoc mem_Collect_eq qbs_closed1_dest)
moreover have "qbs_closed2 (qbs_space X × qbs_space Y) {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
unfolding qbs_closed2_def by auto
moreover have "qbs_closed3 {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
proof(safe intro!: qbs_closed3I)
fix P :: "real ⇒ nat"
fix Fi :: "nat ⇒ real ⇒ 'a × 'b"
define Fj :: "nat ⇒ real ⇒ 'a" where "Fj ≡ λj.(fst ∘ Fi j)"
assume "∀i. Fi i ∈ {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
then have "⋀i. Fj i ∈ qbs_Mx X" by (simp add: Fj_def)
moreover assume "P ∈ borel →⇩M count_space UNIV"
ultimately have "(λr. Fj (P r) r) ∈ qbs_Mx X"
by auto
moreover have "fst ∘ (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
ultimately show "fst ∘ (λr. Fi (P r) r) ∈ qbs_Mx X" by simp
next
fix P :: "real ⇒ nat"
fix Fi :: "nat ⇒ real ⇒ 'a × 'b"
define Fj :: "nat ⇒ real ⇒ 'b" where "Fj ≡ λj.(snd ∘ Fi j)"
assume "∀i. Fi i ∈ {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
then have "⋀i. Fj i ∈ qbs_Mx Y" by (simp add: Fj_def)
moreover assume "P ∈ borel →⇩M count_space UNIV"
ultimately have "(λr. Fj (P r) r) ∈ qbs_Mx Y"
by auto
moreover have "snd ∘ (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
ultimately show "snd ∘ (λr. Fi (P r) r) ∈ qbs_Mx Y" by simp
qed
ultimately have "Rep_quasi_borel (X ⨂⇩Q Y) = (qbs_space X × qbs_space Y, {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y})"
unfolding pair_qbs_def by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro)
thus "qbs_space (X ⨂⇩Q Y) = qbs_space X × qbs_space Y" "qbs_Mx (X ⨂⇩Q Y) = {f. fst ∘ f ∈ qbs_Mx X ∧ snd ∘ f ∈ qbs_Mx Y}"
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
lemma pair_qbs_fst:
assumes "qbs_space Y ≠ {}"
shows "map_qbs fst (X ⨂⇩Q Y) = X"
proof(rule qbs_eqI)
obtain αy where hy:"αy ∈ qbs_Mx Y"
using qbs_empty_equiv[of Y] assms by auto
show "qbs_Mx (map_qbs fst (X ⨂⇩Q Y)) = qbs_Mx X"
by(auto simp: map_qbs_Mx pair_qbs_Mx hy comp_def intro!: exI[where x="λr. (_ r, αy r)"])
qed
lemma pair_qbs_snd:
assumes "qbs_space X ≠ {}"
shows "map_qbs snd (X ⨂⇩Q Y) = Y"
proof(rule qbs_eqI)
obtain αx where hx:"αx ∈ qbs_Mx X"
using qbs_empty_equiv[of X] assms by auto
show "qbs_Mx (map_qbs snd (X ⨂⇩Q Y)) = qbs_Mx Y"
by(auto simp: map_qbs_Mx pair_qbs_Mx hx comp_def intro!: exI[where x="λr. (αx r, _ r)"])
qed
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 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 following 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 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 safe
fix g :: "real ⇒ 'a + 'b"
assume "g ∈ copair_qbs_Mx X Y"
then obtain S where hs:"S∈ sets 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 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 obtain S α1 α2 where Sag:
"S ∈ sets borel" "α1 ∈ qbs_Mx X" "α2 ∈ qbs_Mx Y" "g = (λr. if r ∈ S then Inl (α1 r) else Inr (α2 r))"
by auto
consider "S = {}" | "S = UNIV" | "S ≠ {}" "S ≠ UNIV" by auto
then show "g ∈ 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
show ?thesis
using ‹α2 ∈ qbs_Mx Y› unfolding copair_qbs_Mx_def
by(auto intro! : bexI[where x=UNIV] simp: Sag)
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 Sag by(auto simp add: copair_qbs_Mx_def)
next
assume "S ≠ {}" "S ≠ UNIV"
then show ?thesis
using Sag by(auto simp add: copair_qbs_Mx_def)
qed
qed
qed
lemma
shows copair_qbs_space: "qbs_space (X ⨁⇩Q Y) = qbs_space X <+> qbs_space Y" (is ?goal1)
and copair_qbs_Mx: "qbs_Mx (X ⨁⇩Q Y) = copair_qbs_Mx X Y" (is ?goal2)
proof -
have "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 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 qbs_Mx_to_X by auto
next
assume "S = UNIV"
then show ?thesis
using hs qbs_Mx_to_X 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 dest: qbs_Mx_to_X)
qed
qed
moreover have "qbs_closed1 (copair_qbs_Mx X Y)"
proof(rule qbs_closed1I)
fix g and f :: "real ⇒ real"
assume "g ∈ copair_qbs_Mx X Y" and [measurable]: "f ∈ borel →⇩M 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"
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"
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 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 safe
fix S α1 α2
assume [measurable]:"S ∈ sets borel" and "α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 borel"
using ‹S ∈ sets borel› ‹f ∈ borel_measurable borel› measurable_sets_borel by blast
moreover have "α1 ∘ f ∈ qbs_Mx X"
using ‹α1∈ qbs_Mx X› by(auto simp add: qbs_closed1_def)
moreover have "α2 ∘ f ∈ qbs_Mx Y"
using ‹α2∈ qbs_Mx Y› 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
moreover have "qbs_closed2 (qbs_space X <+> qbs_space Y) (copair_qbs_Mx X Y)"
proof(rule qbs_closed2I)
fix y
assume "y ∈ qbs_space X <+> qbs_space Y"
then consider "y ∈ Inl ` (qbs_space X)" | "y ∈ Inr ` (qbs_space Y)"
by auto
thus "(λr. y) ∈ copair_qbs_Mx X Y"
proof cases
case 1
then obtain x where x: "y = Inl x" "x ∈ qbs_space X"
by auto
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 borel" by auto
ultimately show "(λr. y) ∈ copair_qbs_Mx X Y"
by(auto simp add: copair_qbs_Mx_def x)
next
case 2
then obtain x where x: "y = Inr x" "x ∈ qbs_space Y"
by auto
define α2 :: "real ⇒ _" where "α2 ≡ (λr. x)"
have "α2 ∈ qbs_Mx Y" using ‹x ∈ qbs_space Y› qbs_decomp
by(force simp add: qbs_closed2_def α2_def)
moreover have "(λr. Inr x) = (λl. Inr (α2 l))" by (simp add: α2_def)
moreover have "UNIV ∈ sets borel" by auto
ultimately show "(λr. y) ∈ copair_qbs_Mx X Y"
unfolding copair_qbs_Mx_def
by(auto intro!: bexI[where x=UNIV] simp: x)
qed
qed
moreover have "qbs_closed3 (copair_qbs_Mx X Y)"
proof(safe intro!: qbs_closed3I)
fix P :: "real ⇒ nat"
fix Fi :: "nat ⇒ real ⇒_ + _"
assume "P ∈ borel →⇩M count_space UNIV"
"∀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 ‹P ∈ borel →⇩M count_space UNIV› 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 ‹P ∈ borel →⇩M count_space UNIV› h2
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 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 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 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 ‹P ∈ borel →⇩M count_space UNIV› h1
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 ‹P ∈ borel →⇩M count_space UNIV› h2
have "β2 ∈ qbs_Mx Y" by(simp add: β2_def)
define A :: "nat ⇒ real set" where "A ≡ (λi. S i ∩ P -` {i})"
have [measurable]:"⋀i. A i ∈ sets borel"
using A_def hs measurable_separate[OF ‹P ∈ borel →⇩M count_space UNIV›] 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 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 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
ultimately have "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)
thus ?goal1 ?goal2
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
lemma copair_qbs_MxD:
assumes "g ∈ qbs_Mx (X ⨁⇩Q Y)"
and "⋀α. α ∈ qbs_Mx X ⟹ g = (λr. Inl (α r)) ⟹ P g"
and "⋀β. β ∈ qbs_Mx Y ⟹ g = (λr. Inr (β r)) ⟹ P g"
and "⋀S α β. (S :: real set) ∈ sets borel ⟹ S ≠ {} ⟹ S ≠ UNIV ⟹ α ∈ qbs_Mx X ⟹ β ∈ qbs_Mx Y ⟹ g = (λr. if r ∈ S then Inl (α r) else Inr (β r)) ⟹ P g"
shows "P g"
using assms by(fastforce simp: copair_qbs_Mx copair_qbs_Mx_def)
subsubsection ‹ Product Spaces ›
definition PiQ :: "'a set ⇒ ('a ⇒ 'b quasi_borel) ⇒ ('a ⇒ 'b) quasi_borel" where
"PiQ I X ≡ Abs_quasi_borel (Π⇩E i∈I. qbs_space (X i), {α. ∀i. (i ∈ I ⟶ (λr. α r i) ∈ qbs_Mx (X i)) ∧ (i ∉ I ⟶ (λr. α r i) = (λr. undefined))})"
syntax
"_PiQ" :: "pttrn ⇒ 'i set ⇒ 'a quasi_borel ⇒ ('i => 'a) quasi_borel" ("(3Π⇩Q _∈_./ _)" 10)
syntax_consts
"_PiQ" == PiQ
translations
"Π⇩Q x∈I. X" == "CONST PiQ I (λx. X)"
lemma
shows PiQ_space: "qbs_space (PiQ I X) = (Π⇩E i∈I. qbs_space (X i))" (is ?goal1)
and PiQ_Mx: "qbs_Mx (PiQ I X) = {α. ∀i. (i ∈ I ⟶ (λr. α r i) ∈ qbs_Mx (X i)) ∧ (i ∉ I ⟶ (λr. α r i) = (λr. undefined))}" (is "_ = ?Mx")
proof -
have "?Mx ⊆ UNIV → (Π⇩E i∈I. qbs_space (X i))"
using qbs_Mx_to_X[of _ "X _"] by auto metis
moreover have "qbs_closed1 ?Mx"
proof(safe intro!: qbs_closed1I)
fix α i and f :: "real ⇒ real"
assume h[measurable]:"∀i. (i ∈ I ⟶ (λr. α r i) ∈ qbs_Mx (X i)) ∧ (i ∉ I ⟶ (λr. α r i) = (λr. undefined))"
"f ∈ borel →⇩M borel"
show "(λr. (α ∘ f) r i) ∈ qbs_Mx (X i)" if i:"i ∈ I"
proof -
have "(λr. α r i) ∘ f ∈ qbs_Mx (X i)"
using h i by auto
thus "(λr. (α ∘ f) r i) ∈ qbs_Mx (X i)"
by(simp add: comp_def)
qed
show "i ∉ I ⟹ (λr. (α ∘ f) r i) = (λr. undefined)"
by (metis comp_apply h(1))
qed
moreover have "qbs_closed2 (Π⇩E i∈I. qbs_space (X i)) ?Mx"
by(rule qbs_closed2I) (auto simp: PiE_def extensional_def Pi_def)
moreover have "qbs_closed3 ?Mx"
proof(rule qbs_closed3I)
fix P :: "real ⇒ nat" and Fi
assume h:"P ∈ borel →⇩M count_space UNIV"
"⋀i::nat. Fi i ∈ ?Mx"
show "(λr. Fi (P r) r) ∈ ?Mx"
proof safe
fix i
assume hi:"i ∈ I"
then show "(λr. Fi (P r) r i) ∈ qbs_Mx (X i)"
using h qbs_closed3_dest[OF h(1),of "λj r. Fi j r i"]
by auto
next
show "⋀i. i ∉ I ⟹ (λr. Fi (P r) r i) = (λr. undefined)"
using h by auto meson
qed
qed
ultimately have "Rep_quasi_borel (PiQ I X) = (Π⇩E i∈I. qbs_space (X i), ?Mx)"
by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro simp: PiQ_def)
thus ?goal1 "qbs_Mx (PiQ I X) = ?Mx"
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
lemma prod_qbs_MxI:
assumes "⋀i. i ∈ I ⟹ (λr. α r i) ∈ qbs_Mx (X i)"
and "⋀i. i ∉ I ⟹ (λr. α r i) = (λr. undefined)"
shows "α ∈ qbs_Mx (PiQ I X)"
using assms by(auto simp: PiQ_Mx)
lemma prod_qbs_MxD:
assumes "α ∈ qbs_Mx (PiQ I X)"
shows "⋀i. i ∈ I ⟹ (λr. α r i) ∈ qbs_Mx (X i)"
and "⋀i. i ∉ I ⟹ (λr. α r i) = (λr. undefined)"
and "⋀i r. i ∉ I ⟹ α r i = undefined"
using assms by(auto simp: PiQ_Mx dest: fun_cong[where g="(λr. undefined)"])
lemma PiQ_eqI:
assumes "⋀i. i ∈ I ⟹ X i = Y i"
shows "PiQ I X = PiQ I Y"
by(auto intro!: qbs_eqI simp: PiQ_Mx assms)
lemma PiQ_empty: "qbs_space (PiQ {} X) = {λi. undefined}"
by(auto simp: PiQ_space)
lemma PiQ_empty_Mx: "qbs_Mx (PiQ {} X) = {λr i. undefined}"
by(auto simp: PiQ_Mx) meson
subsubsection ‹ Coproduct Spaces ›
definition coPiQ_Mx :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ (real ⇒ 'a × 'b) set" where
"coPiQ_Mx I X ≡ { λr. (f r, α (f r) r) |f α. f ∈ borel →⇩M count_space I ∧ (∀i∈range f. α i ∈ qbs_Mx (X i))}"
definition coPiQ_Mx' :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ (real ⇒ 'a × 'b) set" where
"coPiQ_Mx' I X ≡ { λr. (f r, α (f r) r) |f α. f ∈ borel →⇩M count_space I ∧ (∀i. (i ∈ range f ∨ qbs_space (X i) ≠ {}) ⟶ α i ∈ qbs_Mx (X i))}"
lemma coPiQ_Mx_eq:
"coPiQ_Mx I X = coPiQ_Mx' I X"
proof safe
fix α
assume "α ∈ coPiQ_Mx I X"
then obtain f β where hfb:
"f ∈ borel →⇩M count_space I" "⋀i. i ∈ range f ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coPiQ_Mx_def by blast
define β' where "β' ≡ (λi. if i ∈ range f then β i
else if qbs_space (X i) ≠ {} then (SOME γ. γ ∈ qbs_Mx (X i))
else β i)"
have 1:"α = (λr. (f r, β' (f r) r))"
by(simp add: hfb(3) β'_def)
have 2:"⋀i. qbs_space (X i) ≠ {} ⟹ β' i ∈ qbs_Mx (X i)"
proof -
fix i
assume hne:"qbs_space (X i) ≠ {}"
then obtain x where "x ∈ qbs_space (X i)" by auto
hence "(λr. x) ∈ qbs_Mx (X i)" by auto
thus "β' i ∈ qbs_Mx (X i)"
by(cases "i ∈ range f") (auto simp: β'_def hfb(2) hne intro!: someI2[where a="λr. x"])
qed
show "α ∈ coPiQ_Mx' I X"
using hfb(1,2) 1 2 β'_def by(auto simp: coPiQ_Mx'_def intro!: exI[where x=f] exI[where x=β'])
next
fix α
assume "α ∈ coPiQ_Mx' I X"
then obtain f β where hfb:
"f ∈ borel →⇩M count_space I" "⋀i. qbs_space (X i) ≠ {} ⟹ β i ∈ qbs_Mx (X i)"
"⋀i. i ∈ range f ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coPiQ_Mx'_def by blast
show "α ∈ coPiQ_Mx I X"
by(auto simp: hfb(4) coPiQ_Mx_def intro!: hfb(1) hfb(3))
qed
definition coPiQ :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ ('a × 'b) quasi_borel" where
"coPiQ I X ≡ Abs_quasi_borel (SIGMA i:I. qbs_space (X i), coPiQ_Mx I X)"
syntax
"_coPiQ" :: "pttrn ⇒ 'i set ⇒ 'a quasi_borel ⇒ ('i × 'a) quasi_borel" ("(3⨿⇩Q _∈_./ _)" 10)
syntax_consts
"_coPiQ" ⇌ coPiQ
translations
"⨿⇩Q x∈I. X" ⇌ "CONST coPiQ I (λx. X)"
lemma
shows coPiQ_space: "qbs_space (coPiQ I X) = (SIGMA i:I. qbs_space (X i))" (is ?goal1)
and coPiQ_Mx: "qbs_Mx (coPiQ I X) = coPiQ_Mx I X" (is ?goal2)
proof -
have "coPiQ_Mx I X ⊆ UNIV → (SIGMA i:I. qbs_space (X i))"
by(fastforce simp: coPiQ_Mx_def dest: measurable_space qbs_Mx_to_X)
moreover have "qbs_closed1 (coPiQ_Mx I X)"
proof(rule qbs_closed1I)
fix α and f :: "real ⇒ real"
assume "α ∈ coPiQ_Mx I X"
and 1[measurable]: "f ∈ borel →⇩M borel"
then obtain β g where ha:
"⋀i. i ∈ range g ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and [measurable]:"g ∈ borel →⇩M count_space I"
by(fastforce simp: coPiQ_Mx_def)
then have "⋀i. i ∈ range g ⟹ β i ∘ f ∈ qbs_Mx (X i)"
by simp
thus "α ∘ f ∈ coPiQ_Mx I X"
unfolding coPiQ_Mx_def by (auto intro!: exI[where x="g ∘ f"] exI[where x="λi. β i ∘ f"] simp: ha(2))
qed
moreover have "qbs_closed2 (SIGMA i:I. qbs_space (X i)) (coPiQ_Mx I X)"
proof(safe intro!: qbs_closed2I)
fix i x
assume "i ∈ I" "x ∈ qbs_space (X i)"
then show "(λr. (i,x)) ∈ coPiQ_Mx I X"
by(auto simp: coPiQ_Mx_def intro!: exI[where x="λr. i"])
qed
moreover have "qbs_closed3 (coPiQ_Mx I X)"
proof(rule qbs_closed3I)
fix P :: "real ⇒ nat" and Fi
assume h[measurable]:"P ∈ borel →⇩M count_space UNIV"
"⋀i :: nat. Fi i ∈ coPiQ_Mx I X"
then have "∀i. ∃fi αi. Fi i = (λr. (fi r, αi (fi r) r)) ∧ fi ∈ borel →⇩M count_space I ∧ (∀j. (j ∈ range fi ∨ qbs_space (X j) ≠ {}) ⟶ αi j ∈ qbs_Mx (X j))"
by(auto simp: coPiQ_Mx_eq coPiQ_Mx'_def)
then obtain fi where
"∀i. ∃αi. Fi i = (λr. (fi i r, αi (fi i r) r)) ∧ fi i ∈ borel →⇩M count_space I ∧ (∀j. (j ∈ range (fi i) ∨ qbs_space (X j) ≠ {}) ⟶ αi j ∈ qbs_Mx (X j))"
by(fastforce intro!: choice)
then obtain αi where
"∀i. Fi i = (λr. (fi i r, αi i (fi i r) r)) ∧ fi i ∈ borel →⇩M count_space I ∧ (∀j. (j ∈ range (fi i) ∨ qbs_space (X j) ≠ {}) ⟶ αi i j ∈ qbs_Mx (X j))"
by(fastforce intro!: choice)
then have hf[measurable]:
"⋀i. Fi i = (λr. (fi i r, αi i (fi i r) r))" "⋀i. fi i ∈ borel →⇩M count_space I" "⋀i j. j ∈ range (fi i) ⟹ αi i j ∈ qbs_Mx (X j)" "⋀i j. qbs_space (X j) ≠ {} ⟹ αi i j ∈ qbs_Mx (X j)"
by auto
define f' where "f' ≡ (λr. fi (P r) r)"
define α' where "α' ≡ (λi r. αi (P r) i r)"
have 1:"(λr. Fi (P r) r) = (λr. (f' r, α' (f' r) r))"
by(simp add: α'_def f'_def hf)
have "f' ∈ borel →⇩M count_space I"
by(simp add: f'_def)
moreover have "⋀i. i ∈ range f' ⟹ α' i ∈ qbs_Mx (X i)"
proof -
fix i
assume hi:"i ∈ range f'"
then obtain r where hr: "i = fi (P r) r" by(auto simp: f'_def)
hence "i ∈ range (fi (P r))" by simp
hence "αi (P r) i ∈ qbs_Mx (X i)" by(simp add: hf)
hence "qbs_space (X i) ≠ {}"
by(auto simp: qbs_empty_equiv)
hence "⋀j. αi j i ∈ qbs_Mx (X i)"
by(simp add: hf(4))
then show "α' i ∈ qbs_Mx (X i)"
by(auto simp: α'_def h(1) intro!: qbs_closed3_dest[of P "λj. αi j i"])
qed
ultimately show "(λr. Fi (P r) r) ∈ coPiQ_Mx I X"
by(auto simp: 1 coPiQ_Mx_def intro!: exI[where x=f'])
qed
ultimately have "Rep_quasi_borel (coPiQ I X) = (SIGMA i:I. qbs_space (X i), coPiQ_Mx I X)"
unfolding coPiQ_def by(fastforce intro!: Abs_quasi_borel_inverse)
thus ?goal1 ?goal2
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
lemma coPiQ_MxI:
assumes "f ∈ borel →⇩M count_space I"
and "⋀i. i ∈ range f ⟹ α i ∈ qbs_Mx (X i)"
shows "(λr. (f r, α (f r) r)) ∈ qbs_Mx (coPiQ I X)"
using assms unfolding coPiQ_Mx_def coPiQ_Mx by blast
lemma coPiQ_eqI:
assumes "⋀i. i ∈ I ⟹ X i = Y i"
shows "coPiQ I X = coPiQ I Y"
using assms by(auto intro!: qbs_eqI simp: coPiQ_Mx coPiQ_Mx_def) (metis UNIV_I measurable_space space_borel space_count_space)+
subsubsection ‹ List Spaces ›
text ‹ We define the quasi-Borel spaces on list using the following isomorphism.
\begin{align*}
List(X) \cong \coprod_{n\in \mathbb{N}} \prod_{0\leq i < n} X
\end{align*}›
definition list_nil :: "nat × (nat ⇒ 'a)" where
"list_nil ≡ (0, λn. undefined)"
definition list_cons :: "['a, nat × (nat ⇒ 'a)] ⇒ nat × (nat ⇒ 'a)" where
"list_cons x l ≡ (Suc (fst l), (λn. if n = 0 then x else (snd l) (n - 1)))"
fun from_list :: "'a list ⇒ nat × (nat ⇒ 'a)" where
"from_list [] = list_nil" |
"from_list (a#l) = list_cons a (from_list l)"
fun to_list' :: "nat ⇒ (nat ⇒ 'a) ⇒ 'a list" where
"to_list' 0 _ = []" |
"to_list' (Suc n) f = f 0 # to_list' n (λn. f (Suc n))"
definition to_list :: "nat × (nat ⇒ 'a) ⇒ 'a list" where
"to_list ≡ case_prod to_list'"
lemma inj_on_to_list: "inj_on (to_list :: nat × (nat ⇒ 'a) ⇒ 'a list) (SIGMA n:UNIV. PiE {..<n} A)"
proof(safe intro!: inj_onI)
fix n m and x y :: "nat ⇒ 'a"
assume h:"to_list (n, x) = to_list (m, y)"
have 1:"⋀a. length (to_list (n, a)) = n" for n
by(induction n) (auto simp: to_list_def)
show n:"n = m"
using 1 arg_cong[OF h,of length] by metis
show "x ∈ PiE {..<n} A ⟹ y ∈ PiE {..<m} A ⟹ x = y"
using h unfolding n
proof(induction m arbitrary: x y A)
case ih:(Suc m)
then have "to_list (m, (λn. x (Suc n))) = to_list (m, (λn. y (Suc n)))"
by(auto simp: to_list_def)
hence 1:"(λn. x (Suc n)) = (λn. y (Suc n))"
using ih(2-4) by(intro ih(1)[of _ "λn. A (Suc n)"]) auto
show ?case
proof
fix n
show "x n = y n"
proof(cases n)
assume "n = 0"
then show "x n = y n"
using ih(4) by(auto simp: to_list_def)
qed(use fun_cong[OF 1] in auto)
qed
qed(auto simp: to_list_def)
qed
text ‹ Definition ›
definition list_qbs :: "'a quasi_borel ⇒ 'a list quasi_borel" where
"list_qbs X ≡ map_qbs to_list (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
definition list_head :: "nat × (nat ⇒ 'a) ⇒ 'a" where
"list_head l = snd l 0"
definition list_tail :: "nat × (nat ⇒ 'a) ⇒ nat × (nat ⇒ 'a)" where
"list_tail l = (fst l - 1, λm. (snd l) (Suc m))"
lemma list_simp1: "list_nil ≠ list_cons x l"
by (simp add: list_nil_def list_cons_def)
lemma list_simp2:
assumes "list_cons a al = list_cons b bl"
shows "a = b" "al = bl"
proof -
have "a = snd (list_cons a al) 0" "b = snd (list_cons b bl) 0"
by (auto simp: list_cons_def)
thus "a = b"
by(simp add: assms)
next
have "fst al = fst bl"
using assms by (simp add: list_cons_def)
moreover have "snd al = snd bl"
proof
fix n
have "snd al n = snd (list_cons a al) (Suc n)"
by (simp add: list_cons_def)
also have "... = snd (list_cons b bl) (Suc n)"
by (simp add: assms)
also have "... = snd bl n"
by (simp add: list_cons_def)
finally show "snd al n = snd bl n" .
qed
ultimately show "al = bl"
by (simp add: prod.expand)
qed
lemma
shows list_simp3:"list_head (list_cons a l) = a"
and list_simp4:"list_tail (list_cons a l) = l"
by(simp_all add: list_head_def list_cons_def list_tail_def)
lemma list_decomp1:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "l = list_nil ∨
(∃a l'. a ∈ qbs_space X ∧ l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ∧ l = list_cons a l')"
proof(cases l)
case hl:(Pair n f)
show ?thesis
proof(cases n)
case 0
then show ?thesis
using assms hl by (simp add: list_nil_def coPiQ_space PiQ_space)
next
case hn:(Suc n')
define f' where "f' ≡ λm. f (Suc m)"
have "l = list_cons (f 0) (n',f')"
unfolding hl hn list_cons_def
proof safe
fix m
show "f = (λm. if m = 0 then f 0 else snd (n', f') (m - 1))"
proof
fix m
show "f m = (if m = 0 then f 0 else snd (n', f') (m - 1))"
using assms hl by(cases m; fastforce simp: f'_def)
qed
qed simp
moreover have "(n', f') ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
proof -
have "⋀x. x ∈ {..<n'} ⟹ f' x ∈ qbs_space X"
using assms hl hn by(fastforce simp: f'_def coPiQ_space PiQ_space)
moreover {
fix x
assume 1:"x ∉ {..<n'}"
hence "f' x = undefined"
using hl assms hn by(auto simp: f'_def coPiQ_space PiQ_space)
}
ultimately show ?thesis
by(auto simp add: coPiQ_space PiQ_space)
qed
ultimately show ?thesis
using hl assms by(auto intro!: exI[where x="f 0"] exI[where x="(n',λm. if m = 0 then undefined else f (Suc m))"] simp: list_cons_def coPiQ_space PiQ_space)
qed
qed
lemma list_simp5:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
and "l ≠ list_nil"
shows "l = list_cons (list_head l) (list_tail l)"
proof -
obtain a l' where hl:
"a ∈ qbs_space X" "l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)" "l = list_cons a l'"
using list_decomp1[OF assms(1)] assms(2) by blast
hence "list_head l = a" "list_tail l = l'"
by(simp_all add: list_simp3 list_simp4)
thus ?thesis
using hl(3) list_simp2 by auto
qed
lemma list_simp6:
"list_nil ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
by (simp add: list_nil_def coPiQ_space PiQ_space)
lemma list_simp7:
assumes "a ∈ qbs_space X"
and "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "list_cons a l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using assms by(fastforce simp: PiE_def extensional_def list_cons_def coPiQ_space PiQ_space)
lemma list_destruct_rule:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
"P list_nil"
and "⋀a l'. a ∈ qbs_space X ⟹ l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⟹ P (list_cons a l')"
shows "P l"
by(rule disjE[OF list_decomp1[OF assms(1)]]) (use assms in auto)
lemma list_induct_rule:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
"P list_nil"
and "⋀a l'. a ∈ qbs_space X ⟹ l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⟹ P l' ⟹ P (list_cons a l')"
shows "P l"
proof(cases l)
case hl:(Pair n f)
then show ?thesis
using assms(1)
proof(induction n arbitrary: f l)
case 0
then show ?case
using assms(2) by (simp add: coPiQ_space PiQ_space list_nil_def)
next
case ih:(Suc n)
then obtain a l' where hl:
"a ∈ qbs_space X" "l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)" "l = list_cons a l'"
using list_decomp1 by(simp add: list_nil_def) blast
have "P l'"
using ih hl(3)
by(auto intro!: ih(1)[OF _ hl(2),of "snd l'"] simp: coPiQ_space PiQ_space list_cons_def)
from assms(3)[OF hl(1,2) this]
show ?case
by(simp add: hl(3))
qed
qed
lemma to_list_simp1: "to_list list_nil = []"
by(simp add: to_list_def list_nil_def)
lemma to_list_simp2:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "to_list (list_cons a l) = a # to_list l"
using assms by(auto simp:PiE_def to_list_def list_cons_def coPiQ_space PiQ_space)
lemma to_list_set:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "set (to_list l) ⊆ qbs_space X"
by(rule list_induct_rule[OF assms]) (auto simp: to_list_simp1 to_list_simp2)
lemma from_list_length: "fst (from_list l) = length l"
by(induction l, simp_all add: list_cons_def list_nil_def)
lemma from_list_in_list_of:
assumes "set l ⊆ qbs_space X"
shows "from_list l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using assms by(induction l) (auto simp: PiE_def extensional_def Pi_def coPiQ_space PiQ_space list_nil_def list_cons_def)
lemma from_list_in_list_of': "from_list l ∈ qbs_space ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. Abs_quasi_borel (UNIV,UNIV)))"
proof -
have "set l ⊆ qbs_space (Abs_quasi_borel (UNIV,UNIV))"
by(simp add: qbs_space_def Abs_quasi_borel_inverse[of "(UNIV,UNIV)",simplified is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def,simplified])
thus ?thesis
using from_list_in_list_of by blast
qed
lemma list_cons_in_list_of:
assumes "set (a#l) ⊆ qbs_space X"
shows "list_cons a (from_list l) ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using from_list_in_list_of[OF assms] by simp
lemma from_list_to_list_ident:
"to_list (from_list l) = l"
by(induction l) (simp add: to_list_def list_nil_def,simp add: to_list_simp2[OF from_list_in_list_of'])
lemma to_list_from_list_ident:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "from_list (to_list l) = l"
proof(rule list_induct_rule[OF assms])
fix a l'
assume h: "l' ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
and ih:"from_list (to_list l') = l'"
show "from_list (to_list (list_cons a l')) = list_cons a l'"
by(auto simp add: to_list_simp2[OF h] ih[simplified])
qed (simp add: to_list_simp1)
definition rec_list' :: "'b ⇒ ('a ⇒ (nat × (nat ⇒ 'a)) ⇒ 'b ⇒ 'b) ⇒ (nat × (nat ⇒ 'a)) ⇒ 'b" where
"rec_list' t0 f l ≡ (rec_list t0 (λx l'. f x (from_list l')) (to_list l))"
lemma rec_list'_simp1:
"rec_list' t f list_nil = t"
by(simp add: rec_list'_def to_list_simp1)
lemma rec_list'_simp2:
assumes "l ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
shows "rec_list' t f (list_cons x l) = f x l (rec_list' t f l)"
by(simp add: rec_list'_def to_list_simp2[OF assms] to_list_from_list_ident[OF assms,simplified])
lemma list_qbs_space: "qbs_space (list_qbs X) = lists (qbs_space X)"
using to_list_set by(auto simp: list_qbs_def map_qbs_space image_def from_list_to_list_ident from_list_in_list_of subset_iff intro!: bexI[where x="from_list _"])
subsubsection ‹ Option Spaces ›
text ‹ The option spaces is defined using the following isomorphism.
\begin{align*}
Option(X) \cong X + 1
\end{align*}›
definition option_qbs :: "'a quasi_borel ⇒ 'a option quasi_borel" where
"option_qbs X = map_qbs (λx. case x of Inl y ⇒ Some y | Inr y ⇒ None) (X ⨁⇩Q 1⇩Q)"
lemma option_qbs_space: "qbs_space (option_qbs X) = {Some x|x. x ∈ qbs_space X} ∪ {None}"
by(auto simp: option_qbs_def map_qbs_space copair_qbs_space) (metis InrI image_eqI insert_iff old.sum.simps(6), metis InlI image_iff sum.case(1))
subsubsection ‹ Function Spaces ›
definition exp_qbs :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a ⇒ 'b) quasi_borel" (infixr "⇒⇩Q" 61) where
"X ⇒⇩Q Y ≡ Abs_quasi_borel ({f. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}, {g. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y})"
lemma
shows exp_qbs_space: "qbs_space (exp_qbs X Y) = {f. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"
and exp_qbs_Mx: "qbs_Mx (exp_qbs X Y) = {g. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y}"
proof -
have "{g:: real ⇒ _. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y} ⊆ UNIV → {f. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"
proof safe
fix g :: "real ⇒ _" and r :: real and α
assume h:"∀α∈borel_measurable borel. ∀β∈qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y" "α ∈ qbs_Mx X"
have [simp]: "g r ∘ α = (λl. g r (α l))" by (auto simp: comp_def)
thus "g r ∘ α ∈ qbs_Mx Y"
using h by auto
qed
moreover have "qbs_closed3 {g. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y}"
by(rule qbs_closed3I, auto) (rule qbs_closed3_dest,auto)
ultimately have "Rep_quasi_borel (exp_qbs X Y) = ({f. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}, {g. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y})"
unfolding exp_qbs_def by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro qbs_closed1I qbs_closed2I simp: comp_def)
thus "qbs_space (exp_qbs X Y) = {f. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"
"qbs_Mx (exp_qbs X Y) = {g. ∀α∈ borel_measurable borel. ∀β∈ qbs_Mx X. (λr. g (α r) (β r)) ∈ qbs_Mx Y}"
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
subsubsection ‹ Ordering on Quasi-Borel Spaces ›
inductive_set generating_Mx :: "'a set ⇒ (real ⇒ 'a) set ⇒ (real ⇒ 'a) set"
for X :: "'a set" and Mx :: "(real ⇒ 'a) set"
where
Basic: "α ∈ Mx ⟹ α ∈ generating_Mx X Mx"
| Const: "x ∈ X ⟹ (λr. x) ∈ generating_Mx X Mx"
| Comp : "f ∈ (borel :: real measure) →⇩M (borel :: real measure) ⟹ α ∈ generating_Mx X Mx ⟹ α ∘ f ∈ generating_Mx X Mx"
| Part : "(⋀i. Fi i ∈ generating_Mx X Mx) ⟹ P ∈ borel →⇩M count_space (UNIV :: nat set) ⟹ (λr. Fi (P r) r) ∈ generating_Mx X Mx"
lemma generating_Mx_to_space:
assumes "Mx ⊆ UNIV → X"
shows "generating_Mx X Mx ⊆ UNIV → X"
proof
fix α
assume "α ∈ generating_Mx X Mx"
then show "α ∈ UNIV → X"
by(induct rule: generating_Mx.induct) (use assms in auto)
qed
lemma generating_Mx_closed1:
"qbs_closed1 (generating_Mx X Mx)"
by (simp add: generating_Mx.Comp qbs_closed1I)
lemma generating_Mx_closed2:
"qbs_closed2 X (generating_Mx X Mx)"
by (simp add: generating_Mx.Const qbs_closed2I)
lemma generating_Mx_closed3:
"qbs_closed3 (generating_Mx X Mx)"
by(simp add: qbs_closed3I generating_Mx.Part)
lemma generating_Mx_Mx:
"generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X"
proof safe
fix α
assume "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)"
then show "α ∈ qbs_Mx X"
by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest')
next
fix α
assume "α ∈ qbs_Mx X"
then show "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)" ..
qed
instantiation quasi_borel :: (type) order_bot
begin
inductive less_eq_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
"qbs_space X ⊂ qbs_space Y ⟹ less_eq_quasi_borel X Y"
| "qbs_space X = qbs_space Y ⟹ qbs_Mx Y ⊆ qbs_Mx X ⟹ less_eq_quasi_borel X Y"
lemma le_quasi_borel_iff:
"X ≤ Y ⟷ (if qbs_space X = qbs_space Y then qbs_Mx Y ⊆ qbs_Mx X else qbs_space X ⊂ qbs_space Y)"
by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros)
definition less_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
"less_quasi_borel X Y ⟷ (X ≤ Y ∧ ¬ Y ≤ X)"
definition bot_quasi_borel :: "'a quasi_borel" where
"bot_quasi_borel = empty_quasi_borel"
instance
proof
show "bot ≤ a" for a :: "'a quasi_borel"
using qbs_empty_equiv
by(auto simp add: le_quasi_borel_iff bot_quasi_borel_def)
qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI)
end
definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel] ⇒ 'a quasi_borel" where
"inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"
lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"
by(auto intro!: Abs_quasi_borel_inverse simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def dest: qbs_Mx_to_X)
lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X ∩ qbs_space X'"
by (simp add: qbs_space_def inf_quasi_borel_correct)
lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X ∩ qbs_Mx X'"
by(simp add: qbs_Mx_def inf_quasi_borel_correct)
definition max_quasi_borel :: "'a set ⇒ 'a quasi_borel" where
"max_quasi_borel X = Abs_quasi_borel (X, UNIV → X)"
lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV → X)"
by(fastforce intro!: Abs_quasi_borel_inverse
simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X"
by(simp add: qbs_space_def max_quasi_borel_correct)
lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV → X"
by(simp add: qbs_Mx_def max_quasi_borel_correct)
instantiation quasi_borel :: (type) semilattice_sup
begin
definition sup_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ 'a quasi_borel" where
"sup_quasi_borel X Y ≡ (if qbs_space X = qbs_space Y then inf_quasi_borel X Y
else if qbs_space X ⊂ qbs_space Y then Y
else if qbs_space Y ⊂ qbs_space X then X
else max_quasi_borel (qbs_space X ∪ qbs_space Y))"
instance
proof
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "X ≤ X ⊔ Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
by(rule less_eq_quasi_borel.intros(2),simp_all add: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
by (simp add: less_eq_quasi_borel.intros(1))
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y :: "'a quasi_borel"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "Y ≤ X ⊔ Y"
proof(cases)
case 1
show ?thesis
unfolding sup_quasi_borel_def
by(rule less_eq_quasi_borel.intros(2)) (simp_all add: 1)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
by (auto simp add: less_eq_quasi_borel.intros(1))
next
case 4
then show ?thesis
unfolding sup_quasi_borel_def
by(auto simp: less_eq_quasi_borel.intros(1))
qed
next
fix X Y Z :: "'a quasi_borel"
assume h:"X ≤ Z" "Y ≤ Z"
let ?X = "qbs_space X"
let ?Y = "qbs_space Y"
let ?Z = "qbs_space Z"
consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
by auto
then show "sup X Y ≤ Z"
proof cases
case 1
show ?thesis
unfolding sup_quasi_borel_def
apply(simp add: 1,rule less_eq_quasi_borel.cases[OF h(1)])
apply(rule less_eq_quasi_borel.intros(1))
apply auto[1]
apply simp
apply(rule less_eq_quasi_borel.intros(2))
apply(simp add: 1)
apply(rule less_eq_quasi_borel.cases[OF h(2)])
using 1
apply fastforce
apply simp
by (metis "1" h(2) inf_qbs_Mx le_inf_iff le_quasi_borel_iff)
next
case 2
then show ?thesis
unfolding sup_quasi_borel_def
using h(2) by auto
next
case 3
then show ?thesis
unfolding sup_quasi_borel_def
using h(1) by auto
next
case 4
then have [simp]:"?X ≠ ?Y" "~ (?X ⊂ ?Y)" "~ (?Y ⊂ ?X)"
by auto
have [simp]:"?X ⊆ ?Z" "?Y ⊆ ?Z"
by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases)
(metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases)
then consider "?X ∪ ?Y = ?Z" | "?X ∪ ?Y ⊂ ?Z"
by blast
then show ?thesis
unfolding sup_quasi_borel_def
apply cases
apply simp
apply(rule less_eq_quasi_borel.intros(2))
apply simp
using qbs_Mx_to_X apply auto[1]
by(simp add: less_eq_quasi_borel.intros(1))
qed
qed
end
end