superpolynomialDecay_iff_superpolynomialDecay_norm

English

For Tendsto k l atTop, SPD(l,k,f) holds iff f is Big-O of k^z for every z ∈ ℤ.

Русский

При Tendsto k l atTop затухание SPD(l,k,f) эквивалентно тому, что f ∈ O[l](k^z) для каждого z ∈ ℤ.

LaTeX

$$$\\operatorname{Tendsto}(k,l,\\operatorname{atTop}) \\Rightarrow \\operatorname{SPD}(l,k,f) \\iff \\forall z \\in \\mathbb{Z},\\ f =O[l](k^{z}).$$$

Lean4

theorem superpolynomialDecay_iff_superpolynomialDecay_norm :
    SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖ :=
  (superpolynomialDecay_iff_norm_tendsto_zero l k f).trans (by simp [SuperpolynomialDecay])

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