Exact Fourier circuits: signed price

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

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

@[instance_reducible]

def Complexity.ExactFourier.SignedBits.instLinearOrderSumBits (m : ℕ) : LinearOrder (Bits m ⊕ Bits m)

Use the next bit-string order on the sum representation of longer bit strings.

Equations

• Complexity.ExactFourier.SignedBits.instLinearOrderSumBits m = Complexity.ExactFourier.SignedBits.bitsLinearOrder (m + 1)

@[instance_reducible]

def Complexity.ExactFourier.SignedBits.instLTSumBits (m : ℕ) : LT (Bits m ⊕ Bits m)

Use the strict order induced by the next bit-string order.

Equations

• Complexity.ExactFourier.SignedBits.instLTSumBits m = (Complexity.ExactFourier.SignedBits.bitsLinearOrder (m + 1)).toLT

def Complexity.ExactFourier.SignedBits.start (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

The initial block matrix used to compare consecutive signed-bit constructions.

Equations

• Complexity.ExactFourier.SignedBits.start m = Matrix.fromBlocks (Complexity.ExactFourier.SignedBits.T m) 0 (Complexity.ExactFourier.SignedBits.T m) (Complexity.ExactFourier.SignedBits.T m)

def Complexity.ExactFourier.SignedBits.oldInputs (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

The input-side block factor retaining the previous signed-bit transformation.

Equations

• Complexity.ExactFourier.SignedBits.oldInputs m = Matrix.fromBlocks 1 0 (Complexity.ExactFourier.SignedBits.T m) (Complexity.ExactFourier.SignedBits.T m)

def Complexity.ExactFourier.SignedBits.oldOutputs (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

Apply the previous signed-bit transformation on the first block alone.

Equations

• Complexity.ExactFourier.SignedBits.oldOutputs m = Matrix.fromBlocks (Complexity.ExactFourier.SignedBits.T m) 0 0 1

noncomputable def Complexity.ExactFourier.SignedBits.transition (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

The transition matrix comparing the old input and output block factorizations.

Equations

• Complexity.ExactFourier.SignedBits.transition m = Matrix.fromBlocks (Complexity.ExactFourier.SignedBits.T m) 0 (-1) (Complexity.ExactFourier.SignedBits.T m)⁻¹

theorem Complexity.ExactFourier.SignedBits.start_lower (m : ℕ) : (start m).IsLowerTriangular

theorem Complexity.ExactFourier.SignedBits.start_diag (m : ℕ) (i : Bits (m + 1)) : start m i i = 1

def Complexity.ExactFourier.SignedBits.bottom (m : ℕ) : Finset (Bits (m + 1))

The coordinates in the lower half of the recursive bit-string representation.

Equations

• Complexity.ExactFourier.SignedBits.bottom m = {i : Complexity.ExactFourier.SignedBits.Bits (m + 1) | Sum.isRight i = true}

theorem Complexity.ExactFourier.SignedBits.input_rows (m : ℕ) : BasisExchange.rows (start m) (bottom m) = oldInputs m

theorem Complexity.ExactFourier.SignedBits.output_rows (m : ℕ) : BasisExchange.rows (start m) (bottom m)ᶜ = oldOutputs m

theorem Complexity.ExactFourier.SignedBits.transition_solve (m : ℕ) : transition m * oldInputs m = oldOutputs m

theorem Complexity.ExactFourier.SignedBits.transition_eq (m : ℕ) : transition m = oldOutputs m * (oldInputs m)⁻¹

def Complexity.ExactFourier.SignedBits.zdiag (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

The diagonal matrix that is positive on the first half and negative on the second.

Equations

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

theorem Complexity.ExactFourier.SignedBits.zdiag_monomial (m : ℕ) : MonomialMatrix (zdiag m)

theorem Complexity.ExactFourier.SignedBits.transition_sign (m : ℕ) : zdiag m * transition m * zdiag m = T (m + 1)

theorem Complexity.ExactFourier.SignedBits.start_tensor (m : ℕ) : start m = (Matrix.reindex (twoProdEquiv (Bits m)) (twoProdEquiv (Bits m))) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.transvection 1 0 1) (T m))

theorem Complexity.ExactFourier.SignedBits.price_step (p : MatrixPrice) (m : ℕ) : p.value (T (m + 1)) = 2 ^ m + 2 * p.value (T m)

theorem Complexity.ExactFourier.SignedBits.price (p : MatrixPrice) (m : ℕ) : 2 * p.value (T m) = ↑m * 2 ^ m

def Complexity.ExactFourier.SignedBits.J (m : ℕ) : Bool → Matrix (Bits m) (Bits m) ℂ

Recursive signed coordinate swaps indexed by a Boolean choice of sign convention.

Equations

• Complexity.ExactFourier.SignedBits.J 0 x✝ = 1
• Complexity.ExactFourier.SignedBits.J m.succ false = Matrix.fromBlocks 0 (Complexity.ExactFourier.SignedBits.J m true) (Complexity.ExactFourier.SignedBits.J m true) 0
• Complexity.ExactFourier.SignedBits.J m.succ true = Matrix.fromBlocks 0 (Complexity.ExactFourier.SignedBits.J m false) (-Complexity.ExactFourier.SignedBits.J m false) 0

theorem Complexity.ExactFourier.SignedBits.J_commute (m : ℕ) (b : Bool) : J m b * D m = (if b = true then -(D m).transpose else (D m).transpose) * J m b

theorem Complexity.ExactFourier.SignedBits.J_orthogonal (m : ℕ) (b : Bool) : J m b * (J m b).transpose = 1

theorem Complexity.ExactFourier.SignedBits.J_sign (m : ℕ) (b : Bool) : ∃ (s : ℂ), s * s = 1 ∧ (J m b).transpose = s • J m b

theorem Complexity.ExactFourier.SignedBits.offDiagonal_monomial {α : Type} [DecidableEq α] {A : Matrix α α ℂ} (hA : MonomialMatrix A) (s : ℂ) (hs : s ≠ 0) : MonomialMatrix (Matrix.fromBlocks 0 A (s • A) 0)

theorem Complexity.ExactFourier.SignedBits.J_monomial (m : ℕ) (b : Bool) : MonomialMatrix (J m b)

def Complexity.ExactFourier.SignedBits.Gamma (m : ℕ) : Matrix (Bits (m + 1)) (Bits (m + 1)) ℂ

The signed-bit involution with diagonal blocks D m and -D m.

Equations

• Complexity.ExactFourier.SignedBits.Gamma m = Matrix.fromBlocks (Complexity.ExactFourier.SignedBits.D m) 1 1 (-Complexity.ExactFourier.SignedBits.D m)

theorem Complexity.ExactFourier.SignedBits.Gamma_square (m : ℕ) : Gamma m * Gamma m = 1

theorem Complexity.ExactFourier.SignedBits.Gamma_unit (m : ℕ) : IsUnit (Gamma m)

theorem Complexity.ExactFourier.SignedBits.Gamma_symmetry (m : ℕ) : J (m + 1) false * Gamma m = (Gamma m).transpose * J (m + 1) false

theorem Complexity.ExactFourier.SignedBits.D_star (m : ℕ) (i j : Bits m) : star (D m i j) = D m i j

theorem Complexity.ExactFourier.SignedBits.J_star (m : ℕ) (b : Bool) (i j : Bits m) : star (J m b i j) = J m b i j

theorem Complexity.ExactFourier.SignedBits.Gamma_star (m : ℕ) (i j : Bits (m + 1)) : star (Gamma m i j) = Gamma m i j

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

The finite set of matrix positions with nonzero entries.

Equations

• Complexity.ExactFourier.support A = {ij : α × β | A ij.1 ij.2 ≠ 0}

noncomputable def Complexity.ExactFourier.nnz {α β : Type} [Fintype α] [Fintype β] (A : Matrix α β ℂ) : ℕ

The number of nonzero entries in a finite matrix.

Equations

• Complexity.ExactFourier.nnz A = (Complexity.ExactFourier.support A).card

@[simp]

theorem Complexity.ExactFourier.mem_support {α β : Type} [Fintype α] [Fintype β] (A : Matrix α β ℂ) (ij : α × β) : ij ∈ support A ↔ A ij.1 ij.2 ≠ 0

@[simp]

theorem Complexity.ExactFourier.nnz_zero {α β : Type} [Fintype α] [Fintype β] : nnz 0 = 0

@[simp]

theorem Complexity.ExactFourier.nnz_neg {α β : Type} [Fintype α] [Fintype β] (A : Matrix α β ℂ) : nnz (-A) = nnz A

theorem Complexity.ExactFourier.nnz_add_le {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A B : Matrix α β ℂ) : nnz (A + B) ≤ nnz A + nnz B

theorem Complexity.ExactFourier.nnz_sub_le {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (A B : Matrix α β ℂ) : nnz (A - B) ≤ nnz A + nnz B

@[simp]

theorem Complexity.ExactFourier.nnz_one {α : Type} [Fintype α] [DecidableEq α] : nnz 1 = Fintype.card α

theorem Complexity.ExactFourier.nnz_kronecker {α β : Type} [Fintype α] [Fintype β] (A : Matrix α α ℂ) (B : Matrix β β ℂ) : nnz (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B) = nnz A * nnz B

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

theorem Complexity.ExactFourier.nnz_sum {α β : Type} [Fintype α] [Fintype β] (A : Matrix α β ℂ) : nnz A = ∑ i : α, ∑ j : β, if A i j = 0 then 0 else 1

theorem Complexity.ExactFourier.nnz_fromBlocks {α β : Type} [Fintype α] [Fintype β] (A : Matrix α α ℂ) (B : Matrix α β ℂ) (C : Matrix β α ℂ) (D : Matrix β β ℂ) : nnz (Matrix.fromBlocks A B C D) = nnz A + nnz B + nnz C + nnz D

theorem Complexity.ExactFourier.SignedBits.D_count (m : ℕ) : 2 * nnz (D m) = m * 2 ^ m

theorem Complexity.ExactFourier.SignedBits.Gamma_count (m : ℕ) : nnz (Gamma m) = (m + 2) * 2 ^ m

noncomputable def Complexity.ExactFourier.Similarity.conj {α : Type} [Fintype α] [DecidableEq α] (U A : Matrix α α ℂ) : Matrix α α ℂ

Conjugate a matrix by U, using the nonsingular matrix inverse.

Equations

• Complexity.ExactFourier.Similarity.conj U A = U * A * U⁻¹

theorem Complexity.ExactFourier.Similarity.one {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) : conj U 1 = 1

theorem Complexity.ExactFourier.Similarity.add {α : Type} [Fintype α] [DecidableEq α] (U A B : Matrix α α ℂ) : conj U (A + B) = conj U A + conj U B

theorem Complexity.ExactFourier.Similarity.sub {α : Type} [Fintype α] [DecidableEq α] (U A B : Matrix α α ℂ) : conj U (A - B) = conj U A - conj U B

theorem Complexity.ExactFourier.Similarity.smul {α : Type} [Fintype α] [DecidableEq α] (U A : Matrix α α ℂ) (c : ℂ) : conj U (c • A) = c • conj U A

theorem Complexity.ExactFourier.Similarity.zero {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) : conj U 0 = 0

theorem Complexity.ExactFourier.Similarity.mul {α : Type} [Fintype α] [DecidableEq α] (U A B : Matrix α α ℂ) (hU : IsUnit U) : conj U A * conj U B = conj U (A * B)

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

theorem Complexity.ExactFourier.Similarity.diagonal_linear {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) (t : ℂ) : 1 + t • conj U (Matrix.diagonal a) = conj U (Matrix.diagonal fun (i : α) => 1 + t * a i)

theorem Complexity.ExactFourier.Similarity.diagonal_linear_sub {α : Type} [Fintype α] [DecidableEq α] (U : Matrix α α ℂ) (hU : IsUnit U) (a : α → ℂ) (t : ℂ) : 1 - t • conj U (Matrix.diagonal a) = conj U (Matrix.diagonal fun (i : α) => 1 - t * a i)

def Complexity.ExactFourier.RealMatrix.complex {α : Type} (A : Matrix α α ℝ) : Matrix α α ℂ

View a real matrix as a complex matrix by embedding each entry.

Equations

• Complexity.ExactFourier.RealMatrix.complex A = A.map Complex.ofReal

theorem Complexity.ExactFourier.RealMatrix.map_mul {α : Type} [Fintype α] (A B : Matrix α α ℝ) : complex (A * B) = complex A * complex B

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_one {α : Type} [DecidableEq α] : complex 1 = 1

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_zero {α : Type} : complex 0 = 0

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_transpose {α : Type} (A : Matrix α α ℝ) : complex A.transpose = (complex A).transpose

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_diagonal {α : Type} [DecidableEq α] (d : α → ℝ) : complex (Matrix.diagonal d) = Matrix.diagonal fun (i : α) => ↑(d i)

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_add {α : Type} (A B : Matrix α α ℝ) : complex (A + B) = complex A + complex B

@[simp]

theorem Complexity.ExactFourier.RealMatrix.map_sub {α : Type} (A B : Matrix α α ℝ) : complex (A - B) = complex A - complex B

theorem Complexity.ExactFourier.RealMatrix.unit {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℝ) (h : IsUnit A) : IsUnit (complex A)

theorem Complexity.ExactFourier.RealMatrix.inv {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℝ) (h : IsUnit A) : complex A⁻¹ = (complex A)⁻¹

theorem Complexity.ExactFourier.RealMatrix.diagonalization {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℝ) (hA : A.IsSymm) : ∃ (U : Matrix α α ℝ) (a : α → ℝ), IsUnit U ∧ U⁻¹ = U.transpose ∧ A = U * Matrix.diagonal a * U⁻¹

theorem Complexity.ExactFourier.RealMatrix.complex_re {α : Type} (A : Matrix α α ℂ) (hA : ∀ (i j : α), star (A i j) = A i j) : complex (A.map Complex.re) = A

theorem Complexity.ExactFourier.RealMatrix.re_symm {α : Type} (A : Matrix α α ℂ) (hA : A.IsSymm) : (A.map Complex.re).IsSymm