Theory Disc_Cond_Expect
section ‹Discrete Conditional Expectation›
theory Disc_Cond_Expect imports "HOL-Probability.Probability" Generated_Subalgebra
begin
subsection ‹Preliminary measurability results›
text ‹These are some useful results, in particular when working with functions that have a countable
codomain.›
definition disc_fct where
"disc_fct f ≡ countable (range f)"
definition point_measurable where
"point_measurable M S f ≡ (f`(space M)⊆ S) ∧ (∀ r ∈ (range f) ∩ S . f-`{r} ∩ (space M) ∈ sets M)"
lemma singl_meas_if:
assumes "f ∈ space M → space N"
and "∀r∈ range f∩ space N. ∃A∈ sets N. range f∩ A = {r}"
shows "point_measurable (fct_gen_subalgebra M N f) (space N) f" unfolding point_measurable_def
proof
show "f`space (fct_gen_subalgebra M N f)⊆ space N" using assms
by (simp add: Pi_iff fct_gen_subalgebra_space image_subsetI)
show "(∀r∈range f ∩ space N. f -` {r} ∩ space (fct_gen_subalgebra M N f) ∈ sets (fct_gen_subalgebra M N f))"
proof
fix r
assume "r∈ range f ∩ space N"
hence "∃A∈ sets N. range f∩ A = {r}" using assms by blast
from this obtain A where "A∈ sets N" and "range f ∩ A = {r}" by auto note Aprops = this
hence "f-`A = f-`{r}" by auto
hence "f-`A ∩ space M = f-`{r} ∩ space (fct_gen_subalgebra M N f)" by (simp add: fct_gen_subalgebra_space)
thus "f -` {r} ∩ space (fct_gen_subalgebra M N f) ∈ sets (fct_gen_subalgebra M N f)"
using Aprops fct_gen_subalgebra_sets_mem[of A N f M] by simp
qed
qed
lemma meas_single_meas:
assumes "f∈ measurable M N"
and "∀r∈ range f∩ space N. ∃A∈ sets N. range f∩ A = {r}"
shows "point_measurable M (space N) f"
proof -
have "subalgebra M (fct_gen_subalgebra M N f) " using assms fct_gen_subalgebra_is_subalgebra by blast
hence "sets (fct_gen_subalgebra M N f) ⊆ sets M" by (simp add: subalgebra_def)
moreover have "point_measurable (fct_gen_subalgebra M N f) (space N) f" using assms singl_meas_if
by (metis (no_types, lifting) Pi_iff measurable_space)
ultimately show ?thesis
proof -
obtain bb :: "'a measure ⇒ 'b set ⇒ ('a ⇒ 'b) ⇒ 'b" where
f1: "∀m B f. (¬ point_measurable m B f ∨ f ` space m ⊆ B ∧ (∀b. b ∉ range f ∩ B ∨ f -` {b} ∩ space m ∈ sets m)) ∧ (¬ f ` space m ⊆ B ∨ bb m B f ∈ range f ∩ B ∧ f -` {bb m B f} ∩ space m ∉ sets m ∨ point_measurable m B f)"
by (metis (no_types) point_measurable_def)
moreover
{ assume "f -` {bb M (space N) f} ∩ space (fct_gen_subalgebra M N f) ∈ sets (fct_gen_subalgebra M N f)"
then have "f -` {bb M (space N) f} ∩ space M ∈ sets (fct_gen_subalgebra M N f)"
by (metis ‹subalgebra M (fct_gen_subalgebra M N f)› subalgebra_def)
then have "f -` {bb M (space N) f} ∩ space M ∈ sets M"
using ‹sets (fct_gen_subalgebra M N f) ⊆ sets M› by blast
then have "f ` space M ⊆ space N ∧ f -` {bb M (space N) f} ∩ space M ∈ sets M"
using f1 by (metis ‹point_measurable (fct_gen_subalgebra M N f) (space N) f› ‹subalgebra M (fct_gen_subalgebra M N f)› subalgebra_def)
then have ?thesis
using f1 by metis }
ultimately show ?thesis
by (metis (no_types) ‹point_measurable (fct_gen_subalgebra M N f) (space N) f› ‹subalgebra M (fct_gen_subalgebra M N f)› subalgebra_def)
qed
qed
definition countable_preimages where
"countable_preimages B Y = (λn. if ((infinite B) ∨ (finite B ∧ n < card B)) then Y -` {(from_nat_into B) n} else {})"
lemma count_pre_disj:
fixes i::nat
assumes "countable B"
and "i ≠ j"
shows "(countable_preimages B Y) i ∩ (countable_preimages B Y) j = {}"
proof (cases "(countable_preimages B Y) i = {} ∨ (countable_preimages B Y) j = {}")
case True
thus ?thesis by auto
next
case False
hence "Y -` {(from_nat_into B) i} ≠ {} ∧ Y -` {(from_nat_into B) j} ≠ {}" unfolding countable_preimages_def by meson
have "(infinite B) ∨ (finite B ∧ i < card B ∧ j < card B)" using False unfolding countable_preimages_def
by meson
have "(from_nat_into B) i ≠ (from_nat_into B) j"
by (metis False assms(1) assms(2) bij_betw_def countable_preimages_def from_nat_into_inj from_nat_into_inj_infinite lessThan_iff to_nat_on_finite)
thus ?thesis
proof -
have f1: "∀A f n. if infinite A ∨ finite A ∧ n < card A then countable_preimages A f n = f -` {from_nat_into A n::'a} else countable_preimages A f n = ({}::'b set)"
by (meson countable_preimages_def)
then have f2: "infinite B ∨ finite B ∧ i < card B"
by (metis (no_types) False)
have "infinite B ∨ finite B ∧ j < card B"
using f1 by (meson False)
then show ?thesis
using f2 f1 ‹from_nat_into B i ≠ from_nat_into B j› by fastforce
qed
qed
lemma count_pre_surj:
assumes "countable B"
and "w ∈ Y -`B"
shows "∃i. w ∈ (countable_preimages B Y) i"
proof (cases "finite B")
case True
have "∃ i < card B. (from_nat_into B) i = Y w"
by (metis True assms(1) assms(2) bij_betw_def from_nat_into_to_nat_on image_eqI lessThan_iff
to_nat_on_finite vimageE)
from this obtain i where "i< card B" and "(from_nat_into B) i = Y w" by blast
hence "w ∈ (countable_preimages B Y) i"
by (simp add: countable_preimages_def)
thus "∃i. w ∈ (countable_preimages B Y) i" by auto
next
case False
hence "∃ i. (from_nat_into B) i = Y w"
by (meson assms(1) assms(2) from_nat_into_to_nat_on vimageE)
from this obtain i where "(from_nat_into B) i = Y w" by blast
hence "w ∈ (countable_preimages B Y) i"
by (simp add: False countable_preimages_def)
thus "∃i. w ∈ (countable_preimages B Y) i" by auto
qed
lemma count_pre_img:
assumes "x ∈ (countable_preimages B Y) n"
shows "Y x = (from_nat_into B) n"
proof -
have "x∈ Y -` {(from_nat_into B) n}" using assms unfolding countable_preimages_def
by (meson empty_iff)
thus ?thesis by simp
qed
lemma count_pre_union_img:
assumes "countable B"
shows "Y -`B = (⋃ i. (countable_preimages B Y) i)"
proof (cases "B = {}")
case False
have "Y -`B ⊆ (⋃ i. (countable_preimages B Y) i)"
by (simp add: assms count_pre_surj subset_eq)
moreover have "(⋃ i. (countable_preimages B Y) i) ⊆ Y -`B"
proof -
have f1: "∀b A f n. (b::'b) ∉ countable_preimages A f n ∨ (f b::'a) = from_nat_into A n"
by (meson count_pre_img)
have "range (from_nat_into B) = B"
by (meson False assms range_from_nat_into)
then show ?thesis
using f1 by blast
qed
ultimately show ?thesis by simp
next
case True
hence "∀ i. (countable_preimages B Y) i = {}" unfolding countable_preimages_def by simp
hence "(⋃ i. (countable_preimages B Y) i) = {}" by auto
moreover have "Y -`B = {}" using True by simp
ultimately show ?thesis by simp
qed
lemma count_pre_meas:
assumes "point_measurable M (space N) Y"
and "B⊆ space N"
and "countable B"
shows "∀i. (countable_preimages B Y) i ∩ space M ∈ sets M"
proof
fix i
have "Y -`B = (⋃ i. (countable_preimages B Y) i)" using assms
by (simp add: count_pre_union_img)
show "countable_preimages B Y i ∩ space M ∈ sets M"
proof (cases "countable_preimages B Y i = {}")
case True
thus ?thesis by simp
next
case False
from this obtain y where "y ∈ countable_preimages B Y i" by auto
hence "countable_preimages B Y i = Y -`{Y y}"
by (metis False count_pre_img countable_preimages_def)
have "Y y = from_nat_into B i"
by (meson ‹y ∈ countable_preimages B Y i› count_pre_img)
hence "Y y ∈ space N"
by (metis UNIV_I UN_I ‹y ∈ countable_preimages B Y i› ‹Y -`B = (⋃ i. (countable_preimages B Y) i)› assms(2) empty_iff from_nat_into subsetCE vimage_empty)
moreover have "Y y ∈ range Y" by simp
thus ?thesis
by (metis IntI ‹countable_preimages B Y i = Y -` {Y y}› assms(1) calculation point_measurable_def)
qed
qed
lemma disct_fct_point_measurable:
assumes "disc_fct f"
and "point_measurable M (space N) f"
shows "f∈ measurable M N" unfolding measurable_def
proof
show "f ∈ space M → space N ∧ (∀y∈sets N. f -` y ∩ space M ∈ sets M)"
proof
show "f ∈ space M → space N" using assms unfolding point_measurable_def by auto
show "∀y∈sets N. f -` y ∩ space M ∈ sets M"
proof
fix y
assume "y∈ sets N"
let ?imY = "range f ∩ y"
have "f-`y = f-`?imY" by auto
moreover have "countable ?imY" using assms unfolding disc_fct_def by auto
ultimately have "f -`y = (⋃ i. (countable_preimages ?imY f) i)" using assms count_pre_union_img by metis
hence yeq: "f -` y ∩ space M = (⋃ i. ((countable_preimages ?imY f) i) ∩ space M)" by auto
have "∀i. countable_preimages ?imY f i ∩ space M ∈ sets M"
by (metis ‹countable (range f ∩ y)› ‹y ∈ sets N› assms(2) inf_le2 le_inf_iff count_pre_meas sets.Int_space_eq1)
hence "(⋃ i. ((countable_preimages ?imY f) i) ∩ space M) ∈ sets M" by blast
thus "f -` y ∩ space M ∈ sets M" using yeq by simp
qed
qed
qed
lemma set_point_measurable:
assumes "point_measurable M (space N) Y"
and "B ⊆ space N"
and "countable B"
shows "(Y -`B) ∩ space M ∈ sets M"
proof -
have "Y -`B = (⋃ i. (countable_preimages B Y) i)" using assms
by (simp add: count_pre_union_img)
hence "Y -`B ∩ space M = (⋃ i. ((countable_preimages B Y) i ∩ space M))"
by auto
have "∀i. (countable_preimages B Y) i ∩ space M ∈ sets M" using assms by (simp add: count_pre_meas)
hence "(⋃ i. ((countable_preimages B Y) i ∩ space M)) ∈ sets M" by blast
show ?thesis
using ‹(⋃i. countable_preimages B Y i ∩ space M) ∈ sets M› ‹Y -` B ∩ space M = (⋃i. countable_preimages B Y i ∩ space M)› by auto
qed
subsection ‹Definition of explicit conditional expectation›
text ‹This section is devoted to an explicit computation of a conditional expectation for random variables
that have a countable codomain. More precisely, the computed random variable is almost everywhere equal to a conditional
expectation of the random variable under consideration.›
definition img_dce where
"img_dce M Y X = (λ y. if measure M ((Y -` {y}) ∩ space M) = 0 then 0 else
((integral⇧L M (λw. ((X w) * (indicator ((Y -`{y})∩ space M) w))))/(measure M ((Y -` {y}) ∩ space M))))"
definition expl_cond_expect where
"expl_cond_expect M Y X = (img_dce M Y X) ∘ Y"
lemma nn_expl_cond_expect_pos:
assumes "∀w ∈ space M. 0 ≤ X w"
shows "∀ w∈ space M. 0 ≤ (expl_cond_expect M Y X) w"
proof
fix w
assume space: "w∈ space M"
show "0 ≤ (expl_cond_expect M Y X) w"
proof (cases "measure M ((Y -` {Y w})∩ space M) = 0")
case True
thus "0 ≤ (expl_cond_expect M Y X) w" unfolding expl_cond_expect_def img_dce_def by simp
next
case False
hence "Y -`{Y w} ∩ space M ∈ sets M" using measure_notin_sets by blast
let ?indA = "((λ x. indicator ((Y -`{Y w})∩ space M) x))"
have "∀w ∈ space M. 0 ≤ (X w) * (?indA w)" by (simp add: assms)
hence "0 ≤ (integral⇧L M (λw. ((X w) * (?indA w))))" by simp
moreover have "(expl_cond_expect M Y X) w = (integral⇧L M (λw. ((X w) * (?indA w)))) / (measure M ((Y -` {Y w})∩ space M))"
unfolding expl_cond_expect_def img_dce_def using False by simp
moreover have "0 < measure M ((Y -` {Y w}) ∩ space M)" using False by (simp add: zero_less_measure_iff)
ultimately show "0 ≤ (expl_cond_expect M Y X) w" by simp
qed
qed
lemma expl_cond_expect_const:
assumes "Y w = Y y"
shows "expl_cond_expect M Y X w = expl_cond_expect M Y X y"
unfolding expl_cond_expect_def img_dce_def
by (simp add: assms)
lemma expl_cond_exp_cong:
assumes "∀w∈space M. X w = Z w"
shows "∀w∈ space M. expl_cond_expect M Y X w = expl_cond_expect M Y Z w" unfolding expl_cond_expect_def img_dce_def
by (metis (no_types, lifting) Bochner_Integration.integral_cong assms(1) o_apply)
lemma expl_cond_exp_add:
assumes "integrable M X"
and "integrable M Z"
shows "∀w∈ space M. expl_cond_expect M Y (λx. X x + Z x) w = expl_cond_expect M Y X w + expl_cond_expect M Y Z w"
proof
fix w
assume "w∈ space M"
define prY where "prY = measure M ((Y -` {Y w}) ∩ space M)"
show "expl_cond_expect M Y (λx. X x + Z x) w = expl_cond_expect M Y X w + expl_cond_expect M Y Z w"
proof (cases "prY = 0")
case True
thus ?thesis unfolding expl_cond_expect_def img_dce_def prY_def by simp
next
case False
hence "(Y -` {Y w}) ∩ space M ∈ sets M" unfolding prY_def using measure_notin_sets by blast
let ?indA = "indicator ((Y -` {Y w}) ∩ space M)::('a⇒real)"
have "integrable M (λx. X x * ?indA x)"
using ‹Y -` {Y w} ∩ space M ∈ sets M› assms(1) integrable_real_mult_indicator by blast
moreover have "integrable M (λx. Z x * ?indA x)"
using ‹Y -` {Y w} ∩ space M ∈ sets M› assms(2) integrable_real_mult_indicator by blast
ultimately have "integral⇧L M (λx. X x * ?indA x + Z x * ?indA x) = integral⇧L M (λx. X x * ?indA x) + integral⇧L M (λx. Z x * ?indA x)"
using Bochner_Integration.integral_add by blast
moreover have "∀x∈ space M. X x * ?indA x + Z x * ?indA x = (X x + Z x) * ?indA x"
by (simp add: indicator_def)
ultimately have fsteq: "integral⇧L M (λx. (X x + Z x) * ?indA x) = integral⇧L M (λx. X x * ?indA x) + integral⇧L M (λx. Z x * ?indA x)"
by (metis (no_types, lifting) Bochner_Integration.integral_cong)
have "integral⇧L M (λx. (X x + Z x) * ?indA x/prY) = integral⇧L M (λx. (X x + Z x) * ?indA x)/prY"
by simp
also have "... = integral⇧L M (λx. X x * ?indA x)/prY + integral⇧L M (λx. Z x * ?indA x)/prY" using fsteq
by (simp add: add_divide_distrib)
also have "... = integral⇧L M (λx. X x * ?indA x/prY) + integral⇧L M (λx. Z x * ?indA x/prY)" by auto
finally have "integral⇧L M (λx. (X x + Z x) * ?indA x/prY) = integral⇧L M (λx. X x * ?indA x/prY) + integral⇧L M (λx. Z x * ?indA x/prY)" .
thus ?thesis using False unfolding expl_cond_expect_def img_dce_def
by (simp add: add_divide_distrib fsteq)
qed
qed
lemma expl_cond_exp_diff:
assumes "integrable M X"
and "integrable M Z"
shows "∀w∈ space M. expl_cond_expect M Y (λx. X x - Z x) w = expl_cond_expect M Y X w - expl_cond_expect M Y Z w"
proof
fix w
assume "w∈ space M"
define prY where "prY = measure M ((Y -` {Y w}) ∩ space M)"
show "expl_cond_expect M Y (λx. X x - Z x) w = expl_cond_expect M Y X w - expl_cond_expect M Y Z w"
proof (cases "prY = 0")
case True
thus ?thesis unfolding expl_cond_expect_def img_dce_def prY_def by simp
next
case False
hence "(Y -` {Y w}) ∩ space M ∈ sets M" unfolding prY_def using measure_notin_sets by blast
let ?indA = "indicator ((Y -` {Y w}) ∩ space M)::('a⇒real)"
have "integrable M (λx. X x * ?indA x)"
using ‹Y -` {Y w} ∩ space M ∈ sets M› assms(1) integrable_real_mult_indicator by blast
moreover have "integrable M (λx. Z x * ?indA x)"
using ‹Y -` {Y w} ∩ space M ∈ sets M› assms(2) integrable_real_mult_indicator by blast
ultimately have "integral⇧L M (λx. X x * ?indA x - Z x * ?indA x) = integral⇧L M (λx. X x * ?indA x) - integral⇧L M (λx. Z x * ?indA x)"
using Bochner_Integration.integral_diff by blast
moreover have "∀x∈ space M. X x * ?indA x - Z x * ?indA x = (X x - Z x) * ?indA x"
by (simp add: indicator_def)
ultimately have fsteq: "integral⇧L M (λx. (X x - Z x) * ?indA x) = integral⇧L M (λx. X x * ?indA x) - integral⇧L M (λx. Z x * ?indA x)"
by (metis (no_types, lifting) Bochner_Integration.integral_cong)
have "integral⇧L M (λx. (X x - Z x) * ?indA x/prY) = integral⇧L M (λx. (X x - Z x) * ?indA x)/prY"
by simp
also have "... = integral⇧L M (λx. X x * ?indA x)/prY - integral⇧L M (λx. Z x * ?indA x)/prY" using fsteq
by (simp add: diff_divide_distrib)
also have "... = integral⇧L M (λx. X x * ?indA x/prY) - integral⇧L M (λx. Z x * ?indA x/prY)" by auto
finally have "integral⇧L M (λx. (X x - Z x) * ?indA x/prY) = integral⇧L M (λx. X x * ?indA x/prY) - integral⇧L M (λx. Z x * ?indA x/prY)" .
thus ?thesis using False unfolding expl_cond_expect_def img_dce_def
by (simp add: diff_divide_distrib fsteq)
qed
qed
lemma expl_cond_expect_prop_sets:
assumes "disc_fct Y"
and "point_measurable M (space N) Y"
and "D = {w∈ space M. Y w ∈ space N ∧ (P (expl_cond_expect M Y X w))}"
shows "D∈ sets M"
proof -
let ?C = "{y ∈ (Y`(space M)) ∩ (space N). P (img_dce M Y X y)}"
have "space M ⊆ UNIV" by simp
hence "Y`(space M) ⊆ range Y" by auto
hence "countable (Y`(space M))" using assms countable_subset unfolding disc_fct_def by auto
hence "countable ?C" using assms unfolding disc_fct_def by auto
have eqset: "D = (⋃ b∈ ?C. Y-`{b})∩ space M"
proof
show "D⊆ (⋃ b∈ ?C. Y-`{b})∩ space M"
proof
fix w
assume "w∈ D"
hence "w∈ space M ∧ Y w ∈ (space N) ∧ (P (expl_cond_expect M Y X w))"
by (simp add: assms)
hence "P (img_dce M Y X (Y w))" by (simp add: expl_cond_expect_def)
hence "Y w ∈ ?C" using ‹w ∈ space M ∧ Y w ∈ space N ∧ P (expl_cond_expect M Y X w)› by blast
thus "w∈ (⋃ b∈ ?C. Y-`{b})∩ space M"
using ‹w ∈ space M ∧ Y w ∈ space N ∧ P (expl_cond_expect M Y X w)› by blast
qed
show "(⋃ b∈ ?C. Y-`{b})∩ space M ⊆ D"
proof
fix w
assume "w∈ (⋃ b∈ ?C. Y-`{b})∩ space M"
from this obtain b where "b∈ ?C ∧ w∈ Y-`{b}" by auto note bprops = this
hence "Y w = b" by auto
hence "Y w∈ space N" using bprops by simp
show "w ∈ D"
by (metis (mono_tags, lifting) IntE ‹Y w = b› ‹w ∈ (⋃b∈?C. Y -` {b}) ∩ space M› assms(3)
bprops mem_Collect_eq o_apply expl_cond_expect_def)
qed
qed
also have "... = (⋃ b∈ ?C. Y-`{b}∩ space M)" by blast
finally have "D = (⋃ b∈ ?C. Y-`{b}∩ space M)".
have "∀b∈ ?C. Y-`{b} ∩ space M ∈ sets M" using assms unfolding point_measurable_def by auto
hence "(⋃ b∈ ?C. Y-`{b}∩ space M) ∈ sets M" using ‹countable ?C› by blast
thus ?thesis
using ‹D = (⋃b∈?C. Y -` {b} ∩ space M)› by blast
qed
lemma expl_cond_expect_prop_sets2:
assumes "disc_fct Y"
and "point_measurable (fct_gen_subalgebra M N Y) (space N) Y"
and "D = {w∈ space M. Y w ∈ space N ∧ (P (expl_cond_expect M Y X w))}"
shows "D∈ sets (fct_gen_subalgebra M N Y)"
proof -
let ?C = "{y ∈ (Y`(space M)) ∩ (space N). P (img_dce M Y X y)}"
have "space M ⊆ UNIV" by simp
hence "Y`(space M) ⊆ range Y" by auto
hence "countable (Y`(space M))" using assms countable_subset unfolding disc_fct_def by auto
hence "countable ?C" using assms unfolding disc_fct_def by auto
have eqset: "D = (⋃ b∈ ?C. Y-`{b})∩ space M"
proof
show "D⊆ (⋃ b∈ ?C. Y-`{b})∩ space M"
proof
fix w
assume "w∈ D"
hence "w∈ space M ∧ Y w ∈ (space N) ∧ (P (expl_cond_expect M Y X w))"
by (simp add: assms)
hence "P (img_dce M Y X (Y w))" by (simp add: expl_cond_expect_def)
hence "Y w ∈ ?C" using ‹w ∈ space M ∧ Y w ∈ space N ∧ P (expl_cond_expect M Y X w)› by blast
thus "w∈ (⋃ b∈ ?C. Y-`{b})∩ space M"
using ‹w ∈ space M ∧ Y w ∈ space N ∧ P (expl_cond_expect M Y X w)› by blast
qed
show "(⋃ b∈ ?C. Y-`{b})∩ space M ⊆ D"
proof
fix w
assume "w∈ (⋃ b∈ ?C. Y-`{b})∩ space M"
from this obtain b where "b∈ ?C ∧ w∈ Y-`{b}" by auto note bprops = this
hence "Y w = b" by auto
hence "Y w∈ space N" using bprops by simp
show "w ∈ D"
by (metis (mono_tags, lifting) IntE ‹Y w = b› ‹w ∈ (⋃b∈?C. Y -` {b}) ∩ space M› assms(3)
bprops mem_Collect_eq o_apply expl_cond_expect_def)
qed
qed
also have "... = (⋃ b∈ ?C. Y-`{b}∩ space M)" by blast
finally have "D = (⋃ b∈ ?C. Y-`{b}∩ space M)".
have "space M = space (fct_gen_subalgebra M N Y)"
by (simp add: fct_gen_subalgebra_space)
hence "∀b∈ ?C. Y-`{b} ∩ space M ∈ sets (fct_gen_subalgebra M N Y)" using assms unfolding point_measurable_def by auto
hence "(⋃ b∈ ?C. Y-`{b}∩ space M) ∈ sets (fct_gen_subalgebra M N Y)" using ‹countable ?C› by blast
thus ?thesis
using ‹D = (⋃b∈?C. Y -` {b} ∩ space M)› by blast
qed
lemma expl_cond_expect_disc_fct:
assumes "disc_fct Y"
shows "disc_fct (expl_cond_expect M Y X)"
using assms unfolding disc_fct_def expl_cond_expect_def
by (metis countable_image image_comp)
lemma expl_cond_expect_point_meas:
assumes "disc_fct Y"
and "point_measurable M (space N) Y"
shows "point_measurable M UNIV (expl_cond_expect M Y X)"
proof -
have "disc_fct (expl_cond_expect M Y X)" using assms by (simp add: expl_cond_expect_disc_fct)
show ?thesis unfolding point_measurable_def
proof
show "(expl_cond_expect M Y X)`space M ⊆ UNIV" by simp
show "∀r∈range (expl_cond_expect M Y X) ∩ UNIV. expl_cond_expect M Y X -` {r} ∩ space M ∈ sets M"
proof
fix r
assume "r∈ range (expl_cond_expect M Y X) ∩ UNIV"
let ?D = "{w ∈ space M. Y w ∈ space N ∧ (expl_cond_expect M Y X w) = r}"
have "?D ∈ sets M" using expl_cond_expect_prop_sets[of Y M N ?D "λx. x = r" X] using assms by simp
moreover have "expl_cond_expect M Y X -`{r}∩ space M = ?D"
proof
show "expl_cond_expect M Y X -`{r}∩ space M ⊆ ?D"
proof
fix w
assume "w∈ expl_cond_expect M Y X -`{r}∩ space M"
hence "Y w ∈ space N"
by (meson IntD2 assms(1) assms(2) disct_fct_point_measurable measurable_space)
thus "w ∈ ?D"
using ‹w ∈ expl_cond_expect M Y X -` {r} ∩ space M› by blast
qed
show "?D ⊆ expl_cond_expect M Y X -`{r}∩ space M"
proof
fix w
assume "w∈ ?D"
thus "w∈ expl_cond_expect M Y X -`{r}∩ space M" by blast
qed
qed
ultimately show "expl_cond_expect M Y X -` {r} ∩ space M ∈ sets M" by simp
qed
qed
qed
lemma expl_cond_expect_borel_measurable:
assumes "disc_fct Y"
and "point_measurable M (space N) Y"
shows "(expl_cond_expect M Y X) ∈ borel_measurable M" using expl_cond_expect_point_meas[of Y M] assms
disct_fct_point_measurable[of "expl_cond_expect M Y X"]
by (simp add: expl_cond_expect_disc_fct)
lemma expl_cond_exp_borel:
assumes "Y ∈ space M → space N"
and "disc_fct Y"
and "∀r∈ range Y∩ space N. ∃A∈ sets N. range Y∩ A = {r}"
shows "(expl_cond_expect M Y X) ∈ borel_measurable (fct_gen_subalgebra M N Y)"
proof (intro borel_measurableI)
fix S::"real set"
assume "open S"
show "expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y) ∈ sets (fct_gen_subalgebra M N Y)"
proof (rule expl_cond_expect_prop_sets2)
show "disc_fct Y" using assms by simp
show "point_measurable (fct_gen_subalgebra M N Y) (space N) Y" using assms
by (simp add: singl_meas_if)
show "expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y) = {w ∈ space M. Y w ∈ space N ∧ (expl_cond_expect M Y X w) ∈ S}"
proof
show " expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y) ⊆ {w ∈ space M. Y w ∈ space N ∧ expl_cond_expect M Y X w ∈ S}"
proof
fix x
assume asm: "x ∈ expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y)"
hence "expl_cond_expect M Y X x ∈ S" by auto
moreover have "x∈ space M" using asm by (simp add:fct_gen_subalgebra_space)
ultimately show "x ∈{w ∈ space M. Y w ∈ space N ∧ expl_cond_expect M Y X w ∈ S}" using assms by auto
qed
show "{w ∈ space M. Y w ∈ space N ∧ expl_cond_expect M Y X w ∈ S} ⊆ expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y)"
proof
fix x
assume asm2: "x ∈ {w ∈ space M. Y w ∈ space N ∧ expl_cond_expect M Y X w ∈ S}"
hence "x∈ space (fct_gen_subalgebra M N Y)" by (simp add:fct_gen_subalgebra_space)
moreover have "x ∈ expl_cond_expect M Y X -`S" using asm2 by simp
ultimately show "x ∈ expl_cond_expect M Y X -` S ∩ space (fct_gen_subalgebra M N Y)" by simp
qed
qed
qed
qed
lemma expl_cond_expect_indic_borel_measurable:
assumes "disc_fct Y"
and "point_measurable M (space N) Y"
and "B⊆ space N"
and "countable B"
shows "(λw. expl_cond_expect M Y X w * indicator (countable_preimages B Y n ∩ space M) w)∈ borel_measurable M"
proof -
have "countable_preimages B Y n ∩ space M ∈ sets M" using assms by (auto simp add: count_pre_meas)
have "(expl_cond_expect M Y X)∈ borel_measurable M" using expl_cond_expect_point_meas[of Y M N X] assms
disct_fct_point_measurable[of "expl_cond_expect M Y X"]
by (simp add: expl_cond_expect_disc_fct)
moreover have "(indicator (countable_preimages B Y n ∩ space M))∈ borel_measurable M"
using ‹countable_preimages B Y n ∩ space M ∈ sets M› borel_measurable_indicator by blast
ultimately show ?thesis
using borel_measurable_times by blast
qed
lemma (in finite_measure) dce_prod:
assumes "point_measurable M (space N) Y"
and "integrable M X"
and "∀ w∈ space M. 0 ≤ X w"
shows "∀ w. (Y w) ∈ space N ⟶ (expl_cond_expect M Y X) w * measure M ((Y -` {Y w})∩ space M) = integral⇧L M (λy. (X y) * (indicator ((Y -`{Y w})∩ space M) y))"
proof (intro allI impI)
fix w
assume "Y w∈ space N"
let ?indY = "(λy. indicator ((Y -`{Y w})∩ space M) y)::'a ⇒ real"
show "expl_cond_expect M Y X w * measure M ((Y -` {Y w})∩ space M) = integral⇧L M (λy. (X y) * ?indY y) "
proof (cases "AE y in M. ?indY y = 0")
case True
hence "emeasure M ((Y -` {Y w})∩ space M) = 0"
proof -
have "AE y in M. y ∉ Y -` {Y w} ∩ space M"
using True eventually_elim2 by auto
hence "∃N∈ null_sets M.{x∈ space M. ¬(x∉ Y -` {Y w} ∩ space M)} ⊆ N"
using eventually_ae_filter[of "λx. x ∉ Y -` {Y w} ∩ space M" M] by simp
hence "∃N∈ null_sets M. {x∈ space M. x∈ Y -` {Y w} ∩ space M} ⊆ N" by simp
from this obtain N where "N∈ null_sets M" and "{x∈ space M. x∈ Y -` {Y w} ∩ space M} ⊆ N" by auto
note Nprops = this
have "{x∈ space M. x∈ Y -` {Y w}} ⊆ N" using Nprops by auto
hence "emeasure M {x∈ space M. x∈ Y -` {Y w}} ≤ emeasure M N"
by (simp add: emeasure_mono Nprops(1) null_setsD2)
thus ?thesis
by (metis (no_types, lifting) Collect_cong Int_def Nprops(1) le_zero_eq null_setsD1)
qed
hence "enn2real (emeasure M ((Y -` {Y w})∩ space M)) = 0" by simp
hence "measure M ((Y -` {Y w})∩ space M) = 0" unfolding measure_def by simp
hence lhs: "expl_cond_expect M Y X w = 0" unfolding expl_cond_expect_def img_dce_def by simp
have zer: "AE y in M. (X y) * ?indY y = (λy. 0) y" using True by auto
hence rhs: "integral⇧L M (λy. (X y) * ?indY y) = 0"
proof -
have "∀ w∈ space M. 0 ≤ X w * ?indY w" using assms by simp
have "integrable M (λy. (X y) * ?indY y)" using assms
by (metis (mono_tags, lifting) IntI UNIV_I ‹Y w ∈ space N› image_eqI Bochner_Integration.integrable_cong integrable_real_mult_indicator point_measurable_def)
hence "(λy. (X y) * ?indY y) ∈ borel_measurable M" by blast
thus ?thesis using zer integral_cong_AE[of "(λy. (X y) * ?indY y)" M "λy. 0"] by simp
qed
thus "expl_cond_expect M Y X w*measure M ((Y -` {Y w})∩ space M) = integral⇧L M (λy. (X y) * ?indY y)" using lhs rhs by simp
next
case False
hence "¬(AE y in M. y ∉ (Y -`{Y w})∩ space M)"
by (simp add: indicator_eq_0_iff)
hence "emeasure M ((Y -` {Y w})∩ space M) ≠ 0"
proof -
have "(Y -` {Y w})∩ space M∈ sets M"
by (meson IntI UNIV_I ‹Y w ∈ space N› assms(1) image_eqI point_measurable_def)
have "(Y -` {Y w})∩ space M ∉ null_sets M"
using ‹¬ (AE y in M. y ∉ Y -` {Y w} ∩ space M)› eventually_ae_filter by blast
thus ?thesis
using ‹Y -` {Y w} ∩ space M ∈ sets M› by blast
qed
hence "measure M ((Y -` {Y w})∩ space M) ≠ 0"
by (simp add: emeasure_eq_measure)
thus "expl_cond_expect M Y X w* measure M ((Y -` {Y w})∩ space M) = integral⇧L M (λy. (X y) * ?indY y)" unfolding expl_cond_expect_def img_dce_def
using o_apply by auto
qed
qed
lemma expl_cond_expect_const_exp:
shows "integral⇧L M (λy. expl_cond_expect M Y X w * (indicator (Y -` {Y w} ∩ space M)) y) =
integral⇧L M (λy. expl_cond_expect M Y X y * (indicator (Y -` {Y w} ∩ space M)) y)"
proof -
let ?ind = "(indicator (Y -` {Y w} ∩ space M))"
have "∀ y∈ space M. expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof
fix y
assume "y∈ space M"
show "expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof (cases "y∈ Y -` {Y w} ∩ space M")
case False
thus ?thesis by simp
next
case True
hence "Y w = Y y" by auto
hence "expl_cond_expect M Y X w = expl_cond_expect M Y X y"
using expl_cond_expect_const[of Y w y M X] by simp
thus ?thesis by simp
qed
qed
thus ?thesis
by (meson Bochner_Integration.integral_cong)
qed
lemma nn_expl_cond_expect_const_exp:
assumes "∀w∈ space M. 0 ≤ X w"
shows "integral⇧N M (λy. expl_cond_expect M Y X w * (indicator (Y -` {Y w} ∩ space M)) y) =
integral⇧N M (λy. expl_cond_expect M Y X y * (indicator (Y -` {Y w} ∩ space M)) y)"
proof -
let ?ind = "(indicator (Y -` {Y w} ∩ space M))"
have forall: "∀ y∈ space M. expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof
fix y
assume "y∈ space M"
show "expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof (cases "y∈ Y -` {Y w} ∩ space M")
case False
thus ?thesis by simp
next
case True
hence "Y w = Y y" by auto
hence "expl_cond_expect M Y X w = expl_cond_expect M Y X y"
using expl_cond_expect_const[of Y] by blast
thus ?thesis by simp
qed
qed
show ?thesis
by (metis (no_types, lifting) forall nn_integral_cong)
qed
lemma (in finite_measure) nn_expl_cond_bounded:
assumes "∀w∈ space M. 0 ≤ X w"
and "integrable M X"
and "point_measurable M (space N) Y"
and "w∈ space M"
and "Y w∈ space N"
shows "integral⇧N M (λy. expl_cond_expect M Y X y * (indicator (Y -` {Y w} ∩ space M)) y) < ∞"
proof -
let ?ind = "(indicator (Y -` {Y w} ∩ space M))::'a⇒real"
have "0 ≤ expl_cond_expect M Y X w" using assms nn_expl_cond_expect_pos[of M X Y] by simp
have "integrable M (λy. expl_cond_expect M Y X w * ?ind y)"
proof -
have eq: "(Y -`{Y w} ∩ space M) ∩ space M = (Y -`{Y w} ∩ space M)" by auto
have "(Y -` {Y w} ∩ space M) ∈ sets M" using assms
by (simp add: point_measurable_def)
moreover have "emeasure M (Y -`{Y w} ∩ space M) < ∞" by (simp add: inf.strict_order_iff)
ultimately have "integrable M (λy. ?ind y)"
using integrable_indicator_iff[of M "(Y -`{Y w} ∩ space M)"] by simp
thus ?thesis using integrable_mult_left_iff[of M "expl_cond_expect M Y X w" "?ind"] by blast
qed
have "∀y∈ space M. 0 ≤ expl_cond_expect M Y X w * ?ind y"
using ‹0 ≤ expl_cond_expect M Y X w› mult_nonneg_nonneg by blast
hence "∀y∈ space M. expl_cond_expect M Y X w * ?ind y = norm (expl_cond_expect M Y X w * ?ind y)" by auto
hence inf: "integral⇧N M (λy. expl_cond_expect M Y X w * ?ind y) < ∞"
using integrable_iff_bounded[of M "(λy. expl_cond_expect M Y X w * ?ind y)"]
‹0 ≤ expl_cond_expect M Y X w› real_norm_def nn_integral_cong
by (metis (no_types, lifting) ‹integrable M (λy. expl_cond_expect M Y X w * indicator (Y -` {Y w} ∩ space M) y)›)
have "integral⇧N M (λy. expl_cond_expect M Y X y * ?ind y) =
integral⇧N M (λy. expl_cond_expect M Y X w * ?ind y)" using assms
by (simp add: nn_expl_cond_expect_const_exp)
also have "... < ∞" using inf by simp
finally show ?thesis .
qed
lemma (in finite_measure) count_prod:
fixes Y::"'a⇒'b"
assumes "B⊆ space N"
and "point_measurable M (space N) Y"
and "integrable M X"
and "∀ w ∈ space M. 0 ≤ X w"
shows "∀i. integral⇧L M (λy. (X y) * (indicator (countable_preimages B Y i ∩ space M)) y) =
integral⇧L M (λy. (expl_cond_expect M Y X y) * (indicator (countable_preimages B Y i ∩ space M)) y)"
proof
fix i
show "integral⇧L M (λy. X y * indicator (countable_preimages B Y i ∩ space M) y) =
integral⇧L M (λy. expl_cond_expect M Y X y * indicator (countable_preimages B Y i ∩ space M) y)"
proof (cases "countable_preimages B Y i ∩ space M = {}")
case True
thus ?thesis by simp
next
case False
from this obtain w where "w∈ countable_preimages B Y i" by auto
hence "Y w = (from_nat_into B) i" by (meson count_pre_img)
hence "Y w ∈ B"
proof (cases "infinite B")
case True
thus ?thesis
by (simp add: ‹Y w = from_nat_into B i› from_nat_into infinite_imp_nonempty)
next
case False
thus ?thesis
by (metis Finite_Set.card_0_eq ‹Y w = from_nat_into B i› ‹w ∈ countable_preimages B Y i› countable_preimages_def equals0D from_nat_into gr_implies_not0)
qed
let ?ind = "(indicator (Y -` {Y w} ∩ space M))::'a⇒real"
have "integral⇧L M (λy. (X y) * (indicator (countable_preimages B Y i ∩ space M)) y) = integral⇧L M (λy. X y * ?ind y)"
by (metis (no_types, opaque_lifting) ‹Y w = from_nat_into B i› ‹⋀thesis. (⋀w. w ∈ countable_preimages B Y i ⟹ thesis) ⟹ thesis› countable_preimages_def empty_iff)
also have "... =
expl_cond_expect M Y X w * measure M (Y -` {Y w} ∩ space M)" using dce_prod[of N Y X]
by (metis (no_types, lifting) ‹Y w ∈ B› assms subsetCE)
also have "... = expl_cond_expect M Y X w * (integral⇧L M ?ind)"
by auto
also have "... = integral⇧L M (λy. expl_cond_expect M Y X w * ?ind y)"
by auto
also have "... = integral⇧L M (λy. expl_cond_expect M Y X y * ?ind y)"
proof -
have "∀ y∈ space M. expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof
fix y
assume "y∈ space M"
show "expl_cond_expect M Y X w * ?ind y = expl_cond_expect M Y X y * ?ind y"
proof (cases "y∈ Y -` {Y w} ∩ space M")
case False
thus ?thesis by simp
next
case True
hence "Y w = Y y" by auto
hence "expl_cond_expect M Y X w = expl_cond_expect M Y X y"
using expl_cond_expect_const[of Y] by blast
thus ?thesis by simp
qed
qed
thus ?thesis
by (meson Bochner_Integration.integral_cong)
qed
also have "... = integral⇧L M (λy. expl_cond_expect M Y X y * indicator (countable_preimages B Y i ∩ space M) y)"
by (metis (no_types, opaque_lifting) ‹Y w = from_nat_into B i› ‹⋀thesis. (⋀w. w ∈ countable_preimages B Y i ⟹ thesis) ⟹ thesis› countable_preimages_def empty_iff)
finally show ?thesis .
qed
qed
lemma (in finite_measure) count_pre_integrable:
assumes "point_measurable M (space N) Y"
and "disc_fct Y"
and "B⊆ space N"
and "countable B"
and "integrable M X"
and "∀ w ∈ space M. 0 ≤ X w"
shows "integrable M (λw. expl_cond_expect M Y X w * indicator (countable_preimages B Y n ∩ space M) w)"
proof-
have "integral⇧L M (λy. (X y) * (indicator (countable_preimages B Y n ∩ space M)) y) =
integral⇧L M (λy. (expl_cond_expect M Y X y) * (indicator (countable_preimages B Y n ∩ space M)) y)" using assms count_prod
by blast
have "∀w ∈ space M. 0 ≤ (expl_cond_expect M Y X w) * (indicator (countable_preimages B Y n ∩ space M)) w"
by (simp add: assms nn_expl_cond_expect_pos)
have "countable_preimages B Y n ∩ space M ∈ sets M" using count_pre_meas[of M] assms by auto
hence "integrable M (λw. X w * indicator (countable_preimages B Y n ∩ space M) w)"
using assms integrable_real_mult_indicator by blast
show ?thesis
proof (rule integrableI_nonneg)
show "(λw. expl_cond_expect M Y X w * indicator (countable_preimages B Y n ∩ space M) w)∈ borel_measurable M"
proof -
have "(expl_cond_expect M Y X)∈ borel_measurable M" using expl_cond_expect_point_meas[of Y M N X] assms
disct_fct_point_measurable[of "expl_cond_expect M Y X"]
by (simp add: expl_cond_expect_disc_fct)
moreover have "(indicator (countable_preimages B Y n ∩ space M))∈ borel_measurable M"
using ‹countable_preimages B Y n ∩ space M ∈ sets M› borel_measurable_indicator by blast
ultimately show ?thesis
using borel_measurable_times by blast
qed
show "AE x in M. 0 ≤ expl_cond_expect M Y X x * indicator (countable_preimages B Y n ∩ space M) x"
by (simp add: ‹∀w∈space M. 0 ≤ expl_cond_expect M Y X w * indicator (countable_preimages B Y n ∩ space M) w›)
show "(∫⇧+ x. ennreal (expl_cond_expect M Y X x * indicator (countable_preimages B Y n ∩ space M) x) ∂M) < ∞"
proof (cases "countable_preimages B Y n ∩ space M = {}")
case True
thus ?thesis by simp
next
case False
from this obtain w where "w∈ countable_preimages B Y n∩ space M" by auto
hence "countable_preimages B Y n = Y -`{Y w}"
by (metis IntD1 count_pre_img countable_preimages_def equals0D)
have "w∈ space M" using False
using ‹w ∈ countable_preimages B Y n ∩ space M› by blast
moreover have "Y w ∈ space N"
by (meson ‹w ∈ space M› assms(1) assms(2) disct_fct_point_measurable measurable_space)
ultimately show ?thesis using assms nn_expl_cond_bounded[of X N Y]
using ‹countable_preimages B Y n = Y -` {Y w}› by presburger
qed
qed
qed
lemma (in finite_measure) nn_cond_expl_is_cond_exp_tmp:
assumes "∀ w∈ space M. 0 ≤ X w"
and "integrable M X"
and "disc_fct Y"
and "point_measurable M (space M') Y"
shows "∀ A ∈ sets M'. integrable M (λw. ((expl_cond_expect M Y X) w) * (indicator ((Y -`A)∩ (space M)) w)) ∧
integral⇧L M (λw. (X w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator ((Y -`A) ∩ (space M))) w)"
proof
fix A
assume "A ∈ sets M'"
let ?imA = "A ∩ (range Y)"
have "countable ?imA" using assms disc_fct_def by blast
have "Y -`A = Y -`?imA" by auto
define prY where "prY = countable_preimages ?imA Y"
have un: "Y -`?imA = (⋃ i. prY i)" using ‹countable ?imA›
by (metis count_pre_union_img prY_def)
have "(Y -`?imA) ∩ (space M) = (⋃ i. prY i) ∩ (space M)" using ‹Y -`A = Y -`?imA› un by simp
also have "... = (⋃ i. (prY i) ∩ (space M))" by blast
finally have eq2: "(Y -`?imA) ∩ (space M) = (⋃ i. (prY i) ∩ (space M))".
define indpre::"nat ⇒ 'a ⇒ real" where "indpre = (λ i x. (indicator ((prY i) ∩ (space M))) x)"
have "∀ i. indpre i ∈ borel_measurable M"
proof
fix i
show "indpre i ∈ borel_measurable M" unfolding indpre_def prY_def
proof (rule borel_measurable_indicator, cases "countable_preimages (A ∩ range Y) Y i ∩ space M = {}")
case True
thus "countable_preimages (A ∩ range Y) Y i ∩ space M ∈ sets M" by simp
next
case False
from this obtain x where "x∈ countable_preimages (A ∩ range Y) Y i ∩ space M" by blast
hence "Y x ∈ space M'"
by (metis Int_iff UN_I ‹A ∈ sets M'› ‹prY ≡ countable_preimages (A ∩ range Y) Y› imageE
rangeI sets.sets_into_space subset_eq un vimage_eq)
thus "countable_preimages (A ∩ range Y) Y i ∩ space M ∈ sets M"
by (metis IntE IntI ‹x ∈ countable_preimages (A ∩ range Y) Y i ∩ space M› assms(4)
count_pre_img countable_preimages_def empty_iff point_measurable_def rangeI)
qed
qed
have "∀i. integrable M (λw. (X w) * indpre i w)"
proof
fix i
show "integrable M (λw. (X w) * indpre i w)" unfolding indpre_def prY_def
proof (rule integrable_real_mult_indicator)
show "countable_preimages (A ∩ range Y) Y i ∩ space M ∈ sets M"
proof (cases "countable_preimages (A ∩ range Y) Y i = {}")
case True
thus "countable_preimages (A ∩ range Y) Y i ∩ space M ∈ sets M" by (simp add: True)
next
case False
hence "Y -` {(from_nat_into (A ∩ range Y)) i} ≠ {}" unfolding countable_preimages_def by meson
have "(infinite (A ∩ range Y)) ∨ (finite (A ∩ range Y) ∧ i < card (A ∩ range Y))" using False unfolding countable_preimages_def
by meson
show ?thesis
by (metis ‹A ∈ sets M'› ‹countable (A ∩ range Y)› assms(4) count_pre_meas le_inf_iff
range_from_nat_into sets.Int_space_eq1 sets.empty_sets sets.sets_into_space subset_range_from_nat_into)
qed
show "integrable M X" using assms by simp
qed
qed
hence prod_bm: "∀ i. (λw. (X w) * indpre i w) ∈ borel_measurable M"
by (simp add: assms(2) borel_measurable_integrable borel_measurable_times)
have posprod: "∀ i w. 0 ≤ (X w) * indpre i w"
proof (intro allI)
fix i
fix w
show "0 ≤ (X w) * indpre i w"
by (metis IntE assms(1) indicator_pos_le indicator_simps(2) indpre_def mult_eq_0_iff mult_sign_intros(1))
qed
let ?indA = "indicator ((Y -`(A ∩ range Y))∩ (space M))::'a⇒real"
have "∀ i j. i ≠ j ⟶ ((prY i) ∩ (space M)) ∩ ((prY j) ∩ (space M)) = {}"
by (simp add: ‹countable (A ∩ range Y)› ‹prY ≡ countable_preimages (A ∩ range Y) Y› count_pre_disj inf_commute inf_sup_aci(3))
hence sumind: "∀x. (λi. indpre i x) sums ?indA x" using ‹countable ?imA› eq2 unfolding prY_def indpre_def
by (metis indicator_sums)
hence sumxlim: "∀x. (λi. (X x) * indpre i x::real) sums ((X x) * indicator ((Y -`?imA) ∩ (space M)) x)" using ‹countable ?imA› unfolding prY_def
using sums_mult by blast
hence sum: "∀x. (∑ i.((X x) * indpre i x)::real) = (X x) * indicator ((Y -`?imA) ∩ (space M)) x" by (metis sums_unique)
hence b: "∀ w. 0 ≤ (∑ i.((X w) * indpre i w))" using suminf_nonneg
by (metis ‹∀x. (λi. X x * indpre i x) sums (X x * indicator (Y -` (A ∩ range Y) ∩ space M) x)› posprod summable_def)
have sumcondlim: "∀x. (λi. (expl_cond_expect M Y X x) * indpre i x::real) sums ((expl_cond_expect M Y X x) * ?indA x)" using ‹countable ?imA› unfolding prY_def
using sums_mult sumind by blast
have "integrable M (λw. (X w) * ?indA w)"
proof (rule integrable_real_mult_indicator)
show "Y -` (A∩ range Y) ∩ space M ∈ sets M"
using ‹A ∈ sets M'› assms(3) assms(4) disct_fct_point_measurable measurable_sets
by (metis ‹Y -` A = Y -` (A ∩ range Y)›)
show "integrable M X" using assms by simp
qed
hence intsum: "integrable M (λw. (∑i. ((X w) * indpre i w)))" using sum
Bochner_Integration.integrable_cong[of M M "λ w.(X w) * (indicator ((Y -`A)∩ (space M)) w)" "λw. (∑ i.((X w) * indpre i w))"]
using ‹Y -` A = Y -` (A ∩ range Y)› by presburger
have "integral⇧L M (λw. (X w) * ?indA w) = integral⇧L M (λw. (∑ i.((X w) * indpre i w)))"
using ‹Y -` A = Y -` (A ∩ range Y)› sum by auto
also have "... =
∫⇧+ w. ((∑ i. ((X w) * indpre i w))) ∂M" using nn_integral_eq_integral
by (metis (mono_tags, lifting) AE_I2 intsum b nn_integral_cong)
also have "(∫⇧+ w. ((∑ i. ((X w) * indpre i w))) ∂M) = ∫⇧+ w. ((∑ i. ennreal ((X w) * indpre i w))) ∂M" using suminf_ennreal2 summable_def posprod sum sumxlim
proof -
{ fix aa :: 'a
have "∀a. ennreal (∑n. X a * indpre n a) = (∑n. ennreal (X a * indpre n a))"
by (metis (full_types) posprod suminf_ennreal2 summable_def sumxlim)
then have "(∫⇧+ a. ennreal (∑n. X a * indpre n a) ∂M) = (∫⇧+ a. (∑n. ennreal (X a * indpre n a)) ∂M) ∨ ennreal (∑n. X aa * indpre n aa) = (∑n. ennreal (X aa * indpre n aa))"
by metis }
then show ?thesis
by presburger
qed
also have "... = (∑i. integral⇧N M ((λi w. (X w) * indpre i w) i))"
proof (intro nn_integral_suminf)
fix i
show "(λx. ennreal (X x * indpre i x))∈ borel_measurable M"
using measurable_compose_rev measurable_ennreal prod_bm by blast
qed
also have "... = (∑i. integral⇧N M ((λi w. (expl_cond_expect M Y X w) * indpre i w) i))"
proof (intro suminf_cong)
fix n
have "A ∩ range Y ⊆ space M'"
using ‹A ∈ sets M'› sets.Int_space_eq1 by auto
have "integral⇧N M (λw. (X w) * indpre n w) = integral⇧L M (λw. (X w) * indpre n w)"
using nn_integral_eq_integral[of M "λw. (X w) * indpre n w"]
by (simp add: ‹∀i. integrable M (λw. X w * indpre i w)› posprod)
also have "... = integral⇧L M (λw. (expl_cond_expect M Y X) w * indpre n w)"
proof -
have "integral⇧L M (λw. X w * indicator (countable_preimages (A ∩ range Y) Y n ∩ space M) w) =
integral⇧L M (λw. expl_cond_expect M Y X w * indicator (countable_preimages (A ∩ range Y) Y n ∩ space M) w)"
using count_prod[of "A∩ range Y" "M'" Y X ] assms ‹A ∩ range Y ⊆ space M'› by blast
thus ?thesis
using ‹indpre ≡ λi. indicator (prY i ∩ space M)› prY_def by presburger
qed
also have "... = integral⇧N M (λw. (expl_cond_expect M Y X) w * indpre n w)"
proof -
have "integrable M (λw. (expl_cond_expect M Y X) w * indpre n w)" unfolding indpre_def prY_def
using count_pre_integrable assms ‹A ∩ range Y ⊆ space M'› ‹countable (A ∩ range Y)› by blast
moreover have "AE w in M. 0 ≤ (expl_cond_expect M Y X) w * indpre n w"
by (simp add: ‹indpre ≡ λi. indicator (prY i ∩ space M)› assms(1) nn_expl_cond_expect_pos)
ultimately show ?thesis by (simp add:nn_integral_eq_integral)
qed
finally show "integral⇧N M (λw. (X w) * indpre n w) = integral⇧N M (λw. (expl_cond_expect M Y X) w * indpre n w)" .
qed
also have "... = integral⇧N M (λw. ∑i. ((expl_cond_expect M Y X w) * indpre i w))"
proof -
have "(λx. (∑i. ennreal (expl_cond_expect M Y X x * indpre i x))) =
(λx. ennreal (∑i. (expl_cond_expect M Y X x * indpre i x)))"
proof-
have posex: "∀ i x. 0 ≤ (expl_cond_expect M Y X x) * (indpre i x)"
by (metis IntE ‹indpre ≡ λi. indicator (prY i ∩ space M)› assms(1) indicator_pos_le indicator_simps(2) mult_eq_0_iff mult_sign_intros(1) nn_expl_cond_expect_pos)
have "∀x. (∑i. ennreal (expl_cond_expect M Y X x * indpre i x)) = (ennreal (∑i. (expl_cond_expect M Y X x * indpre i x)))"
proof
fix x
show "(∑i. ennreal (expl_cond_expect M Y X x * indpre i x)) = (ennreal (∑i. (expl_cond_expect M Y X x * indpre i x)))"
using suminf_ennreal2[of "λi. (expl_cond_expect M Y X x * indpre i x)"] sumcondlim summable_def posex
proof -
have f1: "summable (λn. expl_cond_expect M Y X x * indpre n x)"
using sumcondlim summable_def by blast
obtain nn :: nat where
"¬ 0 ≤ expl_cond_expect M Y X x * indpre nn x ∨ ¬ summable (λn. expl_cond_expect M Y X x * indpre n x) ∨ ennreal (∑n. expl_cond_expect M Y X x * indpre n x) = (∑n. ennreal (expl_cond_expect M Y X x * indpre n x))"
by (metis (full_types) ‹⟦⋀i. 0 ≤ expl_cond_expect M Y X x * indpre i x; summable (λi. expl_cond_expect M Y X x * indpre i x)⟧ ⟹ (∑i. ennreal (expl_cond_expect M Y X x * indpre i x)) = ennreal (∑i. expl_cond_expect M Y X x * indpre i x)›)
then show ?thesis
using f1 posex by presburger
qed
qed
thus ?thesis by simp
qed
have "∀i. (λw. (expl_cond_expect M Y X w) * indpre i w) ∈ borel_measurable M"
proof -
show ?thesis
using ‹∀i. (indpre i)∈ borel_measurable M› assms(3) assms(4) borel_measurable_times expl_cond_expect_borel_measurable by blast
qed
hence "⋀i. (λx. ennreal (expl_cond_expect M Y X x * indpre i x))∈ borel_measurable M"
using measurable_compose_rev measurable_ennreal by blast
thus ?thesis using nn_integral_suminf[of "(λi w. (expl_cond_expect M Y X w) * indpre i w)" M, symmetric]
using ‹(λx. ∑i. ennreal (expl_cond_expect M Y X x * indpre i x)) = (λx. ennreal (∑i. expl_cond_expect M Y X x * indpre i x))› by auto
qed
also have "... = integral⇧N M (λw. (expl_cond_expect M Y X w) * ?indA w)"
using sumcondlim
by (metis (no_types, lifting) sums_unique)
also have "... = integral⇧L M (λw. (expl_cond_expect M Y X w) * ?indA w)"
proof -
have scdint: "integrable M (λw. (expl_cond_expect M Y X w) * ?indA w)"
proof -
have rv: "(λw. (expl_cond_expect M Y X w) * indicator ((Y -`?imA) ∩ (space M)) w) ∈ borel_measurable M"
proof -
have "expl_cond_expect M Y X ∈ borel_measurable M" using expl_cond_expect_borel_measurable
using assms by blast
moreover have "(Y -`?imA) ∩ (space M) ∈ sets M"
by (metis ‹A ∈ sets M'› ‹Y -` A = Y -` (A ∩ range Y)› assms(3) assms(4) disct_fct_point_measurable measurable_sets)
ultimately show ?thesis
using borel_measurable_indicator_iff borel_measurable_times by blast
qed
moreover have born: "integral⇧N M (λw. ennreal (norm (expl_cond_expect M Y X w * ?indA w))) < ∞"
proof -
have "integral⇧N M (λw. ennreal (norm (expl_cond_expect M Y X w * ?indA w))) =
integral⇧N M (λw. ennreal (expl_cond_expect M Y X w * ?indA w))"
proof -
have "∀w∈ space M. norm (expl_cond_expect M Y X w * ?indA w) = expl_cond_expect M Y X w * ?indA w"
using nn_expl_cond_expect_pos by (simp add: nn_expl_cond_expect_pos assms(1))
thus ?thesis by (metis (no_types, lifting) nn_integral_cong)
qed
thus ?thesis
by (metis (no_types, lifting)
‹(∑i. ∫⇧+ x. ennreal (X x * indpre i x) ∂M) = (∑i. ∫⇧+ x. ennreal (expl_cond_expect M Y X x * indpre i x) ∂M)›
‹(∑i. ∫⇧+ x. ennreal (expl_cond_expect M Y X x * indpre i x) ∂M) = (∫⇧+ x. ennreal (∑i. expl_cond_expect M Y X x * indpre i x) ∂M)›
‹(∫⇧+ w. (∑i. ennreal (X w * indpre i w)) ∂M) = (∑i. ∫⇧+ x. ennreal (X x * indpre i x) ∂M)›
‹(∫⇧+ x. ennreal (∑i. X x * indpre i x) ∂M) = (∫⇧+ w. (∑i. ennreal (X w * indpre i w)) ∂M)›
‹(∫⇧+ x. ennreal (∑i. expl_cond_expect M Y X x * indpre i x) ∂M) = (∫⇧+ x. ennreal (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x) ∂M)›
‹ennreal (integral⇧L M (λw. ∑i. X w * indpre i w)) = (∫⇧+ x. ennreal (∑i. X x * indpre i x) ∂M)›
ennreal_less_top infinity_ennreal_def)
qed
show "integrable M (λw. (expl_cond_expect M Y X w) * ?indA w)"
proof (rule iffD2[OF integrable_iff_bounded])
show "((λw. expl_cond_expect M Y X w * indicator (Y -` (A ∩ range Y) ∩ space M) w) ∈ borel_measurable M) ∧
((∫⇧+ x. (ennreal (norm (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x))) ∂M) < ∞)"
proof
show "(λw. expl_cond_expect M Y X w * indicator (Y -` (A ∩ range Y) ∩ space M) w)∈ borel_measurable M"
using rv by simp
show "(∫⇧+ x. ennreal (norm (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x)) ∂M) < ∞"
using born by simp
qed
qed
qed
moreover have "∀w∈ space M. 0 ≤ (expl_cond_expect M Y X w) * indicator ((Y -`?imA) ∩ (space M)) w"
by (simp add: assms(1) nn_expl_cond_expect_pos)
ultimately show ?thesis using nn_integral_eq_integral
by (metis (mono_tags, lifting) AE_I2 nn_integral_cong)
qed
finally have myeq: "ennreal (integral⇧L M (λw. (X w) * ?indA w)) = integral⇧L M (λw. (expl_cond_expect M Y X w) * ?indA w)" .
thus "integrable M (λw. expl_cond_expect M Y X w * indicator (Y -` A ∩ space M) w) ∧ integral⇧L M (λw. X w * indicator (Y -` A ∩ space M) w) =
integral⇧L M (λw. expl_cond_expect M Y X w * indicator (Y -` A ∩ space M) w)"
proof -
have "0 ≤ integral⇧L M (λw. X w * indicator (Y -` A ∩ space M) w)"
using ‹Y -` A = Y -` (A ∩ range Y)› b sum by fastforce
moreover have "0 ≤ integral⇧L M (λw. expl_cond_expect M Y X w * indicator (Y -` A ∩ space M) w)"
by (simp add: assms(1) nn_expl_cond_expect_pos)
ultimately have expeq: "integral⇧L M (λw. X w * indicator (Y -` A ∩ space M) w) =
integral⇧L M (λw. expl_cond_expect M Y X w * indicator (Y -` A ∩ space M) w)"
by (metis (mono_tags, lifting) Bochner_Integration.integral_cong ‹Y -` A = Y -` (A ∩ range Y)› ennreal_inj myeq)
have "integrable M (λw. (expl_cond_expect M Y X w) * ?indA w)"
proof -
have rv: "(λw. (expl_cond_expect M Y X w) * indicator ((Y -`?imA) ∩ (space M)) w) ∈ borel_measurable M"
proof -
have "expl_cond_expect M Y X ∈ borel_measurable M" using expl_cond_expect_borel_measurable
using assms by blast
moreover have "(Y -`?imA) ∩ (space M) ∈ sets M"
by (metis ‹A ∈ sets M'› ‹Y -` A = Y -` (A ∩ range Y)› assms(3) assms(4) disct_fct_point_measurable measurable_sets)
ultimately show ?thesis
using borel_measurable_indicator_iff borel_measurable_times by blast
qed
moreover have born: "integral⇧N M (λw. ennreal (norm (expl_cond_expect M Y X w * ?indA w))) < ∞"
proof -
have "integral⇧N M (λw. ennreal (norm (expl_cond_expect M Y X w * ?indA w))) =
integral⇧N M (λw. ennreal (expl_cond_expect M Y X w * ?indA w))"
proof -
have "∀w∈ space M. norm (expl_cond_expect M Y X w * ?indA w) = expl_cond_expect M Y X w * ?indA w"
using nn_expl_cond_expect_pos by (simp add: nn_expl_cond_expect_pos assms(1))
thus ?thesis by (metis (no_types, lifting) nn_integral_cong)
qed
thus ?thesis
by (metis (no_types, lifting)
‹(∑i. ∫⇧+ x. ennreal (X x * indpre i x) ∂M) = (∑i. ∫⇧+ x. ennreal (expl_cond_expect M Y X x * indpre i x) ∂M)›
‹(∑i. ∫⇧+ x. ennreal (expl_cond_expect M Y X x * indpre i x) ∂M) = (∫⇧+ x. ennreal (∑i. expl_cond_expect M Y X x * indpre i x) ∂M)›
‹(∫⇧+ w. (∑i. ennreal (X w * indpre i w)) ∂M) = (∑i. ∫⇧+ x. ennreal (X x * indpre i x) ∂M)›
‹(∫⇧+ x. ennreal (∑i. X x * indpre i x) ∂M) = (∫⇧+ w. (∑i. ennreal (X w * indpre i w)) ∂M)›
‹(∫⇧+ x. ennreal (∑i. expl_cond_expect M Y X x * indpre i x) ∂M) = (∫⇧+ x. ennreal (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x) ∂M)›
‹ennreal (integral⇧L M (λw. ∑i. X w * indpre i w)) = (∫⇧+ x. ennreal (∑i. X x * indpre i x) ∂M)›
ennreal_less_top infinity_ennreal_def)
qed
show "integrable M (λw. (expl_cond_expect M Y X w) * ?indA w)"
proof (rule iffD2[OF integrable_iff_bounded])
show "((λw. expl_cond_expect M Y X w * indicator (Y -` (A ∩ range Y) ∩ space M) w) ∈ borel_measurable M) ∧
((∫⇧+ x. (ennreal (norm (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x))) ∂M) < ∞)"
proof
show "(λw. expl_cond_expect M Y X w * indicator (Y -` (A ∩ range Y) ∩ space M) w)∈ borel_measurable M"
using rv by simp
show "(∫⇧+ x. ennreal (norm (expl_cond_expect M Y X x * indicator (Y -` (A ∩ range Y) ∩ space M) x)) ∂M) < ∞"
using born by simp
qed
qed
qed
hence "integrable M (λw. expl_cond_expect M Y X w * indicator (Y -` A ∩ space M) w)"
using ‹Y -` A = Y -` (A ∩ range Y)› by presburger
thus ?thesis using expeq by simp
qed
qed
lemma (in finite_measure) nn_expl_cond_exp_integrable:
assumes "∀ w∈ space M. 0 ≤ X w"
and "integrable M X"
and "disc_fct Y"
and "point_measurable M (space N) Y"
shows "integrable M (expl_cond_expect M Y X)"
proof -
have "Y-`space N ∩ space M = space M"
by (meson assms(3) assms(4) disct_fct_point_measurable inf_absorb2 measurable_space subsetI vimageI)
let ?indA = "indicator ((Y -`space N)∩ (space M))::'a⇒real"
have "∀w∈ space M. (?indA w)= (1::real)" by (simp add: ‹Y -` space N ∩ space M = space M›)
hence "∀w∈ space M. ((expl_cond_expect M Y X) w) * (?indA w) = (expl_cond_expect M Y X) w" by simp
moreover have "integrable M (λw. ((expl_cond_expect M Y X) w) * (?indA w))" using assms
nn_cond_expl_is_cond_exp_tmp[of X Y N] by blast
ultimately show ?thesis by (metis (no_types, lifting) Bochner_Integration.integrable_cong)
qed
lemma (in finite_measure) nn_cond_expl_is_cond_exp:
assumes "∀ w∈ space M. 0 ≤ X w"
and "integrable M X"
and "disc_fct Y"
and "point_measurable M (space N) Y"
shows "∀ A ∈ sets N. integral⇧L M (λw. (X w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator ((Y -`A) ∩ (space M))) w)"
by (metis (mono_tags, lifting) assms nn_cond_expl_is_cond_exp_tmp)
lemma (in finite_measure) expl_cond_exp_integrable:
assumes "integrable M X"
and "disc_fct Y"
and "point_measurable M (space N) Y"
shows "integrable M (expl_cond_expect M Y X)"
proof -
let ?zer = "λw. 0"
let ?Xp = "λw. max (?zer w) (X w)"
let ?Xn = "λw. max (?zer 0) (-X w)"
have "∀w. X w = ?Xp w - ?Xn w" by auto
have ints: "integrable M ?Xp" "integrable M ?Xn" using integrable_max assms by auto
hence "integrable M (expl_cond_expect M Y ?Xp)" using assms nn_expl_cond_exp_integrable
by (metis max.cobounded1)
moreover have "integrable M (expl_cond_expect M Y ?Xn)" using ints assms nn_expl_cond_exp_integrable
by (metis max.cobounded1)
ultimately have integr: "integrable M (λw. (expl_cond_expect M Y ?Xp) w - (expl_cond_expect M Y ?Xn) w)" by auto
have "∀w∈ space M. (expl_cond_expect M Y ?Xp) w - (expl_cond_expect M Y ?Xn) w = (expl_cond_expect M Y X) w"
proof
fix w
assume "w∈ space M"
hence "(expl_cond_expect M Y ?Xp) w - (expl_cond_expect M Y ?Xn) w = (expl_cond_expect M Y (λx. ?Xp x - ?Xn x)) w"
using ints by (simp add: expl_cond_exp_diff)
also have "... = expl_cond_expect M Y X w" using expl_cond_exp_cong ‹∀w. X w = ?Xp w - ?Xn w› by auto
finally show "(expl_cond_expect M Y ?Xp) w - (expl_cond_expect M Y ?Xn) w = expl_cond_expect M Y X w" .
qed
thus ?thesis using integr
by (metis (mono_tags, lifting) Bochner_Integration.integrable_cong)
qed
lemma (in finite_measure) is_cond_exp:
assumes "integrable M X"
and "disc_fct Y"
and "point_measurable M (space N) Y"
shows "∀ A ∈ sets N. integral⇧L M (λw. (X w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator ((Y -`A) ∩ (space M))) w)"
proof -
let ?zer = "λw. 0"
let ?Xp = "λw. max (?zer w) (X w)"
let ?Xn = "λw. max (?zer 0) (-X w)"
have "∀w. X w = ?Xp w - ?Xn w" by auto
have ints: "integrable M ?Xp" "integrable M ?Xn" using integrable_max assms by auto
hence posint: "integrable M (expl_cond_expect M Y ?Xp)" using assms nn_expl_cond_exp_integrable
by (metis max.cobounded1)
have negint: "integrable M (expl_cond_expect M Y ?Xn)" using ints assms nn_expl_cond_exp_integrable
by (metis max.cobounded1)
have eqp: "∀ A ∈ sets N. integral⇧L M (λw. (?Xp w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y ?Xp) w) * (indicator ((Y -`A) ∩ (space M))) w)"
using nn_cond_expl_is_cond_exp[of ?Xp Y N] assms by auto
have eqn: "∀ A ∈ sets N. integral⇧L M (λw. (?Xn w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y ?Xn) w) * (indicator ((Y -`A) ∩ (space M))) w)"
using nn_cond_expl_is_cond_exp[of ?Xn Y N] assms by auto
show "∀ A ∈ sets N. integral⇧L M (λw. (X w) * (indicator ((Y -`A)∩ (space M)) w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator ((Y -`A) ∩ (space M))) w)"
proof
fix A
assume "A∈ sets N"
let ?imA = "A ∩ (range Y)"
have "countable ?imA" using assms disc_fct_def by blast
have "Y -`A = Y -`?imA" by auto
have yev: "Y -` (A∩ range Y) ∩ space M ∈ sets M"
using ‹A ∈ sets N› assms(3) assms(2) disct_fct_point_measurable measurable_sets
by (metis ‹Y -` A = Y -` (A ∩ range Y)›)
let ?indA = "indicator ((Y -`(A ∩ range Y))∩ (space M))::'a⇒real"
have intp: "integrable M (λw. (?Xp w) * ?indA w)"
proof (rule integrable_real_mult_indicator)
show "Y -` (A∩ range Y) ∩ space M ∈ sets M" using yev by simp
show "integrable M ?Xp" using assms by simp
qed
have intn: "integrable M (λw. (?Xn w) * ?indA w)"
proof (rule integrable_real_mult_indicator)
show "Y -` (A∩ range Y) ∩ space M ∈ sets M" using yev by simp
show "integrable M ?Xn" using assms by simp
qed
have exintp: "integrable M (λw. (expl_cond_expect M Y ?Xp w) * ?indA w)"
proof (rule integrable_real_mult_indicator)
show "Y -` (A∩ range Y) ∩ space M ∈ sets M" using yev by simp
show "integrable M (expl_cond_expect M Y ?Xp)" using posint by simp
qed
have exintn: "integrable M (λw. (expl_cond_expect M Y ?Xn w) * ?indA w)"
proof (rule integrable_real_mult_indicator)
show "Y -` (A∩ range Y) ∩ space M ∈ sets M" using yev by simp
show "integrable M (expl_cond_expect M Y ?Xn)" using negint by simp
qed
have "integral⇧L M (λw. X w * indicator (Y -` A ∩ space M) w) =
integral⇧L M (λw. (?Xp w - ?Xn w) * indicator (Y -` A ∩ space M) w)"
using ‹∀w. X w =?Xp w - ?Xn w› by auto
also have "... = integral⇧L M (λw. (?Xp w * indicator (Y -` A ∩ space M) w) - ?Xn w * indicator (Y -` A ∩ space M) w)"
by (simp add: left_diff_distrib)
also have "... = integral⇧L M (λw. (?Xp w * indicator (Y -` A ∩ space M) w)) -
integral⇧L M (λw. ?Xn w * indicator (Y -` A ∩ space M) w)"
using ‹Y -` A = Y -` (A ∩ range Y)› intp intn by auto
also have "... = integral⇧L M (λw. ((expl_cond_expect M Y ?Xp) w) * (indicator ((Y -`A) ∩ (space M))) w) -
integral⇧L M (λw. ((expl_cond_expect M Y ?Xn) w) * (indicator ((Y -`A) ∩ (space M))) w)"
using eqp eqn by (simp add: ‹A ∈ sets N›)
also have "... = integral⇧L M (λw. ((expl_cond_expect M Y ?Xp) w) * (indicator ((Y -`A) ∩ (space M))) w -
((expl_cond_expect M Y ?Xn) w) * (indicator ((Y -`A) ∩ (space M))) w)"
using ‹Y -` A = Y -` (A ∩ range Y)› exintn exintp by auto
also have "... = integral⇧L M (λw. ((expl_cond_expect M Y ?Xp) w - (expl_cond_expect M Y ?Xn) w) * (indicator ((Y -`A) ∩ (space M))) w)"
by (simp add: left_diff_distrib)
also have "... = integral⇧L M (λw. ((expl_cond_expect M Y (λx. ?Xp x - ?Xn x) w) * (indicator ((Y -`A) ∩ (space M))) w))"
using expl_cond_exp_diff[of M ?Xp ?Xn Y] ints by (metis (mono_tags, lifting) Bochner_Integration.integral_cong)
also have "... = integral⇧L M (λw. ((expl_cond_expect M Y X w) * (indicator ((Y -`A) ∩ (space M))) w))"
using ‹∀w. X w = ?Xp w - ?Xn w› expl_cond_exp_cong[of M X "λx. ?Xp x - ?Xn x" Y] by presburger
finally show "integral⇧L M (λw. X w * indicator (Y -` A ∩ space M) w) = integral⇧L M (λw. ((expl_cond_expect M Y X w) * (indicator ((Y -`A) ∩ (space M))) w))" .
qed
qed
lemma (in finite_measure) charact_cond_exp:
assumes "disc_fct Y"
and "integrable M X"
and "point_measurable M (space N) Y"
and "Y ∈ space M → space N"
and "∀r∈ range Y∩ space N. ∃A∈ sets N. range Y∩ A = {r}"
shows "AE w in M. real_cond_exp M (fct_gen_subalgebra M N Y) X w = expl_cond_expect M Y X w"
proof (rule sigma_finite_subalgebra.real_cond_exp_charact)
have "Y∈ measurable M N"
by (simp add: assms(1) assms(3) disct_fct_point_measurable)
have "point_measurable M (space N) Y" by (simp add: assms(3))
show "sigma_finite_subalgebra M (fct_gen_subalgebra M N Y)" unfolding sigma_finite_subalgebra_def
proof
show "subalgebra M (fct_gen_subalgebra M N Y)" using ‹Y∈ measurable M N› by (simp add: fct_gen_subalgebra_is_subalgebra)
show "sigma_finite_measure (restr_to_subalg M (fct_gen_subalgebra M N Y))" unfolding sigma_finite_measure_def
proof (intro exI conjI)
let ?A = "{space M}"
show "countable ?A" by simp
show "?A ⊆ sets (restr_to_subalg M (fct_gen_subalgebra M N Y))"
by (metis empty_subsetI insert_subset sets.top space_restr_to_subalg)
show "⋃ ?A = space (restr_to_subalg M (fct_gen_subalgebra M N Y))"
by (simp add: space_restr_to_subalg)
show "∀a∈{space M}. emeasure (restr_to_subalg M (fct_gen_subalgebra M N Y)) a ≠ ∞"
by (metis ‹subalgebra M (fct_gen_subalgebra M N Y)› emeasure_finite emeasure_restr_to_subalg infinity_ennreal_def sets.top singletonD subalgebra_def)
qed
qed
show "integrable M X" using assms by simp
show "expl_cond_expect M Y X ∈ borel_measurable (fct_gen_subalgebra M N Y)" using assms by (simp add:expl_cond_exp_borel)
show "integrable M (expl_cond_expect M Y X)"
using assms expl_cond_exp_integrable by blast
have "∀A∈ sets M. integral⇧L M (λw. (X w) * (indicator A w)) = set_lebesgue_integral M A X"
by (metis (no_types, lifting) Bochner_Integration.integral_cong mult_commute_abs real_scaleR_def set_lebesgue_integral_def)
have "∀A∈ sets M. integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator A w)) = set_lebesgue_integral M A (expl_cond_expect M Y X)"
by (metis (no_types, lifting) Bochner_Integration.integral_cong mult_commute_abs real_scaleR_def set_lebesgue_integral_def)
have "∀A∈ sets (fct_gen_subalgebra M N Y). integral⇧L M (λw. (X w) * (indicator A w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator A w))"
proof
fix A
assume "A ∈ sets (fct_gen_subalgebra M N Y)"
hence "A ∈ {Y -` B ∩ space M |B. B ∈ sets N}" using assms by (simp add:fct_gen_subalgebra_sigma_sets)
hence "∃B ∈ sets N. A = Y -`B ∩ space M" by auto
from this obtain B where "B∈ sets N" and "A = Y -`B∩ space M" by auto
thus "integral⇧L M (λw. (X w) * (indicator A w)) =
integral⇧L M (λw. ((expl_cond_expect M Y X) w) * (indicator A w))" using is_cond_exp
using Bochner_Integration.integral_cong ‹point_measurable M (space N) Y› assms(1) assms(2) by blast
qed
thus "⋀A. A ∈ sets (fct_gen_subalgebra M N Y) ⟹ set_lebesgue_integral M A X = set_lebesgue_integral M A (expl_cond_expect M Y X)"
by (smt Bochner_Integration.integral_cong Groups.mult_ac(2) real_scaleR_def set_lebesgue_integral_def)
qed
lemma (in finite_measure) charact_cond_exp':
assumes "disc_fct Y"
and "integrable M X"
and "Y∈ measurable M N"
and "∀r∈ range Y∩ space N. ∃A∈ sets N. range Y∩ A = {r}"
shows "AE w in M. real_cond_exp M (fct_gen_subalgebra M N Y) X w = expl_cond_expect M Y X w"
proof (rule charact_cond_exp)
show "disc_fct Y" using assms by simp
show "integrable M X" using assms by simp
show "∀r∈range Y ∩ space N. ∃A∈sets N. range Y ∩ A = {r}" using assms by simp
show "Y∈ space M → space N"
by (meson Pi_I assms(3) measurable_space)
show "point_measurable M (space N) Y" using assms by (simp add: meas_single_meas)
qed
end