Exact Fourier circuits: monomial tools

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

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

theorem Complexity.ExactFourier.MonomialMatrix.mul {α : Type} [Fintype α] [DecidableEq α] {A B : Matrix α α ℂ} (hA : MonomialMatrix A) (hB : MonomialMatrix B) : MonomialMatrix (A * B)

theorem Complexity.ExactFourier.MonomialMatrix.unit {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : MonomialMatrix A) : IsUnit A

theorem Complexity.ExactFourier.MonomialMatrix.pow {α : Type} [Fintype α] [DecidableEq α] {A : Matrix α α ℂ} (hA : MonomialMatrix A) (n : ℕ) : MonomialMatrix (A ^ n)

theorem Complexity.ExactFourier.MonomialMatrix.tensor {α β : Type} [DecidableEq α] [DecidableEq β] {A : Matrix α α ℂ} {B : Matrix β β ℂ} (hA : MonomialMatrix A) (hB : MonomialMatrix B) : MonomialMatrix (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)

theorem Complexity.ExactFourier.MonomialMatrix.blockDiagonal {α β : Type} [DecidableEq α] [DecidableEq β] (A : β → Matrix α α ℂ) (hA : ∀ (b : β), MonomialMatrix (A b)) : MonomialMatrix (Matrix.blockDiagonal A)

A direct sum of signed monomials, indexed in (internal,block) order.

def Complexity.ExactFourier.permM {α : Type} [DecidableEq α] (e : Equiv.Perm α) : Matrix α α ℂ

The permutation matrix sending column j to row e j.

Equations

• Complexity.ExactFourier.permM e i j = if i = e j then 1 else 0

theorem Complexity.ExactFourier.permM_monomial {α : Type} [DecidableEq α] (e : Equiv.Perm α) : MonomialMatrix (permM e)

theorem Complexity.ExactFourier.permM_mul_apply {α : Type} [Fintype α] [DecidableEq α] (e : Equiv.Perm α) (X : Matrix α α ℂ) (i j : α) : (permM e * X) i j = X ((Equiv.symm e) i) j

theorem Complexity.ExactFourier.mul_permM_apply {α : Type} [Fintype α] [DecidableEq α] (e : Equiv.Perm α) (X : Matrix α α ℂ) (i j : α) : (X * permM e) i j = X i (e j)

theorem Complexity.ExactFourier.permM_inv {α : Type} [Fintype α] [DecidableEq α] (e : Equiv.Perm α) : (permM e)⁻¹ = permM (Equiv.symm e)

theorem Complexity.ExactFourier.permM_conj {α : Type} [Fintype α] [DecidableEq α] (e : Equiv.Perm α) (X : Matrix α α ℂ) : permM e * X * (permM e)⁻¹ = X.submatrix ⇑(Equiv.symm e) ⇑(Equiv.symm e)

theorem Complexity.ExactFourier.permM_conj_single {α : Type} [Fintype α] [DecidableEq α] (e : Equiv.Perm α) (i j : α) : permM e * Matrix.single i j 1 * (permM e)⁻¹ = Matrix.single (e i) (e j) 1

theorem Complexity.ExactFourier.exists_perm_pair {α : Type} [DecidableEq α] (i j a b : α) (hij : i ≠ j) (hab : a ≠ b) : ∃ (e : Equiv.Perm α), e i = a ∧ e j = b

@[simp]

theorem Complexity.ExactFourier.Embedded.matrix_coordinates {α β : Type} (e : β ↪ α) (A : Matrix β β ℂ) (i j : β ⊕ complement e) : matrix e A ((coordinates e) i) ((coordinates e) j) = Matrix.fromBlocks A 0 0 1 i j

@[simp]

theorem Complexity.ExactFourier.Embedded.matrix_on {α β : Type} (e : β ↪ α) (A : Matrix β β ℂ) (i j : β) : matrix e A (e i) (e j) = A i j

theorem Complexity.ExactFourier.Embedded.matrix_off_row {α β : Type} [DecidableEq α] (e : β ↪ α) (A : Matrix β β ℂ) (i j : α) (hi : i ∉ Set.range ⇑e) : matrix e A i j = if i = j then 1 else 0

theorem Complexity.ExactFourier.Embedded.matrix_off_col {α β : Type} [DecidableEq α] (e : β ↪ α) (A : Matrix β β ℂ) (i j : α) (hj : j ∉ Set.range ⇑e) : matrix e A i j = if i = j then 1 else 0

@[simp]

theorem Complexity.ExactFourier.Embedded.matrix_one {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : β ↪ α) : matrix e 1 = 1

theorem Complexity.ExactFourier.Embedded.matrix_mul {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : β ↪ α) (A B : Matrix β β ℂ) : matrix e (A * B) = matrix e A * matrix e B

theorem Complexity.ExactFourier.Embedded.matrix_comp {α β γ : Type} [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] (e : γ ↪ β) (f : β ↪ α) (A : Matrix γ γ ℂ) : matrix f (matrix e A) = matrix (e.trans f) A

@[simp]

theorem Complexity.ExactFourier.Embedded.matrix_equiv {α β : Type} (e : β ≃ α) (A : Matrix β β ℂ) : matrix e.toEmbedding A = (Matrix.reindex e e) A

theorem Complexity.ExactFourier.MonomialMatrix.reindex {α β : Type} [DecidableEq α] [DecidableEq β] (e : α ≃ β) {A : Matrix α α ℂ} (hA : MonomialMatrix A) : MonomialMatrix ((Matrix.reindex e e) A)

theorem Complexity.ExactFourier.MonomialMatrix.directSum {α β : Type} [DecidableEq α] [DecidableEq β] {A : Matrix α α ℂ} {B : Matrix β β ℂ} (hA : MonomialMatrix A) (hB : MonomialMatrix B) : MonomialMatrix (Matrix.fromBlocks A 0 0 B)

theorem Complexity.ExactFourier.MonomialMatrix.blockDiagonal' {π : Type} [DecidableEq π] {β : π → Type} [(i : π) → DecidableEq (β i)] (A : (i : π) → Matrix (β i) (β i) ℂ) (hA : ∀ (i : π), MonomialMatrix (A i)) : MonomialMatrix (Matrix.blockDiagonal' A)

theorem Complexity.ExactFourier.MonomialMatrix.embed {α β : Type} [DecidableEq α] [DecidableEq β] (e : β ↪ α) {A : Matrix β β ℂ} (hA : MonomialMatrix A) : MonomialMatrix (Embedded.matrix e A)

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

Exact positive pattern: k forward calls, interleaved with arbitrary monomials.

• zero {α : Type} [Fintype α] [DecidableEq α] {A : Matrix α α ℂ} (M : Matrix α α ℂ) (hM : MonomialMatrix M) : Pattern A 0 M
• succ {α : Type} [Fintype α] [DecidableEq α] {A : Matrix α α ℂ} {k : ℕ} {H : Matrix α α ℂ} (hH : Pattern A k H) (M : Matrix α α ℂ) (hM : MonomialMatrix M) : Pattern A (k + 1) (H * A * M)

def Complexity.ExactFourier.PositiveGeneration.Statement {α : Type} [Fintype α] [DecidableEq α] : Prop

Every nonmonomial invertible matrix generates all invertible matrices at one bounded positive length.

Equations

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

theorem Complexity.ExactFourier.PositiveGeneration.pattern_unit {α : Type} [Fintype α] [DecidableEq α] {A H : Matrix α α ℂ} {k : ℕ} (hA : IsUnit A) (h : Pattern A k H) : IsUnit H

theorem Complexity.ExactFourier.PositiveGeneration.monomial_of_projectors {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (hp : ∀ (k i j : α), i ≠ j → A i k * A⁻¹ k j = 0) : MonomialMatrix A

If every column projector is diagonal, the matrix is monomial.

theorem Complexity.ExactFourier.PositiveGeneration.exists_nondiagonal_projector {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) : ∃ (k : α) (i : α) (j : α), i ≠ j ∧ A i k * A⁻¹ k j ≠ 0

def Complexity.ExactFourier.PositiveGeneration.changeSign {α : Type} [DecidableEq α] (i : α) : Matrix α α ℂ

Negate one selected coordinate and leave every other coordinate unchanged.

Equations

• Complexity.ExactFourier.PositiveGeneration.changeSign i = Matrix.diagonal fun (j : α) => if j = i then -1 else 1

def Complexity.ExactFourier.PositiveGeneration.doubleCoord {α : Type} [DecidableEq α] (i : α) : Matrix α α ℂ

Double one selected coordinate and leave every other coordinate unchanged.

Equations

• Complexity.ExactFourier.PositiveGeneration.doubleCoord i = Matrix.diagonal fun (j : α) => if j = i then 2 else 1

theorem Complexity.ExactFourier.PositiveGeneration.changeSign_square {α : Type} [Fintype α] [DecidableEq α] (i : α) : changeSign i * changeSign i = 1

theorem Complexity.ExactFourier.PositiveGeneration.changeSign_inv {α : Type} [Fintype α] [DecidableEq α] (i : α) : (changeSign i)⁻¹ = changeSign i

theorem Complexity.ExactFourier.PositiveGeneration.changeSign_monomial {α : Type} [DecidableEq α] (i : α) : MonomialMatrix (changeSign i)

theorem Complexity.ExactFourier.PositiveGeneration.doubleCoord_monomial {α : Type} [DecidableEq α] (i : α) : MonomialMatrix (doubleCoord i)

theorem Complexity.ExactFourier.PositiveGeneration.doubleCoord_inv {α : Type} [Fintype α] [DecidableEq α] (i : α) : (doubleCoord i)⁻¹ = Matrix.diagonal fun (j : α) => if j = i then 1 / 2 else 1

def Complexity.ExactFourier.PositiveGeneration.cut {α : Type} [Fintype α] [DecidableEq α] (i : α) (X : Matrix α α ℂ) : Matrix α α ℂ

Subtract a sign-conjugate to isolate the selected row and column off the diagonal.

Equations

• Complexity.ExactFourier.PositiveGeneration.cut i X = X - Complexity.ExactFourier.PositiveGeneration.changeSign i * X * Complexity.ExactFourier.PositiveGeneration.changeSign i

theorem Complexity.ExactFourier.PositiveGeneration.cut_apply {α : Type} [Fintype α] [DecidableEq α] (i a b : α) (X : Matrix α α ℂ) : cut i X a b = if a = i ∧ b ≠ i ∨ a ≠ i ∧ b = i then 2 * X a b else 0

theorem Complexity.ExactFourier.PositiveGeneration.double_cut {α : Type} [Fintype α] [DecidableEq α] (i j : α) (hij : i ≠ j) (X : Matrix α α ℂ) : cut i (cut j X) = 4 • (X i j • Matrix.single i j 1 + X j i • Matrix.single j i 1)

theorem Complexity.ExactFourier.PositiveGeneration.isolate_identity {α : Type} [Fintype α] [DecidableEq α] (i j : α) (hij : i ≠ j) (X : Matrix α α ℂ) : doubleCoord i * cut i (cut j X) * (doubleCoord i)⁻¹ - (1 / 2) • cut i (cut j X) = (6 * X i j) • Matrix.single i j 1

theorem Complexity.ExactFourier.PositiveGeneration.single_mem_of_offdiagonal {α : Type} [Fintype α] [DecidableEq α] (V : Submodule ℂ (Matrix α α ℂ)) (hc : ∀ (M : Matrix α α ℂ), MonomialMatrix M → ∀ X ∈ V, M * X * M⁻¹ ∈ V) {X : Matrix α α ℂ} (hX : X ∈ V) (i j : α) (hij : i ≠ j) (hx : X i j ≠ 0) : Matrix.single i j 1 ∈ V