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.mul_log_strictMonoOn : StrictMonoOn (fun (x : ℝ) => x * log x) (Set.Ici (exp (-1)))

@[deprecated Real.mul_log_strictMonoOn (since := "2026-04-07")]

theorem Real.log_mul_self_monotoneOn : MonotoneOn (fun (x : ℝ) => log x * x) {x : ℝ | 1 ≤ x}

theorem Real.mul_log_strictAntiOn : StrictAntiOn (fun (x : ℝ) => x * log x) (Set.Icc 0 (exp (-1)))

theorem Real.log_div_self_antitoneOn : AntitoneOn (fun (x : ℝ) => log x / x) (Set.Ici (exp 1))

theorem Real.log_div_self_rpow_antitoneOn {a : ℝ} (ha : 0 < a) : AntitoneOn (fun (x : ℝ) => log x / x ^ a) (Set.Ici (exp a⁻¹))

theorem Real.log_div_sqrt_antitoneOn : AntitoneOn (fun (x : ℝ) => log x / √x) (Set.Ici (exp 2))