English
Under a modified Big-O condition at infinity, convergence near infinity follows from the top Big-O form.
Русский
При модифицированном условии Big-O на бесконечности сходящесть следует из верхней формы Big-O.
LaTeX
$$$\exists c>0,\; IntegrableOn (t^{s-1} f(t)) (Ioi c).$$$
Lean4
/-- Suppose `f` is locally integrable on `(0, ∞)`, is `O(x ^ (-a))` as `x → ∞`, and is
`O(x ^ (-b))` as `x → 0`. Then its Mellin transform is differentiable on the domain `b < re s < a`.
-/
theorem mellin_differentiableAt_of_isBigO_rpow [NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ}
(hfc : LocallyIntegrableOn f <| Ioi 0) (hf_top : f =O[atTop] (· ^ (-a))) (hs_top : s.re < a)
(hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s.re) : DifferentiableAt ℂ (mellin f) s :=
(mellin_hasDerivAt_of_isBigO_rpow hfc hf_top hs_top hf_bot hs_bot).2.differentiableAt
