English
Let a be a nonzero real number. The Mellin transform of the function t ↦ f(t^a) at s satisfies Mellin(f(t^a))(s) = |a|^{-1} Mellin(f)(s/a). If a = 0, both sides are defined by a convention that makes them vanish.
Русский
Пусть a — ненулевое вещественное число. Преобразование Меллина функции t ↦ f(t^a) в точке s удовлетворяет равенству Mellin(f(t^a))(s) = |a|^{-1} Mellin(f)(s/a). Если a = 0, выражения определяются так, чтобы обе стороны давали нуль.
LaTeX
$$$\operatorname{mellin}(f(\cdot^{a}))(s) = |a|^{-1} \operatorname{mellin}(f)(s/a) \;.$$$
Lean4
theorem mellin_comp_rpow (f : ℝ → E) (s : ℂ) (a : ℝ) : mellin (fun t => f (t ^ a)) s = |a|⁻¹ • mellin f (s / a) := by
/- This is true for `a = 0` as all sides are undefined but turn out to vanish thanks to our
convention. The interesting case is `a ≠ 0` -/
rcases eq_or_ne a 0 with rfl | ha
· by_cases hE : CompleteSpace E
· simp [integral_smul_const, mellin, setIntegral_Ioi_zero_cpow]
· simp [integral, mellin, hE]
simp_rw [mellin]
conv_rhs => rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
dsimp only
rw [← mul_smul, ← mul_assoc, inv_mul_cancel₀ (mt abs_eq_zero.1 ha), one_mul, ← smul_assoc, real_smul]
rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
