Exact Fourier circuits: raw positive

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

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

theorem Complexity.ExactFourier.Packing.RawPrice.embedded (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) (M : Matrix α α ℂ) (hM : IsUnit M) : p.value (Embedded.matrix e M) = p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.zero_iff (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : p.value M = 0 ↔ MonomialMatrix M

theorem Complexity.ExactFourier.MonomialMatrix.transpose {α : Type} [DecidableEq α] {M : Matrix α α ℂ} (hM : MonomialMatrix M) : MonomialMatrix M.transpose

theorem Complexity.ExactFourier.MatrixSymmetry.unit_transpose {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : IsUnit M.transpose

theorem Complexity.ExactFourier.MatrixSymmetry.inverse_tensor {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N)⁻¹ = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M⁻¹ N⁻¹

theorem Complexity.ExactFourier.MatrixSymmetry.inverse_sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : (Matrix.fromBlocks M 0 0 N)⁻¹ = Matrix.fromBlocks M⁻¹ 0 0 N⁻¹

theorem Complexity.ExactFourier.MatrixSymmetry.inverse_reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) (M : Matrix α α ℂ) (hM : IsUnit M) : ((Matrix.reindex e e) M)⁻¹ = (Matrix.reindex e e) M⁻¹

theorem Complexity.ExactFourier.MatrixSymmetry.transpose_tensor {α β : Type} (M : Matrix α α ℂ) (N : Matrix β β ℂ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).transpose = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M.transpose N.transpose

noncomputable def Complexity.ExactFourier.Packing.RawPrice.symValue (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) : ℝ

Average the raw prices of a matrix, its inverse, its transpose, and inverse transpose.

Equations

• p.symValue M = (p.value M + p.value M⁻¹ + p.value M.transpose + p.value M.transpose⁻¹) / 4

theorem Complexity.ExactFourier.Packing.RawPrice.sym_nonneg (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : 0 ≤ p.symValue M

theorem Complexity.ExactFourier.Packing.RawPrice.sym_zero (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : p.symValue M = 0 ↔ MonomialMatrix M

theorem Complexity.ExactFourier.Packing.RawPrice.sym_reindex (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) (M : Matrix α α ℂ) (hM : IsUnit M) : p.symValue ((Matrix.reindex e e) M) = p.symValue M

theorem Complexity.ExactFourier.Packing.RawPrice.sym_mul (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M N : Matrix α α ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.symValue (M * N) ≤ p.symValue M + p.symValue N

theorem Complexity.ExactFourier.Packing.RawPrice.sym_monomial (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M L R : Matrix α α ℂ) (hM : IsUnit M) (hL : MonomialMatrix L) (hR : MonomialMatrix R) : p.symValue (L * M * R) = p.symValue M

theorem Complexity.ExactFourier.Packing.RawPrice.sym_tensor (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.symValue (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) = ↑(Fintype.card β) * p.symValue M + ↑(Fintype.card α) * p.symValue N

theorem Complexity.ExactFourier.Packing.RawPrice.sym_sum (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.symValue (Matrix.fromBlocks M 0 0 N) = p.symValue M + p.symValue N

theorem Complexity.ExactFourier.Packing.RawPrice.sym_inverse (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : p.symValue M⁻¹ = p.symValue M

theorem Complexity.ExactFourier.Packing.RawPrice.sym_transpose (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) : p.symValue M.transpose = p.symValue M

theorem Complexity.ExactFourier.Packing.RawPrice.shear_inverse (p : RawPrice) : p.value shearU⁻¹ = 1

theorem Complexity.ExactFourier.Packing.RawPrice.shear_transpose (p : RawPrice) : p.value shearU.transpose = 1

theorem Complexity.ExactFourier.Packing.RawPrice.shear_transpose_inverse (p : RawPrice) : p.value shearU.transpose⁻¹ = 1

theorem Complexity.ExactFourier.Packing.RawPrice.sym_normalized (p : RawPrice) : p.symValue shearU = 1

noncomputable def Complexity.ExactFourier.Packing.RawPrice.toMatrixPrice (p : RawPrice) : MatrixPrice

The matrix price obtained by symmetrizing a raw comparison price.

Equations

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

def Complexity.ExactFourier.BasisExchange.rows {ι : Type} [DecidableEq ι] (K : Matrix ι ι ℂ) (H : Finset ι) : Matrix ι ι ℂ

Keep the selected rows of K and use identity rows at all remaining positions.

Equations

• Complexity.ExactFourier.BasisExchange.rows K H i j = if i ∈ H then K i j else 1 i j

theorem Complexity.ExactFourier.BasisExchange.rows_insert {ι : Type} [Fintype ι] [DecidableEq ι] (K : Matrix ι ι ℂ) (H : Finset ι) (j : ι) (hj : j ∉ H) : (rows K H).updateRow j (rows K Hᶜ j) = rows K (insert j H) ∧ (rows K Hᶜ).updateRow j (rows K H j) = rows K (insert j H)ᶜ

theorem Complexity.ExactFourier.BasisExchange.price_many {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (K : Matrix ι ι ℂ) (hU : ∀ (H : Finset ι), IsUnit (rows K H)) (H : Finset ι) : p.value (rows K Hᶜ * (rows K H)⁻¹) = p.value K

theorem Complexity.ExactFourier.BasisExchange.rows_unit {ι : Type} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (K : Matrix ι ι ℂ) (hl : K.IsLowerTriangular) (hd : ∀ (i : ι), K i i = 1) (H : Finset ι) : IsUnit (rows K H)

theorem Complexity.ExactFourier.BasisExchange.price_triangular {ι : Type} [Fintype ι] [DecidableEq ι] [LinearOrder ι] (p : MatrixPrice) (K : Matrix ι ι ℂ) (hl : K.IsLowerTriangular) (hd : ∀ (i : ι), K i i = 1) (H : Finset ι) : p.value (rows K Hᶜ * (rows K H)⁻¹) = p.value K

@[reducible, inline]

abbrev Complexity.ExactFourier.SignedBits.Bits : ℕ → Type

Bit strings represented recursively by a sum of two copies of the shorter strings.

Equations

• Complexity.ExactFourier.SignedBits.Bits 0 = PUnit.{1}
• Complexity.ExactFourier.SignedBits.Bits m.succ = (Complexity.ExactFourier.SignedBits.Bits m ⊕ Complexity.ExactFourier.SignedBits.Bits m)

@[reducible]

instance Complexity.ExactFourier.SignedBits.bitsFintype (m : ℕ) : Fintype (Bits m)

Equations

• Complexity.ExactFourier.SignedBits.bitsFintype 0 = { elems := {PUnit.unit}, complete := ⋯ }
• Complexity.ExactFourier.SignedBits.bitsFintype m.succ = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[reducible]

instance Complexity.ExactFourier.SignedBits.bitsDecidableEq (m : ℕ) : DecidableEq (Bits m)

Equations

• Complexity.ExactFourier.SignedBits.bitsDecidableEq 0 = instDecidableEqPUnit
• Complexity.ExactFourier.SignedBits.bitsDecidableEq m.succ = fun (a b : Complexity.ExactFourier.SignedBits.Bits m ⊕ Complexity.ExactFourier.SignedBits.Bits m) => instDecidableEqSum a b

@[reducible]

instance Complexity.ExactFourier.SignedBits.bitsLinearOrder (m : ℕ) : LinearOrder (Bits m)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.SignedBits.bitsLinearOrder m.succ = Sum.Lex.linearOrder

@[reducible, instance 2000]

instance Complexity.ExactFourier.SignedBits.bitsLT (m : ℕ) : LT (Bits m)

Equations

• Complexity.ExactFourier.SignedBits.bitsLT m = (Complexity.ExactFourier.SignedBits.bitsLinearOrder m).toLT

@[simp]

theorem Complexity.ExactFourier.SignedBits.bits_card (m : ℕ) : Fintype.card (Bits m) = 2 ^ m

def Complexity.ExactFourier.SignedBits.D (m : ℕ) : Matrix (Bits m) (Bits m) ℂ

The recursive signed-bit matrix whose square is zero.

Equations

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

def Complexity.ExactFourier.SignedBits.T (m : ℕ) : Matrix (Bits m) (Bits m) ℂ

The identity plus the nilpotent signed-bit matrix D m.

Equations

• Complexity.ExactFourier.SignedBits.T m = 1 + Complexity.ExactFourier.SignedBits.D m

theorem Complexity.ExactFourier.SignedBits.D_square (m : ℕ) : D m * D m = 0

theorem Complexity.ExactFourier.SignedBits.T_inv_mul (m : ℕ) : (1 - D m) * T m = 1

theorem Complexity.ExactFourier.SignedBits.T_unit (m : ℕ) : IsUnit (T m)

theorem Complexity.ExactFourier.SignedBits.T_inv (m : ℕ) : (T m)⁻¹ = 1 - D m

theorem Complexity.ExactFourier.SignedBits.D_lower (m : ℕ) : (D m).IsLowerTriangular

theorem Complexity.ExactFourier.SignedBits.D_diag (m : ℕ) (i : Bits m) : D m i i = 0

theorem Complexity.ExactFourier.SignedBits.T_lower (m : ℕ) : (T m).IsLowerTriangular

theorem Complexity.ExactFourier.SignedBits.T_diag (m : ℕ) (i : Bits m) : T m i i = 1

theorem Complexity.ExactFourier.SignedBits.T_succ (m : ℕ) : T (m + 1) = Matrix.fromBlocks (T m) 0 1 (T m)⁻¹