Exact Fourier circuits: symmetric laplacian

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

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

def Complexity.ExactFourier.SymLap.lap {α : Type} [DecidableEq α] (G : Matrix α α ℂ) : Matrix (α × α) (α × α) ℂ

The tensor difference G ⊗ 1 - 1 ⊗ G.

Equations

• Complexity.ExactFourier.SymLap.lap G = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) G 1 - Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 G

def Complexity.ExactFourier.SymLap.tensor {α : Type} (G : Matrix α α ℂ) : Matrix (α × α) (α × α) ℂ

The tensor square of the matrix G.

Equations

• Complexity.ExactFourier.SymLap.tensor G = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) G G

def Complexity.ExactFourier.SymLap.symmetrized {α : Type} [Fintype α] [DecidableEq α] (G J : Matrix α α ℂ) : Matrix (α × α) (α × α) ℂ

Multiply the tensor difference by the tensor square of the symmetrizing matrix.

Equations

• Complexity.ExactFourier.SymLap.symmetrized G J = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) J J * Complexity.ExactFourier.SymLap.lap G

theorem Complexity.ExactFourier.SymLap.tensor_square {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α ℂ) (hG : G * G = 1) : tensor G * tensor G = 1

theorem Complexity.ExactFourier.SymLap.lap_factor {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α ℂ) (hG : G * G = 1) : lap G = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) G 1 * (1 - tensor G)

theorem Complexity.ExactFourier.SymLap.lap_kill {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α ℂ) (hG : G * G = 1) : lap G * (1 + tensor G) = 0

theorem Complexity.ExactFourier.SymLap.symmetric {α : Type} [Fintype α] [DecidableEq α] (G J : Matrix α α ℂ) (s : ℂ) (hs : s * s = 1) (hJ : J.transpose = s • J) (hc : J * G = G.transpose * J) : (symmetrized G J).IsSymm

theorem Complexity.ExactFourier.SymLap.real_entries {α : Type} [Fintype α] [DecidableEq α] (G J : Matrix α α ℂ) (hG : ∀ (i j : α), star (G i j) = G i j) (hJ : ∀ (i j : α), star (J i j) = J i j) (i j : α × α) : star (symmetrized G J i j) = symmetrized G J i j

theorem Complexity.ExactFourier.SymLap.support_bound {α : Type} [Fintype α] [DecidableEq α] (G J : Matrix α α ℂ) (hJ : MonomialMatrix J) : nnz (symmetrized G J) ≤ 2 * nnz G * Fintype.card α

theorem Complexity.ExactFourier.det_ne_zero_of_eval_unit {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α (Polynomial ℂ)) (z0 : ℂ) (hG : IsUnit (G.map (Polynomial.eval z0))) : G.det ≠ 0

theorem Complexity.ExactFourier.unit_eval_of_not_mem_roots {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α (Polynomial ℂ)) (hG : G.det ≠ 0) (s : ℂ) (hs : s ∉ G.det.roots.toFinset) : IsUnit (G.map (Polynomial.eval s))

noncomputable def Complexity.ExactFourier.LinearProduct.factor {α : Type} [DecidableEq α] (A : Matrix α α ℂ) : Matrix α α (Polynomial ℂ)

The polynomial matrix 1 + X • A associated with one linear factor.

Equations

• Complexity.ExactFourier.LinearProduct.factor A = 1 + Polynomial.X • A.map ⇑Polynomial.C

def Complexity.ExactFourier.LinearProduct.product {α : Type} [Fintype α] [DecidableEq α] : List (Matrix α α ℂ) → Matrix α α (Polynomial ℂ)

Multiply the polynomial factors 1 + X • A in list order.

Equations

• Complexity.ExactFourier.LinearProduct.product [] = 1
• Complexity.ExactFourier.LinearProduct.product (a :: L) = Complexity.ExactFourier.LinearProduct.factor a * Complexity.ExactFourier.LinearProduct.product L

theorem Complexity.ExactFourier.LinearProduct.eval_factor {α : Type} [DecidableEq α] (A : Matrix α α ℂ) (s : ℂ) : (factor A).map ⇑(Polynomial.evalRingHom s) = 1 + s • A

@[simp]

theorem Complexity.ExactFourier.LinearProduct.coeff_zero_factor {α : Type} [DecidableEq α] (A : Matrix α α ℂ) : ((factor A).map fun (f : Polynomial ℂ) => f.coeff 0) = 1

@[simp]

theorem Complexity.ExactFourier.LinearProduct.coeff_one_factor {α : Type} [DecidableEq α] (A : Matrix α α ℂ) : ((factor A).map fun (f : Polynomial ℂ) => f.coeff 1) = A

theorem Complexity.ExactFourier.LinearProduct.coeff_one_mul {α : Type} [Fintype α] (A B : Matrix α α (Polynomial ℂ)) : ((A * B).map fun (f : Polynomial ℂ) => f.coeff 1) = ((A.map fun (f : Polynomial ℂ) => f.coeff 0) * B.map fun (f : Polynomial ℂ) => f.coeff 1) + (A.map fun (f : Polynomial ℂ) => f.coeff 1) * B.map fun (f : Polynomial ℂ) => f.coeff 0

theorem Complexity.ExactFourier.LinearProduct.eval_zero_product {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : (product L).map ⇑(Polynomial.evalRingHom 0) = 1

@[simp]

theorem Complexity.ExactFourier.LinearProduct.coeff_zero_product {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : ((product L).map fun (f : Polynomial ℂ) => f.coeff 0) = 1

@[simp]

theorem Complexity.ExactFourier.LinearProduct.coeff_one_product {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : ((product L).map fun (f : Polynomial ℂ) => f.coeff 1) = L.sum

noncomputable def Complexity.ExactFourier.LinearProduct.quotient {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : Matrix α α (Polynomial ℂ)

Remove the constant coefficient and divide each entry of the product by X.

Equations

• Complexity.ExactFourier.LinearProduct.quotient L = (Complexity.ExactFourier.LinearProduct.product L).map Polynomial.divX

theorem Complexity.ExactFourier.LinearProduct.eval_zero_quotient {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : (quotient L).map ⇑(Polynomial.evalRingHom 0) = L.sum

theorem Complexity.ExactFourier.LinearProduct.split_product {α : Type} [Fintype α] [DecidableEq α] (L : List (Matrix α α ℂ)) : product L = 1 + Polynomial.X • quotient L

theorem Complexity.ExactFourier.LinearProduct.eval_product_cost {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (L : List (Matrix α α ℂ)) (c : Matrix α α ℂ → ℝ) (s : ℂ) (hL : ∀ a ∈ L, IsUnit (1 + s • a) ∧ p.value (1 + s • a) ≤ c a) : IsUnit ((product L).map ⇑(Polynomial.evalRingHom s)) ∧ p.value ((product L).map ⇑(Polynomial.evalRingHom s)) ≤ (List.map c L).sum

structure Complexity.ExactFourier.SparseReflection.PairTerm (α : Type) : Type

Two distinct coordinates with nonzero coefficients for their opposing off-diagonal entries.

• i : α

  The first coordinate of the off-diagonal pair.

• j : α

  The second coordinate, distinct from the first.

• hij : self.i ≠ self.j
• a : ℂ

  The nonzero coefficient in the first-to-second matrix position.

• b : ℂ

  The nonzero coefficient in the second-to-first matrix position.

• ha : self.a ≠ 0
• hb : self.b ≠ 0

def Complexity.ExactFourier.SparseReflection.PairTerm.direction {α : Type} [DecidableEq α] (u : PairTerm α) : Matrix α α ℂ

The matrix supported on the two specified off-diagonal positions.

Equations

• u.direction = Matrix.single u.i u.j u.a + Matrix.single u.j u.i u.b

noncomputable def Complexity.ExactFourier.SparseReflection.PairTerm.den {α : Type} (u : PairTerm α) : Polynomial ℂ

The quadratic polynomial controlling invertibility of this pair perturbation.

Equations

• u.den = 1 - Polynomial.X ^ 2 * Polynomial.C (u.a * u.b)

theorem Complexity.ExactFourier.SparseReflection.PairTerm.den_ne {α : Type} (u : PairTerm α) : u.den ≠ 0

noncomputable def Complexity.ExactFourier.SparseReflection.PairTerm.bad {α : Type} (u : PairTerm α) : Finset ℂ

Zero and the roots of the pair's invertibility polynomial.

Equations

• u.bad = insert 0 u.den.roots.toFinset

theorem Complexity.ExactFourier.SparseReflection.PairTerm.price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (u : PairTerm α) (s : ℂ) (hs : s ∉ u.bad) : IsUnit (1 + s • u.direction) ∧ p.value (1 + s • u.direction) ≤ 3 / 2

theorem Complexity.ExactFourier.SparseReflection.pair_list_cost {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (L : List (PairTerm α)) : ∃ (E : Finset ℂ), ∀ s ∉ E, IsUnit ((LinearProduct.product (List.map PairTerm.direction L)).map ⇑(Polynomial.evalRingHom s)) ∧ p.value ((LinearProduct.product (List.map PairTerm.direction L)).map ⇑(Polynomial.evalRingHom s)) ≤ 3 / 2 * ↑L.length

theorem Complexity.ExactFourier.SparseReflection.diagonal_family {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (d : α → ℂ) : ∃ (E : Finset ℂ), ∀ s ∉ E, IsUnit (1 + s • Matrix.diagonal d) ∧ p.value (1 + s • Matrix.diagonal d) = 0

theorem Complexity.ExactFourier.SparseReflection.exists_tangent {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (d : α → ℂ) (L : List (PairTerm α)) : ∃ (Q : Matrix α α (Polynomial ℂ)) (E : Finset ℂ), Q.map ⇑(Polynomial.evalRingHom 0) = Matrix.diagonal d + (List.map PairTerm.direction L).sum ∧ ∀ s ∉ E, IsUnit (1 + s • Q.map ⇑(Polynomial.evalRingHom s)) ∧ p.value (1 + s • Q.map ⇑(Polynomial.evalRingHom s)) ≤ 3 / 2 * ↑L.length

The exact polynomial tangent used in the first sparse-reflection specialization.

noncomputable def Complexity.ExactFourier.MatrixPrice.cayley {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (t : ℂ) : Matrix α α ℂ

The matrix Cayley transform (1 + t • A) * (1 - t • A)⁻¹.

Equations

• Complexity.ExactFourier.MatrixPrice.cayley A t = (1 + t • A) * (1 - t • A)⁻¹

theorem Complexity.ExactFourier.MatrixPrice.cayley_unit {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (t : ℂ) (hp : IsUnit (1 + t • A)) (hm : IsUnit (1 - t • A)) : IsUnit (cayley A t)

theorem Complexity.ExactFourier.MatrixPrice.cayley_denominator {α : Type} [DecidableEq α] (A : Matrix α α ℂ) (e t : ℂ) (het : e + t ≠ 0) : 1 - (t / (e + t)) • (1 + e • A) = (e / (e + t)) • (1 - t • A)

theorem Complexity.ExactFourier.MatrixPrice.cayley_response {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (e t : ℂ) (he : e ≠ 0) (het : e + t ≠ 0) (hm : IsUnit (1 - t • A)) : CellPoly.feedback ((e - t) • 1) (1 + e • A) ((2 * e) • 1) (1 + e • A) (t / (e + t)) = (e + t) • cayley A t

theorem Complexity.ExactFourier.MatrixPrice.cayley_feedback {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (A : Matrix α α ℂ) (e t : ℂ) (he : e ≠ 0) (hep : e + t ≠ 0) (hem : e - t ≠ 0) (hK : IsUnit (1 + e • A)) (hp : IsUnit (1 + t • A)) (hm : IsUnit (1 - t • A)) : p.value (cayley A t) ≤ p.value (1 + e • A) + 2 * ↑(Fintype.card α)