InformationTheory.Shannon.FisherInfo.DeBruijnGeneral

Imports 3

de Bruijn identity (V2) #

The per-time de Bruijn identity and its integrated form, delegating to the assembled per-time identity debruijnIdentityV2_holds_assembled. These consumers live downstream of the assembly file because the assembly transitively imports FisherInfo/DeBruijn.lean, so they cannot call the assembled identity from there without an import cycle.

Main statements #

deBruijn_identity_v2 — the per-time de Bruijn identity (d/dt) h(X + √t · Z) = (1/2) · J(X + √t · Z) with the V2 Fisher information.
debruijnIntegrationIdentity_holds — its integrated form along the heat-flow path.

References #

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

theorem

InformationTheory.Shannon.FisherInfo.deBruijn_identity_v2

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) {t : ℝ} (ht : 0 < t) (h_reg : IsRegularDeBruijnHypV2 X Z P t) :

HasDerivAt (fun (s : ℝ) => differentialEntropy (MeasureTheory.Measure.map (gaussianConvolution X Z s) P)) (1 / 2 * fisherInfoOfDensityReal h_reg.density_t) t

The de Bruijn identity (V2 form): for X ⊥ Z with Z ∼ 𝒩(0, 1), (d/dt) h(X + √t · Z) = (1/2) · J(X + √t · Z), stated with the V2 Fisher information fisherInfoOfDensityReal on the right. Delegates to debruijnIdentityV2_holds_assembled; h_reg is the regularity precondition.

Used by

theorem

InformationTheory.Shannon.FisherInfo.debruijnIntegrationIdentity_holds

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) (T : ℝ) (hT : 0 ≤ T) (h_path : IsDeBruijnPathRegular X Z P T) :

∃ (fPath : ℝ → ℝ → ℝ), ∀ (h_X h_target : ℝ), h_X = differentialEntropy (MeasureTheory.Measure.map X P) → h_target = differentialEntropy (MeasureTheory.Measure.map (gaussianConvolution X Z T) P) → h_target - h_X = ∫ (t : ℝ) in Set.Ioo 0 T, 1 / 2 * (fisherInfoOfMeasureV2 (MeasureTheory.Measure.map (gaussianConvolution X Z t) P) (fPath t)).toReal

The integrated de Bruijn identity: integrating the per-time identity debruijnIdentityV2_holds_assembled along the heat-flow path (0, T) via FTC gives h(X + √T·Z) − h(X) = ∫₀ᵀ (1/2)·J(X + √t·Z) dt. Here hT : 0 ≤ T and the path-regularity bundle h_path : IsDeBruijnPathRegular are regularity and integrability preconditions.

Used by