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 floors the reconstruction denominator, then applies a shape-preserving postprocessor. The default clips the reconstructed sample to [-1, 1]. 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) (postprocess : TorchLean.Tensor α s → TorchLean.Tensor α s := fun (reconstruction : TorchLean.Tensor α s) => reconstruction.clampSpec (-1) 1) : TorchLean.Tensor α s

One image DDIM update from an already evaluated epsilon prediction.

First reconstruct with the explicitly branched denominator below, then apply postprocess before remixing with the same epsilon prediction at the previous coefficient. The default postprocessor clamps to [-1, 1]; it never recomputes epsilon. The image API defaults to the floor 1e-12. The formula itself makes no positivity or finiteness assumption on the floor.

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) (postprocess : TorchLean.Tensor α s → TorchLean.Tensor α s := fun (reconstruction : TorchLean.Tensor α s) => reconstruction.clampSpec (-1) 1) : 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) (postprocess : TorchLean.Tensor α s → TorchLean.Tensor α s := fun (reconstruction : TorchLean.Tensor α s) => reconstruction.clampSpec (-1) 1) : TorchLean.Tensor α s

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