superpolynomialDecay_iff_abs_tendsto_zero

English

If f decays along l and |g| ≤ᶠ[l] |f|, then g also decays along l.

Русский

Если f затухает вдоль l и |g| ≤ᶠ[l] |f|, то и g затухает вдоль l.

LaTeX

$$$\mathrm{SuperpolynomialDecay}(l,k,f) \Rightarrow (|g| \le^\!l |f|) \Rightarrow \mathrm{SuperpolynomialDecay}(l,k,g)$$$

Lean4

theorem superpolynomialDecay_iff_abs_tendsto_zero :
    SuperpolynomialDecay l k f ↔ ∀ n : ℕ, Tendsto (fun a : α => |k a ^ n * f a|) l (𝓝 0) :=
  ⟨fun h z => (tendsto_zero_iff_abs_tendsto_zero _).1 (h z), fun h z => (tendsto_zero_iff_abs_tendsto_zero _).2 (h z)⟩

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