Theory Lemmas_Disintegration
section ‹ Lemmas ›
theory Lemmas_Disintegration
imports "Standard_Borel_Spaces.StandardBorel"
begin
subsection ‹ Lemmas ›
lemma semiring_of_sets_binary_product_sets[simp]:
"semiring_of_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
proof
show "{a × b |a b. a ∈ sets X ∧ b ∈ sets Y} ⊆ Pow (space X × space Y)"
using pair_measure_closed by blast
next
fix c d
assume "c ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}" "d ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
then obtain ac bc ad bd where
"c = ac × bc" "ac ∈ sets X" "bc ∈ sets Y" "d = ad × bd" "ad ∈ sets X" "bd ∈ sets Y"
by auto
thus "c ∩ d ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
by(auto intro!: exI[where x="ac ∩ ad"] exI[where x="bc ∩ bd"])
next
fix c d
assume "c ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}" "d ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
then obtain ac bc ad bd where cd:
"c = ac × bc" "ac ∈ sets X" "bc ∈ sets Y" "d = ad × bd" "ad ∈ sets X" "bd ∈ sets Y"
by auto
then have eq1:"c - d = ((ac - ad) × (bc - bd)) ∪ ((ac - ad) × (bc ∩ bd)) ∪ ((ac ∩ ad) × (bc - bd))"
by blast
obtain a1 where a1: "a1⊆sets X" "finite a1" "disjoint a1" "ac - ad = ⋃ a1"
using cd sets.Diff_cover[of ac X ad] by auto
obtain a2 where a2 : "a2⊆sets Y" "finite a2" "disjoint a2" "bc - bd = ⋃ a2"
using cd sets.Diff_cover[of bc Y bd] by auto
define A1 A2 A3
where A1_def:"A1 ≡ {a × b|a b. a ∈ a1 ∧ b ∈ a2}"
and A2_def:"A2 ≡ {a × (bc ∩ bd)|a . a ∈ a1}"
and A3_def:"A3 ≡ {(ac ∩ ad) × b|b. b ∈ a2}"
have disj:"disjoint (A1 ∪ A2 ∪ A3)"
proof -
have [simp]: "disjoint A1"
proof
fix x y
assume "x ∈ A1" "y ∈ A1" "x ≠ y"
then obtain xa xb ya yb where xy: "x = xa × xb" "xa ∈ a1" "xb ∈ a2" "y = ya × yb" "ya ∈ a1" "yb ∈ a2"
by(auto simp: A1_def)
with ‹x ≠ y› consider "xa ≠ ya" | "xb ≠ yb" by auto
thus "disjnt x y"
proof cases
case 1
then have "xa ∩ ya = {}"
using a1(3) xy by(auto simp: disjoint_def)
thus ?thesis
by(auto simp: xy disjnt_def)
next
case 2
then have "xb ∩ yb = {}"
using a2(3) xy by(auto simp: disjoint_def)
thus ?thesis
by(auto simp: xy disjnt_def)
qed
qed
have [simp]: "disjoint A2"
proof
fix x y
assume "x ∈ A2" "y ∈ A2" "x ≠ y"
then obtain xa ya where xy: "x = xa × (bc ∩ bd)" "xa ∈ a1" "y = ya × (bc ∩ bd)" "ya ∈ a1"
by(auto simp: A2_def)
with a1(3) ‹x ≠ y› have "xa ∩ ya = {}"
by(auto simp: disjoint_def)
thus "disjnt x y"
by(auto simp: xy disjnt_def)
qed
have [simp]: "disjoint A3"
proof
fix x y
assume "x ∈ A3" "y ∈ A3" "x ≠ y"
then obtain xb yb where xy:"x = (ac ∩ ad) × xb" "xb ∈ a2" "y = (ac ∩ ad) × yb" "yb ∈ a2"
by(auto simp: A3_def)
with a2(3) ‹x ≠ y› have "xb ∩ yb = {}"
by(auto simp: disjoint_def)
thus "disjnt x y"
by(auto simp: xy disjnt_def)
qed
show ?thesis
by(auto intro!: disjoint_union) (insert a1 a2,auto simp: A1_def A2_def A3_def)
qed
have fin: "finite (A1 ∪ A2 ∪ A3)"
using a1 a2 by (auto simp: A1_def A2_def A3_def finite_image_set2)
have cdeq:"c - d = ⋃ (A1 ∪ A2 ∪ A3)"
proof -
have [simp]:"⋃ a1 × ⋃ a2 = ⋃ A1" "⋃ a1 × (bc ∩ bd) = ⋃ A2" "(ac ∩ ad) × ⋃ a2 = ⋃ A3"
by (auto simp: A1_def A2_def A3_def)
show ?thesis
using a1(4) a2(4) by(simp add: eq1)
qed
have "A1 ∪ A2 ∪ A3 ⊆ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
using a1(1) a2(1) cd by(auto simp: A1_def A2_def A3_def)
with fin disj cdeq show "∃C⊆{a × b |a b. a ∈ sets X ∧ b ∈ sets Y}. finite C ∧ disjoint C ∧ c - d = ⋃ C"
by (auto intro!: exI[where x="A1 ∪ A2 ∪ A3"])
qed auto
lemma sets_pair_restrict_space:
"sets (restrict_space X A ⨂⇩M restrict_space Y B) = sets (restrict_space (X ⨂⇩M Y) (A × B))"
(is "?lhs = ?rhs")
proof -
have "?lhs = sigma_sets (space (restrict_space X A) × space (restrict_space Y B)) {a × b |a b. a ∈ sets (restrict_space X A) ∧ b ∈ sets (restrict_space Y B)}"
by(simp add: sets_pair_measure)
also have "... = sigma_sets (space (restrict_space X A) × space (restrict_space Y B)) {a × b ∩ space (restrict_space X A) × space (restrict_space Y B) |a b. a ∈ sets X ∧ b ∈ sets Y}"
proof -
have "{a × b |a b. a ∈ sets (restrict_space X A) ∧ b ∈ sets (restrict_space Y B)} = {a × b ∩ space (restrict_space X A) × space (restrict_space Y B) |a b. a ∈ sets X ∧ b ∈ sets Y}"
unfolding space_restrict_space sets_restrict_space
proof safe
fix xa xb
show "xa ∈ sets X ⟹ xb ∈ sets Y ⟹
∃a b. (A ∩ xa) × (B ∩ xb) = a × b ∩ (A ∩ space X) × (B ∩ space Y) ∧ a ∈ sets X ∧ b ∈ sets Y"
by(auto intro!: exI[where x=xa] exI[where x=xb] dest:sets.sets_into_space)
next
fix a b
show "a ∈ sets X ⟹ b ∈ sets Y ⟹
∃aa ba. a × b ∩ (A ∩ space X) × (B ∩ space Y) = aa × ba ∧ aa ∈ sets.restricted_space X A ∧ ba ∈ sets.restricted_space Y B"
by(auto intro!: exI[where x="a ∩ A"] exI[where x="b ∩ B"] dest:sets.sets_into_space)
qed
thus ?thesis by simp
qed
also have "... = sigma_sets (space (restrict_space X A) × space (restrict_space Y B)) {(λx. x) -` c ∩ space (restrict_space X A) × space (restrict_space Y B) |c. c ∈ {a × b| a b. a ∈ sets X ∧ b ∈ sets Y}}"
proof -
have "{a × b ∩ space (restrict_space X A) × space (restrict_space Y B) |a b. a ∈ sets X ∧ b ∈ sets Y} = {(λx. x) -` c ∩ space (restrict_space X A) × space (restrict_space Y B) |c. c ∈ {a × b| a b. a ∈ sets X ∧ b ∈ sets Y}}"
by auto
thus ?thesis by simp
qed
also have "... = {(λx. x) -` c ∩ space (restrict_space X A) × space (restrict_space Y B) |c. c ∈ sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}}"
by(rule sigma_sets_vimage_commute[symmetric]) (auto simp: space_restrict_space)
also have "... = {c ∩ (A ∩ space X) × (B ∩ space Y) |c. c ∈ sets (X ⨂⇩M Y)}"
by(simp add: space_restrict_space sets_pair_measure)
also have "... = {c ∩ A × B |c. c ∈ sets (X ⨂⇩M Y)}"
using sets.sets_into_space[of _ "X ⨂⇩M Y",simplified space_pair_measure] by blast
also have "... = ?rhs"
by(auto simp: sets_restrict_space)
finally show ?thesis .
qed
lemma restrict_space_space[simp]: "restrict_space M (space M) = M"
by(auto intro!: measure_eqI simp: sets_restrict_space emeasure_restrict_space sets.sets_into_space)
lemma atMostq_Int_stable:
"Int_stable {{..r} |r::real. r ∈ ℚ}"
by(auto simp: Int_stable_def min_def)
lemma rborel_eq_atMostq:
"borel = sigma UNIV { {..r} | r::real. r ∈ ℚ}"
proof(safe intro!: borel_eq_sigmaI1[OF borel_eq_atMost,where F=id,simplified])
fix a :: real
interpret s: sigma_algebra UNIV "sigma_sets UNIV {{..r} |r. r ∈ ℚ}"
by(auto intro!: sigma_algebra_sigma_sets)
have [simp]: "{..a} = (⋂ ((λr. {..r}) ` {r. r ∈ ℚ ∧ a ≤ r}))"
by auto (metis Rats_dense_in_real less_le_not_le nle_le)
show "{..a} ∈ sigma_sets UNIV {{..r} |r. r ∈ ℚ}"
using countable_Collect countable_rat Rats_no_top_le
by(auto intro!: s.countable_INT')
qed auto
corollary rborel_eq_atMostq_sets:
"sets borel = sigma_sets UNIV {{..r} |r::real. r ∈ ℚ}"
by(simp add: rborel_eq_atMostq)
lemma mono_absolutely_continuous:
assumes "sets μ = sets ν" "⋀A. A ∈ sets μ ⟹ μ A ≤ ν A"
shows "absolutely_continuous ν μ"
by(auto simp: absolutely_continuous_def) (metis assms(1) assms(2) fmeasurableD fmeasurableI_null_sets le_zero_eq null_setsD1 null_setsI)
lemma ex_measure_countable_space:
assumes "countable (space X)"
and "sets X = Pow (space X)"
shows "∃μ. sets μ = sets X ∧ (∀x∈space X. μ {x} = f x)"
proof -
define μ where "μ ≡ extend_measure (space X) (space X) (λx. {x}) f"
have s:"sets μ = sets X"
using sets_extend_measure[of "λx. {x}" "space X" "space X"] sigma_sets_singletons[OF assms(1)]
by(auto simp add: μ_def assms(2))
show ?thesis
proof(safe intro!: exI[where x=μ])
fix x
assume x:"x ∈ space X"
show "μ {x} = f x"
proof(cases "finite (space X)")
case fin:True
then have sets_fin:"x ∈ sets μ ⟹ finite x" for x
by(auto intro!: rev_finite_subset[OF fin] sets.sets_into_space simp: s)
define μ' where "μ' ≡ (λA. ∑x∈A. f x)"
show ?thesis
proof(rule emeasure_extend_measure[of μ "space X" "space X" _ f μ' x])
show "countably_additive (sets μ) μ'"
using fin sets_fin
by(auto intro!: sets.countably_additiveI_finite simp: sets_eq_imp_space_eq[OF s] positive_def μ'_def additive_def comm_monoid_add_class.sum.union_disjoint)
qed(auto simp: x μ_def μ'_def positive_def)
next
case inf:False
define μ' where "μ' ≡ (λA. ∑n. if from_nat_into (space X) n ∈ A then f (from_nat_into (space X) n) else 0)"
show ?thesis
proof(rule emeasure_extend_measure[of μ "space X" "space X" _ f μ' x])
fix i
assume "i ∈ space X"
then obtain n where n:"from_nat_into (space X) n = i"
using bij_betw_from_nat_into[OF assms(1) inf] by (meson f_the_inv_into_f_bij_betw)
then have "μ' {i} = (∑m. if m = n then f (from_nat_into (space X) n) else 0)"
using from_nat_into_inj_infinite[OF assms(1) inf]
by(auto simp: μ'_def) metis
also have "... = (∑m. if (m + (Suc n)) = n then f (from_nat_into (space X) n) else 0) + (∑m<Suc n. if m = n then f (from_nat_into (space X) n) else 0)"
by(rule suminf_offset) auto
also have "... = f i"
by(auto simp: n)
finally show "μ' {i} = f i" .
next
show "countably_additive (sets μ) μ'"
proof(rule countably_additiveI)
fix A :: "nat ⇒ _"
assume h:"range A ⊆ sets μ" "disjoint_family A" "⋃ (range A) ∈ sets μ"
show "(∑i. μ' (A i)) = μ' (⋃ (range A))"
proof -
have "(∑i. μ' (A i)) = (∫⇧+ i. μ' (A i) ∂(count_space UNIV))"
by(simp add: nn_integral_count_space_nat)
also have "... = (∫⇧+ i. (∑n. if from_nat_into (space X) n ∈ A i then f (from_nat_into (space X) n) else 0) ∂(count_space UNIV))"
by(simp add: μ'_def)
also have "... = (∑n. (∫⇧+ i. (if from_nat_into (space X) n ∈ A i then f (from_nat_into (space X) n) else 0) ∂(count_space UNIV)))"
by(simp add: nn_integral_suminf)
also have "... = (∑n. (∫⇧+ i. f (from_nat_into (space X) n) * indicator (A i) (from_nat_into (space X) n) ∂(count_space UNIV)))"
by(auto intro!: suminf_cong nn_integral_cong)
also have "... = (∑n. (∑i. f (from_nat_into (space X) n) * indicator (A i) (from_nat_into (space X) n)))"
by(simp add: nn_integral_count_space_nat)
also have "... = (∑n. f (from_nat_into (space X) n) * indicator (⋃ (range A)) (from_nat_into (space X) n))"
by(simp add: suminf_indicator[OF h(2)])
also have "... = μ' (⋃ (range A))"
by(auto simp: μ'_def intro!: suminf_cong)
finally show ?thesis .
qed
qed
qed(auto simp: x μ_def μ'_def positive_def)
qed
qed(simp_all add: s)
qed
lemma ex_prob_space_countable:
assumes "space X ≠ {}" "countable (space X)"
and "sets X = Pow (space X)"
shows "∃μ. sets μ = sets X ∧ prob_space μ"
proof(cases "finite (space X)")
case fin:True
define n where "n ≡ card (space X)"
with fin assms(1) have n: "0 < n"
by(simp add: card_gt_0_iff)
obtain μ where μ: "sets μ = sets X" "⋀x. x ∈ space X ⟹ μ {x} = ennreal (1 / real n)"
using ex_measure_countable_space[OF assms(2,3)] by meson
then have sets_fin:"x ∈ sets μ ⟹ finite x" for x
by(auto intro!: rev_finite_subset[OF fin] sets.sets_into_space)
show ?thesis
proof(safe intro!: exI[where x=μ])
show "prob_space μ"
proof
have "emeasure μ (space μ) = (∑a∈space μ. ennreal (1/n))"
using emeasure_eq_sum_singleton[OF sets_fin[OF sets.top],of μ] assms(3) μ
by auto
also have "... = of_nat n * ennreal (1 / real n)"
using μ(2) sets_eq_imp_space_eq[OF μ(1)] by(simp add: n_def)
also have "... = 1"
using n by(auto simp: ennreal_of_nat_eq_real_of_nat) (metis ennreal_1 ennreal_mult'' mult.commute nonzero_eq_divide_eq not_gr0 of_nat_0_eq_iff of_nat_0_le_iff)
finally show "emeasure μ (space μ) = 1" .
qed
qed(use μ in auto)
next
case inf:False
obtain μ where μ: "sets μ = sets X" "⋀x. x ∈ space X ⟹ μ {x} = (1/2)^(Suc (to_nat_on (space X) x))"
using ex_measure_countable_space[OF assms(2,3),of "λx. (1/2)^(Suc (to_nat_on (space X) x))"] by auto
show ?thesis
proof(safe intro!: exI[where x=μ])
show "prob_space μ"
proof
have "emeasure μ (space μ) = emeasure μ (⋃n. {from_nat_into (space X) n})"
by(simp add: sets_eq_imp_space_eq[OF μ(1)] UNION_singleton_eq_range assms(1) assms(2))
also have "... = (∑n. μ {from_nat_into (space X) n})"
using from_nat_into_inj_infinite[OF assms(2) inf] from_nat_into[OF assms(1)] assms(3)
by(auto intro!: suminf_emeasure[symmetric] simp: μ(1) disjoint_family_on_def)
also have "... = (∑n. (1/2)^(Suc n))"
by(simp add: μ(2)[OF from_nat_into[OF assms(1)]] to_nat_on_from_nat_into_infinite[OF assms(2) inf])
also have "... = (∑i. ennreal ((1 / 2) ^ Suc i))"
by (metis (mono_tags, opaque_lifting) divide_ennreal divide_pos_pos ennreal_numeral ennreal_power le_less power_0 zero_less_numeral zero_less_one)
also have "... = 1"
using suminf_ennreal_eq[OF _ power_half_series]
by (metis ennreal_1 zero_le_divide_1_iff zero_le_numeral zero_le_power)
finally show "emeasure μ (space μ) = 1" .
qed
qed(use μ in auto)
qed
lemma AE_I'':
assumes "N ∈ null_sets M"
and "⋀x. x ∈ space M ⟹ x ∉ N ⟹ P x"
shows "AE x in M. P x"
by (metis (no_types, lifting) assms eventually_ae_filter mem_Collect_eq subsetI)
lemma absolutely_continuous_trans:
assumes "absolutely_continuous L M" "absolutely_continuous M N"
shows "absolutely_continuous L N"
using assms by(auto simp: absolutely_continuous_def)
subsection ‹ Equivalence of Measures ›
abbreviation equivalence_measure :: "'a measure ⇒ 'a measure ⇒ bool" (infix "~⇩M" 60)
where "equivalence_measure M N ≡ absolutely_continuous M N ∧ absolutely_continuous N M"
lemma equivalence_measure_refl: "M ~⇩M M"
by(auto simp: absolutely_continuous_def)
lemma equivalence_measure_sym:
assumes "M ~⇩M N"
shows "N ~⇩M M"
using assms by simp
lemma equivalence_measure_trans:
assumes "M ~⇩M N" "N ~⇩M L"
shows "M ~⇩M L"
using assms by(auto simp: absolutely_continuous_def)
lemma equivalence_measureI:
assumes "absolutely_continuous M N" "absolutely_continuous N M"
shows "M ~⇩M N"
by(simp add: assms)
end