English
If n ≤ m and N ≤ lowerCrossingTime(a,b,f,N,n,ω), then lowerCrossingTime(a,b,f,N,m,ω) = N.
Русский
Если n ≤ m и N ≤ lowerCrossingTime(a,b,f,N,n,ω), тогда lowerCrossingTime(a,b,f,N,m,ω) = N.
LaTeX
$$$\forall n,m\; (n \le m) \land N \le lowerCrossingTime(a,b,f,N,n,ω) \Rightarrow lowerCrossingTime(a,b,f,N,m,ω) = N$$$
Lean4
theorem isStoppingTime_crossing (hf : Adapted ℱ f) :
IsStoppingTime ℱ (upperCrossingTime a b f N n) ∧ IsStoppingTime ℱ (lowerCrossingTime a b f N n) := by
induction n with
| zero =>
refine ⟨isStoppingTime_const _ 0, ?_⟩
simp [hitting_isStoppingTime hf measurableSet_Iic]
| succ k ih =>
obtain ⟨_, ih₂⟩ := ih
have : IsStoppingTime ℱ (upperCrossingTime a b f N (k + 1)) :=
by
intro n
simp_rw [upperCrossingTime_succ_eq]
exact isStoppingTime_hitting_isStoppingTime ih₂ (fun _ => lowerCrossingTime_le) measurableSet_Ici hf _
refine ⟨this, ?_⟩
intro n
exact isStoppingTime_hitting_isStoppingTime this (fun _ => upperCrossingTime_le) measurableSet_Iic hf _
