90 Communication Complexity — KL Divergence

90.1 Overview

This module develops concrete sum formulas for the Kullback–Leibler divergence on finite measurable spaces, bridging Mathlib’s InformationTheory.klDiv with the PFR real-valued KLDiv entropy API. The main results give explicit pointwise summation formulas for KL divergence between finite measures and PMFs, and show how they specialize to the Boolean (\(\mathrm{Bool}\)) case.

90.2 Declarations

Theorem 90.1 KL divergence as log-likelihood ratio sum (absolutely continuous case)

✓

Let \(\Omega \) be a finite measurable space and let \(\mu , \nu \) be finite measures on \(\Omega \) with \(\mu \ll \nu \). Then

\[ D_{\mathrm{KL}}(\mu \, \| \, \nu ) = \mathrm{ofReal}\! \left( \sum _{\omega : \Omega } \mu .\mathrm{real}\, \{ \omega \} \cdot \mathrm{llr}(\mu ,\nu ,\omega ) + \nu .\mathrm{real}\, \mathrm{univ} - \mu .\mathrm{real}\, \mathrm{univ} \right), \]

where \(\mathrm{llr}(\mu ,\nu ,\omega ) = \log \frac{d\mu }{d\nu }(\omega )\) is the log-likelihood ratio at \(\omega \).

Theorem 90.2 KL divergence as log-likelihood ratio sum

✓

Let \(\Omega \) be a finite measurable space and let \(\mu , \nu \) be finite measures on \(\Omega \). Then

\[ D_{\mathrm{KL}}(\mu \, \| \, \nu ) = \begin{cases} \infty & \text{if } \exists \, \omega ,\; \nu \{ \omega \} = 0 \text{ and } \mu \{ \omega \} \neq 0,\\[4pt] \mathrm{ofReal}\! \displaystyle \left( \sum _{\omega }\mu .\mathrm{real}\, \{ \omega \} \cdot \mathrm{llr}(\mu ,\nu ,\omega ) +\nu .\mathrm{real}\, \mathrm{univ}-\mu .\mathrm{real}\, \mathrm{univ} \right) & \text{otherwise.} \end{cases} \]

Theorem 90.3 KL divergence between PMFs as log-likelihood ratio sum

✓

Let \(\Omega \) be a finite measurable space and let \(p, q\) be PMFs on \(\Omega \). Then

\[ D_{\mathrm{KL}}(p \, \| \, q) = \begin{cases} \infty & \text{if } \exists \, \omega ,\; q(\omega ) = 0 \text{ and } p(\omega ) \neq 0,\\[4pt] \mathrm{ofReal}\! \displaystyle \left( \sum _{\omega } p(\omega ).\mathrm{toReal} \cdot \mathrm{llr}(p,q,\omega ) \right) & \text{otherwise.} \end{cases} \]

Theorem 90.4 Radon–Nikodym derivative equals singleton mass ratio

✓

Let \(\Omega \) be a finite measurable space, \(\mu \ll \nu \) finite measures, and \(\omega \in \Omega \) with \(\nu \{ \omega \} \neq 0\). Then the real-valued Radon–Nikodym derivative satisfies

\[ \left(\frac{d\mu }{d\nu }(\omega )\right).\mathrm{toReal} = \frac{\mu .\mathrm{real}\, \{ \omega \} }{\nu .\mathrm{real}\, \{ \omega \} }. \]

Theorem 90.5 Singleton mass times log-likelihood ratio equals log of mass ratio

✓

Let \(\Omega \) be a finite measurable space, \(\mu \ll \nu \) finite measures, and \(\omega \in \Omega \). Then

\[ \mu .\mathrm{real}\, \{ \omega \} \cdot \mathrm{llr}(\mu ,\nu ,\omega ) = \mu .\mathrm{real}\, \{ \omega \} \cdot \log \! \left( \frac{\mu .\mathrm{real}\, \{ \omega \} }{\nu .\mathrm{real}\, \{ \omega \} } \right). \]

Theorem 90.6 KL divergence as logarithmic mass ratio sum

✓

Let \(\Omega \) be a finite measurable space and let \(\mu , \nu \) be finite measures on \(\Omega \). Then

\[ D_{\mathrm{KL}}(\mu \, \| \, \nu ) = \begin{cases} \infty & \text{if } \exists \, \omega ,\; \nu \{ \omega \} = 0 \text{ and } \mu \{ \omega \} \neq 0,\\[4pt] \mathrm{ofReal}\! \displaystyle \left( \sum _{\omega } \mu .\mathrm{real}\, \{ \omega \} \cdot \log \! \frac{\mu .\mathrm{real}\, \{ \omega \} }{\nu .\mathrm{real}\, \{ \omega \} } +\nu .\mathrm{real}\, \mathrm{univ}-\mu .\mathrm{real}\, \mathrm{univ} \right) & \text{otherwise.} \end{cases} \]

Theorem 90.7 KL divergence is finite to full-support probability measure

✓

Let \(\Omega \) be a finite measurable space and let \(\mu , \nu \) be probability measures on \(\Omega \). If \(\nu \) has full support (i.e. \(\nu .\mathrm{toPMF}(\omega ) \neq 0\) for all \(\omega \)), then \(D_{\mathrm{KL}}(\mu \, \| \, \nu ) \neq \infty \).

Theorem 90.8 KL divergence between PMFs as logarithmic mass ratio sum

✓

Let \(\Omega \) be a finite measurable space and let \(p, q\) be PMFs on \(\Omega \). Then

\[ D_{\mathrm{KL}}(p \, \| \, q) = \begin{cases} \infty & \text{if } \exists \, \omega ,\; q(\omega ) = 0 \text{ and } p(\omega ) \neq 0,\\[4pt] \mathrm{ofReal}\! \displaystyle \left( \sum _{\omega } p(\omega ).\mathrm{toReal} \cdot \log \! \frac{p(\omega ).\mathrm{toReal}}{q(\omega ).\mathrm{toReal}} \right) & \text{otherwise.} \end{cases} \]

Theorem 90.9 Boolean KL divergence matches PFR KLDiv

✓

Let \(\mu , \nu \) be probability measures on \(\mathrm{Bool}\) with \(\nu \) of full support. Then

\[ \bigl(D_{\mathrm{KL}}(\mu \, \| \, \nu )\bigr).\mathrm{toReal} = \mathrm{KL}[\mathrm{id};\mu \, \# \, \mathrm{id};\nu ], \]

where the right-hand side is the PFR real-valued KL divergence of the identity random variable.

Theorem 90.10 KL divergence of pushed-forward Boolean variable matches PFR KLDiv

✓

Let \(\mu \) be a finite measure on a measurable space \(\Omega \), \(X : \Omega \to \mathrm{Bool}\) a measurable function, \(S \subseteq \Omega \) a set with \(\mu .\mathrm{real}\, S \neq 0\), and \(\nu \) a full-support probability measure on \(\mathrm{Bool}\). Then

\[ \bigl(D_{\mathrm{KL}}(X_*(\mu [\cdot |S]) \, \| \, \nu )\bigr).\mathrm{toReal} = \mathrm{KL}[X;\mu [\cdot |S] \, \# \, \mathrm{id};\nu ]. \]