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 / Real.sqrt x) {x | Real.exp 2 ≤ x}