English
If a > 0, then Mellin(f(a t))(s) = a^{-s} Mellin(f)(s).
Русский
Если a > 0, то преобразование Меллина функции t ↦ f(a t) в точке s равно a^{-s} умножению преобразования Меллина f в s.
LaTeX
$$$\operatorname{mellin}(f(a t))(s) = a^{-s} \operatorname{mellin}(f)(s),\quad a>0$$$
Lean4
theorem mellin_comp_mul_left (f : ℝ → E) (s : ℂ) {a : ℝ} (ha : 0 < a) :
mellin (fun t => f (a * t)) s = (a : ℂ) ^ (-s) • mellin f s :=
by
simp_rw [mellin]
have :
EqOn (fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t))
(fun t : ℝ => (a : ℂ) ^ (1 - s) • (fun u : ℝ => (u : ℂ) ^ (s - 1) • f u) (a * t)) (Ioi 0) :=
fun t ht ↦ by
dsimp only
rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul, (by ring : 1 - s = -(s - 1)), cpow_neg,
inv_mul_cancel_left₀]
rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]
exact Or.inl ha.ne'
rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha, mul_zero, ← Complex.coe_smul, ← mul_smul,
sub_eq_add_neg, cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv, mul_assoc, mul_comm,
inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')]
