Super-Polynomial Function Decay

This file defines a predicate Asymptotics.SuperpolynomialDecay 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 (superpolynomialDecay_iff_abs_tendsto_zero)
• |x ^ n * f| is bounded for all naturals n (superpolynomialDecay_iff_abs_isBoundedUnder)
• f is o(x ^ c) for all integers c (superpolynomialDecay_iff_isLittleO)
• f is O(x ^ c) for all integers c (superpolynomialDecay_iff_isBigO)

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.natDegree. 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 : β[X]. 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

• SuperpolynomialDecay.polynomial_mul says that if f(x) is negligible, then so is p(x) * f(x) for any polynomial p.
• superpolynomialDecay_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.

def Asymptotics.SuperpolynomialDecay {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [CommSemiring β] (l : Filter α) (k f : α → β) : Prop

f has superpolynomial decay in parameter k along filter l if k ^ n * f tends to zero at l for all naturals n

Equations

• Asymptotics.SuperpolynomialDecay l k f = ∀ (n : ℕ), Filter.Tendsto (fun (a : α) => k a ^ n * f a) l (nhds 0)

theorem Asymptotics.SuperpolynomialDecay.congr' {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) (hfg : f =ᶠ[l] g) : SuperpolynomialDecay l k g

theorem Asymptotics.SuperpolynomialDecay.congr {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) (hfg : ∀ (x : α), f x = g x) : SuperpolynomialDecay l k g

@[simp]

theorem Asymptotics.superpolynomialDecay_zero {α : Type u_1} {β : Type u_2} [TopologicalSpace β] [CommSemiring β] (l : Filter α) (k : α → β) : SuperpolynomialDecay l k 0

theorem Asymptotics.SuperpolynomialDecay.add {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousAdd β] (hf : SuperpolynomialDecay l k f) (hg : SuperpolynomialDecay l k g) : SuperpolynomialDecay l k (f + g)

theorem Asymptotics.SuperpolynomialDecay.mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (hg : SuperpolynomialDecay l k g) : SuperpolynomialDecay l k (f * g)

theorem Asymptotics.SuperpolynomialDecay.mul_const {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (c : β) : SuperpolynomialDecay l k fun (n : α) => f n * c

theorem Asymptotics.SuperpolynomialDecay.const_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (c : β) : SuperpolynomialDecay l k fun (n : α) => c * f n

theorem Asymptotics.SuperpolynomialDecay.param_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (k * f)

theorem Asymptotics.SuperpolynomialDecay.mul_param {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (f * k)

theorem Asymptotics.SuperpolynomialDecay.param_pow_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) (n : ℕ) : SuperpolynomialDecay l k (k ^ n * f)

theorem Asymptotics.SuperpolynomialDecay.mul_param_pow {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] (hf : SuperpolynomialDecay l k f) (n : ℕ) : SuperpolynomialDecay l k (f * k ^ n)

theorem Asymptotics.SuperpolynomialDecay.polynomial_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousAdd β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (p : Polynomial β) : SuperpolynomialDecay l k fun (x : α) => Polynomial.eval (k x) p * f x

theorem Asymptotics.SuperpolynomialDecay.mul_polynomial {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [CommSemiring β] [ContinuousAdd β] [ContinuousMul β] (hf : SuperpolynomialDecay l k f) (p : Polynomial β) : SuperpolynomialDecay l k fun (x : α) => f x * Polynomial.eval (k x) p

theorem Asymptotics.SuperpolynomialDecay.trans_eventuallyLE {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g g' : α → β} [TopologicalSpace β] [CommSemiring β] [PartialOrder β] [IsOrderedRing β] [OrderTopology β] (hk : 0 ≤ᶠ[l] k) (hg : SuperpolynomialDecay l k g) (hg' : SuperpolynomialDecay l k g') (hfg : g ≤ᶠ[l] f) (hfg' : f ≤ᶠ[l] g') : SuperpolynomialDecay l k f

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

theorem Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_abs {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [TopologicalSpace β] [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] : SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun (a : α) => |k a|) fun (a : α) => |f a|

theorem Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hf : SuperpolynomialDecay l k f) (hfg : abs ∘ g ≤ᶠ[l] abs ∘ f) : SuperpolynomialDecay l k g

theorem Asymptotics.SuperpolynomialDecay.trans_abs_le {α : Type u_1} {β : Type u_2} {l : Filter α} {k f g : α → β} [TopologicalSpace β] [CommRing β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hf : SuperpolynomialDecay l k f) (hfg : ∀ (x : α), |g x| ≤ |f x|) : SuperpolynomialDecay l k g

theorem Asymptotics.superpolynomialDecay_mul_const_iff {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [TopologicalSpace β] [Field β] [ContinuousMul β] {c : β} (hc0 : c ≠ 0) : (SuperpolynomialDecay l k fun (n : α) => f n * c) ↔ SuperpolynomialDecay l k f

theorem Asymptotics.superpolynomialDecay_const_mul_iff {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [TopologicalSpace β] [Field β] [ContinuousMul β] {c : β} (hc0 : c ≠ 0) : (SuperpolynomialDecay l k fun (n : α) => c * f n) ↔ SuperpolynomialDecay l k f

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

theorem Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) : SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Filter.Tendsto (fun (a : α) => k a ^ z * f a) l (nhds 0)

theorem Asymptotics.SuperpolynomialDecay.param_zpow_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (hf : SuperpolynomialDecay l k f) (z : ℤ) : SuperpolynomialDecay l k fun (a : α) => k a ^ z * f a

theorem Asymptotics.SuperpolynomialDecay.mul_param_zpow {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (hf : SuperpolynomialDecay l k f) (z : ℤ) : SuperpolynomialDecay l k fun (a : α) => f a * k a ^ z

theorem Asymptotics.SuperpolynomialDecay.inv_param_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (k⁻¹ * f)

theorem Asymptotics.SuperpolynomialDecay.param_inv_mul {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (hf : SuperpolynomialDecay l k f) : SuperpolynomialDecay l k (f * k⁻¹)

theorem Asymptotics.superpolynomialDecay_param_mul_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) : SuperpolynomialDecay l k (k * f) ↔ SuperpolynomialDecay l k f

theorem Asymptotics.superpolynomialDecay_mul_param_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) : SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f

theorem Asymptotics.superpolynomialDecay_param_pow_mul_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (n : ℕ) : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

theorem Asymptotics.superpolynomialDecay_mul_param_pow_iff {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [TopologicalSpace β] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) (n : ℕ) : SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

theorem Asymptotics.superpolynomialDecay_iff_norm_tendsto_zero {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [NormedField β] : SuperpolynomialDecay l k f ↔ ∀ (n : ℕ), Filter.Tendsto (fun (a : α) => ‖k a ^ n * f a‖) l (nhds 0)

theorem Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_norm {α : Type u_1} {β : Type u_2} (l : Filter α) (k f : α → β) [NormedField β] : SuperpolynomialDecay l k f ↔ SuperpolynomialDecay l (fun (a : α) => ‖k a‖) fun (a : α) => ‖f a‖

theorem Asymptotics.superpolynomialDecay_iff_isBigO {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) : SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun (a : α) => k a ^ z

theorem Asymptotics.superpolynomialDecay_iff_isLittleO {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [NormedField β] [LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β] (hk : Filter.Tendsto k l Filter.atTop) : SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun (a : α) => k a ^ z