Theory Probability_Space_QuasiBorel
section ‹Probability Spaces›
subsection ‹Probability Measures ›
theory Probability_Space_QuasiBorel
imports Exponent_QuasiBorel
begin
subsubsection ‹ Probability Measures ›
type_synonym 'a qbs_prob_t = "'a quasi_borel * (real ⇒ 'a) * real measure"
locale in_Mx =
fixes X :: "'a quasi_borel"
and α :: "real ⇒ 'a"
assumes in_Mx[simp]:"α ∈ qbs_Mx X"
locale qbs_prob = in_Mx X α + real_distribution μ
for X :: "'a quasi_borel" and α and μ
begin
declare prob_space_axioms[simp]
lemma m_in_space_prob_algebra[simp]:
"μ ∈ space (prob_algebra real_borel)"
using space_prob_algebra[of real_borel] by simp
end
locale pair_qbs_probs = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν
for X :: "'a quasi_borel"and α μ and Y :: "'b quasi_borel" and β ν
begin
sublocale pair_prob_space μ ν
by standard
lemma ab_measurable[measurable]:
"map_prod α β ∈ real_borel ⨂⇩M real_borel →⇩M qbs_to_measure (X ⨂⇩Q Y)"
using qbs_morphism_map_prod[of α "ℝ⇩Q" X β "ℝ⇩Q" Y] qp1.in_Mx qp2.in_Mx l_preserves_morphisms[of "ℝ⇩Q ⨂⇩Q ℝ⇩Q" "X ⨂⇩Q Y"]
by(auto simp: qbs_Mx_is_morphisms)
lemma ab_g_in_Mx[simp]:
"map_prod α β ∘ real_real.g ∈ pair_qbs_Mx X Y"
using qbs_closed1_dest[OF qp1.in_Mx] qbs_closed1_dest[OF qp2.in_Mx]
by(auto simp add: pair_qbs_Mx_def comp_def)
sublocale qbs_prob "X ⨂⇩Q Y" "map_prod α β ∘ real_real.g" "distr (μ ⨂⇩M ν) real_borel real_real.f"
by(auto simp: qbs_prob_def in_Mx_def)
end
locale pair_qbs_prob = qp1:qbs_prob X α μ + qp2:qbs_prob Y β ν
for X :: "'a quasi_borel"and α μ and Y :: "'a quasi_borel" and β ν
begin
sublocale pair_qbs_probs
by standard
lemma same_spaces[simp]:
assumes "Y = X"
shows "β ∈ qbs_Mx X"
by(simp add: assms[symmetric])
end
lemma prob_algebra_real_prob_measure:
"p ∈ space (prob_algebra (real_borel)) = real_distribution p"
proof
assume "p ∈ space (prob_algebra real_borel)"
then show "real_distribution p"
unfolding real_distribution_def real_distribution_axioms_def
by(simp add: space_prob_algebra sets_eq_imp_space_eq)
next
assume "real_distribution p"
then interpret rd: real_distribution p .
show "p ∈ space (prob_algebra real_borel)"
by (simp add: space_prob_algebra rd.prob_space_axioms)
qed
lemma qbs_probI:
assumes "α ∈ qbs_Mx X"
and "sets μ = sets borel"
and "prob_space μ"
shows "qbs_prob X α μ"
using assms
by(auto intro!: qbs_prob.intro simp: in_Mx_def real_distribution_def real_distribution_axioms_def)
lemma qbs_empty_not_qbs_prob :"¬ qbs_prob (empty_quasi_borel) f M"
by(simp add: qbs_prob_def in_Mx_def)
definition qbs_prob_eq :: "['a qbs_prob_t, 'a qbs_prob_t] ⇒ bool" where
"qbs_prob_eq p1 p2 ≡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
qbs_prob qbs1 a1 m1 ∧ qbs_prob qbs2 a2 m2 ∧ qbs1 = qbs2 ∧
distr m1 (qbs_to_measure qbs1) a1 = distr m2 (qbs_to_measure qbs2) a2)"
definition qbs_prob_eq2 :: "['a qbs_prob_t, 'a qbs_prob_t] ⇒ bool" where
"qbs_prob_eq2 p1 p2 ≡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
qbs_prob qbs1 a1 m1 ∧ qbs_prob qbs2 a2 m2 ∧ qbs1 = qbs2 ∧
(∀f ∈ qbs1 →⇩Q real_quasi_borel.
(∫x. f (a1 x) ∂ m1) = (∫x. f (a2 x) ∂ m2)))"
definition qbs_prob_eq3 :: "['a qbs_prob_t, 'a qbs_prob_t] ⇒ bool" where
"qbs_prob_eq3 p1 p2 ≡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
(qbs_prob qbs1 a1 m1 ∧ qbs_prob qbs2 a2 m2 ∧ qbs1 = qbs2 ∧
(∀f ∈ qbs1 →⇩Q real_quasi_borel.
(∀ k ∈ qbs_space qbs1. 0 ≤ f k) ⟶
(∫x. f (a1 x) ∂ m1) = (∫x. f (a2 x) ∂ m2))))"
definition qbs_prob_eq4 :: "['a qbs_prob_t, 'a qbs_prob_t] ⇒ bool" where
"qbs_prob_eq4 p1 p2 ≡
(let (qbs1, a1, m1) = p1;
(qbs2, a2, m2) = p2 in
(qbs_prob qbs1 a1 m1 ∧ qbs_prob qbs2 a2 m2 ∧ qbs1 = qbs2 ∧
(∀f ∈ qbs1 →⇩Q ℝ⇩Q⇩≥⇩0.
(∫⇧+x. f (a1 x) ∂ m1) = (∫⇧+x. f (a2 x) ∂ m2))))"
lemma(in qbs_prob) qbs_prob_eq_refl[simp]:
"qbs_prob_eq (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq2_refl[simp]:
"qbs_prob_eq2 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq2_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq3_refl[simp]:
"qbs_prob_eq3 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq3_def qbs_prob_axioms)
lemma(in qbs_prob) qbs_prob_eq4_refl[simp]:
"qbs_prob_eq4 (X,α,μ) (X,α,μ)"
by(simp add: qbs_prob_eq4_def qbs_prob_axioms)
lemma(in pair_qbs_prob) qbs_prob_eq_intro:
assumes "X = Y"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
shows "qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq_def)
lemma(in pair_qbs_prob) qbs_prob_eq2_intro:
assumes "X = Y"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
shows "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq2_def)
lemma(in pair_qbs_prob) qbs_prob_eq3_intro:
assumes "X = Y"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel ⟹ (∀ k ∈ qbs_space X. 0 ≤ f k)
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
shows "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq3_def)
lemma(in pair_qbs_prob) qbs_prob_eq4_intro:
assumes "X = Y"
and "⋀f. f ∈ qbs_to_measure X →⇩M ennreal_borel
⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)"
shows "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(auto simp add: qbs_prob_eq4_def)
lemma qbs_prob_eq_dest:
assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
using assms by(auto simp: qbs_prob_eq_def)
lemma qbs_prob_eq2_dest:
assumes "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
using assms by(auto simp: qbs_prob_eq2_def)
lemma qbs_prob_eq3_dest:
assumes "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel ⟹ (∀ k ∈ qbs_space X. 0 ≤ f k)
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
using assms by(auto simp: qbs_prob_eq3_def)
lemma qbs_prob_eq4_dest:
assumes "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
shows "qbs_prob X α μ"
"qbs_prob Y β ν"
"Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M ennreal_borel
⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)"
using assms by(auto simp: qbs_prob_eq4_def)
definition qbs_prob_t_ennintegral :: "['a qbs_prob_t, 'a ⇒ ennreal] ⇒ ennreal" where
"qbs_prob_t_ennintegral p f ≡
(if f ∈ (fst p) →⇩Q ennreal_quasi_borel
then (∫⇧+x. f (fst (snd p) x) ∂ (snd (snd p))) else 0)"
definition qbs_prob_t_integral :: "['a qbs_prob_t, 'a ⇒ real] ⇒ real" where
"qbs_prob_t_integral p f ≡
(if f ∈ (fst p) →⇩Q ℝ⇩Q
then (∫x. f (fst (snd p) x) ∂ (snd (snd p)))
else 0)"
definition qbs_prob_t_integrable :: "['a qbs_prob_t, 'a ⇒ real] ⇒ bool" where
"qbs_prob_t_integrable p f ≡ f ∈ fst p →⇩Q real_quasi_borel ∧ integrable (snd (snd p)) (f ∘ (fst (snd p)))"
definition qbs_prob_t_measure :: "'a qbs_prob_t ⇒ 'a measure" where
"qbs_prob_t_measure p ≡ distr (snd (snd p)) (qbs_to_measure (fst p)) (fst (snd p))"
lemma qbs_prob_eq_symp:
"symp qbs_prob_eq"
by(simp add: symp_def qbs_prob_eq_def)
lemma qbs_prob_eq_transp:
"transp qbs_prob_eq"
by(simp add: transp_def qbs_prob_eq_def)
quotient_type 'a qbs_prob_space = "'a qbs_prob_t" / partial: qbs_prob_eq
morphisms rep_qbs_prob_space qbs_prob_space
proof(rule part_equivpI)
let ?U = "UNIV :: 'a set"
let ?Uf = "UNIV :: (real ⇒ 'a) set"
let ?f = "(λ_. undefined) :: real ⇒ 'a"
have "qbs_prob (Abs_quasi_borel (?U,?Uf)) ?f (return borel 0)"
proof(auto simp add: qbs_prob_def in_Mx_def)
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 "real_distribution (return borel 0)"
by (simp add: prob_space_return real_distribution_axioms_def real_distribution_def)
qed
thus "∃x :: 'a qbs_prob_t . qbs_prob_eq x x"
unfolding qbs_prob_eq_def
by(auto intro!: exI[where x="(Abs_quasi_borel (?U,?Uf), ?f, return borel 0)"])
qed (simp_all add: qbs_prob_eq_symp qbs_prob_eq_transp)
interpretation qbs_prob_space : quot_type "qbs_prob_eq" "Abs_qbs_prob_space" "Rep_qbs_prob_space"
using Abs_qbs_prob_space_inverse Rep_qbs_prob_space
by(simp add: quot_type_def equivp_implies_part_equivp qbs_prob_space_equivp Rep_qbs_prob_space_inverse Rep_qbs_prob_space_inject) blast
lemma qbs_prob_space_induct:
assumes "⋀X α μ. qbs_prob X α μ ⟹ P (qbs_prob_space (X,α,μ))"
shows "P s"
apply(rule qbs_prob_space.abs_induct)
using assms by(auto simp: qbs_prob_eq_def)
lemma qbs_prob_space_induct':
assumes "⋀X α μ. qbs_prob X α μ ⟹ s = qbs_prob_space (X,α,μ)⟹ P (qbs_prob_space (X,α,μ))"
shows "P s"
by (metis (no_types, lifting) Rep_qbs_prob_space_inverse assms case_prodE qbs_prob_eq_def qbs_prob_space.abs_def qbs_prob_space.rep_prop qbs_prob_space_def)
lemma rep_qbs_prob_space:
"∃X α μ. p = qbs_prob_space (X, α, μ) ∧ qbs_prob X α μ"
by(rule qbs_prob_space.abs_induct,auto simp add: qbs_prob_eq_def)
lemma(in qbs_prob) in_Rep:
"(X, α, μ) ∈ Rep_qbs_prob_space (qbs_prob_space (X,α,μ))"
by (metis mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
lemma(in qbs_prob) if_in_Rep:
assumes "(X',α',μ') ∈ Rep_qbs_prob_space (qbs_prob_space (X,α,μ))"
shows "X' = X"
"qbs_prob X' α' μ'"
"qbs_prob_eq (X,α,μ) (X',α',μ')"
proof -
have h:"X' = X"
by (metis assms mem_Collect_eq qbs_prob_eq_dest(3) qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
have [simp]:"qbs_prob X' α' μ'"
by (metis assms mem_Collect_eq prod_cases3 qbs_prob_eq_dest(2) qbs_prob_space.rep_prop)
have [simp]:"qbs_prob_eq (X,α,μ) (X',α',μ')"
by (metis assms mem_Collect_eq qbs_prob_eq_refl qbs_prob_space.abs_def qbs_prob_space.abs_inverse qbs_prob_space_def)
show "X' = X"
"qbs_prob X' α' μ'"
"qbs_prob_eq (X,α,μ) (X',α',μ')"
by simp_all (simp add: h)
qed
lemma(in qbs_prob) in_Rep_induct:
assumes "⋀Y β ν. (Y,β,ν) ∈ Rep_qbs_prob_space (qbs_prob_space (X,α,μ)) ⟹ P (Y,β,ν)"
shows "P (rep_qbs_prob_space (qbs_prob_space (X,α,μ)))"
unfolding rep_qbs_prob_space_def qbs_prob_space.rep_def
by(rule someI2[where a="(X,α,μ)"]) (use in_Rep assms in auto)
lemma qbs_prob_eq_2_implies_3 :
assumes "qbs_prob_eq2 p1 p2"
shows "qbs_prob_eq3 p1 p2"
using assms by(auto simp: qbs_prob_eq2_def qbs_prob_eq3_def)
lemma qbs_prob_eq_3_implies_1 :
assumes "qbs_prob_eq3 (p1 :: 'a qbs_prob_t) p2"
shows "qbs_prob_eq p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq3_def)
note [simp] = qbs_prob_eq3_dest(3)[OF h]
show "qbs_prob_eq (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq_intro)
show "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
proof(rule measure_eqI)
fix U
assume hu:"U ∈ sets (distr μ (qbs_to_measure X) α)"
have "measure (distr μ (qbs_to_measure X) α) U = measure (distr ν (qbs_to_measure X) β) U"
(is "?lhs = ?rhs")
proof -
have "?lhs = measure μ (α -` U ∩ space μ)"
by(rule measure_distr) (use hu in simp_all)
also have "... = integral⇧L μ (indicat_real (α -` U))"
by simp
also have "... = (∫x. indicat_real U (α x) ∂μ)"
using indicator_vimage[of α U] Bochner_Integration.integral_cong[of μ _ "indicat_real (α -` U)" "λx. indicat_real U (α x)"]
by auto
also have "... = (∫x. indicat_real U (β x) ∂ν)"
using qbs_prob_eq3_dest(4)[OF h,of "indicat_real U"] hu
by simp
also have "... = integral⇧L ν (indicat_real (β -` U))"
using indicator_vimage[of β U,symmetric] Bochner_Integration.integral_cong[of ν _ "λx. indicat_real U (β x)" "indicat_real (β -` U)"]
by blast
also have "... = measure ν (β -` U ∩ space ν)"
by simp
also have "... = ?rhs"
by(rule measure_distr[symmetric]) (use hu in simp_all)
finally show ?thesis .
qed
thus "emeasure (distr μ (qbs_to_measure X) α) U = emeasure (distr ν (qbs_to_measure X) β) U"
using qp.qp2.finite_measure_distr[of β] qp.qp1.finite_measure_distr[of α]
by(simp add: finite_measure.emeasure_eq_measure)
qed simp
qed simp
qed
lemma qbs_prob_eq_1_implies_2 :
assumes "qbs_prob_eq p1 (p2 :: 'a qbs_prob_t)"
shows "qbs_prob_eq2 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def)
note [simp] = qbs_prob_eq_dest(3)[OF h]
show "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq2_intro)
fix f :: "'a ⇒ real"
assume [measurable]:"f ∈ borel_measurable (qbs_to_measure X)"
show "(∫r. f (α r) ∂ μ) = (∫r. f (β r) ∂ ν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫x. f x ∂(distr μ (qbs_to_measure X) α))"
by(simp add: Bochner_Integration.integral_distr[symmetric])
also have "... = (∫x. f x ∂(distr ν (qbs_to_measure X) β))"
by(simp add: qbs_prob_eq_dest(4)[OF h])
also have "... = ?rhs"
by(simp add: Bochner_Integration.integral_distr)
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_1_implies_4 :
assumes "qbs_prob_eq p1 p2"
shows "qbs_prob_eq4 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def)
note [simp] = qbs_prob_eq_dest(3)[OF h]
show "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq4_intro)
fix f ::"'a ⇒ ennreal"
assume [measurable]:"f ∈ borel_measurable (qbs_to_measure X)"
show "(∫⇧+ x. f (α x) ∂μ) = (∫⇧+ x. f (β x) ∂ν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = integral⇧N (distr μ (qbs_to_measure X) α) f"
by(simp add: nn_integral_distr)
also have "... = integral⇧N (distr ν (qbs_to_measure X) β) f"
by(simp add: qbs_prob_eq_dest(4)[OF h])
also have "... = ?rhs"
by(simp add: nn_integral_distr)
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_4_implies_3 :
assumes "qbs_prob_eq4 p1 p2"
shows "qbs_prob_eq3 p1 p2"
proof(rule prod_cases3[where y=p1],rule prod_cases3[where y=p2],simp)
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume "p1 = (X,α,μ)" "p2 = (Y,β,ν)"
then have h:"qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using assms by simp
then interpret qp : pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq4_def)
note [simp] = qbs_prob_eq4_dest(3)[OF h]
show "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
proof(rule qp.qbs_prob_eq3_intro)
fix f :: "'a ⇒ real"
assume [measurable]:"f ∈ borel_measurable (qbs_to_measure X)"
and h': "∀k∈qbs_space X. 0 ≤ f k"
show "(∫ x. f (α x) ∂μ) = (∫ x. f (β x) ∂ν)"
(is "?lhs = ?rhs")
proof -
have "?lhs = enn2real (∫⇧+ x. ennreal (f (α x)) ∂μ)"
using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (α x))"] qbs_Mx_to_X(2))
also have "... = enn2real (∫⇧+ x. (ennreal ∘ f) (α x) ∂μ)"
by simp
also have "... = enn2real (∫⇧+ x. (ennreal ∘ f) (β x) ∂ν)"
using qbs_prob_eq4_dest(4)[OF h,of "ennreal ∘ f"] by simp
also have "... = enn2real (∫⇧+ x. ennreal (f (β x)) ∂ν)"
by simp
also have "... = ?rhs"
using h' by(auto simp: integral_eq_nn_integral[where f="(λx. f (β x))"] qbs_Mx_to_X(2))
finally show ?thesis .
qed
qed simp
qed
lemma qbs_prob_eq_equiv12 :
"qbs_prob_eq = qbs_prob_eq2"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv13 :
"qbs_prob_eq = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv14 :
"qbs_prob_eq = qbs_prob_eq4"
using qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3 qbs_prob_eq_1_implies_2
by blast
lemma qbs_prob_eq_equiv23 :
"qbs_prob_eq2 = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_eq_equiv24 :
"qbs_prob_eq2 = qbs_prob_eq4"
using qbs_prob_eq_2_implies_3 qbs_prob_eq_4_implies_3 qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_1_implies_2
by blast
lemma qbs_prob_eq_equiv34:
"qbs_prob_eq3 = qbs_prob_eq4"
using qbs_prob_eq_3_implies_1 qbs_prob_eq_1_implies_4 qbs_prob_eq_4_implies_3
by blast
lemma qbs_prob_eq_equiv31 :
"qbs_prob_eq = qbs_prob_eq3"
using qbs_prob_eq_1_implies_2 qbs_prob_eq_2_implies_3 qbs_prob_eq_3_implies_1
by blast
lemma qbs_prob_space_eq:
assumes "qbs_prob_eq (X,α,μ) (Y,β,ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using Quotient3_rel[OF Quotient3_qbs_prob_space] assms
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq:
assumes "Y = X"
and "distr μ (qbs_to_measure X) α = distr ν (qbs_to_measure X) β"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_intro qbs_prob_space_eq by auto
lemma(in pair_qbs_prob) qbs_prob_space_eq2:
assumes "Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using qbs_prob_space_eq assms qbs_prob_eq_2_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq2_intro qbs_prob_eq_dest(4)
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq3:
assumes "Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M real_borel ⟹ (∀k∈ qbs_space X. 0 ≤ f k)
⟹ (∫x. f (α x) ∂ μ) = (∫x. f (β x) ∂ ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_3_implies_1[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_eq3_intro qbs_prob_space_eq qbs_prob_eq_dest(4)
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq4:
assumes "Y = X"
and "⋀f. f ∈ qbs_to_measure X →⇩M ennreal_borel
⟹ (∫⇧+x. f (α x) ∂ μ) = (∫⇧+x. f (β x) ∂ ν)"
shows "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
using assms qbs_prob_eq_4_implies_3[of "(X,α,μ)" "(Y,β,ν)"] qbs_prob_space_eq3[OF assms(1)] qbs_prob_eq3_dest(4) qbs_prob_eq4_intro
by blast
lemma(in pair_qbs_prob) qbs_prob_space_eq_inverse:
assumes "qbs_prob_space (X,α,μ) = qbs_prob_space (Y,β,ν)"
shows "qbs_prob_eq (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq2 (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq3 (X,α,μ) (Y,β,ν)"
and "qbs_prob_eq4 (X,α,μ) (Y,β,ν)"
using Quotient3_rel[OF Quotient3_qbs_prob_space,of "(X, α, μ)" "(Y,β,ν)",simplified] assms qp1.qbs_prob_axioms qp2.qbs_prob_axioms
by(simp_all add: qbs_prob_eq_equiv13[symmetric] qbs_prob_eq_equiv12[symmetric] qbs_prob_eq_equiv14[symmetric])
lift_definition qbs_prob_space_qbs :: "'a qbs_prob_space ⇒ 'a quasi_borel"
is fst by(auto simp add: qbs_prob_eq_def)
lemma(in qbs_prob) qbs_prob_space_qbs_computation[simp]:
"qbs_prob_space_qbs (qbs_prob_space (X,α,μ)) = X"
by(simp add: qbs_prob_space_qbs.abs_eq)
lemma rep_qbs_prob_space':
assumes "qbs_prob_space_qbs s = X"
shows "∃α μ. s = qbs_prob_space (X,α,μ) ∧ qbs_prob X α μ"
proof -
obtain X' α μ where hs:
"s = qbs_prob_space (X', α, μ)" "qbs_prob X' α μ"
using rep_qbs_prob_space[of s] by auto
then interpret qp:qbs_prob X' α μ
by simp
show ?thesis
using assms hs(2) by(auto simp add: hs(1))
qed
lift_definition qbs_prob_ennintegral :: "['a qbs_prob_space, 'a ⇒ ennreal] ⇒ ennreal"
is qbs_prob_t_ennintegral
by(auto simp add: qbs_prob_t_ennintegral_def qbs_prob_eq_equiv14 qbs_prob_eq4_def)
lift_definition qbs_prob_integral :: "['a qbs_prob_space, 'a ⇒ real] ⇒ real"
is qbs_prob_t_integral
by(auto simp add: qbs_prob_eq_equiv12 qbs_prob_t_integral_def qbs_prob_eq2_def)
syntax
"_qbs_prob_ennintegral" :: "pttrn ⇒ ennreal ⇒ 'a qbs_prob_space ⇒ ennreal" ("∫⇧+⇩Q((2 _./ _)/ ∂_)" [60,61] 110)
translations
"∫⇧+⇩Q x. f ∂p" ⇌ "CONST qbs_prob_ennintegral p (λx. f)"
syntax
"_qbs_prob_integral" :: "pttrn ⇒ real ⇒ 'a qbs_prob_space ⇒ real" ("∫⇩Q((2 _./ _)/ ∂_)" [60,61] 110)
translations
"∫⇩Q x. f ∂p" ⇌ "CONST qbs_prob_integral p (λx. f)"
text ‹ We define the function ‹l⇩X ∈ L(P(X)) →⇩M G(X)›. ›
lift_definition qbs_prob_measure :: "'a qbs_prob_space ⇒ 'a measure"
is qbs_prob_t_measure
by(auto simp add: qbs_prob_eq_def qbs_prob_t_measure_def)
declare [[coercion qbs_prob_measure]]
lemma(in qbs_prob) qbs_prob_measure_computation[simp]:
"qbs_prob_measure (qbs_prob_space (X,α,μ)) = distr μ (qbs_to_measure X) α"
by (simp add: qbs_prob_measure.abs_eq qbs_prob_t_measure_def)
definition qbs_emeasure ::"'a qbs_prob_space ⇒ 'a set ⇒ ennreal" where
"qbs_emeasure s ≡ emeasure (qbs_prob_measure s)"
lemma(in qbs_prob) qbs_emeasure_computation[simp]:
assumes "U ∈ sets (qbs_to_measure X)"
shows "qbs_emeasure (qbs_prob_space (X,α,μ)) U = emeasure μ (α -` U)"
by(simp add: qbs_emeasure_def emeasure_distr[OF _ assms])
definition qbs_measure ::"'a qbs_prob_space ⇒ 'a set ⇒ real" where
"qbs_measure s ≡ measure (qbs_prob_measure s)"