Finite entropy, cross-entropy, and KL divergence

Definition

fep_finite_information

by ActiveInference · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-statefree-energy-principleinformation-theorykl-divergence

Information measures on finite laws: entropy, cross-entropy, and the finite KL divergence, with the nonnegativity and characterization lemmas the mission's theorems use.

For finite laws $p, q$ on a finite type $\alpha$ :

H(p) \;=\; \sum_x \mathrm{negMulLog}(p(x)), \qquad H(p, q) \;=\; \sum_x -\,p(x) \log q(x),

D_{\mathrm{KL}}(p \,\|\, q) \;=\; \sum_x q(x)\cdot \mathrm{klFun}\!\left(\frac{p(x)}{q(x)}\right), \qquad \mathrm{klFun}(x) = x \log x + 1 - x,

where Real.negMulLog is Mathlib's continuous extension with the exact convention $0 \cdot \log 0 = 0$ , so zero-mass atoms contribute exactly zero rather than by exception handling.

Proved in the same file, and needed by the mission's theorems:

entropy and KL are nonnegative (KL also at zero reference atoms, under the totalized real-division convention);
zero self-divergence, $D_{\mathrm{KL}}(p \,\|\, p) = 0$ ;
the pointwise conversion $q(x)\,\mathrm{klFun}(p(x)/q(x)) = -p(x)\log q(x) - \mathrm{negMulLog}(p(x)) + (q(x) - p(x))$ ;
separation without support assumptions: $D_{\mathrm{KL}}(p \,\|\, q) = 0 \iff p = q$ — normalization forces the actual law's mass to zero wherever the reference's is zero;
under full reference support, $D_{\mathrm{KL}}(p\,\|\,q) = H(p, q) - H(p)$ .

Formalization Note — transcribed verbatim from the proved module FepSketches.finite_information of the fep_lean formalization; klFun is Mathlib's InformationTheory.klFun; the file compiles sorry-free.

Definition code

import Definitions.Def_fep_finite_laws
import Mathlib.InformationTheory.KullbackLeibler.KLFun
import Mathlib.Tactic

/-!
# Finite information theory (mission substrate)

Transcribed from the proved module `FepSketches.finite_information` of the
fep_lean formalization (Active Inference Institute).  Entropy uses Mathlib's
continuous extension `Real.negMulLog`, so zero-mass atoms contribute exactly
zero.  Finite KL is represented by the nonnegative `klFun` integrand.
Normalization recovers separation even when the reference law has zero-mass
atoms; strict reference support is required only for the logarithmic
cross-entropy identity.
-/

namespace FreeEnergyPrinciple

open Finset InformationTheory
open scoped BigOperators

variable {α β : Type*} [Fintype α] [Fintype β]

/-- Shannon entropy in nats, with the convention `0 log 0 = 0`. -/
noncomputable def entropy (p : FiniteLaw α) : ℝ :=
  ∑ x, Real.negMulLog (p x)

/-- Expected negative log score of `q` under `p`. -/
noncomputable def crossEntropy (p q : FiniteLaw α) : ℝ :=
  ∑ x, -(p x) * Real.log (q x)

/-- Finite KL divergence as a weighted sum of Mathlib's nonnegative `klFun`. -/
noncomputable def finiteKL (p q : FiniteLaw α) : ℝ :=
  ∑ x, q x * klFun (p x / q x)

/-- Finite Shannon entropy is nonnegative. -/
theorem entropy_nonneg (p : FiniteLaw α) : 0 ≤ entropy p := by
  exact Finset.sum_nonneg fun x _ =>
    Real.negMulLog_nonneg (p.nonneg x) (p.mass_le_one x)

/-- Finite KL is nonnegative, including at zero reference atoms under the
totalized real-division convention. -/
theorem finiteKL_nonneg (p q : FiniteLaw α) : 0 ≤ finiteKL p q := by
  exact Finset.sum_nonneg fun x _ =>
    mul_nonneg (q.nonneg x)
      (klFun_nonneg (div_nonneg (p.nonneg x) (q.nonneg x)))

/-- A finite law has zero divergence from itself, including at zero atoms. -/
theorem finiteKL_self (p : FiniteLaw α) : finiteKL p p = 0 := by
  apply Finset.sum_eq_zero
  intro x _
  by_cases hx : p x = 0
  · simp [hx]
  · rw [div_self hx, klFun_one, mul_zero]

/-- Pointwise conversion from the `klFun` integrand to logarithmic scoring. -/
theorem weighted_klFun_eq_log_score {a b : ℝ} (hb : 0 < b) :
    b * klFun (a / b) =
      (-a * Real.log b - Real.negMulLog a) + (b - a) := by
  by_cases ha : a = 0
  · simp [ha, klFun_zero]
  · rw [klFun_apply, Real.negMulLog_eq_neg, Real.log_div ha (ne_of_gt hb)]
    field_simp [ne_of_gt hb]
    ring

/-- For normalized finite laws, totalized finite KL vanishes exactly at
equality, without any support assumption.  A zero divergence first forces
equality wherever the reference has positive mass.  Normalization then forces
the actual law to put zero mass on every zero-reference atom. -/
theorem finiteKL_eq_zero_iff (p q : FiniteLaw α) :
    finiteKL p q = 0 ↔ p = q := by
  classical
  constructor
  · intro hzero
    have hterms := (Finset.sum_eq_zero_iff_of_nonneg
      (fun y _ =>
        mul_nonneg (q.nonneg y)
          (klFun_nonneg (div_nonneg (p.nonneg y) (q.nonneg y))))).mp hzero
    have heq_of_reference_ne_zero : ∀ x, q x ≠ 0 → p x = q x := by
      intro x hx
      have hterm := hterms x (Finset.mem_univ x)
      have hfun : klFun (p x / q x) = 0 :=
        (mul_eq_zero.mp hterm).resolve_left hx
      have hratio : p x / q x = 1 :=
        (klFun_eq_zero_iff (div_nonneg (p.nonneg x) (q.nonneg x))).mp hfun
      exact (div_eq_one_iff_eq hx).mp hratio
    have hsplit :
        (∑ x : α, p x) =
          (∑ x : α, if q x = 0 then p x else 0) +
            ∑ x : α, if q x ≠ 0 then p x else 0 := by
      rw [← Finset.sum_add_distrib]
      apply Finset.sum_congr rfl
      intro x _
      by_cases hx : q x = 0 <;> simp [hx]
    have hpositiveMass :
        (∑ x : α, if q x ≠ 0 then p x else 0) = 1 := by
      calc
        (∑ x : α, if q x ≠ 0 then p x else 0) =
            ∑ x : α, if q x ≠ 0 then q x else 0 := by
              apply Finset.sum_congr rfl
              intro x _
              by_cases hx : q x = 0
              · simp [hx]
              · simp [hx, heq_of_reference_ne_zero x hx]
        _ = ∑ x : α, q x := by
          apply Finset.sum_congr rfl
          intro x _
          by_cases hx : q x = 0 <;> simp [hx]
        _ = 1 := q.sum_one
    have hzeroReferenceMass :
        (∑ x : α, if q x = 0 then p x else 0) = 0 := by
      linarith [p.sum_one, hsplit, hpositiveMass]
    apply FiniteLaw.ext_mass
    funext x
    by_cases hx : q x = 0
    · have hzeroTerms := (Finset.sum_eq_zero_iff_of_nonneg
        (fun y _ => by
          by_cases hy : q y = 0
          · simpa [hy] using p.nonneg y
          · simp [hy])).mp hzeroReferenceMass
      simpa [hx] using hzeroTerms x (Finset.mem_univ x)
    · exact heq_of_reference_ne_zero x hx
  · intro hpq
    subst p
    exact finiteKL_self q

/-- Under full reference support, finite KL is cross-entropy minus entropy. -/
theorem finiteKL_eq_crossEntropy_sub_entropy (p q : FiniteLaw α)
    (hq : ∀ x, 0 < q x) :
    finiteKL p q = crossEntropy p q - entropy p := by
  simp_rw [finiteKL, weighted_klFun_eq_log_score (hq _)]
  rw [Finset.sum_add_distrib, Finset.sum_sub_distrib]
  have hnorm : (∑ i : α, (q.mass i - p.mass i)) = 0 := by
    rw [Finset.sum_sub_distrib, q.sum_one, p.sum_one, sub_self]
  rw [hnorm, add_zero]
  rfl

end FreeEnergyPrinciple

Source

fep_lean / fep_formal v1.2.0 (Active Inference Institute), FepSketches.finite_information.lean (proved, 0 sorry); https://github.com/ActiveInferenceInstitute/fep_formal

Read-back

What the Lean code literally says, in plain math · glm-flash-latest

entropy. For a finite type $\\alpha$ (with a decidable-finite enumeration) and a FiniteLaw $p$ on $\\alpha$ — a nonnegative real-valued function with total mass $\\sum_x p(x) = 1$ — define

\\operatorname{entropy}(p) = \\sum_{x \\in \\alpha} \\varphi(p(x)),

where $\\varphi(t) = -t\\log t$ is implemented as Mathlib's total continuous extension $\\text{Real.negMulLog}$ , which by convention equals exactly $0$ at $t = 0$ (the $0\\log 0 = 0$ convention). This is the Shannon entropy in nats.

crossEntropy. For two finite laws $p, q$ on $\\alpha$ , define

\\operatorname{crossEntropy}(p, q) = \\sum_{x \\in \\alpha} -\\,p(x) \\cdot \\log q(x).

Note this is a total real-valued expression: when $q(x) = 0$ the term involves $\\log 0$ , which is undefined as a real logarithm, so the summand there takes whatever value $\\text{Real.log}\\, 0$ yields in the Lean total convention (a junk value); nothing in the definition guards against zero atoms of $q$ .

finiteKL. For finite laws $p, q$ on $\\alpha$ , define

\\operatorname{finiteKL}(p, q) = \\sum_{x \\in \\alpha} q(x) \\cdot \\text{klFun}\\big(p(x) / q(x)\\big),

where $\\text{klFun}(t) = t \\log t - t + 1$ for $t \\ge 0$ (extended by $0$ at $t=0$ ) is Mathlib's nonnegative integrand, and the division is totalized real division, so $p(x)/q(x)$ at $q(x) = 0$ is a junk value rather than an error. There is no hypothesis that $q$ has full support.

entropy_nonneg. For every finite law $p$ on $\\alpha$ , $0 \\le \\operatorname{entropy}(p)$ .

finiteKL_nonneg. For all finite laws $p, q$ on $\\alpha$ (no support or positivity assumptions), $0 \\le \\operatorname{finiteKL}(p, q)$ .

finiteKL_self. For every finite law $p$ on $\\alpha$ , $\\operatorname{finiteKL}(p, p) = 0$ , including at any atoms where $p(x) = 0$ .

weighted_klFun_eq_log_score. For all real numbers $a, b$ with $b > 0$ :

b \\cdot \\text{klFun}(a/b) \\;=\\; \\big(-a\\log b - \\varphi(a)\\big) + (b - a),

where $\\varphi(a) = \\text{Real.negMulLog}(a) = -a\\log a$ (with $\\varphi(0)=0$ ). Note this is stated for arbitrary reals $a$ ; if $a < 0$ the expression $\\varphi(a)$ is still well-defined via $\\text{Real.negMulLog}$ , but nothing in the hypothesis requires $a \\ge 0$ .

finiteKL_eq_zero_iff. For all finite laws $p, q$ on $\\alpha$ :

\\operatorname{finiteKL}(p, q) = 0 \\quad\\leftrightarrow\\quad p = q.

That is: the totalized finite KL vanishes if and only if the two laws are equal as mass functions, with no support assumption on the reference law $q$ .

finiteKL_eq_crossEntropy_sub_entropy. Let $p, q$ be finite laws on $\\alpha$ and assume the hypothesis $h_q$ : for every atom $x \\in \\alpha$ , $0 < q(x)$ — i.e. the reference law $q$ has full support with strictly positive mass at every atom (this excludes zero atoms of $q$ ; it does not exclude zero atoms of $p$ ). Then:

\\operatorname{finiteKL}(p, q) \\;=\\; \\operatorname{crossEntropy}(p, q) - \\operatorname{entropy}(p).

In full: under the strict full-support hypothesis on $q$ alone, the weighted sum $\\sum_x q(x)\\,\\text{klFun}(p(x)/q(x))$ equals the expected negative log score $\\sum_x -p(x)\\log q(x)$ minus the entropy $\\sum_x \\varphi(p(x))$ of $p$ . The proof uses, and the statement depends only on, the normalization identities $\\sum_x q(x) = 1$ and $\\sum_x p(x) = 1$ ; the identity is an exact equality, not an inequality. No claim is made here about the case where $q$ has a zero-mass atom.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by ActiveInference · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph