Exact Fourier circuits: boundary active circuit

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/BoundaryActiveCircuit.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.Boundary.activeWeights (t d e : ℕ) (η ℓ : Polynomial ℂ) : Matrix (Times t d e) (Times t d e × Fin (e + 1) × Fin (d + 1)) ℂ

Scalar weights for reconstructing the correction on active boundary times.

Equations

• Complexity.ExactFourier.Boundary.activeWeights t d e η ℓ a b = Complexity.ExactFourier.Boundary.orderedWeight (if ↑↑a < t - d then 1 else η) ℓ ↑↑a ↑↑b.1 ↑b.2.1 ↑b.2.2

theorem Complexity.ExactFourier.Boundary.activeMatrix_blocks {ι : Type} [Fintype ι] [DecidableEq ι] (t d e : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (hG : PolynomialMatrix.Bounded G d) (hJ : PolynomialMatrix.Bounded J e) : activeMatrix t d e η ℓ J G = 1 + TypedDAG.blockMatrix (activeWeights t d e η ℓ) fun (ij : Fin (e + 1) × Fin (d + 1)) => coefficientMatrix J ↑ij.1 * coefficientMatrix G ↑ij.2

theorem Complexity.ExactFourier.Boundary.exists_active_dag {ι : Type} [Fintype ι] [DecidableEq ι] (t d e sG sJ : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (hG : PolynomialMatrix.Bounded G d) (hJ : PolynomialMatrix.Bounded J e) (CG : Fin (d + 1) → TypedDAG ι ι) (CJ : Fin (e + 1) → TypedDAG ι ι) (hsG : ∀ (j : Fin (d + 1)), (CG j).size ≤ sG) (hsJ : ∀ (i : Fin (e + 1)), (CJ i).size ≤ sJ) (heG : ∀ (j : Fin (d + 1)) (x : ι → ℂ), (CG j).eval x = (coefficientMatrix G ↑j).mulVec x) (heJ : ∀ (i : Fin (e + 1)) (x : ι → ℂ), (CJ i).eval x = (coefficientMatrix J ↑i).mulVec x) : ∃ (C : TypedDAG (Times t d e × ι) (Times t d e × ι)), C.size ≤ Fintype.card (Times t d e) * ((e + 1) * (d + 1)) * (sG + sJ) + 2 * Fintype.card ι * Fintype.card (Times t d e) ^ 2 * ((e + 1) * (d + 1)) + Fintype.card (Times t d e) * Fintype.card ι ∧ ∀ (x : Times t d e × ι → ℂ), C.eval x = (activeMatrix t d e η ℓ J G).mulVec x

theorem Complexity.ExactFourier.Boundary.exists_uniform_active_dag {α : Type} [Fintype α] [DecidableEq α] (G J : Matrix α α (Polynomial ℂ)) (dg dj : ℕ) (hG : PolynomialMatrix.Bounded G dg) (hJ : PolynomialMatrix.Bounded J dj) : ∃ (A : ℕ), ∀ (k t : ℕ) (η ℓ : Polynomial ℂ), ℓ.Monic → ∃ (C : TypedDAG (Times t (k * dg) (k * dj) × TensorAxis.Space α k) (Times t (k * dg) (k * dj) × TensorAxis.Space α k)), C.size ≤ A * (k + 1) ^ 6 * Fintype.card α ^ k ∧ ∀ (x : Times t (k * dg) (k * dj) × TensorAxis.Space α k → ℂ), C.eval x = (activeMatrix t (k * dg) (k * dj) η ℓ (TensorAxis.power J k) (TensorAxis.power G k)).mulVec x

theorem Complexity.ExactFourier.Boundary.exists_uniform_active_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G J : Matrix α α (Polynomial ℂ)) (dg dj : ℕ) (hG : PolynomialMatrix.Bounded G dg) (hJ : PolynomialMatrix.Bounded J dj) : ∃ (A : ℕ), ∀ (k t : ℕ) (η ℓ : Polynomial ℂ), ℓ.Monic → ℓ.natDegree = t → 0 < k * dg → IsUnit (1 + activeCorrection t (k * dg) η ℓ (TensorAxis.power J k) (TensorAxis.power G k)) → p.value (1 + activeCorrection t (k * dg) η ℓ (TensorAxis.power J k) (TensorAxis.power G k)) ≤ ↑A * (↑k + 1) ^ 6 * ↑(Fintype.card α) ^ k

theorem Complexity.ExactFourier.ScalarConvolution.exists_prefix_dag (t T : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) : ∃ (C : LinearDAG t t), C.size ≤ 52 * t * (Nat.log 2 t + 1) ∧ ∀ (x : Fin t → ℂ), C.eval x = (CoefficientTime.prefixScalar t T f).mulVec x

theorem Complexity.ExactFourier.ScalarConvolution.prefix_inv (t T : ℕ) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : (CoefficientTime.prefixScalar t T f)⁻¹ = CoefficientTime.prefixScalar t T f⁻¹

theorem Complexity.ExactFourier.ScalarConvolution.price_prefix (p : MatrixPrice) (t T : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : p.value (CoefficientTime.prefixScalar t T f) ≤ 627 / Real.log 2 * ↑t * Real.log (2 * ↑t)

theorem Complexity.ExactFourier.MatrixPrice.conjugate_le {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (P A : Matrix ι ι ℂ) (hP : IsUnit P) (hA : IsUnit A) : p.value (P * A * P⁻¹) ≤ 2 * p.value P + p.value A

theorem Complexity.ExactFourier.MatrixPrice.le_conjugate {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (P A : Matrix ι ι ℂ) (hP : IsUnit P) (hA : IsUnit A) : p.value A ≤ 2 * p.value P + p.value (P * A * P⁻¹)

theorem Complexity.ExactFourier.MatrixPrice.scalar {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (A : Matrix ι ι ℂ) (hA : IsUnit A) (c : ℂ) (hc : c ≠ 0) : p.value (c • A) = p.value A

theorem Complexity.ExactFourier.MatrixPrice.scalar_unit {ι : Type} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℂ) (hA : IsUnit A) (c : ℂ) (hc : c ≠ 0) : IsUnit (c • A)

theorem Complexity.ExactFourier.MatrixPrice.prefix_tensor_price {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (t T : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : p.value (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CoefficientTime.prefixScalar t T f) 1) ≤ ↑(Fintype.card ι) * (627 / Real.log 2) * ↑t * Real.log (2 * ↑t)

theorem Complexity.ExactFourier.Boundary.exists_boundary_bound {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G : Matrix α α (Polynomial ℂ)) (hG0 : IsUnit (G.map fun (f : Polynomial ℂ) => f.coeff 0)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (k t : ℕ), 0 < k → 0 < t → ∀ (ℓ : Polynomial ℂ), ℓ.Monic → ℓ.natDegree = t → ℓ.coeff 0 ≠ 0 → IsUnit (modulusMatrix t ℓ (TensorAxis.power G k)) → |p.value (modulusMatrix t ℓ (TensorAxis.power G k)) - p.value (timeMatrix t (TensorAxis.power G k))| ≤ C * ↑(Fintype.card α) ^ k * (↑t * Real.log (2 * ↑t) + (↑k + 1) ^ 6)