Exact Fourier circuits: sparse spectral

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

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

theorem Complexity.ExactFourier.SparseReflection.spectral_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (A : Matrix α α ℝ) (hA : A.IsSymm) (d : α → ℂ) (L : List (PairTerm α)) (hL : RealMatrix.complex A = Matrix.diagonal d + (List.map PairTerm.direction L).sum) : ∃ (R : Matrix α α ℂ) (T : Matrix α α ℂ), R * R = 1 ∧ R.IsSymm ∧ RealMatrix.complex A * (1 + R) = 0 ∧ 1 - R = RealMatrix.complex A * T ∧ p.value R ≤ 3 / 2 * ↑L.length + 2 * ↑(Fintype.card α)

Algebraic certificate for the real orthogonal reflection in the kernel, together with its uniform sparse price. Both annihilator equations are retained.

noncomputable def Complexity.ExactFourier.SparseReflection.pairs {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) : Finset (α × α)

Strictly upper-triangular positions carrying nonzero entries.

Equations

• Complexity.ExactFourier.SparseReflection.pairs A = {ij : α × α | ij.1 < ij.2 ∧ A ij.1 ij.2 ≠ 0}

@[simp]

theorem Complexity.ExactFourier.SparseReflection.mem_pairs {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (ij : α × α) : ij ∈ pairs A ↔ ij.1 < ij.2 ∧ A ij.1 ij.2 ≠ 0

def Complexity.ExactFourier.SparseReflection.term {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) (ij : ↥(pairs A)) : PairTerm α

The pair term associated with one nonzero off-diagonal entry of a symmetric matrix.

Equations

• Complexity.ExactFourier.SparseReflection.term A hA ij = { i := (↑ij).1, j := (↑ij).2, hij := ⋯, a := A (↑ij).1 (↑ij).2, b := A (↑ij).2 (↑ij).1, ha := ⋯, hb := ⋯ }

noncomputable def Complexity.ExactFourier.SparseReflection.terms {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) : List (PairTerm α)

List the pair terms corresponding to all nonzero upper-triangular entries.

Equations

• Complexity.ExactFourier.SparseReflection.terms A hA = List.map (Complexity.ExactFourier.SparseReflection.term A hA) (Complexity.ExactFourier.SparseReflection.pairs A).attach.toList

@[simp]

theorem Complexity.ExactFourier.SparseReflection.terms_length {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) : (terms A hA).length = (pairs A).card

theorem Complexity.ExactFourier.SparseReflection.terms_sum {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) : (List.map PairTerm.direction (terms A hA)).sum = ∑ ij ∈ pairs A, (Matrix.single ij.1 ij.2 (A ij.1 ij.2) + Matrix.single ij.2 ij.1 (A ij.2 ij.1))

theorem Complexity.ExactFourier.SparseReflection.decomposition {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) : A = (Matrix.diagonal fun (i : α) => A i i) + (List.map PairTerm.direction (terms A hA)).sum

theorem Complexity.ExactFourier.SparseReflection.twice_pairs_le {α : Type} [Fintype α] [LinearOrder α] (A : Matrix α α ℂ) (hA : A.IsSymm) : 2 * (pairs A).card ≤ nnz A

theorem Complexity.ExactFourier.SparseReflection.exists_reflection {α : Type} [Fintype α] [LinearOrder α] (p : MatrixPrice) (A : Matrix α α ℂ) (hA : A.IsSymm) (hreal : ∀ (i j : α), star (A i j) = A i j) : ∃ (R : Matrix α α ℂ) (T : Matrix α α ℂ), R * R = 1 ∧ R.IsSymm ∧ A * (1 + R) = 0 ∧ 1 - R = A * T ∧ p.value R ≤ 3 / 2 * ↑(pairs A).card + 2 * ↑(Fintype.card α)

Uniform sparse reflection certificate, with supported unordered pairs counted exactly. The annihilator identities characterize the reflection when A is real symmetric.

theorem Complexity.ExactFourier.SparseReflection.exists_reflection_nnz {α : Type} [Fintype α] [LinearOrder α] (p : MatrixPrice) (A : Matrix α α ℂ) (hA : A.IsSymm) (hreal : ∀ (i j : α), star (A i j) = A i j) : ∃ (R : Matrix α α ℂ) (T : Matrix α α ℂ), R * R = 1 ∧ R.IsSymm ∧ A * (1 + R) = 0 ∧ 1 - R = A * T ∧ p.value R ≤ 3 / 4 * ↑(nnz A) + 2 * ↑(Fintype.card α)

theorem Complexity.ExactFourier.SymLap.relations {α : Type} [Fintype α] [DecidableEq α] (G J R T M A : Matrix α α ℂ) (hJ : IsUnit J) (hG : IsUnit G) (hA : A = J * G * (1 - M)) (hs : A.IsSymm) (hk : A * (1 + M) = 0) (hp : A * (1 + R) = 0) (hm : 1 - R = A * T) : M * (1 + R) = 1 + R ∧ M.transpose * (1 - R) = -(1 - R)

theorem Complexity.ExactFourier.SymLap.exists_tensor_reflection {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G J : Matrix α α ℂ) (hG : G * G = 1) (hJ : MonomialMatrix J) (s : ℂ) (hs : s * s = 1) (ht : J.transpose = s • J) (hc : J * G = G.transpose * J) (hrG : ∀ (i j : α), star (G i j) = G i j) (hrJ : ∀ (i j : α), star (J i j) = J i j) : ∃ (R : Matrix (α × α) (α × α) ℂ), R * R = 1 ∧ R.IsSymm ∧ tensor G * (1 + R) = 1 + R ∧ (tensor G).transpose * (1 - R) = -(1 - R) ∧ p.value R ≤ 3 / 4 * (2 * ↑(nnz G) * ↑(Fintype.card α)) + 2 * ↑(Fintype.card α) ^ 2

def Complexity.ExactFourier.SignedBits.parity (m : ℕ) : Bits m → Bool

The parity of a recursively represented bit string.

Equations

• Complexity.ExactFourier.SignedBits.parity 0 x_2 = false
• Complexity.ExactFourier.SignedBits.parity m.succ (Sum.inl i) = Complexity.ExactFourier.SignedBits.parity m i
• Complexity.ExactFourier.SignedBits.parity m.succ (Sum.inr i) = !Complexity.ExactFourier.SignedBits.parity m i

theorem Complexity.ExactFourier.SignedBits.D_parity (m : ℕ) (i j : Bits m) : parity m i = parity m j → D m i j = 0

theorem Complexity.ExactFourier.SignedBits.Gamma_parity (m : ℕ) (i j : Bits (m + 1)) : parity (m + 1) i = parity (m + 1) j → Gamma m i j = 0

def Complexity.ExactFourier.SignedBits.paritySwitch (m : ℕ) : Bits (m + 1) → Bits (m + 1)

Exchange the two halves precisely when the shorter bit string has odd parity.

Equations

• Complexity.ExactFourier.SignedBits.paritySwitch m (Sum.inl i) = if Complexity.ExactFourier.SignedBits.parity m i = true then Sum.inr i else Sum.inl i
• Complexity.ExactFourier.SignedBits.paritySwitch m (Sum.inr i) = if Complexity.ExactFourier.SignedBits.parity m i = true then Sum.inl i else Sum.inr i

theorem Complexity.ExactFourier.SignedBits.paritySwitch_involutive (m : ℕ) : Function.Involutive (paritySwitch m)

def Complexity.ExactFourier.SignedBits.parityEquiv (m : ℕ) : Bits m ⊕ Bits m ≃ Bits (m + 1)

Reorder bit strings so that the two halves separate even and odd parity.

Equations

• Complexity.ExactFourier.SignedBits.parityEquiv m = Function.Involutive.toPerm (Complexity.ExactFourier.SignedBits.paritySwitch m) ⋯

theorem Complexity.ExactFourier.SignedBits.parityEquiv_left (m : ℕ) (i : Bits m) : parity (m + 1) ((parityEquiv m) (Sum.inl i)) = false

theorem Complexity.ExactFourier.SignedBits.parityEquiv_right (m : ℕ) (i : Bits m) : parity (m + 1) ((parityEquiv m) (Sum.inr i)) = true

def Complexity.ExactFourier.GraphReflection.swap {α : Type} [DecidableEq α] : Matrix (α ⊕ α) (α ⊕ α) ℂ

Exchange the two equal-sized coordinate blocks.

Equations

• Complexity.ExactFourier.GraphReflection.swap = Matrix.fromBlocks 0 1 1 0

theorem Complexity.ExactFourier.GraphReflection.swap_monomial {α : Type} [DecidableEq α] : MonomialMatrix swap

theorem Complexity.ExactFourier.GraphReflection.swap_square {α : Type} [Fintype α] [DecidableEq α] : swap * swap = 1

def Complexity.ExactFourier.GraphReflection.hadamard {α : Type} [DecidableEq α] : Matrix (α ⊕ α) (α ⊕ α) ℂ

Apply a two-coordinate Hadamard transform to each pair of corresponding coordinates.

Equations

• Complexity.ExactFourier.GraphReflection.hadamard = Matrix.fromBlocks 1 1 1 (-1)

theorem Complexity.ExactFourier.GraphReflection.hadamard_square {α : Type} [Fintype α] [DecidableEq α] : hadamard * hadamard = 2 • 1

theorem Complexity.ExactFourier.GraphReflection.hadamard_unit {α : Type} [Fintype α] [DecidableEq α] : IsUnit hadamard

theorem Complexity.ExactFourier.GraphReflection.hadamard_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) : p.value hadamard ≤ 2 * ↑(Fintype.card α)

noncomputable def Complexity.ExactFourier.GraphReflection.graph {α : Type} [Fintype α] [DecidableEq α] (B : Matrix α α ℂ) : Matrix (α ⊕ α) (α ⊕ α) ℂ

The block involution with off-diagonal blocks B and B⁻¹.

Equations

• Complexity.ExactFourier.GraphReflection.graph B = Matrix.fromBlocks 0 B B⁻¹ 0

theorem Complexity.ExactFourier.GraphReflection.graph_square {α : Type} [Fintype α] [DecidableEq α] (B : Matrix α α ℂ) (hB : IsUnit B) : graph B * graph B = 1

theorem Complexity.ExactFourier.GraphReflection.graph_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (B : Matrix α α ℂ) (hB : IsUnit B) : p.value (graph B) = 2 * p.value B

theorem Complexity.ExactFourier.GraphReflection.gram_unit {α : Type} [Fintype α] [DecidableEq α] (B : Matrix α α ℂ) (hB : ∀ (i j : α), star (B i j) = B i j) : IsUnit (1 + B.transpose * B)

@[reducible, inline]

abbrev Complexity.ExactFourier.SignedBits.Half (m : ℕ) : Type

One parity half of the tensor-square bit-string coordinate space.

Equations

• Complexity.ExactFourier.SignedBits.Half m = (Complexity.ExactFourier.SignedBits.Bits m × Complexity.ExactFourier.SignedBits.Bits (m + 1))

def Complexity.ExactFourier.SignedBits.tensorParityEquiv (m : ℕ) : Half m ⊕ Half m ≃ Bits (m + 1) × Bits (m + 1)

Regroup tensor-square coordinates by the parity of the first factor.

Equations

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

def Complexity.ExactFourier.SignedBits.parityTensor (m : ℕ) : Matrix (Half m ⊕ Half m) (Half m ⊕ Half m) ℂ

The signed tensor involution written in coordinates grouped by parity.

Equations

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

theorem Complexity.ExactFourier.SignedBits.parityTensor_square (m : ℕ) : parityTensor m * parityTensor m = 1

theorem Complexity.ExactFourier.SignedBits.parityTensor_diag_left (m : ℕ) : (parityTensor m).toBlocks₁₁ = 0

theorem Complexity.ExactFourier.SignedBits.parityTensor_diag_right (m : ℕ) : (parityTensor m).toBlocks₂₂ = 0

def Complexity.ExactFourier.SignedBits.graphB (m : ℕ) : Matrix (Half m) (Half m) ℂ

The upper-right block of the parity decomposition of the signed tensor involution.

Equations

• Complexity.ExactFourier.SignedBits.graphB m = (Complexity.ExactFourier.SignedBits.parityTensor m).toBlocks₁₂

theorem Complexity.ExactFourier.SignedBits.graphB_unit (m : ℕ) : IsUnit (graphB m)

theorem Complexity.ExactFourier.SignedBits.parityTensor_graph (m : ℕ) : parityTensor m = GraphReflection.graph (graphB m)

theorem Complexity.ExactFourier.SignedBits.graphB_real (m : ℕ) (i j : Half m) : star (graphB m i j) = graphB m i j