mellin — Mathlib

English

Replacing f by t ↦ t^a f(t) shifts Mellin by a, i.e., Mellin of cpow-smul equals Mellin with s+a.

Русский

Замена f на t^a f(t) смещает Меллин-преобразование на a: mellin(t^a f) с параметром s равно mellin(f) с s+a.

LaTeX

$$$\forall f,s,a:\ MellinConvergent(\lambda t. t^a f(t))\, s \iff \text{MellinConvergent}(f,s+a)$$$

Lean4

/-- The Mellin transform of a function `f` (for a complex exponent `s`), defined as the integral of
`t ^ (s - 1) • f` over `Ioi 0`. -/
def mellin (f : ℝ → E) (s : ℂ) : E :=
  ∫ t : ℝ in Ioi 0, (t : ℂ) ^ (s - 1) • f t

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