Properties of Shannon q-ary entropy and binary entropy functions

The binary entropy function binEntropy p := - p * log p - (1 - p) * log (1 - p) is the Shannon entropy of a Bernoulli random variable with success probability p.

More generally, the q-ary entropy function is the Shannon entropy of the random variable with possible outcomes {1, ..., q}, where outcome 1 has probability 1 - p and all other outcomes are equally likely.

qaryEntropy (q : ℕ) (p : ℝ) := p * log (q - 1) - p * log p - (1 - p) * log (1 - p)

This file assumes that entropy is measured in Nats, hence the use of natural logarithms. Most lemmas are also valid using a logarithm in a different base.

Main declarations

• Real.binEntropy: the binary entropy function
• Real.qaryEntropy: the q-ary entropy function

Main results

The functions are also defined outside the interval Icc 0 1 due to log x = log |x|.

• They are continuous everywhere (binEntropy_continuous and qaryEntropy_continuous).
• They are differentiable everywhere except at points 0 or 1 (hasDerivAt_binEntropy and hasDerivAt_qaryEntropy). In addition, due to junk values, deriv binEntropy p = log (1 - p) - log p holds everywhere (deriv_binEntropy).
• they are strictly increasing on Icc 0 (1 - 1/q)) (qaryEntropy_strictMonoOn, binEntropy_strictMonoOn) and strictly decreasing on Icc (1 - 1/q) 1 (binEntropy_strictAntiOn and qaryEntropy_strictAntiOn).
• they are strictly concave on Icc 0 1 (strictConcaveOn_qaryEntropy and strictConcave_binEntropy).

Tags

entropy, Shannon, binary, nit, nepit

Binary entropy

noncomputable def Real.binEntropy (p : ℝ) : ℝ

The binary entropy function binEntropy p := - p * log p - (1-p) * log (1 - p) is the Shannon entropy of a Bernoulli random variable with success probability p.

@[simp]

theorem Real.binEntropy_zero : binEntropy 0 = 0

@[simp]

theorem Real.binEntropy_one : binEntropy 1 = 0

@[simp]

theorem Real.binEntropy_two_inv : binEntropy 2⁻¹ = log 2

theorem Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub (p : ℝ) : binEntropy p = p.negMulLog + (1 - p).negMulLog

theorem Real.binEntropy_eq_negMulLog_add_negMulLog_one_sub' : binEntropy = fun (p : ℝ) => p.negMulLog + (1 - p).negMulLog

@[simp]

theorem Real.binEntropy_one_sub (p : ℝ) : binEntropy (1 - p) = binEntropy p

binEntropy is symmetric about 1/2.

theorem Real.binEntropy_two_inv_add (p : ℝ) : binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

binEntropy is symmetric about 1/2.

theorem Real.binEntropy_pos {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < binEntropy p

theorem Real.binEntropy_nonneg {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ binEntropy p

theorem Real.binEntropy_neg_of_neg {p : ℝ} (hp : p < 0) : binEntropy p < 0

Outside the usual range of binEntropy, it is negative. This is due to log p = log |p|.

theorem Real.binEntropy_nonpos_of_nonpos {p : ℝ} (hp : p ≤ 0) : binEntropy p ≤ 0

Outside the usual range of binEntropy, it is negative. This is due to log p = log |p|.

theorem Real.binEntropy_neg_of_one_lt {p : ℝ} (hp : 1 < p) : binEntropy p < 0

Outside the usual range of binEntropy, it is negative. This is due to log p = log |p|

theorem Real.binEntropy_nonpos_of_one_le {p : ℝ} (hp : 1 ≤ p) : binEntropy p ≤ 0

Outside the usual range of binEntropy, it is negative. This is due to log p = log |p|

theorem Real.binEntropy_eq_zero {p : ℝ} : binEntropy p = 0 ↔ p = 0 ∨ p = 1

theorem Real.binEntropy_lt_log_two {p : ℝ} : binEntropy p < log 2 ↔ p ≠ 2⁻¹

For probability p ≠ 0.5, binEntropy p < log 2.

theorem Real.binEntropy_le_log_two {p : ℝ} : binEntropy p ≤ log 2

theorem Real.binEntropy_eq_log_two {p : ℝ} : binEntropy p = log 2 ↔ p = 2⁻¹

theorem Real.binEntropy_continuous : Continuous binEntropy

Binary entropy is continuous everywhere. This is due to definition of Real.log for negative numbers.

theorem Real.differentiableAt_binEntropy {p : ℝ} (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : DifferentiableAt ℝ binEntropy p

theorem Real.differentiableAt_binEntropy_iff_ne_zero_one {p : ℝ} : DifferentiableAt ℝ binEntropy p ↔ p ≠ 0 ∧ p ≠ 1

theorem Real.deriv_binEntropy (p : ℝ) : deriv binEntropy p = log (1 - p) - log p

Binary entropy has derivative log (1 - p) - log p. It's not differentiable at 0 or 1 but the junk values of deriv and log coincide there.

q-ary entropy

noncomputable def Real.qaryEntropy (q : ℕ) (p : ℝ) : ℝ

Shannon q-ary Entropy function (measured in Nats, i.e., using natural logs).

It's the Shannon entropy of a random variable with possible outcomes {1, ..., q} where outcome 1 has probability 1 - p and all other outcomes are equally likely.

The usual domain of definition is p ∈ [0,1], i.e., input is a probability.

This is a generalization of the binary entropy function binEntropy.

@[simp]

theorem Real.qaryEntropy_zero (q : ℕ) : qaryEntropy q 0 = 0

@[simp]

theorem Real.qaryEntropy_one (q : ℕ) : qaryEntropy q 1 = log ↑(↑q - 1)

@[simp]

theorem Real.qaryEntropy_two : qaryEntropy 2 = binEntropy

theorem Real.qaryEntropy_pos {q : ℕ} {p : ℝ} (hp₀ : 0 < p) (hp₁ : p < 1) : 0 < qaryEntropy q p

theorem Real.qaryEntropy_nonneg {q : ℕ} {p : ℝ} (hp₀ : 0 ≤ p) (hp₁ : p ≤ 1) : 0 ≤ qaryEntropy q p

theorem Real.qaryEntropy_neg_of_neg {q : ℕ} {p : ℝ} (hp : p < 0) : qaryEntropy q p < 0

Outside the usual range of qaryEntropy, it is negative. This is due to log p = log |p|.

theorem Real.qaryEntropy_nonpos_of_nonpos {q : ℕ} {p : ℝ} (hp : p ≤ 0) : qaryEntropy q p ≤ 0

Outside the usual range of qaryEntropy, it is negative. This is due to log p = log |p|.

theorem Real.qaryEntropy_continuous {q : ℕ} : Continuous (qaryEntropy q)

The q-ary entropy function is continuous everywhere. This is due to definition of Real.log for negative numbers.

theorem Real.differentiableAt_qaryEntropy {q : ℕ} {p : ℝ} (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : DifferentiableAt ℝ (qaryEntropy q) p

theorem Real.deriv_qaryEntropy {q : ℕ} {p : ℝ} (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : deriv (qaryEntropy q) p = log (↑q - 1) + log (1 - p) - log p

theorem Real.hasDerivAt_binEntropy {p : ℝ} (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : HasDerivAt binEntropy (log (1 - p) - log p) p

Binary entropy has derivative log (1 - p) - log p.

theorem Real.hasDerivAt_qaryEntropy {q : ℕ} {p : ℝ} (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) : HasDerivAt (qaryEntropy q) (log (↑q - 1) + log (1 - p) - log p) p

theorem Real.not_continuousAt_deriv_qaryEntropy_one {q : ℕ} : ¬ContinuousAt (deriv (qaryEntropy q)) 1

theorem Real.not_continuousAt_deriv_qaryEntropy_zero {q : ℕ} : ¬ContinuousAt (deriv (qaryEntropy q)) 0

theorem Real.deriv2_qaryEntropy {q : ℕ} {p : ℝ} : deriv^[2] (qaryEntropy q) p = -1 / (p * (1 - p))

Second derivative of q-ary entropy.

theorem Real.deriv2_binEntropy {p : ℝ} : deriv^[2] binEntropy p = -1 / (p * (1 - p))

Strict monotonicity of entropy

theorem Real.qaryEntropy_strictMonoOn {q : ℕ} (qLe2 : 2 ≤ q) : StrictMonoOn (qaryEntropy q) (Set.Icc 0 (1 - 1 / ↑q))

Qary entropy is strictly increasing in the interval [0, 1 - q⁻¹].

theorem Real.qaryEntropy_strictAntiOn {q : ℕ} (qLe2 : 2 ≤ q) : StrictAntiOn (qaryEntropy q) (Set.Icc (1 - 1 / ↑q) 1)

Qary entropy is strictly decreasing in the interval [1 - q⁻¹, 1].

theorem Real.binEntropy_strictMonoOn : StrictMonoOn binEntropy (Set.Icc 0 2⁻¹)

Binary entropy is strictly increasing in interval [0, 1/2].

theorem Real.binEntropy_strictAntiOn : StrictAntiOn binEntropy (Set.Icc 2⁻¹ 1)

Binary entropy is strictly decreasing in interval [1/2, 1].

Strict concavity of entropy

theorem Real.strictConcaveOn_qaryEntropy {q : ℕ} : StrictConcaveOn ℝ (Set.Icc 0 1) (qaryEntropy q)

theorem Real.strictConcave_binEntropy : StrictConcaveOn ℝ (Set.Icc 0 1) binEntropy