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