Exact Fourier circuits: matrix relabel

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

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

theorem Complexity.ExactFourier.reindex_mulVec {α β γ δ : Type} [Fintype α] [Fintype γ] (e : β ≃ δ) (f : α ≃ γ) (M : Matrix β α ℂ) (x : γ → ℂ) : ((Matrix.reindex e f) M).mulVec x = M.mulVec (x ∘ ⇑f) ∘ ⇑e.symm

def Complexity.ExactFourier.RadixTwo.dft (n : ℕ) (ω : ℂ) : Matrix (Fin n) (Fin n) ℂ

The Fourier matrix associated with the specified size and complex root.

Equations

• Complexity.ExactFourier.RadixTwo.dft n ω i j = ω ^ (↑i * ↑j)

def Complexity.ExactFourier.RadixTwo.butterfly (n : ℕ) (ω : ℂ) : Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℂ

The block butterfly matrix combining even and odd Fourier transforms.

Equations

• Complexity.ExactFourier.RadixTwo.butterfly n ω = Matrix.fromBlocks 1 (Matrix.diagonal fun (i : Fin n) => ω ^ ↑i) 1 (-Matrix.diagonal fun (i : Fin n) => ω ^ ↑i)

theorem Complexity.ExactFourier.RadixTwo.butterfly_layer (n : ℕ) (ω : ℂ) (hω : ω ≠ 0) : Layered (butterfly n ω) 1

def Complexity.ExactFourier.RadixTwo.paritySumEquiv (n : ℕ) : Fin n ⊕ Fin n ≃ Fin (n + n)

Interleave two coordinate blocks into the even and odd positions.

Equations

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

@[simp]

theorem Complexity.ExactFourier.RadixTwo.paritySumEquiv_inl (n : ℕ) (i : Fin n) : (paritySumEquiv n) (Sum.inl i) = evenIndex n i

@[simp]

theorem Complexity.ExactFourier.RadixTwo.paritySumEquiv_inr (n : ℕ) (i : Fin n) : (paritySumEquiv n) (Sum.inr i) = oddIndex n i

theorem Complexity.ExactFourier.RadixTwo.dft_step (n : ℕ) (ω : ℂ) (hω : ω ^ n = -1) : dft (n + n) ω = (Matrix.reindex finSumFinEquiv (paritySumEquiv n)) (butterfly n ω * Matrix.fromBlocks (dft n (ω ^ 2)) 0 0 (dft n (ω ^ 2)))

theorem Complexity.ExactFourier.RadixTwo.dft_layers (k : ℕ) (ω : ℂ) (hω : IsPrimitiveRoot ω (2 ^ k)) : Layered (dft (2 ^ k) ω) (2 * k)

noncomputable def Complexity.ExactFourier.NewtonFourier.newton (ω : ℂ) (k : ℕ) : Polynomial ℂ

The Newton basis polynomial with roots at the first k powers of ω.

Equations

• Complexity.ExactFourier.NewtonFourier.newton ω k = ∏ j ∈ Finset.range k, (Polynomial.X - Polynomial.C (ω ^ j))

def Complexity.ExactFourier.NewtonFourier.H (ω : ℂ) (i : ℕ) : ℂ

The product of 1 - ω^j for exponents from one through i.

Equations

• Complexity.ExactFourier.NewtonFourier.H ω i = ∏ j ∈ Finset.range i, (1 - ω ^ (j + 1))

def Complexity.ExactFourier.NewtonFourier.scale (ω : ℂ) (k : ℕ) : ℂ

The product of the negatives of the first k powers of ω.

Equations

• Complexity.ExactFourier.NewtonFourier.scale ω k = ∏ j ∈ Finset.range k, -ω ^ j

noncomputable def Complexity.ExactFourier.NewtonFourier.N (n : ℕ) (ω : ℂ) : Matrix (Fin n) (Fin n) ℂ

Evaluate the Newton basis at successive powers of ω.

Equations

• Complexity.ExactFourier.NewtonFourier.N n ω i k = Polynomial.eval (ω ^ ↑i) (Complexity.ExactFourier.NewtonFourier.newton ω ↑k)

noncomputable def Complexity.ExactFourier.NewtonFourier.P (n : ℕ) (ω : ℂ) : Matrix (Fin n) (Fin n) ℂ

The coefficient matrix expressing the Newton basis in the monomial basis.

Equations

• Complexity.ExactFourier.NewtonFourier.P n ω i k = (Complexity.ExactFourier.NewtonFourier.newton ω ↑k).coeff ↑i

@[simp]

theorem Complexity.ExactFourier.NewtonFourier.newton_zero (ω : ℂ) : newton ω 0 = 1

theorem Complexity.ExactFourier.NewtonFourier.newton_succ (ω : ℂ) (k : ℕ) : newton ω (k + 1) = newton ω k * (Polynomial.X - Polynomial.C (ω ^ k))

@[simp]

theorem Complexity.ExactFourier.NewtonFourier.H_zero (ω : ℂ) : H ω 0 = 1

theorem Complexity.ExactFourier.NewtonFourier.H_succ (ω : ℂ) (i : ℕ) : H ω (i + 1) = H ω i * (1 - ω ^ (i + 1))

@[simp]

theorem Complexity.ExactFourier.NewtonFourier.scale_zero (ω : ℂ) : scale ω 0 = 1

theorem Complexity.ExactFourier.NewtonFourier.scale_succ (ω : ℂ) (k : ℕ) : scale ω (k + 1) = scale ω k * -ω ^ k

theorem Complexity.ExactFourier.NewtonFourier.newton_monic (ω : ℂ) (k : ℕ) : (newton ω k).Monic

@[simp]

theorem Complexity.ExactFourier.NewtonFourier.newton_natDegree (ω : ℂ) (k : ℕ) : (newton ω k).natDegree = k

theorem Complexity.ExactFourier.NewtonFourier.newton_eval_zero (ω : ℂ) (i k : ℕ) (h : i < k) : Polynomial.eval (ω ^ i) (newton ω k) = 0

theorem Complexity.ExactFourier.NewtonFourier.eval_factor (ω : ℂ) (i k : ℕ) (hki : k ≤ i) : Polynomial.eval (ω ^ i) (newton ω k) * H ω (i - k) = scale ω k * H ω i

theorem Complexity.ExactFourier.NewtonFourier.H_ne_zero {ω : ℂ} {n : ℕ} (hω : IsPrimitiveRoot ω n) {i : ℕ} (hi : i < n) : H ω i ≠ 0

theorem Complexity.ExactFourier.NewtonFourier.scale_ne_zero {ω : ℂ} (hω : ω ≠ 0) (k : ℕ) : scale ω k ≠ 0

theorem Complexity.ExactFourier.NewtonFourier.N_lower (n : ℕ) (ω : ℂ) : (N n ω).IsLowerTriangular

theorem Complexity.ExactFourier.NewtonFourier.P_upper (n : ℕ) (ω : ℂ) : (P n ω).IsUpperTriangular

theorem Complexity.ExactFourier.NewtonFourier.dft_mul_P (n : ℕ) (ω : ℂ) : RadixTwo.dft n ω * P n ω = N n ω

theorem Complexity.ExactFourier.Layered.inverse {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} {d : ℕ} (h : Layered M d) : Layered M⁻¹ d

theorem Complexity.ExactFourier.Layered.conjugate {α : Type} [Fintype α] [DecidableEq α] {M N : Matrix α α ℂ} {d e : ℕ} (hM : Layered M d) (hN : Layered N e) : Layered (M * N * M⁻¹) (2 * d + e)

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

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

theorem Complexity.ExactFourier.Layered.rect_neg {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {G : Matrix α β ℂ} {d : ℕ} (hG : Layered (rectangularShear G) d) : Layered (rectangularShear (-G)) d

theorem Complexity.ExactFourier.Layered.rect_mul_left {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {G : Matrix α β ℂ} {d e : ℕ} (hM : Layered M d) (hG : Layered (rectangularShear G) e) : Layered (rectangularShear (M * G)) (2 * d + e)

theorem Complexity.ExactFourier.Layered.rect_mul_right {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix β β ℂ} {G : Matrix α β ℂ} {d e : ℕ} (hM : Layered M d) (hG : Layered (rectangularShear G) e) : Layered (rectangularShear (G * M)) (2 * d + e)

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

Reassociate three coordinate blocks and exchange the last two.

Equations

• Complexity.ExactFourier.Layered.swapLast = (Equiv.sumAssoc α γ β).trans ((Equiv.refl α).sumCongr (Equiv.sumComm γ β))

theorem Complexity.ExactFourier.Layered.rect_first {α β γ : Type} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (G : Matrix α β ℂ) : (Matrix.reindex (Equiv.sumAssoc α β γ) (Equiv.sumAssoc α β γ)) (Matrix.fromBlocks (rectangularShear G) 0 0 1) = rectangularShear (G.fromCols 0)

theorem Complexity.ExactFourier.Layered.rect_last {α β γ : Type} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (G : Matrix α γ ℂ) : (Matrix.reindex swapLast swapLast) (Matrix.fromBlocks (rectangularShear G) 0 0 1) = rectangularShear (Matrix.fromCols 0 G)

theorem Complexity.ExactFourier.Layered.commutator_identity {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (G : Matrix α β ℂ) (H : Matrix β γ ℂ) : rectangularShear (G.fromCols 0) * Matrix.fromBlocks 1 0 0 (rectangularShear H) * rectangularShear ((-G).fromCols 0) * Matrix.fromBlocks 1 0 0 (rectangularShear (-H)) = rectangularShear (Matrix.fromCols 0 (G * H))

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

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

theorem Complexity.ExactFourier.Layered.embedded_injection {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (e : β ↪ α) : Embedded.matrix (e.sumMap (Function.Embedding.refl β)) (rectangularShear 1) = rectangularShear (Matrix.submatrix 1 id ⇑e)

theorem Complexity.ExactFourier.Layered.rect_injection {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : β ↪ α) : Layered (rectangularShear (Matrix.submatrix 1 id ⇑e)) 1

theorem Complexity.ExactFourier.Layered.rect_projection {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : β ↪ α) : Layered (rectangularShear (Matrix.submatrix 1 (⇑e) id)) 1

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