English
Under the same Big-O hypotheses with s.re between a and b, the Mellin transform is differentiable with derivative given by the Mellin transform of log•f.
Русский
При тех же условиях Big-O и для области, где b < Re(s) < a, преобразование Меллина дифференцируемо, а производная равна преобразованию Меллина от log•f.
LaTeX
$$$\text{DifferentiableAt} (\operatorname{mellin} f) s \;\text{with derivative } \operatorname{mellin}(\log t\cdot f(t))(s).$$$
Lean4
/-- If `f` is locally integrable, decays exponentially at infinity, and is `O(x ^ (-b))` at 0, then
its Mellin transform is holomorphic on `b < s.re`. -/
theorem mellin_differentiableAt_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) : DifferentiableAt ℂ (mellin f) s :=
mellin_differentiableAt_of_isBigO_rpow hfc (hf_top.trans (isLittleO_exp_neg_mul_rpow_atTop ha _).isBigO)
(lt_add_one _) hf_bot hs_bot
