Theory QuasiBorel

(*  Title:   QuasiBorel.thy
    Author:  Michikazu Hirata, Yasuhiko Minamide Tokyo Institute of Technology
*)

section ‹Quasi-Borel Spaces›
theory QuasiBorel
imports "HOL-Probability.Probability"
begin

subsection ‹ Definitions ›

subsubsection ‹ Quasi-Borel Spaces›
definition qbs_closed1 :: "(real  'a) set  bool"
  where "qbs_closed1 Mx  (a  Mx. f  (borel :: real measure) M (borel :: real measure). a  f  Mx)"

definition qbs_closed2 :: "['a set, (real  'a) set]  bool"
 where "qbs_closed2 X Mx  (x  X. (λr. x)  Mx)"

definition qbs_closed3 :: "(real  'a) set  bool"
 where "qbs_closed3 Mx  (P::real  nat. Fi::nat  real  'a.
                          (P  borel M count_space UNIV)  (i. Fi i  Mx)  (λr. Fi (P r) r)  Mx)"

lemma separate_measurable:
  fixes P :: "real  nat"
  assumes "i. P -` {i}  sets borel"
  shows "P  borel M count_space UNIV"
  by (auto simp add: assms measurable_count_space_eq_countable)

lemma measurable_separate:
  fixes P :: "real  nat"
  assumes "P  borel M count_space UNIV"
  shows "P -` {i}  sets borel"
  by (metis assms borel_singleton measurable_sets_borel sets.empty_sets sets_borel_eq_count_space)

definition "is_quasi_borel X Mx  Mx  UNIV  X  qbs_closed1 Mx  qbs_closed2 X Mx  qbs_closed3 Mx"

lemma is_quasi_borel_intro[simp]:
  assumes "Mx  UNIV  X"
      and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx"
    shows "is_quasi_borel X Mx"
  using assms by(simp add: is_quasi_borel_def)

typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}"
proof
  show "(UNIV, UNIV)  {(X::'a set, Mx). is_quasi_borel X Mx}"
    by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
qed

definition qbs_space :: "'a quasi_borel  'a set" where
  "qbs_space X  fst (Rep_quasi_borel X)"

definition qbs_Mx :: "'a quasi_borel  (real  'a) set" where
  "qbs_Mx X  snd (Rep_quasi_borel X)"

declare [[coercion qbs_space]]

lemma qbs_decomp : "(qbs_space X,qbs_Mx X)  {(X::'a set, Mx). is_quasi_borel X Mx}"
  by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified])

lemma qbs_Mx_to_X:
  assumes "α  qbs_Mx X"
  shows "α r  qbs_space X"
  using qbs_decomp assms by(auto simp: is_quasi_borel_def)

lemma qbs_closed1I:
  assumes "α f. α  Mx  f  borel M borel  α  f  Mx"
  shows "qbs_closed1 Mx"
  using assms by(simp add: qbs_closed1_def)

lemma qbs_closed1_dest[simp]:
  assumes "α  qbs_Mx X"
      and "f  borel M borel"
    shows "α  f  qbs_Mx X"
  using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def)

lemma qbs_closed1_dest'[simp]:
  assumes "α  qbs_Mx X"
      and "f  borel M borel"
    shows "(λr. α (f r))  qbs_Mx X"
  using qbs_closed1_dest[OF assms] by (simp add: comp_def)

lemma qbs_closed2I:
  assumes "x. x  X  (λr. x)  Mx"
  shows "qbs_closed2 X Mx"
  using assms by(simp add: qbs_closed2_def)

lemma qbs_closed2_dest[simp]:
  assumes "x  qbs_space X"
  shows "(λr. x)  qbs_Mx X"
  using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def)

lemma qbs_closed3I:
  assumes "(P :: real  nat) Fi. P  borel M count_space UNIV  (i. Fi i  Mx)
                   (λr. Fi (P r) r)  Mx"
  shows "qbs_closed3 Mx"
  using assms by(auto simp: qbs_closed3_def)

lemma qbs_closed3I':
  assumes "(P :: real  nat) Fi. (i. P -` {i}  sets borel)  (i. Fi i  Mx)
                   (λr. Fi (P r) r)  Mx"
  shows "qbs_closed3 Mx"
  using assms by(auto intro!: qbs_closed3I dest: measurable_separate)

lemma qbs_closed3_dest[simp]:
  fixes P::"real  nat" and Fi :: "nat  real  _"
  assumes "P  borel M count_space UNIV"
      and "i. Fi i  qbs_Mx X"
    shows "(λr. Fi (P r) r)  qbs_Mx X"
  using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def)

lemma qbs_closed3_dest':
  fixes P::"real  nat" and Fi :: "nat  real  _"
  assumes "i. P -` {i}  sets borel"
      and "i. Fi i  qbs_Mx X"
    shows "(λr. Fi (P r) r)  qbs_Mx X"
  using qbs_closed3_dest[OF separate_measurable[OF assms(1)] assms(2)] .

lemma qbs_closed3_dest2:
  assumes "countable I"
 and [measurable]: "P  borel M count_space I"
      and "i. i  I  Fi i  qbs_Mx X"
    shows "(λr. Fi (P r) r)  qbs_Mx X"
proof -
  have 0:"I  {}"
    using measurable_empty_iff[of "count_space I" P borel] assms(2)
    by fastforce
  define P' where "P'  to_nat_on I  P"
  define Fi' where "Fi'  Fi  (from_nat_into I)"
  have 1:"P'  borel M count_space UNIV"
    by(simp add: P'_def)
  have 2:"i. Fi' i  qbs_Mx X"
    using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def)
  have "(λr. Fi' (P' r) r)  qbs_Mx X"
    using 1 2 measurable_separate by auto
  thus ?thesis
    using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)]
    by(auto simp: Fi'_def P'_def)
qed

lemma qbs_closed3_dest2':
  assumes "countable I"
 and [measurable]: "P  borel M count_space I"
      and "i. i  range P  Fi i  qbs_Mx X"
    shows "(λr. Fi (P r) r)  qbs_Mx X"
proof -
  have 0:"range P  I = range P"
    using measurable_space[OF assms(2)] by auto
  have 1:"P  borel M count_space (range P)"
    using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"]
    by(simp add: 0)
  have 2:"countable (range P)"
    using countable_Int2[OF assms(1),of "range P"]
    by(simp add: 0)
  show ?thesis
    by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)])
qed

lemma qbs_Mx_indicat:
  assumes "S  sets borel" "α  qbs_Mx X" "β  qbs_Mx X"
  shows "(λr. if r  S then α r else β r)  qbs_Mx X"
proof -
  have "(λr::real. if r  S then α r else β r) = (λr. (λb. if b then α else β) (r  S) r)"
    by(auto simp: indicator_def)
  also have "...  qbs_Mx X"
    by(rule qbs_closed3_dest2[where I=UNIV and Fi="λb. if b then α else β"]) (use assms in auto)
  finally show ?thesis .
qed

lemma qbs_space_Mx: "qbs_space X = {α x |x α. α  qbs_Mx X}"
proof safe
  fix x
  assume 1:"x  qbs_space X"
  show "xa α. x = α xa  α  qbs_Mx X"
    by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1)
qed(simp add: qbs_Mx_to_X)

lemma qbs_space_eq_Mx:
  assumes "qbs_Mx X = qbs_Mx Y"
  shows "qbs_space X = qbs_space Y"
  by(simp add: qbs_space_Mx assms)

lemma qbs_eqI:
  assumes "qbs_Mx X = qbs_Mx Y"
  shows "X = Y"
  by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms])

subsubsection ‹ Empty Space ›
definition empty_quasi_borel  :: "'a quasi_borel" where
"empty_quasi_borel  Abs_quasi_borel ({},{})"

lemma
  shows eqb_space[simp]: "qbs_space empty_quasi_borel = ({} :: 'a set)"
    and eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = ({} :: (real  'a) set)"
proof -
  have "Rep_quasi_borel empty_quasi_borel = ({} :: 'a set, {})"
    using Abs_quasi_borel_inverse by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
  thus "qbs_space empty_quasi_borel = ({} :: 'a set)" "qbs_Mx empty_quasi_borel = ({} :: (real  'a) set)"
    by(auto simp add: qbs_space_def qbs_Mx_def)
qed

lemma qbs_empty_equiv :"qbs_space X = {}  qbs_Mx X = {}"
proof safe
  fix x
  assume "qbs_Mx X = {}"
     and h:"x  qbs_space X"
  have "(λr. x)  qbs_Mx X"
    using h by simp
  thus "x  {}" using qbs_Mx X = {} by simp
qed(use qbs_Mx_to_X in blast)

lemma empty_quasi_borel_iff:
  "qbs_space X = {}  X = empty_quasi_borel"
  by(auto intro!: qbs_eqI simp: qbs_empty_equiv)

subsubsection ‹ Unit Space ›
definition unit_quasi_borel :: "unit quasi_borel" ("1Q") where
"unit_quasi_borel  Abs_quasi_borel (UNIV,UNIV)"

lemma
  shows unit_qbs_space[simp]: "qbs_space unit_quasi_borel = {()}"
    and unit_qbs_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}"
proof -
  have "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)"
    using Abs_quasi_borel_inverse by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
  thus "qbs_space unit_quasi_borel = {()}" "qbs_Mx unit_quasi_borel = {λr. ()}"
    by(auto simp add: qbs_space_def qbs_Mx_def UNIV_unit)
qed

subsubsection ‹ Sub-Spaces ›
definition sub_qbs :: "['a quasi_borel, 'a set]  'a quasi_borel" where
"sub_qbs X U  Abs_quasi_borel (qbs_space X  U,{α. α  qbs_Mx X  (r. α r  U)})"

lemma
  shows sub_qbs_space: "qbs_space (sub_qbs X U) = qbs_space X  U"
    and sub_qbs_Mx: "qbs_Mx (sub_qbs X U) = {α. α  qbs_Mx X  (r. α r  U)}"
proof -
  have "qbs_closed1 {α. α  qbs_Mx X  (r. α r  U)}" "qbs_closed2 (qbs_space X  U) {α. α  qbs_Mx X  (r. α r  U)}"
       "qbs_closed3 {α. α  qbs_Mx X  (r. α r  U)}"
    unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto
  hence "Rep_quasi_borel (sub_qbs X U) = (qbs_space X  U,{α. α  qbs_Mx X  (r. α r  U)})"
    by(auto simp: sub_qbs_def is_quasi_borel_def qbs_Mx_to_X intro!: Abs_quasi_borel_inverse)
  thus "qbs_space (sub_qbs X U) = qbs_space X  U" "qbs_Mx (sub_qbs X U) = {α. α  qbs_Mx X  (r. α r  U)}"
    by(simp_all add: qbs_Mx_def qbs_space_def)
qed

lemma sub_qbs:
  assumes "U  qbs_space X"
  shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f  UNIV  U. f  qbs_Mx X})"
  using assms by (auto simp: sub_qbs_space sub_qbs_Mx)

lemma sub_qbs_ident: "sub_qbs X (qbs_space X) = X"
  by(auto intro!: qbs_eqI simp: sub_qbs_Mx qbs_Mx_to_X)

lemma sub_qbs_sub_qbs: "sub_qbs (sub_qbs X A) B = sub_qbs X (A  B)"
  by(auto intro!: qbs_eqI simp: sub_qbs_Mx sub_qbs_space)

subsubsection ‹ Image Spaces ›
definition map_qbs :: "['a  'b]  'a quasi_borel  'b quasi_borel" where
"map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{f  α |α. α qbs_Mx X})"

lemma
  shows map_qbs_space: "qbs_space (map_qbs f X) = f ` (qbs_space X)"
    and map_qbs_Mx: "qbs_Mx (map_qbs f X) = {f  α |α. α qbs_Mx X}"
proof -
  have  "{f  α |α. α qbs_Mx X}  UNIV  f ` (qbs_space X)"
    using qbs_Mx_to_X by fastforce
  moreover have "qbs_closed1 {f  α |α. α qbs_Mx X}"
    unfolding qbs_closed1_def using qbs_closed1_dest by(fastforce simp: comp_def)
  moreover have  "qbs_closed2 (f ` (qbs_space X)) {f  α |α. α qbs_Mx X}"
    unfolding qbs_closed2_def by fastforce
  moreover have  "qbs_closed3 {f  α |α. α qbs_Mx X}"
  proof(rule qbs_closed3I')
    fix P :: "real  nat" and Fi
    assume h:"i::nat. P -` {i}  sets borel"
             "i::nat. Fi i  {f  α |α. α qbs_Mx X}"
    then obtain αi where ha: "i::nat. αi i  qbs_Mx X" "i. Fi i = f  (αi i)"
      by auto metis
    hence 1:"(λr. αi (P r) r)  qbs_Mx X"
      using h(1) qbs_closed3_dest' by blast
    show "(λr. Fi (P r) r)   {f  α |α. α qbs_Mx X}"
      by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def)
  qed
  ultimately have "Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{f  α |α. α qbs_Mx X})"
    unfolding map_qbs_def by(auto intro!: Abs_quasi_borel_inverse)
  thus "qbs_space (map_qbs f X) = f ` (qbs_space X)" "qbs_Mx (map_qbs f X) = {f  α |α. α qbs_Mx X}"
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

subsubsection ‹ Binary Product Spaces ›
definition pair_qbs :: "['a quasi_borel, 'b quasi_borel]  ('a × 'b) quasi_borel" (infixr "Q" 80) where
"pair_qbs X Y = Abs_quasi_borel (qbs_space X × qbs_space Y, {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y})"

lemma
  shows pair_qbs_space: "qbs_space (X Q Y) = qbs_space X × qbs_space Y"
    and pair_qbs_Mx: "qbs_Mx (X Q Y) = {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
proof -
  have "{f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}  UNIV  qbs_space X × qbs_space Y"
    by (auto simp: mem_Times_iff[of _ "qbs_space X" "qbs_space Y"]; use qbs_Mx_to_X in fastforce)
  moreover have "qbs_closed1 {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
    unfolding qbs_closed1_def by (metis (no_types, lifting) comp_assoc mem_Collect_eq qbs_closed1_dest)
  moreover have "qbs_closed2 (qbs_space X × qbs_space Y) {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
    unfolding qbs_closed2_def by auto
  moreover have "qbs_closed3 {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
  proof(safe intro!: qbs_closed3I)
    fix P :: "real  nat"
    fix Fi :: "nat  real  'a × 'b"
    define Fj :: "nat  real  'a" where "Fj  λj.(fst  Fi j)"
    assume "i. Fi i  {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
    then have "i. Fj i  qbs_Mx X" by (simp add: Fj_def)
    moreover assume "P  borel M count_space UNIV"
    ultimately have "(λr. Fj (P r) r)  qbs_Mx X"
      by auto
    moreover have "fst  (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
    ultimately show "fst  (λr. Fi (P r) r)  qbs_Mx X" by simp
  next
    fix P :: "real  nat"
    fix Fi :: "nat  real  'a × 'b"
    define Fj :: "nat  real  'b" where "Fj  λj.(snd  Fi j)"
    assume "i. Fi i  {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
    then have "i. Fj i  qbs_Mx Y" by (simp add: Fj_def)
    moreover assume "P  borel M count_space UNIV"
    ultimately have "(λr. Fj (P r) r)  qbs_Mx Y"
      by auto
    moreover have "snd  (λr. Fi (P r) r) = (λr. Fj (P r) r)" by (auto simp add: Fj_def)
    ultimately show "snd  (λr. Fi (P r) r)  qbs_Mx Y" by simp
  qed
  ultimately have "Rep_quasi_borel (X Q Y) = (qbs_space X × qbs_space Y, {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y})"
    unfolding pair_qbs_def by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro)
  thus "qbs_space (X Q Y) = qbs_space X × qbs_space Y" "qbs_Mx (X Q Y) = {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

lemma pair_qbs_fst:
  assumes "qbs_space Y  {}"
  shows "map_qbs fst (X Q Y) = X"
proof(rule qbs_eqI)
  obtain αy where hy:"αy  qbs_Mx Y"
    using qbs_empty_equiv[of Y] assms by auto
  show "qbs_Mx (map_qbs fst (X Q Y)) = qbs_Mx X"
    by(auto simp: map_qbs_Mx pair_qbs_Mx hy comp_def intro!: exI[where x="λr. (_ r, αy r)"])
qed

lemma pair_qbs_snd:
  assumes "qbs_space X  {}"
  shows "map_qbs snd (X Q Y) = Y"
proof(rule qbs_eqI)
  obtain αx where hx:"αx  qbs_Mx X"
    using qbs_empty_equiv[of X] assms by auto
  show "qbs_Mx (map_qbs snd (X Q Y)) = qbs_Mx Y"
    by(auto simp: map_qbs_Mx pair_qbs_Mx hx comp_def intro!: exI[where x="λr. (αx r, _ r)"])
qed

subsubsection ‹ Binary Coproduct Spaces  ›
definition copair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel]  (real => 'a + 'b) set" where
"copair_qbs_Mx X Y  
  {g.  S  sets borel.
  (S = {}    ( α1 qbs_Mx X. g = (λr. Inl (α1 r)))) 
  (S = UNIV  ( α2 qbs_Mx Y. g = (λr. Inr (α2 r)))) 
  ((S  {}  S  UNIV) 
     ( α1 qbs_Mx X.  α2 qbs_Mx Y.
          g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))))}"

definition copair_qbs :: "['a quasi_borel, 'b quasi_borel]  ('a + 'b) quasi_borel" (infixr "Q" 65) where
"copair_qbs X Y  Abs_quasi_borel (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)"

text ‹ The following is an equivalent definition of @{term copair_qbs_Mx}. ›
definition copair_qbs_Mx2 :: "['a quasi_borel, 'b quasi_borel]  (real => 'a + 'b) set" where
"copair_qbs_Mx2 X Y  
  {g. (if qbs_space X = {}  qbs_space Y = {} then False
       else if qbs_space X  {}  qbs_space Y = {} then 
                  (α1 qbs_Mx X. g = (λr. Inl (α1 r)))
       else if qbs_space X = {}  qbs_space Y  {} then 
                  (α2 qbs_Mx Y. g = (λr. Inr (α2 r)))
       else 
         (S  sets borel. α1 qbs_Mx X. α2 qbs_Mx Y.
          g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r))))) }"

lemma copair_qbs_Mx_equiv :"copair_qbs_Mx (X :: 'a quasi_borel) (Y :: 'b quasi_borel) = copair_qbs_Mx2 X Y"
proof safe
(* ⊆ *)
  fix g :: "real  'a + 'b"
  assume "g  copair_qbs_Mx X Y"
  then obtain S where hs:"S sets borel  
  (S = {}    ( α1 qbs_Mx X. g = (λr. Inl (α1 r)))) 
  (S = UNIV  ( α2 qbs_Mx Y. g = (λr. Inr (α2 r)))) 
  ((S  {}  S  UNIV) 
     ( α1 qbs_Mx X.
       α2 qbs_Mx Y.
          g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))))"
    by (auto simp add: copair_qbs_Mx_def)
  consider "S = {}" | "S = UNIV" | "S  {}  S  UNIV" by auto
  then show "g  copair_qbs_Mx2 X Y"
  proof cases
    assume "S = {}"
    from hs this have " α1 qbs_Mx X. g = (λr. Inl (α1 r))" by simp
    then obtain α1 where h1:"α1 qbs_Mx X  g = (λr. Inl (α1 r))" by auto
    have "qbs_space X  {}"
      using qbs_empty_equiv h1
      by auto
    then have "(qbs_space X  {}  qbs_space Y = {})  (qbs_space X  {}  qbs_space Y  {})"
      by simp
    then show "g  copair_qbs_Mx2 X Y"
    proof
      assume "qbs_space X  {}  qbs_space Y = {}"
      then show "g  copair_qbs_Mx2 X Y" 
        by(simp add: copair_qbs_Mx2_def  α1 qbs_Mx X. g = (λr. Inl (α1 r)))
    next
      assume "qbs_space X  {}  qbs_space Y  {}"
      then obtain α2 where "α2  qbs_Mx Y" using qbs_empty_equiv by force
      define S' :: "real set" 
        where "S'  UNIV"
      define g' :: "real  'a + 'b"
        where "g'  (λr::real. (if (r  S') then Inl (α1 r) else Inr (α2 r)))"
      from qbs_space X  {}  qbs_space Y  {} h1 α2  qbs_Mx Y
      have "g'  copair_qbs_Mx2 X Y" 
        by(force simp add: S'_def g'_def copair_qbs_Mx2_def)
      moreover have "g = g'"
        using h1 by(simp add: g'_def S'_def)
      ultimately show ?thesis
        by simp
    qed
  next
    assume "S = UNIV"
    from hs this have " α2 qbs_Mx Y. g = (λr. Inr (α2 r))" by simp
    then obtain α2 where h2:"α2 qbs_Mx Y  g = (λr. Inr (α2 r))" by auto
    have "qbs_space Y  {}"
      using qbs_empty_equiv h2
      by auto
    then have "(qbs_space X = {}  qbs_space Y  {})  (qbs_space X  {}  qbs_space Y  {})"
      by simp
    then show "g  copair_qbs_Mx2 X Y"
    proof
      assume "qbs_space X = {}  qbs_space Y  {}"
      then show ?thesis
        by(simp add: copair_qbs_Mx2_def  α2 qbs_Mx Y. g = (λr. Inr (α2 r)))
    next
      assume "qbs_space X  {}  qbs_space Y  {}"
      then obtain α1 where "α1  qbs_Mx X" using qbs_empty_equiv by force
      define S' :: "real set"
        where "S'  {}"
      define g' :: "real  'a + 'b"
        where "g'  (λr::real. (if (r  S') then Inl (α1 r) else Inr (α2 r)))"
      from qbs_space X  {}  qbs_space Y  {} h2 α1  qbs_Mx X
      have "g'  copair_qbs_Mx2 X Y" 
        by(force simp add: S'_def g'_def copair_qbs_Mx2_def)
      moreover have "g = g'"
        using h2 by(simp add: g'_def S'_def)
      ultimately show ?thesis
        by simp
    qed
  next
    assume "S  {}  S  UNIV"
    then have 
    h: " α1 qbs_Mx X.
         α2 qbs_Mx Y.
          g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))"
      using hs by simp
    then have "qbs_space X  {}  qbs_space Y  {}"
      by (metis empty_iff qbs_empty_equiv)
    thus ?thesis
      using hs h by(auto simp add: copair_qbs_Mx2_def)
  qed

(* ⊇ *)
next
  fix g :: "real  'a + 'b"
  assume "g  copair_qbs_Mx2 X Y"
  then have
  h: "if qbs_space X = {}  qbs_space Y = {} then False
      else if qbs_space X  {}  qbs_space Y = {} then 
                  (α1 qbs_Mx X. g = (λr. Inl (α1 r)))
      else if qbs_space X = {}  qbs_space Y  {} then 
                  (α2 qbs_Mx Y. g = (λr. Inr (α2 r)))
      else 
          (S  sets borel. α1 qbs_Mx X. α2 qbs_Mx Y.
           g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r))))"
    by(simp add: copair_qbs_Mx2_def)
  consider "(qbs_space X = {}  qbs_space Y = {})" |
           "(qbs_space X  {}  qbs_space Y = {})" |
           "(qbs_space X = {}  qbs_space Y  {})" |
           "(qbs_space X  {}  qbs_space Y  {})" by auto
  then show "g  copair_qbs_Mx X Y"
  proof cases
    assume "qbs_space X = {}  qbs_space Y = {}"
    then show ?thesis
      using g  copair_qbs_Mx2 X Y by(simp add: copair_qbs_Mx2_def)
  next
    assume "qbs_space X  {}  qbs_space Y = {}"
    from h this have "α1 qbs_Mx X. g = (λr. Inl (α1 r))" by simp
    thus ?thesis
      by(auto simp add: copair_qbs_Mx_def)
  next
    assume "qbs_space X = {}  qbs_space Y  {}"
    from h this have "α2 qbs_Mx Y. g = (λr. Inr (α2 r))" by simp
    thus ?thesis
      unfolding copair_qbs_Mx_def 
      by(force simp add: copair_qbs_Mx_def)
  next
    assume "qbs_space X  {}  qbs_space Y  {}"
    from h this obtain S α1 α2 where Sag:
     "S  sets borel" "α1  qbs_Mx X" "α2  qbs_Mx Y" "g = (λr. if r  S then Inl (α1 r) else Inr (α2 r))"
      by auto
    consider "S = {}" | "S = UNIV" | "S  {}" "S  UNIV" by auto
    then show "g  copair_qbs_Mx X Y"
    proof cases
      assume "S = {}"
      then have [simp]: "(λr. if r  S then Inl (α1 r) else Inr (α2 r)) = (λr. Inr (α2 r))"
        by simp
      show ?thesis
        using α2  qbs_Mx Y unfolding copair_qbs_Mx_def
        by(auto intro! : bexI[where x=UNIV] simp: Sag)
    next
      assume "S = UNIV"
      then have "(λr. if r  S then Inl (α1 r) else Inr (α2 r)) = (λr. Inl (α1 r))"
        by simp
      then show ?thesis
        using Sag by(auto simp add: copair_qbs_Mx_def)
    next
      assume "S  {}" "S  UNIV"
      then show ?thesis
        using Sag by(auto simp add: copair_qbs_Mx_def)
    qed
  qed
qed

lemma
  shows copair_qbs_space: "qbs_space (X Q Y) = qbs_space X <+> qbs_space Y" (is ?goal1)
    and copair_qbs_Mx: "qbs_Mx (X Q Y) = copair_qbs_Mx X Y" (is ?goal2)
proof -
  have "copair_qbs_Mx X Y  UNIV  qbs_space X <+> qbs_space Y"
  proof
    fix g
    assume "g  copair_qbs_Mx X Y"
    then obtain S where hs:"S sets borel  
     (S = {}    ( α1 qbs_Mx X. g = (λr. Inl (α1 r)))) 
     (S = UNIV  ( α2 qbs_Mx Y. g = (λr. Inr (α2 r)))) 
     ((S  {}  S  UNIV) 
        ( α1 qbs_Mx X.
          α2 qbs_Mx Y.
             g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))))"
      by (auto simp add: copair_qbs_Mx_def)
    consider "S = {}" | "S = UNIV" | "S  {}  S  UNIV" by auto
    then show "g  UNIV  qbs_space X <+> qbs_space Y"
    proof cases
      assume "S = {}"
      then show ?thesis
        using hs qbs_Mx_to_X by auto
    next
      assume "S = UNIV"
      then show ?thesis
        using hs qbs_Mx_to_X by auto
    next
      assume "S  {}  S  UNIV"
      then have " α1 qbs_Mx X.  α2 qbs_Mx Y.
            g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))" using hs by simp
      then show ?thesis
        by(auto dest: qbs_Mx_to_X)
    qed
  qed
  moreover have "qbs_closed1 (copair_qbs_Mx X Y)"
  proof(rule qbs_closed1I)
    fix g and f :: "real  real"
    assume "g  copair_qbs_Mx X Y" and [measurable]: "f  borel M borel"
    then have "g  copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by auto
    consider "(qbs_space X = {}  qbs_space Y = {})" |
             "(qbs_space X  {}  qbs_space Y = {})" |
             "(qbs_space X = {}  qbs_space Y  {})" |
             "(qbs_space X  {}  qbs_space Y  {})" by auto
    then have "g  f  copair_qbs_Mx2 X Y"
    proof cases
      assume "qbs_space X = {}  qbs_space Y = {}"
      then show ?thesis
        using g  copair_qbs_Mx2 X Y qbs_empty_equiv by(simp add: copair_qbs_Mx2_def)
    next
      assume "qbs_space X  {}  qbs_space Y = {}"
      then obtain α1 where h1:"α1 qbs_Mx X  g = (λr. Inl (α1 r))"
        using g  copair_qbs_Mx2 X Y by(auto simp add: copair_qbs_Mx2_def)
      then have "α1  f  qbs_Mx X"
        by auto
      moreover have "g  f = (λr. Inl ((α1  f) r))"
        using h1 by auto
      ultimately show ?thesis
        using qbs_space X  {}  qbs_space Y = {} by(force simp add: copair_qbs_Mx2_def)
    next
      assume "(qbs_space X = {}  qbs_space Y  {})"
      then obtain α2 where h2:"α2 qbs_Mx Y  g = (λr. Inr (α2 r))"
        using g  copair_qbs_Mx2 X Y by(auto simp add: copair_qbs_Mx2_def)
      then have "α2  f  qbs_Mx Y"
        by auto
      moreover have "g  f = (λr. Inr ((α2  f) r))"
        using h2 by auto
      ultimately show ?thesis
        using (qbs_space X = {}  qbs_space Y  {}) by(force simp add: copair_qbs_Mx2_def)
    next
      assume "qbs_space X  {}  qbs_space Y  {}"
      then have "S  sets borel. α1 qbs_Mx X. α2 qbs_Mx Y.
          g = (λr::real. (if (r  S) then Inl (α1 r) else Inr (α2 r)))"
        using g  copair_qbs_Mx2 X Y by(simp add: copair_qbs_Mx2_def)
      then show ?thesis
      proof safe
        fix S α1 α2
        assume [measurable]:"S  sets borel" and "α1 qbs_Mx X" "α2  qbs_Mx Y"
             "g = (λr. if r  S then Inl (α1 r) else Inr (α2 r))"
        have "f -` S  sets borel"
          using S  sets borel f  borel_measurable borel measurable_sets_borel by blast
        moreover have "α1  f  qbs_Mx X" 
          using α1 qbs_Mx X by(auto simp add: qbs_closed1_def)
        moreover have "α2  f  qbs_Mx Y"
          using α2 qbs_Mx Y by(auto simp add: qbs_closed1_def)
        moreover have "(λr. if r  S then Inl (α1 r) else Inr (α2 r))  f = (λr. if r  f -` S then Inl ((α1  f) r) else Inr ((α2  f) r))"
          by auto
        ultimately show "(λr. if r  S then Inl (α1 r)  else Inr (α2 r))  f  copair_qbs_Mx2 X Y"
          using qbs_space X  {}  qbs_space Y  {} by(force simp add: copair_qbs_Mx2_def)
      qed
    qed
    thus "g  f  copair_qbs_Mx X Y"
      using copair_qbs_Mx_equiv by auto
  qed
  moreover have "qbs_closed2 (qbs_space X <+> qbs_space Y) (copair_qbs_Mx X Y)"
  proof(rule qbs_closed2I)
    fix y
    assume "y  qbs_space X <+> qbs_space Y"
    then consider "y  Inl ` (qbs_space X)" | "y  Inr ` (qbs_space Y)"
      by auto
    thus "(λr. y)  copair_qbs_Mx X Y"
    proof cases
      case 1
      then obtain x where x: "y = Inl x" "x  qbs_space X"
        by auto
      define α1 :: "real  _" where "α1  (λr. x)"
      have "α1  qbs_Mx X" using x  qbs_space X qbs_decomp 
        by(force simp add: qbs_closed2_def α1_def)
      moreover have "(λr. Inl x) = (λl. Inl (α1 l))" by (simp add: α1_def)
      moreover have "{}  sets borel" by auto
      ultimately show "(λr. y)  copair_qbs_Mx X Y"
        by(auto simp add: copair_qbs_Mx_def x)
    next
      case 2
      then obtain x where x: "y = Inr x" "x  qbs_space Y"
        by auto
      define α2 :: "real  _" where "α2  (λr. x)"
      have "α2  qbs_Mx Y" using x  qbs_space Y qbs_decomp 
        by(force simp add: qbs_closed2_def α2_def)
      moreover have "(λr. Inr x) = (λl. Inr (α2 l))" by (simp add: α2_def)
      moreover have "UNIV  sets borel" by auto
      ultimately show "(λr. y)  copair_qbs_Mx X Y"
        unfolding copair_qbs_Mx_def
        by(auto intro!: bexI[where x=UNIV] simp: x)
    qed
  qed
  moreover have "qbs_closed3 (copair_qbs_Mx X Y)"
  proof(safe intro!: qbs_closed3I)
    fix P :: "real  nat"
    fix Fi :: "nat  real _ + _"
    assume "P  borel M count_space UNIV"
         "i. Fi i  copair_qbs_Mx X Y"
    then have "i. Fi i  copair_qbs_Mx2 X Y" using copair_qbs_Mx_equiv by blast
    consider "(qbs_space X = {}  qbs_space Y = {})" |
             "(qbs_space X  {}  qbs_space Y = {})" |
             "(qbs_space X = {}  qbs_space Y  {})" |
             "(qbs_space X  {}  qbs_space Y  {})" by auto
    then have "(λr. Fi (P r) r)  copair_qbs_Mx2 X Y"
    proof cases
      assume "qbs_space X = {}  qbs_space Y = {}"
      then show ?thesis
        using i. Fi i  copair_qbs_Mx2 X Y qbs_empty_equiv
        by(simp add: copair_qbs_Mx2_def)
    next
      assume "qbs_space X  {}  qbs_space Y = {}"
      then have "i. αi. αi  qbs_Mx X  Fi i = (λr. Inl (αi r))"
        using i. Fi i  copair_qbs_Mx2 X Y by(auto simp add: copair_qbs_Mx2_def)
      then have "α1. i. α1 i  qbs_Mx X  Fi i = (λr. Inl (α1 i r))"
        by(rule choice)
      then obtain α1 :: "nat  real  _" 
        where h1: "i. α1 i  qbs_Mx X  Fi i = (λr. Inl (α1 i r))" by auto
      define β :: "real  _"  where "β  (λr. α1 (P r) r)"
      from P  borel M count_space UNIV h1
      have "β  qbs_Mx X" by (simp add: β_def)
      moreover have "(λr. Fi (P r) r) = (λr. Inl (β r))"
        using h1 by(simp add: β_def)
      ultimately show ?thesis
        using qbs_space X  {}  qbs_space Y = {} by (auto simp add: copair_qbs_Mx2_def)
    next
      assume "qbs_space X = {}  qbs_space Y  {}"
      then have "i. αi. αi  qbs_Mx Y  Fi i = (λr. Inr (αi r))"
        using i. Fi i  copair_qbs_Mx2 X Y by(auto simp add: copair_qbs_Mx2_def)
      then have "α2. i. α2 i  qbs_Mx Y  Fi i = (λr. Inr (α2 i r))"
        by(rule choice)
      then obtain α2 :: "nat  real  _" 
        where h2: "i. α2 i  qbs_Mx Y  Fi i = (λr. Inr (α2 i r))" by auto
      define β :: "real  _" where "β  (λr. α2 (P r) r)"
      from P  borel M count_space UNIV h2
      have "β  qbs_Mx Y" by(simp add: β_def)
      moreover have "(λr. Fi (P r) r) = (λr. Inr (β r))"
        using h2 by(simp add: β_def)
      ultimately show ?thesis
        using qbs_space X = {}  qbs_space Y  {} by (auto simp add: copair_qbs_Mx2_def)
    next
      assume "qbs_space X  {}  qbs_space Y  {}"
      then have "i. Si. Si  sets borel  (α1i qbs_Mx X. α2i qbs_Mx Y.
                   Fi i = (λr::real. (if (r  Si) then Inl (α1i r) else Inr (α2i r))))"
        using i. Fi i  copair_qbs_Mx2 X Y by (auto simp add: copair_qbs_Mx2_def)
      then have "S. i. S i  sets borel  (α1i qbs_Mx X. α2i qbs_Mx Y.
                   Fi i = (λr::real. (if (r  S i) then Inl (α1i r) else Inr (α2i r))))"
        by(rule choice)
      then obtain S :: "nat  real set" 
        where hs :"i. S i  sets borel  (α1i qbs_Mx X. α2i qbs_Mx Y.
                   Fi i = (λr::real. (if (r  S i) then Inl (α1i r) else Inr (α2i r))))"
        by auto
      then have "i. α1i. α1i  qbs_Mx X  (α2i qbs_Mx Y.
               Fi i = (λr::real. (if (r  S i) then Inl (α1i r) else Inr (α2i r))))"
        by blast
      then have "α1. i. α1 i  qbs_Mx X  (α2i qbs_Mx Y.
               Fi i = (λr::real. (if (r  S i) then Inl (α1 i r) else Inr (α2i r))))"
        by(rule choice)
      then obtain α1 where h1: "i. α1 i  qbs_Mx X  (α2i qbs_Mx Y.
               Fi i = (λr::real. (if (r  S i) then Inl (α1 i r) else Inr (α2i r))))"
        by auto
      define β1 :: "real  _" where "β1  (λr. α1 (P r) r)"
      from P  borel M count_space UNIV h1
      have "β1  qbs_Mx X" by(simp add: β1_def)
      from h1 have "i. α2i. α2i qbs_Mx Y 
               Fi i = (λr::real. (if (r  S i) then Inl (α1 i r) else Inr (α2i r)))"
        by auto
      then have "α2. i. α2 i qbs_Mx Y 
               Fi i = (λr::real. (if (r  S i) then Inl (α1 i r) else Inr (α2 i r)))"
        by(rule choice)
      then obtain α2
        where h2: "i. α2 i qbs_Mx Y 
               Fi i = (λr::real. (if (r  S i) then Inl (α1 i r) else Inr (α2 i r)))"
        by auto
      define β2 :: "real  _" where "β2  (λr. α2 (P r) r)"
      from P  borel M count_space UNIV h2
      have "β2  qbs_Mx Y" by(simp add: β2_def)
      define A :: "nat  real set" where "A  (λi. S i  P -` {i})"
      have [measurable]:"i. A i  sets borel"
        using A_def hs measurable_separate[OF P  borel M count_space UNIV] by blast
      define S' :: "real set" where "S'  {r. r  S (P r)}"
      have "S' = (i::nat. A i)"
        by(auto simp add: S'_def A_def)
      hence "S'  sets borel" by auto
      from h2 have "(λr. Fi (P r) r) = (λr. (if r  S' then Inl (β1  r)
                                                        else Inr (β2 r)))"
        by(auto simp add: β1_def β2_def S'_def)
      thus "(λr. Fi (P r) r)  copair_qbs_Mx2 X Y"
        using qbs_space X  {}  qbs_space Y  {} S'  sets borel β1  qbs_Mx X β2  qbs_Mx Y
        by(auto simp add: copair_qbs_Mx2_def)
    qed
    thus "(λr. Fi (P r) r)  copair_qbs_Mx X Y"
      using copair_qbs_Mx_equiv by auto
  qed
  ultimately have "Rep_quasi_borel (copair_qbs X Y) = (qbs_space X <+> qbs_space Y, copair_qbs_Mx X Y)"
    unfolding copair_qbs_def by(auto intro!: Abs_quasi_borel_inverse)
  thus ?goal1 ?goal2
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

lemma copair_qbs_MxD:
  assumes "g  qbs_Mx (X Q Y)"
      and "α. α  qbs_Mx X  g = (λr. Inl (α r))  P g"
      and "β. β  qbs_Mx Y  g = (λr. Inr (β r))  P g"
      and "S α β. (S :: real set)  sets borel  S  {}  S  UNIV  α  qbs_Mx X  β  qbs_Mx Y  g = (λr. if r  S then Inl (α r) else Inr (β r))  P g"
    shows "P g"
  using assms by(fastforce simp: copair_qbs_Mx copair_qbs_Mx_def)

subsubsection ‹ Product Spaces ›
definition PiQ :: "'a set  ('a  'b quasi_borel)  ('a  'b) quasi_borel" where
"PiQ I X  Abs_quasi_borel (ΠE iI. qbs_space (X i), {α. i. (i  I  (λr. α r i)  qbs_Mx (X i))  (i  I  (λr. α r i) = (λr. undefined))})"

syntax
  "_PiQ" :: "pttrn  'i set  'a quasi_borel  ('i => 'a) quasi_borel"  ("(3ΠQ __./ _)"  10)
translations
  "ΠQ xI. X" == "CONST PiQ I (λx. X)"

lemma
  shows PiQ_space: "qbs_space (PiQ I X) = (ΠE iI. qbs_space (X i))" (is ?goal1)
    and PiQ_Mx: "qbs_Mx (PiQ I X) = {α. i. (i  I  (λr. α r i)  qbs_Mx (X i))  (i  I  (λr. α r i) = (λr. undefined))}" (is "_ = ?Mx")
proof -
  have "?Mx  UNIV  (ΠE iI. qbs_space (X i))"
    using qbs_Mx_to_X[of _ "X _"] by auto metis
  moreover have "qbs_closed1 ?Mx"
  proof(safe intro!: qbs_closed1I)
    fix α i and f :: "real  real"
    assume h[measurable]:"i. (i  I  (λr. α r i)  qbs_Mx (X i))  (i  I  (λr. α r i) = (λr. undefined))"
                         "f  borel M borel"
    show "(λr. (α  f) r i)  qbs_Mx (X i)" if i:"i  I"
    proof -
      have "(λr. α r i)  f  qbs_Mx (X i)"
        using h i by auto
      thus "(λr. (α  f) r i)  qbs_Mx (X i)"
        by(simp add: comp_def)
    qed
    show "i  I  (λr. (α  f) r i) = (λr. undefined)"
      by (metis comp_apply h(1))
  qed
  moreover have "qbs_closed2 (ΠE iI. qbs_space (X i)) ?Mx"
    by(rule qbs_closed2I) (auto simp: PiE_def extensional_def Pi_def)
  moreover have "qbs_closed3 ?Mx"
  proof(rule qbs_closed3I)
    fix P :: "real  nat" and Fi
    assume h:"P  borel M count_space UNIV"
             "i::nat. Fi i  ?Mx"
    show "(λr. Fi (P r) r)  ?Mx"
    proof safe
      fix i
      assume hi:"i  I"
      then show "(λr. Fi (P r) r i)  qbs_Mx (X i)"
        using h qbs_closed3_dest[OF h(1),of "λj r. Fi j r i"]
        by auto
    next
      show "i. i  I  (λr. Fi (P r) r i) = (λr. undefined)"
        using h by auto meson
    qed
  qed
  ultimately have "Rep_quasi_borel (PiQ I X) = (ΠE iI. qbs_space (X i), ?Mx)"
    by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro simp: PiQ_def)
  thus ?goal1 "qbs_Mx (PiQ I X) = ?Mx"
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

lemma prod_qbs_MxI:
  assumes "i. i  I  (λr. α r i)  qbs_Mx (X i)"
      and "i. i  I  (λr. α r i) = (λr. undefined)"
    shows "α  qbs_Mx (PiQ I X)"
  using assms by(auto simp: PiQ_Mx)

lemma prod_qbs_MxD:
  assumes "α  qbs_Mx (PiQ I X)"
  shows "i. i  I  (λr. α r i)  qbs_Mx (X i)"
    and "i. i  I  (λr. α r i) = (λr. undefined)"
    and "i r. i  I  α r i = undefined"
  using assms by(auto simp: PiQ_Mx dest: fun_cong[where g="(λr. undefined)"])

lemma PiQ_eqI:
  assumes "i. i  I  X i = Y i"
  shows "PiQ I X = PiQ I Y"
  by(auto intro!: qbs_eqI simp: PiQ_Mx assms)

lemma PiQ_empty: "qbs_space (PiQ {} X) = {λi. undefined}"
  by(auto simp: PiQ_space)

lemma PiQ_empty_Mx: "qbs_Mx (PiQ {} X) = {λr i. undefined}"
  by(auto simp: PiQ_Mx) meson

subsubsection ‹ Coproduct Spaces ›
definition coPiQ_Mx :: "['a set, 'a  'b quasi_borel]  (real  'a × 'b) set" where
"coPiQ_Mx I X  { λr. (f r, α (f r) r) |f α. f  borel M count_space I  (irange f. α i  qbs_Mx (X i))}"

definition coPiQ_Mx' :: "['a set, 'a  'b quasi_borel]  (real  'a × 'b) set" where
"coPiQ_Mx' I X  { λr. (f r, α (f r) r) |f α. f  borel M count_space I  (i. (i  range f  qbs_space (X i)  {})  α i  qbs_Mx (X i))}"

lemma coPiQ_Mx_eq:
 "coPiQ_Mx I X = coPiQ_Mx' I X"
proof safe
  fix α
  assume "α   coPiQ_Mx I X"
  then obtain f β where hfb:
    "f  borel M count_space I" "i. i  range f  β i  qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
    unfolding coPiQ_Mx_def by blast
  define β' where "β'  (λi. if i  range f then β i
                              else if qbs_space (X i)  {} then (SOME γ. γ  qbs_Mx (X i))
                              else β i)"
  have 1:"α = (λr. (f r, β' (f r) r))"
    by(simp add: hfb(3) β'_def)
  have 2:"i. qbs_space (X i)  {}  β' i  qbs_Mx (X i)"
  proof -
    fix i
    assume hne:"qbs_space (X i)  {}"
    then obtain x where "x  qbs_space (X i)" by auto
    hence "(λr. x)  qbs_Mx (X i)" by auto
    thus "β' i  qbs_Mx (X i)"
      by(cases "i  range f") (auto simp: β'_def hfb(2) hne intro!: someI2[where a="λr. x"])
  qed
  show "α  coPiQ_Mx' I X"
    using hfb(1,2) 1 2 β'_def by(auto simp: coPiQ_Mx'_def intro!: exI[where x=f] exI[where x=β'])
next
  fix α
  assume "α  coPiQ_Mx' I X"
  then obtain f β where hfb:
    "f  borel M count_space I"  "i. qbs_space (X i)  {}  β i  qbs_Mx (X i)"
    "i. i  range f  β i  qbs_Mx (X i)"  "α = (λr. (f r, β (f r) r))"
    unfolding coPiQ_Mx'_def by blast
  show "α  coPiQ_Mx I X"
    by(auto simp: hfb(4) coPiQ_Mx_def intro!: hfb(1) hfb(3))
qed

definition coPiQ :: "['a set, 'a  'b quasi_borel]  ('a × 'b) quasi_borel" where
"coPiQ I X  Abs_quasi_borel (SIGMA i:I. qbs_space (X i), coPiQ_Mx I X)"

syntax
 "_coPiQ" :: "pttrn  'i set  'a quasi_borel  ('i × 'a) quasi_borel" ("(3⨿Q __./ _)"  10)
translations
 "⨿Q xI. X"  "CONST coPiQ I (λx. X)"

lemma
  shows coPiQ_space: "qbs_space (coPiQ I X) = (SIGMA i:I. qbs_space (X i))" (is ?goal1)
    and coPiQ_Mx: "qbs_Mx (coPiQ I X) = coPiQ_Mx I X" (is ?goal2)
proof -
  have "coPiQ_Mx I X  UNIV  (SIGMA i:I. qbs_space (X i))"
    by(fastforce simp: coPiQ_Mx_def dest: measurable_space qbs_Mx_to_X)
  moreover have "qbs_closed1 (coPiQ_Mx I X)"
  proof(rule qbs_closed1I)
    fix α and f :: "real  real"
    assume "α  coPiQ_Mx I X"
       and 1[measurable]: "f  borel M borel"
    then obtain β g where ha:
      "i. i  range g  β i  qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and [measurable]:"g  borel M count_space I"
      by(fastforce simp: coPiQ_Mx_def)
    then have "i. i  range g  β i  f  qbs_Mx (X i)"
      by simp
    thus "α  f  coPiQ_Mx I X"
      unfolding coPiQ_Mx_def by (auto intro!: exI[where x="g  f"] exI[where x="λi. β i  f"] simp: ha(2))
  qed
  moreover have "qbs_closed2 (SIGMA i:I. qbs_space (X i)) (coPiQ_Mx I X)"
  proof(safe intro!: qbs_closed2I)
    fix i x
    assume "i  I" "x  qbs_space (X i)"
    then show "(λr. (i,x))  coPiQ_Mx I X"
      by(auto simp: coPiQ_Mx_def intro!: exI[where x="λr. i"])
  qed
  moreover have "qbs_closed3 (coPiQ_Mx I X)"
  proof(rule qbs_closed3I)
    fix P :: "real  nat" and Fi
    assume h[measurable]:"P  borel M count_space UNIV"
             "i :: nat. Fi i  coPiQ_Mx I X"
    then have "i. fi αi. Fi i = (λr. (fi r, αi (fi r) r))  fi  borel M count_space I  (j. (j  range fi  qbs_space (X j)  {})  αi j  qbs_Mx (X j))"
      by(auto simp: coPiQ_Mx_eq coPiQ_Mx'_def)
    then obtain fi where
   "i. αi. Fi i = (λr. (fi i r, αi (fi i r) r))  fi i  borel M count_space I  (j. (j  range (fi i)  qbs_space (X j)  {})  αi j  qbs_Mx (X j))"
      by(fastforce intro!: choice)
    then obtain αi where
     "i. Fi i = (λr. (fi i r, αi i (fi i r) r))  fi i  borel M count_space I  (j. (j  range (fi i)  qbs_space (X j)  {})  αi i j  qbs_Mx (X j))"
      by(fastforce intro!: choice)
    then have hf[measurable]:
     "i. Fi i = (λr. (fi i r, αi i (fi i r) r))" "i. fi i  borel M count_space I" "i j. j  range (fi i)  αi i j  qbs_Mx (X j)" "i j. qbs_space (X j)  {}  αi i j  qbs_Mx (X j)"
      by auto

    define f' where "f'  (λr. fi (P r) r)"
    define α' where "α'  (λi r. αi (P r) i r)"
    have 1:"(λr. Fi (P r) r) = (λr. (f' r, α' (f' r) r))"
      by(simp add: α'_def f'_def hf)
    have "f'  borel M count_space I"
      by(simp add: f'_def)
    moreover have "i. i  range f'  α' i  qbs_Mx (X i)"
    proof -
      fix i
      assume hi:"i  range f'"
      then obtain r where hr: "i = fi (P r) r" by(auto simp: f'_def)
      hence "i  range (fi (P r))" by simp
      hence "αi (P r) i  qbs_Mx (X i)" by(simp add: hf)
      hence "qbs_space (X i)  {}"
        by(auto simp: qbs_empty_equiv)
      hence "j. αi j i  qbs_Mx (X i)"
        by(simp add: hf(4))
      then show "α' i  qbs_Mx (X i)"
        by(auto simp: α'_def h(1) intro!: qbs_closed3_dest[of P "λj. αi j i"])
    qed
    ultimately show "(λr. Fi (P r) r)  coPiQ_Mx I X"
      by(auto simp: 1 coPiQ_Mx_def intro!: exI[where x=f'])
  qed
  ultimately have "Rep_quasi_borel (coPiQ I X) = (SIGMA i:I. qbs_space (X i), coPiQ_Mx I X)"
    unfolding coPiQ_def by(fastforce intro!: Abs_quasi_borel_inverse)
  thus ?goal1 ?goal2
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

lemma coPiQ_MxI:
  assumes "f  borel M count_space I"
      and "i. i  range f  α i  qbs_Mx (X i)"
    shows "(λr. (f r, α (f r) r))  qbs_Mx (coPiQ I X)"
  using assms unfolding coPiQ_Mx_def coPiQ_Mx by blast

lemma coPiQ_eqI:
  assumes "i. i  I  X i = Y i"
  shows "coPiQ I X = coPiQ I Y"
  using assms by(auto intro!: qbs_eqI simp: coPiQ_Mx coPiQ_Mx_def) (metis UNIV_I measurable_space space_borel space_count_space)+

subsubsection ‹ List Spaces ›
text ‹ We define the quasi-Borel spaces on list using the following isomorphism.
       \begin{align*}
         List(X) \cong \coprod_{n\in \mathbb{N}} \prod_{0\leq i < n} X
       \end{align*}›
(*definition "list_of X ≡ " *)
definition list_nil :: "nat × (nat  'a)" where
"list_nil  (0, λn. undefined)"
definition list_cons :: "['a, nat × (nat  'a)]  nat × (nat  'a)" where
"list_cons x l  (Suc (fst l), (λn. if n = 0 then x else (snd l) (n - 1)))"

fun from_list :: "'a list  nat × (nat  'a)" where
 "from_list [] = list_nil" |
 "from_list (a#l) = list_cons a (from_list l)"

fun to_list' ::  "nat  (nat  'a)  'a list" where
 "to_list' 0 _ = []" |
 "to_list' (Suc n) f = f 0 # to_list' n (λn. f (Suc n))"

definition to_list :: "nat × (nat  'a)  'a list" where
"to_list  case_prod to_list'"

lemma inj_on_to_list: "inj_on (to_list :: nat × (nat  'a)  'a list) (SIGMA n:UNIV. PiE {..<n} A)"
proof(safe intro!: inj_onI)
  fix n m and x y :: "nat  'a"
  assume h:"to_list (n, x) = to_list (m, y)"
  have 1:"a. length (to_list (n, a)) = n" for n
    by(induction n) (auto simp: to_list_def)
  show n:"n = m"
    using 1 arg_cong[OF h,of length] by metis
  show "x  PiE {..<n} A  y  PiE {..<m} A  x = y"
    using h unfolding n
  proof(induction m arbitrary: x y A)
    case ih:(Suc m)
    then have "to_list (m, (λn. x (Suc n))) = to_list (m, (λn. y (Suc n)))"
      by(auto simp: to_list_def)
    hence 1:"(λn. x (Suc n)) = (λn. y (Suc n))"
      using ih(2-4) by(intro ih(1)[of _ "λn. A (Suc n)"]) auto
    show ?case
    proof
      fix n
      show "x n = y n"
      proof(cases n)
        assume "n = 0"
        then show "x n = y n"
          using ih(4) by(auto simp: to_list_def)
      qed(use fun_cong[OF 1] in auto)
    qed
  qed(auto simp: to_list_def)
qed

text ‹ Definition ›
definition list_qbs :: "'a quasi_borel  'a list quasi_borel" where
"list_qbs X  map_qbs to_list (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"

definition list_head :: "nat × (nat  'a)  'a" where
"list_head l = snd l 0"
definition list_tail :: "nat × (nat  'a)  nat × (nat  'a)" where
"list_tail l = (fst l - 1, λm. (snd l) (Suc m))"

lemma list_simp1: "list_nil  list_cons x l"
  by (simp add: list_nil_def list_cons_def)

lemma list_simp2:
  assumes "list_cons a al = list_cons b bl"
  shows "a = b" "al = bl"
proof -
  have "a = snd (list_cons a al) 0" "b = snd (list_cons b bl) 0"
    by (auto simp: list_cons_def)
  thus "a = b"
    by(simp add: assms)
next
  have "fst al = fst bl"
    using assms by (simp add: list_cons_def)
  moreover have "snd al = snd bl"
  proof
    fix n
    have "snd al n = snd (list_cons a al) (Suc n)"
      by (simp add: list_cons_def)
    also have "... = snd (list_cons b bl) (Suc n)"
      by (simp add: assms)
    also have "... = snd bl n"
      by (simp add: list_cons_def)
    finally show "snd al n = snd bl n" .
  qed
  ultimately show "al = bl"
    by (simp add: prod.expand)
qed

lemma
  shows list_simp3:"list_head (list_cons a l) = a"
    and list_simp4:"list_tail (list_cons a l) = l"
  by(simp_all add: list_head_def list_cons_def list_tail_def)

lemma list_decomp1:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  shows "l = list_nil 
         (a l'. a  qbs_space X  l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)  l = list_cons a l')"
proof(cases l)
  case hl:(Pair n f)
  show ?thesis
  proof(cases n)
    case 0
    then show ?thesis
      using assms hl by (simp add:  list_nil_def coPiQ_space PiQ_space)
  next
    case hn:(Suc n')
    define f' where "f'  λm. f (Suc m)"
    have "l = list_cons (f 0) (n',f')"
      unfolding hl hn list_cons_def
    proof safe
      fix m
      show "f = (λm. if m = 0 then f 0 else snd (n', f') (m - 1))"
      proof
        fix m
        show "f m = (if m = 0 then f 0 else snd (n', f') (m - 1))"
          using assms hl by(cases m; fastforce simp: f'_def) 
      qed
    qed simp
    moreover have "(n', f')  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
    proof -
      have "x. x  {..<n'}  f' x  qbs_space X"
        using assms hl hn by(fastforce simp: f'_def coPiQ_space PiQ_space)
      moreover {
        fix x
        assume 1:"x  {..<n'}"
        hence "f' x = undefined"
          using hl assms hn by(auto simp: f'_def coPiQ_space PiQ_space)
      }
      ultimately show ?thesis
        by(auto simp add: coPiQ_space PiQ_space)
    qed
    ultimately show ?thesis
      using hl assms by(auto intro!: exI[where x="f 0"] exI[where x="(n',λm. if m = 0 then undefined else f (Suc m))"] simp: list_cons_def coPiQ_space PiQ_space)
  qed
qed

lemma list_simp5:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
      and "l  list_nil"
    shows "l = list_cons (list_head l) (list_tail l)"
proof -
  obtain a l' where hl:
  "a  qbs_space X" "l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)" "l = list_cons a l'"
    using list_decomp1[OF assms(1)] assms(2) by blast
  hence "list_head l = a" "list_tail l = l'"
    by(simp_all add: list_simp3 list_simp4)
  thus ?thesis
    using hl(3) list_simp2 by auto
qed

lemma list_simp6:
 "list_nil  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  by (simp add: list_nil_def coPiQ_space PiQ_space)

lemma list_simp7:
  assumes "a  qbs_space X"
      and "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
    shows "list_cons a l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  using assms by(fastforce simp: PiE_def extensional_def list_cons_def coPiQ_space PiQ_space)

lemma list_destruct_rule:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
          "P list_nil"
      and "a l'. a  qbs_space X  l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)  P (list_cons a l')"
    shows "P l"
  by(rule disjE[OF list_decomp1[OF assms(1)]]) (use assms in auto)

lemma list_induct_rule:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
          "P list_nil"
      and "a l'. a  qbs_space X  l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)  P l'  P (list_cons a l')"
    shows "P l"
proof(cases l)
  case hl:(Pair n f)
  then show ?thesis
    using assms(1)
  proof(induction n arbitrary: f l)
    case 0
    then show ?case
      using assms(2) by (simp add: coPiQ_space PiQ_space list_nil_def)
  next
    case ih:(Suc n)
    then obtain a l' where hl:
    "a  qbs_space X" "l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)" "l = list_cons a l'"
      using list_decomp1 by(simp add: list_nil_def) blast
    have "P l'"
      using ih hl(3)
      by(auto intro!: ih(1)[OF _ hl(2),of "snd l'"] simp: coPiQ_space PiQ_space list_cons_def)
    from assms(3)[OF hl(1,2) this]
    show ?case
      by(simp add: hl(3))
  qed
qed

lemma to_list_simp1: "to_list list_nil = []"
  by(simp add: to_list_def list_nil_def)

lemma to_list_simp2:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  shows "to_list (list_cons a l) = a # to_list l"
  using assms by(auto simp:PiE_def to_list_def list_cons_def coPiQ_space PiQ_space)

lemma to_list_set:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  shows "set (to_list l)  qbs_space X"
  by(rule list_induct_rule[OF assms]) (auto simp: to_list_simp1 to_list_simp2)

lemma from_list_length: "fst (from_list l) = length l"
  by(induction l, simp_all add: list_cons_def list_nil_def)

lemma from_list_in_list_of:
  assumes "set l  qbs_space X"
  shows "from_list l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  using assms by(induction l) (auto simp: PiE_def extensional_def Pi_def coPiQ_space PiQ_space list_nil_def list_cons_def)

lemma from_list_in_list_of': "from_list l  qbs_space ((⨿Q n(UNIV :: nat set).ΠQ i{..<n}. Abs_quasi_borel (UNIV,UNIV)))"
proof -
  have "set l  qbs_space (Abs_quasi_borel (UNIV,UNIV))"
    by(simp add: qbs_space_def Abs_quasi_borel_inverse[of "(UNIV,UNIV)",simplified is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def,simplified])
  thus ?thesis
    using from_list_in_list_of by blast
qed

lemma list_cons_in_list_of:
  assumes "set (a#l)  qbs_space X"
  shows "list_cons a (from_list l)  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  using from_list_in_list_of[OF assms] by simp

lemma from_list_to_list_ident:
 "to_list (from_list l) = l"
  by(induction l) (simp add: to_list_def list_nil_def,simp add: to_list_simp2[OF from_list_in_list_of'])

lemma to_list_from_list_ident:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  shows "from_list (to_list l) = l"
proof(rule list_induct_rule[OF assms])
  fix a l'
  assume h: "l'  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
     and ih:"from_list (to_list l') = l'"
  show "from_list (to_list (list_cons a l')) = list_cons a l'"
    by(auto simp add: to_list_simp2[OF h] ih[simplified])
qed (simp add: to_list_simp1)

definition rec_list' :: "'b  ('a  (nat × (nat  'a))  'b  'b)  (nat × (nat  'a))  'b" where
"rec_list' t0 f l  (rec_list t0 (λx l'. f x (from_list l')) (to_list l))"

lemma rec_list'_simp1:
 "rec_list' t f list_nil = t"
  by(simp add: rec_list'_def to_list_simp1)

lemma rec_list'_simp2:
  assumes "l  qbs_space (⨿Q n(UNIV :: nat set).ΠQ i{..<n}. X)"
  shows "rec_list' t f (list_cons x l) = f x l (rec_list' t f l)"
  by(simp add: rec_list'_def to_list_simp2[OF assms] to_list_from_list_ident[OF assms,simplified])

lemma list_qbs_space: "qbs_space (list_qbs X) = lists (qbs_space X)"
  using to_list_set by(auto simp: list_qbs_def map_qbs_space image_def from_list_to_list_ident from_list_in_list_of subset_iff intro!: bexI[where x="from_list _"])

subsubsection ‹ Option Spaces ›
text ‹ The option spaces is defined using the following isomorphism.
       \begin{align*}
         Option(X) \cong X + 1
       \end{align*}›
definition option_qbs :: "'a quasi_borel  'a option quasi_borel" where
"option_qbs X = map_qbs (λx. case x of Inl y  Some y | Inr y  None) (X Q 1Q)"

lemma option_qbs_space: "qbs_space (option_qbs X) = {Some x|x. x  qbs_space X}  {None}"
  by(auto simp: option_qbs_def map_qbs_space copair_qbs_space) (metis InrI image_eqI insert_iff old.sum.simps(6), metis InlI image_iff sum.case(1))

subsubsection ‹ Function Spaces ›
definition exp_qbs :: "['a quasi_borel, 'b quasi_borel]  ('a  'b) quasi_borel" (infixr "Q" 61) where
"X Q Y  Abs_quasi_borel ({f. α  qbs_Mx X. f  α  qbs_Mx Y}, {g. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y})"

lemma
  shows exp_qbs_space: "qbs_space (exp_qbs X Y) = {f. α  qbs_Mx X. f  α  qbs_Mx Y}"
    and exp_qbs_Mx: "qbs_Mx (exp_qbs X Y) = {g. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y}"
proof -
  have "{g:: real  _. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y}  UNIV  {f. α  qbs_Mx X. f  α  qbs_Mx Y}"
  proof safe
    fix g :: "real  _" and r :: real and α
    assume h:"αborel_measurable borel. βqbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y" "α  qbs_Mx X"
    have [simp]: "g r  α = (λl. g r (α l))" by (auto simp: comp_def)
    thus "g r  α  qbs_Mx Y"
      using h by auto
  qed
  moreover have "qbs_closed3 {g. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y}"
    by(rule qbs_closed3I, auto) (rule qbs_closed3_dest,auto)
  ultimately have "Rep_quasi_borel (exp_qbs X Y) = ({f. α  qbs_Mx X. f  α  qbs_Mx Y}, {g. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y})"
    unfolding exp_qbs_def by(auto intro!: Abs_quasi_borel_inverse is_quasi_borel_intro qbs_closed1I qbs_closed2I simp: comp_def)
  thus "qbs_space (exp_qbs X Y) = {f. α  qbs_Mx X. f  α  qbs_Mx Y}"
       "qbs_Mx (exp_qbs X Y) = {g. α borel_measurable borel. β qbs_Mx X. (λr. g (α r) (β r))  qbs_Mx Y}"
    by(simp_all add: qbs_space_def qbs_Mx_def)
qed

subsubsection ‹ Ordering on Quasi-Borel Spaces ›

inductive_set generating_Mx :: "'a set  (real  'a) set  (real  'a) set"
  for X :: "'a set" and Mx :: "(real  'a) set"
  where
    Basic: "α  Mx  α  generating_Mx X Mx"
  | Const: "x  X  (λr. x)  generating_Mx X Mx"
  | Comp : "f  (borel :: real measure) M (borel :: real measure)  α  generating_Mx X Mx  α  f  generating_Mx X Mx"
  | Part : "(i. Fi i  generating_Mx X Mx)  P  borel M count_space (UNIV :: nat set)  (λr. Fi (P r) r)  generating_Mx X Mx"

lemma generating_Mx_to_space:
  assumes "Mx  UNIV  X"
  shows "generating_Mx X Mx  UNIV  X"
proof
  fix α
  assume "α  generating_Mx X Mx"
  then show "α  UNIV  X"
   by(induct rule: generating_Mx.induct) (use assms in auto)
qed

lemma generating_Mx_closed1:
 "qbs_closed1 (generating_Mx X Mx)"
  by (simp add: generating_Mx.Comp qbs_closed1I)

lemma generating_Mx_closed2:
 "qbs_closed2 X (generating_Mx X Mx)"
  by (simp add: generating_Mx.Const qbs_closed2I)

lemma generating_Mx_closed3:
 "qbs_closed3 (generating_Mx X Mx)"
  by(simp add: qbs_closed3I generating_Mx.Part)

lemma generating_Mx_Mx:
 "generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X"
proof safe
  fix α
  assume "α  generating_Mx (qbs_space X) (qbs_Mx X)"
  then show "α  qbs_Mx X"
    by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest')
next
  fix α
  assume "α  qbs_Mx X"
  then show "α  generating_Mx (qbs_space X) (qbs_Mx X)" ..
qed

instantiation quasi_borel :: (type) order_bot
begin

inductive less_eq_quasi_borel :: "'a quasi_borel  'a quasi_borel  bool" where
  "qbs_space X  qbs_space Y  less_eq_quasi_borel X Y"
| "qbs_space X = qbs_space Y  qbs_Mx Y  qbs_Mx X  less_eq_quasi_borel X Y"

lemma le_quasi_borel_iff:
 "X  Y  (if qbs_space X = qbs_space Y then qbs_Mx Y  qbs_Mx X else qbs_space X  qbs_space Y)"
  by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros)

definition less_quasi_borel :: "'a quasi_borel  'a quasi_borel  bool" where
 "less_quasi_borel X Y  (X  Y  ¬ Y  X)"

definition bot_quasi_borel :: "'a quasi_borel" where
 "bot_quasi_borel = empty_quasi_borel"

instance
proof
  show "bot  a" for a :: "'a quasi_borel"
    using qbs_empty_equiv
    by(auto simp add: le_quasi_borel_iff bot_quasi_borel_def)
qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI)
end

definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel]  'a quasi_borel" where
"inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X  qbs_space X', qbs_Mx X  qbs_Mx X')"

lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X  qbs_space X', qbs_Mx X  qbs_Mx X')"
  by(auto intro!: Abs_quasi_borel_inverse  simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def dest: qbs_Mx_to_X)

lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X  qbs_space X'"
  by (simp add: qbs_space_def inf_quasi_borel_correct)

lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X  qbs_Mx X'"
  by(simp add: qbs_Mx_def inf_quasi_borel_correct)

definition max_quasi_borel :: "'a set  'a quasi_borel" where
"max_quasi_borel X = Abs_quasi_borel (X, UNIV  X)"

lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV  X)"
  by(fastforce intro!: Abs_quasi_borel_inverse
   simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X"
  by(simp add: qbs_space_def max_quasi_borel_correct)

lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV  X"
  by(simp add: qbs_Mx_def max_quasi_borel_correct)

instantiation quasi_borel :: (type) semilattice_sup
begin

definition sup_quasi_borel :: "'a quasi_borel  'a quasi_borel  'a quasi_borel" where
"sup_quasi_borel X Y  (if qbs_space X = qbs_space Y      then inf_quasi_borel X Y
                        else if qbs_space X  qbs_space Y then Y
                        else if qbs_space Y  qbs_space X then X
                        else max_quasi_borel (qbs_space X  qbs_space Y))"


instance
proof
  fix X Y :: "'a quasi_borel"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  consider "?X = ?Y" | "?X  ?Y" | "?Y  ?X" | "?X  ?X  ?Y  ?Y  ?X  ?Y"
    by auto
  then show "X  X  Y"
  proof(cases)
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      by(rule less_eq_quasi_borel.intros(2),simp_all add: 1)
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      by (simp add: less_eq_quasi_borel.intros(1))
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      by auto
  next
    case 4
    then show ?thesis
      unfolding sup_quasi_borel_def
      by(auto simp: less_eq_quasi_borel.intros(1))
  qed
next
  fix X Y :: "'a quasi_borel"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  consider "?X = ?Y" | "?X  ?Y" | "?Y  ?X" | "?X  ?X  ?Y  ?Y  ?X  ?Y"
    by auto
  then show "Y  X  Y"
  proof(cases)
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      by(rule less_eq_quasi_borel.intros(2)) (simp_all add: 1)
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      by auto
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      by (auto simp add: less_eq_quasi_borel.intros(1))
  next
    case 4
    then show ?thesis
      unfolding sup_quasi_borel_def
      by(auto simp: less_eq_quasi_borel.intros(1))
  qed
next
  fix X Y Z :: "'a quasi_borel"
  assume h:"X  Z" "Y  Z"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  let ?Z = "qbs_space Z"
  consider "?X = ?Y" | "?X  ?Y" | "?Y  ?X" | "?X  ?X  ?Y  ?Y  ?X  ?Y"
    by auto
  then show "sup X Y  Z"
  proof cases
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      apply(simp add: 1,rule less_eq_quasi_borel.cases[OF h(1)])
       apply(rule less_eq_quasi_borel.intros(1))
       apply auto[1]
      apply simp
      apply(rule less_eq_quasi_borel.intros(2))
       apply(simp add: 1)
      apply(rule less_eq_quasi_borel.cases[OF h(2)])
      using 1
        apply fastforce
       apply simp
      by (metis "1" h(2) inf_qbs_Mx le_inf_iff le_quasi_borel_iff)
      
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      using h(2) by auto
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      using h(1) by auto
  next
    case 4
    then have [simp]:"?X  ?Y" "~ (?X  ?Y)" "~ (?Y  ?X)"
      by auto
    have [simp]:"?X  ?Z" "?Y  ?Z"
      by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases)
         (metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases)
    then consider "?X  ?Y = ?Z" | "?X  ?Y  ?Z"
      by blast
    then show ?thesis
      unfolding sup_quasi_borel_def
      apply cases
       apply simp
       apply(rule less_eq_quasi_borel.intros(2))
        apply simp
      using qbs_Mx_to_X apply auto[1]
      by(simp add: less_eq_quasi_borel.intros(1))
  qed
qed

end

end