mathlib documentation

analysis.special_functions.log.monotone

Logarithm Tonality #

In this file we describe the tonality of the logarithm function when multiplied by functions of the form x ^ a.

Tags #

logarithm, tonality

theorem real.log_mul_self_monotone_on  :
monotone_on (λ (x : ), real.log x * x) {x : | 1 x}
theorem real.log_div_self_antitone_on  :
antitone_on (λ (x : ), real.log x / x) {x : | real.exp 1 x}
theorem real.log_div_self_rpow_antitone_on {a : } (ha : 0 < a) :
antitone_on (λ (x : ), real.log x / x ^ a) {x : | real.exp (1 / a) x}