Exact Fourier circuits: amplification master

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

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

theorem Complexity.ExactFourier.Amplification.saving_exponent {g ρ : ℝ} (hρ : 0 < ρ) (hs : g * ρ < 1) : ∃ (a : ℝ), 0 < a ∧ a < 1 ∧ g * ρ ^ a < 1

theorem Complexity.ExactFourier.Amplification.recurrence_bound (f : ℕ → ℝ) {b : ℕ} {p g C₀ : ℝ} (hb : 2 ≤ b) (hp : 0 < p) (hp1 : p ≤ 1) (hg : 0 ≤ g) (hC₀ : 0 ≤ C₀) (hs : g * (p / ↑b) < 1) (hf : ∀ (k : ℕ), f k ≤ C₀ + g * avg p f (k / b) 0) : ∃ (a : ℝ) (C : ℝ), 0 < a ∧ a < 1 ∧ 0 < C ∧ ∀ (k : ℕ), f k ≤ C * (↑k + 1) ^ a

theorem Complexity.ExactFourier.Amplification.tensor_amplification {q b : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) (hb : 2 ≤ b) (W : List (WordStep A (q ^ b))) (hW : wordMatrix W = tensorPower A b) (hw : wordCalls W < b * q ^ (b - 1)) : ∃ (a : ℝ) (C : ℝ), 0 < a ∧ a < 1 ∧ 0 < C ∧ ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a

Tensor amplification for the literal finite winning word, with charged scalars.

inductive Complexity.ExactFourier.AParallel {q : ℕ} (A : Matrix (Fin q) (Fin q) ℂ) {α : Type} [Fintype α] [DecidableEq α] : Matrix α α ℂ → Prop

A disjoint union of forward calls and untouched coordinates.

• identity {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] : AParallel A 1
• atom {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} : AParallel A A
• reindex {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) {M : Matrix α α ℂ} (h : AParallel A M) : AParallel A ((Matrix.reindex e e) M)
• sum {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} (hM : AParallel A M) (hN : AParallel A N) : AParallel A (Matrix.fromBlocks M 0 0 N)

theorem Complexity.ExactFourier.AParallel.embed {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} (h : AParallel A M) (e : α ↪ β) : AParallel A (Embedded.matrix e M)

structure Complexity.ExactFourier.AFrame {q : ℕ} {α : Type} [Fintype α] [DecidableEq α] (A : Matrix (Fin q) (Fin q) ℂ) (M : Matrix α α ℂ) : Prop

A product of a parallel layer of A and a monomial matrix.

• exists_factors : ∃ (B : Matrix α α ℂ) (Q : Matrix α α ℂ), AParallel A B ∧ MonomialMatrix Q ∧ M = B * Q

theorem Complexity.ExactFourier.AFrame.mono {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : AFrame A M

theorem Complexity.ExactFourier.AFrame.atom_mono {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (M : Matrix (Fin q) (Fin q) ℂ) (hm : MonomialMatrix M) : AFrame A (A * M)

theorem Complexity.ExactFourier.AFrame.reindex {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} (h : AFrame A M) (e : α ≃ β) : AFrame A ((Matrix.reindex e e) M)

theorem Complexity.ExactFourier.AFrame.sum {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} (hM : AFrame A M) (hN : AFrame A N) : AFrame A (Matrix.fromBlocks M 0 0 N)

def Complexity.ExactFourier.AGenerated {q : ℕ} {α : Type} [Fintype α] [DecidableEq α] (A : Matrix (Fin q) (Fin q) ℂ) (M : Matrix α α ℂ) (d : ℕ) : Prop

A factorization into exactly d parallel frames of the fixed matrix A.

Equations

• Complexity.ExactFourier.AGenerated A M d = ∃ (L : List (Matrix α α ℂ)), L.length = d ∧ L.prod = M ∧ ∀ X ∈ L, Complexity.ExactFourier.AFrame A X

theorem Complexity.ExactFourier.AGenerated.identity {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] (d : ℕ) : AGenerated A 1 d

theorem Complexity.ExactFourier.AGenerated.frame {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} (h : AFrame A M) : AGenerated A M 1

theorem Complexity.ExactFourier.AGenerated.mono {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : AGenerated A M 1

theorem Complexity.ExactFourier.AGenerated.mul {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d e : ℕ} (hM : AGenerated A M d) (hN : AGenerated A N e) : AGenerated A (M * N) (d + e)

theorem Complexity.ExactFourier.AGenerated.weaken {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d e : ℕ} (h : AGenerated A M d) (hde : d ≤ e) : AGenerated A M e

theorem Complexity.ExactFourier.AGenerated.reindex {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {d : ℕ} (h : AGenerated A M d) (e : α ≃ β) : AGenerated A ((Matrix.reindex e e) M) d

theorem Complexity.ExactFourier.AGenerated.sum {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {N : Matrix β β ℂ} {d : ℕ} (hM : AGenerated A M d) (hN : AGenerated A N d) : AGenerated A (Matrix.fromBlocks M 0 0 N) d

theorem Complexity.ExactFourier.AGenerated.embed {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {d : ℕ} (h : AGenerated A M d) (e : α ↪ β) : AGenerated A (Embedded.matrix e M) d

theorem Complexity.ExactFourier.AGenerated.from_pattern {q : ℕ} {A M : Matrix (Fin q) (Fin q) ℂ} {h : ℕ} (hp : PositiveGeneration.Pattern A h M) : AGenerated A M (h + 1)

def Complexity.ExactFourier.ParallelTensorCost.Good {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} {α : Type} [Fintype α] (M : Matrix α α ℂ) (m : ℕ) : Prop

A uniform polynomial bound on the cost of tensoring M with powers of A.

Equations

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

theorem Complexity.ExactFourier.ParallelTensorCost.Good.reindex {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} {α β : Type} [Fintype α] [Fintype β] {M : Matrix α α ℂ} {m : ℕ} (hg : Good M m) (e : α ≃ β) : Good ((Matrix.reindex e e) M) m

theorem Complexity.ExactFourier.ParallelTensorCost.Good.parallel {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq β] (ha : 0 ≤ a) (hC : 0 ≤ C) {M : Matrix α α ℂ} {m : ℕ} (hg : Good M m) {N : Matrix β β ℂ} (hN : AParallel A N) : Good (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) (m + 1)

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

Separate the first coordinate of a dependent finite product from its tail.

Equations

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

theorem Complexity.ExactFourier.PiTensor.splitFirst_matrix {n : ℕ} (D : Fin (n + 1) → Type) (M : (i : Fin (n + 1)) → Matrix (D i) (D i) ℂ) : (Matrix.reindex (splitFirst D) (splitFirst D)) (matrix M) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (M 0) (matrix fun (i : Fin n) => M i.succ)

theorem Complexity.ExactFourier.PiTensor.monomial {ι : Type} [Fintype ι] {D : ι → Type} [(i : ι) → DecidableEq (D i)] (M : (i : ι) → Matrix (D i) (D i) ℂ) (hM : ∀ (i : ι), MonomialMatrix (M i)) : MonomialMatrix (matrix M)

theorem Complexity.ExactFourier.ParallelTensorCost.pi_good {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) (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) ℂ) (hM : ∀ (i : Fin n), AParallel A (M i)) : Good (PiTensor.matrix M) n

theorem Complexity.ExactFourier.ParallelTensorCost.pi_cost {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) (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) ℂ) (hM : ∀ (i : Fin n), AParallel A (M i)) : ↑(CircuitCost.cost (PiTensor.matrix M)) ≤ C * ↑(Fintype.card ((i : Fin n) → D i)) * (↑n + 1) ^ a