Diffusion sampler theorems

This file collects the fully proved sampler facts that sit between TorchLean's executable diffusion specs and the stability/verification APIs used elsewhere in the library.

We separate sampler mechanics from measure-level claims. ELBO optimality, reverse-SDE/PF-ODE marginal equivalence, and consistency distillation require additional probability and regularity assumptions; the theorems here prove the sampler-side facts that downstream proofs and verifiers can reuse directly:

• schedule boundary values,
• zero-step sampler behavior, and
• the link between sampler adapters and DynamicalSystem transitions,
• L2 stability of explicit Euler probability-flow updates.

References:

• Ho, Jain, and Abbeel, "Denoising Diffusion Probabilistic Models", NeurIPS 2020.
• Song et al., "Score-Based Generative Modeling through Stochastic Differential Equations", ICLR 2021.
• Hairer, Nørsett, and Wanner, Solving Ordinary Differential Equations I, for the Euler stability estimate used below.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.alphaBar_zero {α : Type} [Context α] {T : ℕ} (sched : Generative.Diffusion.VPSchedule α T) : sched.alphaBar ⟨0, ⋯⟩ = 1

The VP schedule convention is ᾱ₀ = 1.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.ddpmSample_zero_steps {α : Type} [Context α] {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule α 0) (model : Generative.Diffusion.EpsModel α s) (x_T : Spec.Tensor α s) (noise : Fin 0 → Spec.Tensor α s) : Generative.Diffusion.ddpmSample sched model x_T noise = x_T

With no reverse steps, DDPM returns its initial terminal-noise state.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.ddimSample_zero_steps {α : Type} [Context α] {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule α 0) (model : Generative.Diffusion.EpsModel α s) (x_T : Spec.Tensor α s) : Generative.Diffusion.ddimSample sched model x_T = x_T

With no reverse steps, deterministic DDIM returns its initial terminal-noise state.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.pfOdeSampleEuler_zero_steps {α : Type} [Context α] {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule α) (model : Generative.Diffusion.EpsModel α s) (x1 : Spec.Tensor α s) : Generative.Diffusion.pfOdeSampleEuler sch model 0 x1 = x1

With zero Euler steps, the probability-flow sampler returns the initial state.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.ddimStepSystem_eq_step {T : ℕ} {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule Spec.SpecScalar T) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (k : Fin T) (x : Spec.SpecTensor s) : (Generative.Diffusion.ddimStepSystem sched model k).step x = Generative.Diffusion.ddimStep sched model k x

The DDIM system adapter is definitionally the corresponding DDIM step.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.pfOdeEulerSystem_eq_step {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule Spec.SpecScalar) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (t dt : Spec.SpecScalar) (x : Spec.SpecTensor s) : (Generative.Diffusion.pfOdeEulerSystem sch model t dt).step x = Generative.Diffusion.eulerStep (Generative.Diffusion.pfOdeRhs sch model) x t dt

The probability-flow Euler system adapter is definitionally the Euler update.

Quantitative Euler stability for probability-flow samplers

theorem NN.MLTheory.Generative.Diffusion.eulerStep_l2_distance_bound {s : Spec.Shape} (f : Spec.Tensor ℝ s → ℝ → Spec.Tensor ℝ s) (t dt : ℝ) (x y : Spec.Tensor ℝ s) : Robustness.Spec.tensorDistance (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (Generative.Diffusion.eulerStep f x t dt) (Generative.Diffusion.eulerStep f y t dt) ≤ Robustness.Spec.tensorDistance (fun {s : Spec.Shape} => Proofs.tensorL2Norm) x y + |dt| * Robustness.Spec.tensorDistance (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (f x t) (f y t)

One explicit Euler step is stable in L2 up to the current state separation plus the RHS separation.

For an ODE x' = f(x,t), the Euler update is E(x)=x+dt f(x,t). This theorem proves the standard numerical-analysis estimate

‖E(x)-E(y)‖₂ ≤ ‖x-y‖₂ + |dt| ‖f(x,t)-f(y,t)‖₂.

This proof uses TorchLean's real tensor norm library: the algebraic Euler-difference identity above, the L2 triangle inequality, and L2 homogeneity of scalar multiplication. It is the bridge from the executable PF-ODE sampler to quantitative stability/verification arguments.

Reference: this is the elementary one-step stability estimate underlying explicit Euler analyses; see Hairer, Nørsett, and Wanner, Solving Ordinary Differential Equations I.

theorem NN.MLTheory.Generative.Diffusion.eulerStep_l2_lipschitz_of_rhs_lipschitz {s : Spec.Shape} (f : Spec.Tensor ℝ s → ℝ → Spec.Tensor ℝ s) (t dt L : ℝ) (h : Robustness.Spec.isLipschitzContinuous (fun (x : Spec.Tensor ℝ s) => f x t) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L) : Robustness.Spec.isLipschitzContinuous (fun (x : Spec.Tensor ℝ s) => Generative.Diffusion.eulerStep f x t dt) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (1 + |dt| * L)

If the ODE right-hand side is L-Lipschitz in L2 at a fixed time, then one Euler step is (1 + |dt| L)-Lipschitz in L2.

This is a quantitative sampler theorem: once we prove or import a Lipschitz bound for the neural vector field, this theorem converts it into a certified bound for the actual update used by the sampler.

theorem NN.MLTheory.Generative.Diffusion.pfOdeEulerSystem_l2_lipschitz_of_rhs_lipschitz {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule ℝ) (model : Generative.Diffusion.EpsModel ℝ s) (t dt L : ℝ) (h : Robustness.Spec.isLipschitzContinuous (fun (x : Spec.Tensor ℝ s) => Generative.Diffusion.pfOdeRhs sch model x t) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L) : Robustness.Spec.isLipschitzContinuous (Generative.Diffusion.pfOdeEulerSystem sch model t dt).step (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (1 + |dt| * L)

Probability-flow Euler systems inherit the concrete L2 Euler-step Lipschitz bound.

For the PF-ODE vector field pfOdeRhs sch model, any certified L-Lipschitz bound on the RHS at time t yields a (1 + |dt| L) Lipschitz bound on the DynamicalSystem.step used by TorchLean trajectories. This is the theorem downstream PF-ODE certificates should target first.

Lipschitz and contraction transport through sampler adapters

theorem NN.MLTheory.Generative.Diffusion.ddimStepSystem_lipschitz_of_step_lipschitz {T : ℕ} {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule Spec.SpecScalar T) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (k : Fin T) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (L : Spec.SpecScalar) (h : Robustness.Spec.isLipschitzContinuous (fun (x : Spec.SpecTensor s) => Generative.Diffusion.ddimStep sched model k x) (fun {s : Spec.Shape} => norm) (fun {s : Spec.Shape} => norm) L) : Robustness.Spec.isLipschitzContinuous (Generative.Diffusion.ddimStepSystem sched model k).step (fun {s : Spec.Shape} => norm) (fun {s : Spec.Shape} => norm) L

If the underlying DDIM update is L-Lipschitz, then the DynamicalSystem wrapper around that update is also L-Lipschitz.

This is the compositional bridge we want at the API boundary: once a concrete DDIM step bound is available, the same bound is immediately available through the common dynamics API used elsewhere in TorchLean.

theorem NN.MLTheory.Generative.Diffusion.pfOdeEulerSystem_lipschitz_of_step_lipschitz {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule Spec.SpecScalar) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (t dt : Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (L : Spec.SpecScalar) (h : Robustness.Spec.isLipschitzContinuous (fun (x : Spec.SpecTensor s) => Generative.Diffusion.eulerStep (Generative.Diffusion.pfOdeRhs sch model) x t dt) (fun {s : Spec.Shape} => norm) (fun {s : Spec.Shape} => norm) L) : Robustness.Spec.isLipschitzContinuous (Generative.Diffusion.pfOdeEulerSystem sch model t dt).step (fun {s : Spec.Shape} => norm) (fun {s : Spec.Shape} => norm) L

If the underlying probability-flow Euler update is L-Lipschitz, then its DynamicalSystem adapter is L-Lipschitz.

For quantitative PF-ODE certification, this is the bridge from an ODE-step bound (for example via IBP/CROWN on the vector field) to the reusable trajectory and iterate definitions in NN.Spec.Dynamics.System.

theorem NN.MLTheory.Generative.Diffusion.ddimStepSystem_contracts_of_step_contracts {T : ℕ} {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule Spec.SpecScalar T) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (k : Fin T) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (factor : Spec.SpecScalar) (h : Robustness.Spec.isContractive (fun (x : Spec.SpecTensor s) => Generative.Diffusion.ddimStep sched model k x) (fun {s : Spec.Shape} => norm) factor) : Spec.Dynamics.isContractive (Generative.Diffusion.ddimStepSystem sched model k) (fun {s : Spec.Shape} => norm) factor

A contractive DDIM update remains contractive after packaging it as a DynamicalSystem.

This is the formal hook for fixed-point and stability arguments about deterministic diffusion samplers: once a concrete DDIM step bound is proved, the dynamics-level contraction predicate follows without re-opening the sampler definition.

theorem NN.MLTheory.Generative.Diffusion.pfOdeEulerSystem_contracts_of_step_contracts {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule Spec.SpecScalar) (model : Generative.Diffusion.EpsModel Spec.SpecScalar s) (t dt : Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (factor : Spec.SpecScalar) (h : Robustness.Spec.isContractive (fun (x : Spec.SpecTensor s) => Generative.Diffusion.eulerStep (Generative.Diffusion.pfOdeRhs sch model) x t dt) (fun {s : Spec.Shape} => norm) factor) : Spec.Dynamics.isContractive (Generative.Diffusion.pfOdeEulerSystem sch model t dt) (fun {s : Spec.Shape} => norm) factor

A contractive PF-ODE Euler update remains contractive after packaging it as a DynamicalSystem.

This keeps the verification-facing statement compositional: prove the Euler map contracts under the chosen norm, then reuse the dynamics API for iterated sampler trajectories.