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

@[instance_reducible]

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

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

def Runtime.Autograd.Model.F.Fourier.rfft1dReference {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (x : RefTy m α [batch, n]) : m (RefTy m α [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.irfft1dReference {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (x : RefTy m α [batch, n / 2 + 1, 2]) : m (RefTy m α [batch, n])

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

def Runtime.Autograd.Model.F.rfft1d {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (_hn : 0 < n) (x : RefTy m α [batch, n]) : m (RefTy m α [batch, n / 2 + 1, 2])

Unnormalized real Fourier transform of each row, returned as [batch, n / 2 + 1, 2].

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.irfft1d {α : Type} [TorchLean.Storage α] [Context α] {m : Type → Type} [Monad m] [Ops m α] {batch n : ℕ} (_hn : 0 < n) (x : RefTy m α [batch, n / 2 + 1, 2]) : m (RefTy m α [batch, n])

Normalized inverse real transform with output length n.

Interior bins are completed by conjugate symmetry. Imaginary DC and even-length Nyquist inputs are ignored, and their derivatives are zero. Passing n explicitly distinguishes lengths such as four and five, which have the same number of stored bins.