English
If f is locally integrable and decays exponentially at infinity and is O(x^{-b}) near 0 with b < s.re, then Mellin converges for s.re > b.
Русский
Если f локально интегрируема и экспоненциально убывает на бесконечности, а рядом 0 имеет оценку O(x^{-b}) с b < Re(s), то преобразование Меллина сходится для Re(s) > b.
LaTeX
$$$\text{mellinConvergent}(f,s) \text{ under exponential decay at } \infty \text{ and } b<\Re(s).$$$
Lean4
/-- If `f` is `O(x ^ (-a))` as `x → +∞`, then `log • f` is `O(x ^ (-b))` for every `b < a`. -/
theorem isBigO_rpow_top_log_smul [NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E} (hab : b < a) (hf : f =O[atTop] (· ^ (-a))) :
(fun t : ℝ => log t • f t) =O[atTop] (· ^ (-b)) :=
by
refine
((isLittleO_log_rpow_atTop (sub_pos.mpr hab)).isBigO.smul hf).congr' (Eventually.of_forall fun t => by rfl)
((eventually_gt_atTop 0).mp (Eventually.of_forall fun t ht => ?_))
simp only
rw [smul_eq_mul, ← rpow_add ht, ← sub_eq_add_neg, sub_eq_add_neg a, add_sub_cancel_left]
