InformationTheory.Shannon.FisherInfo.DeBruijn

Imports 11

Fisher information V2 — measure-keyed wrapper and de Bruijn identity #

Builds on the density-as-input Fisher information of FisherInfo/OfDensity.lean to define a measure-keyed wrapper, the heat-flow convolution path X + √t · Z, the V2 de Bruijn regularity predicate, and the Gaussian discharge of the de Bruijn identity.

Main definitions #

fisherInfoOfMeasureV2 — the Fisher information of a measure carrying an explicit smooth density witness.
gaussianConvolution — the heat-flow path X + √t · Z.
IsRegularDeBruijnHypV2 — the V2 de Bruijn regularity predicate, whose right-hand side uses the V2 Fisher information.
IsDeBruijnPathRegular — the path-regularity bundle for the integrated de Bruijn identity.

Main statements #

fisherInfoOfMeasureV2_gaussianReal — the Gaussian closed form 1 / v.
gaussianConvolution_law_of_gaussian — the law of X + √t · Z is 𝒩(m, v + t) when X is Gaussian and X ⊥ Z.
deBruijn_identity_v2_gaussian — the de Bruijn identity for a Gaussian X, (d/dt) h(X + √t · Z) = 1 / (2(v + t)).

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Measure-keyed wrapper #

noncomputable def

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2

source

(_μ : MeasureTheory.Measure ℝ) (f : ℝ → ℝ) :

ENNReal

The Fisher information of a measure μ carrying an explicit smooth density witness f, computed as fisherInfoOfDensity f. The witness is syntactically unrelated to μ.rnDeriv volume; the caller is responsible for the relevant a.e.-equality.

Equations

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2 _μ f = InformationTheory.Shannon.FisherInfo.fisherInfoOfDensity f

Instances For

Used by

noncomputable def

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2Real

source

(_μ : MeasureTheory.Measure ℝ) (f : ℝ → ℝ) :

ℝ

Real-valued projection of fisherInfoOfMeasureV2.

Equations

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2Real _μ f = InformationTheory.Shannon.FisherInfo.fisherInfoOfDensityReal f

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2_def

source

(μ : MeasureTheory.Measure ℝ) (f : ℝ → ℝ) :

fisherInfoOfMeasureV2 μ f = fisherInfoOfDensity f

Unfold lemma.

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2Real_def

source

(μ : MeasureTheory.Measure ℝ) (f : ℝ → ℝ) :

fisherInfoOfMeasureV2Real μ f = fisherInfoOfDensityReal f

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2_gaussianReal

source

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

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

The Gaussian Fisher information in measure-keyed form: fisherInfoOfMeasureV2 (gaussianReal m v) (gaussianPDFReal m v) = ENNReal.ofReal (1 / v).

Used by

theorem

InformationTheory.Shannon.FisherInfo.fisherInfoOfMeasureV2Real_gaussianReal

source

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

fisherInfoOfMeasureV2Real (ProbabilityTheory.gaussianReal m v) (ProbabilityTheory.gaussianPDFReal m v) = 1 / ↑v

Real-valued Gaussian Fisher info via V2.

Used by

Heat-flow path #

noncomputable def

InformationTheory.Shannon.FisherInfo.gaussianConvolution

source

{α : Type u_1} (X Z : α → ℝ) (t : ℝ) :

α → ℝ

The heat-flow convolution path X + √t · Z, the t-parametrised family underlying the de Bruijn identity. For Z ∼ 𝒩(0, 1) and X ⊥ Z, the law P.map (gaussianConvolution X Z t) is the convolution of P.map X with 𝒩(0, t).

Equations

InformationTheory.Shannon.FisherInfo.gaussianConvolution X Z t ω = X ω + √t * Z ω

Instances For

Used by

theorem

InformationTheory.Shannon.FisherInfo.gaussianConvolution_law_of_gaussian

source

{Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X Z : Ω → ℝ} (hX : Measurable X) (hZ : Measurable Z) (hXZ : ProbabilityTheory.IndepFun X Z P) {m : ℝ} {v : NNReal} (hX_law : MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m v) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1) {t : ℝ} (ht : 0 ≤ t) :

MeasureTheory.Measure.map (gaussianConvolution X Z t) P = ProbabilityTheory.gaussianReal m (v + ⟨t, ht⟩)

The law of X + √t · Z is 𝒩(m, v + t) when X ∼ 𝒩(m, v), Z ∼ 𝒩(0, 1), and X ⊥ Z.

Used by

The de Bruijn regularity predicate #

structure

InformationTheory.Shannon.FisherInfo.IsRegularDeBruijnHypV2

source

{Ω : Type u_1} [MeasurableSpace Ω] (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (t : ℝ) :

Type

The V2 de Bruijn regularity predicate. It carries a smooth density witness density_t : ℝ → ℝ for the law of X + √t · Z, together with regularity preconditions on X. The Fisher information on the right-hand side of the de Bruijn identity uses fisherInfoOfDensity of an explicit density witness, so the Gaussian case evaluates to 1 / v. The de Bruijn identity itself is not a field of this predicate; it is proved separately in debruijnIdentityV2_holds_assembled.

Z_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1
Z is standard normal.
density_t : ℝ → ℝ
Smooth density witness for P.map (X + √t · Z).
pX : ℝ → ℝ
A real density witness for X itself: the law of X + √s · Z is the convolution of P.map X with a Gaussian, expressed via convDensityAdd pX g_σ. Declared before density_t_eq so the latter's right-hand side can reference pX.
pX_nn(x : ℝ) : 0 ≤ self.pX x
The density witness pX is nonnegative.
pX_meas : Measurable self.pX
The density witness pX is measurable.
pX_law : MeasureTheory.Measure.map X P = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (self.pX x)
X has Lebesgue density pX.
density_t_eq(ht : 0 < t) (x : ℝ) : self.density_t x = EPIConvDensity.convDensityAdd self.pX (ProbabilityTheory.gaussianPDFReal 0 ⟨t, ⋯⟩) x
The density witness density_t equals the smooth representative convDensityAdd pX (gaussianPDFReal 0 ⟨t, ht.le⟩) — the convolution of pX with the time-t Gaussian heat kernel, which is the genuine density of P.map (X + √t · Z). Pinning to this smooth convolution (rather than to the Measure.rnDeriv representative, which is generically non-differentiable) keeps logDeriv and hence fisherInfoOfDensity density_t nonzero. The positivity 0 < t is taken as an argument since the structure does not carry it.
pX_mom : MeasureTheory.Integrable (fun (y : ℝ) => y ^ 2 * self.pX y) MeasureTheory.volume
X has a finite second moment: y ↦ y² · pX y is volume-integrable.

Instances For

Used by

structure

InformationTheory.Shannon.FisherInfo.IsDeBruijnPathRegular

source

{Ω : Type u_1} [MeasurableSpace Ω] (X Z : Ω → ℝ) (P : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure P] (T : ℝ) :

Type

The path-regularity bundle for the integrated de Bruijn identity, packaging the FTC ingredients needed to integrate the per-time debruijnIdentityV2_holds_assembled derivative along the heat-flow path (0, T).

fPath — the density witness path: fPath t is the density of P.map (gaussianConvolution X Z t).
reg_t — per-time V2 de Bruijn regularity at each interior t ∈ (0, T), with density_t = fPath t so the per-time derivative value matches the integrand.
cont — continuity of the heat-flow entropy on [0, T].
integrable — interval-integrability of the path integrand (1/2) · J(X + √t · Z) on (0, T).

@audit:ok

fPath : ℝ → ℝ → ℝ
Density witness path.
reg_t(t : ℝ) : t ∈ Set.Ioo 0 T → ∃ (h_reg : IsRegularDeBruijnHypV2 X Z P t), h_reg.density_t = self.fPath t
Per-time V2 de Bruijn regularity at each interior time, with the density witness pinned to fPath t.
cont : ContinuousOn (fun (s : ℝ) => differentialEntropy (MeasureTheory.Measure.map (gaussianConvolution X Z s) P)) (Set.Icc 0 T)
Continuity of the heat-flow entropy on [0, T].
integrable : IntervalIntegrable (fun (t : ℝ) => 1 / 2 * fisherInfoOfDensityReal (self.fPath t)) MeasureTheory.volume 0 T
The path integrand is interval-integrable.

Instances For

Used by

Gaussian discharge #

theorem

InformationTheory.Shannon.FisherInfo.hasDerivAt_half_log_gaussian_entropy

source

{v : NNReal} (s : ℝ) (hvs : 0 < ↑v + s) :

HasDerivAt (fun (s' : ℝ) => 1 / 2 * Real.log (2 * Real.pi * Real.exp 1 * (↑v + s'))) (1 / (2 * (↑v + s))) s

(1/2) · log (2π e (v + s)) has derivative 1 / (2(v + s)) at s when v + s > 0.

Used by

theorem

InformationTheory.Shannon.FisherInfo.differentialEntropy_gaussianReal_heat_path

source

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

differentialEntropy (ProbabilityTheory.gaussianReal m (v + ⟨s, hs⟩)) = 1 / 2 * Real.log (2 * Real.pi * Real.exp 1 * (↑v + s))

The differential entropy of gaussianReal m (v + s) along the heat-flow path equals (1/2) · log (2π e (v + s)) for s ≥ 0.

Used by

theorem

InformationTheory.Shannon.FisherInfo.deBruijn_identity_v2_gaussian

source

{Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (X Z : Ω → ℝ) (hX : Measurable X) (hZ : Measurable Z) (hXZ : ProbabilityTheory.IndepFun X Z P) {m : ℝ} {v : NNReal} (hv : v ≠ 0) (hX_law : MeasureTheory.Measure.map X P = ProbabilityTheory.gaussianReal m v) (hZ_law : MeasureTheory.Measure.map Z P = ProbabilityTheory.gaussianReal 0 1) {t : ℝ} (ht : 0 < t) :

HasDerivAt (fun (s : ℝ) => differentialEntropy (MeasureTheory.Measure.map (gaussianConvolution X Z s) P)) (1 / 2 * fisherInfoOfMeasureV2Real (MeasureTheory.Measure.map (gaussianConvolution X Z t) P) (ProbabilityTheory.gaussianPDFReal m (v + ⟨t, ⋯⟩))) t

The de Bruijn identity for a Gaussian X (hypothesis-free): for X ∼ 𝒩(m, v), Z ∼ 𝒩(0, 1), X ⊥ Z, and t > 0, (d/dt) h(X + √t · Z) = (1/2) · J(𝒩(m, v + t)) = 1 / (2(v + t)).

Used by