English
Replacing t by t^a in the Mellin transform corresponds to replacing s by s/a in the convergence condition.
Русский
Замена аргумента t на t^a в преобразовании Меллина эквивалентна замене параметра s на s/a в условии сходимости.
LaTeX
$$$\text{MellinConvergent}(f, s) \iff \text{MellinConvergent}(t\mapsto f(t^a), s/a)$ при a ≠ 0$$
Lean4
theorem comp_rpow {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : a ≠ 0) :
MellinConvergent (fun t => f (t ^ a)) s ↔ MellinConvergent f (s / a) :=
by
refine Iff.trans ?_ (integrableOn_Ioi_comp_rpow_iff' _ ha)
rw [MellinConvergent]
refine integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi
dsimp only [Pi.smul_apply]
rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht), ofReal_cpow (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), mul_one, add_comm, ← add_sub_assoc, sub_add_cancel]
