trans_abs_le — Mathlib

English

If f decays, then for any polynomial p, the weighted function x ↦ p(k(x)) · f(x) decays.

Русский

Если f затухает, то взвешенная функцией по полиному p(k(x)) функция p(k(x)) · f(x) затухает.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall p \in \mathbb{β}[X], \mathrm{SuperpolynomialDecay}(l,k,\lambda x. p(k(x)) \cdot f(x))$$$

Lean4

theorem trans_abs_le (hf : SuperpolynomialDecay l k f) (hfg : ∀ x, |g x| ≤ |f x|) : SuperpolynomialDecay l k g :=
  hf.trans_eventually_abs_le (Eventually.of_forall hfg)

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