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)"

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)

subsubsection ‹ The Functor $L$ ›
definition sigma_Mx :: "'a quasi_borel ⇒ 'a set set" where
"sigma_Mx X ≡ {U ∩ qbs_space X |U. ∀α∈qbs_Mx X. α -` U ∈ sets borel}"

definition qbs_to_measure :: "'a quasi_borel ⇒ 'a measure" where
"qbs_to_measure X ≡ Abs_measure (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"

lemma measure_space_L: "measure_space (qbs_space X) (sigma_Mx X) (λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
  unfolding measure_space_def
proof safe

  show "sigma_algebra (qbs_space X) (sigma_Mx X)"
  proof(rule sigma_algebra.intro)
    show "algebra (qbs_space X) (sigma_Mx X)"
    proof
      have "∀ U ∈ sigma_Mx X. U ⊆ qbs_space X"
        using sigma_Mx_def subset_iff by fastforce
      thus "sigma_Mx X ⊆ Pow (qbs_space X)" by auto
    next
      show "{} ∈ sigma_Mx X"
        unfolding sigma_Mx_def by auto
    next
      fix A
      fix B
      assume "A ∈ sigma_Mx X"
             "B ∈ sigma_Mx X"
      then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
        by (simp add: sigma_Mx_def)
      then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
      have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
        using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
      then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
      from pa pb have [simp]:"∀α∈qbs_Mx X. α -` (Ua ∩ Ub) ∈ sets borel"
        by auto
      from this pa pb sigma_Mx_def have [simp]:"(Ua ∩ Ub) ∩ qbs_space X ∈ sigma_Mx X" by blast
      from pa pb have [simp]:"A ∩ B = (Ua ∩ Ub) ∩ qbs_space X" by auto
      thus "A ∩ B ∈ sigma_Mx X" by simp
    next
      fix A
      fix B
      assume "A ∈ sigma_Mx X"
             "B ∈ sigma_Mx X"
      then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
        by (simp add: sigma_Mx_def)
      then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
      have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
        using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
      then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
      from pa pb have [simp]:"A - B = (Ua ∩ -Ub) ∩ qbs_space X" by auto
      from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∩ -Ub) ∈ sets borel"
        by (metis Diff_Compl double_compl sets.Diff vimage_Compl vimage_Int)
      hence 1:"A - B ∈ sigma_Mx X"
        using sigma_Mx_def ‹A - B = Ua ∩ - Ub ∩ qbs_space X› by blast
      show "∃C⊆sigma_Mx X. finite C ∧ disjoint C ∧ A - B = ⋃ C"
      proof
        show "{A - B} ⊆sigma_Mx X ∧ finite {A-B} ∧ disjoint {A-B} ∧ A - B = ⋃ {A-B}"
          using 1 by auto
      qed
    next
      fix A
      fix B
      assume "A ∈ sigma_Mx X"
             "B ∈ sigma_Mx X"
      then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)"
        by (simp add: sigma_Mx_def)
      then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets borel)" by auto
      have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)"
        using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
      then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets borel)" by auto
      from pa pb have "A ∪ B = (Ua ∪ Ub) ∩ qbs_space X" by auto
      from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∪ Ub) ∈ sets borel" by auto
      then show "A ∪ B ∈ sigma_Mx X"
        unfolding sigma_Mx_def
        using ‹A ∪ B = (Ua ∪ Ub) ∩ qbs_space X› by blast
    next
      have "∀α∈qbs_Mx X. α -` (UNIV) ∈ sets borel"
        by simp
      thus "qbs_space X ∈ sigma_Mx X"
        unfolding sigma_Mx_def
        by blast
    qed
  next
    show "sigma_algebra_axioms (sigma_Mx X)"
      unfolding sigma_algebra_axioms_def
    proof safe
      fix A :: "nat ⇒ _"
      assume 1:"range A ⊆ sigma_Mx X"
      then have 2:"∀i. ∃Ui. A i = Ui ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ui ∈ sets borel)"
        unfolding sigma_Mx_def by auto
      then have "∃ U :: nat ⇒ _. ∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets borel)"
        by (rule choice)
      from this obtain U where pu:"∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets borel)"
        by auto
      hence "∀α∈qbs_Mx X. α -` (⋃ (range U)) ∈ sets borel"
        by (simp add: countable_Un_Int(1) vimage_UN)
      from pu have "⋃ (range A) = (⋃i::nat. (U i ∩ qbs_space X))" by blast
      hence "⋃ (range A) = ⋃ (range U) ∩ qbs_space X" by auto
      thus "⋃ (range A) ∈ sigma_Mx X"
        using sigma_Mx_def ‹∀α∈qbs_Mx X. α -` ⋃ (range U) ∈ sets borel› by blast
    qed
  qed
next
  show "countably_additive (sigma_Mx X) (λA. if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞)"
  proof(rule countably_additiveI)
    fix A :: "nat ⇒ _"
    assume h:"range A ⊆ sigma_Mx X"
             "⋃ (range A) ∈ sigma_Mx X"
    consider "⋃ (range A) = {}" | "⋃ (range A) ≠ {}"
      by auto
    then show "(∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) =
               (if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
    proof cases
      case 1
      then have "⋀i. A i = {}"
        by simp
      thus ?thesis
        by(simp add: 1)
    next
      case 2
      then obtain j where hj:"A j ≠ {}"
        by auto
      have "(∑i. if A i = {} then 0  else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
      proof -
        have hsum:"⋀N f. sum f {..<N} ≤ (∑n. (f n :: ennreal))"
          by (simp add: sum_le_suminf)
        have hsum':"⋀P f. (∃j. j ∈ P ∧ f j = (∞ :: ennreal)) ⟹ finite P ⟹ sum f P = ∞"
          by auto
        have h1:"(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
        proof(rule hsum')
          show "∃ja. ja ∈ {..<j + 1} ∧ (if A ja = {} then 0 else if A ja ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
          proof(rule exI[where x=j],rule conjI)
            have "A j ∈ sigma_Mx X"
              using h(1) by auto
            then show "(if A j = {} then 0 else if A j ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
              using hj by simp
          qed simp
        qed simp
        have "(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) ≤ (∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
          by(rule hsum)
        thus ?thesis
          by(simp only: h1) (simp add: top.extremum_unique)
      qed
      moreover have "(if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
        using 2 h(2) by simp
      ultimately show ?thesis
        by simp
    qed
  qed
qed(simp add: positive_def)

lemma
  shows space_L: "space (qbs_to_measure X) = qbs_space X" (is ?goal1)
    and sets_L: "sets (qbs_to_measure X) = sigma_Mx X" (is ?goal2)
    and emeasure_L: "emeasure (qbs_to_measure X) = (λA. if A = {} ∨ A ∉ sigma_Mx X then 0 else ∞)" (is ?goal3)
proof -
  have "Rep_measure (qbs_to_measure X) = (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
    unfolding qbs_to_measure_def by(auto intro!: Abs_measure_inverse simp: measure_space_L)
  thus ?goal1 ?goal2 ?goal3
    by(auto simp: sets_def space_def emeasure_def)
qed

lemma qbs_Mx_sigma_Mx_contra:
  assumes "qbs_space X = qbs_space Y"
      and "qbs_Mx X ⊆ qbs_Mx Y"
  shows "sigma_Mx Y ⊆ sigma_Mx X"
  using assms by(auto simp: sigma_Mx_def)


text ‹ The following lemma says that @{term qbs_to_measure} is a functor from \textbf{QBS} to \textbf{Meas}. ›
lemma l_preserves_morphisms:
  "X →⇩Q Y ⊆ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
proof safe
  fix f
  assume h:"f ∈ X →⇩Q Y"
  show "f ∈ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
  proof(rule measurableI)
    fix A
    assume "A ∈ sets (qbs_to_measure Y)"
    then obtain Ua where pa:"A = Ua ∩ qbs_space Y ∧ (∀α∈qbs_Mx Y. α -` Ua ∈ sets borel)"
      by (auto simp: sigma_Mx_def sets_L)
    have "∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y"
         "∀α∈ qbs_Mx X. α -` (f -` (qbs_space Y)) = UNIV"
      using qbs_morphism_space[OF h] qbs_morphism_Mx[OF h] by (auto simp: qbs_Mx_to_X)
    hence "∀α∈qbs_Mx X. α -` (f -` A) = α -` (f -` Ua)"
      by (simp add: pa)
    from pa this qbs_morphism_def have "∀α∈qbs_Mx X. α -` (f -` A) ∈ sets borel"
      by (simp add: vimage_comp ‹∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y›)
    thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
      using sigma_Mx_def by(auto simp: sets_L space_L)
  qed (insert qbs_morphism_space[OF h], auto simp: space_L)
qed


abbreviation qbs_borel ("borel⇩Q")  where "borel⇩Q ≡ measure_to_qbs borel"
abbreviation qbs_count_space ("count'_space⇩Q") where "qbs_count_space I ≡ measure_to_qbs (count_space I)"

declare [[coercion measure_to_qbs]]

lemma
  shows qbs_space_qbs_borel[simp]: "qbs_space borel⇩Q = UNIV"
    and qbs_space_count_space[simp]: "qbs_space (qbs_count_space I) = I"
    and qbs_Mx_qbs_borel: "qbs_Mx borel⇩Q = borel_measurable borel"
    and qbs_Mx_count_space: "qbs_Mx (qbs_count_space I) = borel →⇩M count_space I"
  by(simp_all add: qbs_space_R qbs_Mx_R)

(* Want to remove the following *)
lemma
  shows qbs_space_qbs_borel'[qbs]: "r ∈ qbs_space borel⇩Q"
    and qbs_space_count_space_UNIV'[qbs]: "x ∈ qbs_space (qbs_count_space (UNIV :: (_ :: countable) set))"
  by simp_all

lemma qbs_Mx_is_morphisms: "qbs_Mx X = borel⇩Q →⇩Q X"
proof safe
  fix α :: "real ⇒ _"
  assume "α ∈ borel⇩Q →⇩Q X"
  have "id ∈ qbs_Mx borel⇩Q" by (simp add: qbs_Mx_R)
  then have "α ∘ id ∈ qbs_Mx X"
    using qbs_morphism_Mx[OF ‹α ∈ borel⇩Q →⇩Q X›]
    by blast
  then show "α ∈ qbs_Mx X" by simp
qed(auto intro!: qbs_morphismI simp: qbs_Mx_qbs_borel)

lemma exp_qbs_Mx': "qbs_Mx (exp_qbs X Y) = {g. case_prod g ∈ borel⇩Q ⨂⇩Q X →⇩Q Y}"
  by(auto simp:  qbs_Mx_qbs_borel comp_def qbs_Mx_is_morphisms split_beta' intro!:curry_preserves_morphisms)

lemma arg_swap_morphism':
  assumes "(λg. f (λw x. g x w)) ∈ exp_qbs X (exp_qbs W Y) →⇩Q Z"
  shows "f ∈ exp_qbs W (exp_qbs X Y) →⇩Q Z"
proof(rule qbs_morphismI)
  fix α
  assume "α ∈ qbs_Mx (exp_qbs W (exp_qbs X Y))"
  then have "(λ((r,w),x). α r w x) ∈ (borel⇩Q ⨂⇩Q W) ⨂⇩Q X →⇩Q Y"
    by(auto simp: qbs_Mx_is_morphisms dest: uncurry_preserves_morphisms)
  hence "(λ(r,w,x). α r w x) ∈ borel⇩Q ⨂⇩Q W ⨂⇩Q X →⇩Q Y"
    by(auto intro!: qbs_morphism_cong'[where f="(λ((r,w),x). α r w x) ∘ (λ(x, y, z). ((x, y), z))" and g="λ(r,w,x). α r w x"] qbs_morphism_comp[OF qbs_morphism_pair_assoc2])
  hence "(λ(r,x,w). α r w x) ∈ borel⇩Q ⨂⇩Q X ⨂⇩Q W →⇩Q Y"
    by(auto intro!: qbs_morphism_cong'[where f="(λ(r,w,x). α r w x) ∘ map_prod id (λ(x,y). (y,x))" and g="(λ(r,x,w). α r w x)"] qbs_morphism_comp qbs_morphism_map_prod qbs_morphism_pair_swap)
  hence "(λ((r,x),w). α r w x) ∈ (borel⇩Q ⨂⇩Q X) ⨂⇩Q W →⇩Q Y"
    by(auto intro!: qbs_morphism_cong'[where f="(λ(r,x,w). α r w x) ∘ (λ((x, y), z). (x, y, z))" and g="λ((r,x),w). α r w x"] qbs_morphism_comp[OF qbs_morphism_pair_assoc1])
  hence "(λr x w. α r w x) ∈ qbs_Mx (exp_qbs X (exp_qbs W Y))"
    by(auto simp: qbs_Mx_is_morphisms split_beta')
  from qbs_morphism_Mx[OF assms this] show "f ∘ α ∈ qbs_Mx Z"
    by(auto simp: comp_def)
qed

lemma qbs_Mx_subset_of_measurable: "qbs_Mx X ⊆ borel →⇩M qbs_to_measure X"
proof
  fix α
  assume "α ∈ qbs_Mx X"
  show "α ∈ borel →⇩M qbs_to_measure X"
  proof(rule measurableI)
    fix x
    show "α x ∈ space (qbs_to_measure X)"
      using qbs_Mx_to_X ‹α ∈ qbs_Mx X› by(simp add: space_L)
  next
    fix A
    assume "A ∈ sets (qbs_to_measure X)"
    then have "α -`(qbs_space X) = UNIV"
      using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by(auto simp: sets_L)
    then show "α -` A ∩ space borel ∈ sets borel"
      using ‹α ∈ qbs_Mx X› ‹A ∈ sets (qbs_to_measure X)›
      by(auto simp add: sigma_Mx_def sets_L)
  qed
qed

lemma L_max_of_measurables:
  assumes "space M = qbs_space X"
      and "qbs_Mx X ⊆ borel →⇩M M"
    shows "sets M ⊆ sets (qbs_to_measure X)"
proof
  fix U
  assume "U ∈ sets M"
  from sets.sets_into_space[OF this] in_mono[OF assms(2)] measurable_sets_borel[OF _ this]
  show "U ∈ sets (qbs_to_measure X)"
    using assms(1)
    by(auto intro!: exI[where x=U] simp: sigma_Mx_def sets_L)
qed


lemma qbs_Mx_are_measurable[simp,measurable]:
  assumes "α ∈ qbs_Mx X"
  shows "α ∈ borel →⇩M qbs_to_measure X"
  using assms qbs_Mx_subset_of_measurable by auto

lemma measure_to_qbs_cong_sets:
  assumes "sets M = sets N"
  shows "measure_to_qbs M = measure_to_qbs N"
  by(rule qbs_eqI) (simp add: qbs_Mx_R measurable_cong_sets[OF _ assms])

lemma lr_sets[simp]:
 "sets X ⊆ sets (qbs_to_measure (measure_to_qbs X))"
  unfolding sets_L
proof safe
  fix U
  assume "U ∈ sets X"
  then have "U ∩ space X = U" by simp
  moreover have "∀α∈borel →⇩M X. α -` U ∈ sets borel"
    using ‹U ∈ sets X› by(auto simp add: measurable_def)
  ultimately show "U ∈ sigma_Mx (measure_to_qbs X)"
    by(auto simp add: sigma_Mx_def qbs_Mx_R qbs_space_R)
qed

lemma(in standard_borel) lr_sets_ident[simp, measurable_cong]:
 "sets (qbs_to_measure (measure_to_qbs M)) = sets M"
  unfolding sets_L
proof safe
  fix V
  assume "V ∈ sigma_Mx (measure_to_qbs M)"
  then obtain U where H2: "V = U ∩ space M" "⋀α::real ⇒ _. α∈borel →⇩M M ⟹ α -` U ∈ sets borel"
    by(auto simp: sigma_Mx_def qbs_Mx_R qbs_space_R)
  consider "space M = {}" | "space M ≠ {}" by auto
  then show "V ∈ sets M"
  proof cases
    case 1
    then show ?thesis
      by(simp add: H2)
  next
    case 2
    have "from_real -` V = from_real -` (U ∩ space M)" using H2 by auto
    also have "... = from_real -` U" using from_real_measurable'[OF 2] by(auto simp add: measurable_def) 
    finally have "to_real -` from_real -` U  ∩ space M ∈ sets M"
      by (meson "2" H2(2) from_real_measurable' measurable_sets to_real_measurable)
    moreover have "to_real -` from_real -` U  ∩ space M =  U ∩ space M"
      by auto
    ultimately show ?thesis using H2 by simp
  qed
qed(insert lr_sets, auto simp: sets_L)

corollary sets_lr_polish_borel[simp, measurable_cong]: "sets (qbs_to_measure qbs_borel) = sets (borel :: (_ :: polish_space) measure)"
  by(auto intro!: standard_borel.lr_sets_ident standard_borel_ne.standard_borel)

corollary sets_lr_count_space[simp, measurable_cong]: "sets (qbs_to_measure (qbs_count_space (UNIV :: (_ :: countable) set))) = sets (count_space UNIV)"
  by(rule standard_borel.lr_sets_ident) (auto intro!:  standard_borel_ne.standard_borel)

subsubsection ‹ The Adjunction ›
lemma lr_adjunction_correspondence :
 "X →⇩Q (measure_to_qbs Y) = (qbs_to_measure X) →⇩M Y"
proof safe
(* ⊆ *)
  fix f
  assume "f ∈ X →⇩Q (measure_to_qbs Y)"
  show "f ∈ qbs_to_measure X →⇩M Y"
  proof(rule measurableI)
    fix x
    assume "x ∈ space (qbs_to_measure X)"
    thus "f x ∈ space Y"
      using qbs_morphism_space[OF ‹f ∈ X →⇩Q (measure_to_qbs Y)›]
      by (auto simp: qbs_space_R space_L)
  next
    fix A
    assume "A ∈ sets Y"
    have "∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx (measure_to_qbs Y)"
      using qbs_morphism_Mx[OF ‹f ∈ X →⇩Q (measure_to_qbs Y)›] by auto
    hence "∀α ∈ qbs_Mx X. f ∘ α ∈ borel →⇩M Y" by (simp add: qbs_Mx_R)
    hence "∀α ∈ qbs_Mx X. α -` (f -` A) ∈ sets borel"
      using ‹A∈ sets Y› measurable_sets_borel vimage_comp by metis
    thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
      using sigma_Mx_def by (auto simp: space_L sets_L)
  qed
   
(* ⊇ *)
next
  fix f
  assume "f ∈ qbs_to_measure X →⇩M Y"
  show "f ∈ X →⇩Q measure_to_qbs Y"
  proof(rule qbs_morphismI)
    fix α
    assume "α ∈ qbs_Mx X"
    have "f ∘ α ∈ borel →⇩M Y"
    proof(rule measurableI)
      fix x :: real
      from ‹α ∈ qbs_Mx X› qbs_Mx_to_X have "α x ∈ qbs_space X" by auto
      hence "α x ∈ space (qbs_to_measure X)" by (simp add: space_L)
      thus "(f ∘ α) x ∈ space Y"
        using ‹f ∈ qbs_to_measure X →⇩M Y›
        by (metis comp_def measurable_space)
    next
      fix A
      assume "A ∈ sets Y"
      from ‹f ∈ qbs_to_measure X →⇩M Y› measurable_sets this measurable_def
      have "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
        by blast
      hence "f -` A ∩ qbs_space X ∈ sigma_Mx X" by (simp add: sets_L space_L)
      then have "∃V. f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets borel)"
        by (simp add: sigma_Mx_def)
      then obtain V where h:"f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets borel)" by auto
      have 1:"α -` (f -` A) = α -` (f -` A ∩ qbs_space X)"
        using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by blast
      have 2:"α -` (V ∩ qbs_space X) = α -` V"
        using ‹α ∈ qbs_Mx X› qbs_Mx_to_X by blast
      from 1 2 h have "(f ∘ α) -` A = α -` V" by (simp add: vimage_comp)
      from this h ‹α ∈ qbs_Mx X ›show "(f ∘ α) -` A ∩ space borel ∈ sets borel" by simp
    qed
    thus "f ∘ α ∈ qbs_Mx (measure_to_qbs Y)"
      by(simp add:qbs_Mx_R)
  qed
qed

lemma(in standard_borel) standard_borel_r_full_faithful:
  "M →⇩M Y = measure_to_qbs M →⇩Q measure_to_qbs Y"
proof
  have "measure_to_qbs M →⇩Q measure_to_qbs Y ⊆ qbs_to_measure (measure_to_qbs M) →⇩M qbs_to_measure (measure_to_qbs Y)"
    by (simp add: l_preserves_morphisms)
  also have "... = M →⇩M qbs_to_measure (measure_to_qbs Y)"
    using measurable_cong_sets by auto
  also have "... ⊆ M →⇩M Y"
    by(rule measurable_mono[OF lr_sets]) (simp_all add: qbs_space_R space_L)
  finally show "measure_to_qbs M →⇩Q measure_to_qbs Y ⊆ M →⇩M Y" .
qed(rule r_preserves_morphisms)

lemma qbs_morphism_dest:
  assumes "f ∈ X →⇩Q measure_to_qbs Y"
  shows "f ∈ qbs_to_measure X →⇩M Y"
  using assms lr_adjunction_correspondence by auto

lemma(in standard_borel) qbs_morphism_dest:
  assumes "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
  shows "k ∈ M →⇩M Y"
  using standard_borel_r_full_faithful assms by auto

lemma qbs_morphism_measurable_intro:
  assumes "f ∈ qbs_to_measure X →⇩M Y"
  shows "f ∈ X →⇩Q measure_to_qbs Y"
  using assms lr_adjunction_correspondence by auto

lemma(in standard_borel) qbs_morphism_measurable_intro:
  assumes "k ∈ M →⇩M Y"
  shows "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
  using standard_borel_r_full_faithful assms by auto

lemma r_preserves_product :
  "measure_to_qbs (X ⨂⇩M Y) = measure_to_qbs X ⨂⇩Q measure_to_qbs Y"
  by(auto intro!: qbs_eqI simp: measurable_pair_iff pair_qbs_Mx qbs_Mx_R)

lemma l_product_sets:
  "sets (qbs_to_measure X ⨂⇩M qbs_to_measure Y) ⊆ sets (qbs_to_measure (X ⨂⇩Q Y))"
proof(rule sets_pair_in_sets)
  fix A B
  assume h:"A ∈ sets (qbs_to_measure X)" "B ∈ sets (qbs_to_measure Y)"
  then obtain Ua Ub where hu:
   "A = Ua ∩ qbs_space X" "∀α∈qbs_Mx X. α -` Ua ∈ sets borel"
   "B = Ub ∩ qbs_space Y" "∀α∈qbs_Mx Y. α -` Ub ∈ sets borel"
    by(auto simp add: sigma_Mx_def sets_L)
  show "A × B ∈ sets (qbs_to_measure (X ⨂⇩Q Y))"
  proof -
    have "A × B = Ua × Ub ∩ qbs_space (X ⨂⇩Q Y) ∧ (∀α∈qbs_Mx (X ⨂⇩Q Y). α -` (Ua × Ub) ∈ sets borel)"
      using hu by(auto simp add: vimage_Times pair_qbs_space pair_qbs_Mx)
    thus ?thesis
      by(auto simp add: sigma_Mx_def sets_L intro!: exI[where x="Ua × Ub"])
  qed
qed

corollary qbs_borel_prod: "qbs_borel ⨂⇩Q qbs_borel = (qbs_borel :: ('a::second_countable_topology × 'b::second_countable_topology) quasi_borel)"
  by(simp add: r_preserves_product[symmetric] borel_prod)

corollary qbs_count_space_prod: "qbs_count_space (UNIV :: ('a :: countable) set) ⨂⇩Q qbs_count_space (UNIV :: ('b :: countable) set) = qbs_count_space UNIV"
  by(auto simp: r_preserves_product[symmetric] count_space_prod)

lemma r_preserves_product': "measure_to_qbs (Π⇩M i∈I. M i) = (Π⇩Q i∈I. measure_to_qbs (M i))"
proof(rule qbs_eqI)
  show "qbs_Mx (measure_to_qbs (Pi⇩M I M)) = qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
  proof safe
    fix f :: "real ⇒ _"
    assume "f ∈ qbs_Mx (measure_to_qbs (Pi⇩M I M))"
    with measurable_space[of f borel "Pi⇩M I M"] show "f ∈ qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
      by(auto simp: qbs_Mx_R PiQ_Mx space_PiM  intro!:ext[of "λr. f r _"])
  next
    fix f :: "real ⇒ _"
    assume "f ∈ qbs_Mx (Π⇩Q i∈I. measure_to_qbs (M i))"
    then have "⋀i. i ∈ I ⟹ (λr. f r i) ∈ borel →⇩M M i" "⋀i. i ∉ I ⟹ (λr. f r i) = (λr. undefined)"
      by (auto simp: qbs_Mx_R PiQ_Mx)
    with measurable_space[OF this(1)] fun_cong[OF this(2)] show "f ∈ qbs_Mx (measure_to_qbs (Pi⇩M I M))"
      by(auto intro!: measurable_PiM_single' simp: qbs_Mx_R)
  qed
qed

lemma PiQ_qbs_borel:
  "(Π⇩Q i::('a:: countable)∈UNIV. (qbs_borel :: ('b::second_countable_topology quasi_borel))) = qbs_borel"
  by(simp add: r_preserves_product'[symmetric] measure_to_qbs_cong_sets[OF sets_PiM_equal_borel])

lemma qbs_morphism_from_countable:
  fixes X :: "'a quasi_borel"
  assumes "countable (qbs_space X)"
          "qbs_Mx X ⊆ borel →⇩M count_space (qbs_space X)"
      and "⋀i. i ∈ qbs_space X ⟹ f i ∈ qbs_space Y"
    shows "f ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
  fix α
  assume "α ∈ qbs_Mx X"
  then have [measurable]: "α ∈ borel →⇩M count_space (qbs_space X)"
    using assms(2) ..
  define k :: "'a ⇒ real ⇒ _"
    where "k ≡ (λi _. f i)"
  have "f ∘ α = (λr. k (α r) r)"
    by(auto simp add: k_def)
  also have "... ∈ qbs_Mx Y"
    by(rule qbs_closed3_dest2[OF assms(1)]) (use assms(3) k_def in simp_all)
  finally show "f ∘ α ∈ qbs_Mx Y" .
qed

corollary qbs_morphism_count_space':
  assumes "⋀i. i ∈ I ⟹ f i ∈ qbs_space Y" "countable I"
  shows "f ∈ qbs_count_space I →⇩Q Y"
  using assms by(auto intro!: qbs_morphism_from_countable simp: qbs_Mx_R)

corollary qbs_morphism_count_space:
  assumes "⋀i. f i ∈ qbs_space Y"
  shows "f ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q Y"
  using assms by(auto intro!: qbs_morphism_from_countable simp: qbs_Mx_R)

lemma [qbs]:
  shows not_qbs_pred: "Not ∈ qbs_count_space UNIV →⇩Q qbs_count_space UNIV"
    and or_qbs_pred: "(∨) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and and_qbs_pred: "(∧) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and implies_qbs_pred: "(⟶) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and iff_qbs_pred: "(⟷) ∈ qbs_count_space UNIV →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
  by(auto intro!: qbs_morphism_count_space)

lemma [qbs]:
  shows less_count_qbs_pred: "(<) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and le_count_qbs_pred: "(≤) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and eq_count_qbs_pred: "(=) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and plus_count_qbs_morphism: "(+) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and minus_count_qbs_morphism: "(-) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and mult_count_qbs_morphism: "(*) ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q exp_qbs (qbs_count_space UNIV) (qbs_count_space UNIV)"
    and Suc_qbs_morphism: "Suc ∈ qbs_count_space UNIV →⇩Q qbs_count_space UNIV"
  by(auto intro!: qbs_morphism_count_space)

lemma qbs_morphism_product_iff:
 "f ∈ X →⇩Q (Π⇩Q i :: (_ :: countable)∈UNIV. Y) ⟷ f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
proof
  assume h:"f ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
  show "f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
    by(rule arg_swap_morphism, rule  qbs_morphism_count_space) (simp add: qbs_morphism_component_singleton'[OF h qbs_morphism_ident'])
next
  assume "f ∈ X →⇩Q qbs_count_space UNIV ⇒⇩Q Y"
  from qbs_morphism_space[OF arg_swap_morphism[OF this]]
  show "f ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
    by(auto intro!: product_qbs_canonical1[where f="(λi x. f x i)"])
qed

lemma qbs_morphism_pair_countable1:
  assumes "countable (qbs_space X)"
          "qbs_Mx X ⊆ borel →⇩M count_space (qbs_space X)"
      and "⋀i. i ∈ qbs_space X ⟹ f i ∈ Y →⇩Q Z"
    shows "(λ(x,y). f x y) ∈ X ⨂⇩Q Y →⇩Q Z"
  by(auto intro!: uncurry_preserves_morphisms qbs_morphism_from_countable[OF assms(1,2)] assms(3))

lemma qbs_morphism_pair_countable2:
  assumes "countable (qbs_space Y)"
          "qbs_Mx Y ⊆ borel →⇩M count_space (qbs_space Y)"
      and "⋀i. i ∈ qbs_space Y ⟹ (λx. f x i) ∈ X →⇩Q Z"
    shows "(λ(x,y). f x y) ∈ X ⨂⇩Q Y →⇩Q Z"
  by(auto intro!: qbs_morphism_pair_swap[of "case_prod (λx y. f y x)",simplified] qbs_morphism_pair_countable1 assms)

corollary qbs_morphism_pair_count_space1:
  assumes "⋀i. f i ∈ Y →⇩Q Z"
  shows "(λ(x,y). f x y) ∈ qbs_count_space (UNIV :: ('a :: countable) set) ⨂⇩Q Y →⇩Q Z"
  by(auto intro!: qbs_morphism_pair_countable1 simp: qbs_Mx_R assms)

corollary qbs_morphism_pair_count_space2:
  assumes "⋀i. (λx. f x i) ∈ X →⇩Q Z"
  shows "(λ(x,y). f x y) ∈ X ⨂⇩Q qbs_count_space (UNIV :: ('a :: countable) set) →⇩Q Z"
  by(auto intro!: qbs_morphism_pair_countable2 simp: qbs_Mx_R assms)

lemma qbs_morphism_compose_countable':
  assumes [qbs]:"⋀i. i ∈ I ⟹ (λx. f i x) ∈ X →⇩Q Y" "g ∈ X →⇩Q qbs_count_space I" "countable I"
  shows "(λx. f (g x) x) ∈ X →⇩Q Y"
proof -
  have [qbs]:"f ∈ qbs_count_space I →⇩Q X ⇒⇩Q Y"
    by(auto intro!: qbs_morphism_count_space' simp: assms(3))
  show ?thesis
    by simp
qed

lemma qbs_morphism_compose_countable:
  assumes [simp]:"⋀i::'i::countable. (λx. f i x) ∈ X →⇩Q Y" "g ∈ X →⇩Q (qbs_count_space UNIV)"
  shows "(λx. f (g x) x) ∈ X →⇩Q Y"
  by(rule qbs_morphism_compose_countable'[of UNIV f]) simp_all

lemma qbs_morphism_op:
  assumes "case_prod f ∈ X ⨂⇩M Y →⇩M Z"
  shows "f ∈ measure_to_qbs X →⇩Q measure_to_qbs Y ⇒⇩Q measure_to_qbs Z"
  using r_preserves_morphisms assms
  by(fastforce simp: r_preserves_product[symmetric] intro!: curry_preserves_morphisms)

lemma [qbs]:
  shows plus_qbs_morphism: "(+) ∈ (qbs_borel :: (_::{second_countable_topology, topological_monoid_add}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and plus_ereal_qbs_morphism: "(+) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and diff_qbs_morphism: "(-) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_vector}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and diff_ennreal_qbs_morphism: "(-) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and diff_ereal_qbs_morphism: "(-) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and times_qbs_morphism: "(*) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_algebra}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and times_ennreal_qbs_morphism: "(*) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and times_ereal_qbs_morphism: "(*) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and divide_qbs_morphism: "(/) ∈ (qbs_borel :: (_::{second_countable_topology, real_normed_div_algebra}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and divide_ennreal_qbs_morphism: "(/) ∈ (qbs_borel :: ennreal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and divide_ereal_qbs_morphism: "(/) ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and log_qbs_morphism: "log ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and root_qbs_morphism: "root ∈ qbs_count_space UNIV →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and scaleR_qbs_morphism: "(*⇩R) ∈ qbs_borel →⇩Q (qbs_borel :: (_::{second_countable_topology, real_normed_vector}) quasi_borel) ⇒⇩Q qbs_borel"
    and qbs_morphism_inner: "(∙) ∈ qbs_borel →⇩Q (qbs_borel :: (_::{second_countable_topology, real_inner}) quasi_borel) ⇒⇩Q qbs_borel"
    and dist_qbs_morphism: "dist ∈ (qbs_borel :: (_::{second_countable_topology, metric_space}) quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and powr_qbs_morphism: "(powr) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q (qbs_borel :: real quasi_borel)"
    and max_qbs_morphism: "(max :: (_ :: {second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and min_qbs_morphism: "(min :: (_ :: {second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and sup_qbs_morphism: "(sup :: (_ :: {lattice,second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and inf_qbs_morphism: "(inf :: (_ :: {lattice,second_countable_topology, linorder_topology}) ⇒ _ ⇒ _) ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel"
    and less_qbs_pred: "(<) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
    and eq_qbs_pred: "(=) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
    and le_qbs_pred: "(≤) ∈ (qbs_borel :: _ ::{second_countable_topology, linorder_topology} quasi_borel) →⇩Q qbs_borel ⇒⇩Q qbs_count_space UNIV"
  by(auto intro!: qbs_morphism_op)

lemma [qbs]:
  shows abs_real_qbs_morphism: "abs ∈ (qbs_borel :: real quasi_borel) →⇩Q qbs_borel"
    and abs_ereal_qbs_morphism: "abs ∈ (qbs_borel :: ereal quasi_borel) →⇩Q qbs_borel"
    and real_floor_qbs_morphism: "(floor :: real ⇒ int) ∈ qbs_borel →⇩Q qbs_count_space UNIV"
    and real_ceiling_qbs_morphism: "(ceiling :: real ⇒ int) ∈ qbs_borel →⇩Q qbs_count_space UNIV"
    and exp_qbs_morphism: "(exp::'a::{real_normed_field,banach}⇒'a) ∈ qbs_borel →⇩Q qbs_borel"
    and ln_qbs_morphism: "ln ∈ (qbs_borel :: real quasi_borel) →⇩Q qbs_borel"
    and sqrt_qbs_morphism: "sqrt ∈ qbs_borel →⇩Q qbs_borel"
    and of_real_qbs_morphism: "(of_real :: _ ⇒ (_::real_normed_algebra)) ∈ qbs_borel →⇩Q qbs_borel"
    and sin_qbs_morphism: "(sin :: _ ⇒ (_::{real_normed_field,banach})) ∈ qbs_borel →⇩Q qbs_borel"
    and cos_qbs_morphism: "(cos :: _ ⇒ (_::{real_normed_field,banach})) ∈ qbs_borel →⇩Q qbs_borel"
    and arctan_qbs_morphism: "arctan ∈ qbs_borel →⇩Q qbs_borel"
    and Re_qbs_morphism: "Re ∈ qbs_borel →⇩Q qbs_borel"
    and Im_qbs_morphism: "Im ∈ qbs_borel →⇩Q qbs_borel"
    and sgn_qbs_morphism: "(sgn::_::real_normed_vector ⇒ _) ∈ qbs_borel →⇩Q qbs_borel"
    and norm_qbs_morphism: "norm ∈ qbs_borel →⇩Q qbs_borel"
    and invers_qbs_morphism: "(inverse :: _ ⇒ (_ ::real_normed_div_algebra)) ∈ qbs_borel →⇩Q qbs_borel"
    and invers_ennreal_qbs_morphism: "(inverse :: _ ⇒ ennreal) ∈ qbs_borel →⇩Q qbs_borel"
    and invers_ereal_qbs_morphism: "(inverse :: _ ⇒ ereal) ∈ qbs_borel →⇩Q qbs_borel"
    and uminus_qbs_morphism: "(uminus :: _ ⇒ (_::{second_countable_topology, real_normed_vector})) ∈ qbs_borel →⇩Q qbs_borel"
    and ereal_qbs_morphism: "ereal ∈ qbs_borel →⇩Q qbs_borel"
    and real_of_ereal_qbs_morphism: "real_of_ereal ∈ qbs_borel →⇩Q qbs_borel"
    and enn2ereal_qbs_morphism: "enn2ereal ∈ qbs_borel →⇩Q qbs_borel"
    and e2ennreal_qbs_morphism: "e2ennreal ∈ qbs_borel →⇩Q qbs_borel"
    and ennreal_qbs_morphism: "ennreal ∈ qbs_borel →⇩Q qbs_borel"
    and qbs_morphism_nth: "(λx::real^'n. x $ i) ∈ qbs_borel →⇩Q qbs_borel"
    and qbs_morphism_product_candidate: "⋀i. (λx. x i) ∈ qbs_borel →⇩Q qbs_borel"
    and uminus_ereal_qbs_morphism: "(uminus :: _ ⇒ ereal) ∈ qbs_borel →⇩Q qbs_borel"
  by(auto intro!: set_mp[OF r_preserves_morphisms])

lemma qbs_morphism_sum:
  fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, topological_comm_monoid_add}"
  assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
  shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_suminf_order:
  fixes f :: "nat ⇒ 'a ⇒ 'b::{complete_linorder, second_countable_topology, linorder_topology, topological_comm_monoid_add}"
  assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
  shows " (λx. ∑i. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_prod:
  fixes f :: "'c ⇒ 'a ⇒ 'b::{second_countable_topology, real_normed_field}"
  assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
  shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_Min:
  "finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Min ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ X →⇩Q qbs_borel"
  by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_Max:
  "finite I ⟹ (⋀i. i ∈ I ⟹ f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Max ((λi. f i x)`I) :: 'b::{second_countable_topology, linorder_topology}) ∈ X →⇩Q qbs_borel"
  by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_Max2:
  fixes f::"_ ⇒ _ ⇒ 'a::{second_countable_topology, dense_linorder, linorder_topology}"
  shows "finite I ⟹ (⋀i. f i ∈ X →⇩Q qbs_borel) ⟹ (λx. Max{f i x |i. i ∈ I}) ∈ X →⇩Q qbs_borel"
  by(simp add: lr_adjunction_correspondence)

lemma [qbs]:
  shows qbs_morphism_liminf: "liminf ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
    and qbs_morphism_limsup: "limsup ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
    and qbs_morphism_lim: "lim ∈ (qbs_count_space UNIV ⇒⇩Q qbs_borel) ⇒⇩Q (qbs_borel :: 'a :: {complete_linorder, second_countable_topology, linorder_topology} quasi_borel)"
proof(safe intro!: qbs_morphismI)
  fix f :: "real ⇒ nat ⇒ 'a"
  assume "f ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q borel⇩Q)"
  then have [measurable]:"⋀i. (λr. f r i) ∈ borel_measurable borel"
    by(auto simp: qbs_Mx_is_morphisms) (metis PiQ_qbs_borel measurable_product_then_coordinatewise qbs_Mx_is_morphisms qbs_Mx_qbs_borel qbs_morphism_product_iff)
  show "liminf ∘ f ∈ qbs_Mx borel⇩Q" "limsup ∘ f ∈ qbs_Mx borel⇩Q" "lim ∘ f ∈ qbs_Mx borel⇩Q"
    by(auto simp: qbs_Mx_is_morphisms lr_adjunction_correspondence comp_def)
qed

lemma qbs_morphism_SUP:
  fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
  assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel"
  shows "(λx. ⨆ i∈I. F i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_INF:
  fixes F :: "_ ⇒ _ ⇒ _::{complete_linorder, linorder_topology, second_countable_topology}"
  assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel"
  shows "(λx. ⨅ i∈I. F i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_cSUP:
  fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
  assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ bdd_above ((λi. F i x) ` I)"
  shows "(λx. ⨆ i∈I. F i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence space_L)

lemma qbs_morphism_cINF:
  fixes F :: "_ ⇒ _ ⇒ 'a::{conditionally_complete_linorder, linorder_topology, second_countable_topology}"
  assumes "countable I" "⋀i. i ∈ I ⟹ F i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ bdd_below ((λi. F i x) ` I)"
  shows "(λx. ⨅ i∈I. F i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence space_L)

lemma qbs_morphism_lim_metric:
  fixes f :: "nat ⇒ 'a ⇒ 'b::{banach, second_countable_topology}"
  assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
  shows "(λx. lim (λi. f i x)) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_LIMSEQ_metric:
  fixes f :: "nat ⇒ 'a ⇒ 'b :: metric_space"
  assumes "⋀i. f i ∈ X →⇩Q qbs_borel" "⋀x. x ∈ qbs_space X ⟹ (λi. f i x) ⇢ g x"
  shows "g ∈ X →⇩Q qbs_borel"
  using borel_measurable_LIMSEQ_metric[where M="qbs_to_measure X"] assms
  by(auto simp add: lr_adjunction_correspondence space_L)

lemma power_qbs_morphism[qbs]:
 "(power :: (_ ::{power,real_normed_algebra}) ⇒ nat ⇒ _) ∈ qbs_borel →⇩Q qbs_count_space UNIV ⇒⇩Q qbs_borel"
  by(rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space set_mp[OF r_preserves_morphisms])

lemma power_ennreal_qbs_morphism[qbs]:
 "(power :: ennreal ⇒ nat ⇒ _) ∈ qbs_borel →⇩Q qbs_count_space UNIV ⇒⇩Q qbs_borel"
  by(rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space set_mp[OF r_preserves_morphisms])

lemma qbs_morphism_compw: "(^^) ∈ (X ⇒⇩Q X) →⇩Q  qbs_count_space UNIV ⇒⇩Q (X ⇒⇩Q X)"
proof(rule arg_swap_morphism,rule qbs_morphism_count_space)
  fix n
  show "(λy. y ^^ n) ∈ X ⇒⇩Q X →⇩Q X ⇒⇩Q X"
    by(induction n) simp_all
qed

lemma qbs_morphism_compose_n[qbs]:
  assumes [qbs]: "f ∈ X →⇩Q X"
  shows "(λn. f^^n) ∈ qbs_count_space UNIV →⇩Q X ⇒⇩Q X"
proof(intro qbs_morphism_count_space)
  fix n
  show "f ^^ n ∈ X →⇩Q X"
    by (induction n) simp_all
qed

lemma qbs_morphism_compose_n':
  assumes "f ∈ X →⇩Q X"
  shows "f^^n ∈ X →⇩Q X"
  using qbs_morphism_space[OF qbs_morphism_compose_n[OF assms]] by(simp add: exp_qbs_space qbs_space_R)

lemma qbs_morphism_uminus_eq_ereal[simp]:
  "(λx. - f x :: ereal) ∈ X →⇩Q qbs_borel ⟷ f ∈ X →⇩Q qbs_borel" (is "?l = ?r")
  by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_ereal_iff:
  shows "(λx. ereal (f x)) ∈ X →⇩Q qbs_borel⟷ f ∈ X →⇩Q qbs_borel"
  by(simp add: borel_measurable_ereal_iff lr_adjunction_correspondence)

lemma qbs_morphism_ereal_sum:
  fixes f :: "'c ⇒ 'a ⇒ ereal"
  assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
  shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_ereal_prod:
  fixes f :: "'c ⇒ 'a ⇒ ereal"
  assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
  shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_extreal_suminf:
  fixes f :: "nat ⇒ 'a ⇒ ereal"
  assumes "⋀i. f i ∈ X →⇩Q qbs_borel"
  shows "(λx. (∑i. f i x)) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_ennreal_iff:
  assumes "⋀x. x ∈ qbs_space X ⟹ 0 ≤ f x"
  shows "(λx. ennreal (f x)) ∈ X →⇩Q qbs_borel ⟷ f ∈ X →⇩Q qbs_borel"
  using borel_measurable_ennreal_iff[where M="qbs_to_measure X"] assms
  by(simp add: space_L lr_adjunction_correspondence)

lemma qbs_morphism_prod_ennreal:
  fixes f :: "'c ⇒ 'a ⇒ ennreal"
  assumes "⋀i. i ∈ S ⟹ f i ∈ X →⇩Q qbs_borel"
  shows "(λx. ∏i∈S. f i x) ∈ X →⇩Q qbs_borel"
  using assms by(simp add: space_L lr_adjunction_correspondence)

lemma count_space_qbs_morphism:
 "f ∈ qbs_count_space (UNIV :: 'a set) →⇩Q qbs_borel"
  by(auto intro!: set_mp[OF r_preserves_morphisms])

declare count_space_qbs_morphism[where 'a="_ :: countable",qbs]

lemma count_space_count_space_qbs_morphism:
 "f ∈ qbs_count_space (UNIV :: (_ :: countable) set) →⇩Q  qbs_count_space (UNIV :: (_ :: countable) set)"
  by(auto intro!: set_mp[OF r_preserves_morphisms])

lemma qbs_morphism_case_nat':
  assumes [qbs]: "i = 0 ⟹ f ∈ X →⇩Q Y"
    "⋀j. i = Suc j ⟹ (λx. g x j) ∈ X →⇩Q Y"
  shows "(λx. case_nat (f x) (g x) i) ∈ X →⇩Q Y"
  by (cases i) simp_all

lemma qbs_morphism_case_nat[qbs]:
  "case_nat ∈ X →⇩Q (qbs_count_space UNIV ⇒⇩Q X) ⇒⇩Q qbs_count_space UNIV ⇒⇩Q X"
  by(rule curry_preserves_morphisms, rule arg_swap_morphism) (auto intro!: qbs_morphism_count_space qbs_morphism_case_nat')


lemma qbs_morphism_case_nat'':
  assumes "f ∈ X →⇩Q Y" "g ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
  shows "(λx. case_nat (f x) (g x)) ∈ X →⇩Q (Π⇩Q i∈UNIV. Y)"
  using assms by (simp add: qbs_morphism_product_iff)

lemma qbs_morphism_rec_nat[qbs]: "rec_nat ∈ X →⇩Q (count_space UNIV ⇒⇩Q X ⇒⇩Q X) ⇒⇩Q count_space UNIV ⇒⇩Q X"
proof(rule curry_preserves_morphisms,rule arg_swap_morphism,rule qbs_morphism_count_space)
  fix n
  show "(λy. rec_nat (fst y) (snd y) n) ∈ X ⨂⇩Q (qbs_count_space UNIV ⇒⇩Q X ⇒⇩Q X) →⇩Q X"
    by (induction n) simp_all
qed

lemma qbs_morphism_Max_nat:
  fixes P :: "nat ⇒ 'a ⇒ bool"
  assumes "⋀i. P i ∈ X →⇩Q qbs_count_space UNIV"
  shows "(λx. Max {i. P i x}) ∈ X →⇩Q qbs_count_space UNIV"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_Min_nat:
  fixes P :: "nat ⇒ 'a ⇒ bool"
  assumes "⋀i. P i ∈ X →⇩Q qbs_count_space UNIV"
  shows "(λx. Min {i. P i x}) ∈ X →⇩Q qbs_count_space UNIV"
  using assms by(simp add: lr_adjunction_correspondence)

lemma qbs_morphism_sum_nat:
  fixes f :: "'c ⇒ 'a ⇒ nat"
  assumes "⋀i. i ∈ S ⟹ f i ∈X →⇩Q qbs_count_space UNIV"
  shows "(λx. ∑i∈S. f i x) ∈ X →⇩Q qbs_count_space UNIV"
  using assms by(simp add: lr_adjunction_correspondence)


lemma qbs_morphism_case_enat':
  assumes f[qbs]: "f ∈ X →⇩Q qbs_count_space UNIV" and [qbs]: "⋀i. g i ∈ X →⇩Q Y" "h ∈ X →⇩Q Y"
  shows "(λx. case f x of enat i ⇒ g i x | ∞ ⇒ h x) ∈ X →⇩Q Y"
proof (rule qbs_morphism_compose_countable[OF _ f])
  fix i                 
  show "(λx. case i of enat i ⇒ g i x | ∞ ⇒ h x) ∈ X →⇩Q Y"
    by (cases i) simp_all
qed

lemma qbs_morphism_case_enat[qbs]: "case_enat ∈ qbs_space ((qbs_count_space UNIV ⇒⇩Q X) ⇒⇩Q X ⇒⇩Q qbs_count_space UNIV ⇒⇩Q X)"
proof -
  note qbs_morphism_case_enat'[qbs]
  show ?thesis
  by(auto intro!: curry_preserves_morphisms,rule qbs_morphismI) (simp add: qbs_Mx_is_morphisms comp_def, qbs, simp_all)
qed

lemma qbs_morphism_restrict[qbs]:
  assumes X: "⋀i. i ∈ I ⟹ f i ∈ X →⇩Q (Y i)"
  shows "(λx. λi∈I. f i x) ∈ X →⇩Q (Π⇩Q i∈I. Y i)"
  using assms by(auto intro!: product_qbs_canonical1)

lemma If_qbs_morphism[qbs]: "If ∈ qbs_count_space UNIV →⇩Q X ⇒⇩Q X ⇒⇩Q X"
proof(rule qbs_morphismI)
  show "α ∈ qbs_Mx (count_space⇩Q UNIV) ⟹ If ∘ α ∈ qbs_Mx (X ⇒⇩Q X ⇒⇩Q X)" for α
    by(auto intro!: qbs_Mx_indicat[where S="{r. α (_ (_ r))}",simplified] simp: qbs_Mx_count_space exp_qbs_Mx)
qed

lemma normal_density_qbs[qbs]: "normal_density ∈ qbs_borel →⇩Q qbs_borel ⇒⇩Q qbs_borel ⇒⇩Q qbs_borel"
proof -
  have [simp]:"normal_density = (λμ σ x. 1 / sqrt (2 * pi * σ⇧2) * exp (-(x - μ)⇧2/ (2 * σ⇧2)))"
    by standard+ (auto simp: normal_density_def)
  show ?thesis
    by simp
qed

lemma erlang_density_qbs[qbs]: "erlang_density ∈ qbs_count_space UNIV →⇩Q qbs_borel ⇒⇩Q qbs_borel ⇒⇩Q qbs_borel"
proof -
  have [simp]: "erlang_density = (λk l x. (if x < 0 then 0 else (l^(Suc k) * x^k * exp (- l * x)) / fact k))"
    by standard+ (auto simp: erlang_density_def)
  show ?thesis
    by simp
qed

lemma list_nil_qbs[qbs]: "[] ∈ qbs_space (list_qbs X)"
  by(simp add: list_qbs_space)

lemma list_cons_qbs_morphism: "list_cons ∈ X →⇩Q (list_of X) ⇒⇩Q (list_of X)"
proof(intro curry_preserves_morphisms pair_qbs_morphismI)
  fix α β
  assume h:"α ∈ qbs_Mx X"
           "β ∈ qbs_Mx (list_of 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: coprod_qbs_Mx_def list_of_def coprod_qbs_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 (list_of X)"
    unfolding list_of_def
  proof(rule coprod_qbs_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 (list_of 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'[where f="(λl x. x # (to_list l)) ∘ from_list"])
    show " (λl x. x # to_list l) ∘ from_list ∈ list_qbs X →⇩Q X ⇒⇩Q list_qbs X"
    proof(rule qbs_morphism_comp[where Y="list_of X"])
      show " (λl x. x # to_list l) ∈ list_of X →⇩Q X ⇒⇩Q list_qbs X"
      proof(rule curry_preserves_morphisms)
        show "(λlx. snd lx # to_list (fst lx)) ∈ list_of X ⨂⇩Q X →⇩Q list_qbs X"
        proof(rule qbs_morphism_cong'[where f="to_list ∘ (λ(l,x). from_list (x # to_list l))"])
          show "to_list ∘ (λ(l, x). from_list (x # to_list l)) ∈ list_of X ⨂⇩Q X →⇩Q list_qbs X"
          proof(rule qbs_morphism_comp[where Y="list_of X"])
            show "(λ(l, x). from_list (x # to_list l)) ∈ list_of X ⨂⇩Q X →⇩Q list_of X"
              by(rule qbs_morphism_cong'[where f="(λ(l,x). list_cons x l)",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 list_of X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_of X ⇒⇩Q Y)"
  unfolding list_of_def
proof(intro curry_preserves_morphisms[OF arg_swap_morphism] coprod_qbs_canonical1')
  fix n
  show "(λx y. rec_list' (fst y) (snd y) (n, x)) ∈ (Π⇩Q i∈{..<n}. X) →⇩Q exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) Y"
  proof(induction n)
    case 0
    show ?case
    proof(rule curry_preserves_morphisms[OF qbs_morphismI])
      fix α
      assume h:"α ∈ qbs_Mx ((Π⇩Q i∈{..<0::nat}. X) ⨂⇩Q Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n::nat}. X) (exp_qbs Y Y)))"
      have "⋀r. fst (α r) = (λn. undefined)"
      proof -
        fix r
        have "⋀i. (λr. fst (α r) i) = (λr. undefined)"
          using h by(auto simp: exp_qbs_Mx PiQ_Mx  pair_qbs_Mx comp_def split_beta')
        thus "fst (α r) = (λn. undefined)"
          by(fastforce dest: fun_cong)
      qed
      hence "(λxy. rec_list' (fst (snd xy)) (snd (snd xy)) (0, fst xy)) ∘ α = (λx. fst (snd (α x)))"
        by(auto simp: rec_list'_simp1[simplified list_nil_def] comp_def split_beta')
      also have "... ∈ qbs_Mx Y"
        using h by(auto simp: pair_qbs_Mx comp_def)
      finally show "(λxy. rec_list' (fst (snd xy)) (snd (snd xy)) (0, fst xy)) ∘ α ∈ qbs_Mx Y" .
    qed
  next
    case ih:(Suc n)
    show ?case
    proof(rule qbs_morphismI)
      fix α
      assume h:"α ∈ qbs_Mx (Π⇩Q i∈{..<Suc n}. X)"
      define α' where "α' ≡ (λr. snd (list_tail (Suc n, α r)))"
      define a where "a ≡ (λr. α r 0)"
      then have ha:"a ∈ qbs_Mx X"
        using h by(auto simp: PiQ_Mx)
      have 1:"α' ∈ qbs_Mx (Π⇩Q i∈{..<n}. X)"
        using h by(fastforce simp: PiQ_Mx list_tail_def α'_def)
      hence 2: "⋀r. (n, α' r) ∈ qbs_space (list_of X)"
        using qbs_Mx_to_X[of α'] by (fastforce simp: PiQ_space coprod_qbs_space list_of_def)
      have 3: "⋀r. (Suc n, α r) ∈ qbs_space (list_of X)"
        using qbs_Mx_to_X[of α] h by (fastforce simp: PiQ_space coprod_qbs_space list_of_def)
      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 (list_of X)"
        using 1 by(auto intro!: coprod_qbs_MxI simp: PiQ_space coprod_qbs_space list_of_def)

      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 (list_of 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 (list_of X) (exp_qbs Y Y))) →⇩Q Y"
        proof(rule qbs_morphism_comp[where Y="exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q list_of 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 (list_of X) (exp_qbs Y Y)) →⇩Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q list_of 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 (list_of 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 (list_of X) (exp_qbs Y Y)) →⇩Q list_of 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 (list_of 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 (list_of X) (exp_qbs Y Y))" Y] qbs_Mx_is_morphisms[of "exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"]
              by(fastforce simp: split_beta' list_of_def)
          qed qbs
        next
          show "(λ(y, x1, x2, x3). y x1 x2 x3) ∈ exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) ⨂⇩Q X ⨂⇩Q list_of X ⨂⇩Q Y →⇩Q Y"
            by simp
        qed
        finally show ?thesis
          by(simp add: exp_qbs_Mx')
      qed
      finally show "(λx y. rec_list' (fst y) (snd y) (Suc n, x)) ∘ α ∈ qbs_Mx (exp_qbs (Y ⨂⇩Q exp_qbs X (exp_qbs (⨿⇩Q n∈UNIV. Π⇩Q i∈{..<n}. X) (exp_qbs Y Y))) Y)"
        by(simp add: list_of_def)
    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="list_of X"]])
    show "(λl' (y,f). rec_list y f (to_list l')) ∈ list_of X →⇩Q Y ⨂⇩Q (X ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q Y"
      apply(rule arg_swap_morphism,simp only: split_beta' list_qbs_def)
      apply(rule uncurry_preserves_morphisms)
      apply(rule arg_swap_morphism)
      apply(rule arg_swap_morphism')
      apply(rule qbs_morphism_cong'[OF _  arg_swap_morphism_map_qbs1[OF arg_swap_morphism'[OF arg_swap_morphism[OF rec_list_morphism']]]])
      apply(auto simp: rec_list'_def from_list_to_list_ident)
      done
  qed(auto simp: from_list_to_list_ident list_qbs_def to_list_from_list_ident intro!: map_qbs_morphism_inverse_f)
qed

hide_const (open) list_nil list_cons list_head list_tail from_list rec_list' to_list'

hide_fact (open) list_simp1 list_simp2 list_simp3 list_simp4 list_simp5 list_simp6 list_simp7 from_list_in_list_of' list_cons_qbs_morphism rec_list'_simp1
          to_list_from_list_ident from_list_in_list_of to_list_set to_list_simp1 to_list_simp2 list_head_def list_tail_def from_list_length
          list_cons_in_list_of rec_list_morphism' rec_list'_simp2 list_decomp1 list_destruct_rule list_induct_rule from_list_to_list_ident

corollary case_list_morphism[qbs]: "case_list ∈ qbs_space ((Y :: 'b quasi_borel) ⇒⇩Q ((X :: 'a quasi_borel) ⇒⇩Q list_qbs X ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y)"
proof -
  have [simp]:"case_list = (λy (f :: 'a ⇒ 'a list ⇒ 'b) l. rec_list y (λx l' y. f x l') l)"
  proof standard+
    fix y :: 'b and f :: "'a ⇒ 'a list ⇒ 'b" and l :: "'a list"
    show "(case l of [] ⇒ y | x # xa ⇒ f x xa) = rec_list y (λx l' y. f x l') l"
      by (cases l) auto
  qed
  show ?thesis
    by simp
qed

lemma fold_qbs_morphism[qbs]: "fold ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y)"
proof -
  have [simp]:"fold = (λf l. rec_list id (λx xs l. l ∘ f x) l)"
    apply standard+
    subgoal for f l x
      by(induction l arbitrary: x) simp_all
    done
  show ?thesis
    by simp
qed

lemma [qbs]:
  shows foldr_qbs_morphism: "foldr ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q Y ⇒⇩Q Y)"
    and foldl_qbs_morphism: "foldl ∈ qbs_space ((X ⇒⇩Q Y ⇒⇩Q X) ⇒⇩Q X ⇒⇩Q list_qbs Y ⇒⇩Q X)"
    and zip_qbs_morphism: "zip ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs Y ⇒⇩Q list_qbs (pair_qbs X Y))"
    and append_qbs_morphism: "append ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
    and concat_qbs_morphism: "concat ∈ qbs_space (list_qbs (list_qbs X) ⇒⇩Q list_qbs X)"
    and drop_qbs_morphism: "drop ∈ qbs_space (qbs_count_space UNIV ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
    and take_qbs_morphism: "take ∈ qbs_space (qbs_count_space UNIV ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
    and rev_qbs_morphism: "rev ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X)"
  by(auto simp: foldr_def foldl_def zip_def append_def concat_def drop_def take_def rev_def)

lemma [qbs]:
  fixes X :: "'a quasi_borel" and Y :: "'b quasi_borel"
  shows map_qbs_morphism: "map ∈ qbs_space ((X ⇒⇩Q Y) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs Y)" (is ?map)
    and fileter_qbs_morphism: "filter ∈ qbs_space ((X ⇒⇩Q count_space⇩Q UNIV) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?filter)
    and length_qbs_morphism: "length ∈ qbs_space (list_qbs X ⇒⇩Q qbs_count_space UNIV)" (is ?length)
    and tl_qbs_morphism: "tl ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X)" (is ?tl)
    and list_all_qbs_morphism: "list_all ∈ qbs_space ((X ⇒⇩Q qbs_count_space UNIV) ⇒⇩Q list_qbs X ⇒⇩Q qbs_count_space UNIV)" (is ?list_all)
    and bind_list_qbs_morphism: "(⤜) ∈ qbs_space (list_qbs X ⇒⇩Q (X ⇒⇩Q list_qbs Y) ⇒⇩Q list_qbs Y)" (is ?bind)
proof -
  have [simp]: "map = (λf. rec_list [] (λx xs l. f x # l))"
    apply standard+
    subgoal for f l
      by(induction l) simp_all
    done
  have [simp]: "filter = (λP. rec_list [] (λx xs l. if P x then x # l else l))"
    apply standard+
    subgoal for f l
      by(induction l) simp_all
    done
  have [simp]: "length = (λl. foldr (λ_ n. Suc n) l 0)"
    apply standard
    subgoal for l
      by (induction l) simp_all
    done
  have [simp]: "tl = (λl. case l of [] ⇒ [] | _ # xs ⇒ xs)"
    by standard (simp add: tl_def)
  have [simp]: "list_all = (λP xs. foldr (λx b. b ∧ P x) xs True)"
    apply (standard,standard)
    subgoal for P xs
      by(induction xs arbitrary: P) auto
    done
  have [simp]: "List.bind = (λxs f. concat (map f xs))"
    by standard+ (simp add: List.bind_def)
  show ?map  ?filter ?length ?tl ?list_all ?bind
    by simp_all
qed

lemma list_eq_qbs_morphism[qbs]:
  assumes [qbs]: "(=) ∈ qbs_space (X ⇒⇩Q X ⇒⇩Q count_space UNIV)"
  shows "(=) ∈ qbs_space (list_qbs X ⇒⇩Q list_qbs X ⇒⇩Q count_space UNIV)"
proof -
  have [simp]:"(=) = (λxs ys. length xs = length ys ∧ list_all (case_prod (=)) (zip xs ys))"
    using Ball_set list_eq_iff_zip_eq by fastforce
  show ?thesis
    by simp
qed

lemma insort_key_qbs_morphism[qbs]:
  shows "insort_key ∈ qbs_space ((X ⇒⇩Q (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel)) ⇒⇩Q X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?g1)
    and "insort_key ∈ qbs_space ((X ⇒⇩Q count_space⇩Q (UNIV :: (_ :: countable) set)) ⇒⇩Q X ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)" (is ?g2)
proof -
  have [simp]:"insort_key = (λf x. rec_list [x] (λy ys l. if f x ≤ f y then x#y#ys else y#l))"
    apply standard+
    subgoal for f x l
      by(induction l) simp_all
    done
  show ?g1 ?g2
    by simp_all
qed

lemma sort_key_qbs_morphism[qbs]:
  shows "sort_key ∈ qbs_space ((X ⇒⇩Q (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel)) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
    and "sort_key ∈ qbs_space ((X ⇒⇩Q count_space⇩Q (UNIV :: (_ :: countable) set)) ⇒⇩Q list_qbs X ⇒⇩Q list_qbs X)"
  unfolding sort_key_def by simp_all

lemma sort_qbs_morphism[qbs]:
  shows "sort ∈ list_qbs (borel⇩Q ::'b :: {second_countable_topology, linorder_topology} quasi_borel) →⇩Q list_qbs borel⇩Q"
    and "sort ∈ list_qbs (count_space⇩Q (UNIV :: (_ :: countable) set)) →⇩Q list_qbs (count_space⇩Q UNIV)"
  by simp_all

subsubsection ‹ Morphism Pred›
abbreviation "qbs_pred X P ≡ P ∈ X →⇩Q qbs_count_space (UNIV :: bool set)"

lemma qbs_pred_iff_measurable_pred:
 "qbs_pred X P = Measurable.pred (qbs_to_measure X) P"
  by(simp add: lr_adjunction_correspondence)

lemma(in standard_borel) qbs_pred_iff_measurable_pred:
 "qbs_pred (measure_to_qbs M) P = Measurable.pred M P"
  by(simp add: qbs_pred_iff_measurable_pred measurable_cong_sets[OF lr_sets_ident refl])

lemma qbs_pred_iff_sets:
"{x ∈space (qbs_to_measure X). P x} ∈ sets (qbs_to_measure X) ⟷ qbs_pred X P"
  by (simp add: Measurable.pred_def lr_adjunction_correspondence space_L)

lemma
  assumes [qbs]:"P ∈ X →⇩Q Y ⇒⇩Q qbs_count_space UNIV" "f ∈ X →⇩Q Y"
  shows indicator_qbs_morphism''': "(λx. indicator {y. P x y} (f x)) ∈ X →⇩Q qbs_borel" (is ?g1)
    and indicator_qbs_morphism'': "(λx. indicator {y∈qbs_space Y. P x y} (f x)) ∈ X →⇩Q qbs_borel" (is ?g2)
proof -
  have [simp]:"{x ∈ qbs_space X. P x (f x)} = {x ∈ qbs_space X. f x ∈ qbs_space Y ∧ P x (f x)}"
    using qbs_morphism_space[OF assms(2)] by blast
  show ?g1 ?g2
    using qbs_morphism_app[OF assms,simplified qbs_pred_iff_sets[symmetric]] qbs_morphism_space[OF assms(2)]
    by(auto intro!: borel_measurable_indicator' simp: lr_adjunction_correspondence space_L)
qed

lemma
  assumes [qbs]:"P ∈ X →⇩Q Y ⇒⇩Q qbs_count_space UNIV"
  shows indicator_qbs_morphism[qbs]:"(λx. indicator {y ∈ qbs_space Y. P x y}) ∈ X →⇩Q Y ⇒⇩Q qbs_borel" (is ?g1)
    and indicator_qbs_morphism':"(λx. indicator {y. P x y}) ∈ X →⇩Q Y ⇒⇩Q qbs_borel" (is ?g2)
proof -
  note indicator_qbs_morphism''[qbs] indicator_qbs_morphism'''[qbs]
  show ?g1 ?g2
    by(auto intro!: curry_preserves_morphisms[OF pair_qbs_morphismI] simp: qbs_Mx_is_morphisms)
qed

lemma indicator_qbs[qbs]:
  assumes "qbs_pred X P"
  shows "indicator {x. P x} ∈ X →⇩Q qbs_borel"
  using assms by(auto simp: lr_adjunction_correspondence)

lemma All_qbs_pred[qbs]: "qbs_pred (count_space⇩Q (UNIV :: ('a :: countable) set) ⇒⇩Q count_space⇩Q UNIV) All"
proof(rule qbs_morphismI)
  fix a :: "real ⇒ 'a ⇒ bool"
  assume "a ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q count_space⇩Q UNIV)"
  hence [measurable]: "⋀f g. f ∈ borel_measurable borel ⟹ g ∈ borel →⇩M count_space UNIV ⟹ (λx::real. a (f x) (g x)) ∈ borel →⇩M count_space UNIV"
    by(auto simp add: exp_qbs_Mx qbs_Mx_R)
  show " All ∘ a ∈ qbs_Mx (count_space⇩Q UNIV)"
    by(simp add: comp_def qbs_Mx_R)
qed

lemma Ex_qbs_pred[qbs]: "qbs_pred (count_space⇩Q (UNIV :: ('a :: countable) set) ⇒⇩Q count_space⇩Q UNIV) Ex"
proof(rule qbs_morphismI)
  fix a :: "real ⇒ 'a ⇒ bool"
  assume "a ∈ qbs_Mx (count_space⇩Q UNIV ⇒⇩Q count_space⇩Q UNIV)"
  hence [measurable]: "⋀f g. f ∈ borel_measurable borel ⟹ g ∈ borel →⇩M count_space UNIV ⟹ (λx::real. a (f x) (g x)) ∈ borel →⇩M count_space UNIV"
    by(auto simp add: exp_qbs_Mx qbs_Mx_R)
  show "Ex ∘ a ∈ qbs_Mx (count_space⇩Q UNIV)"
    by(simp add: comp_def qbs_Mx_R)
qed

lemma Ball_qbs_pred_countable:
  assumes "⋀i::'a :: countable. i ∈ I ⟹ qbs_pred X (P i)"
  shows "qbs_pred X (λx. ∀x∈I. P i x)"
  using assms by(simp add: qbs_pred_iff_measurable_pred)

lemma Ball_qbs_pred:
  assumes "finite I" "⋀i. i ∈ I ⟹ qbs_pred X (P i)"
  shows "qbs_pred X (λx. ∀x∈I. P i x)"
  using assms by(simp add: qbs_pred_iff_measurable_pred)

lemma Bex_qbs_pred_countable:
  assumes "⋀i::'a :: countable. i ∈ I ⟹ qbs_pred X (P i)"
  shows "qbs_pred X (λx. ∃x∈I. P i x)"
  using assms by(simp add: qbs_pred_iff_measurable_pred)

lemma Bex_qbs_pred:
  assumes "finite I" "⋀i. i ∈ I ⟹ qbs_pred X (P i)"
  shows "qbs_pred X (λx. ∃x∈I. P i x)"
  using assms by(simp add: qbs_pred_iff_measurable_pred)

lemma qbs_morphism_If_sub_qbs:
  assumes [qbs]: "qbs_pred X P"
      and [qbs]: "f ∈ sub_qbs X {x∈qbs_space X. P x} →⇩Q Y" "g ∈ sub_qbs X {x∈qbs_space X. ¬ P x} →⇩Q Y"
    shows "(λx. if P x then f x else g x) ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
  fix α
  assume h:"α ∈ qbs_Mx X"
  interpret standard_borel_ne "borel :: real measure" by simp
  have [measurable]: "Measurable.pred borel (λx. P (α x))"
    using h by(simp add: qbs_pred_iff_measurable_pred[symmetric] qbs_Mx_is_morphisms)
  consider "qbs_space X = {}" 
    | "{x∈qbs_space X. ¬ P x} = qbs_space X"
    | "{x∈qbs_space X. P x} = qbs_space X"
    | "{x∈qbs_space X. P x} ≠ {}" "{x∈qbs_space X. ¬ P x} ≠ {}" by blast
  then show "(λx. if P x then f x else g x) ∘ α ∈ qbs_Mx Y" (is "?f ∈ _")
  proof cases
    case 1
    with h show ?thesis
      by(simp add: qbs_empty_equiv)
  next
    case 2
    have [simp]:"(λx. if P x then f x else g x) ∘ α = g ∘ α"
      by standard (use qbs_Mx_to_X[OF h] 2 in auto)
    show ?thesis
      using 2 qbs_morphism_Mx[OF assms(3)] h by(simp add: sub_qbs_ident)
  next
    case 3
    have [simp]:"(λx. if P x then f x else g x) ∘ α = f ∘ α"
      by standard (use qbs_Mx_to_X[OF h] 3 in auto)
    show ?thesis
      using 3 qbs_morphism_Mx[OF assms(2)] h by(simp add: sub_qbs_ident)
  next
    case 4
    then obtain x0 x1 where
     x0:"x0 ∈ qbs_space X" "P x0" and x1:"x1 ∈ qbs_space X" "¬ P x1"
      by blast
    define a0 where "a0 = (λr. if P (α r) then α r else x0)"
    define a1 where "a1 = (λr. if ¬ P (α r) then α r else x1)"
    have "a0 ∈ qbs_Mx (sub_qbs X {x∈qbs_space X. P x})" "a1 ∈ qbs_Mx (sub_qbs X {x∈qbs_space X. ¬ P x})"
      using x0 x1 qbs_Mx_to_X[OF h] h
      by(auto simp: sub_qbs_Mx a0_def a1_def intro!: qbs_closed3_dest2'[of UNIV "λr. P (α r)" "λb r. if b then α r else x0"]) (simp_all add: qbs_Mx_is_morphisms)
    from qbs_morphism_Mx[OF assms(2) this(1)] qbs_morphism_Mx[OF assms(3) this(2)]
    have h0:"(λr. f (a0 r)) ∈ qbs_Mx Y" "(λr. g (a1 r)) ∈ qbs_Mx Y"
      by (simp_all add: comp_def)
    have [simp]:"(λx. if P x then f x else g x) ∘ α = (λr. if P (α r) then f (a0 r) else g (a1 r))"
      by standard (auto simp: comp_def a0_def a1_def)
    show "(λx. if P x then f x else g x) ∘ α ∈ qbs_Mx Y"
      using h h0 by(simp add: qbs_Mx_is_morphisms)
  qed
qed

subsubsection ‹ The Adjunction w.r.t. Ordering›
lemma l_mono: "mono qbs_to_measure"
proof
  fix X Y :: "'a quasi_borel"
  show "X ≤ Y ⟹ qbs_to_measure X ≤ qbs_to_measure Y"
  proof(induction rule: less_eq_quasi_borel.induct)
    case (1 X Y)
    then show ?case
      by(simp add: less_eq_measure.intros(1) space_L)
  next
    case (2 X Y)
    then have "sigma_Mx X ⊆ sigma_Mx Y"
      by(auto simp add: sigma_Mx_def)
    then consider "sigma_Mx X ⊂ sigma_Mx Y" | "sigma_Mx X = sigma_Mx Y"
      by auto
    then show ?case
      apply(cases)
       apply(rule less_eq_measure.intros(2))
        apply(simp_all add: 2 space_L sets_L)
      by(rule less_eq_measure.intros(3),simp_all add: 2 sets_L space_L emeasure_L)
  qed
qed

lemma r_mono: "mono measure_to_qbs"
proof
  fix M N :: "'a measure"
  show "M ≤ N ⟹ measure_to_qbs M ≤ measure_to_qbs N"
  proof(induction rule: less_eq_measure.inducts)
    case (1 M N)
    then show ?case
      by(simp add: less_eq_quasi_borel.intros(1) qbs_space_R)
  next
    case (2 M N)
    then have "(borel :: real measure) →⇩M N ⊆ borel →⇩M M"
      by(simp add: measurable_mono)
    then consider "(borel :: real measure) →⇩M N ⊂ borel →⇩M M" | "(borel :: real measure) →⇩M N = borel →⇩M M"
      by auto
    then show ?case
      by cases (rule less_eq_quasi_borel.intros(2),simp_all add: 2 qbs_space_R qbs_Mx_R)+
  next
    case (3 M N)
    then show ?case
      apply -
      by(rule less_eq_quasi_borel.intros(2)) (simp_all add: measurable_mono qbs_space_R qbs_Mx_R)
  qed
qed

lemma rl_order_adjunction:
  "X ≤ qbs_to_measure Y ⟷ measure_to_qbs X ≤ Y"
proof
  assume 1: "X ≤ qbs_to_measure Y"
  then show "measure_to_qbs X ≤ Y"
  proof(induction rule: less_eq_measure.cases)
    case (1 M N)
    then have [simp]:"qbs_space Y = space N"
      by(simp add: 1(2)[symmetric] space_L)
    show ?case
      by(rule less_eq_quasi_borel.intros(1),simp add: 1 qbs_space_R)
  next
    case (2 M N)
    then have [simp]:"qbs_space Y = space N"
      by(simp add: 2(2)[symmetric] space_L)
    show ?case
    proof(rule less_eq_quasi_borel.intros(2))
      show "qbs_Mx Y ⊆ qbs_Mx (measure_to_qbs X)"
        unfolding qbs_Mx_R
      proof
        fix α
        assume h:"α ∈ qbs_Mx Y"
        show "α ∈ borel →⇩M X"
        proof(rule measurableI)
          show "⋀x. α x ∈ space X"
            using qbs_Mx_to_X[OF h] by (auto simp add: 2)
        next
          fix A
          assume "A ∈ sets X"
          then have "A ∈ sets (qbs_to_measure Y)"
            using 2 by auto
          then obtain U where
            hu:"A = U ∩ space N" "(∀α∈qbs_Mx Y. α -` U ∈ sets borel)"
            by(auto simp add: sigma_Mx_def sets_L)
          have "α -` A  = α -` U"
            using qbs_Mx_to_X[OF h] by(auto simp add: hu)
          thus "α -` A ∩ space borel ∈ sets borel"
            using h hu(2) by simp
        qed
      qed
    qed(auto simp: 2 qbs_space_R)
  next
    case (3 M N)
    then have [simp]:"qbs_space Y = space N"
      by(simp add: 3(2)[symmetric] space_L)
    show ?case
    proof(rule less_eq_quasi_borel.intros(2))
      show "qbs_Mx Y ⊆ qbs_Mx (measure_to_qbs X)"
        unfolding qbs_Mx_R
      proof
        fix α
        assume h:"α ∈ qbs_Mx Y"
        show "α ∈ borel →⇩M X"
        proof(rule measurableI)
          show "⋀x. α x ∈ space X"
            using qbs_Mx_to_X[OF h] by(auto simp: 3)
        next
          fix A
          assume "A ∈ sets X"
          then have "A ∈ sets (qbs_to_measure Y)"
            using 3 by auto
          then obtain U where
            hu:"A = U ∩ space N" "(∀α∈qbs_Mx Y. α -` U ∈ sets borel)"
            by(auto simp add: sigma_Mx_def sets_L)
          have "α -` A  = α -` U"
            using qbs_Mx_to_X[OF h] by(auto simp add: hu)
          thus "α -` A ∩ space borel ∈ sets borel"
            using h hu(2) by simp
        qed
      qed
    qed(auto simp: 3 qbs_space_R)
  qed
next
  assume "measure_to_qbs X ≤ Y"
  then show "X ≤ qbs_to_measure Y"
  proof(induction rule: less_eq_quasi_borel.cases)
    case (1 A B)
    have [simp]: "space X = qbs_space A"
      by(simp add: 1(1)[symmetric] qbs_space_R)
    show ?case
      by(rule less_eq_measure.intros(1)) (simp add: 1 space_L)
  next
    case (2 A B)
    then have hmy:"qbs_Mx Y ⊆ borel →⇩M X"
      using qbs_Mx_R by blast  
    have [simp]: "space X = qbs_space A"
      by(simp add: 2(1)[symmetric] qbs_space_R)
    have "sets X ⊆ sigma_Mx Y"
    proof
      fix U
      assume hu:"U ∈ sets X"
      show "U ∈ sigma_Mx Y"
        unfolding sigma_Mx_def
      proof(safe intro!: exI[where x=U])
        show "⋀x. x ∈ U ⟹ x ∈ qbs_space Y"
          using sets.sets_into_space[OF hu]
          by(auto simp add: 2)
      next
        fix α
        assume "α ∈ qbs_Mx Y"
        then have "α ∈ borel →⇩M X"
          using hmy by(auto)
        thus "α -` U ∈ sets borel"
          using hu by(simp add: measurable_sets_borel)
      qed
    qed
    then consider "sets X = sigma_Mx Y" | "sets X ⊂ sigma_Mx Y"
      by auto
    then show ?case
    proof cases
      case 1
      show ?thesis
      proof(rule less_eq_measure.intros(3))
        show "emeasure X ≤ emeasure (qbs_to_measure Y)"
          unfolding emeasure_L
        proof(rule le_funI)
          fix U
          consider "U = {}" | "U ∉ sigma_Mx Y" | "U ≠ {} ∧ U ∈ sigma_Mx Y"
            by auto
          then show "emeasure X U ≤ (if U = {} ∨ U ∉ sigma_Mx Y then 0 else ∞)"
          proof cases
            case 1
            then show ?thesis by simp
          next
            case h:2
            then have "U ∉ sigma_Mx A"
              using qbs_Mx_sigma_Mx_contra[OF 2(3)[symmetric] 2(4)] 2(2) by auto
            hence "U ∉ sets X"
              using lr_sets 2(1) sets_L by blast
            thus ?thesis
              by(simp add: h emeasure_notin_sets)
          next
            case 3
            then show ?thesis
            by simp
        qed
      qed
    qed(simp_all add: 1 2 space_L sets_L)
    next
      case h2:2
      show ?thesis
        by(rule less_eq_measure.intros(2)) (simp add: space_L 2, simp add: h2 sets_L)
    qed
  qed
qed

end