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
• L2 stability of explicit Euler probability-flow updates.

The link between the sampler adapters and DynamicalSystem transitions is proved next to the adapters themselves, in NN.Spec.Generative.Diffusion.ReverseDDIM and NN.Spec.Generative.Diffusion.PFODE, so those rfl facts stay with the definitions they unfold.

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} [TorchLean.Storage α] [Context α] {T : ℕ} (sched : Generative.Diffusion.VPSchedule α T) : sched.alphaBar ⟨0, ⋯⟩ = 1

The VP schedule convention is $\bar{\alpha}_0 = 1$.

@[simp]

theorem NN.MLTheory.Generative.Diffusion.ddpmSample_zero_steps {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule α 0) (model : Generative.Diffusion.EpsModel α s) (x_T : TorchLean.Tensor α s) (noise : Fin 0 → TorchLean.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} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (sched : Generative.Diffusion.VPSchedule α 0) (model : Generative.Diffusion.EpsModel α s) (x_T : TorchLean.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} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (sch : Generative.Diffusion.VPLinearSchedule α) (model : Generative.Diffusion.EpsModel α s) (x1 : TorchLean.Tensor α s) : Generative.Diffusion.pfOdeSampleEuler sch model 0 x1 = x1

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

Quantitative Euler stability for probability-flow samplers

theorem NN.MLTheory.Generative.Diffusion.eulerStep_l2_distance_bound {s : Spec.Shape} (f : TorchLean.Tensor ℝ s → ℝ → TorchLean.Tensor ℝ s) (t dt : ℝ) (x y : TorchLean.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+\Delta t\,f(x,t)$. This theorem proves the standard numerical-analysis estimate

$$ \lVert E(x)-E(y)\rVert_2 \leq \lVert x-y\rVert_2 + |\Delta t|\,\lVert f(x,t)-f(y,t)\rVert_2. $$

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 : TorchLean.Tensor ℝ s → ℝ → TorchLean.Tensor ℝ s) (t dt L : ℝ) (h : Robustness.Spec.isLipschitzContinuous (fun (x : TorchLean.Tensor ℝ s) => f x t) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) (fun {s : Spec.Shape} => Proofs.tensorL2Norm) L) : Robustness.Spec.isLipschitzContinuous (fun (x : TorchLean.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+|\Delta t|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 : TorchLean.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+|\Delta t|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 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.

Prove the Euler map contracts under the chosen norm, then reuse the dynamics API for iterated sampler trajectories.