Image DDIM

The image API stores one cumulative coefficient per noisy state. Its index zero is the first noisy state, while VPSchedule reserves state zero for the clean sample. Reading the coefficient table directly preserves loaded schedules, including a zero coefficient; no division is needed to recover per-step beta values.

Image sampling also makes two numerical choices: floor the reconstruction denominator, then clip the reconstructed sample to [-1, 1]. These operations belong to this sampler's formula. The separate ddimStep specification retains its additive epsilon and unclipped reconstruction.

def Generative.Diffusion.VPSchedule.noisyAlphaBars {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (schedule : VPSchedule α T) : TorchLean.Tensor α [T]

The cumulative coefficients of the noisy states, excluding the initial clean coefficient.

@[simp]

theorem Generative.Diffusion.VPSchedule.getScalar_noisyAlphaBars {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (schedule : VPSchedule α T) (index : Fin T) : schedule.noisyAlphaBars.getScalar index = schedule.alphaBar index.succ

Entry index describes spec state index + 1.

def Generative.Diffusion.ImageDDIM.alphaBar {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (coefficients : TorchLean.Tensor α [T]) (state : Fin (T + 1)) : α

Read a noisy-state coefficient table using the spec's clean-state indexing.

State zero has coefficient one; state index + 1 reads table entry index. This also defines the sole coefficient of an empty schedule without trying to index its empty table.

@[simp]

theorem Generative.Diffusion.ImageDDIM.alphaBar_zero {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (coefficients : TorchLean.Tensor α [T]) : alphaBar coefficients 0 = 1

The clean state precedes every entry of the stored noisy-state table.

@[simp]

theorem Generative.Diffusion.ImageDDIM.alphaBar_succ {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (coefficients : TorchLean.Tensor α [T]) (index : Fin T) : alphaBar coefficients index.succ = coefficients.getScalar index

Noisy state index + 1 uses table entry index.

theorem Generative.Diffusion.ImageDDIM.alphaBar_noisyAlphaBars {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} (schedule : VPSchedule α T) (state : Fin (T + 1)) : alphaBar schedule.noisyAlphaBars state = schedule.alphaBar state

Dropping and restoring the clean coefficient preserves every VP schedule state.

def Generative.Diffusion.ImageDDIM.timeOfIndex {α : Type} [Context α] {T : ℕ} (index : Fin T) : α

Time conditioning used by the image API.

The first noisy state has time zero and the last has time one when there are at least two states. A single noisy state has time zero. The state index stays explicit, so this convention never requires recovering an integer index from a rounded scalar time.

def Generative.Diffusion.ImageDDIM.stepFromEps {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (denominatorFloor previousAlpha alpha : α) (sample epsilon : TorchLean.Tensor α s) : TorchLean.Tensor α s

One image DDIM update from an already evaluated epsilon prediction.

First reconstruct with 1 / max(sqrt(alphaBar), denominatorFloor), using the explicit comparison below to match the executable branch. Clamp that reconstruction to [-1, 1], then remix it with the same epsilon prediction at the previous coefficient. The caller chooses a positive floor; the image API uses 1e-12. Clipping does not recompute epsilon.

def Generative.Diffusion.ImageDDIM.step {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} {s : Spec.Shape} (denominatorFloor : α) (coefficients : TorchLean.Tensor α [T]) (predict : Fin T → TorchLean.Tensor α s → TorchLean.Tensor α s) (index : Fin T) (sample : TorchLean.Tensor α s) : TorchLean.Tensor α s

Evaluate epsilon once at the noisy-state index, then move to the preceding state.

def Generative.Diffusion.ImageDDIM.sample {α : Type} [TorchLean.Storage α] [Context α] {T : ℕ} {s : Spec.Shape} (denominatorFloor : α) (coefficients : TorchLean.Tensor α [T]) (predict : Fin T → TorchLean.Tensor α s → TorchLean.Tensor α s) (initial : TorchLean.Tensor α s) : TorchLean.Tensor α s

Reverse every noisy state, ending at the clean coefficient one.