Theory Monad_QuasiBorel
subsection ‹The Probability Monad›
theory Monad_QuasiBorel
imports "Probability_Space_QuasiBorel"
begin
subsubsection ‹ The Probability Monad $P$ ›
definition monadP_qbs_Px :: "'a quasi_borel ⇒ 'a qbs_prob_space set" where
"monadP_qbs_Px X ≡ {s. qbs_prob_space_qbs s = X}"
locale in_Px =
fixes X :: "'a quasi_borel" and s :: "'a qbs_prob_space"
assumes in_Px:"s ∈ monadP_qbs_Px X"
begin
lemma qbs_prob_space_X[simp]:
"qbs_prob_space_qbs s = X"
using in_Px by(simp add: monadP_qbs_Px_def)
end
locale in_MPx =
fixes X :: "'a quasi_borel" and β :: "real ⇒ 'a qbs_prob_space"
assumes ex:"∃α∈ qbs_Mx X. ∃g ∈ real_borel →⇩M prob_algebra real_borel.
∀r. β r = qbs_prob_space (X,α,g r)"
begin
lemma rep_inMPx:
"∃α g. α ∈ qbs_Mx X ∧ g ∈ real_borel →⇩M prob_algebra real_borel ∧
β = (λr. qbs_prob_space (X,α,g r))"
proof -
obtain α g where hb:
"α ∈ qbs_Mx X" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (X,α,g r))"
using ex by auto
thus ?thesis
by(auto intro!: exI[where x=α] exI[where x=g] simp: hb)
qed
end
definition monadP_qbs_MPx :: "'a quasi_borel ⇒ (real ⇒ 'a qbs_prob_space) set" where
"monadP_qbs_MPx X ≡ {β. in_MPx X β}"
definition monadP_qbs :: "'a quasi_borel ⇒ 'a qbs_prob_space quasi_borel" where
"monadP_qbs X ≡ Abs_quasi_borel (monadP_qbs_Px X, monadP_qbs_MPx X)"
lemma(in qbs_prob) qbs_prob_space_in_Px:
"qbs_prob_space (X,α,μ) ∈ monadP_qbs_Px X"
using qbs_prob_axioms by(simp add: monadP_qbs_Px_def)
lemma rep_monadP_qbs_Px:
assumes "s ∈ monadP_qbs_Px X"
shows "∃α μ. s = qbs_prob_space (X, α, μ) ∧ qbs_prob X α μ"
using rep_qbs_prob_space' assms in_Px.qbs_prob_space_X
by(auto simp: monadP_qbs_Px_def)
lemma rep_monadP_qbs_MPx:
assumes "β ∈ monadP_qbs_MPx X"
shows "∃α g. α ∈ qbs_Mx X ∧ g ∈ real_borel →⇩M prob_algebra real_borel ∧
β = (λr. qbs_prob_space (X,α,g r))"
using assms in_MPx.rep_inMPx
by(auto simp: monadP_qbs_MPx_def)
lemma qbs_prob_MPx:
assumes "α ∈ qbs_Mx X"
and "g ∈ real_borel →⇩M prob_algebra real_borel"
shows "qbs_prob X α (g r)"
using measurable_space[OF assms(2)]
by(auto intro!: qbs_prob.intro simp: space_prob_algebra in_Mx_def real_distribution_def real_distribution_axioms_def assms(1))
lemma monadP_qbs_f[simp]: "monadP_qbs_MPx X ⊆ UNIV → monadP_qbs_Px X"
unfolding monadP_qbs_MPx_def
proof auto
fix β r
assume "in_MPx X β"
then obtain α g where hb:
"α ∈ qbs_Mx X" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (X,α,g r))"
using in_MPx.rep_inMPx by blast
then interpret qp : qbs_prob X α "g r"
by(simp add: qbs_prob_MPx)
show "β r ∈ monadP_qbs_Px X"
by(simp add: hb(3) qp.qbs_prob_space_in_Px)
qed
lemma monadP_qbs_closed1: "qbs_closed1 (monadP_qbs_MPx X)"
unfolding monadP_qbs_MPx_def in_MPx_def
apply(rule qbs_closed1I)
subgoal for α f
apply auto
subgoal for β g
apply(auto intro!: bexI[where x=β] bexI[where x="g∘f"])
done
done
done
lemma monadP_qbs_closed2: "qbs_closed2 (monadP_qbs_Px X) (monadP_qbs_MPx X)"
unfolding qbs_closed2_def
proof
fix s
assume "s ∈ monadP_qbs_Px X"
then obtain α μ where h:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_qbs_prob_space'[of s X] monadP_qbs_Px_def by blast
then interpret qp : qbs_prob X α μ
by simp
define g :: "real ⇒ real measure"
where "g ≡ (λ_. μ)"
have "g ∈ real_borel →⇩M prob_algebra real_borel"
using h prob_algebra_real_prob_measure[of μ]
by(simp add: qbs_prob_def g_def)
thus "(λr. s) ∈ monadP_qbs_MPx X"
by(auto intro!: bexI[where x=α] bexI[where x=g] simp: monadP_qbs_MPx_def in_MPx_def g_def h)
qed
lemma monadP_qbs_closed3: "qbs_closed3 (monadP_qbs_MPx (X :: 'a quasi_borel))"
proof(rule qbs_closed3I)
fix P :: "real ⇒ nat"
fix Fi
assume "⋀i. P -` {i} ∈ sets real_borel"
then have HP_mble[measurable] : "P ∈ real_borel →⇩M nat_borel"
by (simp add: separate_measurable)
assume "⋀i :: nat. Fi i ∈ monadP_qbs_MPx X"
then have "∀i. ∃αi. ∃gi. αi ∈ qbs_Mx X ∧ gi ∈ real_borel →⇩M prob_algebra real_borel ∧
Fi i = (λr. qbs_prob_space (X, αi, gi r))"
using in_MPx.rep_inMPx[of X] by(simp add: monadP_qbs_MPx_def)
hence "∃α. ∀i. ∃gi. α i ∈ qbs_Mx X ∧ gi ∈ real_borel →⇩M prob_algebra real_borel ∧
Fi i = (λr. qbs_prob_space (X, α i, gi r))"
by(rule choice)
then obtain α :: "nat ⇒ real ⇒ _" where
"∀i. ∃gi. α i ∈ qbs_Mx X ∧ gi ∈ real_borel →⇩M prob_algebra real_borel ∧
Fi i = (λr. qbs_prob_space (X, α i, gi r))"
by auto
hence "∃g. ∀i. α i ∈ qbs_Mx X ∧ g i ∈ real_borel →⇩M prob_algebra real_borel ∧
Fi i = (λr. qbs_prob_space (X, α i, g i r))"
by(rule choice)
then obtain g :: "nat ⇒ real ⇒ real measure" where
H0: "⋀i. α i ∈ qbs_Mx X" "⋀i. g i ∈ real_borel →⇩M prob_algebra real_borel"
"⋀i. Fi i = (λr. qbs_prob_space (X, α i, g i r))"
by blast
hence LHS: "(λr. Fi (P r) r) = (λr. qbs_prob_space (X, α (P r), g (P r) r))"
by auto
define α' :: "nat × real ⇒ 'a"
where "α' ≡ case_prod α"
define α'' :: "real ⇒ 'a"
where "α'' ≡ α' ∘ nat_real.g"
have α_morp: "α ∈ ℕ⇩Q →⇩Q exp_qbs ℝ⇩Q X"
using qbs_Mx_is_morphisms[of X] H0(1)
by(auto intro!: nat_qbs_morphism)
hence α'_morp: "α' ∈ ℕ⇩Q ⨂⇩Q ℝ⇩Q →⇩Q X"
unfolding α'_def
by(intro uncurry_preserves_morphisms)
hence [measurable]:"α' ∈ nat_borel ⨂⇩M real_borel →⇩M qbs_to_measure X"
using l_preserves_morphisms[of "ℕ⇩Q ⨂⇩Q ℝ⇩Q" X]
by(auto simp add: r_preserves_product)
have H_Mx:"α'' ∈ qbs_Mx X"
unfolding α''_def
using qbs_morphism_comp[OF real.qbs_morphism_measurable_intro[OF nat_real.g_meas,simplified r_preserves_product] α'_morp] qbs_Mx_is_morphisms[of X]
by simp
define g' :: "real ⇒ (nat × real) measure"
where "g' ≡ (λr. return nat_borel (P r) ⨂⇩M g (P r) r)"
define g'' :: "real ⇒ real measure"
where "g'' ≡ (λM. distr M real_borel nat_real.f) ∘ g'"
have [measurable]:"(λnr. g (fst nr) (snd nr)) ∈ nat_borel ⨂⇩M real_borel →⇩M prob_algebra real_borel"
using measurable_pair_measure_countable1[of "UNIV :: nat set" "λnr. g (fst nr) (snd nr)",simplified,OF H0(2)] measurable_cong_sets[OF sets_pair_measure_cong[of nat_borel "count_space UNIV" real_borel real_borel,OF sets_borel_eq_count_space refl] refl,of "prob_algebra real_borel"]
by auto
hence [measurable]:"(λr. g (P r) r) ∈ real_borel →⇩M prob_algebra real_borel"
proof -
have "(λr. g (P r) r) = (λnr. g (fst nr) (snd nr)) ∘ (λr. (P r, r))" by auto
also have "... ∈ real_borel →⇩M prob_algebra real_borel"
by simp
finally show ?thesis .
qed
have g'_mble[measurable]:"g' ∈ real_borel →⇩M prob_algebra (nat_borel ⨂⇩M real_borel)"
unfolding g'_def by simp
have H_mble: "g'' ∈ real_borel →⇩M prob_algebra real_borel"
unfolding g''_def by simp
have H_equiv:
"qbs_prob_space (X, α (P r), g (P r) r) = qbs_prob_space (X, α'', g'' r)" for r
proof -
interpret pqp: pair_qbs_prob X "α (P r)" "g (P r) r" X α'' "g'' r"
using qbs_prob_MPx[OF H0(1,2)] measurable_space[OF H_mble,of r] space_prob_algebra[of real_borel] H_Mx
by (simp add: pair_qbs_prob.intro qbs_probI)
interpret pps: pair_prob_space "return nat_borel (P r)" "g (P r) r"
using prob_space_return[of "P r" nat_borel]
by(simp add: pair_prob_space_def pair_sigma_finite_def prob_space_imp_sigma_finite)
have [measurable_cong]: "sets (return nat_borel (P r)) = sets nat_borel"
"sets (g' r) = sets (nat_borel ⨂⇩M real_borel)"
using measurable_space[OF g'_mble,of r] space_prob_algebra by auto
show "qbs_prob_space (X, α (P r), g (P r) r) = qbs_prob_space (X, α'', g'' r)"
proof(rule pqp.qbs_prob_space_eq4)
fix f
assume [measurable]:"f ∈ qbs_to_measure X →⇩M ennreal_borel"
show "(∫⇧+ x. f (α (P r) x) ∂g (P r) r) = (∫⇧+ x. f (α'' x) ∂g'' r)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+s. f (α' ((P r),s)) ∂ (g (P r) r))"
by(simp add: α'_def)
also have "... = (∫⇧+s. (∫⇧+i. f (α' (i, s)) ∂ (return nat_borel (P r))) ∂ (g (P r) r))"
by(auto intro!: nn_integral_cong simp: nn_integral_return[of "P r" nat_borel])
also have "... = (∫⇧+k. (f ∘ α') k ∂ ((return nat_borel (P r)) ⨂⇩M (g (P r) r)))"
by(auto intro!: pps.nn_integral_snd)
also have "... = (∫⇧+k. f (α' k) ∂ (g' r))"
by(simp add: g'_def)
also have "... = (∫⇧+x. f x ∂ (distr (g' r) (qbs_to_measure X) α'))"
by(simp add: nn_integral_distr)
also have "... = (∫⇧+x. f x ∂ (distr (g'' r) (qbs_to_measure X) α''))"
by(simp add: distr_distr comp_def g''_def α''_def)
also have "... = ?rhs"
by(simp add: nn_integral_distr)
finally show ?thesis .
qed
qed simp
qed
have "∀r. Fi (P r) r = qbs_prob_space (X, α'', g'' r)"
by (metis H_equiv LHS)
thus "(λr. Fi (P r) r) ∈ monadP_qbs_MPx X"
using H_mble H_Mx by(auto simp add: monadP_qbs_MPx_def in_MPx_def)
qed
lemma monadP_qbs_correct: "Rep_quasi_borel (monadP_qbs X) = (monadP_qbs_Px X, monadP_qbs_MPx X)"
by(auto intro!: Abs_quasi_borel_inverse monadP_qbs_f simp: monadP_qbs_closed2 monadP_qbs_closed1 monadP_qbs_closed3 monadP_qbs_def)
lemma monadP_qbs_space[simp] : "qbs_space (monadP_qbs X) = monadP_qbs_Px X"
by(simp add: qbs_space_def monadP_qbs_correct)
lemma monadP_qbs_Mx[simp] : "qbs_Mx (monadP_qbs X) = monadP_qbs_MPx X"
by(simp add: qbs_Mx_def monadP_qbs_correct)
lemma monadP_qbs_empty_iff:
"qbs_space X = {} ⟷ qbs_space (monadP_qbs X) = {}"
proof auto
fix x
assume 1:"qbs_space X = {}"
"x ∈ monadP_qbs_Px X"
then obtain α μ where "qbs_prob X α μ"
using rep_monadP_qbs_Px by blast
thus False
using empty_quasi_borel_iff[of X] qbs_empty_not_qbs_prob[of α μ] 1(1)
by auto
next
fix x
assume 1:"monadP_qbs_Px X = {}"
"x ∈ qbs_space X"
then interpret qp: qbs_prob X "λr. x" "return real_borel 0"
by(auto intro!: qbs_probI prob_space_return)
have "qbs_prob_space (X,λr. x,return real_borel 0) ∈ monadP_qbs_Px X"
by(simp add: monadP_qbs_Px_def)
thus False
by(simp add: 1)
qed
text ‹ If ‹β ∈ MPx›, there exists ‹X› ‹α› ‹g› s.t.‹β r = [X,α,g r]›.
We define a function which picks ‹X› ‹α› ‹g› from ‹β ∈ MPx›.›
definition rep_monadP_qbs_MPx :: "(real ⇒ 'a qbs_prob_space) ⇒ 'a quasi_borel × (real ⇒ 'a) × (real ⇒ real measure)" where
"rep_monadP_qbs_MPx β ≡ let X = qbs_prob_space_qbs (β undefined);
αg = (SOME k. (fst k) ∈ qbs_Mx X ∧ (snd k) ∈ real_borel →⇩M prob_algebra real_borel
∧ β = (λr. qbs_prob_space (X,fst k,snd k r)))
in (X,αg)"
lemma qbs_prob_measure_measurable[measurable]:
"qbs_prob_measure ∈ qbs_to_measure (monadP_qbs (X :: 'a quasi_borel)) →⇩M prob_algebra (qbs_to_measure X)"
proof(rule qbs_morphism_dest,rule qbs_morphismI,simp)
fix β
assume "β ∈ monadP_qbs_MPx X"
then obtain α g where hb:
"α ∈ qbs_Mx X" "β = (λr. qbs_prob_space (X, α, g r))"
and g[measurable]: "g ∈ real_borel →⇩M prob_algebra real_borel"
using in_MPx.rep_inMPx[of X β] monadP_qbs_MPx_def by blast
have "qbs_prob_measure ∘ β = (λr. distr (g r) (qbs_to_measure X) α)"
proof
fix r
interpret qp : qbs_prob X α "g r"
using qbs_prob_MPx[OF hb(1) g] by simp
show "(qbs_prob_measure ∘ β) r = distr (g r) (qbs_to_measure X) α"
by(simp add: hb(2))
qed
also have "... ∈ real_borel →⇩M prob_algebra (qbs_to_measure X) "
using hb by simp
finally show "qbs_prob_measure ∘ β ∈ real_borel →⇩M prob_algebra (qbs_to_measure X)" .
qed
lemma qbs_l_inj:
"inj_on qbs_prob_measure (monadP_qbs_Px X)"
apply standard
apply (unfold monadP_qbs_Px_def)
apply simp
apply transfer
apply (auto simp: qbs_prob_eq_def qbs_prob_t_measure_def)
done
lemma qbs_prob_measure_measurable'[measurable]:
"qbs_prob_measure ∈ qbs_to_measure (monadP_qbs (X :: 'a quasi_borel)) →⇩M subprob_algebra (qbs_to_measure X)"
by(auto simp: measurable_prob_algebraD)
subsubsection ‹ Return ›
definition qbs_return :: "['a quasi_borel, 'a] ⇒ 'a qbs_prob_space" where
"qbs_return X x ≡ qbs_prob_space (X,λr. x,Eps real_distribution)"
lemma(in real_distribution) qbs_return_qbs_prob:
assumes "x ∈ qbs_space X"
shows "qbs_prob X (λr. x) M"
using assms
by(simp add: qbs_prob_def in_Mx_def real_distribution_axioms)
lemma(in real_distribution) qbs_return_computation :
assumes "x ∈ qbs_space X"
shows "qbs_return X x = qbs_prob_space (X,λr. x,M)"
unfolding qbs_return_def
proof(rule someI2[where a=M])
fix N
assume "real_distribution N"
then interpret pqp: pair_qbs_prob X "λr. x" N X "λr. x" M
by(simp_all add: pair_qbs_prob_def real_distribution_axioms real_distribution.qbs_return_qbs_prob[OF _ assms])
show "qbs_prob_space (X, λr. x, N) = qbs_prob_space (X, λr. x, M)"
by(auto intro!: pqp.qbs_prob_space_eq simp: distr_const[of x "qbs_to_measure X"] assms)
qed (rule real_distribution_axioms)
lemma qbs_return_morphism:
"qbs_return X ∈ X →⇩Q monadP_qbs X"
proof -
interpret rr : real_distribution "return real_borel 0"
by(simp add: real_distribution_def real_distribution_axioms_def prob_space_return)
show ?thesis
proof(rule qbs_morphismI,simp)
fix α
assume h:"α ∈ qbs_Mx X"
then have h':"⋀l:: real. α l ∈ qbs_space X"
by auto
have "⋀l. (qbs_return X ∘ α) l = qbs_prob_space (X, α, return real_borel l)"
proof -
fix l
interpret pqp: pair_qbs_prob X "λr. α l" "return real_borel 0" X α "return real_borel l"
using h' by(simp add: pair_qbs_prob_def qbs_prob_def in_Mx_def h real_distribution_def prob_space_return real_distribution_axioms_def)
have "(qbs_return X ∘ α) l = qbs_prob_space (X,λr. α l,return real_borel 0)"
using rr.qbs_return_computation[OF h'[of l]] by simp
also have "... = qbs_prob_space (X, α, return real_borel l)"
by(auto intro!: pqp.qbs_prob_space_eq simp: distr_return)
finally show "(qbs_return X ∘ α) l = qbs_prob_space (X, α, return real_borel l)" .
qed
thus "qbs_return X ∘ α ∈ monadP_qbs_MPx X"
by(auto intro!: bexI[where x="α"] bexI[where x="λl. return real_borel l"] simp: h monadP_qbs_MPx_def in_MPx_def)
qed
qed
lemma qbs_return_morphism':
assumes "f ∈ X →⇩Q Y"
shows "(λx. qbs_return Y (f x)) ∈ X →⇩Q monadP_qbs Y"
using qbs_morphism_comp[OF assms(1) qbs_return_morphism[of Y]]
by (simp add: comp_def)
subsubsection ‹Bind›
definition qbs_bind :: "'a qbs_prob_space ⇒ ('a ⇒ 'b qbs_prob_space) ⇒ 'b qbs_prob_space" where
"qbs_bind s f ≡ (let (qbsx,α,μ) = rep_qbs_prob_space s;
(qbsy,β,g) = rep_monadP_qbs_MPx (f ∘ α)
in qbs_prob_space (qbsy,β,μ ⤜ g))"
adhoc_overloading Monad_Syntax.bind qbs_bind
lemma(in qbs_prob) qbs_bind_computation:
assumes"s = qbs_prob_space (X,α,μ)"
"f ∈ X →⇩Q monadP_qbs Y"
"β ∈ qbs_Mx Y"
and [measurable]: "g ∈ real_borel →⇩M prob_algebra real_borel"
and "(f ∘ α) = (λr. qbs_prob_space (Y,β, g r))"
shows "qbs_prob Y β (μ ⤜ g)"
"s ⤜ f = qbs_prob_space (Y,β,μ ⤜ g)"
proof -
interpret qp_bind: qbs_prob Y β "μ ⤜ g"
using assms(3,4) space_prob_algebra[of real_borel] measurable_space[OF assms(4)] events_eq_borel measurable_cong_sets[OF events_eq_borel refl,of "subprob_algebra real_borel"] measurable_prob_algebraD[OF assms(4)]
by(auto intro!: prob_space_bind[of g real_borel] simp: qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def)
show "qbs_prob Y β (μ ⤜ g)"
by (rule qp_bind.qbs_prob_axioms)
show "s ⤜ f = qbs_prob_space (Y, β, μ ⤜ g)"
apply(simp add: assms(1) qbs_bind_def rep_qbs_prob_space_def qbs_prob_space.rep_def)
apply(rule someI2[where a= "(X, α, μ)"])
proof auto
fix X' α' μ'
assume h':"(X',α',μ') ∈ Rep_qbs_prob_space (qbs_prob_space (X, α, μ))"
from if_in_Rep[OF this] interpret pqp1: pair_qbs_prob X α μ X' α' μ'
by(simp add: pair_qbs_prob_def qbs_prob_axioms)
have h_eq: "qbs_prob_space (X, α, μ) = qbs_prob_space (X',α',μ')"
using if_in_Rep(3)[OF h'] by (simp add: qbs_prob_space_eq)
note [simp] = if_in_Rep(1)[OF h']
then obtain β' g' where hb':
"β' ∈ qbs_Mx Y" "g' ∈ real_borel →⇩M prob_algebra real_borel"
"f ∘ α' = (λr. qbs_prob_space (Y, β', g' r))"
using in_MPx.rep_inMPx[of Y "f ∘ α'"] qbs_morphismE(3)[OF assms(2),of α'] pqp1.qp2.qbs_prob_axioms[simplified qbs_prob_def in_Mx_def]
by(auto simp: monadP_qbs_MPx_def)
note [measurable] = hb'(2)
have [simp]:"⋀r. qbs_prob_space_qbs (f (α' r)) = Y"
subgoal for r
using fun_cong[OF hb'(3)] qbs_prob.qbs_prob_space_qbs_computation[OF qbs_prob_MPx[OF hb'(1,2),of r]]
by simp
done
show "(case rep_monadP_qbs_MPx (λa. f (α' a)) of (qbsy, β, g) ⇒ qbs_prob_space (qbsy, β, μ' ⤜ g)) =
qbs_prob_space (Y, β, μ ⤜ g)"
unfolding rep_monadP_qbs_MPx_def Let_def
proof(rule someI2[where a="(β',g')"],auto simp: hb'[simplified comp_def])
fix α'' g''
assume h'':"α'' ∈ qbs_Mx Y"
"g'' ∈ real_borel →⇩M prob_algebra real_borel"
"(λr. qbs_prob_space (Y, β', g' r)) = (λr. qbs_prob_space (Y, α'', g'' r))"
then interpret pqp2: pair_qbs_prob Y α'' "μ' ⤜ g''" Y β "μ ⤜ g"
using space_prob_algebra[of real_borel] measurable_space[OF h''(2)] events_eq_borel measurable_cong_sets[OF events_eq_borel refl,of "subprob_algebra real_borel"] measurable_prob_algebraD[OF h''(2)] h''(3)
by (meson pair_qbs_prob_def in_Mx_def pqp1.qp2.real_distribution_axioms prob_algebra_real_prob_measure prob_space_bind' qbs_probI qbs_prob_def qp_bind.qbs_prob_axioms sets_bind')
note [measurable] = h''(2)
have [measurable]:"f ∈ qbs_to_measure X →⇩M qbs_to_measure (monadP_qbs Y)"
using assms(2) l_preserves_morphisms by auto
show "qbs_prob_space (Y, α'', μ' ⤜ g'') = qbs_prob_space (Y, β, μ ⤜ g)"
proof(rule pqp2.qbs_prob_space_eq)
show "distr (μ' ⤜ g'') (qbs_to_measure Y) α'' = distr (μ ⤜ g) (qbs_to_measure Y) β"
(is "?lhs = ?rhs")
proof -
have "?lhs = μ' ⤜ (λx. distr (g'' x) (qbs_to_measure Y) α'')"
by(auto intro!: distr_bind[where K=real_borel] simp: measurable_prob_algebraD)
also have "... = μ' ⤜ (λx. qbs_prob_measure (qbs_prob_space (Y,α'',g'' x)))"
by(auto intro!: bind_cong simp: qbs_prob_MPx[OF h''(1,2)] qbs_prob.qbs_prob_measure_computation)
also have "... = μ' ⤜ (λx. (qbs_prob_measure ((f ∘ α') x)))"
by(simp add: hb'(3) h''(3))
also have "... = μ' ⤜ (λx. (qbs_prob_measure ∘ f) (α' x))"
by(simp add: comp_def)
also have "... = distr μ' (qbs_to_measure X) α' ⤜ qbs_prob_measure ∘ f"
by(rule bind_distr[where K="qbs_to_measure Y",symmetric],auto)
also have "... = distr μ (qbs_to_measure X) α ⤜ qbs_prob_measure ∘ f"
using pqp1.qbs_prob_space_eq_inverse(1)[OF h_eq]
by(simp add: qbs_prob_eq_def)
also have "... = μ ⤜ (λx. (qbs_prob_measure ∘ f) (α x))"
by(rule bind_distr[where K="qbs_to_measure Y"],auto)
also have "... = μ ⤜ (λx. (qbs_prob_measure ((f ∘ α) x)))"
by(simp add: comp_def)
also have "... = μ ⤜ (λx. qbs_prob_measure (qbs_prob_space (Y,β,g x)))"
by(auto simp: assms(5))
also have "... = μ ⤜ (λx. distr (g x) (qbs_to_measure Y) β)"
by(auto intro!: bind_cong simp: qbs_prob_MPx[OF assms(3)] qbs_prob.qbs_prob_measure_computation)
also have "... = ?rhs"
by(auto intro!: distr_bind[where K=real_borel,symmetric] simp: measurable_prob_algebraD)
finally show ?thesis .
qed
qed simp
qed
qed (rule in_Rep)
qed
lemma qbs_bind_morphism':
assumes "f ∈ X →⇩Q monadP_qbs Y"
shows "(λx. x ⤜ f) ∈ monadP_qbs X →⇩Q monadP_qbs Y"
proof(rule qbs_morphismI,simp)
fix β
assume "β ∈ monadP_qbs_MPx X"
then obtain α g where hb:
"α ∈ qbs_Mx X" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (X, α, g r))"
using rep_monadP_qbs_MPx by blast
obtain γ g' where hc:
"γ ∈ qbs_Mx Y" "g' ∈ real_borel →⇩M prob_algebra real_borel"
"f ∘ α = (λr. qbs_prob_space (Y, γ, g' r))"
using rep_monadP_qbs_MPx[of "f ∘ α" Y] qbs_morphismE(3)[OF assms hb(1),simplified]
by auto
note [measurable] = hb(2) hc(2)
show "(λx. x ⤜ f) ∘ β ∈ monadP_qbs_MPx Y"
proof -
have "(λx. x ⤜ f) ∘ β = (λr. β r ⤜ f)"
by auto
also have "... ∈ monadP_qbs_MPx Y"
unfolding monadP_qbs_MPx_def in_MPx_def
by(auto intro!: bexI[where x="γ"] bexI[where x="λr. g r ⤜ g'"] simp: hc(1) hb(3) qbs_prob.qbs_bind_computation[OF qbs_prob_MPx[OF hb(1,2)] _ assms hc])
finally show ?thesis .
qed
qed
lemma qbs_return_comp:
assumes "α ∈ qbs_Mx X"
shows "(qbs_return X ∘ α) = (λr. qbs_prob_space (X,α,return real_borel r))"
proof
fix r
interpret pqp: pair_qbs_prob X "λk. α r" "return real_borel 0" X α "return real_borel r"
by(simp add: assms qbs_Mx_to_X(2)[OF assms] pair_qbs_prob_def qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def prob_space_return)
show "(qbs_return X ∘ α) r = qbs_prob_space (X, α, return real_borel r)"
by(auto intro!: pqp.qbs_prob_space_eq simp: distr_return pqp.qp1.qbs_return_computation qbs_Mx_to_X(2)[OF assms])
qed
lemma qbs_bind_return':
assumes "x ∈ monadP_qbs_Px X"
shows "x ⤜ qbs_return X = x"
proof -
obtain α μ where h1:"qbs_prob X α μ" "x = qbs_prob_space (X, α, μ)"
using assms rep_monadP_qbs_Px by blast
then interpret qp: qbs_prob X α μ
by simp
show ?thesis
using qp.qbs_bind_computation[OF h1(2) qbs_return_morphism _ measurable_return_prob_space qbs_return_comp[OF qp.in_Mx]]
by(simp add: h1(2) bind_return'' prob_space_return qbs_probI)
qed
lemma qbs_bind_return:
assumes "f ∈ X →⇩Q monadP_qbs Y"
and "x ∈ qbs_space X"
shows "qbs_return X x ⤜ f = f x"
proof -
have "f x ∈ monadP_qbs_Px Y"
using assms by auto
then obtain β μ where hf:"qbs_prob Y β μ" "f x = qbs_prob_space (Y, β, μ)"
using rep_monadP_qbs_Px by blast
then interpret rd: real_distribution "return real_borel 0"
by(simp add: qbs_prob_def prob_space_return real_distribution_def real_distribution_axioms_def)
interpret rd': real_distribution μ
using hf(1) by(simp add: qbs_prob_def)
interpret qp: qbs_prob X "λr. x" "return real_borel 0"
using assms(2) by(auto simp: qbs_prob_def in_Mx_def rd.real_distribution_axioms)
show ?thesis
by(auto intro!: qp.qbs_bind_computation(2)[OF rd.qbs_return_computation[OF assms(2)] assms(1) _ measurable_const[of μ],of β,simplified bind_const'[OF rd.prob_space_axioms rd'.subprob_space_axioms]]
simp: hf[simplified qbs_prob_def in_Mx_def] prob_algebra_real_prob_measure)
qed
lemma qbs_bind_assoc:
assumes "s ∈ monadP_qbs_Px X"
"f ∈ X →⇩Q monadP_qbs Y"
and "g ∈ Y →⇩Q monadP_qbs Z"
shows "s ⤜ (λx. f x ⤜ g) = (s ⤜ f) ⤜ g"
proof -
obtain α μ where H0:"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using assms rep_monadP_qbs_Px by blast
then have "f ∘ α ∈ monadP_qbs_MPx Y"
using assms(2) by(auto simp: qbs_prob_def in_Mx_def)
from rep_monadP_qbs_MPx[OF this] obtain β g1 where H1:
"β ∈ qbs_Mx Y" "g1 ∈ real_borel →⇩M prob_algebra real_borel"
" (f ∘ α) = (λr. qbs_prob_space (Y, β, g1 r))"
by auto
hence "g ∘ β ∈ monadP_qbs_MPx Z"
using assms by(simp add: qbs_morphism_def)
from rep_monadP_qbs_MPx[OF this] obtain γ g2 where H2:
"γ ∈ qbs_Mx Z" "g2 ∈ real_borel →⇩M prob_algebra real_borel"
"(g ∘ β) = (λr. qbs_prob_space (Z, γ, g2 r))"
by auto
note [measurable] = H1(2) H2(2)
interpret rd: real_distribution μ
using H0(1) by(simp add: qbs_prob_def)
have LHS: "(s ⤜ f) ⤜ g = qbs_prob_space (Z, γ, μ ⤜ g1 ⤜ g2)"
by(rule qbs_prob.qbs_bind_computation(2)[OF qbs_prob.qbs_bind_computation[OF H0 assms(2) H1] assms(3) H2])
have RHS: "s ⤜ (λx. f x ⤜ g) = qbs_prob_space (Z, γ, μ ⤜ (λx. g1 x ⤜ g2))"
apply(auto intro!: qbs_prob.qbs_bind_computation[OF H0 qbs_morphism_comp[OF assms(2) qbs_bind_morphism'[OF assms(3)],simplified comp_def]]
simp: real_distribution_def real_distribution_axioms_def qbs_prob_def qbs_prob_MPx[OF H2(1,2),simplified qbs_prob_def] sets_bind'[OF measurable_space[OF H1(2)] H2(2)] prob_space_bind'[OF measurable_space[OF H1(2)] H2(2)] measurable_space[OF H2(2)] space_prob_algebra[of real_borel] H2(1))
proof
fix r
show "((λx. f x ⤜ g) ∘ α) r = qbs_prob_space (Z, γ, g1 r ⤜ g2)" (is "?lhs = ?rhs") for r
by(auto intro!: qbs_prob.qbs_bind_computation(2)[of Y β]
simp: qbs_prob_MPx[OF H1(1,2),of r] assms(3) H2 fun_cong[OF H1(3),simplified comp_def])
qed
have ba: "μ ⤜ g1 ⤜ g2 = μ ⤜ (λx. g1 x ⤜ g2)"
by(auto intro!: bind_assoc[where N=real_borel and R=real_borel] simp: measurable_prob_algebraD)
show ?thesis
by(simp add: LHS RHS ba)
qed
lemma qbs_bind_cong:
assumes "s ∈ monadP_qbs_Px X"
"⋀x. x ∈ qbs_space X ⟹ f x = g x"
and "f ∈ X →⇩Q monadP_qbs Y"
shows "s ⤜ f = s ⤜ g"
proof -
obtain α μ where h0:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then have "f ∘ α ∈ monadP_qbs_MPx Y"
using assms(3) h0(1) by(auto simp: qbs_prob_def in_Mx_def)
from rep_monadP_qbs_MPx[OF this] obtain γ k where h1:
"γ ∈ qbs_Mx Y" "k ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, γ, k r))"
by auto
have hg:"g ∈ X →⇩Q monadP_qbs Y"
using qbs_morphism_cong[OF assms(2,3)] by simp
have hgs: "f ∘ α = g ∘ α"
using h0(1) assms(2) by(force simp: qbs_prob_def in_Mx_def)
show ?thesis
by(simp add: qbs_prob.qbs_bind_computation(2)[OF h0 assms(3) h1]
qbs_prob.qbs_bind_computation(2)[OF h0 hg h1[simplified hgs]])
qed
subsubsection ‹ The Functorial Action $P(f)$›
definition monadP_qbs_Pf :: "['a quasi_borel, 'b quasi_borel,'a ⇒ 'b,'a qbs_prob_space] ⇒ 'b qbs_prob_space" where
"monadP_qbs_Pf _ Y f sx ≡ sx ⤜ qbs_return Y ∘ f"
lemma monadP_qbs_Pf_morphism:
assumes "f ∈ X →⇩Q Y"
shows "monadP_qbs_Pf X Y f ∈ monadP_qbs X →⇩Q monadP_qbs Y"
unfolding monadP_qbs_Pf_def
by(rule qbs_bind_morphism'[OF qbs_morphism_comp[OF assms qbs_return_morphism]])
lemma(in qbs_prob) monadP_qbs_Pf_computation:
assumes "s = qbs_prob_space (X,α,μ)"
and "f ∈ X →⇩Q Y"
shows "qbs_prob Y (f ∘ α) μ"
and "monadP_qbs_Pf X Y f s = qbs_prob_space (Y,f ∘ α,μ)"
by(auto intro!: qbs_bind_computation[OF assms(1) qbs_morphism_comp[OF assms(2) qbs_return_morphism],of "f ∘ α" "return real_borel" ,simplified bind_return''[OF M_is_borel]]
simp: monadP_qbs_Pf_def qbs_return_comp[OF qbs_morphismE(3)[OF assms(2) in_Mx],simplified comp_assoc[symmetric]] qbs_morphismE(3)[OF assms(2) in_Mx] prob_space_return)
text ‹ We show that P is a functor i.e. P preserves identity and composition.›
lemma monadP_qbs_Pf_id:
assumes "s ∈ monadP_qbs_Px X"
shows "monadP_qbs_Pf X X id s = s"
using qbs_bind_return'[OF assms] by(simp add: monadP_qbs_Pf_def)
lemma monadP_qbs_Pf_comp:
assumes "s ∈ monadP_qbs_Px X"
"f ∈ X →⇩Q Y"
and "g ∈ Y →⇩Q Z"
shows "((monadP_qbs_Pf Y Z g) ∘ (monadP_qbs_Pf X Y f)) s = monadP_qbs_Pf X Z (g ∘ f) s"
proof -
obtain α μ where h:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
hence "qbs_prob Y (f ∘ α) μ"
"monadP_qbs_Pf X Y f s = qbs_prob_space (Y,f ∘ α,μ)"
using qbs_prob.monadP_qbs_Pf_computation[OF _ _ assms(2)] by auto
from qbs_prob.monadP_qbs_Pf_computation[OF this assms(3)] qbs_prob.monadP_qbs_Pf_computation[OF h qbs_morphism_comp[OF assms(2,3)]]
show ?thesis
by(simp add: comp_assoc)
qed
subsubsection ‹ Join ›
definition qbs_join :: "'a qbs_prob_space qbs_prob_space ⇒ 'a qbs_prob_space" where
"qbs_join ≡ (λsst. sst ⤜ id)"
lemma qbs_join_morphism:
"qbs_join ∈ monadP_qbs (monadP_qbs X) →⇩Q monadP_qbs X"
by(simp add: qbs_join_def qbs_bind_morphism'[OF qbs_morphism_ident])
lemma qbs_join_computation:
assumes "qbs_prob (monadP_qbs X) β μ"
"ssx = qbs_prob_space (monadP_qbs X,β,μ)"
"α ∈ qbs_Mx X"
"g ∈ real_borel →⇩M prob_algebra real_borel"
and "β =(λr. qbs_prob_space (X,α,g r))"
shows "qbs_prob X α (μ ⤜ g)" "qbs_join ssx = qbs_prob_space (X,α, μ ⤜ g)"
using qbs_prob.qbs_bind_computation[OF assms(1,2) qbs_morphism_ident assms(3,4)]
by(auto simp: assms(5) qbs_join_def)
subsubsection ‹ Strength ›
definition qbs_strength :: "['a quasi_borel,'b quasi_borel,'a × 'b qbs_prob_space] ⇒ ('a × 'b) qbs_prob_space" where
"qbs_strength W X = (λ(w,sx). let (_,α,μ) = rep_qbs_prob_space sx
in qbs_prob_space (W ⨂⇩Q X, λr. (w,α r), μ))"
lemma(in qbs_prob) qbs_strength_computation:
assumes "w ∈ qbs_space W"
and "sx = qbs_prob_space (X,α,μ)"
shows "qbs_prob (W ⨂⇩Q X) (λr. (w,α r)) μ"
"qbs_strength W X (w,sx) = qbs_prob_space (W ⨂⇩Q X, λr. (w,α r), μ)"
proof -
interpret qp1: qbs_prob "W ⨂⇩Q X" "λr. (w,α r)" μ
by(auto intro!: qbs_probI simp: assms(1) pair_qbs_Mx_def comp_def)
show "qbs_prob (W ⨂⇩Q X) (λr. (w,α r)) μ"
"qbs_strength W X (w,sx) = qbs_prob_space (W ⨂⇩Q X, λr. (w,α r), μ)"
apply(simp_all add: qp1.qbs_prob_axioms qbs_strength_def rep_qbs_prob_space_def qbs_prob_space.rep_def)
apply(rule someI2[where a="(X,α,μ)"])
proof(auto simp: in_Rep assms(2))
fix X' α' μ'
assume h:"(X',α',μ') ∈ Rep_qbs_prob_space (qbs_prob_space (X, α, μ))"
from if_in_Rep(1,2)[OF this] interpret pqp: pair_qbs_prob "W ⨂⇩Q X" "λr. (w, α' r)" μ' "W ⨂⇩Q X" "λr. (w,α r)" μ
by(simp add: pair_qbs_prob_def qp1.qbs_prob_axioms)
(auto intro!: qbs_probI simp: pair_qbs_Mx_def comp_def assms(1) qbs_prob_def in_Mx_def)
note [simp] = qbs_prob_eq2_dest[OF if_in_Rep(3)[OF h,simplified qbs_prob_eq_equiv12]]
show "qbs_prob_space (W ⨂⇩Q X, λr. (w, α' r), μ') = qbs_prob_space (W ⨂⇩Q X, λr. (w, α r), μ)"
proof(rule pqp.qbs_prob_space_eq2)
fix f
assume "f ∈ qbs_to_measure (W ⨂⇩Q X) →⇩M real_borel"
note qbs_morphism_dest[OF qbs_morphismE(2)[OF curry_preserves_morphisms[OF qbs_morphism_measurable_intro[OF this]] assms(1),simplified]]
show "(∫y. f ((λr. (w, α' r)) y) ∂ μ') = (∫y. f ((λr. (w, α r)) y) ∂ μ)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫y. curry f w (α' y) ∂ μ')" by auto
also have "... = (∫y. curry f w (α y) ∂ μ)"
by(rule qbs_prob_eq2_dest(4)[OF if_in_Rep(3)[OF h,simplified qbs_prob_eq_equiv12],symmetric]) fact
also have "... = ?rhs" by auto
finally show ?thesis .
qed
qed simp
qed
qed
lemma qbs_strength_natural:
assumes "f ∈ X →⇩Q X'"
"g ∈ Y →⇩Q Y'"
"x ∈ qbs_space X"
and "sy ∈ monadP_qbs_Px Y"
shows "(monadP_qbs_Pf (X ⨂⇩Q Y) (X' ⨂⇩Q Y') (map_prod f g) ∘ qbs_strength X Y) (x,sy) = (qbs_strength X' Y' ∘ map_prod f (monadP_qbs_Pf Y Y' g)) (x,sy)"
(is "?lhs = ?rhs")
proof -
obtain β ν where hy:
"qbs_prob Y β ν" "sy = qbs_prob_space (Y,β,ν)"
using rep_monadP_qbs_Px[OF assms(4)] by auto
have "qbs_prob (X ⨂⇩Q Y) (λr. (x, β r)) ν"
"qbs_strength X Y (x, sy) = qbs_prob_space (X ⨂⇩Q Y, λr. (x, β r), ν)"
using qbs_prob.qbs_strength_computation[OF hy(1) assms(3) hy(2)] by auto
hence LHS:"?lhs = qbs_prob_space (X' ⨂⇩Q Y',map_prod f g ∘ (λr. (x, β r)),ν)"
by(simp add: qbs_prob.monadP_qbs_Pf_computation[OF _ _ qbs_morphism_map_prod[OF assms(1,2)]])
have "map_prod f (monadP_qbs_Pf Y Y' g) (x,sy) = (f x,qbs_prob_space (Y',g ∘ β,ν))"
"qbs_prob Y' (g ∘ β) ν"
by(auto simp: qbs_prob.monadP_qbs_Pf_computation[OF hy assms(2)])
hence RHS:"?rhs = qbs_prob_space (X' ⨂⇩Q Y',λr. (f x, (g ∘ β) r),ν)"
using qbs_prob.qbs_strength_computation[OF _ _ refl,of Y' "g ∘ β" ν "f x" X'] assms(1,3)
by auto
show "?lhs = ?rhs"
unfolding LHS RHS
by(simp add: comp_def)
qed
lemma qbs_strength_ab_r:
assumes "α ∈ qbs_Mx X"
"β ∈ monadP_qbs_MPx Y"
"γ ∈ qbs_Mx Y"
and [measurable]:"g ∈ real_borel →⇩M prob_algebra real_borel"
and "β = (λr. qbs_prob_space (Y,γ,g r))"
shows "qbs_prob (X ⨂⇩Q Y) (map_prod α γ ∘ real_real.g) (distr (return real_borel r ⨂⇩M g r) real_borel real_real.f)"
"qbs_strength X Y (α r, β r) = qbs_prob_space (X ⨂⇩Q Y, map_prod α γ ∘ real_real.g, distr (return real_borel r ⨂⇩M g r) real_borel real_real.f)"
proof -
have [measurable_cong]: "sets (g r) = sets real_borel"
"sets (return real_borel r) = sets real_borel"
using measurable_space[OF assms(4),of r]
by(simp_all add: space_prob_algebra)
interpret qp: qbs_prob "X ⨂⇩Q Y" "map_prod α γ ∘ real_real.g" "distr (return real_borel r ⨂⇩M g r) real_borel real_real.f"
proof(auto intro!: qbs_probI)
show "map_prod α γ ∘ real_real.g ∈ pair_qbs_Mx X Y"
using qbs_closed1_dest[OF assms(1)] qbs_closed1_dest[OF assms(3)]
by(auto simp: comp_def qbs_prob_def in_Mx_def pair_qbs_Mx_def)
next
show "prob_space (distr (return real_borel r ⨂⇩M g r) real_borel real_real.f) "
using measurable_space[OF assms(4),of r]
by(auto intro!: prob_space.prob_space_distr simp: prob_algebra_real_prob_measure prob_space_pair prob_space_return real_distribution.axioms(1))
qed
interpret pqp: pair_qbs_prob "X ⨂⇩Q Y" "λl. (α r, γ l)" "g r" "X ⨂⇩Q Y" "map_prod α γ ∘ real_real.g" "distr (return real_borel r ⨂⇩M g r) real_borel real_real.f"
by(simp add: qbs_prob.qbs_strength_computation[OF qbs_prob_MPx[OF assms(3,4)] qbs_Mx_to_X(2)[OF assms(1)] fun_cong[OF assms(5)],of r] pair_qbs_prob_def qp.qbs_prob_axioms)
have [measurable]: "map_prod α γ ∈ real_borel ⨂⇩M real_borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
proof -
have "map_prod α γ ∈ ℝ⇩Q ⨂⇩Q ℝ⇩Q →⇩Q X ⨂⇩Q Y"
using assms(1,3) by(auto intro!: qbs_morphism_map_prod simp: qbs_Mx_is_morphisms)
hence "map_prod α γ ∈ qbs_to_measure (ℝ⇩Q ⨂⇩Q ℝ⇩Q) →⇩M qbs_to_measure (X ⨂⇩Q Y)"
using l_preserves_morphisms by auto
thus ?thesis
by simp
qed
hence [measurable]:"(λl. (α r, γ l)) ∈ real_borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
using pqp.qp1.in_Mx qbs_Mx_are_measurable by blast
show "qbs_prob (X ⨂⇩Q Y) (map_prod α γ ∘ real_real.g) (distr (return real_borel r ⨂⇩M g r) real_borel real_real.f)"
"qbs_strength X Y (α r, β r) = qbs_prob_space (X ⨂⇩Q Y, map_prod α γ ∘ real_real.g, distr (return real_borel r ⨂⇩M g r) real_borel real_real.f)"
apply(simp_all add: qp.qbs_prob_axioms qbs_prob.qbs_strength_computation(2)[OF qbs_prob_MPx[OF assms(3,4)] qbs_Mx_to_X(2)[OF assms(1)] fun_cong[OF assms(5)],of r])
proof(rule pqp.qbs_prob_space_eq)
show "distr (g r) (qbs_to_measure (X ⨂⇩Q Y)) (λl. (α r, γ l)) = distr (distr (return real_borel r ⨂⇩M g r) real_borel real_real.f) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ ∘ real_real.g)"
(is "?lhs = ?rhs")
proof -
have "?lhs = distr (g r) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ ∘ Pair r)"
by(simp add: comp_def)
also have "... = distr (distr (g r) (real_borel ⨂⇩M real_borel) (Pair r)) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ)"
by(auto intro!: distr_distr[symmetric])
also have "... = distr (return real_borel r ⨂⇩M g r) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ)"
proof -
have "return real_borel r ⨂⇩M g r = distr (g r) (real_borel ⨂⇩M real_borel) (λl. (r,l))"
proof(auto intro!: measure_eqI)
fix A
assume h':"A ∈ sets (real_borel ⨂⇩M real_borel)"
show "emeasure (return real_borel r ⨂⇩M g r) A = emeasure (distr (g r) (real_borel ⨂⇩M real_borel) (Pair r)) A"
(is "?lhs' = ?rhs'")
proof -
have "?lhs' = ∫⇧+ x. emeasure (g r) (Pair x -` A) ∂return real_borel r"
by(auto intro!: pqp.qp1.emeasure_pair_measure_alt simp: h')
also have "... = emeasure (g r) (Pair r -` A)"
by(auto intro!: nn_integral_return pqp.qp1.measurable_emeasure_Pair simp: h')
also have "... = ?rhs'"
by(simp add: emeasure_distr[OF _ h'])
finally show ?thesis .
qed
qed
thus ?thesis by simp
qed
also have "... = ?rhs"
by(rule distr_distr[of "map_prod α γ ∘ real_real.g" real_borel "qbs_to_measure (X ⨂⇩Q Y)" real_real.f "return real_borel r ⨂⇩M g r",simplified comp_assoc,simplified,symmetric])
finally show ?thesis .
qed
qed simp
qed
lemma qbs_strength_morphism:
"qbs_strength X Y ∈ X ⨂⇩Q monadP_qbs Y →⇩Q monadP_qbs (X ⨂⇩Q Y)"
proof(rule pair_qbs_morphismI,simp)
fix α β
assume h:"α ∈ qbs_Mx X"
"β ∈ monadP_qbs_MPx Y"
then obtain γ g where hb:
"γ ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (Y, γ, g r))"
using rep_monadP_qbs_MPx[of β] by blast
note [measurable] = hb(2)
show "qbs_strength X Y ∘ (λr. (α r, β r)) ∈ monadP_qbs_MPx (X ⨂⇩Q Y)"
using qbs_strength_ab_r[OF h hb]
by(auto intro!: bexI[where x="map_prod α γ ∘ real_real.g"] bexI[where x="λr. distr (return real_borel r ⨂⇩M g r) real_borel real_real.f"]
simp: monadP_qbs_MPx_def in_MPx_def qbs_prob_def in_Mx_def)
qed
lemma qbs_bind_morphism'':
"(λ(f,x). x ⤜ f) ∈ exp_qbs X (monadP_qbs Y) ⨂⇩Q (monadP_qbs X) →⇩Q (monadP_qbs Y)"
proof(rule qbs_morphism_cong[of _ "qbs_join ∘ (monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) ⨂⇩Q X) (monadP_qbs Y) qbs_eval) ∘ (qbs_strength (exp_qbs X (monadP_qbs Y)) X)"], auto)
fix f
fix sx
assume h:"f ∈ X →⇩Q monadP_qbs Y"
"sx ∈ monadP_qbs_Px X"
then obtain α μ where h0:"qbs_prob X α μ" "sx = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[of sx X] by auto
hence "f ∘ α ∈ monadP_qbs_MPx Y"
using h(1) by(auto simp: qbs_prob_def in_Mx_def)
then obtain β g where h1:
"β ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, β, g r))"
using rep_monadP_qbs_MPx[of "f ∘ α" Y] by blast
show "qbs_join (monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) ⨂⇩Q X) (monadP_qbs Y) qbs_eval (qbs_strength (exp_qbs X (monadP_qbs Y)) X (f, sx))) =
sx ⤜ f"
by(simp add: qbs_join_computation[OF qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h0(1) _ h0(2),of f "exp_qbs X (monadP_qbs Y)"] qbs_eval_morphism] h1(1,2),simplified qbs_eval_def comp_def,simplified,OF h(1) h1(3)[simplified comp_def]] qbs_prob.qbs_bind_computation[OF h0 h(1) h1])
next
show "qbs_join ∘ monadP_qbs_Pf (exp_qbs X (monadP_qbs Y) ⨂⇩Q X) (monadP_qbs Y) qbs_eval ∘ qbs_strength (exp_qbs X (monadP_qbs Y)) X ∈ exp_qbs X (monadP_qbs Y) ⨂⇩Q monadP_qbs X →⇩Q monadP_qbs Y"
using qbs_join_morphism monadP_qbs_Pf_morphism[OF qbs_eval_morphism]
by(auto intro!: qbs_morphism_comp simp: qbs_strength_morphism)
qed
lemma qbs_bind_morphism''':
"(λf x. x ⤜ f) ∈ exp_qbs X (monadP_qbs Y) →⇩Q exp_qbs (monadP_qbs X) (monadP_qbs Y)"
using qbs_bind_morphism'' curry_preserves_morphisms[of "λ(f, x). qbs_bind x f"]
by fastforce
lemma qbs_bind_morphism:
assumes "f ∈ X →⇩Q monadP_qbs Y"
and "g ∈ X →⇩Q exp_qbs Y (monadP_qbs Z)"
shows "(λx. f x ⤜ g x) ∈ X →⇩Q monadP_qbs Z"
using qbs_morphism_comp[OF qbs_morphism_tuple[OF assms(2,1)] qbs_bind_morphism'']
by(simp add: comp_def)
lemma qbs_bind_morphism'''':
assumes "x ∈ monadP_qbs_Px X"
shows "(λf. x ⤜ f) ∈ exp_qbs X (monadP_qbs Y) →⇩Q monadP_qbs Y"
by(rule qbs_morphismE(2)[OF arg_swap_morphism[OF qbs_bind_morphism'''],simplified,OF assms])
lemma qbs_strength_law1:
assumes "x ∈ qbs_space (unit_quasi_borel ⨂⇩Q monadP_qbs X)"
shows "snd x = (monadP_qbs_Pf (unit_quasi_borel ⨂⇩Q X) X snd ∘ qbs_strength unit_quasi_borel X) x"
proof -
obtain α μ where h:
"qbs_prob X α μ" "(snd x) = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[of "snd x" X] assms by auto
have [simp]: "((),snd x) = x"
using SigmaE assms by auto
show ?thesis
using qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "fst x" "unit_quasi_borel",simplified] snd_qbs_morphism]
by(simp add: h(2) comp_def)
qed
lemma qbs_strength_law2:
assumes "x ∈ qbs_space ((X ⨂⇩Q Y) ⨂⇩Q monadP_qbs Z)"
shows "(qbs_strength X (Y ⨂⇩Q Z) ∘ (map_prod id (qbs_strength Y Z)) ∘ (λ((x,y),z). (x,(y,z)))) x =
(monadP_qbs_Pf ((X ⨂⇩Q Y) ⨂⇩Q Z) (X ⨂⇩Q (Y ⨂⇩Q Z)) (λ((x,y),z). (x,(y,z))) ∘ qbs_strength (X ⨂⇩Q Y) Z) x"
(is "?lhs = ?rhs")
proof -
obtain α μ where h:
"qbs_prob Z α μ" "snd x = qbs_prob_space (Z, α, μ)"
using rep_monadP_qbs_Px[of "snd x" Z] assms by auto
have "?lhs = qbs_prob_space (X ⨂⇩Q Y ⨂⇩Q Z, λr. (fst (fst x), snd (fst x), α r), μ)"
using assms qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "snd (fst x)" Y]
by(auto intro!: qbs_prob.qbs_strength_computation)
also have "... = ?rhs"
using qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h(1) _ h(2),of "fst x" "X ⨂⇩Q Y"] qbs_morphism_pair_assoc1] assms
by(auto simp: comp_def)
finally show ?thesis .
qed
lemma qbs_strength_law3:
assumes "x ∈ qbs_space (X ⨂⇩Q Y)"
shows "qbs_return (X ⨂⇩Q Y) x = (qbs_strength X Y ∘ (map_prod id (qbs_return Y))) x"
proof -
interpret qp: qbs_prob Y "λr. snd x" "return real_borel 0"
using assms by(auto intro!: qbs_probI simp: prob_space_return)
show ?thesis
using qp.qbs_strength_computation[OF _ qp.qbs_return_computation[of "snd x" Y],of "fst x" X] assms
by(auto simp: qp.qbs_return_computation[OF assms])
qed
lemma qbs_strength_law4:
assumes "x ∈ qbs_space (X ⨂⇩Q monadP_qbs (monadP_qbs Y))"
shows "(qbs_strength X Y ∘ map_prod id qbs_join) x = (qbs_join ∘ monadP_qbs_Pf (X ⨂⇩Q monadP_qbs Y) (monadP_qbs (X ⨂⇩Q Y))(qbs_strength X Y) ∘ qbs_strength X (monadP_qbs Y)) x"
(is "?lhs = ?rhs")
proof -
obtain β μ where h0:
"qbs_prob (monadP_qbs Y) β μ" "snd x = qbs_prob_space (monadP_qbs Y, β, μ)"
using rep_monadP_qbs_Px[of "snd x" "monadP_qbs Y"] assms by auto
then obtain γ g where h1:
"γ ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"β = (λr. qbs_prob_space (Y, γ, g r))"
using rep_monadP_qbs_MPx[of β Y] by(auto simp: qbs_prob_def in_Mx_def)
have "?lhs = qbs_prob_space (X ⨂⇩Q Y, λr. (fst x, γ r), μ ⤜ g)"
using qbs_prob.qbs_strength_computation[OF qbs_join_computation(1)[OF h0 h1] _ qbs_join_computation(2)[OF h0 h1],of "fst x" X] assms
by auto
also have "... = ?rhs"
proof -
have "qbs_strength X Y ∘ (λr. (fst x, β r)) = (λr. qbs_prob_space (X ⨂⇩Q Y, λr. (fst x, γ r), g r))"
proof
show "(qbs_strength X Y ∘ (λr. (fst x, β r))) r = qbs_prob_space (X ⨂⇩Q Y, λr. (fst x, γ r), g r)" for r
using qbs_prob.qbs_strength_computation(2)[OF qbs_prob_MPx[OF h1(1,2),of r] _ fun_cong[OF h1(3)],of "fst x" X] assms
by auto
qed
thus ?thesis
using qbs_join_computation(2)[OF qbs_prob.monadP_qbs_Pf_computation[OF qbs_prob.qbs_strength_computation[OF h0(1) _ h0(2),of "fst x" X] qbs_strength_morphism] _ h1(2),of "λr. (fst x, γ r)",symmetric] assms h1(1)
by(auto simp: pair_qbs_Mx_def comp_def)
qed
finally show ?thesis .
qed
lemma qbs_return_Mxpair:
assumes "α ∈ qbs_Mx X"
and "β ∈ qbs_Mx Y"
shows "qbs_return (X ⨂⇩Q Y) (α r, β k) = qbs_prob_space (X ⨂⇩Q Y,map_prod α β ∘ real_real.g, distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f)"
"qbs_prob (X ⨂⇩Q Y) (map_prod α β ∘ real_real.g) (distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f)"
proof -
note [measurable_cong] = sets_return[of real_borel]
interpret qp: qbs_prob "X ⨂⇩Q Y" "map_prod α β ∘ real_real.g" "distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f"
using qbs_closed1_dest[OF assms(1)] qbs_closed1_dest[OF assms(2)]
by(auto intro!: qbs_probI prob_space.prob_space_distr prob_space_pair
simp: pair_qbs_Mx_def comp_def prob_space_return)
show "qbs_return (X ⨂⇩Q Y) (α r, β k) = qbs_prob_space (X ⨂⇩Q Y,map_prod α β ∘ real_real.g, distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f)"
"qbs_prob (X ⨂⇩Q Y) (map_prod α β ∘ real_real.g) (distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f)"
proof -
show "qbs_return (X ⨂⇩Q Y) (α r, β k) = qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, distr (return real_borel r ⨂⇩M return real_borel k) real_borel real_real.f)"
(is "?lhs = ?rhs")
proof -
have 1:"(λr. qbs_prob_space (Y, β, return real_borel k)) ∈ monadP_qbs_MPx Y"
by(auto intro!: in_MPx.intro bexI[where x=β] bexI[where x="λr. return real_borel k"] simp: monadP_qbs_MPx_def assms(2))
have "?lhs = (qbs_strength X Y ∘ map_prod id (qbs_return Y)) (α r, β k)"
by(intro qbs_strength_law3[of "(α r, β k)" X Y]) (use assms in auto)
also have "... = qbs_strength X Y (α r, qbs_prob_space (Y, β, return real_borel k))"
using fun_cong[OF qbs_return_comp[OF assms(2)]] by simp
also have "... = ?rhs"
by(intro qbs_strength_ab_r(2)[OF assms(1) 1 assms(2) _ refl,of r]) auto
finally show ?thesis .
qed
qed(rule qp.qbs_prob_axioms)
qed
lemma pair_return_return:
assumes "l ∈ space M"
and "r ∈ space N"
shows "return M l ⨂⇩M return N r = return (M ⨂⇩M N) (l,r)"
proof(auto intro!: measure_eqI)
fix A
assume h:"A ∈ sets (M ⨂⇩M N)"
show "emeasure (return M l ⨂⇩M return N r) A = indicator A (l, r)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂return N r ∂return M l)"
by(auto intro!: sigma_finite_measure.emeasure_pair_measure prob_space_imp_sigma_finite simp: h prob_space_return assms)
also have "... = (∫⇧+ x. indicator A (x, r) ∂return M l)"
using h by(auto intro!: nn_integral_cong nn_integral_return simp: assms(2))
also have "... = ?rhs"
using h by(auto intro!: nn_integral_return simp: assms)
finally show ?thesis .
qed
qed
lemma bind_bind_return_distr:
assumes "real_distribution μ"
and "real_distribution ν"
shows "μ ⤜ (λr. ν ⤜ (λl. distr (return real_borel r ⨂⇩M return real_borel l) real_borel real_real.f))
= distr (μ ⨂⇩M ν) real_borel real_real.f"
(is "?lhs = ?rhs")
proof -
interpret rd1: real_distribution μ by fact
interpret rd2: real_distribution ν by fact
interpret pp: pair_prob_space μ ν
by (simp add: pair_prob_space.intro pair_sigma_finite_def rd1.prob_space_axioms rd1.sigma_finite_measure_axioms rd2.prob_space_axioms rd2.sigma_finite_measure_axioms)
have "?lhs = μ ⤜ (λr. ν ⤜ (λl. distr (return (real_borel ⨂⇩M real_borel) (r,l)) real_borel real_real.f))"
using pair_return_return[of _ real_borel _ real_borel] by simp
also have "... = μ ⤜ (λr. ν ⤜ (λl. distr (return (μ ⨂⇩M ν) (r, l)) real_borel real_real.f))"
proof -
have "return (real_borel ⨂⇩M real_borel) = return (μ ⨂⇩M ν)"
by(auto intro!: return_sets_cong sets_pair_measure_cong)
thus ?thesis by simp
qed
also have "... = μ ⤜ (λr. distr (ν ⤜ (λl. (return (μ ⨂⇩M ν) (r, l)))) real_borel real_real.f)"
by(auto intro!: bind_cong distr_bind[symmetric,where K="μ ⨂⇩M ν"])
also have "... = distr (μ ⤜ (λr. ν ⤜ (λl. return (μ ⨂⇩M ν) (r, l)))) real_borel real_real.f"
by(auto intro!: distr_bind[symmetric,where K="μ ⨂⇩M ν"])
also have "... = ?rhs"
by(simp add: pp.pair_measure_eq_bind[symmetric])
finally show ?thesis .
qed
lemma(in pair_qbs_probs) qbs_bind_return_qp:
shows "qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_prob_space (X, α, μ) ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,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)"
proof -
show "qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_prob_space (X, α, μ) ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x, y))) = 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 ⨂⇩Q Y, map_prod α β ∘ real_real.g, ν ⤜ (λl. μ ⤜ (λr. distr (return real_borel r ⨂⇩M return real_borel l) real_borel real_real.f)))"
proof(auto intro!: qp2.qbs_bind_computation(2) measurable_bind_prob_space2[where N=real_borel] simp: in_Mx[simplified])
show "(λy. qbs_prob_space (X, α, μ) ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x, y))) ∈ Y →⇩Q monadP_qbs (X ⨂⇩Q Y)"
using qbs_morphism_const[of _ "monadP_qbs X" Y,simplified,OF qp1.qbs_prob_space_in_Px] curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X ⨂⇩Q Y"]]]
by (auto intro!: qbs_bind_morphism)
next
show "(λy. qbs_prob_space (X, α, μ) ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x, y))) ∘ β = (λr. qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, μ ⤜ (λl. distr (return real_borel l ⨂⇩M return real_borel r) real_borel real_real.f)))"
by standard
(auto intro!: qp1.qbs_bind_computation(2) qbs_morphism_comp[OF qbs_morphism_Pair2[of _ Y] qbs_return_morphism[of "X ⨂⇩Q Y"],simplified comp_def]
simp: in_Mx[simplified] qbs_return_Mxpair[OF qp1.in_Mx qp2.in_Mx] qbs_Mx_to_X(2))
qed
also have "... = ?rhs"
proof -
have "ν ⤜ (λl. μ ⤜ (λr. distr (return real_borel r ⨂⇩M return real_borel l) real_borel real_real.f)) = distr (μ ⨂⇩M ν) real_borel real_real.f"
by(auto intro!: bind_rotate[symmetric,where N=real_borel] measurable_prob_algebraD
simp: bind_bind_return_distr[symmetric,OF qp1.real_distribution_axioms qp2.real_distribution_axioms])
thus ?thesis by simp
qed
finally show ?thesis .
qed
show "qbs_prob (X ⨂⇩Q Y) (map_prod α β ∘ real_real.g) (distr (μ ⨂⇩M ν) real_borel real_real.f)"
by(rule qbs_prob_axioms)
qed
lemma(in pair_qbs_probs) qbs_bind_return_pq:
shows "qbs_prob_space (X, α, μ) ⤜ (λx. qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,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)"
proof(simp_all add: qbs_bind_return_qp(2))
show "qbs_prob_space (X, α, μ) ⤜ (λx. qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x, y))) = qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, distr (μ ⨂⇩M ν) real_borel real_real.f)"
(is "?lhs = _")
proof -
have "?lhs = qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, μ ⤜ (λr. ν ⤜ (λl. distr (return real_borel r ⨂⇩M return real_borel l) real_borel real_real.f)))"
proof(auto intro!: qp1.qbs_bind_computation(2) measurable_bind_prob_space2[where N=real_borel])
show "(λx. qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x, y))) ∈ X →⇩Q monadP_qbs (X ⨂⇩Q Y)"
using qbs_morphism_const[of _ "monadP_qbs Y" X,simplified,OF qp2.qbs_prob_space_in_Px] curry_preserves_morphisms[OF qbs_return_morphism[of "X ⨂⇩Q Y"]]
by(auto intro!: qbs_bind_morphism simp: curry_def)
next
show "(λx. qbs_prob_space (Y, β, ν) ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x, y))) ∘ α = (λr. qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, ν ⤜ (λl. distr (return real_borel r ⨂⇩M return real_borel l) real_borel real_real.f)))"
by standard
(auto intro!: qp2.qbs_bind_computation(2) qbs_morphism_comp[OF qbs_morphism_Pair1[of _ X] qbs_return_morphism[of "X ⨂⇩Q Y"],simplified comp_def]
simp: qbs_return_Mxpair[OF qp1.in_Mx qp2.in_Mx] qbs_Mx_to_X(2))
qed
thus ?thesis
by(simp add: bind_bind_return_distr[OF qp1.real_distribution_axioms qp2.real_distribution_axioms])
qed
qed
lemma qbs_bind_return_rotate:
assumes "p ∈ monadP_qbs_Px X"
and "q ∈ monadP_qbs_Px Y"
shows "q ⤜ (λy. p ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,y))) = p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y)))"
proof -
obtain α μ where hp:
"qbs_prob X α μ" "p = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
obtain β ν where hq:
"qbs_prob Y β ν" "q = qbs_prob_space (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(2) hq(2) pqp.qbs_bind_return_pq(1) pqp.qbs_bind_return_qp)
qed
lemma qbs_pair_bind_return1:
assumes "f ∈ X ⨂⇩Q Y →⇩Q monadP_qbs Z"
"p ∈ monadP_qbs_Px X"
and "q ∈ monadP_qbs_Px Y"
shows "q ⤜ (λy. p ⤜ (λx. f (x,y))) = (q ⤜ (λy. p ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,y)))) ⤜ f"
(is "?lhs = ?rhs")
proof -
note [simp] = qbs_morphism_const[of _ "monadP_qbs X",simplified,OF assms(2)]
qbs_morphism_Pair1'[OF _ assms(1)] qbs_morphism_Pair2'[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"]]
arg_swap_morphism[OF curry_preserves_morphisms[OF assms(1)],simplified curry_def]
curry_preserves_morphisms[OF qbs_morphism_comp[OF qbs_morphism_pair_swap[OF qbs_return_morphism[of "X ⨂⇩Q Y"]] qbs_bind_morphism'[OF assms(1)]],simplified curry_def comp_def,simplified]
have [simp]:"(λy. p ⤜ (λx. f (x,y))) ∈ Y →⇩Q monadP_qbs Z"
"(λy. p ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,y) ⤜ f)) ∈ Y →⇩Q monadP_qbs Z"
by(auto intro!: qbs_bind_morphism[where Y=X] simp: curry_def)
have "?lhs = q ⤜ (λy. p ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,y) ⤜ f))"
by(auto intro!: qbs_bind_cong[OF assms(3),where Y=Z] qbs_bind_cong[OF assms(2),where Y=Z] simp: qbs_bind_return[OF assms(1)])
also have "... = q ⤜ (λy. (p ⤜ (λx. qbs_return (X ⨂⇩Q Y) (x,y))) ⤜ f)"
by(auto intro!: qbs_bind_cong[OF assms(3),where Y=Z] qbs_bind_assoc[OF assms(2) _ assms(1)] simp: )
also have "... = ?rhs"
by(auto intro!: qbs_bind_assoc[OF assms(3)_ assms(1)] qbs_bind_morphism[where Y=X])
finally show ?thesis .
qed
lemma qbs_pair_bind_return2:
assumes "f ∈ X ⨂⇩Q Y →⇩Q monadP_qbs Z"
"p ∈ monadP_qbs_Px X"
and "q ∈ monadP_qbs_Px Y"
shows "p ⤜ (λx. q ⤜ (λy. f (x,y))) = (p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y)))) ⤜ f"
(is "?lhs = ?rhs")
proof -
note [simp] = qbs_morphism_const[of _ "monadP_qbs Y",simplified,OF assms(3)]
qbs_morphism_Pair1'[OF _ assms(1)] curry_preserves_morphisms[OF assms(1),simplified curry_def]
qbs_morphism_Pair1'[OF _ qbs_return_morphism[of "X ⨂⇩Q Y"]]
curry_preserves_morphisms[OF qbs_morphism_comp[OF qbs_return_morphism[of "X ⨂⇩Q Y"] qbs_bind_morphism'[OF assms(1)]],simplified curry_def comp_def,simplified]
curry_preserves_morphisms[OF qbs_return_morphism[of "X ⨂⇩Q Y"],simplified curry_def]
have [simp]: "(λx. q ⤜ (λy. f (x, y))) ∈ X →⇩Q monadP_qbs Z"
"(λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x, y) ⤜ f)) ∈ X →⇩Q monadP_qbs Z"
by(auto intro!: qbs_bind_morphism[where Y=Y])
have "?lhs = p ⤜ (λx. q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y) ⤜ f))"
by(auto intro!: qbs_bind_cong[OF assms(2),where Y=Z] qbs_bind_cong[OF assms(3),where Y=Z] simp: qbs_bind_return[OF assms(1)])
also have "... = p ⤜ (λx. (q ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y))) ⤜ f)"
by(auto intro!: qbs_bind_cong[OF assms(2),where Y=Z] qbs_bind_assoc[OF assms(3) _ assms(1)])
also have "... = ?rhs"
by(auto intro!: qbs_bind_assoc[OF assms(2) _ assms(1)] qbs_bind_morphism[where Y=Y])
finally show ?thesis .
qed
lemma qbs_bind_rotate:
assumes "f ∈ X ⨂⇩Q Y →⇩Q monadP_qbs Z"
"p ∈ monadP_qbs_Px X"
and "q ∈ monadP_qbs_Px Y"
shows "q ⤜ (λy. p ⤜ (λx. f (x,y))) = p ⤜ (λx. q ⤜ (λy. f (x,y)))"
using qbs_pair_bind_return1[OF assms(1) assms(2) assms(3)] qbs_bind_return_rotate[OF assms(2) assms(3)] qbs_pair_bind_return2[OF assms(1) assms(2) assms(3)]
by simp
lemma(in pair_qbs_probs) qbs_bind_bind_return:
assumes "f ∈ X ⨂⇩Q Y →⇩Q Z"
shows "qbs_prob Z (f ∘ (map_prod α β ∘ real_real.g)) (distr (μ ⨂⇩M ν) real_borel real_real.f)"
and "qbs_prob_space (X,α,μ) ⤜ (λx. qbs_prob_space (Y,β,ν) ⤜ (λy. qbs_return Z (f (x,y)))) = qbs_prob_space (Z,f ∘ (map_prod α β ∘ real_real.g),distr (μ ⨂⇩M ν) real_borel real_real.f)"
(is "?lhs = ?rhs")
proof -
show "qbs_prob Z (f ∘ (map_prod α β ∘ real_real.g)) (distr (μ ⨂⇩M ν) real_borel real_real.f)"
using qbs_bind_return_qp(2) qbs_morphismE(3)[OF assms] by(simp add: qbs_prob_def in_Mx_def)
next
have "?lhs = (qbs_prob_space (X,α,μ) ⤜ (λx. qbs_prob_space (Y,β,ν) ⤜ (λy. qbs_return (X ⨂⇩Q Y) (x,y)))) ⤜ qbs_return Z ∘ f"
using qbs_pair_bind_return2[OF qbs_morphism_comp[OF assms qbs_return_morphism] qp1.qbs_prob_space_in_Px qp2.qbs_prob_space_in_Px]
by(simp add: comp_def)
also have "... = qbs_prob_space (X ⨂⇩Q Y, map_prod α β ∘ real_real.g, distr (μ ⨂⇩M ν) real_borel real_real.f) ⤜ qbs_return Z ∘ f"
by(simp add: qbs_bind_return_pq(1))
also have "... = ?rhs"
by(rule monadP_qbs_Pf_computation[OF refl assms,simplified monadP_qbs_Pf_def])
finally show "?lhs = ?rhs" .
qed
subsubsection ‹ Properties of Return and Bind ›
lemma qbs_prob_measure_return:
assumes "x ∈ qbs_space X"
shows "qbs_prob_measure (qbs_return X x) = return (qbs_to_measure X) x"
proof -
interpret qp: qbs_prob X "λr. x" "return real_borel 0"
by(auto intro!: qbs_probI simp: prob_space_return assms)
show ?thesis
by(simp add: qp.qbs_return_computation[OF assms] distr_return)
qed
lemma qbs_prob_measure_bind:
assumes "s ∈ monadP_qbs_Px X"
and "f ∈ X →⇩Q monadP_qbs Y"
shows "qbs_prob_measure (s ⤜ f) = qbs_prob_measure s ⤜ qbs_prob_measure ∘ f"
(is "?lhs = ?rhs")
proof -
obtain α μ where hs:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by blast
hence "f ∘ α ∈ monadP_qbs_MPx Y"
using assms(2) by(auto simp: qbs_prob_def in_Mx_def)
then obtain β g where hbg:
"β ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, β, g r))"
using rep_monadP_qbs_MPx by blast
note [measurable] = hbg(2)
have [measurable]:"f ∈ qbs_to_measure X →⇩M qbs_to_measure (monadP_qbs Y)"
using l_preserves_morphisms assms(2) by auto
interpret pqp: pair_qbs_probs X α μ Y β "μ ⤜ g"
by(simp add: pair_qbs_probs_def hs(1) qbs_prob.qbs_bind_computation[OF hs assms(2) hbg])
have "?lhs = distr (μ ⤜ g) (qbs_to_measure Y) β"
by(simp add: pqp.qp1.qbs_bind_computation[OF hs(2) assms(2) hbg])
also have "... = μ ⤜ (λx. distr (g x) (qbs_to_measure Y) β)"
by(auto intro!: distr_bind[where K=real_borel] measurable_prob_algebraD)
also have "... = μ ⤜ (λx. qbs_prob_measure (qbs_prob_space (Y,β,g x)))"
using measurable_space[OF hbg(2)]
by(auto intro!: bind_cong qbs_prob.qbs_prob_measure_computation[symmetric] qbs_probI simp: space_prob_algebra)
also have "... = μ ⤜ (λx. qbs_prob_measure ((f ∘ α) x))"
by(simp add: hbg(3))
also have "... = μ ⤜ (λx. (qbs_prob_measure ∘ f) (α x))" by simp
also have "... = distr μ (qbs_to_measure X) α ⤜ qbs_prob_measure ∘ f"
by(intro bind_distr[symmetric,where K="qbs_to_measure Y"]) auto
also have "... = ?rhs"
by(simp add: hs(2))
finally show ?thesis .
qed
lemma qbs_of_return:
assumes "x ∈ qbs_space X"
shows "qbs_prob_space_qbs (qbs_return X x) = X"
using real_distribution.qbs_return_computation[OF _ assms,of "return real_borel 0"]
qbs_prob.qbs_prob_space_qbs_computation[of X "λr. x" "return real_borel 0"] assms
by(auto simp: qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def prob_space_return)
lemma qbs_of_bind:
assumes "s ∈ monadP_qbs_Px X"
and "f ∈ X →⇩Q monadP_qbs Y"
shows "qbs_prob_space_qbs (s ⤜ f) = Y"
proof -
obtain α μ where hs:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
hence "f ∘ α ∈ monadP_qbs_MPx Y"
using assms(2) by(auto simp: qbs_prob_def in_Mx_def)
then obtain β g where hbg:
"β ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, β, g r))"
using rep_monadP_qbs_MPx by blast
show ?thesis
using qbs_prob.qbs_bind_computation[OF hs assms(2) hbg] qbs_prob.qbs_prob_space_qbs_computation
by simp
qed
subsubsection ‹ Properties of Integrals›
lemma qbs_integrable_return:
assumes "x ∈ qbs_space X"
and "f ∈ X →⇩Q ℝ⇩Q"
shows "qbs_integrable (qbs_return X x) f"
using assms(2) nn_integral_return[of x "qbs_to_measure X" "λx. ¦f x¦",simplified,OF assms(1)]
by(auto intro!: qbs_integrable_if_integrable integrableI_bounded
simp: qbs_prob_measure_return[OF assms(1)] )
lemma qbs_integrable_bind_return:
assumes "s ∈ monadP_qbs_Px Y"
"f ∈ Z →⇩Q ℝ⇩Q"
and "g ∈ Y →⇩Q Z"
shows "qbs_integrable (s ⤜ (λy. qbs_return Z (g y))) f = qbs_integrable s (f ∘ g)"
proof -
obtain α μ where hs:
"qbs_prob Y α μ" "s = qbs_prob_space (Y, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then interpret qp: qbs_prob Y α μ by simp
show ?thesis (is "?lhs = ?rhs")
proof -
have "qbs_return Z ∘ (g ∘ α) = (λr. qbs_prob_space (Z, g ∘ α, return real_borel r))"
by(rule qbs_return_comp) (use assms(3) qp.in_Mx in blast)
hence hb:"qbs_prob Z (g ∘ α) μ"
"s ⤜ (λy. qbs_return Z (g y)) = qbs_prob_space (Z, g ∘ α, μ)"
by(auto intro!: qbs_prob.qbs_bind_computation[OF hs qbs_morphism_comp[OF assms(3) qbs_return_morphism,simplified comp_def] qbs_morphismE(3)[OF assms(3) qp.in_Mx],of "return real_borel",simplified bind_return''[of μ real_borel,simplified]])
(simp_all add: comp_def)
have "?lhs = integrable μ (f ∘ (g ∘ α))"
using assms(2)
by(auto intro!: qbs_prob.qbs_integrable_iff_integrable[OF hb(1),simplified comp_def] simp: hb(2) comp_def)
also have "... = ?rhs"
using qbs_morphism_comp[OF assms(3,2)]
by(auto intro!: qbs_prob.qbs_integrable_iff_integrable[OF hs(1),symmetric] simp: hs(2) comp_def)
finally show ?thesis .
qed
qed
lemma qbs_prob_ennintegral_morphism:
assumes "L ∈ X →⇩Q monadP_qbs Y"
and "f ∈ X →⇩Q exp_qbs Y ℝ⇩Q⇩≥⇩0"
shows "(λx. qbs_prob_ennintegral (L x) (f x)) ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
proof(rule qbs_morphismI,simp_all)
fix α
assume h0:"α ∈ qbs_Mx X"
then obtain β g where h:
"β ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"(L ∘ α) = (λr. qbs_prob_space (Y, β, g r))"
using rep_monadP_qbs_MPx[of "L ∘ α" Y] qbs_morphismE(3)[OF assms(1)] by auto
note [measurable] = h(2)
have [measurable]: "(λ(r, y). f (α r) (β y)) ∈ real_borel ⨂⇩M real_borel →⇩M ennreal_borel"
proof -
have "(λ(r, y). f (α r) (β y)) = case_prod f ∘ map_prod α β"
by auto
also have "... ∈ ℝ⇩Q ⨂⇩Q ℝ⇩Q →⇩Q ℝ⇩Q⇩≥⇩0"
apply(rule qbs_morphism_comp[OF qbs_morphism_map_prod uncurry_preserves_morphisms[OF assms(2)]])
using h0 h(1) by(auto simp: qbs_Mx_is_morphisms)
finally show ?thesis
by auto
qed
have "(λx. qbs_prob_ennintegral (L x) (f x)) ∘ α = (λr. qbs_prob_ennintegral ((L ∘ α) r) ((f ∘ α) r))"
by auto
also have "... = (λr. (∫⇧+ x. (f ∘ α) r (β x) ∂(g r)))"
apply standard
using h0 by(auto intro!: qbs_prob.qbs_prob_ennintegral_def[OF qbs_prob_MPx[OF h(1,2)]] qbs_morphismE(2)[OF assms(2),simplified] simp: h(3))
also have "... ∈ real_borel →⇩M ennreal_borel"
using assms(2) h0 h(1)
by(auto intro!: nn_integral_measurable_subprob_algebra2[where N=real_borel] simp: measurable_prob_algebraD)
finally show "(λx. qbs_prob_ennintegral (L x) (f x)) ∘ α ∈ real_borel →⇩M ennreal_borel " .
qed
lemma qbs_morphism_ennintegral_fst:
assumes "q ∈ monadP_qbs_Px Y"
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(λx. ∫⇧+⇩Q y. f (x, y) ∂q) ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
by(rule qbs_prob_ennintegral_morphism[OF qbs_morphism_const[of _ "monadP_qbs Y",simplified,OF assms(1)] curry_preserves_morphisms[OF assms(2)],simplified curry_def])
lemma qbs_morphism_ennintegral_snd:
assumes "p ∈ monadP_qbs_Px X"
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(λy. ∫⇧+⇩Q x. f (x, y) ∂p) ∈ Y →⇩Q ℝ⇩Q⇩≥⇩0"
using qbs_morphism_ennintegral_fst[OF assms(1) qbs_morphism_pair_swap[OF assms(2)]]
by fastforce
lemma qbs_prob_ennintegral_morphism':
assumes "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(λs. qbs_prob_ennintegral s f) ∈ monadP_qbs X →⇩Q ℝ⇩Q⇩≥⇩0"
apply(rule qbs_prob_ennintegral_morphism[of _ _ X])
using qbs_morphism_ident[of "monadP_qbs X"]
apply (simp add: id_def)
using assms qbs_morphism_const[of f "exp_qbs X ℝ⇩Q⇩≥⇩0"]
by simp
lemma qbs_prob_ennintegral_return:
assumes "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
and "x ∈ qbs_space X"
shows "qbs_prob_ennintegral (qbs_return X x) f = f x"
using assms
by(auto intro!: nn_integral_return
simp: qbs_prob_ennintegral_def2[OF qbs_of_return[OF assms(2)] assms(1)] qbs_prob_measure_return[OF assms(2)])
lemma qbs_prob_ennintegral_bind:
assumes "s ∈ monadP_qbs_Px X"
"f ∈ X →⇩Q monadP_qbs Y"
and "g ∈ Y →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral (s ⤜ f) g = qbs_prob_ennintegral s (λy. (qbs_prob_ennintegral (f y) g))"
(is "?lhs = ?rhs")
proof -
obtain α μ where hs:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then interpret qp: qbs_prob X α μ by simp
obtain β h where hb:
"β ∈ qbs_Mx Y" "h ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, β, h r))"
using rep_monadP_qbs_MPx[OF qbs_morphismE(3)[OF assms(2) qp.in_Mx,simplified]]
by auto
hence h:"qbs_prob Y β (μ ⤜ h)"
"s ⤜ f = qbs_prob_space (Y, β, μ ⤜ h)"
using qp.qbs_bind_computation[OF hs(2) assms(2) hb] by auto
hence LHS:"?lhs = (∫⇧+ x. g (β x) ∂(μ ⤜ h))"
using qbs_prob.qbs_prob_ennintegral_def[OF h(1) assms(3)]
by simp
note [measurable] = hb(2)
have "⋀r. qbs_prob_ennintegral (f (α r)) g = (∫⇧+ y. g (β y) ∂(h r))"
using qbs_prob.qbs_prob_ennintegral_def[OF qbs_prob_MPx[OF hb(1,2)] assms(3)] hb(3)[simplified comp_def]
by metis
hence "?rhs = (∫⇧+ r. (∫⇧+ y. (g ∘ β) y ∂(h r)) ∂μ)"
by(auto intro!: nn_integral_cong
simp: qbs_prob.qbs_prob_ennintegral_def[OF hs(1) qbs_prob_ennintegral_morphism[OF assms(2) qbs_morphism_const[of _ "exp_qbs Y ℝ⇩Q⇩≥⇩0 ",simplified,OF assms(3)]]] hs(2))
also have "... = (integral⇧N (μ ⤜ h) (g ∘ β))"
apply(intro nn_integral_bind[symmetric,of _ real_borel])
using assms(3) hb(1)
by(auto intro!: measurable_prob_algebraD hb(2))
finally show ?thesis
using LHS by(simp add: comp_def)
qed
lemma qbs_prob_ennintegral_bind_return:
assumes "s ∈ monadP_qbs_Px Y"
"f ∈ Z →⇩Q ℝ⇩Q⇩≥⇩0"
and "g ∈ Y →⇩Q Z"
shows "qbs_prob_ennintegral (s ⤜ (λy. qbs_return Z (g y))) f = qbs_prob_ennintegral s (f ∘ g)"
apply(simp add: qbs_prob_ennintegral_bind[OF assms(1) qbs_return_morphism'[OF assms(3)] assms(2)])
using assms(1,3)
by(auto intro!: qbs_prob_ennintegral_cong qbs_prob_ennintegral_return[OF assms(2)]
simp: monadP_qbs_Px_def)
lemma qbs_prob_integral_morphism':
assumes "f ∈ X →⇩Q ℝ⇩Q"
shows "(λs. qbs_prob_integral s f) ∈ monadP_qbs X →⇩Q ℝ⇩Q"
proof(rule qbs_morphismI;simp)
fix α
assume "α ∈ monadP_qbs_MPx X"
then obtain β g where h:
"β ∈ qbs_Mx X" "g ∈ real_borel →⇩M prob_algebra real_borel"
"α = (λr. qbs_prob_space (X, β, g r))"
using rep_monadP_qbs_MPx[of α X] by auto
note [measurable] = h(2)
have [measurable]: "f ∘ β ∈ real_borel →⇩M real_borel"
using assms h(1) by auto
have "(λs. qbs_prob_integral s f) ∘ α = (λr. ∫ x. f (β x) ∂g r)"
apply standard
using assms qbs_prob_MPx[OF h(1,2)] by(auto intro!: qbs_prob.qbs_prob_integral_def simp: h(3))
also have "... = (λM. integral⇧L M (f ∘ β)) ∘ g"
by (simp add: comp_def)
also have "... ∈ real_borel →⇩M real_borel"
by(auto intro!: measurable_comp[where N="subprob_algebra real_borel"]
simp: integral_measurable_subprob_algebra measurable_prob_algebraD)
finally show "(λs. qbs_prob_integral s f) ∘ α ∈ real_borel →⇩M real_borel" .
qed
lemma qbs_morphism_integral_fst:
assumes "q ∈ monadP_qbs_Px Y"
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q"
shows "(λx. ∫⇩Q y. f (x, y) ∂q) ∈ X →⇩Q ℝ⇩Q"
proof(rule qbs_morphismI,simp_all)
fix α
assume ha:"α ∈ qbs_Mx X"
obtain β ν where hq:
"qbs_prob Y β ν" "q = qbs_prob_space (Y, β, ν)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then interpret qp: qbs_prob Y β ν by simp
have "(λx. ∫⇩Q y. f (x, y) ∂q) ∘ α = (λx. ∫ y. f (α x, β y) ∂ν)"
apply standard
using qbs_morphism_Pair1'[OF qbs_Mx_to_X(2)[OF ha] assms(2)]
by(auto intro!: qp.qbs_prob_integral_def
simp: hq(2))
also have "... ∈ borel_measurable borel"
using qbs_morphism_comp[OF qbs_morphism_map_prod assms(2),of α "ℝ⇩Q" β "ℝ⇩Q",simplified comp_def map_prod_def split_beta'] ha qp.in_Mx
by(auto intro!: qp.borel_measurable_lebesgue_integral
simp: qbs_Mx_is_morphisms)
finally show "(λx. ∫⇩Q y. f (x, y) ∂q) ∘ α ∈ borel_measurable borel" .
qed
lemma qbs_morphism_integral_snd:
assumes "p ∈ monadP_qbs_Px X"
and "f ∈ X ⨂⇩Q Y →⇩Q ℝ⇩Q"
shows "(λy. ∫⇩Q x. f (x, y) ∂p) ∈ Y →⇩Q ℝ⇩Q"
using qbs_morphism_integral_fst[OF assms(1) qbs_morphism_pair_swap[OF assms(2)]]
by simp
lemma qbs_prob_integral_morphism:
assumes "L ∈ X →⇩Q monadP_qbs Y"
"f ∈ X →⇩Q exp_qbs Y ℝ⇩Q"
and "⋀x. x ∈ qbs_space X ⟹ qbs_integrable (L x) (f x)"
shows "(λx. qbs_prob_integral (L x) (f x)) ∈ X →⇩Q ℝ⇩Q"
proof(rule qbs_morphismI;simp)
fix α
assume h0:"α ∈ qbs_Mx X"
then obtain β g where h:
"β ∈ qbs_Mx Y" "g ∈ real_borel →⇩M prob_algebra real_borel"
"(L ∘ α) = (λr. qbs_prob_space (Y, β, g r))"
using rep_monadP_qbs_MPx[of "L ∘ α" Y] qbs_morphismE(3)[OF assms(1)] by auto
have "(λx. qbs_prob_integral (L x) (f x)) ∘ α = (λr. qbs_prob_integral ((L ∘ α) r) ((f ∘ α) r))"
by auto
also have "... = (λr. enn2real (qbs_prob_ennintegral ((L ∘ α) r) (λx. ennreal ((f ∘ α) r x)))
- enn2real (qbs_prob_ennintegral ((L ∘ α) r) (λx. ennreal (- (f ∘ α) r x))))"
using h0 assms(3) by(auto intro!: real_qbs_prob_integral_def)
also have "... ∈ real_borel →⇩M real_borel"
proof -
have h2:"L ∘ α ∈ ℝ⇩Q →⇩Q monadP_qbs Y"
using qbs_morphismE(3)[OF assms(1) h0] by(auto simp: qbs_Mx_is_morphisms)
have [measurable]:"(λx. f (fst x) (snd x)) ∈ qbs_to_measure (X ⨂⇩Q Y) →⇩M real_borel"
using uncurry_preserves_morphisms[OF assms(2)] by(auto simp: split_beta')
have h3:"(λr x. ennreal ((f ∘ α) r x)) ∈ ℝ⇩Q →⇩Q exp_qbs Y ℝ⇩Q⇩≥⇩0"
proof(auto intro!: curry_preserves_morphisms[of "(λ(r,x). ennreal ((f ∘ α) r x))",simplified curry_def,simplified])
have "(λ(r, y). ennreal (f (α r) y)) = ennreal ∘ case_prod f ∘ map_prod α id"
by auto
also have "... ∈ ℝ⇩Q ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
apply(rule qbs_morphism_comp[where Y="X ⨂⇩Q Y"])
using h0 qbs_morphism_map_prod[OF _ qbs_morphism_ident,of α "ℝ⇩Q" X Y]
by(auto simp: qbs_Mx_is_morphisms)
finally show "(λ(r, y). ennreal (f (α r) y)) ∈ qbs_to_measure (ℝ⇩Q ⨂⇩Q Y) →⇩M ennreal_borel"
by auto
qed
have h4:"(λr x. ennreal (- (f ∘ α) r x)) ∈ ℝ⇩Q →⇩Q exp_qbs Y ℝ⇩Q⇩≥⇩0"
proof(auto intro!: curry_preserves_morphisms[of "(λ(r,x). ennreal (- (f ∘ α) r x))",simplified curry_def,simplified])
have "(λ(r, y). ennreal (- f (α r) y)) = ennreal ∘ (λr. - r) ∘ case_prod f ∘ map_prod α id"
by auto
also have "... ∈ ℝ⇩Q ⨂⇩Q Y →⇩Q ℝ⇩Q⇩≥⇩0"
apply(rule qbs_morphism_comp[where Y="X ⨂⇩Q Y"])
using h0 qbs_morphism_map_prod[OF _ qbs_morphism_ident,of α "ℝ⇩Q" X Y]
by(auto simp: qbs_Mx_is_morphisms)
finally show "(λ(r, y). ennreal (- f (α r) y)) ∈ qbs_to_measure (ℝ⇩Q ⨂⇩Q Y) →⇩M ennreal_borel"
by auto
qed
have "(λr. qbs_prob_ennintegral ((L ∘ α) r) (λx. ennreal ((f ∘ α) r x))) ∈ real_borel →⇩M ennreal_borel"
"(λr. qbs_prob_ennintegral ((L ∘ α) r) (λx. ennreal (- (f ∘ α) r x))) ∈ real_borel →⇩M ennreal_borel"
using qbs_prob_ennintegral_morphism[OF h2 h3] qbs_prob_ennintegral_morphism[OF h2 h4]
by auto
thus ?thesis by simp
qed
finally show "(λx. qbs_prob_integral (L x) (f x)) ∘ α ∈ real_borel →⇩M real_borel" .
qed
lemma qbs_prob_integral_morphism'':
assumes "f ∈ X →⇩Q ℝ⇩Q"
and "L ∈ Y →⇩Q monadP_qbs X"
shows "(λy. qbs_prob_integral (L y) f) ∈ Y →⇩Q ℝ⇩Q"
using qbs_morphism_comp[OF assms(2) qbs_prob_integral_morphism'[OF assms(1)]]
by(simp add: comp_def)
lemma qbs_prob_integral_return:
assumes "f ∈ X →⇩Q ℝ⇩Q"
and "x ∈ qbs_space X"
shows "qbs_prob_integral (qbs_return X x) f = f x"
using assms
by(auto intro!: integral_return
simp add: qbs_prob_integral_def2 qbs_prob_measure_return[OF assms(2)])
lemma qbs_prob_integral_bind:
assumes "s ∈ monadP_qbs_Px X"
"f ∈ X →⇩Q monadP_qbs Y"
"g ∈ Y →⇩Q ℝ⇩Q"
and "∃K. ∀y ∈ qbs_space Y.¦g y¦ ≤ K"
shows "qbs_prob_integral (s ⤜ f) g = qbs_prob_integral s (λy. (qbs_prob_integral (f y) g))"
(is "?lhs = ?rhs")
proof -
obtain K where hK:
"⋀y. y ∈ qbs_space Y ⟹ ¦g y¦ ≤ K"
using assms(4) by auto
obtain α μ where hs:
"qbs_prob X α μ" "s = qbs_prob_space (X, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then obtain β h where hb:
"β ∈ qbs_Mx Y" "h ∈ real_borel →⇩M prob_algebra real_borel"
"(f ∘ α) = (λr. qbs_prob_space (Y, β, h r))"
using rep_monadP_qbs_MPx[of "f ∘ α" Y] qbs_morphismE(3)[OF assms(2)]
by(auto simp add: qbs_prob_def in_Mx_def)
note [measurable] = hb(2)
interpret rd: real_distribution μ by(simp add: hs(1)[simplified qbs_prob_def])
have h:"qbs_prob Y β (μ ⤜ h)"
"s ⤜ f = qbs_prob_space (Y, β, μ ⤜ h)"
using qbs_prob.qbs_bind_computation[OF hs assms(2) hb] by auto
hence "?lhs = (∫ x. g (β x) ∂(μ ⤜ h))"
by(simp add: qbs_prob.qbs_prob_integral_def[OF h(1) assms(3)])
also have "... = (integral⇧L (μ ⤜ h) (g ∘ β))" by(simp add: comp_def)
also have "... = (∫ r. (∫ y. (g ∘ β) y ∂(h r)) ∂μ)"
apply(rule integral_bind[of _ real_borel K _ _ 1])
using assms(3) hb(1) hK measurable_space[OF hb(2)]
by(auto intro!: measurable_prob_algebraD
simp: space_prob_algebra prob_space.emeasure_le_1)
also have "... = ?rhs"
by(auto intro!: Bochner_Integration.integral_cong
simp: qbs_prob.qbs_prob_integral_def[OF qbs_prob_MPx[OF hb(1,2)] assms(3)] fun_cong[OF hb(3),simplified comp_def] hs(2) qbs_prob.qbs_prob_integral_def[OF hs(1) qbs_prob_integral_morphism''[OF assms(3,2)]])
finally show ?thesis .
qed
lemma qbs_prob_integral_bind_return:
assumes "s ∈ monadP_qbs_Px Y"
"f ∈ Z →⇩Q ℝ⇩Q"
and "g ∈ Y →⇩Q Z"
shows "qbs_prob_integral (s ⤜ (λy. qbs_return Z (g y))) f = qbs_prob_integral s (f ∘ g)"
proof -
obtain α μ where hs:
"qbs_prob Y α μ" "s = qbs_prob_space (Y, α, μ)"
using rep_monadP_qbs_Px[OF assms(1)] by auto
then interpret qp: qbs_prob Y α μ by simp
have hb:"qbs_prob Z (g ∘ α) μ"
"s ⤜ (λy. qbs_return Z (g y)) = qbs_prob_space (Z, g ∘ α, μ)"
by(auto intro!: qp.qbs_bind_computation[OF hs(2) qbs_return_morphism'[OF assms(3)] qbs_morphismE(3)[OF assms(3) qp.in_Mx],of "return real_borel",simplified bind_return''[of μ real_borel,simplified] comp_def]
simp: comp_def qbs_return_comp[OF qbs_morphismE(3)[OF assms(3) qp.in_Mx],simplified comp_def])
thus ?thesis
by(simp add: hb(2) qbs_prob.qbs_prob_integral_def[OF hb(1) assms(2)] hs(2) qbs_prob.qbs_prob_integral_def[OF hs(1) qbs_morphism_comp[OF assms(3,2)]])
qed
lemma qbs_prob_var_bind_return:
assumes "s ∈ monadP_qbs_Px Y"
"f ∈ Z →⇩Q ℝ⇩Q"
and "g ∈ Y →⇩Q Z"
shows "qbs_prob_var (s ⤜ (λy. qbs_return Z (g y))) f = qbs_prob_var s (f ∘ g)"
proof -
have 1:"(λx. (f x - qbs_prob_integral s (f ∘ g))⇧2) ∈ Z →⇩Q ℝ⇩Q"
using assms(2,3) by auto
thus ?thesis
using qbs_prob_integral_bind_return[OF assms(1) 1 assms(3)] qbs_prob_integral_bind_return[OF assms]
by(simp add: comp_def qbs_prob_var_def)
qed
end