Theory Binary_Product_QuasiBorel

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

subsection ‹Product Spaces›

theory Binary_Product_QuasiBorel
  imports "Measure_QuasiBorel_Adjunction"
begin

subsubsection ‹ Binary Product Spaces ›
definition pair_qbs_Mx :: "['a quasi_borel, 'b quasi_borel]  (real => 'a × 'b) set" where
"pair_qbs_Mx X Y  {f. fst  f  qbs_Mx X  snd  f  qbs_Mx Y}"

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, pair_qbs_Mx X Y)"


lemma pair_qbs_f[simp]: "pair_qbs_Mx X Y  UNIV  qbs_space X × qbs_space Y"
  unfolding pair_qbs_Mx_def
  by (auto simp: mem_Times_iff[of _ "qbs_space X" "qbs_space Y"]; fastforce)

lemma pair_qbs_closed1: "qbs_closed1 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))"
  unfolding pair_qbs_Mx_def qbs_closed1_def
  by (metis (no_types, lifting) comp_assoc mem_Collect_eq qbs_closed1_dest)

lemma pair_qbs_closed2: "qbs_closed2 (qbs_space X × qbs_space Y) (pair_qbs_Mx X Y)"
  unfolding qbs_closed2_def pair_qbs_Mx_def
  by auto

lemma pair_qbs_closed3: "qbs_closed3 (pair_qbs_Mx (X::'a quasi_borel) (Y::'b quasi_borel))"
proof(auto simp add: qbs_closed3_def pair_qbs_Mx_def)
  fix P :: "real  nat"
  fix Fi :: "nat  real  'a × 'b"
  define Fj :: "nat  real  'a" where "Fj  λj.(fst  Fi j)"
  assume "i. fst  Fi i  qbs_Mx X  snd  Fi i  qbs_Mx Y"
  then have "i. Fj i  qbs_Mx X" by (simp add: Fj_def)
  moreover assume "i. P -` {i}  sets real_borel"
  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. fst  Fi i  qbs_Mx X  snd  Fi i  qbs_Mx Y"
  then have "i. Fj i  qbs_Mx Y" by (simp add: Fj_def)
  moreover assume "i. P -` {i}  sets real_borel"
  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

lemma pair_qbs_correct: "Rep_quasi_borel (X Q Y) = (qbs_space X × qbs_space Y, pair_qbs_Mx X Y)"
  unfolding pair_qbs_def
  by(auto intro!: Abs_quasi_borel_inverse pair_qbs_f simp: pair_qbs_closed3 pair_qbs_closed2 pair_qbs_closed1)

lemma pair_qbs_space[simp]: "qbs_space (X Q Y) = qbs_space X × qbs_space Y"
  by (simp add: qbs_space_def pair_qbs_correct)

lemma pair_qbs_Mx[simp]: "qbs_Mx (X Q Y) = pair_qbs_Mx X Y"
  by (simp add: qbs_Mx_def pair_qbs_correct)


lemma pair_qbs_morphismI:
  assumes "α β. α  qbs_Mx X  β  qbs_Mx Y 
            f  (λr. (α r, β r))  qbs_Mx Z"
    shows "f  (X Q Y) Q Z"
proof(rule qbs_morphismI)
  fix α
  assume 1:"α  qbs_Mx (X Q Y)"
  have "f  α = f  (λr. ((fst  α) r, (snd  α) r))"
    by auto
  also have "...  qbs_Mx Z"
    using 1 assms[of "fst  α" "snd  α"]
    by(simp add: pair_qbs_Mx_def)
  finally show "f  α  qbs_Mx Z" .
qed


lemma fst_qbs_morphism:
  "fst  X Q Y Q X"
  by(auto simp add: qbs_morphism_def pair_qbs_Mx_def)

lemma snd_qbs_morphism:
  "snd  X Q Y Q Y"
  by(auto simp add: qbs_morphism_def pair_qbs_Mx_def)

lemma qbs_morphism_pair_iff:
 "f  X Q Y Q Z  fst  f  X Q Y  snd  f  X Q Z"
  by(auto intro!: qbs_morphismI qbs_morphism_comp[OF _ fst_qbs_morphism,of f X Y Z ]qbs_morphism_comp[OF _ snd_qbs_morphism,of f X Y Z]
            simp: pair_qbs_Mx_def comp_assoc[symmetric])

lemma qbs_morphism_Pair1:
  assumes "x  qbs_space X"
  shows "Pair x  Y Q X Q Y"
  using assms
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def)

lemma qbs_morphism_Pair1':
  assumes "x  qbs_space X"
      and "f  X Q Y Q Z"
    shows "(λy. f (x,y))  Y Q Z"
  using qbs_morphism_comp[OF qbs_morphism_Pair1[OF assms(1)] assms(2)]
  by(simp add: comp_def)

lemma qbs_morphism_Pair2:
  assumes "y  qbs_space Y"
  shows "(λx. (x,y))  X Q X Q Y"
  using assms
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def comp_def)

lemma qbs_morphism_Pair2':
  assumes "y  qbs_space Y"
      and "f  X Q Y Q Z"
    shows "(λx. f (x,y))  X Q Z"
  using qbs_morphism_comp[OF qbs_morphism_Pair2[OF assms(1)] assms(2)]
  by(simp add: comp_def)

lemma qbs_morphism_fst'':
  assumes "f  X Q Y"
  shows "(λk. f (fst k))  X Q Z Q Y"
  using qbs_morphism_comp[OF fst_qbs_morphism assms,of Z]
  by(simp add: comp_def)

lemma qbs_morphism_snd'':
  assumes "f  X Q Y"
  shows "(λk. f (snd k))  Z Q X Q Y"
  using qbs_morphism_comp[OF snd_qbs_morphism assms,of Z]
  by(simp add: comp_def)

lemma qbs_morphism_tuple:
  assumes "f  Z Q X"
      and "g  Z Q Y"
    shows "(λz. (f z, g z))  Z Q X Q Y"
proof(rule qbs_morphismI,simp)
  fix α
  assume  h:"α  qbs_Mx Z"
  then have "(λz. (f z, g z))  α  UNIV  qbs_space X × qbs_space Y"
    using assms qbs_morphismE(2)[OF assms(1)] qbs_morphismE(2)[OF assms(2)]
    by fastforce
  moreover have "fst  ((λz. (f z, g z))  α) = f  α" by auto
  moreover have "...  qbs_Mx X" 
    using assms(1) h by auto
  moreover have "snd  ((λz. (f z, g z))  α) = g  α" by auto
  moreover have "...  qbs_Mx Y"
    using assms(2) h by auto
  ultimately show "(λz. (f z, g z))  α  pair_qbs_Mx X Y"
    by (simp add: pair_qbs_Mx_def)
qed

lemma qbs_morphism_map_prod:
  assumes "f  X Q Y"
      and "g  X' Q Y'"
    shows "map_prod f g  X Q X'Q Y Q Y'"
proof(rule pair_qbs_morphismI)
  fix α β
  assume h:"α  qbs_Mx X"
           "β  qbs_Mx X'"
  have [simp]: "fst  (map_prod f g  (λr. (α r, β r))) = f  α" by auto
  have [simp]: "snd  (map_prod f g  (λr. (α r, β r))) = g  β" by auto
  show "map_prod f g  (λr. (α r, β r))  qbs_Mx (Y Q Y')"
    using h assms by(auto simp: pair_qbs_Mx_def)
qed

lemma qbs_morphism_pair_swap':
  "(λ(x,y). (y,x))  (X::'a quasi_borel) Q (Y::'b quasi_borel) Q Y Q X"
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)

lemma qbs_morphism_pair_swap:
  assumes "f  X Q Y Q Z"
  shows "(λ(x,y). f (y,x))  Y Q X Q Z"
proof -
  have "(λ(x,y). f (y,x)) = f  (λ(x,y). (y,x))" by auto
  thus ?thesis
    using qbs_morphism_comp[of "(λ(x,y). (y,x))" "Y Q X" _ f] qbs_morphism_pair_swap' assms
    by auto
qed

lemma qbs_morphism_pair_assoc1:
 "(λ((x,y),z). (x,(y,z)))  (X Q Y) Q Z Q X Q (Y Q Z)"
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)

lemma qbs_morphism_pair_assoc2:
 "(λ(x,(y,z)). ((x,y),z))  X Q (Y Q Z) Q (X Q Y) Q Z"
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx_def split_beta' comp_def)

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

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

text ‹ The following lemma corresponds to cite"Heunen_2017" Proposition 19(1). ›
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_def)

lemma l_product_sets[simp,measurable_cong]:
  "sets (qbs_to_measure X M qbs_to_measure Y)  sets (qbs_to_measure (X Q Y))"
proof(rule sets_pair_in_sets,simp)
  fix A B
  assume h:"A  sigma_Mx X"
           "B  sigma_Mx Y"
  then obtain Ua Ub where hu:
   "A = Ua  qbs_space X" "αqbs_Mx X. α -` Ua  sets real_borel"
   "B = Ub  qbs_space Y" "αqbs_Mx Y. α -` Ub  sets real_borel"
    by(auto simp add: sigma_Mx_def)
  show "A × B  sigma_Mx (X Q Y)"
  proof(simp add: sigma_Mx_def, rule exI[where x="Ua × Ub"])
    show "A × B = Ua × Ub  qbs_space X × qbs_space Y 
    (αpair_qbs_Mx X Y. α -` (Ua × Ub)  sets real_borel)"
      using hu by(auto simp add: pair_qbs_Mx_def vimage_Times)
  qed
qed

lemma(in pair_standard_borel) l_r_r_sets[simp,measurable_cong]:
 "sets (qbs_to_measure (measure_to_qbs M Q measure_to_qbs N)) = sets (M M N)"
  by(simp only: r_preserves_product[symmetric]) (rule standard_borel_lr_sets_ident)

end