mellinConvergent_of_isBigO_rpow — Mathlib

English

Same as above in scalar form; the Mellin transform converges for parameters b < s < a under O-conditions.

Русский

То же самое в скалярной форме; преобразование Меллина сходится при b < s < a под условиям O.

LaTeX

$$$\text{MellinConvergent}(f,s) \iff b

Lean4

theorem mellinConvergent_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) : MellinConvergent f s :=
  by
  rw [MellinConvergent, mellin_convergent_iff_norm Subset.rfl measurableSet_Ioi hfc.aestronglyMeasurable]
  exact mellin_convergent_of_isBigO_scalar hfc.norm hf_top.norm_left hs_top hf_bot.norm_left hs_bot

Похожие утверждения