# Theory Product_QuasiBorel

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

subsubsection ‹ Product Spaces›
theory Product_QuasiBorel

imports "Binary_Product_QuasiBorel"

begin

definition prod_qbs_Mx :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ (real ⇒ 'a ⇒ 'b) set" where
"prod_qbs_Mx I M ≡ { α | α. ∀i. (i ∈ I ⟶ (λr. α r i) ∈ qbs_Mx (M i)) ∧ (i ∉ I ⟶ (λr. α r i) = (λr. undefined))}"

lemma prod_qbs_MxI:
assumes "⋀i. i ∈ I ⟹ (λr. α r i) ∈ qbs_Mx (M i)"
and "⋀i. i ∉ I ⟹ (λr. α r i) = (λr. undefined)"
shows "α ∈ prod_qbs_Mx I M"
using assms by(auto simp: prod_qbs_Mx_def)

lemma prod_qbs_MxE:
assumes "α ∈ prod_qbs_Mx I M"
shows "⋀i. i ∈ I ⟹ (λr. α r i) ∈ qbs_Mx (M i)"
and "⋀i. i ∉ I ⟹ (λr. α r i) = (λr. undefined)"
and "⋀i r. i ∉ I ⟹ α r i = undefined"
using assms by(auto simp: prod_qbs_Mx_def dest: fun_cong[where g="(λr. undefined)"])

definition PiQ :: "'a set ⇒ ('a ⇒ 'b quasi_borel) ⇒ ('a ⇒ 'b) quasi_borel" where
"PiQ I M ≡ Abs_quasi_borel (Π⇩E i∈I. qbs_space (M i), prod_qbs_Mx I M)"

syntax
"_PiQ" :: "pttrn ⇒ 'i set ⇒ 'a quasi_borel ⇒ ('i => 'a) quasi_borel"  ("(3Π⇩Q _∈_./ _)"  10)
translations
"Π⇩Q x∈I. M" == "CONST PiQ I (λx. M)"

lemma PiQ_f: "prod_qbs_Mx I M ⊆ UNIV → (Π⇩E i∈I. qbs_space (M i))"
using prod_qbs_MxE by fastforce

lemma PiQ_closed1: "qbs_closed1 (prod_qbs_Mx I M)"
proof(rule qbs_closed1I)
fix α f
assume h:"α ∈ prod_qbs_Mx I M "
"f ∈ real_borel →⇩M real_borel"
show "α ∘ f ∈ prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume "i ∈ I"
from prod_qbs_MxE(1)[OF h(1) this]
have "(λr. α r i) ∘ f ∈ qbs_Mx (M i)"
using h(2) by auto
thus "(λr. (α ∘ f) r i) ∈ qbs_Mx (M i)"
next
fix i
assume "i ∉ I"
from prod_qbs_MxE(3)[OF h(1) this]
show "(λr. (α ∘ f) r i) = (λr. undefined)"
by simp
qed
qed

lemma PiQ_closed2: "qbs_closed2 (Π⇩E i∈I. qbs_space (M i)) (prod_qbs_Mx I M)"
proof(rule qbs_closed2I)
fix x
assume h:"x ∈ (Π⇩E i∈I. qbs_space (M i))"
show "(λr. x) ∈ prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume hi:"i ∈ I"
then have "x i ∈ qbs_space (M i)"
using h by auto
thus "(λr. x i) ∈ qbs_Mx (M i)"
by auto
next
show "⋀i. i ∉ I ⟹ (λr. x i) = (λr. undefined)"
using h by auto
qed
qed

lemma PiQ_closed3: "qbs_closed3 (prod_qbs_Mx I M)"
proof(rule qbs_closed3I)
fix P Fi
assume h:"⋀i::nat. P - {i} ∈ sets real_borel"
"⋀i::nat. Fi i ∈ prod_qbs_Mx I M"
show "(λr. Fi (P r) r) ∈ prod_qbs_Mx I M"
proof(rule prod_qbs_MxI)
fix i
assume hi:"i ∈ I"
show "(λr. Fi (P r) r i) ∈ qbs_Mx (M i)"
using prod_qbs_MxE(1)[OF h(2) hi] 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 prod_qbs_MxE[OF h(2)] by auto
qed
qed

lemma PiQ_correct: "Rep_quasi_borel (PiQ I M) = (Π⇩E i∈I. qbs_space (M i), prod_qbs_Mx I M)"
by(auto intro!: Abs_quasi_borel_inverse PiQ_f is_quasi_borel_intro simp: PiQ_def PiQ_closed1 PiQ_closed2 PiQ_closed3)

lemma PiQ_space[simp]: "qbs_space (PiQ I M) = (Π⇩E i∈I. qbs_space (M i))"

lemma PiQ_Mx[simp]: "qbs_Mx (PiQ I M) = prod_qbs_Mx I M"

lemma qbs_morphism_component_singleton:
assumes "i ∈ I"
shows "(λx. x i) ∈ (Π⇩Q i∈I. (M i)) →⇩Q M i"
by(auto intro!: qbs_morphismI simp: prod_qbs_Mx_def comp_def assms)

lemma product_qbs_canonical1:
assumes "⋀i. i ∈ I ⟹ f i ∈ Y →⇩Q X i"
and "⋀i. i ∉ I ⟹ f i = (λy. undefined)"
shows "(λy i. f i y) ∈ Y →⇩Q (Π⇩Q i∈I. X i)"
using qbs_morphismE(3)[simplified comp_def,OF assms(1)] assms(2)
by(auto intro!: qbs_morphismI prod_qbs_MxI)

lemma product_qbs_canonical2:
assumes "⋀i. i ∈ I ⟹ f i ∈ Y →⇩Q X i"
"⋀i. i ∉ I ⟹ f i = (λy. undefined)"
"g ∈ Y →⇩Q (Π⇩Q i∈I. X i)"
"⋀i. i ∈ I ⟹ f i = (λx. x i) ∘ g"
and "y ∈ qbs_space Y"
shows "g y = (λi. f i y)"
proof(rule ext)+
fix i
show "g y i = f i y"
proof(cases "i ∈ I")
case True
then show ?thesis
using assms(4)[of i] by simp
next
case False
moreover have "(λr. y) ∈ qbs_Mx Y"
using assms(5) by simp
ultimately show ?thesis
using assms(2,3) qbs_morphismE(3)[OF assms(3) _]
by(fastforce simp: prod_qbs_Mx_def)
qed
qed

lemma merge_qbs_morphism:
"merge I J ∈ (Π⇩Q i∈I. (M i)) ⨂⇩Q (Π⇩Q j∈J. (M j)) →⇩Q (Π⇩Q i∈I∪J. (M i))"
proof(rule qbs_morphismI)
fix α
assume h:"α ∈ qbs_Mx ((Π⇩Q i∈I. (M i)) ⨂⇩Q (Π⇩Q j∈J. (M j)))"
show "merge I J ∘ α ∈ qbs_Mx (Π⇩Q i∈I∪J. (M i))"
proof(simp, rule prod_qbs_MxI)
fix i
assume "i ∈ I ∪ J"
then consider "i ∈ I" | "i ∈ I ∧ i ∈ J" | "i ∉ I ∧ i ∈ J"
by auto
then show "(λr. (merge I J ∘ α) r i) ∈ qbs_Mx (M i)"
apply cases
using h
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE)
next
fix i
assume "i ∉ I ∪ J"
then show "(λr. (merge I J ∘ α) r i) = (λr. undefined)"
using h
by(auto simp: merge_def pair_qbs_Mx_def split_beta' dest: prod_qbs_MxE )
qed
qed

text ‹ The following lemma corresponds to \<^cite>‹"Heunen_2017"› Proposition 19(1). ›
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 auto
fix f
assume h:"f ∈ real_borel →⇩M Pi⇩M I M"
show "f ∈ prod_qbs_Mx I (λi. measure_to_qbs (M i))"
proof(rule prod_qbs_MxI)
fix i
assume 1:"i ∈ I"
show "(λr. f r i) ∈ qbs_Mx (measure_to_qbs (M i))"
using measurable_comp[OF h measurable_component_singleton[OF 1,of M]]
next
fix i
assume 1:"i ∉ I"
then show "(λr. f r i) = (λr. undefined)"
using measurable_space[OF h] 1
by(auto simp: space_PiM PiE_def extensional_def)
qed
next
fix f
assume h:"f ∈ prod_qbs_Mx I (λi. measure_to_qbs (M i))"
show "f ∈ real_borel →⇩M Pi⇩M I M"
apply(rule measurable_PiM_single')
using prod_qbs_MxE(1)[OF h] apply auto[1]
using PiQ_f[of I M] h by auto
qed
qed

text ‹ $\prod_{i = 0,1} X_i \cong X_1 \times X_2$. ›
lemma product_binary_product:
"∃f g. f ∈ (Π⇩Q i∈UNIV. if i then X else Y) →⇩Q X ⨂⇩Q Y ∧ g ∈ X ⨂⇩Q Y →⇩Q (Π⇩Q i∈UNIV. if i then X else Y) ∧
g ∘ f = id ∧ f ∘ g = id"
by(auto intro!: exI[where x="λf. (f True, f False)"] exI[where x="λxy b. if b then fst xy else snd xy"] qbs_morphismI
simp: prod_qbs_Mx_def pair_qbs_Mx_def comp_def all_bool_eq ext)

end`