# Theory Probability_Space_QuasiBorel

```(*  Title:   Probability_Space_QuasiBorel.thy
Author:  Michikazu Hirata, Yasuhiko Minamide, Tokyo Institute of Technology
*)

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)

(* qbs_prob_eq[1-4] are equivalent. *)
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)"

interpretation qbs_prob_measure_prob_space : prob_space "qbs_prob_measure (s::'a qbs_prob_space)" for s
proof(transfer,auto)
fix X :: "'a quasi_borel"
fix α μ
assume "qbs_prob_eq (X,α,μ) (X,α,μ)"
then interpret qp: qbs_prob X α μ
by(simp add: qbs_prob_eq_def)
show "prob_space (qbs_prob_t_measure (X,α,μ))"
by(simp add: qbs_prob_t_measure_def qp.prob_space_distr)
qed

lemma qbs_prob_measure_space:
"qbs_space (qbs_prob_space_qbs s) = space (qbs_prob_measure s)"
by(transfer,simp add: qbs_prob_t_measure_def)

lemma qbs_prob_measure_sets[measurable_cong]:
"sets (qbs_to_measure (qbs_prob_space_qbs s)) = sets (qbs_prob_measure s)"
by(transfer,simp add: qbs_prob_t_measure_def)

lemma(in qbs_prob) qbs_prob_ennintegral_def:
assumes "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral (qbs_prob_space (X,α,μ)) f = (∫⇧+x. f (α x) ∂ μ)"
by (simp add: assms qbs_prob_ennintegral.abs_eq qbs_prob_t_ennintegral_def)

lemma(in qbs_prob) qbs_prob_ennintegral_def2:
assumes "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral (qbs_prob_space (X,α,μ)) f = integral⇧N (distr μ (qbs_to_measure X) α) f"
using assms by(auto simp add: qbs_prob_ennintegral.abs_eq qbs_prob_t_ennintegral_def qbs_prob_t_measure_def nn_integral_distr)

lemma (in qbs_prob) qbs_prob_ennintegral_not_morphism:
assumes  "f ∉ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral (qbs_prob_space (X,α,μ)) f = 0"
by(simp add: assms qbs_prob_ennintegral.abs_eq qbs_prob_t_ennintegral_def)

lemma qbs_prob_ennintegral_def2:
assumes "qbs_prob_space_qbs s = (X :: 'a quasi_borel)"
and "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral s f = integral⇧N (qbs_prob_measure s) f"
using assms
proof(transfer,auto)
fix X :: "'a quasi_borel" and α μ f
assume "qbs_prob_eq (X,α,μ) (X,α,μ)"
and h:"f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
then interpret qp : qbs_prob X α μ
by(simp add: qbs_prob_eq_def)
show "qbs_prob_t_ennintegral (X, α, μ) f = integral⇧N (qbs_prob_t_measure (X, α, μ)) f"
using qp.qbs_prob_ennintegral_def2[OF h]
by(simp add: qbs_prob_ennintegral.abs_eq qbs_prob_t_measure_def)
qed

lemma(in qbs_prob) qbs_prob_integral_def:
assumes "f ∈ X →⇩Q real_quasi_borel"
shows "qbs_prob_integral (qbs_prob_space (X,α,μ)) f = (∫x. f (α x) ∂ μ)"
by (simp add: assms qbs_prob_integral.abs_eq qbs_prob_t_integral_def)

lemma(in qbs_prob) qbs_prob_integral_def2:
"qbs_prob_integral (qbs_prob_space (X,α,μ)) f = integral⇧L (distr μ (qbs_to_measure X) α) f"
proof -
consider "f ∈ X →⇩Q ℝ⇩Q" | "f ∉ X →⇩Q ℝ⇩Q" by auto
thus ?thesis
proof cases
case h:2
then have "¬ integrable (qbs_prob_measure (qbs_prob_space (X,α,μ))) f"
by auto
thus ?thesis
using h by(simp add: qbs_prob_integral.abs_eq qbs_prob_t_integral_def not_integrable_integral_eq)
qed (auto simp add: qbs_prob_integral.abs_eq qbs_prob_t_integral_def integral_distr )
qed

lemma qbs_prob_integral_def2:
"qbs_prob_integral (s::'a qbs_prob_space) f = integral⇧L (qbs_prob_measure s) f"
proof(transfer,auto)
fix X :: "'a quasi_borel" and μ α f
assume "qbs_prob_eq (X,α,μ) (X,α,μ)"
then interpret qp : qbs_prob X α μ
by(simp add: qbs_prob_eq_def)
show "qbs_prob_t_integral (X,α,μ) f = integral⇧L (qbs_prob_t_measure (X,α,μ)) f"
using qp.qbs_prob_integral_def2
by(simp add: qbs_prob_t_measure_def qbs_prob_integral.abs_eq)
qed

definition qbs_prob_var :: "'a qbs_prob_space ⇒ ('a ⇒ real) ⇒ real" where
"qbs_prob_var s f ≡ qbs_prob_integral s (λx. (f x - qbs_prob_integral s f)⇧2)"

lemma(in qbs_prob) qbs_prob_var_computation:
assumes "f ∈ X →⇩Q real_quasi_borel"
shows "qbs_prob_var (qbs_prob_space (X,α,μ)) f = (∫x. (f (α x) - (∫x. f (α x) ∂ μ))⇧2 ∂ μ)"
proof -
have "(λx. (f x - qbs_prob_integral (qbs_prob_space (X, α, μ)) f)⇧2) ∈ X →⇩Q ℝ⇩Q"
using assms by auto
thus ?thesis
using assms qbs_prob_integral_def[of "λx. (f x - qbs_prob_integral (qbs_prob_space (X,α,μ)) f)⇧2"]
by(simp add: qbs_prob_var_def qbs_prob_integral_def)
qed

lift_definition qbs_integrable :: "['a qbs_prob_space, 'a ⇒ real] ⇒ bool"
is qbs_prob_t_integrable
proof auto
have H:"⋀ (X::'a quasi_borel) Y α β μ ν f.
qbs_prob_eq (X,α,μ) (Y,β,ν) ⟹ qbs_prob_t_integrable (X,α,μ) f ⟹ qbs_prob_t_integrable (Y,β,ν) f"
proof -
fix X Y :: "'a quasi_borel"
fix α β μ ν f
assume H0:"qbs_prob_eq (X, α, μ) (Y, β, ν)"
"qbs_prob_t_integrable (X, α, μ) f"
then interpret qp: pair_qbs_prob X α μ Y β ν
by(auto intro!: pair_qbs_prob.intro simp: qbs_prob_eq_def)
have [measurable]: "f ∈ qbs_to_measure X →⇩M real_borel"
and h: "integrable μ (f ∘ α)"
using H0 by(auto simp: qbs_prob_t_integrable_def)
note [simp] = qbs_prob_eq_dest(3)[OF H0(1)]

show "qbs_prob_t_integrable (Y, β, ν) f"
unfolding qbs_prob_t_integrable_def
proof auto
have "integrable (distr μ (qbs_to_measure X) α) f"
using h by(simp add: comp_def integrable_distr_eq)
hence "integrable (distr ν (qbs_to_measure X) β) f"
using qbs_prob_eq_dest(4)[OF H0(1)] by simp
thus "integrable ν (f ∘ β)"
by(simp add: comp_def integrable_distr_eq)
qed
qed
fix X Y :: "'a quasi_borel"
fix α β μ ν
assume H0:"qbs_prob_eq (X, α, μ) (Y, β, ν)"
then have H1:"qbs_prob_eq (Y, β, ν) (X, α, μ)"
by(auto simp add: qbs_prob_eq_def)
show "qbs_prob_t_integrable (X, α, μ) = qbs_prob_t_integrable (Y, β, ν)"
using H[OF H0] H[OF H1] by auto
qed

lemma(in qbs_prob) qbs_integrable_def:
"qbs_integrable (qbs_prob_space (X, α, μ)) f = (f ∈ X →⇩Q ℝ⇩Q ∧ integrable μ (f ∘ α))"
by (simp add: qbs_integrable.abs_eq qbs_prob_t_integrable_def)

lemma qbs_integrable_morphism:
assumes "qbs_prob_space_qbs s = X"
and "qbs_integrable s f"
shows "f ∈ X →⇩Q ℝ⇩Q"
using assms by(transfer,auto simp: qbs_prob_t_integrable_def)

lemma(in qbs_prob) qbs_integrable_measurable[simp,measurable]:
assumes "qbs_integrable (qbs_prob_space (X,α,μ)) f"
shows "f ∈ qbs_to_measure X →⇩M real_borel"
using assms by(auto simp add: qbs_integrable_def)

lemma qbs_integrable_iff_integrable:
"(qbs_integrable (s::'a qbs_prob_space) f) = (integrable (qbs_prob_measure s) f)"
apply transfer
subgoal for s f
proof(rule prod_cases3[where y=s],simp)
fix X :: "'a quasi_borel"
fix α μ
assume "qbs_prob_eq (X,α,μ) (X,α,μ)"
then interpret qp: qbs_prob X α μ
by(simp add: qbs_prob_eq_def)

show "qbs_prob_t_integrable (X,α,μ) f = integrable (qbs_prob_t_measure (X,α,μ)) f"
(is "?lhs = ?rhs")
using integrable_distr_eq[of α μ "qbs_to_measure X" f]
by(auto simp add: qbs_prob_t_integrable_def qbs_prob_t_measure_def comp_def)
qed
done

lemma(in qbs_prob) qbs_integrable_iff_integrable_distr:
"qbs_integrable (qbs_prob_space (X,α,μ)) f = integrable (distr μ (qbs_to_measure X) α) f"
by(simp add: qbs_integrable_iff_integrable)

lemma(in qbs_prob) qbs_integrable_iff_integrable:
assumes "f ∈  qbs_to_measure X →⇩M real_borel"
shows "qbs_integrable (qbs_prob_space (X,α,μ)) f = integrable μ (λx. f (α x))"
by(auto intro!: integrable_distr_eq[of α μ "qbs_to_measure X" f] simp: assms qbs_integrable_iff_integrable_distr)

lemma qbs_integrable_if_integrable:
assumes "integrable (qbs_prob_measure s) f"
shows "qbs_integrable (s::'a qbs_prob_space) f"
using assms by(simp add: qbs_integrable_iff_integrable)

lemma integrable_if_qbs_integrable:
assumes "qbs_integrable (s::'a qbs_prob_space) f"
shows "integrable (qbs_prob_measure s) f"
using assms by(simp add: qbs_integrable_iff_integrable)

lemma qbs_integrable_iff_bounded:
assumes "qbs_prob_space_qbs s = X"
shows "qbs_integrable s f ⟷ f ∈ X →⇩Q ℝ⇩Q ∧ qbs_prob_ennintegral s (λx. ennreal ¦f x ¦) < ∞"
(is "?lhs = ?rhs")
proof -
obtain α μ where hs:
"qbs_prob X α μ" "s = qbs_prob_space (X,α,μ)"
using rep_qbs_prob_space'[OF assms] by auto
then interpret qp:qbs_prob X α μ by simp
have "?lhs = integrable (distr μ (qbs_to_measure X) α) f"
by (simp add: hs(2) qbs_integrable_iff_integrable)
also have "... = (f ∈ borel_measurable (distr μ (qbs_to_measure X) α) ∧ ((∫⇧+ x. ennreal (norm (f x)) ∂(distr μ (qbs_to_measure X) α)) < ∞))"
by(rule integrable_iff_bounded)
also have "... = ?rhs"
proof -
have [simp]:"f ∈ X →⇩Q ℝ⇩Q ⟹(λx. ennreal ¦f x¦) ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
by auto
have "f ∈ X →⇩Q ℝ⇩Q ⟹ qbs_prob_ennintegral s (λx. ennreal ¦f x¦) = (∫⇧+ x. ennreal (norm (f x)) ∂qbs_prob_measure s)"
using qp.qbs_prob_ennintegral_def2[of "λx. ennreal ¦f x¦"]
by(auto simp: hs(2))
thus ?thesis
by(simp add: hs(2)) fastforce
qed
finally show ?thesis .
qed

lemma qbs_integrable_cong:
assumes "qbs_prob_space_qbs s = X"
"⋀x. x ∈ qbs_space X ⟹ f x = g x"
and "qbs_integrable s f"
shows "qbs_integrable s g"
by (metis Bochner_Integration.integrable_cong assms integrable_if_qbs_integrable qbs_integrable_if_integrable qbs_prob_measure_space)

lemma qbs_integrable_const[simp]:
"qbs_integrable s (λx. c)"
using qbs_integrable_iff_integrable[of s "λx. c"] by simp

lemma qbs_integrable_add[simp]:
assumes "qbs_integrable s f"
and "qbs_integrable s g"
shows "qbs_integrable s (λx. f x + g x)"
using assms qbs_integrable_iff_integrable by blast

lemma qbs_integrable_diff[simp]:
assumes "qbs_integrable s f"
and "qbs_integrable s g"
shows "qbs_integrable s (λx. f x - g x)"
by(rule qbs_integrable_if_integrable[OF Bochner_Integration.integrable_diff[OF integrable_if_qbs_integrable[OF assms(1)] integrable_if_qbs_integrable[OF assms(2)]]])

lemma qbs_integrable_mult_iff[simp]:
"(qbs_integrable s (λx. c * f x)) = (c = 0 ∨ qbs_integrable s f)"
using qbs_integrable_iff_integrable[of s "λx. c * f x"] integrable_mult_left_iff[of "qbs_prob_measure s" c f] qbs_integrable_iff_integrable[of s f]
by simp

lemma qbs_integrable_mult[simp]:
assumes "qbs_integrable s f"
shows "qbs_integrable s (λx. c * f x)"
using assms qbs_integrable_mult_iff by auto

lemma qbs_integrable_abs[simp]:
assumes "qbs_integrable s f"
shows "qbs_integrable s (λx. ¦f x¦)"
by(rule qbs_integrable_if_integrable[OF integrable_abs[OF integrable_if_qbs_integrable[OF assms]]])

lemma qbs_integrable_sq[simp]:
assumes "qbs_integrable s f"
and "qbs_integrable s (λx. (f x)⇧2)"
shows "qbs_integrable s (λx. (f x - c)⇧2)"
by(simp add: comm_ring_1_class.power2_diff,rule qbs_integrable_diff,rule qbs_integrable_add)
(simp_all add: comm_semiring_1_class.semiring_normalization_rules(16)[of 2] assms)

lemma qbs_ennintegral_eq_qbs_integral:
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable s f"
and "⋀x. x ∈ qbs_space X ⟹ 0 ≤ f x"
shows "qbs_prob_ennintegral s (λx. ennreal (f x)) = ennreal (qbs_prob_integral s f)"
using nn_integral_eq_integral[OF integrable_if_qbs_integrable[OF assms(2)]] assms qbs_prob_ennintegral_def2[OF assms(1) qbs_morphism_comp[OF qbs_integrable_morphism[OF assms(1,2)],of ennreal "ℝ⇩Q⇩≥⇩0",simplified comp_def]] measurable_ennreal
by (metis AE_I2 qbs_prob_integral_def2 qbs_prob_measure_space real.standard_borel_r_full_faithful)

lemma qbs_prob_ennintegral_cong:
assumes "qbs_prob_space_qbs s = X"
and "⋀x. x ∈ qbs_space X ⟹ f x = g x"
shows "qbs_prob_ennintegral s f = qbs_prob_ennintegral s g"
proof -
obtain α μ where hs:
"s = qbs_prob_space (X, α, μ)" "qbs_prob X α μ"
using rep_qbs_prob_space'[OF assms(1)] by auto
then interpret qp : qbs_prob  X α μ
by simp
have H1:"f ∘ α = g ∘ α"
using assms(2)
unfolding comp_def apply standard
using assms(2)[of "α _"] by (simp add: qbs_Mx_to_X(2))
consider "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0" | "f ∉ X →⇩Q ℝ⇩Q⇩≥⇩0" by auto
then have "qbs_prob_t_ennintegral (X,α,μ) f = qbs_prob_t_ennintegral (X,α,μ) g"
proof cases
case h:1
then have "g ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
using qbs_morphism_cong[of X f g "ℝ⇩Q⇩≥⇩0"] assms by simp
then show ?thesis
using h H1 by(simp add: qbs_prob_t_ennintegral_def comp_def)
next
case h:2
then have "g ∉ X →⇩Q ℝ⇩Q⇩≥⇩0"
using assms qbs_morphism_cong[of X g f "ℝ⇩Q⇩≥⇩0"] by auto
then show ?thesis
using h by(simp add: qbs_prob_t_ennintegral_def)
qed
thus ?thesis
using hs(1) by (simp add: qbs_prob_ennintegral.abs_eq)
qed

lemma qbs_prob_ennintegral_const:
"qbs_prob_ennintegral (s::'a qbs_prob_space) (λx. c) = c"
using qbs_prob_ennintegral_def2[OF _ qbs_morphism_const[of c "ℝ⇩Q⇩≥⇩0" "qbs_prob_space_qbs s",simplified]]
by (simp add: qbs_prob_measure_prob_space.emeasure_space_1)

lemma qbs_prob_ennintegral_add:
assumes "qbs_prob_space_qbs s = X"
"f ∈ (X::'a quasi_borel) →⇩Q ℝ⇩Q⇩≥⇩0"
and "g ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral s (λx. f x + g x) = qbs_prob_ennintegral s f + qbs_prob_ennintegral s g"
using qbs_prob_ennintegral_def2[of s X "λx. f x + g x"] qbs_prob_ennintegral_def2[OF assms(1,2)] qbs_prob_ennintegral_def2[OF assms(1,3)] assms nn_integral_add[of f "qbs_prob_measure s" g]
by fastforce

lemma qbs_prob_ennintegral_cmult:
assumes "qbs_prob_space_qbs s = X"
and "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0"
shows "qbs_prob_ennintegral s (λx. c * f x) = c * qbs_prob_ennintegral s f"
using qbs_prob_ennintegral_def2[OF assms(1),of "λx. c * f x"] qbs_prob_ennintegral_def2[OF assms(1,2)] nn_integral_cmult[of f "qbs_prob_measure s"] assms
by fastforce

lemma qbs_prob_ennintegral_cmult_noninfty:
assumes "c ≠ ∞"
shows "qbs_prob_ennintegral s (λx. c * f x) = c * qbs_prob_ennintegral s f"
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
consider "f ∈ X →⇩Q ℝ⇩Q⇩≥⇩0" | "f ∉ X →⇩Q ℝ⇩Q⇩≥⇩0" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(auto intro!: qbs_prob_ennintegral_cmult[where X=X] simp: hs(1))
next
case 2
consider "c = 0" | "c ≠ 0 ∧ c ≠ ∞"
using assms by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(simp add: hs qbs_prob_ennintegral.abs_eq qbs_prob_t_ennintegral_def)
next
case h:2
have "(λx. c * f x) ∉ X →⇩Q ℝ⇩Q⇩≥⇩0"
proof(rule ccontr)
assume "¬ (λx. c * f x) ∉ X →⇩Q ℝ⇩Q⇩≥⇩0"
hence 3:"(λx. c * f x) ∈ qbs_to_measure X →⇩M ennreal_borel"
by auto
have "f = (λx. (1/c) *  (c * f x))"
using h by(simp add: divide_eq_1_ennreal ennreal_divide_times mult.assoc mult.commute[of c] mult_divide_eq_ennreal)
also have "... ∈ qbs_to_measure X →⇩M ennreal_borel"
using 3 by simp
finally show False
using 2 by auto
qed
thus ?thesis
using qp.qbs_prob_ennintegral_not_morphism 2
by(simp add: hs(1))
qed
qed
qed

lemma qbs_prob_integral_cong:
assumes "qbs_prob_space_qbs s = X"
and "⋀x. x ∈ qbs_space X ⟹ f x = g x"
shows "qbs_prob_integral s f = qbs_prob_integral s g"
by(simp add: qbs_prob_integral_def2) (metis Bochner_Integration.integral_cong assms(1) assms(2) qbs_prob_measure_space)

lemma qbs_prob_integral_nonneg:
assumes "qbs_prob_space_qbs s = X"
and "⋀x. x ∈ qbs_space X ⟹ 0 ≤ f x"
shows "0 ≤ qbs_prob_integral s f"
using qbs_prob_measure_space[of s] assms
by(simp add: qbs_prob_integral_def2)

lemma qbs_prob_integral_mono:
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable (s :: 'a qbs_prob_space) f"
"qbs_integrable s g"
and "⋀x. x ∈ qbs_space X ⟹ f x ≤ g x"
shows "qbs_prob_integral s f ≤ qbs_prob_integral s g"
using integral_mono[OF integrable_if_qbs_integrable[OF assms(2)] integrable_if_qbs_integrable[OF assms(3)] assms(4)[simplified qbs_prob_measure_space]]
by(simp add: qbs_prob_integral_def2 assms(1) qbs_prob_measure_space[symmetric])

lemma qbs_prob_integral_const:
"qbs_prob_integral (s::'a qbs_prob_space) (λx. c) = c"
by(simp add: qbs_prob_integral_def2 qbs_prob_measure_prob_space.prob_space)

lemma qbs_prob_integral_add:
assumes "qbs_integrable (s::'a qbs_prob_space) f"
and "qbs_integrable s g"
shows "qbs_prob_integral s (λx. f x + g x) = qbs_prob_integral s f + qbs_prob_integral s g"
using Bochner_Integration.integral_add[OF integrable_if_qbs_integrable[OF assms(1)] integrable_if_qbs_integrable[OF assms(2)]]
by(simp add: qbs_prob_integral_def2)

lemma qbs_prob_integral_diff:
assumes "qbs_integrable (s::'a qbs_prob_space) f"
and "qbs_integrable s g"
shows "qbs_prob_integral s (λx. f x - g x) = qbs_prob_integral s f - qbs_prob_integral s g"
using Bochner_Integration.integral_diff[OF integrable_if_qbs_integrable[OF assms(1)] integrable_if_qbs_integrable[OF assms(2)]]
by(simp add: qbs_prob_integral_def2)

lemma qbs_prob_integral_cmult:
"qbs_prob_integral s (λx. c * f x) = c * qbs_prob_integral s f"
by(simp add: qbs_prob_integral_def2)

lemma real_qbs_prob_integral_def:
assumes "qbs_integrable (s::'a qbs_prob_space) f"
shows "qbs_prob_integral s f = enn2real (qbs_prob_ennintegral s (λx. ennreal (f x))) - enn2real (qbs_prob_ennintegral s (λx. ennreal (- f x)))"
using assms
proof(transfer,auto)
fix X :: "'a quasi_borel"
fix α μ f
assume H:"qbs_prob_eq (X,α,μ) (X,α,μ)"
"qbs_prob_t_integrable (X,α,μ) f"
then interpret qp: qbs_prob X α μ
by(simp add: qbs_prob_eq_def)
show "qbs_prob_t_integral (X,α,μ) f = enn2real (qbs_prob_t_ennintegral (X,α,μ) (λx. ennreal (f x))) - enn2real (qbs_prob_t_ennintegral (X,α,μ) (λx. ennreal (- f x)))"
using H(2) real_lebesgue_integral_def[of μ "f ∘ α"]
by(auto simp add: comp_def qbs_prob_t_integrable_def qbs_prob_t_integral_def qbs_prob_t_ennintegral_def)
qed

lemma qbs_prob_var_eq:
assumes "qbs_integrable (s::'a qbs_prob_space) f"
and "qbs_integrable s (λx. (f x)⇧2)"
shows "qbs_prob_var s f = qbs_prob_integral s (λx. (f x)⇧2) - (qbs_prob_integral s f)⇧2"
unfolding qbs_prob_var_def using assms
proof(transfer,auto)
fix X :: "'a quasi_borel"
fix α μ f
assume H:"qbs_prob_eq (X,α,μ) (X,α,μ)"
"qbs_prob_t_integrable (X,α,μ) f"
"qbs_prob_t_integrable (X,α,μ) (λx. (f x)⇧2)"
then interpret qp: qbs_prob X α μ
by(simp add: qbs_prob_eq_def)
show "qbs_prob_t_integral (X,α,μ) (λx. (f x - qbs_prob_t_integral (X,α,μ) f)⇧2) = qbs_prob_t_integral (X,α,μ) (λx. (f x)⇧2) - (qbs_prob_t_integral (X,α,μ) f)⇧2"
using H(2,3) prob_space.variance_eq[of μ "f ∘ α"]
by(auto simp add: qbs_prob_t_integral_def qbs_prob_def qbs_prob_t_integrable_def comp_def qbs_prob_eq_def)
qed

lemma qbs_prob_var_affine:
assumes "qbs_integrable s f"
shows "qbs_prob_var s (λx. a * f x + b) = a⇧2 * qbs_prob_var s f"
(is "?lhs = ?rhs")
proof -
have "?lhs = qbs_prob_integral s (λx. (a * f x + b - (a * qbs_prob_integral s f + b))⇧2)"
using qbs_prob_integral_add[OF qbs_integrable_mult[OF assms,of a] qbs_integrable_const[of s b]]
by (simp add: qbs_prob_integral_cmult qbs_prob_integral_const qbs_prob_var_def)
also have "... = qbs_prob_integral s (λx. (a * f x - a * qbs_prob_integral s f)⇧2)"
by simp
also have "... = qbs_prob_integral s (λx. a⇧2 * (f x - qbs_prob_integral s f)⇧2)"
by (metis power_mult_distrib right_diff_distrib)
also have "... = ?rhs"
by(simp add: qbs_prob_var_def qbs_prob_integral_cmult[of s "a⇧2"])
finally show ?thesis .
qed

lemma qbs_prob_integral_Markov_inequality:
assumes "qbs_prob_space_qbs s = X"
and "qbs_integrable s f"
"⋀x. x ∈ qbs_space X ⟹ 0 ≤ f x"
and "0 < c"
shows "qbs_emeasure s {x ∈ qbs_space X. c ≤ f x} ≤ ennreal (1/c * qbs_prob_integral s f)"
using integral_Markov_inequality[OF integrable_if_qbs_integrable[OF assms(2)] _ assms(4)] assms(3)
by(force simp add: qbs_prob_integral_def2 qbs_prob_measure_space qbs_emeasure_def assms(1) qbs_prob_measure_space[symmetric])

lemma qbs_prob_integral_Markov_inequality':
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable s f"
"⋀x. x ∈ qbs_space (qbs_prob_space_qbs s) ⟹ 0 ≤ f x"
and "0 < c"
shows "qbs_measure s {x ∈ qbs_space (qbs_prob_space_qbs s). c ≤ f x} ≤ (1/c * qbs_prob_integral s f)"
using qbs_prob_integral_Markov_inequality[OF assms] ennreal_le_iff[of "1/c * qbs_prob_integral s f" "qbs_measure s {x ∈ qbs_space (qbs_prob_space_qbs s). c ≤ f x}"] qbs_prob_integral_nonneg[of s X f,OF assms(1,3)] assms(4)
by(simp add: qbs_measure_def qbs_emeasure_def qbs_prob_measure_prob_space.emeasure_eq_measure assms(1))

lemma qbs_prob_integral_Markov_inequality_abs:
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable s f"
and "0 < c"
shows "qbs_emeasure s {x ∈ qbs_space X. c ≤ ¦f x¦} ≤ ennreal (1/c * qbs_prob_integral s (λx. ¦f x¦))"
using qbs_prob_integral_Markov_inequality[OF assms(1) qbs_integrable_abs[OF assms(2)] _ assms(3)]
by(simp add: assms(1))

lemma qbs_prob_integral_Markov_inequality_abs':
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable s f"
and "0 < c"
shows "qbs_measure s {x ∈ qbs_space X. c ≤ ¦f x¦} ≤ (1/c * qbs_prob_integral s (λx. ¦f x¦))"
using qbs_prob_integral_Markov_inequality'[OF assms(1) qbs_integrable_abs[OF assms(2)] _ assms(3)]
by(simp add: assms(1))

lemma qbs_prob_integral_real_Markov_inequality:
assumes "qbs_prob_space_qbs s = ℝ⇩Q"
"qbs_integrable s f"
and "0 < c"
shows "qbs_emeasure s {r. c ≤ ¦f r¦} ≤ ennreal (1/c * qbs_prob_integral s (λx. ¦f x¦))"
using qbs_prob_integral_Markov_inequality_abs[OF assms]
by simp

lemma qbs_prob_integral_real_Markov_inequality':
assumes "qbs_prob_space_qbs s = ℝ⇩Q"
"qbs_integrable s f"
and "0 < c"
shows "qbs_measure s {r. c ≤ ¦f r¦} ≤ 1/c * qbs_prob_integral s (λx. ¦f x¦)"
using qbs_prob_integral_Markov_inequality_abs'[OF assms]
by simp

lemma qbs_prob_integral_Chebyshev_inequality:
assumes "qbs_prob_space_qbs s = X"
"qbs_integrable s f"
"qbs_integrable s (λx. (f x)⇧2)"
and "0 < b"
shows "qbs_measure s {x ∈ qbs_space X. b ≤ ¦f x - qbs_prob_integral s f¦} ≤ 1 / b⇧2 * qbs_prob_var s f"
proof -
have "qbs_integrable s (λx. ¦f x - qbs_prob_integral s f¦⇧2)"
by(simp, rule qbs_integrable_sq[OF assms(2,3)])
moreover have "{x ∈ qbs_space X. b⇧2 ≤ ¦f x - qbs_prob_integral s f¦⇧2} = {x ∈ qbs_space X. b ≤ ¦f x - qbs_prob_integral s f¦}"
by (metis (mono_tags, opaque_lifting) abs_le_square_iff abs_of_nonneg assms(4) less_imp_le power2_abs)
ultimately show ?thesis
using qbs_prob_integral_Markov_inequality'[OF assms(1),of "λx. ¦f x - qbs_prob_integral s f¦^2" "b^2"] assms(4)
by(simp add: qbs_prob_var_def assms(1))
qed

end
```