English
The integrand exp(-x) x^s is little-o of exp(-x/2) as x → ∞ for any real s, i.e., exp(-x) x^s = o(exp(-x/2)) as x → ∞.
Русский
Пусть s ∈ ℝ. Интегрант exp(-x) x^s является малым по отношению к exp(-x/2) при x → ∞: exp(-x) x^s = o(exp(-x/2)).
LaTeX
$$$$ \exp(-x) x^{s} = o\_{x \to \infty} \exp(-\tfrac{1}{2} x) $$$$
Lean4
/-- Asymptotic bound for the `Γ` function integrand. -/
theorem Gamma_integrand_isLittleO (s : ℝ) : (fun x : ℝ => exp (-x) * x ^ s) =o[atTop] fun x : ℝ => exp (-(1 / 2) * x) :=
by
refine isLittleO_of_tendsto (fun x hx => ?_) ?_
· exfalso; exact (exp_pos (-(1 / 2) * x)).ne' hx
have : (fun x : ℝ => exp (-x) * x ^ s / exp (-(1 / 2) * x)) = (fun x : ℝ => exp (1 / 2 * x) / x ^ s)⁻¹ :=
by
ext1 x
simp [field, ← exp_nsmul, exp_neg]
rw [this]
exact (tendsto_exp_mul_div_rpow_atTop s (1 / 2) one_half_pos).inv_tendsto_atTop
