Theorems · Theorem · approximation theory

Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero

∀ {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [inst : TopologicalSpace β] [inst_1 : CommRing β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Asymptotics.SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun a => |k a ^ n * f a|) l (nhds 0)

Defined in

Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Cited by

3 results in Mathlib

Foundations

Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceCommRingLinearOrderIsStrictOrderedRingOrderTopology