src/HOL/Probability/Conditional_Expectation.thy
author paulson <lp15@cam.ac.uk>
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