Theorems · Theorem · approximation theory

Asymptotics.superpolynomialDecay_iff_abs_isBoundedUnder

∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    (Asymptotics.SuperpolynomialDecay l k f ↔
      ∀ (z : ℕ), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun a => |k a ^ z * f a|)

Defined in

Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceFieldLinearOrderIsStrictOrderedRingOrderTopology