mathlib3

993a470e - feat(analysis/special_functions/log): add log_div_self_antitone_on (#10985)

feat(analysis/special_functions/log): add log_div_self_antitone_on (#10985) Adds lemma `log_div_self_antitone_on`, which shows that `log x / x` is decreasing when `exp 1 \le x`. Needed for Bertrand's postulate (#8002).