The function x ↦ - x * log x

The purpose of this file is to record basic analytic properties of the function x ↦ - x * log x, which is notably used in the theory of Shannon entropy.

Main definitions

• negMulLog: the function x ↦ - x * log x from ℝ to ℝ.

theorem Real.continuous_mul_log : Continuous fun (x : ℝ) => x * Real.log x

theorem Real.differentiableOn_mul_log : DifferentiableOn ℝ (fun (x : ℝ) => x * Real.log x) {0}ᶜ

theorem Real.deriv_mul_log {x : ℝ} (hx : x ≠ 0) : deriv (fun (x : ℝ) => x * Real.log x) x = Real.log x + 1

theorem Real.hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) : HasDerivAt (fun (x : ℝ) => x * Real.log x) (Real.log x + 1) x

theorem Real.deriv2_mul_log {x : ℝ} (hx : x ≠ 0) : deriv^[2] (fun (x : ℝ) => x * Real.log x) x = x⁻¹

theorem Real.strictConvexOn_mul_log : StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * Real.log x

theorem Real.convexOn_mul_log : ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * Real.log x

theorem Real.mul_log_nonneg {x : ℝ} (hx : 1 ≤ x) : 0 ≤ x * Real.log x

theorem Real.mul_log_nonpos {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x * Real.log x ≤ 0

noncomputable def Real.negMulLog (x : ℝ) : ℝ

The function x ↦ - x * log x from ℝ to ℝ.

Equations

• x.negMulLog = -x * Real.log x

theorem Real.negMulLog_def : Real.negMulLog = fun (x : ℝ) => -x * Real.log x

theorem Real.negMulLog_eq_neg : Real.negMulLog = fun (x : ℝ) => -(x * Real.log x)

@[simp]

theorem Real.negMulLog_zero : Real.negMulLog 0 = 0

@[simp]

theorem Real.negMulLog_one : Real.negMulLog 1 = 0

theorem Real.negMulLog_nonneg {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) : 0 ≤ x.negMulLog

theorem Real.negMulLog_mul (x : ℝ) (y : ℝ) : (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog

theorem Real.continuous_negMulLog : Continuous Real.negMulLog

theorem Real.differentiableOn_negMulLog : DifferentiableOn ℝ Real.negMulLog {0}ᶜ

theorem Real.deriv_negMulLog {x : ℝ} (hx : x ≠ 0) : deriv Real.negMulLog x = -Real.log x - 1

theorem Real.hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) : HasDerivAt Real.negMulLog (-Real.log x - 1) x

theorem Real.deriv2_negMulLog {x : ℝ} (hx : x ≠ 0) : deriv^[2] Real.negMulLog x = -x⁻¹

theorem Real.strictConcaveOn_negMulLog : StrictConcaveOn ℝ (Set.Ici 0) Real.negMulLog

theorem Real.concaveOn_negMulLog : ConcaveOn ℝ (Set.Ici 0) Real.negMulLog