Theory Disintegration
section ‹ Disintegration Theorem ›
theory Disintegration
imports "S_Finite_Measure_Monad.Kernels"
"Lemmas_Disintegration"
begin
subsection ‹ Definition 14.D.2. (Mixture and Disintegration) ›
context measure_kernel
begin
definition mixture_of :: "[('a ×'b) measure, 'a measure] ⇒ bool" where
"mixture_of ν μ ⟷ sets ν = sets (X ⨂⇩M Y) ∧ sets μ = sets X ∧ (∀C∈sets (X ⨂⇩M Y). ν C = (∫⇧+x. ∫⇧+y. indicator C (x,y) ∂(κ x) ∂μ))"
definition disintegration :: "[('a ×'b) measure, 'a measure] ⇒ bool" where
"disintegration ν μ ⟷ sets ν = sets (X ⨂⇩M Y) ∧ sets μ = sets X ∧ (∀A∈sets X. ∀B∈sets Y. ν (A × B) = (∫⇧+x∈A. (κ x B) ∂μ))"
lemma disintegrationI:
assumes "sets ν = sets (X ⨂⇩M Y)" "sets μ = sets X"
and "⋀A B. A ∈ sets X ⟹ B ∈ sets Y ⟹ ν (A × B) = (∫⇧+x∈A. (κ x B) ∂μ)"
shows "disintegration ν μ"
by(simp add: disintegration_def assms)
lemma mixture_of_disintegration:
assumes "mixture_of ν μ"
shows "disintegration ν μ"
unfolding disintegration_def
proof safe
fix A B
assume [simp]:"A ∈ sets X" "B ∈ sets Y"
have [simp,measurable_cong]: "sets μ = sets X" "space μ = space X"
using assms by(auto simp: mixture_of_def intro!: sets_eq_imp_space_eq)
have "A × B ∈ sets (X ⨂⇩M Y)" by simp
with assms have "ν (A × B) = (∫⇧+x. ∫⇧+y. indicator (A × B) (x,y) ∂(κ x) ∂μ)"
by(simp add: mixture_of_def)
also have "... = (∫⇧+x. ∫⇧+y. indicator A x * indicator B y ∂(κ x) ∂μ)"
by(simp add: indicator_times)
also have "... = (∫⇧+x∈A. (κ x B) ∂μ)"
by(auto intro!: nn_integral_cong simp: kernel_sets nn_integral_cmult_indicator mult.commute)
finally show "emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B∂μ)" .
qed(use assms[simplified mixture_of_def] in auto)
lemma
shows mixture_of_sets_eq: "mixture_of ν μ ⟹ sets ν = sets (X ⨂⇩M Y)" "mixture_of ν μ ⟹ sets μ = sets X"
and mixture_of_space_eq: "mixture_of ν μ ⟹ space ν = space (X ⨂⇩M Y)" "mixture_of ν μ ⟹ space μ = space X"
and disintegration_sets_eq: "disintegration ν μ ⟹ sets ν = sets (X ⨂⇩M Y)" "disintegration ν μ ⟹ sets μ = sets X"
and disintegration_space_eq: "disintegration ν μ ⟹ space ν = space (X ⨂⇩M Y)" "disintegration ν μ ⟹ space μ = space X"
by(auto simp: mixture_of_def disintegration_def intro!: sets_eq_imp_space_eq)
lemma
shows mixture_ofD: "mixture_of ν μ ⟹ C ∈ sets (X ⨂⇩M Y) ⟹ ν C = (∫⇧+x. ∫⇧+y. indicator C (x,y) ∂(κ x) ∂μ)"
and disintegrationD: "disintegration ν μ ⟹ A ∈ sets X ⟹ B ∈ sets Y ⟹ ν (A × B) = (∫⇧+x∈A. (κ x B) ∂μ)"
by(auto simp: mixture_of_def disintegration_def)
lemma disintegration_restrict_space:
assumes "disintegration ν μ" "A ∩ space X ∈ sets X"
shows "measure_kernel.disintegration (restrict_space X A) Y κ (restrict_space ν (A × space Y)) (restrict_space μ A)"
proof(rule measure_kernel.disintegrationI[OF restrict_measure_kernel[of A]])
have "sets (restrict_space ν (A × space Y)) = sets (restrict_space (X ⨂⇩M Y) (A × space Y))"
by(auto simp: disintegration_sets_eq[OF assms(1)] intro!: sets_restrict_space_cong)
also have "... = sets (restrict_space X A ⨂⇩M Y)"
using sets_pair_restrict_space[of X A Y "space Y"]
by simp
finally show "sets (restrict_space ν (A × space Y)) = sets (restrict_space X A ⨂⇩M Y)" .
next
show "sets (restrict_space μ A) = sets (restrict_space X A)"
by(auto simp: disintegration_sets_eq[OF assms(1)] intro!: sets_restrict_space_cong)
next
fix a b
assume h:"a ∈ sets (restrict_space X A)" "b ∈ sets Y"
then have "restrict_space ν (A × space Y) (a × b) = ν (a × b)"
using sets.sets_into_space
by(auto intro!: emeasure_restrict_space simp: disintegration_space_eq[OF assms(1)] disintegration_sets_eq[OF assms(1)] sets_restrict_space)
(metis Sigma_Int_distrib1 assms(2) pair_measureI sets.top space_pair_measure)
also have "... = (∫⇧+x∈a. emeasure (κ x) b ∂μ)"
using sets_restrict_space_iff[OF assms(2)] h assms(1)
by(auto simp: disintegration_def)
also have "... = (∫⇧+x∈A. (emeasure (κ x) b * indicator a x) ∂μ)"
using h(1) by(auto intro!: nn_integral_cong simp: sets_restrict_space)
(metis IntD1 indicator_simps(1) indicator_simps(2) mult.comm_neutral mult_zero_right)
also have "... = (∫⇧+x∈a. emeasure (κ x) b ∂restrict_space μ A)"
by (metis (no_types, lifting) assms disintegration_sets_eq(2) disintegration_space_eq(2) nn_integral_cong nn_integral_restrict_space)
finally show "restrict_space ν (A × space Y) (a × b) = (∫⇧+x∈a. emeasure (κ x) b ∂restrict_space μ A)" .
qed
end
context subprob_kernel
begin
lemma countable_disintegration_AE_unique:
assumes "countable (space Y)" and [measurable_cong]:"sets Y = Pow (space Y)"
and "subprob_kernel X Y κ'" "sigma_finite_measure μ"
and "disintegration ν μ" "measure_kernel.disintegration X Y κ' ν μ"
shows "AE x in μ. κ x = κ' x"
proof -
interpret κ': subprob_kernel X Y κ' by fact
interpret s: sigma_finite_measure μ by fact
have sets_eq[measurable_cong]: "sets μ = sets X" "sets ν = sets (X ⨂⇩M Y)"
using assms(5) by(auto simp: disintegration_def)
have 1:"AE x in μ. ∀y ∈ space Y. κ x {y} = κ' x {y}"
unfolding AE_ball_countable[OF assms(1)]
proof
fix y
assume y: "y ∈ space Y"
show "AE x in μ. emeasure (κ x) {y} = emeasure (κ' x) {y}"
proof(rule s.sigma_finite)
fix J :: "nat ⇒ _"
assume J:"range J ⊆ sets μ" " ⋃ (range J) = space μ" "⋀i. emeasure μ (J i) ≠ ∞"
from y have [measurable]: "(λx. κ x {y}) ∈ borel_measurable X" "(λx. κ' x {y}) ∈ borel_measurable X"
using emeasure_measurable κ'.emeasure_measurable by auto
define A where "A ≡ {x ∈ space μ. κ x {y} ≤ κ' x {y}}"
have [measurable]:"A ∈ sets μ"
by(auto simp: A_def)
have A: "⋀x. x ∈ space μ ⟹ x ∉ A ⟹ κ' x {y} ≤ κ x {y}"
by(auto simp: A_def)
have 1: "AE x∈A in μ. κ x {y} = κ' x {y}"
proof -
have "AE x in μ. ∀n. (x ∈ A ∩ J n ⟶ κ x {y} = κ' x {y})"
unfolding AE_all_countable
proof
fix n
have ninf:"(∫⇧+x∈A ∩ J n. (κ x) {y}∂μ) < ∞"
proof -
have "(∫⇧+x∈A ∩ J n. (κ x) {y}∂μ) ≤ (∫⇧+x∈A ∩ J n. (κ x) (space Y) ∂μ)"
using kernel_sets y by(auto intro!: nn_integral_mono emeasure_mono simp: indicator_def disintegration_space_eq(2)[OF assms(5)])
also have "... ≤ (∫⇧+x∈A ∩ J n. 1 ∂μ)"
using subprob_space by(auto intro!: nn_integral_mono simp: indicator_def disintegration_space_eq(2)[OF assms(5)])
also have "... = μ (A ∩ J n)"
using J by simp
also have "... ≤ μ (J n)"
using J by (auto intro!: emeasure_mono)
also have "... < ∞"
using J(3)[of n] by (simp add: top.not_eq_extremum)
finally show ?thesis .
qed
have "(∫⇧+x. (κ' x) {y} * indicator (A ∩ J n) x - (κ x) {y} * indicator (A ∩ J n) x ∂μ) = (∫⇧+x∈A ∩ J n. (κ' x) {y} ∂μ) - (∫⇧+x∈A ∩ J n. (κ x) {y} ∂μ)"
using J ninf by(auto intro!: nn_integral_diff simp: indicator_def A_def)
also have "... = 0"
proof -
have 0: "ν ((A ∩ J n) × {y}) = (∫⇧+x∈A ∩ J n. (κ x) {y} ∂μ)"
using J y sets_eq by(auto intro!: disintegrationD[OF assms(5),of "A ∩ J n" "{y}"])
have [simp]: "(∫⇧+x∈A ∩ J n. (κ' x) {y} ∂μ) = ν ((A ∩ J n) × {y})"
using J y sets_eq by(auto intro!: κ'.disintegrationD[OF assms(6),of "A ∩ J n" "{y}",symmetric])
show ?thesis
using ninf by (simp add: 0 diff_eq_0_iff_ennreal)
qed
finally have assm:"AE x in μ. (κ' x) {y} * indicator (A ∩ J n) x - (κ x) {y} * indicator (A ∩ J n) x = 0"
using J by(simp add: nn_integral_0_iff_AE)
show "AE x∈A ∩ J n in μ. (κ x) {y} = (κ' x) {y}"
proof(rule AE_mp[OF assm])
show "AE x in μ. emeasure (κ' x) {y} * indicator (A ∩ J n) x - emeasure (κ x) {y} * indicator (A ∩ J n) x = 0 ⟶ x ∈ A ∩ J n ⟶ emeasure (κ x) {y} = emeasure (κ' x) {y}"
proof -
{
fix x
assume h: "(κ' x) {y} - (κ x) {y} = 0" "x ∈ A"
have "(κ x) {y} = (κ' x) {y}"
using h(2) by(auto intro!: antisym ennreal_minus_eq_0[OF h(1)] simp: A_def)
}
thus ?thesis
by(auto simp: indicator_def)
qed
qed
qed
hence "AE x∈A ∩ (⋃ (range J))in μ. κ x {y} = κ' x {y}"
by auto
thus ?thesis
using J(2) by auto
qed
have 2: "AE x∈ (space μ - A) in μ. κ x {y} = κ' x {y}"
proof -
have "AE x in μ. ∀n. x ∈ (space μ - A) ∩ J n ⟶ κ x {y} = κ' x {y}"
unfolding AE_all_countable
proof
fix n
have ninf:"(∫⇧+x∈(space μ - A) ∩ J n. (κ' x) {y}∂μ) < ∞"
proof -
have "(∫⇧+x∈(space μ - A) ∩ J n. (κ' x) {y}∂μ) ≤ (∫⇧+x∈(space μ - A) ∩ J n. (κ' x) (space Y) ∂μ)"
using kernel_sets y by(auto intro!: nn_integral_mono emeasure_mono simp: indicator_def disintegration_space_eq(2)[OF assms(5)])
also have "... ≤ (∫⇧+x∈(space μ - A) ∩ J n. 1 ∂μ)"
using κ'.subprob_space by(auto intro!: nn_integral_mono simp: indicator_def disintegration_space_eq(2)[OF assms(5)])
also have "... = μ ((space μ - A) ∩ J n)"
using J by simp
also have "... ≤ μ (J n)"
using J by (auto intro!: emeasure_mono)
also have "... < ∞"
using J(3)[of n] by (simp add: top.not_eq_extremum)
finally show ?thesis .
qed
have "(∫⇧+x. (κ x) {y} * indicator ((space μ - A) ∩ J n) x - (κ' x) {y} * indicator ((space μ - A) ∩ J n) x ∂μ) = (∫⇧+x∈(space μ - A) ∩ J n. (κ x) {y} ∂μ) - (∫⇧+x∈(space μ - A) ∩ J n. (κ' x) {y} ∂μ)"
using J ninf A by(auto intro!: nn_integral_diff simp: indicator_def)
also have "... = 0"
proof -
have 0: "(∫⇧+x∈(space μ - A) ∩ J n. (κ' x) {y} ∂μ) = ν (((space μ - A) ∩ J n) × {y})"
using J y sets_eq by(auto intro!: κ'.disintegrationD[OF assms(6),of "(space μ - A) ∩ J n" "{y}",symmetric])
have [simp]: "ν (((space μ - A) ∩ J n) × {y}) = (∫⇧+x∈(space μ - A) ∩ J n. (κ x) {y} ∂μ)"
using J y sets_eq by(auto intro!: disintegrationD[OF assms(5),of "(space μ - A) ∩ J n" "{y}"])
show ?thesis
using ninf by (simp add: 0 diff_eq_0_iff_ennreal)
qed
finally have assm:"AE x in μ. (κ x) {y} * indicator ((space μ - A) ∩ J n) x - (κ' x) {y} * indicator ((space μ - A) ∩ J n) x = 0"
using J by(simp add: nn_integral_0_iff_AE)
show "AE x∈(space μ - A) ∩ J n in μ. (κ x) {y} = (κ' x) {y}"
proof(rule AE_mp[OF assm])
show "AE x in μ. emeasure (κ x) {y} * indicator ((space μ - A) ∩ J n) x - emeasure (κ' x) {y} * indicator ((space μ - A) ∩ J n) x = 0 ⟶ x ∈ (space μ - A) ∩ J n ⟶ emeasure (κ x) {y} = emeasure (κ' x) {y}"
proof -
{
fix x
assume h: "(κ x) {y} - (κ' x) {y} = 0" "x ∈ space μ" "x ∉ A"
have "(κ x) {y} = (κ' x) {y}"
using A[OF h(2,3)] by(auto intro!: antisym ennreal_minus_eq_0[OF h(1)] simp: A_def)
}
thus ?thesis
by(auto simp: indicator_def)
qed
qed
qed
hence "AE x∈(space μ - A) ∩ (⋃ (range J))in μ. κ x {y} = κ' x {y}"
by auto
thus ?thesis
using J(2) by auto
qed
show "AE x in μ. κ x {y} = κ' x {y}"
using 1 2 by(auto simp: A_def)
qed
qed
show ?thesis
proof(rule AE_mp[OF 1])
{
fix x
assume x: "x ∈ space X"
and h: "∀y∈space Y. κ x {y} = κ' x {y}"
have "κ x = κ' x "
by (simp add: κ'.kernel_sets assms h kernel_sets measure_eqI_countable x)
}
thus " AE x in μ. (∀y∈space Y. emeasure (κ x) {y} = emeasure (κ' x) {y}) ⟶ κ x = κ' x"
by(auto simp: sets_eq_imp_space_eq[OF sets_eq(1)])
qed
qed
end
lemma(in subprob_kernel) nu_mu_spaceY_le:
assumes "disintegration ν μ" "A ∈ sets X"
shows "ν (A × space Y) ≤ μ A"
proof -
have "ν (A × space Y) = (∫⇧+x∈A. (κ x (space Y)) ∂μ)"
using assms by(simp add: disintegration_def)
also have "... ≤ (∫⇧+x∈A. 1 ∂μ)"
using assms subprob_space by(auto intro!: nn_integral_mono simp: disintegration_space_eq) (metis dual_order.refl indicator_simps(1) indicator_simps(2) mult.commute mult_1 mult_zero_right)
also have "... = μ A"
using assms by (simp add: disintegration_def)
finally show ?thesis .
qed
context prob_kernel
begin
lemma countable_disintegration_AE_unique_prob:
assumes "countable (space Y)" and [measurable_cong]:"sets Y = Pow (space Y)"
and "prob_kernel X Y κ'" "sigma_finite_measure μ"
and "disintegration ν μ" "measure_kernel.disintegration X Y κ' ν μ"
shows "AE x in μ. κ x = κ' x"
by(auto intro!: countable_disintegration_AE_unique[OF assms(1,2) _ assms(4-6)] prob_kernel.subprob_kernel assms(3))
end
subsection ‹ Lemma 14.D.3. ›
lemma(in prob_kernel) nu_mu_spaceY:
assumes "disintegration ν μ" "A ∈ sets X"
shows "ν (A × space Y) = μ A"
proof -
have "ν (A × space Y) = (∫⇧+x∈A. (κ x (space Y)) ∂μ)"
using assms by(simp add: disintegration_def)
also have "... = (∫⇧+x∈A. 1 ∂μ)"
using assms by(auto intro!: nn_integral_cong simp: prob_space disintegration_space_eq)
also have "... = μ A"
using assms by (simp add: disintegration_def)
finally show ?thesis .
qed
corollary(in subprob_kernel) nu_finite:
assumes "disintegration ν μ" "finite_measure μ"
shows "finite_measure ν"
proof
have "ν (space ν) = ν (space (X ⨂⇩M Y))"
using assms by(simp add: disintegration_space_eq)
also have "... ≤ μ (space μ)"
using assms by(simp add: nu_mu_spaceY_le disintegration_space_eq space_pair_measure)
finally show "ν (space ν) ≠ ∞"
using assms(2) by (metis finite_measure.emeasure_finite infinity_ennreal_def neq_top_trans)
qed
corollary(in subprob_kernel) nu_subprob_space:
assumes "disintegration ν μ" "subprob_space μ"
shows "subprob_space ν"
proof
have "ν (space ν) = ν (space (X ⨂⇩M Y))"
using assms by(simp add: disintegration_space_eq)
also have "... ≤ μ (space μ)"
using assms by(simp add: nu_mu_spaceY_le disintegration_space_eq space_pair_measure)
finally show "ν (space ν) ≤ 1"
using assms(2) order.trans subprob_space.emeasure_space_le_1 by auto
next
show "space ν ≠ {}"
using Y_not_empty assms by(auto simp: disintegration_space_eq subprob_space_def subprob_space_axioms_def space_pair_measure)
qed
corollary(in prob_kernel) nu_prob_space:
assumes "disintegration ν μ" "prob_space μ"
shows "prob_space ν"
proof
have "ν (space ν) = ν (space (X ⨂⇩M Y))"
using assms by(simp add: disintegration_space_eq)
also have "... = μ (space μ)"
using assms by(simp add: nu_mu_spaceY disintegration_space_eq space_pair_measure)
finally show "ν (space ν) = 1"
by (simp add: assms(2) prob_space.emeasure_space_1)
qed
lemma(in subprob_kernel) nu_sigma_finite:
assumes "disintegration ν μ" "sigma_finite_measure μ"
shows "sigma_finite_measure ν"
proof
obtain A where A:"countable A" "A ⊆ sets μ" "⋃ A = space μ" "∀a∈A. emeasure μ a ≠ ∞"
using assms(2) by (meson sigma_finite_measure.sigma_finite_countable)
have "countable {a × space Y |a. a ∈ A}"
using countable_image[OF A(1),of "λa. a × space Y"]
by (simp add: Setcompr_eq_image)
moreover have "{a × space Y |a. a ∈ A} ⊆ sets ν"
using A(2) assms(1) disintegration_def by auto
moreover have "⋃ {a × space Y |a. a ∈ A} = space ν"
using assms A(3) by(simp add: disintegration_space_eq space_pair_measure) blast
moreover have "∀b∈{a × space Y |a. a ∈ A}. emeasure ν b ≠ ∞"
using neq_top_trans[OF _ nu_mu_spaceY_le[OF assms(1)]] A(2,4) assms disintegration_sets_eq(2) by auto
ultimately show "∃B. countable B ∧ B ⊆ sets ν ∧ ⋃ B = space ν ∧ (∀b∈B. emeasure ν b ≠ ∞)"
by blast
qed
subsection ‹ Theorem 14.D.4. (Measure Mixture Theorem) ›
lemma(in measure_kernel) exist_nu:
assumes "sets μ = sets X"
shows "∃ν. disintegration ν μ"
proof -
define ν where "ν = extend_measure (space X × space Y) {(a, b). a ∈ sets X ∧ b ∈ sets Y} (λ(a, b). a × b) (λ(a, b). ∫⇧+x∈a. emeasure (κ x) b∂μ) "
have 1: "sets ν = sets (X ⨂⇩M Y)"
proof -
have "sets ν = sigma_sets (space X × space Y) ((λ(a, b). a × b) ` {(a, b). a ∈ sets X ∧ b ∈ sets Y})"
unfolding ν_def
by(rule sets_extend_measure) (use sets.space_closed[of X] sets.space_closed[of Y] in blast)
also have "... = sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
by(auto intro!: sigma_sets_eqI)
also have "... = sets (X ⨂⇩M Y)"
by(simp add: sets_pair_measure)
finally show ?thesis .
qed
have 2: "ν (A × B) = (∫⇧+x∈A. (κ x B) ∂μ)" if "A ∈ sets X" "B ∈ sets Y" for A B
proof(rule extend_measure_caratheodory_pair[OF ν_def])
fix i j k l
assume "i ∈ sets X ∧ j ∈ sets Y" "k ∈ sets X ∧ l ∈ sets Y" "i × j = k × l"
then consider "i = k" "j = l" | "i × j = {}" "k × l = {}" by blast
thus "(∫⇧+x∈i. emeasure (κ x) j ∂μ) = (∫⇧+x∈k. emeasure (κ x) l ∂μ)"
by cases auto
next
fix A B j k
assume h: "⋀n::nat. A n ∈ sets X ∧ B n ∈ sets Y" "j ∈ sets X ∧ k ∈ sets Y" "disjoint_family (λn. A n × B n)" "(⋃i. A i × B i) = j × k"
show "(∑n. ∫⇧+x∈A n. emeasure (κ x) (B n)∂μ) = (∫⇧+x∈j. emeasure (κ x) k∂μ)"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+x. (∑n. κ x (B n) * indicator (A n) x)∂μ)"
proof(rule nn_integral_suminf[symmetric])
fix n
have [measurable]:"(λx. emeasure (κ x) (B n)) ∈ borel_measurable μ" "indicator (A n) ∈ borel_measurable μ"
using h(1)[of n] emeasure_measurable[of "B n"] assms(1) by auto
thus "(λx. emeasure (κ x) (B n) * indicator (A n) x) ∈ borel_measurable μ"
by simp
qed
also have "... = ?rhs"
proof(safe intro!: nn_integral_cong)
fix x
assume "x ∈ space μ"
consider "j = {}" | "k = {}" | "j ≠ {}" "k ≠ {}" by auto
then show "(∑n. emeasure (κ x) (B n) * indicator (A n) x) = emeasure (κ x) k * indicator j x"
proof cases
case 1
then have "⋀n. A n × B n = {}"
using h(4) by auto
have "emeasure (κ x) (B n) * indicator (A n) x = 0" for n
using ‹A n × B n = {}› by(auto simp: Sigma_empty_iff)
thus ?thesis
by(simp only: 1,simp)
next
case 2
then have "⋀n. A n × B n = {}"
using h(4) by auto
have "emeasure (κ x) (B n) * indicator (A n) x = 0" for n
using ‹A n × B n = {}› by(auto simp: Sigma_empty_iff)
thus ?thesis
by(simp only: 2,simp)
next
case 3
then have xinjiff:"x ∈ j ⟷ (∃i. ∃y∈B i. (x,y) ∈ A i × B i)"
using h(4) by blast
have bunk:"⋃ (B ` {i. x ∈ A i}) = k" if "x ∈ j"
using that 3 h(4) by blast
show ?thesis
proof(cases "x ∈ j")
case False
then have "⋀n. x ∉ A n ∨ B n = {}"
using h(4) 3 xinjiff by auto
have "emeasure (κ x) (B n) * indicator (A n) x = 0" for n
using ‹x ∉ A n ∨ B n = {}› by auto
thus ?thesis
by(simp only:)(simp add: False)
next
case True
then have [simp]: "emeasure (κ x) k * indicator j x = emeasure (κ x) k"
by simp
have "(∑n. emeasure (κ x) (B n) * indicator (A n) x) = (∑n. emeasure (κ x) (if x ∈ A n then B n else {}))"
by(auto intro!: suminf_cong)
also have "... = emeasure (κ x) (⋃n. if x ∈ A n then B n else {})"
proof(rule suminf_emeasure)
show "disjoint_family (λi. if x ∈ A i then B i else {})"
using disjoint_family_onD[OF h(3)] by (auto simp: disjoint_family_on_def)
next
show "range (λi. if x ∈ A i then B i else {}) ⊆ sets (κ x)"
using h(1) kernel_sets[of x] ‹x ∈ space μ› sets_eq_imp_space_eq[OF assms(1)] by auto
qed
also have "... = emeasure (κ x) k"
using True by(simp add: bunk)
finally show ?thesis by simp
qed
qed
qed
finally show ?thesis .
qed
qed(use that in auto)
show ?thesis
using 1 2 assms
by(auto simp: disintegration_def)
qed
lemma(in subprob_kernel) exist_unique_nu_sigma_finite':
assumes "sets μ = sets X" "sigma_finite_measure μ"
shows "∃!ν. disintegration ν μ"
proof -
obtain ν where disi: "disintegration ν μ"
using exist_nu[OF assms(1)] by auto
with assms(2) interpret sf: sigma_finite_measure ν
by(simp add: nu_sigma_finite)
interpret μ: sigma_finite_measure μ by fact
show ?thesis
proof(rule ex1I[where a=ν])
fix ν'
assume disi':"disintegration ν' μ"
show "ν' = ν"
proof(rule μ.sigma_finite_disjoint)
fix A :: "nat ⇒ _"
assume A: "range A ⊆ sets μ" "⋃ (range A) = space μ" "⋀i. emeasure μ (A i) ≠ ∞" "disjoint_family A"
define B where "B ≡ λi. A i × space Y"
show "ν' = ν"
proof(rule measure_eqI_generator_eq[where E=" {a × b|a b. a ∈ sets X ∧ b ∈ sets Y}" and A=B and Ω="space X × space Y"])
show "⋀C. C ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y} ⟹ emeasure ν' C = emeasure ν C"
"sets ν' = sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
"sets ν = sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
using disi disi' by(auto simp: disintegration_def sets_pair_measure)
next
show "range B ⊆ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
"⋃ (range B) = space X × space Y"
using A(1,2) by(auto simp: B_def assms(1) sets_eq_imp_space_eq[OF assms(1)])
next
fix i
show "emeasure ν' (B i) ≠ ∞"
using A(1) nu_mu_spaceY_le[OF disi',of "A i"] A(3)[of i] by(auto simp: B_def assms top.extremum_uniqueI)
qed(simp_all add: Int_stable_pair_measure_generator pair_measure_closed)
qed
qed fact
qed
lemma(in subprob_kernel) exist_unique_nu_sigma_finite:
assumes "sets μ = sets X" "sigma_finite_measure μ"
shows "∃!ν. disintegration ν μ ∧ sigma_finite_measure ν"
using assms exist_unique_nu_sigma_finite' nu_sigma_finite by blast
lemma(in subprob_kernel) exist_unique_nu_finite:
assumes "sets μ = sets X" "finite_measure μ"
shows "∃!ν. disintegration ν μ ∧ finite_measure ν"
using assms nu_finite finite_measure.sigma_finite_measure[OF assms(2)] exist_unique_nu_sigma_finite' by blast
lemma(in subprob_kernel) exist_unique_nu_sub_prob_space:
assumes "sets μ = sets X" "subprob_space μ"
shows "∃!ν. disintegration ν μ ∧ subprob_space ν"
using assms nu_subprob_space subprob_space_imp_sigma_finite[OF assms(2)] exist_unique_nu_sigma_finite' by blast
lemma(in prob_kernel) exist_unique_nu_prob_space:
assumes "sets μ = sets X" "prob_space μ"
shows "∃!ν. disintegration ν μ ∧ prob_space ν"
using assms nu_prob_space prob_space_imp_sigma_finite[OF assms(2)] exist_unique_nu_sigma_finite' by blast
lemma(in subprob_kernel) nn_integral_fst_finite':
assumes "f ∈ borel_measurable (X ⨂⇩M Y)" "disintegration ν μ" "finite_measure μ"
shows "(∫⇧+z. f z ∂ν) = (∫⇧+x. ∫⇧+y. f (x,y) ∂(κ x) ∂μ)"
using assms(1)
proof induction
case (cong f g)
have "integral⇧N ν f = integral⇧N ν g"
using cong(3) by(auto intro!: nn_integral_cong simp: disintegration_space_eq(1)[OF assms(2)])
with cong(3) show ?case
by(auto simp: cong(4) kernel_space disintegration_space_eq(2)[OF assms(2)] space_pair_measure intro!: nn_integral_cong)
next
case (set A)
show ?case
proof(rule sigma_sets_induct_disjoint[of "{a × b|a b. a ∈ sets X ∧ b ∈ sets Y}" "space X × space Y"])
show "A ∈ sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
using set by(simp add: sets_pair_measure)
next
fix A
assume "A ∈ {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
then obtain a b where ab: "A = a × b" "a ∈ sets X" "b ∈ sets Y"
by auto
with assms(2) have "integral⇧N ν (indicator A) = (∫⇧+x∈a. (κ x b) ∂μ)"
by(simp add: disintegration_def)
also have "... = (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
by(auto simp: ab(1) indicator_times disintegration_space_eq(2)[OF assms(2)] ab(3) kernel_sets mult.commute nn_integral_cmult_indicator intro!: nn_integral_cong)
finally show "integral⇧N ν (indicator A) = (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)" .
next
fix A
assume h: "A ∈ sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}" "integral⇧N ν (indicator A) = (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
show "integral⇧N ν (indicator (space X × space Y - A)) = (∫⇧+ x. ∫⇧+ y. indicator (space X × space Y - A) (x, y) ∂κ x ∂μ)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ z. 1 - indicator A z ∂ν)"
by(auto intro!: nn_integral_cong simp: disintegration_space_eq(1)[OF assms(2)] space_pair_measure indicator_def)
also have "... = (∫⇧+ z. 1 ∂ν) - (∫⇧+ z. indicator A z ∂ν)"
proof(rule nn_integral_diff)
show "integral⇧N ν (indicator A) ≠ ∞"
using h(1)[simplified sets_pair_measure[symmetric]] disintegration_sets_eq(1)[OF assms(2)] finite_measure.emeasure_finite[OF nu_finite[OF assms(2,3)]]
by auto
next
show "indicator A ∈ borel_measurable ν"
using h(1)[simplified sets_pair_measure[symmetric]] disintegration_sets_eq(1)[OF assms(2)] by simp
qed(simp_all add: indicator_def)
also have "... = (∫⇧+ z. 1 ∂ν) - (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
by(simp add: h(2))
also have "... = ν (space X × space Y) - (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
using nn_integral_indicator[OF sets.top[of ν]] by(simp add: space_pair_measure disintegration_space_eq(1)[OF assms(2)])
also have "... = (∫⇧+ x. κ x (space Y) ∂μ) - (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
proof -
have "ν (space X × space Y) = (∫⇧+ x. κ x (space Y) ∂μ)"
using assms(2) by(auto simp: disintegration_def disintegration_space_eq(2)[OF assms(2)] intro!: nn_integral_cong)
thus ?thesis by simp
qed
also have "... = (∫⇧+ x. ∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x ∂μ) - (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ)"
proof -
have "(∫⇧+ x. κ x (space Y) ∂μ) = (∫⇧+ x. ∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x ∂μ)"
using kernel_sets by(auto intro!: nn_integral_cong simp: indicator_times disintegration_space_eq(2)[OF assms(2)] )
thus ?thesis by simp
qed
also have "... = (∫⇧+ x. (∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x) - (∫⇧+ y. indicator A (x, y) ∂κ x) ∂μ)"
proof(rule nn_integral_diff[symmetric])
show "(λx. ∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x) ∈ borel_measurable μ"
"(λx. ∫⇧+ y. indicator A (x, y) ∂κ x) ∈ borel_measurable μ"
by(use disintegration_sets_eq[OF assms(2)] nn_integral_measurable_f h(1)[simplified sets_pair_measure[symmetric]] in auto)+
next
have "(∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ) ≤ (∫⇧+ x. ∫⇧+ y. 1 ∂κ x ∂μ)"
by(rule nn_integral_mono)+ (simp add: indicator_def)
also have "... ≤ (∫⇧+ x. 1 ∂μ)"
by(rule nn_integral_mono) (simp add: subprob_spaces disintegration_space_eq(2)[OF assms(2)] subprob_space.subprob_emeasure_le_1)
also have "... < ∞"
using finite_measure.emeasure_finite[OF assms(3)]
by (simp add: top.not_eq_extremum)
finally show "(∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂κ x ∂μ) ≠ ∞"
by auto
next
have "A ⊆ space X × space Y"
by (metis h(1) sets.sets_into_space sets_pair_measure space_pair_measure)
hence "⋀x. (∫⇧+ y. indicator A (x, y) ∂κ x) ≤ (∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x)"
by(auto intro!: nn_integral_mono)
thus "AE x in μ. (∫⇧+ y. indicator A (x, y) ∂κ x) ≤ (∫⇧+ y. indicator (space X × space Y) (x, y) ∂κ x)"
by simp
qed
also have "... = (∫⇧+ x. (∫⇧+ y. indicator (space X × space Y) (x, y) - indicator A (x, y) ∂κ x) ∂μ)"
proof(intro nn_integral_cong nn_integral_diff[symmetric])
fix x
assume "x ∈ space μ"
then have "x ∈ space X"
by(auto simp: disintegration_space_eq(2)[OF assms(2)])
with kernel_sets[OF this] h(1)[simplified sets_pair_measure[symmetric]]
show "(λy. indicator (space X × space Y) (x, y)) ∈ borel_measurable (κ x)"
"(λy. indicator A (x, y)) ∈ borel_measurable (κ x)"
by auto
next
fix x
assume "x ∈ space μ"
then have "x ∈ space X"
by(auto simp: disintegration_space_eq(2)[OF assms(2)])
have "(∫⇧+ y. indicator A (x, y) ∂κ x) ≤ (∫⇧+ y. 1 ∂κ x)"
by(rule nn_integral_mono) (simp add: indicator_def)
also have "... ≤ 1"
using subprob_spaces[OF ‹x ∈ space X›] by (simp add: subprob_space.subprob_emeasure_le_1)
also have "... < ∞"
by auto
finally show "(∫⇧+ y. indicator A (x, y) ∂κ x) ≠ ∞"
by simp
have "A ⊆ space X × space Y"
by (metis h(1) sets.sets_into_space sets_pair_measure space_pair_measure)
thus "AE y in κ x. indicator A (x, y) ≤ (indicator (space X × space Y) (x, y) :: ennreal)"
by auto
qed
also have "... = ?rhs"
by(auto simp: indicator_def intro!: nn_integral_cong)
finally show ?thesis .
qed
next
fix A
assume h:"disjoint_family A" "range A ⊆ sigma_sets (space X × space Y) {a × b |a b. a ∈ sets X ∧ b ∈ sets Y}"
"⋀i::nat. integral⇧N ν (indicator (A i)) = (∫⇧+ x. ∫⇧+ y. indicator (A i) (x, y) ∂κ x ∂μ)"
show "integral⇧N ν (indicator (⋃ (range A))) = (∫⇧+ x. ∫⇧+ y. indicator (⋃ (range A)) (x, y) ∂κ x ∂μ)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ z. (∑i. indicator (A i) z) ∂ν)"
by(simp add: suminf_indicator[OF h(1)])
also have "... = (∑i. (∫⇧+ z. indicator (A i) z ∂ν))"
by(rule nn_integral_suminf) (use disintegration_sets_eq(1)[OF assms(2)] h(2)[simplified sets_pair_measure[symmetric]] in simp)
also have "... = (∑i. (∫⇧+ x. ∫⇧+ y. indicator (A i) (x, y) ∂κ x ∂μ))"
by(simp add: h)
also have "... = (∫⇧+ x. (∑i. (∫⇧+ y. indicator (A i) (x, y) ∂κ x)) ∂μ)"
by(rule nn_integral_suminf[symmetric]) (use h(2)[simplified sets_pair_measure[symmetric]] disintegration_sets_eq(2)[OF assms(2)] nn_integral_measurable_f in simp)
also have "... = (∫⇧+ x. ∫⇧+ y. (∑i. indicator (A i) (x, y)) ∂κ x ∂μ)"
using h(2)[simplified sets_pair_measure[symmetric]] kernel_sets
by(auto intro!: nn_integral_cong nn_integral_suminf[symmetric] simp: disintegration_space_eq(2)[OF assms(2)])
also have "... = ?rhs"
by(simp add: suminf_indicator[OF h(1)])
finally show ?thesis .
qed
qed(simp_all add: Int_stable_pair_measure_generator pair_measure_closed)
next
case (mult u c)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = c * (∫⇧+ z. u z ∂ν)"
using disintegration_sets_eq(1)[OF assms(2)] mult
by(simp add: nn_integral_cmult)
also have "... = c * ( ∫⇧+ x. ∫⇧+ y. u (x, y) ∂κ x ∂μ)"
by(simp add: mult)
also have "... = ( ∫⇧+ x. c * (∫⇧+ y. u (x, y) ∂κ x) ∂μ)"
using nn_integral_measurable_f'[OF mult(2)] disintegration_sets_eq(2)[OF assms(2)]
by(simp add: nn_integral_cmult)
also have "... = ?rhs"
using mult by(auto intro!: nn_integral_cong nn_integral_cmult[symmetric] simp: disintegration_space_eq(2)[OF assms(2)])
finally show ?thesis .
qed
next
case (add u v)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ z. v z ∂ν) + (∫⇧+ z. u z ∂ν)"
using add disintegration_sets_eq(1)[OF assms(2)] by (simp add: nn_integral_add)
also have "... = (∫⇧+ x. ∫⇧+ y. v (x, y) ∂κ x ∂μ) + (∫⇧+ x. ∫⇧+ y. u (x, y) ∂κ x ∂μ)"
by(simp add: add)
also have "... = (∫⇧+ x. (∫⇧+ y. v (x, y) ∂κ x) + (∫⇧+ y. u (x, y) ∂κ x) ∂μ)"
using nn_integral_measurable_f'[OF add(1)] nn_integral_measurable_f'[OF add(3)] disintegration_sets_eq[OF assms(2)]
by(auto intro!: nn_integral_add[symmetric])
also have "... = (∫⇧+ x. (∫⇧+ y. v (x, y) + u (x, y) ∂κ x) ∂μ)"
using add by(auto intro!: nn_integral_add[symmetric] nn_integral_cong simp: disintegration_space_eq(2)[OF assms(2)])
finally show ?thesis .
qed
next
case (seq fi)
have "(∫⇧+ y. (⨆ range fi) (x, y) ∂κ x) = (⨆i. ∫⇧+ y. fi i (x, y) ∂κ x)" (is "?lhs = ?rhs") if "x ∈ space X" for x
proof -
have "?lhs = (∫⇧+ y. (⨆i. fi i (x, y)) ∂κ x)"
by(metis SUP_apply)
also have "... = ?rhs"
proof(rule nn_integral_monotone_convergence_SUP)
show "incseq (λi y. fi i (x, y))"
using seq mono_compose by blast
next
fix i
show "(λy. fi i (x, y)) ∈ borel_measurable (κ x)"
using seq(1)[of i] that kernel_sets[OF that] by simp
qed
finally show ?thesis .
qed
have "integral⇧N ν (⨆ range fi) = (∫⇧+ x. (⨆i. fi i x) ∂ν)"
by (metis SUP_apply)
also have "... = (⨆i. integral⇧N ν (fi i))"
using disintegration_sets_eq(1)[OF assms(2)] seq(1,3)
by(auto intro!: nn_integral_monotone_convergence_SUP)
also have "... = (⨆i. ∫⇧+ x. ∫⇧+ y. fi i (x, y) ∂κ x ∂μ)"
by(simp add: seq)
also have "... = (∫⇧+ x. (⨆i. ∫⇧+ y. fi i (x, y) ∂κ x) ∂μ)"
proof(safe intro!: nn_integral_monotone_convergence_SUP[symmetric])
show "incseq (λi x. ∫⇧+ y. fi i (x, y) ∂κ x)"
using le_funD[OF incseq_SucD[OF seq(3)]]
by(auto intro!: incseq_SucI le_funI nn_integral_mono)
qed(use disintegration_sets_eq(2)[OF assms(2)] nn_integral_measurable_f'[OF seq(1)] in auto)
also have "... = (∫⇧+ x. ∫⇧+ y. (⨆i. fi i (x, y)) ∂κ x ∂μ)"
using kernel_sets seq(1)
by(auto intro!: nn_integral_cong nn_integral_monotone_convergence_SUP[symmetric] simp: disintegration_space_eq(2)[OF assms(2)] mono_compose seq(3))
also have "... = (∫⇧+ x. ∫⇧+ y. (⨆ range fi) (x, y) ∂κ x ∂μ)"
by(auto intro!: nn_integral_cong simp: image_image)
finally show ?case .
qed
lemma(in prob_kernel) nn_integral_fst:
assumes "f ∈ borel_measurable (X ⨂⇩M Y)" "disintegration ν μ" "sigma_finite_measure μ"
shows "(∫⇧+z. f z ∂ν) = (∫⇧+x. ∫⇧+y. f (x,y) ∂(κ x) ∂μ)"
proof(rule sigma_finite_measure.sigma_finite_disjoint[OF assms(3)])
fix A
assume A:"range A ⊆ sets μ" "⋃ (range A) = space μ" "⋀i::nat. emeasure μ (A i) ≠ ∞" "disjoint_family A"
then have A': "range (λi. A i × space Y) ⊆ sets ν" "⋃ (range (λi. A i × space Y)) = space ν" "disjoint_family (λi. A i × space Y)"
by(auto simp: disintegration_sets_eq[OF assms(2)] disjoint_family_on_def disintegration_space_eq[OF assms(2)] space_pair_measure) blast
show ?thesis (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+z∈⋃ (range (λi. A i × space Y)). f z ∂ν)"
using A'(2) by auto
also have "... = (∑i. ∫⇧+z∈ A i × space Y. f z ∂ν)"
using A'(1,3) assms(1) disintegration_sets_eq[OF assms(2)]
by(auto intro!: nn_integral_disjoint_family)
also have "... = (∑i. ∫⇧+z. f z ∂restrict_space ν (A i × space Y))"
using A'(1) by(auto intro!: suminf_cong nn_integral_restrict_space[symmetric])
also have "... = (∑i. ∫⇧+x. ∫⇧+y. f (x,y) ∂(κ x) ∂restrict_space μ (A i))"
proof(safe intro!: suminf_cong)
fix n
interpret pk: prob_kernel "restrict_space X (A n)" Y κ
by(rule restrict_probability_kernel)
have An:"A n ∩ space X ∈ sets X" "A n ∩ space X = A n"
using A(1) by(auto simp: disintegration_sets_eq[OF assms(2)])
have f:"f ∈ borel_measurable (restrict_space X (A n) ⨂⇩M Y)"
proof -
have 1:"sets (restrict_space X (A n) ⨂⇩M Y) = sets (restrict_space (X ⨂⇩M Y) (A n × space Y))"
using sets_pair_restrict_space[where Y=Y and B="space Y"] by simp
show ?thesis
using assms(1) by(simp add: measurable_cong_sets[OF 1 refl] measurable_restrict_space1)
qed
have fin: "finite_measure (restrict_space μ (A n))"
by (metis A(1) A(3) UNIV_I emeasure_restrict_space finite_measureI image_subset_iff space_restrict_space space_restrict_space2 subset_eq)
show "(∫⇧+z. f z ∂restrict_space ν (A n × space Y)) = (∫⇧+x. ∫⇧+y. f (x,y) ∂(κ x) ∂restrict_space μ (A n))"
by(rule pk.nn_integral_fst_finite'[OF f disintegration_restrict_space[OF assms(2) An(1)] fin])
qed
also have "... = (∑i. ∫⇧+x∈A i. ∫⇧+y. f (x,y) ∂(κ x) ∂μ)"
using A(1) by(auto intro!: suminf_cong nn_integral_restrict_space)
also have "... = (∫⇧+x∈⋃ (range A). ∫⇧+y. f (x,y) ∂(κ x) ∂μ)"
using A(1,4) nn_integral_measurable_f'[OF assms(1)] disintegration_sets_eq[OF assms(2)]
by(auto intro!: nn_integral_disjoint_family[symmetric])
also have "... = ?rhs"
using A(2) by simp
finally show ?thesis .
qed
qed
lemma(in prob_kernel) integrable_eq1:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"f ∈ borel_measurable (X ⨂⇩M Y)"
and "disintegration ν μ" "sigma_finite_measure μ"
shows "(∫⇧+ z. ennreal (norm (f z)) ∂ν) < ∞ ⟷ (∫⇧+x. ∫⇧+y. ennreal (norm (f (x,y))) ∂(κ x) ∂μ) < ∞"
by(simp add: nn_integral_fst[OF _ assms(2,3)])
lemma(in prob_kernel) integrable_kernel_integrable:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "integrable ν f" "disintegration ν μ" "sigma_finite_measure μ"
shows "AE x in μ. integrable (κ x) (λy. f (x,y))"
proof -
have [measurable]:"f ∈ borel_measurable (X ⨂⇩M Y)"
using integrable_iff_bounded assms(1) disintegration_sets_eq[OF assms(2)] by simp
show ?thesis
unfolding integrable_iff_bounded
proof -
have 1:"(∫⇧+ x. ∫⇧+ y. ennreal (norm (f (x,y))) ∂κ x ∂μ) < ∞"
using assms(1) integrable_eq1[OF _ assms(2,3),of f] by(simp add: integrable_iff_bounded)
have "AE x in μ. (∫⇧+ y. ennreal (norm (f (x,y))) ∂κ x) ≠ ∞"
by(rule nn_integral_PInf_AE) (use 1 disintegration_sets_eq[OF assms(2)] nn_integral_measurable_f in auto)
thus "AE x in μ. (λy. f (x, y)) ∈ borel_measurable (κ x) ∧ (∫⇧+ y. ennreal (norm (f (x,y))) ∂κ x) < ∞"
using top.not_eq_extremum by(fastforce simp: disintegration_space_eq[OF assms(2)])
qed
qed
lemma(in prob_kernel) integrable_lebesgue_integral_integrable':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "integrable ν f" "disintegration ν μ" "sigma_finite_measure μ"
shows "integrable μ (λx. ∫y. f (x,y) ∂(κ x))"
unfolding integrable_iff_bounded
proof
show "(λx. ∫y. f (x,y) ∂(κ x)) ∈ borel_measurable μ"
using disintegration_sets_eq[OF assms(2)] assms(1) integral_measurable_f'[of f]
by(auto simp: integrable_iff_bounded)
next
have "(∫⇧+ x. ennreal (norm (∫y. f (x,y) ∂(κ x))) ∂μ) ≤ (∫⇧+ x. ∫⇧+y. ennreal (norm (f (x,y))) ∂(κ x) ∂μ)"
using integral_norm_bound_ennreal integrable_kernel_integrable[OF assms]
by(auto intro!: nn_integral_mono_AE)
also have "... < ∞"
using integrable_eq1[OF _ assms(2,3),of f] assms(1) disintegration_sets_eq[OF assms(2)]
by(simp add: integrable_iff_bounded)
finally show "(∫⇧+ x. ennreal (norm (∫y. f (x,y) ∂(κ x))) ∂μ) < ∞" .
qed
lemma(in prob_kernel) integrable_lebesgue_integral_integrable:
fixes f :: "_ ⇒_ ⇒ _::{banach, second_countable_topology}"
assumes "integrable ν (λ(x,y). f x y)" "disintegration ν μ" "sigma_finite_measure μ"
shows "integrable μ (λx. ∫y. f x y ∂(κ x))"
using integrable_lebesgue_integral_integrable'[OF assms] by simp
lemma(in prob_kernel) integral_fst:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "integrable ν f" "disintegration ν μ" "sigma_finite_measure μ"
shows "(∫z. f z ∂ν) = (∫x. ∫y. f (x,y) ∂(κ x) ∂μ)"
using assms(1)
proof induct
case b:(base A c)
then have 0:"integrable ν (indicat_real A)"
by blast
then have 1[measurable]: "indicat_real A ∈ borel_measurable (X ⨂⇩M Y)"
using disintegration_sets_eq[OF assms(2)] by auto
have eq:"(∫z. indicat_real A z ∂ν) = (∫x. ∫y. indicat_real A (x,y) ∂κ x ∂μ)" (is "?lhs = ?rhs")
proof -
have "?lhs = enn2real (∫⇧+ z. ennreal (indicat_real A z) ∂ν)"
by(rule integral_eq_nn_integral) (use b in auto)
also have "... = enn2real (∫⇧+ x. ∫⇧+ y. ennreal (indicat_real A (x,y)) ∂κ x ∂μ)"
using nn_integral_fst[OF _ assms(2,3)] b disintegration_sets_eq[OF assms(2)] by auto
also have "... = enn2real (∫⇧+ x. ennreal (∫ y. indicat_real A (x,y) ∂κ x) ∂μ)"
proof -
have "(∫⇧+ x. ∫⇧+ y. ennreal (indicat_real A (x,y)) ∂κ x ∂μ) = (∫⇧+ x. ennreal (∫ y. indicat_real A (x,y) ∂κ x) ∂μ)"
proof(safe intro!: nn_integral_cong nn_integral_eq_integral)
fix x
assume "x ∈ space μ"
then have "x ∈ space X"
by(simp add: disintegration_space_eq[OF assms(2)])
hence [simp]:"prob_space (κ x)" "sets (κ x) = sets Y" "space (κ x) = space Y"
by(auto intro!: prob_spaces sets_eq_imp_space_eq kernel_sets)
have [simp]:"{y. (x, y) ∈ A} ∈ sets Y"
proof -
have "{y. (x, y) ∈ A} = (λy. (x,y)) -` A ∩ space Y"
using b(1)[simplified disintegration_sets_eq[OF assms(2)]]
by auto
also have "... ∈ sets Y"
using b(1)[simplified disintegration_sets_eq[OF assms(2)]] ‹x ∈ space X›
by auto
finally show ?thesis .
qed
have [simp]: "(λy. indicat_real A (x, y)) = indicat_real {y. (x,y) ∈ A}"
by (auto simp: indicator_def)
show "integrable (κ x) (λy. indicat_real A (x, y))"
using prob_space.emeasure_le_1[of "κ x" "{y. (x, y) ∈ A}"]
by(auto simp add: integrable_indicator_iff order_le_less_trans)
qed simp
thus ?thesis by simp
qed
also have "... = ?rhs"
using disintegration_sets_eq[OF assms(2)] integral_measurable_f'[OF 1]
by(auto intro!: integral_eq_nn_integral[symmetric])
finally show ?thesis .
qed
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = (∫z. indicat_real A z ∂ν) *⇩R c"
using 0 by auto
also have "... = (∫x. ∫y. indicat_real A (x,y) ∂κ x ∂μ) *⇩R c"
by(simp only: eq)
also have "... = (∫x. (∫y. indicat_real A (x,y) ∂κ x) *⇩R c ∂μ)"
using integrable_lebesgue_integral_integrable'[OF 0 assms(2,3)]
by(auto intro!: integral_scaleR_left[symmetric])
also have "... = ?rhs"
using integrable_kernel_integrable[OF 0 assms(2,3)] integral_measurable_f'[of " indicat_real A"] integral_measurable_f'[of "λz. indicat_real A z *⇩R c"] disintegration_sets_eq[OF assms(2)]
by(auto intro!: integral_cong_AE)
finally show ?thesis .
qed
next
case fg:(add f g)
note [measurable] = integrable_lebesgue_integral_integrable'[OF fg(1) assms(2,3)] integrable_lebesgue_integral_integrable'[OF fg(3) assms(2,3)] integrable_lebesgue_integral_integrable'[OF Bochner_Integration.integrable_add[OF fg(1,3)] assms(2,3)]
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = (∫x. (∫y. f (x,y) ∂(κ x)) + (∫y. g (x,y) ∂(κ x)) ∂μ)"
by(simp add: Bochner_Integration.integral_add[OF fg(1,3)] fg Bochner_Integration.integral_add[OF integrable_lebesgue_integral_integrable'[OF fg(1) assms(2,3)] integrable_lebesgue_integral_integrable'[OF fg(3) assms(2,3)]])
also have "... = ?rhs"
using integrable_kernel_integrable[OF fg(1) assms(2,3)] integrable_kernel_integrable[OF fg(3) assms(2,3)]
by(auto intro!: integral_cong_AE)
finally show ?thesis .
qed
next
case (lim f s)
then have [measurable]: "f ∈ borel_measurable ν" "⋀i. s i ∈ borel_measurable ν"
by auto
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L ν (s i)) ⇢ integral⇧L ν f"
proof (rule integral_dominated_convergence)
show "integrable ν (λx. 2 * norm (f x))"
using lim(5) by auto
qed(use lim in auto)
next
have "(λi. ∫ x. ∫ y. s i (x, y) ∂(κ x) ∂μ) ⇢ ∫ x. ∫ y. f (x, y) ∂(κ x) ∂μ"
proof (rule integral_dominated_convergence)
have "AE x in μ. ∀i. integrable (κ x) (λy. s i (x, y))"
unfolding AE_all_countable using integrable_kernel_integrable[OF lim(1) assms(2,3)] ..
with AE_space integrable_kernel_integrable[OF lim(5) assms(2,3)]
show "AE x in μ. (λi. ∫ y. s i (x, y) ∂(κ x)) ⇢ ∫ y. f (x, y) ∂(κ x)"
proof eventually_elim
fix x assume x: "x ∈ space μ" and
s: "∀i. integrable (κ x) (λy. s i (x, y))" and f: "integrable (κ x) (λy. f (x, y))"
show "(λi. ∫ y. s i (x, y) ∂(κ x)) ⇢ ∫ y. f (x, y) ∂(κ x)"
proof (rule integral_dominated_convergence)
show "integrable (κ x) (λy. 2 * norm (f (x, y)))"
using f by auto
show "AE xa in (κ x). (λi. s i (x, xa)) ⇢ f (x, xa)"
using x lim(3) kernel_space by (auto simp: space_pair_measure disintegration_space_eq[OF assms(2)])
show "⋀i. AE xa in (κ x). norm (s i (x, xa)) ≤ 2 * norm (f (x, xa))"
using x lim(4) kernel_space by (auto simp: space_pair_measure disintegration_space_eq[OF assms(2)])
qed (use x disintegration_sets_eq[OF assms(2)] disintegration_space_eq[OF assms(2)] in auto)
qed
next
show "integrable μ (λx. (∫ y. 2 * norm (f (x, y)) ∂(κ x)))"
using integrable_lebesgue_integral_integrable'[OF _ assms(2,3),of "λz. 2 * norm (f (fst z, snd z))"] lim(5)
by auto
next
fix i show "AE x in μ. norm (∫ y. s i (x, y) ∂(κ x)) ≤ (∫ y. 2 * norm (f (x, y)) ∂(κ x))"
using AE_space integrable_kernel_integrable[OF lim(1) assms(2,3),of i] integrable_kernel_integrable[OF lim(5) assms(2,3)]
proof eventually_elim
case sf:(elim x)
from sf(2) have "norm (∫ y. s i (x, y) ∂(κ x)) ≤ (∫⇧+y. norm (s i (x, y)) ∂(κ x))"
by (rule integral_norm_bound_ennreal)
also have "… ≤ (∫⇧+y. 2 * norm (f (x, y)) ∂(κ x))"
using sf lim kernel_space by (auto intro!: nn_integral_mono simp: space_pair_measure disintegration_space_eq[OF assms(2)])
also have "… = (∫y. 2 * norm (f (x, y)) ∂(κ x))"
using sf by (intro nn_integral_eq_integral) auto
finally show "norm (∫ y. s i (x, y) ∂(κ x)) ≤ (∫ y. 2 * norm (f (x, y)) ∂(κ x))"
by simp
qed
qed(use integrable_lebesgue_integral_integrable'[OF lim(1) assms(2,3)] integrable_lebesgue_integral_integrable'[OF lim(5) assms(2,3)] disintegration_sets_eq[OF assms(2)] in auto)
then show "(λi. integral⇧L ν (s i)) ⇢ ∫ x. ∫ y. f (x, y) ∂(κ x) ∂μ"
using lim by simp
qed
qed
subsection ‹ Marginal Measure ›
definition marginal_measure_on :: "['a measure, 'b measure, ('a × 'b) measure, 'b set] ⇒ 'a measure" where
"marginal_measure_on X Y ν B = measure_of (space X) (sets X) (λA. ν (A × B))"
abbreviation marginal_measure :: "['a measure, 'b measure, ('a × 'b) measure] ⇒ 'a measure" where
"marginal_measure X Y ν ≡ marginal_measure_on X Y ν (space Y)"
lemma space_marginal_measure: "space (marginal_measure_on X Y ν B) = space X"
and sets_marginal_measure: "sets (marginal_measure_on X Y ν B) = sets X"
by(simp_all add: marginal_measure_on_def)
lemma emeasure_marginal_measure_on:
assumes "sets ν = sets (X ⨂⇩M Y)" "B ∈ sets Y" "A ∈ sets X"
shows "marginal_measure_on X Y ν B A = ν (A × B)"
unfolding marginal_measure_on_def
proof(rule emeasure_measure_of_sigma)
show "countably_additive (sets X) (λA. emeasure ν (A × B))"
proof(rule countably_additiveI)
fix A :: "nat ⇒ _"
assume h:"range A ⊆ sets X" "disjoint_family A" "⋃ (range A) ∈ sets X"
have [simp]: "(⋃i. A i × B) = (⋃ (range A) × B)"
by blast
have "range (λi. A i × B) ⊆ sets ν" "disjoint_family (λi. A i × B)"
using h assms(1,2) by(auto simp: disjoint_family_on_def)
from suminf_emeasure[OF this]
show " (∑i. ν (A i × B)) = ν (⋃ (range A) × B)"
by simp
qed
qed(insert assms, auto simp: positive_def sets.sigma_algebra_axioms)
lemma emeasure_marginal_measure:
assumes "sets ν = sets (X ⨂⇩M Y)" "A ∈ sets X"
shows "marginal_measure X Y ν A = ν (A × space Y)"
using emeasure_marginal_measure_on[OF assms(1) _ assms(2)] by simp
lemma finite_measure_marginal_measure_on_finite:
assumes "finite_measure ν" "sets ν = sets (X ⨂⇩M Y)" "B ∈ sets Y"
shows "finite_measure (marginal_measure_on X Y ν B)"
by (simp add: assms emeasure_marginal_measure_on finite_measure.emeasure_finite finite_measureI space_marginal_measure)
lemma finite_measure_marginal_measure_finite:
assumes "finite_measure ν" "sets ν = sets (X ⨂⇩M Y)"
shows "finite_measure (marginal_measure X Y ν)"
by(rule finite_measure_marginal_measure_on_finite[OF assms sets.top])
lemma marginal_measure_restrict_space:
assumes "sets ν = sets (X ⨂⇩M Y)" "B ∈ sets Y"
shows "marginal_measure X (restrict_space Y B) (restrict_space ν (space X × B)) = marginal_measure_on X Y ν B"
proof(rule measure_eqI)
fix A
assume "A ∈ sets (marginal_measure X (restrict_space Y B) (restrict_space ν (space X × B)))"
then have "A ∈ sets X"
by(simp add: sets_marginal_measure)
have 1:"sets (restrict_space ν (space X × B)) = sets (X ⨂⇩M restrict_space Y B)"
by (metis assms(1) restrict_space_space sets_pair_restrict_space sets_restrict_space_cong)
show "emeasure (marginal_measure X (restrict_space Y B) (restrict_space ν (space X × B))) A = emeasure (marginal_measure_on X Y ν B) A"
apply(simp add: emeasure_marginal_measure_on[OF assms(1) assms(2) ‹A ∈ sets X›] emeasure_marginal_measure[OF 1 ‹A ∈ sets X›])
apply(simp add: space_restrict_space)
by (metis Sigma_cong Sigma_mono ‹A ∈ sets X› assms(1) assms(2) emeasure_restrict_space inf_le1 pair_measureI sets.Int_space_eq2 sets.sets_into_space sets.top)
qed(simp add: sets_marginal_measure)
lemma restrict_space_marginal_measure_on:
assumes "sets ν = sets (X ⨂⇩M Y)" "B ∈ sets Y" "A ∈ sets X"
shows "restrict_space (marginal_measure_on X Y ν B) A = marginal_measure_on (restrict_space X A) Y (restrict_space ν (A × space Y)) B"
proof(rule measure_eqI)
fix A'
assume "A' ∈ sets (restrict_space (marginal_measure_on X Y ν B) A)"
then have h:"A' ∈ sets.restricted_space X A"
by(simp add: sets_marginal_measure sets_restrict_space)
show "emeasure (restrict_space (marginal_measure_on X Y ν B) A) A' = emeasure (marginal_measure_on (restrict_space X A) Y (restrict_space ν (A × space Y)) B) A'" (is "?lhs = ?rhs")
proof -
have 1:"sets (restrict_space ν (A × space Y)) = sets (restrict_space X A ⨂⇩M Y)"
by (metis assms(1) restrict_space_space sets_pair_restrict_space sets_restrict_space_cong)
have "?lhs = emeasure (marginal_measure_on X Y ν B) A'"
using h by(auto intro!: emeasure_restrict_space simp: space_marginal_measure sets_marginal_measure assms)
also have "... = ν (A' × B)"
using emeasure_marginal_measure_on[OF assms(1,2),of A'] h assms(3) by auto
also have "... = restrict_space ν (A × space Y) (A' × B)"
using h assms sets.sets_into_space
by(auto intro!: emeasure_restrict_space[symmetric])
also have "... = ?rhs"
using emeasure_marginal_measure_on[OF 1 assms(2),simplified sets_restrict_space,OF h] ..
finally show ?thesis .
qed
qed(simp add: sets_marginal_measure sets_restrict_space)
lemma restrict_space_marginal_measure:
assumes "sets ν = sets (X ⨂⇩M Y)" "A ∈ sets X"
shows "restrict_space (marginal_measure X Y ν) A = marginal_measure (restrict_space X A) Y (restrict_space ν (A × space Y))"
using restrict_space_marginal_measure_on[OF assms(1) _ assms(2)] by simp
lemma marginal_measure_mono:
assumes "sets ν = sets (X ⨂⇩M Y)" "A ∈ sets Y" "B ∈ sets Y" "A ⊆ B"
shows "emeasure (marginal_measure_on X Y ν A) ≤ emeasure (marginal_measure_on X Y ν B)"
proof(rule le_funI)
fix U
show "emeasure (marginal_measure_on X Y ν A) U ≤ emeasure (marginal_measure_on X Y ν B) U"
proof -
have 1:"U × A ⊆ U × B" using assms(4) by auto
show ?thesis
proof(cases "U ∈ sets X")
case True
then show ?thesis
by (simp add: "1" assms emeasure_marginal_measure_on emeasure_mono)
next
case False
then show ?thesis
by (simp add: emeasure_notin_sets sets_marginal_measure)
qed
qed
qed
lemma marginal_measure_absolutely_countinuous:
assumes "sets ν = sets (X ⨂⇩M Y)" "A ∈ sets Y" "B ∈ sets Y" "A ⊆ B"
shows "absolutely_continuous (marginal_measure_on X Y ν B) (marginal_measure_on X Y ν A)"
using emeasure_marginal_measure[OF assms(1)] assms(2,3) le_funD[OF marginal_measure_mono[OF assms]]
by(auto intro!: mono_absolutely_continuous simp: sets_marginal_measure)
lemma marginal_measure_absolutely_continuous':
assumes "sets ν = sets (X ⨂⇩M Y)" "A ∈ sets Y"
shows "absolutely_continuous (marginal_measure X Y ν) (marginal_measure_on X Y ν A)"
by(rule marginal_measure_absolutely_countinuous[OF assms sets.top sets.sets_into_space[OF assms(2)]])
subsection ‹ Lemma 14.D.6. ›
locale sigma_finite_measure_on_pair =
fixes X :: "'a measure" and Y :: "'b measure" and ν :: "('a × 'b) measure"
assumes nu_sets[measurable_cong]: "sets ν = sets (X ⨂⇩M Y)"
and sigma_finite: "sigma_finite_measure ν"
begin
abbreviation "νx ≡ marginal_measure X Y ν"
end
locale projection_sigma_finite =
fixes X :: "'a measure" and Y :: "'b measure" and ν :: "('a × 'b) measure"
assumes nu_sets[measurable_cong]: "sets ν = sets (X ⨂⇩M Y)"
and marginal_sigma_finite: "sigma_finite_measure (marginal_measure X Y ν)"
begin
sublocale νx : sigma_finite_measure "marginal_measure X Y ν"
by(rule marginal_sigma_finite)
lemma ν_sigma_finite: "sigma_finite_measure ν"
proof(rule νx.sigma_finite[simplified sets_marginal_measure space_marginal_measure])
fix A :: "nat ⇒ _"
assume A: "range A ⊆ sets X" "⋃ (range A) = space X" "⋀i. marginal_measure X Y ν (A i) ≠ ∞"
define C where "C ≡ range (λn. A n × space Y)"
have 1:"C ⊆ sets ν" "countable C" "⋃ C = space ν"
using nu_sets A(1,2) by(auto simp: C_def sets_eq_imp_space_eq[OF nu_sets] space_pair_measure)
show "sigma_finite_measure ν"
unfolding sigma_finite_measure_def
proof(safe intro!: exI[where x=C,simplified C_def])
fix n
assume "ν (A n × space Y) = ∞"
moreover have "ν (A n × space Y) ≠ ∞"
using A(3)[of n] emeasure_marginal_measure[OF nu_sets,of "A n"] A(1) by auto
ultimately show False by auto
qed (use 1 C_def in auto)
qed
sublocale sigma_finite_measure_on_pair
using ν_sigma_finite by(auto simp: sigma_finite_measure_on_pair_def nu_sets)
definition κ' :: "'a ⇒ 'b set ⇒ ennreal" where
"κ' x B ≡ RN_deriv νx (marginal_measure_on X Y ν B) x"
lemma kernel_measurable[measurable]:
"(λx. RN_deriv (marginal_measure X Y ν) (marginal_measure_on X Y ν B) x) ∈ borel_measurable νx"
by simp
corollary κ'_measurable[measurable]:
"(λx. κ' x B) ∈ borel_measurable X"
using sets_marginal_measure[of X Y ν "space Y"] by(auto simp: κ'_def)
lemma kernel_RN_deriv:
assumes "A ∈ sets X" "B ∈ sets Y"
shows "ν (A × B) = (∫⇧+x∈A. κ' x B ∂νx)"
unfolding κ'_def
proof -
have "emeasure ν (A × B) = emeasure (density νx (RN_deriv νx (marginal_measure_on X Y ν B))) A"
by (simp add: νx.density_RN_deriv assms emeasure_marginal_measure_on marginal_measure_absolutely_continuous' nu_sets sets_marginal_measure)
then show "emeasure ν (A × B) = set_nn_integral νx A (RN_deriv νx (marginal_measure_on X Y ν B))"
by (simp add: assms(1) emeasure_density sets_marginal_measure)
qed
lemma empty_Y_bot:
assumes "space Y = {}"
shows "ν = ⊥"
proof -
have "sets ν = {{}}"
using nu_sets space_empty_iff[of "X ⨂⇩M Y",simplified space_pair_measure] assms
by simp
thus ?thesis
by(simp add: sets_eq_bot)
qed
lemma empty_Y_nux:
assumes "space Y = {}"
shows "νx A = 0"
proof(cases "A ∈ sets X")
case True
from emeasure_marginal_measure[OF nu_sets this]
show ?thesis
by(simp add: assms)
next
case False
with sets_marginal_measure[of X Y ν "space Y"]
show ?thesis
by(auto intro!: emeasure_notin_sets)
qed
lemma kernel_empty0_AE:
"AE x in νx. κ' x {} = 0"
unfolding κ'_def by(rule AE_symmetric[OF νx.RN_deriv_unique]) (auto intro!: measure_eqI simp: sets_marginal_measure emeasure_density emeasure_marginal_measure_on[OF nu_sets])
lemma kernel_Y1_AE:
"AE x in νx. κ' x (space Y) = 1"
unfolding κ'_def by(rule AE_symmetric[OF νx.RN_deriv_unique]) (auto intro!: measure_eqI simp: emeasure_density)
lemma kernel_suminf_AE:
assumes "disjoint_family F"
and "⋀i. F i ∈ sets Y"
shows "AE x in νx. (∑i. κ' x (F i)) = κ' x (⋃ (range F))"
unfolding κ'_def
proof(rule νx.RN_deriv_unique)
show "density νx (λx. ∑i. RN_deriv local.νx (marginal_measure_on X Y ν (F i)) x) = marginal_measure_on X Y ν (⋃ (range F))"
proof(rule measure_eqI)
fix A
assume [measurable]:"A ∈ sets (density νx (λx. ∑i. RN_deriv νx (marginal_measure_on X Y ν (F i)) x))"
then have [measurable]:"A ∈ sets νx" "A ∈ sets X" by(auto simp: sets_marginal_measure)
show "(density νx (λx. ∑i. RN_deriv νx (marginal_measure_on X Y ν (F i)) x)) A = (marginal_measure_on X Y ν (⋃ (range F))) A"
(is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+x∈A. (∑i. RN_deriv νx (marginal_measure_on X Y ν (F i)) x)∂νx)"
by(auto intro!: emeasure_density)
also have "... = (∫⇧+x. (∑i. RN_deriv νx (marginal_measure_on X Y ν (F i)) x * indicator A x)∂νx)"
by simp
also have "... = (∑i. (∫⇧+x∈A. RN_deriv νx (marginal_measure_on X Y ν (F i)) x ∂νx))"
by(rule nn_integral_suminf) auto
also have "... = (∑i. ν (A × F i))"
using kernel_RN_deriv[of A "F _"] assms by(auto intro!: suminf_cong simp: κ'_def)
also have "... = ν (⋃i. A × F i)"
using assms nu_sets by(fastforce intro!: suminf_emeasure simp: disjoint_family_on_def)
also have "... = ν (A × (⋃i. F i))"
proof -
have "(⋃i. A × F i) = (A × (⋃i. F i))" by blast
thus ?thesis by simp
qed
also have "... = ?rhs"
using nu_sets assms by(auto intro!: emeasure_marginal_measure_on[symmetric])
finally show ?thesis .
qed
qed(simp add: sets_marginal_measure)
qed auto
lemma kernel_finite_sum_AE:
assumes "disjoint_family_on F S" "finite S"
and "⋀i. i ∈ S ⟹ F i ∈ sets Y"
shows "AE x in νx. (∑i∈S. κ' x (F i)) = κ' x (⋃i∈S. F i)"
proof -
consider "S = {}" | "S ≠ {}" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(simp add: kernel_empty0_AE)
next
case S:2
define F' where "F' ≡ (λn. if n < card S then F (from_nat_into S n) else {})"
have F'[simp]:"⋀i. F' i ∈ sets Y"
using assms(3)
by (metis F'_def bot.extremum_strict bot_nat_def card.empty from_nat_into sets.empty_sets)
have F'_disj: "disjoint_family F'"
unfolding disjoint_family_on_def
proof safe
fix m n x
assume h:"m ≠ n" "x ∈ F' m" "x ∈ F' n"
consider "n < card S" "m < card S" | "n ≥ card S" | "m ≥ card S" by arith
then show "x ∈ {}"
proof cases
case 1
then have "S ≠ {}"
by auto
with 1 have "from_nat_into S n ∈ S" "from_nat_into S m ∈ S"
using from_nat_into[of S ] by blast+
moreover have "from_nat_into S n ≠ from_nat_into S m"
by (metis "1"(1) "1"(2) assms(2) bij_betw_def h(1) lessThan_iff to_nat_on_finite to_nat_on_from_nat_into)
ultimately show ?thesis
using h assms(1) 1 by(auto simp: disjoint_family_on_def F'_def)
qed(use h F'_def in simp_all)
qed
have 1:"(∑i∈S. κ' x (F i)) = (∑i<card S. κ' x (F' i))" for x
unfolding F'_def by auto (metis (no_types, lifting) sum.card_from_nat_into sum.cong)
have 2: "(⋃ (range F')) = (⋃i∈S. F i)"
proof safe
fix x n
assume h:"x ∈ F' n"
then have "S ≠ {}" "n < card S"
by(auto simp: F'_def) (meson empty_iff)
with h show "x ∈ ⋃ (F ` S)"
by(auto intro!: exI[where x="from_nat_into S n"] simp: F'_def from_nat_into ‹S ≠ {}›)
next
fix x s
assume "s ∈ S" "x ∈ F s"
with bij_betwE[OF to_nat_on_finite[OF assms(2)]]
show "x ∈ ⋃ (range F')"
by(auto intro!: exI[where x="to_nat_on S s"] simp: F'_def from_nat_into_to_nat_on[OF countable_finite[OF assms(2)]])
qed
have "AE x in νx. (∑i<card S. κ' x (F' i)) = (∑i. κ' x (F' i))"
proof -
have "AE x in νx. ∀i≥card S. κ' x (F' i) = 0"
using kernel_empty0_AE by(auto simp: F'_def)
hence "AE x in νx. (∑i. κ' x (F' i)) = (∑i<card S. κ' x (F' i))"
proof
show "AE x in νx. (∀i≥card S. κ' x (F' i) = 0) ⟶ (∑i. κ' x (F' i)) = (∑i<card S. κ' x (F' i))"
proof -
{
fix x
assume "∀i≥card S. κ' x (F' i) = 0"
then have "(∑i. κ' x (F' i)) = (∑i<card S. κ' x (F' i))"
using suminf_offset[of "λi. κ' x (F' i)" "card S"]
by(auto simp: F'_def)
}
thus ?thesis
by auto
qed
qed
thus ?thesis
by auto
qed
moreover have "AE x in νx. (∑i. κ' x (F' i)) = κ' x (⋃ (range F'))"
using kernel_suminf_AE[OF F'_disj] by simp
ultimately show ?thesis
by(auto simp: 1 2)
qed
qed
lemma kernel_disjoint_sum_AE:
assumes "B ∈ sets Y" "C ∈ sets Y"
and "B ∩ C = {}"
shows "AE x in νx. κ' x (B ∪ C) = κ' x B + κ' x C"
proof -
define F where "F ≡ λb. if b then B else C"
have [simp]:"disjoint_family F" "⋀i. F i ∈ sets Y" "⋀x. (∑i∈UNIV. κ' x (F i)) = κ' x B + κ' x C" "⋃ (range F) = B ∪ C"
using assms by(auto simp: F_def disjoint_family_on_def comm_monoid_add_class.sum.Int_Diff[of UNIV _ "{True}"])
show ?thesis
using kernel_finite_sum_AE[of F UNIV] by auto
qed
lemma kernel_mono_AE:
assumes "B ∈ sets Y" "C ∈ sets Y"
and "B ⊆ C"
shows "AE x in νx. κ' x B ≤ κ' x C"
proof -
have 1: "B ∪ (C - B) = C" using assms(3) by auto
have "AE x in νx. κ' x C = κ' x B + κ' x (C - B)"
using assms by(auto intro!: kernel_disjoint_sum_AE[of B "C - B",simplified 1])
thus ?thesis
by auto
qed
lemma kernel_incseq_AE:
assumes "range B ⊆ sets Y" "incseq B"
shows "AE x in νx. incseq (λn. κ' x (B n))"
using assms(1) by(auto simp: incseq_Suc_iff AE_all_countable intro!: kernel_mono_AE[OF _ _ incseq_SucD[OF assms(2)]])
lemma kernel_decseq_AE:
assumes "range B ⊆ sets Y" "decseq B"
shows "AE x in νx. decseq (λn. κ' x (B n))"
using assms(1) by(auto simp: decseq_Suc_iff AE_all_countable intro!: kernel_mono_AE[OF _ _ decseq_SucD[OF assms(2)]])
corollary kernel_01_AE:
assumes "B ∈ sets Y"
shows "AE x in νx. 0 ≤ κ' x B ∧ κ' x B ≤ 1"
proof -
have "{} ⊆ B" "B ⊆ space Y"
using assms sets.sets_into_space by auto
from kernel_empty0_AE kernel_Y1_AE kernel_mono_AE[OF _ _ this(1)] kernel_mono_AE[OF _ _ this(2)] assms
show ?thesis
by auto
qed
lemma kernel_get_0: "0 ≤ κ' x B"
by simp
lemma kernel_le1_AE:
assumes "B ∈ sets Y"
shows "AE x in νx. κ' x B ≤ 1"
using kernel_01_AE[OF assms] by auto
corollary kernel_n_infty:
assumes "B ∈ sets Y"
shows "AE x in νx. κ' x B ≠ ⊤"
by(rule AE_mp[OF kernel_le1_AE[OF assms]],standard) (auto simp: neq_top_trans[OF ennreal_one_neq_top])
corollary kernel_le_infty:
assumes "B ∈ sets Y"
shows "AE x in νx. κ' x B < ⊤"
using kernel_n_infty[OF assms] by (simp add: top.not_eq_extremum)
lemma kernel_SUP_incseq:
assumes "range B ⊆ sets Y" "incseq B"
shows "AE x in νx. κ' x (⋃ (range B)) = (⨆n. κ' x (B n))"
proof -
define Bn where "Bn ≡ (λn. if n = 0 then {} else B (n - 1))"
have "incseq Bn"
using assms(2) by(auto simp: Bn_def incseq_def)
define Cn where "Cn ≡ (λn. Bn (Suc n) - Bn n)"
have Cn_simp: "Cn 0 = B 0" "Cn (Suc n) = B (Suc n) - B n" for n
by(simp_all add: Cn_def Bn_def)
have Cn_sets:"Cn n ∈ sets Y" for n
using assms(1) by(induction n) (auto simp: Cn_simp)
have Cn_disj: "disjoint_family Cn"
by(auto intro!: disjoint_family_Suc[OF ] incseq_SucD[OF ‹incseq Bn›] simp: Cn_def)
have Cn_un: "(⋃k<Suc n. Cn k) = B n" for n
using incseq_SucD[OF assms(2)]
by (induction n) (auto simp: Cn_simp lessThan_Suc sup_commute)
have Cn_sum_Bn:"AE x in νx. ∀n. (∑i<Suc n. κ' x (Cn i)) = κ' x (B n)"
unfolding AE_all_countable
using kernel_finite_sum_AE[OF disjoint_family_on_mono[OF _ Cn_disj],of "{..<Suc _}"] Cn_sets
by(auto simp: Cn_un)
have Cn_bn_un: "(⋃ (range B)) = (⋃ (range Cn))" (is "?lhs = ?rhs")
proof safe
fix n x
assume "x ∈ B n"
with Cn_un[of n] show "x ∈ ⋃ (range Cn)"
by blast
next
fix n x
assume "x ∈ Cn n"
then show "x ∈ ⋃ (range B)"
by(cases n,auto simp: Cn_simp)
qed
hence "AE x in νx. κ' x (⋃ (range B)) = κ' x (⋃ (range Cn))"
by simp
moreover have "AE x in νx. κ' x (⋃ (range Cn)) = (∑n. κ' x (Cn n))"
by(rule AE_symmetric[OF kernel_suminf_AE[OF Cn_disj]]) (use Cn_def Bn_def assms(1) in auto)
moreover have "AE x in νx. (∑n. κ' x (Cn n)) = (⨆n. ∑i<n. κ' x (Cn i))"
by(auto simp: suminf_eq_SUP)
moreover have "AE x in νx. (⨆n. ∑i<n. κ' x (Cn i)) = (⨆n. ∑i<Suc n. κ' x (Cn i))"
proof(intro AE_I2 antisym)
fix x
show "(⨆n. ∑i<n. κ' x (Cn i)) ≤ (⨆n. ∑i<Suc n. κ' x (Cn i))"
by(rule complete_lattice_class.Sup_mono, auto, use le_iff_add in blast)
next
fix x
show "(⨆n. ∑i<n. κ' x (Cn i)) ≥ (⨆n. ∑i<Suc n. κ' x (Cn i))"
by(rule complete_lattice_class.Sup_mono) blast
qed
moreover have "AE x in νx. (⨆n. ∑i<Suc n. κ' x (Cn i)) = (⨆n. κ' x (B n))"
by(rule AE_mp[OF Cn_sum_Bn]) (standard+, auto)
ultimately show ?thesis by auto
qed
lemma kernel_lim_incseq:
assumes "range B ⊆ sets Y" "incseq B"
shows "AE x in νx. (λn. κ' x (B n)) ⇢ κ' x (⋃ (range B))"
by(rule AE_mp[OF AE_conjI[OF kernel_SUP_incseq[OF assms] kernel_incseq_AE[OF assms]]],auto simp: LIMSEQ_SUP)
lemma kernel_INF_decseq:
assumes "range B ⊆ sets Y" "decseq B"
shows "AE x in νx. κ' x (⋂ (range B)) = (⨅n. κ' x (B n))"
proof -
define C where "C ≡ (λk. space Y - B k)"
have C:"range C ⊆ sets Y" "incseq C"
using assms by(auto simp: C_def decseq_def incseq_def)
have eq1: "AE x in νx. 1 - κ' x (⋂ (range B)) = κ' x (⋃ (range C))"
proof -
have "AE x in νx. κ' x (⋃ (range C)) + κ' x (⋂ (range B)) - κ' x (⋂ (range B)) = κ' x (⋃ (range C))"
using assms(1) kernel_n_infty[of "⋂ (range B)"] by auto
moreover have "AE x in νx. κ' x (⋃ (range C)) + κ' x (⋂ (range B)) = 1"
proof -
have [simp]:"(⋃ (range C)) ∪ (⋂ (range B)) = space Y" "(⋃ (range C)) ∩ (⋂ (range B)) = {}"
by(auto simp: C_def) (meson assms(1) range_subsetD sets.sets_into_space subsetD)
from kernel_disjoint_sum_AE[OF _ _ this(2)] C(1) assms(1) kernel_Y1_AE
show ?thesis by auto
qed
ultimately show ?thesis
by auto
qed
have eq2: "AE x in νx. κ' x (⋃ (range C)) = (⨆n. κ' x (C n))"
using kernel_SUP_incseq[OF C] by auto
have eq3: "AE x in νx. (⨆n. κ' x (C n)) = (⨆n. 1 - κ' x (B n))"
proof -
have "AE x in νx. ∀n. κ' x (C n) = 1 - κ' x (B n)"
unfolding AE_all_countable
proof safe
fix n
have "AE x in νx. κ' x (C n) + κ' x (B n) - κ' x (B n) = κ' x (C n)"
using assms(1) kernel_n_infty[of "B n"] by auto
moreover have "AE x in νx. κ' x (C n) + κ' x (B n) = 1"
proof -
have [simp]: "C n ∪ B n = space Y" "C n ∩ B n = {}"
by(auto simp: C_def) (meson assms(1) range_subsetD sets.sets_into_space subsetD)
thus ?thesis
using kernel_disjoint_sum_AE[of "C n" "B n"] C(1) assms(1) kernel_Y1_AE by fastforce
qed
ultimately show "AE x in νx. κ' x (C n) = 1 - κ' x (B n)" by auto
qed
thus ?thesis by auto
qed
have [simp]: "(⨆n. 1 - κ' x (B n)) = 1 - (⨅n. κ' x (B n))" for x
by(auto simp: ennreal_INF_const_minus)
have eq: "AE x in νx. 1 - κ' x (⋂ (range B)) = 1 - (⨅n. κ' x (B n))"
using eq1 eq2 eq3 by auto
have le1: "AE x in νx. (⨅n. κ' x (B n)) ≤ 1"
proof -
have "AE x in νx. ∀n. κ' x (B n) ≤ 1"
using assms(1) by(auto intro!: kernel_le1_AE simp: AE_all_countable)
thus ?thesis
by (auto simp: INF_lower2)
qed
show ?thesis
by(rule AE_mp[OF AE_conjI[OF AE_conjI[OF eq le1] kernel_le1_AE[of "⋂ (range B)"]]])
(insert assms(1),auto simp: ennreal_minus_cancel[OF ennreal_one_neq_top])
qed
lemma kernel_lim_decseq:
assumes "range B ⊆ sets Y" "decseq B"
shows "AE x in νx. (λn. κ' x (B n)) ⇢ κ' x (⋂ (range B))"
by(rule AE_mp[OF AE_conjI[OF kernel_INF_decseq[OF assms] kernel_decseq_AE[OF assms]]],standard,auto simp: LIMSEQ_INF)
end
lemma qlim_eq_lim_mono_at_bot:
fixes g :: "rat ⇒ 'a :: linorder_topology"
assumes "mono f" "(g ⤏ a) at_bot" "⋀r::rat. f (real_of_rat r) = g r"
shows "(f ⤏ a) at_bot"
proof -
have "mono g"
by(metis assms(1,3) mono_def of_rat_less_eq)
have ga:"⋀r. g r ≥ a"
proof(rule ccontr)
fix r
assume "¬ a ≤ g r"
then have "g r < a" by simp
from order_topology_class.order_tendstoD(1)[OF assms(2) this]
obtain Q :: rat where q: "⋀q. q ≤ Q ⟹ g r < g q"
by(auto simp: eventually_at_bot_linorder)
define q where "q ≡ min r Q"
show False
using q[of q] ‹mono g›
by(auto simp: q_def mono_def) (meson linorder_not_less min.cobounded1)
qed
show ?thesis
proof(rule decreasing_tendsto)
show "∀⇩F n in at_bot. a ≤ f n"
unfolding eventually_at_bot_linorder
by(rule exI[where x=undefined],auto) (metis Ratreal_def assms(1,3) dual_order.trans ga less_eq_real_def lt_ex monoD of_rat_dense)
next
fix x
assume "a < x"
with topological_space_class.topological_tendstoD[OF assms(2),of "{..<x}"]
obtain Q :: rat where q: "⋀q. q ≤ Q ⟹ g q < x"
by(auto simp: eventually_at_bot_linorder)
show "∀⇩F n in at_bot. f n < x"
using q assms(1,3) by(auto intro!: exI[where x="real_of_rat Q"] simp: eventually_at_bot_linorder) (metis dual_order.refl monoD order_le_less_trans)
qed
qed
lemma qlim_eq_lim_mono_at_top:
fixes g :: "rat ⇒ 'a :: linorder_topology"
assumes "mono f" "(g ⤏ a) at_top" "⋀r::rat. f (real_of_rat r) = g r"
shows "(f ⤏ a) at_top"
proof -
have "mono g"
by(metis assms(1,3) mono_def of_rat_less_eq)
have ga:"⋀r. g r ≤ a"
proof(rule ccontr)
fix r
assume "¬ g r ≤ a"
then have "a < g r" by simp
from order_topology_class.order_tendstoD(2)[OF assms(2) this]
obtain Q :: rat where q: "⋀q. Q ≤ q ⟹ g q < g r"
by(auto simp: eventually_at_top_linorder)
define q where "q ≡ max r Q"
show False
using q[of q] ‹mono g› by(auto simp: q_def mono_def leD)
qed
show ?thesis
proof(rule increasing_tendsto)
show "∀⇩F n in at_top. f n ≤ a"
unfolding eventually_at_top_linorder
by(rule exI[where x=undefined],auto) (metis (no_types, opaque_lifting) assms(1) assms(3) dual_order.trans ga gt_ex monoD of_rat_dense order_le_less)
next
fix x
assume "x < a"
with topological_space_class.topological_tendstoD[OF assms(2),of "{x<..}"]
obtain Q :: rat where q: "⋀q. Q ≤ q ⟹ x < g q"
by(auto simp: eventually_at_top_linorder)
show "∀⇩F n in at_top. x < f n"
using q assms(1,3) by(auto simp: eventually_at_top_linorder intro!: exI[where x="real_of_rat Q"]) (metis dual_order.refl monoD order_less_le_trans)
qed
qed
subsection ‹ Theorem 14.D.10. (Measure Disintegration Theorem) ›
locale projection_sigma_finite_standard = projection_sigma_finite + standard_borel_ne Y
begin
theorem measure_disintegration:
"∃κ. prob_kernel X Y κ ∧ measure_kernel.disintegration X Y κ ν νx ∧
(∀κ''. prob_kernel X Y κ'' ⟶ measure_kernel.disintegration X Y κ'' ν νx ⟶ (AE x in νx. κ x = κ'' x))"
proof -
have *:"∃κ. prob_kernel X (borel :: real measure) κ ∧ measure_kernel.disintegration X borel κ ν (marginal_measure X borel ν) ∧
(∀κ''. prob_kernel X borel κ'' ⟶ measure_kernel.disintegration X borel κ'' ν (marginal_measure X borel ν) ⟶ (AE x in (marginal_measure X borel ν). κ x = κ'' x))"
if nu_sets': "sets ν = sets (X ⨂⇩M borel)" and marginal_sigma_finite': "sigma_finite_measure (marginal_measure X borel ν)" for X :: "'a measure" and ν
proof -
interpret r: projection_sigma_finite X borel ν
using that by(auto simp: projection_sigma_finite_def)
define φ :: "'a ⇒ rat ⇒ real"
where "φ ≡ (λx r. enn2real (r.κ' x {..real_of_rat r}))"
have as1: "AE x in r.νx. ∀r s. r ≤ s ⟶ φ x r ≤ φ x s"
unfolding AE_all_countable
proof(safe intro!: AE_impI)
fix r s :: rat
assume "r ≤ s"
have "AE x in r.νx. r.κ' x {..real_of_rat k} < top" for k
using atMost_borel r.kernel_le_infty by blast
from this[of s] r.kernel_mono_AE[of "{..real_of_rat r}" "{..real_of_rat s}"] ‹r ≤ s›
show "AE x in r.νx. φ x r ≤ φ x s"
by(auto simp: φ_def of_rat_less_eq enn2real_mono)
qed
have as2: "AE x in r.νx. ∀r. (λn. φ x (r + 1 / rat_of_nat (Suc n))) ⇢ φ x r"
unfolding AE_all_countable
proof safe
fix r
have 1:"(⋂n. {..real_of_rat (r + 1 / rat_of_nat (Suc n))}) = {..real_of_rat r}"
proof safe
fix x
assume h:" x ∈ (⋂n. {..real_of_rat (r + 1 / rat_of_nat (Suc n))})"
show "x ≤ real_of_rat r"
proof(rule ccontr)
assume "¬ x ≤ real_of_rat r"
then have "0 < x - real_of_rat r" by simp
then obtain n where "(1 / (real (Suc n))) < x - real_of_rat r"
using nat_approx_posE by blast
hence "real_of_rat (r + 1 / (1 + rat_of_nat n)) < x"
by (simp add: of_rat_add of_rat_divide)
with h show False
using linorder_not_le by fastforce
qed
next
fix x n
assume "x ≤ real_of_rat r"
then show " x ≤ real_of_rat (r + 1 / rat_of_nat (Suc n))"
by (metis le_add_same_cancel1 of_nat_0_le_iff of_rat_less_eq order_trans zero_le_divide_1_iff)
qed
have "AE x in r.νx. (λn. r.κ' x {..real_of_rat (r + 1 / rat_of_nat (Suc n))}) ⇢ r.κ' x {..real_of_rat r}"
unfolding 1[symmetric] by(rule r.kernel_lim_decseq) (auto simp: decseq_Suc_iff of_rat_less_eq frac_le)
from AE_conjI[OF r.kernel_le_infty[of "{..real_of_rat r}",simplified] this]
show "AE x in r.νx. (λn. φ x (r + 1 / (rat_of_nat (Suc n)))) ⇢ φ x r"
unfolding φ_def by eventually_elim (rule tendsto_enn2real, auto)
qed
have as3: "AE x in r.νx. (φ x ⤏ 0) at_bot"
proof -
have 0: "range (λn. {..- real n}) ⊆ sets borel" "decseq (λn. {..- real n})"
by(auto simp: decseq_def)
show ?thesis
proof(safe intro!: AE_I2[THEN AE_mp[OF AE_conjI[OF r.kernel_empty0_AE AE_conjI[OF r.kernel_lim_decseq[OF 0] as1]]]])
fix x
assume h: "r.κ' x {} = 0" " (λn. r.κ' x {..- real n}) ⇢ r.κ' x (⋂n. {..- real n})" "∀r s. r ≤ s ⟶ φ x r ≤ φ x s"
have [simp]: "(⋂n. {..- real n}) = {}" by auto (meson le_minus_iff linorder_not_less reals_Archimedean2)
show "(φ x ⤏ 0) at_bot"
proof(rule decreasing_tendsto)
fix r :: real
assume "0 < r"
with h(2) eventually_sequentially
obtain N where N:"⋀n. n ≥ N ⟹ r.κ' x {..- real n} < r"
by(fastforce simp: order_tendsto_iff h(1))
show "∀⇩F q in at_bot. φ x q < r"
unfolding eventually_at_bot_linorder
proof(safe intro!: exI[where x="- rat_of_nat N"])
fix q
assume "q ≤ - rat_of_nat N"
with h(3) have "φ x q ≤ φ x (- rat_of_nat N)" by simp
also have "... < r"
by(auto simp: φ_def) (metis N[OF order_refl] ‹0 < r› enn2real_less_iff enn2real_top of_rat_minus of_rat_of_nat_eq top.not_eq_extremum)
finally show "φ x q < r" .
qed
qed(simp add: φ_def)
qed
qed
have as4: "AE x in r.νx. (φ x ⤏ 1) at_top"
proof -
have 0: "range (λn. {..real n}) ⊆ sets borel" "incseq (λn. {..real n})"
by(auto simp: incseq_def)
have [simp]: "(⋃n. {..real n}) = UNIV" by (auto simp: real_arch_simple)
have 1: "AE x in r.νx. ∀n. r.κ' x {..real n} ≤ 1" "AE x in r.νx. ∀q. r.κ' x {..real_of_rat q} ≤ 1"
by(auto simp: AE_all_countable intro!: r.kernel_le1_AE)
show ?thesis
proof(safe intro!: AE_I2[THEN AE_mp[OF AE_conjI[OF AE_conjI[OF 1] AE_conjI[OF r.kernel_Y1_AE AE_conjI[OF r.kernel_lim_incseq[OF 0] as1]]],simplified]])
fix x
assume h: "∀q. r.κ' x {..real_of_rat q} ≤ 1" "∀n. r.κ' x {..real n} ≤ 1"
"(λn. r.κ' x {..real n}) ⇢ r.κ' x UNIV" "∀r s. r ≤ s ⟶ φ x r ≤ φ x s" "r.κ' x UNIV = 1"
then have h3: "(λn. r.κ' x {..real n}) ⇢ 1"
by auto
show "(φ x ⤏ 1) at_top"
proof(rule increasing_tendsto)
fix r :: real
assume "r < 1"
with h3 eventually_sequentially
obtain N where N: "⋀n. n ≥ N ⟹ r < r.κ' x {..real n}"
by(fastforce simp: order_tendsto_iff)
show "∀⇩F n in at_top. r < φ x n"
unfolding eventually_at_top_linorder
proof(safe intro!: exI[where x="rat_of_nat N"])
fix q
assume "rat_of_nat N ≤ q"
have "r < φ x (rat_of_nat N)"
by(auto simp: φ_def) (metis N[OF order_refl] h(2) enn2real_1 enn2real_ennreal enn2real_positive_iff ennreal_cases ennreal_leI linorder_not_less zero_less_one)
also have "... ≤ φ x q"
using h(4) ‹rat_of_nat N ≤ q› by simp
finally show "r < φ x q" .
qed
qed(use h(1) enn2real_leI φ_def in auto)
qed
qed
from AE_E3[OF AE_conjI[OF as1 AE_conjI[OF as2 AE_conjI[OF as3 as4]]],simplified space_marginal_measure]
obtain N where N: "N ∈ null_sets r.νx" "⋀x r s. x ∈ space X - N ⟹ r ≤ s ⟹ φ x r ≤ φ x s"
"⋀x r. x ∈ space X - N ⟹ (λn. φ x (r + 1 / rat_of_nat (Suc n))) ⇢ φ x r"
"⋀x. x ∈ space X - N ⟹ (φ x ⤏ 0) at_bot" "⋀x. x ∈ space X - N ⟹ (φ x ⤏ 1) at_top"
by metis
define F where "F ≡ (λx y. indicat_real (space X - N) x * Inf {φ x r |r. y ≤ real_of_rat r} + indicat_real N x * indicat_real {0..} y)"
have [simp]: "{φ x r |r. y ≤ real_of_rat r} ≠ {}" for x y
by auto (meson gt_ex less_eq_real_def of_rat_dense)
have [simp]: "bdd_below {φ x r |r. y ≤ real_of_rat r}" if "x ∈ space X - N" for x y
proof -
obtain r' where "real_of_rat r' ≤ y"
by (metis less_eq_real_def lt_ex of_rat_dense)
from order_trans[OF this] of_rat_less_eq show ?thesis
by(auto intro!: bdd_belowI[of _ "φ x r'"] N(2)[OF that])
qed
have Feq: "F x (real_of_rat r) = φ x r" if "x ∈ space X - N" for x r
using that N(2)[OF that] by(auto intro!: cInf_eq_minimum simp: of_rat_less_eq F_def)
have Fmono: "mono (F x)" if "x ∈ space X" for x
by(auto simp: F_def mono_def indicator_def intro!: cInf_superset_mono) (meson gt_ex less_eq_real_def of_rat_dense)
have F1: "(F x ⤏ 0) at_bot" if "x ∈ space X" for x
proof(cases "x ∈ N")
case True
with that show ?thesis
by(auto simp: F_def tendsto_iff eventually_at_bot_dense indicator_def intro!: exI[where x=0])
next
case False
with qlim_eq_lim_mono_at_bot[OF Fmono[OF that] N(4)] Feq that
show ?thesis by auto
qed
have F2: "(F x ⤏ 1) at_top" if "x ∈ space X" for x
proof(cases "x ∈ N")
case True
with that show ?thesis
by(auto simp: F_def tendsto_iff eventually_at_top_dense indicator_def intro!: exI[where x=0])
next
case False
with qlim_eq_lim_mono_at_top[OF Fmono[OF that] N(5)] Feq that
show ?thesis by auto
qed
have F3: "continuous (at_right a) (F x)" if "x ∈ space X" for x a
proof(cases "x ∈ N")
case x:True
{
fix e :: real
assume e:"0 < e"
consider "a ≥ 0" | "a < 0" by fastforce
then have "∃d>0. indicat_real {0..} (a + d) - indicat_real {0..} a < e"
proof cases
case 1
with e show ?thesis
by(auto intro!: exI[where x=1])
next
case 2
then obtain b where "b > 0" "a + b < 0"
by (metis add_less_same_cancel2 of_rat_dense real_add_less_0_iff)
with e 2 show ?thesis
by(auto intro!: exI[where x=b])
qed
}
with x show ?thesis
unfolding continuous_at_right_real_increasing[of "F x",OF monoD[OF Fmono[OF that]],simplified]
by(auto simp: F_def)
next
case x:False
{
fix e :: real
assume e: "e > 0"
have "∃k. a ≤ real_of_rat k ∧ ⨅ {φ x r |r. a ≤ real_of_rat r} + e / 2 ≥ φ x k"
proof(rule ccontr)
assume "∄k. a ≤ real_of_rat k ∧ φ x k ≤ ⨅ {φ x r |r. a ≤ real_of_rat r} + e / 2"
then have cont: "⋀k. a ≤ real_of_rat k ⟹ φ x k - e / 2 > ⨅ {φ x r |r. a ≤ real_of_rat r}"
by auto
hence "a ≤ real_of_rat k ⟹ ∃r. a ≤ real_of_rat r ∧ φ x r < φ x k - e / 2" for k
using cont ‹x ∈ space X› x cInf_less_iff [of "{φ x r |r. a ≤ real_of_rat r}" "φ x k - e / 2"]
by auto
then obtain r where r:"⋀k. a ≤ real_of_rat k ⟹ a ≤ real_of_rat (r k)" "⋀k. a ≤ real_of_rat k ⟹ φ x (r k) < φ x k - e / 2"
by metis
obtain k where k:"a ≤ real_of_rat k"
by (meson gt_ex less_eq_real_def of_rat_dense)
define f where "f ≡ rec_nat k (λn fn. r fn)"
have f_simp: "f 0 = k" "f (Suc n) = r (f n)" for n
by(auto simp: f_def)
have f1: "a ≤ real_of_rat (f n)" for n
using r(1) k by(induction n) (auto simp: f_simp)
have f2: "n ≥ 1 ⟹ φ x (f n) < φ x k - real n * e / 2" for n
proof(induction n)
case ih:(Suc n)
consider "n = 0" | "n ≥ 1" by fastforce
then show ?case
proof cases
case 1
with r k show ?thesis
by(simp add: f_simp)
next
case 2
show ?thesis
using less_trans[OF r(2)[OF f1[of n]] diff_strict_right_mono[OF ih(1)[OF 2],of "e / 2"]]
by(auto simp: f_simp ring_distribs(2) add_divide_distrib)
qed
qed simp
have "¬ bdd_below {φ x r |r. a ≤ real_of_rat r}"
unfolding bdd_below_def
proof safe
fix M
obtain n where "φ x k - M < real n * e / 2"
using f2 e reals_Archimedean3 by fastforce
then have "φ x k - M < real (Suc n) * e / 2"
using divide_strict_right_mono pos_divide_less_eq e by fastforce
thus "Ball {φ x r |r. a ≤ real_of_rat r} ((≤) M) ⟹ False"
using f2[of "Suc n"] f1[of "Suc n"] by(auto intro!: exI[where x="φ x (f (Suc n))"])
qed
with that x show False
by simp
qed
then obtain k where k: "a ≤ real_of_rat k" "⨅ {φ x r |r. a ≤ real_of_rat r} + e / 2 ≥ φ x k"
by auto
obtain no where no:"⋀n. n≥no ⟹ (φ x (k + 1 / rat_of_nat (Suc n))) - (φ x k) < e / 2"
using ‹x ∈ space X› x metric_LIMSEQ_D[OF N(3)[of x k],of "e/2"] e N(2)[of x k "k + 1 / rat_of_nat (Suc _)"]
by(auto simp: dist_real_def)
have "∃d>0. ⨅ {φ x r |r. a + d ≤ real_of_rat r} - ⨅ {φ x r |r. a ≤ real_of_rat r} < e"
proof(safe intro!: exI[where x="real_of_rat (1 / rat_of_nat (Suc no))"])
have "φ x (k + 1 / rat_of_nat (Suc no)) - e < φ x k - e / 2"
using no[OF order_refl] by simp
also have "... ≤ ⨅ {φ x r |r. a ≤ real_of_rat r}"
using k by simp
finally have "φ x (k + 1 / rat_of_nat (Suc no)) - ⨅ {φ x r |r. a ≤ real_of_rat r} < e" by simp
moreover have "⨅ {φ x r |r. a + real_of_rat (1 / (1 + rat_of_nat no)) ≤ real_of_rat r} ≤ φ x (k + 1 / rat_of_nat (Suc no))"
using k that x by(auto intro!: cInf_lower simp: of_rat_add)
ultimately show "⨅ {φ x r |r. a + real_of_rat (1 / (rat_of_nat (Suc no))) ≤ real_of_rat r} - ⨅ {φ x r |r. a ≤ real_of_rat r} < e"
by simp
qed simp
}
with that x show ?thesis
unfolding continuous_at_right_real_increasing[of "F x",OF monoD[OF Fmono[OF that]],simplified]
by(auto simp: F_def)
qed
define κ where "κ ≡ (λx. interval_measure (F x))"
have κ: "⋀x. x ∈ space X ⟹ κ x UNIV = 1"
"⋀x r. x ∈ space X ⟹ κ x {..r} = ennreal (F x r)"
and[simp]: "⋀x. sets (κ x) = sets borel" "⋀x. space (κ x) = UNIV"
using emeasure_interval_measure_Iic[OF _ F3 F1] interval_measure_UNIV[OF _ F3 F1 F2] Fmono
by(auto simp: mono_def κ_def)
interpret κ: prob_kernel X borel κ
unfolding prob_kernel_def'
proof(rule measurable_prob_algebra_generated[OF _ atMostq_Int_stable,of _ UNIV])
show "⋀a. a ∈ space X ⟹ prob_space (κ a)"
by(auto intro!: prob_spaceI κ(1))
next
fix A
assume "A ∈ {{..r} |r::real. r ∈ ℚ}"
then obtain r where r: "A = {..real_of_rat r}"
using Rats_cases by blast
have "(λx. ennreal (indicat_real (space X - N) x * φ x r + indicat_real N x * indicat_real {0..} (real_of_rat r))) ∈ borel_measurable X"
proof -
have "N ∈ sets X"
using null_setsD2[OF N(1)] by(auto simp: sets_marginal_measure)
thus ?thesis by(auto simp: φ_def)
qed
moreover have "indicat_real (space X - N) x * φ x r + indicat_real N x * indicat_real {0..} (real_of_rat r) = emeasure (κ x) A" if "x ∈ space X" for x
using Feq[of x r] κ(2)[OF that,of "real_of_rat r"]
by(cases "x ∈ N") (auto simp: r indicator_def F_def)
ultimately show " (λx. emeasure (κ x) A) ∈ borel_measurable X"
using measurable_cong[of _ "λx. emeasure (κ x) A" "λx. ennreal (indicat_real (space X - N) x * φ x r + indicat_real N x * indicat_real {0..} (real_of_rat r))"]
by simp
qed(auto simp: rborel_eq_atMostq)
have κ_AE:"AE x in r.νx. κ x {..real_of_rat r} = r.κ' x {..real_of_rat r}" for r
proof -
have "AE x in r.νx. κ x {..real_of_rat r} = ennreal (F x (real_of_rat r))"
by(auto simp: space_marginal_measure κ(2))
moreover have "AE x in r.νx. ennreal (F x (real_of_rat r))= ennreal (φ x r)"
using Feq[of _ r] by(auto simp add: space_marginal_measure intro!: AE_I''[OF N(1)])
moreover have "AE x in r.νx. ennreal (φ x r) = ennreal (enn2real (r.κ' x {..real_of_rat r}))"
by(simp add: φ_def)
moreover have "AE x in r.νx. ennreal (enn2real (r.κ' x {..real_of_rat r})) = r.κ' x {..real_of_rat r}"
using r.kernel_le_infty[of "{..real_of_rat r}",simplified]
by(auto simp: ennreal_enn2real_if)
ultimately show ?thesis by auto
qed
have κ_dis: "κ.disintegration ν r.νx"
proof -
interpret D: Dynkin_system UNIV "{B ∈ sets borel. ∀A∈ sets X. ν (A × B) = (∫⇧+x∈A. (κ x) B∂r.νx)}"
proof
{
fix A
assume h:"A∈ sets X"
then have "ν (A × UNIV) = (∫⇧+x∈A. 1 ∂r.νx)"
using emeasure_marginal_measure[OF nu_sets' h] sets_marginal_measure[of X borel ν "space borel"] by auto
also have "... = (∫⇧+x∈A. (κ x) UNIV∂r.νx)"
by(auto intro!: nn_integral_cong simp: κ space_marginal_measure)
finally have "ν (A × UNIV) = (∫⇧+x∈A. emeasure (κ x) UNIV∂r.νx)" .
}
thus "UNIV ∈ {B ∈ sets borel. ∀A∈sets X. emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B∂r.νx)}"
by auto
hence univ:"⋀A. A ∈ sets X ⟹ ν (A × UNIV) = (∫⇧+x∈A. emeasure (κ x) UNIV∂r.νx)" by auto
show "⋀B. B ∈ {B ∈ sets borel. ∀A∈sets X. emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B∂r.νx)}
⟹ UNIV - B ∈ {B ∈ sets borel. ∀A∈sets X. emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B∂r.νx)}"
proof(rule r.νx.sigma_finite_disjoint)
fix B and J :: "nat ⇒ _"
assume "B ∈ {B ∈ sets borel. ∀A∈sets X. emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B ∂r.νx)}" "range J ⊆ sets r.νx" "⋃ (range J) = space r.νx"
"(⋀i. emeasure r.νx (J i) ≠ ∞)" "disjoint_family J"
then have B: "B ∈ sets borel" " ∀A∈sets X. ν (A × B) = (∫⇧+x∈A. (κ x) B∂r.νx)"
and J: "range J ⊆ sets X" "⋃ (range J) = space X" "⋀i. emeasure r.νx (J i) ≠ ∞" "disjoint_family J"
by (auto simp: sets_marginal_measure space_marginal_measure)
{
fix A
assume A: "A ∈ sets X"
have "ν (A × (UNIV - B)) = (∫⇧+x∈A. (κ x) (UNIV - B)∂r.νx)" (is "?lhs = ?rhs")
proof -
have AJi1: "disjoint_family (λi. (A ∩ J i) × (UNIV - B))"
using B(1) J(4) by(fastforce simp: disjoint_family_on_def)
have AJi2[simp]: "(⋃i. ((A ∩ J i) × (UNIV - B))) = A × (UNIV - B)"
using J(2) sets.sets_into_space[OF A] by blast
have AJi3: "(range (λi. (A ∩ J i) × (UNIV - B))) ⊆ sets ν"
using B(1) J(1) A by(auto simp: nu_sets')
have "?lhs = (∑i. ν ((A ∩ J i) × (UNIV - B)))"
by(simp add: suminf_emeasure[OF AJi3 AJi1])
also have "... = (∑i. (∫⇧+x∈ A ∩ J i. (κ x) (UNIV - B) ∂r.νx))"
proof(safe intro!: suminf_cong)
fix n
have Jn: "J n ∈ sets X"
using J by auto
have fin: "ν ((A ∩ J n) × C) ≠ ∞" for C
proof(cases "(A ∩ J n) × C ∈ sets ν")
case True
then have "ν ((A ∩ J n) × C) ≤ ν ((A ∩ J n) × UNIV)"
using Jn nu_sets' A by(intro emeasure_mono) auto
also have "ν ((A ∩ J n) × UNIV) ≤ ν (J n × UNIV)"
using Jn nu_sets' by(intro emeasure_mono) auto
also have "... = r.νx (J n)"
using emeasure_marginal_measure[OF nu_sets' Jn] by simp
finally show ?thesis
by (metis J(3)[of n] infinity_ennreal_def neq_top_trans)
qed(simp add: emeasure_notin_sets)
show "ν ((A ∩ J n) × (UNIV - B)) = (∫⇧+x∈ A ∩ J n. (κ x) (UNIV - B) ∂r.νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = ν ((A ∩ J n) × UNIV) - ν ((A ∩ J n) × B)"
proof -
have [simp]: "?lhs + ν ((A ∩ J n) × B) = ν ((A ∩ J n) × UNIV)"
proof -
have [simp]:"((A ∩ J n) × (UNIV - B)) ∪ ((A ∩ J n) × B) = ((A ∩ J n) × UNIV)" by blast
show ?thesis
using B(1) A Jn nu_sets' by(intro plus_emeasure[of "(A ∩ J n) × (UNIV - B)" _ "(A ∩ J n) × B",simplified]) auto
qed
have "?lhs = ?lhs + ν ((A ∩ J n) × B) - ν ((A ∩ J n) × B)"
by(simp only: ennreal_add_diff_cancel[OF fin[of B]])
also have "... = ν ((A ∩ J n) × UNIV) - ν ((A ∩ J n) × B)"
by simp
finally show ?thesis .
qed
also have "... = (∫⇧+x∈ A ∩ J n. (κ x) UNIV ∂r.νx) - (∫⇧+x∈ A ∩ J n. (κ x) B ∂r.νx)"
using B(2) A Jn univ by auto
also have "... = (∫⇧+x. ((κ x) UNIV * indicator (A ∩ J n) x - (κ x) B * indicator (A ∩ J n) x) ∂r.νx)"
proof(rule nn_integral_diff[symmetric])
show "(λx. (κ x) UNIV * indicator (A ∩ J n) x) ∈ borel_measurable r.νx" "(λx. (κ x) B * indicator (A ∩ J n) x) ∈ borel_measurable r.νx"
using sets_marginal_measure[of X borel ν "space borel"] κ.emeasure_measurable[OF B(1)] κ.emeasure_measurable[of UNIV] A Jn
by(auto simp del: space_borel)
next
show "(∫⇧+x∈A ∩ J n. (κ x) B∂r.νx) ≠ ∞"
using B(2) A Jn univ fin[of B] by auto
next
show "AE x in r.νx. (κ x) B * indicator (A ∩ J n) x ≤ (κ x) UNIV * indicator (A ∩ J n) x"
by(standard, auto simp: space_marginal_measure indicator_def intro!: emeasure_mono)
qed
also have "... = (∫⇧+x∈ A ∩ J n. ((κ x) UNIV - (κ x) B) ∂r.νx)"
by(auto intro!: nn_integral_cong simp: indicator_def)
also have "... = ?rhs"
proof(safe intro!: nn_integral_cong)
fix x
assume "x ∈ space r.νx"
then have "x ∈ space X"
by(simp add: space_marginal_measure)
show "((κ x) UNIV - (κ x) B) * indicator (A ∩ J n) x = (κ x) (UNIV - B) * indicator (A ∩ J n) x"
by(auto intro!: emeasure_compl[of B "κ x",simplified,symmetric] simp: B κ.prob_spaces ‹x ∈ space X› prob_space_imp_subprob_space subprob_space.emeasure_subprob_space_less_top indicator_def)
qed
finally show ?thesis .
qed
qed
also have "... = (∫⇧+x. (∑i. (κ x) (UNIV - B) * indicator (A ∩ J i) x)∂r.νx)"
using κ.emeasure_measurable[of "UNIV - B"] B(1) sets_marginal_measure[of X borel ν "space borel"] A J
by(intro nn_integral_suminf[symmetric]) (auto simp del: space_borel)
also have "... = (∫⇧+x. (κ x) (UNIV - B) * indicator A x * (∑i. indicator (A ∩ J i) x) ∂r.νx)"
by(auto simp: indicator_def intro!: nn_integral_cong)
also have "... = (∫⇧+x. (κ x) (UNIV - B) * indicator A x * (indicator (⋃i. A ∩ J i) x) ∂r.νx)"
proof -
have "(∑i. indicator (A ∩ J i) x) = (indicator (⋃i. A ∩ J i) x :: ennreal)" for x
using J(4) by(intro suminf_indicator) (auto simp: disjoint_family_on_def)
thus ?thesis
by(auto intro!: nn_integral_cong)
qed
also have "... = ?rhs"
using J(2) by(auto simp: indicator_def space_marginal_measure intro!: nn_integral_cong)
finally show ?thesis .
qed
}
thus "UNIV - B ∈ {B ∈ sets borel. ∀A∈sets X. emeasure ν (A × B) = (∫⇧+x∈A. emeasure (κ x) B ∂r.νx)}"
using B by auto
qed
next
fix J :: "nat ⇒ _"
assume J1: "disjoint_family J" "range J ⊆ {B ∈ sets borel. ∀A∈sets X. ν (A × B) = (∫⇧+x∈A. (κ x) B∂r.νx)}"
then have J2: "range J ⊆ sets borel" "⋃ (range J) ∈ sets borel" "⋀n A. A ∈ sets X ⟹ ν (A × (J n)) = (∫⇧+x∈A. (κ x) (J n) ∂r.νx)"
by auto
show "⋃ (range J) ∈ {B ∈ sets borel. ∀A∈sets X. ν (A × B) = (∫⇧+x∈A. (κ x) B∂r.νx)}"
proof -
{
fix A
assume A:"A ∈ sets X"
have "ν (A × ⋃ (range J)) = (∫⇧+x∈A. (κ x) (⋃ (range J)) ∂r.νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = ν (⋃n. A × J n)"
proof -
have "(A × ⋃ (range J)) = (⋃n. A × J n)" by blast
thus ?thesis by simp
qed
also have "... = (∑n. ν (A × J n))"
using J1(1) J2(1) A nu_sets' by(fastforce intro!: suminf_emeasure[symmetric] simp: disjoint_family_on_def)
also have "... = (∑n. (∫⇧+x∈A. (κ x) (J n) ∂r.νx))"
by(simp add: J2(3)[OF A])
also have "... = (∫⇧+x. (∑n. (κ x) (J n) * indicator A x) ∂r.νx)"
using κ.emeasure_measurable J2(1) A sets_marginal_measure[of X borel ν "space borel"]
by(intro nn_integral_suminf[symmetric]) auto
also have "... = (∫⇧+x∈A. (∑n. (κ x) (J n)) ∂r.νx)"
by auto
also have "... = (∫⇧+x∈A. (κ x) (⋃ (range J)) ∂r.νx)"
using J1 J2 by(auto intro!: nn_integral_cong suminf_emeasure simp: space_marginal_measure indicator_def)
finally show ?thesis .
qed
}
thus ?thesis
using J2(2) by auto
qed
qed auto
have "{ {..r} | r::real. r ∈ ℚ} ⊆ {B ∈ sets borel. ∀A∈ sets X. ν (A × B) = (∫⇧+x∈A. (κ x) B∂r.νx)}"
proof -
{
fix r ::real and A
assume h: "r ∈ ℚ" "A ∈ sets X"
then obtain r' where r':"r = real_of_rat r'"
using Rats_cases by blast
have "ν (A × {..r}) = (∫⇧+x∈A. (κ x) {..r} ∂r.νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+x∈A. r.κ' x {..r}∂r.νx)"
using h by(simp add: r.kernel_RN_deriv)
also have "... = ?rhs"
using κ_AE[of r'] by(auto intro!: nn_integral_cong_AE simp: r' simp del: space_borel)
finally show ?thesis .
qed
}
thus ?thesis
by auto
qed
from D.Dynkin_subset[OF this] rborel_eq_atMostq[symmetric]
show ?thesis
by(auto simp: κ.disintegration_def sets_marginal_measure nu_sets' sigma_eq_Dynkin[OF _ atMostq_Int_stable,of UNIV,simplified,symmetric] rborel_eq_atMostq_sets simp del: space_borel)
qed
show ?thesis
proof(intro exI conjI strip)
fix κ''
assume "prob_kernel X (borel :: real measure) κ''"
interpret κ'': prob_kernel X borel κ'' by fact
assume disi: "κ''.disintegration ν r.νx"
have eq_atMostr_AE:"AE x in r.νx. ∀r. κ x {..real_of_rat r} = κ'' x {..real_of_rat r}"
unfolding AE_all_countable
proof safe
fix r
have "AE x in r.νx. (κ'' x) {..real_of_rat r} = r.κ' x {..real_of_rat r}"
proof(safe intro!: r.νx.RN_deriv_unique[of "λx. κ'' x {..real_of_rat r}" "marginal_measure_on X borel ν {..real_of_rat r}",simplified r.κ'_def[of _ "{..real_of_rat r}",symmetric]])
show 1:"(λx. emeasure (κ'' x) {..real_of_rat r}) ∈ borel_measurable r.νx"
using κ''.emeasure_measurable[of "{..real_of_rat r}"] sets_marginal_measure[of X borel ν "space borel"] by simp
show "density r.νx (λx. emeasure (κ'' x) {..real_of_rat r}) = marginal_measure_on X borel ν {..real_of_rat r}"
proof(rule measure_eqI)
fix A
assume "A ∈ sets (density r.νx (λx. (κ'' x) {..real_of_rat r}))"
then have A [measurable]:"A ∈ sets X"
by(simp add: sets_marginal_measure)
show "emeasure (density r.νx (λx. emeasure (κ'' x) {..real_of_rat r})) A = emeasure (marginal_measure_on X borel ν {..real_of_rat r}) A" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+x∈A. (κ'' x) {..real_of_rat r} ∂r.νx)"
using emeasure_density[OF 1,of A] A
by(simp add: sets_marginal_measure)
also have "... = ν (A × {..real_of_rat r})"
using disi A by(auto simp: κ''.disintegration_def)
also have "... = ?rhs"
by(simp add: emeasure_marginal_measure_on[OF nu_sets' _ A])
finally show ?thesis .
qed
qed(simp add: sets_marginal_measure)
qed
with κ_AE[of r]
show "AE x in r.νx. κ x {..real_of_rat r} = κ'' x {..real_of_rat r}"
by auto
qed
{ fix x
assume h:"x ∈ space r.νx" " ∀r. (κ x) {..real_of_rat r} = (κ'' x) {..real_of_rat r}"
then have x: "x ∈ space X"
by(simp add: space_marginal_measure)
have "κ x = κ'' x"
proof(rule measure_eqI_generator_eq[OF atMostq_Int_stable,of UNIV _ _ "λn. {..real n}"])
show "⋀A. A ∈ {{..r} |r. r ∈ ℚ} ⟹ (κ x) A = (κ'' x) A"
using h(2) Rats_cases by auto
next
show "(⋃n. {..real n}) = UNIV"
by (simp add: real_arch_simple subsetI subset_antisym)
next
fix n
have "(κ x) {..real n} ≤ κ x UNIV"
by(auto intro!: emeasure_mono)
also have "... = 1"
by(rule κ(1)[OF x])
finally show "(κ x) {..real n} ≠ ∞"
using linorder_not_le by fastforce
next
show "range (λn. {..real n}) ⊆ {{..r} |r. r ∈ ℚ}"
using Rats_of_nat by blast
qed(auto simp: κ.kernel_sets[OF x] κ''.kernel_sets[OF x] rborel_eq_atMostq_sets)
}
then show "AE x in r.νx. κ x = κ'' x"
using eq_atMostr_AE by fastforce
qed(auto simp del: space_borel simp add: κ_dis κ.prob_kernel_axioms)
qed
show ?thesis
proof -
define ν' where "ν' = distr ν (X ⨂⇩M borel) (λ(x,y). (x, to_real y))"
have ν_distr:"ν = distr ν' (X ⨂⇩M Y) (λ(x,y). (x, from_real y))"
using nu_sets sets_eq_imp_space_eq[OF nu_sets] from_real_to_real
by(auto simp: ν'_def distr_distr space_pair_measure intro!: distr_id'[symmetric])
have νx_eq:"(marginal_measure X borel ν') = νx"
using emeasure_marginal_measure[of ν' X borel] emeasure_marginal_measure[OF nu_sets] sets_eq_imp_space_eq[OF nu_sets]
by(auto intro!: measure_eqI simp: sets_marginal_measure ν'_def emeasure_distr map_prod_vimage[of id to_real,simplified map_prod_def id_def] space_pair_measure Times_Int_Times)
interpret ν' : projection_sigma_finite X borel ν'
by(auto simp: projection_sigma_finite_def νx_eq νx.sigma_finite_measure_axioms simp del: space_borel,auto simp add: ν'_def)
obtain κ' where κ': "prob_kernel X borel κ'" "measure_kernel.disintegration X borel κ' ν' ν'.νx"
"⋀κ''. prob_kernel X borel κ'' ⟹ measure_kernel.disintegration X borel κ'' ν' ν'.νx ⟹ (AE x in ν'.νx. κ' x = κ'' x)"
using *[of ν' X] ν'.nu_sets ν'.νx.sigma_finite_measure_axioms by blast
interpret κ': prob_kernel X borel κ' by fact
define κ where "κ ≡ (λx. distr (κ' x) Y from_real)"
interpret κ: prob_kernel X Y κ
by(auto simp: prob_kernel_def' κ_def)
have disi: "κ.disintegration ν νx"
proof(rule κ.disintegrationI)
fix A B
assume A[measurable]:"A ∈ sets X" and B[measurable]: "B ∈ sets Y"
have [measurable]: "from_real -` B ∈ sets borel"
by(simp add: measurable_sets_borel[OF _ B])
show "ν (A × B) = (∫⇧+x∈A. κ x B∂νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = ν' (A × (from_real -` B))"
by(auto simp: ν_distr emeasure_distr map_prod_vimage[of id from_real,simplified map_prod_def id_def])
also have "... = (∫⇧+x∈A. κ' x (from_real -` B) ∂νx)"
using κ'.disintegrationD[OF κ'(2),of A "from_real -` B"]
by(auto simp add: νx_eq simp del: space_borel)
also have "... = ?rhs"
by(auto intro!: nn_integral_cong simp: space_marginal_measure κ_def emeasure_distr)
finally show ?thesis .
qed
qed(simp_all add: sets_marginal_measure nu_sets)
show ?thesis
proof(safe intro!: exI[where x=κ])
fix κ''
assume h:"prob_kernel X Y κ''"
"measure_kernel.disintegration X Y κ'' ν νx"
interpret κ'': prob_kernel X Y κ'' by fact
show "AE x in νx. κ x = κ'' x"
proof -
define κ''' where "κ''' ≡ (λx. distr (κ'' x) borel to_real)"
interpret κ''': prob_kernel X borel κ'''
by(auto simp: prob_kernel_def' κ'''_def)
have κ''_def: "κ'' x = distr (κ''' x) Y from_real" if "x ∈ space X" for x
using distr_distr[of from_real borel Y to_real "κ'' x",simplified measurable_cong_sets[OF κ''.kernel_sets[OF that] refl,of borel]]
by(auto simp: κ'''_def comp_def κ''.kernel_sets[OF that] measurable_cong_sets[OF κ''.kernel_sets[OF that] κ''.kernel_sets[OF that]] sets_eq_imp_space_eq[OF κ''.kernel_sets[OF that]] intro!: distr_id'[symmetric])
have κ'''_disi: "κ'''.disintegration ν' ν'.νx"
proof(rule κ'''.disintegrationI)
fix A and B :: "real set"
assume A[measurable]:"A ∈ sets X" and B[measurable]:"B ∈ sets borel"
show "ν' (A × B) = (∫⇧+x∈A. (κ''' x) B ∂ν'.νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = ν (A × (to_real -` B ∩ space Y))"
by(auto simp: ν'_def emeasure_distr map_prod_vimage[of id to_real,simplified map_prod_def id_def] sets_eq_imp_space_eq[OF nu_sets] space_pair_measure Times_Int_Times)
also have "... = (∫⇧+x∈A. (κ'' x) (to_real -` B ∩ space Y) ∂νx)"
using κ''.disintegrationD[OF h(2) A,of "to_real -` B ∩ space Y"] by auto
also have "... = ?rhs"
by(auto simp: νx_eq[symmetric] space_marginal_measure κ'''_def emeasure_distr sets_eq_imp_space_eq[OF κ''.kernel_sets] intro!: nn_integral_cong)
finally show ?thesis .
qed
qed(auto simp: ν'_def sets_marginal_measure)
show ?thesis
by(rule AE_mp[OF κ'(3)[OF κ'''.prob_kernel_axioms κ'''_disi,simplified νx_eq]],standard) (auto simp: space_marginal_measure κ''_def κ_def)
qed
qed(simp_all add: disi κ.prob_kernel_axioms)
qed
qed
end
subsection ‹ Lemma 14.D.12. ›
lemma ex_finite_density_measure:
fixes A :: "nat ⇒ _"
assumes A: "range A ⊆ sets M" "⋃ (range A) = space M" "⋀i. emeasure M (A i) ≠ ∞" "disjoint_family A"
defines "h ≡ (λx. (∑n. (1/2)^(Suc n) * (1 / (1 + M (A n))) * indicator (A n) x))"
shows "h ∈ borel_measurable M"
"⋀x. x ∈ space M ⟹ 0 < h x"
"⋀x. x ∈ space M ⟹ h x < 1"
"finite_measure (density M h)"
proof -
have less1:"0 < 1 / (1 + M (A n))" "1 / (1 + M (A n)) ≤ 1" for n
using A(3)[of n] ennreal_zero_less_divide[of 1 "1 + M (A n)"]
by (auto intro!: divide_le_posI_ennreal simp: add_pos_nonneg)
show [measurable]:"h ∈ borel_measurable M"
using A by(simp add: h_def)
{
fix x
assume x:"x ∈ space M"
then obtain i where i: "x ∈ A i"
using A(2) by auto
show "0 < h x"
using A(3)[of i] less1[of i]
by(auto simp: h_def suminf_pos_iff i ennreal_divide_times ennreal_zero_less_divide power_divide_distrib_ennreal power_less_top_ennreal intro!: exI[where x=i])
have "h x = (∑n. (1/2)^(Suc n + 2) * (1 / (1 + M (A (n + 2)))) * indicator (A (n + 2)) x) + (1/2) * (1 / (1 + M (A 0))) * indicator (A 0) x + (1/2)^2 * (1 / (1 + M (A 1))) * indicator (A 1) x"
by(auto simp: h_def suminf_split_head suminf_offset[of "λn. (1/2)^(Suc n) * (1 / (1 + M (A n))) * indicator (A n) x" 2] simp del: power_Suc sum_mult_indicator) (auto simp: numeral_2_eq_2)
also have "... ≤ 1/4 + (1/2) * (1 / (1 + M (A 0))) * indicator (A 0) x + (1/2)^2 * (1 / (1 + M (A 1))) * indicator (A 1) x"
proof -
have "(∑n. (1/2)^(Suc n + 2) * (1 / (1 + M (A (n + 2)))) * indicator (A (n + 2)) x) ≤ (∑n. (1/2)^(Suc n + 2))"
using less1(2)[of "Suc (Suc _)"] by(intro suminf_le,auto simp: indicator_def) (metis mult.right_neutral mult_left_mono zero_le)
also have "... = (∑n. ennreal ((1 / 2) ^ (Suc n + 2)))"
by(simp only: ennreal_power[of "1/2",symmetric]) (metis divide_ennreal ennreal_1 ennreal_numeral linorder_not_le not_one_less_zero zero_less_numeral)
also have "... = ennreal (∑n. (1 / 2) ^ (Suc n + 2))"
by(rule suminf_ennreal2) auto
also have "... = ennreal (1/4)"
using nsum_of_r'[of "1/2" "Suc (Suc (Suc 0))" 1] by auto
also have "... = 1 / 4"
by (metis ennreal_divide_numeral ennreal_numeral numeral_One zero_less_one_class.zero_le_one)
finally show ?thesis by simp
qed
also have "... < 1" (is "?lhs < _")
proof(cases "x ∈ A 0")
case True
then have "x ∉ A 1"
using A(4) by (auto simp: disjoint_family_on_def)
hence "?lhs = 1 / 4 + 1 / 2 * (1 / (1 + emeasure M (A 0)))"
by(simp add: True)
also have "... ≤ 1 / 4 + 1 / 2"
using less1(2)[of 0] by (simp add: divide_right_mono_ennreal ennreal_divide_times)
also have "... = 1 / 4 + 2 / 4"
using divide_mult_eq[of 2 1 2] by simp
also have "... = 3 / 4"
by(simp add: add_divide_distrib_ennreal[symmetric])
also have "... < 1"
by(simp add: divide_less_ennreal)
finally show ?thesis .
next
case False
then have "?lhs = 1 / 4 + (1 / 2)⇧2 * (1 / (1 + emeasure M (A 1))) * indicator (A 1) x"
by simp
also have "... ≤ 1 / 4 + (1 / 2)⇧2"
by (metis less1(2)[of 1] add_left_mono indicator_eq_0_iff indicator_eq_1_iff mult.right_neutral mult_eq_0_iff mult_left_mono zero_le)
also have "... = 2 / 4"
by(simp add: power_divide_distrib_ennreal add_divide_distrib_ennreal[symmetric])
also have "... < 1"
by(simp add: divide_less_ennreal)
finally show ?thesis .
qed
finally show "h x < 1" .
}
show "finite_measure (density M h)"
proof
show "emeasure (density M h) (space (density M h)) ≠ ∞"
proof -
have "integral⇧N M h ≠ ⊤" (is "?lhs ≠ _")
proof -
have "?lhs = (∑n. (∫⇧+ x∈A n. ((1/2)^(Suc n) * (1 / (1 + M (A n)))) ∂M))"
using A by(simp add: h_def nn_integral_suminf)
also have "... = (∑n. (1/2)^(Suc n) * (1 / (1 + M (A n))) * M (A n))"
by(rule suminf_cong,rule nn_integral_cmult_indicator) (use A in auto)
also have "... = (∑n. (1/2)^(Suc n) * ((1 / (1 + M (A n))) * M (A n)))"
by (simp add: mult.assoc)
also have "... ≤ (∑n. (1/2)^(Suc n))"
proof -
have "(1 / (1 + M (A n))) * M (A n) ≤ 1" for n
using A(3)[of n] by (simp add: add_pos_nonneg divide_le_posI_ennreal ennreal_divide_times)
thus ?thesis
by(intro suminf_le) (metis mult.right_neutral mult_left_mono zero_le,auto)
qed
also have "... = (∑n. ennreal ((1/2)^(Suc n)))"
by(simp only: ennreal_power[of "1/2",symmetric]) (metis divide_ennreal ennreal_1 ennreal_numeral linorder_not_le not_one_less_zero zero_less_numeral)
also have "... = ennreal (∑n. (1/2)^(Suc n))"
by(rule suminf_ennreal2) auto
also have "... = 1"
using nsum_of_r'[of "1/2" 1 1] by auto
finally show ?thesis
using nle_le by fastforce
qed
thus ?thesis
by(simp add: emeasure_density)
qed
qed
qed
lemma(in sigma_finite_measure) finite_density_measure:
obtains h where "h ∈ borel_measurable M"
"⋀x. x ∈ space M ⟹ 0 < h x"
"⋀x. x ∈ space M ⟹ h x < 1"
"finite_measure (density M h)"
by (metis (no_types, lifting) sigma_finite_disjoint ex_finite_density_measure)
subsection ‹ Lemma 14.D.13. ›
lemma (in measure_kernel)
assumes "disintegration ν μ"
defines "νx ≡ marginal_measure X Y ν"
shows disintegration_absolutely_continuous: "absolutely_continuous μ νx"
and disintegration_density: "νx = density μ (λx. κ x (space Y))"
and disintegration_absolutely_continuous_iff:
"absolutely_continuous νx μ ⟷ (AE x in μ. κ x (space Y) > 0)"
proof -
note sets_eq[measurable_cong] = disintegration_sets_eq[OF assms(1)]
note [measurable] = emeasure_measurable[OF sets.top]
have νx_eq: "νx A = (∫⇧+x∈A. (κ x (space Y)) ∂μ)" if A:"A ∈ sets X" for A
by(simp add: disintegrationD[OF assms(1) A sets.top] emeasure_marginal_measure[OF sets_eq(1) A] νx_def)
thus 1:"νx = density μ (λx. κ x (space Y))"
by(auto intro!: measure_eqI simp: sets_marginal_measure νx_def sets_eq emeasure_density)
hence sets_νx:"sets νx = sets X"
using sets_eq by simp
show "absolutely_continuous μ νx"
unfolding absolutely_continuous_def
proof safe
fix A
assume A: "A ∈ null_sets μ"
have "0 = (∫⇧+x∈A. (κ x (space Y)) ∂μ)"
by(simp add: A nn_integral_null_set)
also have "... = νx A"
using A νx_eq[of A,simplified sets_eq(2)[symmetric]]
by auto
finally show "A ∈ null_sets νx"
using A by(auto simp: null_sets_def νx_def sets_marginal_measure sets_eq)
qed
show "absolutely_continuous νx μ ⟷ (AE x in μ. κ x (space Y) > 0)"
proof
assume h:"absolutely_continuous νx μ"
define N where "N = {x ∈ space μ. (κ x) (space Y) = 0}"
have "N ∈ null_sets μ"
proof -
have "νx N = (∫⇧+x∈N. (κ x (space Y)) ∂μ)"
using νx_eq[of N] by(simp add: N_def sets_eq_imp_space_eq[OF sets_eq(2)])
also have "... = (∫⇧+x∈N. 0 ∂μ)"
by(rule nn_integral_cong) (auto simp: N_def indicator_def)
also have "... = 0" by simp
finally have "N ∈ null_sets νx"
by(auto simp: null_sets_def 1 N_def)
thus ?thesis
using h by(auto simp: absolutely_continuous_def)
qed
then show "AE x in μ. 0 < (κ x) (space Y)"
by(auto intro!: AE_I'[OF _ subset_refl] simp: N_def)
next
assume "AE x in μ. 0 < (κ x) (space Y)"
then show "absolutely_continuous νx μ"
using νx_eq by(auto simp: absolutely_continuous_def intro!: null_if_pos_func_has_zero_nn_int[where f="λx. emeasure (κ x) (space Y)"]) (auto simp: null_sets_def sets_νx)
qed
qed
subsection ‹ Theorem 14.D.14. ›
locale sigma_finite_measure_on_pair_standard = sigma_finite_measure_on_pair + standard_borel_ne Y
sublocale projection_sigma_finite_standard ⊆ sigma_finite_measure_on_pair_standard
by (simp add: sigma_finite_measure_on_pair_axioms sigma_finite_measure_on_pair_standard_def standard_borel_ne_axioms)
context sigma_finite_measure_on_pair_standard
begin
lemma measure_disintegration_extension:
"∃μ κ. finite_measure μ ∧ measure_kernel X Y κ ∧ measure_kernel.disintegration X Y κ ν μ ∧
(∀x∈space X. sigma_finite_measure (κ x)) ∧
(∀x∈space X. κ x (space Y) > 0) ∧
μ ~⇩M νx" (is "?goal")
proof(rule sigma_finite_measure.sigma_finite_disjoint[OF sigma_finite])
fix A :: "nat ⇒ _"
assume A:"range A ⊆ sets ν" "⋃ (range A) = space ν" "⋀i. emeasure ν (A i) ≠ ∞" "disjoint_family A"
define h where "h ≡ (λx. ∑n. (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))) * indicator (A n) x)"
have h: "h ∈ borel_measurable ν" "⋀x y. x ∈ space X ⟹ y ∈ space Y ⟹ 0 < h (x,y)" "⋀x y. x ∈ space X ⟹ y ∈ space Y ⟹ h (x,y) < 1" "finite_measure (density ν h)"
using ex_finite_density_measure[OF A] by(auto simp: sets_eq_imp_space_eq[OF nu_sets] h_def space_pair_measure)
interpret psfs_νx: finite_measure "marginal_measure X Y (density ν h)"
by(rule finite_measure_marginal_measure_finite[OF h(4),simplified,OF nu_sets])
interpret psfs: projection_sigma_finite_standard X Y "density ν h"
by(auto simp: projection_sigma_finite_standard_def projection_sigma_finite_def standard_borel_ne_axioms nu_sets finite_measure.sigma_finite_measure[OF finite_measure_marginal_measure_finite[OF h(4),simplified,OF nu_sets]])
from psfs.measure_disintegration
obtain κ' where κ': "prob_kernel X Y κ'" "measure_kernel.disintegration X Y κ' (density ν h) psfs.νx" by auto
interpret pk: prob_kernel X Y κ' by fact
define κ where "κ ≡ (λx. density (κ' x) (λy. 1 / h (x,y)))"
have κB: "κ x B = (∫⇧+y∈B. (1 / h (x, y))∂κ' x)" if "x ∈ space X" and [measurable]:"B ∈ sets Y" for x B
using nu_sets pk.kernel_sets[OF that(1)] that h(1) by(auto simp: κ_def emeasure_density)
interpret mk: measure_kernel X Y κ
proof
fix B
assume [measurable]:"B ∈ sets Y"
have 1:"(λx. ∫⇧+y∈B. (1 / h (x, y))∂κ' x) ∈ borel_measurable X"
using h(1) nu_sets by(auto intro!: pk.nn_integral_measurable_f'[of "λz. (1 / h z) * indicator B (snd z)",simplified])
show "(λx. (κ x) B) ∈ borel_measurable X"
by(rule measurable_cong[THEN iffD1,OF _ 1],simp add: κB)
qed(simp_all add: κ_def pk.kernel_sets space_ne)
have disi: "mk.disintegration ν psfs.νx"
proof(rule mk.disintegrationI)
fix A B
assume A[measurable]:"A ∈ sets X" and B[measurable]:"B ∈ sets Y"
show "ν (A × B) = (∫⇧+x∈A. (κ x) B∂psfs.νx)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+z∈A × B. 1 ∂ν)"
by auto
also have "... = (∫⇧+z∈A × B. (1 / h z * h z) ∂ν)"
proof -
have 1: "a * (1 / a) = 1" if "0 < a" "a < 1" for a :: ennreal
proof -
have "a * (1 / a) = ennreal (enn2real a * 1 / (enn2real a))"
by (simp add: divide_eq_1_ennreal enn2real_eq_0_iff ennreal_times_divide)
also have "... = ennreal 1"
using enn2real_eq_0_iff that by fastforce
finally show ?thesis
using ennreal_1 by simp
qed
show ?thesis
by(rule nn_integral_cong,auto simp add: sets_eq_imp_space_eq[OF nu_sets] space_pair_measure ennreal_divide_times indicator_def 1[OF h(2,3)])
qed
also have "... = (∫⇧+z. h z * ((1 / h z) * indicator (A × B) z) ∂ν)"
by(auto intro!: nn_integral_cong simp: indicator_def mult.commute)
also have "... = (∫⇧+z∈A × B. (1 / h z) ∂(density ν h))"
using h(1) by(simp add: nn_integral_density)
also have "... = (∫⇧+ x. ∫⇧+ y. (1 / h (x,y) * indicator (A × B) (x,y)) ∂κ' x ∂psfs.νx)"
using h(1) by(simp add: pk.nn_integral_fst_finite'[OF _ κ'(2) psfs_νx.finite_measure_axioms])
also have "... = (∫⇧+ x∈A. (∫⇧+ y∈B. (1 / h (x,y)) ∂κ' x) ∂psfs.νx)"
by(auto intro!: nn_integral_cong simp: indicator_def)
also have "... = ?rhs"
by(auto intro!: nn_integral_cong simp: κB[OF _ B] space_marginal_measure)
finally show ?thesis .
qed
qed(simp_all add: nu_sets sets_marginal_measure)
have geq0: "0 < (κ x) (space Y)" if "x ∈ space X" for x
proof -
have "0 = (∫⇧+ y. 0 ∂κ' x)" by simp
also have "... < (∫⇧+ y. (1 / h (x,y)) ∂κ' x)"
proof(rule nn_integral_less)
show "¬ (AE y in κ' x. 1 / h (x, y) ≤ 0)"
proof
assume "AE y in κ' x. 1 / h (x, y) ≤ 0"
moreover have "h (x,y) ≠ ⊤" if "y ∈ space (κ' x)" for y
using h(3)[OF ‹x ∈ space X› that[simplified sets_eq_imp_space_eq[OF pk.kernel_sets[OF ‹x ∈ space X›]]]] top.not_eq_extremum
by fastforce
ultimately show False
using prob_space.AE_False[OF pk.prob_spaces[OF that]] by simp
qed
qed(use h(1) pk.kernel_sets[OF that] that in auto)
also have "... = (κ x) (space Y)"
by(simp add: κB[OF that sets.top]) (simp add: sets_eq_imp_space_eq[OF pk.kernel_sets[OF that],symmetric])
finally show ?thesis .
qed
show ?goal
proof(safe intro!: exI[where x=psfs.νx] exI[where x=κ] disi)
show "absolutely_continuous νx psfs.νx"
unfolding mk.disintegration_absolutely_continuous_iff[OF disi]
by standard (simp add: space_marginal_measure geq0)
next
fix x
assume x:"x ∈ space X"
define C where "C ≡ range (λn. Pair x -` (A n) ∩ space Y)"
have 1:"countable C" "C ⊆ sets Y"
using A(1,2) x by (auto simp: nu_sets sets_eq_imp_space_eq[OF nu_sets] space_pair_measure C_def)
have 2: "⋃ C = space Y"
using A(1,2) by(auto simp: sets_eq_imp_space_eq[OF nu_sets] space_pair_measure C_def) (use x in auto)
show "sigma_finite_measure (κ x)"
unfolding sigma_finite_measure_def
proof(safe intro!: exI[where x=C])
fix c
assume "c ∈ C" "(κ x) c = ∞"
then obtain n where c:"c = Pair x -` (A n) ∩ space Y" by(auto simp: C_def)
have "(κ x) c = (∫⇧+y∈c. (1 / h (x, y))∂κ' x)"
using κB[OF x,of c] 1 ‹c ∈ C› by auto
also have "... = (∫⇧+y∈Pair x -` (A n). (1 / h (x, y))∂κ' x)"
by(auto intro!: nn_integral_cong simp: c indicator_def sets_eq_imp_space_eq[OF pk.kernel_sets[OF x]])
also have "... = (∫⇧+y∈Pair x -` (A n). (1 / ((1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))))) ∂κ' x)"
proof -
{
fix y
assume xy:"(x, y) ∈ A n"
have "1 / h (x, y) = 1 / ((1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))))"
proof -
have "h (x, y) = (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n)))" (is "?lhs = ?rhs")
proof -
have "?lhs = (∑m. (1 / 2) ^ Suc m * (1 / (1 + emeasure ν (A m))) * indicator (A m) (x,y))"
by(simp add: h_def)
also have "... = (∑m. if m = n then (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))) else 0)"
using xy A(4) by(fastforce intro!: suminf_cong simp: disjoint_family_on_def indicator_def)
also have "... = (∑j. if j + Suc n = n then (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))) else 0) + (∑j<Suc n. if j = n then (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))) else 0)"
by(auto simp: suminf_offset[of "λm. if m = n then (1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))) else 0" "Suc n"] simp del: power_Suc)
also have "... = ?rhs"
by simp
finally show ?thesis .
qed
thus ?thesis by simp
qed
}
thus ?thesis
by(intro nn_integral_cong) (auto simp: sets_eq_imp_space_eq[OF pk.kernel_sets[OF x]] indicator_def simp del: power_Suc)
qed
also have "... ≤ (∫⇧+y. (1 / ((1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n))))) ∂κ' x)"
by(rule nn_integral_mono) (auto simp: indicator_def)
also have "... = (1 / ((1 / 2) ^ Suc n * (1 / (1 + emeasure ν (A n)))))"
by(simp add: prob_space.emeasure_space_1[OF pk.prob_spaces[OF x]])
also have "... < ∞"
by (metis A(3) ennreal_add_eq_top ennreal_divide_eq_0_iff ennreal_divide_eq_top_iff ennreal_top_neq_one infinity_ennreal_def mult_eq_0_iff power_eq_0_iff top.not_eq_extremum top_neq_numeral)
finally show False
using ‹(κ x) c = ∞› by simp
qed(insert 1 2, auto simp: mk.kernel_sets[OF x] sets_eq_imp_space_eq[OF mk.kernel_sets[OF x]])
qed(auto simp: psfs_νx.finite_measure_axioms geq0 mk.measure_kernel_axioms mk.disintegration_absolutely_continuous[OF disi])
qed
end
lemma(in sigma_finite_measure_on_pair) measure_disintegration_extension_AE_unique:
assumes "sigma_finite_measure μ" "sigma_finite_measure μ'"
"measure_kernel X Y κ" "measure_kernel X Y κ'"
"measure_kernel.disintegration X Y κ ν μ" "measure_kernel.disintegration X Y κ' ν μ'"
and "absolutely_continuous μ μ'" "B ∈ sets Y"
shows "AE x in μ. κ' x B * RN_deriv μ μ' x = κ x B"
proof -
interpret s1: sigma_finite_measure μ by fact
interpret s2: sigma_finite_measure μ' by fact
interpret mk1: measure_kernel X Y κ by fact
interpret mk2: measure_kernel X Y κ' by fact
have sets[measurable_cong]:"sets μ = sets X" "sets μ' = sets X"
using assms(5,6) by(auto dest: mk1.disintegration_sets_eq mk2.disintegration_sets_eq)
have 1:"AE x in μ. κ x B = RN_deriv μ (marginal_measure_on X Y ν B) x"
using sets mk1.emeasure_measurable[OF assms(8)] mk1.disintegrationD[OF assms(5) _ assms(8)]
by(auto intro!: measure_eqI s1.RN_deriv_unique simp: emeasure_density emeasure_marginal_measure_on[OF nu_sets assms(8)] sets sets_marginal_measure)
have 2:"AE x in μ. κ' x B * RN_deriv μ μ' x = RN_deriv μ (marginal_measure_on X Y ν B) x"
proof -
{
fix A
assume A: "A ∈ sets X"
have "(∫⇧+x∈A. ((κ' x) B * RN_deriv μ μ' x) ∂μ) = (∫⇧+x. RN_deriv μ μ' x * (κ' x B * indicator A x)∂μ)"
by(auto intro!: nn_integral_cong simp: indicator_def mult.commute)
also have "... = (∫⇧+x∈A. κ' x B ∂μ')"
using mk2.emeasure_measurable[OF assms(8)] sets A
by(auto intro!: s1.RN_deriv_nn_integral[OF assms(7),symmetric])
also have "... = ν (A × B)"
by(simp add: mk2.disintegrationD[OF assms(6) A assms(8)])
finally have "(∫⇧+x∈A. ((κ' x) B * RN_deriv μ μ' x) ∂μ) = ν (A × B)" .
}
thus ?thesis
using sets mk2.emeasure_measurable[OF assms(8)]
by(auto intro!: measure_eqI s1.RN_deriv_unique simp: emeasure_density emeasure_marginal_measure_on[OF nu_sets assms(8)]sets sets_marginal_measure)
qed
show ?thesis
using 1 2 by auto
qed
end