Exact Fourier circuits: main

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

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

theorem Complexity.ExactFourier.PrimeInventory.count_fourth (M : ℕ) (hM : 10 ≤ M) : M ≤ (M ^ 4).primeCounting

def Complexity.ExactFourier.PrimeInventory.upper (q m : ℕ) : ℕ

A polynomial upper bound large enough to contain the required prime inventory.

Equations

• Complexity.ExactFourier.PrimeInventory.upper q m = (m + 2 * q + 10) ^ 4

theorem Complexity.ExactFourier.PrimeInventory.family (q m : ℕ) : ∃ (r : Fin m → ℕ), (∀ (i : Fin m), Nat.Prime (r i)) ∧ Function.Injective r ∧ (∀ (i : Fin m), 2 * q ≤ r i) ∧ ∀ (i : Fin m), r i ≤ upper q m

theorem Complexity.ExactFourier.PrimeInventory.family_coprime {m : ℕ} {r : Fin m → ℕ} (hr : ∀ (i : Fin m), Nat.Prime (r i)) (hi : Function.Injective r) : Pairwise fun (i j : Fin m) => (r i).Coprime (r j)

def Complexity.ExactFourier.FourierTransfer.depth (q m : ℕ) : ℕ

The explicit layer-depth bound used to transfer a finite win to Fourier circuits.

Equations

• Complexity.ExactFourier.FourierTransfer.depth q m = 8388608 * (Nat.log 2 (Complexity.ExactFourier.PrimeInventory.upper q m) + 2) ^ 2 + 5

theorem Complexity.ExactFourier.FourierTransfer.depth_bound (q m : ℕ) : ↑(depth q m) ≤ 536870917 * (Real.log (↑m + 2 * ↑q + 10) + 1) ^ 2

theorem Complexity.ExactFourier.FourierTransfer.family_cost {q h : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) (m : ℕ) : ∃ (n : ℕ), 2 ^ m ≤ n ∧ ↑(CircuitCost.cost (fourierMatrix n)) ≤ 536870917 * ↑(q * (h + 1) + 1) * (C + 1) * ↑n * (Real.log (↑m + 2 * ↑q + 10) + 1) ^ 2 * (↑m + 2 * ↑q + 10) ^ a

theorem Complexity.ExactFourier.FourierTransfer.log_square_littleO {a : ℝ} (ha : a < 1) : (fun (x : ℝ) => (Real.log x + 1) ^ 2) =o[Filter.atTop] fun (x : ℝ) => x ^ (1 - a)

theorem Complexity.ExactFourier.FourierTransfer.log_power_ratio {a : ℝ} (ha : a < 1) : Filter.Tendsto (fun (x : ℝ) => (Real.log x + 1) ^ 2 * x ^ a / x) Filter.atTop (nhds 0)

theorem Complexity.ExactFourier.FourierTransfer.shifted_log_power_ratio {a c : ℝ} (ha : a < 1) : Filter.Tendsto (fun (m : ℕ) => (Real.log (↑m + c) + 1) ^ 2 * (↑m + c) ^ a / ↑m) Filter.atTop (nhds 0)

theorem Complexity.ExactFourier.CircuitCost.exists_circuit {n : ℕ} (M : Matrix (Fin n) (Fin n) ℂ) : ∃ (C : Circuit n), C.size = cost M ∧ C.Computes M

theorem Complexity.ExactFourier.win_to_fourier (win : FiniteWinStatement) : MainStatement

An actual finite win transfers to arbitrarily large exact Fourier DAGs, with every scalar multiplication charged.

theorem Complexity.ExactFourier.main_theorem : MainStatement

theorem Complexity.ExactFourier.finite_win_exists : FiniteWinStatement

theorem Complexity.ExactFourier.exists_fourier_circuit (n : ℕ) : ∃ (k : ℕ) (C : Circuit n), C.size = k ∧ C.Computes (fourierMatrix n)

Existence of an exact circuit in every width, used only to define the minimum.

noncomputable def Complexity.ExactFourier.minimumSize (n : ℕ) : ℕ

The least number of source scalar gates computing the exact Fourier transform.

Equations

• Complexity.ExactFourier.minimumSize n = Nat.find ⋯

theorem Complexity.ExactFourier.minimumSize_attained (n : ℕ) : ∃ (C : Circuit n), C.size = minimumSize n ∧ C.Computes (fourierMatrix n)

theorem Complexity.ExactFourier.minimumSize_le {n : ℕ} (C : Circuit n) (hC : C.Computes (fourierMatrix n)) : minimumSize n ≤ C.size

theorem Complexity.ExactFourier.fourier_denominator_pos {n : ℕ} (hn : 2 ≤ n) : 0 < ↑n * Real.logb 2 ↑n

theorem Complexity.ExactFourier.main_liminf : Filter.liminf (fun (n : ℕ) => ↑(minimumSize n) / (↑n * Real.logb 2 ↑n)) Filter.atTop = 0

The liminf formulation of the main theorem, for the literal minimum scalar gate count.