mellin_cpow_smul — Mathlib

English

The Mellin inverse transform equals a Fourier-type inversion formula with a complex power factor and a Fourier inverse transform.

Русский

Обратное преобразование Меллина выражается через формулу свёртки Фурье с комплексной степенью и обратным Фурье-преобразованием.

LaTeX

$$$\text{mellinInv}(\sigma,f,x) = x^{-\sigma} \cdot \mathcal{F}^{-1}\big( f(\sigma + 2\pi y i) \big)(-\log x)$$$

Lean4

theorem mellin_cpow_smul (f : ℝ → E) (s a : ℂ) : mellin (fun t => (t : ℂ) ^ a • f t) s = mellin f (s + a) :=
  by
  refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
  simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]

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