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 * log x
source
theorem Real.Continuous.mul_log {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) :
Continuous fun (a : α) => f a * log (f a)
source
theorem Real.differentiableOn_mul_log :
DifferentiableOn ℝ (fun (x : ℝ) => x * log x) {0}ᶜ
source
@[simp]
theorem Real.deriv_mul_log {x : ℝ} (hx : x ≠ 0) :
deriv (fun (x : ℝ) => x * log x) x = log x + 1
source
theorem Real.hasDerivAt_mul_log {x : ℝ} (hx : x ≠ 0) :
HasDerivAt (fun (x : ℝ) => x * log x) (log x + 1) x
source
@[simp]
theorem Real.rightDeriv_mul_log {x : ℝ} (hx : x ≠ 0) :
derivWithin (fun (x : ℝ) => x * log x) (Set.Ioi x) x = log x + 1
source
@[simp]
theorem Real.leftDeriv_mul_log {x : ℝ} (hx : x ≠ 0) :
derivWithin (fun (x : ℝ) => x * log x) (Set.Iio x) x = log x + 1
source
theorem Real.tendsto_deriv_mul_log_atTop :
Filter.Tendsto (fun (x : ℝ) => deriv (fun (x : ℝ) => x * log x) x) Filter.atTop Filter.atTop
source
theorem Real.tendsto_rightDeriv_mul_log_atTop :
Filter.Tendsto (fun (x : ℝ) => derivWithin (fun (x : ℝ) => x * log x) (Set.Ioi x) x) Filter.atTop Filter.atTop
source
theorem Real.not_DifferentiableAt_log_mul_zero :
¬DifferentiableAt ℝ (fun (x : ℝ) => x * 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 * 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 * log x) 0
source
theorem Real.deriv2_mul_log (x : ℝ) :
deriv^[2] (fun (x : ℝ) => x * log x) x = x⁻¹
source
theorem Real.strictConvexOn_mul_log :
StrictConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * log x
source
theorem Real.convexOn_mul_log :
ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => x * log x
source
theorem Real.mul_log_nonneg {x : ℝ} (hx : 1 ≤ x) :
0 ≤ x * log x
source
theorem Real.mul_log_nonpos {x : ℝ} (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) :
x * 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 :
    negMulLog = fun (x : ℝ) => -x * log x
    source
    theorem Real.negMulLog_eq_neg :
    negMulLog = fun (x : ℝ) => -(x * log x)
    source
    @[simp]
    theorem Real.negMulLog_zero :
    negMulLog 0 = 0
    source
    @[simp]
    theorem Real.negMulLog_one :
    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 negMulLog
    source
    theorem Real.differentiableOn_negMulLog :
    DifferentiableOn ℝ negMulLog {0}ᶜ
    source
    theorem Real.differentiableAt_negMulLog_iff {x : ℝ} :
    DifferentiableAt ℝ negMulLog x ↔ x ≠ 0
    source
    theorem Real.differentiableAt_negMulLog {x : ℝ} :
    x ≠ 0 → DifferentiableAt ℝ negMulLog x

    Alias of the reverse direction of Real.differentiableAt_negMulLog_iff.

    source
    theorem Real.deriv_negMulLog {x : ℝ} (hx : x ≠ 0) :
    deriv negMulLog x = -log x - 1
    source
    theorem Real.hasDerivAt_negMulLog {x : ℝ} (hx : x ≠ 0) :
    HasDerivAt negMulLog (-log x - 1) x
    source
    theorem Real.deriv2_negMulLog (x : ℝ) :
    deriv^[2] negMulLog x = -x⁻¹
    source
    theorem Real.strictConcaveOn_negMulLog :
    StrictConcaveOn ℝ (Set.Ici 0) negMulLog
    source
    theorem Real.concaveOn_negMulLog :
    ConcaveOn ℝ (Set.Ici 0) negMulLog