Super-Polynomial Function Decay #

This file defines a predicate asymptotics.superpolynomial_decay f for a function satisfying one of following equivalent definitions (The definition is in terms of the first condition):

• x ^ n * f tends to 𝓝 0 for all (or sufficiently large) naturals n
• |x ^ n * f| tends to 𝓝 0 for all naturals n (superpolynomial_decay_iff_abs_tendsto_zero)
• |x ^ n * f| is bounded for all naturals n (superpolynomial_decay_iff_abs_is_bounded_under)
• f is o(x ^ c) for all integers c (superpolynomial_decay_iff_is_o)
• f is O(x ^ c) for all integers c (superpolynomial_decay_iff_is_O)

These conditions are all equivalent to conditions in terms of polynomials, replacing x ^ c with p(x) or p(x)⁻¹ as appropriate, since asymptotically p(x) behaves like X ^ p.nat_degree. These further equivalences are not proven in mathlib but would be good future projects.

The definition of superpolynomial decay for f : α → β is relative to a parameter k : α → β. Super-polynomial decay then means f x decays faster than (k x) ^ c for all integers c. Equivalently f x decays faster than p.eval (k x) for all polynomials p : polynomial β. The definition is also relative to a filter l : filter α where the decay rate is compared.

When the map k is given by n ↦ ↑n : ℕ → ℝ this defines negligible functions: https://en.wikipedia.org/wiki/Negligible_function

When the map k is given by (r₁,...,rₙ) ↦ r₁*...*rₙ : ℝⁿ → ℝ this is equivalent to the definition of rapidly decreasing functions given here: https://ncatlab.org/nlab/show/rapidly+decreasing+function

Main Theorems #

• superpolynomial_decay.polynomial_mul says that if f(x) is negligible, then so is p(x) * f(x) for any polynomial p.
• superpolynomial_decay_iff_zpow_tendsto_zero gives an equivalence between definitions in terms of decaying faster than k(x) ^ n for all naturals n or k(x) ^ c for all integer c.