Exact Fourier circuits: polynomial clearing

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

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

theorem Complexity.ExactFourier.Boundary.time_power_clearing {α : Type} [Fintype α] [DecidableEq α] (G : Matrix α α (Polynomial ℂ)) (H : Matrix α α (PowerSeries ℂ)) (q : Polynomial ℂ) (h : seriesMatrix G = ↑q • H) (k t : ℕ) : timeMatrix t (TensorAxis.power G k) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CoefficientTime.truncMatrix t (↑q ^ k)) 1 * (CoefficientTime.blockTruncHom t) (TensorAxis.power H k)

theorem Complexity.ExactFourier.Boundary.time_power_clearing_price {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G : Matrix α α (Polynomial ℂ)) (H : Matrix α α (PowerSeries ℂ)) (q : Polynomial ℂ) (h : seriesMatrix G = ↑q • H) (hq : q.coeff 0 ≠ 0) (hH : IsUnit (H.map ⇑PowerSeries.constantCoeff)) (k t : ℕ) (ht : 0 < t) : p.value (timeMatrix t (TensorAxis.power G k)) ≤ p.value ((CoefficientTime.blockTruncHom t) (TensorAxis.power H k)) + ↑(Fintype.card α) ^ k * (627 / Real.log 2) * ↑t * Real.log (2 * ↑t)

noncomputable def Complexity.ExactFourier.Taylor.matrix (t : ℕ) (s : ℂ) : Matrix (Fin t) (Fin t) ℂ

The coefficient matrix of polynomial translation by the scalar s.

Equations

• Complexity.ExactFourier.Taylor.matrix t s a b = ((Polynomial.taylor s) (Polynomial.X ^ ↑b)).coeff ↑a

theorem Complexity.ExactFourier.Taylor.coefficient_sum (t : ℕ) (s : ℂ) (f : Polynomial ℂ) (hf : f.natDegree < t) (i : Fin t) : ((Polynomial.taylor s) f).coeff ↑i = ∑ j : Fin t, matrix t s i j * f.coeff ↑j

theorem Complexity.ExactFourier.Taylor.matrix_mul (t : ℕ) (s r : ℂ) : matrix t s * matrix t r = matrix t (s + r)

@[simp]

theorem Complexity.ExactFourier.Taylor.matrix_zero (t : ℕ) : matrix t 0 = 1

theorem Complexity.ExactFourier.Taylor.matrix_unit (t : ℕ) (s : ℂ) : IsUnit (matrix t s)

theorem Complexity.ExactFourier.Taylor.matrix_inv (t : ℕ) (s : ℂ) : (matrix t s)⁻¹ = matrix t (-s)

theorem Complexity.ExactFourier.Taylor.taylor_modulus (t : ℕ) (s : ℂ) : (Polynomial.taylor s) ((Polynomial.X - Polynomial.C s) ^ t) = Polynomial.X ^ t

theorem Complexity.ExactFourier.Taylor.remainder_coeff (t : ℕ) (s : ℂ) (f : Polynomial ℂ) (i : Fin t) : ((Polynomial.taylor s) (f %ₘ (Polynomial.X - Polynomial.C s) ^ t)).coeff ↑i = ((Polynomial.taylor s) f).coeff ↑i

noncomputable def Complexity.ExactFourier.Taylor.translate {α : Type} (s : ℂ) (G : Matrix α α (Polynomial ℂ)) : Matrix α α (Polynomial ℂ)

Translate every polynomial entry of a matrix by the same scalar.

Equations

• Complexity.ExactFourier.Taylor.translate s G = G.map ⇑(Polynomial.taylor s)

theorem Complexity.ExactFourier.Taylor.intertwine {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (ht : 0 < t) (s : ℂ) (G : Matrix α α (Polynomial ℂ)) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (matrix t s) 1 * Boundary.modulusMatrix t ((Polynomial.X - Polynomial.C s) ^ t) G = Boundary.timeMatrix t (translate s G) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (matrix t s) 1

noncomputable def Complexity.ExactFourier.Taylor.kernel (s : ℂ) : PowerSeries ℂ

The formal power series with coefficients s^j / j! used for translation.

Equations

• Complexity.ExactFourier.Taylor.kernel s = PowerSeries.mk fun (j : ℕ) => s ^ j / ↑j.factorial

@[simp]

theorem Complexity.ExactFourier.Taylor.kernel_constant (s : ℂ) : PowerSeries.constantCoeff (kernel s) = 1

theorem Complexity.ExactFourier.Taylor.diagonal_factorization (t : ℕ) (s : ℂ) : matrix t s = (Matrix.diagonal fun (i : Fin t) => (↑(↑i).factorial)⁻¹) * (CoefficientTime.truncMatrix t (kernel s)).transpose * Matrix.diagonal fun (j : Fin t) => ↑(↑j).factorial

theorem Complexity.ExactFourier.Taylor.price (p : MatrixPrice) (t : ℕ) (ht : 0 < t) (s : ℂ) : p.value (matrix t s) ≤ 627 / Real.log 2 * ↑t * Real.log (2 * ↑t)

theorem Complexity.ExactFourier.Taylor.conjugacy {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (ht : 0 < t) (s : ℂ) (G : Matrix α α (Polynomial ℂ)) : have P := Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (matrix t s) 1; P * Boundary.modulusMatrix t ((Polynomial.X - Polynomial.C s) ^ t) G * P⁻¹ = Boundary.timeMatrix t (translate s G)

theorem Complexity.ExactFourier.Taylor.modulus_unit {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (ht : 0 < t) (s : ℂ) (G : Matrix α α (Polynomial ℂ)) (hG : IsUnit (G.map (Polynomial.eval s))) : IsUnit (Boundary.modulusMatrix t ((Polynomial.X - Polynomial.C s) ^ t) G)

theorem Complexity.ExactFourier.Taylor.modulus_lower {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (t : ℕ) (ht : 0 < t) (s : ℂ) (G : Matrix α α (Polynomial ℂ)) (hG : IsUnit (G.map (Polynomial.eval s))) : ↑t * p.value (G.map (Polynomial.eval s)) ≤ p.value (Boundary.modulusMatrix t ((Polynomial.X - Polynomial.C s) ^ t) G) + 2 * ↑(Fintype.card α) * (627 / Real.log 2) * ↑t * Real.log (2 * ↑t)

noncomputable def Complexity.ExactFourier.CellPoly.feedback {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (s : ℂ) : Matrix α α ℂ

The cell transfer matrix after feeding back the state block at scalar parameter s.

Equations

• Complexity.ExactFourier.CellPoly.feedback M C B D s = M + s • (C * (1 - s • D)⁻¹ * B)

theorem Complexity.ExactFourier.CellPoly.eval_Z {β : Type} [DecidableEq β] (D : Matrix β β ℂ) (s : ℂ) : (Z D).map ⇑(Polynomial.evalRingHom s) = 1 - s • D

@[simp]

theorem Complexity.ExactFourier.CellPoly.eval_a {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) (s : ℂ) : Polynomial.eval s (a D) = (1 - s • D).det

theorem Complexity.ExactFourier.CellPoly.eval_R {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) (s : ℂ) : (R D).map ⇑(Polynomial.evalRingHom s) = (1 - s • D).adjugate

theorem Complexity.ExactFourier.CellPoly.adjugate_eq_det_smul_inv {β : Type} [Fintype β] [DecidableEq β] (A : Matrix β β ℂ) (hA : IsUnit A) : A.adjugate = A.det • A⁻¹

theorem Complexity.ExactFourier.CellPoly.eval_F {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (s : ℂ) (hD : IsUnit (1 - s • D)) : (F M C B D).map ⇑(Polynomial.evalRingHom s) = Polynomial.eval s (a D) • feedback M C B D s

noncomputable def Complexity.ExactFourier.boundaryError (m : ℕ) : ℝ

The vanishing error term in the boundary-correction price estimate.

Equations

• Complexity.ExactFourier.boundaryError m = Real.log (2 * (↑m + 2) ^ 8) / (↑m + 1) + (↑m + 2) ^ 6 / ((↑m + 2) ^ 8 * (↑m + 1))

theorem Complexity.ExactFourier.boundaryError_tendsto : Filter.Tendsto boundaryError Filter.atTop (nhds 0)

theorem Complexity.ExactFourier.fixed_price_of_boundary (x y C : ℝ) (h : ∀ (k t : ℕ), 0 < k → 0 < t → ↑t * ↑k * (x - y) ≤ C * (↑t * Real.log (2 * ↑t) + (↑k + 1) ^ 6)) : x ≤ y

theorem Complexity.ExactFourier.MatrixPrice.feedback {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (s : ℂ) (hM : IsUnit M) (hK : IsUnit (Matrix.fromBlocks M C B D)) (hD : IsUnit (1 - s • D)) (hH : IsUnit (CellPoly.feedback M C B D s)) : p.value (CellPoly.feedback M C B D s) ≤ p.value (Matrix.fromBlocks M C B D)