3.1 Real-valued KL bridge
Definition
3.1
Real-valued KL
Lean: InformationTheory.klDivReal
For measures \(P, Q\) on a measurable space, set
\[ \mathrm{KL}_\mathbb {R}(P, Q) \; :=\; \begin{cases} \int \log \tfrac {\mathrm{d}P}{\mathrm{d}Q}\, \mathrm{d}P & \text{if $P \ll Q$,}\\ 0 & \text{otherwise.} \end{cases} \]
This bridges Mathlib’s ENNReal-valued klDiv to \(\mathbb {R}\) for linarith-compatible arithmetic; the identity \(\mathrm{KL}_\mathbb {R}(P,Q) = (\mathrm{KL}(P,Q)).\mathrm{toReal}\) holds unconditionally (klDivReal_eq_toReal_klDiv) [ 7 , § 2.3 ] , [ 16 , § 2.1 ] .
Theorem
3.2
Non-negativity
Lean: InformationTheory.klDivReal_nonneg
\(\mathrm{KL}_\mathbb {R}(P, Q) \ge 0\) for all measures (Gibbs’ inequality) [ 7 , Thm 2.6.3 ] .
Theorem
3.3
Zero iff equal, under finiteness
Lean: InformationTheory.klDivReal_eq_zero_iff
If \(P \ll Q\), \(\mathrm{KL}(P, Q) \ne \infty \), and both are finite measures, then \(\mathrm{KL}_\mathbb {R}(P, Q) = 0 \iff P = Q\) [ 7 , Thm 2.6.3 ] .