mul_polynomial — Mathlib

English

If f decays, then f(x) · p(k(x)) decays for any polynomial p.

Русский

Если f затухает, то f(x) · p(k(x)) затухает для любого полинома p.

LaTeX

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

Lean4

theorem mul_polynomial [ContinuousAdd β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (p : β[X]) :
    SuperpolynomialDecay l k fun x => f x * (p.eval <| k x) :=
  (hf.polynomial_mul p).congr fun _ => mul_comm _ _

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