pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164)

Commit

3 years ago

feat(analysis/special_functions/pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164) Drop an unneeded assumption in `is_o_log_rpow_rpow_at_top`, add a few variants.

Author

urkud

Parents

3543262a

mathlib 7bd47556 - feat(analysis/special_functions/pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164)

mathlib
7bd47556 - feat(analysis/special_functions/pow): drop an assumption in `is_o_log_rpow_rpow_at_top` (#15164)