mul_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_const [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (c : β) :
    SuperpolynomialDecay l k fun n => f n * c := fun z => by
  simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)

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