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_mul_log_div_leq {ι : Type u_1} {s : Finset ι} {a : ι → ℝ} {b : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (habs : ∀ i ∈ s, b i = 0 → a i = 0) : (∑ i ∈ s, a i) * Real.log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i) ≤ ∑ i ∈ s, a i * Real.log (a i / b i)

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}$$. We require additionally that, if $b_s=0$, then $s_s=0$ as otherwise the right hand side should morally be infinite, which it can't be in the formalization using real numbers.

theorem Real.sum_mul_log_div_eq_iff_aux {ι : Type u_1} {s : Finset ι} {a : ι → ℝ} {b : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 < b i) (heq : ∑ i ∈ s, a i * Real.log (a i / b i) = (∑ i ∈ s, a i) * Real.log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i)) : ∃ (r : ℝ), ∀ i ∈ 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}$. Auxiliary version assuming the b i are positive.

theorem Real.sum_mul_log_div_eq_iff {ι : Type u_1} {s : Finset ι} {a : ι → ℝ} {b : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) (habs : ∀ i ∈ s, b i = 0 → a i = 0) (heq : ∑ i ∈ s, a i * Real.log (a i / b i) = (∑ i ∈ s, a i) * Real.log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i)) : ∃ (r : ℝ), ∀ i ∈ 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}$.