English
If f = O(x^{-b}) near 0 and b < s, there exists c>0 such that mellin f converges on (0,c].
Русский
Если f = O(x^{-b}) около 0 и b < s, существует c>0, такое что преобразование Меллина сходится на (0, c].
LaTeX
$$$\exists c>0\; IntegrableOn (t^{s-1} f(t)) (Ioc 0 c).$$$
Lean4
/-- If `f` is a locally integrable real-valued function which is `O(x ^ (-b))` at `0`, then for any
`b < s`, its Mellin transform converges on some right neighbourhood of `0`. -/
theorem mellin_convergent_zero_of_isBigO {b : ℝ} {f : ℝ → ℝ} (hfc : AEStronglyMeasurable f <| volume.restrict (Ioi 0))
(hf : f =O[𝓝[>] 0] (· ^ (-b))) {s : ℝ} (hs : b < s) :
∃ c : ℝ, 0 < c ∧ IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioc 0 c) :=
by
obtain ⟨d, _, hd'⟩ := hf.exists_pos
simp_rw [IsBigOWith, eventually_nhdsWithin_iff, Metric.eventually_nhds_iff, gt_iff_lt] at hd'
obtain ⟨ε, hε, hε'⟩ := hd'
refine ⟨ε, hε, Iff.mpr integrableOn_Ioc_iff_integrableOn_Ioo ⟨?_, ?_⟩⟩
· refine AEStronglyMeasurable.mul ?_ (hfc.mono_set Ioo_subset_Ioi_self)
refine (continuousOn_of_forall_continuousAt fun t ht => ?_).aestronglyMeasurable measurableSet_Ioo
exact continuousAt_rpow_const _ _ (Or.inl ht.1.ne')
· apply HasFiniteIntegral.mono'
· change HasFiniteIntegral (fun t => d * t ^ (s - b - 1)) _
refine (Integrable.hasFiniteIntegral ?_).const_mul _
rw [← IntegrableOn, ← integrableOn_Ioc_iff_integrableOn_Ioo, ←
intervalIntegrable_iff_integrableOn_Ioc_of_le hε.le]
exact intervalIntegral.intervalIntegrable_rpow' (by linarith)
· refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)
rw [mul_comm, norm_mul]
specialize hε' _ ht.1
· rw [dist_eq_norm, sub_zero, norm_of_nonneg (le_of_lt ht.1)]
exact ht.2
· calc
_ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
_ = d * t ^ (s - b - 1) := ?_
simp_rw [norm_of_nonneg (rpow_nonneg (le_of_lt ht.1) _), mul_assoc]
rw [← rpow_add ht.1]
congr 2
abel
