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<