The law of the heat-flow path X + √s · Z factors as the convolution of the law of X with 𝒩(0, s · v_Z) when Z ∼ 𝒩(0, v_Z): P.map (gaussianConvolution X Z s) = (P.map X) ∗ gaussianReal 0 ⟨s · v_Z, _⟩. Holds for arbitrary X (no density witness needed). Via √s · Z ∼ 𝒩(0, s · v_Z) (gaussianReal_map_const_mul) and IndepFun.map_add_eq_map_conv_map.

@audit:ok

When P.map X has a real density witness pX and Z ∼ 𝒩(0, v_Z) with v_Z > 0, the density of the heat-flow path X + √s · Z is a.e. equal to convDensityAdd pX (gaussianPDFReal 0 ⟨s · v_Z, _⟩). The chain composes gaussianConvolution_law_conv (law factorization), gaussianReal_of_var_ne_zero, conv_withDensity_eq_lconvolution, and the bridge pPath_eq_convDensityAdd_lconvolution_bridge. The general v_Z is needed for the sum instance (X+Y, Z_X+Z_Y), whose noise has variance 2.

@audit:ok

The heat kernel g(σ, u) = (√(2πσ))⁻¹ · exp(-u²/(2σ)) with σ ranging over ℝ. Used so the σ-derivative can be taken over a real neighborhood (the coercion ⟨σ, _⟩ : ℝ≥0 cannot be formed for σ < 0); it agrees with gaussianPDFReal 0 ⟨σ, _⟩ for σ > 0 (heatFlow_density_heat_equation_kernel_eq).

The kernel agrees with gaussianPDFReal 0 ⟨σ, _⟩ for σ > 0.

@audit:ok

The spatial first derivative of the Gaussian heat kernel: ∂_u g_σ(u) = g_σ(u) · (-(u/σ)) for σ > 0.

@audit:ok

The spatial second derivative of the Gaussian heat kernel: ∂²_u g_σ(u) = g_σ(u) · (u²/σ² - 1/σ).

@audit:ok

The σ-derivative of the Gaussian heat kernel: ∂_σ g_σ(u) = (1/2) · g_σ(u) · (u²/σ² - 1/σ).

@audit:ok

The Gaussian heat kernel solves the heat equation ∂_σ g_σ(u) = (1/2) · ∂²_u g_σ(u); both sides equal (1/2) · g_σ(u) · (u²/σ² - 1/σ).

@audit:ok

The heat-flow density satisfies the heat equation: ∂_σ pPath σ x = (1/2) ∂²_x pPath σ x at σ = s. Here hpPath pins pPath σ to the heat-flow convolution convDensityAdd pX (gaussianPDFReal 0 ⟨σ, _⟩) on the positive σ-range, and hpathDeriv1 / hpathDeriv2 identify pathDeriv1 / pathDeriv2 as its spatial first and second derivatives. These pins fix which functions the arguments are; the heat-equation equality is the conclusion, derived from the kernel-level heat equation, not a hypothesis. The remaining arguments are per-y integrand domination preconditions in the shape consumed by hasDerivAt_integral_of_dominated_loc_of_deriv_le.

@audit:ok

Differentiation under the integral sign for the entropy along the heat-flow path: (d/ds) ∫ x, negMulLog (pPath s x) ∂volume = ∫ x, entDeriv t x ∂volume at s = t, via the gateway hasDerivAt_integral_of_dominated_loc_of_deriv_le. The domination and per-x derivative hypotheses are quantified over the neighborhood Set.Ioo (t/2) (2*t) (all the gateway needs); a universal form would be un-instantiable since the integrand diverges as s → 0⁺ and s → ∞.

@audit:ok

The de Bruijn integration-by-parts step on the whole line: ∫ x, u x · v' x = - ∫ x, u' x · v x, where the boundary terms vanish by tail decay. A direct application of MeasureTheory.integral_mul_deriv_eq_deriv_mul_of_integrable.

@audit:ok

Shape congruence connecting the IBP output to the V2 Fisher information: ∫ x, (logDeriv p x)² · p x ∂volume = fisherInfoOfDensityReal p, under nonnegativity and integrability so the ℝ≥0∞ ↔ ℝ round-trip holds.

@audit:ok

When pX is a nonnegative integrable density with positive mass (0 < ∫ pX), the Gaussian convolution density is strictly positive at every x. The integrand y ↦ pX y · g_s(x-y) is nonnegative and integrable with support equal to that of pX (the Gaussian factor never vanishes), and 0 < ∫ pX gives positive-measure support, hence a positive integral.

@audit:ok

The Gaussian convolution density is bounded below by a (1/2)-scaled shifted Gaussian: there is a radius R > 0 with (1/2) · g_s (|x| + R) ≤ convDensityAdd pX g_s x for every x. The proof picks R so that ∫_{[-R,R]} pX ≥ 1/2 (tightness), drops the integral to that box, and uses the monotonicity of g_s in |·|.

@audit:ok