src/HOL/Probability/Conditional_Expectation.thy

 
 theory Conditional_Expectation
 imports Probability_Measure
 begin
 
-subsection {*Restricting a measure to a sub-sigma-algebra*}
+subsection \<open>Restricting a measure to a sub-sigma-algebra\<close>
 
 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:

   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 have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] \<open>U \<in> sets F\<close> by auto
   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"

   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+
+text\<open>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$.*}
+current notations, with the removal of the useless assumption $f \geq 0$.\<close>
 
 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)

   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.*}
+text\<open>The following is the direct transposition of \verb+integral_subalgebra+
+(from \verb+Bochner_Integration+) in the current notations.\<close>
 
 lemma integral_subalgebra2:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes "subalgebra M F" and
     [measurable]: "f \<in> borel_measurable F"

     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
+subsection \<open>Nonnegative conditional expectation\<close>
+
+text \<open>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$.

 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.
-*}
+\<close>
 
 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

   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$
+text \<open>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.*}
+This means that a positive integrable function can have no meaningful conditional expectation.\<close>
 
 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)"

   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)
+  moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] \<open>A \<subseteq> sets F\<close> Ap)
   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. *}
+text \<open>Conditional expectations are very often used in probability spaces. This is a special case
+of the previous one, as we prove now.\<close>
 
 locale finite_measure_subalgebra = finite_measure +
   fixes F::"'a measure"
   assumes subalg: "subalgebra M F"
 

 qed
 
 context sigma_finite_subalgebra
 begin
 
-text{* The next lemma is arguably the most fundamental property of conditional expectation:
+text\<open>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.
-*}
+\<close>
 
 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 -

   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`)
+    by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>)
   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`)
+    by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>)
   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:

   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
+subsection \<open>Real conditional expectation\<close>
+
+text \<open>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.)
-*}
+\<close>
 
 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))"
 

   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
+text\<open>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

 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.
-*}
+\<close>
 
 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)"

 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
+  have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
   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"

   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 [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> 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)
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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)
 

     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
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
+          integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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
+    using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> 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)
+    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> 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:

   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
+      using \<open>\<not>(emeasure M X) = 0\<close> 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`)
+      by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
     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`)
+        by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
       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`])
+        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
         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`
+    then show False using \<open>emeasure (restr_to_subalg M F) A > 0\<close>
       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
+  then show ?thesis using AE_iff_null_sets[OF \<open>X \<in> sets M\<close>] 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
+    using real_cond_exp_cmult[OF \<open>integrable M f\<close>, 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
 

   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
+    apply (rule real_cond_exp_gr_c) using assms \<open>u n < c\<close> 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

   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
+    using real_cond_exp_cmult[OF \<open>integrable M f\<close>, 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
 

   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
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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
+    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> 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 "... = (\<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.*}
+text \<open>Jensen's inequality, describing the behavior of the integral under a convex function, admits
+a version for the conditional expectation, as follows.\<close>
 
 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"

   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.*}
+    using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto
+  text \<open>It is not clear that the function $\phi$ is measurable. We replace it by a version which
+        is better behaved.\<close>
   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
+    unfolding A[OF \<open>real_cond_exp M F X x \<in> I\<close>] 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

   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
+  text \<open>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.*}
+         everything integrable.\<close>
 
   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

   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.*}
+  text \<open>To proceed, we need to know that $\psi$ is measurable.\<close>
   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
+      unfolding phi_def apply (rule convex_le_Inf_differential) using \<open>convex_on I q\<close> that \<open>interior I = I\<close> 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)
+      using that \<open>x < y\<close> 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
+        apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
       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
+        apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
       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
+      obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> 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 have "x = y" using \<open>x \<le> y\<close> 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)

                      "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`)
+    apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg \<open>integrable (restr_to_subalg M F) f\<close>)
     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)
+    apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int \<open>integrable M X\<close> 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.*}
+  text \<open>Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
+         the following.\<close>
   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,
+  text \<open>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.*}
+         and then combine all of them to simplify the above equation, again almost everywhere.\<close>
   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`)
+    by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
   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`)
+    by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
   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
+text \<open>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

 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.
-*}
+\<close>
 
 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"

   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
+      using \<open>AE x in M. X x \<in> I\<close> 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
+      using \<open>z \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> 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

     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`
+        using q(2) \<open>0 \<in> I\<close> \<open>open I\<close> \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
+      then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using \<open>e > 0\<close>
         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])
+        by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> 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])
+        by (auto simp add: \<open>d>0\<close> 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

       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
+      finally show False using \<open>emeasure M (space M) = \<infinity>\<close> 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
+      using \<open>0 \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto
+    then have "q y \<ge> A * y" if "y \<in> I" for y using \<open>q 0 = 0\<close> 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