InformationTheory.Shannon.EPI.Plumbing

source

Imports 6

Entropy Power Inequality — plumbing lemmas #

Supporting lemmas for entropyPower μ := Real.exp (2 · h(μ)) published independently.

Main definitions #

gaussianEntropyPowerConst: Cover-Thomas (2πe) normalization constant.

Main statements #

entropyPower_pos_iff, entropyPower_ne_zero: strict positivity.
entropyPower_eq_of_differentialEntropy_eq, entropyPower_le_of_differentialEntropy_le, entropyPower_lt_of_differentialEntropy_lt: monotonicity.
log_entropyPower: log-form.
entropyPower_div_two_pi_e_gaussianReal: Gaussian normalization.
entropyPower_map_add_const_eq_self, entropyPower_map_mul_const, entropyPower_map_affine: translation and scaling.
entropy_power_inequality_normalized: N(X+Y) ≥ N(X) + N(Y) form.
entropy_power_inequality_four_arg: 4-argument chain.

Implementation notes #

The definition entropyPower μ := Real.exp (2 · h(μ)) is chosen so that Real.exp_pos, Real.exp_log, and Real.exp_le_exp apply directly. Stam inequality and de Bruijn integration discharge are out of scope here.

§1 — Positivity, non-zero, log-form #

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_ne_zero

source

(μ : MeasureTheory.Measure ℝ) :

entropyPower μ ≠ 0

entropyPower μ ≠ 0 (corollary of strict positivity).

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.log_entropyPower

source

(μ : MeasureTheory.Measure ℝ) :

Real.log (entropyPower μ) = 2 * differentialEntropy μ

Real.log (entropyPower μ) = 2 · h(μ).

Used by

§2 — Monotonicity in `differentialEntropy` #

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_eq_of_differentialEntropy_eq

source

{μ ν : MeasureTheory.Measure ℝ} (h : differentialEntropy μ = differentialEntropy ν) :

entropyPower μ = entropyPower ν

If two measures share the same differential entropy, their entropy powers coincide.

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_le_of_differentialEntropy_le

source

{μ ν : MeasureTheory.Measure ℝ} (h : differentialEntropy μ ≤ differentialEntropy ν) :

entropyPower μ ≤ entropyPower ν

Monotonicity (≤): h(μ) ≤ h(ν) ⟹ entropyPower μ ≤ entropyPower ν.

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_lt_of_differentialEntropy_lt

source

{μ ν : MeasureTheory.Measure ℝ} (h : differentialEntropy μ < differentialEntropy ν) :

entropyPower μ < entropyPower ν

Strict monotonicity (<): h(μ) < h(ν) ⟹ entropyPower μ < entropyPower ν.

Used by

§3 — Cover-Thomas `(2πe)⁻¹` normalized form #

noncomputable def

InformationTheory.Shannon.EntropyPowerInequality.gaussianEntropyPowerConst

source

ℝ

The Cover-Thomas normalization constant 2πe.

Equations

InformationTheory.Shannon.EntropyPowerInequality.gaussianEntropyPowerConst = 2 * Real.pi * Real.exp 1

Instances For

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.gaussianEntropyPowerConst_pos

source

0 < gaussianEntropyPowerConst

gaussianEntropyPowerConst > 0.

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_div_two_pi_e_gaussianReal

source

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

entropyPower (ProbabilityTheory.gaussianReal m v) / gaussianEntropyPowerConst = ↑v

Under the Cover-Thomas N(μ) := (2πe)⁻¹ · entropyPower μ normalization, the Gaussian saturating case takes the closed form N(gaussianReal m v) = v.

Used by

§4 — Translation / scaling / affine lift to `entropyPower` #

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_map_add_const_eq_self

source

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

entropyPower (MeasureTheory.Measure.map (fun (x : ℝ) => x + a) μ) = entropyPower μ

entropyPower (μ.map (· + a)) = entropyPower μ. This is the entropyPower companion to InformationTheory.Shannon.differentialEntropy_map_add_const.

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_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) :

entropyPower (MeasureTheory.Measure.map (fun (x : ℝ) => x * c) μ) = c ^ 2 * entropyPower μ

entropyPower (μ.map (· * c)) = |c|² · entropyPower μ.

Used by

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropyPower_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) :

entropyPower (MeasureTheory.Measure.map (fun (x : ℝ) => a * x + b) μ) = a ^ 2 * entropyPower μ

entropyPower (μ.map (fun x => a * x + b)) = a² · entropyPower μ.

The translation term + b is absorbed (entropy power is translation-invariant), leaving only the scaling factor a².

Used by

§6 — 4-argument EPI chain #

theorem

InformationTheory.Shannon.EntropyPowerInequality.entropy_power_inequality_four_arg

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (X Y Z W : Ω → ℝ) (h_xyz_w_epi : IsEntropyPowerInequalityHypothesis (fun (ω : Ω) => X ω + Y ω + Z ω) W P) (h_xy_z_epi : IsEntropyPowerInequalityHypothesis (fun (ω : Ω) => X ω + Y ω) Z P) (h_x_y_epi : IsEntropyPowerInequalityHypothesis X Y P) :

entropyPower (MeasureTheory.Measure.map (fun (ω : Ω) => X ω + Y ω + Z ω + W ω) P) ≥ entropyPower (MeasureTheory.Measure.map X P) + entropyPower (MeasureTheory.Measure.map Y P) + entropyPower (MeasureTheory.Measure.map Z P) + entropyPower (MeasureTheory.Measure.map W P)

For independent X, Y, Z, W with the appropriate entropy-power-inequality hypotheses, entropyPower (X+Y+Z+W) ≥ Σ entropyPower (·).

Chains three applications of the 2-arg IsEntropyPowerInequalityHypothesis predicate: once on ((X+Y)+Z) vs W, once on (X+Y) vs Z, once on X vs Y.

The entropy-power-inequality hypothesis is carried transparently through the h_*_epi arguments supplied by the caller; the chain to entropy_power_inequality_three_arg + linarith is a structural composition. The transitive load-bearing-ness lives in the IsEntropyPowerInequalityHypothesis predicate's definition site (EntropyPowerInequality.lean), not in this consumer wrapper. @audit:ok

Used by