HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
authorhoelzl
Thu Oct 13 18:36:06 2016 +0200 (2016-10-13)
changeset 64283979cdfdf7a79
parent 64282 261d42f0bfac
child 64284 f3b905b2eee2
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Radon_Nikodym.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Probability/Characteristic_Functions.thy
src/HOL/Probability/Conditional_Expectation.thy
src/HOL/Probability/Levy.thy
src/HOL/Probability/Probability.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Mon Oct 17 15:20:06 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Oct 13 18:36:06 2016 +0200
     1.3 @@ -1747,11 +1747,23 @@
     1.4      unfolding sums_iff by auto
     1.5  qed
     1.6  
     1.7 -lemma integral_norm_bound:
     1.8 +lemma integral_norm_bound [simp]:
     1.9    fixes f :: "_ \<Rightarrow> 'a :: {banach, second_countable_topology}"
    1.10 -  shows "integrable M f \<Longrightarrow> norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
    1.11 -  using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"]
    1.12 -  using integral_norm_bound_ennreal[of M f] by (simp add: integral_nonneg_AE)
    1.13 +  shows "norm (integral\<^sup>L M f) \<le> (\<integral>x. norm (f x) \<partial>M)"
    1.14 +proof (cases "integrable M f")
    1.15 +  case True then show ?thesis
    1.16 +    using nn_integral_eq_integral[of M "\<lambda>x. norm (f x)"] integral_norm_bound_ennreal[of M f]
    1.17 +    by (simp add: integral_nonneg_AE)
    1.18 +next
    1.19 +  case False
    1.20 +  then have "norm (integral\<^sup>L M f) = 0" by (simp add: not_integrable_integral_eq)
    1.21 +  moreover have "(\<integral>x. norm (f x) \<partial>M) \<ge> 0" by auto
    1.22 +  ultimately show ?thesis by simp
    1.23 +qed
    1.24 +
    1.25 +lemma integral_abs_bound [simp]:
    1.26 +  fixes f :: "'a \<Rightarrow> real" shows "abs (\<integral>x. f x \<partial>M) \<le> (\<integral>x. \<bar>f x\<bar> \<partial>M)"
    1.27 +using integral_norm_bound[of M f] by auto
    1.28  
    1.29  lemma integral_eq_nn_integral:
    1.30    assumes [measurable]: "f \<in> borel_measurable M"
    1.31 @@ -1919,6 +1931,30 @@
    1.32      integral\<^sup>L M f \<le> integral\<^sup>L M g"
    1.33    by (intro integral_mono_AE) auto
    1.34  
    1.35 +text {*The next two statements are useful to bound Lebesgue integrals, as they avoid one
    1.36 +integrability assumption. The price to pay is that the upper function has to be nonnegative,
    1.37 +but this is often true and easy to check in computations.*}
    1.38 +
    1.39 +lemma integral_mono_AE':
    1.40 +  fixes f::"_ \<Rightarrow> real"
    1.41 +  assumes "integrable M f" "AE x in M. g x \<le> f x" "AE x in M. 0 \<le> f x"
    1.42 +  shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
    1.43 +proof (cases "integrable M g")
    1.44 +  case True
    1.45 +  show ?thesis by (rule integral_mono_AE, auto simp add: assms True)
    1.46 +next
    1.47 +  case False
    1.48 +  then have "(\<integral>x. g x \<partial>M) = 0" by (simp add: not_integrable_integral_eq)
    1.49 +  also have "... \<le> (\<integral>x. f x \<partial>M)" by (simp add: integral_nonneg_AE[OF assms(3)])
    1.50 +  finally show ?thesis by simp
    1.51 +qed
    1.52 +
    1.53 +lemma integral_mono':
    1.54 +  fixes f::"_ \<Rightarrow> real"
    1.55 +  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"
    1.56 +  shows "(\<integral>x. g x \<partial>M) \<le> (\<integral>x. f x \<partial>M)"
    1.57 +by (rule integral_mono_AE', insert assms, auto)
    1.58 +
    1.59  lemma (in finite_measure) integrable_measure:
    1.60    assumes I: "disjoint_family_on X I" "countable I"
    1.61    shows "integrable (count_space I) (\<lambda>i. measure M (X i))"
    1.62 @@ -1942,6 +1978,12 @@
    1.63    finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" .
    1.64  qed fact
    1.65  
    1.66 +lemma nn_integral_nonneg_infinite:
    1.67 +  fixes f::"'a \<Rightarrow> real"
    1.68 +  assumes "f \<in> borel_measurable M" "\<not> integrable M f" "AE x in M. f x \<ge> 0"
    1.69 +  shows "(\<integral>\<^sup>+x. f x \<partial>M) = \<infinity>"
    1.70 +using assms integrableI_real_bounded less_top by auto
    1.71 +
    1.72  lemma integral_real_bounded:
    1.73    assumes "0 \<le> r" "integral\<^sup>N M f \<le> ennreal r"
    1.74    shows "integral\<^sup>L M f \<le> r"
    1.75 @@ -1966,6 +2008,220 @@
    1.76      using \<open>0 \<le> r\<close> by (simp add: not_integrable_integral_eq)
    1.77  qed
    1.78  
    1.79 +lemma integrable_Min:
    1.80 +  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
    1.81 +  assumes "finite I" "I \<noteq> {}"
    1.82 +          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
    1.83 +  shows "integrable M (\<lambda>x. Min {f i x|i. i \<in> I})"
    1.84 +using assms apply (induct rule: finite_ne_induct) apply simp+
    1.85 +proof -
    1.86 +  fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Min {f i x |i. i \<in> F})"
    1.87 +                    "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
    1.88 +  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
    1.89 +  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
    1.90 +    using H(1) H(2) Min_insert by simp
    1.91 +  moreover have "integrable M (\<lambda>x. min (f j x) (Min {f i x |i. i \<in> F}))"
    1.92 +    by (rule integrable_min, auto simp add: H)
    1.93 +  ultimately show "integrable M (\<lambda>x. Min {f i x |i. i = j \<or> i \<in> F})" by simp
    1.94 +qed
    1.95 +
    1.96 +lemma integrable_Max:
    1.97 +  fixes f:: "_ \<Rightarrow> _ \<Rightarrow> real"
    1.98 +  assumes "finite I" "I \<noteq> {}"
    1.99 +          "\<And>i. i \<in> I \<Longrightarrow> integrable M (f i)"
   1.100 +  shows "integrable M (\<lambda>x. Max {f i x|i. i \<in> I})"
   1.101 +using assms apply (induct rule: finite_ne_induct) apply simp+
   1.102 +proof -
   1.103 +  fix j F assume H: "finite F" "F \<noteq> {}" "integrable M (\<lambda>x. Max {f i x |i. i \<in> F})"
   1.104 +                    "(\<And>i. i = j \<or> i \<in> F \<Longrightarrow> integrable M (f i))"
   1.105 +  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
   1.106 +  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
   1.107 +    using H(1) H(2) Max_insert by simp
   1.108 +  moreover have "integrable M (\<lambda>x. max (f j x) (Max {f i x |i. i \<in> F}))"
   1.109 +    by (rule integrable_max, auto simp add: H)
   1.110 +  ultimately show "integrable M (\<lambda>x. Max {f i x |i. i = j \<or> i \<in> F})" by simp
   1.111 +qed
   1.112 +
   1.113 +lemma integral_Markov_inequality:
   1.114 +  assumes [measurable]: "integrable M u" and "AE x in M. 0 \<le> u x" "0 < (c::real)"
   1.115 +  shows "(emeasure M) {x\<in>space M. u x \<ge> c} \<le> (1/c) * (\<integral>x. u x \<partial>M)"
   1.116 +proof -
   1.117 +  have "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>\<^sup>+ x. u x \<partial>M)"
   1.118 +    by (rule nn_integral_mono_AE, auto simp add: `c>0` less_eq_real_def)
   1.119 +  also have "... = (\<integral>x. u x \<partial>M)"
   1.120 +    by (rule nn_integral_eq_integral, auto simp add: assms)
   1.121 +  finally have *: "(\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M) \<le> (\<integral>x. u x \<partial>M)"
   1.122 +    by simp
   1.123 +
   1.124 +  have "{x \<in> space M. u x \<ge> c} = {x \<in> space M. ennreal(1/c) * u x \<ge> 1} \<inter> (space M)"
   1.125 +    using `c>0` by (auto simp: ennreal_mult'[symmetric])
   1.126 +  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))"
   1.127 +    by simp
   1.128 +  also have "... \<le> ennreal(1/c) * (\<integral>\<^sup>+ x. ennreal(u x) * indicator (space M) x \<partial>M)"
   1.129 +    by (rule nn_integral_Markov_inequality) (auto simp add: assms)
   1.130 +  also have "... \<le> ennreal(1/c) * (\<integral>x. u x \<partial>M)"
   1.131 +    apply (rule mult_left_mono) using * `c>0` by auto
   1.132 +  finally show ?thesis
   1.133 +    using \<open>0<c\<close> by (simp add: ennreal_mult'[symmetric])
   1.134 +qed
   1.135 +
   1.136 +lemma integral_ineq_eq_0_then_AE:
   1.137 +  fixes f::"_ \<Rightarrow> real"
   1.138 +  assumes "AE x in M. f x \<le> g x" "integrable M f" "integrable M g"
   1.139 +          "(\<integral>x. f x \<partial>M) = (\<integral>x. g x \<partial>M)"
   1.140 +  shows "AE x in M. f x = g x"
   1.141 +proof -
   1.142 +  define h where "h = (\<lambda>x. g x - f x)"
   1.143 +  have "AE x in M. h x = 0"
   1.144 +    apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
   1.145 +    unfolding h_def using assms by auto
   1.146 +  then show ?thesis unfolding h_def by auto
   1.147 +qed
   1.148 +
   1.149 +lemma not_AE_zero_int_E:
   1.150 +  fixes f::"'a \<Rightarrow> real"
   1.151 +  assumes "AE x in M. f x \<ge> 0" "(\<integral>x. f x \<partial>M) > 0"
   1.152 +      and [measurable]: "f \<in> borel_measurable M"
   1.153 +  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)"
   1.154 +proof (rule not_AE_zero_E, auto simp add: assms)
   1.155 +  assume *: "AE x in M. f x = 0"
   1.156 +  have "(\<integral>x. f x \<partial>M) = (\<integral>x. 0 \<partial>M)" by (rule integral_cong_AE, auto simp add: *)
   1.157 +  then have "(\<integral>x. f x \<partial>M) = 0" by simp
   1.158 +  then show False using assms(2) by simp
   1.159 +qed
   1.160 +
   1.161 +lemma tendsto_L1_int:
   1.162 +  fixes u :: "_ \<Rightarrow> _ \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.163 +  assumes [measurable]: "\<And>n. integrable M (u n)" "integrable M f"
   1.164 +          and "((\<lambda>n. (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)) \<longlongrightarrow> 0) F"
   1.165 +  shows "((\<lambda>n. (\<integral>x. u n x \<partial>M)) \<longlongrightarrow> (\<integral>x. f x \<partial>M)) F"
   1.166 +proof -
   1.167 +  have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> (0::ennreal)) F"
   1.168 +  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)
   1.169 +    {
   1.170 +      fix n
   1.171 +      have "(\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M) = (\<integral>x. u n x - f x \<partial>M)"
   1.172 +        apply (rule Bochner_Integration.integral_diff[symmetric]) using assms by auto
   1.173 +      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)"
   1.174 +        by auto
   1.175 +      also have "... \<le> (\<integral>x. norm(u n x - f x) \<partial>M)"
   1.176 +        by (rule integral_norm_bound)
   1.177 +      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)"
   1.178 +        by simp
   1.179 +      also have "... = (\<integral>\<^sup>+x. norm(u n x - f x) \<partial>M)"
   1.180 +        apply (rule nn_integral_eq_integral[symmetric]) using assms by auto
   1.181 +      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
   1.182 +    }
   1.183 +    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"
   1.184 +      by auto
   1.185 +  qed
   1.186 +  then have "((\<lambda>n. norm((\<integral>x. u n x \<partial>M) - (\<integral>x. f x \<partial>M))) \<longlongrightarrow> 0) F"
   1.187 +    by (simp add: ennreal_0[symmetric] del: ennreal_0)
   1.188 +  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
   1.189 +  then show ?thesis using Lim_null by auto
   1.190 +qed
   1.191 +
   1.192 +text {*The next lemma asserts that, if a sequence of functions converges in $L^1$, then
   1.193 +it admits a subsequence that converges almost everywhere.*}
   1.194 +
   1.195 +lemma tendsto_L1_AE_subseq:
   1.196 +  fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   1.197 +  assumes [measurable]: "\<And>n. integrable M (u n)"
   1.198 +      and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
   1.199 +  shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
   1.200 +proof -
   1.201 +  {
   1.202 +    fix k
   1.203 +    have "eventually (\<lambda>n. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k) sequentially"
   1.204 +      using order_tendstoD(2)[OF assms(2)] by auto
   1.205 +    with eventually_elim2[OF eventually_gt_at_top[of k] this]
   1.206 +    have "\<exists>n>k. (\<integral>x. norm(u n x) \<partial>M) < (1/2)^k"
   1.207 +      by (metis eventually_False_sequentially)
   1.208 +  }
   1.209 +  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))"
   1.210 +    by (intro dependent_nat_choice, auto)
   1.211 +  then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
   1.212 +    by (auto simp: subseq_Suc_iff)
   1.213 +  define r where "r = (\<lambda>n. r0(n+1))"
   1.214 +  have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
   1.215 +  have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
   1.216 +  proof -
   1.217 +    have "r0 n \<ge> n" using `subseq r0` by (simp add: seq_suble)
   1.218 +    have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF `r0 n \<ge> n`], auto)
   1.219 +    then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
   1.220 +    then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
   1.221 +    moreover have "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) = (\<integral>x. norm(u (r n) x) \<partial>M)"
   1.222 +      by (rule nn_integral_eq_integral, auto simp add: integrable_norm[OF assms(1)[of "r n"]])
   1.223 +    ultimately show ?thesis by (auto intro: ennreal_lessI)
   1.224 +  qed
   1.225 +
   1.226 +  have "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
   1.227 +  proof (rule AE_upper_bound_inf_ennreal)
   1.228 +    fix e::real assume "e > 0"
   1.229 +    define A where "A = (\<lambda>n. {x \<in> space M. norm(u (r n) x) \<ge> e})"
   1.230 +    have A_meas [measurable]: "\<And>n. A n \<in> sets M" unfolding A_def by auto
   1.231 +    have A_bound: "emeasure M (A n) < (1/e) * ennreal((1/2)^n)" for n
   1.232 +    proof -
   1.233 +      have *: "indicator (A n) x \<le> (1/e) * ennreal(norm(u (r n) x))" for x
   1.234 +        apply (cases "x \<in> A n") unfolding A_def using \<open>0 < e\<close> by (auto simp: ennreal_mult[symmetric])
   1.235 +      have "emeasure M (A n) = (\<integral>\<^sup>+x. indicator (A n) x \<partial>M)" by auto
   1.236 +      also have "... \<le> (\<integral>\<^sup>+x. (1/e) * ennreal(norm(u (r n) x)) \<partial>M)"
   1.237 +        apply (rule nn_integral_mono) using * by auto
   1.238 +      also have "... = (1/e) * (\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M)"
   1.239 +        apply (rule nn_integral_cmult) using `e > 0` by auto
   1.240 +      also have "... < (1/e) * ennreal((1/2)^n)"
   1.241 +        using I[of n] `e > 0` by (intro ennreal_mult_strict_left_mono) auto
   1.242 +      finally show ?thesis by simp
   1.243 +    qed
   1.244 +    have A_fin: "emeasure M (A n) < \<infinity>" for n
   1.245 +      using `e > 0` A_bound[of n]
   1.246 +      by (auto simp add: ennreal_mult less_top[symmetric])
   1.247 +
   1.248 +    have A_sum: "summable (\<lambda>n. measure M (A n))"
   1.249 +    proof (rule summable_comparison_test'[of "\<lambda>n. (1/e) * (1/2)^n" 0])
   1.250 +      have "summable (\<lambda>n. (1/(2::real))^n)" by (simp add: summable_geometric)
   1.251 +      then show "summable (\<lambda>n. (1/e) * (1/2)^n)" using summable_mult by blast
   1.252 +      fix n::nat assume "n \<ge> 0"
   1.253 +      have "norm(measure M (A n)) = measure M (A n)" by simp
   1.254 +      also have "... = enn2real(emeasure M (A n))" unfolding measure_def by simp
   1.255 +      also have "... < enn2real((1/e) * (1/2)^n)"
   1.256 +        using A_bound[of n] \<open>emeasure M (A n) < \<infinity>\<close> \<open>0 < e\<close>
   1.257 +        by (auto simp: emeasure_eq_ennreal_measure ennreal_mult[symmetric] ennreal_less_iff)
   1.258 +      also have "... = (1/e) * (1/2)^n"
   1.259 +        using \<open>0<e\<close> by auto
   1.260 +      finally show "norm(measure M (A n)) \<le> (1/e) * (1/2)^n" by simp
   1.261 +    qed
   1.262 +
   1.263 +    have "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
   1.264 +      by (rule borel_cantelli_AE1[OF A_meas A_fin A_sum])
   1.265 +    moreover
   1.266 +    {
   1.267 +      fix x assume "eventually (\<lambda>n. x \<in> space M - A n) sequentially"
   1.268 +      moreover have "norm(u (r n) x) \<le> ennreal e" if "x \<in> space M - A n" for n
   1.269 +        using that unfolding A_def by (auto intro: ennreal_leI)
   1.270 +      ultimately have "eventually (\<lambda>n. norm(u (r n) x) \<le> ennreal e) sequentially"
   1.271 +        by (simp add: eventually_mono)
   1.272 +      then have "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> e"
   1.273 +        by (simp add: Limsup_bounded)
   1.274 +    }
   1.275 +    ultimately show "AE x in M. limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0 + ennreal e" by auto
   1.276 +  qed
   1.277 +  moreover
   1.278 +  {
   1.279 +    fix x assume "limsup (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
   1.280 +    moreover then have "liminf (\<lambda>n. ennreal (norm(u (r n) x))) \<le> 0"
   1.281 +      by (rule order_trans[rotated]) (auto intro: Liminf_le_Limsup)
   1.282 +    ultimately have "(\<lambda>n. ennreal (norm(u (r n) x))) \<longlonglongrightarrow> 0"
   1.283 +      using tendsto_Limsup[of sequentially "\<lambda>n. ennreal (norm(u (r n) x))"] by auto
   1.284 +    then have "(\<lambda>n. norm(u (r n) x)) \<longlonglongrightarrow> 0"
   1.285 +      by (simp add: ennreal_0[symmetric] del: ennreal_0)
   1.286 +    then have "(\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0"
   1.287 +      by (simp add: tendsto_norm_zero_iff)
   1.288 +  }
   1.289 +  ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
   1.290 +  then show ?thesis using `subseq r` by auto
   1.291 +qed
   1.292 +
   1.293  subsection \<open>Restricted measure spaces\<close>
   1.294  
   1.295  lemma integrable_restrict_space:
   1.296 @@ -2478,6 +2734,12 @@
   1.297    apply auto
   1.298    done
   1.299  
   1.300 +lemma (in finite_measure) integral_bounded_eq_bound_then_AE:
   1.301 +  assumes "AE x in M. f x \<le> (c::real)"
   1.302 +    "integrable M f" "(\<integral>x. f x \<partial>M) = c * measure M (space M)"
   1.303 +  shows "AE x in M. f x = c"
   1.304 +  apply (rule integral_ineq_eq_0_then_AE) using assms by auto
   1.305 +
   1.306  lemma integral_indicator_finite_real:
   1.307    fixes f :: "'a \<Rightarrow> real"
   1.308    assumes [simp]: "finite A"
     2.1 --- a/src/HOL/Analysis/Borel_Space.thy	Mon Oct 17 15:20:06 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Thu Oct 13 18:36:06 2016 +0200
     2.3 @@ -1896,6 +1896,9 @@
     2.4      by auto
     2.5  qed
     2.6  
     2.7 +text \<open>The next lemmas hold in any second countable linorder (including ennreal or ereal for instance),
     2.8 +but in the current state they are restricted to reals.\<close>
     2.9 +
    2.10  lemma borel_measurable_mono_on_fnc:
    2.11    fixes f :: "real \<Rightarrow> real" and A :: "real set"
    2.12    assumes "mono_on f A"
    2.13 @@ -1907,6 +1910,12 @@
    2.14                intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
    2.15    done
    2.16  
    2.17 +lemma borel_measurable_piecewise_mono:
    2.18 +  fixes f::"real \<Rightarrow> real" and C::"real set set"
    2.19 +  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"
    2.20 +  shows "f \<in> borel_measurable borel"
    2.21 +by (rule measurable_piecewise_restrict[of C], auto intro: borel_measurable_mono_on_fnc simp: assms)
    2.22 +
    2.23  lemma borel_measurable_mono:
    2.24    fixes f :: "real \<Rightarrow> real"
    2.25    shows "mono f \<Longrightarrow> f \<in> borel_measurable borel"
     3.1 --- a/src/HOL/Analysis/Measurable.thy	Mon Oct 17 15:20:06 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Measurable.thy	Thu Oct 13 18:36:06 2016 +0200
     3.3 @@ -636,6 +636,16 @@
     3.4      unfolding pred_restrict_space[OF P_f] by (simp cong: measurable_cong)
     3.5  qed
     3.6  
     3.7 +lemma measurable_limsup [measurable (raw)]:
     3.8 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
     3.9 +  shows "limsup A \<in> sets M"
    3.10 +by (subst limsup_INF_SUP, auto)
    3.11 +
    3.12 +lemma measurable_liminf [measurable (raw)]:
    3.13 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
    3.14 +  shows "liminf A \<in> sets M"
    3.15 +by (subst liminf_SUP_INF, auto)
    3.16 +
    3.17  hide_const (open) pred
    3.18  
    3.19  end
     4.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Oct 17 15:20:06 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Oct 13 18:36:06 2016 +0200
     4.3 @@ -1059,6 +1059,11 @@
     4.4    with AE_iff_null[of M P] assms show ?thesis by auto
     4.5  qed
     4.6  
     4.7 +lemma AE_E3:
     4.8 +  assumes "AE x in M. P x"
     4.9 +  obtains N where "\<And>x. x \<in> space M - N \<Longrightarrow> P x" "N \<in> null_sets M"
    4.10 +using assms unfolding eventually_ae_filter by auto
    4.11 +
    4.12  lemma AE_I:
    4.13    assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
    4.14    shows "AE x in M. P x"
    4.15 @@ -1087,6 +1092,10 @@
    4.16    qed
    4.17  qed
    4.18  
    4.19 +text {*The next lemma is convenient to combine with a lemma whose conclusion is of the
    4.20 +form \<open>AE x in M. P x = Q x\<close>: for such a lemma, there is no \verb+[symmetric]+ variant,
    4.21 +but using \<open>AE_symmetric[OF...]\<close> will replace it.*}
    4.22 +
    4.23  (* depricated replace by laws about eventually *)
    4.24  lemma
    4.25    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"
    4.26 @@ -1096,6 +1105,11 @@
    4.27      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)"
    4.28    by auto
    4.29  
    4.30 +lemma AE_symmetric:
    4.31 +  assumes "AE x in M. P x = Q x"
    4.32 +  shows "AE x in M. Q x = P x"
    4.33 +  using assms by auto
    4.34 +
    4.35  lemma AE_impI:
    4.36    "(P \<Longrightarrow> AE x in M. Q x) \<Longrightarrow> AE x in M. P \<longrightarrow> Q x"
    4.37    by (cases P) auto
    4.38 @@ -1166,6 +1180,10 @@
    4.39      unfolding eventually_ae_filter by auto
    4.40  qed auto
    4.41  
    4.42 +lemma AE_ball_countable':
    4.43 +  "(\<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"
    4.44 +  unfolding AE_ball_countable by simp
    4.45 +
    4.46  lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
    4.47    by (auto simp add: pairwise_def)
    4.48  
    4.49 @@ -1225,6 +1243,11 @@
    4.50    using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"]
    4.51    by (cases "{x\<in>space M. P x} \<in> sets M") (simp_all add: emeasure_notin_sets)
    4.52  
    4.53 +lemma emeasure_0_AE:
    4.54 +  assumes "emeasure M (space M) = 0"
    4.55 +  shows "AE x in M. P x"
    4.56 +using eventually_ae_filter assms by blast
    4.57 +
    4.58  lemma emeasure_add_AE:
    4.59    assumes [measurable]: "A \<in> sets M" "B \<in> sets M" "C \<in> sets M"
    4.60    assumes 1: "AE x in M. x \<in> C \<longleftrightarrow> x \<in> A \<or> x \<in> B"
    4.61 @@ -1328,6 +1351,40 @@
    4.62    qed
    4.63  qed
    4.64  
    4.65 +lemma (in sigma_finite_measure) approx_PInf_emeasure_with_finite:
    4.66 +  fixes C::real
    4.67 +  assumes W_meas: "W \<in> sets M"
    4.68 +      and W_inf: "emeasure M W = \<infinity>"
    4.69 +  obtains Z where "Z \<in> sets M" "Z \<subseteq> W" "emeasure M Z < \<infinity>" "emeasure M Z > C"
    4.70 +proof -
    4.71 +  obtain A :: "nat \<Rightarrow> 'a set"
    4.72 +    where A: "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
    4.73 +    using sigma_finite_incseq by blast
    4.74 +  define B where "B = (\<lambda>i. W \<inter> A i)"
    4.75 +  have B_meas: "\<And>i. B i \<in> sets M" using W_meas `range A \<subseteq> sets M` B_def by blast
    4.76 +  have b: "\<And>i. B i \<subseteq> W" using B_def by blast
    4.77 +
    4.78 +  { fix i
    4.79 +    have "emeasure M (B i) \<le> emeasure M (A i)"
    4.80 +      using A by (intro emeasure_mono) (auto simp: B_def)
    4.81 +    also have "emeasure M (A i) < \<infinity>"
    4.82 +      using `\<And>i. emeasure M (A i) \<noteq> \<infinity>` by (simp add: less_top)
    4.83 +    finally have "emeasure M (B i) < \<infinity>" . }
    4.84 +  note c = this
    4.85 +
    4.86 +  have "W = (\<Union>i. B i)" using B_def `(\<Union>i. A i) = space M` W_meas by auto
    4.87 +  moreover have "incseq B" using B_def `incseq A` by (simp add: incseq_def subset_eq)
    4.88 +  ultimately have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> emeasure M W" using W_meas B_meas
    4.89 +    by (simp add: B_meas Lim_emeasure_incseq image_subset_iff)
    4.90 +  then have "(\<lambda>i. emeasure M (B i)) \<longlonglongrightarrow> \<infinity>" using W_inf by simp
    4.91 +  from order_tendstoD(1)[OF this, of C]
    4.92 +  obtain i where d: "emeasure M (B i) > C"
    4.93 +    by (auto simp: eventually_sequentially)
    4.94 +  have "B i \<in> sets M" "B i \<subseteq> W" "emeasure M (B i) < \<infinity>" "emeasure M (B i) > C"
    4.95 +    using B_meas b c d by auto
    4.96 +  then show ?thesis using that by blast
    4.97 +qed
    4.98 +
    4.99  subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
   4.100  
   4.101  definition distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
   4.102 @@ -1824,6 +1881,88 @@
   4.103    then show ?fm ?m by auto
   4.104  qed
   4.105  
   4.106 +lemma suminf_exist_split2:
   4.107 +  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   4.108 +  assumes "summable f"
   4.109 +  shows "(\<lambda>n. (\<Sum>k. f(k+n))) \<longlonglongrightarrow> 0"
   4.110 +by (subst lim_sequentially, auto simp add: dist_norm suminf_exist_split[OF _ assms])
   4.111 +
   4.112 +lemma emeasure_union_summable:
   4.113 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   4.114 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   4.115 +  shows "emeasure M (\<Union>n. A n) < \<infinity>" "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
   4.116 +proof -
   4.117 +  define B where "B = (\<lambda>N. (\<Union>n\<in>{..<N}. A n))"
   4.118 +  have [measurable]: "B N \<in> sets M" for N unfolding B_def by auto
   4.119 +  have "(\<lambda>N. emeasure M (B N)) \<longlonglongrightarrow> emeasure M (\<Union>N. B N)"
   4.120 +    apply (rule Lim_emeasure_incseq) unfolding B_def by (auto simp add: SUP_subset_mono incseq_def)
   4.121 +  moreover have "emeasure M (B N) \<le> ennreal (\<Sum>n. measure M (A n))" for N
   4.122 +  proof -
   4.123 +    have *: "(\<Sum>n\<in>{..<N}. measure M (A n)) \<le> (\<Sum>n. measure M (A n))"
   4.124 +      using assms(3) measure_nonneg sum_le_suminf by blast
   4.125 +
   4.126 +    have "emeasure M (B N) \<le> (\<Sum>n\<in>{..<N}. emeasure M (A n))"
   4.127 +      unfolding B_def by (rule emeasure_subadditive_finite, auto)
   4.128 +    also have "... = (\<Sum>n\<in>{..<N}. ennreal(measure M (A n)))"
   4.129 +      using assms(2) by (simp add: emeasure_eq_ennreal_measure less_top)
   4.130 +    also have "... = ennreal (\<Sum>n\<in>{..<N}. measure M (A n))"
   4.131 +      by auto
   4.132 +    also have "... \<le> ennreal (\<Sum>n. measure M (A n))"
   4.133 +      using * by (auto simp: ennreal_leI)
   4.134 +    finally show ?thesis by simp
   4.135 +  qed
   4.136 +  ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
   4.137 +    by (simp add: Lim_bounded_ereal)
   4.138 +  then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
   4.139 +    unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
   4.140 +  then show "emeasure M (\<Union>n. A n) < \<infinity>"
   4.141 +    by (auto simp: less_top[symmetric] top_unique)
   4.142 +qed
   4.143 +
   4.144 +lemma borel_cantelli_limsup1:
   4.145 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   4.146 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   4.147 +  shows "limsup A \<in> null_sets M"
   4.148 +proof -
   4.149 +  have "emeasure M (limsup A) \<le> 0"
   4.150 +  proof (rule LIMSEQ_le_const)
   4.151 +    have "(\<lambda>n. (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0" by (rule suminf_exist_split2[OF assms(3)])
   4.152 +    then show "(\<lambda>n. ennreal (\<Sum>k. measure M (A (k+n)))) \<longlonglongrightarrow> 0"
   4.153 +      unfolding ennreal_0[symmetric] by (intro tendsto_ennrealI)
   4.154 +    have "emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))" for n
   4.155 +    proof -
   4.156 +      have I: "(\<Union>k\<in>{n..}. A k) = (\<Union>k. A (k+n))" by (auto, metis le_add_diff_inverse2, fastforce)
   4.157 +      have "emeasure M (limsup A) \<le> emeasure M (\<Union>k\<in>{n..}. A k)"
   4.158 +        by (rule emeasure_mono, auto simp add: limsup_INF_SUP)
   4.159 +      also have "... = emeasure M (\<Union>k. A (k+n))"
   4.160 +        using I by auto
   4.161 +      also have "... \<le> (\<Sum>k. measure M (A (k+n)))"
   4.162 +        apply (rule emeasure_union_summable)
   4.163 +        using assms summable_ignore_initial_segment[OF assms(3), of n] by auto
   4.164 +      finally show ?thesis by simp
   4.165 +    qed
   4.166 +    then show "\<exists>N. \<forall>n\<ge>N. emeasure M (limsup A) \<le> (\<Sum>k. measure M (A (k+n)))"
   4.167 +      by auto
   4.168 +  qed
   4.169 +  then show ?thesis using assms(1) measurable_limsup by auto
   4.170 +qed
   4.171 +
   4.172 +lemma borel_cantelli_AE1:
   4.173 +  assumes [measurable]: "\<And>n. A n \<in> sets M"
   4.174 +    and "\<And>n. emeasure M (A n) < \<infinity>" "summable (\<lambda>n. measure M (A n))"
   4.175 +  shows "AE x in M. eventually (\<lambda>n. x \<in> space M - A n) sequentially"
   4.176 +proof -
   4.177 +  have "AE x in M. x \<notin> limsup A"
   4.178 +    using borel_cantelli_limsup1[OF assms] unfolding eventually_ae_filter by auto
   4.179 +  moreover
   4.180 +  {
   4.181 +    fix x assume "x \<notin> limsup A"
   4.182 +    then obtain N where "x \<notin> (\<Union>n\<in>{N..}. A n)" unfolding limsup_INF_SUP by blast
   4.183 +    then have "eventually (\<lambda>n. x \<notin> A n) sequentially" using eventually_sequentially by auto
   4.184 +  }
   4.185 +  ultimately show ?thesis by auto
   4.186 +qed
   4.187 +
   4.188  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
   4.189  
   4.190  locale finite_measure = sigma_finite_measure M for M +
     5.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Mon Oct 17 15:20:06 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Thu Oct 13 18:36:06 2016 +0200
     5.3 @@ -9,6 +9,102 @@
     5.4    imports Measure_Space Borel_Space
     5.5  begin
     5.6  
     5.7 +subsection \<open>Approximating functions\<close>
     5.8 +
     5.9 +lemma AE_upper_bound_inf_ennreal:
    5.10 +  fixes F G::"'a \<Rightarrow> ennreal"
    5.11 +  assumes "\<And>e. (e::real) > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e"
    5.12 +  shows "AE x in M. F x \<le> G x"
    5.13 +proof -
    5.14 +  have "AE x in M. \<forall>n::nat. F x \<le> G x + ennreal (1 / Suc n)"
    5.15 +    using assms by (auto simp: AE_all_countable)
    5.16 +  then show ?thesis
    5.17 +  proof (eventually_elim)
    5.18 +    fix x assume x: "\<forall>n::nat. F x \<le> G x + ennreal (1 / Suc n)"
    5.19 +    show "F x \<le> G x"
    5.20 +    proof (rule ennreal_le_epsilon)
    5.21 +      fix e :: real assume "0 < e"
    5.22 +      then obtain n where n: "1 / Suc n < e"
    5.23 +        by (blast elim: nat_approx_posE)
    5.24 +      have "F x \<le> G x + 1 / Suc n"
    5.25 +        using x by simp
    5.26 +      also have "\<dots> \<le> G x + e"
    5.27 +        using n by (intro add_mono ennreal_leI) auto
    5.28 +      finally show "F x \<le> G x + ennreal e" .
    5.29 +    qed
    5.30 +  qed
    5.31 +qed
    5.32 +
    5.33 +lemma AE_upper_bound_inf:
    5.34 +  fixes F G::"'a \<Rightarrow> real"
    5.35 +  assumes "\<And>e. e > 0 \<Longrightarrow> AE x in M. F x \<le> G x + e"
    5.36 +  shows "AE x in M. F x \<le> G x"
    5.37 +proof -
    5.38 +  have "AE x in M. F x \<le> G x + 1/real (n+1)" for n::nat
    5.39 +    by (rule assms, auto)
    5.40 +  then have "AE x in M. \<forall>n::nat \<in> UNIV. F x \<le> G x + 1/real (n+1)"
    5.41 +    by (rule AE_ball_countable', auto)
    5.42 +  moreover
    5.43 +  {
    5.44 +    fix x assume i: "\<forall>n::nat \<in> UNIV. F x \<le> G x + 1/real (n+1)"
    5.45 +    have "(\<lambda>n. G x + 1/real (n+1)) \<longlonglongrightarrow> G x + 0"
    5.46 +      by (rule tendsto_add, simp, rule LIMSEQ_ignore_initial_segment[OF lim_1_over_n, of 1])
    5.47 +    then have "F x \<le> G x" using i LIMSEQ_le_const by fastforce
    5.48 +  }
    5.49 +  ultimately show ?thesis by auto
    5.50 +qed
    5.51 +
    5.52 +lemma not_AE_zero_ennreal_E:
    5.53 +  fixes f::"'a \<Rightarrow> ennreal"
    5.54 +  assumes "\<not> (AE x in M. f x = 0)" and [measurable]: "f \<in> borel_measurable M"
    5.55 +  shows "\<exists>A\<in>sets M. \<exists>e::real>0. emeasure M A > 0 \<and> (\<forall>x \<in> A. f x \<ge> e)"
    5.56 +proof -
    5.57 +  { assume "\<not> (\<exists>e::real>0. {x \<in> space M. f x \<ge> e} \<notin> null_sets M)"
    5.58 +    then have "0 < e \<Longrightarrow> AE x in M. f x \<le> e" for e :: real
    5.59 +      by (auto simp: not_le less_imp_le dest!: AE_not_in)
    5.60 +    then have "AE x in M. f x \<le> 0"
    5.61 +      by (intro AE_upper_bound_inf_ennreal[where G="\<lambda>_. 0"]) simp
    5.62 +    then have False
    5.63 +      using assms by auto }
    5.64 +  then obtain e::real where e: "e > 0" "{x \<in> space M. f x \<ge> e} \<notin> null_sets M" by auto
    5.65 +  define A where "A = {x \<in> space M. f x \<ge> e}"
    5.66 +  have 1 [measurable]: "A \<in> sets M" unfolding A_def by auto
    5.67 +  have 2: "emeasure M A > 0"
    5.68 +    using e(2) A_def \<open>A \<in> sets M\<close> by auto
    5.69 +  have 3: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> e" unfolding A_def by auto
    5.70 +  show ?thesis using e(1) 1 2 3 by blast
    5.71 +qed
    5.72 +
    5.73 +lemma not_AE_zero_E:
    5.74 +  fixes f::"'a \<Rightarrow> real"
    5.75 +  assumes "AE x in M. f x \<ge> 0"
    5.76 +          "\<not>(AE x in M. f x = 0)"
    5.77 +      and [measurable]: "f \<in> borel_measurable M"
    5.78 +  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)"
    5.79 +proof -
    5.80 +  have "\<exists>e. e > 0 \<and> {x \<in> space M. f x \<ge> e} \<notin> null_sets M"
    5.81 +  proof (rule ccontr)
    5.82 +    assume *: "\<not>(\<exists>e. e > 0 \<and> {x \<in> space M. f x \<ge> e} \<notin> null_sets M)"
    5.83 +    {
    5.84 +      fix e::real assume "e > 0"
    5.85 +      then have "{x \<in> space M. f x \<ge> e} \<in> null_sets M" using * by blast
    5.86 +      then have "AE x in M. x \<notin> {x \<in> space M. f x \<ge> e}" using AE_not_in by blast
    5.87 +      then have "AE x in M. f x \<le> e" by auto
    5.88 +    }
    5.89 +    then have "AE x in M. f x \<le> 0" by (rule AE_upper_bound_inf, auto)
    5.90 +    then have "AE x in M. f x = 0" using assms(1) by auto
    5.91 +    then show False using assms(2) by auto
    5.92 +  qed
    5.93 +  then obtain e where e: "e>0" "{x \<in> space M. f x \<ge> e} \<notin> null_sets M" by auto
    5.94 +  define A where "A = {x \<in> space M. f x \<ge> e}"
    5.95 +  have 1 [measurable]: "A \<in> sets M" unfolding A_def by auto
    5.96 +  have 2: "emeasure M A > 0"
    5.97 +    using e(2) A_def \<open>A \<in> sets M\<close> by auto
    5.98 +  have 3: "\<And>x. x \<in> A \<Longrightarrow> f x \<ge> e" unfolding A_def by auto
    5.99 +  show ?thesis
   5.100 +    using e(1) 1 2 3 by blast
   5.101 +qed
   5.102 +
   5.103  subsection "Simple function"
   5.104  
   5.105  text \<open>
     6.1 --- a/src/HOL/Analysis/Radon_Nikodym.thy	Mon Oct 17 15:20:06 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Radon_Nikodym.thy	Thu Oct 13 18:36:06 2016 +0200
     6.3 @@ -44,6 +44,64 @@
     6.4    qed
     6.5  qed fact
     6.6  
     6.7 +text {*An equivalent characterization of sigma-finite spaces is the existence of integrable
     6.8 +positive functions (or, still equivalently, the existence of a probability measure which is in
     6.9 +the same measure class as the original measure).*}
    6.10 +
    6.11 +lemma (in sigma_finite_measure) obtain_positive_integrable_function:
    6.12 +  obtains f::"'a \<Rightarrow> real" where
    6.13 +    "f \<in> borel_measurable M"
    6.14 +    "\<And>x. f x > 0"
    6.15 +    "\<And>x. f x \<le> 1"
    6.16 +    "integrable M f"
    6.17 +proof -
    6.18 +  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>"
    6.19 +    using sigma_finite by auto
    6.20 +  then have [measurable]:"A n \<in> sets M" for n by auto
    6.21 +  define g where "g = (\<lambda>x. (\<Sum>n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n))))"
    6.22 +  have [measurable]: "g \<in> borel_measurable M" unfolding g_def by auto
    6.23 +  have *: "summable (\<lambda>n. (1/2)^(Suc n) * indicator (A n) x / (1+ measure M (A n)))" for x
    6.24 +    apply (rule summable_comparison_test'[of "\<lambda>n. (1/2)^(Suc n)" 0])
    6.25 +    using power_half_series summable_def by (auto simp add: indicator_def divide_simps)
    6.26 +  have "g x \<le> (\<Sum>n. (1/2)^(Suc n))" for x unfolding g_def
    6.27 +    apply (rule suminf_le) using * power_half_series summable_def by (auto simp add: indicator_def divide_simps)
    6.28 +  then have g_le_1: "g x \<le> 1" for x using power_half_series sums_unique by fastforce
    6.29 +
    6.30 +  have g_pos: "g x > 0" if "x \<in> space M" for x
    6.31 +  unfolding g_def proof (subst suminf_pos_iff[OF *[of x]], auto)
    6.32 +    obtain i where "x \<in> A i" using `(\<Union>i. A i) = space M` `x \<in> space M` by auto
    6.33 +    then have "0 < (1 / 2) ^ Suc i * indicator (A i) x / (1 + Sigma_Algebra.measure M (A i))"
    6.34 +      unfolding indicator_def apply (auto simp add: divide_simps) using measure_nonneg[of M "A i"]
    6.35 +      by (auto, meson add_nonneg_nonneg linorder_not_le mult_nonneg_nonneg zero_le_numeral zero_le_one zero_le_power)
    6.36 +    then show "\<exists>i. 0 < (1 / 2) ^ i * indicator (A i) x / (2 + 2 * Sigma_Algebra.measure M (A i))"
    6.37 +      by auto
    6.38 +  qed
    6.39 +
    6.40 +  have "integrable M g"
    6.41 +  unfolding g_def proof (rule integrable_suminf)
    6.42 +    fix n
    6.43 +    show "integrable M (\<lambda>x. (1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n)))"
    6.44 +      using `emeasure M (A n) \<noteq> \<infinity>`
    6.45 +      by (auto intro!: integrable_mult_right integrable_divide_zero integrable_real_indicator simp add: top.not_eq_extremum)
    6.46 +  next
    6.47 +    show "AE x in M. summable (\<lambda>n. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))))"
    6.48 +      using * by auto
    6.49 +    show "summable (\<lambda>n. (\<integral>x. norm ((1 / 2) ^ Suc n * indicator (A n) x / (1 + Sigma_Algebra.measure M (A n))) \<partial>M))"
    6.50 +      apply (rule summable_comparison_test'[of "\<lambda>n. (1/2)^(Suc n)" 0], auto)
    6.51 +      using power_half_series summable_def apply auto[1]
    6.52 +      apply (auto simp add: divide_simps) using measure_nonneg[of M] not_less by fastforce
    6.53 +  qed
    6.54 +
    6.55 +  define f where "f = (\<lambda>x. if x \<in> space M then g x else 1)"
    6.56 +  have "f x > 0" for x unfolding f_def using g_pos by auto
    6.57 +  moreover have "f x \<le> 1" for x unfolding f_def using g_le_1 by auto
    6.58 +  moreover have [measurable]: "f \<in> borel_measurable M" unfolding f_def by auto
    6.59 +  moreover have "integrable M f"
    6.60 +    apply (subst integrable_cong[of _ _ _ g]) unfolding f_def using `integrable M g` by auto
    6.61 +  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"
    6.62 +    by (meson that)
    6.63 +qed
    6.64 +
    6.65  lemma (in sigma_finite_measure) Ex_finite_integrable_function:
    6.66    "\<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>)"
    6.67  proof -
    6.68 @@ -878,9 +936,6 @@
    6.69    finally show ?thesis by simp
    6.70  qed
    6.71  
    6.72 -lemma null_setsD_AE: "N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
    6.73 -  using AE_iff_null_sets[of N M] by auto
    6.74 -
    6.75  lemma (in sigma_finite_measure) RN_deriv_unique:
    6.76    assumes f: "f \<in> borel_measurable M"
    6.77    and eq: "density M f = N"
     7.1 --- a/src/HOL/Analysis/Set_Integral.thy	Mon Oct 17 15:20:06 2016 +0200
     7.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Thu Oct 13 18:36:06 2016 +0200
     7.3 @@ -1,5 +1,6 @@
     7.4  (*  Title:      HOL/Analysis/Set_Integral.thy
     7.5      Author:     Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU)
     7.6 +    Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     7.7  
     7.8  Notation and useful facts for working with integrals over a set.
     7.9  
    7.10 @@ -7,7 +8,7 @@
    7.11  *)
    7.12  
    7.13  theory Set_Integral
    7.14 -  imports Bochner_Integration
    7.15 +  imports Radon_Nikodym
    7.16  begin
    7.17  
    7.18  (*
    7.19 @@ -523,5 +524,235 @@
    7.20    shows "set_borel_measurable borel {a..b} f"
    7.21    by (rule set_borel_measurable_continuous[OF _ assms]) simp
    7.22  
    7.23 +
    7.24 +text{* This notation is from Sébastien Gouëzel: His use is not directly in line with the
    7.25 +notations in this file, they are more in line with sum, and more readable he thinks. *}
    7.26 +
    7.27 +abbreviation "set_nn_integral M A f \<equiv> nn_integral M (\<lambda>x. f x * indicator A x)"
    7.28 +
    7.29 +syntax
    7.30 +"_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
    7.31 +("(\<integral>\<^sup>+((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
    7.32 +
    7.33 +"_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal"
    7.34 +("(\<integral>((_)\<in>(_)./ _)/\<partial>_)" [0,60,110,61] 60)
    7.35 +
    7.36 +translations
    7.37 +"\<integral>\<^sup>+x \<in> A. f \<partial>M" == "CONST set_nn_integral M A (\<lambda>x. f)"
    7.38 +"\<integral>x \<in> A. f \<partial>M" == "CONST set_lebesgue_integral M A (\<lambda>x. f)"
    7.39 +
    7.40 +lemma nn_integral_disjoint_pair:
    7.41 +  assumes [measurable]: "f \<in> borel_measurable M"
    7.42 +          "B \<in> sets M" "C \<in> sets M"
    7.43 +          "B \<inter> C = {}"
    7.44 +  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)"
    7.45 +proof -
    7.46 +  have mes: "\<And>D. D \<in> sets M \<Longrightarrow> (\<lambda>x. f x * indicator D x) \<in> borel_measurable M" by simp
    7.47 +  have pos: "\<And>D. AE x in M. f x * indicator D x \<ge> 0" using assms(2) by auto
    7.48 +  have "\<And>x. f x * indicator (B \<union> C) x = f x * indicator B x + f x * indicator C x" using assms(4)
    7.49 +    by (auto split: split_indicator)
    7.50 +  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)"
    7.51 +    by simp
    7.52 +  also have "... = (\<integral>\<^sup>+x. f x * indicator B x \<partial>M) + (\<integral>\<^sup>+x. f x * indicator C x \<partial>M)"
    7.53 +    by (rule nn_integral_add) (auto simp add: assms mes pos)
    7.54 +  finally show ?thesis by simp
    7.55 +qed
    7.56 +
    7.57 +lemma nn_integral_disjoint_pair_countspace:
    7.58 +  assumes "B \<inter> C = {}"
    7.59 +  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)"
    7.60 +by (rule nn_integral_disjoint_pair) (simp_all add: assms)
    7.61 +
    7.62 +lemma nn_integral_null_delta:
    7.63 +  assumes "A \<in> sets M" "B \<in> sets M"
    7.64 +          "(A - B) \<union> (B - A) \<in> null_sets M"
    7.65 +  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> B. f x \<partial>M)"
    7.66 +proof (rule nn_integral_cong_AE, auto simp add: indicator_def)
    7.67 +  have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
    7.68 +    using assms(3) AE_not_in by blast
    7.69 +  then show "AE a in M. a \<notin> A \<longrightarrow> a \<in> B \<longrightarrow> f a = 0"
    7.70 +    by auto
    7.71 +  show "AE x\<in>A in M. x \<notin> B \<longrightarrow> f x = 0"
    7.72 +    using * by auto
    7.73 +qed
    7.74 +
    7.75 +lemma nn_integral_disjoint_family:
    7.76 +  assumes [measurable]: "f \<in> borel_measurable M" "\<And>(n::nat). B n \<in> sets M"
    7.77 +      and "disjoint_family B"
    7.78 +  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))"
    7.79 +proof -
    7.80 +  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))"
    7.81 +    by (rule nn_integral_suminf) simp
    7.82 +  moreover have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (\<Union>n. B n) x" for x
    7.83 +  proof (cases)
    7.84 +    assume "x \<in> (\<Union>n. B n)"
    7.85 +    then obtain n where "x \<in> B n" by blast
    7.86 +    have a: "finite {n}" by simp
    7.87 +    have "\<And>i. i \<noteq> n \<Longrightarrow> x \<notin> B i" using `x \<in> B n` assms(3) disjoint_family_on_def
    7.88 +      by (metis IntI UNIV_I empty_iff)
    7.89 +    then have "\<And>i. i \<notin> {n} \<Longrightarrow> indicator (B i) x = (0::ennreal)" using indicator_def by simp
    7.90 +    then have b: "\<And>i. i \<notin> {n} \<Longrightarrow> f x * indicator (B i) x = (0::ennreal)" by simp
    7.91 +
    7.92 +    define h where "h = (\<lambda>i. f x * indicator (B i) x)"
    7.93 +    then have "\<And>i. i \<notin> {n} \<Longrightarrow> h i = 0" using b by simp
    7.94 +    then have "(\<Sum>i. h i) = (\<Sum>i\<in>{n}. h i)"
    7.95 +      by (metis sums_unique[OF sums_finite[OF a]])
    7.96 +    then have "(\<Sum>i. h i) = h n" by simp
    7.97 +    then have "(\<Sum>n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp
    7.98 +    then have "(\<Sum>n. f x * indicator (B n) x) = f x" using `x \<in> B n` indicator_def by simp
    7.99 +    then show ?thesis using `x \<in> (\<Union>n. B n)` by auto
   7.100 +  next
   7.101 +    assume "x \<notin> (\<Union>n. B n)"
   7.102 +    then have "\<And>n. f x * indicator (B n) x = 0" by simp
   7.103 +    have "(\<Sum>n. f x * indicator (B n) x) = 0"
   7.104 +      by (simp add: `\<And>n. f x * indicator (B n) x = 0`)
   7.105 +    then show ?thesis using `x \<notin> (\<Union>n. B n)` by auto
   7.106 +  qed
   7.107 +  ultimately show ?thesis by simp
   7.108 +qed
   7.109 +
   7.110 +lemma nn_set_integral_add:
   7.111 +  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   7.112 +          "A \<in> sets M"
   7.113 +  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)"
   7.114 +proof -
   7.115 +  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)"
   7.116 +    by (auto simp add: indicator_def intro!: nn_integral_cong)
   7.117 +  also have "... = (\<integral>\<^sup>+x. f x * indicator A x \<partial>M) + (\<integral>\<^sup>+x. g x * indicator A x \<partial>M)"
   7.118 +    apply (rule nn_integral_add) using assms(1) assms(2) by auto
   7.119 +  finally show ?thesis by simp
   7.120 +qed
   7.121 +
   7.122 +lemma nn_set_integral_cong:
   7.123 +  assumes "AE x in M. f x = g x"
   7.124 +  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) = (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
   7.125 +apply (rule nn_integral_cong_AE) using assms(1) by auto
   7.126 +
   7.127 +lemma nn_set_integral_set_mono:
   7.128 +  "A \<subseteq> B \<Longrightarrow> (\<integral>\<^sup>+ x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+ x \<in> B. f x \<partial>M)"
   7.129 +by (auto intro!: nn_integral_mono split: split_indicator)
   7.130 +
   7.131 +lemma nn_set_integral_mono:
   7.132 +  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   7.133 +          "A \<in> sets M"
   7.134 +      and "AE x\<in>A in M. f x \<le> g x"
   7.135 +  shows "(\<integral>\<^sup>+x \<in> A. f x \<partial>M) \<le> (\<integral>\<^sup>+x \<in> A. g x \<partial>M)"
   7.136 +by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms)
   7.137 +
   7.138 +lemma nn_set_integral_space [simp]:
   7.139 +  shows "(\<integral>\<^sup>+ x \<in> space M. f x \<partial>M) = (\<integral>\<^sup>+x. f x \<partial>M)"
   7.140 +by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong)
   7.141 +
   7.142 +lemma nn_integral_count_compose_inj:
   7.143 +  assumes "inj_on g A"
   7.144 +  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)"
   7.145 +proof -
   7.146 +  have "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+x. f (g x) \<partial>count_space A)"
   7.147 +    by (auto simp add: nn_integral_count_space_indicator[symmetric])
   7.148 +  also have "... = (\<integral>\<^sup>+y. f y \<partial>count_space (g`A))"
   7.149 +    by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
   7.150 +  also have "... = (\<integral>\<^sup>+y \<in> g`A. f y \<partial>count_space UNIV)"
   7.151 +    by (auto simp add: nn_integral_count_space_indicator[symmetric])
   7.152 +  finally show ?thesis by simp
   7.153 +qed
   7.154 +
   7.155 +lemma nn_integral_count_compose_bij:
   7.156 +  assumes "bij_betw g A B"
   7.157 +  shows "(\<integral>\<^sup>+x \<in> A. f (g x) \<partial>count_space UNIV) = (\<integral>\<^sup>+y \<in> B. f y \<partial>count_space UNIV)"
   7.158 +proof -
   7.159 +  have "inj_on g A" using assms bij_betw_def by auto
   7.160 +  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)"
   7.161 +    by (rule nn_integral_count_compose_inj)
   7.162 +  then show ?thesis using assms by (simp add: bij_betw_def)
   7.163 +qed
   7.164 +
   7.165 +lemma set_integral_null_delta:
   7.166 +  fixes f::"_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   7.167 +  assumes [measurable]: "integrable M f" "A \<in> sets M" "B \<in> sets M"
   7.168 +    and "(A - B) \<union> (B - A) \<in> null_sets M"
   7.169 +  shows "(\<integral>x \<in> A. f x \<partial>M) = (\<integral>x \<in> B. f x \<partial>M)"
   7.170 +proof (rule set_integral_cong_set, auto)
   7.171 +  have *: "AE a in M. a \<notin> (A - B) \<union> (B - A)"
   7.172 +    using assms(4) AE_not_in by blast
   7.173 +  then show "AE x in M. (x \<in> B) = (x \<in> A)"
   7.174 +    by auto
   7.175 +qed
   7.176 +
   7.177 +lemma set_integral_space:
   7.178 +  assumes "integrable M f"
   7.179 +  shows "(\<integral>x \<in> space M. f x \<partial>M) = (\<integral>x. f x \<partial>M)"
   7.180 +by (metis (mono_tags, lifting) indicator_simps(1) Bochner_Integration.integral_cong real_vector.scale_one)
   7.181 +
   7.182 +lemma null_if_pos_func_has_zero_nn_int:
   7.183 +  fixes f::"'a \<Rightarrow> ennreal"
   7.184 +  assumes [measurable]: "f \<in> borel_measurable M" "A \<in> sets M"
   7.185 +    and "AE x\<in>A in M. f x > 0" "(\<integral>\<^sup>+x\<in>A. f x \<partial>M) = 0"
   7.186 +  shows "A \<in> null_sets M"
   7.187 +proof -
   7.188 +  have "AE x in M. f x * indicator A x = 0"
   7.189 +    by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4))
   7.190 +  then have "AE x\<in>A in M. False" using assms(3) by auto
   7.191 +  then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
   7.192 +qed
   7.193 +
   7.194 +lemma null_if_pos_func_has_zero_int:
   7.195 +  assumes [measurable]: "integrable M f" "A \<in> sets M"
   7.196 +      and "AE x\<in>A in M. f x > 0" "(\<integral>x\<in>A. f x \<partial>M) = (0::real)"
   7.197 +  shows "A \<in> null_sets M"
   7.198 +proof -
   7.199 +  have "AE x in M. indicator A x * f x = 0"
   7.200 +    apply (subst integral_nonneg_eq_0_iff_AE[symmetric])
   7.201 +    using assms integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
   7.202 +  then have "AE x\<in>A in M. f x = 0" by auto
   7.203 +  then have "AE x\<in>A in M. False" using assms(3) by auto
   7.204 +  then show "A \<in> null_sets M" using assms(2) by (simp add: AE_iff_null_sets)
   7.205 +qed
   7.206 +
   7.207 +text{*The next lemma is a variant of \<open>density_unique\<close>. Note that it uses the notation
   7.208 +for nonnegative set integrals introduced earlier.*}
   7.209 +
   7.210 +lemma (in sigma_finite_measure) density_unique2:
   7.211 +  assumes [measurable]: "f \<in> borel_measurable M" "f' \<in> borel_measurable M"
   7.212 +  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)"
   7.213 +  shows "AE x in M. f x = f' x"
   7.214 +proof (rule density_unique)
   7.215 +  show "density M f = density M f'"
   7.216 +    by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq)
   7.217 +qed (auto simp add: assms)
   7.218 +
   7.219 +
   7.220 +text {* The next lemma implies the same statement for Banach-space valued functions
   7.221 +using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I
   7.222 +only formulate it for real-valued functions.*}
   7.223 +
   7.224 +lemma density_unique_real:
   7.225 +  fixes f f'::"_ \<Rightarrow> real"
   7.226 +  assumes [measurable]: "integrable M f" "integrable M f'"
   7.227 +  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)"
   7.228 +  shows "AE x in M. f x = f' x"
   7.229 +proof -
   7.230 +  define A where "A = {x \<in> space M. f x < f' x}"
   7.231 +  then have [measurable]: "A \<in> sets M" by simp
   7.232 +  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)"
   7.233 +    using `A \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
   7.234 +  then have "(\<integral>x \<in> A. (f' x - f x) \<partial>M) = 0" using assms(3) by simp
   7.235 +  then have "A \<in> null_sets M"
   7.236 +    using A_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f' x - f x" and ?A = A] assms by auto
   7.237 +  then have "AE x in M. x \<notin> A" by (simp add: AE_not_in)
   7.238 +  then have *: "AE x in M. f' x \<le> f x" unfolding A_def by auto
   7.239 +
   7.240 +
   7.241 +  define B where "B = {x \<in> space M. f' x < f x}"
   7.242 +  then have [measurable]: "B \<in> sets M" by simp
   7.243 +  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)"
   7.244 +    using `B \<in> sets M` assms(1) assms(2) integrable_mult_indicator by blast
   7.245 +  then have "(\<integral>x \<in> B. (f x - f' x) \<partial>M) = 0" using assms(3) by simp
   7.246 +  then have "B \<in> null_sets M"
   7.247 +    using B_def null_if_pos_func_has_zero_int[where ?f = "\<lambda>x. f x - f' x" and ?A = B] assms by auto
   7.248 +  then have "AE x in M. x \<notin> B" by (simp add: AE_not_in)
   7.249 +  then have "AE x in M. f' x \<ge> f x" unfolding B_def by auto
   7.250 +
   7.251 +  then show ?thesis using * by auto
   7.252 +qed
   7.253 +
   7.254  end
   7.255 -
     8.1 --- a/src/HOL/Probability/Characteristic_Functions.thy	Mon Oct 17 15:20:06 2016 +0200
     8.2 +++ b/src/HOL/Probability/Characteristic_Functions.thy	Thu Oct 13 18:36:06 2016 +0200
     8.3 @@ -75,7 +75,7 @@
     8.4  lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
     8.5  proof -
     8.6    have "norm (char M t) \<le> (\<integral>x. norm (iexp (t * x)) \<partial>M)"
     8.7 -    unfolding char_def by (intro integral_norm_bound integrable_iexp) auto
     8.8 +    unfolding char_def by (intro integral_norm_bound)
     8.9    also have "\<dots> \<le> 1"
    8.10      by (simp del: of_real_mult)
    8.11    finally show ?thesis .
    8.12 @@ -318,7 +318,7 @@
    8.13    also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
    8.14      unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
    8.15    also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
    8.16 -    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp
    8.17 +    by (intro integral_norm_bound)
    8.18    also have "\<dots> \<le> expectation (\<lambda>x. 2 * \<bar>t\<bar> ^ n / fact n * \<bar>x\<bar> ^ n)"
    8.19    proof (rule integral_mono)
    8.20      show "integrable M (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k\<le>n. c k x)))"
    8.21 @@ -362,7 +362,7 @@
    8.22    also have "\<dots> = norm ((CLINT x | M. iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
    8.23      unfolding char_def by (subst Bochner_Integration.integral_diff[OF integ_iexp]) (auto intro!: integ_c)
    8.24    also have "\<dots> \<le> expectation (\<lambda>x. cmod (iexp (t * x) - (\<Sum>k \<le> n. c k x)))"
    8.25 -    by (intro integral_norm_bound Bochner_Integration.integrable_diff integ_iexp Bochner_Integration.integrable_sum integ_c) simp
    8.26 +    by (rule integral_norm_bound)
    8.27    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)))"
    8.28      (is "_ \<le> expectation ?f")
    8.29    proof (rule integral_mono)
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy	Thu Oct 13 18:36:06 2016 +0200
     9.3 @@ -0,0 +1,1340 @@
     9.4 +(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     9.5 +    License: BSD
     9.6 +*)
     9.7 +
     9.8 +section \<open>Conditional Expectation\<close>
     9.9 +
    9.10 +theory Conditional_Expectation
    9.11 +imports Probability_Measure
    9.12 +begin
    9.13 +
    9.14 +subsection {*Restricting a measure to a sub-sigma-algebra*}
    9.15 +
    9.16 +definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
    9.17 +  "subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))"
    9.18 +
    9.19 +lemma sub_measure_space:
    9.20 +  assumes i: "subalgebra M F"
    9.21 +  shows "measure_space (space M) (sets F) (emeasure M)"
    9.22 +proof -
    9.23 +  have "sigma_algebra (space M) (sets F)"
    9.24 +    by (metis i measure_space measure_space_def subalgebra_def)
    9.25 +  moreover have "positive (sets F) (emeasure M)"
    9.26 +    using Sigma_Algebra.positive_def by auto
    9.27 +  moreover have "countably_additive (sets F) (emeasure M)"
    9.28 +    by (meson countably_additive_def emeasure_countably_additive i order_trans subalgebra_def subsetCE)
    9.29 +  ultimately show ?thesis unfolding measure_space_def by simp
    9.30 +qed
    9.31 +
    9.32 +definition restr_to_subalg::"'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
    9.33 +  "restr_to_subalg M F = measure_of (space M) (sets F) (emeasure M)"
    9.34 +
    9.35 +lemma space_restr_to_subalg:
    9.36 +  "space (restr_to_subalg M F) = space M"
    9.37 +unfolding restr_to_subalg_def by (simp add: space_measure_of_conv)
    9.38 +
    9.39 +lemma sets_restr_to_subalg [measurable_cong]:
    9.40 +  assumes "subalgebra M F"
    9.41 +  shows "sets (restr_to_subalg M F) = sets F"
    9.42 +unfolding restr_to_subalg_def by (metis sets.sets_measure_of_eq assms subalgebra_def)
    9.43 +
    9.44 +lemma emeasure_restr_to_subalg:
    9.45 +  assumes "subalgebra M F"
    9.46 +          "A \<in> sets F"
    9.47 +  shows "emeasure (restr_to_subalg M F) A = emeasure M A"
    9.48 +unfolding restr_to_subalg_def
    9.49 +by (metis assms subalgebra_def emeasure_measure_of_conv sub_measure_space sets.sigma_sets_eq)
    9.50 +
    9.51 +lemma null_sets_restr_to_subalg:
    9.52 +  assumes "subalgebra M F"
    9.53 +  shows "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F"
    9.54 +proof
    9.55 +  have "x \<in> null_sets M \<inter> sets F" if "x \<in> null_sets (restr_to_subalg M F)" for x
    9.56 +    by (metis that Int_iff assms emeasure_restr_to_subalg null_setsD1 null_setsD2 null_setsI
    9.57 +        sets_restr_to_subalg subalgebra_def subsetD)
    9.58 +  then show "null_sets (restr_to_subalg M F) \<subseteq> null_sets M \<inter> sets F" by auto
    9.59 +next
    9.60 +  have "x \<in> null_sets (restr_to_subalg M F)" if "x \<in> null_sets M \<inter> sets F" for x
    9.61 +    by (metis that Int_iff assms null_setsD1 null_setsI sets_restr_to_subalg emeasure_restr_to_subalg[OF assms])
    9.62 +  then show "null_sets M \<inter> sets F \<subseteq> null_sets (restr_to_subalg M F)" by auto
    9.63 +qed
    9.64 +
    9.65 +lemma AE_restr_to_subalg:
    9.66 +  assumes "subalgebra M F"
    9.67 +          "AE x in (restr_to_subalg M F). P x"
    9.68 +  shows "AE x in M. P x"
    9.69 +proof -
    9.70 +  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)"
    9.71 +    using AE_E3[OF assms(2)] by auto
    9.72 +  then have "A \<in> null_sets M" using null_sets_restr_to_subalg[OF assms(1)] by auto
    9.73 +  moreover have "\<And>x. x \<in> space M - A \<Longrightarrow> P x"
    9.74 +    using space_restr_to_subalg A(1) by fastforce
    9.75 +  ultimately show ?thesis
    9.76 +    unfolding eventually_ae_filter by auto
    9.77 +qed
    9.78 +
    9.79 +lemma AE_restr_to_subalg2:
    9.80 +  assumes "subalgebra M F"
    9.81 +          "AE x in M. P x" and [measurable]: "P \<in> measurable F (count_space UNIV)"
    9.82 +  shows "AE x in (restr_to_subalg M F). P x"
    9.83 +proof -
    9.84 +  define U where "U = {x \<in> space M. \<not>(P x)}"
    9.85 +  then have *: "U = {x \<in> space F. \<not>(P x)}" using assms(1) by (simp add: subalgebra_def)
    9.86 +  then have "U \<in> sets F" by simp
    9.87 +  then have "U \<in> sets M" using assms(1) by (meson subalgebra_def subsetD)
    9.88 +  then have "U \<in> null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast
    9.89 +  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
    9.90 +  then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg)
    9.91 +qed
    9.92 +
    9.93 +lemma prob_space_restr_to_subalg:
    9.94 +  assumes "subalgebra M F"
    9.95 +          "prob_space M"
    9.96 +  shows "prob_space (restr_to_subalg M F)"
    9.97 +by (metis (no_types, lifting) assms(1) assms(2) emeasure_restr_to_subalg prob_space.emeasure_space_1 prob_spaceI
    9.98 +    sets.top space_restr_to_subalg subalgebra_def)
    9.99 +
   9.100 +lemma finite_measure_restr_to_subalg:
   9.101 +  assumes "subalgebra M F"
   9.102 +          "finite_measure M"
   9.103 +  shows "finite_measure (restr_to_subalg M F)"
   9.104 +by (metis (no_types, lifting) assms emeasure_restr_to_subalg finite_measure.finite_emeasure_space
   9.105 +    finite_measureI sets.top space_restr_to_subalg subalgebra_def infinity_ennreal_def)
   9.106 +
   9.107 +lemma measurable_in_subalg:
   9.108 +  assumes "subalgebra M F"
   9.109 +          "f \<in> measurable F N"
   9.110 +  shows "f \<in> measurable (restr_to_subalg M F) N"
   9.111 +by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
   9.112 +
   9.113 +lemma measurable_in_subalg':
   9.114 +  assumes "subalgebra M F"
   9.115 +          "f \<in> measurable (restr_to_subalg M F) N"
   9.116 +  shows "f \<in> measurable F N"
   9.117 +by (metis measurable_cong_sets assms(2) sets_restr_to_subalg[OF assms(1)])
   9.118 +
   9.119 +lemma measurable_from_subalg:
   9.120 +  assumes "subalgebra M F"
   9.121 +          "f \<in> measurable F N"
   9.122 +  shows "f \<in> measurable M N"
   9.123 +using assms unfolding measurable_def subalgebra_def by auto
   9.124 +
   9.125 +text{*The following is the direct transposition of \verb+nn_integral_subalgebra+
   9.126 +(from \verb+Nonnegative_Lebesgue_Integration+) in the
   9.127 +current notations, with the removal of the useless assumption $f \geq 0$.*}
   9.128 +
   9.129 +lemma nn_integral_subalgebra2:
   9.130 +  assumes "subalgebra M F" and [measurable]: "f \<in> borel_measurable F"
   9.131 +  shows "(\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. f x \<partial>M)"
   9.132 +proof (rule nn_integral_subalgebra)
   9.133 +  show "f \<in> borel_measurable (restr_to_subalg M F)"
   9.134 +    by (rule measurable_in_subalg[OF assms(1)]) simp
   9.135 +  show "sets (restr_to_subalg M F) \<subseteq> sets M" by (metis sets_restr_to_subalg[OF assms(1)] assms(1) subalgebra_def)
   9.136 +  fix A assume "A \<in> sets (restr_to_subalg M F)"
   9.137 +  then show "emeasure (restr_to_subalg M F) A = emeasure M A"
   9.138 +    by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)])
   9.139 +qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
   9.140 +
   9.141 +text{*The following is the direct transposition of \verb+integral_subalgebra+
   9.142 +(from \verb+Bochner_Integration+) in the current notations.*}
   9.143 +
   9.144 +lemma integral_subalgebra2:
   9.145 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.146 +  assumes "subalgebra M F" and
   9.147 +    [measurable]: "f \<in> borel_measurable F"
   9.148 +  shows "(\<integral>x. f x \<partial>(restr_to_subalg M F)) = (\<integral>x. f x \<partial>M)"
   9.149 +by (rule integral_subalgebra,
   9.150 +    metis measurable_in_subalg[OF assms(1)] assms(2),
   9.151 +    auto simp add: assms space_restr_to_subalg sets_restr_to_subalg emeasure_restr_to_subalg,
   9.152 +    meson assms(1) subalgebra_def subset_eq)
   9.153 +
   9.154 +lemma integrable_from_subalg:
   9.155 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.156 +  assumes "subalgebra M F"
   9.157 +          "integrable (restr_to_subalg M F) f"
   9.158 +  shows "integrable M f"
   9.159 +proof (rule integrableI_bounded)
   9.160 +  have [measurable]: "f \<in> borel_measurable F" using assms by auto
   9.161 +  then show "f \<in> borel_measurable M" using assms(1) measurable_from_subalg by blast
   9.162 +
   9.163 +  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F))"
   9.164 +    by (rule nn_integral_subalgebra2[symmetric], auto simp add: assms)
   9.165 +  also have "... < \<infinity>" using integrable_iff_bounded assms by auto
   9.166 +  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M) < \<infinity>" by simp
   9.167 +qed
   9.168 +
   9.169 +lemma integrable_in_subalg:
   9.170 +  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   9.171 +  assumes [measurable]: "subalgebra M F"
   9.172 +          "f \<in> borel_measurable F"
   9.173 +          "integrable M f"
   9.174 +  shows "integrable (restr_to_subalg M F) f"
   9.175 +proof (rule integrableI_bounded)
   9.176 +  show "f \<in> borel_measurable (restr_to_subalg M F)" using assms(2) assms(1) by auto
   9.177 +  have "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) = (\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>M)"
   9.178 +    by (rule nn_integral_subalgebra2, auto simp add: assms)
   9.179 +  also have "... < \<infinity>" using integrable_iff_bounded assms by auto
   9.180 +  finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) < \<infinity>" by simp
   9.181 +qed
   9.182 +
   9.183 +subsection {*Nonnegative conditional expectation*}
   9.184 +
   9.185 +text {* The conditional expectation of a function $f$, on a measure space $M$, with respect to a
   9.186 +sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any
   9.187 +$F$-set coincides with the integral of $f$.
   9.188 +Such a function is uniquely defined almost everywhere.
   9.189 +The most direct construction is to use the measure $f dM$, restrict it to the sigma-algebra $F$,
   9.190 +and apply the Radon-Nikodym theorem to write it as $g dM_{|F}$ for some $F$-measurable function $g$.
   9.191 +Another classical construction for $L^2$ functions is done by orthogonal projection on $F$-measurable
   9.192 +functions, and then extending by density to $L^1$. The Radon-Nikodym point of view avoids the $L^2$
   9.193 +machinery, and works for all positive functions.
   9.194 +
   9.195 +In this paragraph, we develop the definition and basic properties for nonnegative functions,
   9.196 +as the basics of the general case. As in the definition of integrals, the nonnegative case is done
   9.197 +with ennreal-valued functions, without any integrability assumption.
   9.198 +*}
   9.199 +
   9.200 +definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
   9.201 +where
   9.202 +  "nn_cond_exp M F f =
   9.203 +    (if f \<in> borel_measurable M \<and> subalgebra M F
   9.204 +        then RN_deriv (restr_to_subalg M F) (restr_to_subalg (density M f) F)
   9.205 +        else (\<lambda>_. 0))"
   9.206 +
   9.207 +lemma
   9.208 +  shows borel_measurable_nn_cond_exp [measurable]: "nn_cond_exp M F f \<in> borel_measurable F"
   9.209 +  and borel_measurable_nn_cond_exp2 [measurable]: "nn_cond_exp M F f \<in> borel_measurable M"
   9.210 +by (simp_all add: nn_cond_exp_def)
   9.211 +  (metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def)
   9.212 +
   9.213 +text {* The good setting for conditional expectations is the situation where the subalgebra $F$
   9.214 +gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
   9.215 +think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
   9.216 +conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
   9.217 +This means that a positive integrable function can have no meaningful conditional expectation.*}
   9.218 +
   9.219 +locale sigma_finite_subalgebra =
   9.220 +  fixes M F::"'a measure"
   9.221 +  assumes subalg: "subalgebra M F"
   9.222 +      and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
   9.223 +
   9.224 +lemma sigma_finite_subalgebra_is_sigma_finite:
   9.225 +  assumes "sigma_finite_subalgebra M F"
   9.226 +  shows "sigma_finite_measure M"
   9.227 +proof
   9.228 +  have subalg: "subalgebra M F"
   9.229 +   and sigma_fin_subalg: "sigma_finite_measure (restr_to_subalg M F)"
   9.230 +    using assms unfolding sigma_finite_subalgebra_def by auto
   9.231 +  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>)"
   9.232 +    using sigma_finite_measure.sigma_finite_countable[OF sigma_fin_subalg] by fastforce
   9.233 +  have "A \<subseteq> sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce
   9.234 +  then have "A \<subseteq> sets M" using subalg subalgebra_def by force
   9.235 +  moreover have "\<Union>A = space M" using Ap space_restr_to_subalg by simp
   9.236 +  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)
   9.237 +  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
   9.238 +qed
   9.239 +
   9.240 +sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure
   9.241 +using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
   9.242 +
   9.243 +text {* Conditional expectations are very often used in probability spaces. This is a special case
   9.244 +of the previous one, as we prove now. *}
   9.245 +
   9.246 +locale finite_measure_subalgebra = finite_measure +
   9.247 +  fixes F::"'a measure"
   9.248 +  assumes subalg: "subalgebra M F"
   9.249 +
   9.250 +lemma finite_measure_subalgebra_is_sigma_finite:
   9.251 +  assumes "finite_measure_subalgebra M F"
   9.252 +  shows "sigma_finite_subalgebra M F"
   9.253 +proof -
   9.254 +  interpret finite_measure_subalgebra M F using assms by simp
   9.255 +  have "finite_measure (restr_to_subalg M F)"
   9.256 +    using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
   9.257 +  then have "sigma_finite_measure (restr_to_subalg M F)"
   9.258 +    unfolding finite_measure_def by simp
   9.259 +  then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
   9.260 +qed
   9.261 +
   9.262 +sublocale finite_measure_subalgebra \<subseteq> sigma_finite_subalgebra
   9.263 +proof -
   9.264 +  have "finite_measure (restr_to_subalg M F)"
   9.265 +    using finite_measure_restr_to_subalg subalg finite_emeasure_space finite_measureI unfolding infinity_ennreal_def by blast
   9.266 +  then have "sigma_finite_measure (restr_to_subalg M F)"
   9.267 +    unfolding finite_measure_def by simp
   9.268 +  then show "sigma_finite_subalgebra M F" unfolding sigma_finite_subalgebra_def using subalg by simp
   9.269 +qed
   9.270 +
   9.271 +context sigma_finite_subalgebra
   9.272 +begin
   9.273 +
   9.274 +text{* The next lemma is arguably the most fundamental property of conditional expectation:
   9.275 +when computing an expectation against an $F$-measurable function, it is equivalent to work
   9.276 +with a function or with its $F$-conditional expectation.
   9.277 +
   9.278 +This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
   9.279 +From this point on, we will only work with it, and forget completely about
   9.280 +the definition using Radon-Nikodym derivatives.
   9.281 +*}
   9.282 +
   9.283 +lemma nn_cond_exp_intg:
   9.284 +  assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
   9.285 +  shows "(\<integral>\<^sup>+ x. f x * nn_cond_exp M F g x \<partial>M) = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
   9.286 +proof -
   9.287 +  have [measurable]: "f \<in> borel_measurable M"
   9.288 +    by (meson assms subalg borel_measurable_subalgebra subalgebra_def)
   9.289 +  have ac: "absolutely_continuous (restr_to_subalg M F) (restr_to_subalg (density M g) F)"
   9.290 +    unfolding absolutely_continuous_def
   9.291 +  proof -
   9.292 +    have "null_sets (restr_to_subalg M F) = null_sets M \<inter> sets F" by (rule null_sets_restr_to_subalg[OF subalg])
   9.293 +    moreover have "null_sets M \<subseteq> null_sets (density M g)"
   9.294 +      by (rule absolutely_continuousI_density[unfolded absolutely_continuous_def]) auto
   9.295 +    ultimately have "null_sets (restr_to_subalg M F) \<subseteq> null_sets (density M g) \<inter> sets F" by auto
   9.296 +    moreover have "null_sets (density M g) \<inter> sets F = null_sets (restr_to_subalg (density M g) F)"
   9.297 +      by (rule null_sets_restr_to_subalg[symmetric]) (metis subalg sets_density space_density subalgebra_def)
   9.298 +    ultimately show "null_sets (restr_to_subalg M F) \<subseteq> null_sets (restr_to_subalg (density M g) F)" by auto
   9.299 +  qed
   9.300 +
   9.301 +  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))"
   9.302 +    by (rule nn_integral_subalgebra2[symmetric]) (simp_all add: assms subalg)
   9.303 +  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))"
   9.304 +    unfolding nn_cond_exp_def using assms subalg by simp
   9.305 +  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))"
   9.306 +    by (simp add: mult.commute)
   9.307 +  also have "... = (\<integral>\<^sup>+ x. f x \<partial>(restr_to_subalg (density M g) F))"
   9.308 +  proof (rule sigma_finite_measure.RN_deriv_nn_integral[symmetric])
   9.309 +    show "sets (restr_to_subalg (density M g) F) = sets (restr_to_subalg M F)"
   9.310 +      by (metis subalg restr_to_subalg_def sets.sets_measure_of_eq space_density subalgebra_def)
   9.311 +  qed (auto simp add: assms measurable_restrict ac measurable_in_subalg subalg sigma_fin_subalg)
   9.312 +  also have "... = (\<integral>\<^sup>+ x. f x \<partial>(density M g))"
   9.313 +    by (metis nn_integral_subalgebra2 subalg assms(1) sets_density space_density subalgebra_def)
   9.314 +  also have "... = (\<integral>\<^sup>+ x. g x * f x \<partial>M)"
   9.315 +    by (rule nn_integral_density) (simp_all add: assms)
   9.316 +  also have "... = (\<integral>\<^sup>+ x. f x * g x \<partial>M)"
   9.317 +    by (simp add: mult.commute)
   9.318 +  finally show ?thesis by simp
   9.319 +qed
   9.320 +
   9.321 +lemma nn_cond_exp_charact:
   9.322 +  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
   9.323 +          [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable F"
   9.324 +  shows "AE x in M. g x = nn_cond_exp M F f x"
   9.325 +proof -
   9.326 +  let ?MF = "restr_to_subalg M F"
   9.327 +  {
   9.328 +    fix A assume "A \<in> sets ?MF"
   9.329 +    then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
   9.330 +    have "(\<integral>\<^sup>+ x \<in> A. g x \<partial> ?MF) = (\<integral>\<^sup>+ x \<in> A. g x \<partial>M)"
   9.331 +      by (simp add: nn_integral_subalgebra2 subalg)
   9.332 +    also have "... = (\<integral>\<^sup>+ x \<in> A. f x \<partial>M)" using assms(1) by simp
   9.333 +    also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
   9.334 +    also have "... = (\<integral>\<^sup>+ x. indicator A x * nn_cond_exp M F f x \<partial>M)"
   9.335 +      by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
   9.336 +    also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
   9.337 +    also have "... = (\<integral>\<^sup>+ x \<in> A. nn_cond_exp M F f x \<partial> ?MF)"
   9.338 +      by (simp add: nn_integral_subalgebra2 subalg)
   9.339 +    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
   9.340 +  } note * = this
   9.341 +  have "AE x in ?MF. g x = nn_cond_exp M F f x"
   9.342 +    by (rule sigma_finite_measure.density_unique2)
   9.343 +       (auto simp add: assms subalg sigma_fin_subalg AE_restr_to_subalg2 *)
   9.344 +  then show ?thesis using AE_restr_to_subalg[OF subalg] by simp
   9.345 +qed
   9.346 +
   9.347 +lemma nn_cond_exp_F_meas:
   9.348 +  assumes "f \<in> borel_measurable F"
   9.349 +  shows "AE x in M. f x = nn_cond_exp M F f x"
   9.350 +by (rule nn_cond_exp_charact) (auto simp add: assms measurable_from_subalg[OF subalg])
   9.351 +
   9.352 +lemma nn_cond_exp_prod:
   9.353 +  assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
   9.354 +  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"
   9.355 +proof (rule nn_cond_exp_charact)
   9.356 +  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(1)])
   9.357 +  show "(\<lambda>x. f x * g x) \<in> borel_measurable M" by measurable
   9.358 +
   9.359 +  fix A assume "A \<in> sets F"
   9.360 +  then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
   9.361 +  have "\<integral>\<^sup>+x\<in>A. (f x * g x) \<partial>M = \<integral>\<^sup>+x. (f x * indicator A x) * g x \<partial>M"
   9.362 +    by (simp add: mult.commute mult.left_commute)
   9.363 +  also have "... = \<integral>\<^sup>+x. (f x * indicator A x) * nn_cond_exp M F g x \<partial>M"
   9.364 +    by (rule nn_cond_exp_intg[symmetric]) (auto simp add: assms)
   9.365 +  also have "... = \<integral>\<^sup>+x\<in>A. (f x * nn_cond_exp M F g x)\<partial>M"
   9.366 +    by (simp add: mult.commute mult.left_commute)
   9.367 +  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
   9.368 +qed (auto simp add: assms)
   9.369 +
   9.370 +lemma nn_cond_exp_sum:
   9.371 +  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   9.372 +  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"
   9.373 +proof (rule nn_cond_exp_charact)
   9.374 +  fix A assume [measurable]: "A \<in> sets F"
   9.375 +  then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
   9.376 +  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)"
   9.377 +    by (rule nn_set_integral_add) (auto simp add: assms `A \<in> sets M`)
   9.378 +  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)"
   9.379 +    by (metis (no_types, lifting) mult.commute nn_integral_cong)
   9.380 +  also have "... = (\<integral>\<^sup>+x. indicator A x * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * g x \<partial>M)"
   9.381 +    by (simp add: nn_cond_exp_intg)
   9.382 +  also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
   9.383 +    by (metis (no_types, lifting) mult.commute nn_integral_cong)
   9.384 +  also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
   9.385 +    by (rule nn_set_integral_add[symmetric]) (auto simp add: assms `A \<in> sets M`)
   9.386 +  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"
   9.387 +    by simp
   9.388 +qed (auto simp add: assms)
   9.389 +
   9.390 +lemma nn_cond_exp_cong:
   9.391 +  assumes "AE x in M. f x = g x"
   9.392 +      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   9.393 +  shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F g x"
   9.394 +proof (rule nn_cond_exp_charact)
   9.395 +  fix A assume [measurable]: "A \<in> sets F"
   9.396 +  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"
   9.397 +    by (simp add: mult.commute)
   9.398 +  also have "... = \<integral>\<^sup>+x. indicator A x * f x \<partial>M" by (simp add: nn_cond_exp_intg assms)
   9.399 +  also have "... = \<integral>\<^sup>+x\<in>A. f x \<partial>M" by (simp add: mult.commute)
   9.400 +  also have "... = \<integral>\<^sup>+x\<in>A. g x \<partial>M" by (rule nn_set_integral_cong[OF assms(1)])
   9.401 +  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
   9.402 +qed (auto simp add: assms)
   9.403 +
   9.404 +lemma nn_cond_exp_mono:
   9.405 +  assumes "AE x in M. f x \<le> g x"
   9.406 +      and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   9.407 +  shows "AE x in M. nn_cond_exp M F f x \<le> nn_cond_exp M F g x"
   9.408 +proof -
   9.409 +  define h where "h = (\<lambda>x. g x - f x)"
   9.410 +  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
   9.411 +  have *: "AE x in M. g x = f x + h x" unfolding h_def using assms(1) by (auto simp: ennreal_ineq_diff_add)
   9.412 +  have "AE x in M. nn_cond_exp M F g x = nn_cond_exp M F (\<lambda>x. f x + h x) x"
   9.413 +    by (rule nn_cond_exp_cong) (auto simp add: * assms)
   9.414 +  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"
   9.415 +    by (rule nn_cond_exp_sum) (auto simp add: assms)
   9.416 +  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
   9.417 +  then show ?thesis by force
   9.418 +qed
   9.419 +
   9.420 +lemma nested_subalg_is_sigma_finite:
   9.421 +  assumes "subalgebra M G" "subalgebra G F"
   9.422 +  shows "sigma_finite_subalgebra M G"
   9.423 +unfolding sigma_finite_subalgebra_def
   9.424 +proof (auto simp add: assms)
   9.425 +  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>)"
   9.426 +    using sigma_fin_subalg sigma_finite_measure_def by auto
   9.427 +  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>)"
   9.428 +    by auto
   9.429 +  have "sets F \<subseteq> sets M"
   9.430 +    by (meson assms order_trans subalgebra_def)
   9.431 +  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>)"
   9.432 +    by (metis (no_types) A assms basic_trans_rules(31) emeasure_restr_to_subalg order_trans sets_restr_to_subalg subalgebra_def)
   9.433 +  then show "sigma_finite_measure (restr_to_subalg M G)"
   9.434 +    by (metis sigma_finite_measure.intro space_restr_to_subalg)
   9.435 +qed
   9.436 +
   9.437 +lemma nn_cond_exp_nested_subalg:
   9.438 +  assumes "subalgebra M G" "subalgebra G F"
   9.439 +    and [measurable]: "f \<in> borel_measurable M"
   9.440 +  shows "AE x in M. nn_cond_exp M F f x = nn_cond_exp M F (nn_cond_exp M G f) x"
   9.441 +proof (rule nn_cond_exp_charact, auto)
   9.442 +  interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
   9.443 +  fix A assume [measurable]: "A \<in> sets F"
   9.444 +  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
   9.445 +
   9.446 +  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)"
   9.447 +    by (metis (no_types) mult.commute)
   9.448 +  also have "... = (\<integral>\<^sup>+ x. indicator A x * f x \<partial>M)" by (rule G.nn_cond_exp_intg, auto simp add: assms)
   9.449 +  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)
   9.450 +  also have "... = set_nn_integral M A (nn_cond_exp M F f)" by (metis (no_types) mult.commute)
   9.451 +  finally show "set_nn_integral M A (nn_cond_exp M G f) = set_nn_integral M A (nn_cond_exp M F f)".
   9.452 +qed
   9.453 +
   9.454 +end
   9.455 +
   9.456 +subsection {*Real conditional expectation*}
   9.457 +
   9.458 +text {*Once conditional expectations of positive functions are defined, the definition for real-valued functions
   9.459 +follows readily, by taking the difference of positive and negative parts.
   9.460 +One could also define a conditional expectation of vector-space valued functions, as in
   9.461 +\verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I
   9.462 +concentrate on it. (It is also essential for the case of the most general Pettis integral.)
   9.463 +*}
   9.464 +
   9.465 +definition real_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where
   9.466 +  "real_cond_exp M F f =
   9.467 +    (\<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))"
   9.468 +
   9.469 +lemma
   9.470 +  shows borel_measurable_cond_exp [measurable]: "real_cond_exp M F f \<in> borel_measurable F"
   9.471 +  and borel_measurable_cond_exp2 [measurable]: "real_cond_exp M F f \<in> borel_measurable M"
   9.472 +unfolding real_cond_exp_def by auto
   9.473 +
   9.474 +context sigma_finite_subalgebra
   9.475 +begin
   9.476 +
   9.477 +lemma real_cond_exp_abs:
   9.478 +  assumes [measurable]: "f \<in> borel_measurable M"
   9.479 +  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"
   9.480 +proof -
   9.481 +  define fp where "fp = (\<lambda>x. ennreal (f x))"
   9.482 +  define fm where "fm = (\<lambda>x. ennreal (- f x))"
   9.483 +  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M" unfolding fp_def fm_def by auto
   9.484 +  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)
   9.485 +
   9.486 +  {
   9.487 +    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"
   9.488 +    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>"
   9.489 +      unfolding real_cond_exp_def fp_def fm_def by (auto intro: abs_triangle_ineq4 simp del: enn2real_nonneg)
   9.490 +    from ennreal_leI[OF this]
   9.491 +    have "abs(real_cond_exp M F f x) \<le> nn_cond_exp M F fp x + nn_cond_exp M F fm x"
   9.492 +      by simp (metis add.commute ennreal_enn2real le_iff_add not_le top_unique)
   9.493 +    also have "... = nn_cond_exp M F (\<lambda>x. fp x + fm x) x" using H by simp
   9.494 +    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
   9.495 +  }
   9.496 +  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"
   9.497 +    by (rule nn_cond_exp_sum) (auto simp add: fp_def fm_def)
   9.498 +  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"
   9.499 +    by auto
   9.500 +  then show ?thesis using eq by simp
   9.501 +qed
   9.502 +
   9.503 +text{* The next lemma shows that the conditional expectation
   9.504 +is an $F$-measurable function whose average against an $F$-measurable
   9.505 +function $f$ coincides with the average of the original function against $f$.
   9.506 +It is obtained as a consequence of the same property for the positive conditional
   9.507 +expectation, taking the difference of the positive and the negative part. The proof
   9.508 +is given first assuming $f \geq 0$ for simplicity, and then extended to the general case in
   9.509 +the subsequent lemma. The idea of the proof is essentially trivial, but the implementation
   9.510 +is slightly tedious as one should check all the integrability properties of the different parts, and go
   9.511 +back and forth between positive integral and signed integrals, and between real-valued
   9.512 +functions and ennreal-valued functions.
   9.513 +
   9.514 +Once this lemma is available, we will use it to characterize the conditional expectation,
   9.515 +and never come back to the original technical definition, as we did in the case of the
   9.516 +nonnegative conditional expectation.
   9.517 +*}
   9.518 +
   9.519 +lemma real_cond_exp_intg_fpos:
   9.520 +  assumes "integrable M (\<lambda>x. f x * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
   9.521 +          [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
   9.522 +  shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
   9.523 +        "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)"
   9.524 +proof -
   9.525 +  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(3)])
   9.526 +  define gp where "gp = (\<lambda>x. ennreal (g x))"
   9.527 +  define gm where "gm = (\<lambda>x. ennreal (- g x))"
   9.528 +  have [measurable]: "gp \<in> borel_measurable M" "gm \<in> borel_measurable M" unfolding gp_def gm_def by auto
   9.529 +  define h where "h = (\<lambda>x. ennreal(abs(g x)))"
   9.530 +  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)
   9.531 +  have [measurable]: "h \<in> borel_measurable M" unfolding h_def by simp
   9.532 +  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
   9.533 +  have gp_real: "\<And>x. enn2real(gp x) = max (g x) 0"
   9.534 +    unfolding gp_def by (simp add: max_def ennreal_neg)
   9.535 +  have gm_real: "\<And>x. enn2real(gm x) = max (-g x) 0"
   9.536 +    unfolding gm_def by (simp add: max_def ennreal_neg)
   9.537 +
   9.538 +  have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
   9.539 +    by (simp add: nn_integral_mono)
   9.540 +  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
   9.541 +  finally have "(\<integral>\<^sup>+ x. norm(f x * max (g x) 0) \<partial>M) < \<infinity>" by simp
   9.542 +  then have int1: "integrable M (\<lambda>x. f x * max (g x) 0)" by (simp add: integrableI_bounded)
   9.543 +
   9.544 +  have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
   9.545 +    by (simp add: nn_integral_mono)
   9.546 +  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
   9.547 +  finally have "(\<integral>\<^sup>+ x. norm(f x * max (-g x) 0) \<partial>M) < \<infinity>" by simp
   9.548 +  then have int2: "integrable M (\<lambda>x. f x * max (-g x) 0)" by (simp add: integrableI_bounded)
   9.549 +
   9.550 +  have "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) = (\<integral>\<^sup>+x. f x * h x \<partial>M)"
   9.551 +    by (rule nn_cond_exp_intg) auto
   9.552 +  also have "\<dots> = \<integral>\<^sup>+ x. ennreal (f x * max (g x) 0 + f x * max (- g x) 0) \<partial>M"
   9.553 +    unfolding h_def
   9.554 +    by (intro nn_integral_cong)(auto simp: ennreal_mult[symmetric] abs_mult split: split_max)
   9.555 +  also have "... < \<infinity>"
   9.556 +    using Bochner_Integration.integrable_add[OF int1 int2, THEN integrableD(2)] by (auto simp add: less_top)
   9.557 +  finally have *: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M) < \<infinity>" by simp
   9.558 +
   9.559 +  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)"
   9.560 +    by (simp add: abs_mult)
   9.561 +  also have "... \<le> (\<integral>\<^sup>+x. f x * nn_cond_exp M F h x \<partial>M)"
   9.562 +  proof (rule nn_integral_mono_AE)
   9.563 +    {
   9.564 +      fix x assume *: "abs(real_cond_exp M F g x) \<le> nn_cond_exp M F h x"
   9.565 +      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>)"
   9.566 +        by (simp add: ennreal_mult)
   9.567 +      also have "... \<le> f x * nn_cond_exp M F h x"
   9.568 +        using * by (auto intro!: mult_left_mono)
   9.569 +      finally have "ennreal (f x * \<bar>real_cond_exp M F g x\<bar>) \<le> f x * nn_cond_exp M F h x"
   9.570 +        by simp
   9.571 +    }
   9.572 +    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"
   9.573 +      using real_cond_exp_abs[OF assms(4)] h_def by auto
   9.574 +  qed
   9.575 +  finally have **: "(\<integral>\<^sup>+x. norm(f x * real_cond_exp M F g x) \<partial>M) < \<infinity>" using * by auto
   9.576 +  show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
   9.577 +    using ** by (intro integrableI_bounded) auto
   9.578 +
   9.579 +
   9.580 +  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)"
   9.581 +  proof (rule nn_integral_mono_AE)
   9.582 +    have "AE x in M. nn_cond_exp M F gp x \<le> nn_cond_exp M F h x"
   9.583 +      by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
   9.584 +    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"
   9.585 +      by (auto simp: mult_left_mono)
   9.586 +  qed
   9.587 +  then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gp x \<partial>M) < \<infinity>"
   9.588 +    using * by auto
   9.589 +  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
   9.590 +    by (auto simp add: ennreal_mult intro!: mult_left_mono)
   9.591 +       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
   9.592 +  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)"
   9.593 +    by (simp add: nn_integral_mono)
   9.594 +  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gp x)) \<partial>M) < \<infinity>" using a by auto
   9.595 +  then have gp_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gp x))" by (simp add: integrableI_bounded)
   9.596 +  have gp_fin: "AE x in M. f x * nn_cond_exp M F gp x \<noteq> \<infinity>"
   9.597 +    apply (rule nn_integral_PInf_AE) using a by auto
   9.598 +
   9.599 +  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)"
   9.600 +    by (rule integral_eq_nn_integral) auto
   9.601 +  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)"
   9.602 +  proof -
   9.603 +    {
   9.604 +      fix x assume "f x * nn_cond_exp M F gp x \<noteq> \<infinity>"
   9.605 +      then have "ennreal (f x * enn2real (nn_cond_exp M F gp x)) = ennreal (f x) * nn_cond_exp M F gp x"
   9.606 +        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
   9.607 +    }
   9.608 +    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"
   9.609 +      using gp_fin by auto
   9.610 +    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)"
   9.611 +      by (rule nn_integral_cong_AE)
   9.612 +    also have "... = (\<integral>\<^sup>+ x. f x * gp x \<partial>M)"
   9.613 +      by (rule nn_cond_exp_intg) (auto simp add: gp_def)
   9.614 +    also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gp x)) \<partial>M)"
   9.615 +      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gp_def)
   9.616 +    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
   9.617 +    then show ?thesis by simp
   9.618 +  qed
   9.619 +  also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M)"
   9.620 +    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gp_def)
   9.621 +  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
   9.622 +
   9.623 +
   9.624 +  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)"
   9.625 +  proof (rule nn_integral_mono_AE)
   9.626 +    have "AE x in M. nn_cond_exp M F gm x \<le> nn_cond_exp M F h x"
   9.627 +      by (rule nn_cond_exp_mono) (auto simp add: hgpgm)
   9.628 +    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"
   9.629 +      by (auto simp: mult_left_mono)
   9.630 +  qed
   9.631 +  then have a: "(\<integral>\<^sup>+x. f x * nn_cond_exp M F gm x \<partial>M) < \<infinity>"
   9.632 +    using * by auto
   9.633 +  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"
   9.634 +    by (auto simp add: ennreal_mult intro!: mult_left_mono)
   9.635 +       (metis enn2real_ennreal enn2real_nonneg le_cases le_ennreal_iff)
   9.636 +  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)"
   9.637 +    by (simp add: nn_integral_mono)
   9.638 +  then have "(\<integral>\<^sup>+x. norm(f x * enn2real(nn_cond_exp M F gm x)) \<partial>M) < \<infinity>" using a by auto
   9.639 +  then have gm_int: "integrable M (\<lambda>x. f x * enn2real(nn_cond_exp M F gm x))" by (simp add: integrableI_bounded)
   9.640 +  have gm_fin: "AE x in M. f x * nn_cond_exp M F gm x \<noteq> \<infinity>"
   9.641 +    apply (rule nn_integral_PInf_AE) using a by auto
   9.642 +
   9.643 +  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)"
   9.644 +    by (rule integral_eq_nn_integral) auto
   9.645 +  also have "... = enn2real(\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)"
   9.646 +  proof -
   9.647 +    {
   9.648 +      fix x assume "f x * nn_cond_exp M F gm x \<noteq> \<infinity>"
   9.649 +      then have "ennreal (f x * enn2real (nn_cond_exp M F gm x)) = ennreal (f x) * nn_cond_exp M F gm x"
   9.650 +        by (auto simp add: ennreal_mult ennreal_mult_eq_top_iff less_top intro!: ennreal_mult_left_cong)
   9.651 +    }
   9.652 +    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"
   9.653 +      using gm_fin by auto
   9.654 +    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)"
   9.655 +      by (rule nn_integral_cong_AE)
   9.656 +    also have "... = (\<integral>\<^sup>+ x. f x * gm x \<partial>M)"
   9.657 +      by (rule nn_cond_exp_intg) (auto simp add: gm_def)
   9.658 +    also have "... = (\<integral>\<^sup>+ x. ennreal(f x * enn2real(gm x)) \<partial>M)"
   9.659 +      by (rule nn_integral_cong_AE) (auto simp: ennreal_mult gm_def)
   9.660 +    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
   9.661 +    then show ?thesis by simp
   9.662 +  qed
   9.663 +  also have "... = (\<integral> x. f x * enn2real(gm x) \<partial>M)"
   9.664 +    by (rule integral_eq_nn_integral[symmetric]) (auto simp add: gm_def)
   9.665 +  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
   9.666 +
   9.667 +
   9.668 +  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)"
   9.669 +    unfolding real_cond_exp_def gp_def gm_def by (simp add: right_diff_distrib)
   9.670 +  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)"
   9.671 +    by (rule Bochner_Integration.integral_diff) (simp_all add: gp_int gm_int)
   9.672 +  also have "... = (\<integral> x. f x * enn2real(gp x) \<partial>M) - (\<integral> x. f x * enn2real(gm x) \<partial>M)"
   9.673 +    using gp_expr gm_expr by simp
   9.674 +  also have "... = (\<integral> x. f x * max (g x) 0 \<partial>M) - (\<integral> x. f x * max (-g x) 0 \<partial>M)"
   9.675 +    using gp_real gm_real by simp
   9.676 +  also have "... = (\<integral> x. f x * max (g x) 0 - f x * max (-g x) 0 \<partial>M)"
   9.677 +    by (rule Bochner_Integration.integral_diff[symmetric]) (simp_all add: int1 int2)
   9.678 +  also have "... = (\<integral>x. f x * g x \<partial>M)"
   9.679 +    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)
   9.680 +  finally show "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral>x. f x * g x \<partial>M)"
   9.681 +    by simp
   9.682 +qed
   9.683 +
   9.684 +lemma real_cond_exp_intg:
   9.685 +  assumes "integrable M (\<lambda>x. f x * g x)" and
   9.686 +          [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
   9.687 +  shows "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
   9.688 +        "(\<integral> x. f x * real_cond_exp M F g x \<partial>M) = (\<integral> x. f x * g x \<partial>M)"
   9.689 +proof -
   9.690 +  have [measurable]: "f \<in> borel_measurable M" by (rule measurable_from_subalg[OF subalg assms(2)])
   9.691 +  define fp where "fp = (\<lambda>x. max (f x) 0)"
   9.692 +  define fm where "fm = (\<lambda>x. max (-f x) 0)"
   9.693 +  have [measurable]: "fp \<in> borel_measurable M" "fm \<in> borel_measurable M"
   9.694 +    unfolding fp_def fm_def by simp_all
   9.695 +  have [measurable]: "fp \<in> borel_measurable F" "fm \<in> borel_measurable F"
   9.696 +    unfolding fp_def fm_def by simp_all
   9.697 +
   9.698 +  have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
   9.699 +    by (simp add: fp_def nn_integral_mono)
   9.700 +  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
   9.701 +  finally have "(\<integral>\<^sup>+ x. norm(fp x * g x) \<partial>M) < \<infinity>" by simp
   9.702 +  then have intp: "integrable M (\<lambda>x. fp x * g x)" by (simp add: integrableI_bounded)
   9.703 +  moreover have "\<And>x. fp x \<ge> 0" unfolding fp_def by simp
   9.704 +  ultimately have Rp: "integrable M (\<lambda>x. fp x * real_cond_exp M F g x)"
   9.705 +    "(\<integral> x. fp x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fp x * g x \<partial>M)"
   9.706 +  using real_cond_exp_intg_fpos by auto
   9.707 +
   9.708 +  have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) \<le> (\<integral>\<^sup>+ x. norm(f x * g x) \<partial>M)"
   9.709 +    by (simp add: fm_def nn_integral_mono)
   9.710 +  also have "... < \<infinity>" using assms(1) by (simp add: integrable_iff_bounded)
   9.711 +  finally have "(\<integral>\<^sup>+ x. norm(fm x * g x) \<partial>M) < \<infinity>" by simp
   9.712 +  then have intm: "integrable M (\<lambda>x. fm x * g x)" by (simp add: integrableI_bounded)
   9.713 +  moreover have "\<And>x. fm x \<ge> 0" unfolding fm_def by simp
   9.714 +  ultimately have Rm: "integrable M (\<lambda>x. fm x * real_cond_exp M F g x)"
   9.715 +    "(\<integral> x. fm x * real_cond_exp M F g x \<partial>M) = (\<integral> x. fm x * g x \<partial>M)"
   9.716 +  using real_cond_exp_intg_fpos by auto
   9.717 +
   9.718 +  have "integrable M (\<lambda>x. fp x * real_cond_exp M F g x - fm x * real_cond_exp M F g x)"
   9.719 +    using Rp(1) Rm(1) integrable_diff by simp
   9.720 +  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"
   9.721 +    unfolding fp_def fm_def by (simp add: max_def)
   9.722 +  ultimately show "integrable M (\<lambda>x. f x * real_cond_exp M F g x)"
   9.723 +    by simp
   9.724 +
   9.725 +  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)"
   9.726 +    using * by simp
   9.727 +  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)"
   9.728 +    using Rp(1) Rm(1) by simp
   9.729 +  also have "... = (\<integral> x. fp x * g x \<partial>M) - (\<integral> x. fm x * g x \<partial>M)"
   9.730 +    using Rp(2) Rm(2) by simp
   9.731 +  also have "... = (\<integral> x. fp x * g x - fm x * g x \<partial>M)"
   9.732 +    using intm intp by simp
   9.733 +  also have "... = (\<integral> x. f x * g x \<partial>M)"
   9.734 +    unfolding fp_def fm_def by (metis (no_types, hide_lams) diff_0 diff_zero max.commute
   9.735 +    max_def minus_minus mult.commute neg_le_iff_le right_diff_distrib)
   9.736 +  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
   9.737 +qed
   9.738 +
   9.739 +lemma real_cond_exp_intA:
   9.740 +  assumes [measurable]: "integrable M f" "A \<in> sets F"
   9.741 +  shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)"
   9.742 +proof -
   9.743 +  have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
   9.744 +  have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
   9.745 +  then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
   9.746 +qed
   9.747 +
   9.748 +lemma real_cond_exp_int [intro]:
   9.749 +  assumes "integrable M f"
   9.750 +  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)"
   9.751 +using real_cond_exp_intg[where ?f = "\<lambda>x. 1" and ?g = f] assms by auto
   9.752 +
   9.753 +lemma real_cond_exp_charact:
   9.754 +  assumes "\<And>A. A \<in> sets F \<Longrightarrow> (\<integral> x \<in> A. f x \<partial>M) = (\<integral> x \<in> A. g x \<partial>M)"
   9.755 +      and [measurable]: "integrable M f" "integrable M g"
   9.756 +          "g \<in> borel_measurable F"
   9.757 +  shows "AE x in M. real_cond_exp M F f x = g x"
   9.758 +proof -
   9.759 +  let ?MF = "restr_to_subalg M F"
   9.760 +  have "AE x in ?MF. real_cond_exp M F f x = g x"
   9.761 +  proof (rule AE_symmetric[OF density_unique_real])
   9.762 +    fix A assume "A \<in> sets ?MF"
   9.763 +    then have [measurable]: "A \<in> sets F" using sets_restr_to_subalg[OF subalg] by simp
   9.764 +    then have a [measurable]: "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
   9.765 +    have "(\<integral>x \<in> A. g x \<partial> ?MF) = (\<integral>x \<in> A. g x \<partial>M)"
   9.766 +      by (simp add: integral_subalgebra2 subalg)
   9.767 +    also have "... = (\<integral>x \<in> A. f x \<partial>M)" using assms(1) by simp
   9.768 +    also have "... = (\<integral>x. indicator A x * f x \<partial>M)" by (simp add: mult.commute)
   9.769 +    also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M)"
   9.770 +      apply (rule real_cond_exp_intg(2)[symmetric]) using integrable_mult_indicator[OF a assms(2)] by (auto simp add: assms)
   9.771 +    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)" by (simp add: mult.commute)
   9.772 +    also have "... = (\<integral>x \<in> A. real_cond_exp M F f x \<partial> ?MF)"
   9.773 +      by (simp add: integral_subalgebra2 subalg)
   9.774 +    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
   9.775 +  next
   9.776 +    have "integrable M (real_cond_exp M F f)" by (rule real_cond_exp_int(1)[OF assms(2)])
   9.777 +    then show "integrable ?MF (real_cond_exp M F f)" by (metis borel_measurable_cond_exp integrable_in_subalg[OF subalg])
   9.778 +    show "integrable (restr_to_subalg M F) g" by (simp add: assms(3) integrable_in_subalg[OF subalg])
   9.779 +  qed
   9.780 +  then show ?thesis using AE_restr_to_subalg[OF subalg] by auto
   9.781 +qed
   9.782 +
   9.783 +lemma real_cond_exp_F_meas [intro, simp]:
   9.784 +  assumes "integrable M f"
   9.785 +          "f \<in> borel_measurable F"
   9.786 +  shows "AE x in M. real_cond_exp M F f x = f x"
   9.787 +by (rule real_cond_exp_charact, auto simp add: assms measurable_from_subalg[OF subalg])
   9.788 +
   9.789 +lemma real_cond_exp_mult:
   9.790 +  assumes [measurable]:"f \<in> borel_measurable F" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f x * g x)"
   9.791 +  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"
   9.792 +proof (rule real_cond_exp_charact)
   9.793 +  fix A assume "A \<in> sets F"
   9.794 +  then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
   9.795 +  have [measurable]: "A \<in> sets M" using subalg by (meson `A \<in> sets F` subalgebra_def subsetD)
   9.796 +  have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
   9.797 +    by (simp add: mult.commute mult.left_commute)
   9.798 +  also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
   9.799 +    apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
   9.800 +    using integrable_mult_indicator[OF `A \<in> sets M` assms(3)] by (simp add: mult.commute mult.left_commute)
   9.801 +  also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
   9.802 +    by (simp add: mult.commute mult.left_commute)
   9.803 +  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
   9.804 +qed (auto simp add: real_cond_exp_intg(1) assms)
   9.805 +
   9.806 +lemma real_cond_exp_add [intro]:
   9.807 +  assumes [measurable]: "integrable M f" "integrable M g"
   9.808 +  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"
   9.809 +proof (rule real_cond_exp_charact)
   9.810 +  have "integrable M (real_cond_exp M F f)" "integrable M (real_cond_exp M F g)"
   9.811 +    using real_cond_exp_int(1) assms by auto
   9.812 +  then show "integrable M (\<lambda>x. real_cond_exp M F f x + real_cond_exp M F g x)"
   9.813 +    by auto
   9.814 +
   9.815 +  fix A assume [measurable]: "A \<in> sets F"
   9.816 +  then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
   9.817 +  have intAf: "integrable M (\<lambda>x. indicator A x * f x)"
   9.818 +    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
   9.819 +  have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
   9.820 +    using integrable_mult_indicator[OF `A \<in> sets M` assms(2)] by auto
   9.821 +
   9.822 +  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)"
   9.823 +    apply (rule set_integral_add, auto simp add: assms)
   9.824 +    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]]
   9.825 +          integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(2)]] by simp_all
   9.826 +  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)"
   9.827 +    by auto
   9.828 +  also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
   9.829 +    using real_cond_exp_intg(2) assms `A \<in> sets F` intAf intAg by auto
   9.830 +  also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
   9.831 +    by auto
   9.832 +  also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
   9.833 +    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms `A \<in> sets M` intAf intAg)
   9.834 +  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"
   9.835 +    by simp
   9.836 +qed (auto simp add: assms)
   9.837 +
   9.838 +lemma real_cond_exp_cong:
   9.839 +  assumes ae: "AE x in M. f x = g x" and [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   9.840 +  shows "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
   9.841 +proof -
   9.842 +  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"
   9.843 +    apply (rule nn_cond_exp_cong) using assms by auto
   9.844 +  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"
   9.845 +    apply (rule nn_cond_exp_cong) using assms by auto
   9.846 +  ultimately show "AE x in M. real_cond_exp M F f x = real_cond_exp M F g x"
   9.847 +    unfolding real_cond_exp_def by auto
   9.848 +qed
   9.849 +
   9.850 +lemma real_cond_exp_cmult [intro, simp]:
   9.851 +  fixes c::real
   9.852 +  assumes "integrable M f"
   9.853 +  shows "AE x in M. real_cond_exp M F (\<lambda>x. c * f x) x = c * real_cond_exp M F f x"
   9.854 +by (rule real_cond_exp_mult[where ?f = "\<lambda>x. c" and ?g = f], auto simp add: assms borel_measurable_integrable)
   9.855 +
   9.856 +lemma real_cond_exp_cdiv [intro, simp]:
   9.857 +  fixes c::real
   9.858 +  assumes "integrable M f"
   9.859 +  shows "AE x in M. real_cond_exp M F (\<lambda>x. f x / c) x = real_cond_exp M F f x / c"
   9.860 +using real_cond_exp_cmult[of _ "1/c", OF assms] by (auto simp add: divide_simps)
   9.861 +
   9.862 +lemma real_cond_exp_diff [intro, simp]:
   9.863 +  assumes [measurable]: "integrable M f" "integrable M g"
   9.864 +  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"
   9.865 +proof -
   9.866 +  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"
   9.867 +    using real_cond_exp_add[where ?f = f and ?g = "\<lambda>x. - g x"] assms by auto
   9.868 +  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -g x) x = - real_cond_exp M F g x"
   9.869 +    using real_cond_exp_cmult[where ?f = g and ?c = "-1"] assms(2) by auto
   9.870 +  ultimately show ?thesis by auto
   9.871 +qed
   9.872 +
   9.873 +lemma real_cond_exp_pos [intro]:
   9.874 +  assumes "AE x in M. f x \<ge> 0" and [measurable]: "f \<in> borel_measurable M"
   9.875 +  shows "AE x in M. real_cond_exp M F f x \<ge> 0"
   9.876 +proof -
   9.877 +  define g where "g = (\<lambda>x. max (f x) 0)"
   9.878 +  have "AE x in M. f x = g x" using assms g_def by auto
   9.879 +  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
   9.880 +
   9.881 +  have "\<And>x. g x \<ge> 0" unfolding g_def by simp
   9.882 +  then have "(\<lambda>x. ennreal(-g x)) = (\<lambda>x. 0)"
   9.883 +    by (simp add: ennreal_neg)
   9.884 +  moreover have "AE x in M. 0 = nn_cond_exp M F (\<lambda>x. 0) x"
   9.885 +    by (rule nn_cond_exp_F_meas, auto)
   9.886 +  ultimately have "AE x in M. nn_cond_exp M F (\<lambda>x. ennreal(-g x)) x = 0"
   9.887 +    by simp
   9.888 +  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)"
   9.889 +    unfolding real_cond_exp_def by auto
   9.890 +  then have "AE x in M. real_cond_exp M F g x \<ge> 0" by auto
   9.891 +  then show ?thesis using * by auto
   9.892 +qed
   9.893 +
   9.894 +lemma real_cond_exp_mono:
   9.895 +  assumes "AE x in M. f x \<le> g x" and [measurable]: "integrable M f" "integrable M g"
   9.896 +  shows "AE x in M. real_cond_exp M F f x \<le> real_cond_exp M F g x"
   9.897 +proof -
   9.898 +  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"
   9.899 +    by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
   9.900 +  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x \<ge> 0"
   9.901 +    by (rule real_cond_exp_pos, auto simp add: assms(1))
   9.902 +  ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x \<ge> 0" by auto
   9.903 +  then show ?thesis by auto
   9.904 +qed
   9.905 +
   9.906 +lemma (in -) measurable_P_restriction [measurable (raw)]:
   9.907 +  assumes [measurable]: "Measurable.pred M P" "A \<in> sets M"
   9.908 +  shows "{x \<in> A. P x} \<in> sets M"
   9.909 +proof -
   9.910 +  have "A \<subseteq> space M" using sets.sets_into_space[OF assms(2)].
   9.911 +  then have "{x \<in> A. P x} = A \<inter> {x \<in> space M. P x}" by blast
   9.912 +  then show ?thesis by auto
   9.913 +qed
   9.914 +
   9.915 +lemma real_cond_exp_gr_c:
   9.916 +  assumes [measurable]: "integrable M f"
   9.917 +      and "AE x in M. f x > c"
   9.918 +  shows "AE x in M. real_cond_exp M F f x > c"
   9.919 +proof -
   9.920 +  define X where "X = {x \<in> space M. real_cond_exp M F f x \<le> c}"
   9.921 +  have [measurable]: "X \<in> sets F"
   9.922 +    unfolding X_def apply measurable by (metis sets.top subalg subalgebra_def)
   9.923 +  then have [measurable]: "X \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
   9.924 +  have "emeasure M X = 0"
   9.925 +  proof (rule ccontr)
   9.926 +    assume "\<not>(emeasure M X) = 0"
   9.927 +    have "emeasure (restr_to_subalg M F) X = emeasure M X"
   9.928 +      by (simp add: emeasure_restr_to_subalg subalg)
   9.929 +    then have "emeasure (restr_to_subalg M F) X > 0"
   9.930 +      using `\<not>(emeasure M X) = 0` gr_zeroI by auto
   9.931 +    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>"
   9.932 +      using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans
   9.933 +      not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
   9.934 +    then have [measurable]: "A \<in> sets F" using subalg sets_restr_to_subalg by blast
   9.935 +    then have [measurable]: "A \<in> sets M" using sets_restr_to_subalg subalg subalgebra_def by blast
   9.936 +    have Ic: "set_integrable M A (\<lambda>x. c)"
   9.937 +      using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
   9.938 +    have If: "set_integrable M A f"
   9.939 +      by (rule integrable_mult_indicator, auto simp add: `integrable M f`)
   9.940 +    have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
   9.941 +    proof (rule antisym)
   9.942 +      show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
   9.943 +        apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
   9.944 +      have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
   9.945 +        by (rule real_cond_exp_intA, auto simp add: `integrable M f`)
   9.946 +      also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
   9.947 +        apply (rule set_integral_mono)
   9.948 +        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF `integrable M f`])
   9.949 +        using Ic X_def \<open>A \<subseteq> X\<close> by auto
   9.950 +      finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
   9.951 +    qed
   9.952 +    have "AE x in M. indicator A x * c = indicator A x * f x"
   9.953 +      apply (rule integral_ineq_eq_0_then_AE) using Ic If * apply auto
   9.954 +      using assms(2) unfolding indicator_def by auto
   9.955 +    then have "AE x\<in>A in M. c = f x" by auto
   9.956 +    then have "AE x\<in>A in M. False" using assms(2) by auto
   9.957 +    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>)
   9.958 +    then show False using `emeasure (restr_to_subalg M F) A > 0`
   9.959 +      by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
   9.960 +  qed
   9.961 +  then show ?thesis using AE_iff_null_sets[OF `X \<in> sets M`] unfolding X_def by auto
   9.962 +qed
   9.963 +
   9.964 +lemma real_cond_exp_less_c:
   9.965 +  assumes [measurable]: "integrable M f"
   9.966 +      and "AE x in M. f x < c"
   9.967 +  shows "AE x in M. real_cond_exp M F f x < c"
   9.968 +proof -
   9.969 +  have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
   9.970 +    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
   9.971 +  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x > -c"
   9.972 +    apply (rule real_cond_exp_gr_c) using assms by auto
   9.973 +  ultimately show ?thesis by auto
   9.974 +qed
   9.975 +
   9.976 +lemma real_cond_exp_ge_c:
   9.977 +  assumes [measurable]: "integrable M f"
   9.978 +      and "AE x in M. f x \<ge> c"
   9.979 +  shows "AE x in M. real_cond_exp M F f x \<ge> c"
   9.980 +proof -
   9.981 +  obtain u::"nat \<Rightarrow> real" where u: "\<And>n. u n < c" "u \<longlonglongrightarrow> c"
   9.982 +    using approx_from_below_dense_linorder[of "c-1" c] by auto
   9.983 +  have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat
   9.984 +    apply (rule real_cond_exp_gr_c) using assms `u n < c` by auto
   9.985 +  have "AE x in M. \<forall>n. real_cond_exp M F f x > u n"
   9.986 +    by (subst AE_all_countable, auto simp add: *)
   9.987 +  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
   9.988 +  proof -
   9.989 +    have "real_cond_exp M F f x \<ge> u n" for n using that less_imp_le by auto
   9.990 +    then show ?thesis using u(2) LIMSEQ_le_const2 by blast
   9.991 +  qed
   9.992 +  ultimately show ?thesis by auto
   9.993 +qed
   9.994 +
   9.995 +lemma real_cond_exp_le_c:
   9.996 +  assumes [measurable]: "integrable M f"
   9.997 +      and "AE x in M. f x \<le> c"
   9.998 +  shows "AE x in M. real_cond_exp M F f x \<le> c"
   9.999 +proof -
  9.1000 +  have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
  9.1001 +    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
  9.1002 +  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x \<ge> -c"
  9.1003 +    apply (rule real_cond_exp_ge_c) using assms by auto
  9.1004 +  ultimately show ?thesis by auto
  9.1005 +qed
  9.1006 +
  9.1007 +lemma real_cond_exp_mono_strict:
  9.1008 +  assumes "AE x in M. f x < g x" and [measurable]: "integrable M f" "integrable M g"
  9.1009 +  shows "AE x in M. real_cond_exp M F f x < real_cond_exp M F g x"
  9.1010 +proof -
  9.1011 +  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"
  9.1012 +    by (rule AE_symmetric[OF real_cond_exp_diff], auto simp add: assms)
  9.1013 +  moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x - f x) x > 0"
  9.1014 +    by (rule real_cond_exp_gr_c, auto simp add: assms)
  9.1015 +  ultimately have "AE x in M. real_cond_exp M F g x - real_cond_exp M F f x > 0" by auto
  9.1016 +  then show ?thesis by auto
  9.1017 +qed
  9.1018 +
  9.1019 +lemma real_cond_exp_nested_subalg [intro, simp]:
  9.1020 +  assumes "subalgebra M G" "subalgebra G F"
  9.1021 +      and [measurable]: "integrable M f"
  9.1022 +  shows "AE x in M. real_cond_exp M F (real_cond_exp M G f) x = real_cond_exp M F f x"
  9.1023 +proof (rule real_cond_exp_charact)
  9.1024 +  interpret G: sigma_finite_subalgebra M G by (rule nested_subalg_is_sigma_finite[OF assms(1) assms(2)])
  9.1025 +  show "integrable M (real_cond_exp M G f)" by (auto simp add: assms G.real_cond_exp_int(1))
  9.1026 +
  9.1027 +  fix A assume [measurable]: "A \<in> sets F"
  9.1028 +  then have [measurable]: "A \<in> sets G" using assms(2) by (meson set_mp subalgebra_def)
  9.1029 +  have "set_lebesgue_integral M A (real_cond_exp M G f) = set_lebesgue_integral M A f"
  9.1030 +    by (rule G.real_cond_exp_intA[symmetric], auto simp add: assms(3))
  9.1031 +  also have "... = set_lebesgue_integral M A (real_cond_exp M F f)"
  9.1032 +    by (rule real_cond_exp_intA, auto simp add: assms(3))
  9.1033 +  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
  9.1034 +qed (auto simp add: assms real_cond_exp_int(1))
  9.1035 +
  9.1036 +lemma real_cond_exp_sum [intro, simp]:
  9.1037 +  fixes f::"'b \<Rightarrow> 'a \<Rightarrow> real"
  9.1038 +  assumes [measurable]: "\<And>i. integrable M (f i)"
  9.1039 +  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)"
  9.1040 +proof (rule real_cond_exp_charact)
  9.1041 +  fix A assume [measurable]: "A \<in> sets F"
  9.1042 +  then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
  9.1043 +  have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
  9.1044 +    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
  9.1045 +  have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
  9.1046 +    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]] by auto
  9.1047 +  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
  9.1048 +    by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
  9.1049 +
  9.1050 +  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)"
  9.1051 +    by (simp add: sum_distrib_left)
  9.1052 +  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * f i x \<partial>M))"
  9.1053 +    by (rule Bochner_Integration.integral_sum, simp add: *)
  9.1054 +  also have "... = (\<Sum>i\<in>I. (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M))"
  9.1055 +    using inti by auto
  9.1056 +  also have "... = (\<integral>x. (\<Sum>i\<in>I. indicator A x * real_cond_exp M F (f i) x)\<partial>M)"
  9.1057 +    by (rule Bochner_Integration.integral_sum[symmetric], simp add: **)
  9.1058 +  also have "... = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)"
  9.1059 +    by (simp add: sum_distrib_left)
  9.1060 +  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
  9.1061 +qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
  9.1062 +
  9.1063 +text {*Jensen's inequality, describing the behavior of the integral under a convex function, admits
  9.1064 +a version for the conditional expectation, as follows.*}
  9.1065 +
  9.1066 +theorem real_cond_exp_jensens_inequality:
  9.1067 +  fixes q :: "real \<Rightarrow> real"
  9.1068 +  assumes X: "integrable M X" "AE x in M. X x \<in> I"
  9.1069 +  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
  9.1070 +  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel"
  9.1071 +  shows "AE x in M. real_cond_exp M F X x \<in> I"
  9.1072 +        "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
  9.1073 +proof -
  9.1074 +  have "open I" using I by auto
  9.1075 +  then have "interior I = I" by (simp add: interior_eq)
  9.1076 +  have [measurable]: "I \<in> sets borel" using I by auto
  9.1077 +  define phi where "phi = (\<lambda>x. Inf ((\<lambda>t. (q x - q t) / (x - t)) ` ({x<..} \<inter> I)))"
  9.1078 +  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)"
  9.1079 +        if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
  9.1080 +    unfolding phi_def apply (rule convex_le_Inf_differential)
  9.1081 +    using `convex_on I q` that `interior I = I` by auto
  9.1082 +  text {*It is not clear that the function $\phi$ is measurable. We replace it by a version which
  9.1083 +        is better behaved.*}
  9.1084 +  define psi where "psi = (\<lambda>x. phi x * indicator I x)"
  9.1085 +  have A: "psi y = phi y" if "y \<in> I" for y unfolding psi_def indicator_def using that by auto
  9.1086 +  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)"
  9.1087 +        if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
  9.1088 +    unfolding A[OF `real_cond_exp M F X x \<in> I`] using ** that by auto
  9.1089 +
  9.1090 +  note I
  9.1091 +  moreover have "AE x in M. real_cond_exp M F X x > a" if "I \<subseteq> {a <..}" for a
  9.1092 +    apply (rule real_cond_exp_gr_c) using X that by auto
  9.1093 +  moreover have "AE x in M. real_cond_exp M F X x < b" if "I \<subseteq> {..<b}" for b
  9.1094 +    apply (rule real_cond_exp_less_c) using X that by auto
  9.1095 +  ultimately show "AE x in M. real_cond_exp M F X x \<in> I"
  9.1096 +    by (elim disjE) (auto simp: subset_eq)
  9.1097 +  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)"
  9.1098 +    using * X(2) by auto
  9.1099 +
  9.1100 +  text {*Then, one wants to take the conditional expectation of this inequality. On the left, one gets
  9.1101 +         the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one
  9.1102 +         is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only
  9.1103 +         works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The
  9.1104 +         trick is to multiply by a $F$-measurable function which is small enough to make
  9.1105 +         everything integrable.*}
  9.1106 +
  9.1107 +  obtain f::"'a \<Rightarrow> real" where [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
  9.1108 +                               "integrable (restr_to_subalg M F) f"
  9.1109 +                           and f: "\<And>x. f x > 0" "\<And>x. f x \<le> 1"
  9.1110 +    using sigma_finite_measure.obtain_positive_integrable_function[OF sigma_fin_subalg] by metis
  9.1111 +  then have [measurable]: "f \<in> borel_measurable F" by (simp add: subalg)
  9.1112 +  then have [measurable]: "f \<in> borel_measurable M" using measurable_from_subalg[OF subalg] by blast
  9.1113 +  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>))"
  9.1114 +  define G where "G = (\<lambda>x. g x * psi (real_cond_exp M F X x))"
  9.1115 +  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)
  9.1116 +  have G: "\<bar>G x\<bar> \<le> 1" for x unfolding G_def g_def using f[of x]
  9.1117 +  proof (auto simp add: abs_mult)
  9.1118 +    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>"
  9.1119 +      apply (rule mult_mono) using f[of x] by auto
  9.1120 +    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
  9.1121 +    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>"
  9.1122 +      by simp
  9.1123 +  qed
  9.1124 +  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))"
  9.1125 +    using main_ineq g by (auto simp add: divide_simps)
  9.1126 +  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)"
  9.1127 +    unfolding G_def by (auto simp add: algebra_simps)
  9.1128 +
  9.1129 +  text {*To proceed, we need to know that $\psi$ is measurable.*}
  9.1130 +  have phi_mono: "phi x \<le> phi y" if "x \<le> y" "x \<in> I" "y \<in> I" for x y
  9.1131 +  proof (cases "x < y")
  9.1132 +    case True
  9.1133 +    have "q x + phi x * (y-x) \<le> q y"
  9.1134 +      unfolding phi_def apply (rule convex_le_Inf_differential) using `convex_on I q` that `interior I = I` by auto
  9.1135 +    then have "phi x \<le> (q x - q y) / (x - y)"
  9.1136 +      using that `x < y` by (auto simp add: divide_simps algebra_simps)
  9.1137 +    moreover have "(q x - q y)/(x - y) \<le> phi y"
  9.1138 +    unfolding phi_def proof (rule cInf_greatest, auto)
  9.1139 +      fix t assume "t \<in> I" "y < t"
  9.1140 +      have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
  9.1141 +        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
  9.1142 +      also have "... \<le> (q y - q t) / (y - t)"
  9.1143 +        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
  9.1144 +      finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
  9.1145 +    next
  9.1146 +      obtain e where "0 < e" "ball y e \<subseteq> I" using `open I` `y \<in> I` openE by blast
  9.1147 +      then have "y + e/2 \<in> {y<..} \<inter> I" by (auto simp: dist_real_def)
  9.1148 +      then show "{y<..} \<inter> I = {} \<Longrightarrow> False" by auto
  9.1149 +    qed
  9.1150 +    ultimately show "phi x \<le> phi y" by auto
  9.1151 +  next
  9.1152 +    case False
  9.1153 +    then have "x = y" using `x \<le> y` by auto
  9.1154 +    then show ?thesis by auto
  9.1155 +  qed
  9.1156 +  have [measurable]: "psi \<in> borel_measurable borel"
  9.1157 +    by (rule borel_measurable_piecewise_mono[of "{I, -I}"])
  9.1158 +       (auto simp add: psi_def indicator_def phi_mono intro: mono_onI)
  9.1159 +  have [measurable]: "q \<in> borel_measurable borel" using q by simp
  9.1160 +
  9.1161 +  have [measurable]: "X \<in> borel_measurable M"
  9.1162 +                     "real_cond_exp M F X \<in> borel_measurable F"
  9.1163 +                     "g \<in> borel_measurable F" "g \<in> borel_measurable M"
  9.1164 +                     "G \<in> borel_measurable F" "G \<in> borel_measurable M"
  9.1165 +    using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto
  9.1166 +  have int1: "integrable (restr_to_subalg M F) (\<lambda>x. g x * q (real_cond_exp M F X x))"
  9.1167 +    apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg `integrable (restr_to_subalg M F) f`)
  9.1168 +    unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps)
  9.1169 +  have int2: "integrable M (\<lambda>x. G x * (X x - real_cond_exp M F X x))"
  9.1170 +    apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>X x\<bar> + \<bar>real_cond_exp M F X x\<bar>"])
  9.1171 +    apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int `integrable M X` AE_I2)
  9.1172 +    using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le)
  9.1173 +  have int3: "integrable M (\<lambda>x. g x * q (X x))"
  9.1174 +    apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. q(X x)"], auto simp add: q(1) abs_mult)
  9.1175 +    using g by (simp add: less_imp_le mult_left_le_one_le)
  9.1176 +
  9.1177 +  text {*Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
  9.1178 +         the following.*}
  9.1179 +  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"
  9.1180 +    apply (rule real_cond_exp_mono[OF main_G])
  9.1181 +    apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]])
  9.1182 +    using int2 int3 by auto
  9.1183 +  text {*This reduces to the desired inequality thanks to the properties of conditional expectation,
  9.1184 +         i.e., the conditional expectation of an $F$-measurable function is this function, and one can
  9.1185 +         multiply an $F$-measurable function outside of conditional expectations.
  9.1186 +         Since all these equalities only hold almost everywhere, we formulate them separately,
  9.1187 +         and then combine all of them to simplify the above equation, again almost everywhere.*}
  9.1188 +  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"
  9.1189 +    by (rule real_cond_exp_mult, auto simp add: int3)
  9.1190 +  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
  9.1191 +      = 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"
  9.1192 +    by (rule real_cond_exp_add, auto simp add: integrable_from_subalg[OF subalg int1] int2)
  9.1193 +  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)"
  9.1194 +    by (rule real_cond_exp_F_meas, auto simp add: integrable_from_subalg[OF subalg int1])
  9.1195 +  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"
  9.1196 +    by (rule real_cond_exp_mult, auto simp add: int2)
  9.1197 +  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"
  9.1198 +    by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int `integrable M X`)
  9.1199 +  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 "
  9.1200 +    by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int `integrable M X`)
  9.1201 +  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)"
  9.1202 +    by auto
  9.1203 +  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)"
  9.1204 +    using g(1) by (auto simp add: divide_simps)
  9.1205 +qed
  9.1206 +
  9.1207 +text {*Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
  9.1208 +bound for it. Indeed, this is not true in general, as the following counterexample shows:
  9.1209 +
  9.1210 +on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
  9.1211 +for integer $n$. Let $q(x) = - \sqrt{x}$ for $x\geq 0$. Define $X$ which is equal to $1/n$ over
  9.1212 +$[n, n+1/n)$ and $2^{-n}$ on $[n+1/n, n+1)$. Then $X$ is integrable as $\sum 1/n^2 < \infty$, and
  9.1213 +$q(X)$ is integrable as $\sum 1/n^{3/2} < \infty$. On the other hand, $E(X|F)$ is essentially equal
  9.1214 +to $1/n^2$ on $[n, n+1)$ (we neglect the term $2^{-n}$, we only put it there because $X$ should take
  9.1215 +its values in $I=(0,\infty)$). Hence, $q(E(X|F))$ is equal to $-1/n$ on $[n, n+1)$, hence it is not
  9.1216 +integrable.
  9.1217 +
  9.1218 +However, this counterexample is essentially the only situation where this function is not
  9.1219 +integrable, as shown by the next lemma.
  9.1220 +*}
  9.1221 +
  9.1222 +lemma integrable_convex_cond_exp:
  9.1223 +  fixes q :: "real \<Rightarrow> real"
  9.1224 +  assumes X: "integrable M X" "AE x in M. X x \<in> I"
  9.1225 +  assumes I: "I = {a <..< b} \<or> I = {a <..} \<or> I = {..< b} \<or> I = UNIV"
  9.1226 +  assumes q: "integrable M (\<lambda>x. q (X x))" "convex_on I q" "q \<in> borel_measurable borel"
  9.1227 +  assumes H: "emeasure M (space M) = \<infinity> \<Longrightarrow> 0 \<in> I"
  9.1228 +  shows "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
  9.1229 +proof -
  9.1230 +  have [measurable]: "(\<lambda>x. q (real_cond_exp M F X x)) \<in> borel_measurable M"
  9.1231 +                     "q \<in> borel_measurable borel"
  9.1232 +                     "X \<in> borel_measurable M"
  9.1233 +    using X(1) q(3) by auto
  9.1234 +  have "open I" using I by auto
  9.1235 +  then have "interior I = I" by (simp add: interior_eq)
  9.1236 +
  9.1237 +  consider "emeasure M (space M) = 0" | "emeasure M (space M) > 0 \<and> emeasure M (space M) < \<infinity>" | "emeasure M (space M) = \<infinity>"
  9.1238 +    by (metis infinity_ennreal_def not_gr_zero top.not_eq_extremum)
  9.1239 +  then show ?thesis
  9.1240 +  proof (cases)
  9.1241 +    case 1
  9.1242 +    show ?thesis by (subst integrable_cong_AE[of _ _ "\<lambda>x. 0"], auto intro: emeasure_0_AE[OF 1])
  9.1243 +  next
  9.1244 +    case 2
  9.1245 +    interpret finite_measure M using 2 by (auto intro!: finite_measureI)
  9.1246 +
  9.1247 +    have "I \<noteq> {}"
  9.1248 +      using `AE x in M. X x \<in> I` 2 eventually_mono integral_less_AE_space by fastforce
  9.1249 +    then obtain z where "z \<in> I" by auto
  9.1250 +
  9.1251 +    define A where "A = Inf ((\<lambda>t. (q z - q t) / (z - t)) ` ({z<..} \<inter> I))"
  9.1252 +    have "q y \<ge> q z + A * (y - z)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
  9.1253 +      using `z \<in> I` `y \<in> I` `interior I = I` q(2) by auto
  9.1254 +    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)"
  9.1255 +      using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
  9.1256 +    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"
  9.1257 +      using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
  9.1258 +    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
  9.1259 +      using that by auto
  9.1260 +    ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar>
  9.1261 +        \<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>"
  9.1262 +      by auto
  9.1263 +
  9.1264 +    show "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
  9.1265 +      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>"])
  9.1266 +      apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
  9.1267 +      using X(1) q(1) * by auto
  9.1268 +  next
  9.1269 +    case 3
  9.1270 +    then have "0 \<in> I" using H finite_measure.finite_emeasure_space by auto
  9.1271 +    have "q(0) = 0"
  9.1272 +    proof (rule ccontr)
  9.1273 +      assume *: "\<not>(q(0) = 0)"
  9.1274 +      define e where "e = \<bar>q(0)\<bar> / 2"
  9.1275 +      then have "e > 0" using * by auto
  9.1276 +      have "continuous (at 0) q"
  9.1277 +        using q(2) `0 \<in> I` `open I` \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
  9.1278 +      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`
  9.1279 +        by (metis continuous_at_real_range real_norm_def)
  9.1280 +      then have *: "\<bar>q(y)\<bar> > e" if "\<bar>y\<bar> < d" for y
  9.1281 +      proof -
  9.1282 +        have "\<bar>q 0\<bar> \<le> \<bar>q 0 - q y\<bar> + \<bar>q y\<bar>" by auto
  9.1283 +        also have "... < e + \<bar>q y\<bar>" using d(2) that by force
  9.1284 +        finally have "\<bar>q y\<bar> > \<bar>q 0\<bar> - e" by auto
  9.1285 +        then show ?thesis unfolding e_def by simp
  9.1286 +      qed
  9.1287 +      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)"
  9.1288 +        by (rule emeasure_mono, auto simp add: * `e>0` less_imp_le ennreal_mult''[symmetric])
  9.1289 +      also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)"
  9.1290 +        by (rule nn_integral_Markov_inequality, auto)
  9.1291 +      also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto
  9.1292 +      also have "... = (1/e) * ennreal(\<integral>x. \<bar>q(X x)\<bar> \<partial>M)"
  9.1293 +        using nn_integral_eq_integral[OF integrable_abs[OF q(1)]] by auto
  9.1294 +      also have "... < \<infinity>"
  9.1295 +        by (simp add: ennreal_mult_less_top)
  9.1296 +      finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp
  9.1297 +
  9.1298 +      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"
  9.1299 +        by (auto simp add: `d>0` ennreal_mult''[symmetric])
  9.1300 +      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)"
  9.1301 +        by auto
  9.1302 +      also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)"
  9.1303 +        by (rule nn_integral_Markov_inequality, auto)
  9.1304 +      also have "... = (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) \<partial>M)" by auto
  9.1305 +      also have "... = (1/d) * ennreal(\<integral>x. \<bar>X x\<bar> \<partial>M)"
  9.1306 +        using nn_integral_eq_integral[OF integrable_abs[OF X(1)]] by auto
  9.1307 +      also have "... < \<infinity>"
  9.1308 +        by (simp add: ennreal_mult_less_top)
  9.1309 +      finally have B: "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} < \<infinity>" by simp
  9.1310 +
  9.1311 +      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
  9.1312 +      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})"
  9.1313 +        by simp
  9.1314 +      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}"
  9.1315 +        by (auto intro!: emeasure_subadditive)
  9.1316 +      also have "... < \<infinity>" using A B by auto
  9.1317 +      finally show False using `emeasure M (space M) = \<infinity>` by auto
  9.1318 +    qed
  9.1319 +
  9.1320 +    define A where "A = Inf ((\<lambda>t. (q 0 - q t) / (0 - t)) ` ({0<..} \<inter> I))"
  9.1321 +    have "q y \<ge> q 0 + A * (y - 0)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
  9.1322 +      using `0 \<in> I` `y \<in> I` `interior I = I` q(2) by auto
  9.1323 +    then have "q y \<ge> A * y" if "y \<in> I" for y using `q 0 = 0` that by auto
  9.1324 +    then have "AE x in M. q (real_cond_exp M F X x) \<ge> A * real_cond_exp M F X x"
  9.1325 +      using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
  9.1326 +    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"
  9.1327 +      using real_cond_exp_jensens_inequality(2)[OF X I q] by auto
  9.1328 +    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
  9.1329 +      using that by auto
  9.1330 +    ultimately have *: "AE x in M. \<bar>q (real_cond_exp M F X x)\<bar>
  9.1331 +        \<le> \<bar>real_cond_exp M F (\<lambda>x. q (X x)) x\<bar> + \<bar>A * real_cond_exp M F X x\<bar>"
  9.1332 +      by auto
  9.1333 +
  9.1334 +    show "integrable M (\<lambda>x. q (real_cond_exp M F X x))"
  9.1335 +      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>"])
  9.1336 +      apply (auto intro!: Bochner_Integration.integrable_add integrable_abs integrable_mult_right Bochner_Integration.integrable_diff real_cond_exp_int(1))
  9.1337 +      using X(1) q(1) * by auto
  9.1338 +  qed
  9.1339 +qed
  9.1340 +
  9.1341 +end
  9.1342 +
  9.1343 +end
    10.1 --- a/src/HOL/Probability/Levy.thy	Mon Oct 17 15:20:06 2016 +0200
    10.2 +++ b/src/HOL/Probability/Levy.thy	Thu Oct 13 18:36:06 2016 +0200
    10.3 @@ -390,7 +390,7 @@
    10.4        by (intro borel_integrable_compact[OF compact_Icc] continuous_at_imp_continuous_on
    10.5                  continuous_intros ballI M'.isCont_char continuous_intros)
    10.6      have "cmod (CLBINT t:{-d/2..d/2}. 1 - char M' t) \<le> LBINT t:{-d/2..d/2}. cmod (1 - char M' t)"
    10.7 -      using integral_norm_bound[OF 2] by simp
    10.8 +      using integral_norm_bound[of _ "\<lambda>x. indicator {u..v} x *\<^sub>R (1 - char M' x)" for u v] by simp
    10.9      also have 4: "\<dots> \<le> LBINT t:{-d/2..d/2}. \<epsilon> / 4"
   10.10        apply (rule integral_mono [OF 3])
   10.11         apply (simp add: emeasure_lborel_Icc_eq)
    11.1 --- a/src/HOL/Probability/Probability.thy	Mon Oct 17 15:20:06 2016 +0200
    11.2 +++ b/src/HOL/Probability/Probability.thy	Thu Oct 13 18:36:06 2016 +0200
    11.3 @@ -11,6 +11,7 @@
    11.4    Random_Permutations
    11.5    SPMF
    11.6    Stream_Space
    11.7 +  Conditional_Expectation
    11.8  begin
    11.9  
   11.10  end
    12.1 --- a/src/HOL/Topological_Spaces.thy	Mon Oct 17 15:20:06 2016 +0200
    12.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Oct 13 18:36:06 2016 +0200
    12.3 @@ -1440,6 +1440,42 @@
    12.4      at_within_def eventually_nhds_within_iff_sequentially comp_def
    12.5    by metis
    12.6  
    12.7 +lemma approx_from_above_dense_linorder:
    12.8 +  fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
    12.9 +  assumes "x < y"
   12.10 +  shows "\<exists>u. (\<forall>n. u n > x) \<and> (u \<longlonglongrightarrow> x)"
   12.11 +proof -
   12.12 +  obtain A :: "nat \<Rightarrow> 'a set" where A: "\<And>i. open (A i)" "\<And>i. x \<in> A i"
   12.13 +                                      "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F \<longlonglongrightarrow> x"
   12.14 +    by (metis first_countable_topology_class.countable_basis)
   12.15 +  define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z > x)"
   12.16 +  have "\<exists>z. z \<in> U \<and> x < z" if "x \<in> U" "open U" for U
   12.17 +    using open_right[OF `open U` `x \<in> U` `x < y`]
   12.18 +    by (meson atLeastLessThan_iff dense less_imp_le subset_eq)
   12.19 +  then have *: "u n \<in> A n \<and> x < u n" for n
   12.20 +    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
   12.21 +  then have "u \<longlonglongrightarrow> x" using A(3) by simp
   12.22 +  then show ?thesis using * by auto
   12.23 +qed
   12.24 +
   12.25 +lemma approx_from_below_dense_linorder:
   12.26 +  fixes x::"'a::{dense_linorder, linorder_topology, first_countable_topology}"
   12.27 +  assumes "x > y"
   12.28 +  shows "\<exists>u. (\<forall>n. u n < x) \<and> (u \<longlonglongrightarrow> x)"
   12.29 +proof -
   12.30 +  obtain A :: "nat \<Rightarrow> 'a set" where A: "\<And>i. open (A i)" "\<And>i. x \<in> A i"
   12.31 +                                      "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F \<longlonglongrightarrow> x"
   12.32 +    by (metis first_countable_topology_class.countable_basis)
   12.33 +  define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z < x)"
   12.34 +  have "\<exists>z. z \<in> U \<and> z < x" if "x \<in> U" "open U" for U
   12.35 +    using open_left[OF `open U` `x \<in> U` `x > y`]
   12.36 +    by (meson dense greaterThanAtMost_iff less_imp_le subset_eq)
   12.37 +  then have *: "u n \<in> A n \<and> u n < x" for n
   12.38 +    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
   12.39 +  then have "u \<longlonglongrightarrow> x" using A(3) by simp
   12.40 +  then show ?thesis using * by auto
   12.41 +qed
   12.42 +
   12.43  
   12.44  subsection \<open>Function limit at a point\<close>
   12.45