Commit 2021-11-24 18:18 daf30fd7

View on Github →

feat(analysis/asymptotics): Generalize superpolynomial decay using limits instead of big O (#10296) This PR generalizes the definition of superpolynomial_decay in terms of filter.tendsto instead of asymptotics.is_O.

Estimated changes

Modified src/analysis/asymptotics/superpolynomial_decay.lean

deleted theorem asymptotics.is_O.trans_superpolynomial_decay

modified theorem asymptotics.superpolynomial_decay.add

deleted theorem asymptotics.superpolynomial_decay.algebra_map_mul

deleted theorem asymptotics.superpolynomial_decay.algebra_map_pow_mul

added theorem asymptotics.superpolynomial_decay.congr'

added theorem asymptotics.superpolynomial_decay.congr

modified theorem asymptotics.superpolynomial_decay.const_mul

deleted theorem asymptotics.superpolynomial_decay.eventually_le

deleted theorem asymptotics.superpolynomial_decay.eventually_mono

added theorem asymptotics.superpolynomial_decay.inv_param_mul

deleted theorem asymptotics.superpolynomial_decay.mono

modified theorem asymptotics.superpolynomial_decay.mul

modified theorem asymptotics.superpolynomial_decay.mul_const

deleted theorem asymptotics.superpolynomial_decay.mul_is_O

deleted theorem asymptotics.superpolynomial_decay.mul_is_O_polynomial

added theorem asymptotics.superpolynomial_decay.mul_param

added theorem asymptotics.superpolynomial_decay.mul_param_pow

added theorem asymptotics.superpolynomial_decay.mul_param_zpow

added theorem asymptotics.superpolynomial_decay.mul_polynomial

added theorem asymptotics.superpolynomial_decay.param_inv_mul

added theorem asymptotics.superpolynomial_decay.param_mul

added theorem asymptotics.superpolynomial_decay.param_pow_mul

added theorem asymptotics.superpolynomial_decay.param_zpow_mul

modified theorem asymptotics.superpolynomial_decay.polynomial_mul

deleted theorem asymptotics.superpolynomial_decay.tendsto_zero

added theorem asymptotics.superpolynomial_decay.trans_abs_le

added theorem asymptotics.superpolynomial_decay.trans_eventually_abs_le

added theorem asymptotics.superpolynomial_decay.trans_eventually_le

modified def asymptotics.superpolynomial_decay

deleted theorem asymptotics.superpolynomial_decay_const_iff

modified theorem asymptotics.superpolynomial_decay_const_mul_iff

deleted theorem asymptotics.superpolynomial_decay_const_mul_iff_of_ne_zero

added theorem asymptotics.superpolynomial_decay_iff_abs_is_bounded_under

added theorem asymptotics.superpolynomial_decay_iff_abs_tendsto_zero

added theorem asymptotics.superpolynomial_decay_iff_is_O

deleted theorem asymptotics.superpolynomial_decay_iff_is_bounded_under

modified theorem asymptotics.superpolynomial_decay_iff_is_o

modified theorem asymptotics.superpolynomial_decay_iff_norm_tendsto_zero

added theorem asymptotics.superpolynomial_decay_iff_superpolynomial_decay_abs

added theorem asymptotics.superpolynomial_decay_iff_superpolynomial_decay_norm

deleted theorem asymptotics.superpolynomial_decay_iff_tendsto_zero

added theorem asymptotics.superpolynomial_decay_iff_zpow_tendsto_zero

modified theorem asymptotics.superpolynomial_decay_mul_const_iff

deleted theorem asymptotics.superpolynomial_decay_mul_const_iff_of_ne_zero

added theorem asymptotics.superpolynomial_decay_mul_param_iff

added theorem asymptotics.superpolynomial_decay_mul_param_pow_iff

deleted theorem asymptotics.superpolynomial_decay_of_eventually_is_O

deleted theorem asymptotics.superpolynomial_decay_of_is_O_zpow_le

deleted theorem asymptotics.superpolynomial_decay_of_is_O_zpow_lt

added theorem asymptotics.superpolynomial_decay_param_mul_iff

added theorem asymptotics.superpolynomial_decay_param_pow_mul_iff

deleted theorem asymptotics.superpolynomial_decay_zero'

modified theorem asymptotics.superpolynomial_decay_zero

Modified src/order/filter/at_top_bot.lean

added theorem filter.eventually_ne_of_tendsto_at_bot

added theorem filter.eventually_ne_of_tendsto_at_top

Modified src/topology/algebra/ordered/basic.lean

added theorem tendsto_zero_iff_abs_tendsto_zero