(* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr License: BSD *) section ‹Conditional Expectation› theory Conditional_Expectation imports Probability_Measure begin subsection ‹Restricting a measure to a sub-sigma-algebra› definition subalgebra::"'a measure ⇒ 'a measure ⇒ bool" where "subalgebra M F = ((space F = space M) ∧ (sets F ⊆ sets M))" lemma sub_measure_space: assumes i: "subalgebra M F" shows "measure_space (space M) (sets F) (emeasure M)" proof - have "sigma_algebra (space M) (sets F)" by (metis i measure_space measure_space_def subalgebra_def) moreover have "positive (sets F) (emeasure M)" using Sigma_Algebra.positive_def by auto moreover have "countably_additive (sets F) (emeasure M)" by (meson countably_additive_def emeasure_countably_additive i order_trans subalgebra_def subsetCE) ultimately show ?thesis unfolding measure_space_def by simp qed definition restr_to_subalg::"'a measure ⇒ 'a measure ⇒ 'a measure" where "restr_to_subalg M F = measure_of (space M) (sets F) (emeasure M)" lemma space_restr_to_subalg: "space (restr_to_subalg M F) = space M" unfolding restr_to_subalg_def by (simp add: space_measure_of_conv) lemma sets_restr_to_subalg [measurable_cong]: assumes "subalgebra M F" shows "sets (restr_to_subalg M F) = sets F" unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def) lemma emeasure_restr_to_subalg: assumes "subalgebra M F" "A ∈ sets F" shows "emeasure (restr_to_subalg M F) A = emeasure M A" unfolding restr_to_subalg_def by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq) lemma null_sets_restr_to_subalg: assumes "subalgebra M F" shows "null_sets (restr_to_subalg M F) = null_sets M ∩ sets F" proof have "x ∈ null_sets M ∩ sets F" if "x ∈ null_sets (restr_to_subalg M F)" for x by (metis that Int_iff assms emeasure_restr_to_subalg null_setsD1 null_setsD2 null_setsI sets_restr_to_subalg subalgebra_def subsetD) then show "null_sets (restr_to_subalg M F) ⊆ null_sets M ∩ sets F" by auto next have "x ∈ null_sets (restr_to_subalg M F)" if "x ∈ null_sets M ∩ sets F" for x by (metis that Int_iff assms null_setsD1 null_setsI sets_restr_to_subalg emeasure_restr_to_subalg[OF assms]) then show "null_sets M ∩ sets F ⊆ null_sets (restr_to_subalg M F)" by auto qed lemma AE_restr_to_subalg: assumes "subalgebra M F" "AE x in (restr_to_subalg M F). P x" shows "AE x in M. P x" proof - obtain A where A: "⋀x. x ∈ space (restr_to_subalg M F) - A ⟹ P x" "A ∈ null_sets (restr_to_subalg M F)" using AE_E3[OF assms(2)] by auto then have "A ∈ null_sets M" using null_sets_restr_to_subalg[OF assms(1)] by auto moreover have "⋀x. x ∈ space M - A ⟹ P x" using space_restr_to_subalg A(1) by fastforce ultimately show ?thesis unfolding eventually_ae_filter by auto qed lemma AE_restr_to_subalg2: assumes "subalgebra M F" "AE x in M. P x" and [measurable]: "P ∈ measurable F (count_space UNIV)" shows "AE x in (restr_to_subalg M F). P x" proof - define U where "U = {x ∈ space M. ¬(P x)}" then have *: "U = {x ∈ space F. ¬(P x)}" using assms(1) by (simp add: subalgebra_def) then have "U ∈ sets F" by simp then have "U ∈ sets M" using assms(1) by (meson subalgebra_def subsetD) then have "U ∈ null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast then have "U ∈ null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] ‹U ∈ sets F› by auto then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg) qed lemma prob_space_restr_to_subalg: assumes "subalgebra M F" "prob_space M" shows "prob_space (restr_to_subalg M F)" by (metis (no_types, lifting) assms(1) assms(2) emeasure_restr_to_subalg prob_space.emeasure_space_1 prob_spaceI sets.top space_restr_to_subalg subalgebra_def) lemma finite_measure_restr_to_subalg: assumes "subalgebra M F" "finite_measure M" shows "finite_measure (restr_to_subalg M F)" by (metis (no_types, lifting) assms emeasure_restr_to_subalg finite_measure.finite_emeasure_space finite_measureI sets.top space_restr_to_subalg subalgebra_def infinity_ennreal_def) lemma measurable_in_subalg: assumes "subalgebra M F" "f ∈ measurable F N" shows "f ∈ measurable (restr_to_subalg M F) N" by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)]) lemma measurable_in_subalg': assumes "subalgebra M F" "f ∈ measurable (restr_to_subalg M F) N" shows "f ∈ measurable F N" by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)]) lemma measurable_from_subalg: assumes "subalgebra M F" "f ∈ measurable F N" shows "f ∈ measurable M N" using assms unfolding measurable_def subalgebra_def by auto text‹The following is the direct transposition of \verb+nn_integral_subalgebra+ (from \verb+Nonnegative_Lebesgue_Integration+) in the current notations, with the removal of the useless assumption $f \geq 0$.› lemma nn_integral_subalgebra2: assumes "subalgebra M F" and [measurable]: "f ∈ borel_measurable F" shows "(∫⇧^{+}x. f x ∂(restr_to_subalg M F)) = (∫⇧^{+}x. f x ∂M)" proof (rule nn_integral_subalgebra) show "f ∈ borel_measurable (restr_to_subalg M F)" by (rule measurable_in_subalg[OF assms(1)]) simp show "sets (restr_to_subalg M F) ⊆ sets M" by (metis sets_restr_to_subalg[OF assms(1)] assms(1) subalgebra_def) fix A assume "A ∈ sets (restr_to_subalg M F)" then show "emeasure (restr_to_subalg M F) A = emeasure M A" by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)]) qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)]) text‹The following is the direct transposition of \verb+integral_subalgebra+ (from \verb+Bochner_Integration+) in the current notations.› lemma integral_subalgebra2: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "subalgebra M F" and [measurable]: "f ∈ borel_measurable F" shows "(∫x. f x ∂(restr_to_subalg M F)) = (∫x. f x ∂M)" by (rule integral_subalgebra, metis measurable_in_subalg[OF assms(1)] assms(2), auto simp add: assms space_restr_to_subalg sets_restr_to_subalg emeasure_restr_to_subalg, meson assms(1) subalgebra_def subset_eq) lemma integrable_from_subalg: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes "subalgebra M F" "integrable (restr_to_subalg M F) f" shows "integrable M f" proof (rule integrableI_bounded) have [measurable]: "f ∈ borel_measurable F" using assms by auto then show "f ∈ borel_measurable M" using assms(1) measurable_from_subalg by blast have "(∫⇧^{+}x. ennreal (norm (f x)) ∂M) = (∫⇧^{+}x. ennreal (norm (f x)) ∂(restr_to_subalg M F))" by (rule nn_integral_subalgebra2[symmetric], auto simp add: assms) also have "... < ∞" using integrable_iff_bounded assms by auto finally show "(∫⇧^{+}x. ennreal (norm (f x)) ∂M) < ∞" by simp qed lemma integrable_in_subalg: fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}" assumes [measurable]: "subalgebra M F" "f ∈ borel_measurable F" "integrable M f" shows "integrable (restr_to_subalg M F) f" proof (rule integrableI_bounded) show "f ∈ borel_measurable (restr_to_subalg M F)" using assms(2) assms(1) by auto have "(∫⇧^{+}x. ennreal (norm (f x)) ∂(restr_to_subalg M F)) = (∫⇧^{+}x. ennreal (norm (f x)) ∂M)" by (rule nn_integral_subalgebra2, auto simp add: assms) also have "... < ∞" using integrable_iff_bounded assms by auto finally show "(∫⇧^{+}x. ennreal (norm (f x)) ∂(restr_to_subalg M F)) < ∞" by simp qed subsection ‹Nonnegative conditional expectation› text ‹The conditional expectation of a function $f$, on a measure space $M$, with respect to a sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any $F$-set coincides with the integral of $f$. Such a function is uniquely defined almost everywhere. The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$, and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$. Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$ machinery, and works for all positive functions. In this paragraph, we develop the definition and basic properties for nonnegative functions, as the basics of the general case. As in the definition of integrals, the nonnegative case is done with ennreal-valued functions, without any integrability assumption. › definition nn_cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ ennreal) ⇒ ('a ⇒ ennreal)" where "nn_cond_exp M F f = (if f ∈ borel_measurable M ∧ subalgebra M F then RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M f) F) else (λ_. 0))" lemma shows borel_measurable_nn_cond_exp [measurable]: "nn_cond_exp M F f ∈ borel_measurable F" and borel_measurable_nn_cond_exp2 [measurable]: "nn_cond_exp M F f ∈ borel_measurable M" by (simp_all add: nn_cond_exp_def) (metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def) text ‹The good setting for conditional expectations is the situation where the subalgebra $F$ gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite, think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case, conditional expectations have to be constant functions, so they have integral $0$ or $\infty$. This means that a positive integrable function can have no meaningful conditional expectation.› locale sigma_finite_subalgebra = fixes M F::"'a measure" assumes subalg: "subalgebra M F" and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)" lemma sigma_finite_subalgebra_is_sigma_finite: assumes "sigma_finite_subalgebra M F" shows "sigma_finite_measure M" proof have subalg: "subalgebra M F" and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)" using assms unfolding sigma_finite_subalgebra_def by auto obtain A where Ap: "countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)" using sigma_finite_measure.sigma_finite_countable[OF sigma_fin_subalg] by fastforce have "A ⊆ sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce then have "A ⊆ sets M" using subalg subalgebra_def by force moreover have "⋃A = space M" using Ap space_restr_to_subalg by simp moreover have "∀a∈A. emeasure M a ≠ ∞" by (metis subsetD emeasure_restr_to_subalg[OF subalg] ‹A ⊆ sets F› Ap) ultimately show "∃A. countable A ∧ A ⊆ sets M ∧ ⋃A = space M ∧ (∀a∈A. emeasure M a ≠ ∞)" using Ap by auto qed sublocale sigma_finite_subalgebra ⊆ sigma_finite_measure using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast text ‹Conditional expectations are very often used in probability spaces. This is a special case of the previous one, as we prove now.› locale finite_measure_subalgebra = finite_measure + fixes F::"'a measure" assumes subalg: "subalgebra M F" lemma finite_measure_subalgebra_is_sigma_finite: assumes "finite_measure_subalgebra M F" shows "sigma_finite_subalgebra M F" proof - interpret finite_measure_subalgebra M F using assms by simp have "finite_measure (restr_to_subalg M F)" using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast then have "sigma_finite_measure (restr_to_subalg M F)" unfolding finite_measure_def by simp then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp qed sublocale finite_measure_subalgebra ⊆ sigma_finite_subalgebra proof - have "finite_measure (restr_to_subalg M F)" using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast then have "sigma_finite_measure (restr_to_subalg M F)" unfolding finite_measure_def by simp then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp qed context sigma_finite_subalgebra begin text‹The next lemma is arguably the most fundamental property of conditional expectation: when computing an expectation against an $F$-measurable function, it is equivalent to work with a function or with its $F$-conditional expectation. This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows. From this point on, we will only work with it, and forget completely about the definition using Radon-Nikodym derivatives. › lemma nn_cond_exp_intg: assumes [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M" shows "(∫⇧^{+}x. f x * nn_cond_exp M F g x ∂M) = (∫⇧^{+}x. f x * g x ∂M)" proof - have [measurable]: "f ∈ borel_measurable M" by (meson assms subalg borel_measurable_subalgebra subalgebra_def) have ac: "absolutely_continuous (restr_to_subalg M F) (restr_to_subalg (density M g) F)" unfolding absolutely_continuous_def proof - have "null_sets (restr_to_subalg M F) = null_sets M ∩ sets F" by (rule null_sets_restr_to_subalg[OF subalg]) moreover have "null_sets M ⊆ null_sets (density M g)" by (rule absolutely_continuousI_density[unfolded absolutely_continuous_def]) auto ultimately have "null_sets (restr_to_subalg M F) ⊆ null_sets (density M g) ∩ sets F" by auto moreover have "null_sets (density M g) ∩ sets F = null_sets (restr_to_subalg (density M g) F)" by (rule null_sets_restr_to_subalg[symmetric]) (metis subalg sets_density space_density subalgebra_def) ultimately show "null_sets (restr_to_subalg M F) ⊆ null_sets (restr_to_subalg (density M g) F)" by auto qed have "(∫⇧^{+}x. f x * nn_cond_exp M F g x ∂M) = (∫⇧^{+}x. f x * nn_cond_exp M F g x ∂(restr_to_subalg M F))" by (rule nn_integral_subalgebra2[symmetric]) (simp_all add: assms subalg) also have "... = (∫⇧^{+}x. f x * RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x ∂(restr_to_subalg M F))" unfolding nn_cond_exp_def using assms subalg by simp also have "... = (∫⇧^{+}x. RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x * f x ∂(restr_to_subalg M F))" by (simp add: mult.commute) also have "... = (∫⇧^{+}x. f x ∂(restr_to_subalg (density M g) F))" proof (rule sigma_finite_measure.RN_deriv_nn_integral[symmetric]) show "sets (restr_to_subalg (density M g) F) = sets (restr_to_subalg M F)" by (metis subalg restr_to_subalg_def sets.sets_measure_of_eq space_density subalgebra_def) qed (auto simp add: assms measurable_restrict ac measurable_in_subalg subalg sigma_fin_subalg) also have "... = (∫⇧^{+}x. f x ∂(density M g))" by (metis nn_integral_subalgebra2 subalg assms(1) sets_density space_density subalgebra_def) also have "... = (∫⇧^{+}x. g x * f x ∂M)" by (rule nn_integral_density) (simp_all add: assms) also have "... = (∫⇧^{+}x. f x * g x ∂M)" by (simp add: mult.commute) finally show ?thesis by simp qed lemma nn_cond_exp_charact: assumes "⋀A. A ∈ sets F ⟹ (∫⇧^{+}x ∈ A. f x ∂M) = (∫⇧^{+}x ∈ A. g x ∂M)" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable F" shows "AE x in M. g x = nn_cond_exp M F f x" proof - let ?MF = "restr_to_subalg M F" { fix A assume "A ∈ sets ?MF" then have [measurable]: "A ∈ sets F" using sets_restr_to_subalg[OF subalg] by simp have "(∫⇧^{+}x ∈ A. g x ∂ ?MF) = (∫⇧^{+}x ∈ A. g x ∂M)" by (simp add: nn_integral_subalgebra2 subalg) also have "... = (∫⇧^{+}x ∈ A. f x ∂M)" using assms(1) by simp also have "... = (∫⇧^{+}x. indicator A x * f x ∂M)" by (simp add: mult.commute) also have "... = (∫⇧^{+}x. indicator A x * nn_cond_exp M F f x ∂M)" by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms) also have "... = (∫⇧^{+}x ∈ A. nn_cond_exp M F f x ∂M)" by (simp add: mult.commute) also have "... = (∫⇧^{+}x ∈ A. nn_cond_exp M F f x ∂ ?MF)" by (simp add: nn_integral_subalgebra2 subalg) finally have "(∫⇧^{+}x ∈ A. g x ∂ ?MF) = (∫⇧^{+}x ∈ A. nn_cond_exp M F f x ∂ ?MF)" by simp } note * = this have "AE x in ?MF. g x = nn_cond_exp M F f x" by (rule sigma_finite_measure.density_unique2) (auto simp add: assms subalg sigma_fin_subalg AE_restr_to_subalg2 *) then show ?thesis using AE_restr_to_subalg[OF subalg] by simp qed lemma nn_cond_exp_F_meas: assumes "f ∈ borel_measurable F" shows "AE x in M. f x = nn_cond_exp M F f x" by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg]) lemma nn_cond_exp_prod: assumes [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M" shows "AE x in M. f x * nn_cond_exp M F g x = nn_cond_exp M F (λx. f x * g x) x" proof (rule nn_cond_exp_charact) have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(1)]) show "(λx. f x * g x) ∈ borel_measurable M" by measurable fix A assume "A ∈ sets F" then have [measurable]: "(λx. f x * indicator A x) ∈ borel_measurable F" by measurable have "∫⇧^{+}x∈A. (f x * g x) ∂M = ∫⇧^{+}x. (f x * indicator A x) * g x ∂M" by (simp add: mult.commute mult.left_commute) also have "... = ∫⇧^{+}x. (f x * indicator A x) * nn_cond_exp M F g x ∂M" by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms) also have "... = ∫⇧^{+}x∈A. (f x * nn_cond_exp M F g x)∂M" by (simp add: mult.commute mult.left_commute) finally show "∫⇧^{+}x∈A. (f x * g x) ∂M = ∫⇧^{+}x∈A. (f x * nn_cond_exp M F g x)∂M" by simp qed (auto simp add: assms) lemma nn_cond_exp_sum: assumes [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "AE x in M. nn_cond_exp M F f x + nn_cond_exp M F g x = nn_cond_exp M F (λx. f x + g x) x" proof (rule nn_cond_exp_charact) fix A assume [measurable]: "A ∈ sets F" then have "A ∈ sets M" by (meson subalg subalgebra_def subsetD) have "∫⇧^{+}x∈A. (nn_cond_exp M F f x + nn_cond_exp M F g x)∂M = (∫⇧^{+}x∈A. nn_cond_exp M F f x ∂M) + (∫⇧^{+}x∈A. nn_cond_exp M F g x ∂M)" by (rule nn_set_integral_add) (auto simp add: assms ‹A ∈ sets M›) also have "... = (∫⇧^{+}x. indicator A x * nn_cond_exp M F f x ∂M) + (∫⇧^{+}x. indicator A x * nn_cond_exp M F g x ∂M)" by (metis (no_types, lifting) mult.commute nn_integral_cong) also have "... = (∫⇧^{+}x. indicator A x * f x ∂M) + (∫⇧^{+}x. indicator A x * g x ∂M)" by (simp add: nn_cond_exp_intg) also have "... = (∫⇧^{+}x∈A. f x ∂M) + (∫⇧^{+}x∈A. g x ∂M)" by (metis (no_types, lifting) mult.commute nn_integral_cong) also have "... = ∫⇧^{+}x∈A. (f x + g x)∂M" by (rule nn_set_integral_add[symmetric]) (auto simp add: assms ‹A ∈ sets M›) finally show "∫⇧^{+}x∈A. (f x + g x)∂M = ∫⇧^{+}x∈A. (nn_cond_exp M F f x + nn_cond_exp M F g x)∂M" by simp qed (auto simp add: assms) lemma nn_cond_exp_cong: assumes "AE x in M. f x = g x" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x" proof (rule nn_cond_exp_charact) fix A assume [measurable]: "A ∈ sets F" have "∫⇧^{+}x∈A. nn_cond_exp M F f x ∂M = ∫⇧^{+}x. indicator A x * nn_cond_exp M F f x ∂M" by (simp add: mult.commute) also have "... = ∫⇧^{+}x. indicator A x * f x ∂M" by (simp add: nn_cond_exp_intg assms) also have "... = ∫⇧^{+}x∈A. f x ∂M" by (simp add: mult.commute) also have "... = ∫⇧^{+}x∈A. g x ∂M" by (rule nn_set_integral_cong[OF assms(1)]) finally show "∫⇧^{+}x∈A. g x ∂M = ∫⇧^{+}x∈A. nn_cond_exp M F f x ∂M" by simp qed (auto simp add: assms) lemma nn_cond_exp_mono: assumes "AE x in M. f x ≤ g x" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "AE x in M. nn_cond_exp M F f x ≤ nn_cond_exp M F g x" proof - define h where "h = (λx. g x - f x)" have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add) have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F (λx. f x + h x) x" by (rule nn_cond_exp_cong) (auto simp add: * assms) moreover have "AE x in M. nn_cond_exp M F f x + nn_cond_exp M F h x = nn_cond_exp M F (λx. f x + h x) x" by (rule nn_cond_exp_sum) (auto simp add: assms) ultimately have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F f x + nn_cond_exp M F h x" by auto then show ?thesis by force qed lemma nested_subalg_is_sigma_finite: assumes "subalgebra M G" "subalgebra G F" shows "sigma_finite_subalgebra M G" unfolding sigma_finite_subalgebra_def proof (auto simp add: assms) have "∃A. countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)" using sigma_fin_subalg sigma_finite_measure_def by auto then obtain A where A:"countable A ∧ A ⊆ sets (restr_to_subalg M F) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M F) a ≠ ∞)" by auto have "sets F ⊆ sets M" by (meson assms order_trans subalgebra_def) then have "countable A ∧ A ⊆ sets (restr_to_subalg M G) ∧ ⋃A = space (restr_to_subalg M F) ∧ (∀a∈A. emeasure (restr_to_subalg M G) a ≠ ∞)" by (metis (no_types) A assms basic_trans_rules(31) emeasure_restr_to_subalg order_trans sets_restr_to_subalg subalgebra_def) then show "sigma_finite_measure (restr_to_subalg M G)" by (metis sigma_finite_measure.intro space_restr_to_subalg) qed lemma nn_cond_exp_nested_subalg: assumes "subalgebra M G" "subalgebra G F" and [measurable]: "f ∈ borel_measurable M" shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F (nn_cond_exp M G f) x" proof (rule nn_cond_exp_charact, auto) interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)]) fix A assume [measurable]: "A ∈ sets F" then have [measurable]: "A ∈ sets G" using assms(2) by (meson set_mp subalgebra_def) have "set_nn_integral M A (nn_cond_exp M G f) = (∫⇧^{+}x. indicator A x * nn_cond_exp M G f x∂M)" by (metis (no_types) mult.commute) also have "... = (∫⇧^{+}x. indicator A x * f x ∂M)" by (rule G.nn_cond_exp_intg, auto simp add: assms) also have "... = (∫⇧^{+}x. indicator A x * nn_cond_exp M F f x ∂M)" by (rule nn_cond_exp_intg[symmetric], auto simp add: assms) also have "... = set_nn_integral M A (nn_cond_exp M F f)" by (metis (no_types) mult.commute) finally show "set_nn_integral M A (nn_cond_exp M G f) = set_nn_integral M A (nn_cond_exp M F f)". qed end subsection ‹Real conditional expectation› text ‹Once conditional expectations of positive functions are defined, the definition for real-valued functions follows readily, by taking the difference of positive and negative parts. One could also define a conditional expectation of vector-space valued functions, as in \verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I concentrate on it. (It is also essential for the case of the most general Pettis integral.) › definition real_cond_exp :: "'a measure ⇒ 'a measure ⇒ ('a ⇒ real) ⇒ ('a ⇒ real)" where "real_cond_exp M F f = (λx. enn2real(nn_cond_exp M F (λx. ennreal (f x)) x) - enn2real(nn_cond_exp M F (λx. ennreal (-f x)) x))" lemma shows borel_measurable_cond_exp [measurable]: "real_cond_exp M F f ∈ borel_measurable F" and borel_measurable_cond_exp2 [measurable]: "real_cond_exp M F f ∈ borel_measurable M" unfolding real_cond_exp_def by auto context sigma_finite_subalgebra begin lemma real_cond_exp_abs: assumes [measurable]: "f ∈ borel_measurable M" shows "AE x in M. abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. ennreal (abs(f x))) x" proof - define fp where "fp = (λx. ennreal (f x))" define fm where "fm = (λx. ennreal (- f x))" have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M" unfolding fp_def fm_def by auto have eq: "⋀x. ennreal ¦f x¦ = fp x + fm x" unfolding fp_def fm_def by (simp add: abs_real_def ennreal_neg) { fix x assume H: "nn_cond_exp M F fp x + nn_cond_exp M F fm x = nn_cond_exp M F (λx. fp x + fm x) x" have "¦real_cond_exp M F f x¦ ≤ ¦enn2real(nn_cond_exp M F fp x)¦ + ¦enn2real(nn_cond_exp M F fm x)¦" unfolding real_cond_exp_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg) from ennreal_leI[OF this] have "abs(real_cond_exp M F f x) ≤ nn_cond_exp M F fp x + nn_cond_exp M F fm x" by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique) also have "... = nn_cond_exp M F (λx. fp x + fm x) x" using H by simp finally have "abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. fp x + fm x) x" by simp } moreover have "AE x in M. nn_cond_exp M F fp x + nn_cond_exp M F fm x = nn_cond_exp M F (λx. fp x + fm x) x" by (rule nn_cond_exp_sum) (auto simp add: fp_def fm_def) ultimately have "AE x in M. abs(real_cond_exp M F f x) ≤ nn_cond_exp M F (λx. fp x + fm x) x" by auto then show ?thesis using eq by simp qed text‹The next lemma shows that the conditional expectation is an $F$-measurable function whose average against an $F$-measurable function $f$ coincides with the average of the original function against $f$. It is obtained as a consequence of the same property for the positive conditional expectation, taking the difference of the positive and the negative part. The proof is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in the subsequent lemma. The idea of the proof is essentially trivial, but the implementation is slightly tedious as one should check all the integrability properties of the different parts, and go back and forth between positive integral and signed integrals, and between real-valued functions and ennreal-valued functions. Once this lemma is available, we will use it to characterize the conditional expectation, and never come back to the original technical definition, as we did in the case of the nonnegative conditional expectation. › lemma real_cond_exp_intg_fpos: assumes "integrable M (λx. f x * g x)" and f_pos[simp]: "⋀x. f x ≥ 0" and [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M" shows "integrable M (λx. f x * real_cond_exp M F g x)" "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)" proof - have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(3)]) define gp where "gp = (λx. ennreal (g x))" define gm where "gm = (λx. ennreal (- g x))" have [measurable]: "gp ∈ borel_measurable M" "gm ∈ borel_measurable M" unfolding gp_def gm_def by auto define h where "h = (λx. ennreal(abs(g x)))" have hgpgm: "⋀x. h x = gp x + gm x" unfolding gp_def gm_def h_def by (simp add: abs_real_def ennreal_neg) have [measurable]: "h ∈ borel_measurable M" unfolding h_def by simp have pos[simp]: "⋀x. h x ≥ 0" "⋀x. gp x ≥ 0" "⋀x. gm x ≥ 0" unfolding h_def gp_def gm_def by simp_all have gp_real: "⋀x. enn2real(gp x) = max (g x) 0" unfolding gp_def by (simp add: max_def ennreal_neg) have gm_real: "⋀x. enn2real(gm x) = max (-g x) 0" unfolding gm_def by (simp add: max_def ennreal_neg) have "(∫⇧^{+}x. norm(f x * max (g x) 0) ∂M) ≤ (∫⇧^{+}x. norm(f x * g x) ∂M)" by (simp add: nn_integral_mono) also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded) finally have "(∫⇧^{+}x. norm(f x * max (g x) 0) ∂M) < ∞" by simp then have int1: "integrable M (λx. f x * max (g x) 0)" by (simp add: integrableI_bounded) have "(∫⇧^{+}x. norm(f x * max (-g x) 0) ∂M) ≤ (∫⇧^{+}x. norm(f x * g x) ∂M)" by (simp add: nn_integral_mono) also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded) finally have "(∫⇧^{+}x. norm(f x * max (-g x) 0) ∂M) < ∞" by simp then have int2: "integrable M (λx. f x * max (-g x) 0)" by (simp add: integrableI_bounded) have "(∫⇧^{+}x. f x * nn_cond_exp M F h x ∂M) = (∫⇧^{+}x. f x * h x ∂M)" by (rule nn_cond_exp_intg) auto also have "… = ∫⇧^{+}x. ennreal (f x * max (g x) 0 + f x * max (- g x) 0) ∂M" unfolding h_def by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max) also have "... < ∞" using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top) finally have *: "(∫⇧^{+}x. f x * nn_cond_exp M F h x ∂M) < ∞" by simp have "(∫⇧^{+}x. norm(f x * real_cond_exp M F g x) ∂M) = (∫⇧^{+}x. f x * abs(real_cond_exp M F g x) ∂M)" by (simp add: abs_mult) also have "... ≤ (∫⇧^{+}x. f x * nn_cond_exp M F h x ∂M)" proof (rule nn_integral_mono_AE) { fix x assume *: "abs(real_cond_exp M F g x) ≤ nn_cond_exp M F h x" have "ennreal (f x * ¦real_cond_exp M F g x¦) = f x * ennreal(¦real_cond_exp M F g x¦)" by (simp add: ennreal_mult) also have "... ≤ f x * nn_cond_exp M F h x" using * by (auto intro!: mult_left_mono) finally have "ennreal (f x * ¦real_cond_exp M F g x¦) ≤ f x * nn_cond_exp M F h x" by simp } then show "AE x in M. ennreal (f x * ¦real_cond_exp M F g x¦) ≤ f x * nn_cond_exp M F h x" using real_cond_exp_abs[OF assms(4)] h_def by auto qed finally have **: "(∫⇧^{+}x. norm(f x * real_cond_exp M F g x) ∂M) < ∞" using * by auto show "integrable M (λx. f x * real_cond_exp M F g x)" using ** by (intro integrableI_bounded) auto have "(∫⇧^{+}x. f x * nn_cond_exp M F gp x ∂M) ≤ (∫⇧^{+}x. f x * nn_cond_exp M F h x ∂M)" proof (rule nn_integral_mono_AE) have "AE x in M. nn_cond_exp M F gp x ≤ nn_cond_exp M F h x" by (rule nn_cond_exp_mono) (auto simp add: hgpgm) then show "AE x in M. f x * nn_cond_exp M F gp x ≤ f x * nn_cond_exp M F h x" by (auto simp: mult_left_mono) qed then have a: "(∫⇧^{+}x. f x * nn_cond_exp M F gp x ∂M) < ∞" using * by auto have "ennreal(norm(f x * enn2real(nn_cond_exp M F gp x))) ≤ f x * nn_cond_exp M F gp x" for x by (auto simp add: ennreal_mult intro!: mult_left_mono) (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff) then have "(∫⇧^{+}x. norm(f x * enn2real(nn_cond_exp M F gp x)) ∂M) ≤ (∫⇧^{+}x. f x * nn_cond_exp M F gp x ∂M)" by (simp add: nn_integral_mono) then have "(∫⇧^{+}x. norm(f x * enn2real(nn_cond_exp M F gp x)) ∂M) < ∞" using a by auto then have gp_int: "integrable M (λx. f x * enn2real(nn_cond_exp M F gp x))" by (simp add: integrableI_bounded) have gp_fin: "AE x in M. f x * nn_cond_exp M F gp x ≠ ∞" apply (rule nn_integral_PInf_AE) using a by auto have "(∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = enn2real (∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gp x) ∂M)" by (rule integral_eq_nn_integral) auto also have "... = enn2real(∫⇧^{+}x. ennreal(f x * enn2real(gp x)) ∂M)" proof - { fix x assume "f x * nn_cond_exp M F gp x ≠ ∞" then have "ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x" by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong) } then have "AE x in M. ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x" using gp_fin by auto then have "(∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫⇧^{+}x. f x * nn_cond_exp M F gp x ∂M)" by (rule nn_integral_cong_AE) also have "... = (∫⇧^{+}x. f x * gp x ∂M)" by (rule nn_cond_exp_intg) (auto simp add: gp_def) also have "... = (∫⇧^{+}x. ennreal(f x * enn2real(gp x)) ∂M)" by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def) finally have "(∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫⇧^{+}x. ennreal(f x * enn2real(gp x)) ∂M)" by simp then show ?thesis by simp qed also have "... = (∫ x. f x * enn2real(gp x) ∂M)" by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def) finally have gp_expr: "(∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) = (∫ x. f x * enn2real(gp x) ∂M)" by simp have "(∫⇧^{+}x. f x * nn_cond_exp M F gm x ∂M) ≤ (∫⇧^{+}x. f x * nn_cond_exp M F h x ∂M)" proof (rule nn_integral_mono_AE) have "AE x in M. nn_cond_exp M F gm x ≤ nn_cond_exp M F h x" by (rule nn_cond_exp_mono) (auto simp add: hgpgm) then show "AE x in M. f x * nn_cond_exp M F gm x ≤ f x * nn_cond_exp M F h x" by (auto simp: mult_left_mono) qed then have a: "(∫⇧^{+}x. f x * nn_cond_exp M F gm x ∂M) < ∞" using * by auto have "⋀x. ennreal(norm(f x * enn2real(nn_cond_exp M F gm x))) ≤ f x * nn_cond_exp M F gm x" by (auto simp add: ennreal_mult intro!: mult_left_mono) (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff) then have "(∫⇧^{+}x. norm(f x * enn2real(nn_cond_exp M F gm x)) ∂M) ≤ (∫⇧^{+}x. f x * nn_cond_exp M F gm x ∂M)" by (simp add: nn_integral_mono) then have "(∫⇧^{+}x. norm(f x * enn2real(nn_cond_exp M F gm x)) ∂M) < ∞" using a by auto then have gm_int: "integrable M (λx. f x * enn2real(nn_cond_exp M F gm x))" by (simp add: integrableI_bounded) have gm_fin: "AE x in M. f x * nn_cond_exp M F gm x ≠ ∞" apply (rule nn_integral_PInf_AE) using a by auto have "(∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = enn2real (∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gm x) ∂M)" by (rule integral_eq_nn_integral) auto also have "... = enn2real(∫⇧^{+}x. ennreal(f x * enn2real(gm x)) ∂M)" proof - { fix x assume "f x * nn_cond_exp M F gm x ≠ ∞" then have "ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x" by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong) } then have "AE x in M. ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x" using gm_fin by auto then have "(∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫⇧^{+}x. f x * nn_cond_exp M F gm x ∂M)" by (rule nn_integral_cong_AE) also have "... = (∫⇧^{+}x. f x * gm x ∂M)" by (rule nn_cond_exp_intg) (auto simp add: gm_def) also have "... = (∫⇧^{+}x. ennreal(f x * enn2real(gm x)) ∂M)" by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def) finally have "(∫⇧^{+}x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫⇧^{+}x. ennreal(f x * enn2real(gm x)) ∂M)" by simp then show ?thesis by simp qed also have "... = (∫ x. f x * enn2real(gm x) ∂M)" by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def) finally have gm_expr: "(∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M) = (∫ x. f x * enn2real(gm x) ∂M)" by simp have "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * enn2real(nn_cond_exp M F gp x) - f x * enn2real(nn_cond_exp M F gm x) ∂M)" unfolding real_cond_exp_def gp_def gm_def by (simp add: right_diff_distrib) also have "... = (∫ x. f x * enn2real(nn_cond_exp M F gp x) ∂M) - (∫ x. f x * enn2real(nn_cond_exp M F gm x) ∂M)" by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int) also have "... = (∫ x. f x * enn2real(gp x) ∂M) - (∫ x. f x * enn2real(gm x) ∂M)" using gp_expr gm_expr by simp also have "... = (∫ x. f x * max (g x) 0 ∂M) - (∫ x. f x * max (-g x) 0 ∂M)" using gp_real gm_real by simp also have "... = (∫ x. f x * max (g x) 0 - f x * max (-g x) 0 ∂M)" by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2) also have "... = (∫x. f x * g x ∂M)" by (metis (mono_tags, hide_lams) diff_0 diff_zero eq_iff max.cobounded2 max_def minus_minus neg_le_0_iff_le right_diff_distrib) finally show "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫x. f x * g x ∂M)" by simp qed lemma real_cond_exp_intg: assumes "integrable M (λx. f x * g x)" and [measurable]: "f ∈ borel_measurable F" "g ∈ borel_measurable M" shows "integrable M (λx. f x * real_cond_exp M F g x)" "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)" proof - have [measurable]: "f ∈ borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(2)]) define fp where "fp = (λx. max (f x) 0)" define fm where "fm = (λx. max (-f x) 0)" have [measurable]: "fp ∈ borel_measurable M" "fm ∈ borel_measurable M" unfolding fp_def fm_def by simp_all have [measurable]: "fp ∈ borel_measurable F" "fm ∈ borel_measurable F" unfolding fp_def fm_def by simp_all have "(∫⇧^{+}x. norm(fp x * g x) ∂M) ≤ (∫⇧^{+}x. norm(f x * g x) ∂M)" by (simp add: fp_def nn_integral_mono) also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded) finally have "(∫⇧^{+}x. norm(fp x * g x) ∂M) < ∞" by simp then have intp: "integrable M (λx. fp x * g x)" by (simp add: integrableI_bounded) moreover have "⋀x. fp x ≥ 0" unfolding fp_def by simp ultimately have Rp: "integrable M (λx. fp x * real_cond_exp M F g x)" "(∫ x. fp x * real_cond_exp M F g x ∂M) = (∫ x. fp x * g x ∂M)" using real_cond_exp_intg_fpos by auto have "(∫⇧^{+}x. norm(fm x * g x) ∂M) ≤ (∫⇧^{+}x. norm(f x * g x) ∂M)" by (simp add: fm_def nn_integral_mono) also have "... < ∞" using assms(1) by (simp add: integrable_iff_bounded) finally have "(∫⇧^{+}x. norm(fm x * g x) ∂M) < ∞" by simp then have intm: "integrable M (λx. fm x * g x)" by (simp add: integrableI_bounded) moreover have "⋀x. fm x ≥ 0" unfolding fm_def by simp ultimately have Rm: "integrable M (λx. fm x * real_cond_exp M F g x)" "(∫ x. fm x * real_cond_exp M F g x ∂M) = (∫ x. fm x * g x ∂M)" using real_cond_exp_intg_fpos by auto have "integrable M (λx. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x)" using Rp(1) Rm(1) integrable_diff by simp moreover have *: "⋀x. f x * real_cond_exp M F g x = fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x" unfolding fp_def fm_def by (simp add: max_def) ultimately show "integrable M (λx. f x * real_cond_exp M F g x)" by simp have "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x ∂M)" using * by simp also have "... = (∫ x. fp x * real_cond_exp M F g x ∂M) - (∫ x. fm x * real_cond_exp M F g x ∂M)" using Rp(1) Rm(1) by simp also have "... = (∫ x. fp x * g x ∂M) - (∫ x. fm x * g x ∂M)" using Rp(2) Rm(2) by simp also have "... = (∫ x. fp x * g x - fm x * g x ∂M)" using intm intp by simp also have "... = (∫ x. f x * g x ∂M)" unfolding fp_def fm_def by (metis (no_types, hide_lams) diff_0 diff_zero max.commute max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib) finally show "(∫ x. f x * real_cond_exp M F g x ∂M) = (∫ x. f x * g x ∂M)" by simp qed lemma real_cond_exp_intA: assumes [measurable]: "integrable M f" "A ∈ sets F" shows "(∫ x ∈ A. f x ∂M) = (∫x ∈ A. real_cond_exp M F f x ∂M)" proof - have "A ∈ sets M" by (meson assms(2) subalg subalgebra_def subsetD) have "integrable M (λx. indicator A x * f x)" using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] unfolding set_lebesgue_integral_def by auto qed lemma real_cond_exp_int [intro]: assumes "integrable M f" shows "integrable M (real_cond_exp M F f)" "(∫x. real_cond_exp M F f x ∂M) = (∫x. f x ∂M)" using real_cond_exp_intg[where ?f = "λx. 1" and ?g = f] assms by auto lemma real_cond_exp_charact: assumes "⋀A. A ∈ sets F ⟹ (∫ x ∈ A. f x ∂M) = (∫ x ∈ A. g x ∂M)" and [measurable]: "integrable M f" "integrable M g" "g ∈ borel_measurable F" shows "AE x in M. real_cond_exp M F f x = g x" proof - let ?MF = "restr_to_subalg M F" have "AE x in ?MF. real_cond_exp M F f x = g x" proof (rule AE_symmetric[OF density_unique_real]) fix A assume "A ∈ sets ?MF" then have [measurable]: "A ∈ sets F" using sets_restr_to_subalg[OF subalg] by simp then have a [measurable]: "A ∈ sets M" by (meson subalg subalgebra_def subsetD) have "(∫x ∈ A. g x ∂ ?MF) = (∫x ∈ A. g x ∂M)" unfolding set_lebesgue_integral_def by (simp add: integral_subalgebra2 subalg) also have "... = (∫x ∈ A. f x ∂M)" using assms(1) by simp also have "... = (∫x. indicator A x * f x ∂M)" by (simp add: mult.commute set_lebesgue_integral_def) also have "... = (∫x. indicator A x * real_cond_exp M F f x ∂M)" apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms) also have "... = (∫x ∈ A. real_cond_exp M F f x ∂M)" by (simp add: mult.commute set_lebesgue_integral_def) also have "... = (∫x ∈ A. real_cond_exp M F f x ∂ ?MF)" by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def) finally show "(∫x ∈ A. g x ∂ ?MF) = (∫x ∈ A. real_cond_exp M F f x ∂ ?MF)" by simp next have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)]) then show "integrable ?MF (real_cond_exp M F f)" by (metis borel_measurable_cond_exp integrable_in_subalg[OF subalg]) show "integrable (restr_to_subalg M F) g" by (simp add: assms(3) integrable_in_subalg[OF subalg]) qed then show ?thesis using AE_restr_to_subalg[OF subalg] by auto qed lemma real_cond_exp_F_meas [intro, simp]: assumes "integrable M f" "f ∈ borel_measurable F" shows "AE x in M. real_cond_exp M F f x = f x" by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg]) lemma real_cond_exp_mult: assumes [measurable]:"f ∈ borel_measurable F" "g ∈ borel_measurable M" "integrable M (λx. f x * g x)" shows "AE x in M. real_cond_exp M F (λx. f x * g x) x = f x * real_cond_exp M F g x" proof (rule real_cond_exp_charact) fix A assume "A ∈ sets F" then have [measurable]: "(λx. f x * indicator A x) ∈ borel_measurable F" by measurable have [measurable]: "A ∈ sets M" using subalg by (meson ‹A ∈ sets F› subalgebra_def subsetD) have "∫x∈A. (f x * g x) ∂M = ∫x. (f x * indicator A x) * g x ∂M" by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def) also have "... = ∫x. (f x * indicator A x) * real_cond_exp M F g x ∂M" apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms) using integrable_mult_indicator[OF ‹A ∈ sets M› assms(3)] by (simp add: mult.commute mult.left_commute) also have "... = ∫x∈A. (f x * real_cond_exp M F g x)∂M" by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def) finally show "∫x∈A. (f x * g x) ∂M = ∫x∈A. (f x * real_cond_exp M F g x)∂M" by simp qed (auto simp add: real_cond_exp_intg(1) assms) lemma real_cond_exp_add [intro]: assumes [measurable]: "integrable M f" "integrable M g" shows "AE x in M. real_cond_exp M F (λx. f x + g x) x = real_cond_exp M F f x + real_cond_exp M F g x" proof (rule real_cond_exp_charact) have "integrable M (real_cond_exp M F f)" "integrable M (real_cond_exp M F g)" using real_cond_exp_int(1) assms by auto then show "integrable M (λx. real_cond_exp M F f x + real_cond_exp M F g x)" by auto fix A assume [measurable]: "A ∈ sets F" then have "A ∈ sets M" by (meson subalg subalgebra_def subsetD) have intAf: "integrable M (λx. indicator A x * f x)" using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto have intAg: "integrable M (λx. indicator A x * g x)" using integrable_mult_indicator[OF ‹A ∈ sets M› assms(2)] by auto have "∫x∈A. (real_cond_exp M F f x + real_cond_exp M F g x)∂M = (∫x∈A. real_cond_exp M F f x ∂M) + (∫x∈A. real_cond_exp M F g x ∂M)" apply (rule set_integral_add, auto simp add: assms set_integrable_def) using integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(1)]] integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(2)]] by simp_all also have "... = (∫x. indicator A x * real_cond_exp M F f x ∂M) + (∫x. indicator A x * real_cond_exp M F g x ∂M)" unfolding set_lebesgue_integral_def by auto also have "... = (∫x. indicator A x * f x ∂M) + (∫x. indicator A x * g x ∂M)" using real_cond_exp_intg(2) assms ‹A ∈ sets F› intAf intAg by auto also have "... = (∫x∈A. f x ∂M) + (∫x∈A. g x ∂M)" unfolding set_lebesgue_integral_def by auto also have "... = ∫x∈A. (f x + g x)∂M" by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def ‹A ∈ sets M› intAf intAg) finally show "∫x∈A. (f x + g x)∂M = ∫x∈A. (real_cond_exp M F f x + real_cond_exp M F g x)∂M" by simp qed (auto simp add: assms) lemma real_cond_exp_cong: assumes ae: "AE x in M. f x = g x" and [measurable]: "f ∈ borel_measurable M" "g ∈ borel_measurable M" shows "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" proof - have "AE x in M. nn_cond_exp M F (λx. ennreal (f x)) x = nn_cond_exp M F (λx. ennreal (g x)) x" apply (rule nn_cond_exp_cong) using assms by auto moreover have "AE x in M. nn_cond_exp M F (λx. ennreal (-f x)) x = nn_cond_exp M F (λx. ennreal(-g x)) x" apply (rule nn_cond_exp_cong) using assms by auto ultimately show "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" unfolding real_cond_exp_def by auto qed lemma real_cond_exp_cmult [intro, simp]: fixes c::real assumes "integrable M f" shows "AE x in M. real_cond_exp M F (λx. c * f x) x = c * real_cond_exp M F f x" by (rule real_cond_exp_mult[where ?f = "λx. c" and ?g = f], auto simp add: assms borel_measurable_integrable) lemma real_cond_exp_cdiv [intro, simp]: fixes c::real assumes "integrable M f" shows "AE x in M. real_cond_exp M F (λx. f x / c) x = real_cond_exp M F f x / c" using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps) lemma real_cond_exp_diff [intro, simp]: assumes [measurable]: "integrable M f" "integrable M g" shows "AE x in M. real_cond_exp M F (λx. f x - g x) x = real_cond_exp M F f x - real_cond_exp M F g x" proof - have "AE x in M. real_cond_exp M F (λx. f x + (- g x)) x = real_cond_exp M F f x + real_cond_exp M F (λx. -g x) x" using real_cond_exp_add[where ?f = f and ?g = "λx. - g x"] assms by auto moreover have "AE x in M. real_cond_exp M F (λx. -g x) x = - real_cond_exp M F g x" using real_cond_exp_cmult[where ?f = g and ?c = "-1"] assms(2) by auto ultimately show ?thesis by auto qed lemma real_cond_exp_pos [intro]: assumes "AE x in M. f x ≥ 0" and [measurable]: "f ∈ borel_measurable M" shows "AE x in M. real_cond_exp M F f x ≥ 0" proof - define g where "g = (λx. max (f x) 0)" have "AE x in M. f x = g x" using assms g_def by auto then have *: "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" using real_cond_exp_cong g_def by auto have "⋀x. g x ≥ 0" unfolding g_def by simp then have "(λx. ennreal(-g x)) = (λx. 0)" by (simp add: ennreal_neg) moreover have "AE x in M. 0 = nn_cond_exp M F (λx. 0) x" by (rule nn_cond_exp_F_meas, auto) ultimately have "AE x in M. nn_cond_exp M F (λx. ennreal(-g x)) x = 0" by simp then have "AE x in M. real_cond_exp M F g x = enn2real(nn_cond_exp M F (λx. ennreal (g x)) x)" unfolding real_cond_exp_def by auto then have "AE x in M. real_cond_exp M F g x ≥ 0" by auto then show ?thesis using * by auto qed lemma real_cond_exp_mono: assumes "AE x in M. f x ≤ g x" and [measurable]: "integrable M f" "integrable M g" shows "AE x in M. real_cond_exp M F f x ≤ real_cond_exp M F g x" proof - have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (λx. g x - f x) x" by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms) moreover have "AE x in M. real_cond_exp M F (λx. g x - f x) x ≥ 0" by (rule real_cond_exp_pos, auto simp add: assms(1)) ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x ≥ 0" by auto then show ?thesis by auto qed lemma (in -) measurable_P_restriction [measurable (raw)]: assumes [measurable]: "Measurable.pred M P" "A ∈ sets M" shows "{x ∈ A. P x} ∈ sets M" proof - have "A ⊆ space M" using sets.sets_into_space[OF assms(2)]. then have "{x ∈ A. P x} = A ∩ {x ∈ space M. P x}" by blast then show ?thesis by auto qed lemma real_cond_exp_gr_c: assumes [measurable]: "integrable M f" and AE: "AE x in M. f x > c" shows "AE x in M. real_cond_exp M F f x > c" proof - define X where "X = {x ∈ space M. real_cond_exp M F f x ≤ c}" have [measurable]: "X ∈ sets F" unfolding X_def apply measurable by (metis sets.top subalg subalgebra_def) then have [measurable]: "X ∈ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast have "emeasure M X = 0" proof (rule ccontr) assume "¬(emeasure M X) = 0" have "emeasure (restr_to_subalg M F) X = emeasure M X" by (simp add: emeasure_restr_to_subalg subalg) then have "emeasure (restr_to_subalg M F) X > 0" using ‹¬(emeasure M X) = 0› gr_zeroI by auto then obtain A where "A ∈ sets (restr_to_subalg M F)" "A ⊆ X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < ∞" using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite) then have [measurable]: "A ∈ sets F" using subalg sets_restr_to_subalg by blast then have [measurable]: "A ∈ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast have Ic: "set_integrable M A (λx. c)" unfolding set_integrable_def using ‹emeasure (restr_to_subalg M F) A < ∞› emeasure_restr_to_subalg subalg by fastforce have If: "set_integrable M A f" unfolding set_integrable_def by (rule integrable_mult_indicator, auto simp add: ‹integrable M f›) have "AE x in M. indicator A x * c = indicator A x * f x" proof (rule integral_ineq_eq_0_then_AE) have "(∫x∈A. c ∂M) = (∫x∈A. f x ∂M)" proof (rule antisym) show "(∫x∈A. c ∂M) ≤ (∫x∈A. f x ∂M)" apply (rule set_integral_mono_AE) using Ic If assms(2) by auto have "(∫x∈A. f x ∂M) = (∫x∈A. real_cond_exp M F f x ∂M)" by (rule real_cond_exp_intA, auto simp add: ‹integrable M f›) also have "... ≤ (∫x∈A. c ∂M)" apply (rule set_integral_mono) unfolding set_integrable_def apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF ‹integrable M f›]) using Ic X_def ‹A ⊆ X› by (auto simp: set_integrable_def) finally show "(∫x∈A. f x ∂M) ≤ (∫x∈A. c ∂M)" by simp qed then have "measure M A * c = LINT x|M. indicat_real A x * f x" by (auto simp: set_lebesgue_integral_def) then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x" by auto show "AE x in M. indicat_real A x * c ≤ indicat_real A x * f x" using AE unfolding indicator_def by auto qed (use Ic If in ‹auto simp: set_integrable_def›) then have "AE x∈A in M. c = f x" by auto then have "AE x∈A in M. False" using assms(2) by auto have "A ∈ null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets ‹A ∈ sets M› ‹AE x∈A in M. False›) then show False using ‹emeasure (restr_to_subalg M F) A > 0› by (simp add: emeasure_restr_to_subalg null_setsD1 subalg) qed then show ?thesis using AE_iff_null_sets[OF ‹X ∈ sets M›] unfolding X_def by auto qed lemma real_cond_exp_less_c: assumes [measurable]: "integrable M f" and "AE x in M. f x < c" shows "AE x in M. real_cond_exp M F f x < c" proof - have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (λx. -f x) x" using real_cond_exp_cmult[OF ‹integrable M f›, of "-1"] by auto moreover have "AE x in M. real_cond_exp M F (λx. -f x) x > -c" apply (rule real_cond_exp_gr_c) using assms by auto ultimately show ?thesis by auto qed lemma real_cond_exp_ge_c: assumes [measurable]: "integrable M f" and "AE x in M. f x ≥ c" shows "AE x in M. real_cond_exp M F f x ≥ c" proof - obtain u::"nat ⇒ real" where u: "⋀n. u n < c" "u ⇢ c" using approx_from_below_dense_linorder[of "c-1" c] by auto have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat apply (rule real_cond_exp_gr_c) using assms ‹u n < c› by auto have "AE x in M. ∀n. real_cond_exp M F f x > u n" by (subst AE_all_countable, auto simp add: *) moreover have "real_cond_exp M F f x ≥ c" if "∀n. real_cond_exp M F f x > u n" for x proof - have "real_cond_exp M F f x ≥ u n" for n using that less_imp_le by auto then show ?thesis using u(2) LIMSEQ_le_const2 by blast qed ultimately show ?thesis by auto qed lemma real_cond_exp_le_c: assumes [measurable]: "integrable M f" and "AE x in M. f x ≤ c" shows "AE x in M. real_cond_exp M F f x ≤ c" proof - have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (λx. -f x) x" using real_cond_exp_cmult[OF ‹integrable M f›, of "-1"] by auto moreover have "AE x in M. real_cond_exp M F (λx. -f x) x ≥ -c" apply (rule real_cond_exp_ge_c) using assms by auto ultimately show ?thesis by auto qed lemma real_cond_exp_mono_strict: assumes "AE x in M. f x < g x" and [measurable]: "integrable M f" "integrable M g" shows "AE x in M. real_cond_exp M F f x < real_cond_exp M F g x" proof - have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (λx. g x - f x) x" by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms) moreover have "AE x in M. real_cond_exp M F (λx. g x - f x) x > 0" by (rule real_cond_exp_gr_c, auto simp add: assms) ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x > 0" by auto then show ?thesis by auto qed lemma real_cond_exp_nested_subalg [intro, simp]: assumes "subalgebra M G" "subalgebra G F" and [measurable]: "integrable M f" shows "AE x in M. real_cond_exp M F (real_cond_exp M G f) x = real_cond_exp M F f x" proof (rule real_cond_exp_charact) interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)]) show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1)) fix A assume [measurable]: "A ∈ sets F" then have [measurable]: "A ∈ sets G" using assms(2) by (meson set_mp subalgebra_def) have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f" by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3)) also have "... = set_lebesgue_integral M A (real_cond_exp M F f)" by (rule real_cond_exp_intA, auto simp add: assms(3)) finally show "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A (real_cond_exp M F f)" by auto qed (auto simp add: assms real_cond_exp_int(1)) lemma real_cond_exp_sum [intro, simp]: fixes f::"'b ⇒ 'a ⇒ real" assumes [measurable]: "⋀i. integrable M (f i)" shows "AE x in M. real_cond_exp M F (λx. ∑i∈I. f i x) x = (∑i∈I. real_cond_exp M F (f i) x)" proof (rule real_cond_exp_charact) fix A assume [measurable]: "A ∈ sets F" then have A_meas [measurable]: "A ∈ sets M" by (meson set_mp subalg subalgebra_def) have *: "integrable M (λx. indicator A x * f i x)" for i using integrable_mult_indicator[OF ‹A ∈ sets M› assms(1)] by auto have **: "integrable M (λx. indicator A x * real_cond_exp M F (f i) x)" for i using integrable_mult_indicator[OF ‹A ∈ sets M› real_cond_exp_int(1)[OF assms(1)]] by auto have inti: "(∫x. indicator A x * f i x ∂M) = (∫x. indicator A x * real_cond_exp M F (f i) x ∂M)" for i by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *) have "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x. (∑i∈I. indicator A x * f i x)∂M)" by (simp add: sum_distrib_left set_lebesgue_integral_def) also have "... = (∑i∈I. (∫x. indicator A x * f i x ∂M))" by (rule Bochner_Integration.integral_sum, simp add: *) also have "... = (∑i∈I. (∫x. indicator A x * real_cond_exp M F (f i) x ∂M))" using inti by auto also have "... = (∫x. (∑i∈I. indicator A x * real_cond_exp M F (f i) x)∂M)" by (rule Bochner_Integration.integral_sum[symmetric], simp add: **) also have "... = (∫x∈A. (∑i∈I. real_cond_exp M F (f i) x)∂M)" by (simp add: sum_distrib_left set_lebesgue_integral_def) finally show "(∫x∈A. (∑i∈I. f i x)∂M) = (∫x∈A. (∑i∈I. real_cond_exp M F (f i) x)∂M)" by auto qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)]) text ‹Jensen's inequality, describing the behavior of the integral under a convex function, admits a version for the conditional expectation, as follows.› theorem real_cond_exp_jensens_inequality: fixes q :: "real ⇒ real" assumes X: "integrable M X" "AE x in M. X x ∈ I" assumes I: "I = {a <..< b} ∨ I = {a <..} ∨ I = {..< b} ∨ I = UNIV" assumes q: "integrable M (λx. q (X x))" "convex_on I q" "q ∈ borel_measurable borel" shows "AE x in M. real_cond_exp M F X x ∈ I" "AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x" proof - have "open I" using I by auto then have "interior I = I" by (simp add: interior_eq) have [measurable]: "I ∈ sets borel" using I by auto define phi where "phi = (λx. Inf ((λt. (q x - q t) / (x - t)) ` ({x<..} ∩ I)))" have **: "q (X x) ≥ q (real_cond_exp M F X x) + phi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)" if "X x ∈ I" "real_cond_exp M F X x ∈ I" for x unfolding phi_def apply (rule convex_le_Inf_differential) using ‹convex_on I q› that ‹interior I = I› by auto text ‹It is not clear that the function $\phi$ is measurable. We replace it by a version which is better behaved.› define psi where "psi = (λx. phi x * indicator I x)" have A: "psi y = phi y" if "y ∈ I" for y unfolding psi_def indicator_def using that by auto have *: "q (X x) ≥ q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)" if "X x ∈ I" "real_cond_exp M F X x ∈ I" for x unfolding A[OF ‹real_cond_exp M F X x ∈ I›] using ** that by auto note I moreover have "AE x in M. real_cond_exp M F X x > a" if "I ⊆ {a <..}" for a apply (rule real_cond_exp_gr_c) using X that by auto moreover have "AE x in M. real_cond_exp M F X x < b" if "I ⊆ {..<b}" for b apply (rule real_cond_exp_less_c) using X that by auto ultimately show "AE x in M. real_cond_exp M F X x ∈ I" by (elim disjE) (auto simp: subset_eq) then have main_ineq: "AE x in M. q (X x) ≥ q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)" using * X(2) by auto text ‹Then, one wants to take the conditional expectation of this inequality. On the left, one gets the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The trick is to multiply by a $F$-measurable function which is small enough to make everything integrable.› obtain f::"'a ⇒ real" where [measurable]: "f ∈ borel_measurable (restr_to_subalg M F)" "integrable (restr_to_subalg M F) f" and f: "⋀x. f x > 0" "⋀x. f x ≤ 1" using sigma_finite_measure.obtain_positive_integrable_function[OF sigma_fin_subalg] by metis then have [measurable]: "f ∈ borel_measurable F" by (simp add: subalg) then have [measurable]: "f ∈ borel_measurable M" using measurable_from_subalg[OF subalg] by blast define g where "g = (λx. f x/(1+ ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦))" define G where "G = (λx. g x * psi (real_cond_exp M F X x))" have g: "g x > 0" "g x ≤ 1" for x unfolding G_def g_def using f[of x] by (auto simp add: abs_mult) have G: "¦G x¦ ≤ 1" for x unfolding G_def g_def using f[of x] proof (auto simp add: abs_mult) have "f x * ¦psi (real_cond_exp M F X x)¦ ≤ 1 * ¦psi (real_cond_exp M F X x)¦" apply (rule mult_mono) using f[of x] by auto also have "... ≤ 1 + ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦" by auto finally show "f x * ¦psi (real_cond_exp M F X x)¦ ≤ 1 + ¦psi (real_cond_exp M F X x)¦ + ¦q (real_cond_exp M F X x)¦" by simp qed have "AE x in M. g x * q (X x) ≥ g x * (q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x))" using main_ineq g by (auto simp add: divide_simps) then have main_G: "AE x in M. g x * q (X x) ≥ g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)" unfolding G_def by (auto simp add: algebra_simps) text ‹To proceed, we need to know that $\psi$ is measurable.› have phi_mono: "phi x ≤ phi y" if "x ≤ y" "x ∈ I" "y ∈ I" for x y proof (cases "x < y") case True have "q x + phi x * (y-x) ≤ q y" unfolding phi_def apply (rule convex_le_Inf_differential) using ‹convex_on I q› that ‹interior I = I› by auto then have "phi x ≤ (q x - q y) / (x - y)" using that ‹x < y› by (auto simp add: divide_simps algebra_simps) moreover have "(q x - q y)/(x - y) ≤ phi y" unfolding phi_def proof (rule cInf_greatest, auto) fix t assume "t ∈ I" "y < t" have "(q x - q y) / (x - y) ≤ (q x - q t) / (x - t)" apply (rule convex_on_diff[OF q(2)]) using ‹y < t› ‹x < y› ‹t ∈ I› ‹x ∈ I› by auto also have "... ≤ (q y - q t) / (y - t)" apply (rule convex_on_diff[OF q(2)]) using ‹y < t› ‹x < y› ‹t ∈ I› ‹x ∈ I› by auto finally show "(q x - q y) / (x - y) ≤ (q y - q t) / (y - t)" by simp next obtain e where "0 < e" "ball y e ⊆ I" using ‹open I› ‹y ∈ I› openE by blast then have "y + e/2 ∈ {y<..} ∩ I" by (auto simp: dist_real_def) then show "{y<..} ∩ I = {} ⟹ False" by auto qed ultimately show "phi x ≤ phi y" by auto next case False then have "x = y" using ‹x ≤ y› by auto then show ?thesis by auto qed have [measurable]: "psi ∈ borel_measurable borel" by (rule borel_measurable_piecewise_mono[of "{I, -I}"]) (auto simp add: psi_def indicator_def phi_mono intro: mono_onI) have [measurable]: "q ∈ borel_measurable borel" using q by simp have [measurable]: "X ∈ borel_measurable M" "real_cond_exp M F X ∈ borel_measurable F" "g ∈ borel_measurable F" "g ∈ borel_measurable M" "G ∈ borel_measurable F" "G ∈ borel_measurable M" using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto have int1: "integrable (restr_to_subalg M F) (λx. g x * q (real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg ‹integrable (restr_to_subalg M F) f›) unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps) have int2: "integrable M (λx. G x * (X x - real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦X x¦ + ¦real_cond_exp M F X x¦"]) apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int ‹integrable M X› AE_I2) using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le) have int3: "integrable M (λx. g x * q (X x))" apply (rule Bochner_Integration.integrable_bound[of _ "λx. q(X x)"], auto simp add: q(1) abs_mult) using g by (simp add: less_imp_le mult_left_le_one_le) text ‹Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get the following.› have "AE x in M. real_cond_exp M F (λx. g x * q (X x)) x ≥ real_cond_exp M F (λx. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x" apply (rule real_cond_exp_mono[OF main_G]) apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]]) using int2 int3 by auto text ‹This reduces to the desired inequality thanks to the properties of conditional expectation, i.e., the conditional expectation of an $F$-measurable function is this function, and one can multiply an $F$-measurable function outside of conditional expectations. Since all these equalities only hold almost everywhere, we formulate them separately, and then combine all of them to simplify the above equation, again almost everywhere.› moreover have "AE x in M. real_cond_exp M F (λx. g x * q (X x)) x = g x * real_cond_exp M F (λx. q (X x)) x" by (rule real_cond_exp_mult, auto simp add: int3) moreover have "AE x in M. real_cond_exp M F (λx. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x = real_cond_exp M F (λx. g x * q (real_cond_exp M F X x)) x + real_cond_exp M F (λx. G x * (X x - real_cond_exp M F X x)) x" by (rule real_cond_exp_add, auto simp add: integrable_from_subalg[OF subalg int1] int2) moreover have "AE x in M. real_cond_exp M F (λx. g x * q (real_cond_exp M F X x)) x = g x * q (real_cond_exp M F X x)" by (rule real_cond_exp_F_meas, auto simp add: integrable_from_subalg[OF subalg int1]) moreover have "AE x in M. real_cond_exp M F (λx. G x * (X x - real_cond_exp M F X x)) x = G x * real_cond_exp M F (λx. (X x - real_cond_exp M F X x)) x" by (rule real_cond_exp_mult, auto simp add: int2) moreover have "AE x in M. real_cond_exp M F (λx. (X x - real_cond_exp M F X x)) x = real_cond_exp M F X x - real_cond_exp M F (λx. real_cond_exp M F X x) x" by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int ‹integrable M X›) moreover have "AE x in M. real_cond_exp M F (λx. real_cond_exp M F X x) x = real_cond_exp M F X x " by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int ‹integrable M X›) ultimately have "AE x in M. g x * real_cond_exp M F (λx. q (X x)) x ≥ g x * q (real_cond_exp M F X x)" by auto then show "AE x in M. real_cond_exp M F (λx. q (X x)) x ≥ q (real_cond_exp M F X x)" using g(1) by (auto simp add: divide_simps) qed text ‹Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper bound for it. Indeed, this is not true in general, as the following counterexample shows: on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$ for integer $n$. Let $q(x) = - \sqrt{x}$ for $x\geq 0$. Define $X$ which is equal to $1/n$ over $[n, n+1/n)$ and $2^{-n}$ on $[n+1/n, n+1)$. Then $X$ is integrable as $\sum 1/n^2 < \infty$, and $q(X)$ is integrable as $\sum 1/n^{3/2} < \infty$. On the other hand, $E(X|F)$ is essentially equal to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not integrable. However, this counterexample is essentially the only situation where this function is not integrable, as shown by the next lemma. › lemma integrable_convex_cond_exp: fixes q :: "real ⇒ real" assumes X: "integrable M X" "AE x in M. X x ∈ I" assumes I: "I = {a <..< b} ∨ I = {a <..} ∨ I = {..< b} ∨ I = UNIV" assumes q: "integrable M (λx. q (X x))" "convex_on I q" "q ∈ borel_measurable borel" assumes H: "emeasure M (space M) = ∞ ⟹ 0 ∈ I" shows "integrable M (λx. q (real_cond_exp M F X x))" proof - have [measurable]: "(λx. q (real_cond_exp M F X x)) ∈ borel_measurable M" "q ∈ borel_measurable borel" "X ∈ borel_measurable M" using X(1) q(3) by auto have "open I" using I by auto then have "interior I = I" by (simp add: interior_eq) consider "emeasure M (space M) = 0" | "emeasure M (space M) > 0 ∧ emeasure M (space M) < ∞" | "emeasure M (space M) = ∞" by (metis infinity_ennreal_def not_gr_zero top.not_eq_extremum) then show ?thesis proof (cases) case 1 show ?thesis by (subst integrable_cong_AE[of _ _ "λx. 0"], auto intro: emeasure_0_AE[OF 1]) next case 2 interpret finite_measure M using 2 by (auto intro!: finite_measureI) have "I ≠ {}" using ‹AE x in M. X x ∈ I› 2 eventually_mono integral_less_AE_space by fastforce then obtain z where "z ∈ I" by auto define A where "A = Inf ((λt. (q z - q t) / (z - t)) ` ({z<..} ∩ I))" have "q y ≥ q z + A * (y - z)" if "y ∈ I" for y unfolding A_def apply (rule convex_le_Inf_differential) using ‹z ∈ I› ‹y ∈ I› ‹interior I = I› q(2) by auto then have "AE x in M. q (real_cond_exp M F X x) ≥ q z + A * (real_cond_exp M F X x - z)" using real_cond_exp_jensens_inequality(1)[OF X I q] by auto moreover have "AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x" using real_cond_exp_jensens_inequality(2)[OF X I q] by auto moreover have "¦a¦ ≤ ¦b¦ + ¦c¦" if "b ≤ a ∧ a ≤ c" for a b c::real using that by auto ultimately have *: "AE x in M. ¦q (real_cond_exp M F X x)¦ ≤ ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦q z + A * (real_cond_exp M F X x - z)¦" by auto show "integrable M (λx. q (real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦q z + A * (real_cond_exp M F X x - z)¦"]) apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1)) using X(1) q(1) * by auto next case 3 then have "0 ∈ I" using H finite_measure.finite_emeasure_space by auto have "q(0) = 0" proof (rule ccontr) assume *: "¬(q(0) = 0)" define e where "e = ¦q(0)¦ / 2" then have "e > 0" using * by auto have "continuous (at 0) q" using q(2) ‹0 ∈ I› ‹open I› ‹interior I = I› continuous_on_interior convex_on_continuous by blast then obtain d where d: "d > 0" "⋀y. ¦y - 0¦ < d ⟹ ¦q y - q 0¦ < e" using ‹e > 0› by (metis continuous_at_real_range real_norm_def) then have *: "¦q(y)¦ > e" if "¦y¦ < d" for y proof - have "¦q 0¦ ≤ ¦q 0 - q y¦ + ¦q y¦" by auto also have "... < e + ¦q y¦" using d(2) that by force finally have "¦q y¦ > ¦q 0¦ - e" by auto then show ?thesis unfolding e_def by simp qed have "emeasure M {x ∈ space M. ¦X x¦ < d} ≤ emeasure M ({x ∈ space M. 1 ≤ ennreal(1/e) * ¦q(X x)¦} ∩ space M)" by (rule emeasure_mono, auto simp add: * ‹e>0› less_imp_le ennreal_mult''[symmetric]) also have "... ≤ (1/e) * (∫⇧^{+}x. ennreal(¦q(X x)¦) * indicator (space M) x ∂M)" by (rule nn_integral_Markov_inequality, auto) also have "... = (1/e) * (∫⇧^{+}x. ennreal(¦q(X x)¦) ∂M)" by auto also have "... = (1/e) * ennreal(∫x. ¦q(X x)¦ ∂M)" using nn_integral_eq_integral[OF integrable_abs[OF q(1)]] by auto also have "... < ∞" by (simp add: ennreal_mult_less_top) finally have A: "emeasure M {x ∈ space M. ¦X x¦ < d} < ∞" by simp have "{x ∈ space M. ¦X x¦ ≥ d} = {x ∈ space M. 1 ≤ ennreal(1/d) * ¦X x¦} ∩ space M" by (auto simp add: ‹d>0› ennreal_mult''[symmetric]) then have "emeasure M {x ∈ space M. ¦X x¦ ≥ d} = emeasure M ({x ∈ space M. 1 ≤ ennreal(1/d) * ¦X x¦} ∩ space M)" by auto also have "... ≤ (1/d) * (∫⇧^{+}x. ennreal(¦X x¦) * indicator (space M) x ∂M)" by (rule nn_integral_Markov_inequality, auto) also have "... = (1/d) * (∫⇧^{+}x. ennreal(¦X x¦) ∂M)" by auto also have "... = (1/d) * ennreal(∫x. ¦X x¦ ∂M)" using nn_integral_eq_integral[OF integrable_abs[OF X(1)]] by auto also have "... < ∞" by (simp add: ennreal_mult_less_top) finally have B: "emeasure M {x ∈ space M. ¦X x¦ ≥ d} < ∞" by simp have "space M = {x ∈ space M. ¦X x¦ < d} ∪ {x ∈ space M. ¦X x¦ ≥ d}" by auto then have "emeasure M (space M) = emeasure M ({x ∈ space M. ¦X x¦ < d} ∪ {x ∈ space M. ¦X x¦ ≥ d})" by simp also have "... ≤ emeasure M {x ∈ space M. ¦X x¦ < d} + emeasure M {x ∈ space M. ¦X x¦ ≥ d}" by (auto intro!: emeasure_subadditive) also have "... < ∞" using A B by auto finally show False using ‹emeasure M (space M) = ∞› by auto qed define A where "A = Inf ((λt. (q 0 - q t) / (0 - t)) ` ({0<..} ∩ I))" have "q y ≥ q 0 + A * (y - 0)" if "y ∈ I" for y unfolding A_def apply (rule convex_le_Inf_differential) using ‹0 ∈ I› ‹y ∈ I› ‹interior I = I› q(2) by auto then have "q y ≥ A * y" if "y ∈ I" for y using ‹q 0 = 0› that by auto then have "AE x in M. q (real_cond_exp M F X x) ≥ A * real_cond_exp M F X x" using real_cond_exp_jensens_inequality(1)[OF X I q] by auto moreover have "AE x in M. q (real_cond_exp M F X x) ≤ real_cond_exp M F (λx. q (X x)) x" using real_cond_exp_jensens_inequality(2)[OF X I q] by auto moreover have "¦a¦ ≤ ¦b¦ + ¦c¦" if "b ≤ a ∧ a ≤ c" for a b c::real using that by auto ultimately have *: "AE x in M. ¦q (real_cond_exp M F X x)¦ ≤ ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦A * real_cond_exp M F X x¦" by auto show "integrable M (λx. q (real_cond_exp M F X x))" apply (rule Bochner_Integration.integrable_bound[of _ "λx. ¦real_cond_exp M F (λx. q (X x)) x¦ + ¦A * real_cond_exp M F X x ¦"]) apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1)) using X(1) q(1) * by auto qed qed end end