Exact Fourier circuits: stream series

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/StreamSeries.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.CellSeries.resolvent {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : Matrix β β (PowerSeries ℂ)

The formal matrix series whose coefficient of degree m is D^m.

Equations

• Complexity.ExactFourier.CellSeries.resolvent D i j = PowerSeries.mk fun (m : ℕ) => (D ^ m) i j

noncomputable def Complexity.ExactFourier.CellSeries.state {α β : Type} [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) : Matrix α β (PowerSeries ℂ)

The formal response from the cell's state coordinates to its output coordinates.

Equations

• Complexity.ExactFourier.CellSeries.state C D = C.map ⇑PowerSeries.C * Complexity.ExactFourier.CellSeries.resolvent D

noncomputable def Complexity.ExactFourier.CellSeries.transfer {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : Matrix α α (PowerSeries ℂ)

The formal transfer matrix of one cell, including its delayed state feedback.

Equations

• Complexity.ExactFourier.CellSeries.transfer M C B D = M.map ⇑PowerSeries.C + PowerSeries.X • (Complexity.ExactFourier.CellSeries.state C D * B.map ⇑PowerSeries.C)

@[simp]

theorem Complexity.ExactFourier.CellSeries.coeff_resolvent {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) (n : ℕ) (i j : β) : (PowerSeries.coeff n) (resolvent D i j) = (D ^ n) i j

@[simp]

theorem Complexity.ExactFourier.CellSeries.coeff_state {α β : Type} [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (n : ℕ) (i : α) (j : β) : (PowerSeries.coeff n) (state C D i j) = (C * D ^ n) i j

@[simp]

theorem Complexity.ExactFourier.CellSeries.coeff_transfer_zero {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (i j : α) : (PowerSeries.coeff 0) (transfer M C B D i j) = M i j

@[simp]

theorem Complexity.ExactFourier.CellSeries.coeff_transfer_succ {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (n : ℕ) (i j : α) : (PowerSeries.coeff (n + 1)) (transfer M C B D i j) = (C * D ^ n * B) i j

theorem Complexity.ExactFourier.CellSeries.constant_transfer {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : (transfer M C B D).map ⇑PowerSeries.constantCoeff = M

theorem Complexity.ExactFourier.CellSeries.resolvent_right_inverse {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : (1 - PowerSeries.X • D.map ⇑PowerSeries.C) * resolvent D = 1

theorem Complexity.ExactFourier.CellSeries.resolvent_left_inverse {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : resolvent D * (1 - PowerSeries.X • D.map ⇑PowerSeries.C) = 1

noncomputable def Complexity.ExactFourier.CellStream.run {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) (t : ℕ) : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ

Execute the same cell at successive times while carrying its state between inputs.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.CellStream.run K 0 = 1

theorem Complexity.ExactFourier.CellStream.unit {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) (hK : IsUnit K) (t : ℕ) : IsUnit (run K t)

theorem Complexity.ExactFourier.CellStream.price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (K : Matrix (α ⊕ β) (α ⊕ β) ℂ) (hK : IsUnit K) (t : ℕ) : p.value (run K t) ≤ ↑t * p.value K

@[simp]

theorem Complexity.ExactFourier.CellStream.fst_fst {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a b : α) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (0, a)) (Sum.inl (0, b)) = M a b

@[simp]

theorem Complexity.ExactFourier.CellStream.fst_succ {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a b : α) (j : Fin t) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (0, a)) (Sum.inl (j.succ, b)) = 0

@[simp]

theorem Complexity.ExactFourier.CellStream.succ_succ {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a b : α) (i j : Fin t) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (i.succ, a)) (Sum.inl (j.succ, b)) = run (Matrix.fromBlocks M C B D) t (Sum.inl (i, a)) (Sum.inl (j, b))

@[simp]

theorem Complexity.ExactFourier.CellStream.succ_fst {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a b : α) (i : Fin t) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (i.succ, a)) (Sum.inl (0, b)) = ∑ w : β, run (Matrix.fromBlocks M C B D) t (Sum.inl (i, a)) (Sum.inr w) * B w b

@[simp]

theorem Complexity.ExactFourier.CellStream.fst_state {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a : α) (b : β) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (0, a)) (Sum.inr b) = C a b

@[simp]

theorem Complexity.ExactFourier.CellStream.succ_state {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (a : α) (b : β) (i : Fin t) : run (Matrix.fromBlocks M C B D) (t + 1) (Sum.inl (i.succ, a)) (Sum.inr b) = ∑ w : β, run (Matrix.fromBlocks M C B D) t (Sum.inl (i, a)) (Sum.inr w) * D w b

theorem Complexity.ExactFourier.CellStream.state_entry {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (i : Fin t) (a : α) (b : β) : run (Matrix.fromBlocks M C B D) t (Sum.inl (i, a)) (Sum.inr b) = (C * D ^ ↑i) a b

theorem Complexity.ExactFourier.CellStream.state_block {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) : (run (Matrix.fromBlocks M C B D) t).toBlocks₁₂ = CoefficientTime.coefficientColumns t (CellSeries.state C D)

theorem Complexity.ExactFourier.CellStream.data_entry {α β : Type} [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) (i j : Fin t) (a b : α) : run (Matrix.fromBlocks M C B D) t (Sum.inl (i, a)) (Sum.inl (j, b)) = if ↑j ≤ ↑i then (PowerSeries.coeff (↑i - ↑j)) (CellSeries.transfer M C B D a b) else 0

theorem Complexity.ExactFourier.CellStream.data_block {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (t : ℕ) : (run (Matrix.fromBlocks M C B D) t).toBlocks₁₁ = (CoefficientTime.blockTruncHom t) (CellSeries.transfer M C B D)

def Complexity.ExactFourier.AxisJoin.rightOrder {α β γ : Type} : (α ⊕ γ) ⊕ β ≃ α ⊕ β ⊕ γ

Reassociate data and state coordinates for composing along a common data axis.

Equations

• Complexity.ExactFourier.AxisJoin.rightOrder = Complexity.ExactFourier.TensorTools.middleEquiv.trans (Equiv.sumAssoc α β γ)

@[reducible, inline]

abbrev Complexity.ExactFourier.AxisJoin.join {α β γ : Type} [Fintype α] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (α ⊕ γ) (α ⊕ γ) ℂ) : Matrix (α ⊕ β ⊕ γ) (α ⊕ β ⊕ γ) ℂ

Compose two cells along their common data coordinates while retaining both state blocks.

Equations

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

theorem Complexity.ExactFourier.AxisJoin.join_eq {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq β] [DecidableEq γ] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (α ⊕ γ) (α ⊕ γ) ℂ) : join X Y = (Matrix.reindex rightOrder rightOrder) (Matrix.fromBlocks Y 0 0 1) * (Matrix.reindex (Equiv.sumAssoc α β γ) (Equiv.sumAssoc α β γ)) (Matrix.fromBlocks X 0 0 1)

theorem Complexity.ExactFourier.AxisJoin.unit {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (α ⊕ γ) (α ⊕ γ) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : IsUnit (join X Y)

theorem Complexity.ExactFourier.AxisJoin.price {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (p : MatrixPrice) (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (α ⊕ γ) (α ⊕ γ) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : p.value (join X Y) ≤ p.value X + p.value Y

def Complexity.ExactFourier.TimeLifts.rightEquiv {σ ρ α : Type} (t : ℕ) : (Fin t × σ ⊕ ρ) × α ≃ Fin t × σ × α ⊕ ρ × α

Regroup a right tensor lift so that time is the leading coordinate.

Equations

• Complexity.ExactFourier.TimeLifts.rightEquiv t = (Equiv.sumProdDistrib (Fin t × σ) ρ α).trans ((Equiv.prodAssoc (Fin t) σ α).sumCongr (Equiv.refl (ρ × α)))

def Complexity.ExactFourier.TimeLifts.timeSwap {σ α : Type} (t : ℕ) : σ × Fin t × α ≃ Fin t × σ × α

Move time before the two spatial coordinate factors.

Equations

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

def Complexity.ExactFourier.TimeLifts.leftEquiv {σ α β : Type} (t : ℕ) : σ × (Fin t × α ⊕ β) ≃ Fin t × σ × α ⊕ σ × β

Regroup a left tensor lift so that time is the leading coordinate.

Equations

• Complexity.ExactFourier.TimeLifts.leftEquiv t = (Equiv.prodSumDistrib σ (Fin t × α) β).trans ((Complexity.ExactFourier.TimeLifts.timeSwap t).sumCongr (Equiv.refl (σ × β)))

noncomputable def Complexity.ExactFourier.TimeLifts.right {σ ρ α : Type} [DecidableEq α] (t : ℕ) (X : Matrix (Fin t × σ ⊕ ρ) (Fin t × σ ⊕ ρ) ℂ) : Matrix (Fin t × σ × α ⊕ ρ × α) (Fin t × σ × α ⊕ ρ × α) ℂ

Tensor a timed computation on the right with an identity and restore time-first order.

Equations

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

noncomputable def Complexity.ExactFourier.TimeLifts.left {σ α β : Type} [DecidableEq σ] (t : ℕ) (X : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) : Matrix (Fin t × σ × α ⊕ σ × β) (Fin t × σ × α ⊕ σ × β) ℂ

Tensor a timed computation on the left with an identity and restore time-first order.

Equations

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

theorem Complexity.ExactFourier.TimeLifts.right_unit {σ ρ α : Type} [Fintype σ] [Fintype ρ] [Fintype α] [DecidableEq σ] [DecidableEq ρ] [DecidableEq α] (t : ℕ) (X : Matrix (Fin t × σ ⊕ ρ) (Fin t × σ ⊕ ρ) ℂ) (hX : IsUnit X) : IsUnit (right t X)

theorem Complexity.ExactFourier.TimeLifts.left_unit {σ α β : Type} [Fintype σ] [Fintype α] [Fintype β] [DecidableEq σ] [DecidableEq α] [DecidableEq β] (t : ℕ) (X : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) (hX : IsUnit X) : IsUnit (left t X)

theorem Complexity.ExactFourier.TimeLifts.right_price {σ ρ α : Type} [Fintype σ] [Fintype ρ] [Fintype α] [DecidableEq σ] [DecidableEq ρ] [DecidableEq α] (p : MatrixPrice) (t : ℕ) (X : Matrix (Fin t × σ ⊕ ρ) (Fin t × σ ⊕ ρ) ℂ) (hX : IsUnit X) : p.value (right t X) = ↑(Fintype.card α) * p.value X

theorem Complexity.ExactFourier.TimeLifts.left_price {σ α β : Type} [Fintype σ] [Fintype α] [Fintype β] [DecidableEq σ] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (t : ℕ) (X : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) (hX : IsUnit X) : p.value (left t X) = ↑(Fintype.card σ) * p.value X

theorem Complexity.ExactFourier.TimeLifts.right_data {σ ρ α : Type} [Fintype σ] [Fintype α] [DecidableEq σ] [DecidableEq α] (t : ℕ) (X : Matrix (Fin t × σ ⊕ ρ) (Fin t × σ ⊕ ρ) ℂ) (H : Matrix σ σ (PowerSeries ℂ)) (hX : X.toBlocks₁₁ = (CoefficientTime.blockTruncHom t) H) : (right t X).toBlocks₁₁ = (CoefficientTime.blockTruncHom t) (Matrix.kroneckerMap (fun (x1 x2 : PowerSeries ℂ) => x1 * x2) H 1)

theorem Complexity.ExactFourier.TimeLifts.left_data {σ α β : Type} [Fintype σ] [Fintype α] [DecidableEq σ] [DecidableEq α] (t : ℕ) (X : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) (H : Matrix α α (PowerSeries ℂ)) (hX : X.toBlocks₁₁ = (CoefficientTime.blockTruncHom t) H) : (left t X).toBlocks₁₁ = (CoefficientTime.blockTruncHom t) (Matrix.kroneckerMap (fun (x1 x2 : PowerSeries ℂ) => x1 * x2) 1 H)

theorem Complexity.ExactFourier.TimeLifts.right_state {σ ρ α : Type} [DecidableEq α] (t : ℕ) (X : Matrix (Fin t × σ ⊕ ρ) (Fin t × σ ⊕ ρ) ℂ) (E : Matrix σ ρ (PowerSeries ℂ)) (hX : X.toBlocks₁₂ = CoefficientTime.coefficientColumns t E) : (right t X).toBlocks₁₂ = CoefficientTime.coefficientColumns t (Matrix.kroneckerMap (fun (x1 x2 : PowerSeries ℂ) => x1 * x2) E 1)

theorem Complexity.ExactFourier.TimeLifts.left_state {σ α β : Type} [DecidableEq σ] (t : ℕ) (X : Matrix (Fin t × α ⊕ β) (Fin t × α ⊕ β) ℂ) (E : Matrix α β (PowerSeries ℂ)) (hX : X.toBlocks₁₂ = CoefficientTime.coefficientColumns t E) : (left t X).toBlocks₁₂ = CoefficientTime.coefficientColumns t (Matrix.kroneckerMap (fun (x1 x2 : PowerSeries ℂ) => x1 * x2) 1 E)

@[reducible, inline]

abbrev Complexity.ExactFourier.TensorAxis.Space (β : Type) : ℕ → Type

The recursive coordinate space for a tensor power.

Equations

• Complexity.ExactFourier.TensorAxis.Space = Complexity.ExactFourier.Triangular.Bottom

@[reducible, inline]

abbrev Complexity.ExactFourier.TensorAxis.Fibers (β : Type) : ℕ → Type

The auxiliary call fibers accumulated by the recursive tensor construction.

Equations

• Complexity.ExactFourier.TensorAxis.Fibers = Complexity.ExactFourier.Triangular.Calls

noncomputable def Complexity.ExactFourier.TensorAxis.power {α R : Type} [CommSemiring R] (A : Matrix α α R) (k : ℕ) : Matrix (Space α k) (Space α k) R

The tensor power of a square matrix on the recursive coordinate space.

Equations

• Complexity.ExactFourier.TensorAxis.power A 0 = 1
• Complexity.ExactFourier.TensorAxis.power A t.succ = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (Complexity.ExactFourier.TensorAxis.power A t) A

@[simp]

theorem Complexity.ExactFourier.TensorAxis.card_space {α : Type} [Fintype α] (k : ℕ) : Fintype.card (Space α k) = Fintype.card α ^ k

theorem Complexity.ExactFourier.TensorAxis.map_power {α R S : Type} [CommSemiring R] [CommSemiring S] (f : R →+* S) (A : Matrix α α R) (k : ℕ) : (power A k).map ⇑f = power (A.map ⇑f) k

theorem Complexity.ExactFourier.TensorAxis.mul_power {α : Type} [Fintype α] {R : Type} [CommSemiring R] (A B : Matrix α α R) (k : ℕ) : power A k * power B k = power (A * B) k

@[simp]

theorem Complexity.ExactFourier.TensorAxis.power_one {α : Type} [DecidableEq α] {R : Type} [CommSemiring R] (k : ℕ) : power 1 k = 1

theorem Complexity.ExactFourier.TensorAxis.unit_power {α : Type} [Fintype α] [DecidableEq α] (A : Matrix α α ℂ) (hA : IsUnit A) (k : ℕ) : IsUnit (power A k)

theorem Complexity.ExactFourier.TensorAxis.price_power {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (A : Matrix α α ℂ) (hA : IsUnit A) (k : ℕ) : p.value (power A k) = ↑(Fintype.card (Fibers α k)) * p.value A