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)"
      by(simp add: comp_def)
  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))"
  by(simp add: qbs_space_def PiQ_correct)

lemma PiQ_Mx[simp]: "qbs_Mx (PiQ I M) = prod_qbs_Mx I M"
  by(simp add: qbs_Mx_def PiQ_correct)


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]]
        by (simp add: comp_def)
    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