hasMellin_sub — 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_sub {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_sub] using hf.sub hg, by
    simpa only [mellin, smul_sub] using integral_sub hf hg⟩

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