English
If N ≤ M and lowerCrossingTime a b f N n ω < N, then the upper and lower crossing times stabilize between M and N: upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω and lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω.
Русский
Если N ≤ M и lowerCrossingTime a b f N n ω < N, то верхнее и нижнее время пересечения стабилизируются между M и N.
LaTeX
$$$N\\le M\\;\\land\\; \\mathrm{lowerCrossingTime}(a,b,f,N,n,\\omega) < N\\Rightarrow \\mathrm{upperCrossingTime}(a,b,f,M,n,\\omega) = \\mathrm{upperCrossingTime}(a,b,f,N,n,\\omega)\\land\\mathrm{lowerCrossingTime}(a,b,f,M,n,\\omega) = \\mathrm{lowerCrossingTime}(a,b,f,N,n,\\omega).$$$
Lean4
theorem crossing_eq_crossing_of_lowerCrossingTime_lt {M : ℕ} (hNM : N ≤ M) (h : lowerCrossingTime a b f N n ω < N) :
upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω ∧
lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω :=
by
have h' : upperCrossingTime a b f N n ω < N := lt_of_le_of_lt upperCrossingTime_le_lowerCrossingTime h
induction n with
| zero =>
simp only [upperCrossingTime_zero, bot_eq_zero', lowerCrossingTime_zero, true_and, eq_comm]
refine hitting_eq_hitting_of_exists hNM ?_
rw [lowerCrossingTime, hitting_lt_iff] at h
· obtain ⟨j, hj₁, hj₂⟩ := h
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
· exact le_rfl
| succ k
ih =>
specialize
ih (lt_of_le_of_lt (lowerCrossingTime_mono (Nat.le_succ _)) h)
(lt_of_le_of_lt (upperCrossingTime_mono (Nat.le_succ _)) h')
have : upperCrossingTime a b f M k.succ ω = upperCrossingTime a b f N k.succ ω :=
by
rw [upperCrossingTime_succ_eq, hitting_lt_iff] at h'
· simp only [upperCrossingTime_succ_eq]
obtain ⟨j, hj₁, hj₂⟩ := h'
rw [eq_comm, ih.2]
exact hitting_eq_hitting_of_exists hNM ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
· exact le_rfl
refine ⟨this, ?_⟩
simp only [lowerCrossingTime, eq_comm, this, Nat.succ_eq_add_one]
refine hitting_eq_hitting_of_exists hNM ?_
rw [lowerCrossingTime, hitting_lt_iff _ le_rfl] at h
obtain ⟨j, hj₁, hj₂⟩ := h
exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
