mellin_comp_inv — Mathlib

English

The Mellin transform of f(t^{-1}) at s equals the Mellin transform of f at -s: mellin(f(t^{-1}))(s) = mellin(f)(-s).

Русский

Преобразование Меллина функции f( t^{-1} ) в точке s равно преобразованию Меллина функции f в точке -s: mellin(f(t^{-1}))(s) = mellin(f)(-s).

LaTeX

$$$\operatorname{mellin}(f(t^{-1}))(s) = \operatorname{mellin}(f)(-s).$$$

Lean4

theorem mellin_comp_inv (f : ℝ → E) (s : ℂ) : mellin (fun t => f t⁻¹) s = mellin f (-s) := by
  simp_rw [← rpow_neg_one, mellin_comp_rpow _ _ _, abs_neg, abs_one, inv_one, one_smul, ofReal_neg, ofReal_one, div_neg,
    div_one]

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