Exact Fourier circuits: parameter algebra

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/ParameterAlgebra.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.PositiveGeneration.evalMatrix {α κ : Type} [Fintype α] [DecidableEq α] (F : Matrix α α (MvPolynomial κ ℂ)) (x : κ → ℂ) : Matrix α α ℂ

Evaluate a matrix of multivariate polynomials at one parameter vector.

Equations

• Complexity.ExactFourier.PositiveGeneration.evalMatrix F x = (MvPolynomial.aeval x).mapMatrix F

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.evalMatrix_apply {α κ : Type} [Fintype α] [DecidableEq α] (F : Matrix α α (MvPolynomial κ ℂ)) (x : κ → ℂ) (i j : α) : evalMatrix F x i j = (MvPolynomial.aeval x) (F i j)

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.evalMatrix_mul {α κ : Type} [Fintype α] [DecidableEq α] (F G : Matrix α α (MvPolynomial κ ℂ)) (x : κ → ℂ) : evalMatrix (F * G) x = evalMatrix F x * evalMatrix G x

theorem Complexity.ExactFourier.PositiveGeneration.evalMatrix_const {α κ : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (x : κ → ℂ) : evalMatrix (MvPolynomial.C.mapMatrix M) x = M

theorem Complexity.ExactFourier.PositiveGeneration.evalMatrix_rename {α κ : Type} [Fintype α] [DecidableEq α] {τ : Type} (e : κ → τ) (F : Matrix α α (MvPolynomial κ ℂ)) (x : τ → ℂ) : evalMatrix ((MvPolynomial.rename e).mapMatrix F) x = evalMatrix F (x ∘ e)

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.evalMatrix_diag {α κ : Type} [Fintype α] [DecidableEq α] (d : α → MvPolynomial κ ℂ) (x : κ → ℂ) : evalMatrix (Matrix.diagonal d) x = Matrix.diagonal fun (i : α) => (MvPolynomial.aeval x) (d i)

noncomputable def Complexity.ExactFourier.PositiveGeneration.diagCLM {α : Type} [Fintype α] [DecidableEq α] : (α → ℂ) →L[ℂ] Matrix α α ℂ

Form a diagonal matrix as a continuous complex linear map.

Equations

• Complexity.ExactFourier.PositiveGeneration.diagCLM = LinearMap.toContinuousLinearMap Complexity.ExactFourier.PositiveGeneration.diagLinear

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.diagCLM_apply {α : Type} [Fintype α] [DecidableEq α] (x : α → ℂ) : diagCLM x = Matrix.diagonal x

noncomputable def Complexity.ExactFourier.PositiveGeneration.leftProj {α κ : Type} : (κ ⊕ α → ℂ) →L[ℂ] κ → ℂ

Project a vector on a sum of coordinate types to its left block.

Equations

• Complexity.ExactFourier.PositiveGeneration.leftProj = ContinuousLinearMap.pi fun (i : κ) => ContinuousLinearMap.proj (Sum.inl i)

noncomputable def Complexity.ExactFourier.PositiveGeneration.rightProj {α κ : Type} : (κ ⊕ α → ℂ) →L[ℂ] α → ℂ

Project a vector on a sum of coordinate types to its right block.

Equations

• Complexity.ExactFourier.PositiveGeneration.rightProj = ContinuousLinearMap.pi fun (i : α) => ContinuousLinearMap.proj (Sum.inr i)

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.leftProj_apply {α κ : Type} (x : κ ⊕ α → ℂ) : leftProj x = x ∘ Sum.inl

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.rightProj_apply {α κ : Type} (x : κ ⊕ α → ℂ) : rightProj x = x ∘ Sum.inr

structure Complexity.ExactFourier.PositiveGeneration.Param {α : Type} [Fintype α] [DecidableEq α] (A p : Matrix α α ℂ) (U : Submodule ℂ (Matrix α α ℂ)) : Type 1

A fixed positive word with polynomial diagonal parameters and its exact derivative.

• Vars : Type

  The finite parameter-coordinate type of the polynomial family.

• finiteVars : Fintype self.Vars
• poly : Matrix α α (MvPolynomial self.Vars ℂ)

  The matrix of polynomials describing the parameterized positive words.

• calls : ℕ

  The fixed number of calls to A in every nonzero-parameter instance.

• base : (evalMatrix self.poly fun (x : self.Vars) => 1) = p
• pattern (x : self.Vars → ℂ) : (∀ (i : self.Vars), x i ≠ 0) → Pattern A self.calls (evalMatrix self.poly x)
• derivative : (self.Vars → ℂ) →L[ℂ] Matrix α α ℂ

  The derivative of the polynomial family at the all-ones parameter vector.

• deriv : HasStrictFDerivAt (evalMatrix self.poly) self.derivative fun (x : self.Vars) => 1
• spans (X : Matrix α α ℂ) : X ∈ U → ∃ (x : self.Vars → ℂ), self.derivative x = X * p

noncomputable def Complexity.ExactFourier.PositiveGeneration.Param.nil {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) : Param A 1 (diagConj 1)

The initial diagonal polynomial family with no calls to A.

Equations

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

noncomputable def Complexity.ExactFourier.PositiveGeneration.Param.nextPoly {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (s : Matrix α α ℂ) : Matrix α α (MvPolynomial (P.Vars ⊕ α) ℂ)

Append a fixed matrix and a fresh diagonal parameter block to the family.

Equations

• P.nextPoly s = (MvPolynomial.rename Sum.inl).mapMatrix P.poly * MvPolynomial.C.mapMatrix s * Matrix.diagonal fun (i : α) => MvPolynomial.X (Sum.inr i)

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.Param.eval_nextPoly {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (s : Matrix α α ℂ) (x : P.Vars ⊕ α → ℂ) : evalMatrix (P.nextPoly s) x = evalMatrix P.poly (x ∘ Sum.inl) * s * Matrix.diagonal (x ∘ Sum.inr)

noncomputable def Complexity.ExactFourier.PositiveGeneration.Param.nextDerivative {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (s : Matrix α α ℂ) : (P.Vars ⊕ α → ℂ) →L[ℂ] Matrix α α ℂ

The product-rule derivative after appending a matrix and diagonal parameters.

Equations

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

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.Param.nextDerivative_apply {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (s : Matrix α α ℂ) (x : P.Vars ⊕ α → ℂ) : (P.nextDerivative s) x = P.derivative (x ∘ Sum.inl) * s + p * s * Matrix.diagonal (x ∘ Sum.inr)

theorem Complexity.ExactFourier.PositiveGeneration.Param.next_deriv {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (s : Matrix α α ℂ) : HasStrictFDerivAt (evalMatrix (P.nextPoly s)) (P.nextDerivative s) fun (x : P.Vars ⊕ α) => 1

theorem Complexity.ExactFourier.PositiveGeneration.Param.base_unit {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (hA : IsUnit A) : IsUnit p

noncomputable def Complexity.ExactFourier.PositiveGeneration.Param.snoc {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (hA : IsUnit A) (s : Matrix α α ℂ) (hs : Reach A s) : Param A (p * s) (U ⊔ diagConj (p * s))

Extend a parameterized family by a reachable matrix and its diagonal directions.

Equations

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

theorem Complexity.ExactFourier.PositiveGeneration.Chain.parameterization {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (h : Chain A p U) (hA : IsUnit A) : Nonempty (Param A p U)

theorem Complexity.ExactFourier.PositiveGeneration.Param.derivative_surjective {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} (P : Param A p ⊤) (hA : IsUnit A) : Function.Surjective ⇑P.derivative

def Complexity.ExactFourier.PositiveGeneration.flatten {α : Type} : Matrix α α ℂ ≃ₗ[ℂ] α × α → ℂ

Identify a matrix with the vector of entries indexed by pairs of coordinates.

Equations

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

noncomputable def Complexity.ExactFourier.PositiveGeneration.flatCLM {α : Type} [Fintype α] : Matrix α α ℂ ≃L[ℂ] α × α → ℂ

The continuous linear equivalence flattening a finite matrix into its entries.

Equations

• Complexity.ExactFourier.PositiveGeneration.flatCLM = Complexity.ExactFourier.PositiveGeneration.flatten.toContinuousLinearEquiv

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.flatCLM_apply {α : Type} [Fintype α] (M : Matrix α α ℂ) (ij : α × α) : flatCLM M ij = M ij.1 ij.2

noncomputable def Complexity.ExactFourier.PositiveGeneration.Param.hom {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) : MvPolynomial (α × α) ℂ →ₐ[ℂ] MvPolynomial P.Vars ℂ

The polynomial substitution homomorphism defined by the parameterized matrix entries.

Equations

• P.hom = MvPolynomial.aeval fun (ij : α × α) => P.poly ij.1 ij.2

@[simp]

theorem Complexity.ExactFourier.PositiveGeneration.Param.polynomialMap_hom {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} {U : Submodule ℂ (Matrix α α ℂ)} (P : Param A p U) (x : P.Vars → ℂ) : polynomialMap P.hom x = flatCLM (evalMatrix P.poly x)

theorem Complexity.ExactFourier.PositiveGeneration.Param.hom_injective {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} (P : Param A p ⊤) (hA : IsUnit A) : Function.Injective ⇑P.hom

theorem Complexity.ExactFourier.PositiveGeneration.Param.open_word {α : Type} [Fintype α] [DecidableEq α] {A p : Matrix α α ℂ} (P : Param A p ⊤) (hA : IsUnit A) : ∃ (g : MvPolynomial (α × α) ℂ), g ≠ 0 ∧ ∀ (H : Matrix α α ℂ), (MvPolynomial.aeval (flatCLM H)) g ≠ 0 → Pattern A P.calls H

theorem Complexity.ExactFourier.PositiveGeneration.polynomial_nonzero_dense {ι : Type} [Fintype ι] (g : MvPolynomial ι ℂ) (hg : g ≠ 0) : Dense {y : ι → ℂ | (MvPolynomial.aeval y) g ≠ 0}

Nonempty Zariski basic opens in complex affine space are Euclidean dense.

theorem Complexity.ExactFourier.PositiveGeneration.polynomial_nonzero_open {ι : Type} [Fintype ι] (g : MvPolynomial ι ℂ) : IsOpen {y : ι → ℂ | (MvPolynomial.aeval y) g ≠ 0}

theorem Complexity.ExactFourier.PositiveGeneration.Pattern.zero_iff {α : Type} [Fintype α] [DecidableEq α] (A H : Matrix α α ℂ) : Pattern A 0 H ↔ MonomialMatrix H

theorem Complexity.ExactFourier.PositiveGeneration.positive_generation {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (hn : ¬MonomialMatrix A) : ∃ (h : ℕ), 0 < h ∧ ∀ (H : Matrix α α ℂ), IsUnit H → Pattern A h H

Positive generation, with a common strictly positive number of forward calls.