author hoelzl Thu Oct 13 18:36:06 2016 +0200 (2016-10-13) changeset 64283 979cdfdf7a79 parent 64282 261d42f0bfac child 64284 f3b905b2eee2
HOL-Probability: move conditional expectation from AFP/Ergodic_Theory
 src/HOL/Analysis/Bochner_Integration.thy file | annotate | diff | revisions src/HOL/Analysis/Borel_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Measurable.thy file | annotate | diff | revisions src/HOL/Analysis/Measure_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy file | annotate | diff | revisions src/HOL/Analysis/Radon_Nikodym.thy file | annotate | diff | revisions src/HOL/Analysis/Set_Integral.thy file | annotate | diff | revisions src/HOL/Probability/Characteristic_Functions.thy file | annotate | diff | revisions src/HOL/Probability/Conditional_Expectation.thy file | annotate | diff | revisions src/HOL/Probability/Levy.thy file | annotate | diff | revisions src/HOL/Probability/Probability.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions
     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.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.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> gA. 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 (gA))"
7.149 +    by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw)
7.150 +  also have "... = (\<integral>\<^sup>+y \<in> gA. 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> gA. 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
`