English
If f is locally integrable, decays exponentially at infinity, and is O(x^{-b}) at 0 with b < s.re, then Mellin converges for s.re > b.
Русский
Если f локально интегрируема, экспоненциально убывает на бесконечности и имеет O(x^{-b}) около 0 с b < Re(s), тогда преобразование Меллина сходится при Re(s) > b.
LaTeX
$$$\text{MellinConvergent}(f,s) \text{ for } \Re(s) > b.$$$
Lean4
/-- If `f` is locally integrable, decays exponentially at infinity, and is `O(x ^ (-b))` at 0, then
its Mellin transform converges for `b < s.re`. -/
theorem mellinConvergent_of_isBigO_rpow_exp [NormedSpace ℂ E] {a b : ℝ} (ha : 0 < a) {f : ℝ → E} {s : ℂ}
(hfc : LocallyIntegrableOn f <| Ioi 0) (hf_top : f =O[atTop] fun t => exp (-a * t))
(hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s.re) : MellinConvergent f s :=
mellinConvergent_of_isBigO_rpow hfc (hf_top.trans (isLittleO_exp_neg_mul_rpow_atTop ha _).isBigO) (lt_add_one _)
hf_bot hs_bot
