Theory Monad_QuasiBorel
section ‹The S-Finite Measure Monad›
theory Monad_QuasiBorel
imports
"Measure_QuasiBorel_Adjunction"
"Kernels"
begin
subsection ‹ The S-Finite Measure Monad›
subsubsection ‹ Space of S-Finite Measures›
locale in_Mx =
fixes X :: "'a quasi_borel"
and α :: "real ⇒ 'a"
assumes in_Mx[simp]:"α ∈ qbs_Mx X"
begin
lemma α_measurable[measurable]: "α ∈ borel →⇩M qbs_to_measure X"
using in_Mx qbs_Mx_subset_of_measurable by blast
lemma α_qbs_morphism[qbs]: "α ∈ qbs_borel →⇩Q X"
using in_Mx by(simp only: qbs_Mx_is_morphisms)
lemma X_not_empty: "qbs_space X ≠ {}"
using in_Mx by(auto simp: qbs_empty_equiv simp del: in_Mx)
lemma inverse_UNIV[simp]: "α -` (qbs_space X) = UNIV"
by fastforce
end
locale qbs_s_finite = in_Mx X α + s_finite_measure μ
for X :: "'a quasi_borel" and α and μ :: "real measure" +
assumes mu_sets[measurable_cong]: "sets μ = sets borel"
begin
lemma mu_not_empty: "space μ ≠ {}"
by(simp add: sets_eq_imp_space_eq[OF mu_sets])
end
lemma qbs_s_finite_All:
assumes "α ∈ qbs_Mx X" "s_finite_kernel M borel k" "x ∈ space M"
shows "qbs_s_finite X α (k x)"
proof -
interpret s_finite_kernel M borel k by fact
show ?thesis
using assms(1,3) image_s_finite_measure[OF assms(3)] by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def kernel_sets)
qed
locale qbs_prob = in_Mx X α + real_distribution μ
for X :: "'a quasi_borel" and α μ
begin
lemma qbs_s_finite: "qbs_s_finite X α μ"
by(auto simp: qbs_s_finite_def qbs_s_finite_axioms_def in_Mx_def s_finite_measure_prob)
sublocale qbs_s_finite by(rule qbs_s_finite)
end
lemma(in qbs_s_finite) qbs_probI: "prob_space μ ⟹ qbs_prob X α μ"
by(auto simp: qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def mu_sets)
locale pair_qbs_s_finites = pq1: qbs_s_finite X α μ + pq2: qbs_s_finite Y β ν
for X :: "'a quasi_borel" and α μ and Y :: "'b quasi_borel" and β ν
begin
lemma ab_measurable[measurable]: "map_prod α β ∈ borel ⨂⇩M borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
proof -
have "map_prod α β ∈ qbs_to_measure (measure_to_qbs (borel ⨂⇩M borel)) →⇩M qbs_to_measure (X ⨂⇩Q Y)"
by(auto intro!: set_mp[OF l_preserves_morphisms] simp: r_preserves_product)
moreover have "sets (qbs_to_measure (measure_to_qbs (borel ⨂⇩M borel))) = sets ((borel ⨂⇩M borel) :: (real × real) measure)"
by(auto intro!: standard_borel.lr_sets_ident pair_standard_borel_ne standard_borel_ne.standard_borel)
ultimately show ?thesis by simp
qed
end
locale pair_qbs_probs = pq1: qbs_prob X α μ + pq2: qbs_prob Y β ν
for X :: "'a quasi_borel" and α μ and Y :: "'b quasi_borel" and β ν
begin
sublocale pair_qbs_s_finites
by standard
end
locale pair_qbs_s_finite = pq1: qbs_s_finite X α μ + pq2: qbs_s_finite X β ν
for X :: "'a quasi_borel" and α μ and β ν
begin
sublocale pair_qbs_s_finites X α μ X β ν
by standard
end
locale pair_qbs_prob = pq1: qbs_prob X α μ + pq2: qbs_prob X β ν
for X :: "'a quasi_borel" and α μ and β ν
begin
sublocale pair_qbs_s_finite X α μ β ν
by standard
sublocale pair_qbs_probs X α μ X β μ
by standard
end
type_synonym 'a qbs_s_finite_t = "'a quasi_borel * (real ⇒ 'a) * real measure"
definition qbs_s_finite_eq :: "['a qbs_s_finite_t, 'a qbs_s_finite_t] ⇒ bool" where
"qbs_s_finite_eq p1 p2 ≡
(let (X, α, μ) = p1;
(Y, β, ν) = p2 in
qbs_s_finite X α μ ∧ qbs_s_finite Y β ν ∧ X = Y ∧
distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure Y) β)"
definition qbs_s_finite_eq' :: "['a qbs_s_finite_t, 'a qbs_s_finite_t] ⇒ bool" where
"qbs_s_finite_eq' p1 p2 ≡
(let (X, α, μ) = p1;
(Y, β, ν) = p2 in
qbs_s_finite X α μ ∧ qbs_s_finite Y β ν ∧ X = Y ∧
(∀f∈X →⇩Q (qbs_borel :: ennreal quasi_borel). (∫⇧+x. f (α x) ∂μ) = (∫⇧+x. f (β x) ∂ν)))"
lemma(in qbs_s_finite)
shows qbs_s_finite_eq_refl[simp]: "qbs_s_finite_eq (X,α,μ) (X,α,μ)"
and qbs_s_finite_eq'_refl[simp]: "qbs_s_finite_eq' (X,α,μ) (X,α,μ)"
by(simp_all add: qbs_s_finite_eq_def qbs_s_finite_eq'_def qbs_s_finite_axioms)
lemma(in pair_qbs_s_finite)
shows qbs_s_finite_eq_intro: "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β ⟹ qbs_s_finite_eq (X,α,μ) (X,β,ν)"
and qbs_s_finite_eq'_intro: "(⋀f. f ∈ X →⇩Q qbs_borel ⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)) ⟹ qbs_s_finite_eq' (X,α,μ) (X,β,ν)"
by(simp_all add: qbs_s_finite_eq_def qbs_s_finite_eq'_def pq1.qbs_s_finite_axioms pq2.qbs_s_finite_axioms)
lemma qbs_s_finite_eq_dest:
assumes "qbs_s_finite_eq (X,α,μ) (Y,β,ν)"
shows "qbs_s_finite X α μ" "qbs_s_finite Y β ν" "Y = X" "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
using assms by(auto simp: qbs_s_finite_eq_def)
lemma qbs_s_finite_eq'_dest:
assumes "qbs_s_finite_eq' (X,α,μ) (Y,β,ν)"
shows "qbs_s_finite X α μ" "qbs_s_finite Y β ν" "Y = X" "⋀f. f ∈ X →⇩Q qbs_borel ⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)"
using assms by(auto simp: qbs_s_finite_eq'_def)
lemma(in qbs_prob) qbs_s_finite_eq_qbs_prob_cong:
assumes "qbs_s_finite_eq (X,α,μ) (Y,β,ν)"
shows "qbs_prob Y β ν"
proof -
interpret qs: pair_qbs_s_finites X α μ Y β ν
using assms(1) by(auto simp: qbs_s_finite_eq_def pair_qbs_s_finites_def)
show ?thesis
by(auto intro!: qs.pq2.qbs_probI prob_space_distrD[of β _ "qbs_to_measure Y"]) (auto simp: qbs_s_finite_eq_dest(3)[OF assms] qbs_s_finite_eq_dest(4)[OF assms,symmetric] intro!: prob_space_distr)
qed
lemma
shows qbs_s_finite_eq_symp: "symp qbs_s_finite_eq"
and qbs_s_finite_eq_transp: "transp qbs_s_finite_eq"
by(simp_all add: qbs_s_finite_eq_def transp_def symp_def)
quotient_type 'a qbs_measure = "'a qbs_s_finite_t" / partial: qbs_s_finite_eq
morphisms rep_qbs_measure qbs_measure
proof(rule part_equivpI)
let ?U = "UNIV :: 'a set"
let ?Uf = "UNIV :: (real ⇒ 'a) set"
let ?f = "(λ_. undefined) :: real ⇒ 'a"
have "qbs_s_finite (Abs_quasi_borel (?U, ?Uf)) ?f (return borel 0)"
unfolding qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def
proof safe
have "Rep_quasi_borel (Abs_quasi_borel (?U,?Uf)) = (?U, ?Uf)"
using Abs_quasi_borel_inverse by (auto simp add: qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)
thus "(λ_. undefined) ∈ qbs_Mx (Abs_quasi_borel (?U, ?Uf))"
by(simp add: qbs_Mx_def)
next
show "s_finite_measure (return borel 0)"
by(auto intro!: sigma_finite_measure.s_finite_measure prob_space_imp_sigma_finite prob_space_return)
qed simp_all
thus "∃x :: 'a qbs_s_finite_t. qbs_s_finite_eq x x"
by(auto simp: qbs_s_finite_eq_def intro!: exI[where x="(Abs_quasi_borel (?U,?Uf), ?f, return borel 0)"])
qed(simp_all add: qbs_s_finite_eq_symp qbs_s_finite_eq_transp)
interpretation qbs_measure : quot_type "qbs_s_finite_eq" "Abs_qbs_measure" "Rep_qbs_measure"
using Abs_qbs_measure_inverse Rep_qbs_measure
by(simp add: quot_type_def equivp_implies_part_equivp qbs_measure_equivp Rep_qbs_measure_inverse Rep_qbs_measure_inject) blast
syntax
"_qbs_measure" :: "'a quasi_borel ⇒ (real ⇒ 'a) ⇒ real measure ⇒ 'a qbs_measure" ("⟦_,/ _,/ _⟧⇩s⇩f⇩i⇩n")
translations
"⟦X, α, μ⟧⇩s⇩f⇩i⇩n" ⇌ "CONST qbs_measure (X, α, μ)"
lemma rep_qbs_s_finite_measure': "∃X α μ. p = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n ∧ qbs_s_finite X α μ"
by(rule qbs_measure.abs_induct,auto simp add: qbs_s_finite_eq_def)
lemma rep_qbs_s_finite_measure:
obtains X α μ where "p = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ"
using that rep_qbs_s_finite_measure' by blast
definition qbs_null_measure :: "'a quasi_borel ⇒ 'a qbs_measure" where
"qbs_null_measure X ≡ ⟦X, SOME a. a ∈ qbs_Mx X, null_measure borel⟧⇩s⇩f⇩i⇩n"
lemma qbs_null_measure_s_finite: "qbs_space X ≠ {} ⟹ qbs_s_finite X (SOME a. a ∈ qbs_Mx X) (null_measure borel)"
by(auto simp: qbs_empty_equiv qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def some_in_eq intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
lemma(in qbs_s_finite) in_Rep_qbs_measure':
assumes "qbs_s_finite_eq (X,α,μ) (X',α',μ')"
shows "(X',α',μ') ∈ Rep_qbs_measure ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
by (metis assms mem_Collect_eq qbs_s_finite_eq_refl qbs_measure_def qbs_measure.abs_def qbs_measure.abs_inverse)
lemmas(in qbs_s_finite) in_Rep_qbs_measure = in_Rep_qbs_measure'[OF qbs_s_finite_eq_refl]
lemma(in qbs_s_finite) if_in_Rep_qbs_measure:
assumes "(X',α',μ') ∈ Rep_qbs_measure ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
shows "X' = X"
"qbs_s_finite X' α' μ'"
"qbs_s_finite_eq (X,α,μ) (X',α',μ')"
proof -
show h:"X' = X"
using assms qbs_measure.Rep_qbs_measure[of "⟦X, α, μ⟧⇩s⇩f⇩i⇩n"]
by auto (metis mem_Collect_eq qbs_s_finite_eq_dest(3) qbs_s_finite_eq_refl qbs_measure_def qbs_measure.abs_def qbs_measure.abs_inverse)
next
show "qbs_s_finite X' α' μ'"
using assms qbs_measure.Rep_qbs_measure[of "⟦X, α, μ⟧⇩s⇩f⇩i⇩n"]
by (auto simp: qbs_s_finite_eq_dest(2))
next
show "qbs_s_finite_eq (X,α,μ) (X',α',μ')"
using assms qbs_measure.Rep_qbs_measure[of "⟦X, α, μ⟧⇩s⇩f⇩i⇩n"]
by auto (metis mem_Collect_eq qbs_s_finite_eq_dest(3) qbs_s_finite_eq_refl qbs_measure_def qbs_measure.abs_def qbs_measure.abs_inverse)
qed
lemma qbs_s_finite_eq_1_imp_2:
assumes "qbs_s_finite_eq (X,α,μ) (Y,β,ν)" "f ∈ X →⇩Q (qbs_borel :: (_ :: {banach}) quasi_borel)"
shows "(∫x. f (α x) ∂μ) = (∫x. f (β x) ∂ν)" (is "?lhs = ?rhs")
proof -
interpret pq : pair_qbs_s_finite X α μ β ν
using assms by(auto intro!: pair_qbs_s_finite.intro simp: qbs_s_finite_eq_def)
have [measurable]: "f ∈ qbs_to_measure X →⇩M borel"
using assms by(simp add: lr_adjunction_correspondence)
have "?lhs = (∫x. f x ∂(distr μ (qbs_to_measure X) α))"
by(simp add: integral_distr)
also have "... = (∫x. f x ∂(distr ν (qbs_to_measure X) β))"
by(simp add: qbs_s_finite_eq_dest(4)[OF assms(1)])
also have "... = ?rhs"
by(simp add: integral_distr)
finally show ?thesis .
qed
lemma qbs_s_finite_eq_equiv: "qbs_s_finite_eq = qbs_s_finite_eq'"
proof(rule ext[OF ext])
show "⋀a b :: 'a qbs_s_finite_t. qbs_s_finite_eq a b = qbs_s_finite_eq' a b"
proof safe
fix X Y :: "'a quasi_borel" and α β μ ν
{
assume h:"qbs_s_finite_eq (X,α,μ) (Y,β,ν)"
then interpret pq : pair_qbs_s_finite X α μ β ν
by(auto intro!: pair_qbs_s_finite.intro simp: qbs_s_finite_eq_def)
show "qbs_s_finite_eq' (X,α,μ) (Y,β,ν)"
unfolding qbs_s_finite_eq_dest(3)[OF h]
proof(rule pq.qbs_s_finite_eq'_intro)
fix f :: "'a ⇒ ennreal"
assume f:"f ∈ X →⇩Q qbs_borel"
show "(∫⇧+ x. f (α x) ∂μ) = (∫⇧+ x. f (β x) ∂ν)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. f x ∂(distr μ (qbs_to_measure X) α))"
by(rule nn_integral_distr[symmetric]) (use f lr_adjunction_correspondence in auto)
also have "... = (∫⇧+ x. f x ∂(distr ν (qbs_to_measure X) β))"
by(simp add: qbs_s_finite_eq_dest(4)[OF h])
also have "... = ?rhs"
by(rule nn_integral_distr) (use f lr_adjunction_correspondence in auto)
finally show ?thesis .
qed
qed
}
{
assume h:"qbs_s_finite_eq' (X,α,μ) (Y,β,ν)"
then interpret pq : pair_qbs_s_finite X α μ β ν
by(auto intro!: pair_qbs_s_finite.intro simp: qbs_s_finite_eq'_def)
show "qbs_s_finite_eq (X,α,μ) (Y,β,ν)"
unfolding qbs_s_finite_eq'_dest(3)[OF h]
proof(rule pq.qbs_s_finite_eq_intro[OF measure_eqI])
fix U
assume hu[measurable]:"U ∈ sets (distr μ (qbs_to_measure X) α)"
show "emeasure (distr μ (qbs_to_measure X) α) U = emeasure (distr ν (qbs_to_measure X) β) U"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. indicator U x ∂ (distr μ (qbs_to_measure X) α))"
using hu by simp
also have "... = (∫⇧+ x. indicator U (α x) ∂μ)"
by(rule nn_integral_distr) (use hu in auto)
also have "... = (∫⇧+ x. indicator U (β x) ∂ν)"
by(auto intro!: qbs_s_finite_eq'_dest(4)[OF h] simp: lr_adjunction_correspondence)
also have "... = (∫⇧+ x. indicator U x ∂ (distr ν (qbs_to_measure X) β))"
by(rule nn_integral_distr[symmetric]) (use hu in auto)
also have "... = ?rhs"
using hu by simp
finally show ?thesis .
qed
qed simp
}
qed
qed
lemma qbs_s_finite_measure_eq: "qbs_s_finite_eq (X,α,μ) (Y,β,ν) ⟹ ⟦X, α, μ⟧⇩s⇩f⇩i⇩n = ⟦Y, β, ν⟧⇩s⇩f⇩i⇩n"
using Quotient3_rel[OF Quotient3_qbs_measure] by blast
lemma(in pair_qbs_s_finite) qbs_s_finite_measure_eq:
"distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β ⟹ ⟦X, α, μ⟧⇩s⇩f⇩i⇩n = ⟦X, β, ν⟧⇩s⇩f⇩i⇩n"
by(auto intro!: qbs_s_finite_measure_eq qbs_s_finite_eq_intro)
lemma(in pair_qbs_s_finite) qbs_s_finite_measure_eq':
"(⋀f. f ∈ X →⇩Q qbs_borel ⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)) ⟹ ⟦X, α, μ⟧⇩s⇩f⇩i⇩n = ⟦X, β, ν⟧⇩s⇩f⇩i⇩n"
using qbs_s_finite_eq'_intro[simplified qbs_s_finite_eq_equiv[symmetric]] by(auto intro!: qbs_s_finite_measure_eq simp: qbs_s_finite_eq_def)
lemma(in pair_qbs_s_finite) qbs_s_finite_measure_eq_inverse:
assumes "⟦X, α, μ⟧⇩s⇩f⇩i⇩n = ⟦X, β, ν⟧⇩s⇩f⇩i⇩n"
shows "qbs_s_finite_eq (X,α,μ) (X,β,ν)" "qbs_s_finite_eq' (X,α,μ) (X,β,ν)"
using Quotient3_rel[OF Quotient3_qbs_measure,of "(X,α,μ)" "(X,β,ν)",simplified]
by(simp_all add: assms qbs_s_finite_eq_equiv)
lift_definition qbs_space_of :: "'a qbs_measure ⇒ 'a quasi_borel"
is fst by(auto simp: qbs_s_finite_eq_def)
lemma(in qbs_s_finite) qbs_space_of[simp]:
"qbs_space_of ⟦X, α, μ⟧⇩s⇩f⇩i⇩n = X" by(simp add: qbs_space_of.abs_eq)
lemma rep_qbs_space_of:
assumes "qbs_space_of s = X"
shows "∃α μ. s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n ∧ qbs_s_finite X α μ"
proof -
obtain X' α μ where hs:
"s = ⟦X', α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X' α μ"
using rep_qbs_s_finite_measure'[of s] by auto
then interpret qs:qbs_s_finite X' α μ
by simp
show ?thesis
using assms hs(2) by(auto simp add: hs(1))
qed
corollary qbs_s_space_of_not_empty: "qbs_space (qbs_space_of X) ≠ {}"
by transfer (auto simp: qbs_s_finite_eq_def qbs_s_finite_def in_Mx_def qbs_empty_equiv)
subsubsection ‹ The S-Finite Measure Monad›
definition monadM_qbs :: "'a quasi_borel ⇒ 'a qbs_measure quasi_borel" where
"monadM_qbs X ≡ Abs_quasi_borel ({s. qbs_space_of s = X}, {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k})"
lemma
shows monadM_qbs_space: "qbs_space (monadM_qbs X) = {s. qbs_space_of s = X}"
and monadM_qbs_Mx: "qbs_Mx (monadM_qbs X) = {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
proof -
have "{λr::real. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k} ⊆ UNIV → {s. qbs_space_of s = X}"
proof safe
fix x α and k :: "real ⇒ real measure"
assume h:"α ∈ qbs_Mx X" "s_finite_kernel borel borel k"
interpret k:s_finite_kernel borel borel k by fact
interpret qbs_s_finite X α "k x"
using k.image_s_finite_measure h(1) by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def k.kernel_sets)
show "qbs_space_of ⟦X, α, k x⟧⇩s⇩f⇩i⇩n = X"
by simp
qed
moreover have "qbs_closed1 {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
proof(safe intro!: qbs_closed1I)
fix α and f :: "real ⇒ real" and k :: "real⇒ real measure"
assume h:"f ∈ borel_measurable borel" "α ∈ qbs_Mx X" "s_finite_kernel borel borel k"
then show "∃α' ka. (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n) ∘ f = (λr. ⟦X, α', ka r⟧⇩s⇩f⇩i⇩n) ∧ α' ∈ qbs_Mx X ∧ s_finite_kernel borel borel ka"
by(auto intro!: exI[where x=α] exI[where x="λx. k (f x)"] simp: s_finite_kernel.comp_measurable[OF h(3,1)])
qed
moreover have "qbs_closed2 {s. qbs_space_of s = X} {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
proof(safe intro!: qbs_closed2I)
fix s
assume h:"X = qbs_space_of s"
from rep_qbs_space_of[OF this[symmetric]] obtain α μ where s:"s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ"
by auto
then interpret qbs_s_finite X α μ by simp
show "∃α k. (λr. s) = (λr. ⟦qbs_space_of s, α, k r⟧⇩s⇩f⇩i⇩n) ∧ α ∈ qbs_Mx (qbs_space_of s) ∧ s_finite_kernel borel borel k"
by(auto intro!: exI[where x=α] exI[where x="λr. μ"] s_finite_kernel_const simp: s(1) s_finite_kernel_cong_sets[OF _ mu_sets[symmetric]] sets_eq_imp_space_eq[OF mu_sets])
qed
moreover have "qbs_closed3 {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
proof(safe intro!: qbs_closed3I)
fix P :: "real ⇒ nat" and Fi :: "nat ⇒ _"
assume P[measurable]: "P ∈ borel →⇩M count_space UNIV"
and "∀i. Fi i ∈ {λr::real. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
then obtain αi ki where Fi: "⋀i. Fi i = (λr. ⟦X, αi i, ki i r⟧⇩s⇩f⇩i⇩n)" "⋀i. αi i ∈ qbs_Mx X" "⋀i. s_finite_kernel borel borel (ki i)"
by auto metis
interpret nat_real: standard_borel_ne "count_space (UNIV :: nat set) ⨂⇩M (borel :: real measure)"
by(auto intro!: pair_standard_borel_ne)
note [simp] = nat_real.from_real_to_real[simplified space_pair_measure, simplified]
define α where "α ≡ (λr. case_prod αi (nat_real.from_real r))"
define k where "k ≡ (λr. distr (distr (ki (P r) r) (count_space UNIV ⨂⇩M borel) (λr'. (P r, r'))) borel nat_real.to_real)"
have α: "α ∈ qbs_Mx X"
unfolding α_def qbs_Mx_is_morphisms
proof(rule qbs_morphism_compose[where g=nat_real.from_real and Y="qbs_count_space UNIV ⨂⇩Q qbs_borel"])
show "nat_real.from_real ∈ qbs_borel →⇩Q qbs_count_space UNIV ⨂⇩Q qbs_borel"
by(simp add: r_preserves_product[symmetric] standard_borel.standard_borel_r_full_faithful[of "borel :: real measure",simplified,symmetric] standard_borel_ne.standard_borel)
next
show "case_prod αi ∈ qbs_count_space UNIV ⨂⇩Q qbs_borel →⇩Q X"
using Fi(2) by(auto intro!: qbs_morphism_pair_count_space1 simp: qbs_Mx_is_morphisms)
qed
have sets_ki[measurable_cong]: "sets (ki i r) = sets borel" "sets (k r) = sets borel" for i r
using Fi(3) by(auto simp: s_finite_kernel_def measure_kernel_def k_def)
interpret k:s_finite_kernel borel borel k
proof -
have 1:"k = (λ(i,r). distr (ki i r) borel (λr'. nat_real.to_real (i, r'))) ∘ (λr. (P r, r))"
by standard (auto simp: k_def distr_distr comp_def)
have "s_finite_kernel borel borel ..."
unfolding comp_def
by(rule s_finite_kernel.comp_measurable[where X="count_space UNIV ⨂⇩M borel"],rule s_finite_kernel_pair_countble1, auto intro!: s_finite_kernel.distr_s_finite_kernel[OF Fi(3)])
thus "s_finite_kernel borel borel k" by(simp add: 1)
qed
have "(λr. Fi (P r) r) = (λr. ⟦X, α, k r ⟧⇩s⇩f⇩i⇩n)"
unfolding Fi(1)
proof
fix r
interpret pq:pair_qbs_s_finite X "αi (P r)" "ki (P r) r" α "k r"
by(auto simp: pair_qbs_s_finite_def qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def k.image_s_finite_measure s_finite_kernel.image_s_finite_measure[OF Fi(3)] sets_ki α Fi(2))
show "⟦X, αi (P r), ki (P r) r⟧⇩s⇩f⇩i⇩n = ⟦X, α, k r⟧⇩s⇩f⇩i⇩n"
by(rule pq.qbs_s_finite_measure_eq, simp add: k_def distr_distr comp_def,simp add: α_def)
qed
thus "∃α k. (λr. Fi (P r) r) = (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n) ∧ α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k"
by(auto intro!: exI[where x=α] exI[where x=k] simp: α k.s_finite_kernel_axioms)
qed
ultimately have "Rep_quasi_borel (monadM_qbs X) = ({s. qbs_space_of s = X}, {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k})"
by(auto intro!: Abs_quasi_borel_inverse simp: monadM_qbs_def is_quasi_borel_def)
thus "qbs_space (monadM_qbs X) = {s. qbs_space_of s = X}" "qbs_Mx (monadM_qbs X) = {λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n |α k. α ∈ qbs_Mx X ∧ s_finite_kernel borel borel k}"
by(simp_all add: qbs_space_def qbs_Mx_def)
qed
lemma monadM_qbs_empty_iff: "qbs_space X = {} ⟷ qbs_space (monadM_qbs X) = {}"
by(auto simp: monadM_qbs_space qbs_s_space_of_not_empty) (meson in_Mx.intro qbs_closed2_dest qbs_s_finite.qbs_space_of qbs_s_finite_def rep_qbs_s_finite_measure')
lemma(in qbs_s_finite) in_space_monadM[qbs]: "⟦X, α, μ⟧⇩s⇩f⇩i⇩n ∈ qbs_space (monadM_qbs X)"
by(simp add: monadM_qbs_space)
lemma rep_qbs_space_monadM:
assumes "s ∈ qbs_space (monadM_qbs X)"
obtains α μ where "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ"
using rep_qbs_space_of assms that by(auto simp: monadM_qbs_space)
lemma rep_qbs_space_monadM_sigma_finite:
assumes "s ∈ qbs_space (monadM_qbs X)"
obtains α μ where "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ" "sigma_finite_measure μ"
proof -
obtain α μ where s:"s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ"
by(metis rep_qbs_space_monadM assms)
hence "standard_borel_ne μ""s_finite_measure μ"
by(auto intro!: standard_borel_ne_sets[of borel μ] simp: qbs_s_finite_def qbs_s_finite_axioms_def)
from exists_push_forward[OF this] obtain μ' f where f:
"f ∈ (borel :: real measure) →⇩M μ" "sets μ' = sets borel" "sigma_finite_measure μ'" "distr μ' μ f = μ"
by metis
hence [measurable]: "f ∈ borel_measurable borel"
using s(2) by(auto simp: qbs_s_finite_def qbs_s_finite_axioms_def cong: measurable_cong_sets)
interpret pair_qbs_s_finite X α μ "α ∘ f" μ'
proof -
have "qbs_s_finite X (α ∘ f) μ'"
using s(2) by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def[of μ'] f(2,3) sigma_finite_measure.s_finite_measure)
thus "pair_qbs_s_finite X α μ (α ∘ f) μ'"
by(auto simp: pair_qbs_s_finite_def s(2))
qed
have "⟦X, α, μ⟧⇩s⇩f⇩i⇩n = ⟦X, α ∘ f, μ'⟧⇩s⇩f⇩i⇩n"
proof -
have [simp]:" distr μ (qbs_to_measure X) α = distr (distr μ' μ f) (qbs_to_measure X) α"
by(simp add: f(4))
show ?thesis
by(auto intro!: qbs_s_finite_measure_eq simp: distr_distr)
qed
with s(1) pq2.qbs_s_finite_axioms f(3) that
show ?thesis by metis
qed
lemma qbs_space_of_in: "s ∈ qbs_space (monadM_qbs X) ⟹ qbs_space_of s = X"
by(simp add: monadM_qbs_space)
lemma in_qbs_space_of: "s ∈ qbs_space (monadM_qbs (qbs_space_of s))"
by(simp add: monadM_qbs_space)
subsubsection ‹ $l$ ›
lift_definition qbs_l :: "'a qbs_measure ⇒ 'a measure"
is "λp. distr (snd (snd p)) (qbs_to_measure (fst p)) (fst (snd p))"
by(auto simp: qbs_s_finite_eq_def)
lemma(in qbs_s_finite) qbs_l: "qbs_l ⟦X, α, μ⟧⇩s⇩f⇩i⇩n = distr μ (qbs_to_measure X) α"
by(simp add: qbs_l.abs_eq)
interpretation qbs_l_s_finite: s_finite_measure "qbs_l (s :: 'a qbs_measure)"
proof(transfer)
show "⋀s:: 'a qbs_s_finite_t. qbs_s_finite_eq s s ⟹ s_finite_measure (distr (snd (snd s)) (qbs_to_measure (fst s)) (fst (snd s)))"
proof safe
fix X :: "'a quasi_borel"
fix α μ
assume "qbs_s_finite_eq (X,α,μ) (X,α,μ)"
then interpret qbs_s_finite X α μ
by(simp add: qbs_s_finite_eq_def)
show "s_finite_measure (distr (snd (snd (X,α,μ))) (qbs_to_measure (fst (X,α,μ))) (fst (snd (X,α,μ))))"
by(auto intro!: s_finite_measure.s_finite_measure_distr simp: s_finite_measure_axioms)
qed
qed
lemma space_qbs_l: "qbs_space (qbs_space_of s) = space (qbs_l s)"
by(transfer, auto simp: space_L)
lemma space_qbs_l_ne: "space (qbs_l s) ≠ {}"
by transfer (auto simp: qbs_s_finite_eq_def qbs_s_finite_def in_Mx_def space_L qbs_empty_equiv)
lemma qbs_l_sets: "sets (qbs_to_measure (qbs_space_of s)) = sets (qbs_l s)"
by(transfer,simp)
lemma qbs_null_measure_in_Mx: "qbs_space X ≠ {} ⟹ qbs_null_measure X ∈ qbs_space (monadM_qbs X)"
by(simp add: qbs_s_finite.in_space_monadM[OF qbs_null_measure_s_finite] qbs_null_measure_def)
lemma qbs_null_measure_null_measure:"qbs_space X ≠ {} ⟹ qbs_l (qbs_null_measure X) = null_measure (qbs_to_measure X)"
by(auto simp: qbs_null_measure_def qbs_s_finite.qbs_l[OF qbs_null_measure_s_finite] null_measure_distr)
lemma space_qbs_l_in:
assumes "s ∈ qbs_space (monadM_qbs X)"
shows "space (qbs_l s) = qbs_space X"
by (metis assms qbs_s_finite.qbs_space_of rep_qbs_space_monadM space_qbs_l)
lemma sets_qbs_l:
assumes "s ∈ qbs_space (monadM_qbs X)"
shows "sets (qbs_l s) = sets (qbs_to_measure X)"
using assms qbs_l_sets qbs_space_of_in by blast
lemma measurable_qbs_l:
assumes "s ∈ qbs_space (monadM_qbs X)"
shows "qbs_l s →⇩M M = X →⇩Q measure_to_qbs M"
by(auto simp: measurable_cong_sets[OF qbs_l_sets[of s,simplified qbs_space_of_in[OF assms(1)],symmetric] refl] lr_adjunction_correspondence)
lemma measurable_qbs_l':
assumes "s ∈ qbs_space (monadM_qbs X)"
shows "qbs_l s →⇩M M = qbs_to_measure X →⇩M M"
by(simp add: measurable_qbs_l[OF assms] lr_adjunction_correspondence)
lemma rep_qbs_Mx_monadM:
assumes "γ ∈ qbs_Mx (monadM_qbs X)"
obtains α k where "γ = (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n)" "α ∈ qbs_Mx X" "s_finite_kernel borel borel k" "⋀r. qbs_s_finite X α (k r)"
proof -
have "⋀α r k. α ∈ qbs_Mx X ⟹ s_finite_kernel borel borel k ⟹ qbs_s_finite X α (k r)"
by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def s_finite_kernel.image_s_finite_measure) (auto simp: s_finite_kernel_def measure_kernel_def)
thus ?thesis
using that assms by(fastforce simp: monadM_qbs_Mx)
qed
lemma qbs_l_measurable[measurable]:"qbs_l ∈ qbs_to_measure (monadM_qbs X) →⇩M s_finite_measure_algebra (qbs_to_measure X)"
proof(rule qbs_morphism_dest[OF qbs_morphismI])
fix γ
assume "γ ∈ qbs_Mx (monadM_qbs X)"
from rep_qbs_Mx_monadM[OF this] obtain α k where h:
"γ = (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n)" "α ∈ qbs_Mx X" "s_finite_kernel borel borel k" "⋀r. qbs_s_finite X α (k r)"
by metis
show "qbs_l ∘ γ ∈ qbs_Mx (measure_to_qbs (s_finite_measure_algebra (qbs_to_measure X)))"
by(auto simp add: qbs_Mx_R comp_def h(1) qbs_s_finite.qbs_l[OF h(4)] h(2,3) intro!: s_finite_kernel.kernel_measurable_s_finite s_finite_kernel.distr_s_finite_kernel[where Y=borel])
qed
lemma qbs_l_measure_kernel: "measure_kernel (qbs_to_measure (monadM_qbs X)) (qbs_to_measure X) qbs_l"
proof(cases "qbs_space X = {}")
case True
with monadM_qbs_empty_iff[of X,simplified this] show ?thesis
by(auto intro!: measure_kernel_empty_trivial simp: space_L)
next
case 1:False
show ?thesis
proof
show "⋀x. x ∈ space (qbs_to_measure (monadM_qbs X)) ⟹ sets (qbs_l x) = sets (qbs_to_measure X)"
using qbs_l_sets by(auto simp: space_L monadM_qbs_space)
next
show "space (qbs_to_measure X) ≠ {}"
by(simp add: space_L 1)
qed (rule measurable_emeasure_kernel_s_finite_measure_algebra[OF qbs_l_measurable])
qed
lemma qbs_l_inj: "inj_on qbs_l (qbs_space (monadM_qbs X))"
by standard (auto simp: monadM_qbs_space, transfer,auto simp: qbs_s_finite_eq_def)
lemma qbs_l_morphism:
assumes [measurable]:"A ∈ sets (qbs_to_measure X)"
shows "(λs. qbs_l s A) ∈ monadM_qbs X →⇩Q qbs_borel"
proof(rule qbs_morphismI)
fix γ
assume h:"γ ∈ qbs_Mx (monadM_qbs X)"
hence [qbs]: "γ ∈ qbs_borel →⇩Q monadM_qbs X"
by(simp_all add: qbs_Mx_is_morphisms)
from rep_qbs_Mx_monadM[OF h(1)] obtain α k where hk:
"γ = (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n)" "α ∈ qbs_Mx X" "s_finite_kernel borel borel k" "⋀r. qbs_s_finite X α (k r)"
by metis
then interpret a: in_Mx X α by(simp add: in_Mx_def)
have k[measurable_cong]:"sets (k r) = sets borel" for r
using hk(3) by(auto simp: s_finite_kernel_def measure_kernel_def)
show "(λs. emeasure (qbs_l s) A) ∘ γ ∈ qbs_Mx qbs_borel"
by(auto simp: hk(1) qbs_s_finite.qbs_l[OF hk(4)] comp_def qbs_Mx_qbs_borel emeasure_distr sets_eq_imp_space_eq[OF k] intro!: s_finite_kernel.emeasure_measurable'[OF hk(3)] measurable_sets_borel[OF _ assms])
qed
lemma qbs_l_finite_pred: "qbs_pred (monadM_qbs X) (λs. finite_measure (qbs_l s))"
proof -
have "qbs_space X ∈ sets (qbs_to_measure X)"
by (metis sets.top space_L)
note qbs_l_morphism[OF this,qbs]
have [simp]:"finite_measure (qbs_l s) ⟷ qbs_l s X ≠ ∞" if "s ∈ monadM_qbs X" for s
by(auto intro!: finite_measureI dest: finite_measure.emeasure_finite simp: space_qbs_l_in[OF that])
show ?thesis
by(simp cong: qbs_morphism_cong)
qed
lemma qbs_l_subprob_pred: "qbs_pred (monadM_qbs X) (λs. subprob_space (qbs_l s))"
proof -
have "qbs_space X ∈ sets (qbs_to_measure X)"
by (metis sets.top space_L)
note qbs_l_morphism[OF this,qbs]
have [simp]:"subprob_space (qbs_l s) ⟷ qbs_l s X ≤ 1" if "s ∈ monadM_qbs X" for s
by(auto intro!: subprob_spaceI dest: subprob_space.subprob_emeasure_le_1 simp: space_qbs_l_ne) (simp add: space_qbs_l_in[OF that])
show ?thesis
by(simp cong: qbs_morphism_cong)
qed
lemma qbs_l_prob_pred: "qbs_pred (monadM_qbs X) (λs. prob_space (qbs_l s))"
proof -
have "qbs_space X ∈ sets (qbs_to_measure X)"
by (metis sets.top space_L)
note qbs_l_morphism[OF this,qbs]
have [simp]:"prob_space (qbs_l s) ⟷ qbs_l s X = 1" if "s ∈ monadM_qbs X" for s
by(auto intro!: prob_spaceI simp: space_qbs_l_ne) (auto simp add: space_qbs_l_in[OF that] dest: prob_space.emeasure_space_1)
show ?thesis
by(simp cong: qbs_morphism_cong)
qed
subsubsection ‹ Return ›
definition return_qbs :: "'a quasi_borel ⇒ 'a ⇒ 'a qbs_measure" where
"return_qbs X x ≡ ⟦X, λr. x, SOME μ. real_distribution μ⟧⇩s⇩f⇩i⇩n"
lemma(in real_distribution)
assumes "x ∈ qbs_space X"
shows return_qbs:"return_qbs X x = ⟦X, λr. x, M⟧⇩s⇩f⇩i⇩n"
and return_qbs_prob:"qbs_prob X (λr. x) M"
and return_qbs_s_finite:"qbs_s_finite X (λr. x) M"
proof -
interpret qs1: qbs_prob X "λr. x" M
by(auto simp: qbs_prob_def in_Mx_def real_distribution_axioms intro!: qbs_closed2_dest assms)
show "return_qbs X x = ⟦X, λr. x, M⟧⇩s⇩f⇩i⇩n"
unfolding return_qbs_def
proof(rule someI2)
show "real_distribution (return borel 0)" by (auto simp: real_distribution_def real_distribution_axioms_def,rule prob_space_return) simp
next
fix N
assume "real_distribution N"
then interpret qs2: qbs_s_finite X "λr. x" N
by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def real_distribution_def real_distribution_axioms_def intro!: qbs_closed2_dest assms sigma_finite_measure.s_finite_measure prob_space_imp_sigma_finite)
interpret pair_qbs_s_finite X "λr. x" N "λr. x" M
by standard
show "⟦X, λr. x, N⟧⇩s⇩f⇩i⇩n = ⟦X, λr. x, M⟧⇩s⇩f⇩i⇩n"
by(auto intro!: qbs_s_finite_measure_eq measure_eqI simp: emeasure_distr) (metis ‹real_distribution N› emeasure_space_1 prob_space.emeasure_space_1 qs2.mu_sets real_distribution.axioms(1) sets_eq_imp_space_eq space_borel space_eq_univ)
qed
show "qbs_prob X (λr. x) M" "qbs_s_finite X (λr. x) M"
by(simp_all add: qs1.qbs_prob_axioms qs1.qbs_s_finite_axioms)
qed
lemma return_qbs_comp:
assumes "α ∈ qbs_Mx X"
shows "(return_qbs X ∘ α) = (λr. ⟦X, α, return borel r⟧⇩s⇩f⇩i⇩n)"
proof
fix r
interpret pqp: pair_qbs_prob X "λk. α r" "return borel 0" α "return borel r"
by(simp add: assms qbs_Mx_to_X[OF assms] pair_qbs_prob_def qbs_prob_def in_Mx_def real_distribution_def real_distribution_axioms_def prob_space_return)
show "(return_qbs X ∘ α) r = ⟦X, α, return borel r⟧⇩s⇩f⇩i⇩n"
by(auto simp: pqp.pq1.return_qbs[OF qbs_Mx_to_X[OF assms]] distr_return intro!: pqp.qbs_s_finite_measure_eq)
qed
corollary return_qbs_morphism[qbs]: "return_qbs X ∈ X →⇩Q monadM_qbs X"
proof(rule qbs_morphismI)
interpret rr : real_distribution "return borel 0"
by(simp add: real_distribution_def real_distribution_axioms_def prob_space_return)
fix α
assume h:"α ∈ qbs_Mx X"
then have 1:"return_qbs X ∘ α = (λr. ⟦X, α, return borel r⟧⇩s⇩f⇩i⇩n)"
by(rule return_qbs_comp)
show "return_qbs X ∘ α ∈ qbs_Mx (monadM_qbs X)"
by(auto simp: 1 monadM_qbs_Mx h prob_kernel_def' intro!: exI[where x=α] exI[where x="return borel"] prob_kernel.s_finite_kernel_prob_kernel)
qed
subsubsection ‹Bind›
definition bind_qbs :: "['a qbs_measure, 'a ⇒ 'b qbs_measure] ⇒ 'b qbs_measure" where
"bind_qbs s f ≡ (let (X, α, μ) = rep_qbs_measure s;
Y = qbs_space_of (f (α undefined));
(β, k) = (SOME (β, k). f ∘ α = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n) ∧ β ∈ qbs_Mx Y ∧ s_finite_kernel borel borel k) in
⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n)"
adhoc_overloading Monad_Syntax.bind bind_qbs
lemma(in qbs_s_finite)
assumes "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
"f ∈ X →⇩Q monadM_qbs Y"
"β ∈ qbs_Mx Y"
"s_finite_kernel borel borel k"
and "(f ∘ α) = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)"
shows bind_qbs_s_finite:"qbs_s_finite Y β (μ ⤜⇩k k)"
and bind_qbs: "s ⤜ f = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof -
interpret k: s_finite_kernel borel borel k by fact
interpret s_fin: qbs_s_finite Y β "μ ⤜⇩k k"
by(auto simp: qbs_s_finite_def in_Mx_def assms(3) mu_sets qbs_s_finite_axioms_def k.sets_bind_kernel[OF _ mu_sets] intro!:k.comp_s_finite_measure s_finite_measure_axioms)
show "s ⤜ f = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof -
{
fix X' α' μ'
assume "(X',α',μ') ∈ Rep_qbs_measure ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
then have h: "X' = X" "qbs_s_finite X' α' μ'" "qbs_s_finite_eq (X,α,μ) (X',α',μ')"
by(simp_all add: if_in_Rep_qbs_measure)
then interpret s_fin_pq1: pair_qbs_s_finite X α μ α' μ'
by(auto simp: pair_qbs_s_finite_def qbs_s_finite_axioms)
have [simp]: "qbs_space_of (f (α' r)) = Y" for r
using qbs_Mx_to_X[OF qbs_morphism_Mx[OF assms(2) s_fin_pq1.pq2.in_Mx],of r]
by(auto simp: monadM_qbs_space)
have "(let Y = qbs_space_of (f (α' undefined)) in case SOME (β, k). (λr. f (α' r)) = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n) ∧ β ∈ qbs_Mx Y ∧ s_finite_kernel borel borel k of
(β, k) ⇒ ⟦Y, β, μ' ⤜⇩k k⟧⇩s⇩f⇩i⇩n) = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof -
have "(case SOME (β, k). (λr. f (α' r)) = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n) ∧ β ∈ qbs_Mx Y ∧ s_finite_kernel borel borel k of (β, k) ⇒ ⟦Y, β, μ' ⤜⇩k k⟧⇩s⇩f⇩i⇩n) = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof(rule someI2_ex)
show "∃a. case a of (β, k) ⇒ (λr. f (α' r)) = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n) ∧ β ∈ qbs_Mx Y ∧ s_finite_kernel borel borel k"
using qbs_morphism_Mx[OF assms(2) s_fin_pq1.pq2.in_Mx]
by(auto simp: comp_def monadM_qbs_Mx)
next
show "⋀x. (case x of (β, k) ⇒ (λr. f (α' r)) = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n) ∧ β ∈ qbs_Mx Y ∧ s_finite_kernel borel borel k) ⟹ (case x of (β, k) ⇒ ⟦Y, β, μ' ⤜⇩k k⟧⇩s⇩f⇩i⇩n) = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof safe
fix β' k'
assume h':"(λr. f (α' r)) = (λr. ⟦Y, β', k' r⟧⇩s⇩f⇩i⇩n)" "β' ∈ qbs_Mx Y" "s_finite_kernel borel borel k'"
interpret k': s_finite_kernel borel borel k' by fact
have "qbs_s_finite Y β' (μ' ⤜⇩k k')"
by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def h'(2) k'.sets_bind_kernel[OF _ s_fin_pq1.pq2.mu_sets] s_fin_pq1.pq2.mu_sets intro!:k'.comp_s_finite_measure s_fin_pq1.pq2.s_finite_measure_axioms)
then interpret s_fin_pq2: pair_qbs_s_finite Y β' "μ' ⤜⇩k k'" β "μ ⤜⇩k k"
by(auto simp: pair_qbs_s_finite_def s_fin.qbs_s_finite_axioms)
show "⟦Y, β', μ' ⤜⇩k k'⟧⇩s⇩f⇩i⇩n = ⟦Y, β, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
proof(rule s_fin_pq2.qbs_s_finite_measure_eq)
show "distr (μ' ⤜⇩k k') (qbs_to_measure Y) β' = distr (μ ⤜⇩k k) (qbs_to_measure Y) β" (is "?lhs = ?rhs")
proof -
have "?lhs = μ' ⤜⇩k (λr. distr (k' r) (qbs_to_measure Y) β')"
by(simp add: k'.distr_bind_kernel[OF _ s_fin_pq1.pq2.mu_sets])
also have "... = μ' ⤜⇩k (λr. qbs_l ⟦Y, β', k' r⟧⇩s⇩f⇩i⇩n)"
by(rule bind_kernel_cong_All,rule qbs_s_finite.qbs_l[symmetric,OF qbs_s_finite_All[where k=k' and M=borel]]) (auto simp: k'.s_finite_kernel_axioms)
also have "... = μ' ⤜⇩k (λr. qbs_l (f (α' r)))"
by(auto simp: fun_cong[OF h'(1)])
also have "... = distr μ' (qbs_to_measure X) α' ⤜⇩k (λx. qbs_l (f x))"
by(simp add: measure_kernel.bind_kernel_distr[OF measure_kernel.measure_kernel_comp[OF qbs_l_measure_kernel set_mp[OF l_preserves_morphisms assms(2)]]] sets_eq_imp_space_eq[OF s_fin_pq1.pq2.mu_sets])
also have "... = distr μ (qbs_to_measure X) α ⤜⇩k (λx. qbs_l (f x))"
by(simp add: qbs_s_finite_eq_dest(4)[OF h(3)])
also have "... = μ ⤜⇩k (λr. qbs_l (f (α r)))"
by(simp add: measure_kernel.bind_kernel_distr[OF measure_kernel.measure_kernel_comp[OF qbs_l_measure_kernel set_mp[OF l_preserves_morphisms assms(2)]]] sets_eq_imp_space_eq[OF mu_sets])
also have "... = μ ⤜⇩k (λr. qbs_l ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)"
by(simp add: fun_cong[OF assms(5),simplified comp_def])
also have "... = μ ⤜⇩k (λr. distr (k r) (qbs_to_measure Y) β)"
by(rule bind_kernel_cong_All,rule qbs_s_finite.qbs_l[OF qbs_s_finite_All[where k=k and M=borel]]) (auto simp: k.s_finite_kernel_axioms)
also have "... = ?rhs"
by(simp add: k.distr_bind_kernel[OF _ mu_sets])
finally show ?thesis .
qed
qed
qed
qed
thus ?thesis by simp
qed
}
show ?thesis
unfolding bind_qbs_def rep_qbs_measure_def qbs_measure.rep_def assms(1)
by(rule someI2, rule in_Rep_qbs_measure, auto) fact
qed
show "qbs_s_finite Y β (μ ⤜⇩k k)"
by(rule s_fin.qbs_s_finite_axioms)
qed
lemma bind_qbs_morphism':
assumes "f ∈ X →⇩Q monadM_qbs Y"
shows "(λx. x ⤜ f) ∈ monadM_qbs X →⇩Q monadM_qbs Y"
proof(rule qbs_morphismI)
fix γ
assume "γ ∈ qbs_Mx (monadM_qbs X)"
from rep_qbs_Mx_monadM[OF this] obtain α k where h:
"γ = (λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n)" "α ∈ qbs_Mx X" "s_finite_kernel borel borel k" "⋀r. qbs_s_finite X α (k r)"
by metis
from rep_qbs_Mx_monadM[OF qbs_morphism_Mx[OF assms this(2)]] obtain α' k' where h':
"f ∘ α = (λr. ⟦Y, α', k' r⟧⇩s⇩f⇩i⇩n)" "α' ∈ qbs_Mx Y" "s_finite_kernel borel borel k'" "⋀r. qbs_s_finite Y α' (k' r)"
by metis
have [simp]:"(λx. x ⤜ f) ∘ γ = (λr. ⟦Y, α', k r ⤜⇩k k'⟧⇩s⇩f⇩i⇩n)"
by standard (simp add: h(1) qbs_s_finite.bind_qbs[OF h(4) _ assms h'(2,3,1)])
show "(λx. x ⤜ f) ∘ γ ∈ qbs_Mx (monadM_qbs Y)"
using h'(2) by(auto simp: s_finite_kernel.bind_kernel_s_finite_kernel[OF h(3) h'(3)] monadM_qbs_Mx intro!: exI[where x=α'])
qed
lemma bind_qbs_return':
assumes "x ∈ qbs_space (monadM_qbs X)"
shows "x ⤜ return_qbs X = x"
proof -
obtain α μ where h:"qbs_s_finite X α μ" "x = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
using rep_qbs_space_monadM[OF assms] by blast
then interpret qs: qbs_s_finite X α μ by simp
interpret prob_kernel borel borel "return borel"
by(simp add: prob_kernel_def')
show ?thesis
by(simp add: qs.bind_qbs[OF h(2) return_qbs_morphism _ _ return_qbs_comp] s_finite_kernel_axioms bind_kernel_return''[OF qs.mu_sets] h(2)[symmetric])
qed
lemma bind_qbs_return:
assumes "f ∈ X →⇩Q monadM_qbs Y"
and "x ∈ qbs_space X"
shows "return_qbs X x ⤜ f = f x"
proof -
from rep_qbs_space_monadM[OF qbs_morphism_space[OF assms]] obtain α μ where h:
"f x = ⟦Y, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite Y α μ" by auto
then interpret qs:qbs_s_finite Y α μ by simp
interpret sk: s_finite_kernel borel borel "λr. μ"
by(auto intro!: s_finite_measure.s_finite_kernel_const simp: s_finite_kernel_cong_sets[OF refl qs.mu_sets[symmetric]] qs.s_finite_measure_axioms qs.mu_not_empty)
interpret rd: real_distribution "return borel 0"
by(simp add: real_distribution_def prob_space_return real_distribution_axioms_def)
interpret qbs_prob X "λr. x" "return borel 0"
by(rule rd.return_qbs_prob[OF assms(2)])
show ?thesis
using bind_qbs[OF rd.return_qbs[OF assms(2)] assms(1) qs.in_Mx sk.s_finite_kernel_axioms]
by(simp add: h(1) sk.bind_kernel_return)
qed
lemma bind_qbs_assoc:
assumes "s ∈ qbs_space (monadM_qbs X)"
"f ∈ X →⇩Q monadM_qbs Y"
and "g ∈ Y →⇩Q monadM_qbs Z"
shows "s ⤜ (λx. f x ⤜ g) = (s ⤜ f) ⤜ g" (is "?lhs = ?rhs")
proof -
obtain α μ where h:"s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ"
using rep_qbs_space_monadM[OF assms(1)] by blast
then interpret qs: qbs_s_finite X α μ by simp
from rep_qbs_Mx_monadM[OF qbs_morphism_Mx[OF assms(2) qs.in_Mx]] obtain β k where h':
"f ∘ α = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)" "β ∈ qbs_Mx Y" "s_finite_kernel borel borel k" "⋀r. qbs_s_finite Y β (k r)"
by metis
from rep_qbs_Mx_monadM[OF qbs_morphism_Mx[OF assms(3) h'(2)]] obtain γ k' where h'':
"g ∘ β = (λr. ⟦Z, γ, k' r⟧⇩s⇩f⇩i⇩n)" "γ ∈ qbs_Mx Z" "s_finite_kernel borel borel k'" "⋀r. qbs_s_finite Z γ (k' r)"
by metis
have 1:"(λx. f x ⤜ g) ∘ α = (λr. ⟦Z, γ, k r ⤜⇩k k'⟧⇩s⇩f⇩i⇩n)"
by standard (simp add: qbs_s_finite.bind_qbs[OF h'(4) fun_cong[OF h'(1),simplified] assms(3) h''(2,3,1)])
have "?lhs = ⟦Z, γ, μ ⤜⇩k (λr. k r ⤜⇩k k')⟧⇩s⇩f⇩i⇩n"
by(rule qs.bind_qbs[OF h(1) qbs_morphism_compose[OF assms(2) bind_qbs_morphism'[OF assms(3)]] h''(2) s_finite_kernel.bind_kernel_s_finite_kernel[OF h'(3) h''(3)] 1])
also have "... = ⟦Z, γ, μ ⤜⇩k k ⤜⇩k k'⟧⇩s⇩f⇩i⇩n"
by(simp add: s_finite_kernel.bind_kernel_assoc[OF h'(3) h''(3) qs.mu_sets])
also have "... = ?rhs"
by(simp add: qbs_s_finite.bind_qbs[OF qs.bind_qbs_s_finite[OF h(1) assms(2) h'(2,3,1)] qs.bind_qbs[OF h(1) assms(2) h'(2,3,1)] assms(3) h''(2,3,1)])
finally show ?thesis .
qed
lemma bind_qbs_cong:
assumes [qbs]:"s ∈ qbs_space (monadM_qbs X)"
"⋀x. x ∈ qbs_space X ⟹ f x = g x"
and [qbs]:"f ∈ X →⇩Q monadM_qbs Y"
shows "s ⤜ f = s ⤜ g"
proof -
from rep_qbs_space_monadM[OF assms(1)] obtain α μ where h:
"s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ" by auto
interpret qbs_s_finite X α μ by fact
from rep_qbs_Mx_monadM[OF qbs_morphism_Mx[OF assms(3) in_Mx]] obtain β k where h':
"f ∘ α = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)" "β ∈ qbs_Mx Y" "s_finite_kernel borel borel k" by metis
have g: "g ∈ X →⇩Q monadM_qbs Y" "g ∘ α = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)"
using qbs_Mx_to_X[OF in_Mx] assms(2) fun_cong[OF h'(1)]
by(auto simp: assms(2)[symmetric] cong: qbs_morphism_cong)
show ?thesis
by(simp add: bind_qbs[OF h(1) assms(3) h'(2,3,1)] bind_qbs[OF h(1) g(1) h'(2,3) g(2)])
qed
subsubsection ‹ The Functorial Action ›
definition distr_qbs :: "['a quasi_borel, 'b quasi_borel,'a ⇒ 'b,'a qbs_measure] ⇒ 'b qbs_measure" where
"distr_qbs _ Y f sx ≡ sx ⤜ return_qbs Y ∘ f"
lemma distr_qbs_morphism':
assumes "f ∈ X →⇩Q Y"
shows "distr_qbs X Y f ∈ monadM_qbs X →⇩Q monadM_qbs Y"
unfolding distr_qbs_def
by(rule bind_qbs_morphism'[OF qbs_morphism_comp[OF assms return_qbs_morphism]])
lemma(in qbs_s_finite)
assumes "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
and "f ∈ X →⇩Q Y"
shows distr_qbs_s_finite:"qbs_s_finite Y (f ∘ α) μ"
and distr_qbs: "distr_qbs X Y f s = ⟦Y, f ∘ α, μ⟧⇩s⇩f⇩i⇩n"
by(auto intro!: bind_qbs[OF assms(1) qbs_morphism_comp[OF assms(2) return_qbs_morphism],of "f ∘ α" "return borel" ,simplified bind_kernel_return''[OF mu_sets]] bind_qbs_s_finite[OF assms(1) qbs_morphism_comp[OF assms(2) return_qbs_morphism],of "f ∘ α" "return borel" ,simplified bind_kernel_return''[OF mu_sets]]
simp: distr_qbs_def return_qbs_comp[OF qbs_morphism_Mx[OF assms(2) in_Mx],simplified comp_assoc[symmetric]] qbs_morphism_Mx[OF assms(2) in_Mx] prob_kernel.s_finite_kernel_prob_kernel[of borel borel "return borel",simplified prob_kernel_def'])
lemma(in qbs_prob)
assumes "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
and "f ∈ X →⇩Q Y"
shows distr_qbs_prob:"qbs_prob Y (f ∘ α) μ"
by(auto simp: distr_qbs_def prob_space_axioms intro!: qbs_s_finite.qbs_probI[OF distr_qbs_s_finite[OF assms]])
text ‹ We show that $M$ is a functor i.e. $M$ preserve identity and composition.›
lemma distr_qbs_id:
assumes "s ∈ qbs_space (monadM_qbs X)"
shows "distr_qbs X X id s = s"
using bind_qbs_return'[OF assms] by(simp add: distr_qbs_def)
lemma distr_qbs_comp:
assumes "s ∈ qbs_space (monadM_qbs X)"
"f ∈ X →⇩Q Y"
and "g ∈ Y →⇩Q Z"
shows "((distr_qbs Y Z g) ∘ (distr_qbs X Y f)) s = distr_qbs X Z (g ∘ f) s"
proof -
from rep_qbs_space_monadM[OF assms(1)] obtain α μ where h:
"qbs_s_finite X α μ" "s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" by metis
have "qbs_s_finite Y (f ∘ α) μ" "distr_qbs X Y f s = ⟦Y, f ∘ α, μ⟧⇩s⇩f⇩i⇩n"
by(simp_all add: qbs_s_finite.distr_qbs_s_finite[OF h assms(2)] qbs_s_finite.distr_qbs[OF h assms(2)])
from qbs_s_finite.distr_qbs[OF this assms(3)] qbs_s_finite.distr_qbs[OF h qbs_morphism_comp[OF assms(2,3)]]
show ?thesis
by(simp add: comp_assoc)
qed
subsubsection ‹ Join ›
definition join_qbs :: "'a qbs_measure qbs_measure ⇒ 'a qbs_measure" where
"join_qbs ≡ (λsst. sst ⤜ id)"
lemma join_qbs_morphism[qbs]: "join_qbs ∈ monadM_qbs (monadM_qbs X) →⇩Q monadM_qbs X"
by(simp add: join_qbs_def bind_qbs_morphism'[OF qbs_morphism_ident])
lemma
assumes "qbs_s_finite (monadM_qbs X) β μ"
"ssx = ⟦monadM_qbs X, β, μ⟧⇩s⇩f⇩i⇩n"
"α ∈ qbs_Mx X"
"s_finite_kernel borel borel k"
and "β =(λr. ⟦X, α, k r⟧⇩s⇩f⇩i⇩n)"
shows qbs_s_finite_join_qbs_s_finite: "qbs_s_finite X α (μ ⤜⇩k k)"
and qbs_s_finite_join_qbs: "join_qbs ssx = ⟦X, α, μ ⤜⇩k k⟧⇩s⇩f⇩i⇩n"
using qbs_s_finite.bind_qbs[OF assms(1,2) qbs_morphism_ident assms(3,4)] qbs_s_finite.bind_qbs_s_finite[OF assms(1,2) qbs_morphism_ident assms(3,4)]
by(auto simp: assms(5) join_qbs_def)
subsubsection ‹ Strength ›
definition strength_qbs :: "['a quasi_borel,'b quasi_borel,'a × 'b qbs_measure] ⇒ ('a × 'b) qbs_measure" where
"strength_qbs W X = (λ(w,sx). let (_,α,μ) = rep_qbs_measure sx
in ⟦W ⨂⇩Q X, λr. (w,α r), μ⟧⇩s⇩f⇩i⇩n)"
lemma(in qbs_s_finite)
assumes "w ∈ qbs_space W"
and "sx = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
shows strength_qbs_s_finite: "qbs_s_finite (W ⨂⇩Q X) (λr. (w,α r)) μ"
and strength_qbs: "strength_qbs W X (w,sx) = ⟦W ⨂⇩Q X, λr. (w,α r), μ⟧⇩s⇩f⇩i⇩n"
proof -
interpret qs: qbs_s_finite "W ⨂⇩Q X" "λr. (w,α r)" μ
by(auto simp: qbs_s_finite_def s_finite_measure_axioms qbs_s_finite_axioms_def mu_sets in_Mx_def assms(1) intro!: pair_qbs_MxI)
show "qbs_s_finite (W ⨂⇩Q X) (λr. (w,α r)) μ" by (rule qs.qbs_s_finite_axioms)
show "strength_qbs W X (w,sx) = ⟦W ⨂⇩Q X, λr. (w,α r), μ⟧⇩s⇩f⇩i⇩n"
proof -
{
fix X' α' μ'
assume "(X',α',μ') ∈ Rep_qbs_measure ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
then have h: "X' = X" "qbs_s_finite X' α' μ'" "qbs_s_finite_eq (X,α,μ) (X',α',μ')"
by(simp_all add: if_in_Rep_qbs_measure)
then interpret qs': qbs_s_finite "W ⨂⇩Q X" "λr. (w,α' r)" μ'
by(auto simp: qbs_s_finite_def in_Mx_def assms(1) intro!: pair_qbs_MxI)
interpret pq: pair_qbs_s_finite "W ⨂⇩Q X" "λr. (w,α r)" μ "λr. (w,α' r)" μ'
by(auto simp: qs.qbs_s_finite_axioms qs'.qbs_s_finite_axioms pair_qbs_s_finite_def)
have "⟦W ⨂⇩Q X, λr. (w, α' r), μ'⟧⇩s⇩f⇩i⇩n = ⟦W ⨂⇩Q X, λr. (w, α r), μ⟧⇩s⇩f⇩i⇩n"
proof(rule pq.qbs_s_finite_measure_eq'[symmetric])
fix f :: "_ ⇒ ennreal"
assume "f ∈ W ⨂⇩Q X →⇩Q qbs_borel"
then have f: "curry f w ∈ X →⇩Q qbs_borel"
by (metis assms(1) qbs_morphism_curry qbs_morphism_space)
show "(∫⇧+ x. f (w, α x) ∂μ) = (∫⇧+ x. f (w, α' x) ∂μ')" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. curry f w (α x) ∂μ)" by simp
also have "... = (∫⇧+ x. curry f w (α' x) ∂μ')"
using h(3) f by(auto simp: qbs_s_finite_eq_equiv qbs_s_finite_eq'_def h(1))
also have "... = ?rhs" by simp
finally show ?thesis .
qed
qed
}
show ?thesis
by(simp add: strength_qbs_def rep_qbs_measure_def qbs_measure.rep_def assms(2)) (rule someI2, rule in_Rep_qbs_measure, auto, fact)
qed
qed
lemma(in qbs_prob)
assumes "w ∈ qbs_space W"
and "sx = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
shows strength_qbs_prob: "qbs_prob (W ⨂⇩Q X) (λr. (w,α r)) μ"
by(auto intro!: qbs_s_finite.qbs_probI[OF strength_qbs_s_finite[OF assms]] prob_space_axioms)
lemma strength_qbs_natural:
assumes "f ∈ X →⇩Q X'"
"g ∈ Y →⇩Q Y'"
"x ∈ qbs_space X"
and "sy ∈ qbs_space (monadM_qbs Y)"
shows "(distr_qbs (X ⨂⇩Q Y) (X' ⨂⇩Q Y') (map_prod f g) ∘ strength_qbs X Y) (x,sy) = (strength_qbs X' Y' ∘ map_prod f (distr_qbs Y Y' g)) (x,sy)"
(is "?lhs = ?rhs")
proof -
from rep_qbs_space_monadM[OF assms(4)] obtain α μ
where h:"sy = ⟦Y, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite Y α μ" by metis
have "?lhs = (distr_qbs (X ⨂⇩Q Y) (X' ⨂⇩Q Y') (map_prod f g)) (⟦X ⨂⇩Q Y, λr. (x,α r), μ⟧⇩s⇩f⇩i⇩n)"
by(simp add: qbs_s_finite.strength_qbs[OF h(2) assms(3) h(1)])
also have "... = ⟦X' ⨂⇩Q Y', map_prod f g ∘ (λr. (x, α r)), μ⟧⇩s⇩f⇩i⇩n"
using assms by(simp add: qbs_s_finite.distr_qbs[OF qbs_s_finite.strength_qbs_s_finite[OF h(2) assms(3) h(1)] refl ])
also have "... = ⟦X' ⨂⇩Q Y',λr. (f x, (g ∘ α) r), μ⟧⇩s⇩f⇩i⇩n" by (simp add: comp_def)
also have "... = ?rhs"
by(simp add: qbs_s_finite.strength_qbs[OF qbs_s_finite.distr_qbs_s_finite[OF h(2,1) assms(2)] qbs_morphism_space[OF assms(1,3)] qbs_s_finite.distr_qbs[OF h(2,1) assms(2)]])
finally show ?thesis .
qed
context
begin
interpretation rr : standard_borel_ne "borel ⨂⇩M borel :: (real × real) measure"
by(auto intro!: pair_standard_borel_ne)
declare rr.from_real_to_real[simplified space_pair_measure,simplified,simp]
lemma rr_from_real_to_real_id[simp]: "rr.from_real ∘ rr.to_real = id"
by(auto simp: comp_def)
lemma
assumes "α ∈ qbs_Mx X"
"β ∈ qbs_Mx (monadM_qbs Y)"
"γ ∈ qbs_Mx Y"
"s_finite_kernel borel borel k"
and "β = (λr. ⟦Y, γ, k r⟧⇩s⇩f⇩i⇩n)"
shows strength_qbs_ab_r_s_finite: "qbs_s_finite (X ⨂⇩Q Y) (map_prod α γ ∘ rr.from_real) (distr (return borel r ⨂⇩M k r) borel rr.to_real)"
and strength_qbs_ab_r: "strength_qbs X Y (α r, β r) = ⟦X ⨂⇩Q Y, map_prod α γ ∘ rr.from_real, distr (return borel r ⨂⇩M k r) borel rr.to_real⟧⇩s⇩f⇩i⇩n" (is ?goal2)
proof -
interpret k: s_finite_kernel borel borel k by fact
note 1[measurable_cong] = sets_return[of borel r] k.kernel_sets[of r,simplified]
show "qbs_s_finite (X ⨂⇩Q Y) (map_prod α γ ∘ rr.from_real) (distr (return borel r ⨂⇩M k r) borel rr.to_real)"
using assms(1,3) by(auto simp: qbs_s_finite_def in_Mx_def qbs_s_finite_axioms_def qbs_Mx_is_morphisms r_preserves_product[symmetric] standard_borel_ne.standard_borel intro!: s_finite_measure.s_finite_measure_distr[OF pair_measure_s_finite_measure[OF prob_space.s_finite_measure_prob[OF prob_space_return[of r borel]] k.image_s_finite_measure[of r]]] qbs_morphism_comp[where Y="qbs_borel ⨂⇩Q qbs_borel"] qbs_morphism_space[OF qbs_morphism_space[OF qbs_morphism_map_prod]] standard_borel.qbs_morphism_measurable_intro[of "borel :: real measure"])
then interpret qs: qbs_s_finite "X ⨂⇩Q Y" "map_prod α γ ∘ rr.from_real" "distr (return borel r ⨂⇩M k r) borel rr.to_real" .
interpret qs2: qbs_s_finite Y γ "k r"
by(auto simp: qbs_s_finite_def k.image_s_finite_measure in_Mx_def assms qbs_s_finite_axioms_def k.kernel_sets)
interpret pq: pair_qbs_s_finite "X ⨂⇩Q Y" "λl. (α r, γ l)" "k r" "map_prod α γ ∘ rr.from_real" "distr (return borel r ⨂⇩M k r) borel rr.to_real"
by (auto simp: pair_qbs_s_finite_def qs.qbs_s_finite_axioms qs2.strength_qbs_s_finite[OF qbs_Mx_to_X[OF assms(1),of r] fun_cong[OF assms(5)]])
have [measurable]: "map_prod α γ ∈ borel ⨂⇩M borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
proof -
have "map_prod α γ ∈ qbs_borel ⨂⇩Q qbs_borel →⇩Q X ⨂⇩Q Y"
using assms by(auto intro!: qbs_morphism_map_prod simp: qbs_Mx_is_morphisms)
also have "... ⊆ qbs_to_measure (qbs_borel ⨂⇩Q qbs_borel) →⇩M qbs_to_measure (X ⨂⇩Q Y)"
by(rule l_preserves_morphisms)
also have "... = borel ⨂⇩M borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
using rr.lr_sets_ident l_preserves_morphisms by(auto simp add: r_preserves_product[symmetric])
finally show ?thesis .
qed
show ?goal2
unfolding qs2.strength_qbs[OF qbs_Mx_to_X[OF assms(1),of r] fun_cong[OF assms(5)]]
proof(rule pq.qbs_s_finite_measure_eq)
show "distr (k r) (qbs_to_measure (X ⨂⇩Q Y)) (λl. (α r, γ l)) = distr (distr (return borel r ⨂⇩M k r) borel rr.to_real) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ ∘ rr.from_real)"
(is "?lhs = ?rhs")
proof -
have "?lhs = distr (k r) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ ∘ Pair r)"
by(simp add: comp_def)
also have "... = distr (distr (k r) (borel ⨂⇩M borel) (Pair r)) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ)"
by(auto intro!: distr_distr[symmetric])
also have "... = distr (return borel r ⨂⇩M k r) (qbs_to_measure (X ⨂⇩Q Y)) (map_prod α γ)"
proof -
have "return borel r ⨂⇩M k r = distr (k r) (borel ⨂⇩M borel) (λl. (r,l))"
by(auto intro!: measure_eqI simp: sets_pair_measure_cong[OF refl 1(2)] qs2.emeasure_pair_measure_alt' emeasure_distr nn_integral_return[OF _ qs2.measurable_emeasure_Pair'])
thus ?thesis by simp
qed
also have "... = ?rhs"
by(simp add: distr_distr comp_def)
finally show ?thesis .
qed
qed
qed
lemma strength_qbs_morphism[qbs]: "strength_qbs X Y ∈ X ⨂⇩Q monadM_qbs Y →⇩Q monadM_qbs (X ⨂⇩Q Y)"
proof(rule pair_qbs_morphismI)
fix α β
assume h:"α ∈ qbs_Mx X"
"β ∈ qbs_Mx (monadM_qbs Y)"
from rep_qbs_Mx_monadM[OF this(2)] obtain γ k where hb:
"β = (λr. ⟦Y, γ, k r⟧⇩s⇩f⇩i⇩n)" "γ ∈ qbs_Mx Y" "s_finite_kernel borel borel k"
by metis
have "s_finite_kernel borel borel (λr. distr (return borel r ⨂⇩M k r) borel rr.to_real)"
by(auto intro!: s_finite_kernel.distr_s_finite_kernel[where Y="borel ⨂⇩M borel"] s_finite_kernel_pair_measure[OF prob_kernel.s_finite_kernel_prob_kernel] simp:hb prob_kernel_def')
thus "(λr. strength_qbs X Y (α r, β r)) ∈ qbs_Mx (monadM_qbs (X ⨂⇩Q Y))"
using strength_qbs_ab_r[OF h hb(2,3,1)] strength_qbs_ab_r_s_finite[OF h hb(2,3,1)]
by(auto simp: monadM_qbs_Mx qbs_s_finite_def in_Mx_def intro!: exI[where x="map_prod α γ ∘ rr.from_real"] exI[where x="λr. distr (return borel r ⨂⇩M k r) borel rr.to_real"])
qed
lemma bind_qbs_morphism[qbs]: "(⤜) ∈ monadM_qbs X →⇩Q (X ⇒⇩Q monadM_qbs Y) ⇒⇩Q monadM_qbs Y"
proof -
{
fix f s
assume h:"f ∈ X →⇩Q monadM_qbs Y" "s ∈ qbs_space (monadM_qbs X)"
from rep_qbs_space_monadM[OF this(2)] obtain α μ where h':
"s = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n" "qbs_s_finite X α μ" by metis
then interpret qbs_s_finite X α μ by simp
from rep_qbs_Mx_monadM[OF qbs_morphism_Mx[OF h(1) in_Mx]] obtain β k
where hb:"f ∘ α = (λr. ⟦Y, β, k r⟧⇩s⇩f⇩i⇩n)" "β ∈ qbs_Mx Y" "s_finite_kernel borel borel k" by metis
have "join_qbs (distr_qbs ((X ⇒⇩Q monadM_qbs Y) ⨂⇩Q X) (monadM_qbs Y) (λfx. fst fx (snd fx)) (strength_qbs (X ⇒⇩Q monadM_qbs Y) X (f, s))) = s ⤜ f"
using qbs_s_finite_join_qbs[OF qbs_s_finite.distr_qbs_s_finite[OF strength_qbs_s_finite[of f "X ⇒⇩Q monadM_qbs Y",OF h(1) h'(1)] strength_qbs[of f "X ⇒⇩Q monadM_qbs Y",OF h(1) h'(1)] qbs_morphism_eval] qbs_s_finite.distr_qbs[OF strength_qbs_s_finite[of f "X ⇒⇩Q monadM_qbs Y",OF h(1) h'(1)] strength_qbs[of f "X ⇒⇩Q monadM_qbs Y",OF h(1) h'(1)] qbs_morphism_eval] hb(2,3)] hb(1)
by(simp add: bind_qbs[OF h'(1) h(1) hb(2,3,1)] comp_def)
}
thus ?thesis
by(auto intro!: arg_swap_morphism[OF curry_preserves_morphisms[OF qbs_morphism_cong'[of _ "join_qbs ∘ (distr_qbs (exp_qbs X (monadM_qbs Y) ⨂⇩Q X) (monadM_qbs Y) (λfx. (fst fx) (snd fx))) ∘ (strength_qbs (exp_qbs X (monadM_qbs Y)) X)"]]] qbs_morphism_comp distr_qbs_morphism' strength_qbs_morphism join_qbs_morphism qbs_morphism_eval simp: pair_qbs_space)
qed
lemma strength_qbs_law1:
assumes "x ∈ qbs_space (unit_quasi_borel ⨂⇩Q monadM_qbs X)"
shows "snd x = (distr_qbs (unit_quasi_borel ⨂⇩Q X) X snd ∘ strength_qbs unit_quasi_borel X) x"
proof -
obtain α μ where h:
"qbs_s_finite X α μ" "(snd x) = ⟦X, α, μ⟧⇩s⇩f⇩i⇩n"
using rep_qbs_space_monadM[of "snd x" X] assms by (auto simp: pair_qbs_space) metis
have [simp]: "((),snd x) = x"
using SigmaE assms by (auto simp: pair_qbs_space)
show ?thesis
using qbs_s_finite.distr_qbs[OF qbs_s_finite.strength_qbs_s_finite[OF h(1) _ h(2),of "fst x" unit_quasi_borel] qbs_s_finite.strength_qbs[OF h(1) _ h(2)] snd_qbs_morphism]
by(auto simp: comp_def,simp add: h(2))
qed
lemma strength_qbs_law2:
assumes "x ∈ qbs_space ((X ⨂⇩Q Y) ⨂⇩Q monadM_qbs Z)"
shows "(strength_qbs X (Y ⨂⇩Q Z) ∘ (map_prod id (strength_qbs Y Z)) ∘ (λ((x,y),z). (x,(y,z)))) x =
(distr_qbs ((X ⨂⇩Q Y) ⨂⇩Q Z) (X ⨂⇩Q (Y ⨂⇩Q Z)) (λ((x,y),z). (x,(y,z))) ∘ strength_qbs (X ⨂⇩Q Y) Z) x"
(is "?lhs = ?rhs")
proof -
obtain α μ where h:
"qbs_s_finite Z α μ" "snd x = ⟦Z, α, μ⟧⇩s⇩f⇩i⇩n"
using rep_qbs_space_monadM[of "snd x" Z] assms by (auto simp: pair_qbs_space) metis
then have "?lhs = ⟦X ⨂⇩Q Y ⨂⇩Q Z, λr. (fst (fst x), snd (fst x), α r)