InformationTheory.Shannon.FisherInfo.DeBruijnAssembly.Assembly
InformationTheory.Shannon.FisherInfo.debruijnIdentityV2_holds_assembled
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 per-time de Bruijn identity: for X ⊥ Z with Z ∼ 𝒩(0, 1) and t > 0,
(d/dt) differentialEntropy (P.map (X + √t · Z)) = (1/2) · fisherInfoOfDensityReal h_reg.density_t.
Proved by assembling the per-time atoms; lives in a separate file from the de Bruijn definitions to
avoid an import cycle. The body threads through _entropy_eq (entropy as ∫ negMulLog), _chain
(its s-derivative), and _fisher_match (the density-witness value), combined via
HasDerivAt.congr_of_eventuallyEq.
@audit:ok