const_mul — Mathlib

English

If f decays superpolynomially along l with k, then the function n ↦ c · f(n) also decays for any constant c.

Русский

Если f имеет сверхполиномиальное затухание вдоль l по k, то функция n ↦ c · f(n) тоже затухает для любого константного c.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow \forall c, \mathrm{SuperpolynomialDecay}(l,k,\lambda n. c \cdot f(n))$$$

Lean4

theorem const_mul [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (c : β) :
    SuperpolynomialDecay l k fun n => c * f n :=
  (hf.mul_const c).congr fun _ => mul_comm _ _

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