Commit 2021-10-07 06:14 b9097f11

View on Github →

feat(analysis/asymptotics): Define superpolynomial decay of a function (#9440) Define superpolynomial decay of functions in terms of asymptotics.is_O.

Estimated changes

Created src/analysis/asymptotics/superpolynomial_decay.lean

added theorem asymptotics.is_O.trans_superpolynomial_decay

added theorem asymptotics.superpolynomial_decay.add

added theorem asymptotics.superpolynomial_decay.algebra_map_mul

added theorem asymptotics.superpolynomial_decay.algebra_map_pow_mul

added theorem asymptotics.superpolynomial_decay.const_mul

added theorem asymptotics.superpolynomial_decay.eventually_le

added theorem asymptotics.superpolynomial_decay.eventually_mono

added theorem asymptotics.superpolynomial_decay.mono

added theorem asymptotics.superpolynomial_decay.mul

added theorem asymptotics.superpolynomial_decay.mul_const

added theorem asymptotics.superpolynomial_decay.mul_is_O

added theorem asymptotics.superpolynomial_decay.mul_is_O_polynomial

added theorem asymptotics.superpolynomial_decay.polynomial_mul

added theorem asymptotics.superpolynomial_decay.tendsto_zero

added def asymptotics.superpolynomial_decay

added theorem asymptotics.superpolynomial_decay_const_iff

added theorem asymptotics.superpolynomial_decay_const_mul_iff

added theorem asymptotics.superpolynomial_decay_const_mul_iff_of_ne_zero

added theorem asymptotics.superpolynomial_decay_iff_is_bounded_under

added theorem asymptotics.superpolynomial_decay_iff_is_o

added theorem asymptotics.superpolynomial_decay_iff_norm_tendsto_zero

added theorem asymptotics.superpolynomial_decay_iff_tendsto_zero

added theorem asymptotics.superpolynomial_decay_mul_const_iff

added theorem asymptotics.superpolynomial_decay_mul_const_iff_of_ne_zero

added theorem asymptotics.superpolynomial_decay_of_eventually_is_O

added theorem asymptotics.superpolynomial_decay_of_is_O_fpow_le

added theorem asymptotics.superpolynomial_decay_of_is_O_fpow_lt

added theorem asymptotics.superpolynomial_decay_zero'

added theorem asymptotics.superpolynomial_decay_zero