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 σ-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).

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.

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.