Commit 2023-05-25 08:46 9d7a61cb

View on Github →

feat: port Analysis.SpecialFunctions.Pow.Asymptotics (#4174)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Asymptotics/Theta.lean

Created Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

added theorem Asymptotics.IsBigO.rpow

added theorem Asymptotics.IsBigOWith.rpow

added theorem Asymptotics.IsLittleO.rpow

added theorem Complex.isBigO_cpow_rpow

added theorem Complex.isTheta_cpow_const_rpow

added theorem Complex.isTheta_cpow_rpow

added theorem Complex.isTheta_exp_arg_mul_im

added theorem ENNReal.tendsto_rpow_at_top

added theorem isLittleO_abs_log_rpow_rpow_nhds_zero

added theorem isLittleO_exp_neg_mul_rpow_atTop

added theorem isLittleO_log_rpow_atTop

added theorem isLittleO_log_rpow_nhds_zero

added theorem isLittleO_log_rpow_rpow_atTop

added theorem isLittleO_pow_exp_pos_mul_atTop

added theorem isLittleO_rpow_exp_atTop

added theorem isLittleO_rpow_exp_pos_mul_atTop

added theorem isLittleO_zpow_exp_pos_mul_atTop

added theorem tendsto_exp_div_rpow_atTop

added theorem tendsto_exp_mul_div_rpow_atTop

added theorem tendsto_log_div_rpow_nhds_zero

added theorem tendsto_log_mul_rpow_nhds_zero

added theorem tendsto_rpow_atTop

added theorem tendsto_rpow_div

added theorem tendsto_rpow_div_mul_add

added theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0

added theorem tendsto_rpow_neg_atTop

added theorem tendsto_rpow_neg_div

Modified Mathlib/Data/Real/Basic.lean