Normalization of the convolution density (EPI A-5 precondition (2)) #

∫ z, convDensityAdd pX g_t z ∂volume = 1 when pX is a normalized probability density and g_t = gaussianPDFReal 0 ⟨t, _⟩ is a Gaussian heat kernel (t > 0).

Route #

convDensityAdd pX g z = ∫ x, pX x * g (z - x) = (pX ⋆[ContinuousLinearMap.mul ℝ ℝ, volume] g) z (definitional match: (mul ℝ ℝ) a b = a * b). We then apply MeasureTheory.integral_convolution, which gives ∫ z, (pX ⋆[L,ν] g) z = L (∫ pX) (∫ g) = (∫ pX) * (∫ g) = 1 * 1 = 1.

• ∫ pX = 1 from hpX_norm.
• ∫ g = 1 from ProbabilityTheory.integral_gaussianPDFReal_eq_one.
• Gaussian integrability Integrable g from ProbabilityTheory.integrable_gaussianPDFReal.