English
The Mellin transform of t^a on Ioc(0,1) is 1/(s+a) provided Re(s)+Re(a) > 0.
Русский
Преобразование Меллина t^a на Ioc(0,1) равно 1/(s+a) при условии Re(s)+Re(a) > 0.
LaTeX
$$$\text{HasMellin}((\,t\,)^a \mathbf{1}_{Ioc(0,1)}, s) = \frac{1}{s+a}, \quad \Re(s)+\Re(a) > 0.$$$
Lean4
/-- The Mellin transform of a power function restricted to `Ioc 0 1`. -/
theorem hasMellin_cpow_Ioc (a : ℂ) {s : ℂ} (hs : 0 < re s + re a) :
HasMellin (indicator (Ioc 0 1) (fun t => ↑t ^ a : ℝ → ℂ)) s (1 / (s + a)) :=
by
have := hasMellin_one_Ioc (by rwa [add_re] : 0 < (s + a).re)
simp_rw [HasMellin, ← MellinConvergent.cpow_smul, ← mellin_cpow_smul, ← indicator_smul, smul_eq_mul, mul_one] at this
exact this
