Actual Gaussian convolution density and C2 normalized potential

Mathematical statement

The actual Gaussian add-noise probability law equals volume.withDensity(ofReal(C_eta Z_eta)). Its density is strictly positive at every y, Z_eta is globally C2, and the exact negative-log density U_eta=-log(C_eta Z_eta) is globally C2. The input law may be singular and may lack moments.

theorem gaussian_convolution_potential_c2 (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let C := ((Real.sqrt (2*Real.pi*η))⁻¹)^Module.finrank ℝ E
    let Z := fun y : E => ∫ x, Real.exp (-‖y-x‖^2/(2*η)) ∂μ
    (μ.prod (stdGaussian E)).map (fun p => p.1+Real.sqrt η • p.2) =
      (volume : Measure E).withDensity (fun y => ENNReal.ofReal (C*Z y)) ∧
    (∀ y, 0 < C*Z y) ∧ ContDiff ℝ 2 Z ∧
      ContDiff ℝ 2 (fun y => -Real.log (C*Z y))

Proof roadmap

1. 1Differentiate the actual Gaussian weight

   For u=y-x, w=exp(-norm(u)^2/(2eta)), differentiate the squared norm and exponential as Frechet maps. D_yw[v]=-eta^-1 w inner(u,v), and D_y²w[v,t]=w(eta^-2 inner(u,v)inner(u,t)-eta^-1 inner(v,t)). These are the explicit kernel derivatives, not derivatives of an assumed regularized potential.

2. 2Derive probability-integrable domination

   The Gaussian weight lies in (0,1]. With q=norm(u)^2/(2eta), q exp(-q)≤exp(-1)≤1 gives w norm(u)^2≤2eta. Since norm(u)≤1+norm(u)^2, the first derivative norm is at most (1+2eta)/eta. The second derivative operator norm is at most w norm(u)^2/eta²+w/eta≤3/eta. These constants are uniform in x and y, so the probability input integrates them without any moment condition.

3. 3Differentiate the actual normalizer twice

   Continuity of the displayed derivatives gives their Borel/strong measurability. Apply the dominated parametric-integral Frechet theorem first to w and then to Dw. Dominated continuity of the integral of D²w makes the first derivative C1, hence Z is C2. Probability mass one and everywhere w>0 imply Z(y)>0 at every observation, not merely almost everywhere.

4. 4Identify the actual smoothed density

   Project the existing genuine GaussianAugmentation joint density to its observation coordinate. For any measurable nonnegative test, the pushforward integral and nonnegative Fubini put the x-integral inside the y-integral. The established Bochner integrability identifies integral ofReal(C_eta w) with ofReal(C_eta Z). Equality against all such tests proves the exact volume density of the actual Gaussian add-noise law.

5. 5Form the exact normalized potential and expose the source convention

   The finite-dimensional Gaussian prefactor C_eta is strictly positive for eta>0, including dimension zero. Compose the C2 positive function C_eta Z with log and negate. This yields C2 of the actual normalized negative-log density, with its normalization constant retained. Source Hessian bounds require additional posterior covariance inequalities and are not inferred from C2 regularity. Source Section3.1 defines the unnormalized convolution exp(-V_eta)=exp(-V)*Gaussian. This theorem constructs the exact normalized density potential U_eta=-log(C_eta Z_mu). For Gibbs mu=exp(-V) volume/Z_V, U_eta=V_eta+log Z_V; formalizing that Gibbs specialization and constant-shift adapter remains separate. This normalization difference does not change derivatives, but the two chosen potentials are not asserted literally identical.