Theory Upcrossing
section ‹Doob's Upcrossing Inequality and Martingale Convergence Theorems›
text ‹In this section we formalize upcrossings and downcrossings. Following this, we prove Doob's upcrossing inequality and first martingale convergence theorem.›
theory Upcrossing
imports Martingales.Martingale Stopping_Time
begin
lemma real_embedding_borel_measurable: "real ∈ borel_measurable borel" by (auto intro: borel_measurable_continuous_onI)
lemma limsup_lower_bound:
fixes u:: "nat ⇒ ereal"
assumes "limsup u > l"
shows "∃N>k. u N > l"
proof -
have "limsup u = - liminf (λn. - u n)" using liminf_ereal_cminus[of 0 u] by simp
hence "liminf (λn. - u n) < - l" using assms ereal_less_uminus_reorder by presburger
hence "∃N>k. - u N < - l" using liminf_upper_bound by blast
thus ?thesis using ereal_less_uminus_reorder by simp
qed
lemma ereal_abs_max_min: "¦c¦ = max 0 c - min 0 c" for c :: ereal
by (cases "c ≥ 0") auto
subsection ‹Upcrossings and Downcrossings›
text ‹Given a stochastic process \<^term>‹X›, real values \<^term>‹a› and \<^term>‹b›, and some point in time \<^term>‹N›, we would like to define a notion of "upcrossings" of \<^term>‹X› across the band \<^term>‹{a..b}› which counts the
number of times any realization of \<^term>‹X› crosses from below \<^term>‹a› to above \<^term>‹b› before time \<^term>‹N›. To make this heuristic rigorous, we inductively define the following hitting times.›
context nat_filtered_measure
begin
context
fixes X :: "nat ⇒ 'a ⇒ real"
and a b :: real
and N :: nat
begin
primrec upcrossing :: "nat ⇒ 'a ⇒ nat" where
"upcrossing 0 = (λω. 0)" |
"upcrossing (Suc n) = (λω. hitting_time X {b..} (hitting_time X {..a} (upcrossing n ω) N ω) N ω)"
definition downcrossing :: "nat ⇒ 'a ⇒ nat" where
"downcrossing n = (λω. hitting_time X {..a} (upcrossing n ω) N ω)"
lemma upcrossing_simps:
"upcrossing 0 = (λω. 0)"
"upcrossing (Suc n) = (λω. hitting_time X {b..} (downcrossing n ω) N ω)"
by (auto simp add: downcrossing_def)
lemma downcrossing_simps:
"downcrossing 0 = hitting_time X {..a} 0 N"
"downcrossing n = (λω. hitting_time X {..a} (upcrossing n ω) N ω)"
by (auto simp add: downcrossing_def)
declare upcrossing.simps[simp del]
lemma upcrossing_le: "upcrossing n ω ≤ N"
by (cases n) (auto simp add: upcrossing_simps hitting_time_le)
lemma downcrossing_le: "downcrossing n ω ≤ N"
by (cases n) (auto simp add: downcrossing_simps hitting_time_le)
lemma upcrossing_le_downcrossing: "upcrossing n ω ≤ downcrossing n ω"
unfolding downcrossing_simps by (auto intro: hitting_time_ge upcrossing_le)
lemma downcrossing_le_upcrossing_Suc: "downcrossing n ω ≤ upcrossing (Suc n) ω"
unfolding upcrossing_simps by (auto intro: hitting_time_ge downcrossing_le)
lemma upcrossing_mono:
assumes "n ≤ m"
shows "upcrossing n ω ≤ upcrossing m ω"
using order_trans[OF upcrossing_le_downcrossing downcrossing_le_upcrossing_Suc] assms
by (rule lift_Suc_mono_le)
lemma downcrossing_mono:
assumes "n ≤ m"
shows "downcrossing n ω ≤ downcrossing m ω"
using order_trans[OF downcrossing_le_upcrossing_Suc upcrossing_le_downcrossing] assms
by (rule lift_Suc_mono_le)
lemma stopped_value_upcrossing:
assumes "upcrossing (Suc n) ω ≠ N"
shows "stopped_value X (upcrossing (Suc n)) ω ≥ b"
proof -
have *: "upcrossing (Suc n) ω < N" using le_neq_implies_less upcrossing_le assms by presburger
have "∃j ∈ {downcrossing n ω..upcrossing (Suc n) ω}. X j ω ∈ {b..}"
using hitting_time_le_iff[THEN iffD1, OF *] upcrossing_simps by fastforce
then obtain j where j: "j ∈ {downcrossing n ω..N}" "X j ω ∈ {b..}" using * by (meson atLeastatMost_subset_iff le_refl subsetD upcrossing_le)
thus ?thesis using stopped_value_hitting_time_mem[of j _ _ X] unfolding upcrossing_simps stopped_value_def by blast
qed
lemma stopped_value_downcrossing:
assumes "downcrossing n ω ≠ N"
shows "stopped_value X (downcrossing n) ω ≤ a"
proof -
have *: "downcrossing n ω < N" using le_neq_implies_less downcrossing_le assms by presburger
have "∃j ∈ {upcrossing n ω..downcrossing n ω}. X j ω ∈ {..a}"
using hitting_time_le_iff[THEN iffD1, OF *] downcrossing_simps by fastforce
then obtain j where j: "j ∈ {upcrossing n ω..N}" "X j ω ∈ {..a}" using * by (meson atLeastatMost_subset_iff le_refl subsetD downcrossing_le)
thus ?thesis using stopped_value_hitting_time_mem[of j _ _ X] unfolding downcrossing_simps stopped_value_def by blast
qed
lemma upcrossing_less_downcrossing:
assumes "a < b" "downcrossing (Suc n) ω ≠ N"
shows "upcrossing (Suc n) ω < downcrossing (Suc n) ω"
proof -
have "upcrossing (Suc n) ω ≠ N" using assms by (metis le_antisym downcrossing_le upcrossing_le_downcrossing)
hence "stopped_value X (downcrossing (Suc n)) ω < stopped_value X (upcrossing (Suc n)) ω"
using assms stopped_value_downcrossing stopped_value_upcrossing by force
hence "downcrossing (Suc n) ω ≠ upcrossing (Suc n) ω" unfolding stopped_value_def by force
thus ?thesis using upcrossing_le_downcrossing by (simp add: le_neq_implies_less)
qed
lemma downcrossing_less_upcrossing:
assumes "a < b" "upcrossing (Suc n) ω ≠ N"
shows "downcrossing n ω < upcrossing (Suc n) ω"
proof -
have "downcrossing n ω ≠ N" using assms by (metis le_antisym upcrossing_le downcrossing_le_upcrossing_Suc)
hence "stopped_value X (downcrossing n) ω < stopped_value X (upcrossing (Suc n)) ω"
using assms stopped_value_downcrossing stopped_value_upcrossing by force
hence "downcrossing n ω ≠ upcrossing (Suc n) ω" unfolding stopped_value_def by force
thus ?thesis using downcrossing_le_upcrossing_Suc by (simp add: le_neq_implies_less)
qed
lemma upcrossing_less_Suc:
assumes "a < b" "upcrossing n ω ≠ N"
shows "upcrossing n ω < upcrossing (Suc n) ω"
by (metis assms upcrossing_le_downcrossing downcrossing_less_upcrossing order_le_less_trans le_neq_implies_less upcrossing_le)
lemma upcrossing_eq_bound:
assumes "a < b" "n ≥ N"
shows "upcrossing n ω = N"
proof -
have *: "upcrossing N ω = N"
proof -
{
assume *: "upcrossing N ω ≠ N"
hence asm: "upcrossing n ω < N" if "n ≤ N" for n using upcrossing_mono upcrossing_le that by (metis le_antisym le_neq_implies_less)
{
fix i j
assume "i ≤ N" "i < j"
hence "upcrossing i ω ≠ upcrossing j ω" by (metis Suc_leI asm assms(1) leD upcrossing_less_Suc upcrossing_mono)
}
moreover
{
fix j
assume "j ≤ N"
hence "upcrossing j ω ≤ upcrossing N ω" using upcrossing_mono by blast
hence "upcrossing (Suc N) ω ≠ upcrossing j ω" using upcrossing_less_Suc[OF assms(1) *] by simp
}
ultimately have "inj_on (λn. upcrossing n ω) {..Suc N}" unfolding inj_on_def by (metis atMost_iff le_SucE linorder_less_linear)
hence "card ((λn. upcrossing n ω) ` {..Suc N}) = Suc (Suc N)" by (simp add: inj_on_iff_eq_card[THEN iffD1])
moreover have "(λn. upcrossing n ω) ` {..Suc N} ⊆ {..N}" using upcrossing_le by blast
moreover have "card ((λn. upcrossing n ω) ` {..Suc N}) ≤ Suc N" using card_mono[OF _ calculation(2)] by simp
ultimately have False by linarith
}
thus ?thesis by blast
qed
thus ?thesis using upcrossing_mono[OF assms(2), of ω] upcrossing_le[of n ω] by simp
qed
lemma downcrossing_eq_bound:
assumes "a < b" "n ≥ N"
shows "downcrossing n ω = N"
using upcrossing_le_downcrossing[of n ω] downcrossing_le[of n ω] upcrossing_eq_bound[OF assms] by simp
lemma stopping_time_crossings:
assumes "adapted_process M F 0 X"
shows "stopping_time (upcrossing n)" "stopping_time (downcrossing n)"
proof -
have "stopping_time (upcrossing n) ∧ stopping_time (downcrossing n)"
proof (induction n)
case 0
then show ?case unfolding upcrossing_simps downcrossing_simps
using stopping_time_const stopping_time_hitting_time[OF assms] by simp
next
case (Suc n)
have "stopping_time (upcrossing (Suc n))" unfolding upcrossing_simps
using assms Suc downcrossing_le by (intro stopping_time_hitting_time') auto
moreover have "stopping_time (downcrossing (Suc n))" unfolding downcrossing_simps
using assms calculation upcrossing_le by (intro stopping_time_hitting_time') auto
ultimately show ?case by blast
qed
thus "stopping_time (upcrossing n)" "stopping_time (downcrossing n)" by blast+
qed
lemmas stopping_time_upcrossing = stopping_time_crossings(1)
lemmas stopping_time_downcrossing = stopping_time_crossings(2)
definition upcrossings_before :: "'a ⇒ nat" where
"upcrossings_before = (λω. Sup {n. upcrossing n ω < N})"
lemma upcrossings_before_bdd_above:
assumes "a < b"
shows "bdd_above {n. upcrossing n ω < N}"
proof -
have "{n. upcrossing n ω < N} ⊆ {..<N}" unfolding lessThan_def Collect_mono_iff
using upcrossing_eq_bound[OF assms] linorder_not_less order_less_irrefl by metis
thus ?thesis by (meson bdd_above_Iio bdd_above_mono)
qed
lemma upcrossings_before_less:
assumes "a < b" "0 < N"
shows "upcrossings_before ω < N"
proof -
have *: "{n. upcrossing n ω < N} ⊆ {..<N}" unfolding lessThan_def Collect_mono_iff
using upcrossing_eq_bound[OF assms(1)] linorder_not_less order_less_irrefl by metis
have "upcrossing 0 ω < N" unfolding upcrossing_simps by (rule assms)
moreover have "Sup {..<N} < N" unfolding Sup_nat_def using assms by simp
ultimately show ?thesis unfolding upcrossings_before_def using cSup_subset_mono[OF _ _ *] by force
qed
lemma upcrossings_before_less_implies_crossing_eq_bound:
assumes "a < b" "upcrossings_before ω < n"
shows "upcrossing n ω = N"
"downcrossing n ω = N"
proof -
have "¬ upcrossing n ω < N" using assms upcrossings_before_bdd_above[of ω] upcrossings_before_def bdd_above_nat finite_Sup_less_iff by fastforce
thus "upcrossing n ω = N" using upcrossing_le[of n ω] by simp
thus "downcrossing n ω = N" using upcrossing_le_downcrossing[of n ω] downcrossing_le[of n ω] by simp
qed
lemma upcrossings_before_le:
assumes "a < b"
shows "upcrossings_before ω ≤ N"
using upcrossings_before_less assms less_le_not_le upcrossings_before_def
by (cases N) auto
lemma upcrossings_before_mem:
assumes "a < b" "0 < N"
shows "upcrossings_before ω ∈ {n. upcrossing n ω < N} ∩ {..<N}"
proof -
have "upcrossing 0 ω < N" using assms unfolding upcrossing_simps by simp
hence "{n. upcrossing n ω < N} ≠ {}" by blast
moreover have "finite {n. upcrossing n ω < N}" using upcrossings_before_bdd_above[OF assms(1)] by (simp add: bdd_above_nat)
ultimately show ?thesis using Max_in upcrossings_before_less[OF assms(1,2)] Sup_nat_def upcrossings_before_def by auto
qed
lemma upcrossing_less_of_le_upcrossings_before:
assumes "a < b" "0 < N" "n ≤ upcrossings_before ω"
shows "upcrossing n ω < N"
using upcrossings_before_mem[OF assms(1,2), of ω] upcrossing_mono[OF assms(3), of ω] by simp
lemma upcrossings_before_sum_def:
assumes "a < b"
shows "upcrossings_before ω = (∑k∈{1..N}. indicator {n. upcrossing n ω < N} k)"
proof (cases N)
case 0
then show ?thesis unfolding upcrossings_before_def by simp
next
case (Suc N')
have "upcrossing 0 ω < N" using assms Suc unfolding upcrossing_simps by simp
hence "{n. upcrossing n ω < N} ≠ {}" by blast
hence *: "¬ upcrossing n ω < N" if "n ∈ {upcrossings_before ω <..N}" for n
using finite_Sup_less_iff[THEN iffD1, OF bdd_above_nat[THEN iffD1, OF upcrossings_before_bdd_above], of ω n]
by (metis that assms greaterThanAtMost_iff less_not_refl mem_Collect_eq upcrossings_before_def)
have **: "upcrossing n ω < N" if "n ∈ {1..upcrossings_before ω}" for n
using assms that Suc by (intro upcrossing_less_of_le_upcrossings_before) auto
have "upcrossings_before ω < N" using upcrossings_before_less Suc assms by simp
hence "{1..N} - {1..upcrossings_before ω} = {upcrossings_before ω<..N}"
"{1..N} ∩ {1..upcrossings_before ω} = {1..upcrossings_before ω}" by force+
hence "(∑k∈{1..N}. indicator {n. upcrossing n ω < N} k) =
(∑k∈{1..upcrossings_before ω}. indicator {n. upcrossing n ω < N} k) + (∑k∈{upcrossings_before ω <..N}. indicator {n. upcrossing n ω < N} k)"
using sum.Int_Diff[OF finite_atLeastAtMost, of _ 1 N "{1..upcrossings_before ω}"] by metis
also have "... = upcrossings_before ω" using * ** by simp
finally show ?thesis by argo
qed
lemma upcrossings_before_measurable:
assumes "adapted_process M F 0 X" "a < b"
shows "upcrossings_before ∈ borel_measurable M"
unfolding upcrossings_before_sum_def[OF assms(2)]
using stopping_time_measurable[OF stopping_time_crossings(1), OF assms(1)] by simp
lemma upcrossings_before_measurable':
assumes "adapted_process M F 0 X" "a < b"
shows "(λω. real (upcrossings_before ω)) ∈ borel_measurable M"
using real_embedding_borel_measurable upcrossings_before_measurable[OF assms] by simp
end
lemma crossing_eq_crossing:
assumes "N ≤ N'"
and "downcrossing X a b N n ω < N"
shows "upcrossing X a b N n ω = upcrossing X a b N' n ω"
"downcrossing X a b N n ω = downcrossing X a b N' n ω"
proof -
have "upcrossing X a b N n ω = upcrossing X a b N' n ω ∧ downcrossing X a b N n ω = downcrossing X a b N' n ω" using assms(2)
proof (induction n)
case 0
show ?case by (metis (no_types, lifting) upcrossing_simps(1) assms atLeast_0 bot_nat_0.extremum hitting_time_def hitting_time_eq_hitting_time inf_top.right_neutral leD downcrossing_mono downcrossing_simps(1) max_nat.left_neutral)
next
case (Suc n)
hence upper_less: "upcrossing X a b N (Suc n) ω < N" using upcrossing_le_downcrossing Suc order.strict_trans1 by blast
hence lower_less: "downcrossing X a b N n ω < N" using downcrossing_le_upcrossing_Suc order.strict_trans1 by blast
obtain j where "j ∈ {downcrossing X a b N n ω..<N}" "X j ω ∈ {b..}"
using hitting_time_less_iff[THEN iffD1, OF order_refl] upper_less by (force simp add: upcrossing_simps)
hence upper_eq: "upcrossing X a b N (Suc n) ω = upcrossing X a b N' (Suc n) ω"
using Suc(1)[OF lower_less] assms(1)
by (auto simp add: upcrossing_simps intro!: hitting_time_eq_hitting_time)
obtain j where j: "j ∈ {upcrossing X a b N (Suc n) ω..<N}" "X j ω ∈ {..a}" using Suc(2) hitting_time_less_iff[THEN iffD1, OF order_refl] by (force simp add: downcrossing_simps)
thus ?case unfolding downcrossing_simps upper_eq by (force intro: hitting_time_eq_hitting_time assms)
qed
thus "upcrossing X a b N n ω = upcrossing X a b N' n ω" "downcrossing X a b N n ω = downcrossing X a b N' n ω" by auto
qed
lemma crossing_eq_crossing':
assumes "N ≤ N'"
and "upcrossing X a b N (Suc n) ω < N"
shows "upcrossing X a b N (Suc n) ω = upcrossing X a b N' (Suc n) ω"
"downcrossing X a b N n ω = downcrossing X a b N' n ω"
proof -
show lower_eq: "downcrossing X a b N n ω = downcrossing X a b N' n ω"
using downcrossing_le_upcrossing_Suc[THEN order.strict_trans1] crossing_eq_crossing assms by fast
have "∃j∈{downcrossing X a b N n ω..<N}. X j ω ∈ {b..}" using assms(2) by (intro hitting_time_less_iff[OF order_refl, THEN iffD1]) (simp add: upcrossing_simps lower_eq)
then obtain j where "j∈{downcrossing X a b N n ω..N}" "X j ω ∈ {b..}" by fastforce
thus "upcrossing X a b N (Suc n) ω = upcrossing X a b N' (Suc n) ω"
unfolding upcrossing_simps stopped_value_def using hitting_time_eq_hitting_time[OF assms(1)] lower_eq by metis
qed
lemma upcrossing_eq_upcrossing:
assumes "N ≤ N'"
and "upcrossing X a b N n ω < N"
shows "upcrossing X a b N n ω = upcrossing X a b N' n ω"
using crossing_eq_crossing'[OF assms(1)] assms(2) upcrossing_simps
by (cases n) (presburger, fast)
lemma upcrossings_before_zero: "upcrossings_before X a b 0 ω = 0"
unfolding upcrossings_before_def by simp
lemma upcrossings_before_less_exists_upcrossing:
assumes "a < b"
and upcrossing: "N ≤ L" "X L ω < a" "L ≤ U" "b < X U ω"
shows "upcrossings_before X a b N ω < upcrossings_before X a b (Suc U) ω"
proof -
have "upcrossing X a b (Suc U) (upcrossings_before X a b N ω) ω ≤ L"
using assms upcrossing_le[THEN order_trans, OF upcrossing(1)]
by (cases "0 < N", subst upcrossing_eq_upcrossing[of N "Suc U", symmetric, OF _ upcrossing_less_of_le_upcrossings_before])
(auto simp add: upcrossings_before_zero upcrossing_simps)
hence "downcrossing X a b (Suc U) (upcrossings_before X a b N ω) ω ≤ U"
unfolding downcrossing_simps using upcrossing by (force intro: hitting_time_le_iff[THEN iffD2])
hence "upcrossing X a b (Suc U) (Suc (upcrossings_before X a b N ω)) ω < Suc U"
unfolding upcrossing_simps using upcrossing by (force intro: hitting_time_less_iff[THEN iffD2])
thus ?thesis using cSup_upper[OF _ upcrossings_before_bdd_above[OF assms(1)]] upcrossings_before_def by fastforce
qed
lemma crossings_translate:
"upcrossing X a b N = upcrossing (λn ω. (X n ω + c)) (a + c) (b + c) N"
"downcrossing X a b N = downcrossing (λn ω. (X n ω + c)) (a + c) (b + c) N"
proof -
have upper: "upcrossing X a b N n = upcrossing (λn ω. (X n ω + c)) (a + c) (b + c) N n" for n
proof (induction n)
case 0
then show ?case by (simp only: upcrossing.simps)
next
case (Suc n)
have "((+) c ` {..a}) = {..a + c}" by simp
moreover have "((+) c ` {b..}) = {b + c..}" by simp
ultimately show ?case unfolding upcrossing.simps using hitting_time_translate[of X "{b..}" c] hitting_time_translate[of X "{..a}" c] Suc by presburger
qed
thus "upcrossing X a b N = upcrossing (λn ω. (X n ω + c)) (a + c) (b + c) N" by blast
have "((+) c ` {..a}) = {..a + c}" by simp
thus "downcrossing X a b N = downcrossing (λn ω. (X n ω + c)) (a + c) (b + c) N" using upper downcrossing_simps hitting_time_translate[of X "{..a}" c] by presburger
qed
lemma upcrossings_before_translate:
"upcrossings_before X a b N = upcrossings_before (λn ω. (X n ω + c)) (a + c) (b + c) N"
using upcrossings_before_def crossings_translate by simp
lemma crossings_pos_eq:
assumes "a < b"
shows "upcrossing X a b N = upcrossing (λn ω. max 0 (X n ω - a)) 0 (b - a) N"
"downcrossing X a b N = downcrossing (λn ω. max 0 (X n ω - a)) 0 (b - a) N"
proof -
have *: "max 0 (x - a) ∈ {..0} ⟷ x - a ∈ {..0}" "max 0 (x - a) ∈ {b - a..} ⟷ x - a ∈ {b - a..}" for x using assms by auto
have "upcrossing X a b N = upcrossing (λn ω. X n ω - a) 0 (b - a) N" using crossings_translate[of X a b N "- a"] by simp
thus upper: "upcrossing X a b N = upcrossing (λn ω. max 0 (X n ω - a)) 0 (b - a) N" unfolding upcrossing_def hitting_time_def' using * by presburger
thus "downcrossing X a b N = downcrossing (λn ω. max 0 (X n ω - a)) 0 (b - a) N"
unfolding downcrossing_simps hitting_time_def' using upper * by simp
qed
lemma upcrossings_before_mono:
assumes "a < b" "N ≤ N'"
shows "upcrossings_before X a b N ω ≤ upcrossings_before X a b N' ω"
proof (cases N)
case 0
then show ?thesis unfolding upcrossings_before_def by simp
next
case (Suc N')
hence "upcrossing X a b N 0 ω < N" unfolding upcrossing_simps by simp
thus ?thesis unfolding upcrossings_before_def using upcrossings_before_bdd_above upcrossing_eq_upcrossing assms by (intro cSup_subset_mono) auto
qed
lemma upcrossings_before_pos_eq:
assumes "a < b"
shows "upcrossings_before X a b N = upcrossings_before (λn ω. max 0 (X n ω - a)) 0 (b - a) N"
using upcrossings_before_def crossings_pos_eq[OF assms] by simp
definition upcrossings :: "(nat ⇒ 'a ⇒ real) ⇒ real ⇒ real ⇒ 'a ⇒ ennreal" where
"upcrossings X a b = (λω. (SUP N. ennreal (upcrossings_before X a b N ω)))"
lemma upcrossings_measurable:
assumes "adapted_process M F 0 X" "a < b"
shows "upcrossings X a b ∈ borel_measurable M"
unfolding upcrossings_def
using upcrossings_before_measurable'[OF assms] by (auto intro!: borel_measurable_SUP)
end
lemma (in nat_finite_filtered_measure) integrable_upcrossings_before:
assumes "adapted_process M F 0 X" "a < b"
shows "integrable M (λω. real (upcrossings_before X a b N ω))"
proof -
have "(∫⇧+ x. ennreal (norm (real (upcrossings_before X a b N x))) ∂M) ≤ (∫⇧+ x. ennreal N ∂M)" using upcrossings_before_le[OF assms(2)] by (intro nn_integral_mono) simp
also have "... = ennreal N * emeasure M (space M)" by simp
also have "... < ∞" by (metis emeasure_real ennreal_less_top ennreal_mult_less_top infinity_ennreal_def)
finally show ?thesis by (intro integrableI_bounded upcrossings_before_measurable' assms)
qed
subsection ‹Doob's Upcrossing Inequality›
text ‹Doob's upcrossing inequality provides a bound on the expected number of upcrossings a submartingale completes before some point in time.
The proof follows the proof presented in the paper ‹A Formalization of Doob's Martingale Convergence Theorems in mathlib› \<^cite>‹ying2022formalization› \<^cite>‹Degenne_Ying_2022›.›
context nat_finite_filtered_measure
begin
theorem upcrossing_inequality:
fixes a b :: real and N :: nat
assumes "submartingale M F 0 X"
shows "(b - a) * (∫ω. real (upcrossings_before X a b N ω) ∂M) ≤ (∫ω. max 0 (X N ω - a) ∂M)"
proof -
interpret submartingale_linorder M F 0 X unfolding submartingale_linorder_def by (intro assms)
show ?thesis
proof (cases "a < b")
case True
have *: "(b - a) * (∫ω. real (upcrossings_before X a b N ω) ∂M) ≤ (∫ω. X N ω ∂M)"
if asm: "submartingale M F 0 X" "a < b" "⋀ω. X 0 ω ≥ 0" "⋀ω. X N ω ≥ a"
for a b X
proof -
interpret subm: submartingale M F 0 X by (intro asm)
define C :: "nat ⇒ 'a ⇒ real" where "C = (λn ω. ∑k < N. indicator {downcrossing X a b N k ω..<upcrossing X a b N (Suc k) ω} n)"
have C_values: "C n ω ∈ {0, 1}" for n ω
proof (cases "∃j < N. n ∈ {downcrossing X a b N j ω..<upcrossing X a b N (Suc j) ω}")
case True
then obtain j where j: "j ∈ {..<N}" "n ∈ {downcrossing X a b N j ω..<upcrossing X a b N (Suc j) ω}" by blast
{
fix k l :: nat assume k_less_l: "k < l"
hence Suc_k_le_l: "Suc k ≤ l" by simp
have "{downcrossing X a b N k ω..<upcrossing X a b N (Suc k) ω} ∩ {downcrossing X a b N l ω..<upcrossing X a b N (Suc l) ω} =
{downcrossing X a b N l ω..<upcrossing X a b N (Suc k) ω}"
using k_less_l upcrossing_mono downcrossing_mono by simp
moreover have "upcrossing X a b N (Suc k) ω ≤ downcrossing X a b N l ω"
using upcrossing_le_downcrossing downcrossing_mono[OF Suc_k_le_l] order_trans by blast
ultimately have "{downcrossing X a b N k ω..<upcrossing X a b N (Suc k) ω} ∩ {downcrossing X a b N l ω..<upcrossing X a b N (Suc l) ω} = {}" by simp
}
hence "disjoint_family_on (λk. {downcrossing X a b N k ω..<upcrossing X a b N (Suc k) ω}) {..<N}"
unfolding disjoint_family_on_def
by (metis Int_commute linorder_less_linear)
hence "C n ω = 1" unfolding C_def using sum_indicator_disjoint_family[where ?f="λ_. 1"] j by fastforce
thus ?thesis by blast
next
case False
hence "C n ω = 0" unfolding C_def by simp
thus ?thesis by simp
qed
hence C_interval: "C n ω ∈ {0..1}" for n ω by (metis atLeastAtMost_iff empty_iff insert_iff order.refl zero_less_one_class.zero_le_one)
define C' where "C' = (λn ω. ∑k < n. C k ω *⇩R (X (Suc k) ω - X k ω))"
define one_minus_C' where "one_minus_C' = (λn ω. ∑k < n. (1 - C k ω) *⇩R (X (Suc k) ω - X k ω))"
have adapted_C: "adapted_process M F 0 C"
proof
fix i
have "(λω. indicat_real {downcrossing X a b N k ω..<upcrossing X a b N (Suc k) ω} i) ∈ borel_measurable (F i)" for k
unfolding indicator_def
using stopping_time_upcrossing[OF subm.adapted_process_axioms, THEN stopping_time_measurable_gr]
stopping_time_downcrossing[OF subm.adapted_process_axioms, THEN stopping_time_measurable_le]
by force
thus "C i ∈ borel_measurable (F i)" unfolding C_def by simp
qed
hence "adapted_process M F 0 (λn ω. 1 - C n ω)" by (intro adapted_process.diff_adapted adapted_process_const)
hence submartingale_one_minus_C': "submartingale M F 0 one_minus_C'" unfolding one_minus_C'_def using C_interval
by (intro submartingale_partial_sum_scaleR[of _ _ 1] submartingale_linorder.intro asm) auto
have "C n ∈ borel_measurable M" for n
using adapted_C adapted_process.adapted measurable_from_subalg subalg by blast
have integrable_C': "integrable M (C' n)" for n unfolding C'_def using C_interval
by (intro submartingale_partial_sum_scaleR[THEN submartingale.integrable] submartingale_linorder.intro adapted_C asm) auto
have "integral⇧L M (C' n) ≤ integral⇧L M (X n)" for n
proof -
interpret subm': submartingale_linorder M F 0 one_minus_C' unfolding submartingale_linorder_def by (rule submartingale_one_minus_C')
have "0 ≤ integral⇧L M (one_minus_C' n)"
using subm'.set_integral_le[OF sets.top, where i=0 and j=n] space_F subm'.integrable by (fastforce simp add: set_integral_space one_minus_C'_def)
moreover have "one_minus_C' n ω = (∑k < n. X (Suc k) ω - X k ω) - C' n ω" for ω
unfolding one_minus_C'_def C'_def by (simp only: scaleR_diff_left sum_subtractf scale_one)
ultimately have "0 ≤ (LINT ω|M. (∑k < n. X (Suc k) ω - X k ω)) - integral⇧L M (C' n)"
using subm.integrable integrable_C'
by (subst Bochner_Integration.integral_diff[symmetric]) (auto simp add: one_minus_C'_def)
moreover have "(LINT ω|M. (∑k<n. X (Suc k) ω - X k ω)) ≤ (LINT ω|M. X n ω)" using asm sum_lessThan_telescope[of "λi. X i _" n] subm.integrable
by (intro integral_mono) auto
ultimately show ?thesis by linarith
qed
moreover have "(b - a) * (∫ω. real (upcrossings_before X a b N ω) ∂M) ≤ integral⇧L M (C' N)"
proof (cases N)
case 0
then show ?thesis using C'_def upcrossings_before_zero by simp
next
case (Suc N')
{
fix ω
have dc_not_N: "downcrossing X a b N k ω ≠ N" if "k < upcrossings_before X a b N ω" for k
by (metis Suc Suc_leI asm(2) downcrossing_le_upcrossing_Suc leD that upcrossing_less_of_le_upcrossings_before zero_less_Suc)
have uc_not_N:"upcrossing X a b N (Suc k) ω ≠ N" if "k < upcrossings_before X a b N ω" for k
by (metis Suc Suc_leI asm(2) order_less_irrefl that upcrossing_less_of_le_upcrossings_before zero_less_Suc)
have subset_lessThan_N: "{downcrossing X a b N i ω..<upcrossing X a b N (Suc i) ω} ⊆ {..<N}" if "i < N" for i using that
by (simp add: lessThan_atLeast0 upcrossing_le)
have "C' N ω = (∑k<N. ∑i<N. indicator {downcrossing X a b N i ω..<upcrossing X a b N (Suc i) ω} k * (X (Suc k) ω - X k ω))"
unfolding C'_def C_def by (simp add: sum_distrib_right)
also have "... = (∑i<N. ∑k<N. indicator {downcrossing X a b N i ω..<upcrossing X a b N (Suc i) ω} k * (X (Suc k) ω - X k ω))"
using sum.swap by fast
also have "... = (∑i<N. ∑k∈{..<N} ∩ {downcrossing X a b N i ω..<upcrossing X a b N (Suc i) ω}. X (Suc k) ω - X k ω)"
by (subst Indicator_Function.sum_indicator_mult) simp+
also have "... = (∑i<N. ∑k∈{downcrossing X a b N i ω..<upcrossing X a b N (Suc i) ω}. X (Suc k) ω - X k ω)"
using subset_lessThan_N[THEN Int_absorb1] by simp
also have "... = (∑i<N. X (upcrossing X a b N (Suc i) ω) ω - X (downcrossing X a b N i ω) ω)"
by (subst sum_Suc_diff'[OF downcrossing_le_upcrossing_Suc]) blast
finally have *: "C' N ω = (∑i<N. X (upcrossing X a b N (Suc i) ω) ω - X (downcrossing X a b N i ω) ω)" .
have summand_zero_if: "X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω = 0" if "k > upcrossings_before X a b N ω" for k
using that upcrossings_before_less_implies_crossing_eq_bound[OF asm(2)] by simp
have summand_nonneg_if: "X (upcrossing X a b N (Suc (upcrossings_before X a b N ω)) ω) ω - X (downcrossing X a b N (upcrossings_before X a b N ω) ω) ω ≥ 0"
using upcrossings_before_less_implies_crossing_eq_bound(1)[OF asm(2) lessI]
stopped_value_downcrossing[of X a b N _ ω, THEN order_trans, OF _ asm(4)[of ω]]
by (cases "downcrossing X a b N (upcrossings_before X a b N ω) ω ≠ N") (simp add: stopped_value_def)+
have interval: "{upcrossings_before X a b N ω..<N} - {upcrossings_before X a b N ω} = {upcrossings_before X a b N ω<..<N}"
using Diff_insert atLeastSucLessThan_greaterThanLessThan lessThan_Suc lessThan_minus_lessThan by metis
have "(b - a) * real (upcrossings_before X a b N ω) = (∑_<upcrossings_before X a b N ω. b - a)" by simp
also have "... ≤ (∑k<upcrossings_before X a b N ω. stopped_value X (upcrossing X a b N (Suc k)) ω - stopped_value X (downcrossing X a b N k) ω)"
using stopped_value_downcrossing[OF dc_not_N] stopped_value_upcrossing[OF uc_not_N] by (force intro!: sum_mono)
also have "... = (∑k<upcrossings_before X a b N ω. X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω)" unfolding stopped_value_def by blast
also have "... ≤ (∑k<upcrossings_before X a b N ω. X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω)
+ (∑k∈{upcrossings_before X a b N ω}. X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω)
+ (∑k∈{upcrossings_before X a b N ω<..<N}. X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω)"
using summand_zero_if summand_nonneg_if by auto
also have "... = (∑k<N. X (upcrossing X a b N (Suc k) ω) ω - X (downcrossing X a b N k ω) ω)"
using upcrossings_before_le[OF asm(2)]
by (subst sum.subset_diff[where A="{..<N}" and B="{..<upcrossings_before X a b N ω}"], simp, simp,
subst sum.subset_diff[where A="{..<N} - {..<upcrossings_before X a b N ω}" and B="{upcrossings_before X a b N ω}"])
(simp add: Suc asm(2) upcrossings_before_less, simp, simp add: interval)
finally have "(b - a) * real (upcrossings_before X a b N ω) ≤ C' N ω" using * by presburger
}
thus ?thesis using integrable_upcrossings_before subm.adapted_process_axioms asm integrable_C'
by (subst integral_mult_right_zero[symmetric], intro integral_mono) auto
qed
ultimately show ?thesis using order_trans by blast
qed
have "(b - a) * (∫ω. real (upcrossings_before X a b N ω) ∂M) = (b - a) * (∫ω. real (upcrossings_before (λn ω. max 0 (X n ω - a)) 0 (b - a) N ω) ∂M)"
using upcrossings_before_pos_eq[OF True] by simp
also have "... ≤ (∫ω. max 0 (X N ω - a) ∂M)"
using *[OF submartingale_linorder.max_0[OF submartingale_linorder.intro, OF submartingale.diff, OF assms supermartingale_const], of 0 "b - a" a] True by simp
finally show ?thesis .
next
case False
have "0 ≤ (∫ω. max 0 (X N ω - a) ∂M)" by simp
moreover have "0 ≤ (∫ω. real (upcrossings_before X a b N ω) ∂M)" by simp
moreover have "b - a ≤ 0" using False by simp
ultimately show ?thesis using mult_nonpos_nonneg order_trans by meson
qed
qed
theorem upcrossing_inequality_Sup:
fixes a b :: real
assumes "submartingale M F 0 X"
shows "(b - a) * (∫⇧+ω. upcrossings X a b ω ∂M) ≤ (SUP N. (∫⇧+ω. max 0 (X N ω - a) ∂M))"
proof -
interpret submartingale M F 0 X by (intro assms)
show ?thesis
proof (cases "a < b")
case True
have "(∫⇧+ω. upcrossings X a b ω ∂M) = (SUP N. (∫⇧+ω. real (upcrossings_before X a b N ω) ∂M))"
unfolding upcrossings_def
using upcrossings_before_mono True upcrossings_before_measurable'[OF adapted_process_axioms]
by (auto intro: nn_integral_monotone_convergence_SUP simp add: mono_def le_funI)
hence "(b - a) * (∫⇧+ω. upcrossings X a b ω ∂M) = (SUP N. (b - a) * (∫⇧+ω. real (upcrossings_before X a b N ω) ∂M))"
by (simp add: SUP_mult_left_ennreal)
moreover
{
fix N
have "(∫⇧+ω. real (upcrossings_before X a b N ω) ∂M) = (∫ω. real (upcrossings_before X a b N ω) ∂M)"
by (force intro!: nn_integral_eq_integral integrable_upcrossings_before True adapted_process_axioms)
moreover have "(∫⇧+ω. max 0 (X N ω - a) ∂M) = (∫ω. max 0 (X N ω - a) ∂M)"
using Bochner_Integration.integrable_diff[OF integrable integrable_const]
by (force intro!: nn_integral_eq_integral)
ultimately have "(b - a) * (∫⇧+ω. real (upcrossings_before X a b N ω) ∂M) ≤ (∫⇧+ω. max 0 (X N ω - a) ∂M)"
using upcrossing_inequality[OF assms, of b a N] True ennreal_mult'[symmetric] by simp
}
ultimately show ?thesis by (force intro!: Sup_mono)
qed (simp add: ennreal_neg)
qed
end
end