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