Diffusion forward process: Gaussian noising

This file gives a small, Mathlib-backed formalization of the forward (noising) step used in diffusion models, expressed as an affine pushforward of the standard Gaussian measure.

We work in a finite-dimensional real inner product space E equipped with its Borel $\sigma$-algebra.

Main definitions:

• forwardNoising a b x : the measure of x' = a • x + b • z with z ∼ stdGaussian E.
• forwardKernel a b : the associated Markov kernel x ↦ forwardNoising a b x.

Main facts:

• forwardNoising is Gaussian (ProbabilityTheory.IsGaussian), hence a probability measure.
• forwardKernel is a Markov kernel (ProbabilityTheory.IsMarkovKernel).
• the step has mean a • x (integral_id_forwardNoising) and isotropic noise of scale b (variance_dual_forwardNoising).

A note on why the moments get their own theorems: IsGaussian says the law is Gaussian, not which Gaussian it is. Anything that reasons about a DDPM noise schedule needs the parameters, so we record the first moment and the dual form of the covariance here instead of asking every caller to redo the same pushforward computation. Reference for the schedule these parameters feed: Ho, Jain, and Abbeel, Denoising Diffusion Probabilistic Models, NeurIPS 2020.

noncomputable def NN.Proofs.Probability.forwardNoising {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] (a b : ℝ) (x : E) : MeasureTheory.Measure E

Forward noising measure for a diffusion step: x' = a • x + b • z with z ∼ stdGaussian E.

This is the measure-level analogue of the forward process used in DDPM-style diffusion models: the current clean state x is scaled by a, and isotropic Gaussian noise is scaled by b and added. The exact schedule that chooses a and b belongs to the model spec; this theorem layer only needs the affine-Gaussian kernel shape.

@[simp]

theorem NN.Proofs.Probability.forwardNoising_eq_map {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : forwardNoising a b x = MeasureTheory.Measure.map (fun (z : E) => a • x + b • z) (ProbabilityTheory.stdGaussian E)

The two-step definition of forwardNoising is equal to one direct affine pushforward.

The definition is written in stages so typeclass inference can see a Gaussian pushforward through a linear map followed by translation; this lemma is the cleaner formula downstream proofs usually want.

instance NN.Proofs.Probability.instIsGaussianForwardNoising {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : ProbabilityTheory.IsGaussian (forwardNoising a b x)

Affine images of a finite-dimensional standard Gaussian are Gaussian.

instance NN.Proofs.Probability.instIsProbabilityMeasureForwardNoising {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : MeasureTheory.IsProbabilityMeasure (forwardNoising a b x)

Every forward-noising measure has total mass one.

@[simp]

theorem NN.Proofs.Probability.forwardNoising_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : (forwardNoising a b x) Set.univ = 1

The explicit total-mass theorem for the forward-noising measure.

theorem NN.Proofs.Probability.integral_id_forwardNoising {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : ∫ (y : E), y ∂forwardNoising a b x = a • x

The mean of one forward-noising step is the scaled clean state:

E[x'] = a • x.

The noise term contributes nothing because the standard Gaussian is centred (ProbabilityTheory.integral_id_stdGaussian), so all that survives the pushforward is the constant a • x. Integrability of the identity under a Gaussian measure comes from Fernique's theorem, which Mathlib exposes as ProbabilityTheory.IsGaussian.integrable_id; we need it to split the integral of the sum.

theorem NN.Proofs.Probability.variance_dual_forwardNoising {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) (L : StrongDual ℝ E) : ProbabilityTheory.variance (⇑L) (forwardNoising a b x) = b ^ 2 * ‖L‖ ^ 2

Every continuous linear functional of a forward-noising step has variance b ^ 2 * ‖L‖ ^ 2.

This is the dual form of "the covariance operator is b ^ 2 times the identity". We state it against StrongDual rather than as a covariance matrix for two reasons: it is the form Mathlib's multivariate Gaussian API is built on (ProbabilityTheory.variance_dual_stdGaussian), and it is what a proof about a single coordinate of the noised state actually consumes. Taking L to be the inner product with a unit vector gives variance b ^ 2 along that direction, and the absence of any dependence on the direction is exactly the isotropy claim.

Note that a and x do not appear on the right: scaling and translating by a constant shifts the mean and leaves the spread alone.

noncomputable def NN.Proofs.Probability.forwardKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] (a b : ℝ) : ProbabilityTheory.Kernel E E

Forward noising kernel for a diffusion step, as a Markov kernel.

instance NN.Proofs.Probability.instIsMarkovKernelForwardKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) : ProbabilityTheory.IsMarkovKernel (forwardKernel a b)

The forward diffusion transition is a Markov kernel.

This packages measurability and probability-mass obligations so later verification statements can compose diffusion steps as kernels rather than manually carrying measure facts.

theorem NN.Proofs.Probability.forwardKernel_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : (forwardKernel a b) x = forwardNoising a b x

Applying the kernel at state x recovers exactly the forward-noising measure at x.

The kernel is built from id × const stdGaussian so it fits Mathlib kernel composition; this theorem reconnects that construction to the simpler noising formula.

theorem NN.Proofs.Probability.isGaussian_forwardKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : ProbabilityTheory.IsGaussian ((forwardKernel a b) x)

Each transition distribution of the forward kernel is Gaussian.

theorem NN.Proofs.Probability.integral_id_forwardKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) : ∫ (y : E), y ∂(forwardKernel a b) x = a • x

The transition at x has mean a • x, read off the kernel rather than the measure.

theorem NN.Proofs.Probability.variance_dual_forwardKernel {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (a b : ℝ) (x : E) (L : StrongDual ℝ E) : ProbabilityTheory.variance (⇑L) ((forwardKernel a b) x) = b ^ 2 * ‖L‖ ^ 2

The transition at x is isotropic with noise scale b, read off the kernel.