Commit 2023-04-14 12:58 9ec2b21e

View on Github →

feat: port Analysis.Asymptotics.SuperpolynomialDecay (#3421)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

added theorem Asymptotics.SuperpolynomialDecay.add

added theorem Asymptotics.SuperpolynomialDecay.congr'

added theorem Asymptotics.SuperpolynomialDecay.congr

added theorem Asymptotics.SuperpolynomialDecay.const_mul

added theorem Asymptotics.SuperpolynomialDecay.inv_param_mul

added theorem Asymptotics.SuperpolynomialDecay.mul

added theorem Asymptotics.SuperpolynomialDecay.mul_const

added theorem Asymptotics.SuperpolynomialDecay.mul_param

added theorem Asymptotics.SuperpolynomialDecay.mul_param_pow

added theorem Asymptotics.SuperpolynomialDecay.mul_param_zpow

added theorem Asymptotics.SuperpolynomialDecay.mul_polynomial

added theorem Asymptotics.SuperpolynomialDecay.param_inv_mul

added theorem Asymptotics.SuperpolynomialDecay.param_mul

added theorem Asymptotics.SuperpolynomialDecay.param_pow_mul

added theorem Asymptotics.SuperpolynomialDecay.param_zpow_mul

added theorem Asymptotics.SuperpolynomialDecay.polynomial_mul

added theorem Asymptotics.SuperpolynomialDecay.trans_abs_le

added theorem Asymptotics.SuperpolynomialDecay.trans_eventuallyLE

added theorem Asymptotics.SuperpolynomialDecay.trans_eventually_abs_le

added def Asymptotics.SuperpolynomialDecay

added theorem Asymptotics.superpolynomialDecay_const_mul_iff

added theorem Asymptotics.superpolynomialDecay_iff_abs_isBoundedUnder

added theorem Asymptotics.superpolynomialDecay_iff_abs_tendsto_zero

added theorem Asymptotics.superpolynomialDecay_iff_isBigO

added theorem Asymptotics.superpolynomialDecay_iff_isLittleO

added theorem Asymptotics.superpolynomialDecay_iff_norm_tendsto_zero

added theorem Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_abs

added theorem Asymptotics.superpolynomialDecay_iff_superpolynomialDecay_norm

added theorem Asymptotics.superpolynomialDecay_iff_zpow_tendsto_zero

added theorem Asymptotics.superpolynomialDecay_mul_const_iff

added theorem Asymptotics.superpolynomialDecay_mul_param_iff

added theorem Asymptotics.superpolynomialDecay_mul_param_pow_iff

added theorem Asymptotics.superpolynomialDecay_param_mul_iff

added theorem Asymptotics.superpolynomialDecay_param_pow_mul_iff

added theorem Asymptotics.superpolynomialDecay_zero