Theory Doob_Convergence
section ‹Doob's First Martingale Convergence Theorem›
theory Doob_Convergence
imports Upcrossing
begin
context nat_finite_filtered_measure
begin
text ‹Doob's martingale convergence theorem states that, if we have a submartingale where the supremum over the mean of the positive parts is finite, then the limit process exists almost surely and is integrable.
Furthermore, the limit process is measurable with respect to the smallest ‹σ›-algebra containing all of the ‹σ›-algebras in the filtration.
The argumentation below is taken mostly from \<^cite>‹durrett2019probability›.›
theorem submartingale_convergence_AE:
fixes X :: "nat ⇒ 'a ⇒ real"
assumes "submartingale M F 0 X"
and "⋀n. (∫ω. max 0 (X n ω) ∂M) ≤ C"
obtains X⇩l⇩i⇩m where "AE ω in M. (λn. X n ω) ⇢ X⇩l⇩i⇩m ω"
"integrable M X⇩l⇩i⇩m"
"X⇩l⇩i⇩m ∈ borel_measurable (F⇩∞)"
proof -
interpret submartingale_linorder M F 0 X unfolding submartingale_linorder_def by (rule assms)
have finite_upcrossings: "AE ω in M. upcrossings X a b ω ≠ ∞" if "a < b" for a b
proof -
have C_nonneg: "C ≥ 0" using assms(2) by (meson Bochner_Integration.integral_nonneg linorder_not_less max.cobounded1 order_less_le_trans)
{
fix n
have "(∫⇧+ω. max 0 (X n ω - a) ∂M) ≤ (∫⇧+ω. max 0 (X n ω) + ¦a¦ ∂M)" by (fastforce intro: nn_integral_mono ennreal_leI)
also have "... = (∫⇧+ω. max 0 (X n ω) ∂M) + ¦a¦ * emeasure M (space M)" by (simp add: nn_integral_add)
also have "... = (∫ω. max 0 (X n ω) ∂M) + ¦a¦ * emeasure M (space M)" using integrable by (simp add: nn_integral_eq_integral)
also have "... ≤ C + ¦a¦ * emeasure M (space M)" using assms(2) ennreal_leI by simp
finally have "(∫⇧+ω. max 0 (X n ω - a) ∂M) ≤ C + ¦a¦ * enn2real (emeasure M (space M))" using finite_emeasure_space C_nonneg by (simp add: ennreal_enn2real_if ennreal_mult)
}
hence "(SUP N. ∫⇧+ x. ennreal (max 0 (X N x - a)) ∂M) / (b - a) ≤ ennreal (C + ¦a¦ * enn2real (emeasure M (space M))) / (b - a)" by (fast intro: divide_right_mono_ennreal Sup_least)
moreover have "ennreal (C + ¦a¦ * enn2real (emeasure M (space M))) / (b - a) < ∞" using that C_nonneg by (subst divide_ennreal) auto
moreover have "integral⇧N M (upcrossings X a b) ≤ (SUP N. ∫⇧+ x. ennreal (max 0 (X N x - a)) ∂M) / (b - a)"
using upcrossing_inequality_Sup[OF assms(1), of b a, THEN divide_right_mono_ennreal, of "b - a"]
ennreal_mult_divide_eq mult.commute[of "ennreal (b - a)"] that by simp
ultimately show ?thesis using upcrossings_measurable adapted_process_axioms that by (intro nn_integral_noteq_infinite) auto
qed
define S where "S = ((λ(a :: real, b). {ω ∈ space M. liminf (λn. ereal (X n ω)) < ereal a ∧ ereal b < limsup (λn. ereal (X n ω))}) ` {(a, b) ∈ ℚ × ℚ. a < b})"
have "(0, 1) ∈ {(a :: real, b). (a, b) ∈ ℚ × ℚ ∧ a < b}" unfolding Rats_def by simp
moreover have "countable {(a, b). (a, b) ∈ ℚ × ℚ ∧ a < b}" by (blast intro: countable_subset[OF _ countable_SIGMA[OF countable_rat countable_rat]])
ultimately have from_nat_into_S: "range (from_nat_into S) = S" "from_nat_into S n ∈ S" for n
unfolding S_def
by (auto intro!: range_from_nat_into from_nat_into simp only: Rats_def)
{
fix a b :: real
assume a_less_b: "a < b"
then obtain N where N: "x ∈ space M - N ⟹ upcrossings X a b x ≠ ∞" "N ∈ null_sets M" for x using AE_E3[OF finite_upcrossings] by blast
{
fix ω
assume liminf_limsup: "liminf (λn. X n ω) < a" "b < limsup (λn. X n ω)"
have "upcrossings X a b ω = ∞"
proof -
{
fix n
have "∃m. upcrossings_before X a b m ω ≥ n"
proof (induction n)
case 0
have "Sup {n. upcrossing X a b 0 n ω < 0} = 0" by simp
then show ?case unfolding upcrossings_before_def by blast
next
case (Suc n)
then obtain m where m: "n ≤ upcrossings_before X a b m ω" by blast
obtain l where l: "l ≥ m" "X l ω < a" using liminf_upper_bound[OF liminf_limsup(1), of m] nless_le by auto
obtain u where u: "u ≥ l" "X u ω > b" using limsup_lower_bound[OF liminf_limsup(2), of l] nless_le by auto
show ?case using upcrossings_before_less_exists_upcrossing[OF a_less_b, where ?X=X, OF l u] m by (metis Suc_leI le_neq_implies_less)
qed
}
thus ?thesis unfolding upcrossings_def by (simp add: ennreal_SUP_eq_top)
qed
}
hence "{ω ∈ space M. liminf (λn. ereal (X n ω)) < ereal a ∧ ereal b < limsup (λn. ereal (X n ω))} ⊆ N" using N by blast
moreover have "{ω ∈ space M. liminf (λn. ereal (X n ω)) < ereal a ∧ ereal b < limsup (λn. ereal (X n ω))} ∩ N ∈ null_sets M" by (force intro: null_set_Int1[OF N(2)])
ultimately have "emeasure M {ω ∈ space M. liminf (λn. ereal (X n ω)) < a ∧ b < limsup (λn. ereal (X n ω))} = 0" by (simp add: Int_absorb1 Int_commute null_setsD1)
}
hence "emeasure M (from_nat_into S n) = 0" for n using from_nat_into_S(2)[of n] unfolding S_def by force
moreover have "S ⊆ M" unfolding S_def by force
ultimately have "emeasure M (⋃ (range (from_nat_into S))) = 0" using from_nat_into_S by (intro emeasure_UN_eq_0) auto
moreover have "(⋃ S) = {ω ∈ space M. liminf (λn. ereal (X n ω)) ≠ limsup (λn. ereal (X n ω))}" (is "?L = ?R")
proof -
{
fix ω
assume asm: "ω ∈ ?L"
then obtain a b :: real where "a < b" "liminf (λn. ereal (X n ω)) < ereal a ∧ ereal b < limsup (λn. ereal (X n ω))" unfolding S_def by blast
hence "liminf (λn. ereal (X n ω)) ≠ limsup (λn. ereal (X n ω))" using ereal_less_le order.asym by fastforce
hence "ω ∈ ?R" using asm unfolding S_def by blast
}
moreover
{
fix ω
assume asm: "ω ∈ ?R"
hence "liminf (λn. ereal (X n ω)) < limsup (λn. ereal (X n ω))" using Liminf_le_Limsup[of sequentially] less_eq_ereal_def by auto
then obtain a' where a': "liminf (λn. ereal (X n ω)) < ereal a'" "ereal a' < limsup (λn. ereal (X n ω))" using ereal_dense2 by blast
then obtain b' where b': "ereal a' < ereal b'" "ereal b' < limsup (λn. ereal (X n ω))" using ereal_dense2 by blast
hence "a' < b'" by simp
then obtain a where a: "a ∈ ℚ" "a' < a" "a < b'" using Rats_dense_in_real by blast
then obtain b where b: "b ∈ ℚ" "a < b" "b < b'" using Rats_dense_in_real by blast
have "liminf (λn. ereal (X n ω)) < ereal a" using a a' le_ereal_less order_less_imp_le by meson
moreover have "ereal b < limsup (λn. ereal (X n ω))" using b b' order_less_imp_le ereal_less_le by meson
ultimately have "ω ∈ ?L" unfolding S_def using a b asm by blast
}
ultimately show ?thesis by blast
qed
ultimately have "emeasure M {ω ∈ space M. liminf (λn. ereal (X n ω)) ≠ limsup (λn. ereal (X n ω))} = 0" using from_nat_into_S by argo
hence liminf_limsup_AE: "AE ω in M. liminf (λn. X n ω) = limsup (λn. X n ω)" by (intro AE_iff_measurable[THEN iffD2, OF _ refl]) auto
hence convergent_AE: "AE ω in M. convergent (λn. ereal (X n ω))" using convergent_ereal by fastforce
have bounded_pos_part: "ennreal (∫ω. max 0 (X n ω) ∂M) ≤ ennreal C" for n using assms(2) ennreal_leI by blast
{
fix ω
assume asm: "convergent (λn. ereal (X n ω))"
hence "(λn. max 0 (ereal (X n ω))) ⇢ max 0 (lim (λn. ereal (X n ω)))"
using convergent_LIMSEQ_iff isCont_tendsto_compose continuous_max continuous_const continuous_ident continuous_at_e2ennreal
by fast
hence "(λn. e2ennreal (max 0 (ereal (X n ω)))) ⇢ e2ennreal (max 0 (lim (λn. ereal (X n ω))))"
using isCont_tendsto_compose continuous_at_e2ennreal by blast
moreover have "lim (λn. e2ennreal (max 0 (ereal (X n ω)))) = e2ennreal (max 0 (lim (λn. ereal (X n ω))))" using limI calculation by blast
ultimately have "e2ennreal (max 0 (liminf (λn. ereal (X n ω)))) = liminf (λn. e2ennreal (max 0 (ereal (X n ω))))" using convergent_liminf_cl by (metis asm convergent_def limI)
}
hence "(∫⇧+ω. e2ennreal (max 0 (liminf (λn. ereal (X n ω)))) ∂M) = (∫⇧+ω. liminf (λn. e2ennreal (max 0 (ereal (X n ω)))) ∂M)" using convergent_AE by (fast intro: nn_integral_cong_AE)
moreover have "(∫⇧+ω. liminf (λn. e2ennreal (max 0 (ereal (X n ω)))) ∂M) ≤ liminf (λn. (∫⇧+ω. e2ennreal (max 0 (ereal (X n ω))) ∂M))"
by (intro nn_integral_liminf) auto
moreover have "(∫⇧+ω. e2ennreal (max 0 (ereal (X n ω))) ∂M) = ennreal (∫ω. max 0 (X n ω) ∂M)" for n
using e2ennreal_ereal ereal_max_0
by (subst nn_integral_eq_integral[symmetric]) (fastforce intro!: nn_integral_cong integrable | presburger)+
moreover have liminf_pos_part_finite: "liminf (λn. ennreal (∫ω. max 0 (X n ω) ∂M)) < ∞"
unfolding liminf_SUP_INF
using Inf_lower2[OF _ bounded_pos_part]
by (intro order.strict_trans1[OF Sup_least, of _ "ennreal C"]) (metis (mono_tags, lifting) atLeast_iff imageE image_eqI order.refl, simp)
ultimately have pos_part_finite: "(∫⇧+ω. e2ennreal (max 0 (liminf (λn. ereal (X n ω)))) ∂M) < ∞" by force
{
fix ω
assume asm: "convergent (λn. ereal (X n ω))"
hence "(λn. - min 0 (ereal (X n ω))) ⇢ - min 0 (lim (λn. ereal (X n ω)))"
using convergent_LIMSEQ_iff isCont_tendsto_compose continuous_min continuous_const continuous_ident continuous_at_e2ennreal
by fast
hence "(λn. e2ennreal (- min 0 (ereal (X n ω)))) ⇢ e2ennreal (- min 0 (lim (λn. ereal (X n ω))))"
using isCont_tendsto_compose continuous_at_e2ennreal by blast
moreover have "lim (λn. e2ennreal (- min 0 (ereal (X n ω)))) = e2ennreal (- min 0 (lim (λn. ereal (X n ω))))" using limI calculation by blast
ultimately have "e2ennreal (- min 0 (liminf (λn. ereal (X n ω)))) = liminf (λn. e2ennreal (- min 0 (ereal (X n ω))))" using convergent_liminf_cl by (metis asm convergent_def limI)
}
hence "(∫⇧+ω. e2ennreal (- min 0 (liminf (λn. ereal (X n ω)))) ∂M) = (∫⇧+ω. liminf (λn. e2ennreal (- min 0 (ereal (X n ω)))) ∂M)" using convergent_AE by (fast intro: nn_integral_cong_AE)
moreover have "(∫⇧+ω. liminf (λn. e2ennreal (- min 0 (ereal (X n ω)))) ∂M) ≤ liminf (λn. (∫⇧+ω. e2ennreal (- min 0 (ereal (X n ω))) ∂M))"
by (intro nn_integral_liminf) auto
moreover have "(∫⇧+ω. e2ennreal (- min 0 (ereal (X n ω))) ∂M) = (∫ω. max 0 (X n ω) ∂M) - (∫ω. X n ω ∂M)" for n
proof -
have *: "(- min 0 c) = max 0 c - c" if "c ≠ ∞" for c :: ereal using that by (cases "c ≥ 0") auto
hence "(∫⇧+ω. e2ennreal (- min 0 (ereal (X n ω))) ∂M) = (∫⇧+ω. e2ennreal (max 0 (ereal (X n ω)) - (ereal (X n ω))) ∂M)" by simp
also have "... = (∫⇧+ ω. ennreal (max 0 (X n ω) - (X n ω)) ∂M)" using e2ennreal_ereal ereal_max_0 ereal_minus(1) by (intro nn_integral_cong) presburger
also have "... = (∫ω. max 0 (X n ω) - (X n ω) ∂M)" using integrable by (intro nn_integral_eq_integral) auto
finally show ?thesis using Bochner_Integration.integral_diff integrable by simp
qed
moreover have "liminf (λn. ennreal ((∫ω. max 0 (X n ω) ∂M) - (∫ω. X n ω ∂M))) < ∞"
proof -
{
fix n A
assume asm: "ennreal ((∫ω. max 0 (X n ω) ∂M) - (∫ω. X n ω ∂M)) ∈ A"
have "(∫ω. X 0 ω ∂M) ≤ (∫ω. X n ω ∂M)" using set_integral_le[OF sets.top order_refl, of n] space_F by (simp add: integrable set_integral_space)
hence "(∫ω. max 0 (X n ω) ∂M) - (∫ω. X n ω ∂M) ≤ C - (∫ω. X 0 ω ∂M)" using assms(2)[of n] by argo
hence "ennreal ((∫ω. max 0 (X n ω) ∂M) - (∫ω. X n ω ∂M)) ≤ ennreal (C - (∫ω. X 0 ω ∂M))" using ennreal_leI by blast
hence "Inf A ≤ ennreal (C - (∫ω. X 0 ω ∂M))" by (rule Inf_lower2[OF asm])
}
thus ?thesis
unfolding liminf_SUP_INF
by (intro order.strict_trans1[OF Sup_least, of _ "ennreal (C - (∫ω. X 0 ω ∂M))"]) (metis (no_types, lifting) atLeast_iff imageE image_eqI order.refl order_trans, simp)
qed
ultimately have neg_part_finite: "(∫⇧+ ω. e2ennreal (- (min 0 (liminf (λn. ereal (X n ω))))) ∂M) < ∞" by simp
have "e2ennreal ¦liminf (λn. ereal (X n ω))¦ = e2ennreal (max 0 (liminf (λn. ereal (X n ω)))) + e2ennreal (- (min 0 (liminf (λn. ereal (X n ω)))))" for ω
unfolding ereal_abs_max_min
by (simp add: eq_onp_same_args max_def plus_ennreal.abs_eq)
hence "(∫⇧+ ω. e2ennreal ¦liminf (λn. ereal (X n ω))¦ ∂M) = (∫⇧+ ω. e2ennreal (max 0 (liminf (λn. ereal (X n ω)))) ∂M) + (∫⇧+ ω. e2ennreal (- (min 0 (liminf (λn. ereal (X n ω))))) ∂M)" by (auto intro: nn_integral_add)
hence nn_integral_finite: "(∫⇧+ ω. e2ennreal ¦liminf (λn. ereal (X n ω))¦ ∂M) ≠ ∞" using pos_part_finite neg_part_finite by auto
hence finite_AE: "AE ω in M. e2ennreal ¦liminf (λn. ereal (X n ω))¦ ≠ ∞" by (intro nn_integral_noteq_infinite) auto
moreover
{
fix ω
assume asm: "liminf (λn. X n ω) = limsup (λn. X n ω)" "¦liminf (λn. ereal (X n ω))¦ ≠ ∞"
hence "(λn. X n ω) ⇢ real_of_ereal (liminf (λn. X n ω))" using limsup_le_liminf_real ereal_real' by simp
}
ultimately have converges: "AE ω in M. (λn. X n ω) ⇢ real_of_ereal (liminf (λn. X n ω))" using liminf_limsup_AE by fastforce
{
fix ω
assume "e2ennreal ¦liminf (λn. ereal (X n ω))¦ ≠ ∞"
hence "¦liminf (λn. ereal (X n ω))¦ ≠ ∞" by force
hence "e2ennreal ¦liminf (λn. ereal (X n ω))¦ = ennreal (norm (real_of_ereal (liminf (λn. ereal (X n ω)))))" by fastforce
}
hence "(∫⇧+ ω. e2ennreal ¦liminf (λn. ereal (X n ω))¦ ∂M) = (∫⇧+ ω. ennreal (norm (real_of_ereal (liminf (λn. ereal (X n ω))))) ∂M)" using finite_AE by (fast intro: nn_integral_cong_AE)
hence "(∫⇧+ ω. ennreal (norm (real_of_ereal (liminf (λn. ereal (X n ω))))) ∂M) < ∞" using nn_integral_finite by (simp add: order_less_le)
hence "integrable M (λω. real_of_ereal (liminf (λn. X n ω)))" by (intro integrableI_bounded) auto
moreover have "(λω. real_of_ereal (liminf (λn. X n ω))) ∈ borel_measurable F⇩∞" using borel_measurable_liminf[OF F_infinity_measurableI] adapted by measurable
ultimately show ?thesis using that converges by presburger
qed
corollary supermartingale_convergence_AE:
fixes X :: "nat ⇒ 'a ⇒ real"
assumes "supermartingale M F 0 X"
and "⋀n. (∫ω. max 0 (- X n ω) ∂M) ≤ C"
obtains X⇩l⇩i⇩m where "AE ω in M. (λn. X n ω) ⇢ X⇩l⇩i⇩m ω"
"integrable M X⇩l⇩i⇩m"
"X⇩l⇩i⇩m ∈ borel_measurable (F⇩∞)"
proof -
obtain Y where *: "AE ω in M. (λn. - X n ω) ⇢ Y ω" "integrable M Y" "Y ∈ borel_measurable (F⇩∞)"
using supermartingale.uminus[OF assms(1), THEN submartingale_convergence_AE] assms(2) by auto
hence "AE ω in M. (λn. X n ω) ⇢ (- Y) ω" "integrable M (- Y)" "- Y ∈ borel_measurable (F⇩∞)"
using isCont_tendsto_compose[OF isCont_minus, OF continuous_ident] integrable_minus borel_measurable_uminus unfolding fun_Compl_def by fastforce+
thus ?thesis using that[of "- Y"] by blast
qed
corollary martingale_convergence_AE:
fixes X :: "nat ⇒ 'a ⇒ real"
assumes "martingale M F 0 X"
and "⋀n. (∫ω. ¦X n ω¦ ∂M) ≤ C"
obtains X⇩l⇩i⇩m where "AE ω in M. (λn. X n ω) ⇢ X⇩l⇩i⇩m ω"
"integrable M X⇩l⇩i⇩m"
"X⇩l⇩i⇩m ∈ borel_measurable (F⇩∞)"
proof -
interpret martingale_linorder M F 0 X unfolding martingale_linorder_def by (rule assms)
have "max 0 (X n ω) ≤ ¦X n ω¦" for n ω by linarith
hence "(∫ω. max 0 (X n ω) ∂M) ≤ C" for n using assms(2)[THEN dual_order.trans, OF integral_mono, OF integrable_max] integrable by fast
thus ?thesis using that submartingale_convergence_AE[OF submartingale_axioms] by blast
qed
corollary martingale_nonneg_convergence_AE:
fixes X :: "nat ⇒ 'a ⇒ real"
assumes "martingale M F 0 X" "⋀n. AE ω in M. X n ω ≥ 0"
obtains X⇩l⇩i⇩m where "AE ω in M. (λn. X n ω) ⇢ X⇩l⇩i⇩m ω"
"integrable M X⇩l⇩i⇩m"
"X⇩l⇩i⇩m ∈ borel_measurable (F⇩∞)"
proof -
interpret martingale_linorder M F 0 X unfolding martingale_linorder_def by (rule assms)
have "AE ω in M. max 0 (- X n ω) = 0" for n using assms(2)[of n] by force
hence "(∫ω. max 0 (- X n ω) ∂M) ≤ 0" for n by (simp add: integral_eq_zero_AE)
thus ?thesis using that supermartingale_convergence_AE[OF supermartingale_axioms] by blast
qed
end
end