Exact Fourier circuits: triangular

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

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

theorem Complexity.ExactFourier.MatrixPrice.triangular_experiment_bound (p : MatrixPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (hD : IsUnit D) (k : ℕ) : ↑(Fintype.card (Triangular.Calls β k)) * (p.value M + p.value D - p.value (Matrix.fromBlocks M C 0 D)) ≤ ↑(Fintype.card α) ^ 2 * ↑(Fintype.card β) * ↑(Fintype.card (Triangular.Bottom β k))

theorem Complexity.ExactFourier.MatrixPrice.upper_triangular (p : MatrixPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (hD : IsUnit D) : p.value M + p.value D ≤ p.value (Matrix.fromBlocks M C 0 D)

The literal upper block triangular conclusion, including empty blocks.

theorem Complexity.ExactFourier.MatrixPrice.lower_triangular (p : MatrixPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix β α ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (hD : IsUnit D) : p.value M + p.value D ≤ p.value (Matrix.fromBlocks M 0 C D)

noncomputable def Complexity.ExactFourier.CoefficientTime.truncMatrix {R : Type u_1} [Semiring R] (t : ℕ) (F : PowerSeries R) : Matrix (Fin t) (Fin t) R

The lower triangular Toeplitz matrix acting on the first t coefficients.

Equations

• Complexity.ExactFourier.CoefficientTime.truncMatrix t F a b = if ↑b ≤ ↑a then (PowerSeries.coeff (↑a - ↑b)) F else 0

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.truncMatrix_one {R : Type u_1} [Semiring R] (t : ℕ) : truncMatrix t 1 = 1

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.truncMatrix_zero {R : Type u_1} [Semiring R] (t : ℕ) : truncMatrix t 0 = 0

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.truncMatrix_add {R : Type u_1} [Semiring R] (t : ℕ) (F G : PowerSeries R) : truncMatrix t (F + G) = truncMatrix t F + truncMatrix t G

theorem Complexity.ExactFourier.CoefficientTime.truncMatrix_mul {R : Type u_1} [Semiring R] (t : ℕ) (F G : PowerSeries R) : truncMatrix t (F * G) = truncMatrix t F * truncMatrix t G

noncomputable def Complexity.ExactFourier.CoefficientTime.truncHom {R : Type u_1} [Semiring R] (t : ℕ) : PowerSeries R →+* Matrix (Fin t) (Fin t) R

Multiplication modulo z^t in the coefficient basis is a literal ring homomorphism.

Equations

• Complexity.ExactFourier.CoefficientTime.truncHom t = { toFun := Complexity.ExactFourier.CoefficientTime.truncMatrix t, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Complexity.ExactFourier.CoefficientTime.trunc_isUnit {R : Type u_1} [Ring R] (t : ℕ) (F : PowerSeries R) (hF : IsUnit (PowerSeries.constantCoeff F)) : IsUnit (truncMatrix t F)

Repeated invertible constant term makes the time coefficient matrix invertible.

noncomputable def Complexity.ExactFourier.CoefficientTime.blockTruncHom {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) : Matrix ι ι (PowerSeries ℂ) →+* Matrix (Fin t × ι) (Fin t × ι) ℂ

Truncate a matrix of formal series into a finite matrix with time-first coordinates.

Equations

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

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.blockTruncHom_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (F : Matrix ι ι (PowerSeries ℂ)) (a b : Fin t × ι) : (blockTruncHom t) F a b = if ↑b.1 ≤ ↑a.1 then (PowerSeries.coeff (↑a.1 - ↑b.1)) (F a.2 b.2) else 0

theorem Complexity.ExactFourier.CoefficientTime.blockTrunc_isUnit {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (F : Matrix ι ι (PowerSeries ℂ)) (hF : IsUnit (F.map ⇑PowerSeries.constantCoeff)) : IsUnit ((blockTruncHom t) F)

theorem Complexity.ExactFourier.CoefficientTime.coeff_mul_truncated {R : Type u_1} [Semiring R] {t : ℕ} (F G : PowerSeries R) (a : Fin t) : (PowerSeries.coeff ↑a) (F * G) = ∑ k : Fin t, (if ↑k ≤ ↑a then (PowerSeries.coeff (↑a - ↑k)) F else 0) * (PowerSeries.coeff ↑k) G

noncomputable def Complexity.ExactFourier.CoefficientTime.coefficientColumns {ι : Type u_1} {κ : Type u_2} (t : ℕ) (V : Matrix ι κ (PowerSeries ℂ)) : Matrix (Fin t × ι) κ ℂ

Stack the first t coefficient matrices of a rectangular matrix of series.

Equations

• Complexity.ExactFourier.CoefficientTime.coefficientColumns t V a b = (PowerSeries.coeff ↑a.1) (V a.2 b)

theorem Complexity.ExactFourier.CoefficientTime.blocks_mul_columns {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (t : ℕ) (F : Matrix ι ι (PowerSeries ℂ)) (V : Matrix ι κ (PowerSeries ℂ)) : (blockTruncHom t) F * coefficientColumns t V = coefficientColumns t (F * V)

A matrix series acts on vectors of truncated coefficients by the literal coefficient product. This is the state-response and boundary-quotient interface.

theorem Complexity.ExactFourier.CoefficientTime.blockTrunc_scalar {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t : ℕ) (f : PowerSeries ℂ) : (blockTruncHom t) ((Matrix.scalar ι) f) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (truncMatrix t f) 1

The scalar Toeplitz factor acts identically on every spatial coordinate.

noncomputable def Complexity.ExactFourier.CoefficientTime.prefixScalar (t T : ℕ) (f : PowerSeries ℂ) : Matrix (Fin t) (Fin t) ℂ

The scalar prefix change of basis leaves the suffix literally fixed. Its prefix-to-suffix block is zero because the convolution is lower triangular.

Equations

• Complexity.ExactFourier.CoefficientTime.prefixScalar t T f a b = if ↑a < T then Complexity.ExactFourier.CoefficientTime.truncMatrix t f a b else 1 a b

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.prefixScalar_one (t T : ℕ) : prefixScalar t T 1 = 1

@[simp]

theorem Complexity.ExactFourier.CoefficientTime.prefixScalar_mul (t T : ℕ) (f g : PowerSeries ℂ) : prefixScalar t T (f * g) = prefixScalar t T f * prefixScalar t T g

theorem Complexity.ExactFourier.CoefficientTime.prefixScalar_isUnit (t T : ℕ) (f : PowerSeries ℂ) (hf : IsUnit (PowerSeries.constantCoeff f)) : IsUnit (prefixScalar t T f)

theorem Complexity.ExactFourier.CoefficientTime.prefix_mul_columns {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] (t T : ℕ) (f : PowerSeries ℂ) (V : Matrix ι κ (PowerSeries ℂ)) (a : Fin t × ι) (b : κ) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (prefixScalar t T f) 1 * coefficientColumns t V) a b = if ↑a.1 < T then (PowerSeries.coeff ↑a.1) (f * V a.2 b) else (PowerSeries.coeff ↑a.1) (V a.2 b)

On an early row the partial scalar convolution is a full coefficient convolution; on a late row it leaves the original series coefficient unchanged.

theorem Complexity.ExactFourier.CoefficientTime.zero_prefix_columns_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (t T : ℕ) (f : PowerSeries ℂ) (S : Matrix (Fin t × ι) (Fin t × ι) ℂ) (hS : ∀ (a b : Fin t × ι), ↑b.1 < T → S a b = 0) : S * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (prefixScalar t T f) 1 = S

def Complexity.ExactFourier.timeSplit (t : ℕ) (α : Type) : Fin (t + 1) × α ≃ α ⊕ Fin t × α

Separate the first time coordinate from all subsequent times.

Equations

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

theorem Complexity.ExactFourier.MatrixPrice.blocks_lower (p : MatrixPrice) {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (F : Matrix (Fin t × α) (Fin t × α) ℂ) (A : Fin t → Matrix α α ℂ) (hA : ∀ (i : Fin t), IsUnit (A i)) (hdiag : ∀ (i : Fin t) (a b : α), F (i, a) (i, b) = A i a b) (hbelow : ∀ (i j : Fin t) (a b : α), i < j → F (i, a) (j, b) = 0) : IsUnit F ∧ ∑ i : Fin t, p.value (A i) ≤ p.value F

theorem Complexity.ExactFourier.MatrixPrice.trunc_lower_bound (p : MatrixPrice) {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (F : Matrix α α (PowerSeries ℂ)) (hF : IsUnit (F.map ⇑PowerSeries.constantCoeff)) : ↑t * p.value (F.map ⇑PowerSeries.constantCoeff) ≤ p.value ((CoefficientTime.blockTruncHom t) F)