Documentation

Mathlib.Analysis.SpecialFunctions.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_monotoneOn :
MonotoneOn (fun x => Real.log x * x) {x | 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}