src/HOL/Probability/Conditional_Expectation.thy
 author paulson Thu Apr 11 15:26:04 2019 +0100 (6 months ago) changeset 70125 b601c2c87076 parent 69712 dc85b5b3a532 child 70817 dd675800469d permissions -rw-r--r--
type instantiations for poly_mapping as a real_normed_vector
1 (*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
3 *)
5 section \<open>Conditional Expectation\<close>
7 theory Conditional_Expectation
8 imports Probability_Measure
9 begin
11 subsection \<open>Restricting a measure to a sub-sigma-algebra\<close>
13 definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
14   "subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))"
16 lemma sub_measure_space:
17   assumes i: "subalgebra M F"
18   shows "measure_space (space M) (sets F) (emeasure M)"
19 proof -
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
27 qed
29 definition 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)"
32 lemma space_restr_to_subalg:
33   "space (restr_to_subalg M F) = space M"
34 unfolding restr_to_subalg_def by (simp add: space_measure_of_conv)
36 lemma sets_restr_to_subalg [measurable_cong]:
37   assumes "subalgebra M F"
38   shows "sets (restr_to_subalg M F) = sets F"
39 unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def)
41 lemma 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"
45 unfolding restr_to_subalg_def
46 by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq)
48 lemma 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"
51 proof
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
56 next
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
60 qed
62 lemma 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"
66 proof -
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
74 qed
76 lemma 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"
80 proof -
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)
88 qed
90 lemma prob_space_restr_to_subalg:
91   assumes "subalgebra M F"
92           "prob_space M"
93   shows "prob_space (restr_to_subalg M F)"
94 by (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)
97 lemma finite_measure_restr_to_subalg:
98   assumes "subalgebra M F"
99           "finite_measure M"
100   shows "finite_measure (restr_to_subalg M F)"
101 by (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)
104 lemma 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"
108 by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
110 lemma 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"
114 by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
116 lemma measurable_from_subalg:
117   assumes "subalgebra M F"
118           "f \<in> measurable F N"
119   shows "f \<in> measurable M N"
120 using assms unfolding measurable_def subalgebra_def by auto
122 text\<open>The following is the direct transposition of \verb+nn_integral_subalgebra+
123 (from \verb+Nonnegative_Lebesgue_Integration+) in the
124 current notations, with the removal of the useless assumption $f \geq 0$.\<close>
126 lemma 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)"
129 proof (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)])
136 qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
138 text\<open>The following is the direct transposition of \verb+integral_subalgebra+
139 (from \verb+Bochner_Integration+) in the current notations.\<close>
141 lemma 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)"
146 by (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)
151 lemma 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"
156 proof (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
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
164 qed
166 lemma 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"
172 proof (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
178 qed
180 subsection \<open>Nonnegative conditional expectation\<close>
182 text \<open>The conditional expectation of a function $f$, on a measure space $M$, with respect to a
183 sub 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$.
185 Such a function is uniquely defined almost everywhere.
186 The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$,
187 and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$.
188 Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable
189 functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$
190 machinery, and works for all positive functions.
192 In this paragraph, we develop the definition and basic properties for nonnegative functions,
193 as the basics of the general case. As in the definition of integrals, the nonnegative case is done
194 with ennreal-valued functions, without any integrability assumption.
195 \<close>
197 definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
198 where
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))"
204 lemma
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"
207 by (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)
210 text \<open>The good setting for conditional expectations is the situation where the subalgebra $F$
211 gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
212 think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
213 conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
214 This means that a positive integrable function can have no meaningful conditional expectation.\<close>
216 locale 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)"
221 lemma sigma_finite_subalgebra_is_sigma_finite:
222   assumes "sigma_finite_subalgebra M F"
223   shows "sigma_finite_measure M"
224 proof
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
235 qed
237 sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure
238 using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
240 text \<open>Conditional expectations are very often used in probability spaces. This is a special case
241 of the previous one, as we prove now.\<close>
243 locale finite_measure_subalgebra = finite_measure +
244   fixes F::"'a measure"
245   assumes subalg: "subalgebra M F"
247 lemma finite_measure_subalgebra_is_sigma_finite:
248   assumes "finite_measure_subalgebra M F"
249   shows "sigma_finite_subalgebra M F"
250 proof -
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
257 qed
259 sublocale finite_measure_subalgebra \<subseteq> sigma_finite_subalgebra
260 proof -
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
266 qed
268 context sigma_finite_subalgebra
269 begin
271 text\<open>The next lemma is arguably the most fundamental property of conditional expectation:
272 when computing an expectation against an $F$-measurable function, it is equivalent to work
273 with a function or with its $F$-conditional expectation.
275 This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
276 From this point on, we will only work with it, and forget completely about
277 the definition using Radon-Nikodym derivatives.
278 \<close>
280 lemma 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)"
283 proof -
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
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
316 qed
318 lemma 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"
322 proof -
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
342 qed
344 lemma 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"
347 by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg])
349 lemma 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"
352 proof (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
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
365 qed (auto simp add: assms)
367 lemma 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"
370 proof (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
385 qed (auto simp add: assms)
387 lemma 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"
391 proof (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
399 qed (auto simp add: assms)
401 lemma 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"
405 proof -
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
415 qed
417 lemma nested_subalg_is_sigma_finite:
418   assumes "subalgebra M G" "subalgebra G F"
419   shows "sigma_finite_subalgebra M G"
420 unfolding sigma_finite_subalgebra_def
421 proof (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)
432 qed
434 lemma 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"
438 proof (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)
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)".
449 qed
451 end
453 subsection \<open>Real conditional expectation\<close>
455 text \<open>Once conditional expectations of positive functions are defined, the definition for real-valued functions
456 follows readily, by taking the difference of positive and negative parts.
457 One 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
459 concentrate on it. (It is also essential for the case of the most general Pettis integral.)
460 \<close>
462 definition 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))"
466 lemma
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"
469 unfolding real_cond_exp_def by auto
471 context sigma_finite_subalgebra
472 begin
474 lemma 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"
477 proof -
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)
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
498 qed
500 text\<open>The next lemma shows that the conditional expectation
501 is an $F$-measurable function whose average against an $F$-measurable
502 function $f$ coincides with the average of the original function against $f$.
503 It is obtained as a consequence of the same property for the positive conditional
504 expectation, taking the difference of the positive and the negative part. The proof
505 is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in
506 the subsequent lemma. The idea of the proof is essentially trivial, but the implementation
507 is slightly tedious as one should check all the integrability properties of the different parts, and go
508 back and forth between positive integral and signed integrals, and between real-valued
509 functions and ennreal-valued functions.
511 Once this lemma is available, we will use it to characterize the conditional expectation,
512 and never come back to the original technical definition, as we did in the case of the
513 nonnegative conditional expectation.
514 \<close>
516 lemma 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)"
521 proof -
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)
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)
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)
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
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
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
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
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
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
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
679 qed
681 lemma 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)"
686 proof -
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
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
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
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
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
734 qed
736 lemma 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)"
739 proof -
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
744 qed
746 lemma 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)"
749 using real_cond_exp_intg[where ?f = "\<lambda>x. 1" and ?g = f] assms by auto
751 lemma 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"
756 proof -
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
779 qed
781 lemma 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"
785 by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg])
787 lemma 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"
790 proof (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
802 qed (auto simp add: real_cond_exp_intg(1) assms)
804 lemma 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"
807 proof (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
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
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
834 qed (auto simp add: assms)
836 lemma 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"
839 proof -
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
846 qed
848 lemma 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"
852 by (rule real_cond_exp_mult[where ?f = "\<lambda>x. c" and ?g = f], auto simp add: assms borel_measurable_integrable)
854 lemma 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"
858 using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps)
860 lemma 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"
863 proof -
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
869 qed
871 lemma 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"
874 proof -
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
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
890 qed
892 lemma 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"
895 proof -
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
902 qed
904 lemma (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"
907 proof -
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
911 qed
913 lemma 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"
917 proof -
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
969 qed
971 lemma 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"
975 proof -
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
981 qed
983 lemma 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"
987 proof -
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
1000 qed
1002 lemma 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"
1006 proof -
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
1012 qed
1014 lemma 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"
1017 proof -
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
1024 qed
1026 lemma 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"
1030 proof (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))
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
1041 qed (auto simp add: assms real_cond_exp_int(1))
1043 lemma 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)"
1047 proof (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: *)
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
1068 qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
1070 text \<open>Jensen's inequality, describing the behavior of the integral under a convex function, admits
1071 a version for the conditional expectation, as follows.\<close>
1073 theorem 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"
1080 proof -
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
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
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>
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)
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: divide_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
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: divide_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)
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: divide_simps)
1212 qed
1214 text \<open>Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
1215 bound for it. Indeed, this is not true in general, as the following counterexample shows:
1217 on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
1218 for 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
1221 to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take
1222 its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not
1223 integrable.
1225 However, this counterexample is essentially the only situation where this function is not
1226 integrable, as shown by the next lemma.
1227 \<close>
1229 lemma 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))"
1236 proof -
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)
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)
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
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
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
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
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
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
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
1346 qed
1348 end
1350 end