English
Scalar multiplication commutes with Mellin in a compatible setting with a commutation constraint.
Русский
Скалярное умножение в рамках допускаемой совместимости с трансформацией Меллина коммутирует.
LaTeX
$$$\text{mellin}(c\cdot f,s) = c\cdot \text{mellin}(f,s)$$$
Lean4
/-- Compatibility with scalar multiplication by a normed field. For scalar multiplication by more
general rings assuming *a priori* that the Mellin transform is defined, see
`hasMellin_const_smul`. -/
theorem mellin_const_smul (f : ℝ → E) (s : ℂ) {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E] [SMulCommClass ℂ 𝕜 E]
(c : 𝕜) : mellin (fun t => c • f t) s = c • mellin f s := by simp only [mellin, smul_comm, integral_smul]
