Exact Fourier circuits: fftcircuit

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/FFTCircuit.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.ExactFourier.RadixTwo.exists_fft_dag (k : ℕ) (ω : ℂ) (hω : IsPrimitiveRoot ω (2 ^ k)) : ∃ (C : LinearDAG (2 ^ k) (2 ^ k)), C.size ≤ 3 * k * 2 ^ k ∧ ∀ (x : Fin (2 ^ k) → ℂ), C.eval x = eval (2 ^ k) ω x

def Complexity.ExactFourier.ScalarConvolution.padIndex (t m : ℕ) (i : Fin m) : Fin (t + 1)

Select an input index when present and otherwise select the free zero wire.

Equations

• Complexity.ExactFourier.ScalarConvolution.padIndex t m i = if h : ↑i < t then ⟨↑i, h⟩.castSucc else Fin.last t

def Complexity.ExactFourier.ScalarConvolution.padded {t m : ℕ} (x : Fin t → ℂ) (i : Fin m) : ℂ

Extend or truncate an input vector to the requested length using zeros.

Equations

• Complexity.ExactFourier.ScalarConvolution.padded x i = if h : ↑i < t then x ⟨↑i, h⟩ else 0

theorem Complexity.ExactFourier.ScalarConvolution.eval_padding (t m : ℕ) (x : Fin t → ℂ) : (LinearDAG.wires (padIndex t m)).eval x = padded x

theorem Complexity.ExactFourier.ScalarConvolution.ofFn_padded {t m : ℕ} (htm : t ≤ m) (x : Fin t → ℂ) : (Polynomial.ofFn m) (padded x) = (Polynomial.ofFn t) x

def Complexity.ExactFourier.ScalarConvolution.diagonalDAG {m : ℕ} (c : Fin m → ℂ) : LinearDAG m m

A fixed diagonal layer charges exactly one multiplication per coordinate.

Equations

• Complexity.ExactFourier.ScalarConvolution.diagonalDAG c = Complexity.ExactFourier.LinearDAG.layer fun (i : Fin m) => Complexity.ExactFourier.Gate.scale (c i) i.castSucc

theorem Complexity.ExactFourier.ScalarConvolution.diagonalDAG_eval {m : ℕ} (c x : Fin m → ℂ) : (diagonalDAG c).eval x = fun (i : Fin m) => c i * x i

theorem Complexity.ExactFourier.ScalarConvolution.convolution_dag_at_power (k t : ℕ) (ht : 0 < t) (htm : 2 * t ≤ 2 ^ k) (f : Polynomial ℂ) (hf : f.natDegree < t) : ∃ (C : LinearDAG t t), C.size ≤ (6 * k + 1) * 2 ^ k ∧ ∀ (x : Fin t → ℂ) (i : Fin t), C.eval x i = (f * (Polynomial.ofFn t) x).coeff ↑i

Polynomial convolution on any containing radix-two length.

theorem Complexity.ExactFourier.ScalarConvolution.exists_truncation_dag (t : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) : ∃ (C : LinearDAG t t), C.size ≤ 52 * t * (Nat.log 2 t + 1) ∧ ∀ (x : Fin t → ℂ), C.eval x = (CoefficientTime.truncMatrix t f).mulVec x

Uniform linear-DAG construction, with logarithmic cost independent of coefficients.

theorem Complexity.ExactFourier.ScalarConvolution.truncMatrix_inv (t : ℕ) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : (CoefficientTime.truncMatrix t f)⁻¹ = CoefficientTime.truncMatrix t f⁻¹

Inversion commutes exactly with truncated scalar multiplication.

theorem Complexity.ExactFourier.ScalarConvolution.price_truncation_nat (p : MatrixPrice) (t : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : p.value (CoefficientTime.truncMatrix t f) ≤ 627 * ↑t * (↑(Nat.log 2 t) + 1)

theorem Complexity.ExactFourier.ScalarConvolution.price_truncation (p : MatrixPrice) (t : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : p.value (CoefficientTime.truncMatrix t f) ≤ 627 / Real.log 2 * ↑t * Real.log (2 * ↑t)

The literal O(t log(2t)) estimate, with one absolute constant, uniform in f and t.

theorem Complexity.ExactFourier.CoefficientTime.blockTrunc_smul_one {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (q : PowerSeries ℂ) : (blockTruncHom t) (q • 1) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (truncMatrix t q) 1

theorem Complexity.ExactFourier.CoefficientTime.scalar_correction {α β : Type} [Fintype α] [DecidableEq α] (H : Matrix α α (PowerSeries ℂ)) (E Q : Matrix α β (PowerSeries ℂ)) (q : PowerSeries ℂ) (hq : PowerSeries.constantCoeff q ≠ 0) (hQ : H * Q = q • E) (t : ℕ) : (blockTruncHom t) H * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (truncMatrix t q⁻¹) 1 * coefficientColumns t Q = coefficientColumns t E

theorem Complexity.ExactFourier.MatrixPrice.eliminate_series (p : MatrixPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (H : Matrix α α (PowerSeries ℂ)) (E Q : Matrix α β (PowerSeries ℂ)) (q : PowerSeries ℂ) (t : ℕ) (K : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) (hK : IsUnit K) (hH : IsUnit (H.map ⇑PowerSeries.constantCoeff)) (hdata : K.toBlocks₁₁ = (CoefficientTime.blockTruncHom t) H) (hstate : K.toBlocks₁₂ = CoefficientTime.coefficientColumns t E) (hq : PowerSeries.constantCoeff q ≠ 0) (hQ : H * Q = q • E) : p.value ((CoefficientTime.blockTruncHom t) H) ≤ p.value K + 2 * ↑(Fintype.card α) * p.value (CoefficientTime.truncMatrix t q⁻¹) + p.value (rectangularShear (CoefficientTime.coefficientColumns t Q))

theorem Complexity.ExactFourier.Cascade.q_constant {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (k : ℕ) : PowerSeries.constantCoeff (CellPoly.ps (CellPoly.b M C B D ^ k)) ≠ 0

theorem Complexity.ExactFourier.Cascade.coefficients_eq_columns {σ ρ : Type} (Q : Matrix σ ρ (Polynomial ℂ)) (t : ℕ) : PolynomialDAG.coefficients Q t = CoefficientTime.coefficientColumns t (Q.map ⇑CellPoly.ps)

theorem Complexity.ExactFourier.Cascade.uniform_bound {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (hK : IsUnit (Matrix.fromBlocks M C B D)) : ∃ (CK : ℝ), 0 ≤ CK ∧ ∀ (k t : ℕ), 0 < t → p.value ((CoefficientTime.blockTruncHom t) (TensorAxis.power (CellSeries.transfer M C B D) k)) ≤ ↑t * ↑(Fintype.card (TensorAxis.Fibers α k)) * p.value (Matrix.fromBlocks M C B D) + CK * (↑(Fintype.card α) ^ k * ↑t * Real.log (2 * ↑t) + (↑k + 1) ^ 3 * ↑(Fintype.card α) ^ k)