Exact Fourier circuits: monomial feedback

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

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

theorem Complexity.ExactFourier.MatrixPrice.one_add_monomial {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (J : Matrix α α ℂ) (hJ : IsUnit J) (hmono : MonomialMatrix J) (hI : IsUnit (1 + J)) : p.value (1 + J) ≤ ↑(Fintype.card α)

theorem Complexity.ExactFourier.MatrixPrice.source_shear {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (U V : Matrix α α ℂ) (hU : IsUnit U) (hV : IsUnit V) (i j : α) (hij : i ≠ j) (c : ℂ) : p.value (V * (Matrix.transvection i j c * U)⁻¹) ≤ p.value (V * U⁻¹) + 1

theorem Complexity.ExactFourier.DensePair.four_price (p : MatrixPrice) (l : ℂ) (hl : l ≠ 0) (hl1 : l ≠ 1) : p.value (X l * (Y6 l)⁻¹) ≤ 6

def Complexity.ExactFourier.DensePair.rowY : Equiv.Perm (Fin 4)

The row permutation exchanging the last two coordinates of the pivot matrix.

Equations

• Complexity.ExactFourier.DensePair.rowY = { toFun := ![0, 1, 3, 2], invFun := ![0, 1, 3, 2], left_inv := ⋯, right_inv := ⋯ }

def Complexity.ExactFourier.DensePair.rowX : Equiv.Perm (Fin 4)

The row permutation exchanging the first pair and the last pair of coordinates.

Equations

• Complexity.ExactFourier.DensePair.rowX = { toFun := ![1, 0, 3, 2], invFun := ![1, 0, 3, 2], left_inv := ⋯, right_inv := ⋯ }

def Complexity.ExactFourier.DensePair.delta (l : ℂ) : Fin 4 → ℂ

The four-entry vector determining the pivot's rank-one correction.

Equations

• Complexity.ExactFourier.DensePair.delta l = ![-1, 1, l, -l]

def Complexity.ExactFourier.DensePair.signs : Fin 4 → ℂ

Alternating signs for the pivot's rank-one correction.

Equations

• Complexity.ExactFourier.DensePair.signs = ![1, -1, 1, -1]

noncomputable def Complexity.ExactFourier.DensePair.rankOne (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The identity plus the pivot correction delta l * signsᵀ / (1 - l).

Equations

• Complexity.ExactFourier.DensePair.rankOne l = 1 + Matrix.of fun (i j : Fin 4) => Complexity.ExactFourier.DensePair.delta l i * Complexity.ExactFourier.DensePair.signs j / (1 - l)

noncomputable def Complexity.ExactFourier.DensePair.scaled (l : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The four-coordinate matrix obtained after the first diagonal normalization.

Equations

• Complexity.ExactFourier.DensePair.scaled l = !![l, 1, 1, 1; 1, l, 1, 1; 1, 1, l⁻¹, 1; 1, 1, 1, l⁻¹]

def Complexity.ExactFourier.DensePair.scaled2 (u : ℂ) : Matrix (Fin 4) (Fin 4) ℂ

The four-coordinate matrix in the second normalization of the dense pair.

Equations

• Complexity.ExactFourier.DensePair.scaled2 u = !![1, u, u, 1; u, 1, u, 1; u, u, u ^ 2, 1; 1, 1, 1, 1]

def Complexity.ExactFourier.DensePair.B (u : ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The two-coordinate matrix with three unit entries and lower-right entry u.

Equations

• Complexity.ExactFourier.DensePair.B u = !![1, 1; 1, u]

theorem Complexity.ExactFourier.DensePair.rankOne_mul (l : ℂ) (hl1 : l ≠ 1) : rankOne l * (Y6 l).submatrix ⇑rowY ⇑(Equiv.refl (Fin 4)) = (X l).submatrix ⇑rowX ⇑(Equiv.refl (Fin 4))

noncomputable def Complexity.ExactFourier.DensePair.left1 (l : ℂ) : Fin 4 → ℂ

Left diagonal weights normalizing the rank-one pivot correction.

Equations

• Complexity.ExactFourier.DensePair.left1 l i = (1 - l) / Complexity.ExactFourier.DensePair.delta l i

theorem Complexity.ExactFourier.DensePair.left1_ne (l : ℂ) (hl : l ≠ 0) (hl1 : l ≠ 1) (i : Fin 4) : left1 l i ≠ 0

theorem Complexity.ExactFourier.DensePair.signs_ne (i : Fin 4) : signs i ≠ 0

theorem Complexity.ExactFourier.DensePair.scale1 (l : ℂ) (hl : l ≠ 0) (hl1 : l ≠ 1) : Matrix.diagonal (left1 l) * rankOne l * Matrix.diagonal signs = scaled l

noncomputable def Complexity.ExactFourier.DensePair.left2 (l : ℂ) : Fin 4 → ℂ

Left diagonal weights for the second normalization of the dense pair.

Equations

• Complexity.ExactFourier.DensePair.left2 l = ![l⁻¹, l⁻¹, l⁻¹, 1]

def Complexity.ExactFourier.DensePair.right2 (l : ℂ) : Fin 4 → ℂ

Right diagonal weights for the second normalization of the dense pair.

Equations

• Complexity.ExactFourier.DensePair.right2 l = ![1, 1, 1, l]

theorem Complexity.ExactFourier.DensePair.left2_ne (l : ℂ) (hl : l ≠ 0) (i : Fin 4) : left2 l i ≠ 0

theorem Complexity.ExactFourier.DensePair.right2_ne (l : ℂ) (hl : l ≠ 0) (i : Fin 4) : right2 l i ≠ 0

theorem Complexity.ExactFourier.DensePair.scale2 (l : ℂ) (hl : l ≠ 0) : Matrix.diagonal (left2 l) * scaled l * Matrix.diagonal (right2 l) = scaled2 l⁻¹

def Complexity.ExactFourier.DensePair.bitsRow : Fin 4 ≃ Fin 2 × Fin 2

Identify four row coordinates with pairs of bits in the chosen tensor order.

Equations

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

def Complexity.ExactFourier.DensePair.bitsCol : Fin 4 ≃ Fin 2 × Fin 2

Identify four column coordinates with pairs of bits in the chosen tensor order.

Equations

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

theorem Complexity.ExactFourier.DensePair.tensor_scaled (u : ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (B u) (B u)).submatrix ⇑bitsRow ⇑bitsCol = scaled2 u

theorem Complexity.ExactFourier.DensePair.B_unit (u : ℂ) (hu : u ≠ 1) : IsUnit (B u)

theorem Complexity.ExactFourier.DensePair.rankOne_price (p : MatrixPrice) (l : ℂ) (hl : l ≠ 0) (hl1 : l ≠ 1) : IsUnit (rankOne l) ∧ p.value (rankOne l) ≤ 6

theorem Complexity.ExactFourier.DensePair.normalized_price (p : MatrixPrice) (u : ℂ) (hu : u ≠ 0) (hu1 : u ≠ 1) : p.value (B u) ≤ 3 / 2

theorem Complexity.ExactFourier.DensePair.price (p : MatrixPrice) (H : Matrix (Fin 2) (Fin 2) ℂ) (hH : IsUnit H) (hdense : ∀ (i j : Fin 2), H i j ≠ 0) : p.value H ≤ 3 / 2

@[reducible, inline]

abbrev Complexity.ExactFourier.Embedded.complement {α β : Type} (e : β ↪ α) : Type

Coordinates outside the image of an embedding.

Equations

• Complexity.ExactFourier.Embedded.complement e = { a : α // a ∉ Set.range ⇑e }

@[instance_reducible]

noncomputable instance Complexity.ExactFourier.Embedded.instFintypeComplement {α β : Type} [Fintype α] (e : β ↪ α) : Fintype (complement e)

Equations

• Complexity.ExactFourier.Embedded.instFintypeComplement e = Fintype.ofFinite (Complexity.ExactFourier.Embedded.complement e)

@[instance_reducible]

noncomputable instance Complexity.ExactFourier.Embedded.instDecidableEqComplement {α β : Type} (e : β ↪ α) : DecidableEq (complement e)

Equations

• Complexity.ExactFourier.Embedded.instDecidableEqComplement e = Classical.decEq (Complexity.ExactFourier.Embedded.complement e)

noncomputable def Complexity.ExactFourier.Embedded.coordinates {α β : Type} (e : β ↪ α) : β ⊕ complement e ≃ α

Split the ambient coordinates into an embedding's image and its complement.

Equations

• Complexity.ExactFourier.Embedded.coordinates e = ((Equiv.ofInjective ⇑e ⋯).sumCongr (Equiv.refl (Complexity.ExactFourier.Embedded.complement e))).trans (Equiv.Set.sumCompl (Set.range ⇑e))

@[simp]

theorem Complexity.ExactFourier.Embedded.coordinates_inl {α β : Type} (e : β ↪ α) (i : β) : (coordinates e) (Sum.inl i) = e i

@[simp]

theorem Complexity.ExactFourier.Embedded.coordinates_inr {α β : Type} (e : β ↪ α) (i : complement e) : (coordinates e) (Sum.inr i) = ↑i

noncomputable def Complexity.ExactFourier.Embedded.matrix {α β : Type} (e : β ↪ α) (A : Matrix β β ℂ) : Matrix α α ℂ

Extend a matrix along an embedding, acting as the identity on unused coordinates.

Equations

• Complexity.ExactFourier.Embedded.matrix e A = (Matrix.reindex (Complexity.ExactFourier.Embedded.coordinates e) (Complexity.ExactFourier.Embedded.coordinates e)) (Matrix.fromBlocks A 0 0 1)

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

theorem Complexity.ExactFourier.Embedded.price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (e : β ↪ α) (A : Matrix β β ℂ) (hA : IsUnit A) : p.value (matrix e A) = p.value A

def Complexity.ExactFourier.Embedded.pair {α : Type} (i j : α) (hij : i ≠ j) : Fin 2 ↪ α

Embed two distinct selected coordinates as a copy of Fin 2.

Equations

• Complexity.ExactFourier.Embedded.pair i j hij = { toFun := fun (a : Fin 2) => if a = 0 then i else j, inj' := ⋯ }

@[simp]

theorem Complexity.ExactFourier.Embedded.pair_zero {α : Type} (i j : α) (hij : i ≠ j) : (pair i j hij) 0 = i

@[simp]

theorem Complexity.ExactFourier.Embedded.pair_one {α : Type} (i j : α) (hij : i ≠ j) : (pair i j hij) 1 = j

theorem Complexity.ExactFourier.Embedded.complement_ne_pair {α : Type} (i j : α) (hij : i ≠ j) (a : complement (pair i j hij)) : ↑a ≠ i ∧ ↑a ≠ j

theorem Complexity.ExactFourier.Embedded.pair_matrix {α : Type} [DecidableEq α] (i j : α) (hij : i ≠ j) (s t : ℂ) : matrix (pair i j hij) !![1, s; t, 1] = 1 + Matrix.single i j s + Matrix.single j i t

theorem Complexity.ExactFourier.Embedded.pair_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (i j : α) (hij : i ≠ j) (s t : ℂ) (hs : s ≠ 0) (ht : t ≠ 0) (hst : 1 - s * t ≠ 0) : IsUnit (1 + Matrix.single i j s + Matrix.single j i t) ∧ p.value (1 + Matrix.single i j s + Matrix.single j i t) ≤ 3 / 2