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<