English
For a on the unit circle, there exists p > 0 such that F_int(0, a, t) - (if a=0 then 1 else 0) is O(exp(-p t)) as t → ∞.
Русский
Для а на единичной окружности существует p>0, такое что F_int(0,a,t) − (если a=0, то 1; иначе 0) = O(exp(-p t)) при t→∞.
LaTeX
$$$\exists p>0:\ F_{int}(0,a,t) - (\mathbf{1}_{a=0}) = O_{atTop}(e^{-p t}).$$$
Lean4
theorem isBigO_atTop_F_int_zero_sub (a : UnitAddCircle) :
∃ p, 0 < p ∧ (fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =O[atTop] fun t ↦ exp (-p * t) :=
by
obtain ⟨a, ha, rfl⟩ := a.eq_coe_Ico
obtain ⟨p, hp, hp'⟩ := isBigO_atTop_F_nat_zero_sub ha.1
obtain ⟨q, hq, hq'⟩ := isBigO_atTop_F_nat_zero_sub (sub_nonneg.mpr ha.2.le)
simp_rw [AddCircle.coe_eq_zero_iff_of_mem_Ico ha]
simp_rw [eq_false_intro (by linarith [ha.2] : 1 - a ≠ 0), if_false, sub_zero] at hq'
refine ⟨_, lt_min hp hq, ?_⟩
have :
(fun t ↦ F_int 0 a t - (if a = 0 then 1 else 0)) =ᶠ[atTop] fun t ↦
(F_nat 0 a t - (if a = 0 then 1 else 0)) + F_nat 0 (1 - a) t :=
by
filter_upwards [eventually_gt_atTop 0] with t ht
rw [F_int_eq_of_mem_Icc 0 (Ico_subset_Icc_self ha) ht]
ring
refine this.isBigO.trans ((hp'.trans ?_).add (hq'.trans ?_)) <;> apply isBigO_exp_neg_mul_of_le
exacts [min_le_left .., min_le_right ..]
