superpolynomialDecay_mul_param_pow_iff

English

For any n ∈ N, multiplying f by k^n on the right does not affect having superpolynomial decay along k, given Tendsto k l atTop.

Русский

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

LaTeX

$$$\\operatorname{Tendsto}(k,l,\\operatorname{atTop}) \\Rightarrow \\bigl( \\operatorname{SuperpolynomialDecay}(l,k,f\\cdot k^{n}) \\iff \\operatorname{SuperpolynomialDecay}(l,k,f) \\bigr).$$$

Lean4

theorem superpolynomialDecay_mul_param_pow_iff (hk : Tendsto k l atTop) (n : ℕ) :
    SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f := by
  simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n

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