Exact Fourier circuits: circuit extensions

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

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

theorem Complexity.ExactFourier.Program.eval_original {n k : ℕ} (p : Program n k) (x : Fin n → ℂ) (i : Fin (n + 1)) : p.eval x (Fin.castAdd k i) = Fin.snoc x 0 i

def Complexity.ExactFourier.LinearDAG.fanout {n a b : ℕ} (C : LinearDAG n a) (D : LinearDAG n b) : LinearDAG n (a + b)

Run two scalar circuits on a shared input and concatenate their outputs.

Equations

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

@[simp]

theorem Complexity.ExactFourier.LinearDAG.size_fanout {n a b : ℕ} (C : LinearDAG n a) (D : LinearDAG n b) : (C.fanout D).size = C.size + D.size

theorem Complexity.ExactFourier.LinearDAG.eval_fanout {n a b : ℕ} (C : LinearDAG n a) (D : LinearDAG n b) (x : Fin n → ℂ) : (C.fanout D).eval x = fun (i : Fin (a + b)) => Fin.addCases (C.eval x) (D.eval x) i

noncomputable def Complexity.ExactFourier.LinearDAG.withInputs {m n a : ℕ} (C : LinearDAG n a) (f : Fin n → Fin m) : LinearDAG m a

Select or duplicate arbitrary existing inputs; these are wire names, not gates.

Equations

• C.withInputs f = C.comp (Complexity.ExactFourier.LinearDAG.wires fun (i : Fin n) => (f i).castSucc)

@[simp]

theorem Complexity.ExactFourier.LinearDAG.size_withInputs {m n a : ℕ} (C : LinearDAG n a) (f : Fin n → Fin m) : (C.withInputs f).size = C.size

theorem Complexity.ExactFourier.LinearDAG.eval_withInputs {m n a : ℕ} (C : LinearDAG n a) (f : Fin n → Fin m) (x : Fin m → ℂ) : (C.withInputs f).eval x = C.eval (x ∘ f)

def Complexity.ExactFourier.LinearDAG.withOutputs {n a b : ℕ} (C : LinearDAG n a) (f : Fin b → Fin a) : LinearDAG n b

Change the ordered output list without performing an arithmetic operation.

Equations

• C.withOutputs f = { size := C.size, program := C.program, outputs := C.outputs ∘ f }

@[simp]

theorem Complexity.ExactFourier.LinearDAG.eval_withOutputs {n a b : ℕ} (C : LinearDAG n a) (f : Fin b → Fin a) (x : Fin n → ℂ) : (C.withOutputs f).eval x = C.eval x ∘ f

def Complexity.ExactFourier.LinearDAG.butterflies {n m : ℕ} (C : LinearDAG n (m + m)) (c : Fin m → ℂ) : LinearDAG n (m + m)

One butterfly for each of m pairs: charge m scalar multiplications, m additions, and m subtractions, retaining the scaled terms for both output signs.

Equations

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

theorem Complexity.ExactFourier.LinearDAG.eval_butterflies {n m : ℕ} (C : LinearDAG n (m + m)) (c : Fin m → ℂ) (x : Fin n → ℂ) : (C.butterflies c).eval x = fun (i : Fin (m + m)) => Fin.addCases (fun (i : Fin m) => C.eval x (Fin.castAdd m i) + c i * C.eval x (Fin.natAdd m i)) (fun (i : Fin m) => C.eval x (Fin.castAdd m i) - c i * C.eval x (Fin.natAdd m i)) i

structure Complexity.ExactFourier.TypedDAG (ι κ : Type) [Fintype ι] [Fintype κ] : Type

A scalar circuit whose finite input and output coordinates have named types.

• circuit : LinearDAG (Fintype.card ι) (Fintype.card κ)

  The underlying scalar circuit after enumerating the coordinate types.

@[reducible, inline]

abbrev Complexity.ExactFourier.TypedDAG.size {ι κ : Type} [Fintype ι] [Fintype κ] (C : TypedDAG ι κ) : ℕ

The number of charged scalar gates in the underlying circuit.

Equations

• C.size = C.circuit.size

noncomputable def Complexity.ExactFourier.TypedDAG.eval {ι κ : Type} [Fintype ι] [Fintype κ] (C : TypedDAG ι κ) (x : ι → ℂ) : κ → ℂ

Evaluate the underlying circuit and restore the named output coordinates.

Equations

• C.eval x j = C.circuit.eval (x ∘ ⇑(Fintype.equivFin ι).symm) ((Fintype.equivFin κ) j)

noncomputable def Complexity.ExactFourier.TypedDAG.comp {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (D : TypedDAG κ τ) (C : TypedDAG ι κ) : TypedDAG ι τ

Feed the outputs of C into D, retaining both circuits' gates.

Equations

• D.comp C = { circuit := D.circuit.comp C.circuit }

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_comp {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (D : TypedDAG κ τ) (C : TypedDAG ι κ) : (D.comp C).size = C.size + D.size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_comp {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (D : TypedDAG κ τ) (C : TypedDAG ι κ) (x : ι → ℂ) : (D.comp C).eval x = D.eval (C.eval x)

noncomputable def Complexity.ExactFourier.TypedDAG.inputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : ι → τ) : TypedDAG τ κ

Relabel or duplicate the input coordinates without adding gates.

Equations

• C.inputs f = { circuit := C.circuit.withInputs fun (i : Fin (Fintype.card ι)) => (Fintype.equivFin τ) (f ((Fintype.equivFin ι).symm i)) }

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_inputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : ι → τ) : (C.inputs f).size = C.size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_inputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : ι → τ) (x : τ → ℂ) : (C.inputs f).eval x = C.eval (x ∘ f)

noncomputable def Complexity.ExactFourier.TypedDAG.outputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : τ → κ) : TypedDAG ι τ

Select, reorder, or duplicate output coordinates without adding gates.

Equations

• C.outputs f = { circuit := C.circuit.withOutputs fun (i : Fin (Fintype.card τ)) => (Fintype.equivFin κ) (f ((Fintype.equivFin τ).symm i)) }

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_outputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : τ → κ) : (C.outputs f).size = C.size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_outputs {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (f : τ → κ) (x : ι → ℂ) : (C.outputs f).eval x = C.eval x ∘ f

noncomputable def Complexity.ExactFourier.TypedDAG.fanout {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG ι τ) : TypedDAG ι (κ ⊕ τ)

Run two typed circuits on a shared input and retain both output vectors.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_fanout {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG ι τ) : (C.fanout D).size = C.size + D.size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_fanout {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG ι τ) (x : ι → ℂ) : (C.fanout D).eval x = Sum.elim (C.eval x) (D.eval x)

noncomputable def Complexity.ExactFourier.TypedDAG.wires {ι κ : Type} [Fintype ι] [Fintype κ] (f : κ → Option ι) : TypedDAG ι κ

A gate-free selection of input wires and the source model's zero wire.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_wires {ι κ : Type} [Fintype ι] [Fintype κ] (f : κ → Option ι) : (wires f).size = 0

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_wires {ι κ : Type} [Fintype ι] [Fintype κ] (f : κ → Option ι) (x : ι → ℂ) : (wires f).eval x = fun (j : κ) => (f j).elim 0 x

noncomputable def Complexity.ExactFourier.TypedDAG.matrix {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι ℂ) : TypedDAG ι κ

Compute an arbitrary matrix by explicitly scaling and summing its entries.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_matrix {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι ℂ) : (matrix A).size = 2 * Fintype.card κ * Fintype.card ι

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_matrix {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι ℂ) (x : ι → ℂ) : (matrix A).eval x = A.mulVec x

noncomputable def Complexity.ExactFourier.TypedDAG.scale {κ : Type} [Fintype κ] (c : κ → ℂ) : TypedDAG κ κ

Multiply each coordinate by its specified scalar using one gate per coordinate.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_scale {κ : Type} [Fintype κ] (c : κ → ℂ) : (scale c).size = Fintype.card κ

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_scale {κ : Type} [Fintype κ] (c x : κ → ℂ) : (scale c).eval x = fun (i : κ) => c i * x i

noncomputable def Complexity.ExactFourier.TypedDAG.addPair {κ : Type} [Fintype κ] : TypedDAG (κ ⊕ κ) κ

Add two vectors coordinatewise using one addition gate per output.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_addPair {κ : Type} [Fintype κ] : addPair.size = Fintype.card κ

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_addPair {κ : Type} [Fintype κ] (x : κ ⊕ κ → ℂ) : addPair.eval x = fun (i : κ) => x (Sum.inl i) + x (Sum.inr i)

noncomputable def Complexity.ExactFourier.TypedDAG.stackFin {ι κ : Type} [Fintype ι] [Fintype κ] (n : ℕ) : (Fin n → TypedDAG ι κ) → TypedDAG ι (Fin n × κ)

Stack a finite list of circuits that share their input and output types.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.TypedDAG.stackFin 0 x_2 = Complexity.ExactFourier.TypedDAG.wires fun (x : Fin 0 × κ) => none

theorem Complexity.ExactFourier.TypedDAG.size_stackFin {ι κ : Type} [Fintype ι] [Fintype κ] (n : ℕ) (C : Fin n → TypedDAG ι κ) : (stackFin n C).size = ∑ i : Fin n, (C i).size

theorem Complexity.ExactFourier.TypedDAG.eval_stackFin {ι κ : Type} [Fintype ι] [Fintype κ] (n : ℕ) (C : Fin n → TypedDAG ι κ) (x : ι → ℂ) : (stackFin n C).eval x = fun (j : Fin n × κ) => (C j.1).eval x j.2

noncomputable def Complexity.ExactFourier.TypedDAG.stack {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : τ → TypedDAG ι κ) : TypedDAG ι (τ × κ)

Stack a finite family of circuits that share the same input.

Equations

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

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_stack {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : τ → TypedDAG ι κ) : (stack C).size = ∑ i : τ, (C i).size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_stack {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : τ → TypedDAG ι κ) (x : ι → ℂ) : (stack C).eval x = fun (j : τ × κ) => (C j.1).eval x j.2

noncomputable def Complexity.ExactFourier.TypedDAG.parallel {ι κ : Type} [Fintype ι] [Fintype κ] (C : TypedDAG ι κ) (τ : Type) [Fintype τ] : TypedDAG (τ × ι) (τ × κ)

Apply independent copies of a circuit to the indexed input vectors.

Equations

• C.parallel τ = Complexity.ExactFourier.TypedDAG.stack fun (t : τ) => C.inputs fun (i : ι) => (t, i)

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_parallel {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) : (C.parallel τ).size = Fintype.card τ * C.size

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_parallel {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (x : τ × ι → ℂ) : (C.parallel τ).eval x = fun (j : τ × κ) => C.eval (fun (i : ι) => x (j.1, i)) j.2

noncomputable def Complexity.ExactFourier.TypedDAG.tensor {ι κ τ υ : Type} [Fintype ι] [Fintype κ] [Fintype τ] [Fintype υ] (C : TypedDAG ι κ) (D : TypedDAG τ υ) : TypedDAG (ι × τ) (κ × υ)

Compute the tensor product of two linear circuits by acting on each coordinate axis.

Equations

• C.tensor D = (((C.parallel υ).inputs Prod.swap).comp (D.parallel ι)).outputs Prod.swap

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_tensor {ι κ τ υ : Type} [Fintype ι] [Fintype κ] [Fintype τ] [Fintype υ] (C : TypedDAG ι κ) (D : TypedDAG τ υ) : (C.tensor D).size = Fintype.card ι * D.size + Fintype.card υ * C.size

theorem Complexity.ExactFourier.TypedDAG.eval_tensor {ι κ τ υ : Type} [Fintype ι] [Fintype κ] [Fintype τ] [Fintype υ] (C : TypedDAG ι κ) (D : TypedDAG τ υ) (A : Matrix κ ι ℂ) (B : Matrix υ τ ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) (hD : ∀ (x : τ → ℂ), D.eval x = B.mulVec x) (x : ι × τ → ℂ) : (C.tensor D).eval x = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec x

noncomputable def Complexity.ExactFourier.TypedDAG.blockCols {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG τ κ) : TypedDAG (ι ⊕ τ) κ

Add the outputs of two circuits acting on disjoint input blocks.

Equations

• C.blockCols D = Complexity.ExactFourier.TypedDAG.addPair.comp ((C.inputs Sum.inl).fanout (D.inputs Sum.inr))

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_blockCols {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG τ κ) : (C.blockCols D).size = C.size + D.size + Fintype.card κ

theorem Complexity.ExactFourier.TypedDAG.eval_blockCols {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] (C : TypedDAG ι κ) (D : TypedDAG τ κ) (A : Matrix κ ι ℂ) (B : Matrix κ τ ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) (hD : ∀ (x : τ → ℂ), D.eval x = B.mulVec x) (x : ι ⊕ τ → ℂ) : (C.blockCols D).eval x = (A.fromCols B).mulVec x

noncomputable def Complexity.ExactFourier.TypedDAG.scalar {ι κ : Type} [Fintype ι] [Fintype κ] (c : ℂ) (C : TypedDAG ι κ) : TypedDAG ι κ

Scale every output of a circuit by one fixed complex scalar.

Equations

• Complexity.ExactFourier.TypedDAG.scalar c C = (Complexity.ExactFourier.TypedDAG.scale fun (x : κ) => c).comp C

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_scalar {ι κ : Type} [Fintype ι] [Fintype κ] (c : ℂ) (C : TypedDAG ι κ) : (scalar c C).size = C.size + Fintype.card κ

theorem Complexity.ExactFourier.TypedDAG.eval_scalar {ι κ : Type} [Fintype ι] [Fintype κ] (c : ℂ) (C : TypedDAG ι κ) (A : Matrix κ ι ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) (x : ι → ℂ) : (scalar c C).eval x = (c • A).mulVec x

noncomputable def Complexity.ExactFourier.TypedDAG.identity {ι : Type} [Fintype ι] : TypedDAG ι ι

The identity circuit, using only direct input wires.

Equations

• Complexity.ExactFourier.TypedDAG.identity = Complexity.ExactFourier.TypedDAG.wires some

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_identity {ι : Type} [Fintype ι] : identity.size = 0

@[simp]

theorem Complexity.ExactFourier.TypedDAG.eval_identity {ι : Type} [Fintype ι] (x : ι → ℂ) : identity.eval x = x

noncomputable def Complexity.ExactFourier.TypedDAG.tensorPower {α : Type} [Fintype α] (A : Matrix α α ℂ) (k : ℕ) : TypedDAG (TensorAxis.Space α k) (TensorAxis.Space α k)

A circuit for a tensor power, obtained by repeatedly tensoring matrix circuits.

Equations

• Complexity.ExactFourier.TypedDAG.tensorPower A 0 = Complexity.ExactFourier.TypedDAG.identity
• Complexity.ExactFourier.TypedDAG.tensorPower A k.succ = (Complexity.ExactFourier.TypedDAG.tensorPower A k).tensor (Complexity.ExactFourier.TypedDAG.matrix A)

theorem Complexity.ExactFourier.TypedDAG.eval_tensorPower {α : Type} [Fintype α] (A : Matrix α α ℂ) (k : ℕ) (x : TensorAxis.Space α k → ℂ) : (tensorPower A k).eval x = (TensorAxis.power A k).mulVec x

theorem Complexity.ExactFourier.TypedDAG.size_tensorPower {α : Type} [Fintype α] (A : Matrix α α ℂ) (k : ℕ) : (tensorPower A k).size = 2 * Fintype.card α * k * Fintype.card α ^ k

noncomputable def Complexity.ExactFourier.PolynomialDAG.nodes (m : ℕ) (i : Fin m) : ℂ

Distinct complex interpolation nodes given by the natural numbers below m.

Equations

• Complexity.ExactFourier.PolynomialDAG.nodes m i = ↑↑i

noncomputable def Complexity.ExactFourier.PolynomialDAG.weights (m : ℕ) : Matrix (Fin m) (Fin m) ℂ

Coefficients of the Lagrange basis at the chosen interpolation nodes.

Equations

• Complexity.ExactFourier.PolynomialDAG.weights m i j = (Lagrange.basis Finset.univ (Complexity.ExactFourier.PolynomialDAG.nodes m) j).coeff ↑i

theorem Complexity.ExactFourier.PolynomialDAG.nodes_injective (m : ℕ) : Function.Injective (nodes m)

theorem Complexity.ExactFourier.PolynomialDAG.coeff_interpolate (f : Polynomial ℂ) (m : ℕ) (hf : f.natDegree < m) (i : Fin m) : f.coeff ↑i = ∑ j : Fin m, weights m i j * Polynomial.eval (nodes m j) f

noncomputable def Complexity.ExactFourier.PolynomialDAG.coefficients {ι κ : Type} (A : Matrix κ ι (Polynomial ℂ)) (t : ℕ) : Matrix (Fin t × κ) ι ℂ

Stack the first t coefficient matrices as successive output blocks.

Equations

• Complexity.ExactFourier.PolynomialDAG.coefficients A t i j = (A i.2 j).coeff ↑i.1

noncomputable def Complexity.ExactFourier.PolynomialDAG.evalMatrix {ι κ : Type} (A : Matrix κ ι (Polynomial ℂ)) (z : ℂ) : Matrix κ ι ℂ

Evaluate each entry of a polynomial matrix at the same complex number.

Equations

• Complexity.ExactFourier.PolynomialDAG.evalMatrix A z = A.map ⇑(Polynomial.evalRingHom z)

noncomputable def Complexity.ExactFourier.PolynomialDAG.reconstruct {ι κ : Type} [Fintype ι] [Fintype κ] (m : ℕ) (C : Fin m → TypedDAG ι κ) : TypedDAG ι (Fin m × κ)

Recover coefficient outputs by interpolating circuits at the chosen nodes.

Equations

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

theorem Complexity.ExactFourier.PolynomialDAG.size_reconstruct {ι κ : Type} [Fintype ι] [Fintype κ] (m : ℕ) (C : Fin m → TypedDAG ι κ) : (reconstruct m C).size = ∑ i : Fin m, (C i).size + 2 * m * m * Fintype.card κ

theorem Complexity.ExactFourier.PolynomialDAG.eval_reconstruct {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι (Polynomial ℂ)) (m : ℕ) (hA : ∀ (i : κ) (j : ι), (A i j).natDegree < m) (C : Fin m → TypedDAG ι κ) (hC : ∀ (j : Fin m) (x : ι → ℂ), (C j).eval x = (evalMatrix A (nodes m j)).mulVec x) (x : ι → ℂ) : (reconstruct m C).eval x = (coefficients A m).mulVec x

noncomputable def Complexity.ExactFourier.PolynomialDAG.pad {κ : Type} [Fintype κ] (m t : ℕ) : TypedDAG (Fin m × κ) (Fin t × κ)

Extend coefficient vectors with zero wires, or truncate them to the requested length.

Equations

• Complexity.ExactFourier.PolynomialDAG.pad m t = Complexity.ExactFourier.TypedDAG.wires fun (i : Fin t × κ) => if h : ↑i.1 < m then some (⟨↑i.1, h⟩, i.2) else none

@[simp]

theorem Complexity.ExactFourier.PolynomialDAG.size_pad {κ : Type} [Fintype κ] (m t : ℕ) : (pad m t).size = 0

theorem Complexity.ExactFourier.PolynomialDAG.eval_pad {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι (Polynomial ℂ)) (m t : ℕ) (hA : ∀ (i : κ) (j : ι), (A i j).natDegree < m) (x : ι → ℂ) : (pad m t).eval ((coefficients A m).mulVec x) = (coefficients A t).mulVec x

theorem Complexity.ExactFourier.PolynomialDAG.exists_coefficients {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix κ ι (Polynomial ℂ)) (m t s : ℕ) (hA : ∀ (i : κ) (j : ι), (A i j).natDegree < m) (hC : ∀ (z : ℂ), ∃ (C : TypedDAG ι κ), C.size ≤ s ∧ ∀ (x : ι → ℂ), C.eval x = (evalMatrix A z).mulVec x) : ∃ (C : TypedDAG ι (Fin t × κ)), C.size ≤ m * s + 2 * m * m * Fintype.card κ ∧ ∀ (x : ι → ℂ), C.eval x = (coefficients A t).mulVec x