superpolynomialDecay_iff_superpolynomialDecay_abs

English

For any integer z, the decay of f is preserved when multiplied pointwise by k^z.

Русский

Для любого целого z затухание f сохраняется при умножении по точкам на k^z.

LaTeX

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

Lean4

theorem superpolynomialDecay_iff_superpolynomialDecay_abs :
    SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a| :=
  (superpolynomialDecay_iff_abs_tendsto_zero l k f).trans (by simp_rw [SuperpolynomialDecay, abs_mul, abs_pow])

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