# Theory Binary_Product_QuasiBorel

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

subsection ‹Product Spaces›

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

lemma pair_qbs_Mx[simp]: "qbs_Mx (X ⨂⇩Q Y) = pair_qbs_Mx X Y"

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 ∘ α"]
finally show "f ∘ α ∈ qbs_Mx Z" .
qed

lemma fst_qbs_morphism:
"fst ∈ X ⨂⇩Q Y →⇩Q X"

lemma snd_qbs_morphism:
"snd ∈ X ⨂⇩Q Y →⇩Q Y"

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

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

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]

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]

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

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

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"