hasMellin_add — Mathlib

English

If f and g have Mellin transforms convergent at s, then mellin(f + g)(s) = mellin f(s) + mellin g(s).

Русский

Если у функций f и g сходятся преобразования Меллина в точке s, то mellin(f+g)(s) = mellin f(s) + mellin g(s).

LaTeX

$$$\text{HasMellin}(f,s,m_f) \land \text{HasMellin}(g,s,m_g) \Rightarrow \text{HasMellin}(f+g,s,m_f+m_g)$.$$

Lean4

theorem hasMellin_add {f g : ℝ → E} {s : ℂ} (hf : MellinConvergent f s) (hg : MellinConvergent g s) :
    HasMellin (fun t => f t + g t) s (mellin f s + mellin g s) :=
  ⟨by simpa only [MellinConvergent, smul_add] using hf.add hg, by
    simpa only [mellin, smul_add] using integral_add hf hg⟩

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