InformationTheory.Shannon.EPI.Stam.Standalone

Imports 4

Stam's inequality — standalone density-level headline (Cover–Thomas) #

This file assembles the genuine, sorry-free parts already present in the project into a clean, self-contained statement of Stam's inequality at the density level, for the non-vacuous class of Gaussian-smoothed densities pX ∗ g_t (t > 0, pX any probability density). No new analytic core is introduced: every ingredient (the convex Fisher bound, the λ-optimization, the regularity and IsBlachmanConvReady producers, the convolution Fisher finiteness bound) is an existing @audit:ok asset; this file is the wiring plus the smoothed-density Fisher positivity producer.

Main statements #

fisherInfoOfDensity_ne_zero_of_regular — a regular density has nonzero Fisher information.
fisherInfoOfDensity_convDensityAdd_gaussian_pos — the Fisher information of a Gaussian-smoothed density pX ∗ g_t is strictly positive and finite (the positivity producer).
stam_inequality_smoothed_density — the headline Stam inequality 1 / J(fX ∗ fY) ≥ 1 / J(fX) + 1 / J(fY) for fX = pX ∗ g_t, fY = pY ∗ g_t.

References #

[CoverThomas2006]; [Blachman1965].

theorem

InformationTheory.Shannon.StamInequality.fisherInfoOfDensity_ne_zero_of_regular

source

{f : ℝ → ℝ} (h_reg : FisherInfo.IsRegularDensityV2 f) :

FisherInfo.fisherInfoOfDensity f ≠ 0

A regular density (IsRegularDensityV2) has strictly positive Fisher information: if it were zero, the score logDeriv f would vanish a.e., forcing deriv f = 0 a.e., hence (by the fundamental theorem of calculus and the integrability of deriv f) f constant, contradicting the tail-vanishing and strict positivity of a regular density.

@audit:ok

Used by

theorem

InformationTheory.Shannon.StamInequality.fisherInfoOfDensity_convDensityAdd_gaussian_pos

source

(pX : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_norm : ∫ (x : ℝ), pX x = 1) :

0 < (FisherInfo.fisherInfoOfDensity (EPIConvDensity.convDensityAdd pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩))).toReal

The Fisher information of a Gaussian-smoothed probability density pX ∗ g_t (t > 0) is strictly positive as a real number: finiteness comes from the convolution Fisher bound J ≤ 1/t, and nonzero-ness from regularity.

@audit:ok

Used by

theorem

InformationTheory.Shannon.StamInequality.stam_inequality_smoothed_density

source

(pX pY : ℝ → ℝ) {t : ℝ} (ht : 0 < t) (hpX_nn : ∀ (x : ℝ), 0 ≤ pX x) (hpX_meas : Measurable pX) (hpX_int : MeasureTheory.Integrable pX MeasureTheory.volume) (hpX_norm : ∫ (x : ℝ), pX x = 1) (hpY_nn : ∀ (x : ℝ), 0 ≤ pY x) (hpY_meas : Measurable pY) (hpY_int : MeasureTheory.Integrable pY MeasureTheory.volume) (hpY_norm : ∫ (x : ℝ), pY x = 1) :

Stam's inequality (density-level headline, Cover–Thomas / Blachman 1965).

For probability densities pX, pY and a Gaussian heat kernel g_t (t > 0), the Gaussian-smoothed densities fX = pX ∗ g_t, fY = pY ∗ g_t satisfy the inverse (harmonic-mean) Fisher information inequality

1 / J(fX ∗ fY) ≥ 1 / J(fX) + 1 / J(fY).

The Gaussian-smoothed class is non-vacuous (it contains every heat-flow smoothing of an arbitrary probability density, not just Gaussian equality cases), so the inequality is not vacuously true.

References: [CoverThomas2006]; [Blachman1965].

@audit:ok

Used by