Theory Measure_QuasiBorel_Adjunction

(*  Title:   Measure_QuasiBorel_Adjunction.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

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 "Csigma_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 ("borelQ")  where "borelQ  measure_to_qbs borel"
abbreviation qbs_count_space ("count'_spaceQ") where "qbs_count_space I  measure_to_qbs (count_space I)"

lemma
  shows qbs_space_qbs_borel[simp]: "qbs_space borelQ = UNIV"
    and qbs_space_count_space[simp]: "qbs_space (qbs_count_space I) = I"
    and qbs_Mx_qbs_borel: "qbs_Mx borelQ = 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)

(* Want to remove the following *)
lemma
  shows qbs_space_qbs_borel'[qbs]: "r  qbs_space borelQ"
    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 = borelQ Q X"
proof safe
  fix α :: "real  _"
  assume "α  borelQ Q X"
  have "id  qbs_Mx borelQ" by (simp add: qbs_Mx_R)
  then have "α  id  qbs_Mx X"
    using qbs_morphism_Mx[OF α  borelQ 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  borelQ 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)  (borelQ Q W) Q X Q Y"
    by(auto simp: qbs_Mx_is_morphisms dest: uncurry_preserves_morphisms)
  hence "(λ(r,w,x). α r w x)  borelQ 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)  borelQ 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)  (borelQ 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 Xshow "(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 iI. M i) = (ΠQ iI. measure_to_qbs (M i))"
proof(rule qbs_eqI)
  show "qbs_Mx (measure_to_qbs (PiM I M)) = qbs_Mx (ΠQ iI. measure_to_qbs (M i))"
  proof safe
    fix f :: "real  _"
    assume "f  qbs_Mx (measure_to_qbs (PiM I M))"
    with measurable_space[of f borel "PiM I M"] show "f  qbs_Mx (ΠQ iI. 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 iI. 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 (PiM 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 iUNIV. 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 iUNIV. 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. iS. 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. iS. 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_spaceQ UNIV Q borelQ)"
  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 borelQ" "limsup  f  qbs_Mx borelQ" "lim  f  qbs_Mx borelQ"
    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.  iI. 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.  iI. 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.  iI. 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.  iI. 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. iS. 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. iS. 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. iS. 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 iUNIV. Y)"
  shows "(λx. case_nat (f x) (g x))  X Q (ΠQ iUNIV. 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. iS. 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. λiI. f i x)  X Q (ΠQ iI. 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_spaceQ 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 nUNIV. Π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 nUNIV. Π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 nUNIV. Π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_spaceQ 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 (borelQ ::'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_spaceQ (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 (borelQ ::'b :: {second_countable_topology, linorder_topology} quasi_borel)) Q list_qbs X Q list_qbs X)"
    and "sort_key  qbs_space ((X Q count_spaceQ (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 (borelQ ::'b :: {second_countable_topology, linorder_topology} quasi_borel) Q list_qbs borelQ"
    and "sort  list_qbs (count_spaceQ (UNIV :: (_ :: countable) set)) Q list_qbs (count_spaceQ 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 {yqbs_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_spaceQ (UNIV :: ('a :: countable) set) Q count_spaceQ UNIV) All"
proof(rule qbs_morphismI)
  fix a :: "real  'a  bool"
  assume "a  qbs_Mx (count_spaceQ UNIV Q count_spaceQ 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_spaceQ UNIV)"
    by(simp add: comp_def qbs_Mx_R)
qed

lemma Ex_qbs_pred[qbs]: "qbs_pred (count_spaceQ (UNIV :: ('a :: countable) set) Q count_spaceQ UNIV) Ex"
proof(rule qbs_morphismI)
  fix a :: "real  'a  bool"
  assume "a  qbs_Mx (count_spaceQ UNIV Q count_spaceQ 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_spaceQ 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. xI. 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. xI. 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. xI. 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. xI. 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 {xqbs_space X. P x} Q Y" "g  sub_qbs X {xqbs_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 = {}" 
    | "{xqbs_space X. ¬ P x} = qbs_space X"
    | "{xqbs_space X. P x} = qbs_space X"
    | "{xqbs_space X. P x}  {}" "{xqbs_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 {xqbs_space X. P x})" "a1  qbs_Mx (sub_qbs X {xqbs_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