hasMellin_const_smul — Mathlib

English

If f is Mellin-convergent at s, then c • f has Mellin transform c • mellin f at s for any scalar c.

Русский

Если f сходится по Меллину в s, то для любого константного множителя c выполняется, что c • f имеет преобразование Меллина равное c • mellin f в s.

LaTeX

$$$\text{HasMellin}(f,s,m) \Rightarrow \text{HasMellin}(c\cdot f,s,c\cdot m)$.$$

Lean4

theorem hasMellin_const_smul {f : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) {R : Type*} [NormedRing R] [Module R E]
    [IsBoundedSMul R E] [SMulCommClass ℂ R E] (c : R) : HasMellin (fun t => c • f t) s (c • mellin f s) :=
  ⟨hf.const_smul c, by simp [mellin, smul_comm, hf.integral_smul]⟩

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