Information inequalities

Inequalities relating entropies, divergences and mutual information, such as the log-sum, Pinsker, Fano, data-processing and Shearer inequalities.

TheoremLog-sum inequality#✓fully proved

Let \(s\) be a finite subset of a type \(\iota\) and let \(p, q : \iota \to \mathbb{R}\) satisfy \(p_i \ge 0\) and \(q_i > 0\) for all \(i \in s\). Then

\[ \Bigl(\sum_{i \in s} p_i\Bigr) \log \frac{\sum_{i \in s} p_i}{\sum_{i \in s} q_i} \le \sum_{i \in s} p_i \log \frac{p_i}{q_i}. \]

Here \(\log\) is the natural logarithm; a summand with \(p_i = 0\) is \(0\), and both sides are \(0\) when \(s\) is empty.

theorem sum_mul_log_sum_div_sum_le_sum_mul_log_div {ι : Type*} (s : Finset ι) (p q : ι → ℝ)
    (hp : ∀ i ∈ s, 0 ≤ p i) (hq : ∀ i ∈ s, 0 < q i) :
    (∑ i ∈ s, p i) * log ((∑ i ∈ s, p i) / ∑ i ∈ s, q i)
      ≤ ∑ i ∈ s, p i * log (p i / q i)

Used by 6

Used byLog-sum estimate for the fiber weights · Log-sum inequality for influences against damped influences · Data-processing inequality for entropy under a two-point mixture · Gibbs' inequality (evidence lower bound form) · Csiszár–Kullback–Pinsker inequality for strictly positive distributions · Fano's inequality, general form

• Data-processing inequality
• Fano's inequality
• Shearer's entropy inequality

TheoremCsiszár–Kullback–Pinsker inequality for strictly positive distributions#✓fully proved

Let \(\alpha\) be a finite nonempty set and let \(p, q : \alpha \to \mathbb{R}\) satisfy \(p(a) > 0\) and \(q(a) > 0\) for every \(a \in \alpha\) and \(\sum_a p(a) = \sum_a q(a) = 1\). Then, with the natural logarithm,

\[ \Bigl(\sum_{a \in \alpha} |p(a) - q(a)|\Bigr)^2 \le 2 \sum_{a \in \alpha} p(a) \log \frac{p(a)}{q(a)}. \]

Equivalently, the total variation distance \(\frac12 \sum_a |p(a) - q(a)|\) is at most \(\sqrt{D/2}\), where \(D = \sum_a p(a) \log (p(a)/q(a))\) is the Kullback–Leibler divergence.

theorem csiszar_kullback_pinsker
    {α : Type*} [Fintype α] [Nonempty α]
    (p q : α → ℝ)
    (hp_pos : ∀ a, 0 < p a)
    (hq_pos : ∀ a, 0 < q a)
    (hp_sum : ∑ a : α, p a = 1)
    (hq_sum : ∑ a : α, q a = 1) :
    (∑ a : α, |p a - q a|) ^ 2 ≤ 2 * ∑ a : α, p a * Real.log (p a / q a)

Sources

• M. S. Pinsker, Information and Information Stability of Random Variables and Processes (1960; English translation 1964), with I. Csiszar, Information-type measures of difference of probability distributions and indirect observations, Studia Sci. Math. Hungar. 2 (1967), 299-318.

Uses 1

Proof usesLog-sum inequality

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.