The Gibbs / Donsker–Varadhan variational principle [UPSTREAM]

For a probability measure μ and a function f, the free energy q ↦ 𝔼_q[f] − KL(q ‖ μ) is maximized over probability measures q ≪ μ by the exponentially tilted (Gibbs) measure μ.tilted f, the maximal value being the cumulant generating function cgf f μ 1 = log ∫ exp f ∂μ. This is the Gibbs variational principle (a.k.a. Donsker–Varadhan), the variational characterization of the Kullback–Leibler divergence whose existence is anticipated by the module docstring of Mathlib/MeasureTheory/Measure/Tilted.lean.

Main definitions

• MeasureTheory.Measure.freeEnergy μ f q = 𝔼_q[f] − (klDiv q μ).toReal — the free-energy functional whose greatest value is the variational principle's value.

Main statements

• InformationTheory.toReal_klDiv_tilted_right — the Gibbs decomposition identity: KL(q ‖ μ.tilted f) = KL(q ‖ μ) − 𝔼_q[f] + cgf f μ 1.
• InformationTheory.freeEnergy_le_cgf — the variational inequality: freeEnergy μ f q ≤ cgf f μ 1 for every probability measure q ≪ μ.
• InformationTheory.freeEnergy_tilted — the bound is attained at μ.tilted f.
• InformationTheory.isGreatest_cgf — the variational principle: cgf f μ 1 is the greatest value of freeEnergy μ f over admissible q.

Implementation notes

The decomposition repackages MeasureTheory.integral_llr_tilted_right at the klDiv level: μ.tilted f is a probability measure, so both klDiv terms collapse to their llr-integrals via toReal_klDiv_of_measure_eq. The value is the cumulant generating function cgf f μ 1 (= log ∫ exp f ∂μ), connecting the principle to the Probability/Moments API. The candidate q is pinned to [IsProbabilityMeasure] by integral_llr_tilted_right (which requires it on its left measure), so relaxing it is a separate upstream concern in LogLikelihoodRatio.

noncomputable def MeasureTheory.Measure.freeEnergy {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) (f : α → ℝ) (q : Measure α) : ℝ

The free-energy functional 𝔼_q[f] − KL(q ‖ μ), whose greatest value over probability measures q ≪ μ is the Gibbs / Donsker–Varadhan variational principle.

Equations

• μ.freeEnergy f q = ∫ (a : α), f a ∂q - (InformationTheory.klDiv q μ).toReal

theorem InformationTheory.toReal_klDiv_tilted_right {α : Type u_1} {mα : MeasurableSpace α} (μ q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure q] {f : α → ℝ} (hqμ : q.AbsolutelyContinuous μ) (h_int_llr : MeasureTheory.Integrable (MeasureTheory.llr q μ) q) (h_int_f : MeasureTheory.Integrable f q) (h_exp : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) : (klDiv q (μ.tilted f)).toReal = (klDiv q μ).toReal - ∫ (x : α), f x ∂q + ProbabilityTheory.cgf f μ 1

Gibbs decomposition identity: for probability measures q ≪ μ, the Kullback–Leibler divergence from the Gibbs measure μ.tilted f splits as KL(q ‖ μ.tilted f) = KL(q ‖ μ) − 𝔼_q[f] + cgf f μ 1.

A klDiv-level repackaging of integral_llr_tilted_right: μ.tilted f is a probability measure, so both divergences collapse to their llr-integrals via toReal_klDiv_of_measure_eq, after which the log-likelihood-ratio decomposition closes it (the value being cgf f μ 1 = log ∫ exp f ∂μ).

theorem InformationTheory.freeEnergy_le_cgf {α : Type u_1} {mα : MeasurableSpace α} (μ q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure q] {f : α → ℝ} (hqμ : q.AbsolutelyContinuous μ) (h_int_llr : MeasureTheory.Integrable (MeasureTheory.llr q μ) q) (h_int_f : MeasureTheory.Integrable f q) (h_exp : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) : μ.freeEnergy f q ≤ ProbabilityTheory.cgf f μ 1

Gibbs / Donsker–Varadhan variational inequality: for every probability measure q ≪ μ, the free energy is bounded by the cumulant generating function, freeEnergy μ f q ≤ cgf f μ 1. Immediate from the decomposition identity and 0 ≤ KL.

theorem InformationTheory.freeEnergy_tilted {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → ℝ} (h_int_f : MeasureTheory.Integrable f (μ.tilted f)) (h_int_llr : MeasureTheory.Integrable (MeasureTheory.llr (μ.tilted f) μ) (μ.tilted f)) (h_exp : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) : μ.freeEnergy f (μ.tilted f) = ProbabilityTheory.cgf f μ 1

The variational bound freeEnergy_le_cgf is attained at the Gibbs measure μ.tilted f: freeEnergy μ f (μ.tilted f) = cgf f μ 1. Immediate from the decomposition at q = μ.tilted f, where KL(μ.tilted f ‖ μ.tilted f) vanishes.

theorem InformationTheory.isGreatest_cgf {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → ℝ} (h_int_f : MeasureTheory.Integrable f (μ.tilted f)) (h_int_llr : MeasureTheory.Integrable (MeasureTheory.llr (μ.tilted f) μ) (μ.tilted f)) (h_exp : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) μ) : IsGreatest (μ.freeEnergy f '' {q : MeasureTheory.Measure α | MeasureTheory.IsProbabilityMeasure q ∧ q.AbsolutelyContinuous μ ∧ MeasureTheory.Integrable (MeasureTheory.llr q μ) q ∧ MeasureTheory.Integrable f q}) (ProbabilityTheory.cgf f μ 1)

Gibbs / Donsker–Varadhan variational principle: the cumulant generating function cgf f μ 1 is the greatest value of the free-energy functional freeEnergy μ f over probability measures q ≪ μ (with the relevant integrability), the maximum being attained at the Gibbs measure μ.tilted f. Bundles freeEnergy_le_cgf (upper bound) and freeEnergy_tilted (attainment).