Documentation

Mathlib.Analysis.SpecialFunctions.Log.NegMulLog

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 #

source
theorem Real.continuous_mul_log :
Continuous fun (x : ℝ) => x * x.log
source
theorem Real.differentiableOn_mul_log :
DifferentiableOn ℝ (fun (x : ℝ) => x * x.log) {0}ᶜ
source
theorem Real.deriv_mul_log {x : ℝ} (hx : x ≠ 0) :
deriv (fun (x : ℝ) => x * x.log) x = x.log + 1
source
theorem Real.hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) :
HasDerivAt (fun (x : ℝ) => x * x.log) (x.log + 1) x
source
theorem Real.deriv2_mul_log {x : ℝ} (hx : x ≠ 0) :
deriv^[2] (fun (x : ℝ) => x * x.log) x = x⁻¹
source
theorem Real.strictConvexOn_mul_log :
StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * x.log
source
theorem Real.convexOn_mul_log :
ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * x.log
source
theorem Real.mul_log_nonneg {x : ℝ} (hx : 1 ≤ x) :
0 ≤ x * x.log
source
theorem Real.mul_log_nonpos {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) :
x * x.log ≤ 0
source
noncomputable def Real.negMulLog (x : ℝ) :
ℝ

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

Equations
  • x.negMulLog = -x * x.log
Instances For
    source
    theorem Real.negMulLog_def :
    Real.negMulLog = fun (x : ℝ) => -x * x.log
    source
    theorem Real.negMulLog_eq_neg :
    Real.negMulLog = fun (x : ℝ) => -(x * x.log)
    source
    @[simp]
    theorem Real.negMulLog_zero :
    Real.negMulLog 0 = 0
    source
    @[simp]
    theorem Real.negMulLog_one :
    Real.negMulLog 1 = 0
    source
    theorem Real.negMulLog_nonneg {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) :
    0 ≤ x.negMulLog
    source
    theorem Real.negMulLog_mul (x : ℝ) (y : ℝ) :
    (x * y).negMulLog = y * x.negMulLog + x * y.negMulLog
    source
    theorem Real.continuous_negMulLog :
    Continuous Real.negMulLog
    source
    theorem Real.differentiableOn_negMulLog :
    DifferentiableOn ℝ Real.negMulLog {0}ᶜ
    source
    theorem Real.deriv_negMulLog {x : ℝ} (hx : x ≠ 0) :
    deriv Real.negMulLog x = -x.log - 1
    source
    theorem Real.hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) :
    HasDerivAt Real.negMulLog (-x.log - 1) x
    source
    theorem Real.deriv2_negMulLog {x : ℝ} (hx : x ≠ 0) :
    deriv^[2] Real.negMulLog x = -x⁻¹
    source
    theorem Real.strictConcaveOn_negMulLog :
    StrictConcaveOn ℝ (Set.Ici 0) Real.negMulLog
    source
    theorem Real.concaveOn_negMulLog :
    ConcaveOn ℝ (Set.Ici 0) Real.negMulLog