Exact Fourier circuits: rect stable algebra

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

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

theorem Complexity.ExactFourier.Layered.stable_rect_add {α β σ : Type} [Fintype α] [Fintype β] [Fintype σ] [DecidableEq α] [DecidableEq β] [DecidableEq σ] {G H : Matrix α β ℂ} {d e : ℕ} (hG : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) (hH : Layered (Matrix.fromBlocks (rectangularShear H) 0 0 1) e) : Layered (Matrix.fromBlocks (rectangularShear (G + H)) 0 0 1) (d + e)

theorem Complexity.ExactFourier.Layered.stable_rect_transpose {α β σ : Type} [Fintype α] [Fintype β] [Fintype σ] [DecidableEq α] [DecidableEq β] [DecidableEq σ] {G : Matrix α β ℂ} {d : ℕ} (hG : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) : Layered (Matrix.fromBlocks (rectangularShear G.transpose) 0 0 1) d

def Complexity.ExactFourier.Layered.splitRowsLeft {α β γ σ : Type} : (α ⊕ γ) ⊕ β ⊕ σ ≃ ((α ⊕ β) ⊕ γ) ⊕ σ

Regroup four coordinate blocks to put the two data blocks first.

Equations

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

def Complexity.ExactFourier.Layered.splitRowsRight {α β γ σ : Type} : (β ⊕ γ) ⊕ α ⊕ σ ≃ ((α ⊕ β) ⊕ γ) ⊕ σ

Regroup four coordinate blocks and restore the common order of the data blocks.

Equations

• Complexity.ExactFourier.Layered.splitRowsRight = Complexity.ExactFourier.Layered.splitRowsLeft.trans (((Equiv.sumComm β α).sumCongr (Equiv.refl γ)).sumCongr (Equiv.refl σ))

theorem Complexity.ExactFourier.Layered.split_rows_left_matrix {α β γ σ : Type} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq σ] (G : Matrix α γ ℂ) : (Matrix.reindex splitRowsLeft splitRowsLeft) (Matrix.fromBlocks (rectangularShear G) 0 0 1) = Matrix.fromBlocks (rectangularShear (G.fromRows 0)) 0 0 1

theorem Complexity.ExactFourier.Layered.split_rows_right_matrix {α β γ σ : Type} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq σ] (H : Matrix β γ ℂ) : (Matrix.reindex splitRowsRight splitRowsRight) (Matrix.fromBlocks (rectangularShear H) 0 0 1) = Matrix.fromBlocks (rectangularShear (Matrix.fromRows 0 H)) 0 0 1

theorem Complexity.ExactFourier.Layered.stable_rect_split_rows {α β γ σ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype σ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq σ] {G : Matrix α γ ℂ} {H : Matrix β γ ℂ} {d e : ℕ} (hG : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) (hH : Layered (Matrix.fromBlocks (rectangularShear H) 0 0 1) e) : Layered (Matrix.fromBlocks (rectangularShear (G.fromRows H)) 0 0 1) (d + e)

theorem Complexity.ExactFourier.Layered.stable_reindex {α β σ α' β' σ' : Type} [Fintype α] [Fintype β] [Fintype σ] [Fintype α'] [Fintype β'] [Fintype σ'] [DecidableEq α] [DecidableEq β] [DecidableEq σ] [DecidableEq α'] [DecidableEq β'] [DecidableEq σ'] {G : Matrix α β ℂ} {d : ℕ} (h : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) (e : α ≃ α') (f : β ≃ β') (g : σ ≃ σ') : Layered (Matrix.fromBlocks (rectangularShear ((Matrix.reindex e f) G)) 0 0 1) d

theorem Complexity.ExactFourier.Layered.stable_extra {α β σ τ : Type} [Fintype α] [Fintype β] [Fintype σ] [Fintype τ] [DecidableEq α] [DecidableEq β] [DecidableEq σ] [DecidableEq τ] {G : Matrix α β ℂ} {d : ℕ} (h : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d

theorem Complexity.ExactFourier.Layered.stable_scratch_mono {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {G : Matrix α β ℂ} {d s t : ℕ} (h : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) (hst : s ≤ t) : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d

theorem Complexity.ExactFourier.Layered.stable_zero {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {G : Matrix α β ℂ} {d : ℕ} (h : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d) : Layered (rectangularShear G) d

theorem Complexity.ExactFourier.Layered.stable_empty_rows {β σ : Type} [Fintype β] [Fintype σ] [DecidableEq β] [DecidableEq σ] (G : Matrix (Fin 0) β ℂ) (d : ℕ) : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d

theorem Complexity.ExactFourier.Layered.stable_empty_cols {α σ : Type} [Fintype α] [Fintype σ] [DecidableEq α] [DecidableEq σ] (G : Matrix α (Fin 0) ℂ) (d : ℕ) : Layered (Matrix.fromBlocks (rectangularShear G) 0 0 1) d

theorem Complexity.ExactFourier.Layered.stable_rows_nat {a b e s d f : ℕ} (M : ℕ → ℕ → ℂ) (hG : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin a) (j : Fin e) => M ↑i ↑j) 0 0 1) d) (hH : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin b) (j : Fin e) => M (a + ↑i) ↑j) 0 0 1) f) : Layered (Matrix.fromBlocks (rectangularShear fun (i : Fin (a + b)) (j : Fin e) => M ↑i ↑j) 0 0 1) (d + f)

def Complexity.ExactFourier.SumLayered {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (d c : ℕ) : Prop

A sum of at most c matrices, each realizable in d parallel layers.

Equations

• Complexity.ExactFourier.SumLayered M d c = ∃ (L : List (Matrix α α ℂ)), L.length ≤ c ∧ L.sum = M ∧ ∀ N ∈ L, Complexity.ExactFourier.Layered N d

theorem Complexity.ExactFourier.SumLayered.single {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : SumLayered M d 1

theorem Complexity.ExactFourier.SumLayered.weaken {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d e c f : ℕ} (h : SumLayered M d c) (hde : d ≤ e) (hcf : c ≤ f) : SumLayered M e f

theorem Complexity.ExactFourier.SumLayered.add {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d c e : ℕ} (hM : SumLayered M d c) (hN : SumLayered N d e) : SumLayered (M + N) d (c + e)

theorem Complexity.ExactFourier.SumLayered.transpose {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d c : ℕ} (hM : SumLayered M d c) : SumLayered M.transpose d c

theorem Complexity.ExactFourier.SumLayered.mul {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d e c f : ℕ} (hM : SumLayered M d c) (hN : SumLayered N e f) : SumLayered (M * N) (d + e) (c * f)

theorem Complexity.ExactFourier.SumLayered.diagonal {α : Type} [Fintype α] [DecidableEq α] (c : α → ℂ) : SumLayered (Matrix.diagonal c) 1 2

theorem Complexity.ExactFourier.SumLayered.submatrix_stable {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] {M : Matrix γ γ ℂ} {d c : ℕ} (hM : SumLayered M d c) (e : α ↪ γ) (f : β ↪ γ) : Layered (Matrix.fromBlocks (rectangularShear (M.submatrix ⇑e ⇑f)) 0 0 1) (c * (4 * d + 4))

noncomputable def Complexity.ExactFourier.RadixTwo.convolutionMatrix (k : ℕ) (f : Polynomial ℂ) : Matrix (Fin (2 ^ k)) (Fin (2 ^ k)) ℂ

Cyclic convolution expressed as inverse Fourier, diagonal scaling, and Fourier factors.

Equations

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

theorem Complexity.ExactFourier.RadixTwo.convolution_sumLayered (k : ℕ) (f : Polynomial ℂ) : SumLayered (convolutionMatrix k f) (4 * k + 1) 2

theorem Complexity.ExactFourier.RadixTwo.convolution_mulVec (k : ℕ) (f : Polynomial ℂ) (x : Fin (2 ^ k) → ℂ) (hx : (f * (Polynomial.ofFn (2 ^ k)) x).natDegree < 2 ^ k) : (convolutionMatrix k f).mulVec x = fun (i : Fin (2 ^ k)) => (f * (Polynomial.ofFn (2 ^ k)) x).coeff ↑i

theorem Complexity.ExactFourier.RadixTwo.ofFn_single {n : ℕ} (j : Fin n) : (Polynomial.ofFn n) (Pi.single j 1) = (Polynomial.monomial ↑j) 1

theorem Complexity.ExactFourier.RadixTwo.convolution_entry (k : ℕ) (f : Polynomial ℂ) (i j : Fin (2 ^ k)) (hj : f.natDegree + ↑j < 2 ^ k) : convolutionMatrix k f i j = if ↑j ≤ ↑i then f.coeff (↑i - ↑j) else 0

def Complexity.ExactFourier.initialEmbedding {a n : ℕ} (h : a ≤ n) : Fin a ↪ Fin n

Embed an initial finite interval into a larger one without changing index values.

Equations

• Complexity.ExactFourier.initialEmbedding h = { toFun := fun (i : Fin a) => ⟨↑i, ⋯⟩, inj' := ⋯ }

@[simp]

theorem Complexity.ExactFourier.initialEmbedding_val {a n : ℕ} (h : a ≤ n) (i : Fin a) : ↑((initialEmbedding h) i) = ↑i

theorem Complexity.ExactFourier.sum_initial {a n : ℕ} (h : a ≤ n) (f : Fin n → ℂ) : (∑ i : Fin n, if ↑i < a then f i else 0) = ∑ i : Fin a, f ((initialEmbedding h) i)

theorem Complexity.ExactFourier.compress_product {a b e n : ℕ} (ha : a ≤ n) (hb : b ≤ n) (he : e ≤ n) (M N : Matrix (Fin n) (Fin n) ℂ) : ((M * Matrix.diagonal fun (i : Fin n) => if ↑i < e then 1 else 0) * N).submatrix ⇑(initialEmbedding ha) ⇑(initialEmbedding hb) = M.submatrix ⇑(initialEmbedding ha) ⇑(initialEmbedding he) * N.submatrix ⇑(initialEmbedding he) ⇑(initialEmbedding hb)