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