Theory Kernels
section ‹ Kernels ›
theory Kernels
imports Lemmas_S_Finite_Measure_Monad
begin
subsection ‹S-Finite Measures›
locale s_finite_measure =
fixes M :: "'a measure"
assumes s_finite_sum: "∃Mi :: nat ⇒ 'a measure. (∀i. sets (Mi i) = sets M) ∧ (∀i. finite_measure (Mi i)) ∧ (∀A∈sets M. M A = (∑i. Mi i A))"
lemma(in sigma_finite_measure) s_finite_measure: "s_finite_measure M"
proof
obtain A :: "nat ⇒ _" where A: "range A ⊆ sets M" "⋃ (range A) = space M" "⋀i. emeasure M (A i) ≠ ∞" "disjoint_family A"
by(metis sigma_finite_disjoint)
define Mi where "Mi ≡ (λi. measure_of (space M) (sets M) (λa. M (a ∩ A i)))"
have emeasure_Mi:"Mi i a = M (a ∩ A i)" if "a ∈ sets M" for i a
proof -
have "positive (sets (Mi i)) (λa. M (a ∩ A i))" "countably_additive (sets (Mi i)) (λa. M (a ∩ A i))"
unfolding positive_def countably_additive_def
proof safe
fix B :: "nat ⇒ _"
assume "range B ⊆ sets (Mi i)" "disjoint_family B"
with A(1) have "range (λj. B j ∩ A i) ⊆ sets M" "disjoint_family (λj. B j ∩ A i)"
by(fastforce simp: Mi_def disjoint_family_on_def)+
thus "(∑j. M (B j ∩ A i)) = M (⋃ (range B) ∩ A i)"
by (metis UN_extend_simps(4) suminf_emeasure)
qed simp
from emeasure_measure_of[OF _ _ this] that show ?thesis
by(auto simp add: Mi_def sets.space_closed)
qed
have sets_Mi:"sets (Mi i) = sets M" for i by(simp add: Mi_def)
show "∃Mi. (∀i. sets (Mi i) = sets M) ∧ (∀i. finite_measure (Mi i)) ∧ (∀A∈sets M. emeasure M A = (∑i. emeasure (Mi i) A))"
proof(safe intro!: exI[where x=Mi])
fix i
show "finite_measure (Mi i)"
using A by(auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF sets_Mi] emeasure_Mi)
next
fix B
assume B:"B ∈ sets M"
with A(1,4) have "range (λi. B ∩ A i) ⊆ sets M" "disjoint_family (λi. B ∩ A i)"
by(auto simp: disjoint_family_on_def)
then show "M B = (∑i. (Mi i) B)"
by(simp add: emeasure_Mi[OF B] suminf_emeasure A(2) B)
qed(simp_all add: sets_Mi)
qed
lemmas(in finite_measure) s_finite_measure_finite_measure = s_finite_measure
lemmas(in subprob_space) s_finite_measure_subprob = s_finite_measure
lemmas(in prob_space) s_finite_measure_prob = s_finite_measure
sublocale sigma_finite_measure ⊆ s_finite_measure
by(rule s_finite_measure)
lemma s_finite_measureI:
assumes "⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. A∈sets M ⟹ M A = (∑i. Mi i A)"
shows "s_finite_measure M"
by standard (use assms in blast)
lemma s_finite_measure_prodI:
assumes "⋀i j. sets (Mij i j) = sets M" "⋀i j. Mij i j (space M) < ∞" "⋀A. A ∈ sets M ⟹ M A = (∑i. (∑j. Mij i j A))"
shows "s_finite_measure M"
proof -
define Mi' where "Mi' ≡ (λn. case_prod Mij (prod_decode n))"
have sets_Mi'[measurable_cong]:"⋀i. sets (Mi' i) = sets M"
using assms(1) by(simp add: Mi'_def split_beta')
have Mi'_finite:"⋀i. finite_measure (Mi' i)"
using assms(2) sets_eq_imp_space_eq[OF sets_Mi'[symmetric]] top.not_eq_extremum
by(fastforce intro!: finite_measureI simp: Mi'_def split_beta')
show ?thesis
proof(safe intro!: s_finite_measureI[where Mi=Mi'] sets_Mi' Mi'_finite)
fix A
show "A ∈ sets M ⟹ M A = (∑i. Mi' i A)"
by(simp add: assms(3) suminf_ennreal_2dimen[where f="λ(x,y). Mij x y A", simplified,OF refl,symmetric] Mi'_def split_beta')
qed
qed
corollary s_finite_measure_s_finite_sumI:
assumes "⋀i. sets (Mi i) = sets M" "⋀i. s_finite_measure (Mi i)" "⋀A. A ∈ sets M ⟹ M A = (∑i. Mi i A)"
shows "s_finite_measure M"
proof -
from s_finite_measure.s_finite_sum[OF assms(2)]
obtain Mij where Mij[measurable]: "⋀i j. sets (Mij i j) = sets M" "⋀i j. finite_measure (Mij i j)" "⋀i j A. A ∈ sets M ⟹ Mi i A = (∑j. Mij i j A)"
by (metis assms(1))
show ?thesis
using finite_measure.emeasure_finite[OF Mij(2)]
by(auto intro!: s_finite_measure_prodI[where Mij = Mij] simp: assms(3) Mij top.not_eq_extremum)
qed
lemma s_finite_measure_finite_sumI:
assumes "finite I" "⋀i. i ∈ I ⟹ s_finite_measure (Mi i)" "⋀i. i ∈ I ⟹ sets (Mi i) = sets M"
and "⋀A. A ∈ sets M ⟹ M A = (∑i∈I. Mi i A)"
shows "s_finite_measure M"
proof -
let ?Mi = "λn. if n < card I then Mi (from_nat_into I n) else null_measure M"
show ?thesis
proof(rule s_finite_measure_s_finite_sumI[of ?Mi])
show "⋀i. s_finite_measure (?Mi i)"
by (metis (full_types) assms(2) bot_nat_0.extremum_strict card.empty emeasure_null_measure ennreal_top_neq_zero finite_measure.s_finite_measure_finite_measure finite_measureI from_nat_into infinity_ennreal_def)
next
show "⋀i. sets (?Mi i) = sets M"
by (metis (full_types) assms(3) card_gt_0_iff dual_order.strict_trans2 from_nat_into less_zeroE linorder_le_less_linear sets_null_measure)
next
fix A
assume "A ∈ sets M"
then have "M A = (∑i∈I. Mi i A)"
by fact
also have "... = (∑n<card I. Mi (from_nat_into I n) A)"
by(rule sum.card_from_nat_into[symmetric])
also have "... = (∑n<card I. ?Mi n A)"
by simp
also have "... = (∑n. ?Mi n A)"
by(rule suminf_finite[symmetric]) auto
finally show "M A = (∑n. ?Mi n A)" .
qed
qed
lemma countable_space_s_finite_measure:
assumes "countable (space M)" "sets M = Pow (space M)"
shows "s_finite_measure M"
proof -
define Mi where "Mi ≡ (λi. measure_of (space M) (sets M) (λA. emeasure M (A ∩ {from_nat_into (space M) i})))"
have sets_Mi[measurable_cong,simp]: "sets (Mi i) = sets M" for i
by(auto simp: Mi_def)
have emeasure_Mi: "emeasure (Mi i) A = emeasure M (A ∩ {from_nat_into (space M) i})" if [measurable]: "A ∈ sets M" and i:"i ∈ to_nat_on (space M) ` (space M)" for i A
proof -
have "from_nat_into (space M) i ∈ space M"
by (simp add: from_nat_into_def i inv_into_into)
hence [measurable]: "{from_nat_into (space M) i} ∈ sets M"
using assms(2) by auto
have 1:"countably_additive (sets M) (λA. emeasure M (A ∩ {from_nat_into (space M) i}))"
unfolding countably_additive_def
proof safe
fix B :: "nat ⇒ _"
assume "range B ⊆ sets M" "disjoint_family B"
then have [measurable]:"⋀i. B i ∈ sets M" and "disjoint_family (λj. B j ∩ {from_nat_into (space M) i})"
by(auto simp: disjoint_family_on_def)
then have "(∑j. emeasure M (B j ∩ {from_nat_into (space M) i})) = emeasure M (⋃ (range (λj. B j ∩ {from_nat_into (space M) i})))"
by(intro suminf_emeasure) auto
thus "(∑j. emeasure M (B j ∩ {from_nat_into (space M) i})) = emeasure M (⋃ (range B) ∩ {from_nat_into (space M) i})"
by simp
qed
have 2:"positive (sets M) (λA. emeasure M (A ∩ {from_nat_into (space M) i}))"
by(auto simp: positive_def)
show ?thesis
by(simp add: Mi_def emeasure_measure_of_sigma[OF sets.sigma_algebra_axioms 2 1])
qed
define Mi' where "Mi' ≡ (λi. if i ∈ to_nat_on (space M) ` (space M) then Mi i else null_measure M)"
have [measurable_cong, simp]: "sets (Mi' i) = sets M" for i
by(auto simp: Mi'_def)
show ?thesis
proof(rule s_finite_measure_s_finite_sumI[where Mi=Mi'])
fix A
assume A[measurable]: "A ∈ sets M"
show "emeasure M A = (∑i. emeasure (Mi' i) A)" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. emeasure M {x} ∂count_space A)"
using sets.sets_into_space[OF A] by(auto intro!: emeasure_countable_singleton simp: assms(2) countable_subset[OF _ assms(1)])
also have "... = (∫⇧+ x. emeasure (Mi (to_nat_on (space M) x)) A ∂count_space A)"
proof(safe intro!: nn_integral_cong)
fix x
assume "x ∈ space (count_space A)"
then have 1:"x ∈ A" by simp
hence 2:"to_nat_on (space M) x ∈ to_nat_on (space M) ` (space M)"
using A assms(2) by auto
have [simp]: "from_nat_into (space M) (to_nat_on (space M) x) = x"
by (metis 1 2 A assms(1) eq_from_nat_into_iff in_mono sets.sets_into_space)
show "emeasure M {x} = emeasure (Mi (to_nat_on (space M) x)) A"
using 1 by(simp add: emeasure_Mi[OF A 2])
qed
also have "... = (∫⇧+ x∈A. emeasure (Mi (to_nat_on (space M) x)) A ∂count_space UNIV)"
by (simp add: nn_integral_count_space_indicator)
also have "... = (∫⇧+ i∈to_nat_on (space M) ` A. emeasure (Mi i) A ∂count_space UNIV)"
by(rule nn_integral_count_compose_inj[OF inj_on_subset[OF inj_on_to_nat_on[OF assms(1)] sets.sets_into_space[OF A]]])
also have "... = (∫⇧+ i∈to_nat_on (space M) ` A. emeasure (Mi' i) A ∂count_space UNIV)"
proof -
{
fix x
assume "x ∈ A"
then have "to_nat_on (space M) x ∈ to_nat_on (space M) ` (space M)"
using sets.sets_into_space[OF A] by auto
hence "emeasure (Mi (to_nat_on (space M) x)) A = emeasure (Mi' (to_nat_on (space M) x)) A"
by(auto simp: Mi'_def)
}
thus ?thesis
by(auto intro!: nn_integral_cong simp: indicator_def)
qed
also have "... = (∫⇧+ i. emeasure (Mi' i) A ∂count_space UNIV)"
proof -
{
fix i
assume i:"i ∉ to_nat_on (space M) ` A"
have "from_nat_into (space M) i ∉ A" if "i ∈ to_nat_on (space M) ` (space M)"
by (metis i image_eqI that to_nat_on_from_nat_into)
with emeasure_Mi have "emeasure (Mi' i) A = 0"
by(auto simp: Mi'_def)
}
thus ?thesis
by(auto intro!: nn_integral_cong simp: indicator_def)
qed
also have "... = ?rhs"
by(rule nn_integral_count_space_nat)
finally show ?thesis .
qed
next
fix i
show "s_finite_measure (Mi' i)"
proof -
{
fix x
assume h:"x ∈ space M" "i = to_nat_on (space M) x"
then have i:"i ∈ to_nat_on (space M) ` space M"
by blast
have x: "from_nat_into (space M) i = x"
using h by (simp add: assms(1))
consider "M {x} = 0" | "M {x} ≠ 0" "M {x} < ∞" | "M {x} = ∞"
using top.not_eq_extremum by fastforce
hence "s_finite_measure (Mi (to_nat_on (space M) x))"
proof cases
case 1
then have [simp]:"Mi i = null_measure M"
by(auto intro!: measure_eqI simp: emeasure_Mi[OF _ i] x Int_insert_right)
show ?thesis
by(auto simp: h(2)[symmetric] intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
next
case 2
then show ?thesis
unfolding h(2)[symmetric]
by(auto intro!: finite_measure.s_finite_measure_finite_measure finite_measureI simp: sets_eq_imp_space_eq[OF sets_Mi] emeasure_Mi[OF _ i] x h(1))
next
case 3
show ?thesis
unfolding h(2)[symmetric] s_finite_measure_def
proof(safe intro!: exI[where x="λj. return M x"] prob_space.finite_measure prob_space_return h(1))
fix A
assume "A ∈ sets (Mi i)"
then have [measurable]: "A ∈ sets M"
by(simp add: Mi_def)
thus "emeasure (Mi i) A = (∑i. emeasure (return M x) A)"
by(simp add: emeasure_Mi[OF _ i] x) (cases "x ∈ A",auto simp: 3 nn_integral_count_space_nat[symmetric])
qed(auto simp: Mi_def)
qed
}
thus ?thesis
by(auto simp: Mi'_def) (auto intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
qed
qed simp
qed
lemma s_finite_measure_subprob_space:
"s_finite_measure M ⟷ (∃Mi :: nat ⇒ 'a measure. (∀i. sets (Mi i) = sets M) ∧ (∀i. (Mi i) (space M) ≤ 1) ∧ (∀A∈sets M. M A = (∑i. Mi i A)))"
proof
assume "∃Mi. (∀i. sets (Mi i) = sets M) ∧ (∀i. emeasure (Mi i) (space M) ≤ 1) ∧ (∀A∈sets M. M A = (∑i. (Mi i) A))"
then obtain Mi where 1:"⋀i. sets (Mi i) = sets M" "⋀i. emeasure (Mi i) (space M) ≤ 1" "(∀A∈sets M. M A = (∑i. (Mi i) A))"
by auto
thus "s_finite_measure M"
by(auto simp: s_finite_measure_def sets_eq_imp_space_eq[OF 1(1)] intro!: finite_measureI exI[where x=Mi]) (metis ennreal_one_less_top linorder_not_le)
next
assume "s_finite_measure M"
then obtain Mi' where Mi': "⋀i. sets (Mi' i) = sets M" "⋀i. finite_measure (Mi' i)" "⋀A. A∈sets M ⟹ M A = (∑i. Mi' i A)"
by (metis s_finite_measure.s_finite_sum)
obtain u where u:"⋀i. u i < ∞" "⋀i. Mi' i (space M) = u i"
using Mi'(2) finite_measure.emeasure_finite top.not_eq_extremum by fastforce
define Mmn where "Mmn ≡ (λ(m,n). if n < nat ⌈enn2real (u m)⌉ then scale_measure (1 / ennreal (real_of_int ⌈enn2real (u m)⌉)) (Mi' m) else (sigma (space M) (sets M)))"
have sets_Mmn : "sets (Mmn k) = sets M" for k by(simp add: Mmn_def split_beta Mi')
have emeasure_Mmn: "(Mmn (m, n)) A = (Mi' m A) / ennreal (real_of_int ⌈enn2real (u m)⌉)" if "n < nat ⌈enn2real (u m)⌉" "A ∈ sets M" for n m A
by(auto simp: Mmn_def that ennreal_divide_times)
have emeasure_Mmn_less1: "(Mmn (m, n)) A ≤ 1" for m n A
proof (cases "n < nat ⌈enn2real (u m)⌉ ∧ A ∈ sets M")
case h:True
have "(Mi' m) A ≤ ennreal (real_of_int ⌈enn2real (u m)⌉)"
by(rule order.trans[OF emeasure_mono[OF sets.sets_into_space sets.top]]) (insert u(1) h, auto simp: u(2)[symmetric] enn2real_le top.not_eq_extremum sets_eq_imp_space_eq[OF Mi'(1)] Mi'(1))
with h show ?thesis
by(simp add: emeasure_Mmn) (metis divide_le_posI_ennreal dual_order.eq_iff ennreal_zero_divide mult.right_neutral not_gr_zero zero_le)
qed(auto simp: Mmn_def emeasure_sigma emeasure_notin_sets Mi')
have Mi'_sum:"Mi' m A = (∑n. Mmn (m, n) A)" if "A ∈ sets M" for m A
proof -
have "(∑n. Mmn (m, n) A) = (∑n. Mmn (m, n + nat ⌈enn2real (u m)⌉) A) + (∑n< nat ⌈enn2real (u m)⌉. Mmn (m, n) A)"
by(simp add: suminf_offset[where f="λn. Mmn (m, n) A"])
also have "... = (∑n< nat ⌈enn2real (u m)⌉. Mmn (m, n) A)"
by(simp add: emeasure_sigma Mmn_def)
also have "... = (∑n< nat ⌈enn2real (u m)⌉. (Mi' m A) / ennreal (real_of_int ⌈enn2real (u m)⌉))"
by(rule Finite_Cartesian_Product.sum_cong_aux) (auto simp: emeasure_Mmn that)
also have "... = Mi' m A"
proof (cases "nat ⌈enn2real (u m)⌉")
case 0
with u[of m] show ?thesis
by simp (metis Mi'(1) emeasure_mono enn2real_positive_iff less_le_not_le linorder_less_linear not_less_zero sets.sets_into_space sets.top that)
next
case (Suc n')
then have "ennreal (real_of_int ⌈enn2real (u m)⌉) > 0"
using ennreal_less_zero_iff by fastforce
with u(1)[of m] have "of_nat (nat ⌈enn2real (u m)⌉) / ennreal (real_of_int ⌈enn2real (u m)⌉) = 1"
by (simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
thus ?thesis
by (simp add: ennreal_divide_times[symmetric])
qed
finally show ?thesis ..
qed
define Mi where "Mi ≡ (λi. Mmn (prod_decode i))"
show "∃Mi. (∀i. sets (Mi i) = sets M) ∧ (∀i. emeasure (Mi i) (space M) ≤ 1) ∧ (∀A∈sets M. M A = (∑i. (Mi i) A))"
by(auto intro!: exI[where x=Mi] simp: Mi_def sets_Mmn suminf_ennreal_2dimen[OF Mi'_sum] Mi'(3)) (metis emeasure_Mmn_less1 prod_decode_aux.cases)
qed
lemma(in s_finite_measure) finite_measures:
obtains Mi where "⋀i. sets (Mi i) = sets M" "⋀i. (Mi i) (space M) ≤ 1" "⋀A. M A = (∑i. Mi i A)"
proof -
obtain Mi where Mi:"⋀i. sets (Mi i) = sets M" "⋀i. (Mi i) (space M) ≤ 1" "⋀A. A ∈ sets M ⟹ M A = (∑i. Mi i A)"
using s_finite_measure_axioms by(metis s_finite_measure_subprob_space)
hence "M A = (∑i. Mi i A)" for A
by(cases "A ∈ sets M") (auto simp: emeasure_notin_sets)
with Mi(1,2) show ?thesis
using that by blast
qed
lemma(in s_finite_measure) finite_measures_ne:
assumes "space M ≠ {}"
obtains Mi where "⋀i. sets (Mi i) = sets M" "⋀i. subprob_space (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by (metis assms finite_measures sets_eq_imp_space_eq subprob_spaceI)
lemma(in s_finite_measure) finite_measures':
obtains Mi where "⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by (metis ennreal_top_neq_one finite_measureI finite_measures infinity_ennreal_def sets_eq_imp_space_eq top.extremum_uniqueI)
lemma(in s_finite_measure) s_finite_measure_distr:
assumes f[measurable]:"f ∈ M →⇩M N"
shows "s_finite_measure (distr M N f)"
proof -
obtain Mi where Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by(metis finite_measures')
show ?thesis
by(auto intro!: s_finite_measureI[where Mi="(λi. distr (Mi i) N f)"] finite_measure.finite_measure_distr[OF Mi(2)] simp: emeasure_distr Mi(3) sets_eq_imp_space_eq[OF Mi(1)])
qed
lemma nn_integral_measure_suminf:
assumes [measurable_cong]:"⋀i. sets (Mi i) = sets M" and "⋀A. A∈sets M ⟹ M A = (∑i. Mi i A)" "f ∈ borel_measurable M"
shows "(∑i. ∫⇧+x. f x ∂(Mi i)) = (∫⇧+x. f x ∂M)"
using assms(3)
proof induction
case (cong f g)
then show ?case
by (metis (no_types, lifting) assms(1) nn_integral_cong sets_eq_imp_space_eq suminf_cong)
next
case (set A)
then show ?case
using assms(1,2) by simp
next
case (mult u c)
then show ?case
by(simp add: nn_integral_cmult)
next
case (add u v)
then show ?case
by(simp add: nn_integral_add suminf_add[symmetric])
next
case ih:(seq U)
have "(∑i. integral⇧N (Mi i) (⨆ range U)) = (∑i. ∫⇧+ x. (⨆j. U j x) ∂(Mi i))"
by(auto intro!: suminf_cong) (metis SUP_apply)
also have "... = (∑i. ⨆j. ∫⇧+ x. U j x ∂(Mi i))"
using ih by(auto intro!: suminf_cong nn_integral_monotone_convergence_SUP)
also have "... = (⨆j. (∑i. ∫⇧+ x. U j x ∂(Mi i)))"
using ih(3) by(auto intro!: ennreal_suminf_SUP_eq incseq_nn_integral)
also have "... = (⨆j. integral⇧N M (U j))"
by(simp add: ih)
also have "... = (∫⇧+ x. (⨆j. U j x) ∂M)"
using ih by(auto intro!: nn_integral_monotone_convergence_SUP[symmetric])
also have "... = integral⇧N M (⨆ range U)"
by(metis SUP_apply)
finally show ?case .
qed
text ‹ A @{term ‹density M f›} of $s$-finite measure @{term M} and @{term ‹f ∈ borel_measurable M›} is again s-finite.
We do not require additional assumption, unlike $\sigma$-finite measures.›
lemma(in s_finite_measure) s_finite_measure_density:
assumes f[measurable]:"f ∈ borel_measurable M"
shows "s_finite_measure (density M f)"
proof -
obtain Mi where Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by(metis finite_measures')
show ?thesis
proof(rule s_finite_measure_s_finite_sumI[where Mi="λi. density (Mi i) f"])
show "s_finite_measure (density (Mi i) f)" for i
proof -
define Mij where "Mij = (λj::nat. if j = 0 then density (Mi i) (λx. ∞ * indicator {x∈space M. f x = ∞} x)
else if j = 1 then density (Mi i) (λx. f x * indicator {x∈space M. f x < ∞} x)
else null_measure M)"
have sets_Mij[measurable_cong]: "sets (Mij j) = sets M" for j
by(auto simp: Mij_def Mi)
have emeasure_Mi:"density (Mi i) f A = (∑j. Mij j A)" (is "?lhs = ?rhs") if A[measurable]: "A ∈ sets M" for A
proof -
have "?lhs = (∫⇧+x ∈ A. f x ∂Mi i)"
by(simp add: emeasure_density)
also have "... = (∫⇧+x. ∞ * indicator {x∈space M. f x = ∞} x * indicator A x + f x * indicator {x∈space M. f x < ∞} x * indicator A x ∂Mi i)"
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF Mi(1)] indicator_def) (simp add: top.not_eq_extremum)
also have "... = density (Mi i) (λx. ∞ * indicator {x∈space M. f x = ∞} x) A + density (Mi i) (λx. f x * indicator {x∈space M. f x < ∞} x) A"
by(simp add: nn_integral_add emeasure_density)
also have "... = ?rhs"
using suminf_finite[of "{..<Suc (Suc 0)}" "λj. Mij j A"] by(auto simp: Mij_def)
finally show ?thesis .
qed
show ?thesis
proof(rule s_finite_measure_s_finite_sumI[OF _ _ emeasure_Mi])
fix j :: nat
consider "j = 0" | "j = 1" | "j ≠ 0" "j ≠ 1" by auto
then show "s_finite_measure (Mij j)"
proof cases
case 1
have 2:"Mij j A = (∑k. density (Mi i) (indicator {x∈space M. f x = ⊤}) A)" if A[measurable]:"A ∈ sets M" for A
by(auto simp: Mij_def 1 emeasure_density nn_integral_suminf[symmetric] sets_eq_imp_space_eq[OF Mi(1)] indicator_def intro!: nn_integral_cong) (simp add: nn_integral_count_space_nat[symmetric])
show ?thesis
by(auto simp: s_finite_measure_def 2 Mi(1)[of i] sets_Mij[of j] intro!: exI[where x="λk. density (Mi i) (indicator {x∈space M. f x = ∞})"] finite_measure.finite_measure_restricted Mi(2))
next
case 2
show ?thesis
by(auto intro!: sigma_finite_measure.s_finite_measure AE_mono_measure[OF Mi(1)] sum_le_suminf[where I="{i}" and f="λi. Mi i _",simplified] simp: sigma_finite_measure.sigma_finite_iff_density_finite[OF finite_measure.sigma_finite_measure[OF Mi(2)[of i]]] le_measure[OF Mi(1)] Mi indicator_def 2 Mij_def) auto
next
case 3
then show ?thesis
by(auto simp: Mij_def intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
qed
qed(auto simp: sets_Mij Mi)
qed
qed(auto simp: emeasure_density nn_integral_measure_suminf[OF Mi(1,3)] Mi(1))
qed
lemma
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable_cong]:"⋀i. sets (Mi i) = sets M" and "⋀A. A∈sets M ⟹ M A = (∑i. Mi i A)" "integrable M f"
shows lebesgue_integral_measure_suminf:"(∑i. ∫x. f x ∂(Mi i)) = (∫x. f x ∂M)" (is "?suminf")
and lebesgue_integral_measure_suminf_summable_norm: "summable (λi. norm (∫x. f x ∂(Mi i)))" (is "?summable2")
and lebesgue_integral_measure_suminf_summable_norm_in: "summable (λi. ∫x. norm (f x) ∂(Mi i))" (is "?summable")
proof -
have Mi:"Mi i ≤ M" for i
using assms(2) ennreal_suminf_lessD linorder_not_le by(fastforce simp: assms(1) le_measure[OF assms(1)])
have sum2: "summable (λi. norm (∫x. g x ∂(Mi i)))" if "summable (λi. ∫x. norm (g x) ∂(Mi i))" for g :: "'a ⇒ 'b"
proof(rule summable_suminf_not_top)
have "(∑i. ennreal (norm (∫x. g x ∂(Mi i)))) ≤ (∑i. ennreal (∫x. norm (g x) ∂(Mi i)))"
by(auto intro!: suminf_le)
thus "(∑i. ennreal (norm (∫x. g x ∂(Mi i)))) ≠ ⊤"
by (metis ennreal_suminf_neq_top[OF that] Bochner_Integration.integral_nonneg neq_top_trans norm_ge_zero)
qed simp
have "?suminf ∧ ?summable"
using assms(3)
proof induction
case h[measurable]:(base A c)
have Mi_fin:"Mi i A < ∞" for i
by(rule order.strict_trans1[OF _ h(2)], auto simp: le_measureD3[OF Mi assms(1)])
have 1: "(∫x. (indicat_real A x *⇩R c) ∂Mi i) = measure (Mi i) A *⇩R c" for i
using Mi_fin by simp
have 2:"summable (λi. ∫x. norm (indicat_real A x *⇩R c) ∂Mi i)"
proof(rule summable_suminf_not_top)
show "(∑i. ennreal (∫x. norm (indicat_real A x *⇩R c) ∂Mi i)) ≠ ⊤" (is "?l ≠ _")
proof -
have "?l = (∑i. Mi i A ) * norm c"
using Mi_fin by(auto intro!: suminf_cong simp: measure_def enn2real_mult ennreal_mult)
also have "... = M A * norm c"
by(simp add: assms(2))
also have "... ≠ ⊤"
using h(2) by (simp add: ennreal_mult_less_top top.not_eq_extremum)
finally show ?thesis .
qed
qed simp
have 3: "(∑i. ∫x. indicat_real A x *⇩R c ∂Mi i) = (∫x. indicat_real A x *⇩R c ∂M)" (is "?l = ?r")
proof -
have [simp]: "summable (λi. enn2real (Mi i A))"
using Mi_fin h by(auto intro!: summable_suminf_not_top simp: assms(2)[symmetric])
have "?l = (∑i. measure (Mi i) A) *⇩R c"
by(auto intro!: suminf_cong simp: 1 measure_def suminf_scaleR_left)
also have "... = ?r"
using h(2) Mi_fin by(simp add: ennreal_inj[where a="(∑i. measure (Mi i) A)" and b="measure M A",OF suminf_nonneg measure_nonneg,symmetric,simplified measure_def] measure_def suminf_ennreal2[symmetric] assms(2)[symmetric])
finally show ?thesis .
qed
from 2 3 show ?case by simp
next
case ih[measurable]:(add f g)
have 1:"summable (λi. ∫x. norm (f x + g x) ∂Mi i)"
proof(rule summable_suminf_not_top)
show "(∑i. ennreal (∫x. norm (f x + g x) ∂Mi i)) ≠ ⊤" (is "?l ≠ _")
proof -
have "?l = (∑i. (∫⇧+x. ennreal (norm (f x + g x)) ∂Mi i))"
using ih by(auto intro!: suminf_cong nn_integral_eq_integral[symmetric] integrable_mono_measure[OF assms(1) Mi])
also have "... ≤ (∑i. (∫⇧+x. ennreal (norm (f x) + norm (g x)) ∂Mi i))"
by(auto intro!: suminf_le nn_integral_mono norm_triangle_ineq simp del: ennreal_plus)
also have "... = (∑i. (∫⇧+x. ennreal (norm (f x)) ∂Mi i)) + (∑i. (∫⇧+x. ennreal (norm (g x)) ∂Mi i))"
by(auto intro!: suminf_cong simp: nn_integral_add suminf_add)
also have "... = (∑i. ennreal (∫x. norm (f x) ∂Mi i)) + (∑i. ennreal (∫x. norm (g x) ∂Mi i))"
using ih by(simp add: nn_integral_eq_integral integrable_mono_measure[OF assms(1) Mi])
also have "... < ⊤"
using ennreal_suminf_neq_top[OF conjunct2[OF ih(3)]] ennreal_suminf_neq_top[OF conjunct2[OF ih(4)]]
by (meson Bochner_Integration.integral_nonneg ennreal_add_eq_top norm_ge_zero top.not_eq_extremum)
finally show ?thesis
using order.strict_iff_order by blast
qed
qed simp
with ih show ?case
by(auto simp: Bochner_Integration.integral_add[OF integrable_mono_measure[OF assms(1) Mi ih(1)] integrable_mono_measure[OF assms(1) Mi ih(2)]] suminf_add[symmetric,OF summable_norm_cancel[OF sum2[OF conjunct2[OF ih(3)]]] summable_norm_cancel[OF sum2[OF conjunct2[OF ih(4)]]]])
next
case ih[measurable]:(lim f fn)
have 1:"summable (λi. ∫x. norm (f x) ∂(Mi i))"
proof(rule summable_suminf_not_top)
show "(∑i. ennreal (∫x. norm (f x) ∂(Mi i))) ≠ ⊤" (is "?lhs ≠ _")
proof -
have "?lhs = (∑i. ∫⇧+ x. ennreal (norm (f x)) ∂Mi i)"
by(auto intro!: suminf_cong nn_integral_eq_integral[symmetric] integrable_mono_measure[OF assms(1) Mi] simp: ih)
also have "... = (∫⇧+ x. ennreal (norm (f x)) ∂M)"
by(simp add: nn_integral_measure_suminf[OF assms(1,2)])
also have "... = ennreal (∫ x. norm (f x) ∂M)"
by(auto intro!: nn_integral_eq_integral ih(4))
also have "... < ⊤" by simp
finally show "?lhs ≠ ⊤"
using linorder_neq_iff by blast
qed
qed simp
have "(∑i. ∫x. f x ∂(Mi i)) = (∫i. ∫x. f x ∂(Mi i) ∂(count_space UNIV))"
by(rule integral_count_space_nat[symmetric]) (simp add: integrable_count_space_nat_iff sum2[OF 1])
also have "... = lim (λm. ∫i. ∫x. fn m x ∂(Mi i) ∂(count_space UNIV))"
proof(rule limI[OF integral_dominated_convergence[where w="λi. 2 * (∫x. norm (f x) ∂(Mi i))"],symmetric],auto simp: AE_count_space integrable_count_space_nat_iff 1)
show "(λm. ∫x. fn m x ∂(Mi i)) ⇢ ∫x. f x ∂(Mi i)" for i
by(rule integral_dominated_convergence[where w="λx. 2 * norm (f x)"],insert ih) (auto intro!: integrable_mono_measure[OF assms(1) Mi] simp: sets_eq_imp_space_eq[OF assms(1)])
next
fix i j
show "norm (∫x. fn j x ∂(Mi i)) ≤ 2 * (∫x. norm (f x) ∂(Mi i))" (is "?l ≤ ?r")
proof -
have "?l ≤ (∫x. norm (fn j x) ∂(Mi i))"
by simp
also have "... ≤ (∫x. 2 * norm (f x) ∂(Mi i))"
by(rule integral_mono,insert ih) (auto intro!: integrable_mono_measure[OF assms(1) Mi] simp: sets_eq_imp_space_eq[OF assms(1)])
finally show "?l ≤ ?r" by simp
qed
qed
also have "... = lim (λm. (∑i. ∫x. fn m x ∂(Mi i)))"
proof -
have "(∫i. ∫x. fn m x ∂(Mi i) ∂(count_space UNIV)) = (∑i. ∫x. fn m x ∂(Mi i))" for m
by(auto intro!: integral_count_space_nat sum2 simp: integrable_count_space_nat_iff) (use ih(5) in auto)
thus ?thesis by simp
qed
also have "... = lim (λm. ∫x. fn m x ∂M)"
by(simp add: ih(5))
also have "... = (∫x. f x ∂M)"
using ih by(auto intro!: limI[OF integral_dominated_convergence[where w="λx. 2 * norm (f x)"]])
finally show ?case
using 1 by auto
qed
thus ?suminf ?summable ?summable2
by(simp_all add: sum2)
qed
lemma (in s_finite_measure) measurable_emeasure_Pair':
assumes "Q ∈ sets (N ⨂⇩M M)"
shows "(λx. emeasure M (Pair x -` Q)) ∈ borel_measurable N" (is "?s Q ∈ _")
proof -
obtain Mi where Mi:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by(metis finite_measures')
show ?thesis
using Mi(1,2) assms finite_measure.finite_measure_cut_measurable[of "Mi _" Q N]
by(simp add: Mi(3))
qed
lemma (in s_finite_measure) measurable_emeasure'[measurable (raw)]:
assumes space: "⋀x. x ∈ space N ⟹ A x ⊆ space M"
assumes A: "{x∈space (N ⨂⇩M M). snd x ∈ A (fst x)} ∈ sets (N ⨂⇩M M)"
shows "(λx. emeasure M (A x)) ∈ borel_measurable N"
proof -
from space have "⋀x. x ∈ space N ⟹ Pair x -` {x ∈ space (N ⨂⇩M M). snd x ∈ A (fst x)} = A x"
by (auto simp: space_pair_measure)
with measurable_emeasure_Pair'[OF A] show ?thesis
by (auto cong: measurable_cong)
qed
lemma(in s_finite_measure) emeasure_pair_measure':
assumes "X ∈ sets (N ⨂⇩M M)"
shows "emeasure (N ⨂⇩M M) X = (∫⇧+ x. ∫⇧+ y. indicator X (x, y) ∂M ∂N)" (is "_ = ?μ X")
proof (rule emeasure_measure_of[OF pair_measure_def])
show "positive (sets (N ⨂⇩M M)) ?μ"
by (auto simp: positive_def)
have eq[simp]: "⋀A x y. indicator A (x, y) = indicator (Pair x -` A) y"
by (auto simp: indicator_def)
show "countably_additive (sets (N ⨂⇩M M)) ?μ"
proof (rule countably_additiveI)
fix F :: "nat ⇒ ('b × 'a) set" assume F: "range F ⊆ sets (N ⨂⇩M M)" "disjoint_family F"
from F have *: "⋀i. F i ∈ sets (N ⨂⇩M M)" by auto
moreover have "⋀x. disjoint_family (λi. Pair x -` F i)"
by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
moreover have "⋀x. range (λi. Pair x -` F i) ⊆ sets M"
using F by (auto simp: sets_Pair1)
ultimately show "(∑n. ?μ (F n)) = ?μ (⋃i. F i)"
by (auto simp add: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure
intro!: nn_integral_cong nn_integral_indicator[symmetric])
qed
show "{a × b |a b. a ∈ sets N ∧ b ∈ sets M} ⊆ Pow (space N × space M)"
using sets.space_closed[of N] sets.space_closed[of M] by auto
qed fact
lemma (in s_finite_measure) emeasure_pair_measure_alt':
assumes X: "X ∈ sets (N ⨂⇩M M)"
shows "emeasure (N ⨂⇩M M) X = (∫⇧+x. emeasure M (Pair x -` X) ∂N)"
proof -
have [simp]: "⋀x y. indicator X (x, y) = indicator (Pair x -` X) y"
by (auto simp: indicator_def)
show ?thesis
using X by (auto intro!: nn_integral_cong simp: emeasure_pair_measure' sets_Pair1)
qed
proposition (in s_finite_measure) emeasure_pair_measure_Times':
assumes A: "A ∈ sets N" and B: "B ∈ sets M"
shows "emeasure (N ⨂⇩M M) (A × B) = emeasure N A * emeasure M B"
proof -
have "emeasure (N ⨂⇩M M) (A × B) = (∫⇧+x. emeasure M B * indicator A x ∂N)"
using A B by (auto intro!: nn_integral_cong simp: emeasure_pair_measure_alt')
also have "… = emeasure M B * emeasure N A"
using A by (simp add: nn_integral_cmult_indicator)
finally show ?thesis
by (simp add: ac_simps)
qed
lemma(in s_finite_measure) measure_times:
assumes[measurable]: "A ∈ sets N" "B ∈ sets M"
shows "measure (N ⨂⇩M M) (A × B) = measure N A * measure M B"
by(auto simp: measure_def emeasure_pair_measure_Times' enn2real_mult)
lemma pair_measure_s_finite_measure_suminf:
assumes Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
and Ni[measurable_cong]:"⋀i. sets (Ni i) = sets N" "⋀i. finite_measure (Ni i)" "⋀A. N A = (∑i. Ni i A)"
shows "(M ⨂⇩M N) A = (∑i j. (Mi i ⨂⇩M Ni j) A)" (is "?lhs = ?rhs")
proof -
interpret N: s_finite_measure N
by(auto intro!: s_finite_measureI[where Mi=Mi] s_finite_measureI[where Mi=Ni] assms)
show ?thesis
proof(cases "A ∈ sets (M ⨂⇩M N)")
case [measurable]:True
show ?thesis
proof -
have "?lhs = (∫⇧+x. N (Pair x -` A) ∂M)"
by(simp add: N.emeasure_pair_measure_alt')
also have "... = (∑i. ∫⇧+x. N (Pair x -` A) ∂Mi i)"
using N.measurable_emeasure_Pair'[of A]
by(auto intro!: nn_integral_measure_suminf[OF Mi(1,3),symmetric])
also have "... = (∑i. ∫⇧+x. (∑j. Ni j (Pair x -` A)) ∂Mi i)"
by(simp add: Ni(3))
also have "... = (∑i j. ∫⇧+x. Ni j (Pair x -` A) ∂Mi i)"
using s_finite_measure.measurable_emeasure_Pair'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)],of A]
by(auto simp: nn_integral_suminf intro!: suminf_cong)
also have "... = ?rhs"
by(auto intro!: suminf_cong simp: s_finite_measure.emeasure_pair_measure_alt'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)]])
finally show ?thesis .
qed
next
case False
with Mi(1) Ni(1) show ?thesis
by(simp add: emeasure_notin_sets)
qed
qed
lemma pair_measure_s_finite_measure_suminf':
assumes Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
and Ni[measurable_cong]:"⋀i. sets (Ni i) = sets N" "⋀i. finite_measure (Ni i)" "⋀A. N A = (∑i. Ni i A)"
shows "(M ⨂⇩M N) A = (∑i j. (Mi j ⨂⇩M Ni i) A)" (is "?lhs = ?rhs")
proof -
interpret N: s_finite_measure N
by(auto intro!: s_finite_measureI[where Mi=Mi] s_finite_measureI[where Mi=Ni] assms)
show ?thesis
proof(cases "A ∈ sets (M ⨂⇩M N)")
case [measurable]:True
show ?thesis
proof -
have "?lhs = (∫⇧+x. N (Pair x -` A) ∂M)"
by(simp add: N.emeasure_pair_measure_alt')
also have "... = (∫⇧+x. (∑i. Ni i (Pair x -` A)) ∂M)"
by(auto intro!: nn_integral_cong simp: Ni)
also have "... = (∑i. (∫⇧+x. Ni i (Pair x -` A) ∂M))"
by(auto intro!: nn_integral_suminf simp: finite_measure.finite_measure_cut_measurable[OF Ni(2)])
also have "... = (∑i j. ∫⇧+x. Ni i (Pair x -` A) ∂Mi j)"
by(auto intro!: suminf_cong nn_integral_measure_suminf[symmetric] simp: finite_measure.finite_measure_cut_measurable[OF Ni(2)] Mi)
also have "... = ?rhs"
by(auto intro!: suminf_cong simp: s_finite_measure.emeasure_pair_measure_alt'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)]])
finally show ?thesis .
qed
next
case False
with Mi(1) Ni(1) show ?thesis
by(simp add: emeasure_notin_sets)
qed
qed
lemma pair_measure_s_finite_measure:
assumes "s_finite_measure M" and "s_finite_measure N"
shows "s_finite_measure (M ⨂⇩M N)"
proof -
obtain Mi where Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by(metis s_finite_measure.finite_measures'[OF assms(1)])
obtain Ni where Ni[measurable_cong]:"⋀i. sets (Ni i) = sets N" "⋀i. finite_measure (Ni i)" "⋀A. N A = (∑i. Ni i A)"
by(metis s_finite_measure.finite_measures'[OF assms(2)])
show ?thesis
proof(rule s_finite_measure_prodI[where Mij="λi j. Mi i ⨂⇩M Ni j"])
show "emeasure (Mi i ⨂⇩M Ni j) (space (M ⨂⇩M N)) < ∞" for i j
using finite_measure.emeasure_finite[OF Mi(2)[of i]] finite_measure.emeasure_finite[OF Ni(2)[of j]]
by(auto simp: sets_eq_imp_space_eq[OF Mi(1)[of i],symmetric] sets_eq_imp_space_eq[OF Ni(1)[of j],symmetric] space_pair_measure s_finite_measure.emeasure_pair_measure_Times'[OF finite_measure.s_finite_measure_finite_measure[OF Ni(2)[of j]]] ennreal_mult_less_top top.not_eq_extremum)
qed(auto simp: pair_measure_s_finite_measure_suminf Mi Ni)
qed
lemma(in s_finite_measure) borel_measurable_nn_integral_fst':
assumes [measurable]: "f ∈ borel_measurable (N ⨂⇩M M)"
shows "(λx. ∫⇧+ y. f (x, y) ∂M) ∈ borel_measurable N"
proof -
obtain Mi where Mi[measurable_cong]:"⋀i. sets (Mi i) = sets M" "⋀i. finite_measure (Mi i)" "⋀A. M A = (∑i. Mi i A)"
by(metis finite_measures')
show ?thesis
by(rule measurable_cong[where g="λx. ∑i. ∫⇧+ y. f (x, y) ∂Mi i",THEN iffD2])
(auto simp: nn_integral_measure_suminf[OF Mi(1,3)] intro!: borel_measurable_suminf_order sigma_finite_measure.borel_measurable_nn_integral_fst[OF finite_measure.sigma_finite_measure[OF Mi(2)]])
qed
lemma (in s_finite_measure) nn_integral_fst':
assumes f: "f ∈ borel_measurable (M1 ⨂⇩M M)"
shows "(∫⇧+ x. ∫⇧+ y. f (x, y) ∂M ∂M1) = integral⇧N (M1 ⨂⇩M M) f" (is "?I f = _")
using f proof induct
case (cong u v)
then have "?I u = ?I v"
by (intro nn_integral_cong) (auto simp: space_pair_measure)
with cong show ?case
by (simp cong: nn_integral_cong)
qed (simp_all add: emeasure_pair_measure' nn_integral_cmult nn_integral_add
nn_integral_monotone_convergence_SUP measurable_compose_Pair1
borel_measurable_nn_integral_fst' nn_integral_mono incseq_def le_fun_def image_comp
cong: nn_integral_cong)
lemma (in s_finite_measure) borel_measurable_nn_integral'[measurable (raw)]:
"case_prod f ∈ borel_measurable (N ⨂⇩M M) ⟹ (λx. ∫⇧+ y. f x y ∂M) ∈ borel_measurable N"
using borel_measurable_nn_integral_fst'[of "case_prod f" N] by simp
lemma distr_pair_swap_s_finite:
assumes "s_finite_measure M1" and "s_finite_measure M2"
shows "M1 ⨂⇩M M2 = distr (M2 ⨂⇩M M1) (M1 ⨂⇩M M2) (λ(x, y). (y, x))" (is "?P = ?D")
proof -
{
from s_finite_measure.finite_measures'[OF assms(1)] s_finite_measure.finite_measures'[OF assms(2)]
obtain Mi1 Mi2
where Mi1:"⋀i. sets (Mi1 i) = sets M1" "⋀i. finite_measure (Mi1 i)" "⋀A. M1 A = (∑i. Mi1 i A)"
and Mi2:"⋀i. sets (Mi2 i) = sets M2" "⋀i. finite_measure (Mi2 i)" "⋀A. M2 A = (∑i. Mi2 i A)"
by metis
fix A
assume A[measurable]:"A ∈ sets (M1 ⨂⇩M M2)"
have "emeasure (M1 ⨂⇩M M2) A = emeasure (M2 ⨂⇩M M1) ((λ(x, y). (y, x)) -` A ∩ space (M2 ⨂⇩M M1))"
proof -
{
fix i j
interpret pair_sigma_finite "Mi1 i" "Mi2 j"
by(auto simp: pair_sigma_finite_def Mi1(2) Mi2(2) finite_measure.sigma_finite_measure)
have "emeasure (Mi1 i ⨂⇩M Mi2 j) A = emeasure (Mi2 j ⨂⇩M Mi1 i) ((λ(x, y). (y, x)) -` A ∩ space (M2 ⨂⇩M M1))"
using Mi1(1) Mi2(1) by(simp add: arg_cong[OF distr_pair_swap,of emeasure] emeasure_distr sets_eq_imp_space_eq[OF sets_pair_measure_cong[OF Mi2(1) Mi1(1)]])
}
thus ?thesis
by(auto simp: pair_measure_s_finite_measure_suminf'[OF Mi2 Mi1] pair_measure_s_finite_measure_suminf[OF Mi1 Mi2] intro!: suminf_cong)
qed
}
thus ?thesis
by(auto intro!: measure_eqI simp: emeasure_distr)
qed
proposition nn_integral_snd':
assumes "s_finite_measure M1" "s_finite_measure M2"
and f[measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M2)"
shows "(∫⇧+ y. (∫⇧+ x. f (x, y) ∂M1) ∂M2) = integral⇧N (M1 ⨂⇩M M2) f"
proof -
interpret M1: s_finite_measure M1 by fact
interpret M2: s_finite_measure M2 by fact
note measurable_pair_swap[OF f]
from M1.nn_integral_fst'[OF this]
have "(∫⇧+ y. (∫⇧+ x. f (x, y) ∂M1) ∂M2) = (∫⇧+ (x, y). f (y, x) ∂(M2 ⨂⇩M M1))"
by simp
also have "(∫⇧+ (x, y). f (y, x) ∂(M2 ⨂⇩M M1)) = integral⇧N (M1 ⨂⇩M M2) f"
by (subst distr_pair_swap_s_finite[OF assms(1,2)]) (auto simp add: nn_integral_distr intro!: nn_integral_cong)
finally show ?thesis .
qed
lemma (in s_finite_measure) borel_measurable_lebesgue_integrable'[measurable (raw)]:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]: "case_prod f ∈ borel_measurable (N ⨂⇩M M)"
shows "Measurable.pred N (λx. integrable M (f x))"
proof -
have [simp]: "⋀x. x ∈ space N ⟹ integrable M (f x) ⟷ (∫⇧+y. norm (f x y) ∂M) < ∞"
unfolding integrable_iff_bounded by simp
show ?thesis
by (simp cong: measurable_cong)
qed
lemma (in s_finite_measure) measurable_measure'[measurable (raw)]:
"(⋀x. x ∈ space N ⟹ A x ⊆ space M) ⟹
{x ∈ space (N ⨂⇩M M). snd x ∈ A (fst x)} ∈ sets (N ⨂⇩M M) ⟹
(λx. measure M (A x)) ∈ borel_measurable N"
unfolding measure_def by (intro measurable_emeasure' borel_measurable_enn2real) auto
proposition (in s_finite_measure) borel_measurable_lebesgue_integral'[measurable (raw)]:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "case_prod f ∈ borel_measurable (N ⨂⇩M M)"
shows "(λx. ∫y. f x y ∂M) ∈ borel_measurable N"
proof -
from borel_measurable_implies_sequence_metric[OF f, of 0]
obtain s where s: "⋀i. simple_function (N ⨂⇩M M) (s i)"
and "∀x∈space (N ⨂⇩M M). (λi. s i x) ⇢ (case x of (x, y) ⇒ f x y)"
and "∀i. ∀x∈space (N ⨂⇩M M). dist (s i x) 0 ≤ 2 * dist (case x of (x, xa) ⇒ f x xa) 0"
by auto
then have *:
"⋀x y. x ∈ space N ⟹ y ∈ space M ⟹ (λi. s i (x, y)) ⇢ f x y"
"⋀i x y. x ∈ space N ⟹ y ∈ space M ⟹ norm (s i (x, y)) ≤ 2 * norm (f x y)"
by (auto simp: space_pair_measure)
have [measurable]: "⋀i. s i ∈ borel_measurable (N ⨂⇩M M)"
by (rule borel_measurable_simple_function) fact
have "⋀i. s i ∈ measurable (N ⨂⇩M M) (count_space UNIV)"
by (rule measurable_simple_function) fact
define f' where [abs_def]: "f' i x =
(if integrable M (f x) then Bochner_Integration.simple_bochner_integral M (λy. s i (x, y)) else 0)" for i x
{ fix i x assume "x ∈ space N"
then have "Bochner_Integration.simple_bochner_integral M (λy. s i (x, y)) =
(∑z∈s i ` (space N × space M). measure M {y ∈ space M. s i (x, y) = z} *⇩R z)"
using s[THEN simple_functionD(1)]
unfolding simple_bochner_integral_def
by (intro sum.mono_neutral_cong_left)
(auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
note eq = this
show ?thesis
proof (rule borel_measurable_LIMSEQ_metric)
fix i show "f' i ∈ borel_measurable N"
unfolding f'_def by (simp_all add: eq cong: measurable_cong if_cong)
next
fix x assume x: "x ∈ space N"
{ assume int_f: "integrable M (f x)"
have int_2f: "integrable M (λy. 2 * norm (f x y))"
by (intro integrable_norm integrable_mult_right int_f)
have "(λi. integral⇧L M (λy. s i (x, y))) ⇢ integral⇧L M (f x)"
proof (rule integral_dominated_convergence)
from int_f show "f x ∈ borel_measurable M" by auto
show "⋀i. (λy. s i (x, y)) ∈ borel_measurable M"
using x by simp
show "AE xa in M. (λi. s i (x, xa)) ⇢ f x xa"
using x * by auto
show "⋀i. AE xa in M. norm (s i (x, xa)) ≤ 2 * norm (f x xa)"
using x * by auto
qed fact
moreover
{ fix i
have "Bochner_Integration.simple_bochner_integrable M (λy. s i (x, y))"
proof (rule simple_bochner_integrableI_bounded)
have "(λy. s i (x, y)) ` space M ⊆ s i ` (space N × space M)"
using x by auto
then show "simple_function M (λy. s i (x, y))"
using simple_functionD(1)[OF s(1), of i] x
by (intro simple_function_borel_measurable)
(auto simp: space_pair_measure dest: finite_subset)
have "(∫⇧+ y. ennreal (norm (s i (x, y))) ∂M) ≤ (∫⇧+ y. 2 * norm (f x y) ∂M)"
using x * by (intro nn_integral_mono) auto
also have "(∫⇧+ y. 2 * norm (f x y) ∂M) < ∞"
using int_2f unfolding integrable_iff_bounded by simp
finally show "(∫⇧+ xa. ennreal (norm (s i (x, xa))) ∂M) < ∞" .
qed
then have "integral⇧L M (λy. s i (x, y)) = Bochner_Integration.simple_bochner_integral M (λy. s i (x, y))"
by (rule simple_bochner_integrable_eq_integral[symmetric]) }
ultimately have "(λi. Bochner_Integration.simple_bochner_integral M (λy. s i (x, y))) ⇢ integral⇧L M (f x)"
by simp }
then
show "(λi. f' i x) ⇢ integral⇧L M (f x)"
unfolding f'_def
by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
qed
qed
lemma integrable_product_swap_s_finite:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
and "integrable (M1 ⨂⇩M M2) f"
shows "integrable (M2 ⨂⇩M M1) (λ(x,y). f (y,x))"
proof -
have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)⇒(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (rule integrable_distr[OF measurable_pair_swap'])
(simp add: distr_pair_swap_s_finite[OF M1 M2,symmetric] assms)
qed
lemma integrable_product_swap_iff_s_finite:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
shows "integrable (M2 ⨂⇩M M1) (λ(x,y). f (y,x)) ⟷ integrable (M1 ⨂⇩M M2) f"
proof -
from integrable_product_swap_s_finite[OF M2 M1,of "λ(x,y). f (y,x)"] integrable_product_swap_s_finite[OF M1 M2,of f]
show ?thesis by auto
qed
lemma integral_product_swap_s_finite:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
and f: "f ∈ borel_measurable (M1 ⨂⇩M M2)"
shows "(∫(x,y). f (y,x) ∂(M2 ⨂⇩M M1)) = integral⇧L (M1 ⨂⇩M M2) f"
proof -
have *: "(λ(x,y). f (y,x)) = (λx. f (case x of (x,y)⇒(y,x)))" by (auto simp: fun_eq_iff)
show ?thesis unfolding *
by (simp add: integral_distr[symmetric, OF measurable_pair_swap' f] distr_pair_swap_s_finite[OF M1 M2,symmetric])
qed
theorem(in s_finite_measure) Fubini_integrable':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M)"
and integ1: "integrable M1 (λx. ∫ y. norm (f (x, y)) ∂M)"
and integ2: "AE x in M1. integrable M (λy. f (x, y))"
shows "integrable (M1 ⨂⇩M M) f"
proof (rule integrableI_bounded)
have "(∫⇧+ p. norm (f p) ∂(M1 ⨂⇩M M)) = (∫⇧+ x. (∫⇧+ y. norm (f (x, y)) ∂M) ∂M1)"
by (simp add: nn_integral_fst'[symmetric])
also have "… = (∫⇧+ x. ¦∫y. norm (f (x, y)) ∂M¦ ∂M1)"
proof(rule nn_integral_cong_AE)
show "AE x in M1. (∫⇧+ y. ennreal (norm (f (x, y))) ∂M) = ennreal ¦LINT y|M. norm (f (x, y))¦"
using integ2
proof eventually_elim
fix x assume "integrable M (λy. f (x, y))"
then have f: "integrable M (λy. norm (f (x, y)))"
by simp
then have "(∫⇧+y. ennreal (norm (f (x, y))) ∂M) = ennreal (LINT y|M. norm (f (x, y)))"
by (rule nn_integral_eq_integral) simp
also have "… = ennreal ¦LINT y|M. norm (f (x, y))¦"
using f by simp
finally show "(∫⇧+y. ennreal (norm (f (x, y))) ∂M) = ennreal ¦LINT y|M. norm (f (x, y))¦" .
qed
qed
also have "… < ∞"
using integ1 by (simp add: integrable_iff_bounded integral_nonneg_AE)
finally show "(∫⇧+ p. norm (f p) ∂(M1 ⨂⇩M M)) < ∞" .
qed fact
lemma(in s_finite_measure) emeasure_pair_measure_finite':
assumes A: "A ∈ sets (M1 ⨂⇩M M)" and finite: "emeasure (M1 ⨂⇩M M) A < ∞"
shows "AE x in M1. emeasure M {y∈space M. (x, y) ∈ A} < ∞"
proof -
from emeasure_pair_measure_alt'[OF A] finite
have "(∫⇧+ x. emeasure M (Pair x -` A) ∂M1) ≠ ∞"
by simp
then have "AE x in M1. emeasure M (Pair x -` A) ≠ ∞"
by (rule nn_integral_PInf_AE[rotated]) (intro measurable_emeasure_Pair' A)
moreover have "⋀x. x ∈ space M1 ⟹ Pair x -` A = {y∈space M. (x, y) ∈ A}"
using sets.sets_into_space[OF A] by (auto simp: space_pair_measure)
ultimately show ?thesis by (auto simp: less_top)
qed
lemma(in s_finite_measure) AE_integrable_fst''':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M) f"
shows "AE x in M1. integrable M (λy. f (x, y))"
proof -
have "(∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M) ∂M1) = (∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M))"
by (rule nn_integral_fst') simp
also have "(∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M)) ≠ ∞"
using f unfolding integrable_iff_bounded by simp
finally have "AE x in M1. (∫⇧+y. norm (f (x, y)) ∂M) ≠ ∞"
by (intro nn_integral_PInf_AE borel_measurable_nn_integral')
(auto simp: measurable_split_conv)
with AE_space show ?thesis
by eventually_elim
(auto simp: integrable_iff_bounded measurable_compose[OF _ borel_measurable_integrable[OF f]] less_top)
qed
lemma(in s_finite_measure) integrable_fst_norm':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M) f"
shows "integrable M1 (λx. ∫y. norm (f (x, y)) ∂M)"
unfolding integrable_iff_bounded
proof
show "(λx. ∫ y. norm (f (x, y)) ∂M) ∈ borel_measurable M1"
by (rule borel_measurable_lebesgue_integral') simp
have "(∫⇧+ x. ennreal (norm (∫y. norm (f (x, y)) ∂M)) ∂M1) = (∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M) ∂M1)"
using AE_integrable_fst'''[OF f] by (auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral)
also have "(∫⇧+x. (∫⇧+y. norm (f (x, y)) ∂M) ∂M1) = (∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M))"
by (rule nn_integral_fst') simp
also have "(∫⇧+x. norm (f x) ∂(M1 ⨂⇩M M)) < ∞"
using f unfolding integrable_iff_bounded by simp
finally show "(∫⇧+ x. ennreal (norm (∫y. norm (f (x, y)) ∂M)) ∂M1) < ∞" .
qed
lemma(in s_finite_measure) integrable_fst''':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f[measurable]: "integrable (M1 ⨂⇩M M) f"
shows "integrable M1 (λx. ∫y. f (x, y) ∂M)"
by(auto intro!: Bochner_Integration.integrable_bound[OF integrable_fst_norm'[OF f]])
proposition(in s_finite_measure) integral_fst''':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes f: "integrable (M1 ⨂⇩M M) f"
shows "(∫x. (∫y. f (x, y) ∂M) ∂M1) = integral⇧L (M1 ⨂⇩M M) f"
using f proof induct
case (base A c)
have A[measurable]: "A ∈ sets (M1 ⨂⇩M M)" by fact
have eq: "⋀x y. x ∈ space M1 ⟹ indicator A (x, y) = indicator {y∈space M. (x, y) ∈ A} y"
using sets.sets_into_space[OF A] by (auto split: split_indicator simp: space_pair_measure)
have int_A: "integrable (M1 ⨂⇩M M) (indicator A :: _ ⇒ real)"
using base by (rule integrable_real_indicator)
have "(∫ x. ∫ y. indicator A (x, y) *⇩R c ∂M ∂M1) = (∫x. measure M {y∈space M. (x, y) ∈ A} *⇩R c ∂M1)"
proof (intro integral_cong_AE)
from AE_integrable_fst'''[OF int_A] AE_space
show "AE x in M1. (∫y. indicator A (x, y) *⇩R c ∂M) = measure M {y∈space M. (x, y) ∈ A} *⇩R c"
by eventually_elim (simp add: eq integrable_indicator_iff)
qed simp_all
also have "… = measure (M1 ⨂⇩M M) A *⇩R c"
proof (subst integral_scaleR_left)
have "(∫⇧+x. ennreal (measure M {y ∈ space M. (x, y) ∈ A}) ∂M1) =
(∫⇧+x. emeasure M {y ∈ space M. (x, y) ∈ A} ∂M1)"
using emeasure_pair_measure_finite'[OF base]
by (intro nn_integral_cong_AE, eventually_elim) (simp add: emeasure_eq_ennreal_measure)
also have "… = emeasure (M1 ⨂⇩M M) A"
using sets.sets_into_space[OF A]
by (subst emeasure_pair_measure_alt')
(auto intro!: nn_integral_cong arg_cong[where f="emeasure M"] simp: space_pair_measure)
finally have *: "(∫⇧+x. ennreal (measure M {y ∈ space M. (x, y) ∈ A}) ∂M1) = emeasure (M1 ⨂⇩M M) A" .
from base * show "integrable M1 (λx. measure M {y ∈ space M. (x, y) ∈ A})"
by (simp add: integrable_iff_bounded)
then have "(∫x. measure M {y ∈ space M. (x, y) ∈ A} ∂M1) =
(∫⇧+x. ennreal (measure M {y ∈ space M. (x, y) ∈ A}) ∂M1)"
by (rule nn_integral_eq_integral[symmetric]) simp
also note *
finally show "(∫x. measure M {y ∈ space M. (x, y) ∈ A} ∂M1) *⇩R c = measure (M1 ⨂⇩M M) A *⇩R c"
using base by (simp add: emeasure_eq_ennreal_measure)
qed
also have "… = (∫ a. indicator A a *⇩R c ∂(M1 ⨂⇩M M))"
using base by simp
finally show ?case .
next
case (add f g)
then have [measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M)" "g ∈ borel_measurable (M1 ⨂⇩M M)"
by auto
have "(∫ x. ∫ y. f (x, y) + g (x, y) ∂M ∂M1) =
(∫ x. (∫ y. f (x, y) ∂M) + (∫ y. g (x, y) ∂M) ∂M1)"
apply (rule integral_cong_AE)
apply simp_all
using AE_integrable_fst'''[OF add(1)] AE_integrable_fst'''[OF add(3)]
apply eventually_elim
apply simp
done
also have "… = (∫ x. f x ∂(M1 ⨂⇩M M)) + (∫ x. g x ∂(M1 ⨂⇩M M))"
using integrable_fst'''[OF add(1)] integrable_fst'''[OF add(3)] add(2,4) by simp
finally show ?case
using add by simp
next
case (lim f s)
then have [measurable]: "f ∈ borel_measurable (M1 ⨂⇩M M)" "⋀i. s i ∈ borel_measurable (M1 ⨂⇩M M)"
by auto
show ?case
proof (rule LIMSEQ_unique)
show "(λi. integral⇧L (M1 ⨂⇩M M) (s i)) ⇢ integral⇧L (M1 ⨂⇩M M) f"
proof (rule integral_dominated_convergence)
show "integrable (M1 ⨂⇩M M) (λx. 2 * norm (f x))"
using lim(5) by auto
qed (insert lim, auto)
have "(λi. ∫ x. ∫ y. s i (x, y) ∂M ∂M1) ⇢ ∫ x. ∫ y. f (x, y) ∂M ∂M1"
proof (rule integral_dominated_convergence)
have "AE x in M1. ∀i. integrable M (λy. s i (x, y))"
unfolding AE_all_countable using AE_integrable_fst'''[OF lim(1)] ..
with AE_space AE_integrable_fst'''[OF lim(5)]
show "AE x in M1. (λi. ∫ y. s i (x, y) ∂M) ⇢ ∫ y. f (x, y) ∂M"
proof eventually_elim
fix x assume x: "x ∈ space M1" and
s: "∀i. integrable M (λy. s i (x, y))" and f: "integrable M (λy. f (x, y))"
show "(λi. ∫ y. s i (x, y) ∂M) ⇢ ∫ y. f (x, y) ∂M"
proof (rule integral_dominated_convergence)
show "integrable M (λy. 2 * norm (f (x, y)))"
using f by auto
show "AE xa in M. (λi. s i (x, xa)) ⇢ f (x, xa)"
using x lim(3) by (auto simp: space_pair_measure)
show "⋀i. AE xa in M. norm (s i (x, xa)) ≤ 2 * norm (f (x, xa))"
using x lim(4) by (auto simp: space_pair_measure)
qed (insert x, measurable)
qed
show "integrable M1 (λx. (∫ y. 2 * norm (f (x, y)) ∂M))"
by (intro integrable_mult_right integrable_norm integrable_fst''' lim)
fix i show "AE x in M1. norm (∫ y. s i (x, y) ∂M) ≤ (∫ y. 2 * norm (f (x, y)) ∂M)"
using AE_space AE_integrable_fst'''[OF lim(1), of i] AE_integrable_fst'''[OF lim(5)]
proof eventually_elim
fix x assume x: "x ∈ space M1"
and s: "integrable M (λy. s i (x, y))" and f: "integrable M (λy. f (x, y))"
from s have "norm (∫ y. s i (x, y) ∂M) ≤ (∫⇧+y. norm (s i (x, y)) ∂M)"
by (rule integral_norm_bound_ennreal)
also have "… ≤ (∫⇧+y. 2 * norm (f (x, y)) ∂M)"
using x lim by (auto intro!: nn_integral_mono simp: space_pair_measure)
also have "… = (∫y. 2 * norm (f (x, y)) ∂M)"
using f by (intro nn_integral_eq_integral) auto
finally show "norm (∫ y. s i (x, y) ∂M) ≤ (∫ y. 2 * norm (f (x, y)) ∂M)"
by simp
qed
qed simp_all
then show "(λi. integral⇧L (M1 ⨂⇩M M) (s i)) ⇢ ∫ x. ∫ y. f (x, y) ∂M ∂M1"
using lim by simp
qed
qed
lemma (in s_finite_measure)
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes f: "integrable (M1 ⨂⇩M M) (case_prod f)"
shows AE_integrable_fst'': "AE x in M1. integrable M (λy. f x y)"
and integrable_fst'': "integrable M1 (λx. ∫y. f x y ∂M)"
and integrable_fst_norm: "integrable M1 (λx. ∫y. norm (f x y) ∂M)"
and integral_fst'': "(∫x. (∫y. f x y ∂M) ∂M1) = integral⇧L (M1 ⨂⇩M M) (λ(x, y). f x y)"
using AE_integrable_fst'''[OF f] integrable_fst'''[OF f] integral_fst'''[OF f] integrable_fst_norm'[OF f] by auto
lemma
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
and f[measurable]: "integrable (M1 ⨂⇩M M2) (case_prod f)"
shows AE_integrable_snd_s_finite: "AE y in M2. integrable M1 (λx. f x y)" (is "?AE")
and integrable_snd_s_finite: "integrable M2 (λy. ∫x. f x y ∂M1)" (is "?INT")
and integrable_snd_norm_s_finite: "integrable M2 (λy. ∫x. norm (f x y) ∂M1)" (is "?INT2")
and integral_snd_s_finite: "(∫y. (∫x. f x y ∂M1) ∂M2) = integral⇧L (M1 ⨂⇩M M2) (case_prod f)" (is "?EQ")
proof -
interpret Q: s_finite_measure M1 by fact
have Q_int: "integrable (M2 ⨂⇩M M1) (λ(x, y). f y x)"
using f unfolding integrable_product_swap_iff_s_finite[OF M1 M2,symmetric] by simp
show ?AE using Q.AE_integrable_fst'''[OF Q_int] by simp
show ?INT using Q.integrable_fst'''[OF Q_int] by simp
show ?INT2 using Q.integrable_fst_norm[OF Q_int] by simp
show ?EQ using Q.integral_fst'''[OF Q_int]
using integral_product_swap_s_finite[OF M1 M2,of "case_prod f"] by simp
qed
proposition Fubini_integral':
fixes f :: "_ ⇒ _ ⇒ _ :: {banach, second_countable_topology}"
assumes M1:"s_finite_measure M1" and M2:"s_finite_measure M2"
and f: "integrable (M1 ⨂⇩M M2) (case_prod f)"
shows "(∫y. (∫x. f x y ∂M1) ∂M2) = (∫x. (∫y. f x y ∂M2) ∂M1)"
unfolding integral_snd_s_finite[OF assms] s_finite_measure.integral_fst''[OF assms(2,3)] ..
locale product_s_finite =
fixes M :: "'i ⇒ 'a measure"
assumes s_finite_measures: "⋀i. s_finite_measure (M i)"
sublocale product_s_finite ⊆ M?: s_finite_measure "M i" for i
by (rule s_finite_measures)
locale finite_product_s_finite = product_s_finite M for M :: "'i ⇒ 'a measure" +
fixes I :: "'i set"
assumes finite_index: "finite I"
lemma (in product_s_finite) emeasure_PiM:
"finite I ⟹ (⋀i. i∈I ⟹ A i ∈ sets (M i)) ⟹ emeasure (PiM I M) (Pi⇩E I A) = (∏i∈I. emeasure (M i) (A i))"
proof (induct I arbitrary: A rule: finite_induct)
case (insert i I)
interpret finite_product_s_finite M I by standard fact
have "finite (insert i I)" using ‹finite I› by auto
interpret I': finite_product_s_finite M "insert i I" by standard fact
let ?h = "(λ(f, y). f(i := y))"
let ?P = "distr (Pi⇩M I M ⨂⇩M M i) (Pi⇩M (insert i I) M) ?h"
let ?μ = "emeasure ?P"
let ?I = "{j ∈ insert i I. emeasure (M j) (space (M j)) ≠ 1}"
let ?f = "λJ E j. if j ∈ J then emeasure (M j) (E j) else emeasure (M j) (space (M j))"
have "emeasure (Pi⇩M (insert i I) M) (prod_emb (insert i I) M (insert i I) (Pi⇩E (insert i I) A)) =
(∏i∈insert i I. emeasure (M i) (A i))"
proof (subst emeasure_extend_measure_Pair[OF PiM_def])
fix J E assume "(J ≠ {} ∨ insert i I = {}) ∧ finite J ∧ J ⊆ insert i I ∧ E ∈ (Π j∈J. sets (M j))"
then have J: "J ≠ {}" "finite J" "J ⊆ insert i I" and E: "∀j∈J. E j ∈ sets (M j)" by auto
let ?p = "prod_emb (insert i I) M J (Pi⇩E J E)"
let ?p' = "prod_emb I M (J - {i}) (Π⇩E j∈J-{i}. E j)"
have "?μ ?p =
emeasure (Pi⇩M I M ⨂⇩M (M i)) (?h -` ?p ∩ space (Pi⇩M I M ⨂⇩M M i))"
by (intro emeasure_distr measurable_add_dim sets_PiM_I) fact+
also have "?h -` ?p ∩ space (Pi⇩M I M ⨂⇩M M i) = ?p' × (if i ∈ J then E i else space (M i))"
using J E[rule_format, THEN sets.sets_into_space]
by (force simp: space_pair_measure space_PiM prod_emb_iff PiE_def Pi_iff split: if_split_asm)
also have "emeasure (Pi⇩M I M ⨂⇩M (M i)) (?p' × (if i ∈ J then E i else space (M i))) =
emeasure (Pi⇩M I M) ?p' * emeasure (M i) (if i ∈ J then (E i) else space (M i))"
using J E by (intro M.emeasure_pair_measure_Times' sets_PiM_I) auto
also have "?p' = (Π⇩E j∈I. if j ∈ J-{i} then E j else space (M j))"
using J E[rule_format, THEN sets.sets_into_space]
by (auto simp: prod_emb_iff PiE_def Pi_iff split: if_split_asm) blast+
also have "emeasure (Pi⇩M I M) (Π⇩E j∈I. if j ∈ J-{i} then E j else space (M j)) =
(∏ j∈I. if j ∈ J-{i} then emeasure (M j) (E j) else emeasure (M j) (space (M j)))"
using E by (subst insert) (auto intro!: prod.cong)
also have "(∏j∈I. if j ∈ J - {i} then emeasure (M j) (E j) else emeasure (M j) (space (M j))) *
emeasure (M i) (if i ∈ J then E i else space (M i)) = (∏j∈insert i I. ?f J E j)"
using insert by (auto simp: mult.commute intro!: arg_cong2[where f="(*)"] prod.cong)
also have "… = (∏j∈J ∪ ?I. ?f J E j)"
using insert(1,2) J E by (intro prod.mono_neutral_right) auto
finally show "?μ ?p = …" .
show "prod_emb (insert i I) M J (Pi⇩E J E) ∈ Pow (Π⇩E i∈insert i I. space (M i))"
using J E[rule_format, THEN sets.sets_into_space] by (auto simp: prod_emb_iff PiE_def)
next
show "positive (sets (Pi⇩M (insert i I) M)) ?μ" "countably_additive (sets (Pi⇩M (insert i I) M)) ?μ"
using emeasure_positive[of ?P] emeasure_countably_additive[of ?P] by simp_all
next
show "(insert i I ≠ {} ∨ insert i I = {}) ∧ finite (insert i I) ∧
insert i I ⊆ insert i I ∧ A ∈ (Π j∈insert i I. sets (M j))"
using insert by auto
qed (auto intro!: prod.cong)
with insert show ?case
by (subst (asm) prod_emb_PiE_same_index) (auto intro!: sets.sets_into_space)
qed simp
lemma (in finite_product_s_finite) measure_times:
"(⋀i. i ∈ I ⟹ A i ∈ sets (M i)) ⟹ emeasure (Pi⇩M I M) (Pi⇩E I A) = (∏i∈I. emeasure (M i) (A i))"
using emeasure_PiM[OF finite_index] by auto
lemma (in product_s_finite) nn_integral_empty:
"0 ≤ f (λk. undefined) ⟹ integral⇧N (Pi⇩M {} M) f = f (λk. undefined)"
by (simp add: PiM_empty nn_integral_count_space_finite)
text ‹ Every s-finite measure is represented as the push-forward measure of a $\sigma$-finite measure.›
definition Mi_to_NM :: "(nat ⇒ 'a measure) ⇒ 'a measure ⇒ (nat × 'a) measure" where
"Mi_to_NM Mi M ≡ measure_of (space (count_space UNIV ⨂⇩M M)) (sets (count_space UNIV ⨂⇩M M)) (λA. ∑i. distr (Mi i) (count_space UNIV ⨂⇩M M) (λx. (i,x)) A)"
lemma
shows sets_Mi_to_NM[measurable_cong,simp]: "sets (Mi_to_NM Mi M) = sets (count_space UNIV ⨂⇩M M)"
and space_Mi_to_NM[simp]: "space (Mi_to_NM Mi M) = space (count_space UNIV ⨂⇩M M)"
by(simp_all add: Mi_to_NM_def)
context
fixes M :: "'a measure" and Mi :: "nat ⇒ 'a measure"
assumes sets_Mi[measurable_cong,simp]: "⋀i. sets (Mi i) = sets M"
and emeasure_Mi: "⋀A. A ∈ sets M ⟹ M A = (∑i. Mi i A)"
begin
lemma emeasure_Mi_to_NM:
assumes [measurable]: "A ∈ sets (count_space UNIV ⨂⇩M M)"
shows "emeasure (Mi_to_NM Mi M) A = (∑i. distr (Mi i) (count_space UNIV ⨂⇩M M) (λx. (i,x)) A)"
proof(rule emeasure_measure_of[where Ω="space (count_space UNIV ⨂⇩M M)" and A="sets (count_space UNIV ⨂⇩M M)"])
show "countably_additive (sets (Mi_to_NM Mi M)) (λA. ∑i. emeasure (distr (Mi i) (count_space UNIV ⨂⇩M M) (Pair i)) A)"
unfolding countably_additive_def
proof safe
fix A :: "nat ⇒ (nat × _) set"
assume "range A ⊆ sets (Mi_to_NM Mi M)" and dA:"disjoint_family A"
hence [measurable]: "⋀i. A i ∈ sets (count_space UNIV ⨂⇩M M)"
by auto
show "(∑j i. emeasure (distr (Mi i) (count_space UNIV ⨂⇩M M) (Pair i)) (A j)) = (∑i. emeasure (distr (Mi i) (count_space UNIV ⨂⇩M M) (Pair i)) (⋃ (range A)))" (is "?lhs = ?rhs")
proof -
have "?lhs = (∑i j. emeasure (distr (Mi i) (count_space UNIV ⨂⇩M M) (Pair i)) (A j))"
by(auto simp: nn_integral_count_space_nat[symmetric] pair_sigma_finite_def sigma_finite_measure_count_space intro!: pair_sigma_finite.Fubini')
also have "... = ?rhs"
proof(rule suminf_cong)
fix n
have [simp]:"Pair n -` ⋃ (range A) = (⋃ (range (λj. Pair n -` A j)))"
by auto
show " (∑j. emeasure (distr (Mi n) (count_space UNIV ⨂⇩M M) (Pair n)) (A j)) = emeasure (distr (Mi n) (count_space UNIV ⨂⇩M M) (Pair n)) (⋃ (range A))"
using dA by(fastforce intro!: suminf_emeasure simp: disjoint_family_on_def emeasure_distr)
qed
finally show ?thesis .
qed
qed
qed(auto simp: positive_def sets.space_closed Mi_to_NM_def)
lemma sigma_finite_Mi_to_NM_measure:
assumes "⋀i. finite_measure (Mi i)"
shows "sigma_finite_measure (Mi_to_NM Mi M)"
proof -
{
fix n
assume "emeasure (Mi_to_NM Mi M) ({n} × space M) = ⊤"
moreover have "emeasure (Mi_to_NM Mi M) ({n} × space M) = emeasure (Mi n) (space M)"
by(simp add: emeasure_Mi_to_NM emeasure_distr suminf_offset[of _ "Suc n"])
ultimately have False
using finite_measure.finite_emeasure_space[OF assms[of n]] by(auto simp: sets_eq_imp_space_eq[OF sets_Mi])
}
thus ?thesis
by(auto intro!: exI[where x="⋃i. {{i} × space M}"] simp: space_pair_measure sigma_finite_measure_def)
qed
lemma distr_Mi_to_NM_M: "distr (Mi_to_NM Mi M) M snd = M"
proof -
have [simp]:"Pair i -` snd -` A ∩ Pair i -` space (count_space UNIV ⨂⇩M M) = A" if "A ∈ sets M" for A and i :: nat
using sets.sets_into_space[OF that] by(auto simp: space_pair_measure)
show ?thesis
by(auto intro!: measure_eqI simp: emeasure_distr emeasure_Mi_to_NM emeasure_Mi)
qed
end
context
fixes μ :: "'a measure"
assumes standard_borel_ne: "standard_borel_ne μ"
and s_finite: "s_finite_measure μ"
begin
interpretation μ : s_finite_measure μ by fact
interpretation n_μ: standard_borel_ne "count_space (UNIV :: nat set) ⨂⇩M μ"
by (simp add: pair_standard_borel_ne standard_borel_ne)
lemma exists_push_forward:
"∃(μ' :: real measure) f. f ∈ borel →⇩M μ ∧ sets μ' = sets borel ∧ sigma_finite_measure μ'
∧ distr μ' μ f = μ"
proof -
obtain μi where μi: "⋀i. sets (μi i) = sets μ" "⋀i. finite_measure (μi i)" "⋀A. μ A = (∑i. μi i A)"
by(metis μ.finite_measures')
show ?thesis
proof(safe intro!: exI[where x="distr (Mi_to_NM μi μ) borel n_μ.to_real"] exI[where x="snd ∘ n_μ.from_real"])
have [simp]:"distr (distr (Mi_to_NM μi μ) borel n_μ.to_real) (count_space UNIV ⨂⇩M μ) n_μ.from_real = Mi_to_NM μi μ"
by(auto simp: distr_distr comp_def intro!:distr_id')
show "sigma_finite_measure (distr (Mi_to_NM μi μ) borel n_μ.to_real)"
by(rule sigma_finite_measure_distr[where N="count_space UNIV ⨂⇩M μ" and f=n_μ.from_real]) (auto intro!: sigma_finite_Mi_to_NM_measure μi)
next
have [simp]: "distr (Mi_to_NM μi μ) μ (snd ∘ n_μ.from_real ∘ n_μ.to_real) = distr (Mi_to_NM μi μ) μ snd"
by(auto intro!: distr_cong[OF refl])
show "distr (distr (Mi_to_NM μi μ) borel n_μ.to_real) μ (snd ∘ n_μ.from_real) = μ"
by(auto simp: distr_distr distr_Mi_to_NM_M[OF μi(1,3)])
qed auto
qed
abbreviation "μ'_and_f ≡ (SOME (μ'::real measure,f). f ∈ borel →⇩M μ ∧ sets μ' = sets borel ∧ sigma_finite_measure μ' ∧ distr μ' μ f = μ)"
definition "sigma_pair_μ ≡ fst μ'_and_f"
definition "sigma_pair_f ≡ snd μ'_and_f"
lemma
shows sigma_pair_f_measurable : "sigma_pair_f ∈ borel →⇩M μ" (is ?g1)
and sets_sigma_pair_μ: "sets sigma_pair_μ = sets borel" (is ?g2)
and sigma_finite_sigma_pair_μ: "sigma_finite_measure sigma_pair_μ" (is ?g3)
and distr_sigma_pair: "distr sigma_pair_μ μ sigma_pair_f = μ" (is ?g4)
proof -
have "case μ'_and_f of (μ',f) ⇒ f ∈ borel →⇩M μ ∧ sets μ' = sets borel ∧ sigma_finite_measure μ' ∧ distr μ' μ f = μ"
by(rule someI_ex) (use exists_push_forward in auto)
then show ?g1 ?g2 ?g3 ?g4
by(auto simp: sigma_pair_μ_def sigma_pair_f_def split_beta)
qed
end
definition s_finite_measure_algebra :: "'a measure ⇒ 'a measure measure" where
"s_finite_measure_algebra K =
(SUP A ∈ sets K. vimage_algebra {M. s_finite_measure M ∧ sets M = sets K} (λM. emeasure M A) borel)"
lemma space_s_finite_measure_algebra:
"space (s_finite_measure_algebra K) = {M. s_finite_measure M ∧ sets M = sets K}"
by (auto simp add: s_finite_measure_algebra_def space_Sup_eq_UN)
lemma s_finite_measure_algebra_cong: "sets M = sets N ⟹ s_finite_measure_algebra M = s_finite_measure_algebra N"
by (simp add: s_finite_measure_algebra_def)
lemma measurable_emeasure_s_finite_measure_algebra[measurable]:
"a ∈ sets A ⟹ (λM. emeasure M a) ∈ borel_measurable (s_finite_measure_algebra A)"
by (auto intro!: measurable_Sup1 measurable_vimage_algebra1 simp: s_finite_measure_algebra_def)
lemma measurable_measure_s_finite_measure_algebra[measurable]:
"a ∈ sets A ⟹ (λM. measure M a) ∈ borel_measurable (s_finite_measure_algebra A)"
unfolding measure_def by measurable
lemma s_finite_measure_algebra_measurableD:
assumes N: "N ∈ measurable M (s_finite_measure_algebra S)" and x: "x ∈ space M"
shows "space (N x) = space S"
and "sets (N x) = sets S"
and "measurable (N x) K = measurable S K"
and "measurable K (N x) = measurable K S"
using measurable_space[OF N x]
by (auto simp: space_s_finite_measure_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
context
fixes K M N assumes K: "K ∈ measurable M (s_finite_measure_algebra N)"
begin
lemma s_finite_measure_algebra_kernel: "a ∈ space M ⟹ s_finite_measure (K a)"
using measurable_space[OF K] by (simp add: space_s_finite_measure_algebra)
lemma s_finite_measure_algebra_sets_kernel: "a ∈ space M ⟹ sets (K a) = sets N"
using measurable_space[OF K] by (simp add: space_s_finite_measure_algebra)
lemma measurable_emeasure_kernel_s_finite_measure_algebra[measurable]:
"A ∈ sets N ⟹ (λa. emeasure (K a) A) ∈ borel_measurable M"
using measurable_compose[OF K measurable_emeasure_s_finite_measure_algebra] .
end
lemma measurable_s_finite_measure_algebra:
"(⋀a. a ∈ space M ⟹ s_finite_measure (K a)) ⟹
(⋀a. a ∈ space M ⟹ sets (K a) = sets N) ⟹
(⋀A. A ∈ sets N ⟹ (λa. emeasure (K a) A) ∈ borel_measurable M) ⟹
K ∈ measurable M (s_finite_measure_algebra N)"
by (auto intro!: measurable_Sup2 measurable_vimage_algebra2 simp: s_finite_measure_algebra_def)
definition bind_kernel :: "'a measure ⇒ ('a ⇒ 'b measure) ⇒ 'b measure" (infixl ‹⤜⇩k› 54) where
"bind_kernel M k = (if space M = {} then count_space {} else
let Y = k (SOME x. x ∈ space M) in
measure_of (space Y) (sets Y) (λB. ∫⇧+x. (k x B) ∂M))"
lemma bind_kernel_cong_All:
assumes "⋀x. x ∈ space M ⟹ f x = g x"
shows "M ⤜⇩k f = M ⤜⇩k g"
proof(cases "space M = {}")
case 1:False
have "(SOME x. x ∈ space M) ∈ space M"
by (rule someI_ex) (use 1 in blast)
with assms have [simp]:"f (SOME x. x ∈ space M) = g (SOME x. x ∈ space M)" by simp
have "(λB. ∫⇧+ x. emeasure (f x) B ∂M) = (λB. ∫⇧+ x. emeasure (g x) B ∂M)"
by standard (auto intro!: nn_integral_cong simp: assms)
thus ?thesis
by(auto simp: bind_kernel_def 1)
qed(simp add: bind_kernel_def)
lemma sets_bind_kernel:
assumes "⋀x. x ∈ space M ⟹ sets (k x) = sets N" "space M ≠ {}"
shows "sets (M ⤜⇩k k) = sets N"
proof -
have "sets (k (SOME x. x ∈ space M)) = sets N"
by(rule someI2_ex) (use assms in auto)
with sets_eq_imp_space_eq[OF this] show ?thesis
by(simp add: bind_kernel_def assms(2))
qed
subsection ‹ Measure Kernel ›
locale measure_kernel =
fixes X :: "'a measure" and Y :: "'b measure" and κ :: "'a ⇒ 'b measure"
assumes kernel_sets[measurable_cong]: "⋀x. x ∈ space X ⟹ sets (κ x) = sets Y"
and emeasure_measurable[measurable]: "⋀B. B ∈ sets Y ⟹ (λx. emeasure (κ x) B) ∈ borel_measurable X"
and Y_not_empty: "space X ≠ {} ⟹ space Y ≠ {}"
begin
lemma kernel_space :"⋀x. x ∈ space X ⟹ space (κ x) = space Y"
by (meson kernel_sets sets_eq_imp_space_eq)
lemma measure_measurable:
assumes "B ∈ sets Y"
shows "(λx. measure (κ x) B) ∈ borel_measurable X"
using emeasure_measurable[OF assms] by (simp add: Sigma_Algebra.measure_def)
lemma set_nn_integral_measure:
assumes [measurable_cong]: "sets μ = sets X" and [measurable]: "A ∈ sets X" "B ∈ sets Y"
defines "ν ≡ measure_of (space Y) (sets Y) (λB. ∫⇧+x∈A. (κ x B) ∂μ)"
shows "ν B = (∫⇧+x∈A. (κ x B) ∂μ)"
proof -
have nu_sets[measurable_cong]: "sets ν = sets Y"
by(simp add: ν_def)
have "positive (sets Y) (λB. ∫⇧+x∈A. (κ x B) ∂μ)"
by(simp add: positive_def)
moreover have "countably_additive (sets Y) (λB. ∫⇧+x∈A. (κ x B) ∂μ)"
unfolding countably_additive_def
proof safe
fix C :: "nat ⇒ _"
assume h:"range C ⊆ sets Y" "disjoint_family C"
thus "(∑i. ∫⇧+x∈A. (κ x) (C i)∂μ) = (∫⇧+x∈A. (κ x) (⋃ (range C))∂μ)"
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF assms(1)] kernel_sets suminf_emeasure nn_integral_suminf[symmetric])
qed
ultimately show ?thesis
using ν_def assms(3) emeasure_measure_of_sigma sets.sigma_algebra_axioms by blast
qed
corollary nn_integral_measure:
assumes "sets μ = sets X" "B ∈ sets Y"
defines "ν ≡ measure_of (space Y) (sets Y) (λB. ∫⇧+x. (κ x B) ∂μ)"
shows "ν B = (∫⇧+x. (κ x B) ∂μ)"
using set_nn_integral_measure[OF assms(1) sets.top assms(2)]
by(simp add: ν_def sets_eq_imp_space_eq[OF assms(1),symmetric])
lemma distr_measure_kernel:
assumes [measurable]:"f ∈ Y →⇩M Z"
shows "measure_kernel X Z (λx. distr (κ x) Z f)"
unfolding measure_kernel_def
proof safe
fix B
assume B[measurable]: "B ∈ sets Z"
show "(λx. emeasure (distr (κ x) Z f) B) ∈ borel_measurable X"
by(rule measurable_cong[where g= "(λx. κ x (f -` B ∩ space Y))",THEN iffD2]) (auto simp: emeasure_distr sets_eq_imp_space_eq[OF kernel_sets])
next
show "⋀x. space Z = {} ⟹ x ∈ space X ⟹ x ∈ {}"
by (metis Y_not_empty assms measurable_empty_iff)
qed auto
lemma measure_kernel_comp:
assumes [measurable]: "f ∈ W →⇩M X"
shows "measure_kernel W Y (λx. κ (f x))"
using measurable_space[OF assms] kernel_sets Y_not_empty
by(auto simp: measure_kernel_def)
lemma emeasure_bind_kernel:
assumes "sets μ = sets X" "B ∈ sets Y" "space X ≠ {}"
shows "(μ ⤜⇩k κ) B = (∫⇧+x. (κ x B) ∂μ)"
proof -
have "sets (κ (SOME x. x ∈ space μ)) = sets Y"
by(rule someI2_ex) (use assms(3) kernel_sets sets_eq_imp_space_eq[OF assms(1)] in auto)
with sets_eq_imp_space_eq[OF this] show ?thesis
by(simp add: bind_kernel_def sets_eq_imp_space_eq[OF assms(1) ]assms(3) nn_integral_measure[OF assms(1,2)])
qed
lemma measure_bind_kernel:
assumes [measurable_cong]:"sets μ = sets X" and [measurable]:"B ∈ sets Y" "space X ≠ {}" "AE x in μ. κ x B < ∞"
shows "measure (μ ⤜⇩k κ) B = (∫x. measure (κ x) B ∂μ)"
using assms(4) by(auto simp: emeasure_bind_kernel[OF assms(1-3)] measure_def integral_eq_nn_integral intro!: arg_cong[of _ _ enn2real] nn_integral_cong_AE)
lemma sets_bind_kernel:
assumes "space X ≠ {}" "sets μ = sets X"
shows "sets (μ ⤜⇩k κ) = sets Y"
using sets_bind_kernel[of μ κ, OF kernel_sets,simplified sets_eq_imp_space_eq[OF assms(2)]]
by(auto simp: assms(1))
lemma distr_bind_kernel:
assumes "space X ≠ {}" and [measurable_cong]:"sets μ = sets X" and [measurable]: "f ∈ Y →⇩M Z"
shows "distr (μ ⤜⇩k κ) Z f = μ ⤜⇩k (λx. distr (κ x) Z f)"
proof -
{
fix A
assume A[measurable]:"A ∈ sets Z"
have sets[measurable_cong]:"sets (μ ⤜⇩k κ) = sets Y"
by(rule sets_bind_kernel[OF assms(1,2)])
have "emeasure (distr (μ ⤜⇩k κ) Z f) A = emeasure (μ ⤜⇩k (λx. distr (κ x) Z f)) A" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. emeasure (κ x) (f -` A ∩ space Y) ∂μ)"
by(simp add: emeasure_distr sets_eq_imp_space_eq[OF sets] emeasure_bind_kernel[OF assms(2) _ assms(1)])
also have "... = (∫⇧+ x. emeasure (distr (κ x) Z f) A ∂μ)"
by(auto simp: emeasure_distr sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] intro!: nn_integral_cong)
also have "... = ?rhs"
by(simp add: measure_kernel.emeasure_bind_kernel[OF distr_measure_kernel[OF assms(3)] assms(2) _ assms(1)])
finally show ?thesis .
qed
}
thus ?thesis
by(auto intro!: measure_eqI simp: measure_kernel.sets_bind_kernel[OF distr_measure_kernel[OF assms(3)] assms(1,2)])
qed
lemma bind_kernel_distr:
assumes [measurable]: "f ∈ W →⇩M X" and "space W ≠ {}"
shows "distr W X f ⤜⇩k κ = W ⤜⇩k (λx. κ (f x))"
proof -
have X: "space X ≠ {}"
using measurable_space[OF assms(1)] assms(2) by auto
show ?thesis
by(rule measure_eqI, insert X) (auto simp: sets_bind_kernel[OF X] measure_kernel.sets_bind_kernel[OF measure_kernel_comp[OF assms(1)] assms(2) refl] emeasure_bind_kernel nn_integral_distr measure_kernel.emeasure_bind_kernel[OF measure_kernel_comp[OF assms(1)] refl _ assms(2)])
qed
lemma bind_kernel_return:
assumes "x ∈ space X"
shows "return X x ⤜⇩k κ = κ x"
proof -
have X: "space X ≠ {}"
using assms by auto
show ?thesis
by(rule measure_eqI) (auto simp: sets_bind_kernel[OF X sets_return] kernel_sets[OF assms] emeasure_bind_kernel[OF sets_return,simplified,OF _ X] nn_integral_return[OF assms])
qed
lemma kernel_nn_integral_measurable:
assumes "f ∈ borel_measurable Y"
shows "(λx. ∫⇧+ y. f y ∂(κ x)) ∈ borel_measurable X"
using assms
proof induction
case (cong f g)
then show ?case
by(auto intro!: measurable_cong[where f="λx. ∫⇧+ y. f y ∂(κ x)" and g= "λx. ∫⇧+ y. g y ∂(κ x)",THEN iffD2] nn_integral_cong simp: sets_eq_imp_space_eq[OF kernel_sets])
next
case (set A)
then show ?case
by(auto intro!: measurable_cong[where f="λx. integral⇧N (κ x) (indicator A)" and g="λx. κ x A",THEN iffD2])
next
case (mult u c)
then show ?case
by(auto intro!: measurable_cong[where f="λx. ∫⇧+ y. c * u y ∂κ x" and g="λx. c * ∫⇧+ y. u y ∂κ x",THEN iffD2] simp: nn_integral_cmult)
next
case (add u v)
then show ?case
by(auto intro!: measurable_cong[where f="λx. ∫⇧+ y. v y + u y ∂κ x" and g="λx. (∫⇧+ y. v y ∂κ x) + (∫⇧+ y. u y ∂κ x)",THEN iffD2] simp: nn_integral_add)
next
case (seq U)
then show ?case
by(intro measurable_cong[where f="λx. integral⇧N (κ x) (⨆ range U)" and g="λx. ⨆i. integral⇧N (κ x) (U i)",THEN iffD2])
(auto simp: nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[symmetric]])
qed
lemma bind_kernel_measure_kernel:
assumes "measure_kernel Y Z k'"
shows "measure_kernel X Z (λx. κ x ⤜⇩k k')"
proof(cases "space X = {}")
case True
then show ?thesis
by(auto simp: measure_kernel_def measurable_def)
next
case X:False
then have Y: "space Y ≠ {}"
by(simp add: Y_not_empty)
interpret k': measure_kernel Y Z k' by fact
show ?thesis
proof
fix B
assume "B ∈ sets Z"
with k'.emeasure_bind_kernel[OF kernel_sets,of _ B] show "(λx. emeasure (κ x ⤜⇩k k') B) ∈ borel_measurable X"
by(auto intro!: measurable_cong[where f="λx. emeasure (κ x ⤜⇩k k') B" and g="λx. ∫⇧+ y. emeasure (k' y) B ∂κ x",THEN iffD2] kernel_nn_integral_measurable simp: sets_eq_imp_space_eq[OF kernel_sets] Y)
qed(use k'.Y_not_empty Y k'.sets_bind_kernel[OF Y kernel_sets] in auto)
qed
lemma restrict_measure_kernel: "measure_kernel (restrict_space X A) Y κ"
proof
fix B
assume "B ∈ sets Y"
from emeasure_measurable[OF this] show "(λx. emeasure (κ x) B) ∈ borel_measurable (restrict_space X A)"
using measurable_restrict_space1 by blast
qed(insert Y_not_empty,auto simp add: space_restrict_space kernel_sets)
end
lemma measure_kernel_cong_sets:
assumes "sets X = sets X'" "sets Y = sets Y'"
shows "measure_kernel X Y = measure_kernel X' Y'"
by standard (simp add: measure_kernel_def measurable_cong_sets[OF assms(1) refl] sets_eq_imp_space_eq[OF assms(1)] assms(2) sets_eq_imp_space_eq[OF assms(2)])
lemma measure_kernel_pair_countble1:
assumes "countable A" "⋀i. i ∈ A ⟹ measure_kernel X Y (λx. k (i,x))"
shows "measure_kernel (count_space A ⨂⇩M X) Y k"
using assms by(auto simp: measure_kernel_def space_pair_measure intro!: measurable_pair_measure_countable1)
lemma measure_kernel_empty_trivial:
assumes "space X = {}"
shows "measure_kernel X Y k"
using assms by(auto simp: measure_kernel_def measurable_def)
subsection ‹ Finite Kernel ›
locale finite_kernel = measure_kernel +
assumes finite_measure_spaces: "∃r<∞. ∀x∈ space X. κ x (space Y) < r"
begin
lemma finite_measures:
assumes "x ∈ space X"
shows "finite_measure (κ x)"
proof-
obtain r where "κ x (space Y) < r"
using finite_measure_spaces assms by metis
then show ?thesis
by(auto intro!: finite_measureI simp: sets_eq_imp_space_eq[OF kernel_sets[OF assms]])
qed
end
lemma finite_kernel_empty_trivial: "space X = {} ⟹ finite_kernel X Y f"
by(auto simp: finite_kernel_def finite_kernel_axioms_def measure_kernel_empty_trivial intro!: exI[where x=1])
lemma finite_kernel_cong_sets:
assumes "sets X = sets X'" "sets Y = sets Y'"
shows "finite_kernel X Y = finite_kernel X' Y'"
by standard (auto simp: measure_kernel_cong_sets[OF assms] finite_kernel_def finite_kernel_axioms_def sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF assms(2)])
subsection ‹ Sub-Probability Kernel›
locale subprob_kernel = measure_kernel +
assumes subprob_spaces: "⋀x. x ∈ space X ⟹ subprob_space (κ x)"
begin
lemma subprob_space:
"⋀x. x ∈ space X ⟹ κ x (space Y) ≤ 1"
by (simp add: subprob_space.subprob_emeasure_le_1 subprob_spaces)
lemma subprob_measurable[measurable]:
"κ ∈ X →⇩M subprob_algebra Y"
by(auto intro!: measurable_subprob_algebra_generated[OF sets.sigma_sets_eq[symmetric] sets.Int_stable sets.space_closed] simp: subprob_spaces kernel_sets emeasure_measurable)
lemma finite_kernel: "finite_kernel X Y κ"
by(auto simp: finite_kernel_def finite_kernel_axioms_def intro!: measure_kernel_axioms exI[where x=2] order.strict_trans1[OF subprob_space.subprob_emeasure_le_1[OF subprob_spaces]])
sublocale finite_kernel
by (rule finite_kernel)
end
lemma subprob_kernel_def':
"subprob_kernel X Y κ ⟷ κ ∈ X →⇩M subprob_algebra Y"
by(auto simp: subprob_kernel.subprob_measurable subprob_kernel_def subprob_kernel_axioms_def measure_kernel_def measurable_subprob_algebra measurable_empty_iff space_subprob_algebra_empty_iff)
(auto simp: subprob_measurableD(2) subprob_space_kernel)
lemmas subprob_kernelI = measurable_subprob_algebra[simplified subprob_kernel_def'[symmetric]]
lemma subprob_kernel_cong_sets:
assumes "sets X = sets X'" "sets Y = sets Y'"
shows "subprob_kernel X Y = subprob_kernel X' Y'"
by standard (auto simp: subprob_kernel_def' subprob_algebra_cong[OF assms(2)] measurable_cong_sets[OF assms(1) refl])
lemma subprob_kernel_empty_trivial:
assumes "space X = {}"
shows "subprob_kernel X Y k"
using assms by(auto simp: subprob_kernel_def subprob_kernel_axioms_def intro!: measure_kernel_empty_trivial)
lemma bind_kernel_bind:
assumes "f ∈ M →⇩M subprob_algebra N"
shows "M ⤜⇩k f = M ⤜ f"
proof(cases "space M = {}")
case True
then show ?thesis
by(simp add: bind_kernel_def bind_def)
next
case h:False
interpret subprob_kernel M N f
using assms(1) by(simp add: subprob_kernel_def')
show ?thesis
by(rule measure_eqI,insert sets_kernel[OF assms]) (auto simp: h sets_bind_kernel emeasure_bind_kernel[OF refl _ h] emeasure_bind[OF h assms])
qed
lemma(in measure_kernel) subprob_kernel_sum:
assumes "⋀x. x ∈ space X ⟹ finite_measure (κ x)"
obtains ki where "⋀i. subprob_kernel X Y (ki i)" "⋀A x. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
proof -
obtain u where u: "⋀x. x ∈ space X ⟹ u x < ∞" "⋀x. x ∈ space X ⟹ u x = κ x (space Y)"
using finite_measure.emeasure_finite[OF assms]
by (simp add: top.not_eq_extremum)
have [measurable]: "u ∈ borel_measurable X"
by(simp cong: measurable_cong add: u(2))
define ki where "ki ≡ (λi x. if i < nat ⌈enn2real (u x)⌉ then scale_measure (1 / ennreal (real_of_int ⌈enn2real (u x)⌉)) (κ x) else (sigma (space Y) (sets Y)))"
have 1:"⋀i x. x ∈ space X ⟹ sets (ki i x) = sets Y"
by(auto simp: ki_def kernel_sets)
have "subprob_kernel X Y (ki i)" for i
proof -
{
fix i B
assume [measurable]: "B ∈ sets Y"
have "(λx. emeasure (ki i x) B) = (λx. if i < nat ⌈enn2real (u x)⌉ then (1 / ennreal (real_of_int ⌈enn2real (u x)⌉)) * emeasure (κ x) B else 0)"
by(auto simp: ki_def emeasure_sigma)
also have "... ∈ borel_measurable X"
by simp
finally have "(λx. emeasure (ki i x) B) ∈ borel_measurable X" .
}
moreover {
fix i x
assume x:"x ∈ space X"
have "emeasure (ki i x) (space Y) ≤ 1"
by(cases "u x = 0",auto simp: ki_def emeasure_sigma u(2)[OF x,symmetric]) (metis u(1)[OF x,simplified] divide_ennreal_def divide_le_posI_ennreal enn2real_le le_of_int_ceiling mult.commute mult.right_neutral not_gr_zero order.strict_iff_not)
hence "subprob_space (ki i x)"
using x Y_not_empty by(fastforce intro!: subprob_spaceI simp: sets_eq_imp_space_eq[OF 1[OF x]])
}
ultimately show ?thesis
by(auto simp: subprob_kernel_def measure_kernel_def 1 Y_not_empty subprob_kernel_axioms_def)
qed
moreover have "κ x A = (∑i. ki i x A)" if x:"x ∈ space X" for x A
proof (cases "A ∈ sets Y")
case A[measurable]:True
have "emeasure (κ x) A = (∑i<nat ⌈enn2real (u x)⌉. emeasure (ki i x) A)"
proof(cases "u x = 0")
case True
then show ?thesis
using u(2)[OF that] by simp (metis A emeasure_eq_0 kernel_sets sets.sets_into_space sets.top x)
next
case u0:False
hence "real_of_int ⌈enn2real (u x)⌉ > 0"
by (metis enn2real_nonneg ennreal_0 ennreal_enn2real_if infinity_ennreal_def linorder_not_le nat_0_iff nle_le of_int_le_0_iff of_nat_eq_0_iff real_nat_ceiling_ge u(1) x)
with u(1)[OF x] have "of_nat (nat ⌈enn2real (u x)⌉) / ennreal (real_of_int ⌈enn2real (u x)⌉) = 1"
by(simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
thus ?thesis
by(simp add: ki_def ennreal_divide_times[symmetric] mult.assoc[symmetric])
qed
then show ?thesis
by(auto simp: suminf_offset[of "λi. emeasure (ki i x) A" "nat ⌈enn2real (u x)⌉"]) (simp add: ki_def emeasure_sigma)
next
case False
then show ?thesis
using kernel_sets[OF x] 1[OF x]
by(simp add: emeasure_notin_sets)
qed
ultimately show ?thesis
using that by blast
qed
subsection ‹ Probability Kernel ›
locale prob_kernel = measure_kernel +
assumes prob_spaces: "⋀x. x ∈ space X ⟹ prob_space (κ x)"
begin
lemma prob_space:
"⋀x. x ∈ space X ⟹ κ x (space Y) = 1"
using kernel_space prob_space.emeasure_space_1 prob_spaces by fastforce
lemma prob_measurable[measurable]:
"κ ∈ X →⇩M prob_algebra Y"
by(auto intro!: measurable_prob_algebra_generated[OF sets.sigma_sets_eq[symmetric] sets.Int_stable sets.space_closed] simp: prob_spaces kernel_sets emeasure_measurable)
lemma subprob_kernel: "subprob_kernel X Y κ"
by (simp add: measurable_prob_algebraD subprob_kernel_def')
sublocale subprob_kernel
by (simp add: subprob_kernel)
lemma restrict_probability_kernel:
"prob_kernel (restrict_space X A) Y κ"
by(auto simp: prob_kernel_def restrict_measure_kernel prob_kernel_axioms_def space_restrict_space prob_spaces)
end
lemma prob_kernel_def':
"prob_kernel X Y κ ⟷ κ ∈ X →⇩M prob_algebra Y"
proof
assume h:"κ ∈ X →⇩M prob_algebra Y"
show "prob_kernel X Y κ"
using subprob_measurableD(2)[OF measurable_prob_algebraD[OF h]] measurable_space[OF h] measurable_emeasure_kernel[OF measurable_prob_algebraD[OF h]]
by(auto simp: prob_kernel_def measure_kernel_def prob_kernel_axioms_def space_prob_algebra ) (metis prob_space.not_empty sets_eq_imp_space_eq)
qed(auto simp: prob_kernel.prob_measurable prob_kernel_def prob_kernel_axioms_def measure_kernel_def)
lemma bind_kernel_return'':
assumes "sets M = sets N"
shows "M ⤜⇩k return N = M"
proof(cases "space M = {}")
case True
then show ?thesis
by(simp add: bind_kernel_def space_empty[symmetric])
next
case False
then have 1: "space N ≠ {}"
by(simp add: sets_eq_imp_space_eq[OF assms])
interpret prob_kernel N N "return N"
by(simp add: prob_kernel_def')
show ?thesis
by(rule measure_eqI) (auto simp: emeasure_bind_kernel[OF assms _ 1] sets_bind_kernel[OF 1 assms] assms)
qed
subsection‹ S-Finite Kernel ›
locale s_finite_kernel = measure_kernel +
assumes s_finite_kernel_sum: "∃ki. (∀i. finite_kernel X Y (ki i) ∧ (∀x∈space X. ∀A∈sets Y. κ x A = (∑i. ki i x A)))"
lemma s_finite_kernel_subI:
assumes "⋀x. x ∈ space X ⟹ sets (κ x) = sets Y" "⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ A ∈ sets Y ⟹ emeasure (κ x) A = (∑i. ki i x A)"
shows "s_finite_kernel X Y κ"
proof -
interpret measure_kernel X Y κ
proof
show "B ∈ sets Y ⟹ (λx. emeasure (κ x) B) ∈ borel_measurable X" for B
using assms(2) by(simp add: assms(3) subprob_kernel_def' cong: measurable_cong)
next
show "space X ≠ {} ⟹ space Y ≠ {}"
using assms(2)[of 0] by(auto simp: subprob_kernel_def measure_kernel_def)
qed fact
show ?thesis
by (auto simp: s_finite_kernel_def measure_kernel_axioms s_finite_kernel_axioms_def assms(2,3) intro!: exI[where x=ki] subprob_kernel.finite_kernel)
qed
context s_finite_kernel
begin
lemma s_finite_kernels_fin:
obtains ki where "⋀i. finite_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
proof -
obtain ki where ki:"⋀i. finite_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ A ∈ sets Y ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernel_sum)
hence "κ x A = (∑i. ki i x A)" if "x ∈ space X " for x A
by(cases "A ∈ sets Y", insert that kernel_sets[OF that]) (auto simp: finite_kernel_def measure_kernel_def emeasure_notin_sets)
with ki show ?thesis
using that by auto
qed
lemma s_finite_kernels:
obtains ki where "⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
proof -
obtain ki where ki:"⋀i. finite_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernels_fin)
have "∃kij. (∀j. subprob_kernel X Y (kij j)) ∧ (∀x A. x ∈ space X ⟶ ki i x A = (∑j. kij j x A))" for i
using measure_kernel.subprob_kernel_sum[of X Y "ki i", OF _ finite_kernel.finite_measures[OF ki(1)[of i]]] ki(1)[of i] by(metis finite_kernel_def)
then obtain kij where kij: "⋀i j. subprob_kernel X Y (kij i j)" "⋀x A i. x ∈ space X ⟹ ki i x A = (∑j. kij i j x A)"
by metis
have "⋀i. subprob_kernel X Y (case_prod kij (prod_decode i))"
using kij(1) by(auto simp: split_beta)
moreover have "x ∈ space X ⟹ κ x A = (∑i. case_prod kij (prod_decode i) x A)" for x A
using suminf_ennreal_2dimen[of "λi. ki i x A" "λ(i,j). kij i j x A"]
by(auto simp: ki(2) kij(2) split_beta')
ultimately show ?thesis
using that by fastforce
qed
lemma image_s_finite_measure:
assumes "x ∈ space X"
shows "s_finite_measure (κ x)"
proof -
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernels)
show ?thesis
using ki(1)[simplified subprob_kernel_def'] measurable_space[OF ki(1)[simplified subprob_kernel_def'] assms]
by(auto intro!: s_finite_measureI[where Mi="λi. ki i x"] subprob_space.axioms(1) simp: kernel_sets[OF assms] space_subprob_algebra ki(2)[OF assms])
qed
corollary kernel_measurable_s_finite[measurable]:"κ ∈ X →⇩M s_finite_measure_algebra Y"
by(auto intro!: measurable_s_finite_measure_algebra simp: kernel_sets image_s_finite_measure)
lemma comp_measurable:
assumes f[measurable]:"f ∈ M →⇩M X"
shows "s_finite_kernel M Y (λx. κ (f x))"
proof -
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernels)
show ?thesis
using ki(1) measurable_space[OF f] by(auto intro!: s_finite_kernel_subI[where ki="λi x. ki i (f x)"] simp: subprob_kernel_def' ki(2) kernel_sets)
qed
lemma distr_s_finite_kernel:
assumes f[measurable]: "f ∈ Y →⇩M Z"
shows "s_finite_kernel X Z (λx. distr (κ x) Z f)"
proof -
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernels)
hence 1:"x ∈ space X ⟹ space (ki i x) = space Y" for x i
by(auto simp: subprob_kernel_def' intro!: subprob_measurableD(1)[of _ X Y])
have [measurable]:"B ∈ sets Z ⟹ (λx. emeasure (distr (κ x) Z f) B) ∈ borel_measurable X" for B
by(rule measurable_cong[where g="λx. κ x (f -` B ∩ space Y)", THEN iffD2]) (auto simp: emeasure_distr sets_eq_imp_space_eq[OF kernel_sets])
show ?thesis
using ki(1) measurable_distr[OF f] by(auto intro!: s_finite_kernel_subI[where ki="λi x. distr (ki i x) Z f"] simp: subprob_kernel_def' emeasure_distr ki(2) sets_eq_imp_space_eq[OF kernel_sets] 1)
qed
lemma comp_s_finite_measure:
assumes "s_finite_measure μ" and [measurable_cong]: "sets μ = sets X"
shows "s_finite_measure (μ ⤜⇩k κ)"
proof(cases "space X = {}")
case 1:True
show ?thesis
by(auto simp: sets_eq_imp_space_eq[OF assms(2)] 1 bind_kernel_def intro!: finite_measure.s_finite_measure_finite_measure finite_measureI)
next
case 0:False
then have 1: "space μ ≠ {}"
by(simp add: sets_eq_imp_space_eq[OF assms(2)])
have 2: "sets (κ (SOME x. x ∈ space μ)) = sets Y"
by(rule someI2_ex, insert 1 kernel_sets) (auto simp: sets_eq_imp_space_eq[OF assms(2)])
have sets_bind[measurable_cong]: "sets (μ ⤜⇩k κ) = sets Y"
by(simp add: bind_kernel_def 1 sets_eq_imp_space_eq[OF 2] 2)
obtain μi where mui[measurable_cong]: "⋀i. sets (μi i) = sets X" "⋀i. (μi i) (space X) ≤ 1" "⋀A. μ A = (∑i. μi i A)"
using s_finite_measure.finite_measures[OF assms(1)] assms(2) sets_eq_imp_space_eq[OF assms(2)] by metis
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by(metis s_finite_kernels)
define Mi where "Mi ≡ (λn. (λ(i,j). measure_of (space Y) (sets Y) (λA. ∫⇧+x. (ki i x A) ∂(μi j))) (prod_decode n))"
have emeasure:"(μ ⤜⇩k κ) A = (∑i. (Mi i) A)" (is "?lhs = ?rhs") if "A ∈ sets Y" for A
proof -
have "?lhs = (∫⇧+x. (κ x A) ∂μ)"
by(simp add: emeasure_bind_kernel[OF assms(2) that 0])
also have "... = (∫⇧+x. (∑i. (ki i x A)) ∂μ)"
by(auto intro!: nn_integral_cong simp: ki sets_eq_imp_space_eq[OF assms(2)])
also have "... = (∑i. ∫⇧+x. (ki i x A) ∂μ)"
by(auto intro!: nn_integral_suminf) (metis ki(1) assms(2) measurable_cong_sets measure_kernel.emeasure_measurable subprob_kernel_def that)
also have "... = ?rhs"
unfolding Mi_def
proof(rule suminf_ennreal_2dimen[symmetric])
fix m
interpret kim: subprob_kernel X Y "ki m"
by(simp add: ki)
show "(∫⇧+ x. (ki m x) A ∂μ) = (∑n. emeasure (case (m, n) of (i, j) ⇒ measure_of (space Y) (sets Y) (λA. ∫⇧+ x. emeasure (ki i x) A ∂μi j)) A)"
using kim.emeasure_measurable[OF that] by(simp add: kim.nn_integral_measure[OF mui(1) that] nn_integral_measure_suminf[OF mui(1)[simplified assms(2)[symmetric]] mui(3)])
qed
finally show ?thesis .
qed
have fin:"finite_measure (Mi i)" for i
proof(rule prod.exhaust[where y="prod_decode i"])
fix j1 j2
interpret kij: subprob_kernel X Y "ki j1"
by(simp add: ki)
assume pd:"prod_decode i = (j1, j2)"
have "Mi i (space (Mi i)) = (∫⇧+x. (ki j1 x (space Y)) ∂μi j2)"
by(auto simp: Mi_def pd kij.nn_integral_measure[OF mui(1) sets.top])
also have "... ≤ (∫⇧+x. 1 ∂μi j2)"
by(intro nn_integral_mono) (metis kij.subprob_space mui(1) sets_eq_imp_space_eq)
also have "... ≤ 1"
using mui by (simp add: sets_eq_imp_space_eq[OF mui(1)])
finally show "finite_measure (Mi i)"
by (metis ennreal_one_less_top finite_measureI infinity_ennreal_def less_le_not_le)
qed
have 3: "sets (Mi i) = sets (μ ⤜⇩k κ)" for i
by(simp add: Mi_def split_beta sets_bind)
show "s_finite_measure (μ ⤜⇩k κ)"
using emeasure fin 3 by (auto intro!: exI[where x=Mi] simp: s_finite_measure_def sets_bind)
qed
end
lemma s_finite_kernel_empty_trivial:
assumes "space X = {}"
shows "s_finite_kernel X Y k"
using assms by(auto simp: s_finite_kernel_def s_finite_kernel_axioms_def intro!: measure_kernel_empty_trivial finite_kernel_empty_trivial)
lemma s_finite_kernel_def': "s_finite_kernel X Y κ ⟷ ((∀x. x ∈ space X ⟶ sets (κ x) = sets Y) ∧ (∃ki. (∀i. subprob_kernel X Y (ki i)) ∧ (∀x A. x ∈ space X ⟶ A ∈ sets Y ⟶ emeasure (κ x) A = (∑i. ki i x A))))" (is "?l ⟷ ?r")
proof
assume ?l
then interpret s_finite_kernel X Y κ .
from s_finite_kernels obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ emeasure (κ x) A = (∑i. emeasure (ki i x) A)"
by metis
thus ?r
by(auto simp: kernel_sets)
qed(auto intro!: s_finite_kernel_subI)
lemma(in finite_kernel) s_finite_kernel_finite_kernel: "s_finite_kernel X Y κ"
proof
consider "space X = {}" | "space X ≠ {}" by auto
then show "∃ki. ∀i. finite_kernel X Y (ki i) ∧ (∀x∈space X. ∀A∈sets Y. (κ x) A = (∑i. (ki i x) A))"
proof cases
case 1
then show ?thesis
by(auto simp: finite_kernel_def measure_kernel_def finite_kernel_axioms_def measurable_def intro!: exI[where x=0])
next
case 2
then have y:"space Y ≠ {}" by(simp add: Y_not_empty)
define ki where "ki i ≡ case i of 0 ⇒ κ | Suc _ ⇒ (λ_. sigma (space Y) (sets Y))" for i
have "finite_kernel X Y (ki i)" for i
by (cases i, auto simp: ki_def finite_kernel_axioms) (auto simp: emeasure_sigma finite_kernel_def measure_kernel_def finite_kernel_axioms_def y intro!: finite_measureI exI[where x=1])
moreover have "(κ x) A = (∑i. (ki i x) A)" for x A
by(simp add: suminf_offset[where i="Suc 0" and f="λi. ki i x A",simplified],simp add: ki_def emeasure_sigma)
ultimately show ?thesis by auto
qed
qed
lemmas(in subprob_kernel) s_finite_kernel_subprob_kernel = s_finite_kernel_finite_kernel
lemmas(in prob_kernel) s_finite_kernel_prob_kernel = s_finite_kernel_subprob_kernel
sublocale finite_kernel ⊆ s_finite_kernel
by(rule s_finite_kernel_finite_kernel)
lemma s_finite_kernel_cong_sets:
assumes "sets X = sets X'" "sets Y = sets Y'"
shows "s_finite_kernel X Y = s_finite_kernel X' Y'"
by standard (simp add: s_finite_kernel_def measurable_cong_sets[OF assms(1) refl] sets_eq_imp_space_eq[OF assms(1)] assms(2) measure_kernel_cong_sets[OF assms] s_finite_kernel_axioms_def finite_kernel_cong_sets[OF assms])
lemma(in s_finite_kernel) s_finite_kernel_cong:
assumes "⋀x. x ∈ space X ⟹ κ x = g x"
shows "s_finite_kernel X Y g"
using assms s_finite_kernel_axioms by(auto simp: s_finite_kernel_def s_finite_kernel_axioms_def measure_kernel_def cong: measurable_cong)
lemma(in s_finite_measure) s_finite_kernel_const:
assumes "space M ≠ {}"
shows "s_finite_kernel X M (λx. M)"
proof
obtain Mi where Mi:"⋀i. sets (Mi i) = sets M" "⋀i. (Mi i) (space M) ≤ 1" "⋀A. M A = (∑i. Mi i A)"
by(metis finite_measures)
hence "⋀i. subprob_kernel X M (λx. Mi i)"
by(auto simp: subprob_kernel_def' space_subprob_algebra sets_eq_imp_space_eq[OF Mi(1)] assms intro!:measurable_const subprob_spaceI)
thus "∃ki. ∀i. finite_kernel X M (ki i) ∧ (∀x∈space X. ∀A∈sets M. M A = (∑i. (ki i x) A))"
by(auto intro!: exI[where x="λi x. Mi i"] Mi(3) subprob_kernel.finite_kernel)
qed (auto simp: assms)
lemma s_finite_kernel_pair_countble1:
assumes "countable A" "⋀i. i ∈ A ⟹ s_finite_kernel X Y (λx. k (i,x))"
shows "s_finite_kernel (count_space A ⨂⇩M X) Y k"
proof -
have "∃ki. (∀j. subprob_kernel X Y (ki j)) ∧ (∀x B. x ∈ space X ⟶ B ∈ sets Y ⟶ k (i,x) B = (∑j. ki j x B))" if "i ∈ A" for i
using s_finite_kernel.s_finite_kernels[OF assms(2)[OF that]] by metis
then obtain ki where ki:"⋀i j. i ∈ A ⟹ subprob_kernel X Y (ki i j)" "⋀i x B. i ∈ A ⟹ x ∈ space X ⟹ B ∈ sets Y ⟹ k (i,x) B = (∑j. ki i j x B)"
by metis
then show ?thesis
using assms(2) by(auto simp: s_finite_kernel_def' measure_kernel_pair_countble1[OF assms(1)] subprob_kernel_def' space_pair_measure intro!: exI[where x="λj (i,x). ki i j x"] measurable_pair_measure_countable1 assms(1))
qed
lemma s_finite_kernel_s_finite_kernel:
assumes "⋀i. s_finite_kernel X Y (ki i)" "⋀x. x ∈ space X ⟹ sets (k x) = sets Y" "⋀x A. x ∈ space X ⟹ A ∈ sets Y ⟹ emeasure (k x) A = (∑i. (ki i) x A)"
shows "s_finite_kernel X Y k"
proof -
have "∃kij. (∀j. subprob_kernel X Y (kij j)) ∧ (∀x A. x ∈ space X ⟶ ki i x A = (∑j. kij j x A))" for i
using s_finite_kernel.s_finite_kernels[OF assms(1)[of i]] by metis
then obtain kij where kij:"⋀i j. subprob_kernel X Y (kij i j)" "⋀i x A. x ∈ space X ⟹ ki i x A = (∑j. kij i j x A)"
by metis
define ki' where "ki' ≡ (λn. case_prod kij (prod_decode n))"
have emeasure_sumk':"emeasure (k x) A = (∑i. emeasure (ki' i x) A)" if x:"x ∈ space X" and A: "A ∈ sets Y" for x A
by(auto simp: assms(3)[OF that] kij(2)[OF x] ki'_def intro!: suminf_ennreal_2dimen[symmetric])
have "subprob_kernel X Y (ki' i)" for i
using kij(1) by(auto simp: ki'_def split_beta')
thus ?thesis
by(auto simp: s_finite_kernel_def' measure_kernel_def assms(2) s_finite_kernel_axioms_def emeasure_sumk' intro!: exI[where x=ki'])
qed
lemma s_finite_kernel_finite_sumI:
assumes [measurable_cong]: "⋀x. x ∈ space X ⟹ sets (κ x) = sets Y"
and "⋀i. i ∈ I ⟹ subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ A ∈ sets Y ⟹ emeasure (κ x) A = (∑i∈I. ki i x A)" "finite I" "I ≠ {}"
shows "s_finite_kernel X Y κ"
proof -
consider "space X = {}" | "space X ≠ {}" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(rule s_finite_kernel_empty_trivial)
next
case 2
then have Y:"space Y ≠ {}"
using assms measure_kernel.Y_not_empty by (fastforce simp: subprob_kernel_def)
define ki' where "ki' ≡ (λi x. if i < card I then ki (from_nat_into I i) x else null_measure Y)"
have [simp]:"subprob_kernel X Y (ki' i)" for i
by(cases "i < card I") (simp add: ki'_def from_nat_into assms, auto simp: ki'_def subprob_kernel_def measure_kernel_def subprob_kernel_axioms_def Y intro!: subprob_spaceI)
have [simp]: "(∑i. emeasure (ki' i x) A) = (∑i∈I. ki i x A)" for x A
using suminf_finite[of "{..<card I}" "λi. (if i < card I then ki (from_nat_into I i) x else null_measure Y) A"]
by(auto simp: sum.reindex_bij_betw[OF bij_betw_from_nat_into_finite[OF assms(4)],symmetric] ki'_def)
have [measurable]:"B ∈ sets Y ⟹ (λx. emeasure (κ x) B) ∈ borel_measurable X" for B
using assms(2) by(auto simp: assms(3) subprob_kernel_def' cong: measurable_cong)
show ?thesis
by (auto simp: s_finite_kernel_def' intro!: exI[where x=ki'] assms)
qed
qed
text ‹ Each kernel does not need to be bounded by a uniform upper-bound in the definition of @{term s_finite_kernel} ›
lemma s_finite_kernel_finite_bounded_sum:
assumes [measurable_cong]: "⋀x. x ∈ space X ⟹ sets (κ x) = sets Y"
and "⋀i. measure_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ A ∈ sets Y ⟹ κ x A = (∑i. ki i x A)" "⋀i x. x ∈ space X ⟹ ki i x (space Y) < ∞"
shows "s_finite_kernel X Y κ"
proof(cases "space X = {}")
case True
then show ?thesis
by(simp add: s_finite_kernel_empty_trivial)
next
case X:False
then have Y: "space Y ≠ {}"
using assms(2)[of 0] by(simp add: measure_kernel_def)
show ?thesis
proof(rule s_finite_kernel_s_finite_kernel[where ki=ki,OF _ assms(1) assms(3)])
fix i
interpret m: measure_kernel X Y "ki i" by fact
define kij where "kij ≡ (λ(j :: nat) x. if j < nat ⌈enn2real (ki i x (space Y))⌉ then scale_measure (1 / ennreal ⌈enn2real (ki i x (space Y))⌉) (ki i x) else sigma (space Y) (sets Y))"
have sets_kij: "sets (kij j x) = sets Y" if "x ∈ space X" for j x
by(auto simp: m.kernel_sets[OF that] kij_def)
have emeasure_kij: "ki i x A = (∑j. kij j x A)" if "x ∈ space X" "A ∈ sets Y" for x A
proof -
have "(∑j. kij j x A) = (∑j< nat ⌈enn2real (ki i x (space Y))⌉. scale_measure (1 / ennreal ⌈enn2real (ki i x (space Y))⌉) (ki i x) A)"
by(simp add: suminf_offset[where i="nat ⌈enn2real (ki i x (space Y))⌉" and f="λj. kij j x A"], simp add: kij_def emeasure_sigma)
also have "... = ki i x A"
proof(cases "nat ⌈enn2real (ki i x (space Y))⌉")
case 0
then show ?thesis
by simp (metis assms(4) emeasure_eq_0 enn2real_le ennreal_0 infinity_ennreal_def le_zero_eq linorder_not_le m.kernel_space nle_le sets.sets_into_space sets.top that)
next
case (Suc n')
then have "ennreal (real_of_int ⌈enn2real (emeasure (ki i x) (space Y))⌉) > 0"
using ennreal_less_zero_iff by fastforce
with assms(4)[OF that(1),of i] have [simp]: "of_nat (nat ⌈enn2real (emeasure (ki i x) (space Y))⌉) / ennreal (real_of_int ⌈enn2real (emeasure (ki i x) (space Y))⌉) = 1"
by (simp add: ennreal_eq_0_iff ennreal_of_nat_eq_real_of_nat)
show ?thesis
by(simp add: mult.assoc[symmetric] ennreal_times_divide)
qed
finally show ?thesis by simp
qed
have sk: "subprob_kernel X Y (kij j)" for j
proof -
{
fix B
assume [measurable]:"B ∈ sets Y"
have "emeasure (kij j x) B = (if j < nat ⌈enn2real (ki i x (space Y))⌉ then (ki i x) B / ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉) else 0)" if "x ∈ space X" for x
by(auto simp: kij_def emeasure_sigma divide_ennreal_def mult.commute)
hence " (λx. emeasure (kij j x) B) ∈ borel_measurable X"
by(auto simp: kij_def cong: measurable_cong)
}
moreover {
fix x
assume x:"x ∈ space X"
have "subprob_space (kij j x)"
proof -
have "emeasure (kij j x) (space Y) ≤ 1"
proof -
{
assume 1:"j < nat ⌈enn2real (emeasure (ki i x) (space Y))⌉"
then have "emeasure (ki i x) (space Y) > 0"
by (metis ceiling_zero enn2real_0 nat_zero_as_int not_gr_zero not_less_zero)
with assms(4)[OF x] have [simp]:"emeasure (ki i x) (space Y) / emeasure (ki i x) (space Y) = 1"
by simp
have [simp]:"emeasure (ki i x) (space Y) / ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉) ≤ 1"
proof(rule order.trans[where b="emeasure (ki i x) (space Y) / ki i x (space Y)",OF divide_le_posI_ennreal])
show "0 < ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉)"
using 1 assms(4)[OF x] enn2real_positive_iff top.not_eq_extremum by fastforce
next
have 1:"ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉) ≥ ki i x (space Y)"
using assms(4)[OF x] enn2real_le by (simp add: linorder_neq_iff)
have "ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉) / ki i x (space Y) ≥ 1"
by(rule order.trans[OF _ divide_right_mono_ennreal[OF 1,of "ki i x (space Y)"]]) simp
thus "emeasure (ki i x) (space Y) ≤ ennreal (real_of_int ⌈enn2real (ki i x (space Y))⌉) * (emeasure (ki i x) (space Y) / ki i x (space Y))"
by (simp add: "1")
qed simp
have "1 / ennreal (real_of_int ⌈enn2real (emeasure (ki i x) (space Y))⌉) * emeasure (ki i x) (space Y) ≤ 1"
by (simp add: ennreal_divide_times)
}
thus ?thesis
by(auto simp: kij_def emeasure_sigma)
qed
thus ?thesis
by(auto intro!: subprob_spaceI simp: sets_eq_imp_space_eq[OF sets_kij[OF x,of j]] Y)
qed
}
ultimately show ?thesis
by(auto simp: subprob_kernel_def measure_kernel_def sets_kij m.Y_not_empty subprob_kernel_axioms_def)
qed
show "s_finite_kernel X Y (ki i)"
by(auto intro!: s_finite_kernel_subI simp: emeasure_kij sk m.kernel_sets)
qed simp_all
qed
lemma(in measure_kernel) s_finite_kernel_finite_bounded:
assumes "⋀x. x ∈ space X ⟹ κ x (space Y) < ∞"
shows "s_finite_kernel X Y κ"
proof(cases "space X = {}")
case True
then show ?thesis
by(simp add: s_finite_kernel_empty_trivial)
next
case False
then have Y:"space Y ≠ {}" by(simp add: Y_not_empty)
have "measure_kernel X Y (case i of 0 ⇒ κ | Suc x ⇒ λx. null_measure Y)" for i
by(cases i,auto simp: measure_kernel_axioms) (auto simp: measure_kernel_def Y)
moreover have "κ x A = (∑i. emeasure ((case i of 0 ⇒ κ | Suc x ⇒ λx. null_measure Y) x) A)" for x A
by(simp add: suminf_offset[where i="Suc 0"])
moreover have "x ∈ space X ⟹ emeasure ((case i of 0 ⇒ κ | Suc x ⇒ λx. null_measure Y) x) (space Y) < ⊤" for x i
by(cases i) (use assms in auto)
ultimately show ?thesis
by(auto intro!: s_finite_kernel_finite_bounded_sum[where ki="λi. case i of 0 ⇒ κ | Suc _ ⇒ (λx. null_measure Y)" and X=X and Y=Y] simp: kernel_sets)
qed
lemma(in s_finite_kernel) density_s_finite_kernel:
assumes f[measurable]: "case_prod f ∈ X ⨂⇩M Y →⇩M borel"
shows "s_finite_kernel X Y (λx. density (κ x) (f x))"
proof(cases "space X = {}")
case True
then show ?thesis
by(simp add: s_finite_kernel_empty_trivial)
next
case False
note Y = Y_not_empty[OF this]
obtain ki' where ki': "⋀i. subprob_kernel X Y (ki' i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki' i x A)"
by(metis s_finite_kernels)
hence sets_ki'[measurable_cong]:"⋀x i. x ∈ space X ⟹ sets (ki' i x) = sets Y"
by(auto simp: subprob_kernel_def measure_kernel_def)
define ki where "ki ≡ (λi x. density (ki' i x) (f x))"
have sets_ki: "x ∈ space X ⟹ sets (ki i x) = sets Y" for i x
using ki'(1) by(auto simp: subprob_kernel_def measure_kernel_def ki_def)
have emeasure_k:"density (κ x) (f x) A = (∑i. ki i x A)" if x:"x ∈ space X" and A[measurable]:"A ∈ sets Y" for x A
using kernel_sets[OF x] x ki'(1) sets_ki'[OF x] by(auto simp: emeasure_density nn_integral_measure_suminf[OF _ ki'(2),of x] ki_def)
show ?thesis
proof(rule s_finite_kernel_s_finite_kernel[where ki="ki",OF _ _ emeasure_k])
fix i
note nn_integral_measurable_subprob_algebra2[OF _ ki'(1)[of i,simplified subprob_kernel_def'],measurable]
define kij where "kij ≡ (λj x. if j = 0 then density (ki' i x) (λy. ∞ * indicator {y∈space Y. f x y = ∞} y)
else if j = (Suc 0) then density (ki' i x) (λy. f x y * indicator {y∈space Y. f x y < ∞} y)
else null_measure Y)"
have emeasure_kij: "ki i x A = (∑j. kij j x A)" (is "?lhs = ?rhs") if x:"x ∈ space X" and [measurable]: "A ∈ sets Y" for x A
proof -
have "?lhs = (∫⇧+y∈A. f x y ∂ki' i x)"
using sets_ki[OF x,of i] x by(auto simp: ki_def emeasure_density)
also have "... = (∫⇧+y. (∞ * indicator {y ∈ space Y. f x y = ∞} y * indicator A y + f x y * indicator {y ∈ space Y. f x y < ∞} y * indicator A y) ∂ki' i x)"
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF sets_ki'[OF x]] indicator_def) (simp add: top.not_eq_extremum)
also have "... = density (ki' i x) (λy. ∞ * indicator {y∈space Y. f x y = ∞} y) A + density (ki' i x) (λy. f x y * indicator {y∈space Y. f x y < ∞} y) A"
using sets_ki[OF x,of i] x by(auto simp: ki_def emeasure_density nn_integral_add)
also have "... = ?rhs"
using suminf_finite[of "{..<Suc (Suc 0)}" "λj. kij j x A"] by(simp add: kij_def)
finally show ?thesis .
qed
have sets_kij[measurable_cong]:"x ∈ space X ⟹ sets (kij j x) = sets Y" for j x
by(auto simp: kij_def sets_ki')
show "s_finite_kernel X Y (ki i)"
proof(rule s_finite_kernel_s_finite_kernel[where ki=kij,OF _ _ emeasure_kij])
fix j
consider "j = 0" | "j = Suc 0" | "j ≠ 0" "j ≠ Suc 0" by auto
then show "s_finite_kernel X Y (kij j)"
proof cases
case 1
have emeasure_ki: "emeasure (kij j x) A = (∑j. emeasure (density (ki' i x) (indicator {y ∈ space Y. f x y = ⊤})) A)" if x:"x ∈ space X" and [measurable]: "A ∈ sets Y" for x A
using sets_ki'[OF x] x by(auto simp: 1 kij_def emeasure_density nn_integral_suminf[symmetric] indicator_def intro!: nn_integral_cong) (simp add: nn_integral_count_space_nat[symmetric])
have [simp]:"subprob_kernel X Y (λx. density (ki' i x) (indicator {y ∈ space Y. f x y = ⊤}))"
proof -
have [simp]:"x ∈ space X ⟹ set_nn_integral (ki' i x) (space Y) (indicator {y ∈ space Y. f x y = ⊤}) ≤ 1" for x
by(rule order.trans[OF nn_integral_mono[where v="λx. 1"]],insert ki'(1)[of i]) (auto simp: indicator_def subprob_kernel_def subprob_kernel_axioms_def intro!: subprob_space.emeasure_space_le_1)
show ?thesis
by(auto simp: subprob_kernel_def measure_kernel_def emeasure_density subprob_kernel_axioms_def sets_ki' sets_eq_imp_space_eq[OF sets_ki'] Y cong: measurable_cong intro!: subprob_spaceI)
qed
show ?thesis
by (auto simp: s_finite_kernel_def' sets_kij intro!: exI[where x="λk x. density (ki' i x) (indicator {y ∈ space Y. f x y = ⊤})"] simp: emeasure_ki )
next
case j:2
have emeasure_ki: "emeasure (kij j x) A = (∑k. density (ki' i x) (λy. f x y * indicator {y ∈ space Y. of_nat k ≤ f x y ∧ f x y < 1 + of_nat k} y) A)" if x:"x ∈ space X" and [measurable]:"A ∈ sets Y" for x A
proof -
have [simp]: "f x y * indicator {y ∈ space Y. f x y < ⊤} y * indicator A y = f x y * (∑k. indicator {y ∈ space Y. of_nat k ≤ f x y ∧ f x y < 1 + of_nat k} y) * indicator A y" if y:"y ∈ space Y" for y
proof(cases "f x y < ⊤")
case f:True
define l where "l ≡ floor (enn2real (f x y))"
have "nat l ≤ enn2real (f x y)" "enn2real (f x y) < 1 + nat l"
by (simp_all add: l_def) linarith
with y have l:"of_nat (nat l) ≤ f x y" "f x y < 1 + of_nat (nat l)"
using Orderings.order_eq_iff enn2real_positive_iff ennreal_enn2real_if ennreal_of_nat_eq_real_of_nat linorder_not_le of_nat_0_le_iff f by fastforce+
then have "(∑j. indicator {y ∈ space Y. of_nat j ≤ f x y ∧ f x y < 1 + of_nat j} y :: ennreal) = (∑j. if j = nat l then 1 else 0)"
by(auto intro!: suminf_cong simp: indicator_def y) (metis Suc_leI linorder_neqE_nat linorder_not_less of_nat_Suc of_nat_le_iff order_trans)
also have "... = 1"
using suminf_finite[where N="{nat l}" and f="λj. if j = nat l then 1 else (0 :: ennreal)"] by simp
finally show ?thesis
by(auto, insert f) (auto simp: indicator_def)
qed(use top.not_eq_extremum in fastforce)
show ?thesis
using sets_ki[OF x] sets_ki'[OF x] x by(auto simp: kij_def j emeasure_density nn_integral_suminf[symmetric] sets_eq_imp_space_eq[OF sets_ki'[OF x]] intro!: nn_integral_cong)
qed
show ?thesis
proof(rule s_finite_kernel_finite_bounded_sum[OF sets_kij _ emeasure_ki])
fix k
show "measure_kernel X Y (λx. density (ki' i x) (λy. f x y * indicator {y ∈ space Y. of_nat k ≤ f x y ∧ f x y < 1 + of_nat k} y))"
using sets_ki'[of _ i] by(auto simp: measure_kernel_def emeasure_density Y cong: measurable_cong)
next
fix k x
assume x:"x ∈space X"
have "emeasure (density (ki' i x) (λy. f x y * indicator {y ∈ space Y. of_nat k ≤ f x y ∧ f x y < 1 + of_nat k} y)) (space Y) ≤ 1 + of_nat k"
by(auto simp: emeasure_density x,rule order.trans[OF nn_integral_mono[where v="λx. 1 + of_nat k"]]) (insert subprob_kernel.subprob_space[OF ki'(1)[of i] x], auto simp: indicator_def subprob_kernel_def subprob_kernel_axioms_def sets_eq_imp_space_eq[OF sets_ki'[OF x]] intro!: mult_mono[where d="1 :: ennreal",OF order.refl,simplified])
also have "... < ∞"
by (simp add: of_nat_less_top)
finally show "emeasure (density (ki' i x) (λy. f x y * indicator {y ∈ space Y. of_nat k ≤ f x y ∧ f x y < 1 + of_nat k} y)) (space Y) < ∞" .
qed auto
next
case 3
then show ?thesis
by(auto simp: kij_def s_finite_kernel_cong_sets[of X X Y,OF _ sets_null_measure[symmetric]] Y intro!: s_finite_measure.s_finite_kernel_const finite_measure.s_finite_measure_finite_measure finite_measureI)
qed
qed(auto simp: sets_ki)
qed(auto simp: kernel_sets)
qed
lemma(in s_finite_kernel) nn_integral_measurable_f:
assumes [measurable]:"(λ(x,y). f x y) ∈ borel_measurable (X ⨂⇩M Y)"
shows "(λx. ∫⇧+y. f x y ∂(κ x)) ∈ borel_measurable X"
proof -
obtain κi where κi:"⋀i. subprob_kernel X Y (κi i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. κi i x A)"
by(metis s_finite_kernels)
show ?thesis
proof(rule measurable_cong[THEN iffD2])
fix x
assume "x ∈ space X"
with κi show "(∫⇧+ y. f x y ∂κ x) = (∑i. ∫⇧+ y. f x y ∂κi i x)"
by(auto intro!: nn_integral_measure_suminf[symmetric] simp: subprob_kernel_def kernel_sets measure_kernel_def)
next
show "(λx. ∑i. ∫⇧+ y. f x y ∂κi i x) ∈ borel_measurable X"
using κi(1) nn_integral_measurable_subprob_algebra2[OF assms] by(simp add: subprob_kernel_def' )
qed
qed
lemma(in s_finite_kernel) nn_integral_measurable_f':
assumes "f ∈ borel_measurable (X ⨂⇩M Y)"
shows "(λx. ∫⇧+y. f (x, y) ∂(κ x)) ∈ borel_measurable X"
using nn_integral_measurable_f[where f="curry f",simplified,OF assms] by simp
lemma(in s_finite_kernel) bind_kernel_s_finite_kernel':
assumes "s_finite_kernel (X ⨂⇩M Y) Z (case_prod g)"
shows "s_finite_kernel X Z (λx. κ x ⤜⇩k g x)"
proof(cases "space X = {}")
case True
then show ?thesis
by (simp add: s_finite_kernel_empty_trivial)
next
case X:False
then have Y:"space Y ≠ {}"
by(simp add: Y_not_empty)
from s_finite_kernels obtain ki where ki:
"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
by metis
interpret g:s_finite_kernel "X ⨂⇩M Y" Z "case_prod g" by fact
from g.s_finite_kernels[simplified space_pair_measure] obtain gi where gi:
"⋀i. subprob_kernel (X ⨂⇩M Y) Z (gi i)" "⋀x y A. x ∈ space X ⟹ y ∈ space Y ⟹ g x y A = (∑i. gi i (x,y) A)"
by auto metis
define kgi where "kgi = (λi x. case prod_decode i of (i,j) ⇒ (ki j x ⤜ curry (gi i) x))"
have emeasure:"emeasure (κ x ⤜⇩k g x) A = (∑i. emeasure (kgi i x) A)" (is "?lhs = ?rhs") if x:"x ∈ space X" and A:"A ∈ sets Z" for x A
proof -
interpret gx: s_finite_kernel Y Z "g x"
using g.comp_measurable[OF measurable_Pair1'[OF x]] by auto
have "?lhs = (∫⇧+ y. g x y A ∂κ x)"
using gx.emeasure_bind_kernel[OF kernel_sets[OF x] A]
by(auto simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] Y)
also have "... = (∫⇧+ y. (∑i. gi i (x, y) A) ∂κ x)"
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] gi(2)[OF x])
also have "... = (∑i. ∫⇧+ y. gi i (x, y) A ∂κ x)"
using gi(1) x A by(auto intro!: nn_integral_suminf simp: subprob_kernel_def')
also have "... = (∑i. (∑j. ∫⇧+ y. gi i (x, y) A ∂ki j x))"
by(rule suminf_cong, rule nn_integral_measure_suminf[symmetric], insert kernel_sets[OF x] ki gi(1) x A)
(auto simp: subprob_kernel_def measure_kernel_def measurable_cong_sets[OF sets_pair_measure_cong[OF refl kernel_sets[OF x]]] intro!: measurable_Pair2[OF _ x])
also have "... = (∑i. (∑j. emeasure (ki j x ⤜ (curry (gi i) x)) A))"
using sets_eq_imp_space_eq[of "ki _ x" Y] ki(1) x gi(1) measurable_cong_sets[of _ _ "subprob_algebra Z" "subprob_algebra Z", OF sets_pair_measure_cong[of X X Y "ki _ x"]]
by(auto intro!: suminf_cong emeasure_bind[OF _ _ A,symmetric] measurable_Pair2[OF _ x] simp: curry_def subprob_kernel_def[of X] subprob_kernel_def'[of "X ⨂⇩M Y"] measure_kernel_def Y)
also have "... = ?rhs"
unfolding kgi_def by(rule suminf_ennreal_2dimen[symmetric]) (simp add: curry_def)
finally show ?thesis .
qed
have sets: "sets (κ x ⤜⇩k g x) = sets Z" if x:"x ∈ space X" for x
proof -
interpret gx: s_finite_kernel Y Z "g x"
using g.comp_measurable[OF measurable_Pair1'[OF x]] by auto
show ?thesis
by(simp add: gx.sets_bind_kernel[OF _ kernel_sets[OF x]] Y)
qed
have sk:"subprob_kernel X Z (kgi i)" for i
using ki(1)[of "snd (prod_decode i)"] gi(1)[of "fst (prod_decode i)"]
by(auto simp: subprob_kernel_def' kgi_def split_beta' curry_def)
show ?thesis
using sk by(auto simp: s_finite_kernel_def' emeasure sets subprob_kernel_def' intro!: exI[where x=kgi] measurable_cong[where g="λx. ∑i. emeasure (kgi i x) _" and f="λx. emeasure (κ x ⤜⇩k g x) _",THEN iffD2])
qed
corollary(in s_finite_kernel) bind_kernel_s_finite_kernel:
assumes "s_finite_kernel Y Z k'"
shows "s_finite_kernel X Z (λx. κ x ⤜⇩k k')"
by(auto intro!: bind_kernel_s_finite_kernel' s_finite_kernel.comp_measurable[OF assms measurable_snd] simp: split_beta')
lemma(in s_finite_kernel) nn_integral_bind_kernel:
assumes "f ∈ borel_measurable Y" "sets μ = sets X"
shows "(∫⇧+ y. f y ∂(μ ⤜⇩k κ)) = (∫⇧+x. (∫⇧+ y. f y ∂(κ x)) ∂μ)"
proof(cases "space X = {}")
case True
then show ?thesis
by(simp add: sets_eq_imp_space_eq[OF assms(2)] bind_kernel_def nn_integral_empty)
next
case X:False
then have μ:"space μ ≠ {}" by(simp add: sets_eq_imp_space_eq[OF assms(2)])
note 1[measurable_cong] = assms(2) sets_bind_kernel[OF X assms(2)]
from assms(1) show ?thesis
proof induction
case ih:(cong f g)
have "(∫⇧+ y. f y ∂(μ ⤜⇩k κ)) = (∫⇧+ y. g y ∂(μ ⤜⇩k κ))" "(∫⇧+ x. integral⇧N (κ x) f ∂μ) = (∫⇧+ x. integral⇧N (κ x) g ∂μ)"
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF 1(2)] sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] ih(3))
then show ?case
by(simp add: ih)
next
case (set A)
then show ?case
by(auto simp: emeasure_bind_kernel[OF 1(1) _ X] sets_eq_imp_space_eq[OF 1(1)] intro!: nn_integral_cong)
next
case ih:(mult u c)
then have "(∫⇧+ x. ∫⇧+ y. c * u y ∂κ x ∂μ) = (∫⇧+ x. c * ∫⇧+ y. u y ∂κ x ∂μ)"
by(auto intro!: nn_integral_cong nn_integral_cmult simp: sets_eq_imp_space_eq[OF 1(1)])
with ih nn_integral_measurable_f[of "λ_ y. u y"] show ?case
by(auto simp: nn_integral_cmult intro!: nn_integral_cong)
next
case ih:(add u v)
then have "(∫⇧+ x. ∫⇧+ y. v y + u y ∂κ x ∂μ) = (∫⇧+ x. (∫⇧+ y. v y ∂κ x) + (∫⇧+ y. u y ∂κ x) ∂μ)"
by(auto intro!: nn_integral_cong simp: nn_integral_add sets_eq_imp_space_eq[OF 1(1)])
with ih nn_integral_measurable_f[of "λ_ y. u y"] nn_integral_measurable_f[of "λ_ y. v y"] show ?case
by(simp add: nn_integral_add)
next
case ih[measurable]:(seq U)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = ((⨆i. integral⇧N (μ ⤜⇩k κ) (U i)))"
by(rule nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[of U UNIV,symmetric]]) (use ih in auto)
also have "... = (⨆i. ∫⇧+ x. (∫⇧+ y. U i y ∂κ x) ∂μ)"
by(simp add: ih)
also have "... = (∫⇧+ x. (⨆i. (∫⇧+ y. U i y ∂κ x)) ∂μ)"
proof(rule nn_integral_monotone_convergence_SUP[symmetric])
show "incseq (λi x. ∫⇧+ y. U i y ∂κ x)"
by standard+ (auto intro!: le_funI nn_integral_mono simp:le_funD[OF incseqD[OF ih(3)]])
qed(use nn_integral_measurable_f[of "λ_ y. U _ y"] in simp)
also have "... = ?rhs"
by(rule nn_integral_cong, rule nn_integral_monotone_convergence_SUP[of U,simplified SUP_apply[of U UNIV,symmetric],OF ih(3),symmetric]) (auto simp: sets_eq_imp_space_eq[OF 1(1)])
finally show ?thesis .
qed
qed
qed
lemma(in s_finite_kernel) bind_kernel_assoc:
assumes "s_finite_kernel Y Z k'" "sets μ = sets X"
shows "μ ⤜⇩k (λx. κ x ⤜⇩k k') = μ ⤜⇩k κ ⤜⇩k k'"
proof(cases "space X = {}")
case X:False
then have μ: "space μ ≠ {}" and Y:"space Y ≠ {}"
by(simp_all add: Y_not_empty sets_eq_imp_space_eq[OF assms(2)])
interpret k':s_finite_kernel Y Z k' by fact
interpret k'': s_finite_kernel X Z "λx. κ x ⤜⇩k k'"
by(rule bind_kernel_s_finite_kernel[OF assms(1)])
show ?thesis
proof(rule measure_eqI)
fix A
assume "A ∈ sets (μ ⤜⇩k (λx. κ x ⤜⇩k k'))"
then have A[measurable]: "A ∈ sets Z"
by(simp add: k''.sets_bind_kernel[OF X assms(2)])
show "emeasure (μ ⤜⇩k (λx. κ x ⤜⇩k k')) A = emeasure (μ ⤜⇩k κ ⤜⇩k k') A" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. emeasure (κ x ⤜⇩k k') A ∂μ)"
by(rule k''.emeasure_bind_kernel[OF assms(2) A X])
also have "... = (∫⇧+ x. ∫⇧+ y. k' y A ∂κ x ∂μ)"
using k'.emeasure_bind_kernel[OF kernel_sets A]
by(auto intro!: nn_integral_cong simp: sets_eq_imp_space_eq[OF assms(2)] sets_eq_imp_space_eq[OF kernel_sets] Y)
also have "... = (∫⇧+ y. k' y A ∂(μ ⤜⇩k κ))"
by(simp add: nn_integral_bind_kernel[OF k'.emeasure_measurable[OF A] assms(2)])
also have "... = ?rhs"
by(simp add: k'.emeasure_bind_kernel[OF sets_bind_kernel[OF X assms(2)] A] sets_eq_imp_space_eq[OF sets_bind_kernel[OF X assms(2)]] Y)
finally show ?thesis .
qed
qed(auto simp: k'.sets_bind_kernel[OF Y sets_bind_kernel[OF X assms(2)]] k''.sets_bind_kernel[OF X assms(2)])
qed(simp add: bind_kernel_def sets_eq_imp_space_eq[OF assms(2)])
lemma s_finite_kernel_pair_measure:
assumes "s_finite_kernel X Y k" and "s_finite_kernel X Z k'"
shows "s_finite_kernel X (Y ⨂⇩M Z) (λx. k x ⨂⇩M k' x)"
proof -
interpret k: s_finite_kernel X Y k by fact
interpret k': s_finite_kernel X Z k' by fact
from k.s_finite_kernels k'.s_finite_kernels obtain ki ki'
where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ k x A = (∑i. ki i x A)"
and ki':"⋀i. subprob_kernel X Z (ki' i)" "⋀x A. x ∈ space X ⟹ k' x A = (∑i. ki' i x A)"
by metis
then have 1[measurable_cong]: "⋀x i. x ∈ space X ⟹ sets (ki i x) = sets Y" "⋀x i. x ∈ space X ⟹ sets (ki' i x) = sets Z"
by(auto simp: subprob_kernel_def measure_kernel_def)
define kki where "kki ≡ (λi x. (λ(j,i). ki i x ⨂⇩M ki' j x) (prod_decode i))"
have kki1: "⋀i. subprob_kernel X (Y ⨂⇩M Z) (kki i)"
using ki(1) ki'(1) by(auto simp: subprob_kernel_def' kki_def split_beta intro!: measurable_pair_measure)
have kki2: "(k x ⨂⇩M k' x) A = (∑i. (kki i x) A)" (is "?lhs = ?rhs") if x:"x ∈ space X" and A[measurable]: "A ∈ sets (Y ⨂⇩M Z)" for x A
proof -
have "?lhs = (∫⇧+ y. ∫⇧+ z. indicator A (y, z) ∂k' x ∂k x)"
using x by(simp add: s_finite_measure.emeasure_pair_measure'[OF k'.image_s_finite_measure])
also have "... = (∫⇧+ y. (∑j. ∫⇧+ z. indicator A (y, z) ∂ki' j x) ∂k x)"
using ki' x by(auto intro!: nn_integral_cong nn_integral_measure_suminf[symmetric] simp: sets_eq_imp_space_eq[OF k.kernel_sets[OF x]] subprob_kernel_def measure_kernel_def k'.kernel_sets)
also have "... = (∑j. ∫⇧+ y. ∫⇧+ z. indicator A (y, z) ∂ki' j x ∂k x)"
using x by(auto intro!: nn_integral_suminf s_finite_measure.borel_measurable_nn_integral_fst' s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]])
also have "... = (∑j. (∑i. (∫⇧+ y. ∫⇧+ z. indicator A (y, z) ∂ki' j x ∂ki i x)))"
using x ki by(auto intro!: suminf_cong nn_integral_measure_suminf[symmetric] s_finite_measure.borel_measurable_nn_integral_fst' simp: k.kernel_sets[OF x] subprob_kernel_def measure_kernel_def s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]])
also have "... = (∑j. (∑i. (ki i x ⨂⇩M ki' j x) A))"
using x by(auto simp: s_finite_measure.emeasure_pair_measure'[OF s_finite_kernel.image_s_finite_measure[OF subprob_kernel.s_finite_kernel_subprob_kernel[OF ki'(1)]]])
also have "... = ?rhs"
unfolding kki_def by(rule suminf_ennreal_2dimen[symmetric]) auto
finally show ?thesis .
qed
show ?thesis
proof
fix B
assume [measurable]:"B ∈ sets (Y ⨂⇩M Z)"
show "(λx. emeasure (k x ⨂⇩M k' x) B) ∈ borel_measurable X"
by(rule measurable_cong[where g="λx. ∑i. (kki i x) B",THEN iffD2], insert kki1) (auto simp: subprob_kernel_def' kki2)
qed(auto intro!: exI[where x=kki] simp: subprob_kernel.finite_kernel kki1 kki2 k.kernel_sets k'.kernel_sets space_pair_measure k.Y_not_empty k'.Y_not_empty)
qed
lemma pair_measure_eq_bind_s_finite:
assumes "s_finite_measure μ" "s_finite_measure ν"
shows "μ ⨂⇩M ν = μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x,y)))"
proof -
consider "space μ = {}" | "space ν = {}" | "space μ ≠ {}" "space ν ≠ {}"
by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(auto simp: bind_kernel_def space_pair_measure intro!: space_empty)
next
case 2
then have "μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x, y))) = count_space {}"
by(auto simp: bind_kernel_def space_empty)
with 2 show ?thesis
by(auto simp: space_pair_measure intro!: space_empty)
next
case 3
show ?thesis
proof(intro measure_eqI sets_bind_kernel[OF _ 3(1),symmetric] sets_bind_kernel[OF _ 3(2)])
fix A
assume A[measurable]: "A ∈ sets (μ ⨂⇩M ν)"
show "emeasure (μ ⨂⇩M ν) A = emeasure (μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x, y)))) A" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. ∫⇧+ y. return (μ ⨂⇩M ν) (x, y) A ∂ν ∂μ)"
by(simp add: s_finite_measure.emeasure_pair_measure'[OF assms(2)])
also have "... = (∫⇧+ x. (ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x,y))) A ∂μ)"
by(auto intro!: nn_integral_cong measure_kernel.emeasure_bind_kernel[OF _ _ A 3(2),symmetric] prob_kernel.axioms(1) simp: prob_kernel_def' simp del: emeasure_return)
also have "... = ?rhs"
by(auto intro!: measure_kernel.emeasure_bind_kernel[OF _ _ A 3(1),symmetric] s_finite_kernel.axioms(1) s_finite_kernel.bind_kernel_s_finite_kernel'[where Y=ν] s_finite_measure.s_finite_kernel_const[OF assms(2) 3(2)] prob_kernel.s_finite_kernel_prob_kernel[of "μ ⨂⇩M ν"] simp: prob_kernel_def')
finally show ?thesis .
qed
qed simp
qed
qed
lemma bind_kernel_rotate_return:
assumes "s_finite_measure μ" "s_finite_measure ν"
shows "μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x,y))) = ν ⤜⇩k (λy. μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x,y)))"
proof -
consider "space μ = {}" | "space ν = {}" | "space μ ≠ {}" "space ν ≠ {}"
by auto
then show ?thesis
proof cases
case 1
then have "ν ⤜⇩k (λy. μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x,y))) = count_space {}"
by(auto simp: bind_kernel_def space_empty)
then show ?thesis
by(auto simp: bind_kernel_def space_pair_measure 1 intro!: space_empty)
next
case 2
then have "μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x, y))) = count_space {}"
by(auto simp: bind_kernel_def space_empty)
with 2 show ?thesis
by(auto simp: space_pair_measure bind_kernel_def intro!: space_empty)
next
case 3
show ?thesis
unfolding pair_measure_eq_bind_s_finite[OF assms,symmetric]
proof(intro measure_eqI)
fix A
assume A[measurable]:"A ∈ sets (μ ⨂⇩M ν)"
show "emeasure (μ ⨂⇩M ν) A = emeasure (ν ⤜⇩k (λy. μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x, y)))) A" (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. ∫⇧+ y. indicator A (x, y) ∂ν ∂μ)"
by(rule s_finite_measure.emeasure_pair_measure'[OF assms(2) A])
also have "... = (∫⇧+ y. ∫⇧+ x. return (μ ⨂⇩M ν) (x, y) A ∂μ ∂ν)"
by(simp add: nn_integral_snd'[OF assms] s_finite_measure.nn_integral_fst'[OF assms(2)])
also have "... = (∫⇧+ y. (μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x, y))) A ∂ν)"
by(auto intro!: nn_integral_cong measure_kernel.emeasure_bind_kernel[OF _ _ A 3(1),symmetric] prob_kernel.axioms(1) simp add: prob_kernel_def' simp del: emeasure_return)
also have "... = ?rhs"
by(auto intro!: measure_kernel.emeasure_bind_kernel[OF _ _ A 3(2),symmetric] s_finite_kernel.axioms(1) s_finite_kernel.bind_kernel_s_finite_kernel'[where Y=μ] s_finite_measure.s_finite_kernel_const[OF assms(1) 3(1)] prob_kernel.s_finite_kernel_prob_kernel[of "ν ⨂⇩M μ"] simp: prob_kernel_def')
finally show ?thesis .
qed
qed(auto intro!: sets_bind_kernel[OF _ 3(2),symmetric] sets_bind_kernel[OF _ 3(1)])
qed
qed
lemma bind_kernel_rotate':
assumes "s_finite_measure μ" "s_finite_measure ν" "s_finite_kernel (μ ⨂⇩M ν) Z (case_prod f)"
shows "μ ⤜⇩k (λx. ν ⤜⇩k (λy. f x y)) = ν ⤜⇩k (λy. μ ⤜⇩k (λx. f x y))" (is "?lhs = ?rhs")
proof -
interpret sk: s_finite_kernel "μ ⨂⇩M ν" Z "case_prod f" by fact
consider "space μ = {}" | "space ν = {}" | "space μ ≠ {}" "space ν ≠ {}"
by auto
then show ?thesis
proof cases
case 1
then have "?rhs = count_space {}"
by(auto simp: bind_kernel_def space_empty)
then show ?thesis
by(auto simp: bind_kernel_def space_pair_measure 1 intro!: space_empty)
next
case 2
then show ?thesis
by(auto simp: space_pair_measure bind_kernel_def intro!: space_empty)
next
case 3
show ?thesis
proof -
have "?lhs = μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x, y)) ⤜⇩k case_prod f)"
by(auto intro!: bind_kernel_cong_All simp: s_finite_kernel.bind_kernel_assoc[OF prob_kernel.s_finite_kernel_prob_kernel assms(3) refl,of ν "λy. return (μ ⨂⇩M ν) (_, y)",simplified prob_kernel_def',symmetric] sk.bind_kernel_return space_pair_measure)
also have "... = μ ⤜⇩k (λx. ν ⤜⇩k (λy. return (μ ⨂⇩M ν) (x,y))) ⤜⇩k (case_prod f)"
by(auto simp: s_finite_kernel.bind_kernel_assoc[OF s_finite_kernel.bind_kernel_s_finite_kernel'[OF s_finite_measure.s_finite_kernel_const[OF assms(2) 3(2),of μ] prob_kernel.s_finite_kernel_prob_kernel,of "μ ⨂⇩M ν" "λx y. return (μ ⨂⇩M ν) (x,y)",simplified] assms(3) refl, simplified prob_kernel_def',symmetric])
also have "... = ν ⤜⇩k (λy. μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x,y))) ⤜⇩k (case_prod f)"
by(simp add: bind_kernel_rotate_return assms)
also have "... = ν ⤜⇩k (λy. μ ⤜⇩k (λx. return (μ ⨂⇩M ν) (x, y)) ⤜⇩k case_prod f)"
by(auto intro!: s_finite_kernel.bind_kernel_assoc[OF _ assms(3),symmetric] s_finite_kernel.bind_kernel_s_finite_kernel'[OF s_finite_measure.s_finite_kernel_const[OF assms(1) 3(1)]] prob_kernel.s_finite_kernel_prob_kernel[of "ν ⨂⇩M μ"] simp: prob_kernel_def')
also have "... = ?rhs"
by(auto intro!: bind_kernel_cong_All simp: s_finite_kernel.bind_kernel_assoc[OF prob_kernel.s_finite_kernel_prob_kernel assms(3) refl,of μ "λx. return (μ ⨂⇩M ν) (x, _)",simplified prob_kernel_def',symmetric] sk.bind_kernel_return space_pair_measure)
finally show ?thesis .
qed
qed
qed
lemma bind_kernel_rotate:
assumes "sets μ = sets X" and "sets ν = sets Y"
and "s_finite_measure μ" "s_finite_measure ν" "s_finite_kernel (X ⨂⇩M Y) Z (λ(x,y). f x y)"
shows "μ ⤜⇩k (λx. ν ⤜⇩k (λy. f x y)) = ν ⤜⇩k (λy. μ ⤜⇩k (λx. f x y))"
by(auto intro!: bind_kernel_rotate' assms simp: s_finite_kernel_cong_sets[OF sets_pair_measure_cong[OF assms(1,2)]])
lemma(in s_finite_kernel) emeasure_measurable':
assumes A[measurable]: "(SIGMA x:space X. A x) ∈ sets (X ⨂⇩M Y)"
shows "(λx. emeasure (κ x) (A x)) ∈ borel_measurable X"
proof -
have **: "A x ∈ sets Y" if "x ∈ space X" for x
proof -
have "Pair x -` Sigma (space X) A = A x"
using that by auto
with sets_Pair1[OF A, of x] show "A x ∈ sets Y"
by auto
qed
have *: "⋀x. fst x ∈ space X ⟹ snd x ∈ A (fst x) ⟷ x ∈ (SIGMA x:space X. A x)"
by (auto simp: fun_eq_iff)
have "(λ(x, y). indicator (A x) y::ennreal) ∈ borel_measurable (X ⨂⇩M Y)"
by (measurable,subst measurable_cong[OF *]) (auto simp: space_pair_measure)
then have "(λx. integral⇧N (κ x) (indicator (A x))) ∈ borel_measurable X"
by(rule nn_integral_measurable_f)
moreover have "integral⇧N (κ x) (indicator (A x)) = emeasure (κ x) (A x)" if "x ∈ space X" for x
using **[OF that] kernel_sets[OF that] by(auto intro!: nn_integral_indicator)
ultimately show "(λx. emeasure (κ x) (A x)) ∈ borel_measurable X"
by(auto cong: measurable_cong)
qed
lemma(in s_finite_kernel) measure_measurable':
assumes "(SIGMA x:space X. A x) ∈ sets (X ⨂⇩M Y)"
shows "(λx. measure (κ x) (A x)) ∈ borel_measurable X"
using emeasure_measurable'[OF assms] by(simp add: measure_def)
lemma(in s_finite_kernel) AE_pred:
assumes P[measurable]:"Measurable.pred (X ⨂⇩M Y) (case_prod P)"
shows "Measurable.pred X (λx. AE y in κ x. P x y)"
proof -
have [measurable]:"Measurable.pred X (λx. emeasure (κ x) {y ∈ space Y. ¬ P x y} = 0)"
proof(rule pred_eq_const1[where N=borel],rule emeasure_measurable')
have "(SIGMA x:space X. {y ∈ space Y. ¬ P x y}) = {xy∈space (X ⨂⇩M Y). ¬ P (fst xy) (snd xy)}"
by (auto simp: space_pair_measure)
also have "... ∈ sets (X ⨂⇩M Y)"
by simp
finally show "(SIGMA x:space X. {y ∈ space Y. ¬ P x y}) ∈ sets (X ⨂⇩M Y)" .
qed simp
have "{x ∈ space X. almost_everywhere (κ x) (P x)} = {x ∈ space X. emeasure (κ x) {y∈space Y. ¬ P x y} = 0}"
proof safe
fix x
assume x:"x ∈ space X"
show "(AE y in κ x. P x y) ⟹ emeasure (κ x) {y ∈ space Y. ¬ P x y} = 0"
using emeasure_eq_0_AE[of "λy. ¬ P x y" "κ x"]
by(simp add: sets_eq_imp_space_eq[OF kernel_sets[OF x]])
show "emeasure (κ x) {y ∈ space Y. ¬ P x y} = 0 ⟹ almost_everywhere (κ x) (P x)"
using x by(auto intro!: AE_I[where N="{y ∈ space Y. ¬ P x y}"] simp: sets_eq_imp_space_eq[OF kernel_sets[OF x]] kernel_sets[OF x])
qed
also have "... ∈ sets X"
by(simp add: pred_def)
finally show ?thesis
by(simp add: pred_def)
qed
lemma(in subprob_kernel) integrable_probability_kernel_pred:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"(λ(x,y). f x y) ∈ borel_measurable (X ⨂⇩M Y)"
shows "Measurable.pred X (λx. integrable (κ x) (f x))"
proof(rule measurable_cong[THEN iffD2])
show "x ∈ space X ⟹ integrable (κ x) (f x) ⟷ (∫⇧+y. norm (f x y) ∂(κ x)) < ∞" for x
by(auto simp: integrable_iff_bounded)
next
have "(λ(x,y). ennreal (norm (f x y))) ∈ borel_measurable (X ⨂⇩M Y)"
by measurable
from nn_integral_measurable_f[OF this]
show "Measurable.pred X (λx. (∫⇧+ y. ennreal (norm (f x y)) ∂κ x) < ∞)"
by simp
qed
corollary integrable_measurable_subprob':
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"(λ(x,y). f x y) ∈ borel_measurable (X ⨂⇩M Y)" "k ∈ X →⇩M subprob_algebra Y"
shows "Measurable.pred X (λx. integrable (k x) (f x))"
by(auto intro!: subprob_kernel.integrable_probability_kernel_pred[where Y=Y] simp: subprob_kernel_def')
lemma(in subprob_kernel) integrable_probability_kernel_pred':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes "f ∈ borel_measurable (X ⨂⇩M Y)"
shows "Measurable.pred X (λx. integrable (κ x) (curry f x))"
using integrable_probability_kernel_pred[of "curry f"] assms by auto
lemma(in subprob_kernel) lebesgue_integral_measurable_f_subprob:
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"f ∈ borel_measurable (X ⨂⇩M Y)"
shows "(λx. ∫y. f (x,y) ∂(κ x)) ∈ borel_measurable X"
proof -
from borel_measurable_implies_sequence_metric[OF assms, of 0]
obtain s where s: "⋀i. simple_function (X ⨂⇩M Y) (s i)"
and "∀x∈space (X ⨂⇩M Y). (λi. s i x) ⇢ f x"
and "∀i. ∀x∈space (X ⨂⇩M Y). dist (s i x) 0 ≤ 2 * dist (f x) 0"
by auto
then have *:
"⋀x y. x ∈ space X ⟹ y ∈ space Y ⟹ (λi. s i (x, y)) ⇢ f (x,y)"
"⋀i x y. x ∈ space X ⟹ y ∈ space Y ⟹ norm (s i (x, y)) ≤ 2 * norm (f (x, y))"
by (auto simp: space_pair_measure)
have [measurable]: "⋀i. s i ∈ borel_measurable (X ⨂⇩M Y)"
by (rule borel_measurable_simple_function) fact
have s':"⋀i. s i ∈ X ⨂⇩M Y →⇩M count_space UNIV"
by (rule measurable_simple_function) fact
define f' where [abs_def]: "f' i x =
(if integrable (κ x) (curry f x) then Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y)) else 0)" for i x
have eq: "Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y)) =
(∑z∈s i ` (space X × space Y). measure (κ x) {y ∈ space (κ x). s i (x, y) = z} *⇩R z)" if "x ∈ space X" for x i
proof -
have [measurable_cong]: "sets (κ x) = sets Y" and [simp]: "space (κ x) = space Y"
using that by (simp_all add: kernel_sets kernel_space)
with that show ?thesis
using s[THEN simple_functionD(1)]
unfolding simple_bochner_integral_def
by (intro sum.mono_neutral_cong_left)
(auto simp: eq_commute space_pair_measure image_iff cong: conj_cong)
qed
show ?thesis
proof (rule borel_measurable_LIMSEQ_metric)
fix i
note [measurable] = integrable_probability_kernel_pred'[OF assms]
have [measurable]:"(SIGMA x:space X. {y ∈ space Y. s i (x, y) = s i (a, b)}) ∈ sets (X ⨂⇩M Y)" for a b
proof -
have "(SIGMA x:space X. {y ∈ space Y. s i (x, y) = s i (a, b)}) = space (X ⨂⇩M Y) ∩ s i -` {s i (a,b)}"
by(auto simp: space_pair_measure)
thus ?thesis
using s'[of i] by simp
qed
show "f' i ∈ borel_measurable X"
by (auto simp : eq kernel_space f'_def cong: measurable_cong if_cong intro!: borel_measurable_sum measurable_If borel_measurable_scaleR measure_measurable')
next
fix x
assume x:"x ∈ space X"
have "(λi. Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y))) ⇢ (∫y. f (x,y) ∂(κ x))" if int_f:"integrable (κ x) (curry f x)"
proof -
have int_2f: "integrable (κ x) (λy. 2 * norm (f (x,y)))"
using int_f by(auto simp: curry_def)
have "(λi. integral⇧L (κ x) (λy. s i (x, y))) ⇢ integral⇧L (κ x) (curry f x)"
proof (rule integral_dominated_convergence)
show "curry f x ∈ borel_measurable (κ x)"
using int_f by auto
next
show "⋀i. (λy. s i (x, y)) ∈ borel_measurable (κ x)"
using x kernel_sets by auto
next
show "AE xa in κ x. (λi. s i (x, xa)) ⇢ curry f x xa"
using x *(1) kernel_space by(auto simp: curry_def)
next
show "⋀i. AE xa in κ x. norm (s i (x, xa)) ≤ 2 * norm (f (x,xa))"
using x * (2) kernel_space by auto
qed fact
moreover have "integral⇧L (κ x) (λy. s i (x, y)) = Bochner_Integration.simple_bochner_integral (κ x) (λy. s i (x, y))" for i
proof -
have "Bochner_Integration.simple_bochner_integrable (κ x) (λy. s i (x, y))"
proof (rule simple_bochner_integrableI_bounded)
have "(λy. s i (x, y)) ` space Y ⊆ s i ` (space X × space Y)"
using x by auto
then show "simple_function (κ x) (λy. s i (x, y))"
using simple_functionD(1)[OF s(1), of i] x kernel_space
by (intro simple_function_borel_measurable) (auto simp: space_pair_measure dest: finite_subset)
next
have "(∫⇧+ y. ennreal (norm (s i (x, y))) ∂κ x) ≤ (∫⇧+ y. 2 * norm (f (x,y)) ∂κ x)"
using x *(2) kernel_space by (intro nn_integral_mono) auto
also have "... < ∞"
using int_2f unfolding integrable_iff_bounded by simp
finally show "(∫⇧+ y. ennreal (norm (s i (x, y))) ∂κ x) < ∞" .
qed
then show ?thesis
by (rule simple_bochner_integrable_eq_integral[symmetric])
qed
ultimately show ?thesis
by(simp add: curry_def)
qed
thus "(λi. f' i x) ⇢ (∫y. f (x,y) ∂(κ x))"
by (cases "integrable (κ x) (curry f x)") (simp_all add: f'_def not_integrable_integral_eq curry_def)
qed
qed
lemma(in s_finite_kernel) integrable_measurable_pred[measurable (raw)]:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"case_prod f ∈ borel_measurable (X ⨂⇩M Y)"
shows "Measurable.pred X (λx. integrable (κ x) (f x))"
proof(cases "space X = {}")
case True
from space_empty[OF this] show ?thesis
by simp
next
case h:False
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
using s_finite_kernels by metis
have [simp]:"integrable (κ x) (f x) = ((∑i. ∫⇧+ y. ennreal (norm (f x y)) ∂ki i x) < ∞)" if "x ∈ space X" for x
using ki(1) nn_integral_measure_suminf[of "λi. ki i x" "κ x",OF _ ki(2)] that kernel_sets
by(auto simp: integrable_iff_bounded subprob_kernel_def measure_kernel_def)
note [measurable] = nn_integral_measurable_subprob_algebra2
show ?thesis
by(rule measurable_cong[where g="λx. (∑i. ∫⇧+y. ennreal (norm (f x y)) ∂(ki i x)) < ∞",THEN iffD2]) (insert ki(1), auto simp: subprob_kernel_def')
qed
lemma(in s_finite_kernel) integral_measurable_f:
fixes f :: "_ ⇒ _ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"case_prod f ∈ borel_measurable (X ⨂⇩M Y)"
shows "(λx. ∫y. f x y ∂(κ x)) ∈ borel_measurable X"
proof -
obtain ki where ki:"⋀i. subprob_kernel X Y (ki i)" "⋀x A. x ∈ space X ⟹ κ x A = (∑i. ki i x A)"
using s_finite_kernels by metis
note [measurable] = integral_measurable_subprob_algebra2
show ?thesis
proof(rule measurable_cong[where f="(λx. if integrable (κ x) (f x) then (∑i. ∫y. f x y ∂(ki i x)) else 0)",THEN iffD1])
fix x
assume h:"x ∈ space X"
{
assume h':"integrable (κ x) (f x)"
have "(∑i. ∫y. f x y ∂(ki i x)) = (∫y. f x y ∂(κ x))"
using lebesgue_integral_measure_suminf[of "λi. ki i x" "κ x",OF _ ki(2) h'] ki(1) kernel_sets[OF h] h
by(auto simp: subprob_kernel_def measure_kernel_def)
}
thus "(if integrable (κ x) (f x) then (∑i. ∫y. f x y ∂(ki i x)) else 0) = (∫y. f x y ∂(κ x))"
using not_integrable_integral_eq by auto
qed(insert ki(1), auto simp: subprob_kernel_def')
qed
lemma(in s_finite_kernel) integral_measurable_f':
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes [measurable]:"f ∈ borel_measurable (X ⨂⇩M Y)"
shows "(λx. ∫y. f (x,y) ∂(κ x)) ∈ borel_measurable X"
using integral_measurable_f[of "curry f"] by simp
lemma(in s_finite_kernel)
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes [measurable_cong]: "sets μ = sets X"
and "integrable (μ ⤜⇩k κ) f"
shows integrable_bind_kernelD1: "integrable μ (λx. ∫y. norm (f y) ∂κ x)" (is ?g1)
and integrable_bind_kernelD1': "integrable μ (λx. ∫y. f y ∂κ x)" (is ?g1')
and integrable_bind_kernelD2: "AE x in μ. integrable (κ x) f" (is ?g2)
and integrable_bind_kernelD3: "space X ≠ {} ⟹ f ∈ borel_measurable Y" (is "_ ⟹ ?g3")
proof -
show 1:"space X ≠ {} ⟹ ?g3"
using assms(2) sets_bind_kernel[OF _ assms(1)] by(simp add: integrable_iff_bounded cong: measurable_cong_sets)
have "integrable μ (λx. ∫y. norm (f y) ∂κ x) ∧ integrable μ (λx. ∫y. f y ∂κ x) ∧ (AE x in μ. integrable (κ x) f)"
proof(cases "space X = {}")
assume ne: "space X ≠ {}"
then have "space μ ≠ {}" by(simp add: sets_eq_imp_space_eq[OF assms(1)])
note h = integral_measurable_f[measurable] sets_bind_kernel[OF ne assms(1),measurable_cong]
have g2: ?g2
unfolding integrable_iff_bounded AE_conj_iff
proof safe
show "AE x in μ. f ∈ borel_measurable (κ x)"
using assms(2) by(auto simp: sets_eq_imp_space_eq[OF assms(1)] measurable_cong_sets[OF kernel_sets])
next
note nn_integral_measurable_f[measurable]
have "AE x in μ. (∫⇧+ x. ennreal (norm (f x)) ∂κ x) ≠ ∞"
by(rule nn_integral_PInf_AE,insert assms(2)) (auto simp: integrable_iff_bounded nn_integral_bind_kernel[OF _ assms(1)] intro!: )
thus "AE x in μ. (∫⇧+ x. ennreal (norm (f x)) ∂κ x) < ∞"
by (simp add: top.not_eq_extremum)
qed
have [simp]:"(∫⇧+ x. ∫⇧+ x. ennreal (norm (f x)) ∂κ x ∂μ) = (∫⇧+ x. ennreal (∫y. norm (f y) ∂κ x)∂μ)"
using g2 by(auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral)
have g1: ?g1
using assms(2) by(auto simp: integrable_iff_bounded measurable_cong_sets[OF h(2)] measurable_cong_sets[OF assms(1)] nn_integral_bind_kernel[OF _ assms(1)])
have ?g1'
using assms(2) by(auto intro!: Bochner_Integration.integrable_bound[OF g1])
with g2 g1 show ?thesis
by auto
qed(auto simp: space_empty[of μ] sets_eq_imp_space_eq[OF assms(1)] integrable_iff_bounded nn_integral_empty)
thus ?g1 ?g1' ?g2
by auto
qed
lemma(in s_finite_kernel)
fixes f :: "_ ⇒ _::{banach, second_countable_topology}"
assumes [measurable_cong]: "sets μ = sets X"
and [measurable]:"AE x in μ. integrable (κ x) f" "integrable μ (λx. ∫y. norm (f y) ∂κ x)" "f ∈ borel_measurable Y"
shows integrable_bind_kernel: "integrable (μ ⤜⇩k κ) f"
and integral_bind_kernel: "(∫y. f y ∂(μ ⤜⇩k κ)) = (∫x. (∫y. f y∂κ x)∂ μ)" (is ?eq)
proof -
have "integrable (μ ⤜⇩k κ) f ∧ (∫y. f y ∂(μ ⤜⇩k κ)) = (∫x. (∫y. f y∂κ x)∂ μ)"
proof(cases "space X = {}")
assume ne: "space X ≠ {}"
note sets_bind[measurable_cong] = sets_bind_kernel[OF ne assms(1)]
note h = integral_measurable_f[measurable]
have 1:"integrable (μ ⤜⇩k κ) f"
unfolding integrable_iff_bounded
proof
show "(∫⇧+ x. ennreal (norm (f x)) ∂(μ ⤜⇩k κ)) < ∞" (is "?l < _")
proof -
have "?l = (∫⇧+ x. ennreal (∫y. norm (f y) ∂κ x)∂μ)"
using assms(2) by(auto intro!: nn_integral_cong_AE simp: nn_integral_eq_integral simp: nn_integral_bind_kernel[OF _ assms(1)])
also have "... < ∞"
using assms(3) by(auto simp: integrable_iff_bounded)
finally show ?thesis .
qed
qed simp
then have ?eq
proof induction
case h[measurable]:(base A c)
hence 1:"integrable (μ ⤜⇩k κ) (indicat_real A)"
by simp
have 2:"integrable μ (λx. measure (κ x) A)"
by(rule Bochner_Integration.integrable_cong[where f="λx. Sigma_Algebra.measure (κ x) (A ∩ space (κ x))",THEN iffD1,OF refl])
(insert h integrable_bind_kernelD1[OF assms(1) 1] sets_eq_imp_space_eq[OF kernel_sets], auto simp: sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF kernel_sets] sets_bind)
have "AE x in μ. emeasure (κ x) A ≠ ∞"
by(rule nn_integral_PInf_AE,insert h) (auto simp: emeasure_bind_kernel[OF assms(1) _ ne] sets_bind)
hence 0:"AE x in μ. emeasure (κ x) A < ∞"
by (simp add: top.not_eq_extremum)
have "(∫x. (∫y. indicat_real A y *⇩R c ∂κ x)∂ μ) = (∫x. measure (κ x) A *⇩R c∂μ)"
using h integrable_bind_kernelD2[OF assms(1) integrable_real_indicator,of A]
by(auto intro!: integral_cong_AE simp: sets_eq_imp_space_eq[OF kernel_sets] sets_bind sets_eq_imp_space_eq[OF assms(1)])
also have "... = (∫x. measure (κ x) A ∂μ) *⇩R c"
using 2 by(auto intro!: integral_scaleR_left)
finally show ?case
using h by(auto simp: measure_bind_kernel[OF assms(1) _ ne 0] sets_bind)
next
case ih:(add f g)
show ?case
using ih(1,2) integrable_bind_kernelD2[OF assms(1) ih(1)] integrable_bind_kernelD2[OF assms(1) ih(2)]
by(auto simp: ih(3,4) Bochner_Integration.integral_add[OF integrable_bind_kernelD1'[OF assms(1) ih(1)] integrable_bind_kernelD1'[OF assms(1) ih(2)],symmetric] intro!: integral_cong_AE)
next
case ih:(lim f fn)
show ?case (is "?lhs = ?rhs")
proof -
have conv: "AE x in μ. (λn. ∫y. fn n y∂κ x) ⇢ (∫y. f y ∂κ x)"
proof -
have conv:"AE x in μ. integrable (κ x) f ⟶ (λn. ∫y. fn n y∂κ x) ⇢ (∫y. f y ∂κ x)"
proof
fix x
assume h:"x ∈ space μ"
then show "integrable (κ x) f ⟶ (λn. ∫y. fn n y∂κ x) ⇢ (∫y. f y ∂κ x)"
using ih by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f x)"] simp: sets_eq_imp_space_eq[OF sets_bind] sets_eq_imp_space_eq[OF kernel_sets[OF h[simplified sets_eq_imp_space_eq[OF assms(1)]]]] sets_eq_imp_space_eq[OF assms(1)])
qed
with conv integrable_bind_kernelD2[OF assms(1) ih(4)]
show ?thesis by fastforce
qed
have "?lhs = lim (λn. ∫y. fn n y ∂(μ ⤜⇩k κ))"
by(rule limI[OF integral_dominated_convergence[where w="λx. 2 * norm (f x)"],symmetric]) (use ih in auto)
also have "... = lim (λn. (∫x. (∫y. fn n y∂κ x)∂ μ))"
by(simp add: ih)
also have "... = (∫x. lim (λn. ∫y. fn n y∂κ x)∂ μ)"
proof(rule limI[OF integral_dominated_convergence[where w="λx. ∫y. 2 * norm (f y) ∂κ x"]])
fix n
show "AE x in μ. norm (∫y. fn n y∂κ x) ≤ (∫y. 2 * norm (f y) ∂κ x)"
by(rule AE_mp[OF integrable_bind_kernelD2[OF assms(1) ih(1),of n] AE_mp[OF integrable_bind_kernelD2[OF assms(1) ih(4)]]],standard+,rule order.trans[OF integral_norm_bound integral_mono[of "κ _" "λy. norm (fn n y)" _,OF _ _ ih(3)[simplified sets_eq_imp_space_eq[OF sets_bind]]]])
(auto simp: sets_eq_imp_space_eq[OF assms(1)] sets_eq_imp_space_eq[OF kernel_sets])
qed(use ih integrable_bind_kernelD1[OF assms(1) ih(4)] conv limI in auto,fastforce)
also have "... = ?rhs"
using ih conv limI by(auto intro!: integral_cong_AE, blast)
finally show ?thesis .
qed
qed
with 1 show ?thesis
by auto
qed(auto simp: bind_kernel_def space_empty[of μ] sets_eq_imp_space_eq[OF assms(1)] integrable_iff_bounded nn_integral_empty Bochner_Integration.integral_empty)
thus "integrable (μ ⤜⇩k κ) f" ?eq
by auto
qed
end