Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-12 10:27 41afd8c2

View on Github →

feat(analysis/special_functions/pow): asymptotics for real powers and log (#14088) From the unit fractions project.

Estimated changes

Modified src/analysis/special_functions/log/basic.lean

added theorem real.is_o_log_id_at_top

modified theorem real.is_o_pow_log_id_at_top

Modified src/analysis/special_functions/pow.lean

added theorem asymptotics.is_O.rpow

added theorem asymptotics.is_O_with.rpow

added theorem asymptotics.is_o.rpow

added theorem is_o_log_rpow_at_top

added theorem is_o_log_rpow_rpow_at_top