The V2 de Bruijn regularity bundle from an explicit Lebesgue density pX of X: a probability density (nonnegative, measurable) carrying the withDensity law pX_law and a finite second moment hpX_mom, together with the standard-normal law of Z. The density witness density_t is pinned to the smooth convolution convDensityAdd pX g_t, so density_t_eq is rfl.

@audit:ok

de Bruijn identity (per-time, density form, Cover–Thomas).

For X ⊥ Z with Z ∼ 𝒩(0, 1) and an explicit Lebesgue density pX of X (a probability density with finite second moment), the heat-flow entropy h(X + √s·Z) has, at every time t > 0, derivative (1/2)·J(X + √t·Z) with the V2 Fisher information of the smooth convolution density pX ∗ g_t.

The class is non-vacuous: Gaussian X ∼ 𝒩(m, v) instantiates it with pX = gaussianPDFReal m v (see isDeBruijnPathRegular_gaussian), and every absolutely-continuous X with finite second moment supplies pX = (P.map X).rnDeriv volume (see isDeBruijnPathRegular_of_heat_flow).

References: [CoverThomas2006].

@audit:ok

The Gaussian inhabitant of IsDeBruijnPathRegular: for X ∼ 𝒩(m, v) (v ≠ 0), Z ∼ 𝒩(0, 1), X ⊥ Z, the heat-flow path is regular on [0, T]. The density witness path is fPath t = gaussianPDFReal m (v + t), whose Fisher information is the bounded continuous closed form 1 / (v + t), so the path integrand is interval-integrable; the heat-flow entropy is the closed form (1/2)·log(2π e (v + s)), continuous on [0, T].

This witness shows IsDeBruijnPathRegular (and hence debruijnIntegrationIdentity_holds) is non-vacuous.

@audit:ok

Integrated de Bruijn identity (gaussian, Cover–Thomas). The integrated form h(X + √T·Z) − h(X) = ∫₀ᵀ (1/2)·J(X + √t·Z) dt for a Gaussian X ∼ 𝒩(m, v), obtained by applying debruijnIntegrationIdentity_holds to the Gaussian path-regularity witness.

References: [CoverThomas2006].

@audit:ok

The general absolutely-continuous producer of IsDeBruijnPathRegular. For X ⊥ Z with Z ∼ 𝒩(0, 1) and an explicit probability density pX of X with finite second moment and finite differential entropy (hpX_ent), the heat-flow path is regular on [0, T]. The per-time regularity (reg_t) is the density bundle isRegularDeBruijnHypV2_of_density; the heat-flow entropy continuity (cont) combines the endpoint continuity heatFlowDifferentialEntropy_continuousWithinAt_zero (at t = 0⁺) with the interior continuity from the per-time de Bruijn HasDerivAt.

The interval-integrability of the path integrand (1/2)·J(X + √t·Z) (integrable) is closed by debruijnHeatPath_intervalIntegrable: the integrand is nonnegative and, by the convolution bound J(pX ∗ g_t) ≤ 1/t (gaussianConv_fisher_le_inv_var), bounded on each [ε, T] (ε > 0); there it equals the derivative of the heat-flow entropy, so the FTC gives ∫_ε^T = h(X + √T·Z) − h(X + √ε·Z), and the G2 endpoint continuity (ε ↓ 0) bounds these uniformly, upgrading to integrability on (0, T) via integrableOn_Ioc_of_intervalIntegral_norm_bounded_left. This routes only through the per-time de Bruijn identity, never its integrated form, so it is non-circular.

@audit:ok

Integrated de Bruijn identity (general a.c. Cover–Thomas). The integrated form h(X + √T·Z) − h(X) = ∫₀ᵀ (1/2)·J(X + √t·Z) dt for a general absolutely-continuous X, obtained by applying debruijnIntegrationIdentity_holds to the general path-regularity producer isDeBruijnPathRegular_of_heat_flow.

References: [CoverThomas2006].

@audit:ok