Relative entropy against an exponentially tilted reference

Let ν be a probability measure and f ≥ 0 a measurable potential. The tilted measure ν.tilted (-f) is the Gibbs probability measure Z⁻¹ e^{-f} ν, where Z = ∫ e^{-f} dν lies in (0, 1]. Changing the reference measure of a relative entropy from ν to this Gibbs measure trades the potential energy ∫ f dμ against the free energy -log Z: klDiv μ (ν.tilted (-f)) - log Z = ∫ f dμ + klDiv μ ν for every probability measure μ.

Mathlib's MeasureTheory.integral_llr_tilted_right gives the real-valued form of this identity, under the hypotheses that f is μ-integrable and both log-likelihood ratios are integrable. The statement here is the one in ℝ≥0∞, with no integrability hypothesis: each side is infinite exactly when the other is. Its two genuinely new cases are a measure μ that is not absolutely continuous with respect to ν, and a potential that is not μ-integrable, where the relative entropy against the Gibbs measure has to be shown infinite. The latter rests on TauCeti.integrable_llr_of_ae_le: the negative part of a log-likelihood ratio between finite measures is always integrable, so an integrable upper bound makes the ratio integrable.

This is the change-of-reference step behind entropic optimal transport, where f is the cost divided by the temperature and ν is the product of the two marginals.

Main statements

• TauCeti.integrable_llr_of_ae_le: for finite measures μ ≪ ν, the log-likelihood ratio llr μ ν is μ-integrable as soon as it is bounded above by a μ-integrable function.
• TauCeti.klDiv_tilted_neg_add_ofReal_neg_log: the change-of-reference identity klDiv μ (ν.tilted (-f)) + ENNReal.ofReal (-log Z) = ∫⁻ x, ENNReal.ofReal (f x) ∂μ + klDiv μ ν.

References

• M. Nutz, Introduction to Entropic Optimal Transport, lecture notes, Columbia University, 2021, for the Gibbs reformulation of entropically regularised transport.

theorem TauCeti.integrable_llr_of_ae_le {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {g : α → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (hμν : μ.AbsolutelyContinuous ν) (hg : MeasureTheory.Integrable g μ) (h : ∀ᵐ (x : α) ∂μ, MeasureTheory.llr μ ν x ≤ g x) : MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ

For finite measures μ ≪ ν, an integrable upper bound on the log-likelihood ratio llr μ ν makes it integrable. Its negative part needs no hypothesis: log t ≥ 1 - t⁻¹ bounds it below by 1 - dν/dμ, which is μ-integrable since ν is finite.

theorem TauCeti.klDiv_tilted_neg_add_ofReal_neg_log {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] (hf : AEMeasurable f ν) (hf0 : 0 ≤ᵐ[ν] f) : InformationTheory.klDiv μ (ν.tilted fun (x : α) => -f x) + ENNReal.ofReal (-Real.log (∫ (x : α), Real.exp (-f x) ∂ν)) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ + InformationTheory.klDiv μ ν

Change of reference to a Gibbs measure. For probability measures μ and ν and a nonnegative potential f, the relative entropy of μ against the Gibbs measure ν.tilted (-f) = Z⁻¹ e^{-f} ν, with Z = ∫ e^{-f} dν, satisfies klDiv μ (ν.tilted (-f)) - log Z = ∫ f dμ + klDiv μ ν. Since 0 < Z ≤ 1, every term is nonnegative, and the identity holds in ℝ≥0∞ with no integrability hypothesis.