The Rényi entropy functional

The Rényi entropy of a measure μ relative to a reference measure m, with dimension parameter N, is

S_N(μ | m) = -∫ ρ^{-1/N} dμᵃᶜ = -∫ ρ^{1-1/N} dm,

where μ = ρ m + μˢ is the Lebesgue decomposition of μ with respect to m and the first integral is over the absolutely continuous part μᵃᶜ = ρ m (TauCeti.renyiEntropy). It is the entropy functional of the finite-dimensional curvature-dimension conditions CD(K, N) and CD*(K, N) and of the measure-contraction property MCP(K, N) of Sturm and Lott–Villani: those conditions compare S_N along a Wasserstein geodesic with distortion coefficients (CD(K, N) with TauCeti.distortionTau, CD*(K, N) with TauCeti.distortionSigma), as CD(K, ∞) does with the Boltzmann entropy.

It is the internal energy (TauCeti.internalEnergy) for U(r) = -r · r^{-1/N}, which is -r^{1-1/N} for r > 0 and 0 at r = 0. For N > 0 the recession constant of U is 0, so the singular part of μ does not contribute, and since U ≤ 0 the entropy takes values in [-∞, 0]: S_N(μ | m) = -∫⁻ ρ · ρ^{-1/N} dm (TauCeti.renyiEntropy_eq_neg_lintegral), which is -∫⁻ ρ^{1-1/N} dm when N > 1 and μ is σ-finite (TauCeti.renyiEntropy_eq_neg_lintegral_rpow). For N = 1 the integrand is the indicator of {ρ > 0}, so S_1(μ | m) = -m {ρ > 0}, as in Sturm's convention S_N(μ | m) = -∫ ρ^{-1/N} dμᵃᶜ. A measure singular with respect to m, such as a Dirac mass against Lebesgue measure, has Rényi entropy 0.

For N ≥ 1, Hölder's inequality bounds the entropy below by the measure of a set carrying μ: if μ(Aᶜ) = 0, then

S_N(μ | m) ≥ -m(A)^{1/N} μ(X)^{1-1/N}

(TauCeti.neg_rpow_mul_rpow_le_renyiEntropy), so the entropy of a finite measure carried by a set of finite m-measure is finite (TauCeti.renyiEntropy_ne_bot_of_measure_compl_eq_zero). The bound is sharp: the uniform law m(A)⁻¹ m|_A on a set of finite positive measure has S_N = -m(A)^{1/N} (TauCeti.renyiEntropy_smul_restrict).

As N → ∞ the Rényi entropies recover the Boltzmann entropy Ent_m(μ) (TauCeti.boltzmannEntropy) of CD(K, ∞): for μ finite and carried by a set of finite m-measure,

N (S_N(μ | m) + μ(X)) → Ent_m(μ)

(TauCeti.tendsto_mul_renyiEntropy_add_measureReal_univ_nhds_boltzmannEntropy). The left side is ∫ U_N(ρ) dm plus N μˢ(X), where U_N(r) = N (r - r^{1-1/N}) increases with N to r log r; a nonzero singular part makes Ent_m(μ) = ⊤, and the left side tends to ⊤ through the term N μˢ(X).

The right-hand side of CD(K, N) and CD*(K, N) is the distorted Rényi entropy

T_β^{(t)}(q | m) = -∫ [β^{(1-t)}(d(x₀, x₁)) ρ₀(x₀)^{-1/N} + β^{(t)}(d(x₀, x₁)) ρ₁(x₁)^{-1/N}] dq

of a plan q on X × X whose marginals have densities ρ₀, ρ₁ with respect to m, for a family β^{(s)}(θ) of distortion coefficients (TauCeti.distortedRenyiEntropy). At time 0, below the critical distance, it is the Rényi entropy of the first marginal (TauCeti.distortedRenyiEntropy_zero).

Main definitions

• TauCeti.renyiEntropy N m μ: the Rényi entropy S_N(μ | m), as an extended real.
• TauCeti.distortedRenyiEntropy β N m q t: the distorted Rényi entropy T_β^{(t)}(q | m).

Main results

• TauCeti.renyiEntropy_eq_neg_lintegral, TauCeti.renyiEntropy_eq_neg_lintegral_rpow, TauCeti.renyiEntropy_eq_neg_lintegral_rpow_neg: the integral formulas for S_N.
• TauCeti.renyiEntropy_nonpos, TauCeti.renyiEntropy_ne_top, TauCeti.renyiEntropy_eq_bot_iff: the entropy lies in [-∞, 0], and is -∞ exactly when ∫ ρ · ρ^{-1/N} dm diverges.
• TauCeti.renyiEntropy_of_mutuallySingular: singular measures have Rényi entropy 0.
• TauCeti.neg_rpow_mul_rpow_le_renyiEntropy: the Hölder lower bound, and TauCeti.renyiEntropy_ne_bot_of_measure_compl_eq_zero, TauCeti.renyiEntropy_ne_bot: the entropy of a finite measure carried by a set of finite m-measure, or against a finite reference, is finite.
• TauCeti.renyiEntropy_smul_restrict: the entropy of a uniform law.
• TauCeti.tendsto_mul_renyiEntropy_add_measureReal_univ_nhds_boltzmannEntropy: the Boltzmann entropy as the limit of the Rényi entropies.
• TauCeti.distortedRenyiEntropy_anti, TauCeti.distortedRenyiEntropy_zero: the distorted Rényi entropy decreases in the coefficients, and at time 0 it is the Rényi entropy of the first marginal.

References

• K.-T. Sturm, On the geometry of metric measure spaces. II, Acta Math. 196 (2006), 133–177.
• J. Lott and C. Villani, Ricci curvature for metric-measure spaces via optimal transport, Ann. of Math. 169 (2009), 903–991.
• C. Villani, Optimal Transport: Old and New, Springer 2009, Chapters 16–17 and 29.

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

The Rényi entropy S_N(μ | m) = -∫ ρ^{1-1/N} dm of a measure μ relative to a reference measure m, where ρ is the density of the absolutely continuous part of μ: the internal energy for U(r) = -r · r^{-1/N}.

For N > 0 the singular part of μ does not contribute and the value lies in [-∞, 0] (TauCeti.renyiEntropy_eq_neg_lintegral). For N = 1 the integrand is the indicator of {ρ > 0}, following Sturm's convention S_N(μ | m) = -∫ ρ^{-1/N} dμᵃᶜ. The curvature-dimension theory uses N ≥ 1; other values of N carry no meaning.

theorem TauCeti.renyiEntropy_def {X : Type u_1} [MeasurableSpace X] (N : ℝ) (m μ : MeasureTheory.Measure X) : renyiEntropy N m μ = internalEnergy (fun (r : ℝ) => -(r * r ^ (-N⁻¹))) m μ

The Rényi entropy is the internal energy for U(r) = -r · r^{-1/N}.

theorem TauCeti.renyiEntropy_eq_neg_lintegral {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} (hN : 0 < N) : renyiEntropy N m μ = -↑(∫⁻ (x : X), μ.rnDeriv m x * μ.rnDeriv m x ^ (-N⁻¹) ∂m)

For N > 0, the Rényi entropy is S_N(μ | m) = -∫⁻ ρ · ρ^{-1/N} dm, where ρ is the Radon–Nikodym derivative of μ with respect to m; the singular part of μ does not contribute.

theorem TauCeti.renyiEntropy_eq_neg_lintegral_rpow {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite μ] (hN : 1 < N) : renyiEntropy N m μ = -↑(∫⁻ (x : X), μ.rnDeriv m x ^ (1 - N⁻¹) ∂m)

For N > 1 and σ-finite μ, the Rényi entropy is S_N(μ | m) = -∫⁻ ρ^{1-1/N} dm.

theorem TauCeti.renyiEntropy_eq_neg_lintegral_rpow_neg {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} [μ.HaveLebesgueDecomposition m] (hN : 0 < N) (hμ : μ.AbsolutelyContinuous m) : renyiEntropy N m μ = -↑(∫⁻ (x : X), μ.rnDeriv m x ^ (-N⁻¹) ∂μ)

Sturm's form of the Rényi entropy. For N > 0 and μ ≪ m, the Rényi entropy is S_N(μ | m) = -∫⁻ ρ^{-1/N} dμ, where ρ is the Radon–Nikodym derivative of μ with respect to m.

theorem TauCeti.renyiEntropy_nonpos {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} (hN : 0 < N) : renyiEntropy N m μ ≤ 0

For N > 0, the Rényi entropy is nonpositive.

theorem TauCeti.renyiEntropy_ne_top {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} (hN : 0 < N) : renyiEntropy N m μ ≠ ⊤

For N > 0, the Rényi entropy is never ⊤.

theorem TauCeti.renyiEntropy_eq_bot_iff {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} (hN : 0 < N) : renyiEntropy N m μ = ⊥ ↔ ∫⁻ (x : X), μ.rnDeriv m x * μ.rnDeriv m x ^ (-N⁻¹) ∂m = ⊤

For N > 0, the Rényi entropy is ⊥ exactly when ∫⁻ ρ · ρ^{-1/N} dm diverges.

@[simp]

theorem TauCeti.renyiEntropy_zero_measure {X : Type u_1} [MeasurableSpace X] (N : ℝ) (m : MeasureTheory.Measure X) : renyiEntropy N m 0 = 0

The Rényi entropy of the zero measure is 0.

theorem TauCeti.renyiEntropy_withDensity {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite m] (hN : 0 < N) {f : X → ENNReal} (hf : AEMeasurable f m) : renyiEntropy N m (m.withDensity f) = -↑(∫⁻ (x : X), f x * f x ^ (-N⁻¹) ∂m)

The Rényi entropy of an absolutely continuous measure does not depend on the choice of density: for N > 0 and every almost everywhere measurable density f, S_N(f m | m) = -∫⁻ f · f^{-1/N} dm.

theorem TauCeti.renyiEntropy_of_mutuallySingular {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} [μ.HaveLebesgueDecomposition m] (hN : 0 < N) (h : μ.MutuallySingular m) : renyiEntropy N m μ = 0

For N > 0, a measure singular with respect to m has Rényi entropy 0.

theorem TauCeti.neg_rpow_mul_rpow_le_renyiEntropy {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} (hN : 1 ≤ N) {A : Set X} (hA : μ Aᶜ = 0) : -↑(m A ^ N⁻¹ * μ Set.univ ^ (1 - N⁻¹)) ≤ renyiEntropy N m μ

For N ≥ 1, Hölder's inequality bounds the Rényi entropy below by the measure of any set carrying μ: if μ(Aᶜ) = 0, then S_N(μ | m) ≥ -m(A)^{1/N} μ(X)^{1-1/N}. The uniform laws attain the bound (TauCeti.renyiEntropy_smul_restrict).

theorem TauCeti.renyiEntropy_ne_bot_of_measure_compl_eq_zero {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] (hN : 1 ≤ N) {A : Set X} (hA : μ Aᶜ = 0) (hmA : m A ≠ ⊤) : renyiEntropy N m μ ≠ ⊥

For N ≥ 1, the Rényi entropy of a finite measure carried by a set of finite m-measure is never ⊥.

theorem TauCeti.renyiEntropy_ne_bot {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure m] [MeasureTheory.IsFiniteMeasure μ] (hN : 1 ≤ N) : renyiEntropy N m μ ≠ ⊥

For N ≥ 1, the Rényi entropy of a finite measure relative to a finite reference measure is never ⊥.

theorem TauCeti.renyiEntropy_smul_restrict {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite m] (hN : 0 < N) {A : Set X} (hA : MeasurableSet A) (h₀ : m A ≠ 0) (h₁ : m A ≠ ⊤) : renyiEntropy N m ((m A)⁻¹ • m.restrict A) = -↑(m A ^ N⁻¹)

The uniform law m(A)⁻¹ m|_A on a measurable set of finite positive measure has Rényi entropy -m(A)^{1/N}, so the bound TauCeti.neg_rpow_mul_rpow_le_renyiEntropy is attained.

theorem TauCeti.renyiEntropy_cond_ne_bot {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [MeasureTheory.SigmaFinite m] (hN : 0 < N) {A : Set X} (hA : MeasurableSet A) : renyiEntropy N m m[|A] ≠ ⊥

The uniform law m[|A] on a measurable set has finite Rényi entropy: it is -m(A)^{1/N} when 0 < m(A) < ∞, and m[|A] = 0 otherwise.

The Boltzmann entropy as the limit N → ∞

theorem TauCeti.tendsto_mul_renyiEntropy_add_measureReal_univ_nhds_boltzmannEntropy {X : Type u_1} [MeasurableSpace X] {m μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.HaveLebesgueDecomposition m] {A : Set X} (hA : μ Aᶜ = 0) (hmA : m A ≠ ⊤) : Filter.Tendsto (fun (N : ℝ) => ↑N * (renyiEntropy N m μ + ↑(μ.real Set.univ))) Filter.atTop (nhds (boltzmannEntropy m μ))

As N → ∞, N (S_N(μ | m) + μ(X)) tends to the Boltzmann entropy Ent_m(μ), for a finite measure μ carried by a set A of finite m-measure.

This is the integrated form of the pointwise limit N (r - r^{1-1/N}) → r log r, which is monotone in N. The limit may be ⊤; in particular it is ⊤ when μ is not absolutely continuous with respect to m, since its singular mass contributes N μˢ(X).

The distorted Rényi entropy

noncomputable def TauCeti.distortedRenyiEntropy {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (β : ℝ → ℝ → ENNReal) (N : ℝ) (m : MeasureTheory.Measure X) (q : MeasureTheory.Measure (X × X)) (t : ℝ) : EReal

The distorted Rényi entropy T_β^{(t)}(q | m) of a plan q on X × X relative to a reference measure m, for a family β s θ = β^{(s)}(θ) of distortion coefficients indexed by a time s and a distance θ:

T_β^{(t)}(q | m) = -∫ [β^{(1-t)}(d(x₀, x₁)) ρ₀(x₀)^{-1/N} + β^{(t)}(d(x₀, x₁)) ρ₁(x₁)^{-1/N}] dq,

where ρ₀ and ρ₁ are the densities with respect to m of the two marginals of q. With β = τ_{K,N} it is the right-hand side of the condition CD(K, N), with β = σ_{K,N} that of CD*(K, N). The integral is in [0, ∞], so the value lies in [-∞, 0].

theorem TauCeti.distortedRenyiEntropy_def {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [PseudoMetricSpace X] {β : ℝ → ℝ → ENNReal} {t : ℝ} {q : MeasureTheory.Measure (X × X)} : distortedRenyiEntropy β N m q t = -↑(∫⁻ (z : X × X), β (1 - t) (dist z.1 z.2) * q.fst.rnDeriv m z.1 ^ (-N⁻¹) + β t (dist z.1 z.2) * q.snd.rnDeriv m z.2 ^ (-N⁻¹) ∂q)

The distorted Rényi entropy, unfolded.

theorem TauCeti.distortedRenyiEntropy_anti {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [PseudoMetricSpace X] {β β' : ℝ → ℝ → ENNReal} {t : ℝ} {q : MeasureTheory.Measure (X × X)} (h : ∀ (θ : ℝ), β (1 - t) θ ≤ β' (1 - t) θ) (h' : ∀ (θ : ℝ), β t θ ≤ β' t θ) : distortedRenyiEntropy β' N m q t ≤ distortedRenyiEntropy β N m q t

Larger distortion coefficients give a smaller distorted Rényi entropy.

theorem TauCeti.distortedRenyiEntropy_zero {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [PseudoMetricSpace X] {β : ℝ → ℝ → ENNReal} {q : MeasureTheory.Measure (X × X)} [q.fst.HaveLebesgueDecomposition m] (hN : 0 < N) (hq : q.fst.AbsolutelyContinuous m) (h₁ : ∀ᵐ (z : X × X) ∂q, β 1 (dist z.1 z.2) = 1) (h₀ : ∀ᵐ (z : X × X) ∂q, β 0 (dist z.1 z.2) = 0) : distortedRenyiEntropy β N m q 0 = renyiEntropy N m q.fst

The distorted Rényi entropy at time 0. If q-almost every pair is below the critical distance, in the sense that β^{(1)} = 1 and β^{(0)} = 0 there, and the first marginal of q is absolutely continuous with respect to m, then T_β^{(0)}(q | m) = S_N(q.fst | m) is the Rényi entropy of that marginal. So the curvature-dimension inequalities hold with equality at time 0.

theorem TauCeti.distortedRenyiEntropy_eq_bot_of_ae {X : Type u_1} [MeasurableSpace X] {N : ℝ} {m : MeasureTheory.Measure X} [PseudoMetricSpace X] {β : ℝ → ℝ → ENNReal} {t : ℝ} {q : MeasureTheory.Measure (X × X)} (hq : q ≠ 0) (h : ∀ᵐ (z : X × X) ∂q, β (1 - t) (dist z.1 z.2) * q.fst.rnDeriv m z.1 ^ (-N⁻¹) + β t (dist z.1 z.2) * q.snd.rnDeriv m z.2 ^ (-N⁻¹) = ⊤) : distortedRenyiEntropy β N m q t = ⊥

If the integrand of T_β^{(t)}(q | m) is infinite q-almost everywhere and q ≠ 0, the distorted Rényi entropy is -∞.