English
Scaling the argument by a positive real a preserves Mellin-convergence, i.e., Mellin of f(a·t) equals Mellin of f with the same s.
Русский
Умножение аргумента на положительное число a сохраняет сходимость Меллина: Меллин от f(a·t) равен Меллину от f с тем же s.
LaTeX
$$$\forall a>0:\ \text{MellinConvergent}(t\mapsto f(a t),s) = \text{MellinConvergent}(f,s)$$$
Lean4
theorem comp_mul_left {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : 0 < a) :
MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s :=
by
have := integrableOn_Ioi_comp_mul_left_iff (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) 0 ha
rw [mul_zero] at this
have h1 :
EqOn (fun t : ℝ => (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
((a : ℂ) ^ (s - 1) • fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) :=
fun t ht ↦ by simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]
have h2 : (a : ℂ) ^ (s - 1) ≠ 0 :=
by
rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]
exact Or.inl ha.ne'
rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi, IntegrableOn,
IntegrableOn, integrable_smul_iff h2]
