InformationTheory.Shannon.FisherInfo.Basic

Imports 9

Fisher information density helpers #

Density-based regularity predicates and score-function lemmas underpinning the Fisher information development. The score function reuses Mathlib's logDeriv f := deriv f / f (Mathlib/Analysis/Calculus/LogDeriv.lean), which is definitionally the score of a density f.

Main definitions #

IsRegularDensity — the regularity predicate (Cover–Thomas) bundling the differentiability, positivity, tail-vanishing, and integrability conditions on a smooth representative of the PDF.

Main statements #

integral_logDeriv_pdf_eq_zero — the score function logDeriv density · density has zero integral over ℝ.

Implementation notes #

The Fisher information itself is defined in FisherInfo/OfDensity.lean (fisherInfoOfDensity) and FisherInfo/DeBruijn.lean (fisherInfoOfMeasureV2); this file holds only the density-based helpers that do not reference those definitions.

structure

InformationTheory.Shannon.IsRegularDensity

source

{Ω : Type u_1} [MeasurableSpace Ω] (X : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.HasPDF X P MeasureTheory.volume] :

Type

The regularity predicate of Cover–Thomas, bundling the differentiability, positivity, tail-vanishing, and integrability conditions needed for integral_logDeriv_pdf_eq_zero. It is exposed as a predicate to be discharged downstream rather than verified for a general random variable X.

Since MeasureTheory.pdf X P volume is defined only up to a.e. equivalence, pointwise smoothness and positivity conditions cannot be stated on the PDF itself. The structure therefore carries a chosen smooth representative density : ℝ → ℝ together with the a.e.-equality pdf_ae_eq, and states the pointwise regularity conditions on density.

density : ℝ → ℝ
A smooth representative of the PDF ((pdf X P volume x).toReal is a.e.-equal to this representative, see pdf_ae_eq).
pdf_ae_eq : (fun (x : ℝ) => (MeasureTheory.pdf X P MeasureTheory.volume x).toReal) =ᵐ[MeasureTheory.volume ] self.density
(pdf X P volume).toReal equals the smooth representative density a.e.
diff : Differentiable ℝ self.density
The representative is differentiable on all of ℝ.
pos(x : ℝ) : 0 < self.density x
The representative is strictly positive everywhere (so logDeriv is well-defined).
tail_bot : Filter.Tendsto self.density Filter.atBot (nhds 0)
The representative tends to 0 at -∞.
tail_top : Filter.Tendsto self.density Filter.atTop (nhds 0)
The representative tends to 0 at +∞.
integrable_deriv : MeasureTheory.Integrable (deriv self.density) MeasureTheory.volume
The derivative of the representative is Lebesgue-integrable on all of ℝ.
integral_deriv_eq_zero : ∫ (x : ℝ), deriv self.density x = 0
The derivative integrates to 0 over ℝ (the boundary difference of density, which vanishes by the tail conditions). A regularity consequence equivalent to FTC plus tail-vanishing on the half-lines, discharged downstream via MeasureTheory.integral_deriv_eq_sub or its improper variants.

Instances For

Used by

theorem

InformationTheory.Shannon.integral_logDeriv_pdf_eq_zero

source

{Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X : Ω → ℝ) [MeasureTheory.HasPDF X P MeasureTheory.volume] (h_reg : IsRegularDensity X P) :

∫ (x : ℝ), logDeriv h_reg.density x * h_reg.density x = 0

The score function has zero expectation (Cover–Thomas). For the smooth representative density of IsRegularDensity, the integral of logDeriv density · density = deriv density over ℝ is 0. Stated on the representative h_reg.density; combine with h_reg.pdf_ae_eq to recast in terms of (pdf X P volume).toReal via an a.e.-integral congruence.

@audit:ok

Used by