InformationTheory.Shannon.FisherInfo.OfDensity

Imports 13

Fisher information of a density #

The Fisher information fisherInfoOfDensity f := ∫⁻ (logDeriv f x)² · f x dx takes the density f : ℝ → ℝ as an explicit argument rather than extracting it from a measure via Measure.rnDeriv. The Radon–Nikodym derivative is defined via Classical.choose of the Lebesgue decomposition and returns a generically non-differentiable representative, so a measure-keyed definition collapses logDeriv to 0 a.e.; supplying the density directly avoids that.

Main definitions #

fisherInfoOfDensity — the Fisher information of a density (ℝ≥0∞-valued).
fisherInfoOfDensityReal — its real-valued projection.
IsRegularDensityV2 — the regularity predicate with the density f as its primary field.

Main statements #

integral_logDeriv_density_eq_zero — the score function has zero expectation.
fisherInfoOfDensity_gaussianPDFReal — the Gaussian closed form fisherInfoOfDensity (gaussianPDFReal m v) = ENNReal.ofReal (1 / v).

noncomputable def

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity

source

(f : ℝ → ℝ) :

ENNReal

The Fisher information of a density f : ℝ → ℝ, defined as ∫⁻ (logDeriv f x)² · f x dx with logDeriv f := deriv f / f Mathlib's score function. Valued in ℝ≥0∞ to capture +∞ for irregular families; use fisherInfoOfDensityReal or .toReal to project to ℝ when finite.

Equations

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity f = ∫⁻ (x : ℝ), ENNReal.ofReal (logDeriv f x ^ 2) * ENNReal.ofReal (f x)

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity_nonneg

source

(f : ℝ → ℝ) :

0 ≤ fisherInfoOfDensity f

Fisher information of a density is non-negative (trivially, as ℝ≥0∞).

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity_zero

source

(fisherInfoOfDensity fun (x : ℝ) => 0) = 0

The Fisher information of the constant-zero density is 0.

Used by

noncomputable def

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensityReal

source

(f : ℝ → ℝ) :

ℝ

Real-valued projection of fisherInfoOfDensity.

Equations

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensityReal f = (InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity f).toReal

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensityReal_nonneg

source

(f : ℝ → ℝ) :

0 ≤ fisherInfoOfDensityReal f

Used by

structure

InformationTheory.Shannon.FisherInfo.IsRegularDensityV2

source

(f : ℝ → ℝ) :

Prop

The regularity predicate on a density f, bundling the differentiability, positivity, tail-vanishing, and integrability conditions needed for integral_logDeriv_density_eq_zero. No measure is mentioned: the link to a random variable X is established separately via an a.e.-equality between f and (pdf X P volume).toReal.

diff : Differentiable ℝ f
f is differentiable on all of ℝ.
pos(x : ℝ) : 0 < f x
f is strictly positive everywhere (so logDeriv f is well-defined).
tail_bot : Filter.Tendsto f Filter.atBot (nhds 0)
f tends to 0 at -∞.
tail_top : Filter.Tendsto f Filter.atTop (nhds 0)
f tends to 0 at +∞.
integrable_deriv : MeasureTheory.Integrable (deriv f) MeasureTheory.volume
deriv f is Lebesgue-integrable on all of ℝ.
integral_deriv_eq_zero : ∫ (x : ℝ), deriv f x = 0
deriv f integrates to 0 over ℝ, a regularity consequence of FTC plus tail-vanishing on the half-lines.

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.integral_logDeriv_density_eq_zero

source

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

∫ (x : ℝ), logDeriv f x * f x = 0

The score function has zero expectation: for a regular density f, the integral of logDeriv f · f = deriv f over ℝ is 0.

@audit:ok

Used by

Gaussian closed form #

theorem

InformationTheory.Shannon.FisherInfo.integrable_logDeriv_sq_mul_gaussianPDFReal

source

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

MeasureTheory.Integrable (fun (x : ℝ) => ((x - m) / ↑v) ^ 2 * ProbabilityTheory.gaussianPDFReal m v x) MeasureTheory.volume

((x - m) / v)² · gaussianPDFReal m v x is Lebesgue-integrable for v ≠ 0.

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity_gaussianPDFReal

source

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

fisherInfoOfDensity (ProbabilityTheory.gaussianPDFReal m v) = ENNReal.ofReal (1 / ↑v)

The Gaussian Fisher information in closed form: fisherInfoOfDensity (gaussianPDFReal m v) = ENNReal.ofReal (1 / v), obtained by supplying the Gaussian PDF directly and evaluating the integral via the variance identity.

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfDensityReal_gaussianPDFReal

source

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

fisherInfoOfDensityReal (ProbabilityTheory.gaussianPDFReal m v) = 1 / ↑v

Real-valued projection of the Gaussian Fisher info closed form.

Used by