Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 20:07 a5ffb9b0

View on Github →

feat(analysis/special_functions): little o behaviour of exp/log at infinity (#11840) from the unit-fractions project

Estimated changes

Modified src/analysis/special_functions/exp.lean

added theorem real.is_o_pow_exp_at_top

modified theorem real.tendsto_div_pow_mul_exp_add_at_top

modified theorem real.tendsto_mul_exp_add_div_pow_at_top

Modified src/analysis/special_functions/log.lean

added theorem real.is_o_pow_log_id_at_top

added theorem real.tendsto_pow_log_div_mul_add_at_top

Modified src/analysis/special_functions/pow.lean