Theory Stopping_Time
section ‹Stopping Times and Hitting Times›
text ‹In this section we formalize stopping times and hitting times. A stopping time is a random variable that represents the time at which a certain event occurs within a stochastic process.
A hitting time, also known as first passage time or first hitting time, is a specific type of stopping time that represents the first time a stochastic process reaches a particular state or crosses a certain threshold.›
theory Stopping_Time
imports Martingales.Stochastic_Process
begin
subsection ‹Stopping Time›
text ‹The formalization of stopping times here is simply a rewrite of the document ‹HOL-Probability.Stopping_Time› \<^cite>‹"hoelzl2011measuretheory"›.
We have adapted the document to use the locales defined in our formalization of filtered measure spaces \<^cite>‹keskin2023formalization› \<^cite>‹"Martingales-AFP"›.
This way, we can omit the partial formalization of filtrations in the original document. Furthermore, we can include the initial time index \<^term>‹t⇩0› that we introduced as well.›
context linearly_filtered_measure
begin
definition stopping_time :: "('a ⇒ 'b) ⇒ bool" where
"stopping_time T = ((T ∈ space M → {t⇩0..}) ∧ (∀t≥t⇩0. Measurable.pred (F t) (λx. T x ≤ t)))"
lemma stopping_time_cong:
assumes "⋀t x. t ≥ t⇩0 ⟹ x ∈ space (F t) ⟹ T x = S x"
shows "stopping_time T = stopping_time S"
proof (cases "T ∈ space M → {t⇩0..}")
case True
hence "S ∈ space M → {t⇩0..}" using assms space_F by force
then show ?thesis unfolding stopping_time_def
using assms arg_cong[where f="(λP. ∀t≥t⇩0. P t)"] measurable_cong[where M="F _" and f="λx. T x ≤ _" and g="λx. S x ≤ _"] True by metis
next
case False
hence "S ∉ space M → {t⇩0..}" using assms space_F by force
then show ?thesis unfolding stopping_time_def using False by blast
qed
lemma stopping_time_ge_zero:
assumes "stopping_time T" "ω ∈ space M"
shows "T ω ≥ t⇩0"
using assms unfolding stopping_time_def by auto
lemma stopping_timeD:
assumes "stopping_time T" "t ≥ t⇩0"
shows "Measurable.pred (F t) (λx. T x ≤ t)"
using assms unfolding stopping_time_def by simp
lemma stopping_timeI[intro?]:
assumes "⋀x. x ∈ space M ⟹ T x ≥ t⇩0"
"(⋀t. t ≥ t⇩0 ⟹ Measurable.pred (F t) (λx. T x ≤ t))"
shows "stopping_time T"
using assms by (auto simp: stopping_time_def)
lemma stopping_time_measurable:
assumes "stopping_time T"
shows "T ∈ borel_measurable M"
proof (rule borel_measurableI_le)
{
fix t assume "¬ t ≥ t⇩0"
hence "{x ∈ space M. T x ≤ t} = {}" using assms dual_order.trans[of _ t "t⇩0"] unfolding stopping_time_def by fastforce
hence "{x ∈ space M. T x ≤ t} ∈ sets M" by (metis sets.empty_sets)
}
moreover
{
fix t assume asm: "t ≥ t⇩0"
hence "{x ∈ space M. T x ≤ t} ∈ sets M" using stopping_timeD[OF assms asm] sets_F_subset unfolding Measurable.pred_def space_F[OF asm] by blast
}
ultimately show "{x ∈ space M. T x ≤ t} ∈ sets M" for t by blast
qed
lemma stopping_time_const:
assumes "t ≥ t⇩0"
shows "stopping_time (λx. t)" using assms by (auto simp: stopping_time_def)
lemma stopping_time_min:
assumes "stopping_time T" "stopping_time S"
shows "stopping_time (λx. min (T x) (S x))"
using assms by (auto simp: stopping_time_def min_le_iff_disj intro!: pred_intros_logic)
lemma stopping_time_max:
assumes "stopping_time T" "stopping_time S"
shows "stopping_time (λx. max (T x) (S x))"
using assms by (auto simp: stopping_time_def intro!: pred_intros_logic max.coboundedI1)
subsection ‹‹σ›-algebra of a Stopping Time›
text ‹Moving on, we define the ‹σ›-algebra associated with a stopping time \<^term>‹T›.
It contains all the information up to time \<^term>‹T›, the same way \<^term>‹F t› contains all the information up to time \<^term>‹t›.›
definition pre_sigma :: "('a ⇒ 'b) ⇒ 'a measure" where
"pre_sigma T = sigma (space M) {A ∈ sets M. ∀t≥t⇩0. {ω ∈ A. T ω ≤ t} ∈ sets (F t)}"
lemma measure_pre_sigma[simp]: "emeasure (pre_sigma T) = (λ_. 0)" by (simp add: pre_sigma_def emeasure_sigma)
lemma sigma_algebra_pre_sigma:
assumes "stopping_time T"
shows "sigma_algebra (space M) {A ∈ sets M. ∀t≥t⇩0. {ω∈A. T ω ≤ t} ∈ sets (F t)}"
proof -
let ?Σ = "{A ∈ sets M. ∀t≥t⇩0. {ω∈A. T ω ≤ t} ∈ sets (F t)}"
{
fix A assume asm: "A ∈ ?Σ"
{
fix t assume asm': "t ≥ t⇩0"
hence "{ω∈A. T ω ≤ t} ∈ sets (F t)" using asm by blast
then have "{ω ∈ space (F t). T ω ≤ t} - {ω ∈ A. T ω ≤ t} ∈ sets (F t)" using assms[THEN stopping_timeD, OF asm'] by auto
also have "{ω ∈ space (F t). T ω ≤ t} - {ω ∈ A. T ω ≤ t} = {ω ∈ space M - A. T ω ≤ t}" using space_F[OF asm'] by blast
finally have "{ω ∈ (space M) - A. T ω ≤ t} ∈ sets (F t)" .
}
hence "space M - A ∈ ?Σ" using asm by blast
}
moreover
{
fix A :: "nat ⇒ 'a set" assume asm: "range A ⊆ ?Σ"
{
fix t assume "t ≥ t⇩0"
then have "(⋃i. {ω ∈ A i. T ω ≤ t}) ∈ sets (F t)" using asm by auto
also have "(⋃i. {ω ∈ A i. T ω ≤ t}) = {ω ∈ ⋃(A ` UNIV). T ω ≤ t}" by auto
finally have "{ω ∈ ⋃(range A). T ω ≤ t} ∈ sets (F t)" .
}
hence "⋃(range A) ∈ ?Σ" using asm by blast
}
ultimately show ?thesis unfolding sigma_algebra_iff2 by (auto intro!: sets.sets_into_space[THEN PowI, THEN subsetI])
qed
lemma space_pre_sigma[simp]: "space (pre_sigma T) = space M" unfolding pre_sigma_def by (intro space_measure_of_conv)
lemma sets_pre_sigma:
assumes "stopping_time T"
shows "sets (pre_sigma T) = {A ∈ sets M. ∀t≥t⇩0. {ω∈A. T ω ≤ t} ∈ F t}"
unfolding pre_sigma_def using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_pre_sigma, OF assms] by blast
lemma sets_pre_sigmaI:
assumes "stopping_time T"
and "⋀t. t ≥ t⇩0 ⟹ {ω ∈ A. T ω ≤ t} ∈ F t"
shows "A ∈ pre_sigma T"
proof (cases "∃t≥t⇩0. ∀t'. t' ≤ t")
case True
then obtain t where "t ≥ t⇩0" "{ω ∈ A. T ω ≤ t} = A" by blast
hence "A ∈ M" using assms(2)[of t] sets_F_subset[of t] by fastforce
thus ?thesis using assms(2) unfolding sets_pre_sigma[OF assms(1)] by blast
next
case False
hence *: "{t<..} ≠ {}" if "t ≥ t⇩0" for t by (metis not_le empty_iff greaterThan_iff)
obtain D :: "'b set" where D: "countable D" "⋀X. open X ⟹ X ≠ {} ⟹ D ∩ X ≠ {}" by (metis countable_dense_setE disjoint_iff)
have **: "D ∩ {t<..} ≠ {}" if "t ≥ t⇩0" for t using * that by (intro D(2)) auto
{
fix ω
obtain t where t: "t ≥ t⇩0" "T ω ≤ t" using linorder_linear by auto
moreover obtain t' where "t' ∈ D ∩ {t<..} ∩ {t⇩0..}" using ** t by fastforce
moreover have "T ω ≤ t'" using calculation by fastforce
ultimately have "∃t. ∃t' ∈ D ∩ {t<..} ∩ {t⇩0..}. T ω ≤ t'" by blast
}
hence "(⋃t'∈(⋃t. D ∩ {t<..} ∩ {t⇩0..}). {ω ∈ A. T ω ≤ t'}) = A" by fast
moreover have "(⋃t'∈(⋃t. D ∩ {t<..} ∩ {t⇩0..}). {ω ∈ A. T ω ≤ t'}) ∈ M" using D assms(2) sets_F_subset by (intro sets.countable_UN'', fastforce, fast)
ultimately have "A ∈ M" by argo
thus ?thesis using assms(2) unfolding sets_pre_sigma[OF assms(1)] by blast
qed
lemma pred_pre_sigmaI:
assumes "stopping_time T"
shows "(⋀t. t ≥ t⇩0 ⟹ Measurable.pred (F t) (λω. P ω ∧ T ω ≤ t)) ⟹ Measurable.pred (pre_sigma T) P"
unfolding pred_def space_pre_sigma using assms by (auto intro: sets_pre_sigmaI[OF assms(1)])
lemma sets_pre_sigmaD:
assumes "stopping_time T" "A ∈ pre_sigma T" "t ≥ t⇩0"
shows "{ω ∈ A. T ω ≤ t} ∈ sets (F t)"
using assms sets_pre_sigma by auto
lemma borel_measurable_stopping_time_pre_sigma:
assumes "stopping_time T"
shows "T ∈ borel_measurable (pre_sigma T)"
proof (intro borel_measurableI_le sets_pre_sigmaI[OF assms])
fix t t' assume asm: "t ≥ t⇩0"
{
assume "¬ t' ≥ t⇩0"
hence "{ω ∈ {x ∈ space (pre_sigma T). T x ≤ t'}. T ω ≤ t} = {}" using assms dual_order.trans[of _ t' "t⇩0"] unfolding stopping_time_def by fastforce
hence "{ω ∈ {x ∈ space (pre_sigma T). T x ≤ t'}. T ω ≤ t} ∈ sets (F t)" by (metis sets.empty_sets)
}
moreover
{
assume asm': "t' ≥ t⇩0"
have "{ω ∈ space (F (min t' t)). T ω ≤ min t' t} ∈ sets (F (min t' t))"
using assms asm asm' unfolding pred_def[symmetric] by (intro stopping_timeD) auto
also have "… ⊆ sets (F t)"
using assms asm asm' by (intro sets_F_mono) auto
finally have "{ω ∈ {x ∈ space (pre_sigma T). T x ≤ t'}. T ω ≤ t} ∈ sets (F t)"
using asm asm' by simp
}
ultimately show "{ω ∈ {x ∈ space (pre_sigma T). T x ≤ t'}. T ω ≤ t} ∈ sets (F t)" by blast
qed
lemma mono_pre_sigma:
assumes "stopping_time T" "stopping_time S"
and "⋀x. x ∈ space M ⟹ T x ≤ S x"
shows "pre_sigma T ⊆ pre_sigma S"
proof
fix A assume "A ∈ pre_sigma T"
hence asm: "A ∈ sets M" "t ≥ t⇩0 ⟹ {ω ∈ A. T ω ≤ t} ∈ sets (F t)" for t using assms sets_pre_sigma by blast+
{
fix t assume asm': "t ≥ t⇩0"
then have "A ⊆ space M" using sets.sets_into_space asm by blast
have "{ω∈A. T ω ≤ t} ∩ {ω∈space (F t). S ω ≤ t} ∈ sets (F t)"
using asm asm' stopping_timeD[OF assms(2)] by (auto simp: pred_def)
also have "{ω∈A. T ω ≤ t} ∩ {ω∈space (F t). S ω ≤ t} = {ω∈A. S ω ≤ t}"
using sets.sets_into_space[OF asm(1)] assms(3) order_trans asm' by fastforce
finally have "{ω∈A. S ω ≤ t} ∈ sets (F t)" by simp
}
thus "A ∈ pre_sigma S" by (intro sets_pre_sigmaI assms asm) blast
qed
lemma stopping_time_measurable_le:
assumes "stopping_time T" "s ≥ t⇩0" "t ≥ s"
shows "Measurable.pred (F t) (λω. T ω ≤ s)"
using assms stopping_timeD[of T] sets_F_mono[of _ t] by (auto simp: pred_def)
lemma stopping_time_measurable_less:
assumes "stopping_time T" "s ≥ t⇩0" "t ≥ s"
shows "Measurable.pred (F t) (λω. T ω < s)"
proof -
have "Measurable.pred (F t) (λω. T ω < t)" if asm: "stopping_time T" "t ≥ t⇩0" for T t
proof -
obtain D :: "'b set" where D: "countable D" "⋀X. open X ⟹ X ≠ {} ⟹ D ∩ X ≠ {}" by (metis countable_dense_setE disjoint_iff)
show ?thesis
proof cases
assume *: "∀t'∈{t⇩0..<t}. {t'<..<t} ≠ {}"
hence **: "D ∩ {t'<..< t} ≠ {}" if "t' ∈ {t⇩0..<t}" for t' using that by (intro D(2)) fastforce+
show ?thesis
proof (rule measurable_cong[THEN iffD2])
show "T ω < t ⟷ (∃r∈D ∩ {t⇩0..<t}. T ω ≤ r)" if "ω ∈ space (F t)" for ω
using **[of "T ω"] that less_imp_le stopping_time_ge_zero asm by fastforce
show "Measurable.pred (F t) (λw. ∃r∈D ∩ {t⇩0..<t}. T w ≤ r)"
using stopping_time_measurable_le asm D by (intro measurable_pred_countable) auto
qed
next
assume "¬ (∀t'∈{t⇩0..<t}. {t'<..<t} ≠ {})"
then obtain t' where t': "t' ∈ {t⇩0..<t}" "{t'<..<t} = {}" by blast
show ?thesis
proof (rule measurable_cong[THEN iffD2])
show "T ω < t ⟷ T ω ≤ t'" for ω using t' by (metis atLeastLessThan_iff emptyE greaterThanLessThan_iff linorder_not_less order.strict_trans1)
show "Measurable.pred (F t) (λw. T w ≤ t')" using t' by (intro stopping_time_measurable_le[OF asm(1)]) auto
qed
qed
qed
thus ?thesis
using assms sets_F_mono[of _ t] by (auto simp add: pred_def)
qed
lemma stopping_time_measurable_ge:
assumes "stopping_time T" "s ≥ t⇩0" "t ≥ s"
shows "Measurable.pred (F t) (λω. T ω ≥ s)"
by (auto simp: not_less[symmetric] intro: stopping_time_measurable_less[OF assms] Measurable.pred_intros_logic)
lemma stopping_time_measurable_gr:
assumes "stopping_time T" "s ≥ t⇩0" "t ≥ s"
shows "Measurable.pred (F t) (λx. s < T x)"
by (auto simp add: not_le[symmetric] intro: stopping_time_measurable_le[OF assms] Measurable.pred_intros_logic)
lemma stopping_time_measurable_eq:
assumes "stopping_time T" "s ≥ t⇩0" "t ≥ s"
shows "Measurable.pred (F t) (λω. T ω = s)"
unfolding eq_iff using stopping_time_measurable_le[OF assms] stopping_time_measurable_ge[OF assms]
by (intro pred_intros_logic)
lemma stopping_time_less_stopping_time:
assumes "stopping_time T" "stopping_time S"
shows "Measurable.pred (pre_sigma T) (λω. T ω < S ω)"
proof (rule pred_pre_sigmaI)
fix t assume asm: "t ≥ t⇩0"
obtain D :: "'b set" where D: "countable D" and semidense_D: "⋀x y. x < y ⟹ (∃b∈D. x ≤ b ∧ b < y)"
using countable_separating_set_linorder2 by auto
show "Measurable.pred (F t) (λω. T ω < S ω ∧ T ω ≤ t)"
proof (rule measurable_cong[THEN iffD2])
let ?f = "λω. if T ω = t then ¬ S ω ≤ t else ∃s∈D ∩ {t⇩0..t}. T ω ≤ s ∧ ¬ (S ω ≤ s)"
{
fix ω assume "ω ∈ space (F t)" "T ω ≤ t" "T ω ≠ t" "T ω < S ω"
hence "t⇩0 ≤ T ω" "T ω < min t (S ω)" using asm stopping_time_ge_zero[OF assms(1)] by auto
then obtain r where "r ∈ D" "t⇩0 ≤ r" "T ω ≤ r" "r < min t (S ω)" using semidense_D order_trans by blast
hence "∃s∈D ∩ {t⇩0..t}. T ω ≤ s ∧ s < S ω" by auto
}
thus "(T ω < S ω ∧ T ω ≤ t) = ?f ω" if "ω ∈ space (F t)" for ω using that by force
show "Measurable.pred (F t) ?f"
using assms asm D
by (intro pred_intros_logic measurable_If measurable_pred_countable countable_Collect
stopping_time_measurable_le predE stopping_time_measurable_eq) auto
qed
qed (intro assms)
end
lemma (in enat_filtered_measure) stopping_time_SUP_enat:
fixes T :: "nat ⇒ ('a ⇒ enat)"
shows "(⋀i. stopping_time (T i)) ⟹ stopping_time (SUP i. T i)"
unfolding stopping_time_def SUP_apply SUP_le_iff by (auto intro!: pred_intros_countable)
lemma (in enat_filtered_measure) stopping_time_Inf_enat:
assumes "⋀i. Measurable.pred (F i) (P i)"
shows "stopping_time (λω. Inf {i. P i ω})"
proof -
{
fix t :: enat assume asm: "t ≠ ∞"
moreover
{
fix i ω assume "Inf {i. P i ω} ≤ t"
moreover have "a < eSuc b ⟷ (a ≤ b ∧ a ≠ ∞)" for a b by (cases a) auto
ultimately have "(∃i≤t. P i ω)" using asm unfolding Inf_le_iff by (cases t) (auto elim!: allE[of _ "eSuc t"])
}
ultimately have *: "⋀ω. Inf {i. P i ω} ≤ t ⟷ (∃i∈{..t}. P i ω)" by (auto intro!: Inf_lower2)
have "Measurable.pred (F t) (λω. Inf {i. P i ω} ≤ t)" unfolding * using sets_F_mono assms by (intro pred_intros_countable_bounded) (auto simp: pred_def)
}
moreover have "Measurable.pred (F t) (λω. Inf {i. P i ω} ≤ t)" if "t = ∞" for t using that by simp
ultimately show ?thesis by (blast intro: stopping_timeI[OF i0_lb])
qed
lemma (in nat_filtered_measure) stopping_time_Inf_nat:
assumes "⋀i. Measurable.pred (F i) (P i)"
"⋀i ω. ω ∈ space M ⟹ ∃n. P n ω"
shows "stopping_time (λω. Inf {i. P i ω})"
proof (rule stopping_time_cong[THEN iffD2])
show "stopping_time (λx. LEAST n. P n x)"
proof
fix t
have "((LEAST n. P n ω) ≤ t) = (∃i≤t. P i ω)" if "ω ∈ space M" for ω by (rule LeastI2_wellorder_ex[OF assms(2)[OF that]]) auto
moreover have "Measurable.pred (F t) (λw. ∃i∈{..t}. P i w)" using sets_F_mono[of _ t] assms by (intro pred_intros_countable_bounded) (auto simp: pred_def)
ultimately show "Measurable.pred (F t) (λω. (LEAST n. P n ω) ≤ t)" by (subst measurable_cong[of "F t"]) auto
qed (simp)
qed (simp add: Inf_nat_def)
definition stopped_value :: "('b ⇒ 'a ⇒ 'c) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'c)" where
"stopped_value X τ ω = X (τ ω) ω"
subsection ‹Hitting Time›
text ‹Given a stochastic process ‹X› and a borel set ‹A›, ‹hitting_time X A s t› is the first time ‹X› is in ‹A› after time ‹s› and before time ‹t›.
If ‹X› does not hit ‹A› after time ‹s› and before ‹t› then the hitting time is simply ‹t›. The definition presented here coincides with the definition of hitting times in mathlib \<^cite>‹"ying2022formalization"›.›
context linearly_filtered_measure
begin
definition hitting_time :: "('b ⇒ 'a ⇒ 'c) ⇒ 'c set ⇒ 'b ⇒ 'b ⇒ ('a ⇒ 'b)" where
"hitting_time X A s t = (λω. if ∃i∈{s..t} ∩ {t⇩0..}. X i ω ∈ A then Inf ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}) else max t⇩0 t)"
lemma hitting_time_def':
"hitting_time X A s t = (λω. Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A})))"
proof cases
assume asm: "t⇩0 ≤ s ∧ s ≤ t"
hence "{s..t} ∩ {t⇩0..} = {s..t}" by simp
{
fix ω
assume *: "{s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A} ≠ {}"
then obtain i where "i ∈ {s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}" by blast
hence "Inf ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}) ≤ t" by (intro cInf_lower[of i, THEN order_trans]) auto
hence "Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A})) = Inf ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A})" using asm * inf_absorb2 by (subst cInf_insert_If) force+
also have "... = hitting_time X A s t ω" using * unfolding hitting_time_def by auto
finally have "hitting_time X A s t ω = Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}))" by argo
}
moreover
{
fix ω
assume "{s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A} = {}"
hence "hitting_time X A s t ω = Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}))" unfolding hitting_time_def by auto
}
ultimately show ?thesis by fast
next
assume "¬ (t⇩0 ≤ s ∧ s ≤ t)"
moreover
{
assume asm: "s < t⇩0" "t ≥ t⇩0"
hence "{s..t} ∩ {t⇩0..} = {t⇩0..t}" by simp
{
fix ω
assume *: "{s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A} ≠ {}"
then obtain i where "i ∈ {s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}" by blast
hence "Inf ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}) ≤ t" by (intro cInf_lower[of i, THEN order_trans]) auto
hence "Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A})) = Inf ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A})" using asm * inf_absorb2 by (subst cInf_insert_If) force+
also have "... = hitting_time X A s t ω" using * unfolding hitting_time_def by auto
finally have "hitting_time X A s t ω = Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}))" by argo
}
moreover
{
fix ω
assume "{s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A} = {}"
hence "hitting_time X A s t ω = Inf (insert (max t⇩0 t) ({s..t} ∩ {t⇩0..} ∩ {i. X i ω ∈ A}))" unfolding hitting_time_def by auto
}
ultimately have ?thesis by fast
}
moreover have ?thesis if "s < t⇩0" "t < t⇩0" using that unfolding hitting_time_def by auto
moreover have ?thesis if "s > t" using that unfolding hitting_time_def by auto
ultimately show ?thesis by fastforce
qed
lemma hitting_time_inj_on:
assumes "inj_on f S" "⋀ω t. t ≥ t⇩0 ⟹ X t ω ∈ S" "A ⊆ S"
shows "hitting_time X A = hitting_time (λt ω. f (X t ω)) (f ` A)"
proof -
have "X t ω ∈ A ⟷ f (X t ω) ∈ f ` A" if "t ≥ t⇩0" for t ω using assms that inj_on_image_mem_iff by meson
hence "{t⇩0..} ∩ {i. X i ω ∈ A} = {t⇩0..} ∩ {i. f (X i ω) ∈ f ` A}" for ω by blast
thus ?thesis unfolding hitting_time_def' Int_assoc by presburger
qed
lemma hitting_time_translate:
fixes c :: "_ :: ab_group_add"
shows "hitting_time X A = hitting_time (λn ω. X n ω + c) (((+) c) ` A)"
by (subst hitting_time_inj_on[OF inj_on_add, of _ UNIV]) (simp add: add.commute)+
lemma hitting_time_le:
assumes "t ≥ t⇩0"
shows "hitting_time X A s t ω ≤ t"
unfolding hitting_time_def' using assms
by (intro cInf_lower[of "max t⇩0 t", THEN order_trans]) auto
lemma hitting_time_ge:
assumes "t ≥ t⇩0" "s ≤ t"
shows "s ≤ hitting_time X A s t ω"
unfolding hitting_time_def' using assms
by (intro le_cInf_iff[THEN iffD2]) auto
lemma hitting_time_mono:
assumes "t ≥ t⇩0" "s ≤ s'" "t ≤ t'"
shows "hitting_time X A s t ω ≤ hitting_time X A s' t' ω"
unfolding hitting_time_def' using assms by (fastforce intro!: cInf_mono)
end
context nat_filtered_measure
begin
lemma stopping_time_hitting_time:
assumes "adapted_process M F 0 X" "A ∈ borel"
shows "stopping_time (hitting_time X A s t)"
proof -
interpret adapted_process M F 0 X by (rule assms)
have "insert t ({s..t} ∩ {i. X i ω ∈ A}) = {i. i = t ∨ i ∈ ({s..t} ∩ {i. X i ω ∈ A})}" for ω by blast
hence "hitting_time X A s t = (λω. Inf {i. i = t ∨ i ∈ ({s..t} ∩ {i. X i ω ∈ A})})" unfolding hitting_time_def' by simp
thus ?thesis using assms by (auto intro: stopping_time_Inf_nat)
qed
lemma stopping_time_hitting_time':
assumes "adapted_process M F 0 X" "A ∈ borel" "stopping_time s" "⋀ω. s ω ≤ t"
shows "stopping_time (λω. hitting_time X A (s ω) t ω)"
proof -
interpret adapted_process M F 0 X by (rule assms)
{
fix n
have "s ω ≤ hitting_time X A (s ω) t ω" if "s ω > n" for ω using hitting_time_ge[OF _ assms(4)] by simp
hence "(⋃i∈{n<..}. {ω. s ω = i} ∩ {ω. hitting_time X A i t ω ≤ n}) = {}" by fastforce
hence *: "(λω. hitting_time X A (s ω) t ω ≤ n) = (λω. ∃i≤n. s ω = i ∧ hitting_time X A i t ω ≤ n)" by force
have "Measurable.pred (F n) (λω. s ω = i ∧ hitting_time X A i t ω ≤ n)" if "i ≤ n" for i
proof -
have "Measurable.pred (F i) (λω. s ω = i)" using stopping_time_measurable_eq assms by blast
hence "Measurable.pred (F n) (λω. s ω = i)" by (meson less_eq_nat.simps measurable_from_subalg subalgebra_F that)
moreover have "Measurable.pred (F n) (λω. hitting_time X A i t ω ≤ n)" using stopping_timeD[OF stopping_time_hitting_time, OF assms(1,2)] by blast
ultimately show ?thesis by auto
qed
hence "Measurable.pred (F n) (λω. ∃i≤n. s ω = i ∧ hitting_time X A i t ω ≤ n)" by (intro pred_intros_countable) auto
hence "Measurable.pred (F n) (λω. hitting_time X A (s ω) t ω ≤ n)" using * by argo
}
thus ?thesis by (intro stopping_timeI) auto
qed
lemma stopped_value_hitting_time_mem:
assumes "j ∈ {s..t}" "X j ω ∈ A"
shows "stopped_value X (hitting_time X A s t) ω ∈ A"
proof -
have "∃i∈{s..t} ∩ {0..}. X i ω ∈ A" using assms by blast
moreover have "Inf ({s..t} ∩ {i. X i ω ∈ A}) ∈ {s..t} ∩ {i. X i ω ∈ A}" using assms by (blast intro!: Inf_nat_def1)
ultimately show ?thesis unfolding hitting_time_def stopped_value_def by simp
qed
lemma hitting_time_le_iff:
assumes "i < t"
shows "hitting_time X A s t ω ≤ i ⟷ (∃j ∈ {s..i}. X j ω ∈ A)" (is "?lhs = ?rhs")
proof
assume ?lhs
moreover have "hitting_time X A s t ω ∈ insert t ({s..t} ∩ {i. X i ω ∈ A})" by (metis hitting_time_def' Int_atLeastAtMostR2 inf_sup_aci(1) insertI1 max_0L wellorder_InfI)
ultimately have "hitting_time X A s t ω ∈ {s..i} ∩ {i. X i ω ∈ A}" using assms by force
thus ?rhs by blast
next
assume ?rhs
then obtain j where j: "j ∈ {s..i}" "X j ω ∈ A" by blast
hence "hitting_time X A s t ω ≤ j" unfolding hitting_time_def' using assms by (auto intro: cInf_lower)
thus ?lhs using j by simp
qed
lemma hitting_time_less_iff:
assumes "i ≤ t"
shows "hitting_time X A s t ω < i ⟷ (∃j ∈ {s..<i}. X j ω ∈ A)" (is "?lhs = ?rhs")
proof
assume ?lhs
moreover have "hitting_time X A s t ω ∈ insert t ({s..t} ∩ {i. X i ω ∈ A})" by (metis hitting_time_def' Int_atLeastAtMostR2 inf_sup_aci(1) insertI1 max_0L wellorder_InfI)
ultimately have "hitting_time X A s t ω ∈ {s..<i} ∩ {i. X i ω ∈ A}" using assms by force
thus ?rhs by blast
next
assume ?rhs
then obtain j where j: "j ∈ {s..<i}" "X j ω ∈ A" by blast
hence "hitting_time X A s t ω ≤ j" unfolding hitting_time_def' using assms by (auto intro: cInf_lower)
thus ?lhs using j by simp
qed
lemma hitting_time_eq_hitting_time:
assumes "t ≤ t'" "j ∈ {s..t}" "X j ω ∈ A"
shows "hitting_time X A s t ω = hitting_time X A s t' ω" (is "?lhs = ?rhs")
proof -
have "hitting_time X A s t ω ∈ {s..t'}" using hitting_time_le[THEN order_trans, of t t' X A s] hitting_time_ge[of t s X A] assms by auto
moreover have "stopped_value X (hitting_time X A s t) ω ∈ A" by (blast intro: stopped_value_hitting_time_mem assms)
ultimately have "hitting_time X A s t' ω ≤ hitting_time X A s t ω" by (fastforce simp add: hitting_time_def'[where t=t'] stopped_value_def intro!: cInf_lower)
thus ?thesis by (blast intro: le_antisym hitting_time_mono[OF _ order_refl assms(1)])
qed
end
end