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 * Real.log x
source
theorem Real.Continuous.mul_log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) :
Continuous fun (a : α) => f a * Real.log (f a)
source
theorem Real.differentiableOn_mul_log :
DifferentiableOn ℝ (fun (x : ℝ) => x * Real.log x) {0}ᶜ
source
theorem Real.deriv_mul_log {x : ℝ} (hx : x ≠ 0) :
deriv (fun (x : ℝ) => x * Real.log x) x = Real.log x + 1
source
theorem Real.hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) :
HasDerivAt (fun (x : ℝ) => x * Real.log x) (Real.log x + 1) x
source
theorem Real.not_DifferentiableAt_log_mul_zero :
¬DifferentiableAt ℝ (fun (x : ℝ) => x * Real.log x) 0

At x=0, (fun x ↦ x * log x) is not differentiable (but note that it is continuous, see continuous_mul_log).

source
theorem Real.deriv_mul_log_zero :
deriv (fun (x : ℝ) => x * Real.log x) 0 = 0

Not differentiable, hence deriv has junk value zero.

source
theorem Real.not_continuousAt_deriv_mul_log_zero :
¬ContinuousAt (deriv fun (x : ℝ) => x * Real.log x) 0
source
theorem Real.deriv2_mul_log (x : ℝ) :
deriv^[2] (fun (x : ℝ) => x * Real.log x) x = x⁻¹
source
theorem Real.strictConvexOn_mul_log :
StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * Real.log x
source
theorem Real.convexOn_mul_log :
ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * Real.log x
source
theorem Real.mul_log_nonneg {x : ℝ} (hx : 1 ≤ x) :
0 ≤ x * Real.log x
source
theorem Real.mul_log_nonpos {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) :
x * Real.log x ≤ 0
source
noncomputable def Real.negMulLog (x : ℝ) :
ℝ

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

Equations
Instances For
    source
    theorem Real.negMulLog_def :
    Real.negMulLog = fun (x : ℝ) => -x * Real.log x
    source
    theorem Real.negMulLog_eq_neg :
    Real.negMulLog = fun (x : ℝ) => -(x * Real.log x)
    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.differentiableAt_negMulLog_iff {x : ℝ} :
    DifferentiableAt ℝ Real.negMulLog x ↔ x ≠ 0
    source
    theorem Real.differentiableAt_negMulLog {x : ℝ} :
    x ≠ 0 → DifferentiableAt ℝ Real.negMulLog x

    Alias of the reverse direction of Real.differentiableAt_negMulLog_iff.

    source
    theorem Real.deriv_negMulLog {x : ℝ} (hx : x ≠ 0) :
    deriv Real.negMulLog x = -Real.log x - 1
    source
    theorem Real.hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) :
    HasDerivAt Real.negMulLog (-Real.log x - 1) x
    source
    theorem Real.deriv2_negMulLog (x : ℝ) :
    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