# HG changeset patch
# User hoelzl
# Date 1476376566 -7200
# Node ID 979cdfdf7a79daa1a06a256e89680b50f6899d80
# Parent  261d42f0bfac06ef84076cf56e707f3cfa68269f
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory

diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -1747,11 +1747,23 @@
     unfolding sums_iff by auto
 qed
 
-lemma integral_norm_bound:
+lemma integral_norm_bound [simp]:
   fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
-  shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
-  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
-  using integral_norm_bound_ennreal[of M f] by (simp add: integral_nonneg_AE)
+  shows "norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
+proof (cases "integrable M f")
+  case True then show ?thesis
+    using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"] integral_norm_bound_ennreal[of M f]
+    by (simp add: integral_nonneg_AE)
+next
+  case False
+  then have "norm (integral\<^sup>L M f) = 0" by (simp add: not_integrable_integral_eq)
+  moreover have "(\<integral>x. norm (f x) \<partial>M) \<ge> 0" by auto
+  ultimately show ?thesis by simp
+qed
+
+lemma integral_abs_bound [simp]:
+  fixes f :: "'a \<Rightarrow> real" shows "abs (\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
+using integral_norm_bound[of M f] by auto
 
 lemma integral_eq_nn_integral:
   assumes [measurable]: "f \<in> borel_measurable M"
@@ -1919,6 +1931,30 @@
     integral\<^sup>L M f \<le> integral\<^sup>L M g"
   by (intro integral_mono_AE) auto
 
+text {*The next two statements are useful to bound Lebesgue integrals, as they avoid one
+integrability assumption. The price to pay is that the upper function has to be nonnegative,
+but this is often true and easy to check in computations.*}
+
+lemma integral_mono_AE':
+  fixes f::"_ \<Rightarrow> real"
+  assumes "integrable M f" "AE x in M. g x \<le> f x" "AE x in M. 0 \<le> f x"
+  shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
+proof (cases "integrable M g")
+  case True
+  show ?thesis by (rule integral_mono_AE, auto simp add: assms True)
+next
+  case False
+  then have "(\<integral>x. g x \<partial>M) = 0" by (simp add: not_integrable_integral_eq)
+  also have "... \<le> (\<integral>x. f x \<partial>M)" by (simp add: integral_nonneg_AE[OF assms(3)])
+  finally show ?thesis by simp
+qed
+
+lemma integral_mono':
+  fixes f::"_ \<Rightarrow> real"
+  assumes "integrable M f" "\<And>x. x \<in> space M \<Longrightarrow> g x \<le> f x" "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> f x"
+  shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
+by (rule integral_mono_AE', insert assms, auto)
+
 lemma (in finite_measure) integrable_measure:
   assumes I: "disjoint_family_on X I" "countable I"
   shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
@@ -1942,6 +1978,12 @@
   finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
 qed fact
 
+lemma nn_integral_nonneg_infinite:
+  fixes f::"'a \<Rightarrow> real"
+  assumes "f \<in> borel_measurable M" "\<not> integrable M f" "AE x in M. f x \<ge> 0"
+  shows "(\<integral>\<^sup>+x. f x \<partial>M) = \<infinity>"
+using assms integrableI_real_bounded less_top by auto
+
 lemma integral_real_bounded:
   assumes "0 \<le> r" "integral\<^sup>N M f \<le> ennreal r"
   shows "integral\<^sup>L M f \<le> r"
@@ -1966,6 +2008,220 @@
     using \<open>0 \<le> r\<close> by (simp add: not_integrable_integral_eq)
 qed
 
+lemma integrable_Min:
+  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
+  shows "integrable M (\<lambda>x. Min {f i x|i. i \<in> I})"
+using assms apply (induct rule: finite_ne_induct) apply simp+
+proof -
+  fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Min {f i x |i. i \<in> F})"
+                    "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
+  have "{f i x |i. i = j \<or> i \<in> F} = insert (f j x) {f i x |i. i \<in> F}" for x by blast
+  then have "Min {f i x |i. i = j \<or> i \<in> F} = min (f j x) (Min {f i x |i. i \<in> F})" for x
+    using H(1) H(2) Min_insert by simp
+  moreover have "integrable M (\<lambda>x. min (f j x) (Min {f i x |i. i \<in> F}))"
+    by (rule integrable_min, auto simp add: H)
+  ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp
+qed
+
+lemma integrable_Max:
+  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
+  assumes "finite I" "I \<noteq> {}"
+          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
+  shows "integrable M (\<lambda>x. Max {f i x|i. i \<in> I})"
+using assms apply (induct rule: finite_ne_induct) apply simp+
+proof -
+  fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Max {f i x |i. i \<in> F})"
+                    "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
+  have "{f i x |i. i = j \<or> i \<in> F} = insert (f j x) {f i x |i. i \<in> F}" for x by blast
+  then have "Max {f i x |i. i = j \<or> i \<in> F} = max (f j x) (Max {f i x |i. i \<in> F})" for x
+    using H(1) H(2) Max_insert by simp
+  moreover have "integrable M (\<lambda>x. max (f j x) (Max {f i x |i. i \<in> F}))"
+    by (rule integrable_max, auto simp add: H)
+  ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp
+qed
+
+lemma integral_Markov_inequality:
+  assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
+  shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
+proof -
+  have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
+    by (rule nn_integral_mono_AE, auto simp add: `c>0` less_eq_real_def)
+  also have "... = (\<integral>x. u x \<partial>M)"
+    by (rule nn_integral_eq_integral, auto simp add: assms)
+  finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
+    by simp
+
+  have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
+    using `c>0` by (auto simp: ennreal_mult'[symmetric])
+  then have "emeasure M {x \<in> space M. u x \<ge> c} = emeasure M ({x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M))"
+    by simp
+  also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
+    by (rule nn_integral_Markov_inequality) (auto simp add: assms)
+  also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
+    apply (rule mult_left_mono) using * `c>0` by auto
+  finally show ?thesis
+    using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
+qed
+
+lemma integral_ineq_eq_0_then_AE:
+  fixes f::"_ \<Rightarrow> real"
+  assumes "AE x in M. f x \<le> g x" "integrable M f" "integrable M g"
+          "(\<integral>x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
+  shows "AE x in M. f x = g x"
+proof -
+  define h where "h = (\<lambda>x. g x - f x)"
+  have "AE x in M. h x = 0"
+    apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
+    unfolding h_def using assms by auto
+  then show ?thesis unfolding h_def by auto
+qed
+
+lemma not_AE_zero_int_E:
+  fixes f::"'a \<Rightarrow> real"
+  assumes "AE x in M. f x \<ge> 0" "(\<integral>x. f x \<partial>M) > 0"
+      and [measurable]: "f \<in> borel_measurable M"
+  shows "\<exists>A e. A \<in> sets M \<and> e>0 \<and> emeasure M A > 0 \<and> (\<forall>x \<in> A. f x \<ge> e)"
+proof (rule not_AE_zero_E, auto simp add: assms)
+  assume *: "AE x in M. f x = 0"
+  have "(\<integral>x. f x \<partial>M) = (\<integral>x. 0 \<partial>M)" by (rule integral_cong_AE, auto simp add: *)
+  then have "(\<integral>x. f x \<partial>M) = 0" by simp
+  then show False using assms(2) by simp
+qed
+
+lemma tendsto_L1_int:
+  fixes u :: "_ \<Rightarrow> _ \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes [measurable]: "\<And>n. integrable M (u n)" "integrable M f"
+          and "((\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) \<longlongrightarrow> 0) F"
+  shows "((\<lambda>n. (\<integral>x. u n x \<partial>M)) \<longlongrightarrow> (\<integral>x. f x \<partial>M)) F"
+proof -
+  have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> (0::ennreal)) F"
+  proof (rule tendsto_sandwich[of "\<lambda>_. 0", where ?h = "\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"], auto simp add: assms)
+    {
+      fix n
+      have "(\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M) = (\<integral>x. u n x - f x \<partial>M)"
+        apply (rule Bochner_Integration.integral_diff[symmetric]) using assms by auto
+      then have "norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) = norm (\<integral>x. u n x - f x \<partial>M)"
+        by auto
+      also have "... \<le> (\<integral>x. norm(u n x - f x) \<partial>M)"
+        by (rule integral_norm_bound)
+      finally have "ennreal(norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<le> (\<integral>x. norm(u n x - f x) \<partial>M)"
+        by simp
+      also have "... = (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"
+        apply (rule nn_integral_eq_integral[symmetric]) using assms by auto
+      finally have "norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) \<le> (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)" by simp
+    }
+    then show "eventually (\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M)) \<le> (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) F"
+      by auto
+  qed
+  then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
+    by (simp add: ennreal_0[symmetric] del: ennreal_0)
+  then have "((\<lambda>n. ((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F" using tendsto_norm_zero_iff by blast
+  then show ?thesis using Lim_null by auto
+qed
+
+text {*The next lemma asserts that, if a sequence of functions converges in $L^1$, then
+it admits a subsequence that converges almost everywhere.*}
+
+lemma tendsto_L1_AE_subseq:
+  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes [measurable]: "\<And>n. integrable M (u n)"
+      and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
+  shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
+proof -
+  {
+    fix k
+    have "eventually (\<lambda>n. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k) sequentially"
+      using order_tendstoD(2)[OF assms(2)] by auto
+    with eventually_elim2[OF eventually_gt_at_top[of k] this]
+    have "\<exists>n>k. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k"
+      by (metis eventually_False_sequentially)
+  }
+  then have "\<exists>r. \<forall>n. True \<and> (r (Suc n) > r n \<and> (\<integral>x. norm(u (r (Suc n)) x) \<partial>M) < (1/2)^(r n))"
+    by (intro dependent_nat_choice, auto)
+  then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
+    by (auto simp: subseq_Suc_iff)
+  define r where "r = (\<lambda>n. r0(n+1))"
+  have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
+  have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
+  proof -
+    have "r0 n \<ge> n" using `subseq r0` by (simp add: seq_suble)
+    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF `r0 n \<ge> n`], auto)
+    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
+    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
+    moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
+      by (rule nn_integral_eq_integral, auto simp add: integrable_norm[OF assms(1)[of "r n"]])
+    ultimately show ?thesis by (auto intro: ennreal_lessI)
+  qed
+
+  have "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
+  proof (rule AE_upper_bound_inf_ennreal)
+    fix e::real assume "e > 0"
+    define A where "A = (\<lambda>n. {x \<in> space M. norm(u (r n) x) \<ge> e})"
+    have A_meas [measurable]: "\<And>n. A n \<in> sets M" unfolding A_def by auto
+    have A_bound: "emeasure M (A n) < (1/e) * ennreal((1/2)^n)" for n
+    proof -
+      have *: "indicator (A n) x \<le> (1/e) * ennreal(norm(u (r n) x))" for x
+        apply (cases "x \<in> A n") unfolding A_def using \<open>0 < e\<close> by (auto simp: ennreal_mult[symmetric])
+      have "emeasure M (A n) = (\<integral>\<^sup>+x. indicator (A n) x \<partial>M)" by auto
+      also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
+        apply (rule nn_integral_mono) using * by auto
+      also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
+        apply (rule nn_integral_cmult) using `e > 0` by auto
+      also have "... < (1/e) * ennreal((1/2)^n)"
+        using I[of n] `e > 0` by (intro ennreal_mult_strict_left_mono) auto
+      finally show ?thesis by simp
+    qed
+    have A_fin: "emeasure M (A n) < \<infinity>" for n
+      using `e > 0` A_bound[of n]
+      by (auto simp add: ennreal_mult less_top[symmetric])
+
+    have A_sum: "summable (\<lambda>n. measure M (A n))"
+    proof (rule summable_comparison_test'[of "\<lambda>n. (1/e) * (1/2)^n" 0])
+      have "summable (\<lambda>n. (1/(2::real))^n)" by (simp add: summable_geometric)
+      then show "summable (\<lambda>n. (1/e) * (1/2)^n)" using summable_mult by blast
+      fix n::nat assume "n \<ge> 0"
+      have "norm(measure M (A n)) = measure M (A n)" by simp
+      also have "... = enn2real(emeasure M (A n))" unfolding measure_def by simp
+      also have "... < enn2real((1/e) * (1/2)^n)"
+        using A_bound[of n] \<open>emeasure M (A n) < \<infinity>\<close> \<open>0 < e\<close>
+        by (auto simp: emeasure_eq_ennreal_measure ennreal_mult[symmetric] ennreal_less_iff)
+      also have "... = (1/e) * (1/2)^n"
+        using \<open>0<e\<close> by auto
+      finally show "norm(measure M (A n)) \<le> (1/e) * (1/2)^n" by simp
+    qed
+
+    have "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
+      by (rule borel_cantelli_AE1[OF A_meas A_fin A_sum])
+    moreover
+    {
+      fix x assume "eventually (\<lambda>n. x \<in> space M - A n) sequentially"
+      moreover have "norm(u (r n) x) \<le> ennreal e" if "x \<in> space M - A n" for n
+        using that unfolding A_def by (auto intro: ennreal_leI)
+      ultimately have "eventually (\<lambda>n. norm(u (r n) x) \<le> ennreal e) sequentially"
+        by (simp add: eventually_mono)
+      then have "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> e"
+        by (simp add: Limsup_bounded)
+    }
+    ultimately show "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0 + ennreal e" by auto
+  qed
+  moreover
+  {
+    fix x assume "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
+    moreover then have "liminf (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
+      by (rule order_trans[rotated]) (auto intro: Liminf_le_Limsup)
+    ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
+      using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
+    then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
+      by (simp add: ennreal_0[symmetric] del: ennreal_0)
+    then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
+      by (simp add: tendsto_norm_zero_iff)
+  }
+  ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
+  then show ?thesis using `subseq r` by auto
+qed
+
 subsection \<open>Restricted measure spaces\<close>
 
 lemma integrable_restrict_space:
@@ -2478,6 +2734,12 @@
   apply auto
   done
 
+lemma (in finite_measure) integral_bounded_eq_bound_then_AE:
+  assumes "AE x in M. f x \<le> (c::real)"
+    "integrable M f" "(\<integral>x. f x \<partial>M) = c * measure M (space M)"
+  shows "AE x in M. f x = c"
+  apply (rule integral_ineq_eq_0_then_AE) using assms by auto
+
 lemma integral_indicator_finite_real:
   fixes f :: "'a \<Rightarrow> real"
   assumes [simp]: "finite A"
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -1896,6 +1896,9 @@
     by auto
 qed
 
+text \<open>The next lemmas hold in any second countable linorder (including ennreal or ereal for instance),
+but in the current state they are restricted to reals.\<close>
+
 lemma borel_measurable_mono_on_fnc:
   fixes f :: "real \<Rightarrow> real" and A :: "real set"
   assumes "mono_on f A"
@@ -1907,6 +1910,12 @@
               intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
   done
 
+lemma borel_measurable_piecewise_mono:
+  fixes f::"real \<Rightarrow> real" and C::"real set set"
+  assumes "countable C" "\<And>c. c \<in> C \<Longrightarrow> c \<in> sets borel" "\<And>c. c \<in> C \<Longrightarrow> mono_on f c" "(\<Union>C) = UNIV"
+  shows "f \<in> borel_measurable borel"
+by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms)
+
 lemma borel_measurable_mono:
   fixes f :: "real \<Rightarrow> real"
   shows "mono f \<Longrightarrow> f \<in> borel_measurable borel"
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Measurable.thy
--- a/src/HOL/Analysis/Measurable.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Measurable.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -636,6 +636,16 @@
     unfolding pred_restrict_space[OF P_f] by (simp cong: measurable_cong)
 qed
 
+lemma measurable_limsup [measurable (raw)]:
+  assumes [measurable]: "\<And>n. A n \<in> sets M"
+  shows "limsup A \<in> sets M"
+by (subst limsup_INF_SUP, auto)
+
+lemma measurable_liminf [measurable (raw)]:
+  assumes [measurable]: "\<And>n. A n \<in> sets M"
+  shows "liminf A \<in> sets M"
+by (subst liminf_SUP_INF, auto)
+
 hide_const (open) pred
 
 end
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -1059,6 +1059,11 @@
   with AE_iff_null[of M P] assms show ?thesis by auto
 qed
 
+lemma AE_E3:
+  assumes "AE x in M. P x"
+  obtains N where "\<And>x. x \<in> space M - N \<Longrightarrow> P x" "N \<in> null_sets M"
+using assms unfolding eventually_ae_filter by auto
+
 lemma AE_I:
   assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
   shows "AE x in M. P x"
@@ -1087,6 +1092,10 @@
   qed
 qed
 
+text {*The next lemma is convenient to combine with a lemma whose conclusion is of the
+form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
+but using \<open>AE_symmetric[OF...]\<close> will replace it.*}
+
 (* depricated replace by laws about eventually *)
 lemma
   shows AE_iffI: "AE x in M. P x \<Longrightarrow> AE x in M. P x \<longleftrightarrow> Q x \<Longrightarrow> AE x in M. Q x"
@@ -1096,6 +1105,11 @@
     and AE_conj_iff[simp]: "(AE x in M. P x \<and> Q x) \<longleftrightarrow> (AE x in M. P x) \<and> (AE x in M. Q x)"
   by auto
 
+lemma AE_symmetric:
+  assumes "AE x in M. P x = Q x"
+  shows "AE x in M. Q x = P x"
+  using assms by auto
+
 lemma AE_impI:
   "(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
   by (cases P) auto
@@ -1166,6 +1180,10 @@
     unfolding eventually_ae_filter by auto
 qed auto
 
+lemma AE_ball_countable':
+  "(\<And>N. N \<in> I \<Longrightarrow> AE x in M. P N x) \<Longrightarrow> countable I \<Longrightarrow> AE x in M. \<forall>N \<in> I. P N x"
+  unfolding AE_ball_countable by simp
+
 lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
   by (auto simp add: pairwise_def)
 
@@ -1225,6 +1243,11 @@
   using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"]
   by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets)
 
+lemma emeasure_0_AE:
+  assumes "emeasure M (space M) = 0"
+  shows "AE x in M. P x"
+using eventually_ae_filter assms by blast
+
 lemma emeasure_add_AE:
   assumes [measurable]: "A \<in> sets M" "B \<in> sets M" "C \<in> sets M"
   assumes 1: "AE x in M. x \<in> C \<longleftrightarrow> x \<in> A \<or> x \<in> B"
@@ -1328,6 +1351,40 @@
   qed
 qed
 
+lemma (in sigma_finite_measure) approx_PInf_emeasure_with_finite:
+  fixes C::real
+  assumes W_meas: "W \<in> sets M"
+      and W_inf: "emeasure M W = \<infinity>"
+  obtains Z where "Z \<in> sets M" "Z \<subseteq> W" "emeasure M Z < \<infinity>" "emeasure M Z > C"
+proof -
+  obtain A :: "nat \<Rightarrow> 'a set"
+    where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
+    using sigma_finite_incseq by blast
+  define B where "B = (\<lambda>i. W \<inter> A i)"
+  have B_meas: "\<And>i. B i \<in> sets M" using W_meas `range A \<subseteq> sets M` B_def by blast
+  have b: "\<And>i. B i \<subseteq> W" using B_def by blast
+
+  { fix i
+    have "emeasure M (B i) \<le> emeasure M (A i)"
+      using A by (intro emeasure_mono) (auto simp: B_def)
+    also have "emeasure M (A i) < \<infinity>"
+      using `\<And>i. emeasure M (A i) \<noteq> \<infinity>` by (simp add: less_top)
+    finally have "emeasure M (B i) < \<infinity>" . }
+  note c = this
+
+  have "W = (\<Union>i. B i)" using B_def `(\<Union>i. A i) = space M` W_meas by auto
+  moreover have "incseq B" using B_def `incseq A` by (simp add: incseq_def subset_eq)
+  ultimately have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> emeasure M W" using W_meas B_meas
+    by (simp add: B_meas Lim_emeasure_incseq image_subset_iff)
+  then have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> \<infinity>" using W_inf by simp
+  from order_tendstoD(1)[OF this, of C]
+  obtain i where d: "emeasure M (B i) > C"
+    by (auto simp: eventually_sequentially)
+  have "B i \<in> sets M" "B i \<subseteq> W" "emeasure M (B i) < \<infinity>" "emeasure M (B i) > C"
+    using B_meas b c d by auto
+  then show ?thesis using that by blast
+qed
+
 subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
 
 definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
@@ -1824,6 +1881,88 @@
   then show ?fm ?m by auto
 qed
 
+lemma suminf_exist_split2:
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes "summable f"
+  shows "(\<lambda>n. (\<Sum>k. f(k+n))) \<longlonglongrightarrow> 0"
+by (subst lim_sequentially, auto simp add: dist_norm suminf_exist_split[OF _ assms])
+
+lemma emeasure_union_summable:
+  assumes [measurable]: "\<And>n. A n \<in> sets M"
+    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
+  shows "emeasure M (\<Union>n. A n) < \<infinity>" "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
+proof -
+  define B where "B = (\<lambda>N. (\<Union>n\<in>{..<N}. A n))"
+  have [measurable]: "B N \<in> sets M" for N unfolding B_def by auto
+  have "(\<lambda>N. emeasure M (B N)) \<longlonglongrightarrow> emeasure M (\<Union>N. B N)"
+    apply (rule Lim_emeasure_incseq) unfolding B_def by (auto simp add: SUP_subset_mono incseq_def)
+  moreover have "emeasure M (B N) \<le> ennreal (\<Sum>n. measure M (A n))" for N
+  proof -
+    have *: "(\<Sum>n\<in>{..<N}. measure M (A n)) \<le> (\<Sum>n. measure M (A n))"
+      using assms(3) measure_nonneg sum_le_suminf by blast
+
+    have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
+      unfolding B_def by (rule emeasure_subadditive_finite, auto)
+    also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
+      using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
+    also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
+      by auto
+    also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
+      using * by (auto simp: ennreal_leI)
+    finally show ?thesis by simp
+  qed
+  ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
+    by (simp add: Lim_bounded_ereal)
+  then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
+    unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
+  then show "emeasure M (\<Union>n. A n) < \<infinity>"
+    by (auto simp: less_top[symmetric] top_unique)
+qed
+
+lemma borel_cantelli_limsup1:
+  assumes [measurable]: "\<And>n. A n \<in> sets M"
+    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
+  shows "limsup A \<in> null_sets M"
+proof -
+  have "emeasure M (limsup A) \<le> 0"
+  proof (rule LIMSEQ_le_const)
+    have "(\<lambda>n. (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0" by (rule suminf_exist_split2[OF assms(3)])
+    then show "(\<lambda>n. ennreal (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0"
+      unfolding ennreal_0[symmetric] by (intro tendsto_ennrealI)
+    have "emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))" for n
+    proof -
+      have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
+      have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
+        by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
+      also have "... = emeasure M (\<Union>k. A (k+n))"
+        using I by auto
+      also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
+        apply (rule emeasure_union_summable)
+        using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
+      finally show ?thesis by simp
+    qed
+    then show "\<exists>N. \<forall>n\<ge>N. emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))"
+      by auto
+  qed
+  then show ?thesis using assms(1) measurable_limsup by auto
+qed
+
+lemma borel_cantelli_AE1:
+  assumes [measurable]: "\<And>n. A n \<in> sets M"
+    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
+  shows "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
+proof -
+  have "AE x in M. x \<notin> limsup A"
+    using borel_cantelli_limsup1[OF assms] unfolding eventually_ae_filter by auto
+  moreover
+  {
+    fix x assume "x \<notin> limsup A"
+    then obtain N where "x \<notin> (\<Union>n\<in>{N..}. A n)" unfolding limsup_INF_SUP by blast
+    then have "eventually (\<lambda>n. x \<notin> A n) sequentially" using eventually_sequentially by auto
+  }
+  ultimately show ?thesis by auto
+qed
+
 subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
 
 locale finite_measure = sigma_finite_measure M for M +
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -9,6 +9,102 @@
   imports Measure_Space Borel_Space
 begin
 
+subsection \<open>Approximating functions\<close>
+
+lemma AE_upper_bound_inf_ennreal:
+  fixes F G::"'a \<Rightarrow> ennreal"
+  assumes "\<And>e. (e::real) > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e"
+  shows "AE x in M. F x \<le> G x"
+proof -
+  have "AE x in M. \<forall>n::nat. F x \<le> G x + ennreal (1 / Suc n)"
+    using assms by (auto simp: AE_all_countable)
+  then show ?thesis
+  proof (eventually_elim)
+    fix x assume x: "\<forall>n::nat. F x \<le> G x + ennreal (1 / Suc n)"
+    show "F x \<le> G x"
+    proof (rule ennreal_le_epsilon)
+      fix e :: real assume "0 < e"
+      then obtain n where n: "1 / Suc n < e"
+        by (blast elim: nat_approx_posE)
+      have "F x \<le> G x + 1 / Suc n"
+        using x by simp
+      also have "\<dots> \<le> G x + e"
+        using n by (intro add_mono ennreal_leI) auto
+      finally show "F x \<le> G x + ennreal e" .
+    qed
+  qed
+qed
+
+lemma AE_upper_bound_inf:
+  fixes F G::"'a \<Rightarrow> real"
+  assumes "\<And>e. e > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e"
+  shows "AE x in M. F x \<le> G x"
+proof -
+  have "AE x in M. F x \<le> G x + 1/real (n+1)" for n::nat
+    by (rule assms, auto)
+  then have "AE x in M. \<forall>n::nat \<in> UNIV. F x \<le> G x + 1/real (n+1)"
+    by (rule AE_ball_countable', auto)
+  moreover
+  {
+    fix x assume i: "\<forall>n::nat \<in> UNIV. F x \<le> G x + 1/real (n+1)"
+    have "(\<lambda>n. G x + 1/real (n+1)) \<longlonglongrightarrow> G x + 0"
+      by (rule tendsto_add, simp, rule LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1])
+    then have "F x \<le> G x" using i LIMSEQ_le_const by fastforce
+  }
+  ultimately show ?thesis by auto
+qed
+
+lemma not_AE_zero_ennreal_E:
+  fixes f::"'a \<Rightarrow> ennreal"
+  assumes "\<not> (AE x in M. f x = 0)" and [measurable]: "f \<in> borel_measurable M"
+  shows "\<exists>A\<in>sets M. \<exists>e::real>0. emeasure M A > 0 \<and> (\<forall>x \<in> A. f x \<ge> e)"
+proof -
+  { assume "\<not> (\<exists>e::real>0. {x \<in> space M. f x \<ge> e} \<notin> null_sets M)"
+    then have "0 < e \<Longrightarrow> AE x in M. f x \<le> e" for e :: real
+      by (auto simp: not_le less_imp_le dest!: AE_not_in)
+    then have "AE x in M. f x \<le> 0"
+      by (intro AE_upper_bound_inf_ennreal[where G="\<lambda>_. 0"]) simp
+    then have False
+      using assms by auto }
+  then obtain e::real where e: "e > 0" "{x \<in> space M. f x \<ge> e} \<notin> null_sets M" by auto
+  define A where "A = {x \<in> space M. f x \<ge> e}"
+  have 1 [measurable]: "A \<in> sets M" unfolding A_def by auto
+  have 2: "emeasure M A > 0"
+    using e(2) A_def \<open>A \<in> sets M\<close> by auto
+  have 3: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> e" unfolding A_def by auto
+  show ?thesis using e(1) 1 2 3 by blast
+qed
+
+lemma not_AE_zero_E:
+  fixes f::"'a \<Rightarrow> real"
+  assumes "AE x in M. f x \<ge> 0"
+          "\<not>(AE x in M. f x = 0)"
+      and [measurable]: "f \<in> borel_measurable M"
+  shows "\<exists>A e. A \<in> sets M \<and> e>0 \<and> emeasure M A > 0 \<and> (\<forall>x \<in> A. f x \<ge> e)"
+proof -
+  have "\<exists>e. e > 0 \<and> {x \<in> space M. f x \<ge> e} \<notin> null_sets M"
+  proof (rule ccontr)
+    assume *: "\<not>(\<exists>e. e > 0 \<and> {x \<in> space M. f x \<ge> e} \<notin> null_sets M)"
+    {
+      fix e::real assume "e > 0"
+      then have "{x \<in> space M. f x \<ge> e} \<in> null_sets M" using * by blast
+      then have "AE x in M. x \<notin> {x \<in> space M. f x \<ge> e}" using AE_not_in by blast
+      then have "AE x in M. f x \<le> e" by auto
+    }
+    then have "AE x in M. f x \<le> 0" by (rule AE_upper_bound_inf, auto)
+    then have "AE x in M. f x = 0" using assms(1) by auto
+    then show False using assms(2) by auto
+  qed
+  then obtain e where e: "e>0" "{x \<in> space M. f x \<ge> e} \<notin> null_sets M" by auto
+  define A where "A = {x \<in> space M. f x \<ge> e}"
+  have 1 [measurable]: "A \<in> sets M" unfolding A_def by auto
+  have 2: "emeasure M A > 0"
+    using e(2) A_def \<open>A \<in> sets M\<close> by auto
+  have 3: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> e" unfolding A_def by auto
+  show ?thesis
+    using e(1) 1 2 3 by blast
+qed
+
 subsection "Simple function"
 
 text \<open>
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -44,6 +44,64 @@
   qed
 qed fact
 
+text {*An equivalent characterization of sigma-finite spaces is the existence of integrable
+positive functions (or, still equivalently, the existence of a probability measure which is in
+the same measure class as the original measure).*}
+
+lemma (in sigma_finite_measure) obtain_positive_integrable_function:
+  obtains f::"'a \<Rightarrow> real" where
+    "f \<in> borel_measurable M"
+    "\<And>x. f x > 0"
+    "\<And>x. f x \<le> 1"
+    "integrable M f"
+proof -
+  obtain A :: "nat \<Rightarrow> 'a set" where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
+    using sigma_finite by auto
+  then have [measurable]:"A n \<in> sets M" for n by auto
+  define g where "g = (\<lambda>x. (\<Sum>n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n))))"
+  have [measurable]: "g \<in> borel_measurable M" unfolding g_def by auto
+  have *: "summable (\<lambda>n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n)))" for x
+    apply (rule summable_comparison_test'[of "\<lambda>n. (1/2)^(Suc n)" 0])
+    using power_half_series summable_def by (auto simp add: indicator_def divide_simps)
+  have "g x \<le> (\<Sum>n. (1/2)^(Suc n))" for x unfolding g_def
+    apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps)
+  then have g_le_1: "g x \<le> 1" for x using power_half_series sums_unique by fastforce
+
+  have g_pos: "g x > 0" if "x \<in> space M" for x
+  unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
+    obtain i where "x \<in> A i" using `(\<Union>i. A i) = space M` `x \<in> space M` by auto
+    then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
+      unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
+      by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
+    then show "\<exists>i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))"
+      by auto
+  qed
+
+  have "integrable M g"
+  unfolding g_def proof (rule integrable_suminf)
+    fix n
+    show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
+      using `emeasure M (A n) \<noteq> \<infinity>`
+      by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
+  next
+    show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
+      using * by auto
+    show "summable (\<lambda>n. (\<integral>x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \<partial>M))"
+      apply (rule summable_comparison_test'[of "\<lambda>n. (1/2)^(Suc n)" 0], auto)
+      using power_half_series summable_def apply auto[1]
+      apply (auto simp add: divide_simps) using measure_nonneg[of M] not_less by fastforce
+  qed
+
+  define f where "f = (\<lambda>x. if x \<in> space M then g x else 1)"
+  have "f x > 0" for x unfolding f_def using g_pos by auto
+  moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto
+  moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto
+  moreover have "integrable M f"
+    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using `integrable M g` by auto
+  ultimately show "(\<And>f. f \<in> borel_measurable M \<Longrightarrow> (\<And>x. 0 < f x) \<Longrightarrow> (\<And>x. f x \<le> 1) \<Longrightarrow> integrable M f \<Longrightarrow> thesis) \<Longrightarrow> thesis"
+    by (meson that)
+qed
+
 lemma (in sigma_finite_measure) Ex_finite_integrable_function:
   "\<exists>h\<in>borel_measurable M. integral\<^sup>N M h \<noteq> \<infinity> \<and> (\<forall>x\<in>space M. 0 < h x \<and> h x < \<infinity>)"
 proof -
@@ -878,9 +936,6 @@
   finally show ?thesis by simp
 qed
 
-lemma null_setsD_AE: "N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
-  using AE_iff_null_sets[of N M] by auto
-
 lemma (in sigma_finite_measure) RN_deriv_unique:
   assumes f: "f \<in> borel_measurable M"
   and eq: "density M f = N"
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/Analysis/Set_Integral.thy
     Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
+    Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
 
 Notation and useful facts for working with integrals over a set.
 
@@ -7,7 +8,7 @@
 *)
 
 theory Set_Integral
-  imports Bochner_Integration
+  imports Radon_Nikodym
 begin
 
 (*
@@ -523,5 +524,235 @@
   shows "set_borel_measurable borel {a..b} f"
   by (rule set_borel_measurable_continuous[OF _ assms]) simp
 
+
+text{* This notation is from Sébastien Gouëzel: His use is not directly in line with the
+notations in this file, they are more in line with sum, and more readable he thinks. *}
+
+abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
+
+syntax
+"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
+("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+
+"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
+("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
+
+translations
+"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
+"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
+
+lemma nn_integral_disjoint_pair:
+  assumes [measurable]: "f \<in> borel_measurable M"
+          "B \<in> sets M" "C \<in> sets M"
+          "B \<inter> C = {}"
+  shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M) + (\<integral>\<^sup>+x \<in> C. f x \<partial>M)"
+proof -
+  have mes: "\<And>D. D \<in> sets M \<Longrightarrow> (\<lambda>x. f x * indicator D x) \<in> borel_measurable M" by simp
+  have pos: "\<And>D. AE x in M. f x * indicator D x \<ge> 0" using assms(2) by auto
+  have "\<And>x. f x * indicator (B \<union> C) x = f x * indicator B x + f x * indicator C x" using assms(4)
+    by (auto split: split_indicator)
+  then have "(\<integral>\<^sup>+x. f x * indicator (B \<union> C) x \<partial>M) = (\<integral>\<^sup>+x. f x * indicator B x + f x * indicator C x \<partial>M)"
+    by simp
+  also have "... = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
+    by (rule nn_integral_add) (auto simp add: assms mes pos)
+  finally show ?thesis by simp
+qed
+
+lemma nn_integral_disjoint_pair_countspace:
+  assumes "B \<inter> C = {}"
+  shows "(\<integral>\<^sup>+x \<in> B \<union> C. f x \<partial>count_space UNIV) = (\<integral>\<^sup>+x \<in> B. f x \<partial>count_space UNIV) + (\<integral>\<^sup>+x \<in> C. f x \<partial>count_space UNIV)"
+by (rule nn_integral_disjoint_pair) (simp_all add: assms)
+
+lemma nn_integral_null_delta:
+  assumes "A \<in> sets M" "B \<in> sets M"
+          "(A - B) \<union> (B - A) \<in> null_sets M"
+  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M)"
+proof (rule nn_integral_cong_AE, auto simp add: indicator_def)
+  have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
+    using assms(3) AE_not_in by blast
+  then show "AE a in M. a \<notin> A \<longrightarrow> a \<in> B \<longrightarrow> f a = 0"
+    by auto
+  show "AE x\<in>A in M. x \<notin> B \<longrightarrow> f x = 0"
+    using * by auto
+qed
+
+lemma nn_integral_disjoint_family:
+  assumes [measurable]: "f \<in> borel_measurable M" "\<And>(n::nat). B n \<in> sets M"
+      and "disjoint_family B"
+  shows "(\<integral>\<^sup>+x \<in> (\<Union>n. B n). f x \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+x \<in> B n. f x \<partial>M))"
+proof -
+  have "(\<integral>\<^sup>+ x. (\<Sum>n. f x * indicator (B n) x) \<partial>M) = (\<Sum>n. (\<integral>\<^sup>+ x. f x * indicator (B n) x \<partial>M))"
+    by (rule nn_integral_suminf) simp
+  moreover have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (\<Union>n. B n) x" for x
+  proof (cases)
+    assume "x \<in> (\<Union>n. B n)"
+    then obtain n where "x \<in> B n" by blast
+    have a: "finite {n}" by simp
+    have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using `x \<in> B n` assms(3) disjoint_family_on_def
+      by (metis IntI UNIV_I empty_iff)
+    then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
+    then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
+
+    define h where "h = (\<lambda>i. f x * indicator (B i) x)"
+    then have "\<And>i. i \<notin> {n} \<Longrightarrow> h i = 0" using b by simp
+    then have "(\<Sum>i. h i) = (\<Sum>i\<in>{n}. h i)"
+      by (metis sums_unique[OF sums_finite[OF a]])
+    then have "(\<Sum>i. h i) = h n" by simp
+    then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
+    then have "(\<Sum>n. f x * indicator (B n) x) = f x" using `x \<in> B n` indicator_def by simp
+    then show ?thesis using `x \<in> (\<Union>n. B n)` by auto
+  next
+    assume "x \<notin> (\<Union>n. B n)"
+    then have "\<And>n. f x * indicator (B n) x = 0" by simp
+    have "(\<Sum>n. f x * indicator (B n) x) = 0"
+      by (simp add: `\<And>n. f x * indicator (B n) x = 0`)
+    then show ?thesis using `x \<notin> (\<Union>n. B n)` by auto
+  qed
+  ultimately show ?thesis by simp
+qed
+
+lemma nn_set_integral_add:
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+          "A \<in> sets M"
+  shows "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x \<in> A. f x \<partial>M) + (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
+proof -
+  have "(\<integral>\<^sup>+x \<in> A. (f x + g x) \<partial>M) = (\<integral>\<^sup>+x. (f x * indicator A x + g x * indicator A x) \<partial>M)"
+    by (auto simp add: indicator_def intro!: nn_integral_cong)
+  also have "... = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
+    apply (rule nn_integral_add) using assms(1) assms(2) by auto
+  finally show ?thesis by simp
+qed
+
+lemma nn_set_integral_cong:
+  assumes "AE x in M. f x = g x"
+  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
+apply (rule nn_integral_cong_AE) using assms(1) by auto
+
+lemma nn_set_integral_set_mono:
+  "A \<subseteq> B \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+ x \<in> B. f x \<partial>M)"
+by (auto intro!: nn_integral_mono split: split_indicator)
+
+lemma nn_set_integral_mono:
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+          "A \<in> sets M"
+      and "AE x\<in>A in M. f x \<le> g x"
+  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
+by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms)
+
+lemma nn_set_integral_space [simp]:
+  shows "(\<integral>\<^sup>+ x \<in> space M. f x \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
+by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong)
+
+lemma nn_integral_count_compose_inj:
+  assumes "inj_on g A"
+  shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
+proof -
+  have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+x. f (g x) \<partial>count_space A)"
+    by (auto simp add: nn_integral_count_space_indicator[symmetric])
+  also have "... = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
+    by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
+  also have "... = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
+    by (auto simp add: nn_integral_count_space_indicator[symmetric])
+  finally show ?thesis by simp
+qed
+
+lemma nn_integral_count_compose_bij:
+  assumes "bij_betw g A B"
+  shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> B. f y \<partial>count_space UNIV)"
+proof -
+  have "inj_on g A" using assms bij_betw_def by auto
+  then have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
+    by (rule nn_integral_count_compose_inj)
+  then show ?thesis using assms by (simp add: bij_betw_def)
+qed
+
+lemma set_integral_null_delta:
+  fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
+  assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
+    and "(A - B) \<union> (B - A) \<in> null_sets M"
+  shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
+proof (rule set_integral_cong_set, auto)
+  have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
+    using assms(4) AE_not_in by blast
+  then show "AE x in M. (x \<in> B) = (x \<in> A)"
+    by auto
+qed
+
+lemma set_integral_space:
+  assumes "integrable M f"
+  shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
+by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
+
+lemma null_if_pos_func_has_zero_nn_int:
+  fixes f::"'a \<Rightarrow> ennreal"
+  assumes [measurable]: "f \<in> borel_measurable M" "A \<in> sets M"
+    and "AE x\<in>A in M. f x > 0" "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = 0"
+  shows "A \<in> null_sets M"
+proof -
+  have "AE x in M. f x * indicator A x = 0"
+    by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4))
+  then have "AE x\<in>A in M. False" using assms(3) by auto
+  then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
+qed
+
+lemma null_if_pos_func_has_zero_int:
+  assumes [measurable]: "integrable M f" "A \<in> sets M"
+      and "AE x\<in>A in M. f x > 0" "(\<integral>x\<in>A. f x \<partial>M) = (0::real)"
+  shows "A \<in> null_sets M"
+proof -
+  have "AE x in M. indicator A x * f x = 0"
+    apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
+    using assms integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+  then have "AE x\<in>A in M. f x = 0" by auto
+  then have "AE x\<in>A in M. False" using assms(3) by auto
+  then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
+qed
+
+text{*The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
+for nonnegative set integrals introduced earlier.*}
+
+lemma (in sigma_finite_measure) density_unique2:
+  assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
+  assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+ x \<in> A. f' x \<partial>M)"
+  shows "AE x in M. f x = f' x"
+proof (rule density_unique)
+  show "density M f = density M f'"
+    by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq)
+qed (auto simp add: assms)
+
+
+text {* The next lemma implies the same statement for Banach-space valued functions
+using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
+only formulate it for real-valued functions.*}
+
+lemma density_unique_real:
+  fixes f f'::"_ \<Rightarrow> real"
+  assumes [measurable]: "integrable M f" "integrable M f'"
+  assumes density_eq: "\<And>A. A \<in> sets M \<Longrightarrow> (\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M)"
+  shows "AE x in M. f x = f' x"
+proof -
+  define A where "A = {x \<in> space M. f x < f' x}"
+  then have [measurable]: "A \<in> sets M" by simp
+  have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = (\<integral>x \<in> A. f' x \<partial>M) - (\<integral>x \<in> A. f x \<partial>M)"
+    using `A \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
+  then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
+  then have "A \<in> null_sets M"
+    using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
+  then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
+  then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
+
+
+  define B where "B = {x \<in> space M. f' x < f x}"
+  then have [measurable]: "B \<in> sets M" by simp
+  have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = (\<integral>x \<in> B. f x \<partial>M) - (\<integral>x \<in> B. f' x \<partial>M)"
+    using `B \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
+  then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
+  then have "B \<in> null_sets M"
+    using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
+  then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
+  then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
+
+  then show ?thesis using * by auto
+qed
+
 end
-
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -75,7 +75,7 @@
 lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
 proof -
   have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)"
-    unfolding char_def by (intro integral_norm_bound integrable_iexp) auto
+    unfolding char_def by (intro integral_norm_bound)
   also have "\<dots> \<le> 1"
     by (simp del: of_real_mult)
   finally show ?thesis .
@@ -318,7 +318,7 @@
   also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
     unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp
+    by (intro integral_norm_bound)
   also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
   proof (rule integral_mono)
     show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
@@ -362,7 +362,7 @@
   also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
     unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
   also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
-    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp
+    by (rule integral_norm_bound)
   also have "\<dots> \<le> expectation (\<lambda>x. min (2 * \<bar>t * x\<bar>^n / fact n) (\<bar>t * x\<bar>^(Suc n) / fact (Suc n)))"
     (is "_ \<le> expectation ?f")
   proof (rule integral_mono)
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Probability/Conditional_Expectation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Probability/Conditional_Expectation.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -0,0 +1,1340 @@
+(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+    License: BSD
+*)
+
+section \<open>Conditional Expectation\<close>
+
+theory Conditional_Expectation
+imports Probability_Measure
+begin
+
+subsection {*Restricting a measure to a sub-sigma-algebra*}
+
+definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+  "subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))"
+
+lemma sub_measure_space:
+  assumes i: "subalgebra M F"
+  shows "measure_space (space M) (sets F) (emeasure M)"
+proof -
+  have "sigma_algebra (space M) (sets F)"
+    by (metis i measure_space measure_space_def subalgebra_def)
+  moreover have "positive (sets F) (emeasure M)"
+    using Sigma_Algebra.positive_def by auto
+  moreover have "countably_additive (sets F) (emeasure M)"
+    by (meson countably_additive_def emeasure_countably_additive i order_trans subalgebra_def subsetCE)
+  ultimately show ?thesis unfolding measure_space_def by simp
+qed
+
+definition restr_to_subalg::"'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
+  "restr_to_subalg M F = measure_of (space M) (sets F) (emeasure M)"
+
+lemma space_restr_to_subalg:
+  "space (restr_to_subalg M F) = space M"
+unfolding restr_to_subalg_def by (simp add: space_measure_of_conv)
+
+lemma sets_restr_to_subalg [measurable_cong]:
+  assumes "subalgebra M F"
+  shows "sets (restr_to_subalg M F) = sets F"
+unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def)
+
+lemma emeasure_restr_to_subalg:
+  assumes "subalgebra M F"
+          "A \<in> sets F"
+  shows "emeasure (restr_to_subalg M F) A = emeasure M A"
+unfolding restr_to_subalg_def
+by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq)
+
+lemma null_sets_restr_to_subalg:
+  assumes "subalgebra M F"
+  shows "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F"
+proof
+  have "x \<in> null_sets M \<inter> sets F" if "x \<in> null_sets (restr_to_subalg M F)" for x
+    by (metis that Int_iff assms emeasure_restr_to_subalg null_setsD1 null_setsD2 null_setsI
+        sets_restr_to_subalg subalgebra_def subsetD)
+  then show "null_sets (restr_to_subalg M F) \<subseteq> null_sets M \<inter> sets F" by auto
+next
+  have "x \<in> null_sets (restr_to_subalg M F)" if "x \<in> null_sets M \<inter> sets F" for x
+    by (metis that Int_iff assms null_setsD1 null_setsI sets_restr_to_subalg emeasure_restr_to_subalg[OF assms])
+  then show "null_sets M \<inter> sets F \<subseteq> null_sets (restr_to_subalg M F)" by auto
+qed
+
+lemma AE_restr_to_subalg:
+  assumes "subalgebra M F"
+          "AE x in (restr_to_subalg M F). P x"
+  shows "AE x in M. P x"
+proof -
+  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)"
+    using AE_E3[OF assms(2)] by auto
+  then have "A \<in> null_sets M" using null_sets_restr_to_subalg[OF assms(1)] by auto
+  moreover have "\<And>x. x \<in> space M - A \<Longrightarrow> P x"
+    using space_restr_to_subalg A(1) by fastforce
+  ultimately show ?thesis
+    unfolding eventually_ae_filter by auto
+qed
+
+lemma AE_restr_to_subalg2:
+  assumes "subalgebra M F"
+          "AE x in M. P x" and [measurable]: "P \<in> measurable F (count_space UNIV)"
+  shows "AE x in (restr_to_subalg M F). P x"
+proof -
+  define U where "U = {x \<in> space M. \<not>(P x)}"
+  then have *: "U = {x \<in> space F. \<not>(P x)}" using assms(1) by (simp add: subalgebra_def)
+  then have "U \<in> sets F" by simp
+  then have "U \<in> sets M" using assms(1) by (meson subalgebra_def subsetD)
+  then have "U \<in> null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast
+  then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] `U \<in> sets F` by auto
+  then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg)
+qed
+
+lemma prob_space_restr_to_subalg:
+  assumes "subalgebra M F"
+          "prob_space M"
+  shows "prob_space (restr_to_subalg M F)"
+by (metis (no_types, lifting) assms(1) assms(2) emeasure_restr_to_subalg prob_space.emeasure_space_1 prob_spaceI
+    sets.top space_restr_to_subalg subalgebra_def)
+
+lemma finite_measure_restr_to_subalg:
+  assumes "subalgebra M F"
+          "finite_measure M"
+  shows "finite_measure (restr_to_subalg M F)"
+by (metis (no_types, lifting) assms emeasure_restr_to_subalg finite_measure.finite_emeasure_space
+    finite_measureI sets.top space_restr_to_subalg subalgebra_def infinity_ennreal_def)
+
+lemma measurable_in_subalg:
+  assumes "subalgebra M F"
+          "f \<in> measurable F N"
+  shows "f \<in> measurable (restr_to_subalg M F) N"
+by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
+
+lemma measurable_in_subalg':
+  assumes "subalgebra M F"
+          "f \<in> measurable (restr_to_subalg M F) N"
+  shows "f \<in> measurable F N"
+by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
+
+lemma measurable_from_subalg:
+  assumes "subalgebra M F"
+          "f \<in> measurable F N"
+  shows "f \<in> measurable M N"
+using assms unfolding measurable_def subalgebra_def by auto
+
+text{*The following is the direct transposition of \verb+nn_integral_subalgebra+
+(from \verb+Nonnegative_Lebesgue_Integration+) in the
+current notations, with the removal of the useless assumption $f \geq 0$.*}
+
+lemma nn_integral_subalgebra2:
+  assumes "subalgebra M F" and [measurable]: "f \<in> borel_measurable F"
+  shows "(\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. f x \<partial>M)"
+proof (rule nn_integral_subalgebra)
+  show "f \<in> borel_measurable (restr_to_subalg M F)"
+    by (rule measurable_in_subalg[OF assms(1)]) simp
+  show "sets (restr_to_subalg M F) \<subseteq> sets M" by (metis sets_restr_to_subalg[OF assms(1)] assms(1) subalgebra_def)
+  fix A assume "A \<in> sets (restr_to_subalg M F)"
+  then show "emeasure (restr_to_subalg M F) A = emeasure M A"
+    by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)])
+qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
+
+text{*The following is the direct transposition of \verb+integral_subalgebra+
+(from \verb+Bochner_Integration+) in the current notations.*}
+
+lemma integral_subalgebra2:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "subalgebra M F" and
+    [measurable]: "f \<in> borel_measurable F"
+  shows "(\<integral>x. f x \<partial>(restr_to_subalg M F)) = (\<integral>x. f x \<partial>M)"
+by (rule integral_subalgebra,
+    metis measurable_in_subalg[OF assms(1)] assms(2),
+    auto simp add: assms space_restr_to_subalg sets_restr_to_subalg emeasure_restr_to_subalg,
+    meson assms(1) subalgebra_def subset_eq)
+
+lemma integrable_from_subalg:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes "subalgebra M F"
+          "integrable (restr_to_subalg M F) f"
+  shows "integrable M f"
+proof (rule integrableI_bounded)
+  have [measurable]: "f \<in> borel_measurable F" using assms by auto
+  then show "f \<in> borel_measurable M" using assms(1) measurable_from_subalg by blast
+
+  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F))"
+    by (rule nn_integral_subalgebra2[symmetric], auto simp add: assms)
+  also have "... < \<infinity>" using integrable_iff_bounded assms by auto
+  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by simp
+qed
+
+lemma integrable_in_subalg:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes [measurable]: "subalgebra M F"
+          "f \<in> borel_measurable F"
+          "integrable M f"
+  shows "integrable (restr_to_subalg M F) f"
+proof (rule integrableI_bounded)
+  show "f \<in> borel_measurable (restr_to_subalg M F)" using assms(2) assms(1) by auto
+  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
+    by (rule nn_integral_subalgebra2, auto simp add: assms)
+  also have "... < \<infinity>" using integrable_iff_bounded assms by auto
+  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) < \<infinity>" by simp
+qed
+
+subsection {*Nonnegative conditional expectation*}
+
+text {* The conditional expectation of a function $f$, on a measure space $M$, with respect to a
+sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any
+$F$-set coincides with the integral of $f$.
+Such a function is uniquely defined almost everywhere.
+The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$,
+and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$.
+Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable
+functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$
+machinery, and works for all positive functions.
+
+In this paragraph, we develop the definition and basic properties for nonnegative functions,
+as the basics of the general case. As in the definition of integrals, the nonnegative case is done
+with ennreal-valued functions, without any integrability assumption.
+*}
+
+definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
+where
+  "nn_cond_exp M F f =
+    (if f \<in> borel_measurable M \<and> subalgebra M F
+        then RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M f) F)
+        else (\<lambda>_. 0))"
+
+lemma
+  shows borel_measurable_nn_cond_exp [measurable]: "nn_cond_exp M F f \<in> borel_measurable F"
+  and borel_measurable_nn_cond_exp2 [measurable]: "nn_cond_exp M F f \<in> borel_measurable M"
+by (simp_all add: nn_cond_exp_def)
+  (metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def)
+
+text {* The good setting for conditional expectations is the situation where the subalgebra $F$
+gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
+think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
+conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
+This means that a positive integrable function can have no meaningful conditional expectation.*}
+
+locale sigma_finite_subalgebra =
+  fixes M F::"'a measure"
+  assumes subalg: "subalgebra M F"
+      and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
+
+lemma sigma_finite_subalgebra_is_sigma_finite:
+  assumes "sigma_finite_subalgebra M F"
+  shows "sigma_finite_measure M"
+proof
+  have subalg: "subalgebra M F"
+   and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
+    using assms unfolding sigma_finite_subalgebra_def by auto
+  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>)"
+    using sigma_finite_measure.sigma_finite_countable[OF sigma_fin_subalg] by fastforce
+  have "A \<subseteq> sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce
+  then have "A \<subseteq> sets M" using subalg subalgebra_def by force
+  moreover have "\<Union>A = space M" using Ap space_restr_to_subalg by simp
+  moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] `A \<subseteq> sets F` Ap)
+  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
+qed
+
+sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure
+using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
+
+text {* Conditional expectations are very often used in probability spaces. This is a special case
+of the previous one, as we prove now. *}
+
+locale finite_measure_subalgebra = finite_measure +
+  fixes F::"'a measure"
+  assumes subalg: "subalgebra M F"
+
+lemma finite_measure_subalgebra_is_sigma_finite:
+  assumes "finite_measure_subalgebra M F"
+  shows "sigma_finite_subalgebra M F"
+proof -
+  interpret finite_measure_subalgebra M F using assms by simp
+  have "finite_measure (restr_to_subalg M F)"
+    using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
+  then have "sigma_finite_measure (restr_to_subalg M F)"
+    unfolding finite_measure_def by simp
+  then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
+qed
+
+sublocale finite_measure_subalgebra \<subseteq> sigma_finite_subalgebra
+proof -
+  have "finite_measure (restr_to_subalg M F)"
+    using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
+  then have "sigma_finite_measure (restr_to_subalg M F)"
+    unfolding finite_measure_def by simp
+  then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
+qed
+
+context sigma_finite_subalgebra
+begin
+
+text{* The next lemma is arguably the most fundamental property of conditional expectation:
+when computing an expectation against an $F$-measurable function, it is equivalent to work
+with a function or with its $F$-conditional expectation.
+
+This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
+From this point on, we will only work with it, and forget completely about
+the definition using Radon-Nikodym derivatives.
+*}
+
+lemma nn_cond_exp_intg:
+  assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
+  shows "(\<integral>\<^sup>+ x. f x * nn_cond_exp M F g x \<partial>M) = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
+proof -
+  have [measurable]: "f \<in> borel_measurable M"
+    by (meson assms subalg borel_measurable_subalgebra subalgebra_def)
+  have ac: "absolutely_continuous (restr_to_subalg M F) (restr_to_subalg (density M g) F)"
+    unfolding absolutely_continuous_def
+  proof -
+    have "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F" by (rule null_sets_restr_to_subalg[OF subalg])
+    moreover have "null_sets M \<subseteq> null_sets (density M g)"
+      by (rule absolutely_continuousI_density[unfolded absolutely_continuous_def]) auto
+    ultimately have "null_sets (restr_to_subalg M F) \<subseteq> null_sets (density M g) \<inter> sets F" by auto
+    moreover have "null_sets (density M g) \<inter> sets F = null_sets (restr_to_subalg (density M g) F)"
+      by (rule null_sets_restr_to_subalg[symmetric]) (metis subalg sets_density space_density subalgebra_def)
+    ultimately show "null_sets (restr_to_subalg M F) \<subseteq> null_sets (restr_to_subalg (density M g) F)" by auto
+  qed
+
+  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))"
+    by (rule nn_integral_subalgebra2[symmetric]) (simp_all add: assms subalg)
+  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))"
+    unfolding nn_cond_exp_def using assms subalg by simp
+  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))"
+    by (simp add: mult.commute)
+  also have "... = (\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg (density M g) F))"
+  proof (rule sigma_finite_measure.RN_deriv_nn_integral[symmetric])
+    show "sets (restr_to_subalg (density M g) F) = sets (restr_to_subalg M F)"
+      by (metis subalg restr_to_subalg_def sets.sets_measure_of_eq space_density subalgebra_def)
+  qed (auto simp add: assms measurable_restrict ac measurable_in_subalg subalg sigma_fin_subalg)
+  also have "... = (\<integral>\<^sup>+ x. f x \<partial>(density M g))"
+    by (metis nn_integral_subalgebra2 subalg assms(1) sets_density space_density subalgebra_def)
+  also have "... = (\<integral>\<^sup>+ x. g x * f x \<partial>M)"
+    by (rule nn_integral_density) (simp_all add: assms)
+  also have "... = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
+    by (simp add: mult.commute)
+  finally show ?thesis by simp
+qed
+
+lemma nn_cond_exp_charact:
+  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
+          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable F"
+  shows "AE x in M. g x = nn_cond_exp M F f x"
+proof -
+  let ?MF = "restr_to_subalg M F"
+  {
+    fix A assume "A \<in> sets ?MF"
+    then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
+    have "(\<integral>\<^sup>+ x \<in> A. g x \<partial> ?MF) = (\<integral>\<^sup>+ x \<in> A. g x \<partial>M)"
+      by (simp add: nn_integral_subalgebra2 subalg)
+    also have "... = (\<integral>\<^sup>+ x \<in> A. f x \<partial>M)" using assms(1) by simp
+    also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
+    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)
+    also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial> ?MF)"
+      by (simp add: nn_integral_subalgebra2 subalg)
+    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
+  } note * = this
+  have "AE x in ?MF. g x = nn_cond_exp M F f x"
+    by (rule sigma_finite_measure.density_unique2)
+       (auto simp add: assms subalg sigma_fin_subalg AE_restr_to_subalg2 *)
+  then show ?thesis using AE_restr_to_subalg[OF subalg] by simp
+qed
+
+lemma nn_cond_exp_F_meas:
+  assumes "f \<in> borel_measurable F"
+  shows "AE x in M. f x = nn_cond_exp M F f x"
+by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg])
+
+lemma nn_cond_exp_prod:
+  assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
+  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"
+proof (rule nn_cond_exp_charact)
+  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(1)])
+  show "(\<lambda>x. f x * g x) \<in> borel_measurable M" by measurable
+
+  fix A assume "A \<in> sets F"
+  then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
+  have "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
+    by (simp add: mult.commute mult.left_commute)
+  also have "... = \<integral>\<^sup>+x. (f x * indicator A x) * nn_cond_exp M F g x \<partial>M"
+    by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
+  also have "... = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M"
+    by (simp add: mult.commute mult.left_commute)
+  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
+qed (auto simp add: assms)
+
+lemma nn_cond_exp_sum:
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  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"
+proof (rule nn_cond_exp_charact)
+  fix A assume [measurable]: "A \<in> sets F"
+  then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
+  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)"
+    by (rule nn_set_integral_add) (auto simp add: assms `A \<in> sets M`)
+  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)"
+    by (metis (no_types, lifting) mult.commute nn_integral_cong)
+  also have "... = (\<integral>\<^sup>+x. indicator A x * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * g x \<partial>M)"
+    by (simp add: nn_cond_exp_intg)
+  also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
+    by (metis (no_types, lifting) mult.commute nn_integral_cong)
+  also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
+    by (rule nn_set_integral_add[symmetric]) (auto simp add: assms `A \<in> sets M`)
+  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"
+    by simp
+qed (auto simp add: assms)
+
+lemma nn_cond_exp_cong:
+  assumes "AE x in M. f x = g x"
+      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x"
+proof (rule nn_cond_exp_charact)
+  fix A assume [measurable]: "A \<in> sets F"
+  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"
+    by (simp add: mult.commute)
+  also have "... = \<integral>\<^sup>+x. indicator A x * f x \<partial>M" by (simp add: nn_cond_exp_intg assms)
+  also have "... = \<integral>\<^sup>+x\<in>A. f x \<partial>M" by (simp add: mult.commute)
+  also have "... = \<integral>\<^sup>+x\<in>A. g x \<partial>M" by (rule nn_set_integral_cong[OF assms(1)])
+  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
+qed (auto simp add: assms)
+
+lemma nn_cond_exp_mono:
+  assumes "AE x in M. f x \<le> g x"
+      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows "AE x in M. nn_cond_exp M F f x \<le> nn_cond_exp M F g x"
+proof -
+  define h where "h = (\<lambda>x. g x - f x)"
+  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
+  have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add)
+  have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F (\<lambda>x. f x + h x) x"
+    by (rule nn_cond_exp_cong) (auto simp add: * assms)
+  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"
+    by (rule nn_cond_exp_sum) (auto simp add: assms)
+  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
+  then show ?thesis by force
+qed
+
+lemma nested_subalg_is_sigma_finite:
+  assumes "subalgebra M G" "subalgebra G F"
+  shows "sigma_finite_subalgebra M G"
+unfolding sigma_finite_subalgebra_def
+proof (auto simp add: assms)
+  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>)"
+    using sigma_fin_subalg sigma_finite_measure_def by auto
+  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>)"
+    by auto
+  have "sets F \<subseteq> sets M"
+    by (meson assms order_trans subalgebra_def)
+  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>)"
+    by (metis (no_types) A assms basic_trans_rules(31) emeasure_restr_to_subalg order_trans sets_restr_to_subalg subalgebra_def)
+  then show "sigma_finite_measure (restr_to_subalg M G)"
+    by (metis sigma_finite_measure.intro space_restr_to_subalg)
+qed
+
+lemma nn_cond_exp_nested_subalg:
+  assumes "subalgebra M G" "subalgebra G F"
+    and [measurable]: "f \<in> borel_measurable M"
+  shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F (nn_cond_exp M G f) x"
+proof (rule nn_cond_exp_charact, auto)
+  interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
+  fix A assume [measurable]: "A \<in> sets F"
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+
+  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)"
+    by (metis (no_types) mult.commute)
+  also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (rule G.nn_cond_exp_intg, auto simp add: assms)
+  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)
+  also have "... = set_nn_integral M A (nn_cond_exp M F f)" by (metis (no_types) mult.commute)
+  finally show "set_nn_integral M A (nn_cond_exp M G f) = set_nn_integral M A (nn_cond_exp M F f)".
+qed
+
+end
+
+subsection {*Real conditional expectation*}
+
+text {*Once conditional expectations of positive functions are defined, the definition for real-valued functions
+follows readily, by taking the difference of positive and negative parts.
+One could also define a conditional expectation of vector-space valued functions, as in
+\verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I
+concentrate on it. (It is also essential for the case of the most general Pettis integral.)
+*}
+
+definition real_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where
+  "real_cond_exp M F f =
+    (\<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))"
+
+lemma
+  shows borel_measurable_cond_exp [measurable]: "real_cond_exp M F f \<in> borel_measurable F"
+  and borel_measurable_cond_exp2 [measurable]: "real_cond_exp M F f \<in> borel_measurable M"
+unfolding real_cond_exp_def by auto
+
+context sigma_finite_subalgebra
+begin
+
+lemma real_cond_exp_abs:
+  assumes [measurable]: "f \<in> borel_measurable M"
+  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"
+proof -
+  define fp where "fp = (\<lambda>x. ennreal (f x))"
+  define fm where "fm = (\<lambda>x. ennreal (- f x))"
+  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M" unfolding fp_def fm_def by auto
+  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)
+
+  {
+    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"
+    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>"
+      unfolding real_cond_exp_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg)
+    from ennreal_leI[OF this]
+    have "abs(real_cond_exp M F f x) \<le> nn_cond_exp M F fp x + nn_cond_exp M F fm x"
+      by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique)
+    also have "... = nn_cond_exp M F (\<lambda>x. fp x + fm x) x" using H by simp
+    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
+  }
+  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"
+    by (rule nn_cond_exp_sum) (auto simp add: fp_def fm_def)
+  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"
+    by auto
+  then show ?thesis using eq by simp
+qed
+
+text{* The next lemma shows that the conditional expectation
+is an $F$-measurable function whose average against an $F$-measurable
+function $f$ coincides with the average of the original function against $f$.
+It is obtained as a consequence of the same property for the positive conditional
+expectation, taking the difference of the positive and the negative part. The proof
+is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in
+the subsequent lemma. The idea of the proof is essentially trivial, but the implementation
+is slightly tedious as one should check all the integrability properties of the different parts, and go
+back and forth between positive integral and signed integrals, and between real-valued
+functions and ennreal-valued functions.
+
+Once this lemma is available, we will use it to characterize the conditional expectation,
+and never come back to the original technical definition, as we did in the case of the
+nonnegative conditional expectation.
+*}
+
+lemma real_cond_exp_intg_fpos:
+  assumes "integrable M (\<lambda>x. f x * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
+          [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
+  shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
+        "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)"
+proof -
+  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(3)])
+  define gp where "gp = (\<lambda>x. ennreal (g x))"
+  define gm where "gm = (\<lambda>x. ennreal (- g x))"
+  have [measurable]: "gp \<in> borel_measurable M" "gm \<in> borel_measurable M" unfolding gp_def gm_def by auto
+  define h where "h = (\<lambda>x. ennreal(abs(g x)))"
+  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)
+  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
+  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
+  have gp_real: "\<And>x. enn2real(gp x) = max (g x) 0"
+    unfolding gp_def by (simp add: max_def ennreal_neg)
+  have gm_real: "\<And>x. enn2real(gm x) = max (-g x) 0"
+    unfolding gm_def by (simp add: max_def ennreal_neg)
+
+  have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
+    by (simp add: nn_integral_mono)
+  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
+  finally have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) < \<infinity>" by simp
+  then have int1: "integrable M (\<lambda>x. f x * max (g x) 0)" by (simp add: integrableI_bounded)
+
+  have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
+    by (simp add: nn_integral_mono)
+  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
+  finally have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) < \<infinity>" by simp
+  then have int2: "integrable M (\<lambda>x. f x * max (-g x) 0)" by (simp add: integrableI_bounded)
+
+  have "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) = (\<integral>\<^sup>+x. f x * h x \<partial>M)"
+    by (rule nn_cond_exp_intg) auto
+  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (f x * max (g x) 0 + f x * max (- g x) 0) \<partial>M"
+    unfolding h_def
+    by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
+  also have "... < \<infinity>"
+    using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top)
+  finally have *: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) < \<infinity>" by simp
+
+  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)"
+    by (simp add: abs_mult)
+  also have "... \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M)"
+  proof (rule nn_integral_mono_AE)
+    {
+      fix x assume *: "abs(real_cond_exp M F g x) \<le> nn_cond_exp M F h x"
+      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>)"
+        by (simp add: ennreal_mult)
+      also have "... \<le> f x * nn_cond_exp M F h x"
+        using * by (auto intro!: mult_left_mono)
+      finally have "ennreal (f x * \<bar>real_cond_exp M F g x\<bar>) \<le> f x * nn_cond_exp M F h x"
+        by simp
+    }
+    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"
+      using real_cond_exp_abs[OF assms(4)] h_def by auto
+  qed
+  finally have **: "(\<integral>\<^sup>+x. norm(f x * real_cond_exp M F g x) \<partial>M) < \<infinity>" using * by auto
+  show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
+    using ** by (intro integrableI_bounded) auto
+
+
+  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)"
+  proof (rule nn_integral_mono_AE)
+    have "AE x in M. nn_cond_exp M F gp x \<le> nn_cond_exp M F h x"
+      by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
+    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"
+      by (auto simp: mult_left_mono)
+  qed
+  then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gp x \<partial>M) < \<infinity>"
+    using * by auto
+  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
+    by (auto simp add: ennreal_mult intro!: mult_left_mono)
+       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
+  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)"
+    by (simp add: nn_integral_mono)
+  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gp x)) \<partial>M) < \<infinity>" using a by auto
+  then have gp_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gp x))" by (simp add: integrableI_bounded)
+  have gp_fin: "AE x in M. f x * nn_cond_exp M F gp x \<noteq> \<infinity>"
+    apply (rule nn_integral_PInf_AE) using a by auto
+
+  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)"
+    by (rule integral_eq_nn_integral) auto
+  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)"
+  proof -
+    {
+      fix x assume "f x * nn_cond_exp M F gp x \<noteq> \<infinity>"
+      then have "ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x"
+        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
+    }
+    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"
+      using gp_fin by auto
+    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)"
+      by (rule nn_integral_cong_AE)
+    also have "... = (\<integral>\<^sup>+ x. f x * gp x \<partial>M)"
+      by (rule nn_cond_exp_intg) (auto simp add: gp_def)
+    also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)"
+      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
+    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
+    then show ?thesis by simp
+  qed
+  also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M)"
+    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
+  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
+
+
+  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)"
+  proof (rule nn_integral_mono_AE)
+    have "AE x in M. nn_cond_exp M F gm x \<le> nn_cond_exp M F h x"
+      by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
+    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"
+      by (auto simp: mult_left_mono)
+  qed
+  then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gm x \<partial>M) < \<infinity>"
+    using * by auto
+  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"
+    by (auto simp add: ennreal_mult intro!: mult_left_mono)
+       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
+  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)"
+    by (simp add: nn_integral_mono)
+  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gm x)) \<partial>M) < \<infinity>" using a by auto
+  then have gm_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gm x))" by (simp add: integrableI_bounded)
+  have gm_fin: "AE x in M. f x * nn_cond_exp M F gm x \<noteq> \<infinity>"
+    apply (rule nn_integral_PInf_AE) using a by auto
+
+  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)"
+    by (rule integral_eq_nn_integral) auto
+  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)"
+  proof -
+    {
+      fix x assume "f x * nn_cond_exp M F gm x \<noteq> \<infinity>"
+      then have "ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x"
+        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
+    }
+    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"
+      using gm_fin by auto
+    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)"
+      by (rule nn_integral_cong_AE)
+    also have "... = (\<integral>\<^sup>+ x. f x * gm x \<partial>M)"
+      by (rule nn_cond_exp_intg) (auto simp add: gm_def)
+    also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)"
+      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
+    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
+    then show ?thesis by simp
+  qed
+  also have "... = (\<integral> x. f x * enn2real(gm x) \<partial>M)"
+    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
+  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
+
+
+  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)"
+    unfolding real_cond_exp_def gp_def gm_def by (simp add: right_diff_distrib)
+  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)"
+    by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
+  also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M) - (\<integral> x. f x * enn2real(gm x) \<partial>M)"
+    using gp_expr gm_expr by simp
+  also have "... = (\<integral> x. f x * max (g x) 0 \<partial>M) - (\<integral> x. f x * max (-g x) 0 \<partial>M)"
+    using gp_real gm_real by simp
+  also have "... = (\<integral> x. f x * max (g x) 0 - f x * max (-g x) 0 \<partial>M)"
+    by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
+  also have "... = (\<integral>x. f x * g x \<partial>M)"
+    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)
+  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
+qed
+
+lemma real_cond_exp_intg:
+  assumes "integrable M (\<lambda>x. f x * g x)" and
+          [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
+  shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
+        "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)"
+proof -
+  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(2)])
+  define fp where "fp = (\<lambda>x. max (f x) 0)"
+  define fm where "fm = (\<lambda>x. max (-f x) 0)"
+  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M"
+    unfolding fp_def fm_def by simp_all
+  have [measurable]: "fp \<in> borel_measurable F" "fm \<in> borel_measurable F"
+    unfolding fp_def fm_def by simp_all
+
+  have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
+    by (simp add: fp_def nn_integral_mono)
+  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
+  finally have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) < \<infinity>" by simp
+  then have intp: "integrable M (\<lambda>x. fp x * g x)" by (simp add: integrableI_bounded)
+  moreover have "\<And>x. fp x \<ge> 0" unfolding fp_def by simp
+  ultimately have Rp: "integrable M (\<lambda>x. fp x * real_cond_exp M F g x)"
+    "(\<integral> x. fp x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fp x * g x \<partial>M)"
+  using real_cond_exp_intg_fpos by auto
+
+  have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
+    by (simp add: fm_def nn_integral_mono)
+  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
+  finally have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) < \<infinity>" by simp
+  then have intm: "integrable M (\<lambda>x. fm x * g x)" by (simp add: integrableI_bounded)
+  moreover have "\<And>x. fm x \<ge> 0" unfolding fm_def by simp
+  ultimately have Rm: "integrable M (\<lambda>x. fm x * real_cond_exp M F g x)"
+    "(\<integral> x. fm x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fm x * g x \<partial>M)"
+  using real_cond_exp_intg_fpos by auto
+
+  have "integrable M (\<lambda>x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x)"
+    using Rp(1) Rm(1) integrable_diff by simp
+  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"
+    unfolding fp_def fm_def by (simp add: max_def)
+  ultimately show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
+    by simp
+
+  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)"
+    using * by simp
+  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)"
+    using Rp(1) Rm(1) by simp
+  also have "... = (\<integral> x. fp x * g x \<partial>M) - (\<integral> x. fm x * g x \<partial>M)"
+    using Rp(2) Rm(2) by simp
+  also have "... = (\<integral> x. fp x * g x - fm x * g x \<partial>M)"
+    using intm intp by simp
+  also have "... = (\<integral> x. f x * g x \<partial>M)"
+    unfolding fp_def fm_def by (metis (no_types, hide_lams) diff_0 diff_zero max.commute
+    max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
+  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
+qed
+
+lemma real_cond_exp_intA:
+  assumes [measurable]: "integrable M f" "A \<in> sets F"
+  shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)"
+proof -
+  have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
+  have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
+qed
+
+lemma real_cond_exp_int [intro]:
+  assumes "integrable M f"
+  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)"
+using real_cond_exp_intg[where ?f = "\<lambda>x. 1" and ?g = f] assms by auto
+
+lemma real_cond_exp_charact:
+  assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)"
+      and [measurable]: "integrable M f" "integrable M g"
+          "g \<in> borel_measurable F"
+  shows "AE x in M. real_cond_exp M F f x = g x"
+proof -
+  let ?MF = "restr_to_subalg M F"
+  have "AE x in ?MF. real_cond_exp M F f x = g x"
+  proof (rule AE_symmetric[OF density_unique_real])
+    fix A assume "A \<in> sets ?MF"
+    then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
+    then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
+    have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)"
+      by (simp add: integral_subalgebra2 subalg)
+    also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp
+    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)"
+      apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
+    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
+    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)"
+      by (simp add: integral_subalgebra2 subalg)
+    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
+  next
+    have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
+    then show "integrable ?MF (real_cond_exp M F f)" by (metis borel_measurable_cond_exp integrable_in_subalg[OF subalg])
+    show "integrable (restr_to_subalg M F) g" by (simp add: assms(3) integrable_in_subalg[OF subalg])
+  qed
+  then show ?thesis using AE_restr_to_subalg[OF subalg] by auto
+qed
+
+lemma real_cond_exp_F_meas [intro, simp]:
+  assumes "integrable M f"
+          "f \<in> borel_measurable F"
+  shows "AE x in M. real_cond_exp M F f x = f x"
+by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg])
+
+lemma real_cond_exp_mult:
+  assumes [measurable]:"f \<in> borel_measurable F" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f x * g x)"
+  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"
+proof (rule real_cond_exp_charact)
+  fix A assume "A \<in> sets F"
+  then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
+  have [measurable]: "A \<in> sets M" using subalg by (meson `A \<in> sets F` subalgebra_def subsetD)
+  have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
+    by (simp add: mult.commute mult.left_commute)
+  also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
+    apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
+    using integrable_mult_indicator[OF `A \<in> sets M` assms(3)] by (simp add: mult.commute mult.left_commute)
+  also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
+    by (simp add: mult.commute mult.left_commute)
+  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
+qed (auto simp add: real_cond_exp_intg(1) assms)
+
+lemma real_cond_exp_add [intro]:
+  assumes [measurable]: "integrable M f" "integrable M g"
+  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"
+proof (rule real_cond_exp_charact)
+  have "integrable M (real_cond_exp M F f)" "integrable M (real_cond_exp M F g)"
+    using real_cond_exp_int(1) assms by auto
+  then show "integrable M (\<lambda>x. real_cond_exp M F f x + real_cond_exp M F g x)"
+    by auto
+
+  fix A assume [measurable]: "A \<in> sets F"
+  then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
+  have intAf: "integrable M (\<lambda>x. indicator A x * f x)"
+    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+  have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
+    using integrable_mult_indicator[OF `A \<in> sets M` assms(2)] by auto
+
+  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)"
+    apply (rule set_integral_add, auto simp add: assms)
+    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]]
+          integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(2)]] by simp_all
+  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)"
+    by auto
+  also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
+    using real_cond_exp_intg(2) assms `A \<in> sets F` intAf intAg by auto
+  also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
+    by auto
+  also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
+    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms `A \<in> sets M` intAf intAg)
+  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"
+    by simp
+qed (auto simp add: assms)
+
+lemma real_cond_exp_cong:
+  assumes ae: "AE x in M. f x = g x" and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  shows "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
+proof -
+  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"
+    apply (rule nn_cond_exp_cong) using assms by auto
+  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"
+    apply (rule nn_cond_exp_cong) using assms by auto
+  ultimately show "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
+    unfolding real_cond_exp_def by auto
+qed
+
+lemma real_cond_exp_cmult [intro, simp]:
+  fixes c::real
+  assumes "integrable M f"
+  shows "AE x in M. real_cond_exp M F (\<lambda>x. c * f x) x = c * real_cond_exp M F f x"
+by (rule real_cond_exp_mult[where ?f = "\<lambda>x. c" and ?g = f], auto simp add: assms borel_measurable_integrable)
+
+lemma real_cond_exp_cdiv [intro, simp]:
+  fixes c::real
+  assumes "integrable M f"
+  shows "AE x in M. real_cond_exp M F (\<lambda>x. f x / c) x = real_cond_exp M F f x / c"
+using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps)
+
+lemma real_cond_exp_diff [intro, simp]:
+  assumes [measurable]: "integrable M f" "integrable M g"
+  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"
+proof -
+  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"
+    using real_cond_exp_add[where ?f = f and ?g = "\<lambda>x. - g x"] assms by auto
+  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -g x) x = - real_cond_exp M F g x"
+    using real_cond_exp_cmult[where ?f = g and ?c = "-1"] assms(2) by auto
+  ultimately show ?thesis by auto
+qed
+
+lemma real_cond_exp_pos [intro]:
+  assumes "AE x in M. f x \<ge> 0" and [measurable]: "f \<in> borel_measurable M"
+  shows "AE x in M. real_cond_exp M F f x \<ge> 0"
+proof -
+  define g where "g = (\<lambda>x. max (f x) 0)"
+  have "AE x in M. f x = g x" using assms g_def by auto
+  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
+
+  have "\<And>x. g x \<ge> 0" unfolding g_def by simp
+  then have "(\<lambda>x. ennreal(-g x)) = (\<lambda>x. 0)"
+    by (simp add: ennreal_neg)
+  moreover have "AE x in M. 0 = nn_cond_exp M F (\<lambda>x. 0) x"
+    by (rule nn_cond_exp_F_meas, auto)
+  ultimately have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal(-g x)) x = 0"
+    by simp
+  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)"
+    unfolding real_cond_exp_def by auto
+  then have "AE x in M. real_cond_exp M F g x \<ge> 0" by auto
+  then show ?thesis using * by auto
+qed
+
+lemma real_cond_exp_mono:
+  assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g"
+  shows "AE x in M. real_cond_exp M F f x \<le> real_cond_exp M F g x"
+proof -
+  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"
+    by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
+  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x \<ge> 0"
+    by (rule real_cond_exp_pos, auto simp add: assms(1))
+  ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x \<ge> 0" by auto
+  then show ?thesis by auto
+qed
+
+lemma (in -) measurable_P_restriction [measurable (raw)]:
+  assumes [measurable]: "Measurable.pred M P" "A \<in> sets M"
+  shows "{x \<in> A. P x} \<in> sets M"
+proof -
+  have "A \<subseteq> space M" using sets.sets_into_space[OF assms(2)].
+  then have "{x \<in> A. P x} = A \<inter> {x \<in> space M. P x}" by blast
+  then show ?thesis by auto
+qed
+
+lemma real_cond_exp_gr_c:
+  assumes [measurable]: "integrable M f"
+      and "AE x in M. f x > c"
+  shows "AE x in M. real_cond_exp M F f x > c"
+proof -
+  define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}"
+  have [measurable]: "X \<in> sets F"
+    unfolding X_def apply measurable by (metis sets.top subalg subalgebra_def)
+  then have [measurable]: "X \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
+  have "emeasure M X = 0"
+  proof (rule ccontr)
+    assume "\<not>(emeasure M X) = 0"
+    have "emeasure (restr_to_subalg M F) X = emeasure M X"
+      by (simp add: emeasure_restr_to_subalg subalg)
+    then have "emeasure (restr_to_subalg M F) X > 0"
+      using `\<not>(emeasure M X) = 0` gr_zeroI by auto
+    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>"
+      using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans
+      not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
+    then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
+    then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
+    have Ic: "set_integrable M A (\<lambda>x. c)"
+      using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
+    have If: "set_integrable M A f"
+      by (rule integrable_mult_indicator, auto simp add: `integrable M f`)
+    have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
+    proof (rule antisym)
+      show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
+        apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
+      have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
+        by (rule real_cond_exp_intA, auto simp add: `integrable M f`)
+      also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
+        apply (rule set_integral_mono)
+        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF `integrable M f`])
+        using Ic X_def \<open>A \<subseteq> X\<close> by auto
+      finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
+    qed
+    have "AE x in M. indicator A x * c = indicator A x * f x"
+      apply (rule integral_ineq_eq_0_then_AE) using Ic If * apply auto
+      using assms(2) unfolding indicator_def by auto
+    then have "AE x\<in>A in M. c = f x" by auto
+    then have "AE x\<in>A in M. False" using assms(2) by auto
+    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>)
+    then show False using `emeasure (restr_to_subalg M F) A > 0`
+      by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
+  qed
+  then show ?thesis using AE_iff_null_sets[OF `X \<in> sets M`] unfolding X_def by auto
+qed
+
+lemma real_cond_exp_less_c:
+  assumes [measurable]: "integrable M f"
+      and "AE x in M. f x < c"
+  shows "AE x in M. real_cond_exp M F f x < c"
+proof -
+  have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
+    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
+  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x > -c"
+    apply (rule real_cond_exp_gr_c) using assms by auto
+  ultimately show ?thesis by auto
+qed
+
+lemma real_cond_exp_ge_c:
+  assumes [measurable]: "integrable M f"
+      and "AE x in M. f x \<ge> c"
+  shows "AE x in M. real_cond_exp M F f x \<ge> c"
+proof -
+  obtain u::"nat \<Rightarrow> real" where u: "\<And>n. u n < c" "u \<longlonglongrightarrow> c"
+    using approx_from_below_dense_linorder[of "c-1" c] by auto
+  have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat
+    apply (rule real_cond_exp_gr_c) using assms `u n < c` by auto
+  have "AE x in M. \<forall>n. real_cond_exp M F f x > u n"
+    by (subst AE_all_countable, auto simp add: *)
+  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
+  proof -
+    have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto
+    then show ?thesis using u(2) LIMSEQ_le_const2 by blast
+  qed
+  ultimately show ?thesis by auto
+qed
+
+lemma real_cond_exp_le_c:
+  assumes [measurable]: "integrable M f"
+      and "AE x in M. f x \<le> c"
+  shows "AE x in M. real_cond_exp M F f x \<le> c"
+proof -
+  have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
+    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
+  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x \<ge> -c"
+    apply (rule real_cond_exp_ge_c) using assms by auto
+  ultimately show ?thesis by auto
+qed
+
+lemma real_cond_exp_mono_strict:
+  assumes "AE x in M. f x < g x" and [measurable]: "integrable M f" "integrable M g"
+  shows "AE x in M. real_cond_exp M F f x < real_cond_exp M F g x"
+proof -
+  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"
+    by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
+  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x > 0"
+    by (rule real_cond_exp_gr_c, auto simp add: assms)
+  ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x > 0" by auto
+  then show ?thesis by auto
+qed
+
+lemma real_cond_exp_nested_subalg [intro, simp]:
+  assumes "subalgebra M G" "subalgebra G F"
+      and [measurable]: "integrable M f"
+  shows "AE x in M. real_cond_exp M F (real_cond_exp M G f) x = real_cond_exp M F f x"
+proof (rule real_cond_exp_charact)
+  interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
+  show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
+
+  fix A assume [measurable]: "A \<in> sets F"
+  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
+  have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
+    by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
+  also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
+    by (rule real_cond_exp_intA, auto simp add: assms(3))
+  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
+qed (auto simp add: assms real_cond_exp_int(1))
+
+lemma real_cond_exp_sum [intro, simp]:
+  fixes f::"'b \<Rightarrow> 'a \<Rightarrow> real"
+  assumes [measurable]: "\<And>i. integrable M (f i)"
+  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)"
+proof (rule real_cond_exp_charact)
+  fix A assume [measurable]: "A \<in> sets F"
+  then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
+  have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
+    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
+  have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
+    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]] by auto
+  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
+    by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
+
+  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)"
+    by (simp add: sum_distrib_left)
+  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))"
+    by (rule Bochner_Integration.integral_sum, simp add: *)
+  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))"
+    using inti by auto
+  also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)"
+    by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
+  also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)"
+    by (simp add: sum_distrib_left)
+  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
+qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
+
+text {*Jensen's inequality, describing the behavior of the integral under a convex function, admits
+a version for the conditional expectation, as follows.*}
+
+theorem real_cond_exp_jensens_inequality:
+  fixes q :: "real \<Rightarrow> real"
+  assumes X: "integrable M X" "AE x in M. X x \<in> I"
+  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
+  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel"
+  shows "AE x in M. real_cond_exp M F X x \<in> I"
+        "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
+proof -
+  have "open I" using I by auto
+  then have "interior I = I" by (simp add: interior_eq)
+  have [measurable]: "I \<in> sets borel" using I by auto
+  define phi where "phi = (\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I)))"
+  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)"
+        if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
+    unfolding phi_def apply (rule convex_le_Inf_differential)
+    using `convex_on I q` that `interior I = I` by auto
+  text {*It is not clear that the function $\phi$ is measurable. We replace it by a version which
+        is better behaved.*}
+  define psi where "psi = (\<lambda>x. phi x * indicator I x)"
+  have A: "psi y = phi y" if "y \<in> I" for y unfolding psi_def indicator_def using that by auto
+  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)"
+        if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
+    unfolding A[OF `real_cond_exp M F X x \<in> I`] using ** that by auto
+
+  note I
+  moreover have "AE x in M. real_cond_exp M F X x > a" if "I \<subseteq> {a <..}" for a
+    apply (rule real_cond_exp_gr_c) using X that by auto
+  moreover have "AE x in M. real_cond_exp M F X x < b" if "I \<subseteq> {..<b}" for b
+    apply (rule real_cond_exp_less_c) using X that by auto
+  ultimately show "AE x in M. real_cond_exp M F X x \<in> I"
+    by (elim disjE) (auto simp: subset_eq)
+  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)"
+    using * X(2) by auto
+
+  text {*Then, one wants to take the conditional expectation of this inequality. On the left, one gets
+         the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one
+         is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only
+         works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The
+         trick is to multiply by a $F$-measurable function which is small enough to make
+         everything integrable.*}
+
+  obtain f::"'a \<Rightarrow> real" where [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
+                               "integrable (restr_to_subalg M F) f"
+                           and f: "\<And>x. f x > 0" "\<And>x. f x \<le> 1"
+    using sigma_finite_measure.obtain_positive_integrable_function[OF sigma_fin_subalg] by metis
+  then have [measurable]: "f \<in> borel_measurable F" by (simp add: subalg)
+  then have [measurable]: "f \<in> borel_measurable M" using measurable_from_subalg[OF subalg] by blast
+  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>))"
+  define G where "G = (\<lambda>x. g x * psi (real_cond_exp M F X x))"
+  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)
+  have G: "\<bar>G x\<bar> \<le> 1" for x unfolding G_def g_def using f[of x]
+  proof (auto simp add: abs_mult)
+    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>"
+      apply (rule mult_mono) using f[of x] by auto
+    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
+    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>"
+      by simp
+  qed
+  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))"
+    using main_ineq g by (auto simp add: divide_simps)
+  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)"
+    unfolding G_def by (auto simp add: algebra_simps)
+
+  text {*To proceed, we need to know that $\psi$ is measurable.*}
+  have phi_mono: "phi x \<le> phi y" if "x \<le> y" "x \<in> I" "y \<in> I" for x y
+  proof (cases "x < y")
+    case True
+    have "q x + phi x * (y-x) \<le> q y"
+      unfolding phi_def apply (rule convex_le_Inf_differential) using `convex_on I q` that `interior I = I` by auto
+    then have "phi x \<le> (q x - q y) / (x - y)"
+      using that `x < y` by (auto simp add: divide_simps algebra_simps)
+    moreover have "(q x - q y)/(x - y) \<le> phi y"
+    unfolding phi_def proof (rule cInf_greatest, auto)
+      fix t assume "t \<in> I" "y < t"
+      have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
+        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
+      also have "... \<le> (q y - q t) / (y - t)"
+        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
+      finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
+    next
+      obtain e where "0 < e" "ball y e \<subseteq> I" using `open I` `y \<in> I` openE by blast
+      then have "y + e/2 \<in> {y<..} \<inter> I" by (auto simp: dist_real_def)
+      then show "{y<..} \<inter> I = {} \<Longrightarrow> False" by auto
+    qed
+    ultimately show "phi x \<le> phi y" by auto
+  next
+    case False
+    then have "x = y" using `x \<le> y` by auto
+    then show ?thesis by auto
+  qed
+  have [measurable]: "psi \<in> borel_measurable borel"
+    by (rule borel_measurable_piecewise_mono[of "{I, -I}"])
+       (auto simp add: psi_def indicator_def phi_mono intro: mono_onI)
+  have [measurable]: "q \<in> borel_measurable borel" using q by simp
+
+  have [measurable]: "X \<in> borel_measurable M"
+                     "real_cond_exp M F X \<in> borel_measurable F"
+                     "g \<in> borel_measurable F" "g \<in> borel_measurable M"
+                     "G \<in> borel_measurable F" "G \<in> borel_measurable M"
+    using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto
+  have int1: "integrable (restr_to_subalg M F) (\<lambda>x. g x * q (real_cond_exp M F X x))"
+    apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg `integrable (restr_to_subalg M F) f`)
+    unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps)
+  have int2: "integrable M (\<lambda>x. G x * (X x - real_cond_exp M F X x))"
+    apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>X x\<bar> + \<bar>real_cond_exp M F X x\<bar>"])
+    apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int `integrable M X` AE_I2)
+    using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le)
+  have int3: "integrable M (\<lambda>x. g x * q (X x))"
+    apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. q(X x)"], auto simp add: q(1) abs_mult)
+    using g by (simp add: less_imp_le mult_left_le_one_le)
+
+  text {*Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
+         the following.*}
+  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"
+    apply (rule real_cond_exp_mono[OF main_G])
+    apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]])
+    using int2 int3 by auto
+  text {*This reduces to the desired inequality thanks to the properties of conditional expectation,
+         i.e., the conditional expectation of an $F$-measurable function is this function, and one can
+         multiply an $F$-measurable function outside of conditional expectations.
+         Since all these equalities only hold almost everywhere, we formulate them separately,
+         and then combine all of them to simplify the above equation, again almost everywhere.*}
+  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"
+    by (rule real_cond_exp_mult, auto simp add: int3)
+  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
+      = 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"
+    by (rule real_cond_exp_add, auto simp add: integrable_from_subalg[OF subalg int1] int2)
+  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)"
+    by (rule real_cond_exp_F_meas, auto simp add: integrable_from_subalg[OF subalg int1])
+  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"
+    by (rule real_cond_exp_mult, auto simp add: int2)
+  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"
+    by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int `integrable M X`)
+  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 "
+    by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int `integrable M X`)
+  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)"
+    by auto
+  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)"
+    using g(1) by (auto simp add: divide_simps)
+qed
+
+text {*Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
+bound for it. Indeed, this is not true in general, as the following counterexample shows:
+
+on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
+for integer $n$. Let $q(x) = - \sqrt{x}$ for $x\geq 0$. Define $X$ which is equal to $1/n$ over
+$[n, n+1/n)$ and $2^{-n}$ on $[n+1/n, n+1)$. Then $X$ is integrable as $\sum 1/n^2 < \infty$, and
+$q(X)$ is integrable as $\sum 1/n^{3/2} < \infty$. On the other hand, $E(X|F)$ is essentially equal
+to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take
+its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not
+integrable.
+
+However, this counterexample is essentially the only situation where this function is not
+integrable, as shown by the next lemma.
+*}
+
+lemma integrable_convex_cond_exp:
+  fixes q :: "real \<Rightarrow> real"
+  assumes X: "integrable M X" "AE x in M. X x \<in> I"
+  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
+  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel"
+  assumes H: "emeasure M (space M) = \<infinity> \<Longrightarrow> 0 \<in> I"
+  shows "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
+proof -
+  have [measurable]: "(\<lambda>x. q (real_cond_exp M F X x)) \<in> borel_measurable M"
+                     "q \<in> borel_measurable borel"
+                     "X \<in> borel_measurable M"
+    using X(1) q(3) by auto
+  have "open I" using I by auto
+  then have "interior I = I" by (simp add: interior_eq)
+
+  consider "emeasure M (space M) = 0" | "emeasure M (space M) > 0 \<and> emeasure M (space M) < \<infinity>" | "emeasure M (space M) = \<infinity>"
+    by (metis infinity_ennreal_def not_gr_zero top.not_eq_extremum)
+  then show ?thesis
+  proof (cases)
+    case 1
+    show ?thesis by (subst integrable_cong_AE[of _ _ "\<lambda>x. 0"], auto intro: emeasure_0_AE[OF 1])
+  next
+    case 2
+    interpret finite_measure M using 2 by (auto intro!: finite_measureI)
+
+    have "I \<noteq> {}"
+      using `AE x in M. X x \<in> I` 2 eventually_mono integral_less_AE_space by fastforce
+    then obtain z where "z \<in> I" by auto
+
+    define A where "A = Inf ((\<lambda>t. (q z - q t) / (z - t)) ` ({z<..} \<inter> I))"
+    have "q y \<ge> q z + A * (y - z)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
+      using `z \<in> I` `y \<in> I` `interior I = I` q(2) by auto
+    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)"
+      using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
+    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"
+      using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
+    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
+      using that by auto
+    ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar>
+        \<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>"
+      by auto
+
+    show "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
+      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>"])
+      apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
+      using X(1) q(1) * by auto
+  next
+    case 3
+    then have "0 \<in> I" using H finite_measure.finite_emeasure_space by auto
+    have "q(0) = 0"
+    proof (rule ccontr)
+      assume *: "\<not>(q(0) = 0)"
+      define e where "e = \<bar>q(0)\<bar> / 2"
+      then have "e > 0" using * by auto
+      have "continuous (at 0) q"
+        using q(2) `0 \<in> I` `open I` \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
+      then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using `e > 0`
+        by (metis continuous_at_real_range real_norm_def)
+      then have *: "\<bar>q(y)\<bar> > e" if "\<bar>y\<bar> < d" for y
+      proof -
+        have "\<bar>q 0\<bar> \<le> \<bar>q 0 - q y\<bar> + \<bar>q y\<bar>" by auto
+        also have "... < e + \<bar>q y\<bar>" using d(2) that by force
+        finally have "\<bar>q y\<bar> > \<bar>q 0\<bar> - e" by auto
+        then show ?thesis unfolding e_def by simp
+      qed
+      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)"
+        by (rule emeasure_mono, auto simp add: * `e>0` less_imp_le ennreal_mult''[symmetric])
+      also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)"
+        by (rule nn_integral_Markov_inequality, auto)
+      also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto
+      also have "... = (1/e) * ennreal(\<integral>x. \<bar>q(X x)\<bar> \<partial>M)"
+        using nn_integral_eq_integral[OF integrable_abs[OF q(1)]] by auto
+      also have "... < \<infinity>"
+        by (simp add: ennreal_mult_less_top)
+      finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp
+
+      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"
+        by (auto simp add: `d>0` ennreal_mult''[symmetric])
+      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)"
+        by auto
+      also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)"
+        by (rule nn_integral_Markov_inequality, auto)
+      also have "... = (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) \<partial>M)" by auto
+      also have "... = (1/d) * ennreal(\<integral>x. \<bar>X x\<bar> \<partial>M)"
+        using nn_integral_eq_integral[OF integrable_abs[OF X(1)]] by auto
+      also have "... < \<infinity>"
+        by (simp add: ennreal_mult_less_top)
+      finally have B: "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} < \<infinity>" by simp
+
+      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
+      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})"
+        by simp
+      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}"
+        by (auto intro!: emeasure_subadditive)
+      also have "... < \<infinity>" using A B by auto
+      finally show False using `emeasure M (space M) = \<infinity>` by auto
+    qed
+
+    define A where "A = Inf ((\<lambda>t. (q 0 - q t) / (0 - t)) ` ({0<..} \<inter> I))"
+    have "q y \<ge> q 0 + A * (y - 0)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
+      using `0 \<in> I` `y \<in> I` `interior I = I` q(2) by auto
+    then have "q y \<ge> A * y" if "y \<in> I" for y using `q 0 = 0` that by auto
+    then have "AE x in M. q (real_cond_exp M F X x) \<ge> A * real_cond_exp M F X x"
+      using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
+    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"
+      using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
+    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
+      using that by auto
+    ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar>
+        \<le> \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>A * real_cond_exp M F X x\<bar>"
+      by auto
+
+    show "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
+      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>"])
+      apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
+      using X(1) q(1) * by auto
+  qed
+qed
+
+end
+
+end
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Probability/Levy.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -390,7 +390,7 @@
       by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
                 continuous_intros ballI M'.isCont_char continuous_intros)
     have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
-      using integral_norm_bound[OF 2] by simp
+      using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
     also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
       apply (rule integral_mono [OF 3])
        apply (simp add: emeasure_lborel_Icc_eq)
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Probability/Probability.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -11,6 +11,7 @@
   Random_Permutations
   SPMF
   Stream_Space
+  Conditional_Expectation
 begin
 
 end
diff -r 261d42f0bfac -r 979cdfdf7a79 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Oct 17 15:20:06 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Oct 13 18:36:06 2016 +0200
@@ -1440,6 +1440,42 @@
     at_within_def eventually_nhds_within_iff_sequentially comp_def
   by metis
 
+lemma approx_from_above_dense_linorder:
+  fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
+  assumes "x < y"
+  shows "\<exists>u. (\<forall>n. u n > x) \<and> (u \<longlonglongrightarrow> x)"
+proof -
+  obtain A :: "nat \<Rightarrow> 'a set" where A: "\<And>i. open (A i)" "\<And>i. x \<in> A i"
+                                      "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F \<longlonglongrightarrow> x"
+    by (metis first_countable_topology_class.countable_basis)
+  define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z > x)"
+  have "\<exists>z. z \<in> U \<and> x < z" if "x \<in> U" "open U" for U
+    using open_right[OF `open U` `x \<in> U` `x < y`]
+    by (meson atLeastLessThan_iff dense less_imp_le subset_eq)
+  then have *: "u n \<in> A n \<and> x < u n" for n
+    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
+  then have "u \<longlonglongrightarrow> x" using A(3) by simp
+  then show ?thesis using * by auto
+qed
+
+lemma approx_from_below_dense_linorder:
+  fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
+  assumes "x > y"
+  shows "\<exists>u. (\<forall>n. u n < x) \<and> (u \<longlonglongrightarrow> x)"
+proof -
+  obtain A :: "nat \<Rightarrow> 'a set" where A: "\<And>i. open (A i)" "\<And>i. x \<in> A i"
+                                      "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F \<longlonglongrightarrow> x"
+    by (metis first_countable_topology_class.countable_basis)
+  define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z < x)"
+  have "\<exists>z. z \<in> U \<and> z < x" if "x \<in> U" "open U" for U
+    using open_left[OF `open U` `x \<in> U` `x > y`]
+    by (meson dense greaterThanAtMost_iff less_imp_le subset_eq)
+  then have *: "u n \<in> A n \<and> u n < x" for n
+    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
+  then have "u \<longlonglongrightarrow> x" using A(3) by simp
+  then show ?thesis using * by auto
+qed
+
 
 subsection \<open>Function limit at a point\<close>