Commit 2022-07-12 21:43 7bd47556

View on Github →

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.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem is_o_abs_log_rpow_rpow_nhds_zero

added theorem is_o_log_rpow_nhds_zero

modified theorem is_o_log_rpow_rpow_at_top

added theorem tendsto_log_div_rpow_nhds_zero

added theorem tensdto_log_mul_rpow_nhds_zero