polynomial_mul — Mathlib

English

If f decays, then for any β[X]-polynomial p, the product f(x) · p(k(x)) decays.

Русский

Если f затухает, то при любом полиномиальном выражении p(k(x)) произведение f(x) · p(k(x)) затухает.

LaTeX

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

Lean4

theorem polynomial_mul [ContinuousAdd β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (p : β[X]) :
    SuperpolynomialDecay l k fun x => (p.eval <| k x) * f x :=
  Polynomial.induction_on' p (fun p q hp hq => by simpa [add_mul] using hp.add hq) fun n c => by
    simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c

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