Exact Fourier circuits: circuit cost

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

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

@[reducible, inline]

abbrev Complexity.ExactFourier.CircuitCost.Realizes {α β : Type} [Fintype α] [Fintype β] (C : TypedDAG α β) (M : Matrix β α ℂ) : Prop

The typed scalar circuit computes matrix multiplication on every input.

Equations

• Complexity.ExactFourier.CircuitCost.Realizes C M = ∀ (x : α → ℂ), C.eval x = M.mulVec x

theorem Complexity.ExactFourier.CircuitCost.exists_size {α β : Type} [Fintype α] [Fintype β] (M : Matrix β α ℂ) : ∃ (n : ℕ) (C : TypedDAG α β), C.size = n ∧ Realizes C M

noncomputable def Complexity.ExactFourier.CircuitCost.cost {α β : Type} [Fintype α] [Fintype β] (M : Matrix β α ℂ) : ℕ

The minimum number of scalar gates realizing the given matrix.

Equations

• Complexity.ExactFourier.CircuitCost.cost M = Nat.find ⋯

theorem Complexity.ExactFourier.CircuitCost.optimal {α β : Type} [Fintype α] [Fintype β] (M : Matrix β α ℂ) : ∃ (C : TypedDAG α β), C.size = cost M ∧ Realizes C M

theorem Complexity.ExactFourier.CircuitCost.cost_le {α β : Type} [Fintype α] [Fintype β] (M : Matrix β α ℂ) (C : TypedDAG α β) (hC : Realizes C M) : cost M ≤ C.size

theorem Complexity.ExactFourier.CircuitCost.cost_matrix {α β : Type} [Fintype α] [Fintype β] (M : Matrix β α ℂ) : cost M ≤ 2 * Fintype.card β * Fintype.card α

@[simp]

theorem Complexity.ExactFourier.CircuitCost.cost_one {α : Type} [Fintype α] [DecidableEq α] : cost 1 = 0

theorem Complexity.ExactFourier.CircuitCost.cost_mul {α : Type} [Fintype α] (M N : Matrix α α ℂ) : cost (M * N) ≤ cost M + cost N

theorem Complexity.ExactFourier.CircuitCost.cost_reindex_le {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (M : Matrix α α ℂ) : cost ((Matrix.reindex e e) M) ≤ cost M

theorem Complexity.ExactFourier.CircuitCost.cost_reindex {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (M : Matrix α α ℂ) : cost ((Matrix.reindex e e) M) = cost M

theorem Complexity.ExactFourier.CircuitCost.cost_monomial {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : MonomialMatrix M) : cost M ≤ Fintype.card α

theorem Complexity.ExactFourier.CircuitCost.cost_sum {α β : Type} [Fintype α] [Fintype β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) : cost (Matrix.fromBlocks M 0 0 N) ≤ cost M + cost N

theorem Complexity.ExactFourier.CircuitCost.cost_tensor {α β : Type} [Fintype α] [Fintype β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) : cost (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) ≤ Fintype.card β * cost M + Fintype.card α * cost N

def Complexity.ExactFourier.sigmaFinSucc {n : ℕ} (D : Fin (n + 1) → Type) : (i : Fin (n + 1)) × D i ≃ D 0 ⊕ (i : Fin n) × D i.succ

Separating the first output block, without inserting extra coordinates.

Equations

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

def Complexity.ExactFourier.TypedDAG.stackDepFin {α : Type} [Fintype α] (n : ℕ) (D : Fin n → Type) [inst : (i : Fin n) → Fintype (D i)] : ((i : Fin n) → TypedDAG α (D i)) → TypedDAG α ((i : Fin n) × D i)

Stack a finite list of circuits with potentially different output types.

Equations

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

theorem Complexity.ExactFourier.TypedDAG.size_stackDepFin {α : Type} [Fintype α] (n : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] (C : (i : Fin n) → TypedDAG α (D i)) : (stackDepFin n D C).size = ∑ i : Fin n, (C i).size

theorem Complexity.ExactFourier.TypedDAG.eval_stackDepFin {α : Type} [Fintype α] (n : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] (C : (i : Fin n) → TypedDAG α (D i)) (x : α → ℂ) : (stackDepFin n D C).eval x = fun (j : (i : Fin n) × D i) => (C j.fst).eval x j.snd

noncomputable def Complexity.ExactFourier.TypedDAG.stackDep {α : Type} [Fintype α] {σ : Type} [Fintype σ] (D : σ → Type) [(i : σ) → Fintype (D i)] (C : (i : σ) → TypedDAG α (D i)) : TypedDAG α ((i : σ) × D i)

Stack a dependently indexed family of circuits sharing the same input.

Equations

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

theorem Complexity.ExactFourier.TypedDAG.size_stackDep {α : Type} [Fintype α] {σ : Type} [Fintype σ] (D : σ → Type) [(i : σ) → Fintype (D i)] (C : (i : σ) → TypedDAG α (D i)) : (stackDep D C).size = ∑ i : σ, (C i).size

theorem Complexity.ExactFourier.TypedDAG.eval_stackDep {α : Type} [Fintype α] {σ : Type} [Fintype σ] (D : σ → Type) [(i : σ) → Fintype (D i)] (C : (i : σ) → TypedDAG α (D i)) (x : α → ℂ) : (stackDep D C).eval x = fun (j : (i : σ) × D i) => (C j.fst).eval x j.snd

theorem Complexity.ExactFourier.CircuitCost.cost_blocks {σ : Type} [Fintype σ] [DecidableEq σ] {D : σ → Type} [(i : σ) → Fintype (D i)] (M : (i : σ) → Matrix (D i) (D i) ℂ) : cost (Matrix.blockDiagonal' M) ≤ ∑ i : σ, cost (M i)

theorem Complexity.ExactFourier.Layered.blocks_fin (n : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] [(i : Fin n) → DecidableEq (D i)] (M : (i : Fin n) → Matrix (D i) (D i) ℂ) (d : ℕ) (hM : ∀ (i : Fin n), Layered (M i) d) : Layered (Matrix.blockDiagonal' M) d

theorem Complexity.ExactFourier.Layered.blocks {σ : Type} [Fintype σ] [DecidableEq σ] (D : σ → Type) [(i : σ) → Fintype (D i)] [(i : σ) → DecidableEq (D i)] (M : (i : σ) → Matrix (D i) (D i) ℂ) (d : ℕ) (hM : ∀ (i : σ), Layered (M i) d) : Layered (Matrix.blockDiagonal' M) d

theorem Complexity.ExactFourier.Layered.blockDiagonal {α σ : Type} [Fintype α] [Fintype σ] [DecidableEq α] [DecidableEq σ] (M : σ → Matrix α α ℂ) (d : ℕ) (hM : ∀ (i : σ), Layered (M i) d) : Layered (Matrix.blockDiagonal M) d

theorem Complexity.ExactFourier.Layered.transpose {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : Layered M.transpose d

theorem Complexity.ExactFourier.Layered.two_reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) (e f : α ≃ β) : Layered ((Matrix.reindex e f) M) (d + 1)

inductive Complexity.ExactFourier.Round {α : Type} [Fintype α] [DecidableEq α] : Matrix α α ℂ → Prop

A parallel layer generated by monomial matrices and invertible two-coordinate gates.

• mono {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (h : MonomialMatrix M) : Round M
• pair (M : Matrix (Fin 2) (Fin 2) ℂ) (h : IsUnit M) : Round M
• reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) {M : Matrix α α ℂ} (h : Round M) : Round ((Matrix.reindex e e) M)
• sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} (hM : Round M) (hN : Round N) : Round (Matrix.fromBlocks M 0 0 N)

theorem Complexity.ExactFourier.Round.one {α : Type} [Fintype α] [DecidableEq α] : Round 1

def Complexity.ExactFourier.Round.joint {α β : Type} (M : List (Matrix α α ℂ)) (N : List (Matrix β β ℂ)) : List (Matrix (α ⊕ β) (α ⊕ β) ℂ)

Pair corresponding rounds of two lists by taking their block direct sums.

Equations

• Complexity.ExactFourier.Round.joint M N = List.zipWith (fun (X : Matrix α α ℂ) (Y : Matrix β β ℂ) => Matrix.fromBlocks X 0 0 Y) M N

theorem Complexity.ExactFourier.Round.joint_length {α β : Type} (M : List (Matrix α α ℂ)) (N : List (Matrix β β ℂ)) (h : M.length = N.length) : (joint M N).length = M.length

theorem Complexity.ExactFourier.Round.joint_prod {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : List (Matrix α α ℂ)) (N : List (Matrix β β ℂ)) (h : M.length = N.length) : (joint M N).prod = Matrix.fromBlocks M.prod 0 0 N.prod

theorem Complexity.ExactFourier.Round.joint_all {α β : Type} (M : List (Matrix α α ℂ)) (N : List (Matrix β β ℂ)) (P : Matrix α α ℂ → Prop) (Q : Matrix β β ℂ → Prop) (R : Matrix (α ⊕ β) (α ⊕ β) ℂ → Prop) (hM : ∀ X ∈ M, P X) (hN : ∀ X ∈ N, Q X) (hR : ∀ (X : Matrix α α ℂ) (Y : Matrix β β ℂ), P X → Q Y → R (Matrix.fromBlocks X 0 0 Y)) (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) : X ∈ joint M N → R X

theorem Complexity.ExactFourier.Round.joint_rounds {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : List (Matrix α α ℂ)) (N : List (Matrix β β ℂ)) (hM : ∀ X ∈ M, Round X) (hN : ∀ X ∈ N, Round X) (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) : X ∈ joint M N → Round X

theorem Complexity.ExactFourier.Layered.rounds {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : ∃ (L : List (Matrix α α ℂ)), L.length = d ∧ L.prod = M ∧ ∀ X ∈ L, Round X

Finite lists of simultaneous rounds, with identity padding and no change of width.