InformationTheory.Shannon.DifferentialEntropy

Imports 8

Differential entropy and Gaussian max-entropy #

Differential entropy h(X) = -∫ f log f dx for real-valued random variables and the Gaussian maximum-entropy theorem (Cover–Thomas).

Main definitions #

differentialEntropy — -∫ negMulLog (dμ/dλ) dλ where λ is the Lebesgue measure.

Main statements #

differentialEntropy_eq_integral_withDensity — rewrite for μ = volume.withDensity f.
differentialEntropy_eq_integral_density — rewrite as -∫ f log f dλ for a real density.
integrable_density_log_density_of_gaussian — integrability of f log f for Gaussian f.
differentialEntropy_map_add_const — translation invariance: h(X + y) = h(X).
differentialEntropy_map_mul_const — scaling: h(cX) = h(X) + log |c|.
differentialEntropy_map_affine — affine corollary: h(aX + b) = h(X) + log |a|.
differentialEntropy_gaussianReal — h(𝒩(m, v)) = (1/2) log (2πe v).
differentialEntropy_le_gaussian_of_variance_le — Gaussian max-entropy theorem.
klDiv_gaussianReal_gaussianReal_eq — closed-form KL between two Gaussians.
concaveOn_log_one_add_div — concavity of x ↦ log(1 + x/N) on [0, ∞).

Differential entropy: definition and basic integrability #

noncomputable def

InformationTheory.Shannon.differentialEntropy

source

(μ : MeasureTheory.Measure ℝ) :

ℝ

Differential entropy. For a measure μ on ℝ, define differentialEntropy μ := ∫ x, Real.negMulLog ((μ.rnDeriv volume x).toReal) ∂volume, i.e. -∫ f log f dx where f := dμ/dvolume is the Radon-Nikodym derivative w.r.t. the Lebesgue measure. Real.negMulLog 0 = 0 covers the support boundary automatically. The value is meaningful primarily when μ ≪ volume; under singular μ, the rnDeriv captures only the absolutely continuous part.

Equations

InformationTheory.Shannon.differentialEntropy μ = ∫ (x : ℝ), (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog

Instances For

Used by

theorem

InformationTheory.Shannon.differentialEntropy_eq_integral_withDensity

source

{f : ℝ → ENNReal} (hf : Measurable f) :

differentialEntropy (MeasureTheory.volume.withDensity f) = ∫ (x : ℝ), (f x).toReal.negMulLog

For μ = volume.withDensity f with measurable f, differentialEntropy μ equals ∫ x, negMulLog (f x).toReal ∂volume.

Used by

theorem

InformationTheory.Shannon.differentialEntropy_eq_integral_density

source

{f : ℝ → ℝ} (hf : Measurable f) (hf_nn : ∀ (x : ℝ), 0 ≤ f x) (μ : MeasureTheory.Measure ℝ) (hμ : μ = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (f x)) :

differentialEntropy μ = -∫ (x : ℝ), f x * Real.log (f x)

For μ = volume.withDensity (fun x => ENNReal.ofReal (f x)) with 0 ≤ f, differentialEntropy μ = -∫ x, f x * Real.log (f x) ∂volume.

Used by

theorem

InformationTheory.Shannon.integrable_density_log_density_of_gaussian

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

MeasureTheory.Integrable (fun (x : ℝ) => ProbabilityTheory.gaussianPDFReal m v x * Real.log (ProbabilityTheory.gaussianPDFReal m v x)) MeasureTheory.volume

The integrand gaussianPDFReal m v x * Real.log (gaussianPDFReal m v x) is integrable on Lebesgue volume.

Used by

theorem

InformationTheory.Shannon.differentialEntropy_dirac

source

(m : ℝ) :

differentialEntropy (MeasureTheory.Measure.dirac m) = 0

The differential entropy of Measure.dirac m is 0.

Used by

Translation invariance and scaling #

theorem

InformationTheory.Shannon.differentialEntropy_map_add_const

source

{μ : MeasureTheory.Measure ℝ} (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) [MeasureTheory.SigmaFinite μ] (y : ℝ) :

differentialEntropy (MeasureTheory.Measure.map (fun (x : ℝ) => x + y) μ) = differentialEntropy μ

Differential entropy is translation invariant: h(X + y) = h(X).

Used by

theorem

InformationTheory.Shannon.differentialEntropy_map_mul_const

source

{μ : MeasureTheory.Measure ℝ} (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) [MeasureTheory.IsProbabilityMeasure μ] {c : ℝ} (hc : c ≠ 0) (h_ent_int : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

differentialEntropy (MeasureTheory.Measure.map (fun (x : ℝ) => x * c) μ) = differentialEntropy μ + Real.log |c|

Differential entropy under scaling: h(cX) = h(X) + log |c|.

Requires h_ent_int: integrability of negMulLog (μ.rnDeriv volume) (not automatic from μ ≪ volume; heavy-tail densities can have non-integrable negMulLog).

Used by

theorem

InformationTheory.Shannon.differentialEntropy_map_affine

source

{μ : MeasureTheory.Measure ℝ} (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) [MeasureTheory.IsProbabilityMeasure μ] {a : ℝ} (ha : a ≠ 0) (b : ℝ) (h_ent_int : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

differentialEntropy (MeasureTheory.Measure.map (fun (x : ℝ) => a * x + b) μ) = differentialEntropy μ + Real.log |a|

The affine corollary: h(aX + b) = h(X) + log |a|.

Used by

Differential entropy of the Gaussian: `h(𝒩(m, v)) = (1/2) log (2πe v)` #

theorem

InformationTheory.Shannon.differentialEntropy_gaussianReal_form

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

differentialEntropy (ProbabilityTheory.gaussianReal m v) = ∫ (x : ℝ), ProbabilityTheory.gaussianPDFReal m v x * -Real.log (ProbabilityTheory.gaussianPDFReal m v x)

Used by

theorem

InformationTheory.Shannon.log_gaussianPDFReal_eq

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) :

Real.log (ProbabilityTheory.gaussianPDFReal m v x) = -(1 / 2) * Real.log (2 * Real.pi * ↑v) - (x - m) ^ 2 / (2 * ↑v)

Used by

theorem

InformationTheory.Shannon.differentialEntropy_gaussianReal

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

differentialEntropy (ProbabilityTheory.gaussianReal m v) = 1 / 2 * Real.log (2 * Real.pi * Real.exp 1 * ↑v)

The differential entropy of a Gaussian: h(𝒩(m, v)) = (1/2) log (2πe v).

Used by

theorem

InformationTheory.Shannon.differentialEntropy_gaussianReal_std

source

differentialEntropy (ProbabilityTheory.gaussianReal 0 1) = 1 / 2 * Real.log (2 * Real.pi * Real.exp 1)

h(𝒩(0, 1)) = (1/2) log (2πe).

Used by

Gaussian maximum-entropy theorem #

theorem

InformationTheory.Shannon.differentialEntropy_le_gaussian_of_variance_le

source

{μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ.AbsolutelyContinuous MeasureTheory.volume) (m : ℝ) {v : NNReal} (hv : v ≠ 0) (h_mean : ∫ (x : ℝ), x ∂μ = m) (h_var : ∫ (x : ℝ), (x - m) ^ 2 ∂μ ≤ ↑v) (h_var_int : MeasureTheory.Integrable (fun (x : ℝ) => (x - m) ^ 2) μ) (h_ent_int : MeasureTheory.Integrable (fun (x : ℝ) => (μ.rnDeriv MeasureTheory.volume x).toReal.negMulLog) MeasureTheory.volume) :

differentialEntropy μ ≤ 1 / 2 * Real.log (2 * Real.pi * Real.exp 1 * ↑v)

Gaussian maximum-entropy theorem: for μ ≪ volume with mean m and variance ≤ v, differentialEntropy μ ≤ (1/2) log (2πe v).

The side hypotheses h_ent_int (integrability of negMulLog (dμ/dλ)) and h_var_int (integrability of (x - m)²) are needed because Bochner integration returns 0 for non-integrable functions, so without them the formal statement degenerates.

Used by

KL divergence between Gaussians and corollaries #

Gaussian moment helpers for KL computation #

theorem

InformationTheory.Shannon.gaussianReal_variance_eq

source

(m : ℝ) {v : NNReal} (_hv : v ≠ 0) :

∫ (x : ℝ), (x - m) ^ 2 ∂ProbabilityTheory.gaussianReal m v = ↑v

Used by

theorem

InformationTheory.Shannon.gaussianReal_integrable_sq

source

(m : ℝ) {v : NNReal} (_hv : v ≠ 0) :

MeasureTheory.Integrable (fun (x : ℝ) => x ^ 2) (ProbabilityTheory.gaussianReal m v)

Used by

theorem

InformationTheory.Shannon.gaussianReal_integrable_sq_sub

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) (c : ℝ) :

MeasureTheory.Integrable (fun (x : ℝ) => (x - c) ^ 2) (ProbabilityTheory.gaussianReal m v)

Used by

theorem

InformationTheory.Shannon.gaussianReal_integral_sq_sub_eq

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) (c : ℝ) :

∫ (x : ℝ), (x - c) ^ 2 ∂ProbabilityTheory.gaussianReal m v = ↑v + (m - c) ^ 2

Used by

theorem

InformationTheory.Shannon.gaussianReal_integrable_log_gaussianPDFReal

source

(m m' : ℝ) {v v' : NNReal} (hv : v ≠ 0) (hv' : v' ≠ 0) :

MeasureTheory.Integrable (fun (x : ℝ) => Real.log (ProbabilityTheory.gaussianPDFReal m' v' x)) (ProbabilityTheory.gaussianReal m v)

Used by

theorem

InformationTheory.Shannon.gaussianReal_integral_log_gaussianPDFReal_eq

source

(m m' : ℝ) {v v' : NNReal} (hv : v ≠ 0) (hv' : v' ≠ 0) :

∫ (x : ℝ), Real.log (ProbabilityTheory.gaussianPDFReal m' v' x) ∂ProbabilityTheory.gaussianReal m v = -(1 / 2) * Real.log (2 * Real.pi * ↑v') - (↑v + (m - m') ^ 2) / (2 * ↑v')

Used by

theorem

InformationTheory.Shannon.klDiv_gaussianReal_gaussianReal_eq

source

(m₁ m₂ : ℝ) {v₁ v₂ : NNReal} (hv₁ : v₁ ≠ 0) (hv₂ : v₂ ≠ 0) :

(klDiv (ProbabilityTheory.gaussianReal m₁ v₁) (ProbabilityTheory.gaussianReal m₂ v₂)).toReal = 1 / 2 * (Real.log (↑v₂ / ↑v₁) + ↑v₁ / ↑v₂ + (m₁ - m₂) ^ 2 / ↑v₂ - 1)

Closed-form KL divergence between two Gaussians.

Used by

Helper — concavity of `x ↦ log(1 + x/N)` on `Ici 0` #

Affine-substitution concavity used by AWGN converse C-1c (ConverseCapacityBound.sum_log_one_add_le_n_log_one_add_avg).

Built by composing Real.strictConcaveOn_log_Ioi.concaveOn (concavity of Real.log on Ioi 0) with the affine map x ↦ 1 + x/N, then restricting via ConcaveOn.subset to Ici 0 (since 1 + x/N ≥ 1 > 0 for x ≥ 0).

theorem

InformationTheory.Shannon.concaveOn_log_one_add_div

source

{N : ℝ} (hN_pos : 0 < N) :

ConcaveOn ℝ (Set.Ici 0) fun (x : ℝ) => Real.log (1 + x / N)

Used by

InformationTheory.Shannon.DifferentialEntropy

Differential entropy and Gaussian max-entropy #

Main definitions #

Main statements #

Differential entropy: definition and basic integrability #

Translation invariance and scaling #

Differential entropy of the Gaussian: h(𝒩(m, v)) = (1/2) log (2πe v) #

Gaussian maximum-entropy theorem #

KL divergence between Gaussians and corollaries #

Gaussian moment helpers for KL computation #

Helper — concavity of x ↦ log(1 + x/N) on Ici 0 #

Differential entropy of the Gaussian: `h(𝒩(m, v)) = (1/2) log (2πe v)` #

Helper — concavity of `x ↦ log(1 + x/N)` on `Ici 0` #