Diffusion forward process: Gaussian law

We use this file as the mathlib-backed anchor for diffusion probability theory.

It formalizes a standard fact used implicitly throughout diffusion models:

If $Z$ is standard Gaussian in a finite-dimensional Euclidean space $E$, then

$x_t = c_0 x_0 + c_1 Z$

is Gaussian for any fixed $x_0 \in E$ and scalar coefficients $c_0,c_1 \in \mathbb{R}$.

In the DDPM/VP setting, the usual coefficients are:

• $c_0 = \sqrt{\bar{\alpha}_t}$
• $c_1 = \sqrt{1-\bar{\alpha}_t}$

At the spec layer (NN.Spec.Generative.Diffusion.ForwardProcess), we treat the noise $\varepsilon$ as an explicit tensor input. This file provides the probability-theory side: when that noise is sampled from stdGaussian, the resulting distribution is Gaussian.

The result gives the exact law-level fact used by VP/DDPM forward processes: affine noising of a fixed data point by standard Gaussian noise produces another Gaussian probability measure. We keep the statement at this level because it is the reusable primitive needed by ELBO or SDE developments.

References:

• Ho, Jain, and Abbeel, "Denoising Diffusion Probabilistic Models", NeurIPS 2020.
• Song et al., "Score-Based Generative Modeling through Stochastic Differential Equations", ICLR 2021.

noncomputable def NN.MLTheory.Generative.Diffusion.forwardGaussian {ι : Type u_1} [Fintype ι] (c0 c1 : ℝ) (x0 : EuclideanSpace ℝ ι) : MeasureTheory.Measure (EuclideanSpace ℝ ι)

Forward noising measure in a finite-dimensional Euclidean space:

$x \mapsto c_0 x_0 + c_1 x$, where $x$ follows the standard Gaussian law.

We define it as a composition of:

• a linear map $x \mapsto c_1 x$, and
• a translation $y \mapsto y + c_0 x_0$,

so that Gaussian-closure lemmas in mathlib apply directly.

instance NN.MLTheory.Generative.Diffusion.instIsProbabilityMeasureEuclideanSpaceRealForwardGaussian {ι : Type u_1} [Fintype ι] (c0 c1 : ℝ) (x0 : EuclideanSpace ℝ ι) : MeasureTheory.IsProbabilityMeasure (forwardGaussian c0 c1 x0)

theorem NN.MLTheory.Generative.Diffusion.forwardGaussian_isGaussian {ι : Type u_1} [Fintype ι] (c0 c1 : ℝ) (x0 : EuclideanSpace ℝ ι) : ProbabilityTheory.IsGaussian (forwardGaussian c0 c1 x0)