Packed real Fourier transforms

A real transform keeps frequencies 0 through n / 2. The final axis stores the real and imaginary components, so the scalar type stays real throughout a differentiable program. The forward transform has no normalization; the inverse divides by n. Its interior bins represent a conjugate pair and therefore contribute twice. DC and the even-length Nyquist bin contribute once, and their imaginary coordinates have no effect.

The matrices below specify the real linear maps used by the portable runtime. In particular, their ordinary real transposes are the adjoints for the packed Euclidean pairing. Taking an inverse transform alone is not the forward transform's adjoint.

def Spec.RealFFT.isEndpoint (n frequency : ℕ) : Bool

Whether a stored frequency is its own conjugate: DC, or Nyquist for an even length.

def Spec.RealFFT.multiplicity (n frequency : ℕ) : ℕ

Number of full-spectrum frequencies represented by a stored real-transform bin.

def Spec.RealFFT.forwardMatrix {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) : TorchLean.Tensor α [n, (n / 2 + 1) * 2]

Forward real-transform matrix, with interleaved real/imaginary columns.

Endpoint imaginary columns are exactly zero. Evaluating sin(pi * integer) instead would introduce a small, artificial derivative in coordinates that the real transform ignores.

def Spec.RealFFT.inverseMatrix {α : Type} [TorchLean.Storage α] [Context α] (n : ℕ) : TorchLean.Tensor α [(n / 2 + 1) * 2, n]

Normalized inverse matrix, including the conjugate-pair multiplicity of interior bins.