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.eq_tilted_of_freeEnergy_eq_cgf — and only there.
• InformationTheory.isGreatest_cgf — the variational principle: cgf f μ 1 is the greatest value of freeEnergy μ f over admissible q.
• MeasureTheory.tilted_real_singleton — on a finite type, the tilted measure at an atom; MeasureTheory.eq_tilted_iff, a measure is a tilt exactly when its atoms are proportional.

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.eq_tilted_of_freeEnergy_eq_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)) μ) (h : μ.freeEnergy f q = ProbabilityTheory.cgf f μ 1) : q = μ.tilted f

The variational bound is attained only at the Gibbs measure: a probability measure q ≪ μ with freeEnergy μ f q = cgf f μ 1 is μ.tilted f. From the decomposition identity, KL(q ‖ μ.tilted f) = 0.

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).

theorem MeasureTheory.tilted_real_singleton {α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] (f : α → ℝ) (a : α) : (μ.tilted f).real {a} = μ.real {a} * Real.exp (f a) / ∑ b : α, μ.real {b} * Real.exp (f b)

On a finite type, the tilted measure at an atom is the atom's mass reweighted by the exponential of f and renormalized.

theorem MeasureTheory.eq_tilted_iff {α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (μ ν : Measure α) [IsProbabilityMeasure μ] [IsFiniteMeasure ν] [NeZero ν] (f : α → ℝ) : μ = ν.tilted f ↔ ∃ Z > 0, ∀ (a : α), μ.real {a} = ν.real {a} * Real.exp (f a) / Z

On a finite type, a probability measure is the tilt of ν by f exactly when its atoms are proportional to those of ν reweighted by the exponential of f.