English
If a/b give a scale between s and a with f bounded by O[x^{(-a)}] and O[x^{(-b)}] on appropriate domains, then the Mellin integral converges for s between b and a.
Русский
Если существуют оценки типа O[x^{(-a)}] и O[x^{(-b)}] на подходящих областях, то интеграл Меллина сходится для s между b и a.
LaTeX
$$$\text{MellinConvergent}(f,s)\iff b < \Re(s) < a\text{ under the given Big-O controls.}$$$
Lean4
/-- If `f` is a locally integrable real-valued function on `Ioi 0` which is `O(x ^ (-a))` at `∞`
and `O(x ^ (-b))` at `0`, then its Mellin transform integral converges for `b < s < a`. -/
theorem mellin_convergent_of_isBigO_scalar {a b : ℝ} {f : ℝ → ℝ} {s : ℝ} (hfc : LocallyIntegrableOn f <| Ioi 0)
(hf_top : f =O[atTop] (· ^ (-a))) (hs_top : s < a) (hf_bot : f =O[𝓝[>] 0] (· ^ (-b))) (hs_bot : b < s) :
IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioi 0) :=
by
obtain ⟨c1, hc1, hc1'⟩ := mellin_convergent_top_of_isBigO hfc.aestronglyMeasurable hf_top hs_top
obtain ⟨c2, hc2, hc2'⟩ := mellin_convergent_zero_of_isBigO hfc.aestronglyMeasurable hf_bot hs_bot
have : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1 := by
rw [union_assoc, Ioc_union_Ioi (le_max_right _ _), Ioc_union_Ioi ((min_le_left _ _).trans (le_max_right _ _)),
min_eq_left (lt_min hc2 hc1).le]
rw [this, integrableOn_union, integrableOn_union]
refine ⟨⟨hc2', Iff.mp integrableOn_Icc_iff_integrableOn_Ioc ?_⟩, hc1'⟩
refine
(hfc.continuousOn_mul ?_ isOpen_Ioi.isLocallyClosed).integrableOn_compact_subset
(fun t ht => (hc2.trans_le ht.1 : 0 < t)) isCompact_Icc
exact continuousOn_of_forall_continuousAt fun t ht ↦ continuousAt_rpow_const _ _ <| Or.inl <| ne_of_gt ht
