1(* Author: S��bastien Gou��zel sebastien.gouezel@univ-rennes1.fr 2 License: BSD 3*) 4 5section \<open>Conditional Expectation\<close> 6 7theory Conditional_Expectation 8imports Probability_Measure 9begin 10 11subsection \<open>Restricting a measure to a sub-sigma-algebra\<close> 12 13definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where 14 "subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))" 15 16lemma sub_measure_space: 17 assumes i: "subalgebra M F" 18 shows "measure_space (space M) (sets F) (emeasure M)" 19proof - 20 have "sigma_algebra (space M) (sets F)" 21 by (metis i measure_space measure_space_def subalgebra_def) 22 moreover have "positive (sets F) (emeasure M)" 23 using Sigma_Algebra.positive_def by auto 24 moreover have "countably_additive (sets F) (emeasure M)" 25 by (meson countably_additive_def emeasure_countably_additive i order_trans subalgebra_def subsetCE) 26 ultimately show ?thesis unfolding measure_space_def by simp 27qed 28 29definition restr_to_subalg::"'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where 30 "restr_to_subalg M F = measure_of (space M) (sets F) (emeasure M)" 31 32lemma space_restr_to_subalg: 33 "space (restr_to_subalg M F) = space M" 34unfolding restr_to_subalg_def by (simp add: space_measure_of_conv) 35 36lemma sets_restr_to_subalg [measurable_cong]: 37 assumes "subalgebra M F" 38 shows "sets (restr_to_subalg M F) = sets F" 39unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def) 40 41lemma emeasure_restr_to_subalg: 42 assumes "subalgebra M F" 43 "A \<in> sets F" 44 shows "emeasure (restr_to_subalg M F) A = emeasure M A" 45unfolding restr_to_subalg_def 46by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq) 47 48lemma null_sets_restr_to_subalg: 49 assumes "subalgebra M F" 50 shows "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F" 51proof 52 have "x \<in> null_sets M \<inter> sets F" if "x \<in> null_sets (restr_to_subalg M F)" for x 53 by (metis that Int_iff assms emeasure_restr_to_subalg null_setsD1 null_setsD2 null_setsI 54 sets_restr_to_subalg subalgebra_def subsetD) 55 then show "null_sets (restr_to_subalg M F) \<subseteq> null_sets M \<inter> sets F" by auto 56next 57 have "x \<in> null_sets (restr_to_subalg M F)" if "x \<in> null_sets M \<inter> sets F" for x 58 by (metis that Int_iff assms null_setsD1 null_setsI sets_restr_to_subalg emeasure_restr_to_subalg[OF assms]) 59 then show "null_sets M \<inter> sets F \<subseteq> null_sets (restr_to_subalg M F)" by auto 60qed 61 62lemma AE_restr_to_subalg: 63 assumes "subalgebra M F" 64 "AE x in (restr_to_subalg M F). P x" 65 shows "AE x in M. P x" 66proof - 67 obtain A where A: "\<And>x. x \<in> space (restr_to_subalg M F) - A \<Longrightarrow> P x" "A \<in> null_sets (restr_to_subalg M F)" 68 using AE_E3[OF assms(2)] by auto 69 then have "A \<in> null_sets M" using null_sets_restr_to_subalg[OF assms(1)] by auto 70 moreover have "\<And>x. x \<in> space M - A \<Longrightarrow> P x" 71 using space_restr_to_subalg A(1) by fastforce 72 ultimately show ?thesis 73 unfolding eventually_ae_filter by auto 74qed 75 76lemma AE_restr_to_subalg2: 77 assumes "subalgebra M F" 78 "AE x in M. P x" and [measurable]: "P \<in> measurable F (count_space UNIV)" 79 shows "AE x in (restr_to_subalg M F). P x" 80proof - 81 define U where "U = {x \<in> space M. \<not>(P x)}" 82 then have *: "U = {x \<in> space F. \<not>(P x)}" using assms(1) by (simp add: subalgebra_def) 83 then have "U \<in> sets F" by simp 84 then have "U \<in> sets M" using assms(1) by (meson subalgebra_def subsetD) 85 then have "U \<in> null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast 86 then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] \<open>U \<in> sets F\<close> by auto 87 then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg) 88qed 89 90lemma prob_space_restr_to_subalg: 91 assumes "subalgebra M F" 92 "prob_space M" 93 shows "prob_space (restr_to_subalg M F)" 94by (metis (no_types, lifting) assms(1) assms(2) emeasure_restr_to_subalg prob_space.emeasure_space_1 prob_spaceI 95 sets.top space_restr_to_subalg subalgebra_def) 96 97lemma finite_measure_restr_to_subalg: 98 assumes "subalgebra M F" 99 "finite_measure M" 100 shows "finite_measure (restr_to_subalg M F)" 101by (metis (no_types, lifting) assms emeasure_restr_to_subalg finite_measure.finite_emeasure_space 102 finite_measureI sets.top space_restr_to_subalg subalgebra_def infinity_ennreal_def) 103 104lemma measurable_in_subalg: 105 assumes "subalgebra M F" 106 "f \<in> measurable F N" 107 shows "f \<in> measurable (restr_to_subalg M F) N" 108by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)]) 109 110lemma measurable_in_subalg': 111 assumes "subalgebra M F" 112 "f \<in> measurable (restr_to_subalg M F) N" 113 shows "f \<in> measurable F N" 114by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)]) 115 116lemma measurable_from_subalg: 117 assumes "subalgebra M F" 118 "f \<in> measurable F N" 119 shows "f \<in> measurable M N" 120using assms unfolding measurable_def subalgebra_def by auto 121 122text\<open>The following is the direct transposition of \verb+nn_integral_subalgebra+ 123(from \verb+Nonnegative_Lebesgue_Integration+) in the 124current notations, with the removal of the useless assumption $f \geq 0$.\<close> 125 126lemma nn_integral_subalgebra2: 127 assumes "subalgebra M F" and [measurable]: "f \<in> borel_measurable F" 128 shows "(\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. f x \<partial>M)" 129proof (rule nn_integral_subalgebra) 130 show "f \<in> borel_measurable (restr_to_subalg M F)" 131 by (rule measurable_in_subalg[OF assms(1)]) simp 132 show "sets (restr_to_subalg M F) \<subseteq> sets M" by (metis sets_restr_to_subalg[OF assms(1)] assms(1) subalgebra_def) 133 fix A assume "A \<in> sets (restr_to_subalg M F)" 134 then show "emeasure (restr_to_subalg M F) A = emeasure M A" 135 by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)]) 136qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)]) 137 138text\<open>The following is the direct transposition of \verb+integral_subalgebra+ 139(from \verb+Bochner_Integration+) in the current notations.\<close> 140 141lemma integral_subalgebra2: 142 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 143 assumes "subalgebra M F" and 144 [measurable]: "f \<in> borel_measurable F" 145 shows "(\<integral>x. f x \<partial>(restr_to_subalg M F)) = (\<integral>x. f x \<partial>M)" 146by (rule integral_subalgebra, 147 metis measurable_in_subalg[OF assms(1)] assms(2), 148 auto simp add: assms space_restr_to_subalg sets_restr_to_subalg emeasure_restr_to_subalg, 149 meson assms(1) subalgebra_def subset_eq) 150 151lemma integrable_from_subalg: 152 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 153 assumes "subalgebra M F" 154 "integrable (restr_to_subalg M F) f" 155 shows "integrable M f" 156proof (rule integrableI_bounded) 157 have [measurable]: "f \<in> borel_measurable F" using assms by auto 158 then show "f \<in> borel_measurable M" using assms(1) measurable_from_subalg by blast 159 160 have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F))" 161 by (rule nn_integral_subalgebra2[symmetric], auto simp add: assms) 162 also have "... < \<infinity>" using integrable_iff_bounded assms by auto 163 finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by simp 164qed 165 166lemma integrable_in_subalg: 167 fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" 168 assumes [measurable]: "subalgebra M F" 169 "f \<in> borel_measurable F" 170 "integrable M f" 171 shows "integrable (restr_to_subalg M F) f" 172proof (rule integrableI_bounded) 173 show "f \<in> borel_measurable (restr_to_subalg M F)" using assms(2) assms(1) by auto 174 have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)" 175 by (rule nn_integral_subalgebra2, auto simp add: assms) 176 also have "... < \<infinity>" using integrable_iff_bounded assms by auto 177 finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) < \<infinity>" by simp 178qed 179 180subsection \<open>Nonnegative conditional expectation\<close> 181 182text \<open>The conditional expectation of a function $f$, on a measure space $M$, with respect to a 183sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any 184$F$-set coincides with the integral of $f$. 185Such a function is uniquely defined almost everywhere. 186The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$, 187and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$. 188Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable 189functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$ 190machinery, and works for all positive functions. 191 192In this paragraph, we develop the definition and basic properties for nonnegative functions, 193as the basics of the general case. As in the definition of integrals, the nonnegative case is done 194with ennreal-valued functions, without any integrability assumption. 195\<close> 196 197definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)" 198where 199 "nn_cond_exp M F f = 200 (if f \<in> borel_measurable M \<and> subalgebra M F 201 then RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M f) F) 202 else (\<lambda>_. 0))" 203 204lemma 205 shows borel_measurable_nn_cond_exp [measurable]: "nn_cond_exp M F f \<in> borel_measurable F" 206 and borel_measurable_nn_cond_exp2 [measurable]: "nn_cond_exp M F f \<in> borel_measurable M" 207by (simp_all add: nn_cond_exp_def) 208 (metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def) 209 210text \<open>The good setting for conditional expectations is the situation where the subalgebra $F$ 211gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite, 212think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case, 213conditional expectations have to be constant functions, so they have integral $0$ or $\infty$. 214This means that a positive integrable function can have no meaningful conditional expectation.\<close> 215 216locale sigma_finite_subalgebra = 217 fixes M F::"'a measure" 218 assumes subalg: "subalgebra M F" 219 and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)" 220 221lemma sigma_finite_subalgebra_is_sigma_finite: 222 assumes "sigma_finite_subalgebra M F" 223 shows "sigma_finite_measure M" 224proof 225 have subalg: "subalgebra M F" 226 and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)" 227 using assms unfolding sigma_finite_subalgebra_def by auto 228 obtain A where Ap: "countable A \<and> A \<subseteq> sets (restr_to_subalg M F) \<and> \<Union>A = space (restr_to_subalg M F) \<and> (\<forall>a\<in>A. emeasure (restr_to_subalg M F) a \<noteq> \<infinity>)" 229 using sigma_finite_measure.sigma_finite_countable[OF sigma_fin_subalg] by fastforce 230 have "A \<subseteq> sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce 231 then have "A \<subseteq> sets M" using subalg subalgebra_def by force 232 moreover have "\<Union>A = space M" using Ap space_restr_to_subalg by simp 233 moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] \<open>A \<subseteq> sets F\<close> Ap) 234 ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)" using Ap by auto 235qed 236 237sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure 238using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast 239 240text \<open>Conditional expectations are very often used in probability spaces. This is a special case 241of the previous one, as we prove now.\<close> 242 243locale finite_measure_subalgebra = finite_measure + 244 fixes F::"'a measure" 245 assumes subalg: "subalgebra M F" 246 247lemma finite_measure_subalgebra_is_sigma_finite: 248 assumes "finite_measure_subalgebra M F" 249 shows "sigma_finite_subalgebra M F" 250proof - 251 interpret finite_measure_subalgebra M F using assms by simp 252 have "finite_measure (restr_to_subalg M F)" 253 using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast 254 then have "sigma_finite_measure (restr_to_subalg M F)" 255 unfolding finite_measure_def by simp 256 then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp 257qed 258 259sublocale finite_measure_subalgebra \<subseteq> sigma_finite_subalgebra 260proof - 261 have "finite_measure (restr_to_subalg M F)" 262 using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast 263 then have "sigma_finite_measure (restr_to_subalg M F)" 264 unfolding finite_measure_def by simp 265 then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp 266qed 267 268context sigma_finite_subalgebra 269begin 270 271text\<open>The next lemma is arguably the most fundamental property of conditional expectation: 272when computing an expectation against an $F$-measurable function, it is equivalent to work 273with a function or with its $F$-conditional expectation. 274 275This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows. 276From this point on, we will only work with it, and forget completely about 277the definition using Radon-Nikodym derivatives. 278\<close> 279 280lemma nn_cond_exp_intg: 281 assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M" 282 shows "(\<integral>\<^sup>+ x. f x * nn_cond_exp M F g x \<partial>M) = (\<integral>\<^sup>+ x. f x * g x \<partial>M)" 283proof - 284 have [measurable]: "f \<in> borel_measurable M" 285 by (meson assms subalg borel_measurable_subalgebra subalgebra_def) 286 have ac: "absolutely_continuous (restr_to_subalg M F) (restr_to_subalg (density M g) F)" 287 unfolding absolutely_continuous_def 288 proof - 289 have "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F" by (rule null_sets_restr_to_subalg[OF subalg]) 290 moreover have "null_sets M \<subseteq> null_sets (density M g)" 291 by (rule absolutely_continuousI_density[unfolded absolutely_continuous_def]) auto 292 ultimately have "null_sets (restr_to_subalg M F) \<subseteq> null_sets (density M g) \<inter> sets F" by auto 293 moreover have "null_sets (density M g) \<inter> sets F = null_sets (restr_to_subalg (density M g) F)" 294 by (rule null_sets_restr_to_subalg[symmetric]) (metis subalg sets_density space_density subalgebra_def) 295 ultimately show "null_sets (restr_to_subalg M F) \<subseteq> null_sets (restr_to_subalg (density M g) F)" by auto 296 qed 297 298 have "(\<integral>\<^sup>+ x. f x * nn_cond_exp M F g x \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_cond_exp M F g x \<partial>(restr_to_subalg M F))" 299 by (rule nn_integral_subalgebra2[symmetric]) (simp_all add: assms subalg) 300 also have "... = (\<integral>\<^sup>+ x. f x * RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x \<partial>(restr_to_subalg M F))" 301 unfolding nn_cond_exp_def using assms subalg by simp 302 also have "... = (\<integral>\<^sup>+ x. RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M g) F) x * f x \<partial>(restr_to_subalg M F))" 303 by (simp add: mult.commute) 304 also have "... = (\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg (density M g) F))" 305 proof (rule sigma_finite_measure.RN_deriv_nn_integral[symmetric]) 306 show "sets (restr_to_subalg (density M g) F) = sets (restr_to_subalg M F)" 307 by (metis subalg restr_to_subalg_def sets.sets_measure_of_eq space_density subalgebra_def) 308 qed (auto simp add: assms measurable_restrict ac measurable_in_subalg subalg sigma_fin_subalg) 309 also have "... = (\<integral>\<^sup>+ x. f x \<partial>(density M g))" 310 by (metis nn_integral_subalgebra2 subalg assms(1) sets_density space_density subalgebra_def) 311 also have "... = (\<integral>\<^sup>+ x. g x * f x \<partial>M)" 312 by (rule nn_integral_density) (simp_all add: assms) 313 also have "... = (\<integral>\<^sup>+ x. f x * g x \<partial>M)" 314 by (simp add: mult.commute) 315 finally show ?thesis by simp 316qed 317 318lemma nn_cond_exp_charact: 319 assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+ x \<in> A. g x \<partial>M)" and 320 [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable F" 321 shows "AE x in M. g x = nn_cond_exp M F f x" 322proof - 323 let ?MF = "restr_to_subalg M F" 324 { 325 fix A assume "A \<in> sets ?MF" 326 then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp 327 have "(\<integral>\<^sup>+ x \<in> A. g x \<partial> ?MF) = (\<integral>\<^sup>+ x \<in> A. g x \<partial>M)" 328 by (simp add: nn_integral_subalgebra2 subalg) 329 also have "... = (\<integral>\<^sup>+ x \<in> A. f x \<partial>M)" using assms(1) by simp 330 also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (simp add: mult.commute) 331 also have "... = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M F f x \<partial>M)" 332 by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms) 333 also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial>M)" by (simp add: mult.commute) 334 also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial> ?MF)" 335 by (simp add: nn_integral_subalgebra2 subalg) 336 finally have "(\<integral>\<^sup>+ x \<in> A. g x \<partial> ?MF) = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial> ?MF)" by simp 337 } note * = this 338 have "AE x in ?MF. g x = nn_cond_exp M F f x" 339 by (rule sigma_finite_measure.density_unique2) 340 (auto simp add: assms subalg sigma_fin_subalg AE_restr_to_subalg2 *) 341 then show ?thesis using AE_restr_to_subalg[OF subalg] by simp 342qed 343 344lemma nn_cond_exp_F_meas: 345 assumes "f \<in> borel_measurable F" 346 shows "AE x in M. f x = nn_cond_exp M F f x" 347by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg]) 348 349lemma nn_cond_exp_prod: 350 assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M" 351 shows "AE x in M. f x * nn_cond_exp M F g x = nn_cond_exp M F (\<lambda>x. f x * g x) x" 352proof (rule nn_cond_exp_charact) 353 have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(1)]) 354 show "(\<lambda>x. f x * g x) \<in> borel_measurable M" by measurable 355 356 fix A assume "A \<in> sets F" 357 then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable 358 have "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M" 359 by (simp add: mult.commute mult.left_commute) 360 also have "... = \<integral>\<^sup>+x. (f x * indicator A x) * nn_cond_exp M F g x \<partial>M" 361 by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms) 362 also have "... = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M" 363 by (simp add: mult.commute mult.left_commute) 364 finally show "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M" by simp 365qed (auto simp add: assms) 366 367lemma nn_cond_exp_sum: 368 assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 369 shows "AE x in M. nn_cond_exp M F f x + nn_cond_exp M F g x = nn_cond_exp M F (\<lambda>x. f x + g x) x" 370proof (rule nn_cond_exp_charact) 371 fix A assume [measurable]: "A \<in> sets F" 372 then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD) 373 have "\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)" 374 by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>) 375 also have "... = (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F g x \<partial>M)" 376 by (metis (no_types, lifting) mult.commute nn_integral_cong) 377 also have "... = (\<integral>\<^sup>+x. indicator A x * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * g x \<partial>M)" 378 by (simp add: nn_cond_exp_intg) 379 also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)" 380 by (metis (no_types, lifting) mult.commute nn_integral_cong) 381 also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M" 382 by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>) 383 finally show "\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M = \<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M" 384 by simp 385qed (auto simp add: assms) 386 387lemma nn_cond_exp_cong: 388 assumes "AE x in M. f x = g x" 389 and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 390 shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x" 391proof (rule nn_cond_exp_charact) 392 fix A assume [measurable]: "A \<in> sets F" 393 have "\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M = \<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M" 394 by (simp add: mult.commute) 395 also have "... = \<integral>\<^sup>+x. indicator A x * f x \<partial>M" by (simp add: nn_cond_exp_intg assms) 396 also have "... = \<integral>\<^sup>+x\<in>A. f x \<partial>M" by (simp add: mult.commute) 397 also have "... = \<integral>\<^sup>+x\<in>A. g x \<partial>M" by (rule nn_set_integral_cong[OF assms(1)]) 398 finally show "\<integral>\<^sup>+x\<in>A. g x \<partial>M = \<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M" by simp 399qed (auto simp add: assms) 400 401lemma nn_cond_exp_mono: 402 assumes "AE x in M. f x \<le> g x" 403 and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 404 shows "AE x in M. nn_cond_exp M F f x \<le> nn_cond_exp M F g x" 405proof - 406 define h where "h = (\<lambda>x. g x - f x)" 407 have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp 408 have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add) 409 have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F (\<lambda>x. f x + h x) x" 410 by (rule nn_cond_exp_cong) (auto simp add: * assms) 411 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 (\<lambda>x. f x + h x) x" 412 by (rule nn_cond_exp_sum) (auto simp add: assms) 413 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 414 then show ?thesis by force 415qed 416 417lemma nested_subalg_is_sigma_finite: 418 assumes "subalgebra M G" "subalgebra G F" 419 shows "sigma_finite_subalgebra M G" 420unfolding sigma_finite_subalgebra_def 421proof (auto simp add: assms) 422 have "\<exists>A. countable A \<and> A \<subseteq> sets (restr_to_subalg M F) \<and> \<Union>A = space (restr_to_subalg M F) \<and> (\<forall>a\<in>A. emeasure (restr_to_subalg M F) a \<noteq> \<infinity>)" 423 using sigma_fin_subalg sigma_finite_measure_def by auto 424 then obtain A where A:"countable A \<and> A \<subseteq> sets (restr_to_subalg M F) \<and> \<Union>A = space (restr_to_subalg M F) \<and> (\<forall>a\<in>A. emeasure (restr_to_subalg M F) a \<noteq> \<infinity>)" 425 by auto 426 have "sets F \<subseteq> sets M" 427 by (meson assms order_trans subalgebra_def) 428 then have "countable A \<and> A \<subseteq> sets (restr_to_subalg M G) \<and> \<Union>A = space (restr_to_subalg M F) \<and> (\<forall>a\<in>A. emeasure (restr_to_subalg M G) a \<noteq> \<infinity>)" 429 by (metis (no_types) A assms basic_trans_rules(31) emeasure_restr_to_subalg order_trans sets_restr_to_subalg subalgebra_def) 430 then show "sigma_finite_measure (restr_to_subalg M G)" 431 by (metis sigma_finite_measure.intro space_restr_to_subalg) 432qed 433 434lemma nn_cond_exp_nested_subalg: 435 assumes "subalgebra M G" "subalgebra G F" 436 and [measurable]: "f \<in> borel_measurable M" 437 shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F (nn_cond_exp M G f) x" 438proof (rule nn_cond_exp_charact, auto) 439 interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)]) 440 fix A assume [measurable]: "A \<in> sets F" 441 then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def) 442 443 have "set_nn_integral M A (nn_cond_exp M G f) = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M G f x\<partial>M)" 444 by (metis (no_types) mult.commute) 445 also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (rule G.nn_cond_exp_intg, auto simp add: assms) 446 also have "... = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M F f x \<partial>M)" by (rule nn_cond_exp_intg[symmetric], auto simp add: assms) 447 also have "... = set_nn_integral M A (nn_cond_exp M F f)" by (metis (no_types) mult.commute) 448 finally show "set_nn_integral M A (nn_cond_exp M G f) = set_nn_integral M A (nn_cond_exp M F f)". 449qed 450 451end 452 453subsection \<open>Real conditional expectation\<close> 454 455text \<open>Once conditional expectations of positive functions are defined, the definition for real-valued functions 456follows readily, by taking the difference of positive and negative parts. 457One could also define a conditional expectation of vector-space valued functions, as in 458\verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I 459concentrate on it. (It is also essential for the case of the most general Pettis integral.) 460\<close> 461 462definition real_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where 463 "real_cond_exp M F f = 464 (\<lambda>x. enn2real(nn_cond_exp M F (\<lambda>x. ennreal (f x)) x) - enn2real(nn_cond_exp M F (\<lambda>x. ennreal (-f x)) x))" 465 466lemma 467 shows borel_measurable_cond_exp [measurable]: "real_cond_exp M F f \<in> borel_measurable F" 468 and borel_measurable_cond_exp2 [measurable]: "real_cond_exp M F f \<in> borel_measurable M" 469unfolding real_cond_exp_def by auto 470 471context sigma_finite_subalgebra 472begin 473 474lemma real_cond_exp_abs: 475 assumes [measurable]: "f \<in> borel_measurable M" 476 shows "AE x in M. abs(real_cond_exp M F f x) \<le> nn_cond_exp M F (\<lambda>x. ennreal (abs(f x))) x" 477proof - 478 define fp where "fp = (\<lambda>x. ennreal (f x))" 479 define fm where "fm = (\<lambda>x. ennreal (- f x))" 480 have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M" unfolding fp_def fm_def by auto 481 have eq: "\<And>x. ennreal \<bar>f x\<bar> = fp x + fm x" unfolding fp_def fm_def by (simp add: abs_real_def ennreal_neg) 482 483 { 484 fix x assume H: "nn_cond_exp M F fp x + nn_cond_exp M F fm x = nn_cond_exp M F (\<lambda>x. fp x + fm x) x" 485 have "\<bar>real_cond_exp M F f x\<bar> \<le> \<bar>enn2real(nn_cond_exp M F fp x)\<bar> + \<bar>enn2real(nn_cond_exp M F fm x)\<bar>" 486 unfolding real_cond_exp_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg) 487 from ennreal_leI[OF this] 488 have "abs(real_cond_exp M F f x) \<le> nn_cond_exp M F fp x + nn_cond_exp M F fm x" 489 by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique) 490 also have "... = nn_cond_exp M F (\<lambda>x. fp x + fm x) x" using H by simp 491 finally have "abs(real_cond_exp M F f x) \<le> nn_cond_exp M F (\<lambda>x. fp x + fm x) x" by simp 492 } 493 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 (\<lambda>x. fp x + fm x) x" 494 by (rule nn_cond_exp_sum) (auto simp add: fp_def fm_def) 495 ultimately have "AE x in M. abs(real_cond_exp M F f x) \<le> nn_cond_exp M F (\<lambda>x. fp x + fm x) x" 496 by auto 497 then show ?thesis using eq by simp 498qed 499 500text\<open>The next lemma shows that the conditional expectation 501is an $F$-measurable function whose average against an $F$-measurable 502function $f$ coincides with the average of the original function against $f$. 503It is obtained as a consequence of the same property for the positive conditional 504expectation, taking the difference of the positive and the negative part. The proof 505is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in 506the subsequent lemma. The idea of the proof is essentially trivial, but the implementation 507is slightly tedious as one should check all the integrability properties of the different parts, and go 508back and forth between positive integral and signed integrals, and between real-valued 509functions and ennreal-valued functions. 510 511Once this lemma is available, we will use it to characterize the conditional expectation, 512and never come back to the original technical definition, as we did in the case of the 513nonnegative conditional expectation. 514\<close> 515 516lemma real_cond_exp_intg_fpos: 517 assumes "integrable M (\<lambda>x. f x * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and 518 [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M" 519 shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)" 520 "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)" 521proof - 522 have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(3)]) 523 define gp where "gp = (\<lambda>x. ennreal (g x))" 524 define gm where "gm = (\<lambda>x. ennreal (- g x))" 525 have [measurable]: "gp \<in> borel_measurable M" "gm \<in> borel_measurable M" unfolding gp_def gm_def by auto 526 define h where "h = (\<lambda>x. ennreal(abs(g x)))" 527 have hgpgm: "\<And>x. h x = gp x + gm x" unfolding gp_def gm_def h_def by (simp add: abs_real_def ennreal_neg) 528 have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp 529 have pos[simp]: "\<And>x. h x \<ge> 0" "\<And>x. gp x \<ge> 0" "\<And>x. gm x \<ge> 0" unfolding h_def gp_def gm_def by simp_all 530 have gp_real: "\<And>x. enn2real(gp x) = max (g x) 0" 531 unfolding gp_def by (simp add: max_def ennreal_neg) 532 have gm_real: "\<And>x. enn2real(gm x) = max (-g x) 0" 533 unfolding gm_def by (simp add: max_def ennreal_neg) 534 535 have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)" 536 by (simp add: nn_integral_mono) 537 also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded) 538 finally have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) < \<infinity>" by simp 539 then have int1: "integrable M (\<lambda>x. f x * max (g x) 0)" by (simp add: integrableI_bounded) 540 541 have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)" 542 by (simp add: nn_integral_mono) 543 also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded) 544 finally have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) < \<infinity>" by simp 545 then have int2: "integrable M (\<lambda>x. f x * max (-g x) 0)" by (simp add: integrableI_bounded) 546 547 have "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) = (\<integral>\<^sup>+x. f x * h x \<partial>M)" 548 by (rule nn_cond_exp_intg) auto 549 also have "\<dots> = \<integral>\<^sup>+ x. ennreal (f x * max (g x) 0 + f x * max (- g x) 0) \<partial>M" 550 unfolding h_def 551 by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max) 552 also have "... < \<infinity>" 553 using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top) 554 finally have *: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) < \<infinity>" by simp 555 556 have "(\<integral>\<^sup>+x. norm(f x * real_cond_exp M F g x) \<partial>M) = (\<integral>\<^sup>+x. f x * abs(real_cond_exp M F g x) \<partial>M)" 557 by (simp add: abs_mult) 558 also have "... \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M)" 559 proof (rule nn_integral_mono_AE) 560 { 561 fix x assume *: "abs(real_cond_exp M F g x) \<le> nn_cond_exp M F h x" 562 have "ennreal (f x * \<bar>real_cond_exp M F g x\<bar>) = f x * ennreal(\<bar>real_cond_exp M F g x\<bar>)" 563 by (simp add: ennreal_mult) 564 also have "... \<le> f x * nn_cond_exp M F h x" 565 using * by (auto intro!: mult_left_mono) 566 finally have "ennreal (f x * \<bar>real_cond_exp M F g x\<bar>) \<le> f x * nn_cond_exp M F h x" 567 by simp 568 } 569 then show "AE x in M. ennreal (f x * \<bar>real_cond_exp M F g x\<bar>) \<le> f x * nn_cond_exp M F h x" 570 using real_cond_exp_abs[OF assms(4)] h_def by auto 571 qed 572 finally have **: "(\<integral>\<^sup>+x. norm(f x * real_cond_exp M F g x) \<partial>M) < \<infinity>" using * by auto 573 show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)" 574 using ** by (intro integrableI_bounded) auto 575 576 577 have "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gp x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M)" 578 proof (rule nn_integral_mono_AE) 579 have "AE x in M. nn_cond_exp M F gp x \<le> nn_cond_exp M F h x" 580 by (rule nn_cond_exp_mono) (auto simp add: hgpgm) 581 then show "AE x in M. f x * nn_cond_exp M F gp x \<le> f x * nn_cond_exp M F h x" 582 by (auto simp: mult_left_mono) 583 qed 584 then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gp x \<partial>M) < \<infinity>" 585 using * by auto 586 have "ennreal(norm(f x * enn2real(nn_cond_exp M F gp x))) \<le> f x * nn_cond_exp M F gp x" for x 587 by (auto simp add: ennreal_mult intro!: mult_left_mono) 588 (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff) 589 then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gp x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F gp x \<partial>M)" 590 by (simp add: nn_integral_mono) 591 then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gp x)) \<partial>M) < \<infinity>" using a by auto 592 then have gp_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gp x))" by (simp add: integrableI_bounded) 593 have gp_fin: "AE x in M. f x * nn_cond_exp M F gp x \<noteq> \<infinity>" 594 apply (rule nn_integral_PInf_AE) using a by auto 595 596 have "(\<integral> x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M)" 597 by (rule integral_eq_nn_integral) auto 598 also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)" 599 proof - 600 { 601 fix x assume "f x * nn_cond_exp M F gp x \<noteq> \<infinity>" 602 then have "ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x" 603 by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong) 604 } 605 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" 606 using gp_fin by auto 607 then have "(\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_cond_exp M F gp x \<partial>M)" 608 by (rule nn_integral_cong_AE) 609 also have "... = (\<integral>\<^sup>+ x. f x * gp x \<partial>M)" 610 by (rule nn_cond_exp_intg) (auto simp add: gp_def) 611 also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)" 612 by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def) 613 finally have "(\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)" by simp 614 then show ?thesis by simp 615 qed 616 also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M)" 617 by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def) 618 finally have gp_expr: "(\<integral> x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M) = (\<integral> x. f x * enn2real(gp x) \<partial>M)" by simp 619 620 621 have "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gm x \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M)" 622 proof (rule nn_integral_mono_AE) 623 have "AE x in M. nn_cond_exp M F gm x \<le> nn_cond_exp M F h x" 624 by (rule nn_cond_exp_mono) (auto simp add: hgpgm) 625 then show "AE x in M. f x * nn_cond_exp M F gm x \<le> f x * nn_cond_exp M F h x" 626 by (auto simp: mult_left_mono) 627 qed 628 then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gm x \<partial>M) < \<infinity>" 629 using * by auto 630 have "\<And>x. ennreal(norm(f x * enn2real(nn_cond_exp M F gm x))) \<le> f x * nn_cond_exp M F gm x" 631 by (auto simp add: ennreal_mult intro!: mult_left_mono) 632 (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff) 633 then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gm x)) \<partial>M) \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F gm x \<partial>M)" 634 by (simp add: nn_integral_mono) 635 then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gm x)) \<partial>M) < \<infinity>" using a by auto 636 then have gm_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gm x))" by (simp add: integrableI_bounded) 637 have gm_fin: "AE x in M. f x * nn_cond_exp M F gm x \<noteq> \<infinity>" 638 apply (rule nn_integral_PInf_AE) using a by auto 639 640 have "(\<integral> x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M) = enn2real (\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M)" 641 by (rule integral_eq_nn_integral) auto 642 also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)" 643 proof - 644 { 645 fix x assume "f x * nn_cond_exp M F gm x \<noteq> \<infinity>" 646 then have "ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x" 647 by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong) 648 } 649 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" 650 using gm_fin by auto 651 then have "(\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M) = (\<integral>\<^sup>+ x. f x * nn_cond_exp M F gm x \<partial>M)" 652 by (rule nn_integral_cong_AE) 653 also have "... = (\<integral>\<^sup>+ x. f x * gm x \<partial>M)" 654 by (rule nn_cond_exp_intg) (auto simp add: gm_def) 655 also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)" 656 by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def) 657 finally have "(\<integral>\<^sup>+ x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M) = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)" by simp 658 then show ?thesis by simp 659 qed 660 also have "... = (\<integral> x. f x * enn2real(gm x) \<partial>M)" 661 by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def) 662 finally have gm_expr: "(\<integral> x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M) = (\<integral> x. f x * enn2real(gm x) \<partial>M)" by simp 663 664 665 have "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * enn2real(nn_cond_exp M F gp x) - f x * enn2real(nn_cond_exp M F gm x) \<partial>M)" 666 unfolding real_cond_exp_def gp_def gm_def by (simp add: right_diff_distrib) 667 also have "... = (\<integral> x. f x * enn2real(nn_cond_exp M F gp x) \<partial>M) - (\<integral> x. f x * enn2real(nn_cond_exp M F gm x) \<partial>M)" 668 by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int) 669 also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M) - (\<integral> x. f x * enn2real(gm x) \<partial>M)" 670 using gp_expr gm_expr by simp 671 also have "... = (\<integral> x. f x * max (g x) 0 \<partial>M) - (\<integral> x. f x * max (-g x) 0 \<partial>M)" 672 using gp_real gm_real by simp 673 also have "... = (\<integral> x. f x * max (g x) 0 - f x * max (-g x) 0 \<partial>M)" 674 by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2) 675 also have "... = (\<integral>x. f x * g x \<partial>M)" 676 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) 677 finally show "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral>x. f x * g x \<partial>M)" 678 by simp 679qed 680 681lemma real_cond_exp_intg: 682 assumes "integrable M (\<lambda>x. f x * g x)" and 683 [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M" 684 shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)" 685 "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)" 686proof - 687 have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(2)]) 688 define fp where "fp = (\<lambda>x. max (f x) 0)" 689 define fm where "fm = (\<lambda>x. max (-f x) 0)" 690 have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M" 691 unfolding fp_def fm_def by simp_all 692 have [measurable]: "fp \<in> borel_measurable F" "fm \<in> borel_measurable F" 693 unfolding fp_def fm_def by simp_all 694 695 have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)" 696 by (simp add: fp_def nn_integral_mono) 697 also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded) 698 finally have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) < \<infinity>" by simp 699 then have intp: "integrable M (\<lambda>x. fp x * g x)" by (simp add: integrableI_bounded) 700 moreover have "\<And>x. fp x \<ge> 0" unfolding fp_def by simp 701 ultimately have Rp: "integrable M (\<lambda>x. fp x * real_cond_exp M F g x)" 702 "(\<integral> x. fp x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fp x * g x \<partial>M)" 703 using real_cond_exp_intg_fpos by auto 704 705 have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)" 706 by (simp add: fm_def nn_integral_mono) 707 also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded) 708 finally have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) < \<infinity>" by simp 709 then have intm: "integrable M (\<lambda>x. fm x * g x)" by (simp add: integrableI_bounded) 710 moreover have "\<And>x. fm x \<ge> 0" unfolding fm_def by simp 711 ultimately have Rm: "integrable M (\<lambda>x. fm x * real_cond_exp M F g x)" 712 "(\<integral> x. fm x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fm x * g x \<partial>M)" 713 using real_cond_exp_intg_fpos by auto 714 715 have "integrable M (\<lambda>x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x)" 716 using Rp(1) Rm(1) integrable_diff by simp 717 moreover have *: "\<And>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" 718 unfolding fp_def fm_def by (simp add: max_def) 719 ultimately show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)" 720 by simp 721 722 have "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x \<partial>M)" 723 using * by simp 724 also have "... = (\<integral> x. fp x * real_cond_exp M F g x \<partial>M) - (\<integral> x. fm x * real_cond_exp M F g x \<partial>M)" 725 using Rp(1) Rm(1) by simp 726 also have "... = (\<integral> x. fp x * g x \<partial>M) - (\<integral> x. fm x * g x \<partial>M)" 727 using Rp(2) Rm(2) by simp 728 also have "... = (\<integral> x. fp x * g x - fm x * g x \<partial>M)" 729 using intm intp by simp 730 also have "... = (\<integral> x. f x * g x \<partial>M)" 731 unfolding fp_def fm_def by (metis (no_types, hide_lams) diff_0 diff_zero max.commute 732 max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib) 733 finally show "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)" by simp 734qed 735 736lemma real_cond_exp_intA: 737 assumes [measurable]: "integrable M f" "A \<in> sets F" 738 shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" 739proof - 740 have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD) 741 have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto 742 then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] 743 unfolding set_lebesgue_integral_def by auto 744qed 745 746lemma real_cond_exp_int [intro]: 747 assumes "integrable M f" 748 shows "integrable M (real_cond_exp M F f)" "(\<integral>x. real_cond_exp M F f x \<partial>M) = (\<integral>x. f x \<partial>M)" 749using real_cond_exp_intg[where ?f = "\<lambda>x. 1" and ?g = f] assms by auto 750 751lemma real_cond_exp_charact: 752 assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)" 753 and [measurable]: "integrable M f" "integrable M g" 754 "g \<in> borel_measurable F" 755 shows "AE x in M. real_cond_exp M F f x = g x" 756proof - 757 let ?MF = "restr_to_subalg M F" 758 have "AE x in ?MF. real_cond_exp M F f x = g x" 759 proof (rule AE_symmetric[OF density_unique_real]) 760 fix A assume "A \<in> sets ?MF" 761 then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp 762 then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD) 763 have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)" 764 unfolding set_lebesgue_integral_def by (simp add: integral_subalgebra2 subalg) 765 also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp 766 also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def) 767 also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)" 768 apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms) 769 also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute set_lebesgue_integral_def) 770 also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)" 771 by (simp add: integral_subalgebra2 subalg set_lebesgue_integral_def) 772 finally show "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)" by simp 773 next 774 have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)]) 775 then show "integrable ?MF (real_cond_exp M F f)" by (metis borel_measurable_cond_exp integrable_in_subalg[OF subalg]) 776 show "integrable (restr_to_subalg M F) g" by (simp add: assms(3) integrable_in_subalg[OF subalg]) 777 qed 778 then show ?thesis using AE_restr_to_subalg[OF subalg] by auto 779qed 780 781lemma real_cond_exp_F_meas [intro, simp]: 782 assumes "integrable M f" 783 "f \<in> borel_measurable F" 784 shows "AE x in M. real_cond_exp M F f x = f x" 785by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg]) 786 787lemma real_cond_exp_mult: 788 assumes [measurable]:"f \<in> borel_measurable F" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f x * g x)" 789 shows "AE x in M. real_cond_exp M F (\<lambda>x. f x * g x) x = f x * real_cond_exp M F g x" 790proof (rule real_cond_exp_charact) 791 fix A assume "A \<in> sets F" 792 then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable 793 have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD) 794 have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M" 795 by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def) 796 also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M" 797 apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms) 798 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute) 799 also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" 800 by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def) 801 finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp 802qed (auto simp add: real_cond_exp_intg(1) assms) 803 804lemma real_cond_exp_add [intro]: 805 assumes [measurable]: "integrable M f" "integrable M g" 806 shows "AE x in M. real_cond_exp M F (\<lambda>x. f x + g x) x = real_cond_exp M F f x + real_cond_exp M F g x" 807proof (rule real_cond_exp_charact) 808 have "integrable M (real_cond_exp M F f)" "integrable M (real_cond_exp M F g)" 809 using real_cond_exp_int(1) assms by auto 810 then show "integrable M (\<lambda>x. real_cond_exp M F f x + real_cond_exp M F g x)" 811 by auto 812 813 fix A assume [measurable]: "A \<in> sets F" 814 then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD) 815 have intAf: "integrable M (\<lambda>x. indicator A x * f x)" 816 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto 817 have intAg: "integrable M (\<lambda>x. indicator A x * g x)" 818 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto 819 820 have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)" 821 apply (rule set_integral_add, auto simp add: assms set_integrable_def) 822 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]] 823 integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all 824 also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)" 825 unfolding set_lebesgue_integral_def by auto 826 also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)" 827 using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto 828 also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)" 829 unfolding set_lebesgue_integral_def by auto 830 also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M" 831 by (rule set_integral_add(2)[symmetric]) (auto simp add: assms set_integrable_def \<open>A \<in> sets M\<close> intAf intAg) 832 finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M" 833 by simp 834qed (auto simp add: assms) 835 836lemma real_cond_exp_cong: 837 assumes ae: "AE x in M. f x = g x" and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M" 838 shows "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" 839proof - 840 have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal (f x)) x = nn_cond_exp M F (\<lambda>x. ennreal (g x)) x" 841 apply (rule nn_cond_exp_cong) using assms by auto 842 moreover have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal (-f x)) x = nn_cond_exp M F (\<lambda>x. ennreal(-g x)) x" 843 apply (rule nn_cond_exp_cong) using assms by auto 844 ultimately show "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x" 845 unfolding real_cond_exp_def by auto 846qed 847 848lemma real_cond_exp_cmult [intro, simp]: 849 fixes c::real 850 assumes "integrable M f" 851 shows "AE x in M. real_cond_exp M F (\<lambda>x. c * f x) x = c * real_cond_exp M F f x" 852by (rule real_cond_exp_mult[where ?f = "\<lambda>x. c" and ?g = f], auto simp add: assms borel_measurable_integrable) 853 854lemma real_cond_exp_cdiv [intro, simp]: 855 fixes c::real 856 assumes "integrable M f" 857 shows "AE x in M. real_cond_exp M F (\<lambda>x. f x / c) x = real_cond_exp M F f x / c" 858using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: field_split_simps) 859 860lemma real_cond_exp_diff [intro, simp]: 861 assumes [measurable]: "integrable M f" "integrable M g" 862 shows "AE x in M. real_cond_exp M F (\<lambda>x. f x - g x) x = real_cond_exp M F f x - real_cond_exp M F g x" 863proof - 864 have "AE x in M. real_cond_exp M F (\<lambda>x. f x + (- g x)) x = real_cond_exp M F f x + real_cond_exp M F (\<lambda>x. -g x) x" 865 using real_cond_exp_add[where ?f = f and ?g = "\<lambda>x. - g x"] assms by auto 866 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -g x) x = - real_cond_exp M F g x" 867 using real_cond_exp_cmult[where ?f = g and ?c = "-1"] assms(2) by auto 868 ultimately show ?thesis by auto 869qed 870 871lemma real_cond_exp_pos [intro]: 872 assumes "AE x in M. f x \<ge> 0" and [measurable]: "f \<in> borel_measurable M" 873 shows "AE x in M. real_cond_exp M F f x \<ge> 0" 874proof - 875 define g where "g = (\<lambda>x. max (f x) 0)" 876 have "AE x in M. f x = g x" using assms g_def by auto 877 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 878 879 have "\<And>x. g x \<ge> 0" unfolding g_def by simp 880 then have "(\<lambda>x. ennreal(-g x)) = (\<lambda>x. 0)" 881 by (simp add: ennreal_neg) 882 moreover have "AE x in M. 0 = nn_cond_exp M F (\<lambda>x. 0) x" 883 by (rule nn_cond_exp_F_meas, auto) 884 ultimately have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal(-g x)) x = 0" 885 by simp 886 then have "AE x in M. real_cond_exp M F g x = enn2real(nn_cond_exp M F (\<lambda>x. ennreal (g x)) x)" 887 unfolding real_cond_exp_def by auto 888 then have "AE x in M. real_cond_exp M F g x \<ge> 0" by auto 889 then show ?thesis using * by auto 890qed 891 892lemma real_cond_exp_mono: 893 assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g" 894 shows "AE x in M. real_cond_exp M F f x \<le> real_cond_exp M F g x" 895proof - 896 have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (\<lambda>x. g x - f x) x" 897 by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms) 898 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x \<ge> 0" 899 by (rule real_cond_exp_pos, auto simp add: assms(1)) 900 ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x \<ge> 0" by auto 901 then show ?thesis by auto 902qed 903 904lemma (in -) measurable_P_restriction [measurable (raw)]: 905 assumes [measurable]: "Measurable.pred M P" "A \<in> sets M" 906 shows "{x \<in> A. P x} \<in> sets M" 907proof - 908 have "A \<subseteq> space M" using sets.sets_into_space[OF assms(2)]. 909 then have "{x \<in> A. P x} = A \<inter> {x \<in> space M. P x}" by blast 910 then show ?thesis by auto 911qed 912 913lemma real_cond_exp_gr_c: 914 assumes [measurable]: "integrable M f" 915 and AE: "AE x in M. f x > c" 916 shows "AE x in M. real_cond_exp M F f x > c" 917proof - 918 define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}" 919 have [measurable]: "X \<in> sets F" 920 unfolding X_def apply measurable by (metis sets.top subalg subalgebra_def) 921 then have [measurable]: "X \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast 922 have "emeasure M X = 0" 923 proof (rule ccontr) 924 assume "\<not>(emeasure M X) = 0" 925 have "emeasure (restr_to_subalg M F) X = emeasure M X" 926 by (simp add: emeasure_restr_to_subalg subalg) 927 then have "emeasure (restr_to_subalg M F) X > 0" 928 using \<open>\<not>(emeasure M X) = 0\<close> gr_zeroI by auto 929 then obtain A where "A \<in> sets (restr_to_subalg M F)" "A \<subseteq> X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < \<infinity>" 930 using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans 931 not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite) 932 then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast 933 then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast 934 have Ic: "set_integrable M A (\<lambda>x. c)" 935 unfolding set_integrable_def 936 using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce 937 have If: "set_integrable M A f" 938 unfolding set_integrable_def 939 by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>) 940 have "AE x in M. indicator A x * c = indicator A x * f x" 941 proof (rule integral_ineq_eq_0_then_AE) 942 have "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)" 943 proof (rule antisym) 944 show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)" 945 apply (rule set_integral_mono_AE) using Ic If assms(2) by auto 946 have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)" 947 by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>) 948 also have "... \<le> (\<integral>x\<in>A. c \<partial>M)" 949 apply (rule set_integral_mono) 950 unfolding set_integrable_def 951 apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>]) 952 using Ic X_def \<open>A \<subseteq> X\<close> by (auto simp: set_integrable_def) 953 finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp 954 qed 955 then have "measure M A * c = LINT x|M. indicat_real A x * f x" 956 by (auto simp: set_lebesgue_integral_def) 957 then show "LINT x|M. indicat_real A x * c = LINT x|M. indicat_real A x * f x" 958 by auto 959 show "AE x in M. indicat_real A x * c \<le> indicat_real A x * f x" 960 using AE unfolding indicator_def by auto 961 qed (use Ic If in \<open>auto simp: set_integrable_def\<close>) 962 then have "AE x\<in>A in M. c = f x" by auto 963 then have "AE x\<in>A in M. False" using assms(2) by auto 964 have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>) 965 then show False using \<open>emeasure (restr_to_subalg M F) A > 0\<close> 966 by (simp add: emeasure_restr_to_subalg null_setsD1 subalg) 967 qed 968 then show ?thesis using AE_iff_null_sets[OF \<open>X \<in> sets M\<close>] unfolding X_def by auto 969qed 970 971lemma real_cond_exp_less_c: 972 assumes [measurable]: "integrable M f" 973 and "AE x in M. f x < c" 974 shows "AE x in M. real_cond_exp M F f x < c" 975proof - 976 have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x" 977 using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto 978 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x > -c" 979 apply (rule real_cond_exp_gr_c) using assms by auto 980 ultimately show ?thesis by auto 981qed 982 983lemma real_cond_exp_ge_c: 984 assumes [measurable]: "integrable M f" 985 and "AE x in M. f x \<ge> c" 986 shows "AE x in M. real_cond_exp M F f x \<ge> c" 987proof - 988 obtain u::"nat \<Rightarrow> real" where u: "\<And>n. u n < c" "u \<longlonglongrightarrow> c" 989 using approx_from_below_dense_linorder[of "c-1" c] by auto 990 have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat 991 apply (rule real_cond_exp_gr_c) using assms \<open>u n < c\<close> by auto 992 have "AE x in M. \<forall>n. real_cond_exp M F f x > u n" 993 by (subst AE_all_countable, auto simp add: *) 994 moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x 995 proof - 996 have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto 997 then show ?thesis using u(2) LIMSEQ_le_const2 by metis 998 qed 999 ultimately show ?thesis by auto 1000qed 1001 1002lemma real_cond_exp_le_c: 1003 assumes [measurable]: "integrable M f" 1004 and "AE x in M. f x \<le> c" 1005 shows "AE x in M. real_cond_exp M F f x \<le> c" 1006proof - 1007 have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x" 1008 using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto 1009 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x \<ge> -c" 1010 apply (rule real_cond_exp_ge_c) using assms by auto 1011 ultimately show ?thesis by auto 1012qed 1013 1014lemma real_cond_exp_mono_strict: 1015 assumes "AE x in M. f x < g x" and [measurable]: "integrable M f" "integrable M g" 1016 shows "AE x in M. real_cond_exp M F f x < real_cond_exp M F g x" 1017proof - 1018 have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x = real_cond_exp M F (\<lambda>x. g x - f x) x" 1019 by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms) 1020 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x > 0" 1021 by (rule real_cond_exp_gr_c, auto simp add: assms) 1022 ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x > 0" by auto 1023 then show ?thesis by auto 1024qed 1025 1026lemma real_cond_exp_nested_subalg [intro, simp]: 1027 assumes "subalgebra M G" "subalgebra G F" 1028 and [measurable]: "integrable M f" 1029 shows "AE x in M. real_cond_exp M F (real_cond_exp M G f) x = real_cond_exp M F f x" 1030proof (rule real_cond_exp_charact) 1031 interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)]) 1032 show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1)) 1033 1034 fix A assume [measurable]: "A \<in> sets F" 1035 then have [measurable]: "A \<in> sets G" using assms(2) by (meson subsetD subalgebra_def) 1036 have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f" 1037 by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3)) 1038 also have "... = set_lebesgue_integral M A (real_cond_exp M F f)" 1039 by (rule real_cond_exp_intA, auto simp add: assms(3)) 1040 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 1041qed (auto simp add: assms real_cond_exp_int(1)) 1042 1043lemma real_cond_exp_sum [intro, simp]: 1044 fixes f::"'b \<Rightarrow> 'a \<Rightarrow> real" 1045 assumes [measurable]: "\<And>i. integrable M (f i)" 1046 shows "AE x in M. real_cond_exp M F (\<lambda>x. \<Sum>i\<in>I. f i x) x = (\<Sum>i\<in>I. real_cond_exp M F (f i) x)" 1047proof (rule real_cond_exp_charact) 1048 fix A assume [measurable]: "A \<in> sets F" 1049 then have A_meas [measurable]: "A \<in> sets M" by (meson subsetD subalg subalgebra_def) 1050 have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i 1051 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto 1052 have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i 1053 using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]] by auto 1054 have inti: "(\<integral>x. indicator A x * f i x \<partial>M) = (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M)" for i 1055 by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *) 1056 1057 have "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x. (\<Sum>i\<in>I. indicator A x * f i x)\<partial>M)" 1058 by (simp add: sum_distrib_left set_lebesgue_integral_def) 1059 also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))" 1060 by (rule Bochner_Integration.integral_sum, simp add: *) 1061 also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))" 1062 using inti by auto 1063 also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)" 1064 by (rule Bochner_Integration.integral_sum[symmetric], simp add: **) 1065 also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" 1066 by (simp add: sum_distrib_left set_lebesgue_integral_def) 1067 finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto 1068qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)]) 1069 1070text \<open>Jensen's inequality, describing the behavior of the integral under a convex function, admits 1071a version for the conditional expectation, as follows.\<close> 1072 1073theorem real_cond_exp_jensens_inequality: 1074 fixes q :: "real \<Rightarrow> real" 1075 assumes X: "integrable M X" "AE x in M. X x \<in> I" 1076 assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" 1077 assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel" 1078 shows "AE x in M. real_cond_exp M F X x \<in> I" 1079 "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x" 1080proof - 1081 have "open I" using I by auto 1082 then have "interior I = I" by (simp add: interior_eq) 1083 have [measurable]: "I \<in> sets borel" using I by auto 1084 define phi where "phi = (\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I)))" 1085 have **: "q (X x) \<ge> 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)" 1086 if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x 1087 unfolding phi_def apply (rule convex_le_Inf_differential) 1088 using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto 1089 text \<open>It is not clear that the function $\phi$ is measurable. We replace it by a version which 1090 is better behaved.\<close> 1091 define psi where "psi = (\<lambda>x. phi x * indicator I x)" 1092 have A: "psi y = phi y" if "y \<in> I" for y unfolding psi_def indicator_def using that by auto 1093 have *: "q (X x) \<ge> 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)" 1094 if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x 1095 unfolding A[OF \<open>real_cond_exp M F X x \<in> I\<close>] using ** that by auto 1096 1097 note I 1098 moreover have "AE x in M. real_cond_exp M F X x > a" if "I \<subseteq> {a <..}" for a 1099 apply (rule real_cond_exp_gr_c) using X that by auto 1100 moreover have "AE x in M. real_cond_exp M F X x < b" if "I \<subseteq> {..<b}" for b 1101 apply (rule real_cond_exp_less_c) using X that by auto 1102 ultimately show "AE x in M. real_cond_exp M F X x \<in> I" 1103 by (elim disjE) (auto simp: subset_eq) 1104 then have main_ineq: "AE x in M. q (X x) \<ge> 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)" 1105 using * X(2) by auto 1106 1107 text \<open>Then, one wants to take the conditional expectation of this inequality. On the left, one gets 1108 the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one 1109 is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only 1110 works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The 1111 trick is to multiply by a $F$-measurable function which is small enough to make 1112 everything integrable.\<close> 1113 1114 obtain f::"'a \<Rightarrow> real" where [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)" 1115 "integrable (restr_to_subalg M F) f" 1116 and f: "\<And>x. f x > 0" "\<And>x. f x \<le> 1" 1117 using sigma_finite_measure.obtain_positive_integrable_function[OF sigma_fin_subalg] by metis 1118 then have [measurable]: "f \<in> borel_measurable F" by (simp add: subalg) 1119 then have [measurable]: "f \<in> borel_measurable M" using measurable_from_subalg[OF subalg] by blast 1120 define g where "g = (\<lambda>x. f x/(1+ \<bar>psi (real_cond_exp M F X x)\<bar> + \<bar>q (real_cond_exp M F X x)\<bar>))" 1121 define G where "G = (\<lambda>x. g x * psi (real_cond_exp M F X x))" 1122 have g: "g x > 0" "g x \<le> 1" for x unfolding G_def g_def using f[of x] by (auto simp add: abs_mult) 1123 have G: "\<bar>G x\<bar> \<le> 1" for x unfolding G_def g_def using f[of x] 1124 proof (auto simp add: abs_mult) 1125 have "f x * \<bar>psi (real_cond_exp M F X x)\<bar> \<le> 1 * \<bar>psi (real_cond_exp M F X x)\<bar>" 1126 apply (rule mult_mono) using f[of x] by auto 1127 also have "... \<le> 1 + \<bar>psi (real_cond_exp M F X x)\<bar> + \<bar>q (real_cond_exp M F X x)\<bar>" by auto 1128 finally show "f x * \<bar>psi (real_cond_exp M F X x)\<bar> \<le> 1 + \<bar>psi (real_cond_exp M F X x)\<bar> + \<bar>q (real_cond_exp M F X x)\<bar>" 1129 by simp 1130 qed 1131 have "AE x in M. g x * q (X x) \<ge> 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))" 1132 using main_ineq g by (auto simp add: divide_simps) 1133 then have main_G: "AE x in M. g x * q (X x) \<ge> g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)" 1134 unfolding G_def by (auto simp add: algebra_simps) 1135 1136 text \<open>To proceed, we need to know that $\psi$ is measurable.\<close> 1137 have phi_mono: "phi x \<le> phi y" if "x \<le> y" "x \<in> I" "y \<in> I" for x y 1138 proof (cases "x < y") 1139 case True 1140 have "q x + phi x * (y-x) \<le> q y" 1141 unfolding phi_def apply (rule convex_le_Inf_differential) using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto 1142 then have "phi x \<le> (q x - q y) / (x - y)" 1143 using that \<open>x < y\<close> by (auto simp add: field_split_simps algebra_simps) 1144 moreover have "(q x - q y)/(x - y) \<le> phi y" 1145 unfolding phi_def proof (rule cInf_greatest, auto) 1146 fix t assume "t \<in> I" "y < t" 1147 have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)" 1148 apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto 1149 also have "... \<le> (q y - q t) / (y - t)" 1150 apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto 1151 finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp 1152 next 1153 obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> openE by blast 1154 then have "y + e/2 \<in> {y<..} \<inter> I" by (auto simp: dist_real_def) 1155 then show "{y<..} \<inter> I = {} \<Longrightarrow> False" by auto 1156 qed 1157 ultimately show "phi x \<le> phi y" by auto 1158 next 1159 case False 1160 then have "x = y" using \<open>x \<le> y\<close> by auto 1161 then show ?thesis by auto 1162 qed 1163 have [measurable]: "psi \<in> borel_measurable borel" 1164 by (rule borel_measurable_piecewise_mono[of "{I, -I}"]) 1165 (auto simp add: psi_def indicator_def phi_mono intro: mono_onI) 1166 have [measurable]: "q \<in> borel_measurable borel" using q by simp 1167 1168 have [measurable]: "X \<in> borel_measurable M" 1169 "real_cond_exp M F X \<in> borel_measurable F" 1170 "g \<in> borel_measurable F" "g \<in> borel_measurable M" 1171 "G \<in> borel_measurable F" "G \<in> borel_measurable M" 1172 using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto 1173 have int1: "integrable (restr_to_subalg M F) (\<lambda>x. g x * q (real_cond_exp M F X x))" 1174 apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg \<open>integrable (restr_to_subalg M F) f\<close>) 1175 unfolding g_def by (auto simp add: field_split_simps abs_mult algebra_simps) 1176 have int2: "integrable M (\<lambda>x. G x * (X x - real_cond_exp M F X x))" 1177 apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>X x\<bar> + \<bar>real_cond_exp M F X x\<bar>"]) 1178 apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int \<open>integrable M X\<close> AE_I2) 1179 using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le) 1180 have int3: "integrable M (\<lambda>x. g x * q (X x))" 1181 apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. q(X x)"], auto simp add: q(1) abs_mult) 1182 using g by (simp add: less_imp_le mult_left_le_one_le) 1183 1184 text \<open>Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get 1185 the following.\<close> 1186 have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x \<ge> real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x" 1187 apply (rule real_cond_exp_mono[OF main_G]) 1188 apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]]) 1189 using int2 int3 by auto 1190 text \<open>This reduces to the desired inequality thanks to the properties of conditional expectation, 1191 i.e., the conditional expectation of an $F$-measurable function is this function, and one can 1192 multiply an $F$-measurable function outside of conditional expectations. 1193 Since all these equalities only hold almost everywhere, we formulate them separately, 1194 and then combine all of them to simplify the above equation, again almost everywhere.\<close> 1195 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x = g x * real_cond_exp M F (\<lambda>x. q (X x)) x" 1196 by (rule real_cond_exp_mult, auto simp add: int3) 1197 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x 1198 = real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x)) x + real_cond_exp M F (\<lambda>x. G x * (X x - real_cond_exp M F X x)) x" 1199 by (rule real_cond_exp_add, auto simp add: integrable_from_subalg[OF subalg int1] int2) 1200 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x)) x = g x * q (real_cond_exp M F X x)" 1201 by (rule real_cond_exp_F_meas, auto simp add: integrable_from_subalg[OF subalg int1]) 1202 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. G x * (X x - real_cond_exp M F X x)) x = G x * real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x" 1203 by (rule real_cond_exp_mult, auto simp add: int2) 1204 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x = real_cond_exp M F X x - real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x" 1205 by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int \<open>integrable M X\<close>) 1206 moreover have "AE x in M. real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x = real_cond_exp M F X x " 1207 by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int \<open>integrable M X\<close>) 1208 ultimately have "AE x in M. g x * real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> g x * q (real_cond_exp M F X x)" 1209 by auto 1210 then show "AE x in M. real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> q (real_cond_exp M F X x)" 1211 using g(1) by (auto simp add: field_split_simps) 1212qed 1213 1214text \<open>Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper 1215bound for it. Indeed, this is not true in general, as the following counterexample shows: 1216 1217on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$ 1218for integer $n$. Let $q(x) = - \sqrt{x}$ for $x\geq 0$. Define $X$ which is equal to $1/n$ over 1219$[n, n+1/n)$ and $2^{-n}$ on $[n+1/n, n+1)$. Then $X$ is integrable as $\sum 1/n^2 < \infty$, and 1220$q(X)$ is integrable as $\sum 1/n^{3/2} < \infty$. On the other hand, $E(X|F)$ is essentially equal 1221to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take 1222its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not 1223integrable. 1224 1225However, this counterexample is essentially the only situation where this function is not 1226integrable, as shown by the next lemma. 1227\<close> 1228 1229lemma integrable_convex_cond_exp: 1230 fixes q :: "real \<Rightarrow> real" 1231 assumes X: "integrable M X" "AE x in M. X x \<in> I" 1232 assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV" 1233 assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel" 1234 assumes H: "emeasure M (space M) = \<infinity> \<Longrightarrow> 0 \<in> I" 1235 shows "integrable M (\<lambda>x. q (real_cond_exp M F X x))" 1236proof - 1237 have [measurable]: "(\<lambda>x. q (real_cond_exp M F X x)) \<in> borel_measurable M" 1238 "q \<in> borel_measurable borel" 1239 "X \<in> borel_measurable M" 1240 using X(1) q(3) by auto 1241 have "open I" using I by auto 1242 then have "interior I = I" by (simp add: interior_eq) 1243 1244 consider "emeasure M (space M) = 0" | "emeasure M (space M) > 0 \<and> emeasure M (space M) < \<infinity>" | "emeasure M (space M) = \<infinity>" 1245 by (metis infinity_ennreal_def not_gr_zero top.not_eq_extremum) 1246 then show ?thesis 1247 proof (cases) 1248 case 1 1249 show ?thesis by (subst integrable_cong_AE[of _ _ "\<lambda>x. 0"], auto intro: emeasure_0_AE[OF 1]) 1250 next 1251 case 2 1252 interpret finite_measure M using 2 by (auto intro!: finite_measureI) 1253 1254 have "I \<noteq> {}" 1255 using \<open>AE x in M. X x \<in> I\<close> 2 eventually_mono integral_less_AE_space by fastforce 1256 then obtain z where "z \<in> I" by auto 1257 1258 define A where "A = Inf ((\<lambda>t. (q z - q t) / (z - t)) ` ({z<..} \<inter> I))" 1259 have "q y \<ge> q z + A * (y - z)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential) 1260 using \<open>z \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto 1261 then have "AE x in M. q (real_cond_exp M F X x) \<ge> q z + A * (real_cond_exp M F X x - z)" 1262 using real_cond_exp_jensens_inequality(1)[OF X I q] by auto 1263 moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x" 1264 using real_cond_exp_jensens_inequality(2)[OF X I q] by auto 1265 moreover have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>c\<bar>" if "b \<le> a \<and> a \<le> c" for a b c::real 1266 using that by auto 1267 ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar> 1268 \<le> \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>q z + A * (real_cond_exp M F X x - z)\<bar>" 1269 by auto 1270 1271 show "integrable M (\<lambda>x. q (real_cond_exp M F X x))" 1272 apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>q z + A * (real_cond_exp M F X x - z)\<bar>"]) 1273 apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1)) 1274 using X(1) q(1) * by auto 1275 next 1276 case 3 1277 then have "0 \<in> I" using H finite_measure.finite_emeasure_space by auto 1278 have "q(0) = 0" 1279 proof (rule ccontr) 1280 assume *: "\<not>(q(0) = 0)" 1281 define e where "e = \<bar>q(0)\<bar> / 2" 1282 then have "e > 0" using * by auto 1283 have "continuous (at 0) q" 1284 using q(2) \<open>0 \<in> I\<close> \<open>open I\<close> \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast 1285 then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using \<open>e > 0\<close> 1286 by (metis continuous_at_real_range real_norm_def) 1287 then have *: "\<bar>q(y)\<bar> > e" if "\<bar>y\<bar> < d" for y 1288 proof - 1289 have "\<bar>q 0\<bar> \<le> \<bar>q 0 - q y\<bar> + \<bar>q y\<bar>" by auto 1290 also have "... < e + \<bar>q y\<bar>" using d(2) that by force 1291 finally have "\<bar>q y\<bar> > \<bar>q 0\<bar> - e" by auto 1292 then show ?thesis unfolding e_def by simp 1293 qed 1294 have "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} \<le> emeasure M ({x \<in> space M. 1 \<le> ennreal(1/e) * \<bar>q(X x)\<bar>} \<inter> space M)" 1295 by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> less_imp_le ennreal_mult''[symmetric]) 1296 also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)" 1297 by (rule nn_integral_Markov_inequality, auto) 1298 also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto 1299 also have "... = (1/e) * ennreal(\<integral>x. \<bar>q(X x)\<bar> \<partial>M)" 1300 using nn_integral_eq_integral[OF integrable_abs[OF q(1)]] by auto 1301 also have "... < \<infinity>" 1302 by (simp add: ennreal_mult_less_top) 1303 finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp 1304 1305 have "{x \<in> space M. \<bar>X x\<bar> \<ge> d} = {x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M" 1306 by (auto simp add: \<open>d>0\<close> ennreal_mult''[symmetric]) 1307 then have "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} = emeasure M ({x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M)" 1308 by auto 1309 also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)" 1310 by (rule nn_integral_Markov_inequality, auto) 1311 also have "... = (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) \<partial>M)" by auto 1312 also have "... = (1/d) * ennreal(\<integral>x. \<bar>X x\<bar> \<partial>M)" 1313 using nn_integral_eq_integral[OF integrable_abs[OF X(1)]] by auto 1314 also have "... < \<infinity>" 1315 by (simp add: ennreal_mult_less_top) 1316 finally have B: "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} < \<infinity>" by simp 1317 1318 have "space M = {x \<in> space M. \<bar>X x\<bar> < d} \<union> {x \<in> space M. \<bar>X x\<bar> \<ge> d}" by auto 1319 then have "emeasure M (space M) = emeasure M ({x \<in> space M. \<bar>X x\<bar> < d} \<union> {x \<in> space M. \<bar>X x\<bar> \<ge> d})" 1320 by simp 1321 also have "... \<le> emeasure M {x \<in> space M. \<bar>X x\<bar> < d} + emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d}" 1322 by (auto intro!: emeasure_subadditive) 1323 also have "... < \<infinity>" using A B by auto 1324 finally show False using \<open>emeasure M (space M) = \<infinity>\<close> by auto 1325 qed 1326 1327 define A where "A = Inf ((\<lambda>t. (q 0 - q t) / (0 - t)) ` ({0<..} \<inter> I))" 1328 have "q y \<ge> q 0 + A * (y - 0)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential) 1329 using \<open>0 \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto 1330 then have "q y \<ge> A * y" if "y \<in> I" for y using \<open>q 0 = 0\<close> that by auto 1331 then have "AE x in M. q (real_cond_exp M F X x) \<ge> A * real_cond_exp M F X x" 1332 using real_cond_exp_jensens_inequality(1)[OF X I q] by auto 1333 moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x" 1334 using real_cond_exp_jensens_inequality(2)[OF X I q] by auto 1335 moreover have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>c\<bar>" if "b \<le> a \<and> a \<le> c" for a b c::real 1336 using that by auto 1337 ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar> 1338 \<le> \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>A * real_cond_exp M F X x\<bar>" 1339 by auto 1340 1341 show "integrable M (\<lambda>x. q (real_cond_exp M F X x))" 1342 apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>A * real_cond_exp M F X x \<bar>"]) 1343 apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1)) 1344 using X(1) q(1) * by auto 1345 qed 1346qed 1347 1348end 1349 1350end 1351