English
Let l be a filter on α, and k: α → β, f: α → β. The function f has superpolynomial decay in the parameter k along l if for every natural number n, the product k(a)^n · f(a) tends to 0 along l.
Русский
Пусть l — фильтр на A, k: A → B, f: A → B. Функция f имеет сверхполиномиальное затухание вдоль k по фильтру l, если для каждого натурального n landet k(a)^n · f(a) стремится к 0 вдоль l.
LaTeX
$$$\forall n \in \mathbb{N}, \operatorname{Tendsto}\bigl(a \mapsto k(a)^n \cdot f(a)\bigr)\ l\ (\mathcal{N}(0))$$$
Lean4
/-- `f` has superpolynomial decay in parameter `k` along filter `l` if
`k ^ n * f` tends to zero at `l` for all naturals `n` -/
def SuperpolynomialDecay {α β : Type*} [TopologicalSpace β] [CommSemiring β] (l : Filter α) (k : α → β) (f : α → β) :=
∀ n : ℕ, Tendsto (fun a : α => k a ^ n * f a) l (𝓝 0)
