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

     2     License: BSD

     3 *)

     4

     5 section \<open>Conditional Expectation\<close>

     6

     7 theory Conditional_Expectation

     8 imports Probability_Measure

     9 begin

    10

    11 subsection \<open>Restricting a measure to a sub-sigma-algebra\<close>

    12

    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))"

    15

    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

    28

    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)"

    31

    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)

    35

    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)

    40

    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)

    47

    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

    61

    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

    75

    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

    89

    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)

    96

    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)

   103

   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)])

   109

   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)])

   115

   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

   121

   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>

   125

   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)])

   137

   138 text\<open>The following is the direct transposition of \verb+integral_subalgebra+

   139 (from \verb+Bochner_Integration+) in the current notations.\<close>

   140

   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)

   150

   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

   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

   164 qed

   165

   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

   179

   180 subsection \<open>Nonnegative conditional expectation\<close>

   181

   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.

   191

   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>

   196

   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))"

   203

   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)

   209

   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>

   215

   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)"

   220

   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

   236

   237 sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure

   238 using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast

   239

   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>

   242

   243 locale finite_measure_subalgebra = finite_measure +

   244   fixes F::"'a measure"

   245   assumes subalg: "subalgebra M F"

   246

   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

   258

   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

   267

   268 context sigma_finite_subalgebra

   269 begin

   270

   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.

   274

   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>

   279

   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

   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

   316 qed

   317

   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

   343

   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])

   348

   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

   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

   365 qed (auto simp add: assms)

   366

   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)

   386

   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)

   400

   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

   416

   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

   433

   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)

   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)".

   449 qed

   450

   451 end

   452

   453 subsection \<open>Real conditional expectation\<close>

   454

   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>

   461

   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))"

   465

   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

   470

   471 context sigma_finite_subalgebra

   472 begin

   473

   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)

   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

   498 qed

   499

   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.

   510

   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>

   515

   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)

   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

   679 qed

   680

   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

   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

   734 qed

   735

   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

   745

   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

   750

   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

   780

   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])

   786

   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)

   803

   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

   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

   834 qed (auto simp add: assms)

   835

   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

   847

   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)

   853

   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)

   859

   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

   870

   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

   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

   890 qed

   891

   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

   903

   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

   912

   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

   970

   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

   982

   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

  1001

  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

  1013

  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

  1025

  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))

  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

  1041 qed (auto simp add: assms real_cond_exp_int(1))

  1042

  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: *)

  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

  1068 qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])

  1069

  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>

  1072

  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

  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: 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

  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: 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)

  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: divide_simps)

  1212 qed

  1213

  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:

  1216

  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.

  1224

  1225 However, this counterexample is essentially the only situation where this function is not

  1226 integrable, as shown by the next lemma.

  1227 \<close>

  1228

  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)

  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

  1346 qed

  1347

  1348 end

  1349

  1350 end
`