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_monotoneOn : MonotoneOn (fun (x : ℝ) => Real.log x * x) {x : ℝ | 1 ≤ x}

theorem Real.log_div_self_antitoneOn : AntitoneOn (fun (x : ℝ) => Real.log x / x) {x : ℝ | Real.exp 1 ≤ x}

theorem Real.log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) : AntitoneOn (fun (x : ℝ) => Real.log x / x ^ a) {x : ℝ | Real.exp (1 / a) ≤ x}

theorem Real.log_div_sqrt_antitoneOn : AntitoneOn (fun (x : ℝ) => Real.log x / √x) {x : ℝ | Real.exp 2 ≤ x}