mathlib3 documentation

analysis.special_functions.log.monotone

Logarithm Tonality #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Tags #

logarithm, tonality

source
theorem real.log_mul_self_monotone_on  :
monotone_on (λ (x : ℝ), real.log x * x) {x : ℝ | 1 ≤ x}
source
theorem real.log_div_self_antitone_on  :
antitone_on (λ (x : ℝ), real.log x / x) {x : ℝ | rexp 1 ≤ x}
source
theorem real.log_div_self_rpow_antitone_on {a : ℝ} (ha : 0 < a) :
antitone_on (λ (x : ℝ), real.log x / x ^ a) {x : ℝ | rexp (1 / a) ≤ x}
source
theorem real.log_div_sqrt_antitone_on  :
antitone_on (λ (x : ℝ), real.log x / √ x) {x : ℝ | rexp 2 ≤ x}