RelEntPositivity · section of the QIQT-H book

QIQTH.RelEntPositivity

← all sections · ← RecordContract · RicciSymm →

RelEntPositivity · entries 582–583 of 1000

Definition 582 (KL). source ↗

Classical KL non-negativity — the finite-distribution version of Klein’s inequality. Provable from the elementary log inequality log x ≤ x − 1 (i.e. −log x ≥ 1 − x).

For finite probability distributions p, q : ι → ℝ: KL(p ‖ q) := Σ_i p_i · log(p_i / q_i) ≥ 0.

We axiomatize at this layer to keep the file small; the proof is Real.log_le_sub_one_of_pos applied to each term plus Finset.sum_nonneg.

\mathrm{KL}\,\iota\,s\,p\,q \;:=\; \sum_{i s} p\,i \cdot \log\,(p\,i / q\,i)

Used by clausius_package_from_finite_model, qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_ppwave, qiqt_gr_ppwave_showcase, qiqt_gr_freefield_thermo, KL_classical_nonneg.

Lemma 583 (KL_classical_nonneg). source ↗

Klein-style inequality for finite classical KL — PROVED (the full-support finite Gibbs’ inequality: q strictly positive on all of s, the standard hypothesis; the more general support-degenerate form would instead require only p_i > 0 → q_i > 0 with the 0·log(0/q)=0 convention). Discharges the former axiom by the elementary log bound Real.log x ≤ x − 1: termwise p_i - q_i ≤ p_i·log(p_i/q_i), then sum and use ∑ p = ∑ q = 1. This is the finite-classical shadow of Klein / relative-entropy positivity (Open Problem 9 / the information bound behind Open Problem 6); the continuum vN-algebraic D_nonneg remains analytic (operator convexity of −log, not in Mathlib).

(\forall i\in s, 0 \le p\,i) \to (\forall i\in s, 0 < q\,i) \to \sum_{i s} p\,i = 1 \to \sum_{i s} q\,i = 1 \to 0 \le \href{/browser/qiqth-relentpositivity#d-qiqth-relentpositivity-kl}{D_{\mathrm{KL}}({p}\,\|\,{q})}

Proof. Immediate from the definitions. $\square$

Used by clausius_package_from_finite_model.

← all sections · ← RecordContract · RicciSymm →