Theory Measure_QuasiBorel_Adjunction
subsection ‹Relation to Measurable Spaces›
theory Measure_QuasiBorel_Adjunction
imports "QuasiBorel" "QBS_Morphism" Lemmas_S_Finite_Measure_Monad
begin
text ‹ We construct the adjunction between \textbf{Meas} and \textbf{QBS},
where \textbf{Meas} is the category of measurable spaces and measurable functions,
and \textbf{QBS} is the category of quasi-Borel spaces and morphisms.›
subsubsection ‹ The Functor $R$ ›
definition measure_to_qbs :: "'a measure ⇒ 'a quasi_borel" where
"measure_to_qbs X ≡ Abs_quasi_borel (space X, borel →⇩M X)"
declare [[coercion measure_to_qbs]]
lemma
shows qbs_space_R: "qbs_space (measure_to_qbs X) = space X" (is ?goal1)
and qbs_Mx_R: "qbs_Mx (measure_to_qbs X) = borel →⇩M X" (is ?goal2)
proof -
have "Rep_quasi_borel (measure_to_qbs X) = (space X, borel →⇩M X)"
by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro qbs_closed1I qbs_closed2I simp: measure_to_qbs_def dest:measurable_space) (rule qbs_closed3I, auto)
thus ?goal1 ?goal2
by (simp_all add: qbs_space_def qbs_Mx_def)
qed
text ‹ The following lemma says that @{term measure_to_qbs} is a functor from \textbf{Meas} to \textbf{QBS}. ›
lemma r_preserves_morphisms:
"X →⇩M Y ⊆ (measure_to_qbs X) →⇩Q (measure_to_qbs Y)"
by(auto intro!: qbs_morphismI simp: qbs_Mx_R)
lemma measurable_imp_qbs_morphism: "f ∈ M →⇩M N ⟹ f ∈ M →⇩Q N"
using r_preserves_morphisms by blast
subsubsection ‹ The Functor $L$ ›
definition sigma_Mx :: "'a quasi_borel ⇒ 'a set set" where
"sigma_Mx X ≡ {U ∩ qbs_space X |U. ∀α∈qbs_Mx X. α -` U ∈ sets borel}"
definition qbs_to_measure :: "'a quasi_borel ⇒ 'a measure" where
"qbs_to_measure X ≡ Abs_measure (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
lemma measure_space_L: "measure_space (qbs_space X) (sigma_Mx X) (λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
unfolding measure_space_def
proof safe
show "sigma_algebra (qbs_space X) (sigma_Mx X)"
proof(rule sigma_algebra.intro)
show "algebra (qbs_space X) (sigma_Mx X)"
proof
have "∀ U ∈ sigma_Mx X. U ⊆ qbs_space X"
using sigma_Mx_def subset_iff by fastforce
thus "sigma_Mx X ⊆ Pow (qbs_space X)" by auto
next
show "{} ∈ sigma_Mx X"
unfolding sigma_Mx_def by auto
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
from pa pb have [simp]:"∀α∈qbs_Mx X. α -` (Ua ∩ Ub) ∈ sets borel"
by auto
from this pa pb sigma_Mx_def have [simp]:"(Ua ∩ Ub) ∩ qbs_space X ∈ sigma_Mx X" by blast
from pa pb have [simp]:"A ∩ B = (Ua ∩ Ub) ∩ qbs_space X" by auto
thus "A ∩ B ∈ sigma_Mx X" by simp
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
from pa pb have [simp]:"A - B = (Ua ∩ -Ub) ∩ qbs_space X" by auto
from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∩ -Ub) ∈ sets borel"
by (metis Diff_Compl double_compl sets.Diff vimage_Compl vimage_Int)
hence 1:"A - B ∈ sigma_Mx X"
using sigma_Mx_def ‹A - B = Ua ∩ - Ub ∩ qbs_space X› by blast
show "∃C⊆sigma_Mx X. finite C ∧ disjoint C ∧ A - B = ⋃ C"
proof
show "{A - B} ⊆sigma_Mx X ∧ finite {A-B} ∧ disjoint {A-B} ∧ A - B = ⋃ {A-B}"
using 1 by auto
qed
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
from pa pb have "A ∪ B = (Ua ∪ Ub) ∩ qbs_space X" by auto
from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∪ Ub) ∈ sets borel" by auto
then show "A ∪ B ∈ sigma_Mx X"
unfolding sigma_Mx_def
using ‹A ∪ B = (Ua ∪ Ub) ∩ qbs_space X› by blast
next
have "∀α∈qbs_Mx X. α -` (UNIV) ∈ sets borel"
by simp
thus "qbs_space X ∈ sigma_Mx X"
unfolding sigma_Mx_def
by blast
qed
next
show "sigma_algebra_axioms (sigma_Mx X)"
unfolding sigma_algebra_axioms_def
proof safe
fix A :: "nat ⇒ _"
assume 1:"range A ⊆ sigma_Mx X"
then have 2:"∀i. ∃Ui. A i = Ui ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ui ∈ sets borel)"
unfolding sigma_Mx_def by auto
then have "∃ U :: nat ⇒ _. ∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets borel)"
by (rule choice)
from this obtain U where pu:"∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets borel)"
by auto
hence "∀α∈qbs_Mx X. α -` (⋃ (range U)) ∈ sets borel"
by (simp add: countable_Un_Int(1) vimage_UN)
from pu have "⋃ (range A) = (⋃i::nat. (U i ∩ qbs_space X))" by blast
hence "⋃ (range A) = ⋃ (range U) ∩ qbs_space X" by auto
thus "⋃ (range A) ∈ sigma_Mx X"
using sigma_Mx_def ‹∀α∈qbs_Mx X. α -` ⋃ (range U) ∈ sets borel› by blast
qed
qed
next
show "countably_additive (sigma_Mx X) (λA. if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞)"
proof(rule countably_additiveI)
fix A :: "nat ⇒ _"
assume h:"range A ⊆ sigma_Mx X"
"⋃ (range A) ∈ sigma_Mx X"
consider "⋃ (range A) = {}" | "⋃ (range A) ≠ {}"
by auto
then show "(∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) =
(if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
proof cases
case 1
then have "⋀i. A i = {}"
by simp
thus ?thesis
by(simp add: 1)
next
case 2
then obtain j where hj:"A j ≠ {}"
by auto
have "(∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof -
have hsum:"⋀N f. sum f {..<N} ≤ (∑n. (f n :: ennreal))"
by (simp add: sum_le_suminf)
have hsum':"⋀P f. (∃j. j ∈ P ∧ f j = (∞ :: ennreal)) ⟹ finite P ⟹ sum f P = ∞"
by auto
have h1:"(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof(rule hsum')
show "∃ja. ja ∈ {..<j + 1} ∧ (if A ja = {} then 0 else if A ja ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof(rule exI[where x=j],rule conjI)
have "A j ∈ sigma_Mx X"
using h(1) by auto
then show "(if A j = {} then 0 else if A j ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
using hj by simp
qed simp
qed simp
have "(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) ≤ (∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
by(rule hsum)
thus ?thesis
by(simp only: h1) (simp add: top.extremum_unique)
qed
moreover have "(if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
using 2 h(2) by simp
ultimately show ?thesis
by simp
qed
qed
qed(simp add: positive_def)
lemma
shows space_L: "space (qbs_to_measure X) = qbs_space X" (is ?goal1)
and sets_L: "sets (qbs_to_measure X) = sigma_Mx X" (is ?goal2)
and emeasure_L: "emeasure (qbs_to_measure X) = (λA. if A = {} ∨ A ∉ sigma_Mx X then 0 else ∞)" (is ?goal3)
proof -
have "Rep_measure (qbs_to_measure X) = (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
unfolding qbs_to_measure_def by(auto intro!: Abs_measure_inverse simp: measure_space_L)
thus ?goal1 ?goal2 ?goal3
by(auto simp: sets_def space_def emeasure_def)
qed
lemma qbs_Mx_sigma_Mx_contra:
assumes "qbs_space X = qbs_space Y"
and "qbs_Mx X ⊆ qbs_Mx Y"
shows "sigma_Mx Y ⊆ sigma_Mx X"
using assms by(auto simp: sigma_Mx_def)
text ‹ The following lemma says that @{term qbs_to_measure} is a functor from \textbf{QBS} to \textbf{Meas}. ›
lemma l_preserves_morphisms:
"X →⇩Q Y ⊆ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
proof safe
fix f
assume h:"f ∈ X →⇩Q Y"
show "f ∈ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
proof(rule measurableI)
fix A
assume "A ∈ sets (qbs_to_measure Y)"
then obtain Ua where pa:"A = Ua ∩ qbs_space Y ∧ (∀α∈qbs_Mx Y. α -` Ua ∈ sets borel)"
by (auto simp: sigma_Mx_def sets_L)
have "∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y"
"∀α∈ qbs_Mx X. α -` (f -` (qbs_space Y)) = UNIV"
using qbs_morphism_space[OF h] qbs_morphism_Mx[OF h] by (auto simp: qbs_Mx_to_X)
hence "∀α∈qbs_Mx X. α -` (f -` A) = α -` (f -` Ua)"
by (simp add: pa)
from pa this qbs_morphism_def have "∀α∈qbs_Mx X. α -` (f -` A) ∈ sets borel"
by (simp add: vimage_comp ‹∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y›)
thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
using sigma_Mx_def by(auto simp: sets_L space_L)
qed (insert qbs_morphism_space[OF h], auto simp: space_L)
qed
lemma qbs_morphism_imp_measurable: "f ∈ X →⇩Q Y ⟹ f ∈ qbs_to_measure X →⇩M qbs_to_measure Y"
using l_preserves_morphisms by blast
abbreviation qbs_borel ("borel⇩Q") where "borel⇩Q ≡ measure_to_qbs borel"
abbreviation qbs_count_space ("count'_space⇩Q") where "qbs_count_space I ≡ measure_to_qbs (count_space I)"
lemma
shows qbs_space_qbs_borel[simp]: "qbs_space borel⇩Q = UNIV"
and qbs_space_count_space[simp]: "qbs_space (qbs_count_space I) = I"
and qbs_Mx_qbs_borel: "qbs_Mx borel⇩Q = borel_measurable borel"
and qbs_Mx_count_space: "qbs_Mx (qbs_count_space I) = borel →⇩M count_space I"
by(simp_all add: qbs_space_R qbs_Mx_R)
lemma
shows qbs_space_qbs_borel'[qbs]: "r ∈ qbs_space borel⇩Q"
and qbs_space_count_space_UNIV'[qbs]: "x ∈ qbs_space (qbs_count_space (UNIV :: (_ :: countable) set))"
by simp_all
lemma qbs_Mx_is_morphisms: "qbs_Mx X = borel⇩Q →⇩Q X"
proof safe
fix α :: "real ⇒ _"
assume "α ∈ borel⇩Q →⇩Q X"
have "id ∈ qbs_Mx borel⇩Q" by (simp add: qbs_Mx_R)
then have "α ∘ id ∈ qbs_Mx X"
using qbs_morphism_Mx[OF ‹α ∈ borel⇩Q →⇩Q X›]
by blast
then show "α ∈ qbs_Mx X" by simp
qed(auto intro!: qbs_morphismI simp: qbs_Mx_qbs_borel)
lemma exp_qbs_Mx': "qbs_Mx (exp_qbs X Y) = {g. case_prod g ∈ borel⇩Q ⨂⇩Q X →⇩Q Y}"
by(auto simp: qbs_Mx_qbs_borel comp_def qbs_Mx_is_morphisms split_beta' intro!:curry_preserves_morphisms)
lemma arg_swap_morphism':
assumes "(λg. f (λw x. g x w)) ∈ exp_qbs X (exp_qbs W Y) →⇩Q Z"
shows "f ∈ exp_qbs W (exp_qbs X Y) →⇩Q Z"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx (exp_qbs W (exp_qbs X Y))"
then have "(λ((r,w),x). α r w x) ∈ (borel⇩Q ⨂⇩Q W) ⨂⇩Q X →⇩Q Y"
by(auto simp: qbs_Mx_is_morphisms dest: uncurry_preserves_morphisms)
hence "(λ(r,w,x). α r w x) ∈ borel⇩Q ⨂⇩Q W ⨂⇩Q X →⇩Q Y"
by(auto intro!: qbs_morphism_cong'[where f="(λ((r,w),x). α r w x) ∘ (λ(x, y, z). ((x, y), z))" and g="λ(r,w,x). α r w x"] qbs_morphism_comp[OF qbs_morphism_pair_assoc2])
hence "(λ(r,x,w). α r w x) ∈ borel⇩Q ⨂⇩Q X ⨂⇩Q W →⇩Q Y"
by(auto intro!: qbs_morphism_cong'[where f="(λ(r,w,x). α r w x) ∘ map_prod id (λ(x,y). (y,x))" and g="(λ(r,x,w). α r w x)"] qbs_morphism_comp qbs_morphism_map_prod qbs_morphism_pair_swap)
hence "(λ((r,x),w). α r w x) ∈ (borel⇩Q ⨂⇩Q X) ⨂⇩Q W →⇩Q Y"
by(auto intro!: qbs_morphism_cong'[where f="(λ(r,x,w). α r w x) ∘ (λ((x, y), z). (x, y, z))" and g="λ((r,x),w). α r w x"] qbs_morphism_comp[OF qbs_morphism_pair_assoc1])
hence "(λr x w. α r w x) ∈ qbs_Mx (exp_qbs X (exp_qbs W Y))"
by(auto simp: qbs_Mx_is_morphisms split_beta')
from qbs_morphism_Mx[OF assms this] show "f ∘ α ∈ qbs_Mx Z"
by(auto simp: comp_def)
qed
lemma qbs_Mx_subset_of_measurable: "qbs_Mx X ⊆ borel →⇩M qbs_to_measure X"
proof
fix α
assume "α ∈ qbs_Mx X"
show "α ∈ borel →⇩M qbs_to_measure X"
proof(rule measurableI)
fix x
show "α x ∈ space (qbs_to_measure X)"
using qbs_Mx_to_X ‹α ∈ qbs_Mx X› by(simp add: space_L)
next
fix A
assume "A ∈ sets (qbs_to_measure X)"
then have "α -`(qbs_space X) = UNIV"
using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by(auto simp: sets_L)
then show "α -` A ∩ space borel ∈ sets borel"
using ‹α ∈ qbs_Mx X› ‹A ∈ sets (qbs_to_measure X)›
by(auto simp add: sigma_Mx_def sets_L)
qed
qed
lemma L_max_of_measurables:
assumes "space M = qbs_space X"
and "qbs_Mx X ⊆ borel →⇩M M"
shows "sets M ⊆ sets (qbs_to_measure X)"
proof
fix U
assume "U ∈ sets M"
from sets.sets_into_space[OF this] in_mono[OF assms(2)] measurable_sets_borel[OF _ this]
show "U ∈ sets (qbs_to_measure X)"
using assms(1)
by(auto intro!: exI[where x=U] simp: sigma_Mx_def sets_L)
qed
lemma qbs_Mx_are_measurable[simp,measurable]:
assumes "α ∈ qbs_Mx X"
shows "α ∈ borel →⇩M qbs_to_measure X"
using assms qbs_Mx_subset_of_measurable by auto
lemma measure_to_qbs_cong_sets:
assumes "sets M = sets N"
shows "measure_to_qbs M = measure_to_qbs N"
by(rule qbs_eqI) (simp add: qbs_Mx_R measurable_cong_sets[OF _ assms])
lemma lr_sets[simp]:
"sets X ⊆ sets (qbs_to_measure (measure_to_qbs X))"
unfolding sets_L
proof safe
fix U
assume "U ∈ sets X"
then have "U ∩ space X = U" by simp
moreover have "∀α∈borel →⇩M X. α -` U ∈ sets borel"
using ‹U ∈ sets X› by(auto simp add: measurable_def)
ultimately show "U ∈ sigma_Mx (measure_to_qbs X)"
by(auto simp add: sigma_Mx_def qbs_Mx_R qbs_space_R)
qed
lemma(in standard_borel) lr_sets_ident[simp, measurable_cong]:
"sets (qbs_to_measure (measure_to_qbs M)) = sets M"
unfolding sets_L
proof safe
fix V
assume "V ∈ sigma_Mx (measure_to_qbs M)"
then obtain U where H2: "V = U ∩ space M" "⋀α::real ⇒ _. α∈borel →⇩M M ⟹ α -` U ∈ sets borel"
by(auto simp: sigma_Mx_def qbs_Mx_R qbs_space_R)
consider "space M = {}" | "space M ≠ {}" by auto
then show "V ∈ sets M"
proof cases
case 1
then show ?thesis
by(simp add: H2)
next
case 2
have "from_real -` V = from_real -` (U ∩ space M)" using H2 by auto
also have "... = from_real -` U" using from_real_measurable'[OF 2] by(auto simp add: measurable_def)
finally have "to_real -` from_real -` U ∩ space M ∈ sets M"
by (meson "2" H2(2) from_real_measurable' measurable_sets to_real_measurable)
moreover have "to_real -` from_real -` U ∩ space M = U ∩ space M"
by auto
ultimately show ?thesis using H2 by simp
qed
qed(insert lr_sets, auto simp: sets_L)
corollary sets_lr_polish_borel[simp, measurable_cong]: "sets (qbs_to_measure qbs_borel) = sets (borel :: (_ :: polish_space) measure)"
by(auto intro!: standard_borel.lr_sets_ident standard_borel_ne.standard_borel)
corollary sets_lr_count_space[simp, measurable_cong]: "sets (qbs_to_measure (qbs_count_space (UNIV :: (_ :: countable) set))) = sets (count_space UNIV)"
by(rule standard_borel.lr_sets_ident) (auto intro!: standard_borel_ne.standard_borel)
lemma map_qbs_embed_measure1:
assumes "inj_on f (space M)"
shows "map_qbs f (measure_to_qbs M) = measure_to_qbs (embed_measure M f)"
proof(safe intro!: qbs_eqI)
fix α
show "α ∈ qbs_Mx (map_qbs f (measure_to_qbs M)) ⟹ α ∈ qbs_Mx (measure_to_qbs (embed_measure M f))"
using measurable_embed_measure2'[OF assms] by(auto intro!: qbs_eqI simp: map_qbs_Mx qbs_Mx_R)
next
fix α
assume "α ∈ qbs_Mx (measure_to_qbs (embed_measure M f))"
hence h[measurable]:"α ∈ borel →⇩M embed_measure M f"
by(simp add: qbs_Mx_R)
have [measurable]:"the_inv_into (space M) f ∈ embed_measure M f →⇩M M"
by (simp add: assms in_sets_embed_measure measurable_def sets.sets_into_space space_embed_measure the_inv_into_into the_inv_into_vimage)
show "α ∈ qbs_Mx (map_qbs f (measure_to_qbs M))"
using measurable_space[OF h] f_the_inv_into_f[OF assms] by(auto intro!: exI[where x="the_inv_into (space M) f ∘ α"] simp: map_qbs_Mx qbs_Mx_R space_embed_measure)
qed
lemma map_qbs_embed_measure2:
assumes "inj_on f (qbs_space X)"
shows "sets (qbs_to_measure (map_qbs f X)) = sets (embed_measure (qbs_to_measure X) f)"
proof safe
fix A
assume "A ∈ sets (qbs_to_measure (map_qbs f X))"
then obtain U where "A = U ∩ f ` qbs_space X" "⋀α. α ∈ qbs_Mx X ⟹ (f ∘ α) -` U ∈ sets borel"
by(auto simp: sets_L sigma_Mx_def map_qbs_space map_qbs_Mx)
thus "A ∈ sets (embed_measure (qbs_to_measure X) f)"
by(auto simp: sets_L sets_embed_measure'[of _ "qbs_to_measure X",simplified space_L,OF assms] sigma_Mx_def qbs_Mx_to_X vimage_def intro!: exI[where x="f -` U ∩ qbs_space X"])
next
fix A
assume A:"A ∈ sets (embed_measure (qbs_to_measure X) f)"
then obtain B U where "A = f ` B" "B = U ∩ qbs_space X" "⋀α. α ∈ qbs_Mx X ⟹ α -` U ∈ sets borel"
by(auto simp: sets_L sigma_Mx_def sets_embed_measure'[of _ "qbs_to_measure X",simplified space_L,OF assms])
thus "A ∈ sets (qbs_to_measure (map_qbs f X))"
using measurable_sets_borel[OF measurable_comp[OF qbs_Mx_are_measurable measurable_embed_measure2'[of _ "qbs_to_measure X",simplified space_L,OF assms]]] A
by(auto simp: sets_L sigma_Mx_def map_qbs_space map_qbs_Mx intro!: exI[where x="f ` (U ∩ qbs_space X)"])
qed
lemma(in standard_borel) map_qbs_embed_measure2':
assumes "inj_on f (space M)"
shows "sets (qbs_to_measure (map_qbs f (measure_to_qbs M))) = sets (embed_measure M f)"
by(auto intro!: standard_borel.lr_sets_ident[OF standard_borel_embed_measure] assms simp: map_qbs_embed_measure1[OF assms])
subsubsection ‹ The Adjunction ›
lemma lr_adjunction_correspondence :
"X →⇩Q (measure_to_qbs Y) = (qbs_to_measure X) →⇩M Y"
proof safe
fix f
assume "f ∈ X →⇩Q (measure_to_qbs Y)"
show "f ∈ qbs_to_measure X →⇩M Y"
proof(rule measurableI)
fix x
assume "x ∈ space (qbs_to_measure X)"
thus "f x ∈ space Y"
using qbs_morphism_space[OF ‹f ∈ X →⇩Q (measure_to_qbs Y)›]
by (auto simp: qbs_space_R space_L)
next
fix A
assume "A ∈ sets Y"
have "∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx (measure_to_qbs Y)"
using qbs_morphism_Mx[OF ‹f ∈ X →⇩Q (measure_to_qbs Y)›] by auto
hence "∀α ∈ qbs_Mx X. f ∘ α ∈ borel →⇩M Y" by (simp add: qbs_Mx_R)
hence "∀α ∈ qbs_Mx X. α -` (f -` A) ∈ sets borel"
using ‹A∈ sets Y› measurable_sets_borel vimage_comp by metis
thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
using sigma_Mx_def by (auto simp: space_L sets_L)
qed
next
fix f
assume "f ∈ qbs_to_measure X →⇩M Y"
show "f ∈ X →⇩Q measure_to_qbs Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx X"
have "f ∘ α ∈ borel →⇩M Y"
proof(rule measurableI)
fix x :: real
from ‹α ∈ qbs_Mx X› qbs_Mx_to_X have "α x ∈ qbs_space X" by auto
hence "α x ∈ space (qbs_to_measure X)" by (simp add: space_L)
thus "(f ∘ α) x ∈ space Y"
using ‹f ∈ qbs_to_measure X →⇩M Y›
by (metis comp_def measurable_space)
next
fix A
assume "A ∈ sets Y"
from ‹f ∈ qbs_to_measure X →⇩M Y› measurable_sets this measurable_def
have "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
by blast
hence "f -` A ∩ qbs_space X ∈ sigma_Mx X" by (simp add: sets_L space_L)
then have "∃V. f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets borel)"
by (simp add: sigma_Mx_def)
then obtain V where h:"f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets borel)" by auto
have 1:"α -` (f -` A) = α -` (f -` A ∩ qbs_space X)"
using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by blast
have 2:"α -` (V ∩ qbs_space X) = α -` V"
using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by blast
from 1 2 h have "(f ∘ α) -` A = α -` V" by (simp add: vimage_comp)
from this h ‹α ∈ qbs_Mx X ›show "(f ∘ α) -` A ∩ space borel ∈ sets borel" by simp
qed
thus "f ∘ α ∈ qbs_Mx (measure_to_qbs Y)"
by(simp add:qbs_Mx_R)
qed
qed
lemma(in standard_borel) standard_borel_r_full_faithful:
"M →⇩M Y = measure_to_qbs M →⇩Q measure_to_qbs Y"
proof
have "measure_to_qbs M →⇩Q measure_to_qbs Y ⊆ qbs_to_measure (measure_to_qbs M) →⇩M qbs_to_measure (measure_to_qbs Y)"
by (simp add: l_preserves_morphisms)
also have "... = M →⇩M qbs_to_measure (measure_to_qbs Y)"
using measurable_cong_sets by auto
also have "... ⊆ M →⇩M Y"
by(rule measurable_mono[OF lr_sets]) (simp_all add: qbs_space_R space_L)
finally show "measure_to_qbs M →⇩Q measure_to_qbs Y ⊆ M →⇩M Y" .
qed(rule r_preserves_morphisms)
lemma qbs_morphism_dest:
assumes "f ∈ X →⇩Q measure_to_qbs Y"
shows "f ∈ qbs_to_measure X →⇩M Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_dest:
assumes "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
shows "k ∈ M →⇩M Y"
using standard_borel_r_full_faithful assms by auto
lemma qbs_morphism_measurable_intro:
assumes "f ∈ qbs_to_measure X →⇩M Y"
shows "f ∈ X →⇩Q measure_to_qbs Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_measurable_intro:
assumes "k ∈ M →⇩M Y"
shows "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
using standard_borel_r_full_faithful assms by auto
lemma r_preserves_product :
"measure_to_qbs (X ⨂⇩M Y) = measure_to_qbs X ⨂⇩Q measure_to_qbs Y"
by(auto intro!: qbs_eqI simp: measurable_pair_iff pair_qbs_Mx qbs_Mx_R)
lemma l_product_sets:
"sets (qbs_to_measure X ⨂⇩M qbs_to_measure Y) ⊆ sets (qbs_to_measure (X ⨂⇩Q Y))"
proof(rule sets_pair_in_sets)
fix A B
assume h:"A ∈ sets (qbs_to_measure X)" "B ∈ sets (qbs_to_measure Y)"
then obtain Ua Ub where hu:
"A = Ua ∩ qbs_space X" "∀α∈qbs_Mx X. α -` Ua ∈ sets borel"
"B = Ub ∩ qbs_space Y" "∀α∈qbs_Mx Y. α -` Ub ∈ sets borel"
by(auto simp add: sigma_Mx_def sets_L)
show "A × B ∈ sets (qbs_to_measure (X ⨂⇩Q Y))"
proof -
have "A × B = Ua × Ub ∩ qbs_space (X ⨂⇩Q Y) ∧ (∀α∈qbs_Mx (X ⨂⇩Q Y). α -` (Ua × Ub) ∈ sets borel)"
using hu by(auto simp add: vimage_Times pair_qbs_space pair_qbs_Mx)
thus ?thesis
by(auto simp add: sigma_Mx_def sets_L intro!: exI[where x="Ua × Ub"])
qed
qed
corollary qbs_borel_prod: "qbs_borel ⨂⇩Q qbs_borel = (qbs_borel :: ('a::second_countable_topology × 'b::second_countable_topology) quasi_borel)"
by(simp add: r_preserves_product[symmetric] borel_prod)
corollary qbs_count_space_prod: "qbs_count_space (UNIV :: ('a :: countable) set) ⨂⇩Q qbs_count_space (UNIV :: ('b :: countable) set) = qbs_count_space UNIV"
by(auto simp: r_preserves_product[symmetric] count_space_prod)
lemma r_preserves_product': "measure_to_qbs (Π⇩M i∈I. M i) = (Π⇩Q i∈I. measure_to_qbs (M i))"
proof(rule qbs_eqI)
show "qbs_Mx (measure_to_qbs (Pi⇩M I M)) = qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
proof safe
fix f :: "real ⇒ _"
assume "f ∈ qbs_Mx (measure_to_qbs (Pi⇩M I M))"
with measurable_space[of f borel "Pi⇩M I M"] show "f ∈ qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
by(auto simp: qbs_Mx_R PiQ_Mx space_PiM intro!:ext[of "λr. f r _"])
next
fix f :: "real ⇒ _"
assume "f ∈ qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
then have "⋀i. i ∈ I ⟹ (λr. f r i) ∈ borel →⇩M M i" "⋀i. i ∉ I ⟹ (λr. f r i) = (λr. undefined)"
by (auto simp: qbs_Mx_R PiQ_Mx)
with measurable_space[OF this(1)] fun_cong[OF this(2)] show "f ∈ qbs_Mx (measure_to_qbs (Pi⇩M I M))"
by(auto intro!: measurable_PiM_single' simp: qbs_Mx_R)
qed
qed
lemma PiQ_qbs_borel:
"(Π⇩Q i::('a:: countable)∈UNIV. (qbs_borel :: ('b::second_countable_topology quasi_borel))) = qbs_borel"
by(simp add: r_preserves_product'[symmetric] measure_to_qbs_cong_sets[OF sets_PiM_equal_borel])
lemma qbs_morphism_from_countable:
fixes X :: "'a quasi_borel"
assumes "countable (qbs_space X)"
"qbs_Mx X ⊆ borel →⇩M count_space (qbs_space X)"
and "⋀i. i ∈ qbs_space X ⟹ f i ∈ qbs_space Y"
shows "f ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx X"
then have [measurable]: "α ∈ borel →⇩M count_space (qbs_space X)"
using assms(2) ..
define k :: "'a ⇒ real ⇒ _"
where "k ≡ (λi _. f i)"
have "f ∘ α = (λr. k (α r) r)"
by(auto simp add: k_def)
also have "... ∈ qbs_Mx Y"
by(rule qbs_closed3_dest2[OF assms(1)]) (use assms(3) k_def in simp_all)
finally show "f ∘ α ∈ qbs_Mx Y" .
qed
corollary qbs_morphism_count_space':
assumes "⋀i. i ∈ I ⟹ f i ∈ qbs_space Y" "countable I"
shows "f ∈ qbs_count_space I →⇩Q Y"
using assms by(auto intro!: qbs_morphism_from_countable simp: qbs_Mx_R)
corollary qbs_morphism_count_space:
assumes "⋀i. f i ∈ qbs_space Y"
shows "f ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q Y"
using assms by(auto intro!: qbs_morphism_from_countable simp: qbs_Mx_R)
lemma [qbs]:
shows not_qbs_pred: "Not ∈ qbs_count_space UNIV →⇩Q qbs_count_space UNIV"
and or_qbs_pred: "(∨) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and and_qbs_pred: "(∧) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and implies_qbs_pred: "(⟶) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and iff_qbs_pred: "(⟷) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
by(auto intro!: qbs_morphism_count_space)
lemma [qbs]:
shows less_count_qbs_pred: "(<) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and le_count_qbs_pred: "(≤) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and eq_count_qbs_pred: "(=) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and plus_count_qbs_morphism: "(+) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and minus_count_qbs_morphism: "(-) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and mult_count_qbs_morphism: "(*) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
and Suc_qbs_morphism: "Suc ∈ qbs_count_space UNIV →⇩Q qbs_count_space UNIV"
by(auto intro!: qbs_morphism_count_space)
lemma qbs_morphism_product_iff:
"f ∈ X →⇩Q (Π⇩Q i :: (_ :: countable)∈UNIV. Y) ⟷ f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
proof
assume h:"f ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
show "f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
by(rule arg_swap_morphism, rule qbs_morphism_count_space) (simp add: qbs_morphism_component_singleton'[OF h qbs_morphism_ident'])
next
assume "f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
from qbs_morphism_space[OF arg_swap_morphism[OF this]]
show "f ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
by(auto intro!: product_qbs_canonical1[where f="(λi x. f x i)"])
qed
lemma qbs_morphism_pair_countable1:
assumes "countable (qbs_space X)"
"qbs_Mx X ⊆ borel →⇩M count_space (qbs_space X)"
and "⋀i. i ∈ qbs_space X ⟹ f i ∈ Y →⇩Q Z"
shows "(λ(x,y). f x y) ∈ X ⨂⇩Q Y →⇩Q Z"
by(auto intro!: uncurry_preserves_morphisms qbs_morphism_from_countable[OF assms(1,2)] assms(3))
lemma qbs_morphism_pair_countable2:
assumes "countable (qbs_space Y)"
"qbs_Mx Y ⊆ borel →⇩M count_space (qbs_space Y)"
and "⋀i. i ∈ qbs_space Y ⟹ (λx. f x i) ∈ X →⇩Q Z"
shows "(λ(x,y). f x y) ∈ X ⨂⇩Q Y →⇩Q Z"
by(auto intro!: qbs_morphism_pair_swap[of "case_prod (λx y. f y x)",simplified] qbs_morphism_pair_countable1 assms)
corollary qbs_morphism_pair_count_space1:
assumes "⋀i. f i ∈ Y →⇩Q Z"
shows "(λ(x,y). f x y) ∈ qbs_count_space (UNIV :: ('a :: countable) set) ⨂⇩Q Y →⇩Q Z"
by(auto intro!: qbs_morphism_pair_countable1 simp: qbs_Mx_R assms)
corollary qbs_morphism_pair_count_space2:
assumes "⋀i. (λx. f x i) ∈ X →⇩Q Z"
shows "(λ(x,y). f x y) ∈ X ⨂⇩Q qbs_count_space (UNIV :: ('a :: countable) set) →⇩Q Z"
by(auto intro!: qbs_morphism_pair_countable2 simp: qbs_Mx_R assms)
lemma qbs_morphism_compose_countable':
assumes [qbs]:"⋀i. i ∈ I ⟹ (λx. f i x) ∈ X →⇩Q Y" "g ∈ X →⇩Q qbs_count_space I" "countable I"
shows "(λx. f (g x) x) ∈ X →⇩Q Y"
proof -
have [qbs]:"f ∈ qbs_count_space I →⇩Q X ⇒⇩Q Y"
by(auto intro!: qbs_morphism_count_space' simp: assms(3))
show ?thesis
by simp
qed
lemma qbs_morphism_compose_countable:
assumes [simp]:"⋀i::'i::countable. (λx. f i x) ∈ X →⇩Q Y" "g ∈ X →⇩Q (qbs_count_space UNIV)"
shows "(λx. f (g x) x) ∈ X →⇩Q Y"
by(rule qbs_morphism_compose_countable'[of UNIV f]) simp_all
lemma qbs_morphism_op:
assumes "case_prod f ∈ X ⨂⇩M Y →⇩M Z"
shows "f ∈ measure_to_qbs X →⇩Q measure_to_qbs Y ⇒⇩Q measure_to_qbs Z"
using r_preserves_morphisms assms
by(fastforce simp: r_preserves_product[symmetric] intro!: curry_preserves_morphisms)
lemma [qbs]:
shows plus_qbs_morphism: "(+) ∈ (qbs_borel :: (_::{second_countable_topology, topological_monoid_add}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and plus_ereal_qbs_morphism: "(+) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and diff_qbs_morphism: "(-) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_vector}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and diff_ennreal_qbs_morphism: "(-) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and diff_ereal_qbs_morphism: "(-) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and times_qbs_morphism: "(*) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_algebra}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and times_ennreal_qbs_morphism: "(*) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and times_ereal_qbs_morphism: "(*) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and divide_qbs_morphism: "(/) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_div_algebra}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and divide_ennreal_qbs_morphism: "(/) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and divide_ereal_qbs_morphism: "(/) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and log_qbs_morphism: "log ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and root_qbs_morphism: "root ∈ qbs_count_space UNIV →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and scaleR_qbs_morphism: "(*⇩R) ∈ qbs_borel →⇩Q (qbs_borel :: (_::{second_countable_topology, real_normed_vector}) quasi_borel) ⇒⇩Q qbs_borel"
and qbs_morphism_inner: "(∙) ∈ qbs_borel →⇩Q (qbs_borel :: (_::{second_countable_topology, real_inner}) quasi_borel) ⇒⇩Q qbs_borel"
and dist_qbs_morphism: "dist ∈ (qbs_borel :: (_::{second_countable_topology, metric_space}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and powr_qbs_morphism: "(powr) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q (qbs_borel :: real quasi_borel)"
and max_qbs_morphism: "(max :: (_ :: {second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and min_qbs_morphism: "(min :: (_ :: {second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and sup_qbs_morphism: "(sup :: (_ :: {lattice,second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and inf_qbs_morphism: "(inf :: (_ :: {lattice,second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
and less_qbs_pred: "(<) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
and eq_qbs_pred: "(=) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
and le_qbs_pred: "(≤) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
by(auto intro!: qbs_morphism_op)
lemma [qbs]:
shows abs_real_qbs_morphism: "abs ∈ (qbs_borel :: real quasi_borel) →⇩Q qbs_borel"
and abs_ereal_qbs_morphism: "abs ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel"
and real_floor_qbs_morphism: "(floor :: real ⇒ int) ∈ qbs_borel →⇩Q qbs_count_space UNIV"
and real_ceiling_qbs_morphism: "(ceiling :: real ⇒ int) ∈ qbs_borel →⇩Q qbs_count_space UNIV"
and exp_qbs_morphism: "(exp::'a::{real_normed_field,banach}⇒'a) ∈ qbs_borel →⇩Q qbs_borel"
and ln_qbs_morphism: "ln ∈ (qbs_borel :: real quasi_borel) →⇩Q qbs_borel"
and sqrt_qbs_morphism: "sqrt ∈ qbs_borel →⇩Q qbs_borel"
and of_real_qbs_morphism: "(of_real :: _ ⇒ (_::real_normed_algebra)) ∈ qbs_borel →⇩Q qbs_borel"
and sin_qbs_morphism: "(sin :: _ ⇒ (_::{real_normed_field,banach})) ∈ qbs_borel →⇩Q qbs_borel"
and cos_qbs_morphism: "(cos :: _ ⇒ (_::{real_normed_field,banach})) ∈ qbs_borel →⇩Q qbs_borel"
and arctan_qbs_morphism: "arctan ∈ qbs_borel →⇩Q qbs_borel"
and Re_qbs_morphism: "Re ∈ qbs_borel →⇩Q qbs_borel"
and Im_qbs_morphism: "Im ∈ qbs_borel →⇩Q qbs_borel"
and sgn_qbs_morphism: "(sgn::_::real_normed_vector ⇒ _) ∈ qbs_borel →⇩Q qbs_borel"
and norm_qbs_morphism: "norm ∈ qbs_borel →⇩Q qbs_borel"
and invers_qbs_morphism: "(inverse :: _ ⇒ (_ ::real_normed_div_algebra)) ∈ qbs_borel →⇩Q qbs_borel"
and invers_ennreal_qbs_morphism: "(inverse :: _ ⇒ ennreal) ∈ qbs_borel →⇩Q qbs_borel"
and invers_ereal_qbs_morphism: "(inverse :: _ ⇒ ereal) ∈ qbs_borel →⇩Q qbs_borel"
and uminus_qbs_morphism: "(uminus :: _ ⇒ (_::{second_countable_topology, real_normed_vector})) ∈ qbs_borel →⇩Q qbs_borel"
and ereal_qbs_morphism: "ereal ∈ qbs_borel →⇩Q qbs_borel"
and real_of_ereal_qbs_morphism: "real_of_ereal ∈ qbs_borel →⇩Q qbs_borel"
and enn2ereal_qbs_morphism: "enn2ereal ∈ qbs_borel →⇩Q qbs_borel"
and e2ennreal_qbs_morphism: "e2ennreal ∈ qbs_borel →⇩Q qbs_borel"
and ennreal_qbs_morphism: "ennreal ∈ qbs_borel →⇩Q qbs_borel"
and qbs_morphism_nth: "(λx::real^'n. x $ i) ∈ qbs_borel →⇩Q qbs_borel"
and qbs_morphism_product_candidate: "⋀i. (λx. x i) ∈ qbs_borel →⇩Q qbs_borel"
and uminus_ereal_qbs_morphism: "(uminus :: _ ⇒ ereal) ∈ qbs_borel →⇩Q qbs_borel"
by(auto intro!: set_mp[OF r_preserves_morphisms])
lemma qbs_morphism_sum:
fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, topological_comm_monoid_add}"
assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_suminf_order:
fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}"
assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
shows " (λx. ∑i. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_prod:
fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, real_normed_field}"
assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_Min:
"finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Min ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ X →⇩Q qbs_borel"
by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_Max:
"finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Max ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ X →⇩Q qbs_borel"
by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_Max2:
fixes f::"_ ⇒ _ ⇒ 'a::{second_countable_topology, dense_linorder, linorder_topology}"
shows "finite I ⟹ (⋀i. f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Max{f i x |i. i ∈ I}) ∈ X →⇩Q qbs_borel"
by(simp add: lr_adjunction_correspondence)
lemma [qbs]:
shows qbs_morphism_liminf: "liminf ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
and qbs_morphism_limsup: "limsup ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
and qbs_morphism_lim: "lim ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
proof(safe intro!: qbs_morphismI)
fix f :: "real ⇒ nat ⇒ 'a"
assume "f ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q borel⇩Q)"
then have [measurable]:"⋀i. (λr. f r i) ∈ borel_measurable borel"
by(auto simp: qbs_Mx_is_morphisms) (metis PiQ_qbs_borel measurable_product_then_coordinatewise qbs_Mx_is_morphisms qbs_Mx_qbs_borel qbs_morphism_product_iff)
show "liminf ∘ f ∈ qbs_Mx borel⇩Q" "limsup ∘ f ∈ qbs_Mx borel⇩Q" "lim ∘ f ∈ qbs_Mx borel⇩Q"
by(auto simp: qbs_Mx_is_morphisms lr_adjunction_correspondence comp_def)
qed
lemma qbs_morphism_SUP:
fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel"
shows "(λx. ⨆ i∈I. F i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_INF:
fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel"
shows "(λx. ⨅ i∈I. F i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_cSUP:
fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ bdd_above ((λi. F i x) ` I)"
shows "(λx. ⨆ i∈I. F i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence space_L)
lemma qbs_morphism_cINF:
fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ bdd_below ((λi. F i x) ` I)"
shows "(λx. ⨅ i∈I. F i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence space_L)
lemma qbs_morphism_lim_metric:
fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
shows "(λx. lim (λi. f i x)) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_LIMSEQ_metric:
fixes f :: "nat ⇒ 'a ⇒ 'b :: metric_space"
assumes "⋀i. f i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ (λi. f i x) ⇢ g x"
shows "g ∈ X →⇩Q qbs_borel"
using borel_measurable_LIMSEQ_metric[where M="qbs_to_measure X"] assms
by(auto simp add: lr_adjunction_correspondence space_L)
lemma power_qbs_morphism[qbs]:
"(power :: (_ ::{power,real_normed_algebra}) ⇒ nat ⇒ _) ∈ qbs_borel →⇩Q qbs_count_space UNIV ⇒⇩Q qbs_borel"
by(rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space set_mp[OF r_preserves_morphisms])
lemma power_ennreal_qbs_morphism[qbs]:
"(power :: ennreal ⇒ nat ⇒ _) ∈ qbs_borel →⇩Q qbs_count_space UNIV ⇒⇩Q qbs_borel"
by(rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space set_mp[OF r_preserves_morphisms])
lemma qbs_morphism_compw: "(^^) ∈ (X ⇒⇩Q X) →⇩Q qbs_count_space UNIV ⇒⇩Q (X ⇒⇩Q X)"
proof(rule arg_swap_morphism,rule qbs_morphism_count_space)
fix n
show "(λy. y ^^ n) ∈ X ⇒⇩Q X →⇩Q X ⇒⇩Q X"
by(induction n) simp_all
qed
lemma qbs_morphism_compose_n[qbs]:
assumes [qbs]: "f ∈ X →⇩Q X"
shows "(λn. f^^n) ∈ qbs_count_space UNIV →⇩Q X ⇒⇩Q X"
proof(intro qbs_morphism_count_space)
fix n
show "f ^^ n ∈ X →⇩Q X"
by (induction n) simp_all
qed
lemma qbs_morphism_compose_n':
assumes "f ∈ X →⇩Q X"
shows "f^^n ∈ X →⇩Q X"
using qbs_morphism_space[OF qbs_morphism_compose_n[OF assms]] by(simp add: exp_qbs_space qbs_space_R)
lemma qbs_morphism_uminus_eq_ereal[simp]:
"(λx. - f x :: ereal) ∈ X →⇩Q qbs_borel ⟷ f ∈ X →⇩Q qbs_borel" (is "?l = ?r")
by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_ereal_iff:
shows "(λx. ereal (f x)) ∈ X →⇩Q qbs_borel⟷ f ∈ X →⇩Q qbs_borel"
by(simp add: borel_measurable_ereal_iff lr_adjunction_correspondence)
lemma qbs_morphism_ereal_sum:
fixes f :: "'c ⇒ 'a ⇒ ereal"
assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_ereal_prod:
fixes f :: "'c ⇒ 'a ⇒ ereal"
assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_extreal_suminf:
fixes f :: "nat ⇒ 'a ⇒ ereal"
assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
shows "(λx. (∑i. f i x)) ∈ X →⇩Q qbs_borel"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_ennreal_iff:
assumes "⋀x. x ∈ qbs_space X ⟹ 0 ≤ f x"
shows "(λx. ennreal (f x)) ∈ X →⇩Q qbs_borel ⟷ f ∈ X →⇩Q qbs_borel"
using borel_measurable_ennreal_iff[where M="qbs_to_measure X"] assms
by(simp add: space_L lr_adjunction_correspondence)
lemma qbs_morphism_prod_ennreal:
fixes f :: "'c ⇒ 'a ⇒ ennreal"
assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
using assms by(simp add: space_L lr_adjunction_correspondence)
lemma count_space_qbs_morphism:
"f ∈ qbs_count_space (UNIV :: 'a set) →⇩Q qbs_borel"
by(auto intro!: set_mp[OF r_preserves_morphisms])
declare count_space_qbs_morphism[where 'a="_ :: countable",qbs]
lemma count_space_count_space_qbs_morphism:
"f ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q qbs_count_space (UNIV :: (_ :: countable) set)"
by(auto intro!: set_mp[OF r_preserves_morphisms])
lemma qbs_morphism_case_nat':
assumes [qbs]: "i = 0 ⟹ f ∈ X →⇩Q Y"
"⋀j. i = Suc j ⟹ (λx. g x j) ∈ X →⇩Q Y"
shows "(λx. case_nat (f x) (g x) i) ∈ X →⇩Q Y"
by (cases i) simp_all
lemma qbs_morphism_case_nat[qbs]:
"case_nat ∈ X →⇩Q (qbs_count_space UNIV ⇒⇩Q X) ⇒⇩Q qbs_count_space UNIV ⇒⇩Q X"
by(rule curry_preserves_morphisms, rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space qbs_morphism_case_nat')
lemma qbs_morphism_case_nat'':
assumes "f ∈ X →⇩Q Y" "g ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
shows "(λx. case_nat (f x) (g x)) ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
using assms by (simp add: qbs_morphism_product_iff)
lemma qbs_morphism_rec_nat[qbs]: "rec_nat ∈ X →⇩Q (count_space UNIV ⇒⇩Q X ⇒⇩Q X) ⇒⇩Q count_space UNIV ⇒⇩Q X"
proof(rule curry_preserves_morphisms,rule arg_swap_morphism,rule qbs_morphism_count_space)
fix n
show "(λy. rec_nat (fst y) (snd y) n) ∈ X ⨂⇩Q (qbs_count_space UNIV ⇒⇩Q X ⇒⇩Q X) →⇩Q X"
by (induction n) simp_all
qed
lemma qbs_morphism_Max_nat:
fixes P :: "nat ⇒ 'a ⇒ bool"
assumes "⋀i. P i ∈ X →⇩Q qbs_count_space UNIV"
shows "(λx. Max {i. P i x}) ∈ X →⇩Q qbs_count_space UNIV"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_Min_nat:
fixes P :: "nat ⇒ 'a ⇒ bool"
assumes "⋀i. P i ∈ X →⇩Q qbs_count_space UNIV"
shows "(λx. Min {i. P i x}) ∈ X →⇩Q qbs_count_space UNIV"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_sum_nat:
fixes f :: "'c ⇒ 'a ⇒ nat"
assumes "⋀i. i ∈ S ⟹ f i ∈X →⇩Q qbs_count_space UNIV"
shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_count_space UNIV"
using assms by(simp add: lr_adjunction_correspondence)
lemma qbs_morphism_case_enat':
assumes f[qbs]: "f ∈ X →⇩Q qbs_count_space UNIV" and [qbs]: "⋀i. g i ∈ X →⇩Q Y" "h ∈ X →⇩Q Y"
shows "(λx. case f x of enat i ⇒ g i x | ∞ ⇒ h x) ∈ X →⇩Q Y"
proof (rule qbs_morphism_compose_countable[OF _ f])
fix i
show "(λx. case i of enat i ⇒ g i x | ∞ ⇒ h x) ∈ X →⇩Q Y"
by (cases i) simp_all
qed
lemma qbs_morphism_case_enat[qbs]: "case_enat ∈ qbs_space ((qbs_count_space UNIV ⇒⇩Q X) ⇒⇩Q X ⇒⇩Q qbs_count_space UNIV ⇒⇩Q X)"
proof -
note qbs_morphism_case_enat'[qbs]
show ?thesis
by(auto intro!: curry_preserves_morphisms,rule qbs_morphismI) (simp add: qbs_Mx_is_morphisms comp_def, qbs, simp_all)
qed
lemma qbs_morphism_restrict[qbs]:
assumes X: "⋀i. i ∈ I ⟹ f i ∈ X →⇩Q (Y i)"
shows "(λx. λi∈I. f i x) ∈ X →⇩Q (Π⇩Q i∈I. Y i)"
using assms by(auto intro!: product_qbs_canonical1)
lemma If_qbs_morphism[qbs]: "If ∈ qbs_count_space UNIV →⇩Q X ⇒⇩Q X ⇒⇩Q X"
proof(rule qbs_morphismI)
show "α ∈ qbs_Mx (count_space⇩Q UNIV) ⟹ If ∘ α ∈ qbs_Mx (X ⇒⇩Q X ⇒⇩Q X)" for α
by(auto intro!: qbs_Mx_indicat[where S="{r. α (_ (_ r))}",simplified] simp: qbs_Mx_count_space exp_qbs_Mx)
qed
lemma normal_density_qbs[qbs]: "normal_density ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel ⇒⇩Q qbs_borel"
proof -
have [simp]:"normal_density = (λμ σ x. 1 / sqrt (2 * pi * σ⇧2) * exp (-(x - μ)⇧2/ (2 * σ⇧2)))"
by standard+ (auto simp: normal_density_def)
show ?thesis
by simp
qed
lemma erlang_density_qbs[qbs]: "erlang_density ∈ qbs_count_space UNIV →⇩Q qbs_borel ⇒⇩Q qbs_borel ⇒⇩Q qbs_borel"
proof -
have [simp]: "erlang_density = (λk l x. (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k))"
by standard+ (auto simp: erlang_density_def)
show ?thesis
by simp
qed
lemma list_nil_qbs[qbs]: "[] ∈ qbs_space (list_qbs X)"
by(simp add: list_qbs_space)
lemma list_cons_qbs_morphism: "list_cons ∈ X →⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⇒⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
proof(intro curry_preserves_morphisms pair_qbs_morphismI)
fix α β
assume h:"α ∈ qbs_Mx X"
"β ∈ qbs_Mx (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
then obtain γ f where hf:
"β = (λr. (f r, γ (f r) r))" "f ∈ borel →⇩M count_space UNIV" "⋀i. i ∈ range f ⟹ γ i ∈ qbs_Mx (Π⇩Q j∈{..<i}. X)"
by(auto simp: coPiQ_Mx_def coPiQ_Mx)
define f' β'
where "f' ≡ (λr. Suc (f r))" "β' ≡ (λi r n. if n = 0 then α r else γ (i - 1) r (n - 1))"
then have "(λr. list_cons (fst (α r, β r)) (snd (α r, β r))) = (λr. (f' r, β' (f' r) r))"
by(auto simp: comp_def hf(1) ext list_cons_def)
also have "... ∈ qbs_Mx (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
proof(rule coPiQ_MxI)
show "f' ∈ borel →⇩M count_space UNIV"
using hf by(simp add: f'_β'_def(1))
next
fix j
assume hj:"j ∈ range f'"
then have hj':"j - 1 ∈ range f"
by(auto simp: f'_β'_def(1))
show "β' j ∈ qbs_Mx (Π⇩Q i∈{..<j}. X)"
proof(rule prod_qbs_MxI)
fix i
assume hi:"i ∈ {..<j}"
then consider "i = 0" | "0 < i" "i < j"
by auto
then show "(λr. β' j r i) ∈ qbs_Mx X"
proof cases
case 1
then show ?thesis by(simp add: h(1) f'_β'_def(2))
next
case 2
then have "i - 1 ∈ {..<j - 1}" by simp
from prod_qbs_MxD(1)[OF hf(3)[OF hj'] this] 2
show ?thesis
by(simp add: f'_β'_def(2))
qed
next
fix i
assume hi:"i ∉ {..<j}"
then have "i ≠ 0" "i - Suc 0 ∉ {..<j - Suc 0}"
using f'_β'_def(1) hj by fastforce+
with prod_qbs_MxD(2)[OF hf(3)[OF hj']]
show "(λr. β' j r i) = (λr. undefined)"
by(simp add: f'_β'_def(2))
qed
qed
finally show "(λr. list_cons (fst (α r, β r)) (snd (α r, β r))) ∈ qbs_Mx (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)" .
qed
corollary cons_qbs_morphism[qbs]: "Cons ∈ X →⇩Q (list_qbs X) ⇒⇩Q list_qbs X"
proof(rule arg_swap_morphism)
show "(λx y. y # x) ∈ list_qbs X →⇩Q X ⇒⇩Q list_qbs X"
proof(rule qbs_morphism_cong')
show " (λl x. x # to_list l) ∘ from_list ∈ list_qbs X →⇩Q X ⇒⇩Q list_qbs X"
proof(rule qbs_morphism_comp)
show " (λl x. x # to_list l) ∈ (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) →⇩Q X ⇒⇩Q list_qbs X"
proof(rule curry_preserves_morphisms)
show "(λlx. snd lx # to_list (fst lx)) ∈ (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q X →⇩Q list_qbs X"
proof(rule qbs_morphism_cong')
show "to_list ∘ (λ(l, x). from_list (x # to_list l)) ∈ (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q X →⇩Q list_qbs X"
proof(rule qbs_morphism_comp)
show "(λ(l, x). from_list (x # to_list l)) ∈(⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q X →⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
by(rule qbs_morphism_cong'[OF _ uncurry_preserves_morphisms[of "λ(l,x). list_cons x l",simplified,OF arg_swap_morphism[OF list_cons_qbs_morphism]]]) (auto simp: pair_qbs_space to_list_from_list_ident)
qed(simp add: list_qbs_def map_qbs_morphism_f)
qed(auto simp: pair_qbs_space to_list_from_list_ident to_list_simp2)
qed
qed(auto simp: list_qbs_def to_list_from_list_ident intro!: map_qbs_morphism_inverse_f)
qed(simp add: from_list_to_list_ident)
qed
lemma rec_list_morphism':
"rec_list' ∈ qbs_space (Y ⇒⇩Q (X ⇒⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⇒⇩Q Y)"
proof(intro curry_preserves_morphisms[OF arg_swap_morphism] coPiQ_canonical1')
fix n
show "(λx y. rec_list' (fst y) (snd y) (n, x)) ∈ (Π⇩Q i∈{..<n}. X) →⇩Q exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) Y"
proof(induction n)
case 0
show ?case
proof(rule curry_preserves_morphisms[OF qbs_morphismI])
fix α
assume h:"α ∈ qbs_Mx ((Π⇩Q i∈{..<0::nat}. X) ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n::nat}. X) (exp_qbs Y Y)))"
have "⋀r. fst (α r) = (λn. undefined)"
proof -
fix r
have "⋀i. (λr. fst (α r) i) = (λr. undefined)"
using h by(auto simp: exp_qbs_Mx PiQ_Mx pair_qbs_Mx comp_def split_beta')
thus "fst (α r) = (λn. undefined)"
by(fastforce dest: fun_cong)
qed
hence "(λxy. rec_list' (fst (snd xy)) (snd (snd xy)) (0, fst xy)) ∘ α = (λx. fst (snd (α x)))"
by(auto simp: rec_list'_simp1[simplified list_nil_def] comp_def split_beta')
also have "... ∈ qbs_Mx Y"
using h by(auto simp: pair_qbs_Mx comp_def)
finally show "(λxy. rec_list' (fst (snd xy)) (snd (snd xy)) (0, fst xy)) ∘ α ∈ qbs_Mx Y" .
qed
next
case ih:(Suc n)
show ?case
proof(rule qbs_morphismI)
fix α
assume h:"α ∈ qbs_Mx (Π⇩Q i∈{..<Suc n}. X)"
define α' where "α' ≡ (λr. snd (list_tail (Suc n, α r)))"
define a where "a ≡ (λr. α r 0)"
then have ha:"a ∈ qbs_Mx X"
using h by(auto simp: PiQ_Mx)
have 1:"α' ∈ qbs_Mx (Π⇩Q i∈{..<n}. X)"
using h by(fastforce simp: PiQ_Mx list_tail_def α'_def)
hence 2: "⋀r. (n, α' r) ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using qbs_Mx_to_X[of α'] by (fastforce simp: PiQ_space coPiQ_space)
have 3: "⋀r. (Suc n, α r) ∈ qbs_space (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using qbs_Mx_to_X[of α] h by (fastforce simp: PiQ_space coPiQ_space)
have 4: "⋀r. (n, α' r) = list_tail (Suc n, α r)"
by(simp add: list_tail_def α'_def)
have 5: "⋀r. (Suc n, α r) = list_cons (a r) (n, α' r)"
unfolding a_def by(simp add: list_simp5[OF 3,simplified 4[symmetric],simplified list_head_def list_cons_def list_nil_def] list_cons_def) auto
have 6: "(λr. (n, α' r)) ∈ qbs_Mx (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using 1 by(auto intro!: coPiQ_MxI simp: PiQ_space coPiQ_space)
have "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) ∘ α = (λr y. rec_list' (fst y) (snd y) (Suc n, α r))"
by auto
also have "... = (λr y. snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r)))"
by(simp only: 5 rec_list'_simp2[OF 2])
also have "... ∈ qbs_Mx (exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) Y)"
proof -
have "(λ(r,y). snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r))) = (λ(y,x1,x2,x3). y x1 x2 x3) ∘ (λ(r,y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r)))"
by auto
also have "... ∈ qbs_borel ⨂⇩Q (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) →⇩Q Y"
proof(rule qbs_morphism_comp[where Y="exp_qbs X (exp_qbs (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q Y"])
show "(λ(r, y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r))) ∈ qbs_borel ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) →⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q Y"
unfolding split_beta'
proof(safe intro!: qbs_morphism_Pair)
show "(λx. a (fst x)) ∈ qbs_borel ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) →⇩Q X"
using ha qbs_Mx_is_morphisms[of X] ha by auto
next
show "(λx. (n, α' (fst x))) ∈ qbs_borel ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) →⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"
using 6 by(simp add: qbs_Mx_is_morphisms) (use fst_qbs_morphism qbs_morphism_compose in blast)
next
show "(λx. rec_list' (fst (snd x)) (snd (snd x)) (n, α' (fst x))) ∈ qbs_borel ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) →⇩Q Y"
using qbs_morphism_Mx[OF ih 1, simplified comp_def] uncurry_preserves_morphisms[of "(λ(x,y). rec_list' (fst y) (snd y) (n, α' x))" qbs_borel "Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y))" Y] qbs_Mx_is_morphisms[of "exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y))) Y"]
by(fastforce simp: split_beta')
qed qbs
next
show "(λ(y, x1, x2, x3). y x1 x2 x3) ∈ exp_qbs X (exp_qbs ((⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) ⨂⇩Q Y →⇩Q Y"
by simp
qed
finally show ?thesis
by(simp add: exp_qbs_Mx')
qed
finally show "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) ∘ α ∈ qbs_Mx (exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) Y)"
by blast
qed
qed
qed simp
lemma rec_list_morphism[qbs]: "rec_list ∈ qbs_space (Y ⇒⇩Q (X ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y)"
proof(rule curry_preserves_morphisms[OF arg_swap_morphism])
show "(λl yf. rec_list (fst yf) (snd yf) l) ∈ list_qbs X →⇩Q Y ⨂⇩Q (X ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q Y"
proof(rule qbs_morphism_cong'[where f="(λl' (y,f). rec_list y f (to_list l')) ∘ from_list",OF _ qbs_morphism_comp[where Y="(⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X)"]])
show "(λl' (y,f). rec_list y f (to_list l')) ∈ (⨿⇩Q n∈(UNIV :: nat set).Π⇩Q i∈{..<n}. X) →⇩Q Y ⨂⇩Q (X ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q Y"
apply(rule arg_swap_morphism,simp only: split_beta' list_qbs_def)
apply(rule uncurry_preserves_morphisms)
apply(rule arg_swap_morphism)
apply(rule arg_swap_morphism')
apply(rule qbs_morphism_cong'[OF _ arg_swap_morphism_map_qbs1[OF arg_swap_morphism'[OF arg_swap_morphism[OF rec_list_morphism']]]])
apply(auto simp: rec_list'_def from_list_to_list_ident)
done
qed(auto simp: from_list_to_list_ident list_qbs_def to_list_from_list_ident intro!: map_qbs_morphism_inverse_f)
qed
hide_const (open) list_nil list_cons list_head list_tail from_list rec_list' to_list'
hide_fact (open) list_simp1 list_simp2 list_simp3 list_simp4 list_simp5 list_simp6 list_simp7 from_list_in_list_of' list_cons_qbs_morphism rec_list'_simp1
to_list_from_list_ident from_list_in_list_of to_list_set to_list_simp1 to_list_simp2 list_head_def list_tail_def from_list_length
list_cons_in_list_of rec_list_morphism' rec_list'_simp2 list_decomp1 list_destruct_rule list_induct_rule from_list_to_list_ident
corollary case_list_morphism[qbs]: "case_list ∈ qbs_space ((Y :: 'b quasi_borel) ⇒⇩Q ((X :: 'a quasi_borel) ⇒⇩Q list_qbs X ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y)"
proof -
have [simp]:"case_list = (λy (f :: 'a ⇒ 'a list ⇒ 'b) l. rec_list y (λx l' y. f x l') l)"
proof standard+
fix y :: 'b and f :: "'a ⇒ 'a list ⇒ 'b" and l :: "'a list"
show "(case l of [] ⇒ y | x # xa ⇒ f x xa) = rec_list y (λx l' y. f x l') l"
by (cases l) auto
qed
show ?thesis
by simp
qed
lemma fold_qbs_morphism[qbs]: "fold ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y)"
proof -
have [simp]:"fold = (λf l. rec_list id (λx xs l. l ∘ f x) l)"
apply standard+
subgoal for f l x
by(induction l arbitrary: x) simp_all
done
show ?thesis
by simp
qed
lemma [qbs]:
shows foldr_qbs_morphism: "foldr ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y)"
and foldl_qbs_morphism: "foldl ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q X) ⇒⇩Q X ⇒⇩Q list_qbs Y ⇒⇩Q X)"
and zip_qbs_morphism: "zip ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs Y ⇒⇩Q list_qbs (pair_qbs X Y))"
and append_qbs_morphism: "append ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
and concat_qbs_morphism: "concat ∈ qbs_space (list_qbs (list_qbs X) ⇒⇩Q list_qbs X)"
and drop_qbs_morphism: "drop ∈ qbs_space (qbs_count_space UNIV ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
and take_qbs_morphism: "take ∈ qbs_space (qbs_count_space UNIV ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
and rev_qbs_morphism: "rev ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X)"
by(auto simp: foldr_def foldl_def zip_def append_def concat_def drop_def take_def rev_def)
lemma [qbs]:
fixes X :: "'a quasi_borel" and Y :: "'b quasi_borel"
shows map_qbs_morphism: "map ∈ qbs_space ((X ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs Y)" (is ?map)
and fileter_qbs_morphism: "filter ∈ qbs_space ((X ⇒⇩Q count_space⇩Q UNIV) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?filter)
and length_qbs_morphism: "length ∈ qbs_space (list_qbs X ⇒⇩Q qbs_count_space UNIV)" (is ?length)
and tl_qbs_morphism: "tl ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X)" (is ?tl)
and list_all_qbs_morphism: "list_all ∈ qbs_space ((X ⇒⇩Q qbs_count_space UNIV) ⇒⇩Q list_qbs X ⇒⇩Q qbs_count_space UNIV)" (is ?list_all)
and bind_list_qbs_morphism: "(⤜) ∈ qbs_space (list_qbs X ⇒⇩Q (X ⇒⇩Q list_qbs Y) ⇒⇩Q list_qbs Y)" (is ?bind)
proof -
have [simp]: "map = (λf. rec_list [] (λx xs l. f x # l))"
apply standard+
subgoal for f l
by(induction l) simp_all
done
have [simp]: "filter = (λP. rec_list [] (λx xs l. if P x then x # l else l))"
apply standard+
subgoal for f l
by(induction l) simp_all
done
have [simp]: "length = (λl. foldr (λ_ n. Suc n) l 0)"
apply standard
subgoal for l
by (induction l) simp_all
done
have [simp]: "tl = (λl. case l of [] ⇒ [] | _ # xs ⇒ xs)"
by standard (simp add: tl_def)
have [simp]: "list_all = (λP xs. foldr (λx b. b ∧ P x) xs True)"
apply (standard,standard)
subgoal for P xs
by(induction xs arbitrary: P) auto
done
have [simp]: "List.bind = (λxs f. concat (map f xs))"
by standard+ (simp add: List.bind_def)
show ?map ?filter ?length ?tl ?list_all ?bind
by simp_all
qed
lemma list_eq_qbs_morphism[qbs]:
assumes [qbs]: "(=) ∈ qbs_space (X ⇒⇩Q X ⇒⇩Q count_space UNIV)"
shows "(=) ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X ⇒⇩Q count_space UNIV)"
proof -
have [simp]:"(=) = (λxs ys. length xs = length ys ∧ list_all (case_prod (=)) (zip xs ys))"
using Ball_set list_eq_iff_zip_eq by fastforce
show ?thesis
by simp
qed
lemma insort_key_qbs_morphism[qbs]:
shows "insort_key ∈ qbs_space ((X ⇒⇩Q (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel)) ⇒⇩Q X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?g1)
and "insort_key ∈ qbs_space ((X ⇒⇩Q count_space⇩Q (UNIV :: (_ :: countable) set)) ⇒⇩Q X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?g2)
proof -
have [simp]:"insort_key = (λf x. rec_list [x] (λy ys l. if f x ≤ f y then x#y#ys else y#l))"
apply standard+
subgoal for f x l
by(induction l) simp_all
done
show ?g1 ?g2
by simp_all
qed
lemma sort_key_qbs_morphism[qbs]:
shows "sort_key ∈ qbs_space ((X ⇒⇩Q (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel)) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
and "sort_key ∈ qbs_space ((X ⇒⇩Q count_space⇩Q (UNIV :: (_ :: countable) set)) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
unfolding sort_key_def by simp_all
lemma sort_qbs_morphism[qbs]:
shows "sort ∈ list_qbs (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel) →⇩Q list_qbs borel⇩Q"
and "sort ∈ list_qbs (count_space⇩Q (UNIV :: (_ :: countable) set)) →⇩Q list_qbs (count_space⇩Q UNIV)"
by simp_all
subsubsection ‹ Morphism Pred›
abbreviation "qbs_pred X P ≡ P ∈ X →⇩Q qbs_count_space (UNIV :: bool set)"
lemma qbs_pred_iff_measurable_pred:
"qbs_pred X P = Measurable.pred (qbs_to_measure X) P"
by(simp add: lr_adjunction_correspondence)
lemma(in standard_borel) qbs_pred_iff_measurable_pred:
"qbs_pred (measure_to_qbs M) P = Measurable.pred M P"
by(simp add: qbs_pred_iff_measurable_pred measurable_cong_sets[OF lr_sets_ident refl])
lemma qbs_pred_iff_sets:
"{x ∈space (qbs_to_measure X). P x} ∈ sets (qbs_to_measure X) ⟷ qbs_pred X P"
by (simp add: Measurable.pred_def lr_adjunction_correspondence space_L)
lemma
assumes [qbs]:"P ∈ X →⇩Q Y ⇒⇩Q qbs_count_space UNIV" "f ∈ X →⇩Q Y"
shows indicator_qbs_morphism''': "(λx. indicator {y. P x y} (f x)) ∈ X →⇩Q qbs_borel" (is ?g1)
and indicator_qbs_morphism'': "(λx. indicator {y∈qbs_space Y. P x y} (f x)) ∈ X →⇩Q qbs_borel" (is ?g2)
proof -
have [simp]:"{x ∈ qbs_space X. P x (f x)} = {x ∈ qbs_space X. f x ∈ qbs_space Y ∧ P x (f x)}"
using qbs_morphism_space[OF assms(2)] by blast
show ?g1 ?g2
using qbs_morphism_app[OF assms,simplified qbs_pred_iff_sets[symmetric]] qbs_morphism_space[OF assms(2)]
by(auto intro!: borel_measurable_indicator' simp: lr_adjunction_correspondence space_L)
qed
lemma
assumes [qbs]:"P ∈ X →⇩Q Y ⇒⇩Q qbs_count_space UNIV"
shows indicator_qbs_morphism[qbs]:"(λx. indicator {y ∈ qbs_space Y. P x y}) ∈ X →⇩Q Y ⇒⇩Q qbs_borel" (is ?g1)
and indicator_qbs_morphism':"(λx. indicator {y. P x y}) ∈ X →⇩Q Y ⇒⇩Q qbs_borel" (is ?g2)
proof -
note indicator_qbs_morphism''[qbs] indicator_qbs_morphism'''[qbs]
show ?g1 ?g2
by(auto intro!: curry_preserves_morphisms[OF pair_qbs_morphismI] simp: qbs_Mx_is_morphisms)
qed
lemma indicator_qbs[qbs]:
assumes "qbs_pred X P"
shows "indicator {x. P x} ∈ X →⇩Q qbs_borel"
using assms by(auto simp: lr_adjunction_correspondence)
lemma All_qbs_pred[qbs]: "qbs_pred (count_space⇩Q (UNIV :: ('a :: countable) set) ⇒⇩Q count_space⇩Q UNIV) All"
proof(rule qbs_morphismI)
fix a :: "real ⇒ 'a ⇒ bool"
assume "a ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q count_space⇩Q UNIV)"
hence [measurable]: "⋀f g. f ∈ borel_measurable borel ⟹ g ∈ borel →⇩M count_space UNIV ⟹ (λx::real. a (f x) (g x)) ∈ borel →⇩M count_space UNIV"
by(auto simp add: exp_qbs_Mx qbs_Mx_R)
show " All ∘ a ∈ qbs_Mx (count_space⇩Q UNIV)"
by(simp add: comp_def qbs_Mx_R)
qed
lemma Ex_qbs_pred[qbs]: "qbs_pred (count_space⇩Q (UNIV :: ('a :: countable) set) ⇒⇩Q count_space⇩Q UNIV) Ex"
proof(rule qbs_morphismI)
fix a :: "real ⇒ 'a ⇒ bool"
assume "a ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q count_space⇩Q UNIV)"
hence [measurable]: "⋀f g. f ∈ borel_measurable borel ⟹ g ∈ borel →⇩M count_space UNIV ⟹ (λx::real. a (f x) (g x)) ∈ borel →⇩M count_space UNIV"
by(auto simp add: exp_qbs_Mx qbs_Mx_R)
show "Ex ∘ a ∈ qbs_Mx (count_space⇩Q UNIV)"
by(simp add: comp_def qbs_Mx_R)
qed
lemma Ball_qbs_pred_countable:
assumes "⋀i::'a :: countable. i ∈ I ⟹ qbs_pred X (P i)"
shows "qbs_pred X (λx. ∀x∈I. P i x)"
using assms by(simp add: qbs_pred_iff_measurable_pred)
lemma Ball_qbs_pred:
assumes "finite I" "⋀i. i ∈ I ⟹ qbs_pred X (P i)"
shows "qbs_pred X (λx. ∀x∈I. P i x)"
using assms by(simp add: qbs_pred_iff_measurable_pred)
lemma Bex_qbs_pred_countable:
assumes "⋀i::'a :: countable. i ∈ I ⟹ qbs_pred X (P i)"
shows "qbs_pred X (λx. ∃x∈I. P i x)"
using assms by(simp add: qbs_pred_iff_measurable_pred)
lemma Bex_qbs_pred:
assumes "finite I" "⋀i. i ∈ I ⟹ qbs_pred X (P i)"
shows "qbs_pred X (λx. ∃x∈I. P i x)"
using assms by(simp add: qbs_pred_iff_measurable_pred)
lemma qbs_morphism_If_sub_qbs:
assumes [qbs]: "qbs_pred X P"
and [qbs]: "f ∈ sub_qbs X {x∈qbs_space X. P x} →⇩Q Y" "g ∈ sub_qbs X {x∈qbs_space X. ¬ P x} →⇩Q Y"
shows "(λx. if P x then f x else g x) ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume h:"α ∈ qbs_Mx X"
interpret standard_borel_ne "borel :: real measure" by simp
have [measurable]: "Measurable.pred borel (λx. P (α x))"
using h by(simp add: qbs_pred_iff_measurable_pred[symmetric] qbs_Mx_is_morphisms)
consider "qbs_space X = {}"
| "{x∈qbs_space X. ¬ P x} = qbs_space X"
| "{x∈qbs_space X. P x} = qbs_space X"
| "{x∈qbs_space X. P x} ≠ {}" "{x∈qbs_space X. ¬ P x} ≠ {}" by blast
then show "(λx. if P x then f x else g x) ∘ α ∈ qbs_Mx Y" (is "?f ∈ _")
proof cases
case 1
with h show ?thesis
by(simp add: qbs_empty_equiv)
next
case 2
have [simp]:"(λx. if P x then f x else g x) ∘ α = g ∘ α"
by standard (use qbs_Mx_to_X[OF h] 2 in auto)
show ?thesis
using 2 qbs_morphism_Mx[OF assms(3)] h by(simp add: sub_qbs_ident)
next
case 3
have [simp]:"(λx. if P x then f x else g x) ∘ α = f ∘ α"
by standard (use qbs_Mx_to_X[OF h] 3 in auto)
show ?thesis
using 3 qbs_morphism_Mx[OF assms(2)] h by(simp add: sub_qbs_ident)
next
case 4
then obtain x0 x1 where
x0:"x0 ∈ qbs_space X" "P x0" and x1:"x1 ∈ qbs_space X" "¬ P x1"
by blast
define a0 where "a0 = (λr. if P (α r) then α r else x0)"
define a1 where "a1 = (λr. if ¬ P (α r) then α r else x1)"
have "a0 ∈ qbs_Mx (sub_qbs X {x∈qbs_space X. P x})" "a1 ∈ qbs_Mx (sub_qbs X {x∈qbs_space X. ¬ P x})"
using x0 x1 qbs_Mx_to_X[OF h] h
by(auto simp: sub_qbs_Mx a0_def a1_def intro!: qbs_closed3_dest2'[of UNIV "λr. P (α r)" "λb r. if b then α r else x0"]) (simp_all add: qbs_Mx_is_morphisms)
from qbs_morphism_Mx[OF assms(2) this(1)] qbs_morphism_Mx[OF assms(3) this(2)]
have h0:"(λr. f (a0 r)) ∈ qbs_Mx Y" "(λr. g (a1 r)) ∈ qbs_Mx Y"
by (simp_all add: comp_def)
have [simp]:"(λx. if P x then f x else g x) ∘ α = (λr. if P (α r) then f (a0 r) else g (a1 r))"
by standard (auto simp: comp_def a0_def a1_def)
show "(λx. if P x then f x else g x) ∘ α ∈ qbs_Mx Y"
using h h0 by(simp add: qbs_Mx_is_morphisms)
qed
qed
subsubsection ‹ The Adjunction w.r.t. Ordering›
lemma l_mono: "mono qbs_to_measure"
proof
fix X Y :: "'a quasi_borel"
show "X ≤ Y ⟹ qbs_to_measure X ≤ qbs_to_measure Y"
proof(induction rule: less_eq_quasi_borel.induct)
case (1 X Y)
then show ?case
by(simp add: less_eq_measure.intros(1) space_L)
next
case (2 X Y)
then have "sigma_Mx X ⊆ sigma_Mx Y"
by(auto simp add: sigma_Mx_def)
then consider "sigma_Mx X ⊂ sigma_Mx Y" | "sigma_Mx X = sigma_Mx Y"
by auto
then show ?case
apply(cases)
apply(rule less_eq_measure.intros(2))
apply(simp_all add: 2 space_L sets_L)
by(rule less_eq_measure.intros(3),simp_all add: 2 sets_L space_L emeasure_L)
qed
qed
lemma r_mono: "mono measure_to_qbs"
proof
fix M N :: "'a measure"
show "M ≤ N ⟹ measure_to_qbs M ≤ measure_to_qbs N"
proof(induction rule: less_eq_measure.inducts)
case (1 M N)
then show ?case
by(simp add: less_eq_quasi_borel.intros(1) qbs_space_R)
next
case (2 M N)
then have "(borel :: real measure) →⇩M N ⊆ borel →⇩M M"
by(simp add: measurable_mono)
then consider "(borel :: real measure) →⇩M N ⊂ borel →⇩M M" | "(borel :: real measure) →⇩M N = borel →⇩M M"
by auto
then show ?case
by cases (rule less_eq_quasi_borel.intros(2),simp_all add: 2 qbs_space_R qbs_Mx_R)+
next
case (3 M N)
then show ?case
apply -
by(rule less_eq_quasi_borel.intros(2)) (simp_all add: measurable_mono qbs_space_R qbs_Mx_R)
qed
qed
lemma rl_order_adjunction:
"X ≤ qbs_to_measure Y ⟷ measure_to_qbs X ≤ Y"
proof
assume 1: "X ≤ qbs_to_measure Y"
then show "measure_to_qbs X ≤ Y"
proof(induction rule: less_eq_measure.cases)
case (1 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 1(2)[symmetric] space_L)
show ?case
by(rule less_eq_quasi_borel.intros(1),simp add: 1 qbs_space_R)
next
case (2 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 2(2)[symmetric] space_L)
show ?case
proof(rule less_eq_quasi_borel.intros(2))
show "qbs_Mx Y ⊆ qbs_Mx (measure_to_qbs X)"
unfolding qbs_Mx_R
proof
fix α
assume h:"α ∈ qbs_Mx Y"
show "α ∈ borel →⇩M X"
proof(rule measurableI)
show "⋀x. α x ∈ space X"
using qbs_Mx_to_X[OF h] by (auto simp add: 2)
next
fix A
assume "A ∈ sets X"
then have "A ∈ sets (qbs_to_measure Y)"
using 2 by auto
then obtain U where
hu:"A = U ∩ space N" "(∀α∈qbs_Mx Y. α -` U ∈ sets borel)"
by(auto simp add: sigma_Mx_def sets_L)
have "α -` A = α -` U"
using qbs_Mx_to_X[OF h] by(auto simp add: hu)
thus "α -` A ∩ space borel ∈ sets borel"
using h hu(2) by simp
qed
qed
qed(auto simp: 2 qbs_space_R)
next
case (3 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 3(2)[symmetric] space_L)
show ?case
proof(rule less_eq_quasi_borel.intros(2))
show "qbs_Mx Y ⊆ qbs_Mx (measure_to_qbs X)"
unfolding qbs_Mx_R
proof
fix α
assume h:"α ∈ qbs_Mx Y"
show "α ∈ borel →⇩M X"
proof(rule measurableI)
show "⋀x. α x ∈ space X"
using qbs_Mx_to_X[OF h] by(auto simp: 3)
next
fix A
assume "A ∈ sets X"
then have "A ∈ sets (qbs_to_measure Y)"
using 3 by auto
then obtain U where
hu:"A = U ∩ space N" "(∀α∈qbs_Mx Y. α -` U ∈ sets borel)"
by(auto simp add: sigma_Mx_def sets_L)
have "α -` A = α -` U"
using qbs_Mx_to_X[OF h] by(auto simp add: hu)
thus "α -` A ∩ space borel ∈ sets borel"
using h hu(2) by simp
qed
qed
qed(auto simp: 3 qbs_space_R)
qed
next
assume "measure_to_qbs X ≤ Y"
then show "X ≤ qbs_to_measure Y"
proof(induction rule: less_eq_quasi_borel.cases)
case (1 A B)
have [simp]: "space X = qbs_space A"
by(simp add: 1(1)[symmetric] qbs_space_R)
show ?case
by(rule less_eq_measure.intros(1)) (simp add: 1 space_L)
next
case (2 A B)
then have hmy:"qbs_Mx Y ⊆ borel →⇩M X"
using qbs_Mx_R by blast
have [simp]: "space X = qbs_space A"
by(simp add: 2(1)[symmetric] qbs_space_R)
have "sets X ⊆ sigma_Mx Y"
proof
fix U
assume hu:"U ∈ sets X"
show "U ∈ sigma_Mx Y"
unfolding sigma_Mx_def
proof(safe intro!: exI[where x=U])
show "⋀x. x ∈ U ⟹ x ∈ qbs_space Y"
using sets.sets_into_space[OF hu]
by(auto simp add: 2)
next
fix α
assume "α ∈ qbs_Mx Y"
then have "α ∈ borel →⇩M X"
using hmy by(auto)
thus "α -` U ∈ sets borel"
using hu by(simp add: measurable_sets_borel)
qed
qed
then consider "sets X = sigma_Mx Y" | "sets X ⊂ sigma_Mx Y"
by auto
then show ?case
proof cases
case 1
show ?thesis
proof(rule less_eq_measure.intros(3))
show "emeasure X ≤ emeasure (qbs_to_measure Y)"
unfolding emeasure_L
proof(rule le_funI)
fix U
consider "U = {}" | "U ∉ sigma_Mx Y" | "U ≠ {} ∧ U ∈ sigma_Mx Y"
by auto
then show "emeasure X U ≤ (if U = {} ∨ U ∉ sigma_Mx Y then 0 else ∞)"
proof cases
case 1
then show ?thesis by simp
next
case h:2
then have "U ∉ sigma_Mx A"
using qbs_Mx_sigma_Mx_contra[OF 2(3)[symmetric] 2(4)] 2(2) by auto
hence "U ∉ sets X"
using lr_sets 2(1) sets_L by blast
thus ?thesis
by(simp add: h emeasure_notin_sets)
next
case 3
then show ?thesis
by simp
qed
qed
qed(simp_all add: 1 2 space_L sets_L)
next
case h2:2
show ?thesis
by(rule less_eq_measure.intros(2)) (simp add: space_L 2, simp add: h2 sets_L)
qed
qed
qed
end