# Theory Pair_QuasiBorel_Measure

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

subsection ‹Binary Product Measure›

theory Pair_QuasiBorel_Measure
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 "⨂⇩Q⇩m⇩e⇩s" 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)))"
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"
finally show ?thesis .
qed
qed
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_computation:
"(qbs_prob_space (X,α,μ)) ⨂⇩Q⇩m⇩e⇩s (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)"

lemma qbs_prob_pair_measure_qbs:
"qbs_prob_space_qbs (p ⨂⇩Q⇩m⇩e⇩s q) = qbs_prob_space_qbs p ⨂⇩Q qbs_prob_space_qbs q"

lemma(in pair_qbs_probs) qbs_prob_pair_measure_measure:
shows "qbs_prob_measure (qbs_prob_space (X,α,μ) ⨂⇩Q⇩m⇩e⇩s qbs_prob_space (Y,β,ν)) = distr (μ ⨂⇩M ν) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α β)"

lemma qbs_prob_pair_measure_morphism:
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))"
note [measurable] = ha(2,5)
have "(λ(x, y). x ⨂⇩Q⇩m⇩e⇩s 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"]
finally show "(λ(x, y). x ⨂⇩Q⇩m⇩e⇩s 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,α,μ) ⨂⇩Q⇩m⇩e⇩s 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)"
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,α,μ) ⨂⇩Q⇩m⇩e⇩s 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)"
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:
shows "p ⨂⇩Q⇩m⇩e⇩s q = p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y)))"
proof -
obtain α μ where hp:
"p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
obtain β ν where hq:
"q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
interpret pqp: pair_qbs_probs X α μ Y β ν
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:
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q x. ∫⇧+⇩Q y. f (x,y) ∂q ∂p) = (∫⇧+⇩Q z. f z ∂(p ⨂⇩Q⇩m⇩e⇩s 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"]]
have "?rhs = (∫⇧+⇩Q z. f z ∂(p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y)))))"
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:
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q y. ∫⇧+⇩Q x. f (x,y) ∂p ∂q) = (∫⇧+⇩Q x. f x ∂(p ⨂⇩Q⇩m⇩e⇩s 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"]]
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:
and "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q z. f (fst z) ∂(p ⨂⇩Q⇩m⇩e⇩s 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)]]
thus ?thesis
qed

lemma qbs_prob_ennintegral_indep2:
and "f ∈ Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q z. f (snd z) ∂(p ⨂⇩Q⇩m⇩e⇩s 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)]]
thus ?thesis
qed

lemma qbs_ennintegral_indep_mult:
"f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
and "g ∈ Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q z. f (fst z) * g (snd z) ∂(p ⨂⇩Q⇩m⇩e⇩s 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)
also have "... = ?rhs"
using qbs_prob_ennintegral_cmult[of p,OF _ assms(3)] assms(1)
finally show ?thesis .
qed

lemma(in pair_qbs_probs) qbs_prob_pair_measure_integrable:
assumes "qbs_integrable (qbs_prob_space (X,α,μ) ⨂⇩Q⇩m⇩e⇩s 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 α β)"
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,α,μ) ⨂⇩Q⇩m⇩e⇩s 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
qed

lemma qbs_integrable_pair_swap:
assumes "qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) f"
shows "qbs_integrable (q ⨂⇩Q⇩m⇩e⇩s 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 β ν
interpret pqp2: pair_qbs_probs Y β ν X α μ

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 β α)"
from pqp2.qbs_prob_pair_measure_integrable' [OF this]
show ?thesis by(simp add: hp(1) hq(1))
qed

lemma qbs_integrable_pair1:
"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 ⨂⇩Q⇩m⇩e⇩s q) f"
proof -
obtain α μ where hp:
"p = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
obtain β ν where hq:
"q = qbs_prob_space (Y, β, ν)" "qbs_prob Y β ν"
interpret pqp: pair_qbs_probs X α μ Y β ν

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

lemma qbs_integrable_pair2:
"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 ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s 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 β ν
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]

show "qbs_integrable p (λx. ∫⇩Q y. f (x, y) ∂q)"
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 ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s 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 β ν
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)]

show ?thesis
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 ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s q) (λx. g (snd x))"
using qbs_integrable_pair_swap[OF qbs_integrable_indep1[OF assms],of p]

lemma qbs_prob_integral_Fubini_fst:
assumes "qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) f"
shows "(∫⇩Q x. ∫⇩Q y. f (x,y) ∂q ∂p) = (∫⇩Q z. f z ∂(p ⨂⇩Q⇩m⇩e⇩s 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 β ν
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]

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)]]]
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 ⨂⇩Q⇩m⇩e⇩s q) f"
shows "(∫⇩Q y. ∫⇩Q x. f (x,y) ∂p ∂q) = (∫⇩Q z. f z ∂(p ⨂⇩Q⇩m⇩e⇩s 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 β ν
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]

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)]]
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 ⨂⇩Q⇩m⇩e⇩s q)) = (∫⇩Q x. f x ∂p)"
using qbs_prob_integral_Fubini_snd[OF qbs_integrable_indep1[OF assms],of q]

lemma qbs_prob_integral_indep2:
assumes "qbs_integrable q g"
shows "(∫⇩Q z. g (snd z) ∂(p ⨂⇩Q⇩m⇩e⇩s q)) = (∫⇩Q y. g y ∂q)"
using qbs_prob_integral_Fubini_fst[OF qbs_integrable_indep2[OF assms],of p]

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 ⨂⇩Q⇩m⇩e⇩s 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)"
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 ⨂⇩Q⇩m⇩e⇩s q) f"
"qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) (λz. (f z)⇧2)"
"qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) g"
"qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) (λz. (g z)⇧2)"
"qbs_integrable (p ⨂⇩Q⇩m⇩e⇩s q) (λz. (f z) * (g z))"
and "(∫⇩Q z. f z * g z ∂(p ⨂⇩Q⇩m⇩e⇩s q)) = (∫⇩Q z. f z ∂(p ⨂⇩Q⇩m⇩e⇩s q)) * (∫⇩Q z. g z ∂(p ⨂⇩Q⇩m⇩e⇩s q))"
shows "qbs_prob_var (p ⨂⇩Q⇩m⇩e⇩s q) (λz. f z + g z) = qbs_prob_var (p ⨂⇩Q⇩m⇩e⇩s q) f + qbs_prob_var (p ⨂⇩Q⇩m⇩e⇩s q) g"
unfolding qbs_prob_var_def
proof -
show "(∫⇩Q z. (f z + g z - ∫⇩Q w. f w + g w ∂(p ⨂⇩Q⇩m⇩e⇩s q))⇧2 ∂(p ⨂⇩Q⇩m⇩e⇩s q)) = (∫⇩Q z. (f z - qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) f)⇧2 ∂(p ⨂⇩Q⇩m⇩e⇩s q)) + (∫⇩Q z. (g z - qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g)⇧2 ∂(p ⨂⇩Q⇩m⇩e⇩s q))"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇩Q z. ((f z - (∫⇩Q w. f w ∂(p ⨂⇩Q⇩m⇩e⇩s q))) + (g z - (∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q))))⇧2 ∂(p ⨂⇩Q⇩m⇩e⇩s q))"
also have "... = (∫⇩Q z. (f z - (∫⇩Q w. f w ∂(p ⨂⇩Q⇩m⇩e⇩s q)))⇧2 + (g z - (∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q)))⇧2 + (2 * f z * g z - 2 * (∫⇩Q w. f w ∂(p ⨂⇩Q⇩m⇩e⇩s q)) * g z - (2 * f z * (∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q)) - 2 * (∫⇩Q w. f w ∂(p ⨂⇩Q⇩m⇩e⇩s q)) * (∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q)))) ∂(p ⨂⇩Q⇩m⇩e⇩s q))"
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 ⨂⇩Q⇩m⇩e⇩s q) f"]] qbs_integrable_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) f * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"]]]]
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 ⨂⇩Q⇩m⇩e⇩s q) f"]] qbs_integrable_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) f * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s q) f"]]
qbs_prob_integral_diff[OF qbs_integrable_mult[OF assms(1),of "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g",simplified ab_semigroup_mult_class.mult_ac(1)[where b="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of _ _ "qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"]] qbs_integrable_const[of _ "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) f * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"]]
qbs_prob_integral_cmult[of "p ⨂⇩Q⇩m⇩e⇩s q" 2 "λz. f z * g z",simplified assms(6) comm_semiring_1_class.semiring_normalization_rules(18)]
qbs_prob_integral_cmult[of "p ⨂⇩Q⇩m⇩e⇩s q" "2 * (∫⇩Q w. f w ∂(p ⨂⇩Q⇩m⇩e⇩s q))" g]
qbs_prob_integral_cmult[of "p ⨂⇩Q⇩m⇩e⇩s q" "2 * (∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q))" f,simplified semigroup_mult_class.mult.assoc[of 2 "∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q)"] ab_semigroup_mult_class.mult.commute[where a="qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) g"] comm_semiring_1_class.semiring_normalization_rules(18)[of 2 _ "∫⇩Q w. g w ∂(p ⨂⇩Q⇩m⇩e⇩s q)"]]
qbs_prob_integral_const[of "p ⨂⇩Q⇩m⇩e⇩s q" "2 * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s q) f * qbs_prob_integral (p ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s 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 ⨂⇩Q⇩m⇩e⇩s q)"] qbs_prob_integral_indep2[OF qbs_integrable_sq[OF assms(3,4)],of p "∫⇩Q z. g (snd z) ∂(p ⨂⇩Q⇩m⇩e⇩s q)"]
by(simp add: qbs_prob_var_def qbs_prob_integral_indep1[OF assms(1)] qbs_prob_integral_indep2[OF assms(3)])

end