no goals
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a => abs (k a ^ n * f a)) l (𝓝 0)) ↔
    SuperpolynomialDecay l (fun a => abs (k a)) fun a => abs (f a)
simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]