diff --git a/thys/Martingales/Bochner_Integration_Supplement.thy b/thys/Martingales/Bochner_Integration_Supplement.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Bochner_Integration_Supplement.thy @@ -0,0 +1,722 @@ +(* Author: Ata Keskin, TU München +*) + +theory Bochner_Integration_Supplement + imports "HOL-Analysis.Bochner_Integration" "HOL-Analysis.Set_Integral" Elementary_Metric_Spaces_Supplement +begin + +section \Supplementary Lemmas for Bochner Integration\ + +subsection \Integrable Simple Functions\ + +text \We restate some basic results concerning Bochner-integrable functions.\ + +lemma integrable_implies_simple_function_sequence: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes "integrable M f" + obtains s where "\i. simple_function M (s i)" + and "\i. emeasure M {y \ space M. s i y \ 0} \ \" + and "\x. x \ space M \ (\i. s i x) \ f x" + and "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" +proof- + have f: "f \ borel_measurable M" "(\\<^sup>+x. norm (f x) \M) < \" using assms unfolding integrable_iff_bounded by auto + obtain s where s: "\i. simple_function M (s i)" "\x. x \ space M \ (\i. s i x) \ f x" "\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)" using borel_measurable_implies_sequence_metric[OF f(1)] unfolding norm_conv_dist by metis + { + fix i + have "(\\<^sup>+x. norm (s i x) \M) \ (\\<^sup>+x. ennreal (2 * norm (f x)) \M)" using s by (intro nn_integral_mono, auto) + also have "\ < \" using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult) + finally have sbi: "Bochner_Integration.simple_bochner_integrable M (s i)" using s by (intro simple_bochner_integrableI_bounded) auto + hence "emeasure M {y \ space M. s i y \ 0} \ \" by (auto intro: integrableI_simple_bochner_integrable simple_bochner_integrable.cases) + } + thus ?thesis using that s by blast +qed + +text \Simple functions can be represented by sums of indicator functions.\ + +lemma simple_function_indicator_representation: + fixes f ::"'a \ 'b :: {second_countable_topology, banach}" + assumes "simple_function M f" "x \ space M" + shows "f x = (\y \ f ` space M. indicator (f -` {y} \ space M) x *\<^sub>R y)" + (is "?l = ?r") +proof - + have "?r = (\y \ f ` space M. + (if y = f x then indicator (f -` {y} \ space M) x *\<^sub>R y else 0))" by (auto intro!: sum.cong) + also have "... = indicator (f -` {f x} \ space M) x *\<^sub>R f x" using assms by (auto dest: simple_functionD) + also have "... = f x" using assms by (auto simp: indicator_def) + finally show ?thesis by auto +qed + +lemma simple_function_indicator_representation_AE: + fixes f ::"'a \ 'b :: {second_countable_topology, banach}" + assumes "simple_function M f" + shows "AE x in M. f x = (\y \ f ` space M. indicator (f -` {y} \ space M) x *\<^sub>R y)" + by (metis (mono_tags, lifting) AE_I2 simple_function_indicator_representation assms) + +lemmas simple_function_scaleR[intro] = simple_function_compose2[where h="(*\<^sub>R)"] +lemmas integrable_simple_function = simple_bochner_integrable.intros[THEN has_bochner_integral_simple_bochner_integrable, THEN integrable.intros] + +text \Induction rule for simple integrable functions.\ + +lemma\<^marker>\tag important\ integrable_simple_function_induct[consumes 2, case_names cong indicator add, induct set: simple_function]: + fixes f :: "'a \ 'b :: {second_countable_topology, banach}" + assumes f: "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" + assumes cong: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ + \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ + \ (\x. x \ space M \ f x = g x) \ P f \ P g" + assumes indicator: "\A y. A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R y)" + assumes add: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ + simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ + (\z. z \ space M \ norm (f z + g z) = norm (f z) + norm (g z)) \ + P f \ P g \ P (\x. f x + g x)" + shows "P f" +proof- + let ?f = "\x. (\y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + have f_ae_eq: "f x = ?f x" if "x \ space M" for x using simple_function_indicator_representation[OF f(1) that] . + moreover have "emeasure M {y \ space M. ?f y \ 0} \ \" by (metis (no_types, lifting) Collect_cong calculation f(2)) + moreover have "P (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + "simple_function M (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + "emeasure M {y \ space M. (\x\S. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ \" + if "S \ f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that + proof (induction rule: finite_induct) + case empty + { + case 1 + then show ?case using indicator[of "{}"] by force + next + case 2 + then show ?case by force + next + case 3 + then show ?case by force + } + next + case (insert x F) + have "(f -` {x} \ space M) \ {y \ space M. f y \ 0}" if "x \ 0" using that by blast + moreover have "{y \ space M. f y \ 0} = space M - (f -` {0} \ space M)" by blast + moreover have "space M - (f -` {0} \ space M) \ sets M" using simple_functionD(2)[OF f(1)] by blast + ultimately have fin_0: "emeasure M (f -` {x} \ space M) < \" if "x \ 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique) + hence fin_1: "emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0} \ \" if "x \ 0" by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that) + + have *: "(\y\insert x F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) = (\y\F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) + indicat_real (f -` {x} \ space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) Diff_empty Diff_insert0 add.commute insert.hyps(1) insert.hyps(2) sum.insert_remove) + have **: "{y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" unfolding * by fastforce + { + case 1 + hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert(3)[OF F] by simp + next + case False + have norm_argument: "norm ((\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + indicat_real (f -` {x} \ space M) z *\<^sub>R x) = norm (\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \ space M) z *\<^sub>R x)" if z: "z \ space M" for z + proof (cases "f z = x") + case True + have "indicat_real (f -` {y} \ space M) z *\<^sub>R y = 0" if "y \ F" for y using True insert(2) z that 1 unfolding indicator_def by force + hence "(\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) = 0" by (meson sum.neutral) + then show ?thesis by force + next + case False + then show ?thesis by force + qed + show ?thesis using False simple_functionD(2)[OF f(1)] insert(3,5)[OF F] simple_function_scaleR fin_0 fin_1 by (subst *, subst add, subst simple_function_sum) (blast intro: norm_argument indicator)+ + qed + next + case 2 + hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert(4)[OF F] by simp + next + case False + then show ?thesis unfolding * using insert(4)[OF F] simple_functionD(2)[OF f(1)] by fast + qed + next + case 3 + hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert(5)[OF F] by simp + next + case False + have "emeasure M {y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ emeasure M ({y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0})" + using ** simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_mono, force+) + also have "... \ emeasure M {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} + emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" + using simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+) + also have "... < \" using insert(5)[OF F] fin_1[OF False] by (simp add: less_top) + finally show ?thesis by simp + qed + } + qed + moreover have "simple_function M (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast + moreover have "P (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast + ultimately show ?thesis by (intro cong[OF _ _ f(1,2)], blast, presburger+) +qed + +text \Induction rule for non-negative simple integrable functions\ +lemma\<^marker>\tag important\ integrable_simple_function_induct_nn[consumes 3, case_names cong indicator add, induct set: simple_function]: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes f: "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" "\x. x \ space M \ f x \ 0" + assumes cong: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ (\x. x \ space M \ f x \ 0) \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ (\x. x \ space M \ g x \ 0) \ (\x. x \ space M \ f x = g x) \ P f \ P g" + assumes indicator: "\A y. y \ 0 \ A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R y)" + assumes add: "\f g. (\x. x \ space M \ f x \ 0) \ simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ + (\x. x \ space M \ g x \ 0) \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ + (\z. z \ space M \ norm (f z + g z) = norm (f z) + norm (g z)) \ + P f \ P g \ P (\x. f x + g x)" + shows "P f" +proof- + let ?f = "\x. (\y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + have f_ae_eq: "f x = ?f x" if "x \ space M" for x using simple_function_indicator_representation[OF f(1) that] . + moreover have "emeasure M {y \ space M. ?f y \ 0} \ \" by (metis (no_types, lifting) Collect_cong calculation f(2)) + moreover have "P (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + "simple_function M (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + "emeasure M {y \ space M. (\x\S. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ \" + "\x. x \ space M \ 0 \ (\y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" + if "S \ f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that + proof (induction rule: finite_subset_induct') + case empty + { + case 1 + then show ?case using indicator[of 0 "{}"] by force + next + case 2 + then show ?case by force + next + case 3 + then show ?case by force + next + case 4 + then show ?case by force + } + next + case (insert x F) + have "(f -` {x} \ space M) \ {y \ space M. f y \ 0}" if "x \ 0" using that by blast + moreover have "{y \ space M. f y \ 0} = space M - (f -` {0} \ space M)" by blast + moreover have "space M - (f -` {0} \ space M) \ sets M" using simple_functionD(2)[OF f(1)] by blast + ultimately have fin_0: "emeasure M (f -` {x} \ space M) < \" if "x \ 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique) + hence fin_1: "emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0} \ \" if "x \ 0" by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that) + + have nonneg_x: "x \ 0" using insert f by blast + have *: "(\y\insert x F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) = (\y\F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) + indicat_real (f -` {x} \ space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) add.commute insert.hyps(1) insert.hyps(4) sum.insert) + have **: "{y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" unfolding * by fastforce + { + case 1 + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert by simp + next + case False + have norm_argument: "norm ((\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + indicat_real (f -` {x} \ space M) z *\<^sub>R x) = norm (\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \ space M) z *\<^sub>R x)" if z: "z \ space M" for z + proof (cases "f z = x") + case True + have "indicat_real (f -` {y} \ space M) z *\<^sub>R y = 0" if "y \ F" for y using True insert z that 1 unfolding indicator_def by force + hence "(\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) = 0" by (meson sum.neutral) + thus ?thesis by force + qed (force) + show ?thesis using False fin_0 fin_1 f norm_argument by (subst *, subst add, presburger add: insert, intro insert, intro insert, fastforce simp add: indicator_def intro!: insert(2) f(3), auto intro!: indicator insert nonneg_x) + qed + next + case 2 + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert by simp + next + case False + then show ?thesis unfolding * using insert simple_functionD(2)[OF f(1)] by fast + qed + next + case 3 + show ?case + proof (cases "x = 0") + case True + then show ?thesis unfolding * using insert by simp + next + case False + have "emeasure M {y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ emeasure M ({y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0})" + using ** simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] insert.IH(2) by (intro emeasure_mono, blast, simp) + also have "... \ emeasure M {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} + emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" + using simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+) + also have "... < \" using insert(7) fin_1[OF False] by (simp add: less_top) + finally show ?thesis by simp + qed + next + case (4 \) + thus ?case using insert nonneg_x f(3) by (auto simp add: scaleR_nonneg_nonneg intro: sum_nonneg) + } + qed + moreover have "simple_function M (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast + moreover have "P (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast + moreover have "\x. x \ space M \ 0 \ f x" using f(3) by simp + ultimately show ?thesis by (intro cong[OF _ _ _ f(1,2)], blast, blast, fast) presburger+ +qed + +lemma finite_nn_integral_imp_ae_finite: + fixes f :: "'a \ ennreal" + assumes "f \ borel_measurable M" "(\\<^sup>+x. f x \M) < \" + shows "AE x in M. f x < \" +proof (rule ccontr, goal_cases) + case 1 + let ?A = "space M \ {x. f x = \}" + have *: "emeasure M ?A > 0" using 1 assms(1) by (metis (mono_tags, lifting) assms(2) eventually_mono infinity_ennreal_def nn_integral_noteq_infinite top.not_eq_extremum) + have "(\\<^sup>+x. f x * indicator ?A x \M) = (\\<^sup>+x. \ * indicator ?A x \M)" by (metis (mono_tags, lifting) indicator_inter_arith indicator_simps(2) mem_Collect_eq mult_eq_0_iff) + also have "... = \ * emeasure M ?A" using assms(1) by (intro nn_integral_cmult_indicator, simp) + also have "... = \" using * by fastforce + finally have "(\\<^sup>+x. f x * indicator ?A x \M) = \" . + moreover have "(\\<^sup>+x. f x * indicator ?A x \M) \ (\\<^sup>+x. f x \M)" by (intro nn_integral_mono, simp add: indicator_def) + ultimately show ?case using assms(2) by simp +qed + +text \Convergence in L1-Norm implies existence of a subsequence which convergences almost everywhere. + This lemma is easier to use than the existing one in \<^theory>\HOL-Analysis.Bochner_Integration\\ + +lemma cauchy_L1_AE_cauchy_subseq: + fixes s :: "nat \ 'a \ 'b::{banach, second_countable_topology}" + assumes [measurable]: "\n. integrable M (s n)" + and "\e. e > 0 \ \N. \i\N. \j\N. LINT x|M. norm (s i x - s j x) < e" + obtains r where "strict_mono r" "AE x in M. Cauchy (\i. s (r i) x)" +proof- + have "\r. \n. (\i\r n. \j\ r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n) \ (r (Suc n) > r n)" + proof (intro dependent_nat_choice, goal_cases) + case 1 + then show ?case using assms(2) by presburger + next + case (2 x n) + obtain N where *: "LINT x|M. norm (s i x - s j x) < (1 / 2) ^ Suc n" if "i \ N" "j \ N" for i j using assms(2)[of "(1 / 2) ^ Suc n"] by auto + { + fix i j assume "i \ max N (Suc x)" "j \ max N (Suc x)" + hence "integral\<^sup>L M (\x. norm (s i x - s j x)) < (1 / 2) ^ Suc n" using * by fastforce + } + then show ?case by fastforce + qed + then obtain r where strict_mono: "strict_mono r" and "\i\r n. \j\ r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n" for n using strict_mono_Suc_iff by blast + hence r_is: "LINT x|M. norm (s (r (Suc n)) x - s (r n) x) < (1 / 2) ^ n" for n by (simp add: strict_mono_leD) + + define g where "g = (\n x. (\i\n. ennreal (norm (s (r (Suc i)) x - s (r i) x))))" + define g' where "g' = (\x. \i. ennreal (norm (s (r (Suc i)) x - s (r i) x)))" + + have integrable_g: "(\\<^sup>+ x. g n x \M) < 2" for n + proof - + have "(\\<^sup>+ x. g n x \M) = (\\<^sup>+ x. (\i\n. ennreal (norm (s (r (Suc i)) x - s (r i) x))) \M)" using g_def by simp + also have "... = (\i\n. (\\<^sup>+ x. ennreal (norm (s (r (Suc i)) x - s (r i) x)) \M))" by (intro nn_integral_sum, simp) + also have "... = (\i\n. LINT x|M. norm (s (r (Suc i)) x - s (r i) x))" unfolding dist_norm using assms(1) by (subst nn_integral_eq_integral[OF integrable_norm], auto) + also have "... < ennreal (\i\n. (1 / 2) ^ i)" by (intro ennreal_lessI[OF sum_pos sum_strict_mono[OF finite_atMost _ r_is]], auto) + also have "... \ ennreal 2" unfolding sum_gp0[of "1 / 2" n] by (intro ennreal_leI, auto) + finally show "(\\<^sup>+ x. g n x \M) < 2" by simp + qed + + have integrable_g': "(\\<^sup>+ x. g' x \M) \ 2" + proof - + have "incseq (\n. g n x)" for x by (intro incseq_SucI, auto simp add: g_def ennreal_leI) + hence "convergent (\n. g n x)" for x unfolding convergent_def using LIMSEQ_incseq_SUP by fast + hence "(\n. g n x) \ g' x" for x unfolding g_def g'_def by (intro summable_iff_convergent'[THEN iffD2, THEN summable_LIMSEQ'], blast) + hence "(\\<^sup>+ x. g' x \M) = (\\<^sup>+ x. liminf (\n. g n x) \M)" by (metis lim_imp_Liminf trivial_limit_sequentially) + also have "... \ liminf (\n. \\<^sup>+ x. g n x \M)" by (intro nn_integral_liminf, simp add: g_def) + also have "... \ liminf (\n. 2)" using integrable_g by (intro Liminf_mono) (simp add: order_le_less) + also have "... = 2" using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast + finally show ?thesis . + qed + hence "AE x in M. g' x < \" by (intro finite_nn_integral_imp_ae_finite) (auto simp add: order_le_less_trans g'_def) + moreover have "summable (\i. norm (s (r (Suc i)) x - s (r i) x))" if "g' x \ \" for x using that unfolding g'_def by (intro summable_suminf_not_top) fastforce+ + ultimately have ae_summable: "AE x in M. summable (\i. s (r (Suc i)) x - s (r i) x)" using summable_norm_cancel unfolding dist_norm by force + + { + fix x assume "summable (\i. s (r (Suc i)) x - s (r i) x)" + hence "(\n. \i (\i. s (r (Suc i)) x - s (r i) x)" using summable_LIMSEQ by blast + moreover have "(\n. (\in. s (r n) x - s (r 0) x)" using sum_lessThan_telescope by fastforce + ultimately have "(\n. s (r n) x - s (r 0) x) \ (\i. s (r (Suc i)) x - s (r i) x)" by argo + hence "(\n. s (r n) x - s (r 0) x + s (r 0) x) \ (\i. s (r (Suc i)) x - s (r i) x) + s (r 0) x" by (intro isCont_tendsto_compose[of _ "\z. z + s (r 0) x"], auto) + hence "Cauchy (\n. s (r n) x)" by (simp add: LIMSEQ_imp_Cauchy) + } + hence "AE x in M. Cauchy (\i. s (r i) x)" using ae_summable by fast + thus ?thesis by (rule that[OF strict_mono(1)]) +qed + +subsection \Totally Ordered Banach Spaces\ + +lemma integrable_max[simp, intro]: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology}" + assumes fg[measurable]: "integrable M f" "integrable M g" + shows "integrable M (\x. max (f x) (g x))" +proof (rule Bochner_Integration.integrable_bound) + { + fix x y :: 'b + have "norm (max x y) \ max (norm x) (norm y)" by linarith + also have "... \ norm x + norm y" by simp + finally have "norm (max x y) \ norm (norm x + norm y)" by simp + } + thus "AE x in M. norm (max (f x) (g x)) \ norm (norm (f x) + norm (g x))" by simp +qed (auto intro: Bochner_Integration.integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]) + +lemma integrable_min[simp, intro]: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology}" + assumes [measurable]: "integrable M f" "integrable M g" + shows "integrable M (\x. min (f x) (g x))" +proof - + have "norm (min (f x) (g x)) \ norm (f x) \ norm (min (f x) (g x)) \ norm (g x)" for x by linarith + thus ?thesis by (intro integrable_bound[OF integrable_max[OF integrable_norm(1,1), OF assms]], auto) +qed + +text \Restatement of \integral_nonneg_AE\ for functions taking values in a Banach space.\ +lemma integral_nonneg_AE_banach: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes [measurable]: "f \ borel_measurable M" and nonneg: "AE x in M. 0 \ f x" + shows "0 \ integral\<^sup>L M f" +proof cases + assume integrable: "integrable M f" + hence max: "(\x. max 0 (f x)) \ borel_measurable M" "\x. 0 \ max 0 (f x)" "integrable M (\x. max 0 (f x))" by auto + hence "0 \ integral\<^sup>L M (\x. max 0 (f x))" + proof - + obtain s where *: "\i. simple_function M (s i)" + "\i. emeasure M {y \ space M. s i y \ 0} \ \" + "\x. x \ space M \ (\i. s i x) \ f x" + "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" using integrable_implies_simple_function_sequence[OF integrable] by blast + have simple: "\i. simple_function M (\x. max 0 (s i x))" using * by fast + have "\i. {y \ space M. max 0 (s i y) \ 0} \ {y \ space M. s i y \ 0}" unfolding max_def by force + moreover have "\i. {y \ space M. s i y \ 0} \ sets M" using * by measurable + ultimately have "\i. emeasure M {y \ space M. max 0 (s i y) \ 0} \ emeasure M {y \ space M. s i y \ 0}" by (rule emeasure_mono) + hence **:"\i. emeasure M {y \ space M. max 0 (s i y) \ 0} \ \" using *(2) by (auto intro: order.strict_trans1 simp add: top.not_eq_extremum) + have "\x. x \ space M \ (\i. max 0 (s i x)) \ max 0 (f x)" using *(3) tendsto_max by blast + moreover have "\x i. x \ space M \ norm (max 0 (s i x)) \ norm (2 *\<^sub>R f x)" using *(4) unfolding max_def by auto + ultimately have tendsto: "(\i. integral\<^sup>L M (\x. max 0 (s i x))) \ integral\<^sup>L M (\x. max 0 (f x))" + using borel_measurable_simple_function simple integrable by (intro integral_dominated_convergence[OF max(1) _ integrable_norm[OF integrable_scaleR_right], of _ 2 f], blast+) + { + fix h :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assume "simple_function M h" "emeasure M {y \ space M. h y \ 0} \ \" "\x. x \ space M \ h x \ 0" + hence *: "integral\<^sup>L M h \ 0" + proof (induct rule: integrable_simple_function_induct_nn) + case (cong f g) + then show ?case using Bochner_Integration.integral_cong by force + next + case (indicator A y) + hence "A \ {} \ y \ 0" using sets.sets_into_space by fastforce + then show ?case using indicator by (cases "A = {}", auto simp add: scaleR_nonneg_nonneg) + next + case (add f g) + then show ?case by (simp add: integrable_simple_function) + qed + } + thus ?thesis using LIMSEQ_le_const[OF tendsto, of 0] ** simple by fastforce + qed + also have "\ = integral\<^sup>L M f" using nonneg by (auto intro: integral_cong_AE) + finally show ?thesis . +qed (simp add: not_integrable_integral_eq) + +lemma integral_mono_AE_banach: + fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" "AE x in M. f x \ g x" + shows "integral\<^sup>L M f \ integral\<^sup>L M g" + using integral_nonneg_AE_banach[of "\x. g x - f x"] assms Bochner_Integration.integral_diff[OF assms(1,2)] by force + +lemma integral_mono_banach: + fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" "\x. x \ space M \ f x \ g x" + shows "integral\<^sup>L M f \ integral\<^sup>L M g" + using integral_mono_AE_banach assms by blast + +subsection \Integrability and Measurability of the Diameter\ + +context + fixes s :: "nat \ 'a \ 'b :: {second_countable_topology, banach}" and M + assumes bounded: "\x. x \ space M \ bounded (range (\i. s i x))" +begin + +lemma borel_measurable_diameter: + assumes [measurable]: "\i. (s i) \ borel_measurable M" + shows "(\x. diameter {s i x |i. n \ i}) \ borel_measurable M" +proof - + have "{s i x |i. N \ i} \ {}" for x N by blast + hence diameter_SUP: "diameter {s i x |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) + + have "case_prod dist ` ({s i x |i. n \ i} \ {s i x |i. n \ i}) = ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" for x by fast + hence *: "(\x. diameter {s i x |i. n \ i}) = (\x. Sup ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})))" using diameter_SUP by (simp add: case_prod_beta') + + have "bounded ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" if "x \ space M" for x by (rule bounded_imp_dist_bounded[OF bounded, OF that]) + hence bdd: "bdd_above ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" if "x \ space M" for x using that bounded_imp_bdd_above by presburger + have "fst p \ borel_measurable M" "snd p \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p using that by fastforce+ + hence "(\x. fst p x - snd p x) \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p using that borel_measurable_diff by simp + hence "(\x. case p of (f, g) \ dist (f x) (g x)) \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p unfolding dist_norm using that by measurable + moreover have "countable (s ` {n..} \ s ` {n..})" by (intro countable_SIGMA countable_image, auto) + ultimately show ?thesis unfolding * by (auto intro!: borel_measurable_cSUP bdd) +qed + +lemma integrable_bound_diameter: + fixes f :: "'a \ real" + assumes "integrable M f" + and [measurable]: "\i. (s i) \ borel_measurable M" + and "\x i. x \ space M \ norm (s i x) \ f x" + shows "integrable M (\x. diameter {s i x |i. n \ i})" +proof - + have "{s i x |i. N \ i} \ {}" for x N by blast + hence diameter_SUP: "diameter {s i x |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) + { + fix x assume x: "x \ space M" + let ?S = "(\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})" + have "case_prod dist ` ({s i x |i. n \ i} \ {s i x |i. n \ i}) = (\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})" by fast + hence *: "diameter {s i x |i. n \ i} = Sup ?S" using diameter_SUP by (simp add: case_prod_beta') + + have "bounded ?S" by (rule bounded_imp_dist_bounded[OF bounded[OF x]]) + hence Sup_S_nonneg:"0 \ Sup ?S" by (auto intro!: cSup_upper2 x bounded_imp_bdd_above) + + have "dist (s i x) (s j x) \ 2 * f x" for i j by (intro dist_triangle2[THEN order_trans, of _ 0]) (metis norm_conv_dist assms(3) x add_mono mult_2) + hence "\c \ ?S. c \ 2 * f x" by force + hence "Sup ?S \ 2 * f x" by (intro cSup_least, auto) + hence "norm (Sup ?S) \ 2 * norm (f x)" using Sup_S_nonneg by auto + also have "... = norm (2 *\<^sub>R f x)" by simp + finally have "norm (diameter {s i x |i. n \ i}) \ norm (2 *\<^sub>R f x)" unfolding * . + } + hence "AE x in M. norm (diameter {s i x |i. n \ i}) \ norm (2 *\<^sub>R f x)" by blast + thus "integrable M (\x. diameter {s i x |i. n \ i})" using borel_measurable_diameter by (intro Bochner_Integration.integrable_bound[OF assms(1)[THEN integrable_scaleR_right[of 2]]], measurable) +qed +end + +subsection \Auxiliary Lemmas for Set Integrals\ + +lemma set_integral_scaleR_left: + assumes "A \ sets M" "c \ 0 \ integrable M f" + shows "LINT t:A|M. f t *\<^sub>R c = (LINT t:A|M. f t) *\<^sub>R c" + unfolding set_lebesgue_integral_def + using integrable_mult_indicator[OF assms] + by (subst integral_scaleR_left[symmetric], auto) + +lemma nn_set_integral_eq_set_integral: + assumes [measurable]:"integrable M f" + and "AE x \ A in M. 0 \ f x" "A \ sets M" + shows "(\\<^sup>+x\A. f x \M) = (\ x \ A. f x \M)" +proof- + have "(\\<^sup>+x. indicator A x *\<^sub>R f x \M) = (\ x \ A. f x \M)" + unfolding set_lebesgue_integral_def using assms(2) by (intro nn_integral_eq_integral[of _ "\x. indicat_real A x *\<^sub>R f x"], blast intro: assms integrable_mult_indicator, fastforce) + moreover have "(\\<^sup>+x. indicator A x *\<^sub>R f x \M) = (\\<^sup>+x\A. f x \M)" by (metis ennreal_0 indicator_simps(1) indicator_simps(2) mult.commute mult_1 mult_zero_left real_scaleR_def) + ultimately show ?thesis by argo +qed + +lemma set_integral_restrict_space: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + assumes "\ \ space M \ sets M" + shows "set_lebesgue_integral (restrict_space M \) A f = set_lebesgue_integral M A (\x. indicator \ x *\<^sub>R f x)" + unfolding set_lebesgue_integral_def + by (subst integral_restrict_space, auto intro!: integrable_mult_indicator assms simp: mult.commute) + +lemma set_integral_const: + fixes c :: "'b::{banach, second_countable_topology}" + assumes "A \ sets M" "emeasure M A \ \" + shows "set_lebesgue_integral M A (\_. c) = measure M A *\<^sub>R c" + unfolding set_lebesgue_integral_def + using assms by (metis has_bochner_integral_indicator has_bochner_integral_integral_eq infinity_ennreal_def less_top) + +lemma set_integral_mono_banach: + fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "set_integrable M A f" "set_integrable M A g" + "\x. x \ A \ f x \ g x" + shows "(LINT x:A|M. f x) \ (LINT x:A|M. g x)" + using assms unfolding set_integrable_def set_lebesgue_integral_def + by (auto intro: integral_mono_banach split: split_indicator) + +lemma set_integral_mono_AE_banach: + fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "set_integrable M A f" "set_integrable M A g" "AE x\A in M. f x \ g x" + shows "set_lebesgue_integral M A f \ set_lebesgue_integral M A g" using assms unfolding set_lebesgue_integral_def by (auto simp add: set_integrable_def intro!: integral_mono_AE_banach[of M "\x. indicator A x *\<^sub>R f x" "\x. indicator A x *\<^sub>R g x"], simp add: indicator_def) + +subsection \Averaging Theorem\ + +text \We aim to lift results from the real case to arbitrary Banach spaces. + Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \cite{Lang_1993}. + The theorem allows us to make statements about a function’s value almost everywhere, depending on the value its integral takes on various sets of the measure space.\ + +text \Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof. + While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \cite{engelking_1989}.\ +(* Engelking's book General Topology *) +lemma balls_countable_basis: + obtains D :: "'a :: {metric_space, second_countable_topology} set" + where "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" + and "countable D" + and "D \ {}" +proof - + obtain D :: "'a set" where dense_subset: "countable D" "D \ {}" "\open U; U \ {}\ \ \y \ D. y \ U" for U using countable_dense_exists by blast + have "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" + proof (intro topological_basis_iff[THEN iffD2], fast, clarify) + fix U and x :: 'a assume asm: "open U" "x \ U" + obtain e where e: "e > 0" "ball x e \ U" using asm openE by blast + obtain y where y: "y \ D" "y \ ball x (e / 3)" using dense_subset(3)[OF open_ball, of x "e / 3"] centre_in_ball[THEN iffD2, OF divide_pos_pos[OF e(1), of 3]] by force + obtain r where r: "r \ \ \ {e/3<.. ball y r" using r y by (simp add: dist_commute) + hence "ball y r \ U" using r by (intro order_trans[OF _ e(2)], simp, metric) + moreover have "ball y r \ (case_prod ball ` (D \ (\ \ {0<..})))" using y(1) r by force + ultimately show "\B'\(case_prod ball ` (D \ (\ \ {0<..}))). x \ B' \ B' \ U" using * by meson + qed + thus ?thesis using that dense_subset by blast +qed + +context sigma_finite_measure +begin + +text \To show statements concerning \\\-finite measure spaces, one usually shows the statement for finite measure spaces and uses a limiting argument to show it for the \\\-finite case. + The following induction scheme formalizes this.\ +lemma sigma_finite_measure_induct[case_names finite_measure, consumes 0]: + assumes "\(N :: 'a measure) \. finite_measure N + \ N = restrict_space M \ + \ \ \ sets M + \ emeasure N \ \ \ + \ emeasure N \ \ 0 + \ almost_everywhere N Q" + and [measurable]: "Measurable.pred M Q" + shows "almost_everywhere M Q" +proof - + have *: "almost_everywhere N Q" if "finite_measure N" "N = restrict_space M \" "\ \ sets M" "emeasure N \ \ \" for N \ using that by (cases "emeasure N \ = 0", auto intro: emeasure_0_AE assms(1)) + + obtain A :: "nat \ 'a set" where A: "range A \ sets M" "(\i. A i) = space M" and emeasure_finite: "emeasure M (A i) \ \" for i using sigma_finite by metis + note A(1)[measurable] + have space_restr: "space (restrict_space M (A i)) = A i" for i unfolding space_restrict_space by simp + { + fix i + have *: "{x \ A i \ space M. Q x} = {x \ space M. Q x} \ (A i)" by fast + have "Measurable.pred (restrict_space M (A i)) Q" using A by (intro measurableI, auto simp add: space_restr intro!: sets_restrict_space_iff[THEN iffD2], measurable, auto) + } + note this[measurable] + { + fix i + have "finite_measure (restrict_space M (A i))" using emeasure_finite by (intro finite_measureI, subst space_restr, subst emeasure_restrict_space, auto) + hence "emeasure (restrict_space M (A i)) {x \ A i. \Q x} = 0" using emeasure_finite by (intro AE_iff_measurable[THEN iffD1, OF _ _ *], measurable, subst space_restr[symmetric], intro sets.top, auto simp add: emeasure_restrict_space) + hence "emeasure M {x \ A i. \ Q x} = 0" by (subst emeasure_restrict_space[symmetric], auto) + } + hence "emeasure M (\i. {x \ A i. \ Q x}) = 0" by (intro emeasure_UN_eq_0, auto) + moreover have "(\i. {x \ A i. \ Q x}) = {x \ space M. \ Q x}" using A by auto + ultimately show ?thesis by (intro AE_iff_measurable[THEN iffD2], auto) +qed + +(* Real Functional Analysis - Lang*) +text \The Averaging Theorem allows us to make statements concerning how a function behaves almost everywhere, depending on its behaviour on average.\ +lemma averaging_theorem: + fixes f::"_ \ 'b::{second_countable_topology, banach}" + assumes [measurable]:"integrable M f" + and closed: "closed S" + and "\A. A \ sets M \ measure M A > 0 \ (1 / measure M A) *\<^sub>R set_lebesgue_integral M A f \ S" + shows "AE x in M. f x \ S" +proof (induct rule: sigma_finite_measure_induct) + case (finite_measure N \) + + interpret finite_measure N by (rule finite_measure) + + have integrable[measurable]: "integrable N f" using assms finite_measure by (auto simp: integrable_restrict_space integrable_mult_indicator) + have average: "(1 / Sigma_Algebra.measure N A) *\<^sub>R set_lebesgue_integral N A f \ S" if "A \ sets N" "measure N A > 0" for A + proof - + have *: "A \ sets M" using that by (simp add: sets_restrict_space_iff finite_measure) + have "A = A \ \" by (metis finite_measure(2,3) inf.orderE sets.sets_into_space space_restrict_space that(1)) + hence "set_lebesgue_integral N A f = set_lebesgue_integral M A f" unfolding finite_measure by (subst set_integral_restrict_space, auto simp add: finite_measure set_lebesgue_integral_def indicator_inter_arith[symmetric]) + moreover have "measure N A = measure M A" using that by (auto intro!: measure_restrict_space simp add: finite_measure sets_restrict_space_iff) + ultimately show ?thesis using that * assms(3) by presburger + qed + + obtain D :: "'b set" where balls_basis: "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" and countable_D: "countable D" using balls_countable_basis by blast + have countable_balls: "countable (case_prod ball ` (D \ (\ \ {0<..})))" using countable_rat countable_D by blast + + obtain B where B_balls: "B \ case_prod ball ` (D \ (\ \ {0<..}))" "\B = -S" using topological_basis[THEN iffD1, OF balls_basis] open_Compl[OF assms(2)] by meson + hence countable_B: "countable B" using countable_balls countable_subset by fast + + define b where "b = from_nat_into (B \ {{}})" + have "B \ {{}} \ {}" by simp + have range_b: "range b = B \ {{}}" using countable_B by (auto simp add: b_def intro!: range_from_nat_into) + have open_b: "open (b i)" for i unfolding b_def using B_balls open_ball from_nat_into[of "B \ {{}}" i] by force + have Union_range_b: "\(range b) = -S" using B_balls range_b by simp + + { + fix v r assume ball_in_Compl: "ball v r \ -S" + define A where "A = f -` ball v r \ space N" + have dist_less: "dist (f x) v < r" if "x \ A" for x using that unfolding A_def vimage_def by (simp add: dist_commute) + hence AE_less: "AE x \ A in N. norm (f x - v) < r" by (auto simp add: dist_norm) + have *: "A \ sets N" unfolding A_def by simp + have "emeasure N A = 0" + proof - + { + assume asm: "emeasure N A > 0" + hence measure_pos: "measure N A > 0" unfolding emeasure_eq_measure by simp + hence "(1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v = (1 / measure N A) *\<^sub>R set_lebesgue_integral N A (\x. f x - v)" using integrable integrable_const * by (subst set_integral_diff(2), auto simp add: set_integrable_def set_integral_const[OF *] algebra_simps intro!: integrable_mult_indicator) + moreover have "norm (\x\A. (f x - v)\N) \ (\x\A. norm (f x - v)\N)" using * by (auto intro!: integral_norm_bound[of N "\x. indicator A x *\<^sub>R (f x - v)", THEN order_trans] integrable_mult_indicator integrable simp add: set_lebesgue_integral_def) + ultimately have "norm ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v) \ set_lebesgue_integral N A (\x. norm (f x - v)) / measure N A" using asm by (auto intro: divide_right_mono) + also have "... < set_lebesgue_integral N A (\x. r) / measure N A" + unfolding set_lebesgue_integral_def + using asm * integrable integrable_const AE_less measure_pos + by (intro divide_strict_right_mono integral_less_AE[of _ _ A] integrable_mult_indicator) + (fastforce simp add: dist_less dist_norm indicator_def)+ + also have "... = r" using * measure_pos by (simp add: set_integral_const) + finally have "dist ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f) v < r" by (subst dist_norm) + hence "False" using average[OF * measure_pos] by (metis ComplD dist_commute in_mono mem_ball ball_in_Compl) + } + thus ?thesis by fastforce + qed + } + note * = this + { + fix b' assume "b' \ B" + hence ball_subset_Compl: "b' \ -S" and ball_radius_pos: "\v \ D. \r>0. b' = ball v r" using B_balls by (blast, fast) + } + note ** = this + hence "emeasure N (f -` b i \ space N) = 0" for i by (cases "b i = {}", simp) (metis UnE singletonD * range_b[THEN eq_refl, THEN range_subsetD]) + hence "emeasure N (\i. f -` b i \ space N) = 0" using open_b by (intro emeasure_UN_eq_0) fastforce+ + moreover have "(\i. f -` b i \ space N) = f -` (\(range b)) \ space N" by blast + ultimately have "emeasure N (f -` (-S) \ space N) = 0" using Union_range_b by argo + hence "AE x in N. f x \ -S" using open_Compl[OF assms(2)] by (intro AE_iff_measurable[THEN iffD2], auto) + thus ?case by force +qed (simp add: pred_sets2[OF borel_closed] assms(2)) + +lemma density_zero: + fixes f::"'a \ 'b::{second_countable_topology, banach}" + assumes "integrable M f" + and density_0: "\A. A \ sets M \ set_lebesgue_integral M A f = 0" + shows "AE x in M. f x = 0" + using averaging_theorem[OF assms(1), of "{0}"] assms(2) + by (simp add: scaleR_nonneg_nonneg) + +text \The following lemma shows that densities are unique in Banach spaces.\ +lemma density_unique_banach: + fixes f f'::"'a \ 'b::{second_countable_topology, banach}" + assumes "integrable M f" "integrable M f'" + and density_eq: "\A. A \ sets M \ set_lebesgue_integral M A f = set_lebesgue_integral M A f'" + shows "AE x in M. f x = f' x" +proof- + { + fix A assume asm: "A \ sets M" + hence "LINT x|M. indicat_real A x *\<^sub>R (f x - f' x) = 0" using density_eq assms(1,2) by (simp add: set_lebesgue_integral_def algebra_simps Bochner_Integration.integral_diff[OF integrable_mult_indicator(1,1)]) + } + thus ?thesis using density_zero[OF Bochner_Integration.integrable_diff[OF assms(1,2)]] by (simp add: set_lebesgue_integral_def) +qed + +lemma density_nonneg: + fixes f::"_ \ 'b::{second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" + and "\A. A \ sets M \ set_lebesgue_integral M A f \ 0" + shows "AE x in M. f x \ 0" + using averaging_theorem[OF assms(1), of "{0..}", OF closed_atLeast] assms(2) + by (simp add: scaleR_nonneg_nonneg) + +corollary integral_nonneg_eq_0_iff_AE_banach: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \ f x" + shows "integral\<^sup>L M f = 0 \ (AE x in M. f x = 0)" +proof + assume *: "integral\<^sup>L M f = 0" + { + fix A assume asm: "A \ sets M" + have "0 \ integral\<^sup>L M (\x. indicator A x *\<^sub>R f x)" using nonneg by (subst integral_zero[of M, symmetric], intro integral_mono_AE_banach integrable_mult_indicator asm f integrable_zero, auto simp add: indicator_def) + moreover have "... \ integral\<^sup>L M f" using nonneg by (intro integral_mono_AE_banach integrable_mult_indicator asm f, auto simp add: indicator_def) + ultimately have "set_lebesgue_integral M A f = 0" unfolding set_lebesgue_integral_def using * by force + } + thus "AE x in M. f x = 0" by (intro density_zero f, blast) +qed (auto simp add: integral_eq_zero_AE) + +corollary integral_eq_mono_AE_eq_AE: + fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" "integral\<^sup>L M f = integral\<^sup>L M g" "AE x in M. f x \ g x" + shows "AE x in M. f x = g x" +proof - + define h where "h = (\x. g x - f x)" + have "AE x in M. h x = 0" unfolding h_def using assms by (subst integral_nonneg_eq_0_iff_AE_banach[symmetric]) auto + then show ?thesis unfolding h_def by auto +qed + +end + +end \ No newline at end of file diff --git a/thys/Martingales/Conditional_Expectation_Banach.thy b/thys/Martingales/Conditional_Expectation_Banach.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Conditional_Expectation_Banach.thy @@ -0,0 +1,1048 @@ +(* Author: Ata Keskin, TU München +*) + +theory Conditional_Expectation_Banach + imports "HOL-Probability.Conditional_Expectation" "HOL-Probability.Independent_Family" Bochner_Integration_Supplement +begin + +section \Conditional Expectation in Banach Spaces\ + +text \While constructing the conditional expectation operator, we have come up with the following approach, which is based on the construction in \cite{Hytoenen_2016}. + Both our approach, and the one in \cite{Hytoenen_2016} are based on showing that the conditional expectation is a contraction on some dense subspace of the space of functions \L\<^sup>1(E)\. + In our approach, we start by constructing the conditional expectation explicitly for simple functions. + Then we show that the conditional expectation is a contraction on simple functions, i.e. \\E(s|F)(x)\ \ E(\s(x)\|F)\ for \\\-almost all \x \ \\ with \s : \ \ E\ simple and integrable. + Using this, we can show that the conditional expectation of a convergent sequence of simple functions is again convergent. + Finally, we show that this limit exhibits the properties of a conditional expectation. + This approach has the benefit of being straightforward and easy to implement, since we could make use of the existing formalization for real-valued functions. + To use the construction in \cite{Hytoenen_2016} we need more tools from functional analysis, which Isabelle/HOL currently does not have.\ + +text \Before we can talk about 'the' conditional expectation, we must define what it means for a function to have a conditional expectation.\ + +definition has_cond_exp :: "'a measure \ 'a measure \ ('a \ 'b) \ ('a \ 'b::{real_normed_vector, second_countable_topology}) \ bool" where + "has_cond_exp M F f g = ((\A \ sets F. (\ x \ A. f x \M) = (\ x \ A. g x \M)) + \ integrable M f + \ integrable M g + \ g \ borel_measurable F)" + +text \This predicate precisely characterizes what it means for a function \<^term>\f\ to have a conditional expectation \<^term>\g\, + with respect to the measure \<^term>\M\ and the sub-\\\-algebra \<^term>\F\.\ + +lemma has_cond_expI': + assumes "\A. A \ sets F \ (\ x \ A. f x \M) = (\ x \ A. g x \M)" + "integrable M f" + "integrable M g" + "g \ borel_measurable F" + shows "has_cond_exp M F f g" + using assms unfolding has_cond_exp_def by simp + +lemma has_cond_expD: + assumes "has_cond_exp M F f g" + shows "\A. A \ sets F \ (\ x \ A. f x \M) = (\ x \ A. g x \M)" + "integrable M f" + "integrable M g" + "g \ borel_measurable F" + using assms unfolding has_cond_exp_def by simp+ + +text \Now we can use Hilbert’s \\\-operator to define the conditional expectation, if it exists.\ + +definition cond_exp :: "'a measure \ 'a measure \ ('a \ 'b) \ ('a \ 'b::{banach, second_countable_topology})" where + "cond_exp M F f = (if \g. has_cond_exp M F f g then (SOME g. has_cond_exp M F f g) else (\_. 0))" + +lemma borel_measurable_cond_exp[measurable]: "cond_exp M F f \ borel_measurable F" + by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const) + +lemma integrable_cond_exp[intro]: "integrable M (cond_exp M F f)" + by (metis cond_exp_def has_cond_expD(3) integrable_zero someI) + +lemma set_integrable_cond_exp[intro]: + assumes "A \ sets M" + shows "set_integrable M A (cond_exp M F f)" using integrable_mult_indicator[OF assms integrable_cond_exp, of F f] by (auto simp add: set_integrable_def intro!: integrable_mult_indicator[OF assms integrable_cond_exp]) + +lemma has_cond_exp_self: + assumes "integrable M f" + shows "has_cond_exp M (vimage_algebra (space M) f borel) f f" + using assms by (auto intro!: has_cond_expI' measurable_vimage_algebra1) + +lemma has_cond_exp_sets_cong: + assumes "sets F = sets G" + shows "has_cond_exp M F = has_cond_exp M G" + using assms unfolding has_cond_exp_def by force + +lemma cond_exp_sets_cong: + assumes "sets F = sets G" + shows "AE x in M. cond_exp M F f x = cond_exp M G f x" + by (intro AE_I2, simp add: cond_exp_def has_cond_exp_sets_cong[OF assms, of M]) + +context sigma_finite_subalgebra +begin + +lemma borel_measurable_cond_exp'[measurable]: "cond_exp M F f \ borel_measurable M" + by (metis cond_exp_def someI has_cond_exp_def borel_measurable_const subalg measurable_from_subalg) + +lemma cond_exp_null: + assumes "\g. has_cond_exp M F f g" + shows "cond_exp M F f = (\_. 0)" + unfolding cond_exp_def using assms by argo + +text \We state the tower property of the conditional expectation in terms of the predicate \<^term>\has_cond_exp\.\ + +lemma has_cond_exp_nested_subalg: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "subalgebra G F" "has_cond_exp M F f h" "has_cond_exp M G f h'" + shows "has_cond_exp M F h' h" + by (intro has_cond_expI') (metis assms has_cond_expD in_mono subalgebra_def)+ + +text \The following lemma shows that the conditional expectation is unique as an element of L1, given that it exists.\ + +lemma has_cond_exp_charact: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "has_cond_exp M F f g" + shows "has_cond_exp M F f (cond_exp M F f)" + "AE x in M. cond_exp M F f x = g x" +proof - + show cond_exp: "has_cond_exp M F f (cond_exp M F f)" using assms someI cond_exp_def by metis + let ?MF = "restr_to_subalg M F" + interpret sigma_finite_measure ?MF by (rule sigma_fin_subalg) + { + fix A assume "A \ sets ?MF" + then have [measurable]: "A \ sets F" using sets_restr_to_subalg[OF subalg] by simp + have "(\x \ A. g x \?MF) = (\x \ A. g x \M)" using assms subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def dest!: has_cond_expD) + also have "... = (\x \ A. cond_exp M F f x \M)" using assms cond_exp by (simp add: has_cond_exp_def) + also have "... = (\x \ A. cond_exp M F f x \?MF)" using subalg by (auto simp add: integral_subalgebra2 set_lebesgue_integral_def) + finally have "(\x \ A. g x \?MF) = (\x \ A. cond_exp M F f x \?MF)" by simp + } + hence "AE x in ?MF. cond_exp M F f x = g x" using cond_exp assms subalg by (intro density_unique_banach, auto dest: has_cond_expD intro!: integrable_in_subalg) + then show "AE x in M. cond_exp M F f x = g x" using AE_restr_to_subalg[OF subalg] by simp +qed + +corollary cond_exp_charact: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "\A. A \ sets F \ (\ x \ A. f x \M) = (\ x \ A. g x \M)" + "integrable M f" + "integrable M g" + "g \ borel_measurable F" + shows "AE x in M. cond_exp M F f x = g x" + by (intro has_cond_exp_charact has_cond_expI' assms) auto + +text \Identity on F-measurable functions:\ + +text \If an integrable function \<^term>\f\ is already \<^term>\F\-measurable, then \<^term>\cond_exp M F f = f\ \\\-a.e. + This is a corollary of the lemma on the characterization of \<^term>\cond_exp\.\ +corollary cond_exp_F_meas[intro, simp]: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "integrable M f" + "f \ borel_measurable F" + shows "AE x in M. cond_exp M F f x = f x" + by (rule cond_exp_charact, auto intro: assms) + +text \Congruence\ + +lemma has_cond_exp_cong: + assumes "integrable M f" "\x. x \ space M \ f x = g x" "has_cond_exp M F g h" + shows "has_cond_exp M F f h" +proof (intro has_cond_expI'[OF _ assms(1)]) + fix A assume asm: "A \ sets F" + hence "set_lebesgue_integral M A f = set_lebesgue_integral M A g" by (intro set_lebesgue_integral_cong) (meson assms(2) subalg in_mono subalgebra_def sets.sets_into_space subalgebra_def subsetD)+ + thus "set_lebesgue_integral M A f = set_lebesgue_integral M A h" using asm assms(3) by (simp add: has_cond_exp_def) +qed (auto simp add: has_cond_expD[OF assms(3)]) + +lemma cond_exp_cong: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" "integrable M g" "\x. x \ space M \ f x = g x" + shows "AE x in M. cond_exp M F f x = cond_exp M F g x" +proof (cases "\h. has_cond_exp M F f h") + case True + then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong assms by metis + show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce +next + case False + moreover have "\h. has_cond_exp M F g h" using False has_cond_exp_cong assms by auto + ultimately show ?thesis unfolding cond_exp_def by auto +qed + +lemma has_cond_exp_cong_AE: + assumes "integrable M f" "AE x in M. f x = g x" "has_cond_exp M F g h" + shows "has_cond_exp M F f h" + using assms(1,2) subalg subalgebra_def subset_iff + by (intro has_cond_expI', subst set_lebesgue_integral_cong_AE[OF _ assms(1)[THEN borel_measurable_integrable] borel_measurable_integrable(1)[OF has_cond_expD(2)[OF assms(3)]]]) + (fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+ + +lemma has_cond_exp_cong_AE': + assumes "h \ borel_measurable F" "AE x in M. h x = h' x" "has_cond_exp M F f h'" + shows "has_cond_exp M F f h" + using assms(1, 2) subalg subalgebra_def subset_iff + using AE_restr_to_subalg2[OF subalg assms(2)] measurable_from_subalg + by (intro has_cond_expI' , subst set_lebesgue_integral_cong_AE[OF _ measurable_from_subalg(1,1)[OF subalg], OF _ assms(1) has_cond_expD(4)[OF assms(3)]]) + (fast intro: has_cond_expD[OF assms(3)] integrable_cong_AE_imp[OF _ _ AE_symmetric])+ + +lemma cond_exp_cong_AE: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" "integrable M g" "AE x in M. f x = g x" + shows "AE x in M. cond_exp M F f x = cond_exp M F g x" +proof (cases "\h. has_cond_exp M F f h") + case True + then obtain h where h: "has_cond_exp M F f h" "has_cond_exp M F g h" using has_cond_exp_cong_AE assms by (metis (mono_tags, lifting) eventually_mono) + show ?thesis using h[THEN has_cond_exp_charact(2)] by fastforce +next + case False + moreover have "\h. has_cond_exp M F g h" using False has_cond_exp_cong_AE assms by auto + ultimately show ?thesis unfolding cond_exp_def by auto +qed + +text \The conditional expectation operator on the reals, \<^term>\real_cond_exp\, satisfies the conditions of the conditional expectation as we have defined it.\ +lemma has_cond_exp_real: + fixes f :: "'a \ real" + assumes "integrable M f" + shows "has_cond_exp M F f (real_cond_exp M F f)" + by (intro has_cond_expI', auto intro!: real_cond_exp_intA assms) + +lemma cond_exp_real[intro]: + fixes f :: "'a \ real" + assumes "integrable M f" + shows "AE x in M. cond_exp M F f x = real_cond_exp M F f x" + using has_cond_exp_charact has_cond_exp_real assms by blast + +lemma cond_exp_cmult: + fixes f :: "'a \ real" + assumes "integrable M f" + shows "AE x in M. cond_exp M F (\x. c * f x) x = c * cond_exp M F f x" + using real_cond_exp_cmult[OF assms(1), of c] assms(1)[THEN cond_exp_real] assms(1)[THEN integrable_mult_right, THEN cond_exp_real, of c] by fastforce + +subsection \Existence\ + +text \Showing the existence is a bit involved. Specifically, what we aim to show is that \<^term>\has_cond_exp M F f (cond_exp M F f)\ holds for any Bochner-integrable \<^term>\f\. + We will employ the standard machinery of measure theory. First, we will prove existence for indicator functions. + Then we will extend our proof by linearity to simple functions. + Finally we use a limiting argument to show that the conditional expectation exists for all Bochner-integrable functions.\ + +text \Indicator functions\ + +lemma has_cond_exp_indicator: + assumes "A \ sets M" "emeasure M A < \" + shows "has_cond_exp M F (\x. indicat_real A x *\<^sub>R y) (\x. real_cond_exp M F (indicator A) x *\<^sub>R y)" +proof (intro has_cond_expI', goal_cases) + case (1 B) + have "\x\B. (indicat_real A x *\<^sub>R y) \M = (\x\B. indicat_real A x \M) *\<^sub>R y" using assms by (intro set_integral_scaleR_left, meson 1 in_mono subalg subalgebra_def, blast) + also have "... = (\x\B. real_cond_exp M F (indicator A) x \M) *\<^sub>R y" using 1 assms by (subst real_cond_exp_intA, auto) + also have "... = \x\B. (real_cond_exp M F (indicator A) x *\<^sub>R y) \M" using assms by (intro set_integral_scaleR_left[symmetric], meson 1 in_mono subalg subalgebra_def, blast) + finally show ?case . +next + case 2 + show ?case using integrable_scaleR_left integrable_real_indicator assms by blast +next + case 3 + show ?case using assms by (intro integrable_scaleR_left, intro real_cond_exp_int, blast+) +next + case 4 + show ?case by (intro borel_measurable_scaleR, intro Conditional_Expectation.borel_measurable_cond_exp, simp) +qed + +lemma cond_exp_indicator[intro]: + fixes y :: "'b::{second_countable_topology,banach}" + assumes [measurable]: "A \ sets M" "emeasure M A < \" + shows "AE x in M. cond_exp M F (\x. indicat_real A x *\<^sub>R y) x = cond_exp M F (indicator A) x *\<^sub>R y" +proof - + have "AE x in M. cond_exp M F (\x. indicat_real A x *\<^sub>R y) x = real_cond_exp M F (indicator A) x *\<^sub>R y" using has_cond_exp_indicator[OF assms] has_cond_exp_charact by blast + thus ?thesis using cond_exp_real[OF integrable_real_indicator, OF assms] by fastforce +qed + +text \Addition\ + +lemma has_cond_exp_add: + fixes f g :: "'a \ 'b::{second_countable_topology,banach}" + assumes "has_cond_exp M F f f'" "has_cond_exp M F g g'" + shows "has_cond_exp M F (\x. f x + g x) (\x. f' x + g' x)" +proof (intro has_cond_expI', goal_cases) + case (1 A) + have "\x\A. (f x + g x)\M = (\x\A. f x \M) + (\x\A. g x \M)" using assms[THEN has_cond_expD(2)] subalg 1 by (intro set_integral_add(2), auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator) + also have "... = (\x\A. f' x \M) + (\x\A. g' x \M)" using assms[THEN has_cond_expD(1)[OF _ 1]] by argo + also have "... = \x\A. (f' x + g' x)\M" using assms[THEN has_cond_expD(3)] subalg 1 by (intro set_integral_add(2)[symmetric], auto simp add: subalgebra_def set_integrable_def intro: integrable_mult_indicator) + finally show ?case . +next + case 2 + show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(2)) +next + case 3 + show ?case by (metis Bochner_Integration.integrable_add assms has_cond_expD(3)) +next + case 4 + show ?case using assms borel_measurable_add has_cond_expD(4) by blast +qed + +lemma has_cond_exp_scaleR_right: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "has_cond_exp M F f f'" + shows "has_cond_exp M F (\x. c *\<^sub>R f x) (\x. c *\<^sub>R f' x)" + using has_cond_expD[OF assms] by (intro has_cond_expI', auto) + +lemma cond_exp_scaleR_right: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" + shows "AE x in M. cond_exp M F (\x. c *\<^sub>R f x) x = c *\<^sub>R cond_exp M F f x" +proof (cases "\f'. has_cond_exp M F f f'") + case True + then show ?thesis using assms has_cond_exp_charact has_cond_exp_scaleR_right by metis +next + case False + show ?thesis + proof (cases "c = 0") + case True + then show ?thesis by simp + next + case c_nonzero: False + have "\f'. has_cond_exp M F (\x. c *\<^sub>R f x) f'" + proof (standard, goal_cases) + case 1 + then obtain f' where f': "has_cond_exp M F (\x. c *\<^sub>R f x) f'" by blast + have "has_cond_exp M F f (\x. inverse c *\<^sub>R f' x)" using has_cond_expD[OF f'] divideR_right[OF c_nonzero] assms by (intro has_cond_expI', auto) + then show ?case using False by blast + qed + then show ?thesis using cond_exp_null[OF False] cond_exp_null by force + qed +qed + +lemma cond_exp_uminus: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" + shows "AE x in M. cond_exp M F (\x. - f x) x = - cond_exp M F f x" + using cond_exp_scaleR_right[OF assms, of "-1"] by force + +text \Together with the induction scheme \integrable_simple_function_induct\, we can show that the conditional expectation of an integrable simple function exists.\ + +corollary has_cond_exp_simple: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" + shows "has_cond_exp M F f (cond_exp M F f)" + using assms +proof (induction rule: integrable_simple_function_induct) + case (cong f g) + then show ?case using has_cond_exp_cong by (metis (no_types, opaque_lifting) Bochner_Integration.integrable_cong has_cond_expD(2) has_cond_exp_charact(1)) +next + case (indicator A y) + then show ?case using has_cond_exp_charact[OF has_cond_exp_indicator] by fast +next + case (add u v) + then show ?case using has_cond_exp_add has_cond_exp_charact(1) by blast +qed + +text \Now comes the most difficult part. Given a convergent sequence of integrable simple functions \<^term>\\n. s n\, + we must show that the sequence \<^term>\\n. cond_exp M F (s n)\ is also convergent. Furthermore, we must show that this limit satisfies the properties of a conditional expectation. + Unfortunately, we will only be able to show that this sequence convergences in the L1-norm. + Luckily, this is enough to show that the operator \<^term>\cond_exp M F\ preserves limits as a function from L1 to L1.\ + +text \In anticipation of this result, we show that the conditional expectation operator is a contraction for simple functions. + We first reformulate the lemma \real_cond_exp_abs\, which shows the statement for real-valued functions, using our definitions. + Then we show the statement for simple functions via induction.\ + +lemma cond_exp_contraction_real: + fixes f :: "'a \ real" + assumes integrable[measurable]: "integrable M f" + shows "AE x in M. norm (cond_exp M F f x) \ cond_exp M F (\x. norm (f x)) x" +proof- + have int: "integrable M (\x. norm (f x))" using assms by blast + have *: "AE x in M. 0 \ cond_exp M F (\x. norm (f x)) x" using cond_exp_real[THEN AE_symmetric, OF integrable_norm[OF integrable]] real_cond_exp_ge_c[OF integrable_norm[OF integrable], of 0] norm_ge_zero by fastforce + have **: "A \ sets F \ \x\A. \f x\ \M = \x\A. real_cond_exp M F (\x. norm (f x)) x \M" for A unfolding real_norm_def using assms integrable_abs real_cond_exp_intA by blast + + have norm_int: "A \ sets F \ (\x\A. \f x\ \M) = (\\<^sup>+x\A. \f x\ \M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD) + + have "AE x in M. real_cond_exp M F (\x. norm (f x)) x \ 0" using int real_cond_exp_ge_c by force + hence cond_exp_norm_int: "A \ sets F \ (\x\A. real_cond_exp M F (\x. norm (f x)) x \M) = (\\<^sup>+x\A. real_cond_exp M F (\x. norm (f x)) x \M)" for A using assms by (intro nn_set_integral_eq_set_integral[symmetric], blast, fastforce) (meson subalg subalgebra_def subsetD) + + have "A \ sets F \ \\<^sup>+x\A. \f x\\M = \\<^sup>+x\A. real_cond_exp M F (\x. norm (f x)) x \M" for A using ** norm_int cond_exp_norm_int by (auto simp add: nn_integral_set_ennreal) + moreover have "(\x. ennreal \f x\) \ borel_measurable M" by measurable + moreover have "(\x. ennreal (real_cond_exp M F (\x. norm (f x)) x)) \ borel_measurable F" by measurable + ultimately have "AE x in M. nn_cond_exp M F (\x. ennreal \f x\) x = real_cond_exp M F (\x. norm (f x)) x" by (intro nn_cond_exp_charact[THEN AE_symmetric], auto) + hence "AE x in M. nn_cond_exp M F (\x. ennreal \f x\) x \ cond_exp M F (\x. norm (f x)) x" using cond_exp_real[OF int] by force + moreover have "AE x in M. \real_cond_exp M F f x\ = norm (cond_exp M F f x)" unfolding real_norm_def using cond_exp_real[OF assms] * by force + ultimately have "AE x in M. ennreal (norm (cond_exp M F f x)) \ cond_exp M F (\x. norm (f x)) x" using real_cond_exp_abs[OF assms[THEN borel_measurable_integrable]] by fastforce + hence "AE x in M. enn2real (ennreal (norm (cond_exp M F f x))) \ enn2real (cond_exp M F (\x. norm (f x)) x)" using ennreal_le_iff2 by force + thus ?thesis using * by fastforce +qed + +lemma cond_exp_contraction_simple: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" + shows "AE x in M. norm (cond_exp M F f x) \ cond_exp M F (\x. norm (f x)) x" + using assms +proof (induction rule: integrable_simple_function_induct) + case (cong f g) + hence ae: "AE x in M. f x = g x" by blast + hence "AE x in M. cond_exp M F f x = cond_exp M F g x" using cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto intro!: has_cond_expD(2)) + hence "AE x in M. norm (cond_exp M F f x) = norm (cond_exp M F g x)" by force + moreover have "AE x in M. cond_exp M F (\x. norm (f x)) x = cond_exp M F (\x. norm (g x)) x" using ae cong has_cond_exp_simple by (subst cond_exp_cong_AE) (auto dest: has_cond_expD) + ultimately show ?case using cong(6) by fastforce +next + case (indicator A y) + hence "AE x in M. cond_exp M F (\a. indicator A a *\<^sub>R y) x = cond_exp M F (indicator A) x *\<^sub>R y" by blast + hence *: "AE x in M. norm (cond_exp M F (\a. indicat_real A a *\<^sub>R y) x) \ norm y * cond_exp M F (\x. norm (indicat_real A x)) x" using cond_exp_contraction_real[OF integrable_real_indicator, OF indicator] by fastforce + + have "AE x in M. norm y * cond_exp M F (\x. norm (indicat_real A x)) x = norm y * real_cond_exp M F (\x. norm (indicat_real A x)) x" using cond_exp_real[OF integrable_real_indicator, OF indicator] by fastforce + moreover have "AE x in M. cond_exp M F (\x. norm y * norm (indicat_real A x)) x = real_cond_exp M F (\x. norm y * norm (indicat_real A x)) x" using indicator by (intro cond_exp_real, auto) + ultimately have "AE x in M. norm y * cond_exp M F (\x. norm (indicat_real A x)) x = cond_exp M F (\x. norm y * norm (indicat_real A x)) x" using real_cond_exp_cmult[of "\x. norm (indicat_real A x)" "norm y"] indicator by fastforce + moreover have "(\x. norm y * norm (indicat_real A x)) = (\x. norm (indicat_real A x *\<^sub>R y))" by force + ultimately show ?case using * by force +next + case (add u v) + have "AE x in M. norm (cond_exp M F (\a. u a + v a) x) = norm (cond_exp M F u x + cond_exp M F v x)" using has_cond_exp_charact(2)[OF has_cond_exp_add, OF has_cond_exp_simple(1,1), OF add(1,2,3,4)] by fastforce + moreover have "AE x in M. norm (cond_exp M F u x + cond_exp M F v x) \ norm (cond_exp M F u x) + norm (cond_exp M F v x)" using norm_triangle_ineq by blast + moreover have "AE x in M. norm (cond_exp M F u x) + norm (cond_exp M F v x) \ cond_exp M F (\x. norm (u x)) x + cond_exp M F (\x. norm (v x)) x" using add(6,7) by fastforce + moreover have "AE x in M. cond_exp M F (\x. norm (u x)) x + cond_exp M F (\x. norm (v x)) x = cond_exp M F (\x. norm (u x) + norm (v x)) x" using integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro has_cond_exp_charact(2)[OF has_cond_exp_add[OF has_cond_exp_charact(1,1)], THEN AE_symmetric], auto intro: has_cond_exp_real) + moreover have "AE x in M. cond_exp M F (\x. norm (u x) + norm (v x)) x = cond_exp M F (\x. norm (u x + v x)) x" using add(5) integrable_simple_function[OF add(1,2)] integrable_simple_function[OF add(3,4)] by (intro cond_exp_cong, auto) + ultimately show ?case by force +qed + +lemma has_cond_exp_simple_lim: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes integrable[measurable]: "integrable M f" + and "\i. simple_function M (s i)" + and "\i. emeasure M {y \ space M. s i y \ 0} \ \" + and "\x. x \ space M \ (\i. s i x) \ f x" + and "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" + obtains r + where "strict_mono r" "has_cond_exp M F f (\x. lim (\i. cond_exp M F (s (r i)) x))" + "AE x in M. convergent (\i. cond_exp M F (s (r i)) x)" +proof - + have [measurable]: "(s i) \ borel_measurable M" for i using assms(2) by (simp add: borel_measurable_simple_function) + have integrable_s: "integrable M (\x. s i x)" for i using assms integrable_simple_function by blast + have integrable_4f: "integrable M (\x. 4 * norm (f x))" using assms(1) by simp + have integrable_2f: "integrable M (\x. 2 * norm (f x))" using assms(1) by simp + have integrable_2_cond_exp_norm_f: "integrable M (\x. 2 * cond_exp M F (\x. norm (f x)) x)" by fast + + have "emeasure M {y \ space M. s i y - s j y \ 0} \ emeasure M {y \ space M. s i y \ 0} + emeasure M {y \ space M. s j y \ 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto) + hence fin_sup: "emeasure M {y \ space M. s i y - s j y \ 0} \ \" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def) + + have "emeasure M {y \ space M. norm (s i y - s j y) \ 0} \ emeasure M {y \ space M. s i y \ 0} + emeasure M {y \ space M. s j y \ 0}" for i j using simple_functionD(2)[OF assms(2)] by (intro order_trans[OF emeasure_mono emeasure_subadditive], auto) + hence fin_sup_norm: "emeasure M {y \ space M. norm (s i y - s j y) \ 0} \ \" for i j using assms(3) by (metis (mono_tags) ennreal_add_eq_top linorder_not_less top.not_eq_extremum infinity_ennreal_def) + + have Cauchy: "Cauchy (\n. s n x)" if "x \ space M" for x using assms(4) LIMSEQ_imp_Cauchy that by blast + hence bounded_range_s: "bounded (range (\n. s n x))" if "x \ space M" for x using that cauchy_imp_bounded by fast + + text \Since the sequence \<^term>\(\n. s n x)\ is Cauchy for almost all \<^term>\x\, we know that the diameter tends to zero almost everywhere.\ + text \Dominated convergence tells us that the integral of the diameter also converges to zero.\ + have "AE x in M. (\n. diameter {s i x | i. n \ i}) \ 0" using Cauchy cauchy_iff_diameter_tends_to_zero_and_bounded by fast + moreover have "(\x. diameter {s i x |i. n \ i}) \ borel_measurable M" for n using bounded_range_s borel_measurable_diameter by measurable + moreover have "AE x in M. norm (diameter {s i x |i. n \ i}) \ 4 * norm (f x)" for n + proof - + { + fix x assume x: "x \ space M" + have "diameter {s i x |i. n \ i} \ 2 * norm (f x) + 2 * norm (f x)" by (intro diameter_le, blast, subst dist_norm[symmetric], intro dist_triangle3[THEN order_trans, of 0], intro add_mono) (auto intro: assms(5)[OF x]) + hence "norm (diameter {s i x |i. n \ i}) \ 4 * norm (f x)" using diameter_ge_0[OF bounded_subset[OF bounded_range_s], OF x, of "{s i x |i. n \ i}"] by force + } + thus ?thesis by fast + qed + ultimately have diameter_tendsto_zero: "(\n. LINT x|M. diameter {s i x | i. n \ i}) \ 0" by (intro integral_dominated_convergence[OF borel_measurable_const[of 0] _ integrable_4f, simplified]) (fast+) + + have diameter_integrable: "integrable M (\x. diameter {s i x | i. n \ i})" for n using assms(1,5) + by (intro integrable_bound_diameter[OF bounded_range_s integrable_2f], auto) + + have dist_integrable: "integrable M (\x. dist (s i x) (s j x))" for i j using assms(5) dist_triangle3[of "s i _" _ 0, THEN order_trans, OF add_mono, of _ "2 * norm (f _)"] + by (intro Bochner_Integration.integrable_bound[OF integrable_4f]) fastforce+ + + text \Since \<^term>\cond_exp M F\ is a contraction for simple functions, the following sequence of integral values is also Cauchy.\ + text \This follows, since the distance between the terms of this sequence are always less than or equal to the diameter, which itself converges to zero.\ + text \Hence, we obtain a subsequence which is Cauchy almost everywhere.\ + have "\N. \i\N. \j\N. LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) < e" if e_pos: "e > 0" for e + proof - + obtain N where *: "LINT x|M. diameter {s i x | i. n \ i} < e" if "n \ N" for n using that order_tendsto_iff[THEN iffD1, OF diameter_tendsto_zero, unfolded eventually_sequentially] e_pos by presburger + { + fix i j x assume asm: "i \ N" "j \ N" "x \ space M" + have "case_prod dist ` ({s i x |i. N \ i} \ {s i x |i. N \ i}) = case_prod (\i j. dist (s i x) (s j x)) ` ({N..} \ {N..})" by fast + hence "diameter {s i x | i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x))" unfolding diameter_def by auto + moreover have "(SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x)) \ dist (s i x) (s j x)" using asm bounded_imp_bdd_above[OF bounded_imp_dist_bounded, OF bounded_range_s] by (intro cSup_upper, auto) + ultimately have "diameter {s i x | i. N \ i} \ dist (s i x) (s j x)" by presburger + } + hence "LINT x|M. dist (s i x) (s j x) < e" if "i \ N" "j \ N" for i j using that * by (intro integral_mono[OF dist_integrable diameter_integrable, THEN order.strict_trans1], blast+) + moreover have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) \ LINT x|M. dist (s i x) (s j x)" for i j + proof - + have "LINT x|M. norm (cond_exp M F (s i) x - cond_exp M F (s j) x) = LINT x|M. norm (cond_exp M F (s i) x + - 1 *\<^sub>R cond_exp M F (s j) x)" unfolding dist_norm by simp + also have "... = LINT x|M. norm (cond_exp M F (\x. s i x - s j x) x)" using has_cond_exp_charact(2)[OF has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_exp_charact(1,1), OF has_cond_exp_simple(1,1)[OF assms(2,3)]], THEN AE_symmetric, of i "-1" j] by (intro integral_cong_AE) force+ + also have "... \ LINT x|M. cond_exp M F (\x. norm (s i x - s j x)) x" using cond_exp_contraction_simple[OF _ fin_sup, of i j] integrable_cond_exp assms(2) by (intro integral_mono_AE, fast+) + also have "... = LINT x|M. norm (s i x - s j x)" unfolding set_integral_space(1)[OF integrable_cond_exp, symmetric] set_integral_space[OF dist_integrable[unfolded dist_norm], symmetric] by (intro has_cond_expD(1)[OF has_cond_exp_simple[OF _ fin_sup_norm], symmetric]) (metis assms(2) simple_function_compose1 simple_function_diff, metis sets.top subalg subalgebra_def) + finally show ?thesis unfolding dist_norm . + qed + ultimately show ?thesis using order.strict_trans1 by meson + qed + then obtain r where strict_mono_r: "strict_mono r" and AE_Cauchy: "AE x in M. Cauchy (\i. cond_exp M F (s (r i)) x)" + by (rule cauchy_L1_AE_cauchy_subseq[OF integrable_cond_exp], auto) + hence ae_lim_cond_exp: "AE x in M. (\n. cond_exp M F (s (r n)) x) \ lim (\n. cond_exp M F (s (r n)) x)" using Cauchy_convergent_iff convergent_LIMSEQ_iff by fastforce + + text \Now that we have a candidate for the conditional expectation, we must show that it actually has the required properties.\ + + text \Dominated convergence shows that this limit is indeed integrable.\ + text \Here, we again use the fact that conditional expectation is a contraction on simple functions.\ + have cond_exp_bounded: "AE x in M. norm (cond_exp M F (s (r n)) x) \ cond_exp M F (\x. 2 * norm (f x)) x" for n + proof - + have "AE x in M. norm (cond_exp M F (s (r n)) x) \ cond_exp M F (\x. norm (s (r n) x)) x" by (rule cond_exp_contraction_simple[OF assms(2,3)]) + moreover have "AE x in M. real_cond_exp M F (\x. norm (s (r n) x)) x \ real_cond_exp M F (\x. 2 * norm (f x)) x" using integrable_s integrable_2f assms(5) by (intro real_cond_exp_mono, auto) + ultimately show ?thesis using cond_exp_real[OF integrable_norm, OF integrable_s, of "r n"] cond_exp_real[OF integrable_2f] by force + qed + have lim_integrable: "integrable M (\x. lim (\i. cond_exp M F (s (r i)) x))" by (intro integrable_dominated_convergence[OF _ borel_measurable_cond_exp' integrable_cond_exp ae_lim_cond_exp cond_exp_bounded], simp) + + text \Moreover, we can use the DCT twice to show that the conditional expectation property holds, i.e. the value of the integral of the candidate, agrees with \<^term>\f\ on sets \<^term>\A \ F\.\ + { + fix A assume A_in_sets_F: "A \ sets F" + have "AE x in M. norm (indicator A x *\<^sub>R cond_exp M F (s (r n)) x) \ cond_exp M F (\x. 2 * norm (f x)) x" for n + proof - + have "AE x in M. norm (indicator A x *\<^sub>R cond_exp M F (s (r n)) x) \ norm (cond_exp M F (s (r n)) x)" unfolding indicator_def by simp + thus ?thesis using cond_exp_bounded[of n] by force + qed + hence lim_cond_exp_int: "(\n. LINT x:A|M. cond_exp M F (s (r n)) x) \ LINT x:A|M. lim (\n. cond_exp M F (s (r n)) x)" + using ae_lim_cond_exp measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] cond_exp_bounded + unfolding set_lebesgue_integral_def + by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_cond_exp]) (fastforce simp add: tendsto_scaleR)+ + + have "AE x in M. norm (indicator A x *\<^sub>R s (r n) x) \ 2 * norm (f x)" for n + proof - + have "AE x in M. norm (indicator A x *\<^sub>R s (r n) x) \ norm (s (r n) x)" unfolding indicator_def by simp + thus ?thesis using assms(5)[of _ "r n"] by fastforce + qed + hence lim_s_int: "(\n. LINT x:A|M. s (r n) x) \ LINT x:A|M. f x" + using measurable_from_subalg[OF subalg borel_measurable_indicator, OF A_in_sets_F] LIMSEQ_subseq_LIMSEQ[OF assms(4) strict_mono_r] assms(5) + unfolding set_lebesgue_integral_def comp_def + by (intro integral_dominated_convergence[OF borel_measurable_scaleR borel_measurable_scaleR integrable_2f]) (fastforce simp add: tendsto_scaleR)+ + + have "LINT x:A|M. lim (\n. cond_exp M F (s (r n)) x) = lim (\n. LINT x:A|M. cond_exp M F (s (r n)) x)" using limI[OF lim_cond_exp_int] by argo + also have "... = lim (\n. LINT x:A|M. s (r n) x)" using has_cond_expD(1)[OF has_cond_exp_simple[OF assms(2,3)] A_in_sets_F, symmetric] by presburger + also have "... = LINT x:A|M. f x" using limI[OF lim_s_int] by argo + finally have "LINT x:A|M. lim (\n. cond_exp M F (s (r n)) x) = LINT x:A|M. f x" . + } + text \Putting it all together, we have the statement we are looking for.\ + hence "has_cond_exp M F f (\x. lim (\i. cond_exp M F (s (r i)) x))" using assms(1) lim_integrable by (intro has_cond_expI', auto) + thus thesis using AE_Cauchy Cauchy_convergent strict_mono_r by (auto intro!: that) +qed + +text \Now, we can show that the conditional expectation is well-defined for all integrable functions.\ +corollary has_cond_expI: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" + shows "has_cond_exp M F f (cond_exp M F f)" +proof - + obtain s where s_is: "\i. simple_function M (s i)" "\i. emeasure M {y \ space M. s i y \ 0} \ \" "\x. x \ space M \ (\i. s i x) \ f x" "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" using integrable_implies_simple_function_sequence[OF assms] by blast + show ?thesis using has_cond_exp_simple_lim[OF assms s_is] has_cond_exp_charact(1) by metis +qed + +subsection \Properties\ + +text \The defining property of the conditional expectation now always holds, given that the function \<^term>\f\ is integrable.\ + +lemma cond_exp_set_integral: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" "A \ sets F" + shows "(\ x \ A. f x \M) = (\ x \ A. cond_exp M F f x \M)" + using has_cond_expD(1)[OF has_cond_expI, OF assms] by argo + +(* Tower Property *) + +text \The following property of the conditional expectation is called the "Tower Property".\ + +lemma cond_exp_nested_subalg: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" "subalgebra M G" "subalgebra G F" + shows "AE \ in M. cond_exp M F f \ = cond_exp M F (cond_exp M G f) \" + using has_cond_expI assms sigma_finite_subalgebra_def by (auto intro!: has_cond_exp_nested_subalg[THEN has_cond_exp_charact(2), THEN AE_symmetric] sigma_finite_subalgebra.has_cond_expI[OF sigma_finite_subalgebra.intro[OF assms(2)]] nested_subalg_is_sigma_finite) + +(* Linearity *) + +text \The conditional expectation is linear.\ + +lemma cond_exp_add: + fixes f :: "'a \ 'b::{second_countable_topology,banach}" + assumes "integrable M f" "integrable M g" + shows "AE x in M. cond_exp M F (\x. f x + g x) x = cond_exp M F f x + cond_exp M F g x" + using has_cond_exp_add[OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2)] . + +lemma cond_exp_diff: + fixes f :: "'a \ 'b :: {second_countable_topology, banach}" + assumes "integrable M f" "integrable M g" + shows "AE x in M. cond_exp M F (\x. f x - g x) x = cond_exp M F f x - cond_exp M F g x" + using has_cond_exp_add[OF _ has_cond_exp_scaleR_right, OF has_cond_expI(1,1), OF assms, THEN has_cond_exp_charact(2), of "-1"] by simp + +lemma cond_exp_diff': + fixes f :: "'a \ 'b :: {second_countable_topology, banach}" + assumes "integrable M f" "integrable M g" + shows "AE x in M. cond_exp M F (f - g) x = cond_exp M F f x - cond_exp M F g x" + unfolding fun_diff_def using assms by (rule cond_exp_diff) + +lemma cond_exp_scaleR_left: + fixes f :: "'a \ real" + assumes "integrable M f" + shows "AE x in M. cond_exp M F (\x. f x *\<^sub>R c) x = cond_exp M F f x *\<^sub>R c" + using cond_exp_set_integral[OF assms] subalg assms unfolding subalgebra_def + by (intro cond_exp_charact, + subst set_integral_scaleR_left, blast, intro assms, + subst set_integral_scaleR_left, blast, intro integrable_cond_exp) + auto + +text \The conditional expectation operator is a contraction, i.e. a bounded linear operator with operator norm less than or equal to 1.\ +text \To show this we first obtain a subsequence \<^term>\\x. (\i. s (r i) x)\, such that \<^term>\(\i. cond_exp M F (s (r i)) x)\ converges to \<^term>\cond_exp M F f x\ a.e. + Afterwards, we obtain a sub-subsequence \<^term>\\x. (\i. s (r (r' i)) x)\, such that \<^term>\(\i. cond_exp M F (\x. norm (s (r i))) x)\ converges to \<^term>\cond_exp M F (\x. norm (f x)) x\ a.e. + Finally, we show that the inequality holds by showing that the terms of the subsequences obey the inequality and the fact that a subsequence of a convergent sequence converges to the same limit.\ + +lemma cond_exp_contraction: + fixes f :: "'a \ 'b::{second_countable_topology, banach}" + assumes "integrable M f" + shows "AE x in M. norm (cond_exp M F f x) \ cond_exp M F (\x. norm (f x)) x" +proof - + obtain s where s: "\i. simple_function M (s i)" "\i. emeasure M {y \ space M. s i y \ 0} \ \" "\x. x \ space M \ (\i. s i x) \ f x" "\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)" + by (blast intro: integrable_implies_simple_function_sequence[OF assms]) + + obtain r where r: "strict_mono r" and "has_cond_exp M F f (\x. lim (\i. cond_exp M F (s (r i)) x))" "AE x in M. (\i. cond_exp M F (s (r i)) x) \ lim (\i. cond_exp M F (s (r i)) x)" + using has_cond_exp_simple_lim[OF assms s] unfolding convergent_LIMSEQ_iff by blast + hence r_tendsto: "AE x in M. (\i. cond_exp M F (s (r i)) x) \ cond_exp M F f x" using has_cond_exp_charact(2) by force + + have norm_s_r: "\i. simple_function M (\x. norm (s (r i) x))" "\i. emeasure M {y \ space M. norm (s (r i) y) \ 0} \ \" "\x. x \ space M \ (\i. norm (s (r i) x)) \ norm (f x)" "\i x. x \ space M \ norm (norm (s (r i) x)) \ 2 * norm (norm (f x))" + using s by (auto intro: LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r, unfolded comp_def] simple_function_compose1) + + obtain r' where r': "strict_mono r'" and "has_cond_exp M F (\x. norm (f x)) (\x. lim (\i. cond_exp M F (\x. norm (s (r (r' i)) x)) x))" "AE x in M. (\i. cond_exp M F (\x. norm (s (r (r' i)) x)) x) \ lim (\i. cond_exp M F (\x. norm (s (r (r' i)) x)) x)" using has_cond_exp_simple_lim[OF integrable_norm norm_s_r, OF assms] unfolding convergent_LIMSEQ_iff by blast + hence r'_tendsto: "AE x in M. (\i. cond_exp M F (\x. norm (s (r (r' i)) x)) x) \ cond_exp M F (\x. norm (f x)) x" using has_cond_exp_charact(2) by force + + have "AE x in M. \i. norm (cond_exp M F (s (r (r' i))) x) \ cond_exp M F (\x. norm (s (r (r' i)) x)) x" using s by (auto intro: cond_exp_contraction_simple simp add: AE_all_countable) + moreover have "AE x in M. (\i. norm (cond_exp M F (s (r (r' i))) x)) \ norm (cond_exp M F f x)" using r_tendsto LIMSEQ_subseq_LIMSEQ[OF tendsto_norm r', unfolded comp_def] by fast + ultimately show ?thesis using LIMSEQ_le r'_tendsto by fast +qed + +text \The following lemmas are called "pulling out whats known". We first show the statement for real-valued functions using the lemma \real_cond_exp_intg\, which is already present. + We then show it for arbitrary \<^term>\g\ using the lecture notes of Gordan Zitkovic for the course "Theory of Probability I" \cite{Zitkovic_2015}.\ + +lemma cond_exp_measurable_mult: + fixes f g :: "'a \ real" + assumes [measurable]: "integrable M (\x. f x * g x)" "integrable M g" "f \ borel_measurable F" + shows "integrable M (\x. f x * cond_exp M F g x)" + "AE x in M. cond_exp M F (\x. f x * g x) x = f x * cond_exp M F g x" +proof- + show integrable: "integrable M (\x. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] by (intro integrable_cong_AE_imp[OF real_cond_exp_intg(1), OF assms(1,3) assms(2)[THEN borel_measurable_integrable]] measurable_from_subalg[OF subalg]) auto + interpret sigma_finite_measure "restr_to_subalg M F" by (rule sigma_fin_subalg) + { + fix A assume asm: "A \ sets F" + hence asm': "A \ sets M" using subalg by (fastforce simp add: subalgebra_def) + have "set_lebesgue_integral M A (cond_exp M F (\x. f x * g x)) = set_lebesgue_integral M A (\x. f x * g x)" by (simp add: cond_exp_set_integral[OF assms(1) asm]) + also have "... = set_lebesgue_integral M A (\x. f x * real_cond_exp M F g x)" using borel_measurable_times[OF borel_measurable_indicator[OF asm] assms(3)] borel_measurable_integrable[OF assms(2)] integrable_mult_indicator[OF asm' assms(1)] by (fastforce simp add: set_lebesgue_integral_def mult.assoc[symmetric] intro: real_cond_exp_intg(2)[symmetric]) + also have "... = set_lebesgue_integral M A (\x. f x * cond_exp M F g x)" using cond_exp_real[OF assms(2)] asm' borel_measurable_cond_exp' borel_measurable_cond_exp2 measurable_from_subalg[OF subalg assms(3)] by (auto simp add: set_lebesgue_integral_def intro: integral_cong_AE) + finally have "set_lebesgue_integral M A (cond_exp M F (\x. f x * g x)) = \x\A. (f x * cond_exp M F g x)\M" . + } + hence "AE x in restr_to_subalg M F. cond_exp M F (\x. f x * g x) x = f x * cond_exp M F g x" by (intro density_unique_banach integrable_cond_exp integrable integrable_in_subalg subalg, measurable, simp add: set_lebesgue_integral_def integral_subalgebra2[OF subalg] sets_restr_to_subalg[OF subalg]) + thus "AE x in M. cond_exp M F (\x. f x * g x) x = f x * cond_exp M F g x" by (rule AE_restr_to_subalg[OF subalg]) +qed + +lemma cond_exp_measurable_scaleR: + fixes f :: "'a \ real" and g :: "'a \ 'b :: {second_countable_topology, banach}" + assumes [measurable]: "integrable M (\x. f x *\<^sub>R g x)" "integrable M g" "f \ borel_measurable F" + shows "integrable M (\x. f x *\<^sub>R cond_exp M F g x)" + "AE x in M. cond_exp M F (\x. f x *\<^sub>R g x) x = f x *\<^sub>R cond_exp M F g x" +proof - + let ?F = "restr_to_subalg M F" + have subalg': "subalgebra M (restr_to_subalg M F)" by (metis sets_eq_imp_space_eq sets_restr_to_subalg subalg subalgebra_def) + { + fix z assume asm[measurable]: "integrable M (\x. z x *\<^sub>R g x)" "z \ borel_measurable ?F" + hence asm'[measurable]: "z \ borel_measurable F" using measurable_in_subalg' subalg by blast + have "integrable M (\x. z x *\<^sub>R cond_exp M F g x)" "LINT x|M. z x *\<^sub>R g x = LINT x|M. z x *\<^sub>R cond_exp M F g x" + proof - + obtain s where s_is: "\i. simple_function ?F (s i)" "\x. x \ space ?F \ (\i. s i x) \ z x" "\i x. x \ space ?F \ norm (s i x) \ 2 * norm (z x)" using borel_measurable_implies_sequence_metric[OF asm(2), of 0] by force + + text \We need to apply the dominated convergence theorem twice, therefore we need to show the following prerequisites.\ + + have s_scaleR_g_tendsto: "AE x in M. (\i. s i x *\<^sub>R g x) \ z x *\<^sub>R g x" using s_is(2) by (simp add: space_restr_to_subalg tendsto_scaleR) + have s_scaleR_cond_exp_g_tendsto: "AE x in ?F. (\i. s i x *\<^sub>R cond_exp M F g x) \ z x *\<^sub>R cond_exp M F g x" using s_is(2) by (simp add: tendsto_scaleR) + + have s_scaleR_g_meas: "(\x. s i x *\<^sub>R g x) \ borel_measurable M" for i using s_is(1)[THEN borel_measurable_simple_function, THEN subalg'[THEN measurable_from_subalg]] by simp + have s_scaleR_cond_exp_g_meas: "(\x. s i x *\<^sub>R cond_exp M F g x) \ borel_measurable ?F" for i using s_is(1)[THEN borel_measurable_simple_function] measurable_in_subalg[OF subalg borel_measurable_cond_exp] by (fastforce intro: borel_measurable_scaleR) + + have s_scaleR_g_AE_bdd: "AE x in M. norm (s i x *\<^sub>R g x) \ 2 * norm (z x *\<^sub>R g x)" for i using s_is(3) by (fastforce simp add: space_restr_to_subalg mult.assoc[symmetric] mult_right_mono) + { + fix i + have asm: "integrable M (\x. norm (z x) * norm (g x))" using asm(1)[THEN integrable_norm] by simp + have "AE x in ?F. norm (s i x *\<^sub>R cond_exp M F g x) \ 2 * norm (z x) * norm (cond_exp M F g x)" using s_is(3) by (fastforce simp add: mult_mono) + moreover have "AE x in ?F. norm (z x) * cond_exp M F (\x. norm (g x)) x = cond_exp M F (\x. norm (z x) * norm (g x)) x" by (rule cond_exp_measurable_mult(2)[THEN AE_symmetric, OF asm integrable_norm, OF assms(2), THEN AE_restr_to_subalg2[OF subalg]], auto) + ultimately have "AE x in ?F. norm (s i x *\<^sub>R cond_exp M F g x) \ 2 * cond_exp M F (\x. norm (z x *\<^sub>R g x)) x" using cond_exp_contraction[OF assms(2), THEN AE_restr_to_subalg2[OF subalg]] order_trans[OF _ mult_mono] by fastforce + } + note s_scaleR_cond_exp_g_AE_bdd = this + + text \In the following section we need to pay attention to which measures we are using for integration. The rhs is F-measurable while the lhs is only M-measurable.\ + + { + fix i + have s_meas_M[measurable]: "s i \ borel_measurable M" by (meson borel_measurable_simple_function measurable_from_subalg s_is(1) subalg') + have s_meas_F[measurable]: "s i \ borel_measurable F" by (meson borel_measurable_simple_function measurable_in_subalg' s_is(1) subalg) + + have s_scaleR_eq: "s i x *\<^sub>R h x = (\y\s i ` space M. (indicator (s i -` {y} \ space M) x *\<^sub>R y) *\<^sub>R h x)" if "x \ space M" for x and h :: "'a \ 'b" using simple_function_indicator_representation[OF s_is(1), of x i] that unfolding space_restr_to_subalg scaleR_left.sum[of _ _ "h x", symmetric] by presburger + + have "LINT x|M. s i x *\<^sub>R g x = LINT x|M. (\y\s i ` space M. indicator (s i -` {y} \ space M) x *\<^sub>R y *\<^sub>R g x)" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto + also have "... = (\y\s i ` space M. LINT x|M. indicator (s i -` {y} \ space M) x *\<^sub>R y *\<^sub>R g x)" by (intro Bochner_Integration.integral_sum integrable_mult_indicator[OF _ integrable_scaleR_right] assms(2)) simp + also have "... = (\y\s i ` space M. y *\<^sub>R set_lebesgue_integral M (s i -` {y} \ space M) g)" by (simp only: set_lebesgue_integral_def[symmetric]) simp + also have "... = (\y\s i ` space M. y *\<^sub>R set_lebesgue_integral M (s i -` {y} \ space M) (cond_exp M F g))" using assms(2) subalg borel_measurable_vimage[OF s_meas_F] by (subst cond_exp_set_integral, auto simp add: subalgebra_def) + also have "... = (\y\s i ` space M. LINT x|M. indicator (s i -` {y} \ space M) x *\<^sub>R y *\<^sub>R cond_exp M F g x)" by (simp only: set_lebesgue_integral_def[symmetric]) simp + also have "... = LINT x|M. (\y\s i ` space M. indicator (s i -` {y} \ space M) x *\<^sub>R y *\<^sub>R cond_exp M F g x)" by (intro Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator[OF _ integrable_scaleR_right]) auto + also have "... = LINT x|M. s i x *\<^sub>R cond_exp M F g x" using s_scaleR_eq by (intro Bochner_Integration.integral_cong) auto + finally have "LINT x|M. s i x *\<^sub>R g x = LINT x|?F. s i x *\<^sub>R cond_exp M F g x" by (simp add: integral_subalgebra2[OF subalg]) + } + note integral_s_eq = this + + text \Now we just plug in the results we obtained into DCT, and use the fact that limits are unique.\ + + show "integrable M (\x. z x *\<^sub>R cond_exp M F g x)" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integrable_from_subalg[OF subalg] integrable_cond_exp integrable_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg) + + have "(\i. LINT x|M. s i x *\<^sub>R g x) \ LINT x|M. z x *\<^sub>R g x" using s_scaleR_g_meas asm(1)[THEN integrable_norm] asm' borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_g_tendsto s_scaleR_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg]) + moreover have "(\i. LINT x|?F. s i x *\<^sub>R cond_exp M F g x) \ LINT x|?F. z x *\<^sub>R cond_exp M F g x" using s_scaleR_cond_exp_g_meas asm(2) borel_measurable_cond_exp' by (intro integral_dominated_convergence[OF _ _ _ s_scaleR_cond_exp_g_tendsto s_scaleR_cond_exp_g_AE_bdd]) (auto intro: measurable_from_subalg[OF subalg] integrable_in_subalg measurable_in_subalg subalg) + ultimately show "LINT x|M. z x *\<^sub>R g x = LINT x|M. z x *\<^sub>R cond_exp M F g x" using integral_s_eq using subalg by (simp add: LIMSEQ_unique integral_subalgebra2) + qed + } + note * = this + + text \The main statement now follows with \<^term>\z = (\x. indicator A x * f x)\.\ + show "integrable M (\x. f x *\<^sub>R cond_exp M F g x)" using * assms measurable_in_subalg[OF subalg] by blast + + { + fix A assume asm: "A \ F" + hence "integrable M (\x. indicat_real A x *\<^sub>R f x *\<^sub>R g x)" using subalg by (fastforce simp add: subalgebra_def intro!: integrable_mult_indicator assms(1)) + hence "set_lebesgue_integral M A (\x. f x *\<^sub>R g x) = set_lebesgue_integral M A (\x. f x *\<^sub>R cond_exp M F g x)" unfolding set_lebesgue_integral_def using asm by (auto intro!: * measurable_in_subalg[OF subalg]) + } + thus "AE x in M. cond_exp M F (\x. f x *\<^sub>R g x) x = f x *\<^sub>R cond_exp M F g x" using borel_measurable_cond_exp by (intro cond_exp_charact, auto intro!: * assms measurable_in_subalg[OF subalg]) +qed + +lemma cond_exp_sum [intro, simp]: + fixes f :: "'t \ 'a \ 'b :: {second_countable_topology,banach}" + assumes [measurable]: "\i. integrable M (f i)" + shows "AE x in M. cond_exp M F (\x. \i\I. f i x) x = (\i\I. cond_exp M F (f i) x)" +proof (rule has_cond_exp_charact, intro has_cond_expI') + fix A assume [measurable]: "A \ sets F" + then have A_meas [measurable]: "A \ sets M" by (meson subsetD subalg subalgebra_def) + + have "(\x\A. (\i\I. f i x)\M) = (\x. (\i\I. indicator A x *\<^sub>R f i x)\M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right) + also have "... = (\i\I. (\x. indicator A x *\<^sub>R f i x \M))" using assms by (auto intro!: Bochner_Integration.integral_sum integrable_mult_indicator) + also have "... = (\i\I. (\x. indicator A x *\<^sub>R cond_exp M F (f i) x \M))" using cond_exp_set_integral[OF assms] by (simp add: set_lebesgue_integral_def) + also have "... = (\x. (\i\I. indicator A x *\<^sub>R cond_exp M F (f i) x)\M)" using assms by (auto intro!: Bochner_Integration.integral_sum[symmetric] integrable_mult_indicator) + also have "... = (\x\A. (\i\I. cond_exp M F (f i) x)\M)" unfolding set_lebesgue_integral_def by (simp add: scaleR_sum_right) + finally show "(\x\A. (\i\I. f i x)\M) = (\x\A. (\i\I. cond_exp M F (f i) x)\M)" by auto +qed (auto simp add: assms integrable_cond_exp) + +subsection \Linearly Ordered Banach Spaces\ + +text \In this subsection we show monotonicity results concerning the conditional expectation operator.\ + +lemma cond_exp_gr_c: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "AE x in M. f x > c" + shows "AE x in M. cond_exp M F f x > c" +proof - + define X where "X = {x \ space M. cond_exp M F f x \ c}" + have [measurable]: "X \ sets F" unfolding X_def by measurable (metis sets.top subalg subalgebra_def) + hence X_in_M: "X \ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast + have "emeasure M X = 0" + proof (rule ccontr) + assume "emeasure M X \ 0" + have "emeasure (restr_to_subalg M F) X = emeasure M X" by (simp add: emeasure_restr_to_subalg subalg) + hence "emeasure (restr_to_subalg M F) X > 0" using \\(emeasure M X) = 0\ gr_zeroI by auto + then obtain A where A: "A \ sets (restr_to_subalg M F)" "A \ X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < \" + 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) + hence [simp]: "A \ sets F" using subalg sets_restr_to_subalg by blast + hence A_in_sets_M[simp]: "A \ sets M" using sets_restr_to_subalg subalg subalgebra_def by blast + have [simp]: "set_integrable M A (\x. c)" using A subalg by (auto simp add: set_integrable_def emeasure_restr_to_subalg) + have [simp]: "set_integrable M A f" unfolding set_integrable_def by (rule integrable_mult_indicator, auto simp add: assms(1)) + have "AE x in M. indicator A x *\<^sub>R c = indicator A x *\<^sub>R f x" + proof (rule integral_eq_mono_AE_eq_AE) + have "(\x\A. c \M) \ (\x\A. f x \M)" using assms(2) by (intro set_integral_mono_AE_banach) auto + moreover + { + have "(\x\A. f x \M) = (\x\A. cond_exp M F f x \M)" by (rule cond_exp_set_integral, auto simp add: assms) + also have "... \ (\x\A. c \M)" using A by (auto intro!: set_integral_mono_banach simp add: X_def) + finally have "(\x\A. f x \M) \ (\x\A. c \M)" by simp + } + ultimately show "LINT x|M. indicator A x *\<^sub>R c = LINT x|M. indicator A x *\<^sub>R f x" unfolding set_lebesgue_integral_def by simp + show "AE x in M. indicator A x *\<^sub>R c \ indicator A x *\<^sub>R f x" using assms by (auto simp add: X_def indicator_def) + qed (auto simp add: set_integrable_def[symmetric]) + hence "AE x\A in M. c = f x" by auto + hence "AE x\A in M. False" using assms(2) by auto + hence "A \ null_sets M" using AE_iff_null_sets A_in_sets_M by metis + thus False using A(3) by (simp add: emeasure_restr_to_subalg null_setsD1 subalg) + qed + thus ?thesis using AE_iff_null_sets[OF X_in_M] unfolding X_def by auto +qed + +corollary cond_exp_less_c: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "AE x in M. f x < c" + shows "AE x in M. cond_exp M F f x < c" +proof - + have "AE x in M. cond_exp M F f x = - cond_exp M F (\x. - f x) x" using cond_exp_uminus[OF assms(1)] by auto + moreover have "AE x in M. cond_exp M F (\x. - f x) x > - c" using assms by (intro cond_exp_gr_c) auto + ultimately show ?thesis by (force simp add: minus_less_iff) +qed + +lemma cond_exp_mono_strict: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" "AE x in M. f x < g x" + shows "AE x in M. cond_exp M F f x < cond_exp M F g x" + using cond_exp_less_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0] + cond_exp_diff[OF assms(1,2)] assms(3) by auto + +lemma cond_exp_ge_c: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes [measurable]: "integrable M f" + and "AE x in M. f x \ c" + shows "AE x in M. cond_exp M F f x \ c" +proof - + let ?F = "restr_to_subalg M F" + interpret sigma_finite_measure "restr_to_subalg M F" using sigma_fin_subalg by auto + { + fix A assume asm: "A \ sets ?F" "0 < measure ?F A" + have [simp]: "sets ?F = sets F" "measure ?F A = measure M A" using asm by (auto simp add: measure_def sets_restr_to_subalg[OF subalg] emeasure_restr_to_subalg[OF subalg]) + have M_A: "emeasure M A < \" using measure_zero_top asm by (force simp add: top.not_eq_extremum) + hence F_A: "emeasure ?F A < \" using asm(1) emeasure_restr_to_subalg subalg by fastforce + have "set_lebesgue_integral M A (\_. c) \ set_lebesgue_integral M A f" using assms asm M_A subalg by (intro set_integral_mono_AE_banach, auto simp add: set_integrable_def integrable_mult_indicator subalgebra_def sets_restr_to_subalg) + also have "... = set_lebesgue_integral M A (cond_exp M F f)" using cond_exp_set_integral[OF assms(1)] asm by auto + also have "... = set_lebesgue_integral ?F A (cond_exp M F f)" unfolding set_lebesgue_integral_def using asm borel_measurable_cond_exp by (intro integral_subalgebra2[OF subalg, symmetric], simp) + finally have "(1 / measure ?F A) *\<^sub>R set_lebesgue_integral ?F A (cond_exp M F f) \ {c..}" using asm subalg M_A by (auto simp add: set_integral_const subalgebra_def intro!: pos_divideR_le_eq[THEN iffD1]) + } + thus ?thesis using AE_restr_to_subalg[OF subalg] averaging_theorem[OF integrable_in_subalg closed_atLeast, OF subalg borel_measurable_cond_exp integrable_cond_exp] by auto +qed + +corollary cond_exp_le_c: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" + and "AE x in M. f x \ c" + shows "AE x in M. cond_exp M F f x \ c" +proof - + have "AE x in M. cond_exp M F f x = - cond_exp M F (\x. - f x) x" using cond_exp_uminus[OF assms(1)] by force + moreover have "AE x in M. cond_exp M F (\x. - f x) x \ - c" using assms by (intro cond_exp_ge_c) auto + ultimately show ?thesis by (force simp add: minus_le_iff) +qed + +corollary cond_exp_mono: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" "AE x in M. f x \ g x" + shows "AE x in M. cond_exp M F f x \ cond_exp M F g x" + using cond_exp_le_c[OF Bochner_Integration.integrable_diff, OF assms(1,2), of 0] + cond_exp_diff[OF assms(1,2)] assms(3) by auto + +corollary cond_exp_min: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" + shows "AE \ in M. cond_exp M F (\x. min (f x) (g x)) \ \ min (cond_exp M F f \) (cond_exp M F g \)" +proof - + have "AE \ in M. cond_exp M F (\x. min (f x) (g x)) \ \ cond_exp M F f \" by (intro cond_exp_mono integrable_min assms, simp) + moreover have "AE \ in M. cond_exp M F (\x. min (f x) (g x)) \ \ cond_exp M F g \" by (intro cond_exp_mono integrable_min assms, simp) + ultimately show "AE \ in M. cond_exp M F (\x. min (f x) (g x)) \ \ min (cond_exp M F f \) (cond_exp M F g \)" by fastforce +qed + +corollary cond_exp_max: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" + assumes "integrable M f" "integrable M g" + shows "AE \ in M. cond_exp M F (\x. max (f x) (g x)) \ \ max (cond_exp M F f \) (cond_exp M F g \)" +proof - + have "AE \ in M. cond_exp M F (\x. max (f x) (g x)) \ \ cond_exp M F f \" by (intro cond_exp_mono integrable_max assms, simp) + moreover have "AE \ in M. cond_exp M F (\x. max (f x) (g x)) \ \ cond_exp M F g \" by (intro cond_exp_mono integrable_max assms, simp) + ultimately show "AE \ in M. cond_exp M F (\x. max (f x) (g x)) \ \ max (cond_exp M F f \) (cond_exp M F g \)" by fastforce +qed + +corollary cond_exp_inf: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}" + assumes "integrable M f" "integrable M g" + shows "AE \ in M. cond_exp M F (\x. inf (f x) (g x)) \ \ inf (cond_exp M F f \) (cond_exp M F g \)" + unfolding inf_min using assms by (rule cond_exp_min) + +corollary cond_exp_sup: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector, lattice}" + assumes "integrable M f" "integrable M g" + shows "AE \ in M. cond_exp M F (\x. sup (f x) (g x)) \ \ sup (cond_exp M F f \) (cond_exp M F g \)" + unfolding sup_max using assms by (rule cond_exp_max) + +end + +subsection \Probability Spaces\ + +lemma (in prob_space) sigma_finite_subalgebra_restr_to_subalg: + assumes "subalgebra M F" + shows "sigma_finite_subalgebra M F" +proof (intro sigma_finite_subalgebra.intro) + interpret F: prob_space "restr_to_subalg M F" using assms prob_space_restr_to_subalg prob_space_axioms by blast + show "sigma_finite_measure (restr_to_subalg M F)" by (rule F.sigma_finite_measure_axioms) +qed (rule assms) + +lemma (in prob_space) cond_exp_trivial: + fixes f :: "'a \ 'b :: {second_countable_topology, banach}" + assumes "integrable M f" + shows "AE x in M. cond_exp M (sigma (space M) {}) f x = expectation f" +proof - + interpret sigma_finite_subalgebra M "sigma (space M) {}" by (auto intro: sigma_finite_subalgebra_restr_to_subalg simp add: subalgebra_def sigma_sets_empty_eq) + show ?thesis using assms by (intro cond_exp_charact) (auto simp add: sigma_sets_empty_eq set_lebesgue_integral_def prob_space cong: Bochner_Integration.integral_cong) +qed + +text \The following lemma shows that independent \\\-algebras don't matter for the conditional expectation. The proof is adapted from \cite{Zitkovic_2015}.\ + +lemma (in prob_space) cond_exp_indep_subalgebra: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, real_normed_field}" + assumes subalgebra: "subalgebra M F" "subalgebra M G" + and independent: "indep_set G (sigma (space M) (F \ vimage_algebra (space M) f borel))" + assumes [measurable]: "integrable M f" + shows "AE x in M. cond_exp M (sigma (space M) (F \ G)) f x = cond_exp M F f x" +proof - + interpret Un_sigma: sigma_finite_subalgebra M "sigma (space M) (F \ G)" using assms(1,2) by (auto intro!: sigma_finite_subalgebra_restr_to_subalg sets.sigma_sets_subset simp add: subalgebra_def space_measure_of_conv sets_measure_of_conv) + interpret sigma_finite_subalgebra M F using assms by (auto intro: sigma_finite_subalgebra_restr_to_subalg) + { + fix A + assume asm: "A \ sigma (space M) {a \ b | a b. a \ F \ b \ G}" + have in_events: "sigma_sets (space M) {a \ b |a b. a \ sets F \ b \ sets G} \ events" using subalgebra by (intro sets.sigma_sets_subset, auto simp add: subalgebra_def) + have "Int_stable {a \ b | a b. a \ F \ b \ G}" + proof - + { + fix af bf ag bg + assume F: "af \ F" "bf \ F" and G: "ag \ G" "bg \ G" + have "af \ bf \ F" by (intro sets.Int F) + moreover have "ag \ bg \ G" by (intro sets.Int G) + ultimately have "\a b. af \ ag \ (bf \ bg) = a \ b \ a \ sets F \ b \ sets G" by (metis inf_assoc inf_left_commute) + } + thus ?thesis by (force intro!: Int_stableI) + qed + moreover have "{a \ b | a b. a \ F \ b \ G} \ Pow (space M)" using subalgebra by (force simp add: subalgebra_def dest: sets.sets_into_space) + moreover have "A \ sigma_sets (space M) {a \ b | a b. a \ F \ b \ G}" using calculation asm by force + ultimately have "set_lebesgue_integral M A f = set_lebesgue_integral M A (cond_exp M F f)" + proof (induction rule: sigma_sets_induct_disjoint) + case (basic A) + then obtain a b where A: "A = a \ b" "a \ F" "b \ G" by blast + + hence events[measurable]: "a \ events" "b \ events" using subalgebra by (auto simp add: subalgebra_def) + + have [simp]: "sigma_sets (space M) {indicator b -` A \ space M |A. A \ borel} \ G" + using borel_measurable_indicator[OF A(3), THEN measurable_sets] sets.top subalgebra + by (intro sets.sigma_sets_subset') (fastforce simp add: subalgebra_def)+ + + have Un_in_sigma: "F \ vimage_algebra (space M) f borel \ sigma (space M) (F \ vimage_algebra (space M) f borel)" by (metis equalityE le_supI sets.space_closed sigma_le_sets space_vimage_algebra subalg subalgebra_def) + + have [intro]: "indep_var borel (indicator b) borel (\\. indicator a \ *\<^sub>R f \)" + proof - + have [simp]: "sigma_sets (space M) {(\\. indicator a \ *\<^sub>R f \) -` A \ space M |A. A \ borel} \ sigma (space M) (F \ vimage_algebra (space M) f borel)" + proof - + have *: "(\\. indicator a \ *\<^sub>R f \) \ borel_measurable (sigma (space M) (F \ vimage_algebra (space M) f borel))" + using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra + by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD]) + (auto simp add: space_measure_of_conv subalgebra_def sets_vimage_algebra2) + thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv) + qed + have "indep_set (sigma_sets (space M) {indicator b -` A \ space M |A. A \ borel}) (sigma_sets (space M) {(\\. indicator a \ *\<^sub>R f \) -` A \ space M |A. A \ borel})" + using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split) + thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR) + qed + + have [intro]: "indep_var borel (indicator b) borel (\\. indicat_real a \ *\<^sub>R cond_exp M F f \)" + proof - + have [simp]:"sigma_sets (space M) {(\\. indicator a \ *\<^sub>R cond_exp M F f \) -` A \ space M |A. A \ borel} \ sigma (space M) (F \ vimage_algebra (space M) f borel)" + proof - + have *: "(\\. indicator a \ *\<^sub>R cond_exp M F f \) \ borel_measurable (sigma (space M) (F \ vimage_algebra (space M) f borel))" + using borel_measurable_indicator[OF A(2), THEN measurable_sets, OF borel_open] subalgebra + borel_measurable_cond_exp[THEN measurable_sets, OF borel_open, of _ M F f] + by (intro borel_measurable_scaleR borel_measurableI Un_in_sigma[THEN subsetD]) + (auto simp add: space_measure_of_conv subalgebra_def) + thus ?thesis using measurable_sets[OF *] by (intro sets.sigma_sets_subset', auto simp add: space_measure_of_conv) + qed + have "indep_set (sigma_sets (space M) {indicator b -` A \ space M |A. A \ borel}) (sigma_sets (space M) {(\\. indicator a \ *\<^sub>R cond_exp M F f \) -` A \ space M |A. A \ borel})" + using independent unfolding indep_set_def by (rule indep_sets_mono_sets, auto split: bool.split) + thus ?thesis by (subst indep_var_eq, auto intro!: borel_measurable_scaleR) + qed + + have "set_lebesgue_integral M A f = (LINT x|M. indicator b x * (indicator a x *\<^sub>R f x))" + unfolding set_lebesgue_integral_def A indicator_inter_arith + by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1)) + also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *\<^sub>R f x)" + by (intro indep_var_lebesgue_integral + Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator] + integrable_mult_indicator[OF _ assms(4)], blast) (auto simp add: indicator_def) + also have "... = (LINT x|M. indicator b x) * (LINT x|M. indicator a x *\<^sub>R cond_exp M F f x)" + using cond_exp_set_integral[OF assms(4) A(2)] unfolding set_lebesgue_integral_def by argo + also have "... = (LINT x|M. indicator b x * (indicator a x *\<^sub>R cond_exp M F f x))" + by (intro indep_var_lebesgue_integral[symmetric] + Bochner_Integration.integrable_bound[OF integrable_const[of "1 :: 'b"] borel_measurable_indicator] + integrable_mult_indicator[OF _ integrable_cond_exp], blast) (auto simp add: indicator_def) + also have "... = set_lebesgue_integral M A (cond_exp M F f)" + unfolding set_lebesgue_integral_def A indicator_inter_arith + by (intro Bochner_Integration.integral_cong, auto simp add: scaleR_scaleR[symmetric] indicator_times_eq_if(1)) + finally show ?case . + next + case empty + then show ?case unfolding set_lebesgue_integral_def by simp + next + case (compl A) + have A_in_space: "A \ space M" using compl using in_events sets.sets_into_space by blast + have "set_lebesgue_integral M (space M - A) f = set_lebesgue_integral M (space M - A \ A) f - set_lebesgue_integral M A f" + using compl(1) in_events + by (subst set_integral_Un[of "space M - A" A], blast) + (simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)], fast)+ + also have "... = set_lebesgue_integral M (space M - A \ A) (cond_exp M F f) - set_lebesgue_integral M A (cond_exp M F f)" + using cond_exp_set_integral[OF assms(4) sets.top] compl subalgebra by (simp add: subalgebra_def Un_absorb2[OF A_in_space]) + also have "... = set_lebesgue_integral M (space M - A) (cond_exp M F f)" + using compl(1) in_events + by (subst set_integral_Un[of "space M - A" A], blast) + (simp | intro integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp], fast)+ + finally show ?case . + next + case (union A) + have "set_lebesgue_integral M (\ (range A)) f = (\i. set_lebesgue_integral M (A i) f)" + using union in_events + by (intro lebesgue_integral_countable_add) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ assms(4)]) + also have "... = (\i. set_lebesgue_integral M (A i) (cond_exp M F f))" using union by presburger + also have "... = set_lebesgue_integral M (\ (range A)) (cond_exp M F f)" + using union in_events + by (intro lebesgue_integral_countable_add[symmetric]) (auto simp add: disjoint_family_onD intro!: integrable_mult_indicator[folded set_integrable_def, OF _ integrable_cond_exp]) + finally show ?case . + qed + } + moreover have "sigma (space M) {a \ b | a b. a \ F \ b \ G} = sigma (space M) (F \ G)" + proof - + have "sigma_sets (space M) {a \ b |a b. a \ sets F \ b \ sets G} = sigma_sets (space M) (sets F \ sets G)" + proof - + { + fix a b assume asm: "a \ F" "b \ G" + hence "a \ b \ sigma_sets (space M) (F \ G)" using subalgebra unfolding Int_range_binary by (intro sigma_sets_Inter[OF _ binary_in_sigma_sets]) (force simp add: subalgebra_def dest: sets.sets_into_space)+ + } + moreover + { + fix a + assume "a \ sets F" + hence "a \ sigma_sets (space M) {a \ b |a b. a \ sets F \ b \ sets G}" + using subalgebra sets.top[of G] sets.sets_into_space[of _ F] + by (intro sigma_sets.Basic, auto simp add: subalgebra_def) + } + moreover + { + fix a assume "a \ sets F \ a \ sets G" "a \ sets F" + hence "a \ sets G" by blast + hence "a \ sigma_sets (space M) {a \ b |a b. a \ sets F \ b \ sets G}" + using subalgebra sets.top[of F] sets.sets_into_space[of _ G] + by (intro sigma_sets.Basic, auto simp add: subalgebra_def) + } + ultimately show ?thesis by (intro sigma_sets_eqI) auto + qed + thus ?thesis using subalgebra by (intro sigma_eqI) (force simp add: subalgebra_def dest: sets.sets_into_space)+ + qed + moreover have "(cond_exp M F f) \ borel_measurable (sigma (space M) (sets F \ sets G))" + proof - + have "F \ sigma (space M) (F \ G)" by (metis Un_least Un_upper1 measure_of_of_measure sets.space_closed sets_measure_of sigma_sets_subseteq subalg subalgebra(2) subalgebra_def) + thus ?thesis using borel_measurable_cond_exp[THEN measurable_sets, OF borel_open, of _ M F f] subalgebra by (intro borel_measurableI, force simp only: space_measure_of_conv subalgebra_def) + qed + ultimately show ?thesis using assms(4) integrable_cond_exp by (intro Un_sigma.cond_exp_charact) presburger+ +qed + +text \If a random variable is independent of a \\\-algebra \<^term>\F\, its conditional expectation \<^term>\cond_exp M F f\ is just its expectation.\ + +lemma (in prob_space) cond_exp_indep: + fixes f :: "'a \ 'b :: {second_countable_topology, banach, real_normed_field}" + assumes subalgebra: "subalgebra M F" + and independent: "indep_set F (vimage_algebra (space M) f borel)" + and integrable: "integrable M f" + shows "AE x in M. cond_exp M F f x = expectation f" +proof - + have "indep_set F (sigma (space M) (sigma (space M) {} \ (vimage_algebra (space M) f borel)))" + using independent unfolding indep_set_def + by (rule indep_sets_mono_sets, simp add: bool.split) + (metis bot.extremum dual_order.refl sets.sets_measure_of_eq sets.sigma_sets_subset' sets_vimage_algebra_space space_vimage_algebra sup.absorb_iff2) + hence cond_exp_indep: "AE x in M. cond_exp M (sigma (space M) (sigma (space M) {} \ F)) f x = expectation f" + using cond_exp_indep_subalgebra[OF _ subalgebra _ integrable, of "sigma (space M) {}"] cond_exp_trivial[OF integrable] + by (auto simp add: subalgebra_def sigma_sets_empty_eq) + have "sets (sigma (space M) (sigma (space M) {} \ F)) = F" + using subalgebra sets.top[of F] unfolding subalgebra_def + by (simp add: sigma_sets_empty_eq, subst insert_absorb[of "space M" F], blast) + (metis insert_absorb[OF sets.empty_sets] sets.sets_measure_of_eq) + hence "AE x in M. cond_exp M (sigma (space M) (sigma (space M) {} \ F)) f x = cond_exp M F f x" by (rule cond_exp_sets_cong) + thus ?thesis using cond_exp_indep by force +qed + +end \ No newline at end of file diff --git a/thys/Martingales/Elementary_Metric_Spaces_Supplement.thy b/thys/Martingales/Elementary_Metric_Spaces_Supplement.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Elementary_Metric_Spaces_Supplement.thy @@ -0,0 +1,71 @@ +theory Elementary_Metric_Spaces_Supplement + imports "HOL-Analysis.Elementary_Metric_Spaces" +begin + +section \Supplementary Lemmas for Elementary Metric Spaces\ + +subsection \Diameter Lemma\ + +lemma diameter_comp_strict_mono: + fixes s :: "nat \ 'a :: metric_space" + assumes "strict_mono r" "bounded {s i |i. r n \ i}" + shows "diameter {s (r i) | i. n \ i} \ diameter {s i | i. r n \ i}" +proof (rule diameter_subset) + show "{s (r i) | i. n \ i} \ {s i | i. r n \ i}" using assms(1) monotoneD strict_mono_mono by fastforce +qed (intro assms(2)) + +lemma diameter_bounded_bound': + fixes S :: "'a :: metric_space set" + assumes S: "bdd_above (case_prod dist ` (S\S))" "x \ S" "y \ S" + shows "dist x y \ diameter S" +proof - + have "(x,y) \ S\S" using S by auto + then have "dist x y \ (SUP (x,y)\S\S. dist x y)" by (rule cSUP_upper2[OF assms(1)]) simp + with \x \ S\ show ?thesis by (auto simp: diameter_def) +qed + +lemma bounded_imp_dist_bounded: + assumes "bounded (range s)" + shows "bounded ((\(i, j). dist (s i) (s j)) ` ({n..} \ {n..}))" + using bounded_dist_comp[OF bounded_fst bounded_snd, OF bounded_Times(1,1)[OF assms(1,1)]] by (rule bounded_subset, force) + +text \A sequence is Cauchy, if and only if it is bounded and it's diameter tends to zero. The diameter is well-defined only if the sequence is bounded.\ +lemma cauchy_iff_diameter_tends_to_zero_and_bounded: + fixes s :: "nat \ 'a :: metric_space" + shows "Cauchy s \ ((\n. diameter {s i | i. i \ n}) \ 0 \ bounded (range s))" +proof - + have "{s i |i. N \ i} \ {}" for N by blast + hence diameter_SUP: "diameter {s i |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i) (s j))" for N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) + show ?thesis + proof (intro iffI) + assume asm: "Cauchy s" + have "\N. \n\N. norm (diameter {s i |i. n \ i}) < e" if e_pos: "e > 0" for e + proof - + obtain N where dist_less: "dist (s n) (s m) < (1/2) * e" if "n \ N" "m \ N" for n m using asm e_pos by (metis Cauchy_def mult_pos_pos zero_less_divide_iff zero_less_numeral zero_less_one) + { + fix r assume "r \ N" + hence "dist (s n) (s m) < (1/2) * e" if "n \ r" "m \ r" for n m using dist_less that by simp + hence "(SUP (i, j) \ {r..} \ {r..}. dist (s i) (s j)) \ (1/2) * e" by (intro cSup_least) fastforce+ + also have "... < e" using e_pos by simp + finally have "diameter {s i |i. r \ i} < e" using diameter_SUP by presburger + } + moreover have "diameter {s i |i. r \ i} \ 0" for r unfolding diameter_SUP using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above, OF asm] by (intro cSup_upper2, auto) + ultimately show ?thesis by auto + qed + thus "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" using cauchy_imp_bounded[OF asm] by (simp add: LIMSEQ_iff) + next + assume asm: "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" + have "\N. \n\N. \m\N. dist (s n) (s m) < e" if e_pos: "e > 0" for e + proof - + obtain N where diam_less: "diameter {s i |i. r \ i} < e" if "r \ N" for r using LIMSEQ_D asm(1) e_pos by fastforce + { + fix n m assume "n \ N" "m \ N" + hence "dist (s n) (s m) < e" using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], OF _ diam_less[unfolded diameter_SUP]] asm by auto + } + thus ?thesis by blast + qed + then show "Cauchy s" by (simp add: Cauchy_def) + qed +qed + +end \ No newline at end of file diff --git a/thys/Martingales/Example_Coin_Toss.thy b/thys/Martingales/Example_Coin_Toss.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Example_Coin_Toss.thy @@ -0,0 +1,246 @@ +(* Author: Ata Keskin, TU München +*) + +theory Example_Coin_Toss + imports Martingale "HOL-Probability.Stream_Space" "HOL-Probability.Probability_Mass_Function" +begin + +section \Example: Coin Toss\ + +text \Consider a coin-tossing game, where the coin lands on heads with probability \p \ [0, 1]\. Assume that the gambler wins a fixed amount \c > 0\ on a heads outcome + and loses the same amount \c\ on a tails outcome. Let \(X\<^sub>n)\<^sub>n\<^sub>\\<^sub>\\ be a stochastic process, where \X\<^sub>n\ denotes the gambler’s fortune after the \n\-th coin toss. + Then, we have the following three cases.\ + +text \1. If \p = 1/2\, it means the coin is fair and has an equal chance of landing heads or tails. + In this case, the gambler, on average, neither wins nor loses money over time. The expected value of the gambler’s fortune stays the same over time. + Therefore, \(X\<^sub>n)\<^sub>n\<^sub>\\<^sub>\\ is a martingale.\ +text \2. If \p \ 1/2\ , it means the coin is biased in favor of heads. In this case, the gambler is more likely to win money on each bet. + Over time, the gambler’s fortune tends to increase on average. + Therefore, \(X\<^sub>n)\<^sub>n\<^sub>\\<^sub>\\ is a submartingale.\ + +text \3. If \p \ 1/2\ , it means the coin is biased in favor of tails. In this scenario, the gambler is more likely to lose money on each bet. + Over time, the gambler’s fortune decreases on average. + Therefore, \(X\<^sub>n)\<^sub>n\<^sub>\\<^sub>\\ is a supermartingale.\ + +text \To formalize this example, we first consider a probability space consisting of infinite sequences of coin tosses.\ + +definition bernoulli_stream :: "real \ (bool stream) measure" where + "bernoulli_stream p = stream_space (measure_pmf (bernoulli_pmf p))" + +lemma space_bernoulli_stream[simp]: "space (bernoulli_stream p) = UNIV" by (simp add: bernoulli_stream_def space_stream_space) + +text \We define the fortune of the player at time \<^term>\n\ to be the number of heads minus number of tails.\ + +definition fortune :: "nat \ bool stream \ real" where + "fortune n = (\s. \b \ stake (Suc n) s. if b then 1 else -1)" + +definition toss :: "nat \ bool stream \ real" where + "toss n = (\s. if snth s n then 1 else -1)" + +lemma toss_indicator_def: "toss n = indicator {s. s !! n} - indicator {s. \ s !! n}" + unfolding toss_def indicator_def by force + +lemma range_toss: "range (toss n) = {-1, 1}" +proof - + have "sconst True !! n" by simp + moreover have "\sconst False !! n" by simp + ultimately have "\x. x !! n" "\x. \x !! n" by blast+ + thus ?thesis unfolding toss_def image_def by auto +qed + +lemma vimage_toss: "toss n -` A = (if 1 \ A then {s. s !! n} else {}) \ (if -1 \ A then {s. \s !! n} else {})" + unfolding vimage_def toss_def by auto + +lemma fortune_Suc: "fortune (Suc n) s = fortune n s + toss (Suc n) s" + by (induction n arbitrary: s) (simp add: fortune_def toss_def)+ + +lemma fortune_toss_sum: "fortune n s = (\i \ {..n}. toss i s)" + by (induction n arbitrary: s) (simp add: fortune_def toss_def, simp add: fortune_Suc) + +lemma fortune_bound: "norm (fortune n s) \ Suc n" by (induction n) (force simp add: fortune_toss_sum toss_def)+ + +text \Our definition of \<^term>\bernoulli_stream\ constitutes a probability space.\ + +interpretation prob_space "bernoulli_stream p" unfolding bernoulli_stream_def by (simp add: measure_pmf.prob_space_axioms prob_space.prob_space_stream_space) + +abbreviation "toss_filtration p \ nat_natural_filtration (bernoulli_stream p) toss" + +text \The stochastic process \<^term>\toss\ is adapted to the filtration it generates.\ + +interpretation toss: nat_adapted_process "bernoulli_stream p" "nat_natural_filtration (bernoulli_stream p) toss" toss + by (intro nat_adapted_process.intro stochastic_process.adapted_process_natural_filtration) + (unfold_locales, auto simp add: toss_def bernoulli_stream_def) + +text \Similarly, the stochastic process \<^term>\fortune\ is adapted to the filtration generated by the tosses.\ + +interpretation fortune: nat_finite_adapted_process_linorder "bernoulli_stream p" "nat_natural_filtration (bernoulli_stream p) toss" fortune +proof - + show "nat_finite_adapted_process_linorder (bernoulli_stream p) (toss_filtration p) fortune" + unfolding fortune_toss_sum + by (intro nat_finite_adapted_process_linorder.intro + finite_adapted_process_linorder.intro + finite_adapted_process_order.intro + finite_adapted_process.intro + toss.partial_sum_adapted[folded atMost_atLeast0]) intro_locales +qed + +lemma integrable_toss: "integrable (bernoulli_stream p) (toss n)" + using toss.random_variable + by (intro Bochner_Integration.integrable_bound[OF integrable_const[of _ "1 :: real"]]) (auto simp add: toss_def) + +lemma integrable_fortune: "integrable (bernoulli_stream p) (fortune n)" using fortune_bound + by (intro Bochner_Integration.integrable_bound[OF integrable_const[of _ "Suc n"] fortune.random_variable]) auto + +text \We provide the following lemma to explicitly calculate the probability of events in this probability space.\ + +lemma measure_bernoulli_stream_snth_pred: + assumes "0 \ p" and "p \ 1" and "finite J" + shows "prob p {w \ space (bernoulli_stream p). \j\J. P j = w !! j} = p ^ card (J \ Collect P) * (1 - p) ^ (card (J - Collect P))" +proof - + let ?PiE = "(\\<^sub>E i\J. if P i then {True} else {False})" + have "product_prob_space (\_. measure_pmf (bernoulli_pmf p))" by unfold_locales + + hence *: "to_stream -` {s. \i\J. P i = s !! i} = {s. \i\J. P i = s i}" using assms by (simp add: to_stream_def) + also have "... = prod_emb UNIV (\_. measure_pmf (bernoulli_pmf p)) J ?PiE" + proof - + { + fix s assume "(\i\J. P i = s i)" + hence "(\i\J. P i = s i) = (s \ prod_emb UNIV (\_. measure_pmf (bernoulli_pmf p)) J ?PiE)" + by (subst prod_emb_iff[of s]) (smt (verit, best) not_def assms(3) id_def PiE_eq_singleton UNIV_I extensional_UNIV insert_iff singletonD space_measure_pmf) + } + moreover + { + fix s assume "\(\i\J. P i = s i)" + then obtain i where "i \ J" "P i \ s i" by blast + hence "(\i\J. P i = s i) = (s \ prod_emb UNIV (\_. measure_pmf (bernoulli_pmf p)) J ?PiE)" + by (simp add: restrict_def prod_emb_iff[of s]) (smt (verit, ccfv_SIG) PiE_mem assms(3) id_def insert_iff singleton_iff) + } + ultimately show ?thesis by auto + qed + finally have inteq: "(to_stream -` {s. \i\J. P i = s !! i}) = prod_emb UNIV (\_. measure_pmf (bernoulli_pmf p)) J ?PiE" . + let ?M = "(Pi\<^sub>M UNIV (\_. measure_pmf (bernoulli_pmf p)))" + have "emeasure (bernoulli_stream p) {s \ space (bernoulli_stream p). \i\J. P i = s !! i} = emeasure ?M (to_stream -` {s. \i\J. P i = s !! i})" + using assms emeasure_distr[of "to_stream" ?M "(vimage_algebra (streams (space (measure_pmf (bernoulli_pmf p)))) (!!) ?M)" "{s. \i\J. P i = s !! i}", symmetric] measurable_to_stream[of "(measure_pmf (bernoulli_pmf p))"] + by (simp only: bernoulli_stream_def stream_space_def *, simp add: space_PiM ) (smt (verit, best) emeasure_notin_sets in_vimage_algebra inf_top.right_neutral sets_distr vimage_Collect) + also have "... = emeasure ?M (prod_emb UNIV (\_. measure_pmf (bernoulli_pmf p)) J ?PiE)" using inteq by (simp add: space_PiM) + also have "... = (\i\J. emeasure (measure_pmf (bernoulli_pmf p)) (if P i then {True} else {False}))" + by (subst emeasure_PiM_emb) (auto simp add: prob_space_measure_pmf assms(3)) + also have "... = (\i\J \ Collect P. ennreal p) * (\i\J - Collect P. ennreal (1 - p))" + unfolding emeasure_pmf_single[of "bernoulli_pmf p" True, unfolded pmf_bernoulli_True[OF assms(1,2)], symmetric] + emeasure_pmf_single[of "bernoulli_pmf p" False, unfolded pmf_bernoulli_False[OF assms(1,2)], symmetric] + by (simp add: prod.Int_Diff[OF assms(3), of _ "Collect P"]) + also have "... = p ^ card (J \ Collect P) * (1 - p) ^ card (J - Collect P)" using assms by (simp add: prod_ennreal ennreal_mult' ennreal_power) + finally show ?thesis using assms by (intro measure_eq_emeasure_eq_ennreal) auto +qed + +lemma + assumes "0 \ p" and "p \ 1" + shows measure_bernoulli_stream_snth: "prob p {w \ space (bernoulli_stream p). w !! i} = p" + and measure_bernoulli_stream_neg_snth: "prob p {w \ space (bernoulli_stream p). \w !! i} = 1 - p" + using measure_bernoulli_stream_snth_pred[OF assms, of "{i}" "\x. True"] + measure_bernoulli_stream_snth_pred[OF assms, of "{i}" "\x. False"] by auto + +text \Now we can express the expected value of a single coin toss.\ + +lemma integral_toss: + assumes "0 \ p" "p \ 1" + shows "expectation p (toss n) = 2 * p - 1" +proof - + have [simp]:"{s. s !! n} \ events p" using measurable_snth[THEN measurable_sets, of "{True}" "measure_pmf (bernoulli_pmf p)" n, folded bernoulli_stream_def] + by (simp add: vimage_def) + have "expectation p (toss n) = Bochner_Integration.simple_bochner_integral (bernoulli_stream p) (toss n)" + using toss.random_variable[of n, THEN measurable_sets] + by (intro simple_bochner_integrable_eq_integral[symmetric] simple_bochner_integrable.intros) (auto simp add: toss_def simple_function_def image_def) + also have "... = p - prob p {s. \ s !! n}" unfolding simple_bochner_integral_def using measure_bernoulli_stream_snth[OF assms] + by (simp add: range_toss, simp add: toss_def) + also have "... = p - (1 - prob p {s. s !! n})" by (subst prob_compl[symmetric], auto simp add: Collect_neg_eq Compl_eq_Diff_UNIV) + finally show ?thesis using measure_bernoulli_stream_snth[OF assms] by simp +qed + +text \Now, we show that the tosses are independent from one another.\ + +lemma indep_vars_toss: + assumes "0 \ p" "p \ 1" + shows "indep_vars p (\_. borel) toss {0..}" +proof (subst indep_vars_def, intro conjI indep_sets_sigma) + { + fix A J assume asm: "J \ {}" "finite J" "\j\J. A j \ {toss j -` A \ space (bernoulli_stream p) |A. A \ borel}" + hence "\j\J. \B \ borel. A j = toss j -` B \ space (bernoulli_stream p)" by auto + then obtain B where B_is: "A j = toss j -` B j \ space (bernoulli_stream p)" "B j \ borel" if "j \ J" for j by metis + + have "prob p (\ (A ` J)) = (\j\J. prob p (A j))" + proof cases + text \We consider the case where there is a zero probability event.\ + assume "\j \ J. 1 \ B j \ -1 \ B j" + then obtain j where j_is: "j \ J" "1 \ B j" "-1 \ B j" by blast + hence A_j_empty: "A j = {}" using B_is by (force simp add: toss_def vimage_def) + hence "\ (A ` J) = {}" using j_is by blast + moreover have "prob p (A j) = 0" using A_j_empty by simp + ultimately show ?thesis using j_is asm(2) by auto + next + text \We now assume all events have positive probability.\ + assume "\(\j \ J. 1 \ B j \ -1 \ B j)" + hence *: "1 \ B j \ -1 \ B j" if "j \ J" for j using that by blast + + + define J' where [simp]: "J' = {j \ J. (1 \ B j) \ (-1 \ B j)}" + hence "toss j w \ B j \ (1 \ B j) = w !! j" if "j \ J'" for w j using that unfolding toss_def by simp + hence "(\ (A ` J')) = {w \ space (bernoulli_stream p). \j\J'. (1 \ B j) = w !! j}" using B_is by force + hence prob_J': "prob p (\ (A ` J')) = p ^ card (J' \ {j. 1 \ B j}) * (1 - p) ^ card (J' - {j. 1 \ B j})" + using measure_bernoulli_stream_snth_pred[OF assms finite_subset[OF _ asm(2)], of J' "\j. 1 \ B j"] by auto + + text \The index set \<^term>\J'\ consists of the indices of all non-trivial events.\ + + have A_j_True: "A j = {w \ space (bernoulli_stream p). w !! j}" if "j \ J' \ {j. 1 \ B j}" for j + using that by (auto simp add: toss_def B_is(1) split: if_splits) + + have A_j_False: "A j = {w \ space (bernoulli_stream p). \w !! j}" if "j \ J' - {j. 1 \ B j}" for j + using that B_is by (auto simp add: toss_def) + + have A_j_top: "A j = space (bernoulli_stream p)" if "j \ J - J'" for j using that * by (auto simp add: B_is toss_def) + hence "\ (A ` J) = \ (A ` J')" by auto + hence "prob p (\ (A ` J)) = prob p (\ (A ` J'))" by presburger + also have "... = (\j\J' \ {j. 1 \ B j}. prob p (A j)) * (\j\J' - {j. 1 \ B j}. prob p (A j))" + by (simp only: prob_J' A_j_True A_j_False measure_bernoulli_stream_snth[OF assms] measure_bernoulli_stream_neg_snth[OF assms] cong: prod.cong) simp + also have "... = (\j\J'. prob p (A j))" using asm(2) by (intro prod.Int_Diff[symmetric]) auto + also have "... = (\j\J'. prob p (A j)) * (\j\J - J'. prob p (A j))" using A_j_top prob_space by simp + also have "... = (\j\J. prob p (A j))" using asm(2) by (metis (no_types, lifting) J'_def mem_Collect_eq mult.commute prod.subset_diff subsetI) + finally show ?thesis . + qed + } + thus "indep_sets p (\i. {toss i -` A \ space (bernoulli_stream p) |A. A \ sets borel}) {0..}" using measurable_sets[OF toss.random_variable] + by (intro indep_setsI subsetI) fastforce +qed (simp, intro Int_stableI, simp, metis sets.Int vimage_Int) + +text \The fortune of a player is a martingale (resp. sub- or supermartingale) with respect to the filtration generated by the coin tosses.\ + +theorem fortune_martingale: + assumes "p = 1/2" + shows "nat_martingale (bernoulli_stream p) (toss_filtration p) fortune" + using cond_exp_indep[OF fortune.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p] + integral_toss assms + by (intro fortune.martingale_of_cond_exp_diff_Suc_eq_zero integrable_fortune) (force simp add: fortune_toss_sum) + +theorem fortune_submartingale: + assumes "1/2 \ p" "p \ 1" + shows "nat_submartingale (bernoulli_stream p) (toss_filtration p) fortune" +proof (intro fortune.submartingale_of_cond_exp_diff_Suc_nonneg integrable_fortune) + fix n + show "AE \ in bernoulli_stream p. 0 \ cond_exp (bernoulli_stream p) (toss_filtration p n) (\\. fortune (Suc n) \ - fortune n \) \" + using cond_exp_indep[OF fortune.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p n] + integral_toss[of p "Suc n"] assms + by (force simp add: fortune_toss_sum) +qed + +theorem fortune_supermartingale: + assumes "0 \ p" "p \ 1/2" + shows "nat_supermartingale (bernoulli_stream p) (toss_filtration p) fortune" +proof (intro fortune.supermartingale_of_cond_exp_diff_Suc_le_zero integrable_fortune) + fix n + show "AE \ in bernoulli_stream p. 0 \ cond_exp (bernoulli_stream p) (toss_filtration p n) (\\. fortune (Suc n) \ - fortune n \) \" + using cond_exp_indep[OF fortune.subalg indep_set_natural_filtration integrable_toss, OF zero_order(1) lessI indep_vars_toss, of p n] + integral_toss[of p "Suc n"] assms + by (force simp add: fortune_toss_sum) +qed + +end diff --git a/thys/Martingales/Filtered_Measure.thy b/thys/Martingales/Filtered_Measure.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Filtered_Measure.thy @@ -0,0 +1,86 @@ +(* Author: Ata Keskin, TU München +*) + +theory Filtered_Measure + imports "HOL-Probability.Conditional_Expectation" +begin + +section \Filtered Measure Spaces\ + +subsection \Filtered Measure\ + +locale filtered_measure = + fixes M F and t\<^sub>0 :: "'b :: {second_countable_topology, order_topology, t2_space}" + assumes subalgebras: "\i. t\<^sub>0 \ i \ subalgebra M (F i)" + and sets_F_mono: "\i j. t\<^sub>0 \ i \ i \ j \ sets (F i) \ sets (F j)" +begin + +lemma space_F[simp]: + assumes "t\<^sub>0 \ i" + shows "space (F i) = space M" + using subalgebras assms by (simp add: subalgebra_def) + +lemma subalgebra_F[intro]: + assumes "t\<^sub>0 \ i" "i \ j" + shows "subalgebra (F j) (F i)" + unfolding subalgebra_def using assms by (simp add: sets_F_mono) + +lemma borel_measurable_mono: + assumes "t\<^sub>0 \ i" "i \ j" + shows "borel_measurable (F i) \ borel_measurable (F j)" + unfolding subset_iff by (metis assms subalgebra_F measurable_from_subalg) + +end + +locale linearly_filtered_measure = filtered_measure M F t\<^sub>0 for M and F :: "_ :: {linorder_topology} \ _" and t\<^sub>0 + +locale nat_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "nat \ _" +locale real_filtered_measure = linearly_filtered_measure M F 0 for M and F :: "real \ _" + +subsection \\\\-Finite Filtered Measure\ + +text \The locale presented here is a generalization of the \<^locale>\sigma_finite_subalgebra\ for a particular filtration.\ + +locale sigma_finite_filtered_measure = filtered_measure + + assumes sigma_finite_initial: "sigma_finite_subalgebra M (F t\<^sub>0)" + +lemma (in sigma_finite_filtered_measure) sigma_finite_subalgebra_F[intro]: + assumes "t\<^sub>0 \ i" + shows "sigma_finite_subalgebra M (F i)" + using assms by (metis dual_order.refl sets_F_mono sigma_finite_initial sigma_finite_subalgebra.nested_subalg_is_sigma_finite subalgebras subalgebra_def) + +locale nat_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: nat" for M F +locale real_sigma_finite_filtered_measure = sigma_finite_filtered_measure M F "0 :: real" for M F + +sublocale nat_sigma_finite_filtered_measure \ sigma_finite_subalgebra M "F i" by blast +sublocale real_sigma_finite_filtered_measure \ sigma_finite_subalgebra M "F \i\" by fastforce + +subsection \Finite Filtered Measure\ + +locale finite_filtered_measure = filtered_measure + finite_measure + +sublocale finite_filtered_measure \ sigma_finite_filtered_measure + using subalgebras by (unfold_locales, blast, meson dual_order.refl finite_measure_axioms finite_measure_def finite_measure_restr_to_subalg sigma_finite_measure.sigma_finite_countable) + +locale nat_finite_filtered_measure = finite_filtered_measure M F "0 :: nat" for M F +locale real_finite_filtered_measure = finite_filtered_measure M F "0 :: real" for M F + +sublocale nat_finite_filtered_measure \ nat_sigma_finite_filtered_measure .. +sublocale real_finite_filtered_measure \ real_sigma_finite_filtered_measure .. + +subsection \Constant Filtration\ + +lemma filtered_measure_constant_filtration: + assumes "subalgebra M F" + shows "filtered_measure M (\_. F) t\<^sub>0" + using assms by (unfold_locales) blast+ + +sublocale sigma_finite_subalgebra \ constant_filtration: sigma_finite_filtered_measure M "\_ :: 't :: {second_countable_topology, linorder_topology}. F" t\<^sub>0 + using subalg by (unfold_locales) blast+ + +lemma (in finite_measure) filtered_measure_constant_filtration: + assumes "subalgebra M F" + shows "finite_filtered_measure M (\_. F) t\<^sub>0" + using assms by (unfold_locales) blast+ + +end \ No newline at end of file diff --git a/thys/Martingales/Martingale.thy b/thys/Martingales/Martingale.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Martingale.thy @@ -0,0 +1,714 @@ +(* Author: Ata Keskin, TU München +*) + +theory Martingale + imports Stochastic_Process Conditional_Expectation_Banach +begin + +section \Martingales\ + +text \The following locales are necessary for defining martingales.\ + +subsection \Additional Locale Definitions\ + +locale sigma_finite_adapted_process = sigma_finite_filtered_measure M F t\<^sub>0 + adapted_process M F t\<^sub>0 X for M F t\<^sub>0 X + +locale nat_sigma_finite_adapted_process = sigma_finite_adapted_process M F "0 :: nat" X for M F X +locale real_sigma_finite_adapted_process = sigma_finite_adapted_process M F "0 :: real" X for M F X + +sublocale nat_sigma_finite_adapted_process \ nat_sigma_finite_filtered_measure .. +sublocale real_sigma_finite_adapted_process \ real_sigma_finite_filtered_measure .. + +locale finite_adapted_process = finite_filtered_measure M F t\<^sub>0 + adapted_process M F t\<^sub>0 X for M F t\<^sub>0 X + +sublocale finite_adapted_process \ sigma_finite_adapted_process .. + +locale nat_finite_adapted_process = finite_adapted_process M F "0 :: nat" X for M F X +locale real_finite_adapted_process = finite_adapted_process M F "0 :: real" X for M F X + +sublocale nat_finite_adapted_process \ nat_sigma_finite_adapted_process .. +sublocale real_finite_adapted_process \ real_sigma_finite_adapted_process .. + +(* with ordering *) + +locale sigma_finite_adapted_process_order = sigma_finite_adapted_process M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {order_topology, ordered_real_vector}" + +locale nat_sigma_finite_adapted_process_order = sigma_finite_adapted_process_order M F "0 :: nat" X for M F X +locale real_sigma_finite_adapted_process_order = sigma_finite_adapted_process_order M F "0 :: real" X for M F X + +sublocale nat_sigma_finite_adapted_process_order \ nat_sigma_finite_adapted_process .. +sublocale real_sigma_finite_adapted_process_order \ real_sigma_finite_adapted_process .. + +locale finite_adapted_process_order = finite_adapted_process M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {order_topology, ordered_real_vector}" + +locale nat_finite_adapted_process_order = finite_adapted_process_order M F "0 :: nat" X for M F X +locale real_finite_adapted_process_order = finite_adapted_process_order M F "0 :: real" X for M F X + +sublocale nat_finite_adapted_process_order \ nat_sigma_finite_adapted_process_order .. +sublocale real_finite_adapted_process_order \ real_sigma_finite_adapted_process_order .. + +(* with linear ordering *) + +locale sigma_finite_adapted_process_linorder = sigma_finite_adapted_process_order M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {linorder_topology}" + +locale nat_sigma_finite_adapted_process_linorder = sigma_finite_adapted_process_linorder M F "0 :: nat" X for M F X +locale real_sigma_finite_adapted_process_linorder = sigma_finite_adapted_process_linorder M F "0 :: real" X for M F X + +sublocale nat_sigma_finite_adapted_process_linorder \ nat_sigma_finite_adapted_process_order .. +sublocale real_sigma_finite_adapted_process_linorder \ real_sigma_finite_adapted_process_order .. + +locale finite_adapted_process_linorder = finite_adapted_process_order M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {linorder_topology}" + +locale nat_finite_adapted_process_linorder = finite_adapted_process_linorder M F "0 :: nat" X for M F X +locale real_finite_adapted_process_linorder = finite_adapted_process_linorder M F "0 :: real" X for M F X + +sublocale nat_finite_adapted_process_linorder \ nat_sigma_finite_adapted_process_linorder .. +sublocale real_finite_adapted_process_linorder \ real_sigma_finite_adapted_process_linorder .. + +subsection \Martingale\ + +text \A martingale is an adapted process where the expected value of the next observation, given all past observations, is equal to the current value.\ + +locale martingale = sigma_finite_adapted_process + + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and martingale_property: "\i j. t\<^sub>0 \ i \ i \ j \ AE \ in M. X i \ = cond_exp M (F i) (X j) \" + +locale martingale_order = martingale M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {order_topology, ordered_real_vector}" +locale martingale_linorder = martingale M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {linorder_topology, ordered_real_vector}" +sublocale martingale_linorder \ martingale_order .. + +lemma (in sigma_finite_filtered_measure) martingale_const_fun[intro]: + assumes "integrable M f" "f \ borel_measurable (F t\<^sub>0)" + shows "martingale M F t\<^sub>0 (\_. f)" + using assms sigma_finite_subalgebra.cond_exp_F_meas[OF _ assms(1), THEN AE_symmetric] borel_measurable_mono + by (unfold_locales) blast+ + +lemma (in sigma_finite_filtered_measure) martingale_cond_exp[intro]: + assumes "integrable M f" + shows "martingale M F t\<^sub>0 (\i. cond_exp M (F i) f)" + using sigma_finite_subalgebra.borel_measurable_cond_exp' borel_measurable_cond_exp + by (unfold_locales) (auto intro: sigma_finite_subalgebra.cond_exp_nested_subalg[OF _ assms] simp add: subalgebra_F subalgebras) + +corollary (in sigma_finite_filtered_measure) martingale_zero[intro]: "martingale M F t\<^sub>0 (\_ _. 0)" by fastforce + +corollary (in finite_filtered_measure) martingale_const[intro]: "martingale M F t\<^sub>0 (\_ _. c)" by fastforce + +subsection \Submartingale\ + +text \A submartingale is an adapted process where the expected value of the next observation, given all past observations, is greater than or equal to the current value.\ + +locale submartingale = sigma_finite_adapted_process_order + + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and submartingale_property: "\i j. t\<^sub>0 \ i \ i \ j \ AE \ in M. X i \ \ cond_exp M (F i) (X j) \" + +locale submartingale_linorder = submartingale M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {linorder_topology}" + +sublocale martingale_order \ submartingale using martingale_property by (unfold_locales) (force simp add: integrable)+ +sublocale martingale_linorder \ submartingale_linorder .. + +subsection \Supermartingale\ + +text \A supermartingale is an adapted process where the expected value of the next observation, given all past observations, is less than or equal to the current value.\ + +locale supermartingale = sigma_finite_adapted_process_order + + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and supermartingale_property: "\i j. t\<^sub>0 \ i \ i \ j \ AE \ in M. X i \ \ cond_exp M (F i) (X j) \" + +locale supermartingale_linorder = supermartingale M F t\<^sub>0 X for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {linorder_topology}" + +sublocale martingale_order \ supermartingale using martingale_property by (unfold_locales) (force simp add: integrable)+ +sublocale martingale_linorder \ supermartingale_linorder .. + +text \A stochastic process is a martingale, if and only if it is both a submartingale and a supermartingale.\ + +lemma martingale_iff: + shows "martingale M F t\<^sub>0 X \ submartingale M F t\<^sub>0 X \ supermartingale M F t\<^sub>0 X" +proof (rule iffI) + assume asm: "martingale M F t\<^sub>0 X" + interpret martingale_order M F t\<^sub>0 X by (intro martingale_order.intro asm) + show "submartingale M F t\<^sub>0 X \ supermartingale M F t\<^sub>0 X" using submartingale_axioms supermartingale_axioms by blast +next + assume asm: "submartingale M F t\<^sub>0 X \ supermartingale M F t\<^sub>0 X" + interpret submartingale M F t\<^sub>0 X by (simp add: asm) + interpret supermartingale M F t\<^sub>0 X by (simp add: asm) + show "martingale M F t\<^sub>0 X" using submartingale_property supermartingale_property by (unfold_locales) (intro integrable, blast, force) +qed + +subsection \Martingale Lemmas\ + +text \In the following segment, we cover basic properties of martingales.\ + +context martingale +begin + +lemma cond_exp_diff_eq_zero: + assumes "t\<^sub>0 \ i" "i \ j" + shows "AE \ in M. cond_exp M (F i) (\\. X j \ - X i \) \ = 0" + using martingale_property[OF assms] assms + sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] + sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] by fastforce + +lemma set_integral_eq: + assumes "A \ F i" "t\<^sub>0 \ i" "i \ j" + shows "set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)" +proof - + interpret sigma_finite_subalgebra M "F i" using assms(2) by blast + have "\x \ A. X i x \M = \x \ A. cond_exp M (F i) (X j) x \M" using martingale_property[OF assms(2,3)] borel_measurable_cond_exp' assms subalgebras subalgebra_def by (intro set_lebesgue_integral_cong_AE[OF _ random_variable]) fastforce+ + also have "... = \x \ A. X j x \M" using assms by (auto simp: integrable intro: cond_exp_set_integral[symmetric]) + finally show ?thesis . +qed + +lemma scaleR_const[intro]: + shows "martingale M F t\<^sub>0 (\i x. c *\<^sub>R X i x)" +proof - + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + interpret sigma_finite_subalgebra M "F i" using asm by blast + have "AE x in M. c *\<^sub>R X i x = cond_exp M (F i) (\x. c *\<^sub>R X j x) x" using asm cond_exp_scaleR_right[OF integrable, of j, THEN AE_symmetric] martingale_property[OF asm] by force + } + thus ?thesis by (unfold_locales) (auto simp add: integrable martingale.integrable) +qed + +lemma uminus[intro]: + shows "martingale M F t\<^sub>0 (- X)" + using scaleR_const[of "-1"] by (force intro: back_subst[of "martingale M F t\<^sub>0"]) + +lemma add[intro]: + assumes "martingale M F t\<^sub>0 Y" + shows "martingale M F t\<^sub>0 (\i \. X i \ + Y i \)" +proof - + interpret Y: martingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ + Y i \ = cond_exp M (F i) (\x. X j x + Y j x) \" + using sigma_finite_subalgebra.cond_exp_add[OF _ integrable martingale.integrable[OF assms], of "F i" j j, THEN AE_symmetric] + martingale_property[OF asm] martingale.martingale_property[OF assms asm] by force + } + thus ?thesis using assms + by (unfold_locales) (auto simp add: integrable martingale.integrable) +qed + +lemma diff[intro]: + assumes "martingale M F t\<^sub>0 Y" + shows "martingale M F t\<^sub>0 (\i x. X i x - Y i x)" +proof - + interpret Y: martingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ - Y i \ = cond_exp M (F i) (\x. X j x - Y j x) \" + using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable martingale.integrable[OF assms], of "F i" j j, THEN AE_symmetric] + martingale_property[OF asm] martingale.martingale_property[OF assms asm] by fastforce + } + thus ?thesis using assms by (unfold_locales) (auto simp add: integrable martingale.integrable) +qed + +end + +text \Using properties of the conditional expectation, we present the following alternative characterizations of martingales.\ + +lemma (in sigma_finite_adapted_process) martingale_of_cond_exp_diff_eq_zero: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and diff_zero: "\i j. t\<^sub>0 \ i \ i \ j \ AE x in M. cond_exp M (F i) (\\. X j \ - X i \) x = 0" + shows "martingale M F t\<^sub>0 X" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. X i \ = cond_exp M (F i) (X j) \" + using diff_zero[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] + sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce + } +qed (intro integrable) + +lemma (in sigma_finite_adapted_process) martingale_of_set_integral_eq: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and "\A i j. t\<^sub>0 \ i \ i \ j \ A \ F i \ set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)" + shows "martingale M F t\<^sub>0 X" +proof (unfold_locales) + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + interpret sigma_finite_subalgebra M "F i" using asm by blast + interpret r: sigma_finite_measure "restr_to_subalg M (F i)" by (simp add: sigma_fin_subalg) + { + fix A assume "A \ restr_to_subalg M (F i)" + hence *: "A \ F i" using sets_restr_to_subalg subalgebras asm by blast + have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral M A (X i)" using * subalg asm by (auto simp: set_lebesgue_integral_def intro: integral_subalgebra2 borel_measurable_scaleR adapted borel_measurable_indicator) + also have "... = set_lebesgue_integral M A (cond_exp M (F i) (X j))" using * assms(2)[OF asm] cond_exp_set_integral[OF integrable] asm by auto + finally have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral (restr_to_subalg M (F i)) A (cond_exp M (F i) (X j))" using * subalg by (auto simp: set_lebesgue_integral_def intro!: integral_subalgebra2[symmetric] borel_measurable_scaleR borel_measurable_cond_exp borel_measurable_indicator) + } + hence "AE \ in restr_to_subalg M (F i). X i \ = cond_exp M (F i) (X j) \" using asm by (intro r.density_unique_banach, auto intro: integrable_in_subalg subalg borel_measurable_cond_exp integrable) + thus "AE \ in M. X i \ = cond_exp M (F i) (X j) \" using AE_restr_to_subalg[OF subalg] by blast +qed (simp add: integrable) + +subsection \Submartingale Lemmas\ + +context submartingale +begin + +lemma cond_exp_diff_nonneg: + assumes "t\<^sub>0 \ i" "i \ j" + shows "AE x in M. cond_exp M (F i) (\\. X j \ - X i \) x \ 0" + using submartingale_property[OF assms] assms sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of _ j i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce + +lemma add[intro]: + assumes "submartingale M F t\<^sub>0 Y" + shows "submartingale M F t\<^sub>0 (\i \. X i \ + Y i \)" +proof - + interpret Y: submartingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ + Y i \ \ cond_exp M (F i) (\x. X j x + Y j x) \" + using sigma_finite_subalgebra.cond_exp_add[OF _ integrable submartingale.integrable[OF assms], of "F i" j j] + submartingale_property[OF asm] submartingale.submartingale_property[OF assms asm] add_mono[of "X i _" _ "Y i _"] by force + } + thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_add random_variable adapted integrable Y.random_variable Y.adapted submartingale.integrable) +qed + +lemma diff[intro]: + assumes "supermartingale M F t\<^sub>0 Y" + shows "submartingale M F t\<^sub>0 (\i \. X i \ - Y i \)" +proof - + interpret Y: supermartingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ - Y i \ \ cond_exp M (F i) (\x. X j x - Y j x) \" + using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable supermartingale.integrable[OF assms], of "F i" j j] + submartingale_property[OF asm] supermartingale.supermartingale_property[OF assms asm] diff_mono[of "X i _" _ _ "Y i _"] by force + } + thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_diff random_variable adapted integrable Y.random_variable Y.adapted supermartingale.integrable) +qed + +lemma scaleR_nonneg: + assumes "c \ 0" + shows "submartingale M F t\<^sub>0 (\i \. c *\<^sub>R X i \)" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. c *\<^sub>R X i \ \ cond_exp M (F i) (\\. c *\<^sub>R X j \) \" + using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] submartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono[OF _ assms]) + } +qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR) + +lemma scaleR_le_zero: + assumes "c \ 0" + shows "supermartingale M F t\<^sub>0 (\i \. c *\<^sub>R X i \)" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. c *\<^sub>R X i \ \ cond_exp M (F i) (\\. c *\<^sub>R X j \) \" + using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] submartingale_property[OF asm] + by (fastforce intro!: scaleR_left_mono_neg[OF _ assms]) + } +qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR) + +lemma uminus[intro]: + shows "supermartingale M F t\<^sub>0 (- X)" + unfolding fun_Compl_def using scaleR_le_zero[of "-1"] by simp + +end + +context submartingale_linorder +begin + +lemma set_integral_le: + assumes "A \ F i" "t\<^sub>0 \ i" "i \ j" + shows "set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X j)" + using submartingale_property[OF assms(2), of j] assms subalgebras + by (subst sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable assms(1), of j]) + (auto intro!: scaleR_left_mono integral_mono_AE_banach integrable_mult_indicator integrable simp add: subalgebra_def set_lebesgue_integral_def) + +lemma max: + assumes "submartingale_linorder M F t\<^sub>0 Y" + shows "submartingale_linorder M F t\<^sub>0 (\i \. max (X i \) (Y i \))" +proof (unfold_locales) + interpret Y: submartingale_linorder M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + have "AE \ in M. max (X i \) (Y i \) \ max (cond_exp M (F i) (X j) \) (cond_exp M (F i) (Y j) \)" using submartingale_property Y.submartingale_property asm unfolding max_def by fastforce + thus "AE \ in M. max (X i \) (Y i \) \ cond_exp M (F i) (\\. max (X j \) (Y j \)) \" using sigma_finite_subalgebra.cond_exp_max[OF _ integrable Y.integrable, of "F i" j j] asm by (fast intro: order.trans) + } + show "\i. t\<^sub>0 \ i \ (\\. max (X i \) (Y i \)) \ borel_measurable (F i)" "\i. t\<^sub>0 \ i \ integrable M (\\. max (X i \) (Y i \))" by (force intro: Y.integrable integrable assms)+ +qed + +lemma max_0: + shows "submartingale_linorder M F t\<^sub>0 (\i \. max 0 (X i \))" +proof - + interpret zero: martingale_linorder M F t\<^sub>0 "\_ _. 0" by (force intro: martingale_linorder.intro martingale_order.intro) + show ?thesis by (intro zero.max submartingale_linorder.intro submartingale_axioms) +qed + +end + +lemma (in sigma_finite_adapted_process_order) submartingale_of_cond_exp_diff_nonneg: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and diff_nonneg: "\i j. t\<^sub>0 \ i \ i \ j \ AE x in M. cond_exp M (F i) (\\. X j \ - X i \) x \ 0" + shows "submartingale M F t\<^sub>0 X" +proof (unfold_locales) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. X i \ \ cond_exp M (F i) (X j) \" + using diff_nonneg[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] + sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce + } +qed (intro integrable) + +lemma (in sigma_finite_adapted_process_linorder) submartingale_of_set_integral_le: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and "\A i j. t\<^sub>0 \ i \ i \ j \ A \ F i \ set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X j)" + shows "submartingale M F t\<^sub>0 X" +proof (unfold_locales) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + interpret r: sigma_finite_measure "restr_to_subalg M (F i)" using asm sigma_finite_subalgebra.sigma_fin_subalg by blast + { + fix A assume "A \ restr_to_subalg M (F i)" + hence *: "A \ F i" using asm sets_restr_to_subalg subalgebras by blast + have "set_lebesgue_integral (restr_to_subalg M (F i)) A (X i) = set_lebesgue_integral M A (X i)" using * asm subalgebras by (auto simp: set_lebesgue_integral_def intro: integral_subalgebra2 borel_measurable_scaleR adapted borel_measurable_indicator) + also have "... \ set_lebesgue_integral M A (cond_exp M (F i) (X j))" using * assms(2)[OF asm] asm sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable] by fastforce + also have "... = set_lebesgue_integral (restr_to_subalg M (F i)) A (cond_exp M (F i) (X j))" using * asm subalgebras by (auto simp: set_lebesgue_integral_def intro!: integral_subalgebra2[symmetric] borel_measurable_scaleR borel_measurable_cond_exp borel_measurable_indicator) + finally have "0 \ set_lebesgue_integral (restr_to_subalg M (F i)) A (\\. cond_exp M (F i) (X j) \ - X i \)" using * asm subalgebras by (subst set_integral_diff, auto simp add: set_integrable_def sets_restr_to_subalg intro!: integrable adapted integrable_in_subalg borel_measurable_scaleR borel_measurable_indicator borel_measurable_cond_exp integrable_mult_indicator) + } + hence "AE \ in restr_to_subalg M (F i). 0 \ cond_exp M (F i) (X j) \ - X i \" + by (intro r.density_nonneg integrable_in_subalg asm subalgebras borel_measurable_diff borel_measurable_cond_exp adapted Bochner_Integration.integrable_diff integrable_cond_exp integrable) + thus "AE \ in M. X i \ \ cond_exp M (F i) (X j) \" using AE_restr_to_subalg[OF subalgebras] asm by simp + } +qed (intro integrable) + +subsection \Supermartingale Lemmas\ + +text \The following lemmas are exact duals of the ones for submartingales.\ + +context supermartingale +begin + +lemma cond_exp_diff_nonneg: + assumes "t\<^sub>0 \ i" "i \ j" + shows "AE x in M. cond_exp M (F i) (\\. X i \ - X j \) x \ 0" + using assms supermartingale_property[OF assms] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" i j] + sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce + +lemma add[intro]: + assumes "supermartingale M F t\<^sub>0 Y" + shows "supermartingale M F t\<^sub>0 (\i \. X i \ + Y i \)" +proof - + interpret Y: supermartingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ + Y i \ \ cond_exp M (F i) (\x. X j x + Y j x) \" + using sigma_finite_subalgebra.cond_exp_add[OF _ integrable supermartingale.integrable[OF assms], of "F i" j j] + supermartingale_property[OF asm] supermartingale.supermartingale_property[OF assms asm] add_mono[of _ "X i _" _ "Y i _"] by force + } + thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_add random_variable adapted integrable Y.random_variable Y.adapted supermartingale.integrable) +qed + +lemma diff[intro]: + assumes "submartingale M F t\<^sub>0 Y" + shows "supermartingale M F t\<^sub>0 (\i \. X i \ - Y i \)" +proof - + interpret Y: submartingale M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + hence "AE \ in M. X i \ - Y i \ \ cond_exp M (F i) (\x. X j x - Y j x) \" + using sigma_finite_subalgebra.cond_exp_diff[OF _ integrable submartingale.integrable[OF assms], of "F i" j j, unfolded fun_diff_def] + supermartingale_property[OF asm] submartingale.submartingale_property[OF assms asm] diff_mono[of _ "X i _" "Y i _"] by force + } + thus ?thesis using assms by (unfold_locales) (auto simp add: borel_measurable_diff random_variable adapted integrable Y.random_variable Y.adapted submartingale.integrable) +qed + +lemma scaleR_nonneg: + assumes "c \ 0" + shows "supermartingale M F t\<^sub>0 (\i \. c *\<^sub>R X i \)" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. c *\<^sub>R X i \ \ cond_exp M (F i) (\\. c *\<^sub>R X j \) \" + using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] supermartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono[OF _ assms]) + } +qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR) + +lemma scaleR_le_zero: + assumes "c \ 0" + shows "submartingale M F t\<^sub>0 (\i \. c *\<^sub>R X i \)" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. c *\<^sub>R X i \ \ cond_exp M (F i) (\\. c *\<^sub>R X j \) \" + using sigma_finite_subalgebra.cond_exp_scaleR_right[OF _ integrable, of "F i" j c] supermartingale_property[OF asm] by (fastforce intro!: scaleR_left_mono_neg[OF _ assms]) + } +qed (auto simp add: borel_measurable_integrable borel_measurable_scaleR integrable random_variable adapted borel_measurable_const_scaleR) + +lemma uminus[intro]: + shows "submartingale M F t\<^sub>0 (- X)" + unfolding fun_Compl_def using scaleR_le_zero[of "-1"] by simp + +end + +context supermartingale_linorder +begin + +lemma set_integral_ge: + assumes "A \ F i" "t\<^sub>0 \ i" "i \ j" + shows "set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X j)" + using supermartingale_property[OF assms(2), of j] assms subalgebras + by (subst sigma_finite_subalgebra.cond_exp_set_integral[OF _ integrable assms(1), of j]) + (auto intro!: scaleR_left_mono integral_mono_AE_banach integrable_mult_indicator integrable simp add: subalgebra_def set_lebesgue_integral_def) + +lemma min: + assumes "supermartingale_linorder M F t\<^sub>0 Y" + shows "supermartingale_linorder M F t\<^sub>0 (\i \. min (X i \) (Y i \))" +proof (unfold_locales) + interpret Y: supermartingale_linorder M F t\<^sub>0 Y by (rule assms) + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + have "AE \ in M. min (X i \) (Y i \) \ min (cond_exp M (F i) (X j) \) (cond_exp M (F i) (Y j) \)" using supermartingale_property Y.supermartingale_property asm unfolding min_def by fastforce + thus "AE \ in M. min (X i \) (Y i \) \ cond_exp M (F i) (\\. min (X j \) (Y j \)) \" using sigma_finite_subalgebra.cond_exp_min[OF _ integrable Y.integrable, of "F i" j j] asm by (fast intro: order.trans) + } + show "\i. t\<^sub>0 \ i \ (\\. min (X i \) (Y i \)) \ borel_measurable (F i)" "\i. t\<^sub>0 \ i \ integrable M (\\. min (X i \) (Y i \))" by (force intro: Y.integrable integrable assms)+ +qed + +lemma min_0: + shows "supermartingale_linorder M F t\<^sub>0 (\i \. min 0 (X i \))" +proof - + interpret zero: martingale_linorder M F t\<^sub>0 "\_ _. 0" by (force intro: martingale_linorder.intro) + show ?thesis by (intro zero.min supermartingale_linorder.intro supermartingale_axioms) +qed + +end + +lemma (in sigma_finite_adapted_process_order) supermartingale_of_cond_exp_diff_le_zero: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and diff_le_zero: "\i j. t\<^sub>0 \ i \ i \ j \ AE x in M. cond_exp M (F i) (\\. X j \ - X i \) x \ 0" + shows "supermartingale M F t\<^sub>0 X" +proof + { + fix i j :: 'b assume asm: "t\<^sub>0 \ i" "i \ j" + thus "AE \ in M. X i \ \ cond_exp M (F i) (X j) \" + using diff_le_zero[OF asm] sigma_finite_subalgebra.cond_exp_diff[OF _ integrable(1,1), of "F i" j i] + sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, of i] by fastforce + } +qed (intro integrable) + +lemma (in sigma_finite_adapted_process_linorder) supermartingale_of_set_integral_ge: + assumes integrable: "\i. t\<^sub>0 \ i \ integrable M (X i)" + and "\A i j. t\<^sub>0 \ i \ i \ j \ A \ F i \ set_lebesgue_integral M A (X j) \ set_lebesgue_integral M A (X i)" + shows "supermartingale M F t\<^sub>0 X" +proof - + interpret _: adapted_process M F t\<^sub>0 "-X" by (rule uminus_adapted) + interpret uminus_X: sigma_finite_adapted_process_linorder M F t\<^sub>0 "-X" .. + note * = set_integral_uminus[unfolded set_integrable_def, OF integrable_mult_indicator[OF _ integrable]] + have "supermartingale M F t\<^sub>0 (-(- X))" + using ord_eq_le_trans[OF * ord_le_eq_trans[OF le_imp_neg_le[OF assms(2)] *[symmetric]]] subalgebras + by (intro submartingale.uminus uminus_X.submartingale_of_set_integral_le) + (clarsimp simp add: fun_Compl_def subalgebra_def integrable | fastforce)+ + thus ?thesis unfolding fun_Compl_def by simp +qed + +text \Many of the statements we have made concerning martingales can be simplified when the indexing set is the natural numbers. + Given a point in time \<^term>\i \ \\, it suffices to consider the successor \<^term>\i + 1\, instead of all future times \<^term>\j \ i\.\ + +subsection \Discrete Time Martingales\ + +locale nat_martingale = martingale M F "0 :: nat" X for M F X +locale nat_submartingale = submartingale M F "0 :: nat" X for M F X +locale nat_supermartingale = supermartingale M F "0 :: nat" X for M F X + +locale nat_submartingale_linorder = submartingale_linorder M F "0 :: nat" X for M F X +locale nat_supermartingale_linorder = supermartingale_linorder M F "0 :: nat" X for M F X + +sublocale nat_submartingale_linorder \ nat_submartingale .. +sublocale nat_supermartingale_linorder \ nat_supermartingale .. + +text \A predictable martingale is necessarily constant.\ +lemma (in nat_martingale) predictable_const: + assumes "nat_predictable_process M F X" + shows "AE \ in M. X i \ = X j \" +proof - + have *: "AE \ in M. X i \ = X 0 \" for i + proof (induction i) + case 0 + then show ?case by (simp add: bot_nat_def) + next + case (Suc i) + interpret S: nat_adapted_process M F "\i. X (Suc i)" by (intro nat_predictable_process.adapted_Suc assms) + show ?case using Suc S.adapted[of i] martingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce + qed + show ?thesis using *[of i] *[of j] by force +qed + +lemma (in nat_sigma_finite_adapted_process) martingale_of_set_integral_eq_Suc: + assumes integrable: "\i. integrable M (X i)" + and "\A i. A \ F i \ set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X (Suc i))" + shows "nat_martingale M F X" +proof (intro nat_martingale.intro martingale_of_set_integral_eq) + fix i j A assume asm: "i \ j" "A \ sets (F i)" + show "set_lebesgue_integral M A (X i) = set_lebesgue_integral M A (X j)" using asm + proof (induction "j - i" arbitrary: i j) + case 0 + then show ?case using asm by simp + next + case (Suc n) + hence *: "n = j - Suc i" by linarith + have "Suc i \ j" using Suc(2,3) by linarith + thus ?case using sets_F_mono[OF _ le_SucI] Suc(4) Suc(1)[OF *] by (auto intro: assms(2)[THEN trans]) + qed +qed (simp add: integrable) + +lemma (in nat_sigma_finite_adapted_process) martingale_nat: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. X i \ = cond_exp M (F i) (X (Suc i)) \" + shows "nat_martingale M F X" +proof (unfold_locales) + fix i j :: nat assume asm: "i \ j" + show "AE \ in M. X i \ = cond_exp M (F i) (X j) \" using asm + proof (induction "j - i" arbitrary: i j) + case 0 + hence "j = i" by simp + thus ?case using sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable adapted, THEN AE_symmetric] by blast + next + case (Suc n) + have j: "j = Suc (n + i)" using Suc by linarith + have n: "n = n + i - i" using Suc by linarith + have *: "AE \ in M. cond_exp M (F (n + i)) (X j) \ = X (n + i) \" unfolding j using assms(2)[THEN AE_symmetric] by blast + have "AE \ in M. cond_exp M (F i) (X j) \ = cond_exp M (F i) (cond_exp M (F (n + i)) (X j)) \" by (intro cond_exp_nested_subalg integrable subalg, simp add: subalgebra_def sets_F_mono) + hence "AE \ in M. cond_exp M (F i) (X j) \ = cond_exp M (F i) (X (n + i)) \" using cond_exp_cong_AE[OF integrable_cond_exp integrable *] by force + thus ?case using Suc(1)[OF n] by fastforce + qed +qed (simp add: integrable) + +lemma (in nat_sigma_finite_adapted_process) martingale_of_cond_exp_diff_Suc_eq_zero: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. cond_exp M (F i) (\\. X (Suc i) \ - X i \) \ = 0" + shows "nat_martingale M F X" +proof (intro martingale_nat integrable) + fix i + show "AE \ in M. X i \ = cond_exp M (F i) (X (Suc i)) \" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(2)[of i] by fastforce +qed + +subsection \Discrete Time Submartingales\ + +lemma (in nat_submartingale) predictable_mono: + assumes "nat_predictable_process M F X" "i \ j" + shows "AE \ in M. X i \ \ X j \" + using assms(2) +proof (induction "j - i" arbitrary: i j) + case 0 + then show ?case by simp +next + case (Suc n) + hence *: "n = j - Suc i" by linarith + interpret S: nat_adapted_process M F "\i. X (Suc i)" by (intro nat_predictable_process.adapted_Suc assms) + have "Suc i \ j" using Suc(2,3) by linarith + thus ?case using Suc(1)[OF *] S.adapted[of i] submartingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce +qed + +lemma (in nat_sigma_finite_adapted_process_linorder) submartingale_of_set_integral_le_Suc: + assumes integrable: "\i. integrable M (X i)" + and "\A i. A \ F i \ set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X (Suc i))" + shows "nat_submartingale M F X" +proof (intro nat_submartingale.intro submartingale_of_set_integral_le) + fix i j A assume asm: "i \ j" "A \ sets (F i)" + show "set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X j)" using asm + proof (induction "j - i" arbitrary: i j) + case 0 + then show ?case using asm by simp + next + case (Suc n) + hence *: "n = j - Suc i" by linarith + have "Suc i \ j" using Suc(2,3) by linarith + thus ?case using sets_F_mono[OF _ le_SucI] Suc(4) Suc(1)[OF *] by (auto intro: assms(2)[THEN order_trans]) + qed +qed (simp add: integrable) + +lemma (in nat_sigma_finite_adapted_process_linorder) submartingale_nat: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. X i \ \ cond_exp M (F i) (X (Suc i)) \" + shows "nat_submartingale M F X" + using subalg integrable assms(2) + by (intro submartingale_of_set_integral_le_Suc ord_le_eq_trans[OF set_integral_mono_AE_banach cond_exp_set_integral[symmetric]], simp) + (meson in_mono integrable_mult_indicator set_integrable_def subalgebra_def, meson integrable_cond_exp in_mono integrable_mult_indicator set_integrable_def subalgebra_def, fast+) + +lemma (in nat_sigma_finite_adapted_process_linorder) submartingale_of_cond_exp_diff_Suc_nonneg: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. cond_exp M (F i) (\\. X (Suc i) \ - X i \) \ \ 0" + shows "nat_submartingale M F X" +proof (intro submartingale_nat integrable) + fix i + show "AE \ in M. X i \ \ cond_exp M (F i) (X (Suc i)) \" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(2)[of i] by fastforce +qed + +lemma (in nat_submartingale_linorder) partial_sum_scaleR: + assumes "nat_adapted_process M F C" "\i. AE \ in M. 0 \ C i \" "\i. AE \ in M. C i \ \ R" + shows "nat_submartingale M F (\n \. \i *\<^sub>R (X (Suc i) \ - X i \))" +proof- + interpret C: nat_adapted_process M F C by (rule assms) + interpret C': nat_adapted_process M F "\i \. C (i - 1) \ *\<^sub>R (X i \ - X (i - 1) \)" by (intro nat_adapted_process.intro adapted_process.scaleR_right_adapted adapted_process.diff_adapted, unfold_locales) (auto intro: adaptedD C.adaptedD)+ + interpret C'': nat_adapted_process M F "\n \. \i *\<^sub>R (X (Suc i) \ - X i \)" by (rule C'.partial_sum_Suc_adapted[unfolded diff_Suc_1]) + interpret S: nat_sigma_finite_adapted_process_linorder M F "(\n \. \i *\<^sub>R (X (Suc i) \ - X i \))" .. + have "integrable M (\x. C i x *\<^sub>R (X (Suc i) x - X i x))" for i using assms(2,3)[of i] by (intro Bochner_Integration.integrable_bound[OF integrable_scaleR_right, OF Bochner_Integration.integrable_diff, OF integrable(1,1), of R "Suc i" i]) (auto simp add: mult_mono) + moreover have "AE \ in M. 0 \ cond_exp M (F i) (\\. (\i *\<^sub>R (X (Suc i) \ - X i \)) - (\i *\<^sub>R (X (Suc i) \ - X i \))) \" for i + using sigma_finite_subalgebra.cond_exp_measurable_scaleR[OF _ calculation _ C.adapted, of i] + cond_exp_diff_nonneg[OF _ le_SucI, OF _ order.refl, of i] assms(2,3)[of i] by (fastforce simp add: scaleR_nonneg_nonneg integrable) + ultimately show ?thesis by (intro S.submartingale_of_cond_exp_diff_Suc_nonneg Bochner_Integration.integrable_sum, blast+) +qed + +lemma (in nat_submartingale_linorder) partial_sum_scaleR': + assumes "nat_predictable_process M F C" "\i. AE \ in M. 0 \ C i \" "\i. AE \ in M. C i \ \ R" + shows "nat_submartingale M F (\n \. \i *\<^sub>R (X (Suc i) \ - X i \))" +proof - + interpret C: nat_predictable_process M F C by (rule assms) + interpret Suc_C: nat_adapted_process M F "\i. C (Suc i)" using C.adapted_Suc . + show ?thesis by (intro partial_sum_scaleR[of _ R] assms) (intro_locales) +qed + +subsection \Discrete Time Supermartingales\ + +lemma (in nat_supermartingale) predictable_mono: + assumes "nat_predictable_process M F X" "i \ j" + shows "AE \ in M. X i \ \ X j \" + using assms(2) +proof (induction "j - i" arbitrary: i j) + case 0 + then show ?case by simp +next + case (Suc n) + hence *: "n = j - Suc i" by linarith + interpret S: nat_adapted_process M F "\i. X (Suc i)" by (intro nat_predictable_process.adapted_Suc assms) + have "Suc i \ j" using Suc(2,3) by linarith + thus ?case using Suc(1)[OF *] S.adapted[of i] supermartingale_property[OF _ le_SucI, of i] sigma_finite_subalgebra.cond_exp_F_meas[OF _ integrable, of "F i" "Suc i"] by fastforce +qed + +lemma (in nat_sigma_finite_adapted_process_linorder) supermartingale_of_set_integral_ge_Suc: + assumes integrable: "\i. integrable M (X i)" + and "\A i. A \ F i \ set_lebesgue_integral M A (X i) \ set_lebesgue_integral M A (X (Suc i))" + shows "nat_supermartingale M F X" +proof - + interpret _: adapted_process M F 0 "-X" by (rule uminus_adapted) + interpret uminus_X: nat_sigma_finite_adapted_process_linorder M F "-X" .. + note * = set_integral_uminus[unfolded set_integrable_def, OF integrable_mult_indicator[OF _ integrable]] + have "nat_supermartingale M F (-(- X))" + using ord_eq_le_trans[OF * ord_le_eq_trans[OF le_imp_neg_le[OF assms(2)] *[symmetric]]] subalgebras + by (intro nat_supermartingale.intro submartingale.uminus nat_submartingale.axioms uminus_X.submartingale_of_set_integral_le_Suc) + (clarsimp simp add: fun_Compl_def subalgebra_def integrable | fastforce)+ + thus ?thesis unfolding fun_Compl_def by simp +qed + +lemma (in nat_sigma_finite_adapted_process_linorder) supermartingale_nat: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. X i \ \ cond_exp M (F i) (X (Suc i)) \" + shows "nat_supermartingale M F X" +proof - + interpret _: adapted_process M F 0 "-X" by (rule uminus_adapted) + interpret uminus_X: nat_sigma_finite_adapted_process_linorder M F "-X" .. + have "AE \ in M. - X i \ \ cond_exp M (F i) (\x. - X (Suc i) x) \" for i using assms(2) cond_exp_uminus[OF integrable, of i "Suc i"] by force + hence "nat_supermartingale M F (-(- X))" by (intro nat_supermartingale.intro submartingale.uminus nat_submartingale.axioms uminus_X.submartingale_nat) (auto simp add: fun_Compl_def integrable) + thus ?thesis unfolding fun_Compl_def by simp +qed + +lemma (in nat_sigma_finite_adapted_process_linorder) supermartingale_of_cond_exp_diff_Suc_le_zero: + assumes integrable: "\i. integrable M (X i)" + and "\i. AE \ in M. cond_exp M (F i) (\\. X (Suc i) \ - X i \) \ \ 0" + shows "nat_supermartingale M F X" +proof (intro supermartingale_nat integrable) + fix i + show "AE \ in M. X i \ \ cond_exp M (F i) (X (Suc i)) \" using cond_exp_diff[OF integrable(1,1), of i "Suc i" i] cond_exp_F_meas[OF integrable adapted, of i] assms(2)[of i] by fastforce +qed + +end \ No newline at end of file diff --git a/thys/Martingales/Measure_Space_Supplement.thy b/thys/Martingales/Measure_Space_Supplement.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Measure_Space_Supplement.thy @@ -0,0 +1,61 @@ +(* Author: Ata Keskin, TU München +*) + +theory Measure_Space_Supplement + imports "HOL-Analysis.Measure_Space" +begin + +section \Supplementary Lemmas for Measure Spaces\ + +subsection \\\\-Algebra Generated by a Family of Functions\ + +definition family_vimage_algebra :: "'a set \ ('a \ 'b) set \ 'b measure \ 'a measure" where + "family_vimage_algebra \ S M \ sigma \ (\f \ S. {f -` A \ \ | A. A \ M})" + +text \For singleton \<^term>\S\, i.e. \<^term>\S = {f}\ for some \<^term>\f\, the definition simplifies to that of \<^term>\vimage_algebra\.\ + +lemma family_vimage_algebra_singleton: "family_vimage_algebra \ {f} M = vimage_algebra \ f M" unfolding family_vimage_algebra_def vimage_algebra_def by simp + +lemma + shows sets_family_vimage_algebra: "sets (family_vimage_algebra \ S M) = sigma_sets \ (\f \ S. {f -` A \ \ | A. A \ M})" + and space_family_vimage_algebra[simp]: "space (family_vimage_algebra \ S M) = \" + by (auto simp add: family_vimage_algebra_def sets_measure_of_conv space_measure_of_conv) + +lemma measurable_family_vimage_algebra: + assumes "f \ S" "f \ \ \ space M" + shows "f \ family_vimage_algebra \ S M \\<^sub>M M" + using assms by (intro measurableI, auto simp add: sets_family_vimage_algebra) + +lemma measurable_family_vimage_algebra_singleton: + assumes "f \ \ \ space M" + shows "f \ family_vimage_algebra \ {f} M \\<^sub>M M" + using assms measurable_family_vimage_algebra by blast + +text \A collection of functions are measurable with respect to some \\\-algebra \<^term>\N\, if and only if the \\\-algebra they generate is contained in \<^term>\N\.\ +lemma measurable_family_iff_sets: + shows "(S \ N \\<^sub>M M) \ S \ space N \ space M \ family_vimage_algebra (space N) S M \ N" +proof (standard, goal_cases) + case 1 + hence subset: "S \ space N \ space M" using measurable_space by fast + have "{f -` A \ space N |A. A \ M} \ N" if "f \ S" for f using measurable_iff_sets[unfolded family_vimage_algebra_singleton[symmetric], of f] 1 subset that by (fastforce simp add: sets_family_vimage_algebra) + then show ?case unfolding sets_family_vimage_algebra using sets.sigma_algebra_axioms by (simp add: subset, intro sigma_algebra.sigma_sets_subset, blast+) +next + case 2 + hence subset: "S \ space N \ space M" by simp + show ?case + proof (standard, goal_cases) + case (1 x) + have "family_vimage_algebra (space N) {x} M \ N" by (metis (no_types, lifting) 1 2 sets_family_vimage_algebra SUP_le_iff sigma_sets_le_sets_iff singletonD) + thus ?case using measurable_iff_sets[unfolded family_vimage_algebra_singleton[symmetric]] subset[THEN subsetD, OF 1] by fast + qed +qed + +lemma family_vimage_algebra_diff: + shows "family_vimage_algebra \ S M = sigma \ (sets (family_vimage_algebra \ (S - I) M) \ family_vimage_algebra \ (S \ I) M)" + using sets.space_closed space_measure_of_conv + unfolding family_vimage_algebra_def sets_family_vimage_algebra + by (intro sigma_eqI, blast, fastforce) + (intro sigma_sets_eqI, blast, simp add: sets_measure_of_conv split: if_splits, + meson Diff_subset Sup_subset_mono in_mono inf_sup_ord(1) sigma_sets_subseteq subset_image_iff, fastforce+) + +end \ No newline at end of file diff --git a/thys/Martingales/ROOT b/thys/Martingales/ROOT new file mode 100755 --- /dev/null +++ b/thys/Martingales/ROOT @@ -0,0 +1,16 @@ +chapter AFP + +session "Martingales" (AFP) = "HOL-Probability" + + options [timeout = 1200] + theories + Measure_Space_Supplement + Elementary_Metric_Spaces_Supplement + Bochner_Integration_Supplement + Conditional_Expectation_Banach + Filtered_Measure + Stochastic_Process + Martingale + Example_Coin_Toss + document_files + "root.tex" + "root.bib" diff --git a/thys/Martingales/Stochastic_Process.thy b/thys/Martingales/Stochastic_Process.thy new file mode 100644 --- /dev/null +++ b/thys/Martingales/Stochastic_Process.thy @@ -0,0 +1,773 @@ +(* Author: Ata Keskin, TU München +*) + +theory Stochastic_Process +imports Filtered_Measure Measure_Space_Supplement "HOL-Probability.Independent_Family" +begin + +section \Stochastic Processes\ + +subsection \Stochastic Process\ + +text \A stochastic process is a collection of random variables, indexed by a type \<^typ>\'b\.\ + +locale stochastic_process = + fixes M t\<^sub>0 and X :: "'b :: {second_countable_topology, order_topology, t2_space} \ 'a \ 'c :: {second_countable_topology, banach}" + assumes random_variable[measurable]: "\i. t\<^sub>0 \ i \ X i \ borel_measurable M" +begin + +definition left_continuous where "left_continuous = (AE \ in M. \t. continuous (at_left t) (\i. X i \))" +definition right_continuous where "right_continuous = (AE \ in M. \t. continuous (at_right t) (\i. X i \))" + +end + +text \We specify the following locales to formalize discrete time and continuous time processes.\ + +locale nat_stochastic_process = stochastic_process M "0 :: nat" X for M X +locale real_stochastic_process = stochastic_process M "0 :: real" X for M X + +lemma stochastic_process_const_fun: + assumes "f \ borel_measurable M" + shows "stochastic_process M t\<^sub>0 (\_. f)" using assms by (unfold_locales) + +lemma stochastic_process_const: + shows "stochastic_process M t\<^sub>0 (\i _. c i)" by (unfold_locales) simp + +text \In the following segment, we cover basic operations on stochastic processes.\ + +context stochastic_process +begin + +lemma compose_stochastic: + assumes "\i. t\<^sub>0 \ i \ f i \ borel_measurable borel" + shows "stochastic_process M t\<^sub>0 (\i \. (f i) (X i \))" + by (unfold_locales) (intro measurable_compose[OF random_variable assms]) + +lemma norm_stochastic: "stochastic_process M t\<^sub>0 (\i \. norm (X i \))" by (fastforce intro: compose_stochastic) + +lemma scaleR_right_stochastic: + assumes "stochastic_process M t\<^sub>0 Y" + shows "stochastic_process M t\<^sub>0 (\i \. (Y i \) *\<^sub>R (X i \))" + using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp + +lemma scaleR_right_const_fun_stochastic: + assumes "f \ borel_measurable M" + shows "stochastic_process M t\<^sub>0 (\i \. f \ *\<^sub>R (X i \))" + by (unfold_locales) (intro borel_measurable_scaleR assms random_variable) + +lemma scaleR_right_const_stochastic: "stochastic_process M t\<^sub>0 (\i \. c i *\<^sub>R (X i \))" + by (unfold_locales) simp + +lemma add_stochastic: + assumes "stochastic_process M t\<^sub>0 Y" + shows "stochastic_process M t\<^sub>0 (\i \. X i \ + Y i \)" + using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp + +lemma diff_stochastic: + assumes "stochastic_process M t\<^sub>0 Y" + shows "stochastic_process M t\<^sub>0 (\i \. X i \ - Y i \)" + using stochastic_process.random_variable[OF assms] random_variable by (unfold_locales) simp + +lemma uminus_stochastic: "stochastic_process M t\<^sub>0 (-X)" using scaleR_right_const_stochastic[of "\_. -1"] by (simp add: fun_Compl_def) + +lemma partial_sum_stochastic: "stochastic_process M t\<^sub>0 (\n \. \i\{t\<^sub>0..n}. X i \)" by (unfold_locales) simp + +lemma partial_sum'_stochastic: "stochastic_process M t\<^sub>0 (\n \. \i\{t\<^sub>0..)" by (unfold_locales) simp + +end + +lemma stochastic_process_sum: + assumes "\i. i \ I \ stochastic_process M t\<^sub>0 (X i)" + shows "stochastic_process M t\<^sub>0 (\k \. \i \ I. X i k \)" using assms[THEN stochastic_process.random_variable] by (unfold_locales, auto) + +subsubsection \Natural Filtration\ + +text \The natural filtration induced by a stochastic process \<^term>\X\ is the filtration generated by all events involving the process up to the time index \<^term>\t\, i.e. \F t = \({X s | s. s \ t})\.\ + +definition natural_filtration :: "'a measure \ 'b \ ('b \ 'a \ 'c :: topological_space) \ 'b :: {second_countable_topology, order_topology} \ 'a measure" where + "natural_filtration M t\<^sub>0 Y = (\t. family_vimage_algebra (space M) {Y i | i. i \ {t\<^sub>0..t}} borel)" + +abbreviation "nat_natural_filtration \ \M. natural_filtration M (0 :: nat)" +abbreviation "real_natural_filtration \ \M. natural_filtration M (0 :: real)" + +lemma space_natural_filtration[simp]: "space (natural_filtration M t\<^sub>0 X t) = space M" unfolding natural_filtration_def space_family_vimage_algebra .. + +lemma sets_natural_filtration: "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A. A \ borel})" + unfolding natural_filtration_def sets_family_vimage_algebra by (intro sigma_sets_eqI) blast+ + +lemma sets_natural_filtration': + assumes "borel = sigma UNIV S" + shows "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A. A \ S})" +proof (subst sets_natural_filtration, intro sigma_sets_eqI, clarify) + fix i and A :: "'a set" assume asm: "i \ {t\<^sub>0..t}" "A \ sets borel" + hence "A \ sigma_sets UNIV S" unfolding assms by simp + thus "X i -` A \ space M \ sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M |A. A \ S})" + proof (induction) + case (Compl a) + have "X i -` (UNIV - a) \ space M = space M - (X i -` a \ space M)" by blast + then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger + next + case (Union a) + have "X i -` \ (range a) \ space M = \ (range (\j. X i -` a j \ space M))" by blast + then show ?case using Union(2)[THEN sigma_sets.Union] by presburger + qed (auto intro: asm sigma_sets.Empty) +qed (intro sigma_sets.Basic, force simp add: assms) + +lemma sets_natural_filtration_open: + "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A. open A})" + using sets_natural_filtration' by (force simp only: borel_def mem_Collect_eq) + +lemma sets_natural_filtration_oi: + "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A :: _ :: {linorder_topology, second_countable_topology} set. A \ range greaterThan})" + by (rule sets_natural_filtration'[OF borel_Ioi]) + +lemma sets_natural_filtration_io: + "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A :: _ :: {linorder_topology, second_countable_topology} set. A \ range lessThan})" + by (rule sets_natural_filtration'[OF borel_Iio]) + +lemma sets_natural_filtration_ci: + "sets (natural_filtration M t\<^sub>0 X t) = sigma_sets (space M) (\i\{t\<^sub>0..t}. {X i -` A \ space M | A :: real set. A \ range atLeast})" + by (rule sets_natural_filtration'[OF borel_Ici]) + +context stochastic_process +begin + +lemma subalgebra_natural_filtration: + shows "subalgebra M (natural_filtration M t\<^sub>0 X i)" + unfolding subalgebra_def using measurable_family_iff_sets by (force simp add: natural_filtration_def) + +lemma filtered_measure_natural_filtration: + shows "filtered_measure M (natural_filtration M t\<^sub>0 X) t\<^sub>0" + by (unfold_locales) (intro subalgebra_natural_filtration, simp only: sets_natural_filtration, intro sigma_sets_subseteq, force) + +text \In order to show that the natural filtration constitutes a filtered \\\-finite measure, we need to provide a countable exhausting set in the preimage of \<^term>\X t\<^sub>0\.\ + +lemma sigma_finite_filtered_measure_natural_filtration: + assumes exhausting_set: "countable A" "(\A) = space M" "\a. a \ A \ emeasure M a \ \" "\a. a \ A \ \b \ borel. a = X t\<^sub>0 -` b \ space M" + shows "sigma_finite_filtered_measure M (natural_filtration M t\<^sub>0 X) t\<^sub>0" +proof (unfold_locales) + have "A \ sets (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0))" using exhausting_set by (simp add: sets_restr_to_subalg[OF subalgebra_natural_filtration] sets_natural_filtration) fast + moreover have "\ A = space (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0))" unfolding space_restr_to_subalg using exhausting_set by simp + moreover have "\a\A. emeasure (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0)) a \ \" using calculation(1) exhausting_set(3) + by (auto simp add: sets_restr_to_subalg[OF subalgebra_natural_filtration] emeasure_restr_to_subalg[OF subalgebra_natural_filtration]) + ultimately show "\A. countable A \ A \ sets (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0)) \ \ A = space (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0)) \ (\a\A. emeasure (restr_to_subalg M (natural_filtration M t\<^sub>0 X t\<^sub>0)) a \ \)" using exhausting_set by blast + show "\i j. \t\<^sub>0 \ i; i \ j\ \ sets (natural_filtration M t\<^sub>0 X i) \ sets (natural_filtration M t\<^sub>0 X j)" using filtered_measure.subalgebra_F[OF filtered_measure_natural_filtration] by (simp add: subalgebra_def) +qed (auto intro: subalgebra_natural_filtration) + +lemma finite_filtered_measure_natural_filtration: + assumes "finite_measure M" + shows "finite_filtered_measure M (natural_filtration M t\<^sub>0 X) t\<^sub>0" + using finite_measure.axioms[OF assms] filtered_measure_natural_filtration by intro_locales + +end + +text \Filtration generated by independent variables.\ + +lemma (in prob_space) indep_set_natural_filtration: + assumes "t\<^sub>0 \ s" "s < t" "indep_vars (\_. borel) X {t\<^sub>0..}" + shows "indep_set (natural_filtration M t\<^sub>0 X s) (vimage_algebra (space M) (X t) borel)" +proof - + have "indep_sets (\i. {X i -` A \ space M |A. A \ sets borel}) (\(range (case_bool {t\<^sub>0..s} {t})))" + using assms + by (intro assms(3)[unfolded indep_vars_def, THEN conjunct2, THEN indep_sets_mono]) (auto simp add: case_bool_if) + thus ?thesis unfolding indep_set_def using assms + by (intro indep_sets_cong[THEN iffD1, OF refl _ indep_sets_collect_sigma[of "\i. {X i -` A \ space M | A. A \ borel}" "case_bool {t\<^sub>0..s} {t}"]]) + (simp add: sets_natural_filtration sets_vimage_algebra split: bool.split, simp, intro Int_stableI, clarsimp, metis sets.Int vimage_Int Int_commute Int_left_absorb Int_left_commute, force simp add: disjoint_family_on_def split: bool.split) +qed + +subsection \Adapted Process\ + +text \We call a collection a stochastic process \<^term>\X\ adapted if \<^term>\X i\ is \<^term>\F i\-borel-measurable for all indices \<^term>\i :: 't\.\ + +locale adapted_process = filtered_measure M F t\<^sub>0 for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {second_countable_topology, banach}" + + assumes adapted[measurable]: "\i. t\<^sub>0 \ i \ X i \ borel_measurable (F i)" +begin + +lemma adaptedE[elim]: + assumes "\\j i. t\<^sub>0 \ j \ j \ i \ X j \ borel_measurable (F i)\ \ P" + shows P + using assms using adapted by (metis dual_order.trans borel_measurable_subalgebra sets_F_mono space_F) + +lemma adaptedD: + assumes "t\<^sub>0 \ j" "j \ i" + shows "X j \ borel_measurable (F i)" using assms adaptedE by meson + +end + +locale nat_adapted_process = adapted_process M F "0 :: nat" X for M F X +locale real_adapted_process = adapted_process M F "0 :: real" X for M F X + +sublocale nat_adapted_process \ nat_filtered_measure .. +sublocale real_adapted_process \ real_filtered_measure .. + +lemma (in filtered_measure) adapted_process_const_fun: + assumes "f \ borel_measurable (F t\<^sub>0)" + shows "adapted_process M F t\<^sub>0 (\_. f)" + using measurable_from_subalg subalgebra_F assms by (unfold_locales) blast + +lemma (in filtered_measure) adapted_process_const: + shows "adapted_process M F t\<^sub>0 (\i _. c i)" by (unfold_locales) simp + + +text \Again, we cover basic operations.\ + +context adapted_process +begin + +lemma compose_adapted: + assumes "\i. t\<^sub>0 \ i \ f i \ borel_measurable borel" + shows "adapted_process M F t\<^sub>0 (\i \. (f i) (X i \))" + by (unfold_locales) (intro measurable_compose[OF adapted assms]) + +lemma norm_adapted: "adapted_process M F t\<^sub>0 (\i \. norm (X i \))" by (fastforce intro: compose_adapted) + +lemma scaleR_right_adapted: + assumes "adapted_process M F t\<^sub>0 R" + shows "adapted_process M F t\<^sub>0 (\i \. (R i \) *\<^sub>R (X i \))" + using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp + +lemma scaleR_right_const_fun_adapted: + assumes "f \ borel_measurable (F t\<^sub>0)" + shows "adapted_process M F t\<^sub>0 (\i \. f \ *\<^sub>R (X i \))" + using assms by (fast intro: scaleR_right_adapted adapted_process_const_fun) + +lemma scaleR_right_const_adapted: "adapted_process M F t\<^sub>0 (\i \. c i *\<^sub>R (X i \))" by (unfold_locales) simp + +lemma add_adapted: + assumes "adapted_process M F t\<^sub>0 Y" + shows "adapted_process M F t\<^sub>0 (\i \. X i \ + Y i \)" + using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp + +lemma diff_adapted: + assumes "adapted_process M F t\<^sub>0 Y" + shows "adapted_process M F t\<^sub>0 (\i \. X i \ - Y i \)" + using adapted_process.adapted[OF assms] adapted by (unfold_locales) simp + +lemma uminus_adapted: "adapted_process M F t\<^sub>0 (-X)" using scaleR_right_const_adapted[of "\_. -1"] by (simp add: fun_Compl_def) + +lemma partial_sum_adapted: "adapted_process M F t\<^sub>0 (\n \. \i\{t\<^sub>0..n}. X i \)" +proof (unfold_locales) + fix i :: 'b + have "X j \ borel_measurable (F i)" if "t\<^sub>0 \ j" "j \ i" for j using that adaptedE by meson + thus "(\\. \i\{t\<^sub>0..i}. X i \) \ borel_measurable (F i)" by simp +qed + +lemma partial_sum'_adapted: "adapted_process M F t\<^sub>0 (\n \. \i\{t\<^sub>0..)" +proof (unfold_locales) + fix i :: 'b + have "X j \ borel_measurable (F i)" if "t\<^sub>0 \ j" "j < i" for j using that adaptedE by fastforce + thus "(\\. \i\{t\<^sub>0..) \ borel_measurable (F i)" by simp +qed + +end + +text \In the dicrete time case, we have the following lemma which will be useful later on.\ + +lemma (in nat_adapted_process) partial_sum_Suc_adapted: "nat_adapted_process M F (\n \. \i)" +proof (unfold_locales) + fix i + have "X j \ borel_measurable (F i)" if "j \ i" for j using that adaptedD by blast + thus "(\\. \i) \ borel_measurable (F i)" by auto +qed + +lemma (in filtered_measure) adapted_process_sum: + assumes "\i. i \ I \ adapted_process M F t\<^sub>0 (X i)" + shows "adapted_process M F t\<^sub>0 (\k \. \i \ I. X i k \)" +proof - + { + fix i k assume "i \ I" and asm: "t\<^sub>0 \ k" + then interpret adapted_process M F t\<^sub>0 "X i" using assms by simp + have "X i k \ borel_measurable M" "X i k \ borel_measurable (F k)" using measurable_from_subalg subalgebras adapted asm by (blast, simp) + } + thus ?thesis by (unfold_locales) simp +qed + +text \An adapted process is necessarily a stochastic process.\ + +sublocale adapted_process \ stochastic_process using measurable_from_subalg subalgebras adapted by (unfold_locales) blast + +sublocale nat_adapted_process \ nat_stochastic_process .. +sublocale real_adapted_process \ real_stochastic_process .. + +text \A stochastic process is always adapted to the natural filtration it generates.\ + +lemma (in stochastic_process) adapted_process_natural_filtration: "adapted_process M (natural_filtration M t\<^sub>0 X) t\<^sub>0 X" + using filtered_measure_natural_filtration + by (intro_locales) (auto simp add: natural_filtration_def intro!: adapted_process_axioms.intro measurable_family_vimage_algebra) + +subsection \Progressively Measurable Process\ + +locale progressive_process = filtered_measure M F t\<^sub>0 for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {second_countable_topology, banach}" + + assumes progressive[measurable]: "\t. t\<^sub>0 \ t \ (\(i, x). X i x) \ borel_measurable (restrict_space borel {t\<^sub>0..t} \\<^sub>M F t)" +begin + +lemma progressiveD: + assumes "S \ borel" + shows "(\(j, \). X j \) -` S \ ({t\<^sub>0..i} \ space M) \ (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i)" + using measurable_sets[OF progressive, OF _ assms, of i] + by (cases "t\<^sub>0 \ i") (auto simp add: space_restrict_space sets_pair_measure space_pair_measure) + +end + +locale nat_progressive_process = progressive_process M F "0 :: nat" X for M F X +locale real_progressive_process = progressive_process M F "0 :: real" X for M F X + +lemma (in filtered_measure) progressive_process_const_fun: + assumes "f \ borel_measurable (F t\<^sub>0)" + shows "progressive_process M F t\<^sub>0 (\_. f)" +proof (unfold_locales) + fix i assume asm: "t\<^sub>0 \ i" + have "f \ borel_measurable (F i)" using borel_measurable_mono[OF order.refl asm] assms by blast + thus "case_prod (\_. f) \ borel_measurable (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i)" using measurable_compose[OF measurable_snd] by simp +qed + +lemma (in filtered_measure) progressive_process_const: + assumes "c \ borel_measurable borel" + shows "progressive_process M F t\<^sub>0 (\i _. c i)" + using assms by (unfold_locales) (auto simp add: measurable_split_conv intro!: measurable_compose[OF measurable_fst] measurable_restrict_space1) + +context progressive_process +begin + +lemma compose_progressive: + assumes "case_prod f \ borel_measurable borel" + shows "progressive_process M F t\<^sub>0 (\i \. (f i) (X i \))" +proof + fix i assume asm: "t\<^sub>0 \ i" + have "(\(j, \). (j, X j \)) \ (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i) \\<^sub>M borel \\<^sub>M borel" + using progressive[OF asm] measurable_fst''[OF measurable_restrict_space1, OF measurable_id] + by (auto simp add: measurable_pair_iff measurable_split_conv) + moreover have "(\(j, \). f j (X j \)) = case_prod f o ((\(j, y). (j, y)) o (\(j, \). (j, X j \)))" by fastforce + ultimately show "(\(j, \). (f j) (X j \)) \ borel_measurable (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i)" using assms by (simp add: borel_prod) +qed + +lemma norm_progressive: "progressive_process M F t\<^sub>0 (\i \. norm (X i \))" using measurable_compose[OF progressive borel_measurable_norm] by (unfold_locales) simp + +lemma scaleR_right_progressive: + assumes "progressive_process M F t\<^sub>0 R" + shows "progressive_process M F t\<^sub>0 (\i \. (R i \) *\<^sub>R (X i \))" + using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms) + +lemma scaleR_right_const_fun_progressive: + assumes "f \ borel_measurable (F t\<^sub>0)" + shows "progressive_process M F t\<^sub>0 (\i \. f \ *\<^sub>R (X i \))" + using assms by (fast intro: scaleR_right_progressive progressive_process_const_fun) + +lemma scaleR_right_const_progressive: + assumes "c \ borel_measurable borel" + shows "progressive_process M F t\<^sub>0 (\i \. c i *\<^sub>R (X i \))" + using assms by (fastforce intro: scaleR_right_progressive progressive_process_const) + +lemma add_progressive: + assumes "progressive_process M F t\<^sub>0 Y" + shows "progressive_process M F t\<^sub>0 (\i \. X i \ + Y i \)" + using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms) + +lemma diff_progressive: + assumes "progressive_process M F t\<^sub>0 Y" + shows "progressive_process M F t\<^sub>0 (\i \. X i \ - Y i \)" + using progressive_process.progressive[OF assms] by (unfold_locales) (simp add: progressive assms) + +lemma uminus_progressive: "progressive_process M F t\<^sub>0 (-X)" using scaleR_right_const_progressive[of "\_. -1"] by (simp add: fun_Compl_def) + +end + +text \A progressively measurable process is also adapted.\ + +sublocale progressive_process \ adapted_process using measurable_compose_rev[OF progressive measurable_Pair1'] + unfolding prod.case space_restrict_space + by unfold_locales simp + +sublocale nat_progressive_process \ nat_adapted_process .. +sublocale real_progressive_process \ real_adapted_process .. + +text \In the discrete setting, adaptedness is equivalent to progressive measurability.\ + +theorem nat_progressive_iff_adapted: "nat_progressive_process M F X \ nat_adapted_process M F X" +proof (intro iffI) + assume asm: "nat_progressive_process M F X" + interpret nat_progressive_process M F X by (rule asm) + show "nat_adapted_process M F X" .. +next + assume asm: "nat_adapted_process M F X" + interpret nat_adapted_process M F X by (rule asm) + show "nat_progressive_process M F X" + proof (unfold_locales, intro borel_measurableI) + fix S :: "'b set" and i :: nat assume open_S: "open S" + { + fix j assume asm: "j \ i" + hence "X j -` S \ space M \ F i" using adaptedD[of j, THEN measurable_sets] space_F open_S by fastforce + moreover have "case_prod X -` S \ {j} \ space M = {j} \ (X j -` S \ space M)" for j by fast + moreover have "{j :: nat} \ restrict_space borel {0..i}" using asm by (simp add: sets_restrict_space_iff) + ultimately have "case_prod X -` S \ {j} \ space M \ restrict_space borel {0..i} \\<^sub>M F i" by simp + } + hence "(\j. (\(x, y). X x y) -` S \ {j} \ space M) ` {..i} \ restrict_space borel {0..i} \\<^sub>M F i" by blast + moreover have "case_prod X -` S \ space (restrict_space borel {0..i} \\<^sub>M F i) = (\j\i. case_prod X -` S \ {j} \ space M)" unfolding space_pair_measure space_restrict_space space_F by force + ultimately show "case_prod X -` S \ space (restrict_space borel {0..i} \\<^sub>M F i) \ restrict_space borel {0..i} \\<^sub>M F i" by (metis sets.countable_UN) + qed +qed + +subsection \Predictable Process\ + +text \We introduce the constant \<^term>\\\<^sub>P\ to denote the predictable \\\-algebra.\ + +context linearly_filtered_measure +begin + +definition \\<^sub>P :: "('b \ 'a) measure" where predictable_sigma: "\\<^sub>P \ sigma ({t\<^sub>0..} \ space M) ({{s<..t} \ A | A s t. A \ F s \ t\<^sub>0 \ s \ s < t} \ {{t\<^sub>0} \ A | A. A \ F t\<^sub>0})" + +lemma space_predictable_sigma[simp]: "space \\<^sub>P = ({t\<^sub>0..} \ space M)" unfolding predictable_sigma space_measure_of_conv by blast + +lemma sets_predictable_sigma: "sets \\<^sub>P = sigma_sets ({t\<^sub>0..} \ space M) ({{s<..t} \ A | A s t. A \ F s \ t\<^sub>0 \ s \ s < t} \ {{t\<^sub>0} \ A | A. A \ F t\<^sub>0})" + unfolding predictable_sigma using space_F sets.sets_into_space by (subst sets_measure_of) fastforce+ + +lemma measurable_predictable_sigma_snd: + assumes "countable \" "\ \ {{s<..t} | s t. t\<^sub>0 \ s \ s < t}" "{t\<^sub>0<..} \ (\\)" + shows "snd \ \\<^sub>P \\<^sub>M F t\<^sub>0" +proof (intro measurableI) + fix S :: "'a set" assume asm: "S \ F t\<^sub>0" + have countable: "countable ((\I. I \ S) ` \)" using assms(1) by blast + have "(\I. I \ S) ` \ \ {{s<..t} \ A | A s t. A \ F s \ t\<^sub>0 \ s \ s < t}" using sets_F_mono[OF order_refl, THEN subsetD, OF _ asm] assms(2) by blast + hence "(\I\\. I \ S) \ {t\<^sub>0} \ S \ \\<^sub>P" unfolding sets_predictable_sigma using asm by (intro sigma_sets_Un[OF sigma_sets_UNION[OF countable] sigma_sets.Basic] sigma_sets.Basic) blast+ + moreover have "snd -` S \ space \\<^sub>P = {t\<^sub>0..} \ S" using sets.sets_into_space[OF asm] by fastforce + moreover have "{t\<^sub>0} \ {t\<^sub>0<..} = {t\<^sub>0..}" by auto + moreover have "(\I\\. I \ S) \ {t\<^sub>0} \ S = {t\<^sub>0..} \ S" using assms(2,3) calculation(3) by fastforce + ultimately show "snd -` S \ space \\<^sub>P \ \\<^sub>P" by argo +qed (auto) + +lemma measurable_predictable_sigma_fst: + assumes "countable \" "\ \ {{s<..t} | s t. t\<^sub>0 \ s \ s < t}" "{t\<^sub>0<..} \ (\\)" + shows "fst \ \\<^sub>P \\<^sub>M borel" +proof - + have "A \ space M \ sets \\<^sub>P" if "A \ sigma_sets {t\<^sub>0..} {{s<..t} | s t. t\<^sub>0 \ s \ s < t}" for A unfolding sets_predictable_sigma using that + proof (induction rule: sigma_sets.induct) + case (Basic a) + thus ?case using space_F sets.top by blast + next + case (Compl a) + have "({t\<^sub>0..} - a) \ space M = {t\<^sub>0..} \ space M - a \ space M" by blast + then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger + next + case (Union a) + have "\ (range a) \ space M = \ (range (\i. a i \ space M))" by blast + then show ?case using Union(2)[THEN sigma_sets.Union] by presburger + qed (auto) + moreover have "restrict_space borel {t\<^sub>0..} = sigma {t\<^sub>0..} {{s<..t} | s t. t\<^sub>0 \ s \ s < t}" + proof - + have "sigma_sets {t\<^sub>0..} ((\) {t\<^sub>0..} ` sigma_sets UNIV (range greaterThan)) = sigma_sets {t\<^sub>0..} {{s<..t} |s t. t\<^sub>0 \ s \ s < t}" + proof (intro sigma_sets_eqI ; clarify) + fix A :: "'b set" assume asm: "A \ sigma_sets UNIV (range greaterThan)" + thus "{t\<^sub>0..} \ A \ sigma_sets {t\<^sub>0..} {{s<..t} |s t. t\<^sub>0 \ s \ s < t}" + proof (induction rule: sigma_sets.induct) + case (Basic a) + then obtain s where s: "a = {s<..}" by blast + show ?case + proof (cases "t\<^sub>0 \ s") + case True + hence *: "{t\<^sub>0..} \ a = (\i \ \. {s<..} \ i)" using s assms(3) by force + have "((\) {s<..} ` \) \ sigma_sets {t\<^sub>0..} {{s<..t} | s t. t\<^sub>0 \ s \ s < t}" + proof (clarify) + fix A assume "A \ \" + then obtain s' t' where A: "A = {s'<..t'}" "t\<^sub>0 \ s'" "s' < t'" using assms(2) by blast + hence "{s<..} \ A = {max s s'<..t'}" by fastforce + moreover have "t\<^sub>0 \ max s s'" using A True by linarith + moreover have "max s s' < t'" if "s < t'" using A that by linarith + moreover have "{s<..} \ A = {}" if "\ s < t'" using A that by force + ultimately show "{s<..} \ A \ sigma_sets {t\<^sub>0..} {{s<..t} |s t. t\<^sub>0 \ s \ s < t}" by (cases "s < t'") (blast, simp add: sigma_sets.Empty) + qed + thus ?thesis unfolding * using assms(1) by (intro sigma_sets_UNION) auto + next + case False + hence "{t\<^sub>0..} \ a = {t\<^sub>0..}" using s by force + thus ?thesis using sigma_sets_top by auto + qed + next + case (Compl a) + have "{t\<^sub>0..} \ (UNIV - a) = {t\<^sub>0..} - ({t\<^sub>0..} \ a)" by blast + then show ?case using Compl(2)[THEN sigma_sets.Compl] by presburger + next + case (Union a) + have "{t\<^sub>0..} \ \ (range a) = \ (range (\i. {t\<^sub>0..} \ a i))" by blast + then show ?case using Union(2)[THEN sigma_sets.Union] by presburger + qed (simp add: sigma_sets.Empty) + next + fix s t assume asm: "t\<^sub>0 \ s" "s < t" + hence *: "{s<..t} = {s<..} \ ({t\<^sub>0..} - {t<..})" by force + have "{s<..} \ sigma_sets {t\<^sub>0..} ((\) {t\<^sub>0..} ` sigma_sets UNIV (range greaterThan))" using asm by (intro sigma_sets.Basic) auto + moreover have "{t\<^sub>0..} - {t<..} \ sigma_sets {t\<^sub>0..} ((\) {t\<^sub>0..} ` sigma_sets UNIV (range greaterThan))" using asm by (intro sigma_sets.Compl sigma_sets.Basic) auto + ultimately show "{s<..t} \ sigma_sets {t\<^sub>0..} ((\) {t\<^sub>0..} ` sigma_sets UNIV (range greaterThan))" unfolding * Int_range_binary[of "{s<..}"] by (intro sigma_sets_Inter[OF _ binary_in_sigma_sets]) auto + qed + thus ?thesis unfolding borel_Ioi restrict_space_def emeasure_sigma by (force intro: sigma_eqI) + qed + ultimately have "restrict_space borel {t\<^sub>0..} \\<^sub>M sigma (space M) {} \ sets \\<^sub>P" + unfolding sets_pair_measure space_restrict_space space_measure_of_conv + using space_predictable_sigma sets.sigma_algebra_axioms[of \\<^sub>P] + by (intro sigma_algebra.sigma_sets_subset) (auto simp add: sigma_sets_empty_eq sets_measure_of_conv) + moreover have "space (restrict_space borel {t\<^sub>0..} \\<^sub>M sigma (space M) {}) = space \\<^sub>P" by (simp add: space_pair_measure) + moreover have "fst \ restrict_space borel {t\<^sub>0..} \\<^sub>M sigma (space M) {} \\<^sub>M borel" by (fastforce intro: measurable_fst''[OF measurable_restrict_space1, of "\x. x"]) + ultimately show ?thesis by (meson borel_measurable_subalgebra) +qed + +end + +locale predictable_process = linearly_filtered_measure M F t\<^sub>0 for M F t\<^sub>0 and X :: "_ \ _ \ _ :: {second_countable_topology, banach}" + + assumes predictable: "(\(t, x). X t x) \ borel_measurable \\<^sub>P" +begin + +lemmas predictableD = measurable_sets[OF predictable, unfolded space_predictable_sigma] + +end + +(* * *) + +locale nat_predictable_process = predictable_process M F "0 :: nat" X for M F X +locale real_predictable_process = predictable_process M F "0 :: real" X for M F X + +lemma (in nat_filtered_measure) measurable_predictable_sigma_snd': + shows "snd \ \\<^sub>P \\<^sub>M F 0" + by (intro measurable_predictable_sigma_snd[of "range (\x. {Suc x})"]) (force | simp add: greaterThan_0)+ + +lemma (in nat_filtered_measure) measurable_predictable_sigma_fst': + shows "fst \ \\<^sub>P \\<^sub>M borel" + by (intro measurable_predictable_sigma_fst[of "range (\x. {Suc x})"]) (force | simp add: greaterThan_0)+ + +lemma (in real_filtered_measure) measurable_predictable_sigma_snd': + shows "snd \ \\<^sub>P \\<^sub>M F 0" + using real_arch_simple by (intro measurable_predictable_sigma_snd[of "range (\x::nat. {0<..real (Suc x)})"]) (fastforce intro: add_increasing)+ + +lemma (in real_filtered_measure) measurable_predictable_sigma_fst': + shows "fst \ \\<^sub>P \\<^sub>M borel" + using real_arch_simple by (intro measurable_predictable_sigma_fst[of "range (\x::nat. {0<..real (Suc x)})"]) (fastforce intro: add_increasing)+ + +text \We show sufficient conditions for functions constant in one argument to constitute a predictable process. In contrast to the cases before, this is not a triviality.\ + +lemma (in linearly_filtered_measure) predictable_process_const_fun: + assumes "snd \ \\<^sub>P \\<^sub>M F t\<^sub>0" "f \ borel_measurable (F t\<^sub>0)" + shows "predictable_process M F t\<^sub>0 (\_. f)" + using measurable_compose_rev[OF assms(2)] assms(1) by (unfold_locales) (auto simp add: measurable_split_conv) + +lemma (in nat_filtered_measure) predictable_process_const_fun'[intro]: + assumes "f \ borel_measurable (F 0)" + shows "nat_predictable_process M F (\_. f)" + using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd', THEN nat_predictable_process.intro]) + +lemma (in real_filtered_measure) predictable_process_const_fun'[intro]: + assumes "f \ borel_measurable (F 0)" + shows "real_predictable_process M F (\_. f)" + using assms by (intro predictable_process_const_fun[OF measurable_predictable_sigma_snd', THEN real_predictable_process.intro]) + +lemma (in linearly_filtered_measure) predictable_process_const: + assumes "fst \ borel_measurable \\<^sub>P" "c \ borel_measurable borel" + shows "predictable_process M F t\<^sub>0 (\i _. c i)" + using assms by (unfold_locales) (simp add: measurable_split_conv) + +lemma (in linearly_filtered_measure) predictable_process_const_const[intro]: + shows "predictable_process M F t\<^sub>0 (\_ _. c)" + by (unfold_locales) simp + +lemma (in nat_filtered_measure) predictable_process_const'[intro]: + assumes "c \ borel_measurable borel" + shows "nat_predictable_process M F (\i _. c i)" + using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst', THEN nat_predictable_process.intro]) + +lemma (in real_filtered_measure) predictable_process_const'[intro]: + assumes "c \ borel_measurable borel" + shows "real_predictable_process M F (\i _. c i)" + using assms by (intro predictable_process_const[OF measurable_predictable_sigma_fst', THEN real_predictable_process.intro]) + +context predictable_process +begin + +lemma compose_predictable: + assumes "fst \ borel_measurable \\<^sub>P" "case_prod f \ borel_measurable borel" + shows "predictable_process M F t\<^sub>0 (\i \. (f i) (X i \))" +proof + have "(\(i, \). (i, X i \)) \ \\<^sub>P \\<^sub>M borel \\<^sub>M borel" using predictable assms(1) by (auto simp add: measurable_pair_iff measurable_split_conv) + moreover have "(\(i, \). f i (X i \)) = case_prod f o (\(i, \). (i, X i \))" by fastforce + ultimately show "(\(i, \). f i (X i \)) \ borel_measurable \\<^sub>P" unfolding borel_prod using assms by simp +qed + +lemma norm_predictable: "predictable_process M F t\<^sub>0 (\i \. norm (X i \))" using measurable_compose[OF predictable borel_measurable_norm] + by (unfold_locales) (simp add: prod.case_distrib) + +lemma scaleR_right_predictable: + assumes "predictable_process M F t\<^sub>0 R" + shows "predictable_process M F t\<^sub>0 (\i \. (R i \) *\<^sub>R (X i \))" + using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv) + +lemma scaleR_right_const_fun_predictable: + assumes "snd \ \\<^sub>P \\<^sub>M F t\<^sub>0" "f \ borel_measurable (F t\<^sub>0)" + shows "predictable_process M F t\<^sub>0 (\i \. f \ *\<^sub>R (X i \))" + using assms by (fast intro: scaleR_right_predictable predictable_process_const_fun) + +lemma scaleR_right_const_predictable: + assumes "fst \ borel_measurable \\<^sub>P" "c \ borel_measurable borel" + shows "predictable_process M F t\<^sub>0 (\i \. c i *\<^sub>R (X i \))" + using assms by (fastforce intro: scaleR_right_predictable predictable_process_const) + +lemma scaleR_right_const'_predictable: "predictable_process M F t\<^sub>0 (\i \. c *\<^sub>R (X i \))" + by (fastforce intro: scaleR_right_predictable) + +lemma add_predictable: + assumes "predictable_process M F t\<^sub>0 Y" + shows "predictable_process M F t\<^sub>0 (\i \. X i \ + Y i \)" + using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv) + +lemma diff_predictable: + assumes "predictable_process M F t\<^sub>0 Y" + shows "predictable_process M F t\<^sub>0 (\i \. X i \ - Y i \)" + using predictable predictable_process.predictable[OF assms] by (unfold_locales) (auto simp add: measurable_split_conv) + +lemma uminus_predictable: "predictable_process M F t\<^sub>0 (-X)" using scaleR_right_const'_predictable[of "-1"] by (simp add: fun_Compl_def) + +end + +text \Every predictable process is also progressively measurable.\ + +sublocale predictable_process \ progressive_process +proof (unfold_locales) + fix i :: 'b assume asm: "t\<^sub>0 \ i" + { + fix S :: "('b \ 'a) set" assume "S \ {{s<..t} \ A | A s t. A \ F s \ t\<^sub>0 \ s \ s < t} \ {{t\<^sub>0} \ A | A. A \ F t\<^sub>0}" + hence "(\x. x) -` S \ ({t\<^sub>0..i} \ space M) \ restrict_space borel {t\<^sub>0..i} \\<^sub>M F i" + proof + assume "S \ {{s<..t} \ A | A s t. A \ F s \ t\<^sub>0 \ s \ s < t}" + then obtain s t A where S_is: "S = {s<..t} \ A" "t\<^sub>0 \ s" "s < t" "A \ F s" by blast + hence "(\x. x) -` S \ ({t\<^sub>0..i} \ space M) = {s<..min i t} \ A" using sets.sets_into_space[OF S_is(4)] by auto + then show ?thesis using S_is sets_F_mono[of s i] by (cases "s \ i") (fastforce simp add: sets_restrict_space_iff)+ + next + assume "S \ {{t\<^sub>0} \ A | A. A \ F t\<^sub>0}" + then obtain A where S_is: "S = {t\<^sub>0} \ A" "A \ F t\<^sub>0" by blast + hence "(\x. x) -` S \ ({t\<^sub>0..i} \ space M) = {t\<^sub>0} \ A" using asm sets.sets_into_space[OF S_is(2)] by auto + thus ?thesis using S_is(2) sets_F_mono[OF order_refl asm] asm by (fastforce simp add: sets_restrict_space_iff) + qed + hence "(\x. x) -` S \ space (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i) \ restrict_space borel {t\<^sub>0..i} \\<^sub>M F i" by (simp add: space_pair_measure space_F[OF asm]) + } + moreover have "{{s<..t} \ A |A s t. A \ sets (F s) \ t\<^sub>0 \ s \ s < t} \ {{t\<^sub>0} \ A |A. A \ sets (F t\<^sub>0)} \ Pow ({t\<^sub>0..} \ space M)" using sets.sets_into_space by force + ultimately have "(\x. x) \ restrict_space borel {t\<^sub>0..i} \\<^sub>M F i \\<^sub>M \\<^sub>P" using space_F[OF asm] by (intro measurable_sigma_sets[OF sets_predictable_sigma]) (fast, force simp add: space_pair_measure) + thus "case_prod X \ borel_measurable (restrict_space borel {t\<^sub>0..i} \\<^sub>M F i)" using predictable by simp +qed + +sublocale nat_predictable_process \ nat_progressive_process .. +sublocale real_predictable_process \ real_progressive_process .. + +text \The following lemma characterizes predictability in a discrete-time setting.\ + +lemma (in nat_filtered_measure) sets_in_filtration: + assumes "(\i. {i} \ A i) \ \\<^sub>P" + shows "A (Suc i) \ F i" "A 0 \ F 0" + using assms unfolding sets_predictable_sigma +proof (induction "(\i. {i} \ A i)" arbitrary: A) + case Basic + { + assume "\S. (\i. {i} \ A i) = {0} \ S" + then obtain S where S: "(\i. {i} \ A i) = {bot} \ S" unfolding bot_nat_def by blast + hence "S \ F bot" using Basic by (fastforce simp add: times_eq_iff bot_nat_def) + moreover have "A i = {}" if "i \ bot" for i using that S by blast + moreover have "A bot = S" using S by blast + ultimately have "A (Suc i) \ F i" "A 0 \ F 0" for i unfolding bot_nat_def by (auto simp add: bot_nat_def) + } + note * = this + { + assume "\S. (\i. {i} \ A i) = {0} \ S" + then obtain s t B where B: "(\i. {i} \ A i) = {s<..t} \ B" "B \ sets (F s)" "s < t" using Basic by auto + hence "A i = B" if "i \ {s<..t}" for i using that by fast + moreover have "A i = {}" if "i \ {s<..t}" for i using B that by fastforce + ultimately have "A (Suc i) \ F i" "A 0 \ F 0" for i unfolding bot_nat_def using B sets_F_mono by (auto simp add: bot_nat_def) (metis less_Suc_eq_le sets.empty_sets subset_eq) + } + note ** = this + show "A (Suc i) \ sets (F i)" "A 0 \ sets (F 0)" using *(1)[of i] *(2) **(1)[of i] **(2) by blast+ +next + case Empty + { + case 1 + then show ?case using Empty by simp + next + case 2 + then show ?case using Empty by simp + } +next + case (Compl a) + have a_in: "a \ {0..} \ space M" using Compl(1) sets.sets_into_space sets_predictable_sigma space_predictable_sigma by metis + hence A_in: "A i \ space M" for i using Compl(4) by blast + have a: "a = {0..} \ space M - (\i. {i} \ A i)" using a_in Compl(4) by blast + also have "... = - (\j. - ({j} \ (space M - A j)))" by blast + also have "... = (\j. {j} \ (space M - A j))" by blast + finally have *: "(space M - A (Suc i)) \ F i" "(space M - A 0) \ F 0" using Compl(2,3) by auto + { + case 1 + then show ?case using * A_in by (metis bot_nat_0.extremum double_diff sets.Diff sets.top sets_F_mono sets_le_imp_space_le space_F) + next + case 2 + then show ?case using * A_in by (metis bot_nat_0.extremum double_diff sets.Diff sets.top sets_F_mono sets_le_imp_space_le space_F) + } +next + case (Union a) + have a_in: "a i \ {0..} \ space M" for i using Union(1) sets.sets_into_space sets_predictable_sigma space_predictable_sigma by metis + hence A_in: "A i \ space M" for i using Union(4) by blast + have "snd x \ snd ` (a i \ ({fst x} \ space M))" if "x \ a i" for i x using that a_in by fastforce + hence a_i: "a i = (\j. {j} \ (snd ` (a i \ ({j} \ space M))))" for i by force + have A_i: "A i = snd ` (\ (range a) \ ({i} \ space M))" for i unfolding Union(4) using A_in by force + have *: "snd ` (a j \ ({Suc i} \ space M)) \ F i" "snd ` (a j \ ({0} \ space M)) \ F 0" for j using Union(2,3)[OF a_i] by auto + { + case 1 + have "(\j. snd ` (a j \ ({Suc i} \ space M))) \ F i" using * by fast + moreover have "(\j. snd ` (a j \ ({Suc i} \ space M))) = snd ` (\ (range a) \ ({Suc i} \ space M))" by fast + ultimately show ?case using A_i by metis + next + case 2 + have "(\j. snd ` (a j \ ({0} \ space M))) \ F 0" using * by fast + moreover have "(\j. snd ` (a j \ ({0} \ space M))) = snd ` (\ (range a) \ ({0} \ space M))" by fast + ultimately show ?case using A_i by metis + } +qed + +text \This leads to the following useful fact.\ + +lemma (in nat_predictable_process) adapted_Suc: "nat_adapted_process M F (\i. X (Suc i))" +proof (unfold_locales, intro borel_measurableI) + fix S :: "'b set" and i assume open_S: "open S" + have "{Suc i} = {i<..Suc i}" by fastforce + hence "{Suc i} \ space M \ \\<^sub>P" using space_F[symmetric, of i] unfolding sets_predictable_sigma by (intro sigma_sets.Basic) blast + moreover have "case_prod X -` S \ (UNIV \ space M) \ \\<^sub>P" unfolding atLeast_0[symmetric] using open_S by (intro predictableD, simp add: borel_open) + ultimately have "case_prod X -` S \ ({Suc i} \ space M) \ \\<^sub>P" unfolding sets_predictable_sigma using space_F sets.sets_into_space + by (subst Times_Int_distrib1[of "{Suc i}" UNIV "space M", simplified], subst inf.commute, subst Int_assoc[symmetric], subst Int_range_binary) + (intro sigma_sets_Inter binary_in_sigma_sets, fast)+ + moreover have "case_prod X -` S \ ({Suc i} \ space M) = {Suc i} \ (X (Suc i) -` S \ space M)" by (auto simp add: le_Suc_eq) + moreover have "... = (\j. {j} \ (if j = Suc i then (X (Suc i) -` S \ space M) else {}))" by (force split: if_splits) + ultimately have "(\j. {j} \ (if j = Suc i then (X (Suc i) -` S \ space M) else {})) \ \\<^sub>P" by argo + thus "X (Suc i) -` S \ space (F i) \ sets (F i)" using sets_in_filtration[of "\j. if j = Suc i then (X (Suc i) -` S \ space M) else {}"] space_F[OF zero_le] by presburger +qed + +text \The following lemma characterizes predictability in the discrete setting.\ + +theorem nat_predictable_process_iff: "nat_predictable_process M F X \ nat_adapted_process M F (\i. X (Suc i)) \ X 0 \ borel_measurable (F 0)" +proof (intro iffI) + assume asm: "nat_adapted_process M F (\i. X (Suc i)) \ X 0 \ borel_measurable (F 0)" + interpret nat_adapted_process M F "\i. X (Suc i)" using asm by blast + have "(\(x, y). X x y) \ borel_measurable \\<^sub>P" + proof (intro borel_measurableI) + fix S :: "'b set" assume open_S: "open S" + have "{i} \ (X i -` S \ space M) \ sets \\<^sub>P" for i + proof (cases i) + case 0 + then show ?thesis unfolding sets_predictable_sigma + using measurable_sets[OF _ borel_open[OF open_S], of "X 0" "F 0"] asm by auto + next + case (Suc i) + have "{Suc i} = {i<..Suc i}" by fastforce + then show ?thesis unfolding sets_predictable_sigma + using measurable_sets[OF adapted borel_open[OF open_S], of i] + by (intro sigma_sets.Basic, auto simp add: Suc) + qed + moreover have "(\(x, y). X x y) -` S \ space \\<^sub>P = (\i. {i} \ (X i -` S \ space M))" by fastforce + ultimately show "(\(x, y). X x y) -` S \ space \\<^sub>P \ sets \\<^sub>P" by simp + qed + thus "nat_predictable_process M F X" by (unfold_locales) +next + assume asm: "nat_predictable_process M F X" + interpret nat_predictable_process M F X by (rule asm) + show "nat_adapted_process M F (\i. X (Suc i)) \ X 0 \ borel_measurable (F 0)" using adapted_Suc by simp +qed + +end \ No newline at end of file diff --git a/thys/Martingales/document/root.bib b/thys/Martingales/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Martingales/document/root.bib @@ -0,0 +1,46 @@ +@book{Hytoenen_2016, + place={Cham, Switzerland}, + title={Analysis in Banach Spaces Volume I: Martingales and Littlewood-Paley theory}, + publisher={Springer International Publishing}, + author={Hytönen, Tuomas and Neerven, Jan van and Veraar, Mark and Weis, Lutz}, + year={2016}, + ISBN={978-3-319-48519-5} +} + +@book{Lang_1993, + place={New York}, + title={Real and Functional Analysis}, + publisher={Springer}, + author={Lang, Serge}, + year={1993}, + isbn={978-1-4612-0897-6} +} + +@article{keskin2023formalization, + title={A Formalization of Martingales in {Isabelle/HOL}}, + author={Ata Keskin}, + year={2023}, + eprint={2311.06188}, + archivePrefix={arXiv}, + primaryClass={cs.LO} +} + +@book{engelking_1989, + title={General Topology}, + author={Engelking, R.}, + isbn={978-3-8853-8006-1}, + series={Sigma series in pure mathematics}, + url={https://books.google.com.tr/books?id=K3spAQAAMAAJ}, + year={1989}, + publisher={Heldermann} +} + +@misc{Zitkovic_2015, + place={Austin, Texas}, + title={Lecture Notes on Conditional Expectation, Theory of Probability {I}, {UT Austin}}, + note={\url{https://web.ma.utexas.edu/users/gordanz/notes/conditional_expectation.pdf}}, + journal={Theory of Probability I}, publisher={The University of Texas at Austin}, + author={Zitkovic, Gordan}, + year={2015}, + month={Jan} +} \ No newline at end of file diff --git a/thys/Martingales/document/root.tex b/thys/Martingales/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Martingales/document/root.tex @@ -0,0 +1,79 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{amsmath} +\usepackage{amssymb} +\usepackage{isabelle,isabellesym} + +% further packages required for unusual symbols (see also +% isabellesym.sty), use only when needed + +%\usepackage{amssymb} + %for \, \, \, \, \, \, + %\, \, \, \, \, + %\, \, \ + +%\usepackage{eurosym} + %for \ + +%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd} + %for \, \, \, \, \ + +%\usepackage{eufrak} + %for \ ... \, \ ... \ (also included in amssymb) + +%\usepackage{textcomp} + %for \, \, \, \, \, + %\ + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +% for uniform font size +%\renewcommand{\isastyle}{\isastyleminor} + +\begin{document} + +\title{On the Formalization of Martingales} +\author{Ata Keskin} +\maketitle +\begin{abstract} +In the scope of this project, we present a formalization of martingales in arbitrary Banach spaces using Isabelle/HOL. + +The current formalization of conditional expectation in the Isabelle library is limited to real-valued functions. To overcome this limitation, we extend the construction of conditional expectation to general Banach spaces, employing an approach similar to the one described in \cite{Hytoenen_2016}. We use measure theoretic arguments to construct the conditional expectation using suitable limits of simple functions. + +Subsequently, we define stochastic processes and introduce the concepts of adapted, progressively measurable and predictable processes using suitable locale definitions\footnote{\texttt{Martingale.Stochastic\_Process}}. We show the relation +\[ + \text{adapted} \supseteq \text{progressive} \supseteq \text{predictable} +\] +Furthermore, we show that progressive measurability and adaptedness are equivalent when the indexing set is discrete. +We pay special attention to predictable processes in discrete-time, showing that $(X_n)_{n \in \mathbb{N}}$ is predictable if and only if $(X_{n + 1})_{n \in \mathbb{N}}$ is adapted. + +Moving forward, we rigorously define martingales, submartingales, and supermartingales, presenting their first consequences and corollaries\footnote{\texttt{Martingale.Martingale}}. Discrete-time martingales are given special attention in the formalization. In every step of our formalization, we make extensive use of the powerful locale system of Isabelle. + +The formalization further contributes by generalizing concepts in Bochner integration by extending their application from the real numbers to arbitrary Banach spaces equipped with a second-countable topology. Induction schemes for integrable simple functions on Banach spaces are introduced, accommodating various scenarios with or without a real vector ordering\footnote{\texttt{Martingale.Bochner\_Integration\_Addendum}}. Specifically, we formalize a powerful result called the ``Averaging Theorem''\cite{Lang_1993} which allows us to show that densities are unique in Banach spaces. + +In-depth information on the formalization and the proofs of the individual theorems can be found in \cite{keskin2023formalization}. +\end{abstract} +\tableofcontents +\pagebreak + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +% generated text of all theories +\input{session} + +% optional bibliography +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,789 +1,790 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel Concentration_Inequalities CRDT CRYSTALS-Kyber CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_Series Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage +Martingales Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems