Exact Fourier circuits: pivot algebra

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

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

noncomputable def Complexity.ExactFourier.Pivot.matrix {α β : Type} [Fintype β] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : Matrix (α ⊕ β) (α ⊕ β) ℂ

The block pivot transform using the inverse of the lower-right block.

Equations

• Complexity.ExactFourier.Pivot.matrix A C B D = Matrix.fromBlocks (A - C * D⁻¹ * B) (C * D⁻¹) (-D⁻¹ * B) D⁻¹

theorem Complexity.ExactFourier.Pivot.factor {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : matrix A C B D = Matrix.fromBlocks A C 0 1 * Matrix.fromBlocks 1 0 (-D⁻¹ * B) D⁻¹

theorem Complexity.ExactFourier.Pivot.unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hA : IsUnit A) (hD : IsUnit D) : IsUnit (matrix A C B D)

theorem Complexity.ExactFourier.Pivot.solve {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hD : IsUnit D) : matrix A C B D * Matrix.fromBlocks 1 0 B D = Matrix.fromBlocks A C 0 1

theorem Complexity.ExactFourier.Pivot.involutive {α β : Type} [Fintype β] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hD : IsUnit D) : matrix (A - C * D⁻¹ * B) (C * D⁻¹) (-D⁻¹ * B) D⁻¹ = Matrix.fromBlocks A C B D

theorem Complexity.ExactFourier.Pivot.schur_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hD : IsUnit D) (hK : IsUnit (Matrix.fromBlocks A C B D)) : IsUnit (A - C * D⁻¹ * B)

theorem Complexity.ExactFourier.MatrixPrice.pair_le_two_of_entry (p : MatrixPrice) (A : Matrix (Fin 2) (Fin 2) ℂ) (hA : IsUnit A) (ha : A 0 0 ≠ 0) : p.value A ≤ 2

theorem Complexity.ExactFourier.MatrixPrice.pair_le_two (p : MatrixPrice) (A : Matrix (Fin 2) (Fin 2) ℂ) (hA : IsUnit A) : p.value A ≤ 2

def Complexity.ExactFourier.twoProdEquiv (β : Type) : Fin 2 × β ≃ β ⊕ β

Identify a two-valued coordinate tag with a sum of two copies of the coordinate type.

Equations

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

noncomputable def Complexity.ExactFourier.pairLayer {β : Type} [DecidableEq β] (A : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (β ⊕ β) (β ⊕ β) ℂ

Apply the same two-coordinate matrix to each pair of corresponding block coordinates.

Equations

• Complexity.ExactFourier.pairLayer A = (Matrix.reindex (Complexity.ExactFourier.twoProdEquiv β) (Complexity.ExactFourier.twoProdEquiv β)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1)

theorem Complexity.ExactFourier.pairLayer_eq {β : Type} [DecidableEq β] (A : Matrix (Fin 2) (Fin 2) ℂ) : pairLayer A = Matrix.fromBlocks (A 0 0 • 1) (A 0 1 • 1) (A 1 0 • 1) (A 1 1 • 1)

theorem Complexity.ExactFourier.pairLayer_unit {β : Type} [Fintype β] [DecidableEq β] (A : Matrix (Fin 2) (Fin 2) ℂ) (hA : IsUnit A) : IsUnit (pairLayer A)

theorem Complexity.ExactFourier.MatrixPrice.pair_layer {β : Type} [Fintype β] [DecidableEq β] (p : MatrixPrice) (A : Matrix (Fin 2) (Fin 2) ℂ) (hA : IsUnit A) : p.value (pairLayer A) ≤ 2 * ↑(Fintype.card β)

theorem Complexity.ExactFourier.exists_invertible_evaluation {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α (Polynomial ℂ)) (z0 : ℂ) (hG : IsUnit (G.map (Polynomial.eval z0))) (E : Finset ℂ) : ∃ s ∉ E, IsUnit (G.map (Polynomial.eval s))

noncomputable def Complexity.ExactFourier.Pivot.side {α β : Type} [DecidableEq α] [DecidableEq β] (L : Matrix (Fin 2) (Fin 2) ℂ) : Matrix ((α ⊕ β) ⊕ β) ((α ⊕ β) ⊕ β) ℂ

Extend a pair layer on the two state blocks by the identity on the data block.

Equations

• Complexity.ExactFourier.Pivot.side L = (Matrix.reindex (Equiv.sumAssoc α β β).symm (Equiv.sumAssoc α β β).symm) (Matrix.fromBlocks 1 0 0 (Complexity.ExactFourier.pairLayer L))

theorem Complexity.ExactFourier.Pivot.side_eq {α β : Type} [DecidableEq α] [DecidableEq β] (L : Matrix (Fin 2) (Fin 2) ℂ) : side L = Matrix.fromBlocks (Matrix.fromBlocks 1 0 0 (L 0 0 • 1)) (Matrix.fromRows 0 (L 0 1 • 1)) (Matrix.fromCols 0 (L 1 0 • 1)) (L 1 1 • 1)

theorem Complexity.ExactFourier.Pivot.side_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (L : Matrix (Fin 2) (Fin 2) ℂ) (hL : IsUnit L) : IsUnit (side L)

theorem Complexity.ExactFourier.Pivot.side_price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (L : Matrix (Fin 2) (Fin 2) ℂ) (hL : IsUnit L) : p.value (side L) ≤ 2 * ↑(Fintype.card β)

noncomputable def Complexity.ExactFourier.Pivot.middle {α β : Type} [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : Matrix ((α ⊕ β) ⊕ β) ((α ⊕ β) ⊕ β) ℂ

Place the original block matrix between the state coordinates used by the pivot.

Equations

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

theorem Complexity.ExactFourier.Pivot.middle_eq {α β : Type} [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : middle A C B D = Matrix.fromBlocks (Matrix.fromBlocks A 0 0 1) (C.fromRows 0) (B.fromCols 0) D

def Complexity.ExactFourier.Pivot.P (b : ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The two-coordinate pivot factor with entries [[b, 1], [1, 1]].

Equations

• Complexity.ExactFourier.Pivot.P b = !![b, 1; 1, 1]

def Complexity.ExactFourier.Pivot.Q (b : ℂ) : Matrix (Fin 2) (Fin 2) ℂ

The two-coordinate pivot factor with entries [[1, 1-b], [1, -b]].

Equations

• Complexity.ExactFourier.Pivot.Q b = !![1, 1 - b; 1, -b]

theorem Complexity.ExactFourier.Pivot.P_unit (b : ℂ) (hb : b ≠ 1) : IsUnit (P b)

theorem Complexity.ExactFourier.Pivot.Q_unit (b : ℂ) : IsUnit (Q b)

noncomputable def Complexity.ExactFourier.Pivot.data {α β : Type} [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) : Matrix (α ⊕ β) (α ⊕ β) ℂ

The data block of the parameterized pivot cell.

Equations

• Complexity.ExactFourier.Pivot.data A C B D b = Matrix.fromBlocks A C ((1 - b) • B) (b • 1 + (1 - b) • D)

noncomputable def Complexity.ExactFourier.Pivot.co {α β : Type} [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (b : ℂ) : Matrix (α ⊕ β) β ℂ

The block carrying the pivot cell's state contribution into its data coordinates.

Equations

• Complexity.ExactFourier.Pivot.co C D b = C.fromRows (1 + (1 - b) • D)

noncomputable def Complexity.ExactFourier.Pivot.bo {α β : Type} [DecidableEq β] (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) : Matrix β (α ⊕ β) ℂ

The block carrying the pivot cell's data contribution into its state coordinates.

Equations

• Complexity.ExactFourier.Pivot.bo B D b = (-b • B).fromCols (b • (1 - D))

noncomputable def Complexity.ExactFourier.Pivot.state {β : Type} [DecidableEq β] (D : Matrix β β ℂ) (b : ℂ) : Matrix β β ℂ

The pivot cell's state block 1 - b • D.

Equations

• Complexity.ExactFourier.Pivot.state D b = 1 - b • D

noncomputable def Complexity.ExactFourier.Pivot.cell {α β : Type} [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) : Matrix ((α ⊕ β) ⊕ β) ((α ⊕ β) ⊕ β) ℂ

Assemble the parameterized data, coupling, and state blocks into one pivot cell.

Equations

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

theorem Complexity.ExactFourier.Pivot.cell_eq {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) : cell A C B D b = side (Q b) * middle A C B D * side (P b)

theorem Complexity.ExactFourier.Pivot.cell_unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) (hb : b ≠ 1) (hK : IsUnit (Matrix.fromBlocks A C B D)) : IsUnit (cell A C B D b)

theorem Complexity.ExactFourier.Pivot.cell_price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) (hb : b ≠ 1) (hK : IsUnit (Matrix.fromBlocks A C B D)) : p.value (cell A C B D b) ≤ p.value (Matrix.fromBlocks A C B D) + 4 * ↑(Fintype.card β)

theorem Complexity.ExactFourier.Pivot.choose_data {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hK : IsUnit (Matrix.fromBlocks A C B D)) : ∃ (b : ℂ), b ≠ 0 ∧ b ≠ 1 ∧ IsUnit (data A C B D b)

theorem Complexity.ExactFourier.Pivot.denominator {β : Type} [DecidableEq β] (D : Matrix β β ℂ) (b : ℂ) : 1 - 1 • state D b = b • D

theorem Complexity.ExactFourier.Pivot.cell_feedback {α β : Type} [Fintype β] [DecidableEq β] (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (b : ℂ) (hb : b ≠ 0) (hD : IsUnit D) : CellPoly.feedback (data A C B D b) (co C D b) (bo B D b) (state D b) 1 = matrix A C B D

theorem Complexity.ExactFourier.MatrixPrice.pivot_bound {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (A : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (hA : IsUnit A) (hD : IsUnit D) (hK : IsUnit (Matrix.fromBlocks A C B D)) : p.value (Pivot.matrix A C B D) ≤ p.value (Matrix.fromBlocks A C B D) + 4 * ↑(Fintype.card β)