Exact Fourier circuits: cleared circuit

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

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

noncomputable def Complexity.ExactFourier.Cascade.clearedDAG {α β : Type} [Fintype α] [Fintype β] (b : ℂ) (L : Matrix α α ℂ) (T : Matrix α β ℂ) (k : ℕ) : TypedDAG (States α β k) (TensorAxis.Space α k)

A scalar circuit realizing the recursively cleared cascade response.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Cascade.clearedDAG b L T 0 = Complexity.ExactFourier.TypedDAG.wires fun (x : Complexity.ExactFourier.TensorAxis.Space α 0) => none

theorem Complexity.ExactFourier.Cascade.eval_clearedDAG {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] (b : ℂ) (L : Matrix α α ℂ) (T : Matrix α β ℂ) (k : ℕ) (x : States α β k → ℂ) : (clearedDAG b L T k).eval x = (cleared b L T k).mulVec x

theorem Complexity.ExactFourier.Cascade.size_clearedDAG {α β : Type} [Fintype α] [Fintype β] (b : ℂ) (L : Matrix α α ℂ) (T : Matrix α β ℂ) (k : ℕ) : (clearedDAG b L T k).size ≤ 2 * (Fintype.card β + Fintype.card α + 1) * k ^ 2 * Fintype.card α ^ k

theorem Complexity.ExactFourier.Cascade.exists_cleared_coeff_dag {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] (b : Polynomial ℂ) (L : Matrix α α (Polynomial ℂ)) (T : Matrix α β (Polynomial ℂ)) : ∃ (A : ℕ), ∀ (k t : ℕ), ∃ (C : TypedDAG (States α β k) (Fin t × TensorAxis.Space α k)), C.size ≤ A * (k + 1) ^ 3 * Fintype.card α ^ k ∧ ∀ (x : States α β k → ℂ), C.eval x = (PolynomialDAG.coefficients (cleared b L T k) t).mulVec x

theorem Complexity.ExactFourier.TypedDAG.circuit_eval_of_matrix {ι κ : Type} [Fintype ι] [Fintype κ] (C : TypedDAG ι κ) (A : Matrix κ ι ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) (x : Fin (Fintype.card ι) → ℂ) : C.circuit.eval x = ((Matrix.reindex (Fintype.equivFin κ) (Fintype.equivFin ι)) A).mulVec x

theorem Complexity.ExactFourier.TypedDAG.shear_price {ι κ : Type} [Fintype ι] [Fintype κ] (p : MatrixPrice) [DecidableEq ι] [DecidableEq κ] (C : TypedDAG ι κ) (A : Matrix κ ι ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) : p.value (rectangularShear A) ≤ 8 * ↑C.size + 2 * ↑(Fintype.card κ)

theorem Complexity.ExactFourier.MatrixPrice.eliminate_top_right (p : MatrixPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A P : Matrix α α ℂ) (E Q : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hK : IsUnit (Matrix.fromBlocks A E B D)) (hA : IsUnit A) (hP : IsUnit P) (hQ : A * P * Q = E) : p.value A ≤ p.value (Matrix.fromBlocks A E B D) + 2 * p.value P + p.value (rectangularShear Q)

def Complexity.ExactFourier.RadixTwo.evenIndex (n : ℕ) (i : Fin n) : Fin (n + n)

Embed an index into the even positions of a vector of twice the length.

Equations

• Complexity.ExactFourier.RadixTwo.evenIndex n i = ⟨2 * ↑i, ⋯⟩

def Complexity.ExactFourier.RadixTwo.oddIndex (n : ℕ) (i : Fin n) : Fin (n + n)

Embed an index into the odd positions of a vector of twice the length.

Equations

• Complexity.ExactFourier.RadixTwo.oddIndex n i = ⟨2 * ↑i + 1, ⋯⟩

def Complexity.ExactFourier.RadixTwo.parityEquiv (n : ℕ) : Fin n × Fin 2 ≃ Fin (n + n)

Identify an index with its quotient by two and its parity.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.ExactFourier.RadixTwo.sum_even_odd {R : Type u_1} [AddCommMonoid R] (n : ℕ) (f : Fin (n + n) → R) : ∑ i : Fin (n + n), f i = ∑ i : Fin n, f (evenIndex n i) + ∑ i : Fin n, f (oddIndex n i)

noncomputable def Complexity.ExactFourier.RadixTwo.evalAt (n : ℕ) (ω : ℂ) (x : Fin n → ℂ) (r : ℕ) : ℂ

Evaluate the coefficient vector at the specified power of ω.

Equations

• Complexity.ExactFourier.RadixTwo.evalAt n ω x r = ∑ j : Fin n, ω ^ (r * ↑j) * x j

noncomputable def Complexity.ExactFourier.RadixTwo.eval (n : ℕ) (ω : ℂ) (x : Fin n → ℂ) : Fin n → ℂ

Evaluate at the first n powers of ω, yielding a Fourier-type transform.

Equations

• Complexity.ExactFourier.RadixTwo.eval n ω x i = Complexity.ExactFourier.RadixTwo.evalAt n ω x ↑i

theorem Complexity.ExactFourier.RadixTwo.power_even (ω : ℂ) (r j : ℕ) : ω ^ (r * (2 * j)) = (ω ^ 2) ^ (r * j)

theorem Complexity.ExactFourier.RadixTwo.power_odd (ω : ℂ) (r j : ℕ) : ω ^ (r * (2 * j + 1)) = ω ^ r * (ω ^ 2) ^ (r * j)

theorem Complexity.ExactFourier.RadixTwo.evalAt_split (n : ℕ) (ω : ℂ) (x : Fin (n + n) → ℂ) (r : ℕ) : evalAt (n + n) ω x r = evalAt n (ω ^ 2) (x ∘ evenIndex n) r + ω ^ r * evalAt n (ω ^ 2) (x ∘ oddIndex n) r

theorem Complexity.ExactFourier.RadixTwo.evalAt_periodic (n : ℕ) (ω : ℂ) (hω : ω ^ n = 1) (x : Fin n → ℂ) (r : ℕ) : evalAt n ω x (r + n) = evalAt n ω x r

theorem Complexity.ExactFourier.RadixTwo.square_period {n : ℕ} (ω : ℂ) (hω : ω ^ n = -1) : (ω ^ 2) ^ n = 1

theorem Complexity.ExactFourier.RadixTwo.eval_split (n : ℕ) (ω : ℂ) (hω : ω ^ n = -1) (x : Fin (n + n) → ℂ) : eval (n + n) ω x = fun (i : Fin (n + n)) => Fin.addCases (fun (i : Fin n) => eval n (ω ^ 2) (x ∘ evenIndex n) i + ω ^ ↑i * eval n (ω ^ 2) (x ∘ oddIndex n) i) (fun (i : Fin n) => eval n (ω ^ 2) (x ∘ evenIndex n) i - ω ^ ↑i * eval n (ω ^ 2) (x ∘ oddIndex n) i) i

First and second frequency halves are the sum and difference butterfly.

theorem Complexity.ExactFourier.RadixTwo.orthogonality {n : ℕ} (hn : 0 < n) (ω : ℂ) (hω : IsPrimitiveRoot ω n) (i k : Fin n) : ∑ j : Fin n, ω⁻¹ ^ (↑i * ↑j) * ω ^ (↑k * ↑j) = if i = k then ↑n else 0

Orthogonality of the exact n-th root evaluation matrix.

theorem Complexity.ExactFourier.RadixTwo.eval_inverse {n : ℕ} (hn : 0 < n) (ω : ℂ) (hω : IsPrimitiveRoot ω n) (x : Fin n → ℂ) : eval n ω⁻¹ (eval n ω x) = fun (i : Fin n) => ↑n * x i

The inverse FFT uses the inverse root and one scalar normalization.

theorem Complexity.ExactFourier.RadixTwo.eval_ofFn (n : ℕ) (ω : ℂ) (x : Fin n → ℂ) (i : Fin n) : Polynomial.eval (ω ^ ↑i) ((Polynomial.ofFn n) x) = eval n ω x i

Polynomial evaluation of the vector of coefficients is exactly the DFT.

theorem Complexity.ExactFourier.RadixTwo.convolution_formula {n : ℕ} (hn : 0 < n) (ω : ℂ) (hω : IsPrimitiveRoot ω n) (f g : Polynomial ℂ) (hfg : (f * g).natDegree < n) : (eval n ω⁻¹ fun (i : Fin n) => (↑n)⁻¹ * Polynomial.eval (ω ^ ↑i) f * Polynomial.eval (ω ^ ↑i) g) = fun (i : Fin n) => (f * g).coeff ↑i

Transform, multiply by precomputed scalar evaluations, inverse transform. The only degree condition is that the product is represented by fewer than n coefficients, so there is no wraparound.