Theory Coproduct_Measure_Additional
section ‹ Additional Properties ›
theory Coproduct_Measure_Additional
imports "Coproduct_Measure"
"Standard_Borel_Spaces.StandardBorel"
"S_Finite_Measure_Monad.Kernels"
"S_Finite_Measure_Monad.Measure_QuasiBorel_Adjunction"
begin
subsection ‹ S-Finiteness›
lemma s_finite_measure_copair_measure:
assumes "s_finite_measure M" "s_finite_measure N"
shows "s_finite_measure (copair_measure M N)"
proof -
note [measurable] = measurable_vimage_Inl[of _ M N] measurable_vimage_Inr[of _ M N]
obtain Mi Ni where [measurable_cong]:
"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
"⋀i. sets (Ni i) = sets N" "⋀i. finite_measure (Ni i)" "⋀A. N A = (∑i. Ni i A)"
by (metis assms(1) assms(2) s_finite_measure.finite_measures')
thus ?thesis
by(auto intro!: s_finite_measureI[where Mi="λi. Mi i ⨁⇩M Ni i"] finite_measure_copair_measure
cong: sets_copair_measure_cong simp: emeasure_copair_measure suminf_add)
qed
lemma s_finite_measure_coPiM:
assumes "countable I" "⋀i. i ∈ I ⟹ s_finite_measure (Mi i)"
shows "s_finite_measure (coPiM I Mi)"
proof -
note measurable_Pair_vimage[measurable (raw)]
consider "finite I" | "infinite I" "countable I"
using assms by argo
then show ?thesis
proof cases
assume I:"finite I"
show ?thesis
by(auto intro!: s_finite_measure_finite_sumI[where Mi="λi. distr (Mi i) (coPiM I Mi) (Pair i)"
and I=I,OF _ s_finite_measure.s_finite_measure_distr[OF assms(2)]]
simp: emeasure_distr emeasure_coPiM_finite I)
next
assume I:"infinite I" "countable I"
then have [simp]:"⋀n. from_nat_into I n ∈ I"
by (simp add: from_nat_into infinite_imp_nonempty)
show ?thesis
by(auto intro!: s_finite_measure_s_finite_sumI[where
Mi="λn. distr (Mi (from_nat_into I n)) (coPiM I Mi) (Pair (from_nat_into I n))",
OF _ s_finite_measure.s_finite_measure_distr[OF assms(2)]]
simp: emeasure_distr I emeasure_coPiM_countable_infinite' coPair_inverse_space_unit[where I=I])
qed
qed
subsection ‹ Standardness ›
lemma standard_borel_copair_measure:
assumes "standard_borel M" "standard_borel N"
shows "standard_borel (M ⨁⇩M N)"
proof -
obtain A where A[measurable]: "A ∈ sets borel" "A ⊆ {0<..<1::real}"
"M measurable_isomorphic restrict_space borel A"
by (meson assms(1) greaterThanLessThan_borel linorder_not_le not_one_le_zero
standard_borel.isomorphic_subset_real uncountable_open_interval)
then obtain f f'
where f[measurable]: "f ∈ M →⇩M restrict_space borel A"
"f' ∈ restrict_space borel A →⇩M M"
"⋀x. x ∈ space M ⟹ f' (f x) = x" "⋀y. y ∈ A ⟹ f (f' y) = y"
using measurable_isomorphicD[OF A(3)] unfolding space_restrict_space by fastforce
obtain B where B[measurable]:"B ∈ sets borel" "B ⊆ {1<..<2::real}"
"N measurable_isomorphic restrict_space borel B"
by (metis assms(2) greaterThanLessThan_borel linorder_not_le numeral_le_one_iff
semiring_norm(69) standard_borel.isomorphic_subset_real uncountable_open_interval)
then obtain g g'
where g[measurable]: "g ∈ N →⇩M restrict_space borel B"
"g' ∈ restrict_space borel B →⇩M N"
"⋀x. x ∈ space N ⟹ g' (g x) = x"
"⋀y. y ∈ B ⟹ g (g' y) = y"
using measurable_isomorphicD[OF B(3)] unfolding space_restrict_space by fastforce
have AB:"A ∩ B = {}"
using A B by fastforce
have [measurable]:"f ∈ M →⇩M restrict_space borel (A ∪ B)"
using f(1) unfolding measurable_restrict_space2_iff by blast
have [measurable]:"g ∈ N →⇩M restrict_space borel (A ∪ B)"
using g(1) unfolding measurable_restrict_space2_iff by blast
have iso:"restrict_space borel (A ∪ B) measurable_isomorphic M ⨁⇩M N"
proof(safe intro!: measurable_isomorphic_byWitness)
show "case_sum f g ∈ M ⨁⇩M N →⇩M restrict_space borel (A ∪ B)"
by(auto intro!: measurable_copair_Inl_Inr)
show "(λr. if r ∈ A then Inl (f' r) else if r ∈ B then Inr (g' r) else undefined)
∈ restrict_space borel (A ∪ B) →⇩M M ⨁⇩M N" (is "?f ∈ _")
proof -
have 1:
"restrict_space (restrict_space borel (A ∪ B)) {r. r ∈ A} = restrict_space borel A"
"restrict_space (restrict_space borel (A ∪ B)) {r. r ∉ A} = restrict_space borel B"
"restrict_space (restrict_space borel B) {x. x ∈ B} = restrict_space borel B"
"restrict_space (restrict_space borel B) {x. x ∉ B} = count_space {}"
using AB by(auto simp: restrict_restrict_space
intro!: arg_cong[where f="restrict_space borel"] space_empty)
have 2:"{r ∈ space (restrict_space borel (A ∪ B)). r ∈ A} = A"
"{x ∈ space (restrict_space (restrict_space borel (A ∪ B)) {r. r ∉ A}). x ∈ B} = B"
"{x ∈ space (restrict_space borel B). x ∈ B} = B"
using AB by (auto simp: space_restrict_space)
show ?thesis
by (intro measurable_If_restrict_space_iff[THEN iffD2] conjI)
(unfold 1 2, simp_all add: sets_restrict_space_iff)
qed
show "⋀x. x ∈ space (M ⨁⇩M N) ⟹ ?f (case_sum f g x) = x"
"⋀r. r ∈ space (restrict_space borel (A ∪ B)) ⟹ case_sum f g (?f r) = r"
using measurable_space[OF f(1)] measurable_space[OF g(1)] AB
by (auto simp: space_copair_measure f g)
qed
show ?thesis
by(auto intro!: standard_borel.measurable_isomorphic_standard[OF _ iso]
standard_borel.standard_borel_restrict_space[OF standard_borel_ne.standard_borel])
qed
corollary
shows standard_borel_ne_copair_measure1: "standard_borel_ne M ⟹ standard_borel N ⟹ standard_borel_ne (M ⨁⇩M N)"
and standard_borel_ne_copair_measure2: "standard_borel M ⟹ standard_borel_ne N ⟹ standard_borel_ne (M ⨁⇩M N)"
and standard_borel_ne_copair_measure: "standard_borel_ne M ⟹ standard_borel_ne N ⟹ standard_borel_ne (M ⨁⇩M N)"
by(auto simp: standard_borel_ne_def standard_borel_ne_axioms_def standard_borel_copair_measure space_copair_measure)
lemma standard_borel_coPiM:
assumes "countable I" "⋀i. i ∈ I ⟹ standard_borel (Mi i)"
shows "standard_borel (coPiM I Mi)"
proof -
let ?I = "{i∈I. space (Mi i) ≠ {}}"
have countable_I: "countable ?I"
using assms by auto
define I' where "I' ≡ to_nat_on ?I ` ?I"
define Mn where "Mn ≡ λn. Mi (from_nat_into ?I n)"
have I':"countable I'" "⋀n. n ∈ I' ⟹ space (Mn n) ≠ {}"
"⋀n. n ∈ I' ⟹ standard_borel_ne (Mn n)"
using countable_I from_nat_into_to_nat_on[OF countable_I] assms(2)
by(fastforce simp: I'_def Mn_def standard_borel_ne_def standard_borel_ne_axioms_def
simp del: from_nat_into_to_nat_on)+
have iso1:"coPiM I Mi measurable_isomorphic coPiM I' Mn"
proof(safe intro!: measurable_isomorphic_byWitness[where f="λ(i,x). (to_nat_on ?I i, x)"
and g="λ(n,x). (from_nat_into ?I n, x)"])
show "(λ(i, x). (to_nat_on ?I i, x)) ∈ coPiM I Mi →⇩M coPiM I' Mn"
proof(rule measurable_coPiM2)
fix i
assume i:"i ∈ I"
show "Pair (to_nat_on ?I i) ∈ Mi i →⇩M coPiM I' Mn"
proof(cases "space (Mi i) = {}")
assume "space (Mi i) ≠ {}"
then show ?thesis
by(intro measurable_compose[OF _ measurable_Pair_coPiM[where I=I']])
(use I'_def i countable_I Mn_def in auto)
qed(simp add: measurable_def)
qed
show "(λ(n,x). (from_nat_into ?I n, x)) ∈ coPiM I' Mn →⇩M coPiM I Mi"
proof(rule measurable_coPiM2)
fix n
assume "n ∈ I'"
show "Pair (from_nat_into ?I n) ∈ Mn n →⇩M coPiM I Mi"
by (metis (no_types, lifting) Mn_def I'_def ‹n ∈ I'› emptyE empty_is_image
from_nat_into measurable_Pair_coPiM mem_Collect_eq)
qed
qed(auto intro!: from_nat_into_to_nat_on to_nat_on_from_nat_into simp: space_coPiM I'_def countable_I)
have "∃A. A ∈ sets borel ∧ A ⊆ {real n<..real n + 1} ∧ Mn n measurable_isomorphic (restrict_space borel A)"
if n:"n ∈ I'" for n
using standard_borel.isomorphic_subset_real[OF
standard_borel_ne.standard_borel[OF I'(3)[OF n] ],of "{real n<..real n + 1}"]
uncountable_half_open_interval_2[of "real n" "real n + 1"]
by fastforce
then obtain An'
where An': "⋀n. n ∈ I' ⟹ An' n ∈ sets borel"
"⋀n. n ∈ I' ⟹ An' n ⊆ {real n<..real n + 1}"
"⋀n. n ∈ I' ⟹ Mn n measurable_isomorphic (restrict_space borel (An' n))"
by metis
define An where "An ≡ λn. if n ∈ I' then An' n else {real n + 1}"
have An[measurable]: "⋀n. An n ∈ sets borel"
"⋀n. An n ⊆ {real n<..real n + 1}"
"⋀n. n ∈ I' ⟹ Mn n measurable_isomorphic (restrict_space borel (An n))"
using An' by(auto simp: An_def)
hence disj_An:"disjoint_family An"
unfolding disjoint_family_on_def
by safe (metis (no_types, opaque_lifting) greaterThanAtMost_iff less_le nat_less_real_le not_less order_trans subset_eq)
obtain fn gn'
where fg:"⋀n. n ∈ I' ⟹ fn n ∈ Mn n →⇩M restrict_space borel (An n)"
"⋀n. n ∈ I' ⟹ gn' n ∈ restrict_space borel (An n) →⇩M Mn n"
"⋀n x. n ∈ I' ⟹ x ∈ space (Mn n) ⟹ gn' n (fn n x) = x"
"⋀n r. n ∈ I' ⟹ r ∈ space (restrict_space borel (An n)) ⟹ fn n (gn' n r) = r"
using measurable_isomorphicD[OF An(3)] by metis
define gn where "gn ≡ (λn r. if r ∈ An n then gn' n r else (SOME x. x ∈ space (Mn n)))"
have gn_meas[measurable]:"gn n ∈ borel →⇩M Mn n" if n:"n ∈ I'" for n
unfolding gn_def by(rule measurable_restrict_space_iff[THEN iffD1,OF _ _ fg(2)[OF n]])
(auto simp add: I'(2) some_in_eq that)
have fg':"⋀n x. n ∈ I' ⟹ x ∈ space (Mn n) ⟹ gn n (fn n x) = x"
"⋀n r. n ∈ I' ⟹ r ∈ An n ⟹ fn n (gn n r) = r"
using fg measurable_space[OF fg(1)] by(auto simp: gn_def)
have fn[measurable]:"fn n ∈ Mn n →⇩M restrict_space borel (⋃n∈I'. An n)" if n:"n ∈ I'" for n
using measurable_restrict_space2_iff[THEN iffD1,OF fg(1)[OF n]]
by(auto intro!: measurable_restrict_space2 n)
let ?f = "λ(n,x). fn n x" and ?g ="λr. (nat ⌈r⌉ - 1, gn (nat ⌈r⌉ - 1) r)"
have iso2:"coPiM I' Mn measurable_isomorphic restrict_space borel (⋃n∈I'. An n)"
proof(safe intro!: measurable_isomorphic_byWitness)
show "?f ∈ coPiM I' Mn →⇩M restrict_space borel (⋃n∈I'. An n)"
by(auto intro!: measurable_coPiM2)
next
show "?g ∈ restrict_space borel (⋃n∈I'. An n) →⇩M coPiM I' Mn"
proof(safe intro!: measurable_coPiM1)
have 1:"restrict_space borel (⋃ (An ` I')) →⇩M count_space I'
= restrict_space borel (⋃ (An ` I')) →⇩M restrict_space (count_space UNIV) I'"
by (simp add: restrict_count_space)
show "(λx. nat ⌈x⌉ - 1) ∈ restrict_space borel (⋃ (An ` I')) →⇩M count_space I'"
unfolding 1
proof(safe intro!: measurable_restrict_space3)
fix n r
assume n:"n ∈ I'" "r ∈ An n"
then have "real n < r" "r ≤ real n + 1"
using An(2) by fastforce+
thus "nat ⌈r⌉ - 1 ∈ I'"
by (metis n(1) add.commute diff_Suc_1 le_SucE nat_ceiling_le_eq not_less of_nat_Suc)
qed simp
qed(auto simp: measurable_restrict_space1)
next
fix n x
assume "(n,x)∈space (coPiM I' Mn)"
then have nx:"n ∈ I'" "x ∈ space (Mn n)"
by(auto simp: space_coPiM)
have 1:"nat ⌈?f (n,x)⌉ = n + 1"
using measurable_space[OF fg(1)[OF nx(1)] nx(2)] An(2)[of n]
by simp
(metis add.commute greaterThanAtMost_iff le_SucE nat_ceiling_le_eq not_less of_nat_Suc subset_eq)
show "?g (?f (n,x)) = (n,x)"
unfolding 1 using fg'(1)[OF nx] by simp
next
fix y
assume "y ∈ space (restrict_space borel (⋃ (An ` I')))"
then obtain n where n: "n ∈ I'" "y ∈ An n"
by auto
then have [simp]:"nat ⌈y⌉ = n + 1"
using An(2)[of n]
by simp (metis add.commute greaterThanAtMost_iff le_SucE nat_ceiling_le_eq not_less of_nat_Suc subset_eq)
show "?f (?g y) = y"
using fg'(2)[OF n(1)] n(2) by auto
qed
have "standard_borel (restrict_space borel (⋃ (An ` I')))"
by(auto intro!: standard_borel_ne.standard_borel[THEN standard_borel.standard_borel_restrict_space])
with iso1 iso2 show ?thesis
by (meson measurable_isomorphic_sym standard_borel.measurable_isomorphic_standard)
qed
lemma standard_borel_ne_coPiM:
assumes "countable I" "⋀i. i ∈ I ⟹ standard_borel (Mi i)"
and "i ∈ I" "space (Mi i) ≠ {}"
shows "standard_borel_ne (coPiM I Mi)"
proof -
have "space (coPiM I Mi) ≠ {}"
using assms(3) assms(4) space_coPiM by fastforce
thus ?thesis
by(auto intro!: standard_borel_coPiM assms simp: standard_borel_ne_def standard_borel_ne_axioms_def)
qed
subsection ‹ Relationships with Quasi-Borel Spaces›
text ‹ Proposition19(3)~\cite{Heunen_2017}›
lemma r_preserve_copair: "measure_to_qbs (copair_measure M N) = measure_to_qbs M ⨁⇩Q measure_to_qbs N"
proof(safe intro!: qbs_eqI)
fix α
assume "α ∈ qbs_Mx (measure_to_qbs (M ⨁⇩M N))"
then have a[measurable]: "α ∈ borel →⇩M M ⨁⇩M N"
by(simp add: qbs_Mx_R)
have s[measurable]: "α -` Inr ` space N ∈ sets borel" "α -` Inl ` space M ∈ sets borel"
by(auto intro!: measurable_sets_borel[OF a])
consider "α -` Inl ` space M ∩ space borel = space borel"
| "α -` Inr ` (space N) ∩ space borel = space borel"
| "α -` Inl ` space M ∩ space borel ⊂ space borel"
"α -` Inr ` (space N) ∩ space borel ⊂ space borel"
by blast
then show "α ∈ qbs_Mx (measure_to_qbs M ⨁⇩Q measure_to_qbs N)"
proof cases
assume 1:"α -` Inl ` space M ∩ space borel = space borel"
then obtain f' where "f' ∈ borel →⇩M M" "⋀x. x ∈ space borel ⟹ α x = Inl (f' x)"
using measurable_copair_dest1[OF a] by blast
thus ?thesis
using 1 by(auto simp: copair_qbs_Mx copair_qbs_Mx_def qbs_Mx_R
intro!: bexI[where x="α -` Inr ` space N"] bexI[where x=f'])
next
assume 2:"α -` Inr ` space N ∩ space borel = space borel"
then obtain f' where "f' ∈ borel →⇩M N" "⋀x. x ∈ space borel ⟹ α x = Inr (f' x)"
using measurable_copair_dest2[OF a] by blast
thus ?thesis
using 2 by(auto simp: copair_qbs_Mx copair_qbs_Mx_def qbs_Mx_R
intro!: bexI[where x="α -` Inr ` space N"] bexI[where x=f'])
next
case 3
then obtain f' f''
where f[measurable]:"f' ∈ borel →⇩M M"
"f'' ∈ borel →⇩M N"
"⋀x. x ∈ space borel ⟹ x ∈ α -` Inl ` space M ⟹ α x = Inl (f' x)"
"⋀x. x ∈ space borel ⟹ x ∉ α -` Inl ` space M ⟹ α x = Inr (f'' x)"
using measurable_copair_dest3[OF a] by metis
moreover have "α -` Inl ` space M ≠ UNIV" "α -` Inl ` space M ≠ {}"
using 3 measurable_space[OF a] by(fastforce simp: space_copair_measure)+
ultimately show ?thesis
by(auto simp: copair_qbs_Mx copair_qbs_Mx_def qbs_Mx_R simp del: vimage_eq
intro!: bexI[where x="α -` Inl ` space M"] bexI[where x=f'] bexI[where x=f''])
qed
qed(auto simp: qbs_Mx_R copair_qbs_Mx copair_qbs_Mx_def)
lemma r_preserve_coproduct:
assumes "countable I"
shows "measure_to_qbs (coPiM I M) = (⨿⇩Q i∈I. measure_to_qbs (M i))"
proof(safe intro!: qbs_eqI)
fix α
assume h:"α ∈ qbs_Mx (measure_to_qbs (coPiM I M))"
then obtain a g
where "a ∈ borel →⇩M count_space I"
"⋀i. i ∈ I ⟹ space (M i) ≠ {} ⟹ g i ∈ borel →⇩M M i"
"α = (λx. (a x, g (a x) x))"
using measurable_coPiM1_elements[OF assms] unfolding qbs_Mx_R by blast
thus "α ∈ qbs_Mx (⨿⇩Q i∈I. measure_to_qbs (M i))"
using qbs_Mx_to_X[OF h]
by(safe intro!: coPiQ_MxI) (auto simp: qbs_Mx_R qbs_space_R space_coPiM)
next
fix α
assume "α ∈ qbs_Mx (⨿⇩Q i∈I. measure_to_qbs (M i))"
then obtain a g where "a ∈ borel →⇩M count_space I"
"⋀i. i ∈ range a ⟹ g i ∈ borel →⇩M M i" "α = (λx. (a x, g (a x) x))"
unfolding coPiQ_Mx coPiQ_Mx_def qbs_Mx_R by blast
thus "α ∈ qbs_Mx (measure_to_qbs (coPiM I M))"
by(auto intro!: measurable_coPiM1' simp: qbs_Mx_R assms)
qed
end