English
For nonpositive a, there exists p > 0 such that F_nat(0, a, t) − (1−a) is O(exp(-p t)) as t → ∞.
Русский
Для a ≤ 0 существует p>0 такое, что F_nat(0,a,t) − (1−a) = O(exp(-p t)) при t→∞.
LaTeX
$$$\exists p>0:\ F_{nat}(0, a, t) - (1 - a) = O_{atTop}(e^{-p t}).$$$
Lean4
theorem isBigO_atTop_F_int_one (a : UnitAddCircle) : ∃ p, 0 < p ∧ F_int 1 a =O[atTop] fun t ↦ exp (-p * t) :=
by
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_one ha.1
obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_one (sub_nonneg.mpr ha.2.le)
refine ⟨_, lt_min hp hq, ?_⟩
have : F_int 1 a =ᶠ[atTop] fun t ↦ F_nat 1 a t + F_nat 1 (1 - a) t :=
by
filter_upwards [eventually_gt_atTop 0] with t ht
exact F_int_eq_of_mem_Icc 1 (Ico_subset_Icc_self ha) ht
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;> apply isBigO_exp_neg_mul_of_le
exacts [min_le_left .., min_le_right ..]
