Variational free energy upper-bounds surprisal (measure-theoretic core)

Variational free energy upper-bounds surprisal — the measure-theoretic core of the free energy principle's evidence bound, in Mathlib's native nonnegative extended reals.

Let $\alpha$ be a measurable space and let $q$, $p$ be measures on $\alpha$ (no finiteness or absolute-continuity assumption). Fix a surprisal value $s \in \mathbb{R}_{\ge 0}^{\infty}$ — abstractly, the negative log marginal likelihood of the observed data, whatever its provenance. The variational free energy of the approximate posterior $q$ against the exact posterior $p$ is

where $D_{\mathrm{KL}}$ is Mathlib's InformationTheory.klDiv, valued in $\mathbb{R}_{\ge 0}^{\infty}$ and equal to $\infty$ unless $q \ll p$ with integrable log-likelihood ratio. Then, unconditionally:

The variational (KL) remainder can only push the free energy above the surprisal, never below it; the extended-real codomain absorbs every degenerate case, which is why the statement needs no side conditions. In the source catalogue this is the flagship bound of topic fep-002, "Variational Evidence Bound via KL Divergence": the bound is exact precisely when $q = p$ at finite surprisal — realized on the platform by the mission's finite-model uniqueness milestone.

Role: this is the abstract core every concrete instance of the free energy principle descends from; the goal theorem instantiates it with the KL gap closing exactly at the Bayesian posterior.

Formalization Note — the source states the theorem through a named definition (fep002_variationalFreeEnergy q posterior surprisal := surprisal + InformationTheory.klDiv q posterior); the statement here is that definition unfolded, so the platform theorem asserts the same inequality without carrying a separate one-line definition. Transcribed from topic fep-002 of the fep_lean formalization; compiled against the platform environment.