(* Title: Measure_QuasiBorel_Adjunction.thy Author: Michikazu Hirata, Tokyo Institute of Technology *) 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