Kullback–Leibler divergence

In the definitions below, \(G\) is a set.

DefinitionKullback–Leibler divergence#

If \(X,Y\) are two \(G\)-valued random variables, the Kullback–Leibler divergence is defined as

\[ D_{KL}(X\Vert Y) := \sum_x \mathbf{P}(X=x) \log \frac{\mathbf{P}(X=x)}{\mathbf{P}(Y=x)}. \]
Lean

Formalized as KLDiv.

Sources
LeanKLDiv
Used by 4
Used byGibbs inequality · Convexity of Kullback–Leibler · Kullback–Leibler divergence of copy · Kullback–Leibler and injections

LemmaKullback–Leibler divergence of copy#

If \(X'\) is a copy of \(X\), and \(Y'\) is a copy of \(Y\), then \(D_{KL}(X'\Vert Y') = D_{KL}(X\Vert Y)\).

Proof

Clear from definition.

Lean

Formalized as ProbabilityTheory.IdentDistrib.KLDiv_eq.

Sources
LeanProbabilityTheory.IdentDistrib.KLDiv_eq
Uses 1
Proof usesKullback–Leibler divergence

LemmaGibbs inequality#

\(D_{KL}(X\Vert Y) \geq 0\).

Proof

Apply log sum inequality on the definition.

Lean

Formalized as KLDiv_nonneg.

Sources
LeanKLDiv_nonneg
Uses 2 · Used by 1
Statement usesKullback–Leibler divergence
Proof useslog sum inequality
Used byConditional Gibbs inequality

LemmaConverse Gibbs inequality#

If \(D_{KL}(X\Vert Y) = 0\), then \(Y\) is a copy of \(X\).

Proof

Apply converse log sum.

Lean

Formalized as KLDiv_eq_zero_iff_identDistrib.

Sources
LeanKLDiv_eq_zero_iff_identDistrib
Uses 1
Proof usesconverse log sum

LemmaConvexity of Kullback–Leibler#

If \(S\) is a finite set, \(\sum_{s \in S} w_s = 1\) for some non-negative \(w_s\), and \({\bf P}(X=x) = \sum_{s\in S} w_s {\bf P}(X_s=x)\), \({\bf P}(Y=x) = \sum_{s\in S} w_s {\bf P}(Y_s=x)\) for all \(x\), then

\[ D_{KL}(X\Vert Y) \le \sum_{s\in S} w_s D_{KL}(X_s\Vert Y_s). \]
Proof

For each \(x\), replace \(\log \frac{\mathbf{P}(X_s=x)}{\mathbf{P}(Y_s=x)}\) in the definition with \(\log \frac{w_s\mathbf{P}(X_s=x)}{w_s\mathbf{P}(Y_s=x)}\) for each \(s\), and apply log sum inequality.

Lean

Formalized as KLDiv_of_convex.

Sources
LeanKLDiv_of_convex
Uses 2 · Used by 1
Proof usesKullback–Leibler divergence · log sum inequality
Used byKullback–Leibler and sums

LemmaKullback–Leibler and injections#

If \(f:G \to H\) is an injection, then \(D_{KL}(f(X)\Vert f(Y)) = D_{KL}(X\Vert Y)\).

Proof

Clear from definition.

Lean

Formalized as KLDiv_of_comp_inj.

Sources
LeanKLDiv_of_comp_inj
Uses 1 · Used by 2
Proof usesKullback–Leibler divergence
Used byKullback–Leibler and sums · Rho invariant

Now let \(G\) be an additive group.

LemmaKullback–Leibler and sums#

If \(X, Y, Z\) are independent \(G\)-valued random variables, then

\[ D_{KL}(X+Z\Vert Y+Z) \leq D_{KL}(X\Vert Y). \]
Proof

For each \(z\), \(D_{KL}(X+z\Vert Y+z)=D_{KL}(X\Vert Y)\) by Kullback–Leibler and injections. Then apply Convexity of Kullback–Leibler with \(w_z=\mathbf{P}(Z=z)\).

Lean

Formalized as KLDiv_add_le_KLDiv_of_indep.

Sources
LeanKLDiv_add_le_KLDiv_of_indep
Uses 2 · Used by 1
Proof usesKullback–Leibler and injections · Convexity of Kullback–Leibler
Used byRho and sums

LemmaKullback–Leibler and conditioning#

If \(X, Y\) are independent \(G\)-valued random variables, and \(Z\) is another random variable defined on the same sample space as \(X\), then

\[ D_{KL}((X|Z)\Vert Y) = D_{KL}(X\Vert Y) + \mathbb{H}[X] - \mathbb{H}[X|Z]. \]
Proof

Compare the terms correspond to each \(x\in G\) on both sides.

Lean

Formalized as condKLDiv_eq.

Sources
LeancondKLDiv_eq
Used by 1
Used byRho and conditioning

LemmaConditional Gibbs inequality#

\(D_{KL}((X|W)\Vert Y) \geq 0\).

Proof

Clear from Definition Conditional Kullback–Leibler divergence and Lemma Gibbs inequality.

Lean

Formalized as condKLDiv_nonneg.

Sources
LeancondKLDiv_nonneg
Uses 1
Proof usesGibbs inequality

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.