Shannon entropy

Definitions and facts about the Shannon entropy function -x*ln(x), both on a single variable and on a distribution.

There is significant overlap with Real.negMulLog and Real.binEntropy in Mathlib, and probably these files could be combined in some form.

def H₁ : Prob → ℝ

The one-event entropy function, H₁(p) = -p*ln(p). Uses nits.

Equations

• H₁ x = -↑x * Real.log ↑x

@[simp]

def H₁_zero_eq_zero : H₁ 0 = 0

H₁ of 0 is zero.

Equations

• H₁_zero_eq_zero = ⋯

@[simp]

def H₁_one_eq_zero : H₁ 1 = 0

H₁ of 1 is zero.

Equations

• H₁_one_eq_zero = ⋯

theorem H₁_nonneg (p : Prob) : 0 ≤ H₁ p

Entropy is nonnegative.

theorem H₁_le_1 (p : Prob) : H₁ p < 1

Entropy is less than 1.

theorem H₁_le_exp_m1 (p : Prob) : H₁ p ≤ Real.exp (-1)

TODO: Entropy is at most 1/e.

theorem H₁_concave (x y p : Prob) : p.mix (H₁ x) (H₁ y) ≤ H₁ (p.mix x y)

def Hₛ {α : Type u} [Fintype α] (d : Distribution α) : ℝ

The Shannon entropy of a discrete distribution, H(X) = ∑ H₁(p_x).

Equations

• Hₛ d = ∑ x : α, H₁ (d.prob x)

theorem Hₛ_nonneg {α : Type u} [Fintype α] (d : Distribution α) : 0 ≤ Hₛ d

Shannon entropy of a distribution is nonnegative.

theorem Hₛ_le_log_d {α : Type u} [Fintype α] (d : Distribution α) : Hₛ d ≤ Real.log ↑Finset.univ.card

Shannon entropy of a distribution is at most ln d.

@[simp]

theorem Hₛ_constant_eq_zero {α : Type u} [Fintype α] {i : α} : Hₛ (Distribution.constant i) = 0

The shannon entropy of a constant variable is zero.

theorem Hₛ_uniform {α : Type u} [Fintype α] [Nonempty α] : Hₛ Distribution.uniform = Real.log ↑Finset.univ.card

Shannon entropy of a uniform distribution is ln d.