Internal energy and the signed Boltzmann entropy

The internal energy of a measure μ relative to a reference measure m, for a density function U : ℝ → ℝ, is

∫ U(ρ) dm + U'(∞) μˢ(X),

where μ = ρ m + μˢ is the Lebesgue decomposition of μ with respect to m and U'(∞) is the recession constant of U (TauCeti.recessionConstant). It is the third basic energy on the Wasserstein space, with the potential and interaction energies; its Wasserstein gradient flows are the nonlinear diffusion equations.

Neither integrand need be integrable and U'(∞) may be infinite, so the energy takes values in EReal, with the convention of TauCeti.potentialEnergy: the positive contributions ∫ U(ρ)⁺ dm + (U'(∞))⁺ μˢ(X) and the negative ones ∫ U(ρ)⁻ dm + (U'(∞))⁻ μˢ(X) are summed separately in ℝ≥0∞, and the energy is ⊤ when the positive sum is infinite and their difference otherwise (TauCeti.internalEnergy). For an absolutely continuous measure it is the potential energy of U(ρ) against m (TauCeti.internalEnergy_of_absolutelyContinuous), and it does not depend on the chosen density (TauCeti.internalEnergy_withDensity).

The formula needs a Lebesgue decomposition of μ whose density ρ is finite m-almost everywhere. Both hold when μ and m are σ-finite (Measure.rnDeriv_ne_top), in particular for finite measures against a finite reference or against Lebesgue measure, and this is the intended domain. For other measures Mathlib's Measure.rnDeriv and Measure.singularPart are junk values, and so is the internal energy.

The Boltzmann entropy Ent_m(μ) is the internal energy for U(r) = r log r (TauCeti.boltzmannEntropy). Its recession constant is ⊤, so the entropy is ⊤ as soon as μ is not absolutely continuous with respect to m, and otherwise it is ∫ ρ log ρ dm with the conventions above. The reference measure may be infinite, as Lebesgue measure is, and then the entropy may be ⊥. Against a finite reference measure it is never ⊥, and for finite measures it is Mathlib's Kullback–Leibler divergence up to the mass correction: klDiv μ m = Ent_m(μ) + m(X) - μ(X) (TauCeti.klDiv_eq_boltzmannEntropy_add_sub).

Changing the reference measure to a Gibbs measure m.tilted f = Z⁻¹ exp(f) m, with Z = ∫ exp f dm finite, shifts the entropy by a potential energy and a free energy: Ent_{m.tilted f}(μ) = Ent_m(μ) - ∫ f dμ + μ(X) log Z (TauCeti.boltzmannEntropy_tilted). This is how the entropy against an infinite reference is controlled: for f x = -a d(x, x₀)² with exp f integrable against a nonzero m, the tilted reference is a probability measure, and the entropy of a law with finite second moment is a relative entropy minus a moment and a constant, in particular never ⊥.

Main definitions

• TauCeti.internalEnergy U m μ: the internal energy of μ relative to m, as an extended real.
• TauCeti.boltzmannEntropy m μ: the signed Boltzmann entropy Ent_m(μ).

Main results

• TauCeti.internalEnergy_of_absolutelyContinuous, TauCeti.internalEnergy_withDensity: the internal energy of an absolutely continuous measure is the potential energy of U(ρ), for any density ρ.
• TauCeti.internalEnergy_eq_potentialEnergy_add: for a real recession constant and finite singular mass, the internal energy is ∫ U(ρ) dm + U'(∞) μˢ(X).
• TauCeti.boltzmannEntropy_eq_top_iff, TauCeti.boltzmannEntropy_eq_bot_iff, TauCeti.integrable_mul_log_iff_boltzmannEntropy_ne_top_and_ne_bot: when the entropy is ⊤, ⊥, or finite.
• TauCeti.klDiv_eq_boltzmannEntropy_add_sub: klDiv μ m = Ent_m(μ) + m(X) - μ(X) for finite measures.
• TauCeti.boltzmannEntropy_eq_potentialEnergy_llr: for μ ≪ m, the entropy is ∫ log ρ dμ.
• TauCeti.boltzmannEntropy_tilted, TauCeti.klDiv_tilted_eq_boltzmannEntropy: change of reference to a Gibbs measure.
• TauCeti.boltzmannEntropy_ne_bot_of_integrable_exp: the entropy is not ⊥ when some exp f is integrable against m and f is integrable against μ.

References

• L. Ambrosio, N. Gigli, G. Savaré, Gradient Flows in Metric Spaces and in the Space of Probability Measures, 2nd ed., Birkhäuser 2008, §9.3.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapter 17.

noncomputable def TauCeti.internalEnergy {X : Type u_1} [MeasurableSpace X] (U : ℝ → ℝ) (m μ : MeasureTheory.Measure X) : EReal

The internal energy ∫ U(ρ) dm + U'(∞) μˢ(X) of a measure μ relative to a reference measure m, where μ = ρ m + μˢ is the Lebesgue decomposition of μ with respect to m and U'(∞) is the recession constant of U, as an extended real. The positive parts ∫ U(ρ)⁺ dm + (U'(∞))⁺ μˢ(X) and the negative parts ∫ U(ρ)⁻ dm + (U'(∞))⁻ μˢ(X) are summed separately; the energy is ⊤ when the positive sum is infinite, and otherwise the positive sum minus the negative one, which is ⊥ when only the latter is infinite.

The intended domain is σ-finite μ and m, for which ρ is finite m-almost everywhere, so taking ρ through ENNReal.toReal changes it only on an m-null set.

theorem TauCeti.internalEnergy_def {X : Type u_1} [MeasurableSpace X] (U : ℝ → ℝ) (m μ : MeasureTheory.Measure X) : internalEnergy U m μ = if ∫⁻ (x : X), ENNReal.ofReal (U (μ.rnDeriv m x).toReal) ∂m + (recessionConstant U).toENNReal * (μ.singularPart m) Set.univ = ⊤ then ⊤ else ↑(∫⁻ (x : X), ENNReal.ofReal (U (μ.rnDeriv m x).toReal) ∂m + (recessionConstant U).toENNReal * (μ.singularPart m) Set.univ) - ↑(∫⁻ (x : X), ENNReal.ofReal (-U (μ.rnDeriv m x).toReal) ∂m + (-recessionConstant U).toENNReal * (μ.singularPart m) Set.univ)

The defining formula of the internal energy.

theorem TauCeti.internalEnergy_of_singularPart_eq_zero {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m μ : MeasureTheory.Measure X} (h : μ.singularPart m = 0) : internalEnergy U m μ = potentialEnergy (fun (x : X) => U (μ.rnDeriv m x).toReal) m

Without singular part, the internal energy is the potential energy of U(ρ) against m.

theorem TauCeti.internalEnergy_of_absolutelyContinuous {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m μ : MeasureTheory.Measure X} (h : μ.AbsolutelyContinuous m) : internalEnergy U m μ = potentialEnergy (fun (x : X) => U (μ.rnDeriv m x).toReal) m

The internal energy of a measure absolutely continuous with respect to m is the potential energy of U(ρ) against m, where ρ is the Radon–Nikodym derivative.

theorem TauCeti.internalEnergy_withDensity {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite m] {f : X → NNReal} (hf : AEMeasurable f m) : internalEnergy U m (m.withDensity fun (x : X) => ↑(f x)) = potentialEnergy (fun (x : X) => U ↑(f x)) m

The internal energy does not depend on the choice of density: for every almost everywhere measurable finite density f, the internal energy of f m is the potential energy of U ∘ f against m.

theorem TauCeti.internalEnergy_eq_top_of_recessionConstant_eq_top {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m μ : MeasureTheory.Measure X} (hU : recessionConstant U = ⊤) (h : μ.singularPart m ≠ 0) : internalEnergy U m μ = ⊤

If the recession constant of U is ⊤, every measure with a nonzero singular part has internal energy ⊤.

theorem TauCeti.internalEnergy_eq_potentialEnergy_add {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m μ : MeasureTheory.Measure X} {r : ℝ} (hU : recessionConstant U = ↑r) (h : (μ.singularPart m) Set.univ ≠ ⊤) : internalEnergy U m μ = potentialEnergy (fun (x : X) => U (μ.rnDeriv m x).toReal) m + ↑(r * ((μ.singularPart m) Set.univ).toReal)

For a real recession constant r and a finite singular part, the internal energy is ∫ U(ρ) dm + r μˢ(X), with the first term the potential energy of U(ρ) against m.

theorem TauCeti.internalEnergy_eq_potentialEnergy_of_lintegral_eq {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} {m μ : MeasureTheory.Measure X} {W : X → ℝ} (hpos : ∫⁻ (x : X), ENNReal.ofReal (U (μ.rnDeriv m x).toReal) ∂m + (recessionConstant U).toENNReal * (μ.singularPart m) Set.univ = ∫⁻ (x : X), ENNReal.ofReal (W x) ∂m) (hneg : ∫⁻ (x : X), ENNReal.ofReal (-U (μ.rnDeriv m x).toReal) ∂m + (-recessionConstant U).toENNReal * (μ.singularPart m) Set.univ = ∫⁻ (x : X), ENNReal.ofReal (-W x) ∂m) : internalEnergy U m μ = potentialEnergy W m

The internal energy is the potential energy of any potential W whose positive and negative parts have the integrals of the positive and negative parts occurring in the definition of the internal energy.

@[simp]

theorem TauCeti.internalEnergy_zero_measure {X : Type u_1} [MeasurableSpace X] {U : ℝ → ℝ} (hU : U 0 = 0) (m : MeasureTheory.Measure X) : internalEnergy U m 0 = 0

The internal energy of the zero measure is 0 when U 0 = 0.

noncomputable def TauCeti.boltzmannEntropy {X : Type u_1} [MeasurableSpace X] (m μ : MeasureTheory.Measure X) : EReal

The signed Boltzmann entropy Ent_m(μ) of a measure μ relative to a reference measure m: the internal energy for U(r) = r log r. It is ⊤ when μ is not absolutely continuous with respect to m (TauCeti.boltzmannEntropy_of_not_absolutelyContinuous), and otherwise ∫ ρ log ρ dm for the density ρ of μ, with the extended-real conventions of TauCeti.potentialEnergy (TauCeti.boltzmannEntropy_of_absolutelyContinuous).

theorem TauCeti.boltzmannEntropy_def {X : Type u_1} [MeasurableSpace X] (m μ : MeasureTheory.Measure X) : boltzmannEntropy m μ = internalEnergy (fun (r : ℝ) => r * Real.log r) m μ

The Boltzmann entropy is the internal energy for U(r) = r log r.

theorem TauCeti.boltzmannEntropy_of_absolutelyContinuous {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} (h : μ.AbsolutelyContinuous m) : boltzmannEntropy m μ = potentialEnergy (fun (x : X) => (μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal) m

The Boltzmann entropy of a measure absolutely continuous with respect to m is the potential energy of ρ log ρ against m, where ρ is the Radon–Nikodym derivative.

theorem TauCeti.boltzmannEntropy_of_not_absolutelyContinuous {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [μ.HaveLebesgueDecomposition m] (h : ¬μ.AbsolutelyContinuous m) : boltzmannEntropy m μ = ⊤

A measure that is not absolutely continuous with respect to m has Boltzmann entropy ⊤.

theorem TauCeti.boltzmannEntropy_withDensity {X : Type u_1} [MeasurableSpace X] {m : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite m] {f : X → NNReal} (hf : AEMeasurable f m) : boltzmannEntropy m (m.withDensity fun (x : X) => ↑(f x)) = potentialEnergy (fun (x : X) => ↑(f x) * Real.log ↑(f x)) m

The Boltzmann entropy does not depend on the choice of density: for every almost everywhere measurable finite density f, the entropy of f m is the potential energy of f log f against m.

theorem TauCeti.boltzmannEntropy_eq_top_iff {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [μ.HaveLebesgueDecomposition m] : boltzmannEntropy m μ = ⊤ ↔ μ.AbsolutelyContinuous m → ∫⁻ (x : X), ENNReal.ofReal ((μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal) ∂m = ⊤

The Boltzmann entropy is ⊤ exactly when μ is not absolutely continuous with respect to m, or the positive part of ρ log ρ has infinite integral.

theorem TauCeti.boltzmannEntropy_eq_bot_iff {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [μ.HaveLebesgueDecomposition m] : boltzmannEntropy m μ = ⊥ ↔ μ.AbsolutelyContinuous m ∧ ∫⁻ (x : X), ENNReal.ofReal ((μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal) ∂m ≠ ⊤ ∧ ∫⁻ (x : X), ENNReal.ofReal (-((μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal)) ∂m = ⊤

The Boltzmann entropy is ⊥ exactly when μ is absolutely continuous with respect to m, the positive part of ρ log ρ has finite integral, and its negative part has infinite integral.

theorem TauCeti.integrable_mul_log_iff_boltzmannEntropy_ne_top_and_ne_bot {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} (h : μ.AbsolutelyContinuous m) : MeasureTheory.Integrable (fun (x : X) => (μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal) m ↔ boltzmannEntropy m μ ≠ ⊤ ∧ boltzmannEntropy m μ ≠ ⊥

For μ absolutely continuous with respect to m, the Boltzmann entropy is finite exactly when ρ log ρ is integrable against m.

theorem TauCeti.boltzmannEntropy_of_integrable {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} (h : μ.AbsolutelyContinuous m) (hi : MeasureTheory.Integrable (fun (x : X) => (μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal) m) : boltzmannEntropy m μ = ↑(∫ (x : X), (μ.rnDeriv m x).toReal * Real.log (μ.rnDeriv m x).toReal ∂m)

If ρ log ρ is integrable against m, the Boltzmann entropy is its integral.

theorem TauCeti.boltzmannEntropy_ne_bot {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure m] : boltzmannEntropy m μ ≠ ⊥

Against a finite reference measure, the Boltzmann entropy is never ⊥.

@[simp]

theorem TauCeti.boltzmannEntropy_zero_measure {X : Type u_1} [MeasurableSpace X] (m : MeasureTheory.Measure X) : boltzmannEntropy m 0 = 0

The Boltzmann entropy of the zero measure is 0.

@[simp]

theorem TauCeti.boltzmannEntropy_self {X : Type u_1} [MeasurableSpace X] (m : MeasureTheory.Measure X) [MeasureTheory.SigmaFinite m] : boltzmannEntropy m m = 0

The Boltzmann entropy of a σ-finite measure relative to itself is 0.

theorem TauCeti.klDiv_eq_boltzmannEntropy_add_sub {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure m] : ↑(InformationTheory.klDiv μ m) = boltzmannEntropy m μ + ↑(m.real Set.univ) - ↑(μ.real Set.univ)

For finite measures, the Kullback–Leibler divergence is the Boltzmann entropy up to the mass correction: klDiv μ m = Ent_m(μ) + m(X) - μ(X).

theorem TauCeti.klDiv_eq_boltzmannEntropy_of_measure_univ_eq {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (h : μ Set.univ = m Set.univ) : ↑(InformationTheory.klDiv μ m) = boltzmannEntropy m μ

For finite measures of equal mass, in particular for probability measures, the Kullback–Leibler divergence is the Boltzmann entropy.

theorem TauCeti.boltzmannEntropy_eq_potentialEnergy_llr {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite m] (h : μ.AbsolutelyContinuous m) : boltzmannEntropy m μ = potentialEnergy (MeasureTheory.llr μ m) μ

For μ ≪ m, the Boltzmann entropy ∫ ρ log ρ dm is the potential energy ∫ log ρ dμ of the log-likelihood ratio log ρ = llr μ m against μ itself.

theorem TauCeti.boltzmannEntropy_tilted {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {f : X → ℝ} (hf : MeasureTheory.Integrable (fun (x : X) => Real.exp (f x)) m) (hfμ : MeasureTheory.Integrable f μ) : boltzmannEntropy (m.tilted f) μ = boltzmannEntropy m μ - ↑(∫ (x : X), f x ∂μ) + ↑(μ.real Set.univ * Real.log (∫ (x : X), Real.exp (f x) ∂m))

Change of reference for the Boltzmann entropy. If exp f is integrable against m, so that the tilted measure m.tilted f = Z⁻¹ exp(f) m with Z = ∫ exp f dm is a finite reference measure, then for every finite measure μ against which f is integrable, Ent_{m.tilted f}(μ) = Ent_m(μ) - ∫ f dμ + μ(X) log Z. The reference m may be infinite.

theorem TauCeti.klDiv_tilted_eq_boltzmannEntropy {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [NeZero m] [MeasureTheory.IsFiniteMeasure μ] {f : X → ℝ} (hf : MeasureTheory.Integrable (fun (x : X) => Real.exp (f x)) m) (hfμ : MeasureTheory.Integrable f μ) : ↑(InformationTheory.klDiv μ (m.tilted f)) = boltzmannEntropy m μ - ↑(∫ (x : X), f x ∂μ) + ↑(μ.real Set.univ * Real.log (∫ (x : X), Real.exp (f x) ∂m)) + 1 - ↑(μ.real Set.univ)

Change of reference to a Gibbs measure. If exp f is integrable against a nonzero σ-finite reference m, then the tilted measure m.tilted f = Z⁻¹ exp(f) m, with Z = ∫ exp f dm, is a probability measure, and for every finite measure μ against which f is integrable, klDiv μ (m.tilted f) = Ent_m(μ) - ∫ f dμ + μ(X) log Z + 1 - μ(X). For f x = -a d(x, x₀)² this is the confining Gaussian reference against which the entropy of laws with finite second moment is controlled.

theorem TauCeti.boltzmannEntropy_ne_bot_of_integrable_exp {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {f : X → ℝ} (hf : MeasureTheory.Integrable (fun (x : X) => Real.exp (f x)) m) (hfμ : MeasureTheory.Integrable f μ) : boltzmannEntropy m μ ≠ ⊥

If exp f is integrable against the reference m and f is integrable against a finite measure μ, then the Boltzmann entropy of μ is not ⊥, even when m is infinite: it is bounded below through the entropy against the finite reference m.tilted f.