English
There exists p > 0 such that F_nat(0, a, t) - (if a = 0 then 1 else 0) is Big-O of exp(-p t) as t → ∞, uniformly for a with a ≤ 0.
Русский
Существует p > 0 такое, что F_nat(0,a,t) - (if a=0 then 1 else 0) = O(exp(-p t)) при t→∞, равномерно по a с a ≤ 0.
LaTeX
$$$\exists p>0:\ (F_{nat}(0,a,t) - (\mathbf{1}_{a=0})) = O_{\text{atTop}}(e^{-p t})$.$$
Lean4
theorem isBigO_atTop_F_nat_zero_sub {a : ℝ} (ha : 0 ≤ a) :
∃ p, 0 < p ∧ (fun t ↦ F_nat 0 a t - (if a = 0 then 1 else 0)) =O[atTop] fun t ↦ exp (-p * t) :=
by
split_ifs with h
· rw [h]
have : (fun t ↦ F_nat 0 0 t - 1) =O[atTop] fun t ↦ rexp (-π * t) / (1 - rexp (-π * t)) :=
by
apply Eventually.isBigO
filter_upwards [eventually_gt_atTop 0] with t ht
exact F_nat_zero_zero_sub_le ht
refine ⟨_, pi_pos, this.trans ?_⟩
simpa using (isBigO_refl (fun t ↦ rexp (-π * t)) _).mul isBigO_one_aux
· simp_rw [sub_zero]
have : (fun t ↦ F_nat 0 a t) =O[atTop] fun t ↦ rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t)) :=
by
apply Eventually.isBigO
filter_upwards [eventually_gt_atTop 0] with t ht
exact F_nat_zero_le ha ht
refine ⟨π * a ^ 2, mul_pos pi_pos (sq_pos_of_ne_zero h), this.trans ?_⟩
simpa only [neg_mul π (a ^ 2), mul_one] using (isBigO_refl _ _).mul isBigO_one_aux
