The Mellin transform

We define the Mellin transform of a locally integrable function on Ioi 0, and show it is differentiable in a suitable vertical strip.

Main statements

• mellin : the Mellin transform ∫ (t : ℝ) in Ioi 0, t ^ (s - 1) • f t, where s is a complex number.
• HasMellin: shorthand asserting that the Mellin transform exists and has a given value (analogous to HasSum).
• mellin_differentiableAt_of_isBigO_rpow : if f is O(x ^ (-a)) at infinity, and O(x ^ (-b)) at 0, then mellin f is holomorphic on the domain b < re s < a.

theorem stronglyMeasurable_mellin {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : ℝ → E) : MeasureTheory.StronglyMeasurable (mellin f)

The Mellin transform of any function is strongly measurable, with no hypotheses on f: either f is a.e. strongly measurable on Ioi 0 and the parametric-integral machinery applies, or the integrand is non-measurable for every s (the kernel x ^ (s - 1) never vanishes on Ioi 0), so mellin f ≡ 0.