The Donsker–Varadhan variational formula for relative entropy

For finite measures μ and ν, Mathlib's relative entropy klDiv μ ν is the I-divergence ∫ klFun (dμ/dν) dν, where klFun x = x log x + 1 - x, and it carries the mass correction ν univ - μ univ. The convex conjugate of klFun is y ↦ exp y - 1, and integrating the Fenchel–Young inequality gives a variational formula with the mass correction built in: klDiv μ ν = sup_f (∫ f dμ - ∫ (exp f - 1) dν), the supremum running over bounded measurable functions. On a normal Borel space with weakly regular μ + ν, the bounded continuous functions already give the supremum; finite measures on pseudometrizable Borel spaces satisfy these hypotheses. For probability measures the formula takes the classical Donsker–Varadhan form klDiv μ ν = sup_f (∫ f dμ - log ∫ exp f dν).

Each functional (μ, ν) ↦ ∫ f dμ - ∫ (exp f - 1) dν with f bounded and continuous is continuous for the weak topology, so the continuous form of the formula makes klDiv jointly lower semicontinuous on pairs of finite measures, and on pairs of probability measures. This is the lower semicontinuity used by stability and limit theorems for entropic optimal transport, where both the coupling and the reference measure move.

Main statements

• TauCeti.mul_sub_exp_sub_one_le_klFun: the Fenchel–Young inequality x * y - (exp y - 1) ≤ klFun x for x ≥ 0.
• TauCeti.mul_sub_exp_sub_one_eq_klFun_iff: its equality case, x = exp y.
• TauCeti.ofReal_integral_sub_integral_exp_sub_one_le_klDiv and TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv: the variational lower bounds, for every integrable f with integrable exp ∘ f.
• TauCeti.integral_sub_integral_indicator_exp_sub_one_eq and TauCeti.ae_mul_sub_indicator_exp_sub_one_le_klFun: for μ ≪ ν, the truncated objective as a single ν-integral against the density, and the pointwise Fenchel–Young bound on its integrand.
• TauCeti.ofReal_integral_sub_integral_indicator_exp_sub_one_le_klDiv: the first bound with exp ∘ f truncated to a set carrying μ, which reads f as -∞ off that set.
• TauCeti.integral_sub_integral_indicator_exp_sub_one_eq_toReal_klDiv_iff: the truncated bound is an equality exactly when the truncated exp ∘ f is the density of μ with respect to ν.
• TauCeti.klDiv_eq_iSup_integral_sub_integral_exp_sub_one and TauCeti.klDiv_eq_iSup_integral_sub_log_integral_exp: the variational formulas over bounded measurable functions, on an arbitrary measurable space.
• TauCeti.klDiv_eq_iSup_boundedContinuousFunction_integral_sub_integral_exp_sub_one and TauCeti.klDiv_eq_iSup_boundedContinuousFunction_integral_sub_log_integral_exp: the same formulas over bounded continuous functions, on a normal Borel space with weakly regular sum.
• TauCeti.lowerSemicontinuous_klDiv_finiteMeasure and TauCeti.lowerSemicontinuous_klDiv_probabilityMeasure: joint weak lower semicontinuity.
• TauCeti.ofReal_mul_measureReal_sub_le_klDiv: the entropy inequality t μ(s) - (exp t - 1) ν(s) ≤ klDiv μ ν for arbitrary sets.
• TauCeti.isTightMeasureSet_setOf_klDiv_le: sublevel sets of klDiv · ν are tight when ν is.

References

• M. D. Donsker and S. R. S. Varadhan, Asymptotic evaluation of certain Markov process expectations for large time. IV, Comm. Pure Appl. Math. 36 (1983), 183–212.
• Y. Polyanskiy and Y. Wu, Information Theory: From Coding to Learning, Cambridge University Press, 2025, Chapter 4 (variational characterizations and lower semicontinuity of divergence).

theorem TauCeti.mul_sub_exp_sub_one_le_klFun {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x * y - (Real.exp y - 1) ≤ InformationTheory.klFun x

The Fenchel–Young inequality for klFun: the convex conjugate of klFun x = x log x + 1 - x on [0, ∞) is y ↦ exp y - 1.

theorem TauCeti.mul_sub_exp_sub_one_eq_klFun_iff {x : ℝ} (hx : 0 ≤ x) (y : ℝ) : x * y - (Real.exp y - 1) = InformationTheory.klFun x ↔ x = Real.exp y

The equality case of the Fenchel–Young inequality for klFun: x * y - (exp y - 1) = klFun x exactly when x = exp y.

theorem TauCeti.integral_sub_integral_indicator_exp_sub_one_eq {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.SigmaFinite μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hμν : μ.AbsolutelyContinuous ν) (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (s.indicator fun (x : α) => Real.exp (f x)) ν) : ∫ (x : α), f x ∂μ - ∫ (x : α), s.indicator (fun (x : α) => Real.exp (f x)) x - 1 ∂ν = ∫ (x : α), (μ.rnDeriv ν x).toReal * f x - (s.indicator (fun (x : α) => Real.exp (f x)) x - 1) ∂ν

For μ ≪ ν, the variational objective with the truncated exponential s.indicator (exp ∘ f) is a single ν-integral against the density.

theorem TauCeti.ae_mul_sub_indicator_exp_sub_one_le_klFun {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} {s : Set α} (hs : ∀ᵐ (x : α) ∂μ, x ∈ s) : ∀ᵐ (x : α) ∂ν, (μ.rnDeriv ν x).toReal * f x - (s.indicator (fun (x : α) => Real.exp (f x)) x - 1) ≤ InformationTheory.klFun (μ.rnDeriv ν x).toReal

Off s the density vanishes, so the integrand of the truncated variational objective is 1 = klFun 0 there; on s it is bounded by the Fenchel–Young inequality.

theorem TauCeti.ofReal_integral_sub_integral_indicator_exp_sub_one_le_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : ∀ᵐ (x : α) ∂μ, x ∈ s) (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (s.indicator fun (x : α) => Real.exp (f x)) ν) : ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), s.indicator (fun (x : α) => Real.exp (f x)) x - 1 ∂ν) ≤ InformationTheory.klDiv μ ν

Variational lower bound with a truncated exponential. If μ is concentrated on s, then ∫ f dμ - ∫ (s.indicator (exp ∘ f) - 1) dν ≤ klDiv μ ν. The truncation reads f as -∞ off s, where exp (-∞) = 0.

theorem TauCeti.ofReal_integral_sub_integral_exp_sub_one_le_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) : ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), Real.exp (f x) - 1 ∂ν) ≤ InformationTheory.klDiv μ ν

Variational lower bound for relative entropy between finite measures, with the mass correction built in: ∫ f dμ - ∫ (exp f - 1) dν ≤ klDiv μ ν.

theorem TauCeti.integral_sub_integral_indicator_exp_sub_one_eq_toReal_klDiv_iff {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (hs : ∀ᵐ (x : α) ∂μ, x ∈ s) (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (s.indicator fun (x : α) => Real.exp (f x)) ν) (h : InformationTheory.klDiv μ ν ≠ ⊤) : ∫ (x : α), f x ∂μ - ∫ (x : α), s.indicator (fun (x : α) => Real.exp (f x)) x - 1 ∂ν = (InformationTheory.klDiv μ ν).toReal ↔ μ = ν.withDensity fun (x : α) => ENNReal.ofReal (s.indicator (fun (x : α) => Real.exp (f x)) x)

The equality case of the variational lower bound. For finite measures with klDiv μ ν < ∞ and μ concentrated on s, the bound ∫ f dμ - ∫ (s.indicator (exp ∘ f) - 1) dν ≤ klDiv μ ν is an equality exactly when s.indicator (exp ∘ f) is the density of μ with respect to ν. Taking s = Set.univ gives the equality case of ofReal_integral_sub_integral_exp_sub_one_le_klDiv.

theorem TauCeti.ofReal_integral_sub_log_integral_exp_le_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf : MeasureTheory.Integrable f μ) (hef : MeasureTheory.Integrable (fun (x : α) => Real.exp (f x)) ν) : ENNReal.ofReal (∫ (x : α), f x ∂μ - Real.log (∫ (x : α), Real.exp (f x) ∂ν)) ≤ InformationTheory.klDiv μ ν

The Donsker–Varadhan lower bound (Gibbs variational inequality) for probability measures: ∫ f dμ - log ∫ exp f dν ≤ klDiv μ ν.

theorem TauCeti.ofReal_mul_measureReal_sub_le_klDiv {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {s : Set α} (t : ℝ) : ENNReal.ofReal (t * μ.real s - (Real.exp t - 1) * ν.real s) ≤ InformationTheory.klDiv μ ν

The entropy inequality for a set s: for finite measures and every real t, t μ(s) - (exp t - 1) ν(s) ≤ klDiv μ ν. A set of small ν-measure therefore has small μ-measure, uniformly over a sublevel set of klDiv · ν.

theorem TauCeti.klDiv_eq_iSup_integral_sub_integral_exp_sub_one {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : InformationTheory.klDiv μ ν = ⨆ (f : α → ℝ), ⨆ (_ : Measurable f), ⨆ (_ : ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C), ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), Real.exp (f x) - 1 ∂ν)

The variational formula for the relative entropy of finite measures, with the mass correction built in: klDiv μ ν is the supremum of ∫ f dμ - ∫ (exp f - 1) dν over bounded measurable functions f.

theorem TauCeti.klDiv_eq_iSup_integral_sub_log_integral_exp {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : InformationTheory.klDiv μ ν = ⨆ (f : α → ℝ), ⨆ (_ : Measurable f), ⨆ (_ : ∃ (C : ℝ), ∀ (x : α), |f x| ≤ C), ENNReal.ofReal (∫ (x : α), f x ∂μ - Real.log (∫ (x : α), Real.exp (f x) ∂ν))

The Donsker–Varadhan variational formula: for probability measures, klDiv μ ν is the supremum of ∫ f dμ - log ∫ exp f dν over bounded measurable functions f.

theorem TauCeti.klDiv_eq_iSup_boundedContinuousFunction_integral_sub_integral_exp_sub_one {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [TopologicalSpace α] [NormalSpace α] [BorelSpace α] [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [(μ + ν).WeaklyRegular] : InformationTheory.klDiv μ ν = ⨆ (f : BoundedContinuousFunction α ℝ), ENNReal.ofReal (∫ (x : α), f x ∂μ - ∫ (x : α), Real.exp (f x) - 1 ∂ν)

The variational formula for the relative entropy of finite measures on a normal Borel space, when μ + ν is weakly regular: klDiv μ ν is the supremum of ∫ f dμ - ∫ (exp f - 1) dν over bounded continuous functions f.

theorem TauCeti.klDiv_eq_iSup_boundedContinuousFunction_integral_sub_log_integral_exp {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} [TopologicalSpace α] [NormalSpace α] [BorelSpace α] [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] [(μ + ν).WeaklyRegular] : InformationTheory.klDiv μ ν = ⨆ (f : BoundedContinuousFunction α ℝ), ENNReal.ofReal (∫ (x : α), f x ∂μ - Real.log (∫ (x : α), Real.exp (f x) ∂ν))

The Donsker–Varadhan variational formula on a normal Borel space: for probability measures with weakly regular sum, klDiv μ ν is the supremum of ∫ f dμ - log ∫ exp f dν over bounded continuous functions f.

theorem TauCeti.lowerSemicontinuous_klDiv_finiteMeasure {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [BorelSpace α] : LowerSemicontinuous fun (p : MeasureTheory.FiniteMeasure α × MeasureTheory.FiniteMeasure α) => InformationTheory.klDiv ↑p.1 ↑p.2

Lower semicontinuity of relative entropy: (μ, ν) ↦ klDiv μ ν is jointly lower semicontinuous for the weak topology on pairs of finite measures.

theorem TauCeti.lowerSemicontinuous_klDiv_probabilityMeasure {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [BorelSpace α] : LowerSemicontinuous fun (p : MeasureTheory.ProbabilityMeasure α × MeasureTheory.ProbabilityMeasure α) => InformationTheory.klDiv ↑p.1 ↑p.2

Lower semicontinuity of relative entropy: (μ, ν) ↦ klDiv μ ν is jointly lower semicontinuous for the weak topology on pairs of probability measures.

theorem TauCeti.isTightMeasureSet_setOf_klDiv_le {α : Type u_1} [MeasurableSpace α] {ν : MeasureTheory.Measure α} [TopologicalSpace α] [MeasureTheory.IsFiniteMeasure ν] (hν : MeasureTheory.IsTightMeasureSet {ν}) {C : ENNReal} (hC : C ≠ ⊤) : MeasureTheory.IsTightMeasureSet {μ : MeasureTheory.Measure α | MeasureTheory.IsFiniteMeasure μ ∧ InformationTheory.klDiv μ ν ≤ C}

Sublevel sets of relative entropy are tight. If a finite measure ν is tight, then so is the set of finite measures μ with klDiv μ ν ≤ C, for every finite C.