Commit 2023-04-13 11:26 47213b87

View on Github →

feat: port Analysis.Asymptotics.Theta (#3416)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/Theta.lean

added theorem Asymptotics.IsBigO.antisymm

added theorem Asymptotics.IsBigO.trans_isTheta

added theorem Asymptotics.IsLittleO.trans_isTheta

added theorem Asymptotics.IsTheta.div

added theorem Asymptotics.IsTheta.eq_zero_iff

added theorem Asymptotics.IsTheta.inv

added theorem Asymptotics.IsTheta.isBigO_congr_left

added theorem Asymptotics.IsTheta.isBigO_congr_right

added theorem Asymptotics.IsTheta.isBoundedUnder_le_iff

added theorem Asymptotics.IsTheta.isLittleO_congr_left

added theorem Asymptotics.IsTheta.isLittleO_congr_right

added theorem Asymptotics.IsTheta.mono

added theorem Asymptotics.IsTheta.mul

added theorem Asymptotics.IsTheta.pow

added theorem Asymptotics.IsTheta.smul

added theorem Asymptotics.IsTheta.sup

added theorem Asymptotics.IsTheta.tendsto_norm_atTop_iff

added theorem Asymptotics.IsTheta.tendsto_zero_iff

added theorem Asymptotics.IsTheta.trans

added theorem Asymptotics.IsTheta.trans_eventuallyEq

added theorem Asymptotics.IsTheta.trans_isBigO

added theorem Asymptotics.IsTheta.trans_isLittleO

added theorem Asymptotics.IsTheta.zpow

added def Asymptotics.IsTheta

added theorem Asymptotics.isTheta_comm

added theorem Asymptotics.isTheta_const_const

added theorem Asymptotics.isTheta_const_const_iff

added theorem Asymptotics.isTheta_const_mul_left

added theorem Asymptotics.isTheta_const_mul_right

added theorem Asymptotics.isTheta_const_smul_left

added theorem Asymptotics.isTheta_const_smul_right

added theorem Asymptotics.isTheta_inv

added theorem Asymptotics.isTheta_norm_left

added theorem Asymptotics.isTheta_norm_right

added theorem Asymptotics.isTheta_of_norm_eventuallyEq'

added theorem Asymptotics.isTheta_of_norm_eventuallyEq

added theorem Asymptotics.isTheta_refl

added theorem Asymptotics.isTheta_rfl

added theorem Asymptotics.isTheta_sup

added theorem Asymptotics.isTheta_zero_left

added theorem Asymptotics.isTheta_zero_right

added theorem Filter.EventuallyEq.trans_isTheta