English
There exists p > 0 such that F_nat(1, a, t) = O_atTop exp(-p t) for a ≤ 0 and t > 0.
Русский
Существует p > 0 такое, что F_nat(1,a,t) = O_atTop(exp(-p t)) при a ≤ 0 и t > 0.
LaTeX
$$$\exists p>0:\ F_{nat}(1,a,t) = O_{\text{atTop}}(e^{-p t}) \ (a \le 0, \; t>0).$$$
Lean4
theorem isBigO_atTop_F_nat_one {a : ℝ} (ha : 0 ≤ a) : ∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t ↦ exp (-p * t) :=
by
suffices
∃ p,
0 < p ∧
(fun t ↦
rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 +
a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop]
fun t ↦ exp (-p * t)
by
let ⟨p, hp, hp'⟩ := this
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
filter_upwards [eventually_gt_atTop 0] with t ht
exact F_nat_one_le ha ht
have aux' : IsBigO atTop (fun t : ℝ ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) (fun _ ↦ (1 : ℝ)) := by
simpa only [inv_pow, one_pow] using isBigO_one_aux.pow 2
rcases eq_or_lt_of_le ha with rfl | ha'
·
exact
⟨_, pi_pos, by
simpa only [zero_pow two_ne_zero, zero_add, mul_one, zero_mul, zero_div, add_zero] using
(isBigO_refl _ _).mul aux'⟩
· refine ⟨π * a ^ 2, mul_pos pi_pos <| pow_pos ha' _, IsBigO.add ?_ ?_⟩
· conv_rhs => enter [t]; rw [← mul_one (rexp _)]
refine (Eventually.isBigO ?_).mul aux'
filter_upwards [eventually_gt_atTop 0] with t ht
rw [norm_of_nonneg (exp_pos _).le, exp_le_exp]
nlinarith [pi_pos]
· simp_rw [mul_div_assoc, ← neg_mul]
apply IsBigO.const_mul_left
simpa only [mul_one] using (isBigO_refl _ _).mul isBigO_one_aux
