Applications of Jensen's inequality

In this chapter, \(h\) denotes the function \(h(x) := x \log \frac{1}{x}\) for \(x \in [0,1]\).

LemmaConcavity#

\(h\) is strictly concave on \([0,\infty)\).

Proof

Check that \(h'\) is strictly monotone decreasing.

Lean

Formalized as Real.strictConcaveOn_negMulLog.

Sources

• Polynomial Freiman-Ruzsa blueprint: chapter/jensen.tex, line 5

LeanReal.strictConcaveOn_negMulLog

Used by 5

Used byconverse log sum · Jensen bound · Nonnegativity of mutual information · Entropy of uniform random variable · Vanishing of mutual information

Lemmalog sum inequality#

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

Proof

Let \(B:=\sum_{s\in S} b_s\). Apply Jensen and Concavity to show that \(\sum_{s\in S} \frac{b_s}{B} h(\frac{a_s}{b_s})\ge h(\frac{\sum_{s\in S} a_s}{B})\).

Lean

Formalized as Real.sum_mul_log_div_leq.

Sources

• Polynomial Freiman-Ruzsa blueprint: chapter/jensen.tex, line 14

LeanReal.sum_mul_log_div_leq

Used by 3

Used byGibbs inequality · Convexity of Kullback–Leibler · Rho minus of subgroup

Lemmaconverse log sum#

If equality holds in log sum inequality, then \(a_s=r\cdot b_s\) for every \(s\in S\), for some constant \(r\in \mathbb{R}\).

Proof

By the fact that \(h\) is strictly concave and the equality condition of Jensen.

Lean

Formalized as Real.sum_mul_log_div_eq_iff.

Sources

• Polynomial Freiman-Ruzsa blueprint: chapter/jensen.tex, line 24

LeanReal.sum_mul_log_div_eq_iff

Uses 1 · Used by 1

Proof usesConcavity

Used byConverse Gibbs inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.