const_smul — Mathlib

English

For scalar c in any normed field, Mellin of c·f equals c times Mellin of f.

Русский

Для скаляра c из нормированного поля, преобразование Меллина от c·f равно c умноженному на преобразование Меллина от f.

LaTeX

$$$\text{mellin}(c\cdot f, s) = c\cdot \text{mellin}(f,s)$$$

Lean4

theorem const_smul {f : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) {𝕜 : Type*} [NormedAddCommGroup 𝕜]
    [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E] [SMulCommClass ℂ 𝕜 E] (c : 𝕜) : MellinConvergent (fun t => c • f t) s := by
  simpa only [MellinConvergent, smul_comm] using hf.smul c

Похожие утверждения