Exact Fourier circuits: cascade word

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

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

@[reducible, inline]

abbrev Complexity.ExactFourier.Cascade.States (α β : Type) : ℕ → Type

Auxiliary state coordinates accumulated by successive tensor cascade stages.

Equations

• Complexity.ExactFourier.Cascade.States α β 0 = PEmpty.{1}
• Complexity.ExactFourier.Cascade.States α β k.succ = (Complexity.ExactFourier.Cascade.States α β k × α ⊕ Complexity.ExactFourier.TensorAxis.Space α k × β)

@[reducible]

noncomputable instance Complexity.ExactFourier.Cascade.statesFintype (α β : Type) [Fintype α] [Fintype β] (k : ℕ) : Fintype (States α β k)

Equations

• Complexity.ExactFourier.Cascade.statesFintype α β 0 = { elems := ∅, complete := ⋯ }
• Complexity.ExactFourier.Cascade.statesFintype α β k.succ = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[reducible]

instance Complexity.ExactFourier.Cascade.statesDecidableEq (α β : Type) [DecidableEq α] [DecidableEq β] (k : ℕ) : DecidableEq (States α β k)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Cascade.statesDecidableEq α β 0 = instDecidableEqPEmpty

noncomputable def Complexity.ExactFourier.Cascade.response {α β : Type} [DecidableEq α] (H : Matrix α α (PowerSeries ℂ)) (S : Matrix α β (PowerSeries ℂ)) (k : ℕ) : Matrix (TensorAxis.Space α k) (States α β k) (PowerSeries ℂ)

The formal power series response of the cascade's accumulated state coordinates.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Cascade.response H S 0 = 0

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

Join successive time-domain cell computations into a tensor cascade.

Equations

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

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

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

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

theorem Complexity.ExactFourier.Cascade.columns_fromCols {σ ρ τ : Type} (t : ℕ) (E : Matrix σ ρ (PowerSeries ℂ)) (F : Matrix σ τ (PowerSeries ℂ)) : CoefficientTime.coefficientColumns t (E.fromCols F) = (CoefficientTime.coefficientColumns t E).fromCols (CoefficientTime.coefficientColumns t F)

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

@[reducible, inline]

abbrev Complexity.ExactFourier.CellPoly.ps : Polynomial ℂ →+* PowerSeries ℂ

The canonical embedding of complex polynomials into formal power series.

Equations

• Complexity.ExactFourier.CellPoly.ps = Polynomial.coeToPowerSeries.ringHom

theorem Complexity.ExactFourier.CellPoly.map_smul {R S : Type} [CommSemiring R] [CommSemiring S] {ι κ : Type} (f : R →+* S) (a : R) (A : Matrix ι κ R) : (a • A).map ⇑f = f a • A.map ⇑f

noncomputable def Complexity.ExactFourier.CellPoly.Z {β : Type} [DecidableEq β] (D : Matrix β β ℂ) : Matrix β β (Polynomial ℂ)

The polynomial matrix 1 - X • D governing the cell's state feedback.

Equations

• Complexity.ExactFourier.CellPoly.Z D = 1 - Polynomial.X • D.map ⇑Polynomial.C

noncomputable def Complexity.ExactFourier.CellPoly.a {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : Polynomial ℂ

The determinant of the cell's polynomial state-feedback matrix.

Equations

• Complexity.ExactFourier.CellPoly.a D = (Complexity.ExactFourier.CellPoly.Z D).det

noncomputable def Complexity.ExactFourier.CellPoly.R {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : Matrix β β (Polynomial ℂ)

The adjugate of the cell's polynomial state-feedback matrix.

Equations

• Complexity.ExactFourier.CellPoly.R D = (Complexity.ExactFourier.CellPoly.Z D).adjugate

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

The cell's transfer numerator after clearing its state-feedback denominator.

Equations

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

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

The determinant of the cleared transfer numerator.

Equations

• Complexity.ExactFourier.CellPoly.b M C B D = (Complexity.ExactFourier.CellPoly.F M C B D).det

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

The adjugate of the cleared transfer numerator.

Equations

• Complexity.ExactFourier.CellPoly.J M C B D = (Complexity.ExactFourier.CellPoly.F M C B D).adjugate

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

The adjugate of the transfer numerator scaled by the state denominator.

Equations

• Complexity.ExactFourier.CellPoly.L M C B D = Complexity.ExactFourier.CellPoly.a D • Complexity.ExactFourier.CellPoly.J M C B D

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

The cleared state-response numerator formed from the two adjugates.

Equations

• Complexity.ExactFourier.CellPoly.T M C B D = Complexity.ExactFourier.CellPoly.J M C B D * C.map ⇑Polynomial.C * Complexity.ExactFourier.CellPoly.R D

theorem Complexity.ExactFourier.CellPoly.map_const {ι κ : Type} (A : Matrix ι κ ℂ) : (A.map ⇑Polynomial.C).map ⇑ps = A.map ⇑PowerSeries.C

@[simp]

theorem Complexity.ExactFourier.CellPoly.map_Z {β : Type} [DecidableEq β] (D : Matrix β β ℂ) : (Z D).map ⇑ps = 1 - PowerSeries.X • D.map ⇑PowerSeries.C

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

theorem Complexity.ExactFourier.CellPoly.eval_a_zero {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : Polynomial.eval 0 (a D) = 1

theorem Complexity.ExactFourier.CellPoly.eval_F_zero {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : (F M C B D).map ⇑(Polynomial.evalRingHom 0) = M

@[simp]

theorem Complexity.ExactFourier.CellPoly.eval_b_zero {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : Polynomial.eval 0 (b M C B D) = M.det

theorem Complexity.ExactFourier.CellPoly.cleared_resolvent {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) : ps (a D) • CellSeries.resolvent D = (R D).map ⇑ps

theorem Complexity.ExactFourier.CellPoly.cleared_state {α β : Type} [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) : ps (a D) • CellSeries.state C D = (C.map ⇑Polynomial.C * R D).map ⇑ps

theorem Complexity.ExactFourier.CellPoly.cleared_transfer {α β : Type} [Fintype β] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : ps (a D) • CellSeries.transfer M C B D = (F M C B D).map ⇑ps

theorem Complexity.ExactFourier.CellPoly.right_clearing {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : CellSeries.transfer M C B D * (L M C B D).map ⇑ps = ps (b M C B D) • 1

theorem Complexity.ExactFourier.CellPoly.state_clearing {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) : CellSeries.transfer M C B D * (T M C B D).map ⇑ps = ps (b M C B D) • CellSeries.state C D

theorem Complexity.ExactFourier.Cascade.power_smul {α R : Type} [CommSemiring R] (c : R) (A : Matrix α α R) (k : ℕ) : TensorAxis.power (c • A) k = c ^ k • TensorAxis.power A k

noncomputable def Complexity.ExactFourier.Cascade.cleared {α β : Type} [DecidableEq α] {R : Type} [CommSemiring R] (b : R) (L : Matrix α α R) (T : Matrix α β R) (k : ℕ) : Matrix (TensorAxis.Space α k) (States α β k) R

Recursively assemble the cascade response with its denominators cleared.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Cascade.cleared b L T 0 = 0

theorem Complexity.ExactFourier.Cascade.map_cleared {α β : Type} [DecidableEq α] {R S : Type} [CommSemiring R] [CommSemiring S] (f : R →+* S) (b : R) (L : Matrix α α R) (T : Matrix α β R) (k : ℕ) : (cleared b L T k).map ⇑f = cleared (f b) (L.map ⇑f) (T.map ⇑f) k

theorem Complexity.ExactFourier.Cascade.clearing_identity {α β : Type} [Fintype α] [DecidableEq α] (c : PowerSeries ℂ) (H L : Matrix α α (PowerSeries ℂ)) (S T : Matrix α β (PowerSeries ℂ)) (hL : H * L = c • 1) (hT : H * T = c • S) (k : ℕ) : TensorAxis.power H k * cleared c L T k = c ^ k • response H S k

theorem Complexity.ExactFourier.Cascade.cell_clearing {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (B : Matrix β α ℂ) (D : Matrix β β ℂ) (k : ℕ) : TensorAxis.power (CellSeries.transfer M C B D) k * (cleared (CellPoly.b M C B D) (CellPoly.L M C B D) (CellPoly.T M C B D) k).map ⇑CellPoly.ps = CellPoly.ps (CellPoly.b M C B D ^ k) • response (CellSeries.transfer M C B D) (CellSeries.state C D) k

noncomputable def Complexity.ExactFourier.PolynomialMatrix.bound {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix ι κ (Polynomial ℂ)) : ℕ

The sum of entry degrees, bounding the degree of every matrix entry.

Equations

• Complexity.ExactFourier.PolynomialMatrix.bound A = ∑ i : ι, ∑ j : κ, (A i j).natDegree

theorem Complexity.ExactFourier.PolynomialMatrix.le_bound {ι κ : Type} [Fintype ι] [Fintype κ] (A : Matrix ι κ (Polynomial ℂ)) (i : ι) (j : κ) : (A i j).natDegree ≤ bound A

def Complexity.ExactFourier.PolynomialMatrix.Bounded {ι κ : Type} (A : Matrix ι κ (Polynomial ℂ)) (d : ℕ) : Prop

Every entry of the polynomial matrix has degree at most d.

Equations

• Complexity.ExactFourier.PolynomialMatrix.Bounded A d = ∀ (i : ι) (j : κ), (A i j).natDegree ≤ d

theorem Complexity.ExactFourier.PolynomialMatrix.bounded_one {ι : Type} [DecidableEq ι] : Bounded 1 0

theorem Complexity.ExactFourier.PolynomialMatrix.bounded_tensor {ι κ τ υ : Type} (A : Matrix ι κ (Polynomial ℂ)) (B : Matrix τ υ (Polynomial ℂ)) {d e : ℕ} (hA : Bounded A d) (hB : Bounded B e) : Bounded (Matrix.kroneckerMap (fun (x1 x2 : Polynomial ℂ) => x1 * x2) A B) (d + e)

theorem Complexity.ExactFourier.PolynomialMatrix.bounded_smul {ι κ : Type} (b : Polynomial ℂ) (A : Matrix ι κ (Polynomial ℂ)) {d e : ℕ} (hb : b.natDegree ≤ d) (hA : Bounded A e) : Bounded (b • A) (d + e)

theorem Complexity.ExactFourier.PolynomialMatrix.bounded_power {α : Type} (A : Matrix α α (Polynomial ℂ)) {d : ℕ} (hA : Bounded A d) (k : ℕ) : Bounded (TensorAxis.power A k) (k * d)

theorem Complexity.ExactFourier.Cascade.bounded_cleared {α β : Type} [DecidableEq α] (b : Polynomial ℂ) (L : Matrix α α (Polynomial ℂ)) (T : Matrix α β (Polynomial ℂ)) {d : ℕ} (hb : b.natDegree ≤ d) (hL : PolynomialMatrix.Bounded L d) (hT : PolynomialMatrix.Bounded T d) (k : ℕ) : PolynomialMatrix.Bounded (cleared b L T k) (k * d)

theorem Complexity.ExactFourier.Cascade.exists_cleared_degree {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] (b : Polynomial ℂ) (L : Matrix α α (Polynomial ℂ)) (T : Matrix α β (Polynomial ℂ)) : ∃ (d : ℕ), ∀ (k : ℕ), PolynomialMatrix.Bounded (cleared b L T k) (k * d)