Exact Fourier circuits: tensor cost algebra

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

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

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

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

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

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

theorem Complexity.ExactFourier.CircuitCost.tensor_punit {α : Type} [Fintype α] (M : Matrix α α ℂ) : cost (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1) = cost M

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

def Complexity.ExactFourier.TensorAxis.funCoordinates {α : Type} (k : ℕ) : Space α k ≃ (Fin k → α)

Identify recursive tensor coordinates with functions on a finite set of axes.

Equations

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

theorem Complexity.ExactFourier.TensorAxis.power_entries {α : Type} (M : Matrix α α ℂ) (k : ℕ) (x y : Space α k) : power M k x y = ∏ i : Fin k, M ((funCoordinates k) x i) ((funCoordinates k) y i)

theorem Complexity.ExactFourier.TensorAxis.power_fun_reindex {α : Type} (M : Matrix α α ℂ) (k : ℕ) : (Matrix.reindex (funCoordinates k) (funCoordinates k)) (power M k) = fun (x y : Fin k → α) => ∏ i : Fin k, M (x i) (y i)

def Complexity.ExactFourier.TensorAxis.appendCoordinates {α : Type} (k l : ℕ) : Space α (k + l) ≃ Space α k × Space α l

Grouping changes coordinate indexing only, not the scalar operation.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.TensorAxis.appendCoordinates k 0 = (Equiv.prodPUnit (Complexity.ExactFourier.TensorAxis.Space α (k + 0))).symm

theorem Complexity.ExactFourier.TensorAxis.power_append {α : Type} (M : Matrix α α ℂ) (k l : ℕ) : (Matrix.reindex (appendCoordinates k l) (appendCoordinates k l)) (power M (k + l)) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (power M k) (power M l)

theorem Complexity.ExactFourier.TensorAxis.power_reindex {α β : Type} (e : α ≃ β) (M : Matrix α α ℂ) (k : ℕ) : ∃ (f : Space α k ≃ Space β k), (Matrix.reindex f f) (power M k) = power ((Matrix.reindex e e) M) k

def Complexity.ExactFourier.Amplification.avg (p : ℝ) (f : ℕ → ℝ) : ℕ → ℕ → ℝ

Finite dimension-weighted sector average; no random choices enter a circuit.

Equations

• Complexity.ExactFourier.Amplification.avg p f 0 x✝ = f x✝
• Complexity.ExactFourier.Amplification.avg p f j.succ x✝ = p * Complexity.ExactFourier.Amplification.avg p f j (x✝ + 1) + (1 - p) * Complexity.ExactFourier.Amplification.avg p f j x✝

theorem Complexity.ExactFourier.Amplification.avg_mono {p : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (f g : ℕ → ℝ) (j r : ℕ) (h : ∀ (i : ℕ), r ≤ i → i ≤ r + j → f i ≤ g i) : avg p f j r ≤ avg p g j r

theorem Complexity.ExactFourier.Amplification.avg_const_mul (p C : ℝ) (f : ℕ → ℝ) (j r : ℕ) : avg p (fun (i : ℕ) => C * f i) j r = C * avg p f j r

theorem Complexity.ExactFourier.Amplification.avg_rpow {p a : ℝ} (hp : 0 ≤ p) (hp1 : p ≤ 1) (ha : 0 ≤ a) (ha1 : a ≤ 1) (j r : ℕ) : avg p (fun (i : ℕ) => (↑i + 1) ^ a) j r ≤ (↑r + p * ↑j + 1) ^ a

def Complexity.ExactFourier.Amplification.sectorCost (l : ℕ → ℕ) (s : ℕ) : ℕ → ℕ → ℕ

The recursive cost bound obtained by splitting off identity sectors.

Equations

• Complexity.ExactFourier.Amplification.sectorCost l s 0 x✝ = l x✝
• Complexity.ExactFourier.Amplification.sectorCost l s j.succ x✝ = Complexity.ExactFourier.Amplification.sectorCost l s j (x✝ + 1) + s * Complexity.ExactFourier.Amplification.sectorCost l s j x✝

theorem Complexity.ExactFourier.Amplification.cost_sectors {α δ : Type} [Fintype α] [Fintype δ] [DecidableEq δ] (A : Matrix α α ℂ) (j r : ℕ) : CircuitCost.cost (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (TensorAxis.power (Matrix.fromBlocks A 0 0 1) j) (TensorAxis.power A r)) ≤ sectorCost (fun (k : ℕ) => CircuitCost.cost (TensorAxis.power A k)) (Fintype.card δ) j r

theorem Complexity.ExactFourier.Amplification.cost_call_power {α δ : Type} [Fintype α] [Fintype δ] (A : Matrix α α ℂ) (e : α ↪ δ) (j : ℕ) : CircuitCost.cost (TensorAxis.power (Embedded.matrix e A) j) ≤ sectorCost (fun (k : ℕ) => CircuitCost.cost (TensorAxis.power A k)) (Fintype.card (Embedded.complement e)) j 0

theorem Complexity.ExactFourier.Amplification.sectorCost_avg (l : ℕ → ℕ) {q s : ℕ} (hq : 0 < q) (j r : ℕ) : ↑(sectorCost l s j r) = ↑q ^ r * (↑q + ↑s) ^ j * avg (↑q / (↑q + ↑s)) (fun (i : ℕ) => ↑(l i) / ↑q ^ i) j r

theorem Complexity.ExactFourier.TensorAxis.power_group {α : Type} (A : Matrix α α ℂ) (b j : ℕ) : ∃ (e : Space α (b * j) ≃ Space (Space α b) j), (Matrix.reindex e e) (power A (b * j)) = power (power A b) j

theorem Complexity.ExactFourier.TensorAxis.power_monomial {α : Type} [DecidableEq α] (A : Matrix α α ℂ) (hA : MonomialMatrix A) (j : ℕ) : MonomialMatrix (power A j)

theorem Complexity.ExactFourier.TensorAxis.source_power_reindex {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (b : ℕ) : (Matrix.reindex ((funCoordinates b).trans (tensorCoordinates q b).symm) ((funCoordinates b).trans (tensorCoordinates q b).symm)) (power A b) = tensorPower A b

theorem Complexity.ExactFourier.Amplification.cost_source_power {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (b : ℕ) : CircuitCost.cost (tensorPower A b) = CircuitCost.cost (TensorAxis.power A b)

theorem Complexity.ExactFourier.Amplification.cost_group {α : Type} [Fintype α] (A : Matrix α α ℂ) (b j : ℕ) : CircuitCost.cost (TensorAxis.power A (b * j)) = CircuitCost.cost (TensorAxis.power (TensorAxis.power A b) j)

theorem Complexity.ExactFourier.Amplification.cost_reindexed_power {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (A : Matrix α α ℂ) (j : ℕ) : CircuitCost.cost (TensorAxis.power ((Matrix.reindex e e) A) j) = CircuitCost.cost (TensorAxis.power A j)

theorem Complexity.ExactFourier.Amplification.complement_card {q Q : ℕ} (e : Fin q ↪ Fin Q) : Fintype.card (Embedded.complement e) = Q - q

theorem Complexity.ExactFourier.Amplification.cost_word_power {q Q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (W : List (WordStep A Q)) (j : ℕ) : CircuitCost.cost (TensorAxis.power (wordMatrix W) j) ≤ W.length * Q ^ j + wordCalls W * sectorCost (fun (k : ℕ) => CircuitCost.cost (TensorAxis.power A k)) (Q - q) j 0

noncomputable def Complexity.ExactFourier.Amplification.normalizedCost {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (k : ℕ) : ℝ

The scalar circuit cost of a tensor power divided by its dimension.

Equations

• Complexity.ExactFourier.Amplification.normalizedCost A k = ↑(Complexity.ExactFourier.CircuitCost.cost (Complexity.ExactFourier.TensorAxis.power A k)) / ↑q ^ k

theorem Complexity.ExactFourier.Amplification.normalized_add {q : ℕ} (hq : 0 < q) (A : Matrix (Fin q) (Fin q) ℂ) (k l : ℕ) : normalizedCost A (k + l) ≤ normalizedCost A k + normalizedCost A l

theorem Complexity.ExactFourier.Amplification.normalized_linear {q : ℕ} (hq : 0 < q) (A : Matrix (Fin q) (Fin q) ℂ) (k : ℕ) : normalizedCost A k ≤ 2 * ↑q * ↑k

theorem Complexity.ExactFourier.Amplification.normalized_word {q b : ℕ} (hq : 0 < q) (A : Matrix (Fin q) (Fin q) ℂ) (hb : 1 ≤ b) (W : List (WordStep A (q ^ b))) (hW : wordMatrix W = tensorPower A b) (j : ℕ) : normalizedCost A (b * j) ≤ ↑W.length + ↑(wordCalls W) * avg (↑q / ↑(q ^ b)) (normalizedCost A) j 0

theorem Complexity.ExactFourier.Amplification.normalized_recurrence {q b : ℕ} (hq : 0 < q) (A : Matrix (Fin q) (Fin q) ℂ) (hb : 1 ≤ b) (W : List (WordStep A (q ^ b))) (hW : wordMatrix W = tensorPower A b) (k : ℕ) : normalizedCost A k ≤ ↑W.length + 2 * ↑q * ↑b + ↑(wordCalls W) * avg (↑q / ↑(q ^ b)) (normalizedCost A) (k / b) 0