Commit 2023-04-13 17:26 95431739

View on Github →

feat: port Analysis.Asymptotics.SpecificAsymptotics (#3420)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

added theorem Asymptotics.IsBigO.trans_tendsto_norm_atTop

added theorem Asymptotics.IsLittleO.sum_range

added theorem Asymptotics.isLittleO_pow_pow_atTop_of_lt

added theorem Asymptotics.isLittleO_sum_range_of_tendsto_zero

added theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv

added theorem Filter.Tendsto.cesaro

added theorem Filter.Tendsto.cesaro_smul

added theorem pow_div_pow_eventuallyEq_atBot

added theorem pow_div_pow_eventuallyEq_atTop

added theorem tendsto_pow_div_pow_atTop_atTop

added theorem tendsto_pow_div_pow_atTop_zero

added theorem tendsto_zpow_atTop_atTop