Exact Fourier circuits: words

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

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

def Complexity.ExactFourier.IsMonomial {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) : Prop

A permutation matrix times an invertible diagonal matrix, literally P D.

Equations

• Complexity.ExactFourier.IsMonomial A = ∃ (σ : Equiv.Perm (Fin q)) (d : Fin q → ℂ), (∀ (j : Fin q), d j ≠ 0) ∧ ∀ (i j : Fin q), A i j = if i = σ j then d j else 0

noncomputable def Complexity.ExactFourier.embeddedCall {q w : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (e : Fin q ↪ Fin w) : Matrix (Fin w) (Fin w) ℂ

A call on an ordered tuple of distinct coordinates; all other values are fixed.

Equations

• Complexity.ExactFourier.embeddedCall A e u v = (∑ i : Fin q, ∑ j : Fin q, if e i = u then if e j = v then A i j else 0 else 0) + if u = v ∧ ¬∃ (i : Fin q), e i = u then 1 else 0

inductive Complexity.ExactFourier.WordStep {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (w : ℕ) : Type

Only forward calls to the specified A are allowed.

• monomial {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {w : ℕ} (M : Matrix (Fin w) (Fin w) ℂ) (hM : IsMonomial M) : WordStep A w
• call {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {w : ℕ} (e : Fin q ↪ Fin w) : WordStep A w

noncomputable def Complexity.ExactFourier.WordStep.matrix {q w : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} : WordStep A w → Matrix (Fin w) (Fin w) ℂ

The ambient matrix of a monomial step or an embedded call to the fixed matrix.

Equations

• (Complexity.ExactFourier.WordStep.monomial M hM).matrix = M
• (Complexity.ExactFourier.WordStep.call e).matrix = Complexity.ExactFourier.embeddedCall A e

def Complexity.ExactFourier.WordStep.calls {q w : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} : WordStep A w → ℕ

Charge one call for a matrix invocation and zero for a monomial step.

Equations

• (Complexity.ExactFourier.WordStep.monomial M hM).calls = 0
• (Complexity.ExactFourier.WordStep.call e).calls = 1

noncomputable def Complexity.ExactFourier.wordMatrix {q w : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (W : List (WordStep A w)) : Matrix (Fin w) (Fin w) ℂ

Stored chronologically, so a new step left-multiplies earlier steps.

Equations

• Complexity.ExactFourier.wordMatrix W = (List.map Complexity.ExactFourier.WordStep.matrix W).reverse.prod

def Complexity.ExactFourier.wordCalls {q w : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (W : List (WordStep A w)) : ℕ

The total number of calls to the fixed matrix in the finite-win word.

Equations

• Complexity.ExactFourier.wordCalls W = (List.map Complexity.ExactFourier.WordStep.calls W).sum

noncomputable def Complexity.ExactFourier.tensorCoordinates (q b : ℕ) : Fin (q ^ b) ≃ (Fin b → Fin q)

A fixed coordinate relabeling of the ordinary Kronecker tensor power.

Equations

• Complexity.ExactFourier.tensorCoordinates q b = (Equiv.cast ⋯).trans (Fintype.equivFin (Fin b → Fin q)).symm

noncomputable def Complexity.ExactFourier.tensorPower {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (b : ℕ) : Matrix (Fin (q ^ b)) (Fin (q ^ b)) ℂ

The ordinary matrix tensor power under the fixed finite-coordinate numbering.

Equations

• Complexity.ExactFourier.tensorPower A b i j = ∏ k : Fin b, A ((Complexity.ExactFourier.tensorCoordinates q b) i k) ((Complexity.ExactFourier.tensorCoordinates q b) j k)

def Complexity.ExactFourier.FiniteWinStatement : Prop

An invertible nonmonomial matrix has a tensor power using fewer calls than the standard construction.

Equations

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