Exact Fourier circuits: displacement kernel

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

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

def Complexity.ExactFourier.Displacement.kernel (v w : ℕ → ℂ) (i j : ℕ) : ℂ

The convolution kernel reconstructed along successive matrix diagonals.

Equations

• Complexity.ExactFourier.Displacement.kernel v w i j = ∑ l ∈ Finset.range (min i j + 1), v (i - l) * w (j - l)

@[simp]

theorem Complexity.ExactFourier.Displacement.kernel_zero_left (v w : ℕ → ℂ) (j : ℕ) : kernel v w 0 j = v 0 * w j

@[simp]

theorem Complexity.ExactFourier.Displacement.kernel_zero_right (v w : ℕ → ℂ) (i : ℕ) : kernel v w i 0 = v i * w 0

theorem Complexity.ExactFourier.Displacement.kernel_succ (v w : ℕ → ℂ) (i j : ℕ) : kernel v w (i + 1) (j + 1) = v (i + 1) * w (j + 1) + kernel v w i j

def Complexity.ExactFourier.Displacement.lower (v : ℕ → ℂ) (a e : ℕ) : Matrix (Fin a) (Fin e) ℂ

A rectangular lower triangular Toeplitz matrix built from a sequence.

Equations

• Complexity.ExactFourier.Displacement.lower v a e i j = if ↑j ≤ ↑i then v (↑i - ↑j) else 0

theorem Complexity.ExactFourier.Displacement.kernel_eq_mul (v w : ℕ → ℂ) (a e : ℕ) : (fun (i : Fin a) (j : Fin e) => kernel v w ↑i ↑j) = lower v a e * (lower w e e).transpose

def Complexity.ExactFourier.Displacement.delta : ℕ → ℂ

The sequence that is one at zero and zero elsewhere.

Equations

• Complexity.ExactFourier.Displacement.delta i = if i = 0 then 1 else 0

theorem Complexity.ExactFourier.Displacement.reconstruct (a e : ℕ) (ha : 0 < a) (he : 0 < e) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : have row := fun (j : ℕ) => M 0 j - v 0 * w j; have col := fun (i : ℕ) => if i = 0 then 0 else M i 0 - v i * w 0; ∀ (i j : ℕ), i < a → j < e → M i j = kernel v w i j + kernel delta row i j + kernel col delta i j

The exact rank-three displacement reconstruction, with only the stated interior outer-product recurrence; no analytic or generic-position premise.

def Complexity.ExactFourier.Displacement.extendVector {a : ℕ} (v : Fin a → ℂ) : ℕ → ℂ

Extend a finite vector to a sequence by setting all later entries to zero.

Equations

• Complexity.ExactFourier.Displacement.extendVector v i = if hi : i < a then v ⟨i, hi⟩ else 0

theorem Complexity.ExactFourier.Displacement.coeff_ofFn_extend (a : ℕ) (v : Fin a → ℂ) : ⇑((Polynomial.ofFn a) v).coeff = extendVector v

theorem Complexity.ExactFourier.Displacement.convolution_submatrix (a e k : ℕ) (ha : 0 < a) (h : a + e ≤ 2 ^ k) (haL : a ≤ 2 ^ k) (heL : e ≤ 2 ^ k) (v : Fin a → ℂ) : (RadixTwo.convolutionMatrix k ((Polynomial.ofFn a) v)).submatrix ⇑(initialEmbedding haL) ⇑(initialEmbedding heL) = lower (extendVector v) a e

noncomputable def Complexity.ExactFourier.Displacement.fullKernel (k a e : ℕ) (v : Fin a → ℂ) (w : Fin e → ℂ) : Matrix (Fin (2 ^ k)) (Fin (2 ^ k)) ℂ

Realize a displacement kernel by convolution matrices and a coordinate projection.

Equations

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

theorem Complexity.ExactFourier.Displacement.fullKernel_sumLayered (k a e : ℕ) (v : Fin a → ℂ) (w : Fin e → ℂ) : SumLayered (fullKernel k a e v w) (8 * k + 3) 8

theorem Complexity.ExactFourier.Displacement.kernel_submatrix (a e k : ℕ) (ha : 0 < a) (he : 0 < e) (h : 2 * (a + e) ≤ 2 ^ k) (v : Fin a → ℂ) (w : Fin e → ℂ) : (fullKernel k a e v w).submatrix ⇑(initialEmbedding ⋯) ⇑(initialEmbedding ⋯) = fun (i : Fin a) (j : Fin e) => kernel (extendVector v) (extendVector w) ↑i ↑j

theorem Complexity.ExactFourier.Displacement.kernel_stable (a e k : ℕ) (ha : 0 < a) (he : 0 < e) (h : 2 * (a + e) ≤ 2 ^ k) (v : Fin a → ℂ) (w : Fin e → ℂ) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => kernel (extendVector v) (extendVector w) ↑i ↑j) 0 0 1) (256 * k + 128)

theorem Complexity.ExactFourier.Displacement.kernel_congr (v v' w w' : ℕ → ℂ) (i j : ℕ) (hv : ∀ l ≤ i, v l = v' l) (hw : ∀ l ≤ j, w l = w' l) : kernel v w i j = kernel v' w' i j

theorem Complexity.ExactFourier.Displacement.kernel_restrict (v w : ℕ → ℂ) (a e : ℕ) (i : Fin a) (j : Fin e) : kernel (extendVector fun (u : Fin a) => v ↑u) (extendVector fun (v : Fin e) => w ↑v) ↑i ↑j = kernel v w ↑i ↑j

theorem Complexity.ExactFourier.Displacement.stable_of_displacement (a e k : ℕ) (ha : 0 < a) (he : 0 < e) (h : 2 * (a + e) ≤ 2 ^ k) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) 0 0 1) (768 * k + 384)

theorem Complexity.ExactFourier.Displacement.small_stable (a e s c k : ℕ) (ha : a ≤ c) (he : e ≤ c) (hfft : 4 * c ≤ 2 ^ k) (hspace : 2 ^ k + 2 * c ≤ a + e + s) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) 0 0 1) (768 * k + 384)

theorem Complexity.ExactFourier.Displacement.row_chunks (p a e s c k : ℕ) (ha : a ≤ p * c) (he : e ≤ c) (hfft : 4 * c ≤ 2 ^ k) (hspace : 2 ^ k + 2 * c ≤ a + e + s) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) 0 0 1) (p * (768 * k + 384))

theorem Complexity.ExactFourier.Displacement.all_chunks (q p a e s c k : ℕ) (ha : a ≤ p * c) (he : e ≤ q * c) (hfft : 4 * c ≤ 2 ^ k) (hspace : 2 ^ k + 2 * c ≤ a + e + s) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) 0 0 1) (q * p * (768 * k + 384))

theorem Complexity.ExactFourier.Layered.rect_single {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (i : α) (j : β) (c : ℂ) : Layered (rectangularShear (Matrix.single i j c)) 1

theorem Complexity.ExactFourier.Layered.rect_finset_sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {τ : Type} (s : Finset τ) (G : τ → Matrix α β ℂ) (d : τ → ℕ) (h : ∀ i ∈ s, Layered (rectangularShear (G i)) (d i)) : Layered (rectangularShear (∑ i ∈ s, G i)) (∑ i ∈ s, d i)

theorem Complexity.ExactFourier.Layered.rect_dense {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (G : Matrix α β ℂ) : Layered (rectangularShear G) (Fintype.card α * Fintype.card β)

theorem Complexity.ExactFourier.Displacement.exact_width (a e : ℕ) (M : ℕ → ℕ → ℂ) (v w : ℕ → ℂ) (hrec : ∀ (i j : ℕ), i + 1 < a → j + 1 < e → M (i + 1) (j + 1) = M i j + v (i + 1) * w (j + 1)) : Layered (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) (2097152 * (Nat.log 2 (a + e) + 1))

Exact-width displacement shear; dirty scratch is borrowed internally.