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).negMulLog

@[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)

Entropy is at most 1/e.

theorem H₁_concave (x y p : Prob) : p[H₁ x↔H₁ y] ≤ H₁ (p[x↔y])

def Hₛ {α : Type u_1} [Fintype α] (d : ProbDistribution α) : ℝ

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_1} [Fintype α] (d : ProbDistribution α) : 0 ≤ Hₛ d

Shannon entropy of a distribution is nonnegative.

theorem Hₛ_le_log_d {α : Type u_1} [Fintype α] (d : ProbDistribution α) : Hₛ d ≤ Real.log ↑(Fintype.card α)

Shannon entropy of a distribution is at most ln d.

@[simp]

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

The shannon entropy of a constant variable is zero.

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

Shannon entropy of a uniform distribution is ln d.

theorem Hₛ_coin (p : Prob) : Hₛ (ProbDistribution.coin p) = Real.binEntropy ↑p

Shannon entropy of two-event distribution.

theorem Hₛ_eq_of_multiset_map_eq {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (d₁ : ProbDistribution α) (d₂ : ProbDistribution β) (h : Multiset.map d₁.prob Finset.univ.val = Multiset.map d₂.prob Finset.univ.val) : Hₛ d₁ = Hₛ d₂