superpolynomialDecay_param_pow_mul_iff

English

For any n ∈ N, multiplying f by k^n does not affect having superpolynomial decay along k, assuming 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,k^{n}\\cdot f) \\iff \\operatorname{SuperpolynomialDecay}(l,k,f) \\bigr).$$$

Lean4

theorem superpolynomialDecay_param_pow_mul_iff (hk : Tendsto k l atTop) (n : ℕ) :
    SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f := by
  induction n with
  | zero => simp
  | succ n hn => simpa [pow_succ, ← mul_comm k, mul_assoc, superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn

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