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