Theory Pair_QuasiBorel_Measure

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

subsection ‹Binary Product Measure›

theory Pair_QuasiBorel_Measure
  imports "Monad_QuasiBorel"
begin

subsubsection ‹ Binary Product Measure›
text ‹ Special case of cite‹"Heunen_2017"› Proposition 23 where $\Omega = \mathbb{R}\times \mathbb{R}$ and $X = X \times Y$.
      Let $[\alpha,\mu ] \in P(X)$ and $[\beta ,\nu] \in P(Y)$. $\alpha\times\beta$ is the $\alpha$ in Proposition 23. ›
definition qbs_prob_pair_measure_t :: "['a qbs_prob_t, 'b qbs_prob_t] ⇒ ('a × 'b) qbs_prob_t" where
"qbs_prob_pair_measure_t p q  ≡ (let (X,α,μ) = p;
                                     (Y,β,ν) = q in
                                 (X ⨂Q Y, map_prod α β ∘ real_real.g, distr (μ ⨂M ν) real_borel real_real.f))"

lift_definition qbs_prob_pair_measure :: "['a qbs_prob_space, 'b qbs_prob_space] ⇒ ('a × 'b) qbs_prob_space" (infix "⨂Qmes" 80)
is qbs_prob_pair_measure_t
  unfolding qbs_prob_pair_measure_t_def
proof auto
  fix X X' :: "'a quasi_borel"
  fix Y Y' :: "'b quasi_borel"
  fix α α' μ μ' β β' ν ν'
  assume h:"qbs_prob_eq (X,α,μ) (X',α',μ')"
           "qbs_prob_eq (Y,β,ν) (Y',β',ν')"
  then have 1: "X = X'" "Y = Y'"
    by(auto simp: qbs_prob_eq_def)
  interpret pqp1: pair_qbs_probs X α μ Y β ν
    by(simp add: pair_qbs_probs_def qbs_prob_eq_dest(1)[OF h(1)] qbs_prob_eq_dest(1)[OF h(2)])
  interpret pqp2: pair_qbs_probs X' α' μ' Y' β' ν'
    by(simp add: pair_qbs_probs_def qbs_prob_eq_dest(2)[OF h(1)] qbs_prob_eq_dest(2)[OF h(2)])
  interpret pqp: pair_qbs_prob "X ⨂Q Y" "map_prod α β ∘ real_real.g" "distr (μ ⨂M ν) real_borel real_real.f" "X' ⨂Q Y'" "map_prod α' β' ∘ real_real.g" "distr (μ' ⨂M ν') real_borel real_real.f"
    by(auto intro!: qbs_probI pqp1.P.prob_space_distr pqp2.P.prob_space_distr simp: pair_qbs_prob_def)

  show "qbs_prob_eq (X ⨂Q Y, map_prod α β ∘ real_real.g, distr (μ ⨂M ν) real_borel real_real.f) (X' ⨂Q Y', map_prod α' β' ∘ real_real.g, distr (μ' ⨂M ν') real_borel real_real.f)"
  proof(rule pqp.qbs_prob_space_eq_inverse(1))
    show "qbs_prob_space (X ⨂Q Y, map_prod α β ∘ real_real.g, distr (μ ⨂M ν) real_borel real_real.f)
           = qbs_prob_space (X' ⨂Q Y', map_prod α' β' ∘ real_real.g, distr (μ' ⨂M ν') real_borel real_real.f)"
         (is "?lhs = ?rhs")
    proof -
      have "?lhs = qbs_prob_space (X, α, μ) ⤜ (λx. qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_return (X ⨂Q Y) (x, y)))"
        by(simp add: pqp1.qbs_bind_return_pq)
      also have "... = qbs_prob_space (X', α', μ') ⤜ (λx. qbs_prob_space (Y', β', ν') ⤜ (λy. qbs_return (X' ⨂Q Y') (x, y)))"
        using h by(simp add: qbs_prob_space_eq 1)
      also have "... = ?rhs"
        by(simp add: pqp2.qbs_bind_return_pq)
      finally show ?thesis .
    qed
  qed
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_computation:
  "(qbs_prob_space (X,α,μ)) ⨂Qmes (qbs_prob_space (Y,β,ν)) = qbs_prob_space (X ⨂Q Y, map_prod α β ∘ real_real.g , distr (μ ⨂M ν) real_borel real_real.f)"
  "qbs_prob (X ⨂Q Y) (map_prod α β ∘ real_real.g) (distr (μ ⨂M ν) real_borel real_real.f)"
  by(simp_all add: qbs_prob_pair_measure.abs_eq qbs_prob_pair_measure_t_def qbs_bind_return_pq)

lemma qbs_prob_pair_measure_qbs:
  "qbs_prob_space_qbs (p ⨂Qmes q) = qbs_prob_space_qbs p ⨂Q qbs_prob_space_qbs q"
  by(transfer,simp add: qbs_prob_pair_measure_t_def Let_def prod.case_eq_if)

lemma(in pair_qbs_probs) qbs_prob_pair_measure_measure:
    shows "qbs_prob_measure (qbs_prob_space (X,α,μ) ⨂Qmes qbs_prob_space (Y,β,ν)) = distr (μ ⨂M ν) (qbs_to_measure (X ⨂Q Y)) (map_prod α β)"
  by(simp add: qbs_prob_pair_measure_computation distr_distr comp_assoc)

lemma qbs_prob_pair_measure_morphism:
 "case_prod qbs_prob_pair_measure ∈ monadP_qbs X ⨂Q monadP_qbs Y →Q monadP_qbs (X ⨂Q Y)"
proof(rule pair_qbs_morphismI)
  fix βx βy
  assume h: "βx ∈ qbs_Mx (monadP_qbs X)" " βy ∈ qbs_Mx (monadP_qbs Y)"
  then obtain αx αy gx gy where ha:
   "αx ∈ qbs_Mx X" "gx ∈ real_borel →M prob_algebra real_borel" "βx = (λr. qbs_prob_space (X, αx, gx r))"
   "αy ∈ qbs_Mx Y" "gy ∈ real_borel →M prob_algebra real_borel" "βy = (λr. qbs_prob_space (Y, αy, gy r))"
    using rep_monadP_qbs_MPx[of βx X] rep_monadP_qbs_MPx[of βy Y] by auto
  note [measurable] = ha(2,5)
  have "(λ(x, y). x ⨂Qmes y) ∘ (λr. (βx r, βy r)) = (λr. qbs_prob_space (X ⨂Q Y, map_prod αx αy ∘ real_real.g, distr (gx r ⨂M gy r) real_borel real_real.f))"
    apply standard
    using qbs_prob_MPx[OF ha(1,2)] qbs_prob_MPx[OF ha(4,5)] pair_qbs_probs.qbs_prob_pair_measure_computation[of X αx _ Y αy]
    by (auto simp: ha pair_qbs_probs_def)
  also have "... ∈ qbs_Mx (monadP_qbs (X ⨂Q Y))"
    using qbs_prob_MPx[OF ha(1,2)] qbs_prob_MPx[OF ha(4,5)] pair_qbs_probs.ab_g_in_Mx[of X αx _ Y αy]
    by(auto intro!: bexI[where x="map_prod αx αy ∘ real_real.g"] bexI[where x="λr. distr (gx r ⨂M gy r) real_borel real_real.f"]
         simp: monadP_qbs_MPx_def in_MPx_def pair_qbs_probs_def)
  finally show "(λ(x, y). x ⨂Qmes y) ∘ (λr. (βx r, βy r)) ∈ qbs_Mx (monadP_qbs (X ⨂Q Y))" .
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_nnintegral:
  assumes "f ∈ X ⨂Q Y →Q ℝQ≥0"
  shows "(∫+Q z. f z ∂(qbs_prob_space (X,α,μ) ⨂Qmes qbs_prob_space (Y,β,ν))) = (∫+ z. (f ∘ map_prod α β) z ∂(μ ⨂M ν))"
        (is "?lhs = ?rhs")
proof -
  have "?lhs = (∫+ x. ((f ∘ map_prod α β) ∘ real_real.g) x ∂distr (μ ⨂M ν) real_borel real_real.f)"
    by(simp add: qbs_prob_ennintegral_def[OF assms] qbs_prob_pair_measure_computation)
  also have "... = (∫+ x. ((f ∘ map_prod α β) ∘ real_real.g) (real_real.f x) ∂(μ ⨂M ν))"
    using assms by(intro nn_integral_distr) auto
  also have "... = ?rhs" by simp
  finally show ?thesis .
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_integral:
  assumes "f ∈ X ⨂Q Y →Q ℝQ"
    shows "(∫Q z. f z ∂(qbs_prob_space (X,α,μ) ⨂Qmes qbs_prob_space (Y,β,ν))) = (∫z. (f ∘ map_prod α β) z ∂(μ ⨂M ν))"
          (is "?lhs = ?rhs")
proof -
  have "?lhs = (∫x. ((f ∘ map_prod α β) ∘ real_real.g) x ∂distr (μ ⨂M ν) real_borel real_real.f)"
    by(simp add: qbs_prob_integral_def[OF assms] qbs_prob_pair_measure_computation)
  also have "... = (∫ x. ((f ∘ map_prod α β) ∘ real_real.g) (real_real.f x) ∂(μ ⨂M ν))"
    using assms by(intro integral_distr) auto
  also have "... = ?rhs" by simp
  finally show ?thesis .
qed

lemma qbs_prob_pair_measure_eq_bind:
  assumes "p ∈ monadP_qbs_Px X"
      and "q ∈ monadP_qbs_Px Y"
    shows "p ⨂Qmes q = p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂Q Y) (x,y)))"
proof -
  obtain α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_monadP_qbs_Px[OF assms(1)] by auto
  obtain β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_monadP_qbs_Px[OF assms(2)] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: pair_qbs_probs_def hp hq)
  show ?thesis
    by(simp add: hp(1) hq(1) pqp.qbs_prob_pair_measure_computation(1) pqp.qbs_bind_return_pq(1))
qed

subsubsection ‹Fubini Theorem›
lemma qbs_prob_ennintegral_Fubini_fst:
  assumes "p ∈ monadP_qbs_Px X"
          "q ∈ monadP_qbs_Px Y"
      and "f ∈ X ⨂Q Y →Q ℝQ≥0"
    shows "(∫+Q x. ∫+Q y. f (x,y) ∂q ∂p) = (∫+Q z. f z ∂(p ⨂Qmes q))"
          (is "?lhs = ?rhs")
proof -
  note [simp] = qbs_bind_morphism[OF qbs_morphism_const[of _ "monadP_qbs Y",simplified,OF assms(2)] curry_preserves_morphisms[OF qbs_return_morphism[of "X ⨂Q Y"]],simplified curry_def,simplified]
                qbs_morphism_Pair1'[OF _ qbs_return_morphism[of "X ⨂Q Y"]]
                assms(1)[simplified monadP_qbs_Px_def,simplified] assms(2)[simplified monadP_qbs_Px_def,simplified]
  have "?rhs = (∫+Q z. f z ∂(p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂Q Y) (x,y)))))"
    by(simp add: qbs_prob_pair_measure_eq_bind[OF assms(1,2)])
  also have "... = (∫+Q x. qbs_prob_ennintegral (q ⤜ (λy. qbs_return (X ⨂Q Y) (x, y))) f ∂p)"
    by(auto intro!: qbs_prob_ennintegral_bind[OF assms(1) _ assms(3)])
  also have "... =  (∫+Q x. ∫+Q y. qbs_prob_ennintegral (qbs_return (X ⨂Q Y) (x, y)) f ∂q ∂p)"
    by(auto intro!: qbs_prob_ennintegral_cong qbs_prob_ennintegral_bind[OF assms(2) _ assms(3)])
  also have "... = ?lhs"
    using assms(3) by(auto intro!: qbs_prob_ennintegral_cong qbs_prob_ennintegral_return)
  finally show ?thesis by simp
qed

lemma qbs_prob_ennintegral_Fubini_snd:
  assumes "p ∈ monadP_qbs_Px X"
          "q ∈ monadP_qbs_Px Y"
      and "f ∈ X ⨂Q Y →Q ℝQ≥0"
    shows "(∫+Q y. ∫+Q x. f (x,y) ∂p ∂q) = (∫+Q x. f x ∂(p ⨂Qmes q))"
          (is "?lhs = ?rhs")
proof -
  note [simp] = qbs_bind_morphism[OF qbs_morphism_const[of _ "monadP_qbs X",simplified,OF assms(1)] curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X ⨂Q Y"]],simplified curry_def,simplified]]
                qbs_morphism_Pair2'[OF _ qbs_return_morphism[of "X ⨂Q Y"]]
                assms(1)[simplified monadP_qbs_Px_def,simplified] assms(2)[simplified monadP_qbs_Px_def,simplified]
  have "?rhs = (∫+Q z. f z ∂(q ⤜ (λy. p ⤜ (λx. qbs_return (X ⨂Q Y) (x,y)))))"
    by(simp add: qbs_prob_pair_measure_eq_bind[OF assms(1,2)] qbs_bind_return_rotate[OF assms(1,2)])
  also have "... = (∫+Q y. qbs_prob_ennintegral (p ⤜ (λx. qbs_return (X ⨂Q Y) (x, y))) f ∂q)"
    by(auto intro!: qbs_prob_ennintegral_bind[OF assms(2) _ assms(3)])
  also have "... =  (∫+Q y. ∫+Q x. qbs_prob_ennintegral (qbs_return (X ⨂Q Y) (x, y)) f ∂p ∂q)"
    by(auto intro!: qbs_prob_ennintegral_cong qbs_prob_ennintegral_bind[OF assms(1) _ assms(3)])
  also have "... = ?lhs"
    using assms(3) by(auto intro!: qbs_prob_ennintegral_cong qbs_prob_ennintegral_return)
  finally show ?thesis by simp
qed

lemma qbs_prob_ennintegral_indep1:
  assumes "p ∈ monadP_qbs_Px X"
      and "f ∈ X →Q ℝQ≥0"
    shows "(∫+Q z. f (fst z) ∂(p ⨂Qmes q)) = (∫+Q x. f x ∂p)"
          (is "?lhs = _")
proof -
 obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  have "?lhs = (∫+Q y. ∫+Q x. f x ∂p ∂q)"
    using qbs_prob_ennintegral_Fubini_snd[OF assms(1) qbs_prob.qbs_prob_space_in_Px[OF hq(2)] qbs_morphism_fst''[OF assms(2)]]
    by(simp add: hq(1))
  thus ?thesis
    by(simp add: qbs_prob_ennintegral_const)
qed

lemma qbs_prob_ennintegral_indep2:
  assumes "q ∈ monadP_qbs_Px Y"
      and "f ∈ Y →Q ℝQ≥0"
    shows "(∫+Q z. f (snd z) ∂(p ⨂Qmes q)) = (∫+Q y. f y ∂q)"
          (is "?lhs = _")
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  have "?lhs = (∫+Q x. ∫+Q y. f y ∂q ∂p)"
    using qbs_prob_ennintegral_Fubini_fst[OF qbs_prob.qbs_prob_space_in_Px[OF hp(2)] assms(1) qbs_morphism_snd''[OF assms(2)]]
    by(simp add: hp(1))
  thus ?thesis
    by(simp add: qbs_prob_ennintegral_const)
qed

lemma qbs_ennintegral_indep_mult:
  assumes "p ∈ monadP_qbs_Px X"
          "q ∈ monadP_qbs_Px Y"
          "f ∈ X →Q ℝQ≥0"
      and "g ∈ Y →Q ℝQ≥0"
    shows "(∫+Q z. f (fst z) * g (snd z) ∂(p ⨂Qmes q)) = (∫+Q x. f x ∂p) * (∫+Q y. g y ∂q)"
          (is "?lhs = ?rhs")
proof -
  have h:"(λz. f (fst z) * g (snd z)) ∈ X ⨂Q Y →Q ℝQ≥0"
    using assms(4,3)
    by(auto intro!: borel_measurable_subalgebra[OF l_product_sets[of X Y]] simp: space_pair_measure lr_adjunction_correspondence)

  have "?lhs = (∫+Q x. ∫+Q y .f x * g y ∂q ∂p)"
    using qbs_prob_ennintegral_Fubini_fst[OF assms(1,2) h] by simp
  also have "... = (∫+Q x. f x * ∫+Q y . g y ∂q ∂p)"
    using qbs_prob_ennintegral_cmult[of q,OF _ assms(4)] assms(2)
    by(simp add: monadP_qbs_Px_def)
  also have "... = ?rhs"
    using qbs_prob_ennintegral_cmult[of p,OF _ assms(3)] assms(1)
    by(simp add: ab_semigroup_mult_class.mult.commute[where b="qbs_prob_ennintegral q g"] monadP_qbs_Px_def)
  finally show ?thesis .
qed


lemma(in pair_qbs_probs) qbs_prob_pair_measure_integrable:
  assumes "qbs_integrable (qbs_prob_space (X,α,μ) ⨂Qmes qbs_prob_space (Y,β,ν)) f"
    shows "f ∈ X ⨂Q Y →Q ℝQ"
          "integrable (μ ⨂M ν) (f ∘ (map_prod α β))"
proof -
  show "f ∈ X ⨂Q Y →Q ℝQ"
    using qbs_integrable_morphism[OF qbs_prob_pair_measure_qbs assms]
    by simp
next
  have 1:"integrable (distr (μ ⨂M ν) real_borel real_real.f) (f ∘ (map_prod α β ∘ real_real.g))"
    using assms[simplified qbs_prob_pair_measure_computation] qbs_integrable_def[of f]
    by simp
  have "integrable (μ ⨂M ν) (λx. (f ∘ (map_prod α β ∘ real_real.g)) (real_real.f x))"
    by(intro integrable_distr[OF _ 1]) simp
  thus "integrable (μ ⨂M ν) (f ∘ map_prod α β)"
    by(simp add: comp_def)
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_integrable':
  assumes "f ∈ X ⨂Q Y →Q ℝQ"
      and "integrable (μ ⨂M ν) (f ∘ (map_prod α β))"
    shows "qbs_integrable (qbs_prob_space (X,α,μ) ⨂Qmes qbs_prob_space (Y,β,ν)) f"
proof -
  have "integrable (distr (μ ⨂M ν) real_borel real_real.f) (f ∘ (map_prod α β ∘ real_real.g)) = integrable (μ ⨂M ν) (λx. (f ∘ (map_prod α β ∘ real_real.g)) (real_real.f x))"
    by(intro integrable_distr_eq) (use assms(1) in auto)
  thus ?thesis
    using assms qbs_integrable_def
    by(simp add: comp_def qbs_prob_pair_measure_computation)
qed

lemma qbs_integrable_pair_swap:
  assumes "qbs_integrable (p ⨂Qmes q) f"
  shows "qbs_integrable (q ⨂Qmes p) (λ(x,y). f (y,x))"
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: pair_qbs_probs_def hp hq)
  interpret pqp2: pair_qbs_probs Y β ν X α μ
    by(simp add: pair_qbs_probs_def hp hq)

  have "f ∈ X ⨂Q Y →Q ℝQ"
       "integrable (μ ⨂M ν) (f ∘ map_prod α β)"
    by(auto simp: pqp.qbs_prob_pair_measure_integrable[OF assms[simplified hp(1) hq(1)]])
  from qbs_morphism_pair_swap[OF this(1)] pqp.integrable_product_swap[OF this(2)]
  have "(λ(x,y). f (y,x)) ∈ Y ⨂Q X →Q ℝQ"
        "integrable (ν ⨂M μ) ((λ(x,y). f (y,x)) ∘ map_prod β α)"
    by(simp_all add: map_prod_def comp_def split_beta')
  from pqp2.qbs_prob_pair_measure_integrable' [OF this]
  show ?thesis by(simp add: hp(1) hq(1))
qed

lemma qbs_integrable_pair1:
  assumes "p ∈ monadP_qbs_Px X"
          "q ∈ monadP_qbs_Px Y"
          "f ∈ X ⨂Q Y →Q ℝQ"
          "qbs_integrable p (λx. ∫Q y. ¦f (x,y)¦ ∂q)"
      and "⋀x. x ∈ qbs_space X ⟹ qbs_integrable q (λy. f (x,y))"
    shows "qbs_integrable (p ⨂Qmes q) f"
proof -
  obtain α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_monadP_qbs_Px[OF assms(1)] by auto
  obtain β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_monadP_qbs_Px[OF assms(2)] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: pair_qbs_probs_def hp hq)

  have "integrable (μ ⨂M ν) (f ∘ map_prod α β)"
  proof(rule pqp.Fubini_integrable)
    show "f ∘ map_prod α β ∈ borel_measurable (μ ⨂M ν)"
      using assms(3) by auto
  next
    have "(λx. LINT y|ν. norm ((f ∘ map_prod α β) (x, y))) = (λx. ∫Q y. ¦f (x,y)¦ ∂q) ∘ α"
      apply standard subgoal for x
        using qbs_morphism_Pair1'[OF qbs_Mx_to_X(2)[OF pqp.qp1.in_Mx,of x] assms(3)]
        by(auto intro!: pqp.qp2.qbs_prob_integral_def[symmetric] simp: hq(1))
      done
    moreover have "integrable μ ..."
      using assms(4) pqp.qp1.qbs_integrable_def
      by (simp add: hp(1))
    ultimately show "integrable μ (λx. LINT y|ν. norm ((f ∘ map_prod α β) (x, y)))"
      by simp
  next
    have "⋀x. integrable ν (λy. (f ∘ map_prod α β) (x, y))"
    proof-
      fix x
      have "(λy. (f ∘ map_prod α β) (x, y)) = (λy. f (α x,y)) ∘ β"
        by auto
      moreover have "qbs_integrable (qbs_prob_space (Y, β, ν)) (λy. f (α x, y))"
        by(auto intro!: assms(5)[simplified hq(1)] simp: qbs_Mx_to_X)
      ultimately show "integrable ν (λy. (f ∘ map_prod α β) (x, y))"
        by(simp add: pqp.qp2.qbs_integrable_def)
    qed
    thus "AE x in μ. integrable ν (λy. (f ∘ map_prod α β) (x, y))"
      by simp
  qed
  thus ?thesis
    using pqp.qbs_prob_pair_measure_integrable'[OF assms(3)]
    by(simp add: hp(1) hq(1))
qed

lemma qbs_integrable_pair2:
  assumes "p ∈ monadP_qbs_Px X"
          "q ∈ monadP_qbs_Px Y"
          "f ∈ X ⨂Q Y →Q ℝQ"
          "qbs_integrable q (λy. ∫Q x. ¦f (x,y)¦ ∂p)"
      and "⋀y. y ∈ qbs_space Y ⟹ qbs_integrable p (λx. f (x,y))"
    shows "qbs_integrable (p ⨂Qmes q) f"
  using qbs_integrable_pair_swap[OF qbs_integrable_pair1[OF assms(2,1) qbs_morphism_pair_swap[OF assms(3)],simplified,OF assms(4,5)]]
  by simp

lemma qbs_integrable_fst:
  assumes "qbs_integrable (p ⨂Qmes q) f"
  shows "qbs_integrable p (λx. ∫Q y. f (x,y) ∂q)"
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: hp hq  pair_qbs_probs_def)
  have h0: "p ∈ monadP_qbs_Px X" "q ∈ monadP_qbs_Px Y" "f ∈ X ⨂Q Y →Q ℝQ"
    using qbs_integrable_morphism[OF _ assms,simplified qbs_prob_pair_measure_qbs]
    by(simp_all add: monadP_qbs_Px_def hp(1) hq(1))

  show "qbs_integrable p (λx. ∫Q y. f (x, y) ∂q)"
  proof(auto simp add: pqp.qp1.qbs_integrable_def hp(1))
    show "(λx. ∫Q y. f (x, y) ∂q) ∈ borel_measurable (qbs_to_measure X)"
      using qbs_morphism_integral_fst[OF h0(2,3)] by auto
  next
    have "integrable μ (λx. LINT y|ν. (f ∘ map_prod α β) (x, y))"
      by(intro pqp.integrable_fst') (rule pqp.qbs_prob_pair_measure_integrable(2)[OF assms[simplified hp(1) hq(1)]])
    moreover have "⋀x. ((λx. ∫Q y. f (x, y) ∂q) ∘ α) x = LINT y|ν. (f ∘ map_prod α β) (x, y)"
     by(auto intro!: pqp.qp2.qbs_prob_integral_def qbs_morphism_Pair1'[OF qbs_Mx_to_X(2)[OF pqp.qp1.in_Mx] h0(3)] simp: hq)
    ultimately show "integrable μ ((λx. ∫Q y. f (x, y) ∂q) ∘ α)"
      using Bochner_Integration.integrable_cong[of μ μ "(λx. ∫Q y. f (x, y) ∂q) ∘ α" " (λx. LINT y|ν. (f ∘ map_prod α β) (x, y))"]
      by simp
  qed
qed

lemma qbs_integrable_snd:
  assumes "qbs_integrable (p ⨂Qmes q) f"
  shows "qbs_integrable q (λy. ∫Q x. f (x,y) ∂p)"
  using qbs_integrable_fst[OF qbs_integrable_pair_swap[OF assms]]
  by simp

lemma qbs_integrable_indep_mult:
  assumes "qbs_integrable p f"
      and "qbs_integrable q g"
    shows "qbs_integrable (p ⨂Qmes q) (λx. f (fst x) * g (snd x))"
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: hp hq  pair_qbs_probs_def)
  have h0: "p ∈ monadP_qbs_Px X" "q ∈ monadP_qbs_Px Y" "f ∈ X →Q ℝQ" "g ∈ Y →Q ℝQ"
    using qbs_integrable_morphism[OF _ assms(1)] qbs_integrable_morphism[OF _ assms(2)]
    by(simp_all add: monadP_qbs_Px_def hp(1) hq(1))

  show ?thesis
  proof(rule qbs_integrable_pair1[OF h0(1,2)],simp_all add: assms(2))
    show "(λz. f (fst z) * g (snd z)) ∈  X ⨂Q Y →Q ℝQ"
      using h0(3,4) by(auto intro!: borel_measurable_subalgebra[OF l_product_sets[of X Y]] simp: space_pair_measure lr_adjunction_correspondence)
  next
    show "qbs_integrable p (λx. ∫Q y. ¦f x * g y¦ ∂q)"
      by(auto intro!: qbs_integrable_mult[OF qbs_integrable_abs[OF assms(1)]]
           simp only: idom_abs_sgn_class.abs_mult qbs_prob_integral_cmult ab_semigroup_mult_class.mult.commute[where b="∫Q y. ¦g y¦ ∂q"])
  qed
qed

lemma qbs_integrable_indep1:
  assumes "qbs_integrable p f"
  shows "qbs_integrable (p ⨂Qmes q) (λx. f (fst x))"
  using qbs_integrable_indep_mult[OF assms qbs_integrable_const[of q 1]]
  by simp

lemma qbs_integrable_indep2:
  assumes "qbs_integrable q g"
  shows "qbs_integrable (p ⨂Qmes q) (λx. g (snd x))"
  using qbs_integrable_pair_swap[OF qbs_integrable_indep1[OF assms],of p]
  by(simp add: split_beta')


lemma qbs_prob_integral_Fubini_fst:
  assumes "qbs_integrable (p ⨂Qmes q) f"
    shows "(∫Q x. ∫Q y. f (x,y) ∂q ∂p) = (∫Q z. f z ∂(p ⨂Qmes q))"
          (is "?lhs = ?rhs")
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: hp hq  pair_qbs_probs_def)
  have h0: "p ∈ monadP_qbs_Px X" "q ∈ monadP_qbs_Px Y" "f ∈ X ⨂Q Y →Q ℝQ"
    using qbs_integrable_morphism[OF _ assms,simplified qbs_prob_pair_measure_qbs]
    by(simp_all add: monadP_qbs_Px_def hp(1) hq(1))

  have "?lhs = (∫ x. ∫Q y. f (α x, y) ∂q ∂μ)"
    using qbs_morphism_integral_fst[OF h0(2) h0(3)]
    by(auto intro!: pqp.qp1.qbs_prob_integral_def simp: hp(1))
  also have "... = (∫x. ∫y. f (α x, β y) ∂ν ∂μ)"
    using qbs_morphism_Pair1'[OF qbs_Mx_to_X(2)[OF pqp.qp1.in_Mx] h0(3)]
    by(auto intro!: Bochner_Integration.integral_cong pqp.qp2.qbs_prob_integral_def
              simp: hq(1))
  also have "... = (∫z. (f ∘ map_prod α β) z ∂(μ ⨂M ν))"
    using pqp.integral_fst'[OF pqp.qbs_prob_pair_measure_integrable(2)[OF assms[simplified hp(1) hq(1)]]]
    by(simp add: map_prod_def comp_def)
  also have "... = ?rhs"
    by(simp add: pqp.qbs_prob_pair_measure_integral[OF h0(3)] hp(1) hq(1))
  finally show ?thesis .
qed

lemma qbs_prob_integral_Fubini_snd:
  assumes "qbs_integrable (p ⨂Qmes q) f"
    shows "(∫Q y. ∫Q x. f (x,y) ∂p ∂q) = (∫Q z. f z ∂(p ⨂Qmes q))"
          (is "?lhs = ?rhs")
proof -
  obtain X α μ where hp:
    "p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
    using rep_qbs_prob_space[of p] by auto
  obtain Y β ν where hq:
   "q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
    using rep_qbs_prob_space[of q] by auto
  interpret pqp: pair_qbs_probs X α μ Y β ν
    by(simp add: hp hq  pair_qbs_probs_def)
  have h0: "p ∈ monadP_qbs_Px X" "q ∈ monadP_qbs_Px Y" "f ∈ X ⨂Q Y →Q ℝQ"
    using qbs_integrable_morphism[OF _ assms,simplified qbs_prob_pair_measure_qbs]
    by(simp_all add: monadP_qbs_Px_def hp(1) hq(1))

  have "?lhs = (∫ y. ∫Q x. f (x,β y) ∂p ∂ν)"
    using qbs_morphism_integral_snd[OF h0(1) h0(3)]
    by(auto intro!: pqp.qp2.qbs_prob_integral_def simp: hq(1))
  also have "... = (∫y. ∫x. f (α x, β y) ∂μ ∂ν)"
    using qbs_morphism_Pair2'[OF qbs_Mx_to_X(2)[OF pqp.qp2.in_Mx] h0(3)]
    by(auto intro!: Bochner_Integration.integral_cong pqp.qp1.qbs_prob_integral_def
              simp: hp(1))
  also have "... = (∫z. (f ∘ map_prod α β) z ∂(μ ⨂M ν))"
    using pqp.integral_snd[of "curry (f ∘ map_prod α β)"] pqp.qbs_prob_pair_measure_integrable(2)[OF assms[simplified hp(1) hq(1)]]
    by(simp add: map_prod_def comp_def split_beta')
  also have "... = ?rhs"
    by(simp add: pqp.qbs_prob_pair_measure_integral[OF h0(3)] hp(1) hq(1))
  finally show ?thesis .
qed

lemma qbs_prob_integral_indep1:
  assumes "qbs_integrable p f"
  shows "(∫Q z. f (fst z) ∂(p ⨂Qmes q)) = (∫Q x. f x ∂p)"
  using qbs_prob_integral_Fubini_snd[OF qbs_integrable_indep1[OF assms],of q]
  by(simp add: qbs_prob_integral_const)

lemma qbs_prob_integral_indep2:
  assumes "qbs_integrable q g"
  shows "(∫Q z. g (snd z) ∂(p ⨂Qmes q)) = (∫Q y. g y ∂q)"
  using qbs_prob_integral_Fubini_fst[OF qbs_integrable_indep2[OF assms],of p]
  by(simp add: qbs_prob_integral_const)

lemma qbs_prob_integral_indep_mult:
  assumes "qbs_integrable p f"
      and "qbs_integrable q g"
    shows "(∫Q z. f (fst z) * g (snd z) ∂(p ⨂Qmes q)) = (∫Q x. f x ∂p) * (∫Q y. g y ∂q)"
          (is "?lhs = ?rhs")
proof -
  have "?lhs = (∫Q x. ∫Q y. f x * g y ∂q ∂p)"
    using qbs_prob_integral_Fubini_fst[OF qbs_integrable_indep_mult[OF assms]]
    by simp
  also have "... = (∫Q x. f x * (∫Q y.  g y ∂q) ∂p)"
    by(simp add: qbs_prob_integral_cmult)
  also have "... = ?rhs"
    by(simp add: qbs_prob_integral_cmult ab_semigroup_mult_class.mult.commute[where b="∫Q y.  g y ∂q"])
  finally show ?thesis .
qed

lemma qbs_prob_var_indep_plus:
  assumes "qbs_integrable (p ⨂Qmes q) f"
          "qbs_integrable (p ⨂Qmes q) (λz. (f z)2)"
          "qbs_integrable (p ⨂Qmes q) g"
          "qbs_integrable (p ⨂Qmes q) (λz. (g z)2)"
          "qbs_integrable (p ⨂Qmes q) (λz. (f z) * (g z))"
      and "(∫Q z. f z * g z ∂(p ⨂Qmes q)) = (∫Q z. f z ∂(p ⨂Qmes q)) * (∫Q z. g z ∂(p ⨂Qmes q))"
    shows "qbs_prob_var (p ⨂Qmes q) (λz. f z + g z) = qbs_prob_var (p ⨂Qmes q) f + qbs_prob_var (p ⨂Qmes q) g"
  unfolding qbs_prob_var_def
proof -
  show "(∫Q z. (f z + g z - ∫Q w. f w + g w ∂(p ⨂Qmes q))2 ∂(p ⨂Qmes q)) = (∫Q z. (f z - qbs_prob_integral (p ⨂Qmes q) f)2 ∂(p ⨂Qmes q)) + (∫Q z. (g z - qbs_prob_integral (p ⨂Qmes q) g)2 ∂(p ⨂Qmes q))"
       (is "?lhs = ?rhs")
  proof -
    have "?lhs = (∫Q z. ((f z - (∫Q w. f w ∂(p ⨂Qmes q))) + (g z - (∫Q w. g w ∂(p ⨂Qmes q))))2 ∂(p ⨂Qmes q))"
      by(simp add: qbs_prob_integral_add[OF assms(1,3)] add_diff_add)
    also have "... = (∫Q z. (f z - (∫Q w. f w ∂(p ⨂Qmes q)))2 + (g z - (∫Q w. g w ∂(p ⨂Qmes q)))2 + (2 * f z * g z - 2 * (∫Q w. f w ∂(p ⨂Qmes q)) * g z - (2 * f z * (∫Q w. g w ∂(p ⨂Qmes q)) - 2 * (∫Q w. f w ∂(p ⨂Qmes q)) * (∫Q w. g w ∂(p ⨂Qmes q)))) ∂(p ⨂Qmes q))"
      by(simp add: comm_semiring_1_class.power2_sum comm_semiring_1_cancel_class.left_diff_distrib' ring_class.right_diff_distrib)
    also have "... = ?rhs"
      using qbs_prob_integral_add[OF qbs_integrable_add[OF qbs_integrable_sq[OF assms(1,2)] qbs_integrable_sq[OF assms(3,4)]] qbs_integrable_diff[OF qbs_integrable_diff[OF qbs_integrable_mult[OF assms(5),of 2,simplified comm_semiring_1_class.semiring_normalization_rules(18)] qbs_integrable_mult[OF assms(3),of "2 * qbs_prob_integral (p ⨂Qmes q) f"]] qbs_integrable_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂Qmes q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂Qmes q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂Qmes q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂Qmes q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂Qmes q) f * qbs_prob_integral (p ⨂Qmes q) g"]]]]
            qbs_prob_integral_add[OF qbs_integrable_sq[OF assms(1,2)] qbs_integrable_sq[OF assms(3,4)]]
            qbs_prob_integral_diff[OF qbs_integrable_diff[OF qbs_integrable_mult[OF assms(5),of 2,simplified comm_semiring_1_class.semiring_normalization_rules(18)] qbs_integrable_mult[OF assms(3),of "2 * qbs_prob_integral (p ⨂Qmes q) f"]] qbs_integrable_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂Qmes q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂Qmes q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂Qmes q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂Qmes q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂Qmes q) f * qbs_prob_integral (p ⨂Qmes q) g"]]]
            qbs_prob_integral_diff[OF qbs_integrable_mult[OF assms(5),of 2,simplified comm_semiring_1_class.semiring_normalization_rules(18)] qbs_integrable_mult[OF assms(3),of "2 * qbs_prob_integral (p ⨂Qmes q) f"]]
            qbs_prob_integral_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂Qmes q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂Qmes q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂Qmes q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂Qmes q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂Qmes q) f * qbs_prob_integral (p ⨂Qmes q) g"]]
            qbs_prob_integral_cmult[of "p ⨂Qmes q" 2 "λz. f z * g z",simplified assms(6) comm_semiring_1_class.semiring_normalization_rules(18)]
            qbs_prob_integral_cmult[of "p ⨂Qmes q" "2 * (∫Q w. f w ∂(p ⨂Qmes q))" g]
            qbs_prob_integral_cmult[of "p ⨂Qmes q" "2 * (∫Q w. g w ∂(p ⨂Qmes q))" f,simplified semigroup_mult_class.mult.assoc[of 2 "∫Q w. g w ∂(p ⨂Qmes q)"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂Qmes q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of 2 _ "∫Q w. g w ∂(p ⨂Qmes q)"]]
            qbs_prob_integral_const[of "p ⨂Qmes q" "2 * qbs_prob_integral (p ⨂Qmes q) f * qbs_prob_integral (p ⨂Qmes q) g"]
      by simp
    finally show ?thesis .
  qed
qed

lemma qbs_prob_var_indep_plus':
  assumes "qbs_integrable p f"
          "qbs_integrable p (λx. (f x)2)"
          "qbs_integrable q g"
      and "qbs_integrable q (λx. (g x)2)"
    shows "qbs_prob_var (p ⨂Qmes q) (λz. f (fst z) + g (snd z)) = qbs_prob_var p f + qbs_prob_var q g"
  using qbs_prob_var_indep_plus[OF qbs_integrable_indep1[OF assms(1)] qbs_integrable_indep1[OF assms(2)] qbs_integrable_indep2[OF assms(3)] qbs_integrable_indep2[OF assms(4)] qbs_integrable_indep_mult[OF assms(1) assms(3)] qbs_prob_integral_indep_mult[OF assms(1) assms(3),simplified  qbs_prob_integral_indep1[OF assms(1),of q,symmetric] qbs_prob_integral_indep2[OF assms(3),of p,symmetric]]]
        qbs_prob_integral_indep1[OF qbs_integrable_sq[OF assms(1,2)],of q "∫Q z. f (fst z) ∂(p ⨂Qmes q)"] qbs_prob_integral_indep2[OF qbs_integrable_sq[OF assms(3,4)],of p "∫Q z. g (snd z) ∂(p ⨂Qmes q)"]
  by(simp add: qbs_prob_var_def qbs_prob_integral_indep1[OF assms(1)] qbs_prob_integral_indep2[OF assms(3)])

end