Theory Measure_as_QuasiBorel_Measure
subsection ‹ Measure as QBS Measure›
theory Measure_as_QuasiBorel_Measure
imports "Pair_QuasiBorel_Measure"
begin
lemma distr_id':
assumes "sets N = sets M"
"f ∈ N →⇩M N"
and "⋀x. x ∈ space N ⟹ f x = x"
shows "distr N M f = N"
proof(rule measure_eqI)
fix A
assume 0:"A ∈ sets (distr N M f)"
then have 1:"A ⊆ space N"
by (auto simp: assms(1) sets.sets_into_space)
have 2:"A ∈ sets M"
using 0 by simp
have 3:"f ∈ N →⇩M M"
using assms(2) by(simp add: measurable_cong_sets[OF _ assms(1)])
have "f -` A ∩ space N = A"
proof -
have "f -` A = A ∪ {x. x ∉ space N ∧ f x ∈ A}"
proof(standard;standard)
fix x
assume h:"x ∈ f -` A"
consider "x ∈ A" | "x ∉ A"
by auto
thus "x ∈ A ∪ {x. x ∉ space N ∧ f x ∈ A}"
proof cases
case 1
then show ?thesis
by simp
next
case 2
have "x ∉ space N"
proof(rule ccontr)
assume "¬ x ∉ space N"
then have "x ∈ space N"
by simp
hence "f x = x"
by(simp add: assms(3))
hence "f x ∉ A"
by(simp add: 2)
thus False
using h by simp
qed
thus ?thesis
using h by simp
qed
next
fix x
show "x ∈ A ∪ {x. x ∉ space N ∧ f x ∈ A} ⟹ x ∈ f -` A"
using 1 assms by auto
qed
thus ?thesis
using "1" by blast
qed
thus "emeasure (distr N M f) A = emeasure N A"
by(simp add: emeasure_distr[OF 3 2])
qed (simp add: assms(1))
text ‹ Every probability measure on a standard Borel space can be represented as a measure on
a quasi-Borel space~\<^cite>‹"Heunen_2017"›, Proposition 23.›
locale standard_borel_prob_space = standard_borel P + p:prob_space P
for P :: "'a measure"
begin
sublocale qbs_prob "measure_to_qbs P" g "distr P real_borel f"
by(auto intro!: qbs_probI p.prob_space_distr)
lift_definition as_qbs_measure :: "'a qbs_prob_space" is
"(measure_to_qbs P, g, distr P real_borel f)"
by simp
lemma as_qbs_measure_retract:
assumes [measurable]:"a ∈ P →⇩M real_borel"
and [measurable]:"b ∈ real_borel →⇩M P"
and [simp]:"⋀x. x ∈ space P ⟹ (b ∘ a) x = x"
shows "qbs_prob (measure_to_qbs P) b (distr P real_borel a)"
"as_qbs_measure = qbs_prob_space (measure_to_qbs P, b, distr P real_borel a)"
proof -
interpret pqp: pair_qbs_prob "measure_to_qbs P" g "distr P real_borel f" "measure_to_qbs P" b "distr P real_borel a"
by(auto intro!: qbs_probI p.prob_space_distr simp: pair_qbs_prob_def)
show "qbs_prob (measure_to_qbs P) b (distr P real_borel a)"
"as_qbs_measure = qbs_prob_space (measure_to_qbs P, b, distr P real_borel a)"
by(auto intro!: pqp.qbs_prob_space_eq
simp: distr_distr distr_id'[OF standard_borel_lr_sets_ident[symmetric]] distr_id'[OF standard_borel_lr_sets_ident[symmetric] _ assms(3)] pqp.qp2.qbs_prob_axioms as_qbs_measure.abs_eq)
qed
lemma measure_as_qbs_measure_qbs:
"qbs_prob_space_qbs as_qbs_measure = measure_to_qbs P"
by transfer auto
lemma measure_as_qbs_measure_image:
"as_qbs_measure ∈ monadP_qbs_Px (measure_to_qbs P)"
by(auto simp: measure_as_qbs_measure_qbs monadP_qbs_Px_def)
lemma as_qbs_measure_as_measure[simp]:
"distr (distr P real_borel f) (qbs_to_measure (measure_to_qbs P)) g = P"
by(auto intro!: distr_id'[OF standard_borel_lr_sets_ident[symmetric]] simp : qbs_prob_t_measure_def distr_distr )
lemma measure_as_qbs_measure_recover:
"qbs_prob_measure as_qbs_measure = P"
by transfer (simp add: qbs_prob_t_measure_def)
end
lemma(in standard_borel) qbs_prob_measure_recover:
assumes "q ∈ monadP_qbs_Px (measure_to_qbs M)"
shows "standard_borel_prob_space.as_qbs_measure (qbs_prob_measure q) = q"
proof -
obtain α μ where hq:
"q = qbs_prob_space (measure_to_qbs M, α, μ)" "qbs_prob (measure_to_qbs M) α μ"
using rep_monadP_qbs_Px[OF assms] by auto
then interpret qp: qbs_prob "measure_to_qbs M" α μ by simp
interpret sp: standard_borel_prob_space "distr μ (qbs_to_measure (measure_to_qbs M)) α"
using qp.in_Mx
by(auto intro!: prob_space.prob_space_distr
simp: standard_borel_prob_space_def standard_borel_sets[OF sets_distr[of μ "qbs_to_measure (measure_to_qbs M)" α,simplified standard_borel_lr_sets_ident,symmetric]])
interpret st: standard_borel "distr μ M α"
by(auto intro!: standard_borel_sets)
have [measurable]:"st.g ∈ real_borel →⇩M M"
using measurable_distr_eq2 st.g_meas by blast
show ?thesis
by(auto intro!: pair_qbs_prob.qbs_prob_space_eq
simp add: hq(1) sp.as_qbs_measure.abs_eq pair_qbs_prob_def qp.qbs_prob_axioms sp.qbs_prob_axioms)
(simp_all add: measure_to_qbs_cong_sets[OF sets_distr[of μ "qbs_to_measure (measure_to_qbs M)" α,simplified standard_borel_lr_sets_ident]])
qed
lemma(in standard_borel_prob_space) ennintegral_as_qbs_ennintegral:
assumes "k ∈ borel_measurable P"
shows "(∫⇧+⇩Q x. k x ∂as_qbs_measure) = (∫⇧+ x. k x ∂P)"
proof -
have 1:"k ∈ measure_to_qbs P →⇩Q ℝ⇩Q⇩≥⇩0"
using assms by auto
thus ?thesis
by(simp add: as_qbs_measure.abs_eq qbs_prob_ennintegral_def2[OF 1])
qed
lemma(in standard_borel_prob_space) integral_as_qbs_integral:
"(∫⇩Q x. k x ∂as_qbs_measure) = (∫ x. k x ∂P)"
by(simp add: as_qbs_measure.abs_eq qbs_prob_integral_def2)
lemma(in standard_borel) measure_with_args_morphism:
assumes [measurable]:"μ ∈ X →⇩M prob_algebra M"
shows "standard_borel_prob_space.as_qbs_measure ∘ μ ∈ measure_to_qbs X →⇩Q monadP_qbs (measure_to_qbs M)"
proof(auto intro!: qbs_morphismI)
fix α
assume h[measurable]:"α ∈ real_borel →⇩M X"
have "∀r. (standard_borel_prob_space.as_qbs_measure ∘ μ ∘ α) r = qbs_prob_space (measure_to_qbs M, g, ((λl. distr (μ l) real_borel f) ∘ α) r)"
proof auto
fix r
interpret sp: standard_borel_prob_space "μ (α r)"
using measurable_space[OF assms measurable_space[OF h]]
by(simp add: standard_borel_prob_space_def space_prob_algebra)
have 1[measurable_cong]: "sets (μ (α r)) = sets M"
using measurable_space[OF assms measurable_space[OF h]] by(simp add: space_prob_algebra)
have 2:"f ∈ μ (α r) →⇩M real_borel" "g ∈ real_borel →⇩M μ (α r)" "⋀x. x ∈ space (μ (α r)) ⟹ (g ∘ f) x = x"
using measurable_space[OF assms measurable_space[OF h]]
by(simp_all add: standard_borel_prob_space_def sets_eq_imp_space_eq[OF 1])
show "standard_borel_prob_space.as_qbs_measure (μ (α r)) = qbs_prob_space (measure_to_qbs M, g, distr (μ (α r)) real_borel f)"
by(simp add: sp.as_qbs_measure_retract[OF 2] measure_to_qbs_cong_sets[OF subprob_measurableD(2)[OF measurable_prob_algebraD[OF assms] measurable_space[OF h]]])
qed
thus "standard_borel_prob_space.as_qbs_measure ∘ μ ∘ α ∈ monadP_qbs_MPx (measure_to_qbs M)"
by(auto intro!: bexI[where x=g] bexI[where x="(λl. distr (μ l) real_borel f) ∘ α"] simp: monadP_qbs_MPx_def in_MPx_def)
qed
lemma(in standard_borel) measure_with_args_recover:
assumes "μ ∈ space X → space (prob_algebra M)"
and "x ∈ space X"
shows "qbs_prob_measure (standard_borel_prob_space.as_qbs_measure (μ x)) = μ x"
using standard_borel_sets[of "μ x"] funcset_mem[OF assms]
by(simp add: standard_borel_prob_space_def space_prob_algebra standard_borel_prob_space.measure_as_qbs_measure_recover)
subsection ‹Example of Probability Measures›
text ‹Probability measures on $\mathbb{R}$ can be represented as probability measures on the quasi-Borel space $\mathbb{R}$.›
subsubsection ‹ Normal Distribution ›
definition normal_distribution :: "real × real ⇒ real measure" where
"normal_distribution μσ = (if 0 < (snd μσ) then density lborel (λx. ennreal (normal_density (fst μσ) (snd μσ) x))
else return lborel 0)"
lemma normal_distribution_measurable:
"normal_distribution ∈ real_borel ⨂⇩M real_borel →⇩M prob_algebra real_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G=borel])
fix A :: "real set"
assume h:"A ∈ sets borel"
have "(λx. emeasure (normal_distribution x) A) = (λx. if 0 < (snd x) then emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A
else emeasure (return lborel 0) A)"
by(auto simp add: normal_distribution_def)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
proof(rule measurable_If)
have [simp]:"(λx. indicat_real A (snd x)) ∈ borel_measurable ((borel ⨂⇩M borel) ⨂⇩M borel)"
proof -
have "(λx. indicat_real A (snd x)) = indicat_real A ∘ snd"
by auto
also have "... ∈ borel_measurable ((borel ⨂⇩M borel) ⨂⇩M borel)"
by (meson borel_measurable_indicator h measurable_comp measurable_snd)
finally show ?thesis .
qed
have "(λx. emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A) = (λx. set_nn_integral lborel A (λr. ennreal (normal_density (fst x) (snd x) r)))"
using h by(auto intro!: emeasure_density)
also have "... = (λx. ∫⇧+r. ennreal (normal_density (fst x) (snd x) r * indicat_real A r)∂lborel)"
by(simp add: nn_integral_set_ennreal)
also have "... ∈ borel_measurable (borel ⨂⇩M borel)"
apply(auto intro!: lborel.borel_measurable_nn_integral
simp: split_beta' measurable_cong_sets[OF sets_pair_measure_cong[OF refl sets_lborel]] )
unfolding normal_density_def
by(rule borel_measurable_times) simp_all
finally show "(λx. emeasure (density lborel (λr. ennreal (normal_density (fst x) (snd x) r))) A) ∈ borel_measurable (borel ⨂⇩M borel)" .
qed simp_all
finally show "(λx. emeasure (normal_distribution x) A) ∈ borel_measurable (borel ⨂⇩M borel)" .
qed (auto simp add: sets.sigma_sets_eq[of borel,simplified] sets.Int_stable prob_space_normal_density normal_distribution_def prob_space_return)
definition qbs_normal_distribution :: "real ⇒ real ⇒ real qbs_prob_space" where
"qbs_normal_distribution ≡ curry (standard_borel_prob_space.as_qbs_measure ∘ normal_distribution)"
lemma qbs_normal_distribution_morphism:
"qbs_normal_distribution ∈ ℝ⇩Q →⇩Q exp_qbs ℝ⇩Q (monadP_qbs ℝ⇩Q)"
unfolding qbs_normal_distribution_def
by(rule curry_preserves_morphisms[OF real.measure_with_args_morphism[OF normal_distribution_measurable,simplified r_preserves_product]])
context
fixes μ σ :: real
assumes sigma:"σ > 0"
begin
interpretation n_dist:standard_borel_prob_space "normal_distribution (μ,σ)"
by(simp add: standard_borel_prob_space_def sigma prob_space_normal_density normal_distribution_def)
lemma qbs_normal_distribution_def2:
"qbs_normal_distribution μ σ = n_dist.as_qbs_measure"
by(simp add: qbs_normal_distribution_def)
lemma qbs_normal_distribution_integral:
"(∫⇩Q x. f x ∂ (qbs_normal_distribution μ σ)) = (∫ x. f x ∂ (density lborel (λx. ennreal (normal_density μ σ x))))"
by(simp add: qbs_normal_distribution_def2 n_dist.integral_as_qbs_integral)
(simp add: normal_distribution_def sigma)
lemma qbs_normal_distribution_expectation:
assumes "f ∈ real_borel →⇩M real_borel"
shows "(∫⇩Q x. f x ∂ (qbs_normal_distribution μ σ)) = (∫ x. normal_density μ σ x * f x ∂ lborel)"
by(simp add: qbs_normal_distribution_integral assms integral_real_density integral_density)
end
subsubsection ‹ Uniform Distribution ›
definition interval_uniform_distribution :: "real ⇒ real ⇒ real measure" where
"interval_uniform_distribution a b ≡ (if a < b then uniform_measure lborel {a<..<b}
else return lborel 0)"
lemma sets_interval_uniform_distribution[measurable_cong]:
"sets (interval_uniform_distribution a b) = borel"
by(simp add: interval_uniform_distribution_def)
lemma interval_uniform_distribution_meaurable:
"(λr. interval_uniform_distribution (fst r) (snd r)) ∈ real_borel ⨂⇩M real_borel →⇩M prob_algebra real_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G="range (λ(a, b). {a<..<b})"])
show "sets real_borel = sigma_sets UNIV (range (λ(a, b). {a<..<b}))"
by(simp add: borel_eq_box)
next
show "Int_stable (range (λ(a, b). {a<..<b::real}))"
by(fastforce intro!: Int_stableI simp: split_beta' image_iff)
next
show "range (λ(a, b). {a<..<b}) ⊆ Pow UNIV"
by simp
next
fix a
show "prob_space (interval_uniform_distribution (fst a) (snd a))"
by(simp add: interval_uniform_distribution_def prob_space_return prob_space_uniform_measure)
next
fix a
show " sets (interval_uniform_distribution (fst a) (snd a)) = sets real_borel"
by(simp add: interval_uniform_distribution_def)
next
fix A
assume "A ∈ range (λ(a, b). {a<..<b::real})"
then obtain a b where ha:"A = {a<..<b}" by auto
consider "b ≤ a" | "a < b" by fastforce
then show "(λx. emeasure (interval_uniform_distribution (fst x) (snd x)) A) ∈ real_borel ⨂⇩M real_borel →⇩M ennreal_borel"
(is "?f ∈ ?meas")
proof cases
case 1
then show ?thesis
by(simp add: ha)
next
case h2:2
have "?f = (λx. if fst x < snd x then ennreal (min (snd x) b - max (fst x) a) / ennreal (snd x - fst x) else indicator A 0)"
proof(standard; auto simp: interval_uniform_distribution_def ha)
fix x y :: real
assume hxy:"x < y"
consider "b ≤ x" | "a ≤ x ∧ x < b" | "x < a ∧ a < y" | "y ≤ a"
using h2 by fastforce
thus "emeasure lborel ({max x a<..<min y b}) / ennreal (y - x) = ennreal (min y b - max x a) / ennreal (y - x)"
by cases (use hxy ennreal_neg h2 in auto)
qed
also have "... ∈ ?meas"
by simp
finally show ?thesis .
qed
qed
definition qbs_interval_uniform_distribution :: "real ⇒ real ⇒ real qbs_prob_space" where
"qbs_interval_uniform_distribution ≡ curry (standard_borel_prob_space.as_qbs_measure ∘ (λr. interval_uniform_distribution (fst r) (snd r)))"
lemma qbs_interval_uniform_distribution_morphism:
"qbs_interval_uniform_distribution ∈ ℝ⇩Q →⇩Q exp_qbs ℝ⇩Q (monadP_qbs ℝ⇩Q)"
unfolding qbs_interval_uniform_distribution_def
using curry_preserves_morphisms[OF real.measure_with_args_morphism[OF interval_uniform_distribution_meaurable,simplified r_preserves_product]] .
context
fixes a b :: real
assumes a_less_than_b:"a < b"
begin
definition "ab_qbs_uniform_distribution ≡ qbs_interval_uniform_distribution a b"
interpretation ab_u_dist: standard_borel_prob_space "interval_uniform_distribution a b"
by(auto intro!: prob_space_uniform_measure simp: interval_uniform_distribution_def standard_borel_prob_space_def prob_space_return)
lemma qbs_interval_uniform_distribution_def2:
"ab_qbs_uniform_distribution = ab_u_dist.as_qbs_measure"
by(simp add: qbs_interval_uniform_distribution_def ab_qbs_uniform_distribution_def)
lemma qbs_uniform_distribution_expectation:
assumes "f ∈ ℝ⇩Q →⇩Q ℝ⇩Q⇩≥⇩0"
shows "(∫⇧+⇩Q x. f x ∂ab_qbs_uniform_distribution) = (∫⇧+x ∈ {a<..<b}. f x ∂lborel) / (b - a)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+x. f x ∂(interval_uniform_distribution a b))"
using assms by(auto simp: qbs_interval_uniform_distribution_def2 intro!:ab_u_dist.ennintegral_as_qbs_ennintegral dest:ab_u_dist.qbs_morphism_dest[simplified measure_to_qbs_cong_sets[OF sets_interval_uniform_distribution]])
also have "... = ?rhs"
using assms
by(auto simp: interval_uniform_distribution_def a_less_than_b intro!:nn_integral_uniform_measure[where M=lborel and S="{a<..<b}",simplified emeasure_lborel_Ioo[OF order.strict_implies_order[OF a_less_than_b]]])
finally show ?thesis .
qed
end
subsubsection ‹ Bernoulli Distribution ›
definition qbs_bernoulli :: "real ⇒ bool qbs_prob_space" where
"qbs_bernoulli ≡ standard_borel_prob_space.as_qbs_measure ∘ (λx. measure_pmf (bernoulli_pmf x))"
lemma bernoulli_measurable:
"(λx. measure_pmf (bernoulli_pmf x)) ∈ real_borel →⇩M prob_algebra bool_borel"
proof(rule measurable_prob_algebra_generated[where Ω=UNIV and G=UNIV],simp_all)
fix A :: "bool set"
have "A ⊆ {True,False}"
by auto
then consider "A = {}" | "A = {True}" | "A = {False}" | "A = {False,True}"
by auto
thus "(λa. emeasure (measure_pmf (bernoulli_pmf a)) A) ∈ borel_measurable borel"
by(cases,simp_all add: emeasure_measure_pmf_finite bernoulli_pmf.rep_eq UNIV_bool[symmetric])
qed (auto simp add: sets_borel_eq_count_space Int_stable_def measure_pmf.prob_space_axioms)
lemma qbs_bernoulli_morphism:
"qbs_bernoulli ∈ ℝ⇩Q →⇩Q monadP_qbs 𝔹⇩Q"
using bool.measure_with_args_morphism[OF bernoulli_measurable]
by (simp add: qbs_bernoulli_def)
lemma qbs_bernoulli_measure:
"qbs_prob_measure (qbs_bernoulli p) = measure_pmf (bernoulli_pmf p)"
using bool.measure_with_args_recover[of "λx. measure_pmf (bernoulli_pmf x)" real_borel p] bernoulli_measurable
by(simp add: measurable_def qbs_bernoulli_def)
context
fixes p :: real
assumes pgeq_0[simp]:"0 ≤ p" and pleq_1[simp]:"p ≤ 1"
begin
lemma qbs_bernoulli_expectation:
"(∫⇩Q x. f x ∂qbs_bernoulli p) = f True * p + f False * (1 - p)"
by(simp add: qbs_prob_integral_def2 qbs_bernoulli_measure)
end
end