mellin_comp_mul_right — Mathlib

English

If a > 0, then Mellin(f(t a))(s) = a^{-s} Mellin(f)(s).

Русский

Если a > 0, то преобразование Меллина функции t ↦ f(t a) в точке s равно a^{-s} умножению преобразования Меллина f в s.

LaTeX

$$$\operatorname{mellin}(f(t a))(s) = a^{-s} \operatorname{mellin}(f)(s),\quad a>0$$$

Lean4

theorem mellin_comp_mul_right (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) :
    mellin (fun t => f (t * a)) s = (a : ℂ) ^ (-s) • mellin f s := by
  simpa only [mul_comm] using mellin_comp_mul_left f s ha

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