mathlib documentation

analysis.asymptotics.superpolynomial_decay

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):

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 #

def asymptotics.superpolynomial_decay {α : Type u_1} {β : Type u_2} [topological_space β] [comm_semiring β] (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
theorem asymptotics.superpolynomial_decay.congr' {α : Type u_1} {β : Type u_2} {l : filter α} {k f g : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) (hfg : f =ᶠ[l] g) :
theorem asymptotics.superpolynomial_decay.congr {α : Type u_1} {β : Type u_2} {l : filter α} {k f g : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) (hfg : ∀ (x : α), f x = g x) :
@[simp]
theorem asymptotics.superpolynomial_decay_zero {α : Type u_1} {β : Type u_2} [topological_space β] [comm_semiring β] (l : filter α) (k : α → β) :
theorem asymptotics.superpolynomial_decay.add {α : Type u_1} {β : Type u_2} {l : filter α} {k f g : α → β} [topological_space β] [comm_semiring β] [has_continuous_add β] (hf : asymptotics.superpolynomial_decay l k f) (hg : asymptotics.superpolynomial_decay l k g) :
theorem asymptotics.superpolynomial_decay.mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f g : α → β} [topological_space β] [comm_semiring β] [has_continuous_mul β] (hf : asymptotics.superpolynomial_decay l k f) (hg : asymptotics.superpolynomial_decay l k g) :
theorem asymptotics.superpolynomial_decay.mul_const {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] [has_continuous_mul β] (hf : asymptotics.superpolynomial_decay l k f) (c : β) :
asymptotics.superpolynomial_decay l k (λ (n : α), (f n) * c)
theorem asymptotics.superpolynomial_decay.const_mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] [has_continuous_mul β] (hf : asymptotics.superpolynomial_decay l k f) (c : β) :
asymptotics.superpolynomial_decay l k (λ (n : α), c * f n)
theorem asymptotics.superpolynomial_decay.param_mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) :
theorem asymptotics.superpolynomial_decay.mul_param {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) :
theorem asymptotics.superpolynomial_decay.param_pow_mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) (n : ) :
theorem asymptotics.superpolynomial_decay.mul_param_pow {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] (hf : asymptotics.superpolynomial_decay l k f) (n : ) :
theorem asymptotics.superpolynomial_decay.polynomial_mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] [has_continuous_add β] [has_continuous_mul β] (hf : asymptotics.superpolynomial_decay l k f) (p : polynomial β) :
asymptotics.superpolynomial_decay l k (λ (x : α), (polynomial.eval (k x) p) * f x)
theorem asymptotics.superpolynomial_decay.mul_polynomial {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [comm_semiring β] [has_continuous_add β] [has_continuous_mul β] (hf : asymptotics.superpolynomial_decay l k f) (p : polynomial β) :
asymptotics.superpolynomial_decay l k (λ (x : α), (f x) * polynomial.eval (k x) p)
theorem asymptotics.superpolynomial_decay.trans_eventually_le {α : Type u_1} {β : Type u_2} {l : filter α} {k f g g' : α → β} [topological_space β] [ordered_comm_semiring β] [order_topology β] (hk : 0 ≤ᶠ[l] k) (hg : asymptotics.superpolynomial_decay l k g) (hg' : asymptotics.superpolynomial_decay l k g') (hfg : g ≤ᶠ[l] f) (hfg' : f ≤ᶠ[l] g') :
theorem asymptotics.superpolynomial_decay_iff_abs_tendsto_zero {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [topological_space β] [linear_ordered_comm_ring β] [order_topology β] :
asymptotics.superpolynomial_decay l k f ∀ (n : ), filter.tendsto (λ (a : α), |(k a ^ n) * f a|) l (𝓝 0)
theorem asymptotics.superpolynomial_decay_iff_superpolynomial_decay_abs {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [topological_space β] [linear_ordered_comm_ring β] [order_topology β] :
theorem asymptotics.superpolynomial_decay.trans_abs_le {α : Type u_1} {β : Type u_2} {l : filter α} {k f g : α → β} [topological_space β] [linear_ordered_comm_ring β] [order_topology β] (hf : asymptotics.superpolynomial_decay l k f) (hfg : ∀ (x : α), |g x| |f x|) :
theorem asymptotics.superpolynomial_decay_mul_const_iff {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [topological_space β] [field β] [has_continuous_mul β] {c : β} (hc0 : c 0) :
theorem asymptotics.superpolynomial_decay_const_mul_iff {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [topological_space β] [field β] [has_continuous_mul β] {c : β} (hc0 : c 0) :
theorem asymptotics.superpolynomial_decay_iff_abs_is_bounded_under {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
asymptotics.superpolynomial_decay l k f ∀ (z : ), filter.is_bounded_under has_le.le l (λ (a : α), |(k a ^ z) * f a|)
theorem asymptotics.superpolynomial_decay_iff_zpow_tendsto_zero {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
asymptotics.superpolynomial_decay l k f ∀ (z : ), filter.tendsto (λ (a : α), (k a ^ z) * f a) l (𝓝 0)
theorem asymptotics.superpolynomial_decay.param_zpow_mul {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) (hf : asymptotics.superpolynomial_decay l k f) (z : ) :
asymptotics.superpolynomial_decay l k (λ (a : α), (k a ^ z) * f a)
theorem asymptotics.superpolynomial_decay.mul_param_zpow {α : Type u_1} {β : Type u_2} {l : filter α} {k f : α → β} [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) (hf : asymptotics.superpolynomial_decay l k f) (z : ) :
asymptotics.superpolynomial_decay l k (λ (a : α), (f a) * k a ^ z)
theorem asymptotics.superpolynomial_decay_param_mul_iff {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
theorem asymptotics.superpolynomial_decay_mul_param_iff {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
theorem asymptotics.superpolynomial_decay_param_pow_mul_iff {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) (n : ) :
theorem asymptotics.superpolynomial_decay_mul_param_pow_iff {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [topological_space β] [linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) (n : ) :
theorem asymptotics.superpolynomial_decay_iff_norm_tendsto_zero {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [normed_linear_ordered_field β] :
asymptotics.superpolynomial_decay l k f ∀ (n : ), filter.tendsto (λ (a : α), (k a ^ n) * f a) l (𝓝 0)
theorem asymptotics.superpolynomial_decay_iff_superpolynomial_decay_norm {α : Type u_1} {β : Type u_2} (l : filter α) (k f : α → β) [normed_linear_ordered_field β] :
theorem asymptotics.superpolynomial_decay_iff_is_O {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [normed_linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
asymptotics.superpolynomial_decay l k f ∀ (z : ), asymptotics.is_O f (λ (a : α), k a ^ z) l
theorem asymptotics.superpolynomial_decay_iff_is_o {α : Type u_1} {β : Type u_2} {l : filter α} {k : α → β} (f : α → β) [normed_linear_ordered_field β] [order_topology β] (hk : filter.tendsto k l filter.at_top) :
asymptotics.superpolynomial_decay l k f ∀ (z : ), asymptotics.is_o f (λ (a : α), k a ^ z) l