English
If f = O(x^{-a}) at infinity and s < a, then there exists c>0 such that mellin f converges on (c, ∞).
Русский
Если f = O(x^{-a}) при x → ∞ и s < a, то существует c > 0, такое что преобразование Меллина сходится на (c, ∞).
LaTeX
$$$\exists c>0\; IntegrableOn (t^{s-1} f(t)) (Ioi c).$$$
Lean4
/-- If `f` is a locally integrable real-valued function which is `O(x ^ (-a))` at `∞`, then for any
`s < a`, its Mellin transform converges on some neighbourhood of `+∞`. -/
theorem mellin_convergent_top_of_isBigO {f : ℝ → ℝ} (hfc : AEStronglyMeasurable f <| volume.restrict (Ioi 0)) {a s : ℝ}
(hf : f =O[atTop] (· ^ (-a))) (hs : s < a) :
∃ c : ℝ, 0 < c ∧ IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioi c) :=
by
obtain ⟨d, hd'⟩ := hf.isBigOWith
simp_rw [IsBigOWith, eventually_atTop] at hd'
obtain ⟨e, he⟩ := hd'
have he' : 0 < max e 1 := zero_lt_one.trans_le (le_max_right _ _)
refine ⟨max e 1, he', ?_, ?_⟩
· refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))
refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable measurableSet_Ioi
exact continuousAt_rpow_const _ _ (Or.inl <| (he'.trans ht).ne')
· have : ∀ᵐ t : ℝ ∂volume.restrict (Ioi <| max e 1), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d :=
by
refine (ae_restrict_mem measurableSet_Ioi).mono fun t ht => ?_
have ht' : 0 < t := he'.trans ht
rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc, mul_comm _ d,
norm_of_nonneg (rpow_nonneg ht'.le _)]
gcongr
exact he t ((le_max_left e 1).trans_lt ht).le
refine (HasFiniteIntegral.mul_const ?_ _).mono' this
exact (integrableOn_Ioi_rpow_of_lt (by linarith) he').hasFiniteIntegral
