Entropy function

The purpose of this file is to record basic analytic properties of the function $$h(x) = - x * \log x$$ on the unit interval, for use in the theory of Shannon entropy.

Main results

• sum_negMulLog_le: a Jensen inequality for negMulLog
• sum_negMulLog_eq: the equality case of this inequality

theorem Real.sum_negMulLog_le {ι : Type u_1} {s : Finset ι} {w : ι → ℝ} {p : ι → ℝ} (h₀ : ∀ i ∈ s, 0 ≤ w i) (h₁ : (s.sum fun (i : ι) => w i) = 1) (hmem : ∀ i ∈ s, 0 ≤ p i) : (s.sum fun (i : ι) => w i * (p i).negMulLog) ≤ (s.sum fun (i : ι) => w i * p i).negMulLog

Jensen's inequality for the entropy function.

theorem Real.sum_negMulLog_lt {ι : Type u_1} {s : Finset ι} {w : ι → ℝ} {p : ι → ℝ} (h₀ : ∀ i ∈ s, 0 < w i) (h₁ : (s.sum fun (i : ι) => w i) = 1) (hmem : ∀ i ∈ s, 0 ≤ p i) (hp : ∃ j ∈ s, ∃ k ∈ s, p j ≠ p k) : (s.sum fun (i : ι) => w i * (p i).negMulLog) < (s.sum fun (i : ι) => w i * p i).negMulLog

The strict Jensen inequality for the entropy function.

theorem Real.sum_negMulLog_eq_iff {ι : Type u_1} {s : Finset ι} {w : ι → ℝ} {p : ι → ℝ} (h₀ : ∀ i ∈ s, 0 < w i) (h₁ : (s.sum fun (i : ι) => w i) = 1) (hmem : ∀ i ∈ s, 0 ≤ p i) : (s.sum fun (i : ι) => w i * (p i).negMulLog) = (s.sum fun (i : ι) => w i * p i).negMulLog ↔ ∀ j ∈ s, p j = s.sum fun (i : ι) => w i * p i

The equality case of Jensen's inequality for the entropy function.

theorem Real.sum_negMulLog_eq_iff' {ι : Type u_1} {s : Finset ι} {w : ι → ℝ} {p : ι → ℝ} (h₀ : ∀ i ∈ s, 0 ≤ w i) (h₁ : (s.sum fun (i : ι) => w i) = 1) (hmem : ∀ i ∈ s, 0 ≤ p i) : (s.sum fun (i : ι) => w i * (p i).negMulLog) = (s.sum fun (i : ι) => w i * p i).negMulLog ↔ ∀ j ∈ s, w j ≠ 0 → p j = s.sum fun (i : ι) => w i * p i

The equality case of Jensen's inequality for the entropy function.

theorem Real.sum_mul_log_div_leq {ι : Type u_1} {s : Finset ι} {a : { x : ι // x ∈ s } → ℝ} {b : { x : ι // x ∈ s } → ℝ} (ha : ∀ (i : { x : ι // x ∈ s }), 0 ≤ a i) (hb : ∀ (i : { x : ι // x ∈ s }), 0 ≤ b i) : (Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i * (a i / b i).log) ≤ (Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i) * ((Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i) / Finset.univ.sum fun (i : { x : ι // x ∈ s }) => b i).log

If $S$ is a finite set, and $a_s,b_s$ are non-negative for $s\in S$, then $$\sum_{s\in S} a_s \log\frac{a_s}{b_s}\ge \left(\sum_{s\in S}a_s\right)\log\frac{\sum_{s\in S} a_s}{\sum_{s\in S} b_s},$$ with the convention $0\log\frac{0}{b}=0$ for any $b\ge 0$ and $0\log\frac{a}{0}=\infty$ for any $a>0$.

theorem Real.sum_mul_log_div_eq_iff {ι : Type u_1} {s : Finset ι} {a : { x : ι // x ∈ s } → ℝ} {b : { x : ι // x ∈ s } → ℝ} (ha : ∀ (i : { x : ι // x ∈ s }), 0 ≤ a i) (hb : ∀ (i : { x : ι // x ∈ s }), 0 ≤ b i) (heq : (Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i * (a i / b i).log) = (Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i) * ((Finset.univ.sum fun (i : { x : ι // x ∈ s }) => a i) / Finset.univ.sum fun (i : { x : ι // x ∈ s }) => b i).log) : ∃ (r : ℝ), ∀ (i : { x : ι // x ∈ s }), a i = r * b i

If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$.