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} [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (k : Fin T) (x_t : Spec.Tensor α s) : Spec.Tensor α s

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

We reuse the same x0Pred reconstruction as DDPM and then recompose $x_{t-1}$ using the forward-process coefficients at time $t-1$:

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

def Generative.Diffusion.ddimSample {α : Type} [Context α] {T : ℕ} {s : Spec.Shape} (sched : VPSchedule α T) (model : EpsModel α s) (x_T : Spec.Tensor α s) : Spec.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) : NN.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