mul_param_pow — Mathlib

English

For any n, f times k^n decays if f does.

Русский

Для любого n, f · k^n затухает при условии сверхполиномиального затухания для f.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall n \in \mathbb{N}, \mathrm{SuperpolynomialDecay}(l,k,\lambda a. f(a) \cdot (k(a))^n)$$$

Lean4

theorem mul_param_pow (hf : SuperpolynomialDecay l k f) (n : ℕ) : SuperpolynomialDecay l k (f * k ^ n) :=
  (hf.param_pow_mul n).congr fun _ => mul_comm _ _

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