add — Mathlib

English

If f and g both have superpolynomial decay along l with parameter k, then f + g also has superpolynomial decay along l with k.

Русский

Если оба f и g обладают сверхполиномиальным затуханием вдоль l по параметру k, то сумма f + g также затухает сверхполиномиально.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \wedge \mathrm{SuperpolynomialDecay}(l,k,g) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,f+g)$$$

Lean4

theorem add [ContinuousAdd β] (hf : SuperpolynomialDecay l k f) (hg : SuperpolynomialDecay l k g) :
    SuperpolynomialDecay l k (f + g) := fun z => by simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)

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