Differentiable real Fourier transforms

These operations keep real and imaginary coordinates in a final axis of length two. Models can therefore use real FFTs without changing scalar type. Eager CUDA execution uses the native transform and its packed-real adjoint. Other interpreters multiply by the specification matrices, so their existing matrix JVP and VJP rules also cover these transforms and higher derivatives.

The portable implementation is a dense reference transform. The native implementation uses cuFFT; selecting the same mathematical operation does not imply the same floating-point order.

inductive Runtime.Autograd.Model.F.SpectralPath : Type

Choose Fourier execution without changing normalization or spectral parameters.

• automatic : SpectralPath

  Use native FFT hooks when supported, otherwise differentiable reference operations.

• denseReference : SpectralPath

  Always use dense reference transforms.

def Runtime.Autograd.Model.F.instBEqSpectralPath.beq : SpectralPath → SpectralPath → Bool

@[instance_reducible]

instance Runtime.Autograd.Model.F.instBEqSpectralPath : BEq SpectralPath

@[instance_reducible]

instance Runtime.Autograd.Model.F.instDecidableEqSpectralPath : DecidableEq SpectralPath

def Runtime.Autograd.Model.F.instReprSpectralPath.repr : SpectralPath → ℕ → Std.Format

@[instance_reducible]

instance Runtime.Autograd.Model.F.instReprSpectralPath : Repr SpectralPath

def Runtime.Autograd.Model.F.Fourier.rfft {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (x : Ref [batch, n]) : m (Ref [batch, n / 2 + 1, 2])

Dense real-linear reference transform, used when the interpreter has no native FFT hook.

def Runtime.Autograd.Model.F.Fourier.irfft {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (x : Ref [batch, n / 2 + 1, 2]) : m (Ref [batch, n])

Dense normalized inverse, with explicit length so odd and even inputs remain distinct.

def Runtime.Autograd.Model.F.rfft {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch : Spec.Shape} {n : ℕ} (_hn : 0 < n) (x : Ref (batch.concat [n])) (path : SpectralPath := SpectralPath.automatic) : m (Ref (batch.concat [n / 2 + 1, 2]))

Unnormalized real Fourier transform along the last axis, preserving all leading batch dimensions.

The last coordinate is (real, imaginary) and the phase convention is exp(-2*pi*i*k*t/n). The positive-length witness rules out an undefined transform; an empty batch is allowed. This operation records differentiable references, including on interpreters that use the dense fallback.

def Runtime.Autograd.Model.F.irfft {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch : Spec.Shape} {n : ℕ} (_hn : 0 < n) (x : Ref (batch.concat [n / 2 + 1, 2])) (path : SpectralPath := SpectralPath.automatic) : m (Ref (batch.concat [n]))

Normalized inverse real transform with output length n.

Interior bins are completed by conjugate symmetry. In exact real arithmetic, imaginary DC and even-length Nyquist coordinates contribute zero and have zero derivatives. The dense path still multiplies these coordinates by zero, so it does not suppress NaN or infinity. Passing n explicitly distinguishes lengths such as four and five, which store the same number of bins.