English
There is a positional equality between upper crossing times for shifted functions: crossing_pos_eq relates (f(n) − a)⁺ with upperCrossingTime for a shifted argument.
Русский
Существует равенство положения верхнего времени пересечения для сдвинутых функций.
LaTeX
$$$\\text{CrossingPos Eq}: \\text{see precise equality in lemma }(\\text{crossing_pos_eq}).$$$
Lean4
theorem crossing_pos_eq (hab : a < b) :
upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = upperCrossingTime a b f N n ∧
lowerCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N n = lowerCrossingTime a b f N n :=
by
have hab' : 0 < b - a := sub_pos.2 hab
have hf : ∀ ω i, b - a ≤ (f i ω - a)⁺ ↔ b ≤ f i ω := by
intro i ω
refine ⟨fun h => ?_, fun h => ?_⟩
· rwa [← sub_le_sub_iff_right a, ← posPart_eq_of_posPart_pos (lt_of_lt_of_le hab' h)]
· rw [← sub_le_sub_iff_right a] at h
rwa [posPart_eq_self.2 (le_trans hab'.le h)]
have hf' (ω i) : (f i ω - a)⁺ ≤ 0 ↔ f i ω ≤ a := by rw [posPart_nonpos, sub_nonpos]
induction n with
| zero =>
refine ⟨rfl, ?_⟩
simp +unfoldPartialApp only [lowerCrossingTime_zero, hitting, Set.mem_Icc, Set.mem_Iic]
simp_all
| succ k
ih =>
have : upperCrossingTime 0 (b - a) (fun n ω => (f n ω - a)⁺) N (k + 1) = upperCrossingTime a b f N (k + 1) :=
by
ext ω
simp only [upperCrossingTime_succ_eq, ← ih.2, hitting, Set.mem_Ici, tsub_le_iff_right]
split_ifs with h₁ h₂ h₂
· simp_rw [← sub_le_iff_le_add, hf ω]
· refine False.elim (h₂ ?_)
simp_all only [Set.mem_Ici, not_true_eq_false]
· refine False.elim (h₁ ?_)
simp_all only [Set.mem_Ici]
· rfl
refine ⟨this, ?_⟩
ext ω
simp only [lowerCrossingTime, this, hitting, Set.mem_Iic]
split_ifs with h₁ h₂ h₂
· simp_rw [hf' ω]
· refine False.elim (h₂ ?_)
simp_all only [Set.mem_Iic, not_true_eq_false]
· refine False.elim (h₁ ?_)
simp_all only [Set.mem_Iic]
· rfl
