Theory Measure_QuasiBorel_Adjunction
subsection ‹Relation to Measurable Spaces›
theory Measure_QuasiBorel_Adjunction
imports "QuasiBorel"
begin
text ‹ We construct the adjunction between \textbf{Meas} and \textbf{QBS},
where \textbf{Meas} is the category of measurable spaces and measurable functions
and \textbf{QBS} is the category of quasi-Borel spaces and morphisms.›
subsubsection ‹ The Functor $R$ ›
definition measure_to_qbs :: "'a measure ⇒ 'a quasi_borel" where
"measure_to_qbs X ≡ Abs_quasi_borel (space X, real_borel →⇩M X)"
lemma R_Mx_correct: "real_borel →⇩M X ⊆ UNIV → space X"
by (simp add: measurable_space subsetI)
lemma R_qbs_closed1: "qbs_closed1 (real_borel →⇩M X)"
by (simp add: qbs_closed1_def)
lemma R_qbs_closed2: "qbs_closed2 (space X) (real_borel →⇩M X)"
by (simp add: qbs_closed2_def)
lemma R_qbs_closed3: "qbs_closed3 (real_borel →⇩M (X :: 'a measure))"
proof(rule qbs_closed3I)
fix P::"real ⇒ nat"
fix Fi::"nat ⇒ real ⇒ 'a"
assume h:"⋀i. P -` {i} ∈ sets real_borel"
"⋀i. Fi i ∈ real_borel →⇩M X"
show "(λr. Fi (P r) r) ∈ real_borel →⇩M X"
proof(rule measurableI)
fix x
assume "x ∈ space real_borel"
then show "Fi (P x) x ∈ space X"
using h(2) measurable_space[of "Fi (P x)" real_borel X x]
by auto
next
fix A
assume h':"A ∈ sets X"
have "(λr. Fi (P r) r) -` A = (⋃i::nat. ((Fi i -` A) ∩ (P -` {i})))"
by auto
also have "... ∈ sets real_borel"
using sets.Int measurable_sets[OF h(2) h'] h(1)
by(auto intro!: countable_Un_Int(1))
finally show "(λr. Fi (P r) r) -` A ∩ space real_borel ∈ sets real_borel"
by simp
qed
qed
lemma R_correct[simp]: "Rep_quasi_borel (measure_to_qbs X) = (space X, real_borel →⇩M X)"
unfolding measure_to_qbs_def
by (rule Abs_quasi_borel_inverse) (simp add: R_Mx_correct R_qbs_closed1 R_qbs_closed2 R_qbs_closed3)
lemma qbs_space_R[simp]: "qbs_space (measure_to_qbs X) = space X"
by (simp add: qbs_space_def)
lemma qbs_Mx_R[simp]: "qbs_Mx (measure_to_qbs X) = real_borel →⇩M X"
by (simp add: qbs_Mx_def)
text ‹ The following lemma says that @{term measure_to_qbs} is a functor from \textbf{Meas} to \textbf{QBS}. ›
lemma r_preserves_morphisms:
"X →⇩M Y ⊆ (measure_to_qbs X) →⇩Q (measure_to_qbs Y)"
by(auto intro!: qbs_morphismI)
subsubsection ‹ The Functor $L$ ›
definition sigma_Mx :: "'a quasi_borel ⇒ 'a set set" where
"sigma_Mx X ≡ {U ∩ qbs_space X |U. ∀α∈qbs_Mx X. α -` U ∈ sets real_borel}"
definition qbs_to_measure :: "'a quasi_borel ⇒ 'a measure" where
"qbs_to_measure X ≡ Abs_measure (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
lemma measure_space_L: "measure_space (qbs_space X) (sigma_Mx X) (λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
unfolding measure_space_def
proof auto
show "sigma_algebra (qbs_space X) (sigma_Mx X)"
proof(rule sigma_algebra.intro)
show "algebra (qbs_space X) (sigma_Mx X)"
proof
have "∀ U ∈ sigma_Mx X. U ⊆ qbs_space X"
using sigma_Mx_def subset_iff by fastforce
thus "sigma_Mx X ⊆ Pow (qbs_space X)" by auto
next
show "{} ∈ sigma_Mx X"
unfolding sigma_Mx_def by auto
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)" by auto
from pa pb have [simp]:"∀α∈qbs_Mx X. α -` (Ua ∩ Ub) ∈ sets real_borel"
by auto
from this pa pb sigma_Mx_def have [simp]:"(Ua ∩ Ub) ∩ qbs_space X ∈ sigma_Mx X" by blast
from pa pb have [simp]:"A ∩ B = (Ua ∩ Ub) ∩ qbs_space X" by auto
thus "A ∩ B ∈ sigma_Mx X" by simp
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)" by auto
from pa pb have [simp]:"A - B = (Ua ∩ -Ub) ∩ qbs_space X" by auto
from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∩ -Ub) ∈ sets real_borel"
by (metis Diff_Compl double_compl sets.Diff vimage_Compl vimage_Int)
hence 1:"A - B ∈ sigma_Mx X"
using sigma_Mx_def ‹A - B = Ua ∩ - Ub ∩ qbs_space X› by blast
show "∃C⊆sigma_Mx X. finite C ∧ disjoint C ∧ A - B = ⋃ C"
proof
show "{A - B} ⊆sigma_Mx X ∧ finite {A-B} ∧ disjoint {A-B} ∧ A - B = ⋃ {A-B}"
using 1 by auto
qed
next
fix A
fix B
assume "A ∈ sigma_Mx X"
"B ∈ sigma_Mx X"
then have "∃ Ua. A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)"
by (simp add: sigma_Mx_def)
then obtain Ua where pa:"A = Ua ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ua ∈ sets real_borel)" by auto
have "∃ Ub. B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)"
using ‹B ∈ sigma_Mx X› sigma_Mx_def by auto
then obtain Ub where pb:"B = Ub ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ub ∈ sets real_borel)" by auto
from pa pb have "A ∪ B = (Ua ∪ Ub) ∩ qbs_space X" by auto
from pa pb have "∀α∈qbs_Mx X. α -`(Ua ∪ Ub) ∈ sets real_borel" by auto
then show "A ∪ B ∈ sigma_Mx X"
unfolding sigma_Mx_def
using ‹A ∪ B = (Ua ∪ Ub) ∩ qbs_space X› by blast
next
have "∀α∈qbs_Mx X. α -` (UNIV) ∈ sets real_borel"
by simp
thus "qbs_space X ∈ sigma_Mx X"
unfolding sigma_Mx_def
by blast
qed
next
show "sigma_algebra_axioms (sigma_Mx X)"
unfolding sigma_algebra_axioms_def
proof(auto)
fix A :: "nat ⇒ _"
assume 1:"range A ⊆ sigma_Mx X"
then have 2:"∀i. ∃Ui. A i = Ui ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` Ui ∈ sets real_borel)"
unfolding sigma_Mx_def by auto
then have "∃ U :: nat ⇒ _. ∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets real_borel)"
by (rule choice)
from this obtain U where pu:"∀i. A i = U i ∩ qbs_space X ∧ (∀α∈qbs_Mx X. α -` (U i) ∈ sets real_borel)"
by auto
hence "∀α∈qbs_Mx X. α -` (⋃ (range U)) ∈ sets real_borel"
by (simp add: countable_Un_Int(1) vimage_UN)
from pu have "⋃ (range A) = (⋃i::nat. (U i ∩ qbs_space X))" by blast
hence "⋃ (range A) = ⋃ (range U) ∩ qbs_space X" by auto
thus "⋃ (range A) ∈ sigma_Mx X"
using sigma_Mx_def ‹∀α∈qbs_Mx X. α -` ⋃ (range U) ∈ sets real_borel› by blast
qed
qed
next
show "countably_additive (sigma_Mx X) (λA. if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞)"
proof(rule countably_additiveI)
fix A :: "nat ⇒ _"
assume h:"range A ⊆ sigma_Mx X"
"⋃ (range A) ∈ sigma_Mx X"
consider "⋃ (range A) = {}" | "⋃ (range A) ≠ {}"
by auto
then show "(∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) =
(if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
proof cases
case 1
then have "⋀i. A i = {}"
by simp
thus ?thesis
by(simp add: 1)
next
case 2
then obtain j where hj:"A j ≠ {}"
by auto
have "(∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof -
have hsum:"⋀N f. sum f {..<N} ≤ (∑n. (f n :: ennreal))"
by (simp add: sum_le_suminf)
have hsum':"⋀P f. (∃j. j ∈ P ∧ f j = (∞ :: ennreal)) ⟹ finite P ⟹ sum f P = ∞"
by auto
have h1:"(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof(rule hsum')
show "∃ja. ja ∈ {..<j + 1} ∧ (if A ja = {} then 0 else if A ja ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
proof(rule exI[where x=j],rule conjI)
have "A j ∈ sigma_Mx X"
using h(1) by auto
then show "(if A j = {} then 0 else if A j ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
using hj by simp
qed simp
qed simp
have "(∑i<j+1. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else ∞) ≤ (∑i. if A i = {} then 0 else if A i ∈ - sigma_Mx X then 0 else (∞ :: ennreal))"
by(rule hsum)
thus ?thesis
by(simp only: h1) (simp add: top.extremum_unique)
qed
moreover have "(if ⋃ (range A) = {} then 0 else if ⋃ (range A) ∈ - sigma_Mx X then 0 else ∞) = (∞ :: ennreal)"
using 2 h(2) by simp
ultimately show ?thesis
by simp
qed
qed
qed(simp add: positive_def)
lemma L_correct[simp]:"Rep_measure (qbs_to_measure X) = (qbs_space X, sigma_Mx X, λA. (if A = {} then 0 else if A ∈ - sigma_Mx X then 0 else ∞))"
unfolding qbs_to_measure_def
by(auto intro!: Abs_measure_inverse simp: measure_space_L)
lemma space_L[simp]: "space (qbs_to_measure X) = qbs_space X"
by (simp add: space_def)
lemma sets_L[simp]: "sets (qbs_to_measure X) = sigma_Mx X"
by (simp add: sets_def)
lemma emeasure_L[simp]: "emeasure (qbs_to_measure X) = (λA. if A = {} ∨ A ∉ sigma_Mx X then 0 else ∞)"
by(auto simp: emeasure_def)
lemma qbs_Mx_sigma_Mx_contra:
assumes "qbs_space X = qbs_space Y"
and "qbs_Mx X ⊆ qbs_Mx Y"
shows "sigma_Mx Y ⊆ sigma_Mx X"
using assms by(auto simp: sigma_Mx_def)
text ‹ The following lemma says that @{term qbs_to_measure} is a functor from \textbf{QBS} to \textbf{Meas}. ›
lemma l_preserves_morphisms:
"X →⇩Q Y ⊆ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
proof(auto)
fix f
assume h:"f ∈ X →⇩Q Y"
show "f ∈ (qbs_to_measure X) →⇩M (qbs_to_measure Y)"
proof(rule measurableI)
fix x
assume "x ∈ space (qbs_to_measure X)"
then show "f x ∈ space (qbs_to_measure Y)"
using h by auto
next
fix A
assume "A ∈ sets (qbs_to_measure Y)"
then obtain Ua where pa:"A = Ua ∩ qbs_space Y ∧ (∀α∈qbs_Mx Y. α -` Ua ∈ sets real_borel)"
by (auto simp: sigma_Mx_def)
have "∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y"
"∀α∈ qbs_Mx X. α -` (f -` (qbs_space Y)) = UNIV"
using h by auto
hence "∀α∈qbs_Mx X. α -` (f -` A) = α -` (f -` Ua)"
by (simp add: pa)
from pa this qbs_morphism_def have "∀α∈qbs_Mx X. α -` (f -` A) ∈ sets real_borel"
by (simp add: vimage_comp ‹∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y›)
thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
using sigma_Mx_def by auto
qed
qed
abbreviation "qbs_borel ≡ measure_to_qbs borel"
declare [[coercion measure_to_qbs]]
abbreviation real_quasi_borel :: "real quasi_borel" ("ℝ⇩Q") where
"real_quasi_borel ≡ qbs_borel"
abbreviation nat_quasi_borel :: "nat quasi_borel" ("ℕ⇩Q") where
"nat_quasi_borel ≡ qbs_borel"
abbreviation ennreal_quasi_borel :: "ennreal quasi_borel" ("ℝ⇩Q⇩≥⇩0") where
"ennreal_quasi_borel ≡ qbs_borel"
abbreviation bool_quasi_borel :: "bool quasi_borel" ("𝔹⇩Q") where
"bool_quasi_borel ≡ qbs_borel"
lemma qbs_Mx_is_morphisms:
"qbs_Mx X = real_quasi_borel →⇩Q X"
proof(auto)
fix α
assume "α ∈ qbs_Mx X"
then have "α ∈ UNIV → qbs_space X ∧ (∀ f ∈ real_borel →⇩M real_borel. α ∘ f ∈ qbs_Mx X)"
by fastforce
thus "α ∈ real_quasi_borel →⇩Q X"
by(simp add: qbs_morphism_def)
next
fix α
assume "α ∈ real_quasi_borel →⇩Q X"
have "id ∈ qbs_Mx real_quasi_borel" by simp
then have "α ∘ id ∈ qbs_Mx X"
using ‹α ∈ real_quasi_borel →⇩Q X› qbs_morphism_def[of real_quasi_borel X]
by blast
then show "α ∈ qbs_Mx X" by simp
qed
lemma qbs_Mx_subset_of_measurable:
"qbs_Mx X ⊆ real_borel →⇩M qbs_to_measure X"
proof
fix α
assume "α ∈ qbs_Mx X"
show "α ∈ real_borel →⇩M qbs_to_measure X"
proof(rule measurableI)
fix x
show "α x ∈ space (qbs_to_measure X)"
using qbs_decomp ‹α ∈ qbs_Mx X› by auto
next
fix A
assume "A ∈ sets (qbs_to_measure X)"
then have "α -`(qbs_space X) = UNIV"
using ‹α ∈ qbs_Mx X› qbs_decomp by auto
then show "α -` A ∩ space real_borel ∈ sets real_borel"
using ‹α ∈ qbs_Mx X› ‹A ∈ sets (qbs_to_measure X)›
by(auto simp add: sigma_Mx_def)
qed
qed
lemma L_max_of_measurables:
assumes "space M = qbs_space X"
and "qbs_Mx X ⊆ real_borel →⇩M M"
shows "sets M ⊆ sets (qbs_to_measure X)"
proof
fix U
assume "U ∈ sets M"
from sets.sets_into_space[OF this] in_mono[OF assms(2)] measurable_sets_borel[OF _ this]
show "U ∈ sets (qbs_to_measure X)"
using assms(1)
by(auto intro!: exI[where x=U] simp: sigma_Mx_def)
qed
lemma qbs_Mx_are_measurable[simp,measurable]:
assumes "α ∈ qbs_Mx X"
shows "α ∈ real_borel →⇩M qbs_to_measure X"
using assms qbs_Mx_subset_of_measurable by auto
lemma measure_to_qbs_cong_sets:
assumes "sets M = sets N"
shows "measure_to_qbs M = measure_to_qbs N"
by(rule qbs_eqI) (simp add: measurable_cong_sets[OF _ assms])
lemma lr_sets[simp,measurable_cong]:
"sets X ⊆ sets (qbs_to_measure (measure_to_qbs X))"
proof auto
fix U
assume "U ∈ sets X"
then have "U ∩ space X = U" by simp
moreover have "∀α∈real_borel →⇩M X. α -` U ∈ sets real_borel"
using ‹U ∈ sets X› by(auto simp add: measurable_def)
ultimately show "U ∈ sigma_Mx (measure_to_qbs X)"
by(auto simp add: sigma_Mx_def)
qed
lemma(in standard_borel) standard_borel_lr_sets_ident[simp, measurable_cong]:
"sets (qbs_to_measure (measure_to_qbs M)) = sets M"
proof auto
fix V
assume "V ∈ sigma_Mx (measure_to_qbs M)"
then obtain U where H2: "V = U ∩ space M ∧ (∀α∈real_borel →⇩M M. α -` U ∈ sets real_borel)"
by(auto simp: sigma_Mx_def)
hence "g -` V = g -` (U ∩ space M)" by auto
have "... = g -` U" using g_meas by(auto simp add: measurable_def)
hence "f -` g -` U ∩ space M ∈ sets M"
by (meson f_meas g_meas measurable_sets H2)
moreover have "f -` g -` U ∩ space M = U ∩ space M"
by auto
ultimately show "V ∈ sets M" using H2 by simp
next
fix U
assume "U ∈ sets M"
then show "U ∈ sigma_Mx (measure_to_qbs M)"
using lr_sets by auto
qed
subsubsection ‹ The Adjunction ›
lemma lr_adjunction_correspondence :
"X →⇩Q (measure_to_qbs Y) = (qbs_to_measure X) →⇩M Y"
proof(auto)
fix f
assume "f ∈ X →⇩Q (measure_to_qbs Y)"
show "f ∈ qbs_to_measure X →⇩M Y"
proof(rule measurableI)
fix x
assume "x ∈ space (qbs_to_measure X)"
hence "x ∈ qbs_space X" by simp
thus "f x ∈ space Y"
using ‹f ∈ X →⇩Q (measure_to_qbs Y)› qbs_morphismE[of f X "measure_to_qbs Y"]
by auto
next
fix A
assume "A ∈ sets Y"
have "∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx (measure_to_qbs Y)"
using ‹f ∈ X →⇩Q (measure_to_qbs Y)› by auto
hence "∀α ∈ qbs_Mx X. f ∘ α ∈ real_borel →⇩M Y" by simp
hence "∀α ∈ qbs_Mx X. α -` (f -` A) ∈ sets real_borel"
using ‹A∈ sets Y› measurable_sets_borel vimage_comp by metis
thus "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
using sigma_Mx_def by auto
qed
next
fix f
assume "f ∈ qbs_to_measure X →⇩M Y"
show "f ∈ X →⇩Q measure_to_qbs Y"
proof(rule qbs_morphismI,simp)
fix α
assume "α ∈ qbs_Mx X"
show "f ∘ α ∈ real_borel →⇩M Y"
proof(rule measurableI)
fix x
assume "x ∈ space real_borel"
from this ‹α ∈ qbs_Mx X ›qbs_decomp have "α x ∈ qbs_space X" by auto
hence "α x ∈ space (qbs_to_measure X)" by simp
thus "(f ∘ α) x ∈ space Y"
using ‹f ∈ qbs_to_measure X →⇩M Y›
by (metis comp_def measurable_space)
next
fix A
assume "A ∈ sets Y"
from ‹f ∈ qbs_to_measure X →⇩M Y› measurable_sets this measurable_def
have "f -` A ∩ space (qbs_to_measure X) ∈ sets (qbs_to_measure X)"
by blast
hence "f -` A ∩ qbs_space X ∈ sigma_Mx X" by simp
then have "∃ V. f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets real_borel)"
by (simp add:sigma_Mx_def)
then obtain V where h:"f -` A ∩ qbs_space X = V ∩ qbs_space X ∧ (∀β∈ qbs_Mx X. β -` V ∈ sets real_borel)" by auto
have 1:"α -` (f -` A) = α -` (f -` A ∩ qbs_space X)"
using ‹α ∈ qbs_Mx X› by blast
have 2:"α -` (V ∩ qbs_space X) = α -` V"
using ‹α ∈ qbs_Mx X› by blast
from 1 2 h have "(f ∘ α) -` A = α -` V" by (simp add: vimage_comp)
from this h ‹α ∈ qbs_Mx X ›show "(f ∘ α) -` A ∩ space real_borel ∈ sets real_borel" by simp
qed
qed
qed
lemma(in standard_borel) standard_borel_r_full_faithful:
"M →⇩M Y = measure_to_qbs M →⇩Q measure_to_qbs Y"
proof(standard;standard)
fix h
assume "h ∈ M →⇩M Y"
then show "h ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
using r_preserves_morphisms by auto
next
fix h
assume h:"h ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
show "h ∈ M →⇩M Y"
proof(rule measurableI)
fix x
assume "x ∈ space M"
then show "h x ∈ space Y"
using h by auto
next
fix U
assume "U ∈ sets Y"
have "h ∘ g ∈ real_borel →⇩M Y"
using ‹h ∈ measure_to_qbs M →⇩Q measure_to_qbs Y›
by(simp add: qbs_morphism_def)
hence "(h ∘ g) -` U ∈ sets real_borel"
by (simp add: ‹U ∈ sets Y› measurable_sets_borel)
hence "f -` ((h ∘ g) -` U) ∩ space M ∈ sets M"
using f_meas in_borel_measurable_borel by blast
moreover have "f -` ((h ∘ g) -` U) ∩ space M = h -` U ∩ space M"
using f_meas by auto
ultimately show "h -` U ∩ space M ∈ sets M" by simp
qed
qed
lemma qbs_morphism_dest[dest]:
assumes "f ∈ X →⇩Q measure_to_qbs Y"
shows "f ∈ qbs_to_measure X →⇩M Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_dest[dest]:
assumes "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
shows "k ∈ M →⇩M Y"
using standard_borel_r_full_faithful assms by auto
lemma qbs_morphism_measurable_intro[intro!]:
assumes "f ∈ qbs_to_measure X →⇩M Y"
shows "f ∈ X →⇩Q measure_to_qbs Y"
using assms lr_adjunction_correspondence by auto
lemma(in standard_borel) qbs_morphism_measurable_intro[intro!]:
assumes "k ∈ M →⇩M Y"
shows "k ∈ measure_to_qbs M →⇩Q measure_to_qbs Y"
using standard_borel_r_full_faithful assms by auto
text ‹ We can use the measurability prover when we reason about morphisms. ›
lemma
assumes "f ∈ ℝ⇩Q →⇩Q ℝ⇩Q"
shows "(λx. 2 * f x + (f x)^2) ∈ ℝ⇩Q →⇩Q ℝ⇩Q"
using assms by auto
lemma
assumes "f ∈ X →⇩Q ℝ⇩Q"
and "α ∈ qbs_Mx X"
shows "(λx. 2 * f (α x) + (f (α x))^2) ∈ ℝ⇩Q →⇩Q ℝ⇩Q"
using assms by auto
lemma qbs_morphisn_from_countable:
fixes X :: "'a quasi_borel"
assumes "countable (qbs_space X)"
"qbs_Mx X ⊆ real_borel →⇩M count_space (qbs_space X)"
and "⋀i. i ∈ qbs_space X ⟹ f i ∈ qbs_space Y"
shows "f ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx X"
then have [measurable]: "α ∈ real_borel →⇩M count_space (qbs_space X)"
using assms(2) ..
define k :: "'a ⇒ real ⇒ _"
where "k ≡ (λi _. f i)"
have "f ∘ α = (λr. k (α r) r)"
by(auto simp add: k_def)
also have "... ∈ qbs_Mx Y"
by(rule qbs_closed3_dest2[OF assms(1)]) (use assms(3) k_def in simp_all)
finally show "f ∘ α ∈ qbs_Mx Y" .
qed
corollary nat_qbs_morphism:
assumes "⋀n. f n ∈ qbs_space Y"
shows "f ∈ ℕ⇩Q →⇩Q Y"
using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel]
by(auto intro!: qbs_morphisn_from_countable)
corollary bool_qbs_morphism:
assumes "⋀b. f b ∈ qbs_space Y"
shows "f ∈ 𝔹⇩Q →⇩Q Y"
using assms measurable_cong_sets[OF refl sets_borel_eq_count_space,of real_borel]
by(auto intro!: qbs_morphisn_from_countable)
subsubsection ‹ The Adjunction w.r.t. Ordering›
lemma l_mono:
"mono qbs_to_measure"
apply standard
subgoal for X Y
proof(induction rule: less_eq_quasi_borel.induct)
case (1 X Y)
then show ?case
by(simp add: less_eq_measure.intros(1))
next
case (2 X Y)
then have "sigma_Mx X ⊆ sigma_Mx Y"
by(auto simp add: sigma_Mx_def)
then consider "sigma_Mx X ⊂ sigma_Mx Y" | "sigma_Mx X = sigma_Mx Y"
by auto
then show ?case
apply(cases)
apply(rule less_eq_measure.intros(2))
apply(simp_all add: 2)
by(rule less_eq_measure.intros(3),simp_all add: 2)
qed
done
lemma r_mono:
"mono measure_to_qbs"
apply standard
subgoal for M N
proof(induction rule: less_eq_measure.inducts)
case (1 M N)
then show ?case
by(simp add: less_eq_quasi_borel.intros(1))
next
case (2 M N)
then have "real_borel →⇩M N ⊆ real_borel →⇩M M"
by(simp add: measurable_mono)
then consider "real_borel →⇩M N ⊂ real_borel →⇩M M" | "real_borel →⇩M N = real_borel →⇩M M"
by auto
then show ?case
by cases (rule less_eq_quasi_borel.intros(2),simp_all add: 2)+
next
case (3 M N)
then show ?case
apply -
by(rule less_eq_quasi_borel.intros(2)) (simp_all add: measurable_mono)
qed
done
lemma rl_order_adjunction:
"X ≤ qbs_to_measure Y ⟷ measure_to_qbs X ≤ Y"
proof
assume 1: "X ≤ qbs_to_measure Y"
then show "measure_to_qbs X ≤ Y"
proof(induction rule: less_eq_measure.cases)
case (1 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 1(2)[symmetric])
show ?case
by(rule less_eq_quasi_borel.intros(1),simp add: 1)
next
case (2 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 2(2)[symmetric])
show ?case
proof(rule less_eq_quasi_borel.intros(2),simp add:2,auto)
fix α
assume h:"α ∈ qbs_Mx Y"
show "α ∈ real_borel →⇩M X"
proof(rule measurableI,simp_all)
show "⋀x. α x ∈ space X"
using h by (auto simp add: 2)
next
fix A
assume "A ∈ sets X"
then have "A ∈ sets (qbs_to_measure Y)"
using 2 by auto
then obtain U where
hu:"A = U ∩ space N"
"(∀α∈qbs_Mx Y. α -` U ∈ sets real_borel)"
by(auto simp add: sigma_Mx_def)
have "α -` A = α -` U"
using h qbs_decomp[of Y]
by(auto simp add: hu)
thus "α -` A ∈ sets borel"
using h hu(2) by simp
qed
qed
next
case (3 M N)
then have [simp]:"qbs_space Y = space N"
by(simp add: 3(2)[symmetric])
show ?case
proof(rule less_eq_quasi_borel.intros(2),simp add: 3,auto)
fix α
assume h:"α ∈ qbs_Mx Y"
show "α ∈ real_borel →⇩M X"
proof(rule measurableI,simp_all)
show "⋀x. α x ∈ space X"
using h by(auto simp: 3)
next
fix A
assume "A ∈ sets X"
then have "A ∈ sets (qbs_to_measure Y)"
using 3 by auto
then obtain U where
hu:"A = U ∩ space N"
"(∀α∈qbs_Mx Y. α -` U ∈ sets real_borel)"
by(auto simp add: sigma_Mx_def)
have "α -` A = α -` U"
using h qbs_decomp[of Y]
by(auto simp add: hu)
thus "α -` A ∈ sets borel"
using h hu(2) by simp
qed
qed
qed
next
assume "measure_to_qbs X ≤ Y"
then show "X ≤ qbs_to_measure Y"
proof(induction rule: less_eq_quasi_borel.cases)
case (1 A B)
have [simp]: "space X = qbs_space A"
by(simp add: 1(1)[symmetric])
show ?case
by(rule less_eq_measure.intros(1)) (simp add: 1)
next
case (2 A B)
then have hmy:"qbs_Mx Y ⊆ real_borel →⇩M X"
by auto
have [simp]: "space X = qbs_space A"
by(simp add: 2(1)[symmetric])
have "sets X ⊆ sigma_Mx Y"
proof
fix U
assume hu:"U ∈ sets X"
show "U ∈ sigma_Mx Y"
proof(simp add: sigma_Mx_def,rule exI[where x=U],auto)
show "⋀x. x ∈ U ⟹ x ∈ qbs_space Y"
using sets.sets_into_space[OF hu]
by(auto simp add: 2)
next
fix α
assume "α ∈ qbs_Mx Y"
then have "α ∈ real_borel →⇩M X"
using hmy by(auto)
thus "α -` U ∈ sets real_borel"
using hu by(simp add: measurable_sets_borel)
qed
qed
then consider "sets X = sigma_Mx Y" | "sets X ⊂ sigma_Mx Y"
by auto
then show ?case
proof cases
case 1
show ?thesis
apply(rule less_eq_measure.intros(3),simp_all add: 1 2)
proof(rule le_funI)
fix U
consider "U = {}" | "U ∉ sigma_Mx B" | "U ≠ {} ∧ U ∈ sigma_Mx B"
by auto
then show "emeasure X U ≤ (if U = {} ∨ U ∉ sigma_Mx B then 0 else ∞)"
proof cases
case 1
then show ?thesis by simp
next
case h:2
then have "U ∉ sigma_Mx A"
using qbs_Mx_sigma_Mx_contra[OF 2(3)[symmetric] 2(4)]
by auto
hence "U ∉ sets X"
using lr_sets 2(1) by auto
thus ?thesis
by(simp add: h emeasure_notin_sets)
next
case 3
then show ?thesis
by simp
qed
qed
next
case h2:2
show ?thesis
by(rule less_eq_measure.intros(2)) (simp add: 2,simp add: h2)
qed
qed
qed
end