Reverse DDIM sampler (spec layer)

DDIM (Denoising Diffusion Implicit Models) can be viewed as a deterministic sampler that reuses the same denoiser $\varepsilon_\theta(x,t)$ but removes per-step noise.

This file provides the $\eta=0$ variant (fully deterministic), which is often used as a simple "flow-like" sampler derived from the same diffusion model.

Reference (informal pointer):

• Song, Meng, Ermon (2021), "Denoising Diffusion Implicit Models" (DDIM).

def Generative.Diffusion.ddimStep {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (k : Fin T) (x_t : TorchLean.Tensor α s) : TorchLean.Tensor α s

One deterministic DDIM step $x_t\to x_{t-1}$ ($\eta=0$).

Evaluate the denoiser once, reconstruct $x_0$ with x0PredFromEps, and reuse that prediction in the direction term. The coefficients are those of the forward process at time $t-1$:

$$ x_{t-1}=\sqrt{\bar\alpha_{t-1}}\,\widehat{x}_0 +\sqrt{1-\bar\alpha_{t-1}}\,\hat\varepsilon. $$

theorem Generative.Diffusion.ddimStep_eq_x0Pred {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (k : Fin T) (x_t : TorchLean.Tensor α s) : ddimStep sched model k x_t = (x0Pred sched model x_t k.succ).scaleSpec (sqrtNonneg (sched.alphaBar k.castSucc)) + (model.eps x_t (VPSchedule.timeOfIndex k.succ)).scaleSpec (sqrtNonneg (1 - sched.alphaBar k.castSucc))

Sharing the denoiser output preserves the reconstruction-and-direction formula.

This equality uses the same tensor operations in the same order, so it holds for every scalar context, including floating-point contexts. It does not require field identities or a claim about the compiler's treatment of repeated pure function calls.

def Generative.Diffusion.ddimSample {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (x_T : TorchLean.Tensor α s) : TorchLean.Tensor α s

Run the full deterministic DDIM sampler for $T$ steps ($\eta=0$).

noncomputable def Generative.Diffusion.ddimStepSystem {T : ℕ} {s : Spec.Shape} (sched : VPSchedule Spec.SpecScalar T) (model : EpsModel Spec.SpecScalar s) (k : Fin T) : Spec.Dynamics.DynamicalSystem s

Real-valued DDIM transition as a DynamicalSystem.

DynamicalSystem is fixed to SpecScalar = ℝ, so this adapter gives DDIM samplers the same trajectory/fixed-point API used by SSMs and other discrete systems.

@[simp]

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

The DDIM system steps by one ddimStep, so system-level lemmas transfer to the sampler.