English
The Mellin inverse transform interacts with cpow-scalar-smoothing via a shift relation in the frequency-like variable.
Русский
Обратное преобразование Меллина взаимодействует с cpow-масштабированием через сдвиг в частотной переменной.
LaTeX
$$$\text{mellin}(t \mapsto t^a f(t), s) = \text{mellin}(f, s+a)$$$
Lean4
/-- The Mellin inverse transform of a function `f`, defined as `1 / (2π)` times
the integral of `y ↦ x ^ -(σ + yi) • f (σ + yi)`. -/
def mellinInv (σ : ℝ) (f : ℂ → E) (x : ℝ) : E :=
(1 / (2 * π)) •
∫ y : ℝ,
(x : ℂ) ^ (-(σ + y * I)) •
f
(σ + y * I)
-- next few lemmas don't require convergence of the Mellin transform (they are just 0 = 0 otherwise)
