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 : ) => x.log * x) {x : | 1 x}
theorem Real.log_div_self_antitoneOn :
AntitoneOn (fun (x : ) => x.log / x) {x : | Real.exp 1 x}
theorem Real.log_div_self_rpow_antitoneOn {a : } (ha : 0 < a) :
AntitoneOn (fun (x : ) => x.log / x ^ a) {x : | (1 / a).exp x}
theorem Real.log_div_sqrt_antitoneOn :
AntitoneOn (fun (x : ) => x.log / x.sqrt) {x : | Real.exp 2 x}