Exact Fourier circuits: cascade limit

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/CascadeLimit.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.cascadeError (m : ℕ) : ℝ

The vanishing error term in the asymptotic cascade cost estimate.

Equations

• Complexity.ExactFourier.cascadeError m = Real.log (2 * (↑m + 2) ^ 4) / (↑m + 1) + (↑m + 2) ^ 3 / ((↑m + 2) ^ 4 * (↑m + 1))

theorem Complexity.ExactFourier.cascadeError_tendsto : Filter.Tendsto cascadeError Filter.atTop (nhds 0)

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

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

theorem Complexity.ExactFourier.MatrixPrice.submatrix_equiv (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℂ) (hA : IsUnit A) (e f : κ ≃ ι) : p.value (A.submatrix ⇑e ⇑f) = p.value A

noncomputable def Complexity.ExactFourier.extendInjection {ι κ : Type} [Fintype κ] (f : κ → ι) (hf : Function.Injective f) : κ ⊕ { i : ι // i ∉ Set.range f } ≃ ι

Complete an injection to an equivalence by adjoining its range complement.

Equations

• Complexity.ExactFourier.extendInjection f hf = ((Equiv.ofInjective f hf).sumCongr (Equiv.refl { i : ι // i ∉ Set.range f })).trans (Equiv.Set.sumCompl (Set.range f))

@[simp]

theorem Complexity.ExactFourier.extendInjection_inl {ι κ : Type} [Fintype κ] (f : κ → ι) (hf : Function.Injective f) (j : κ) : (extendInjection f hf) (Sum.inl j) = f j

theorem Complexity.ExactFourier.MatrixPrice.corner (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (K : Matrix ι ι ℂ) (hK : IsUnit K) (rows cols : κ → ι) (hr : Function.Injective rows) (hc : Function.Injective cols) (hM : IsUnit (K.submatrix rows cols)) : p.value (K.submatrix rows cols) ≤ p.value K

theorem Complexity.ExactFourier.MatrixPrice.le_shear (p : MatrixPrice) {ι : Type} [Fintype ι] [DecidableEq ι] (G : Matrix ι ι ℂ) (hG : IsUnit G) : p.value G ≤ p.value (rectangularShear G)

theorem Complexity.ExactFourier.TypedDAG.price {ι : Type} [Fintype ι] [DecidableEq ι] (C : TypedDAG ι ι) (p : MatrixPrice) (G : Matrix ι ι ℂ) (hG : IsUnit G) (hC : ∀ (x : ι → ℂ), C.eval x = G.mulVec x) : p.value G ≤ 8 * ↑C.size + 2 * ↑(Fintype.card ι)

noncomputable def Complexity.ExactFourier.TypedDAG.weightedBlocks {α β γ ι : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] (W : Matrix α (β × γ) ℂ) (C : γ → TypedDAG ι ι) : TypedDAG (β × ι) (α × ι)

Combine copies of component circuits using a matrix of scalar block weights.

Equations

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

noncomputable def Complexity.ExactFourier.TypedDAG.blockMatrix {α β γ ι : Type} [Fintype γ] (W : Matrix α (β × γ) ℂ) (G : γ → Matrix ι ι ℂ) : Matrix (α × ι) (β × ι) ℂ

The matrix obtained by summing the scalar-weighted component blocks.

Equations

• Complexity.ExactFourier.TypedDAG.blockMatrix W G a b = ∑ g : γ, W a.1 (b.1, g) * G g a.2 b.2

theorem Complexity.ExactFourier.TypedDAG.size_weightedBlocks {α β γ ι : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] (W : Matrix α (β × γ) ℂ) (C : γ → TypedDAG ι ι) : (weightedBlocks W C).size = Fintype.card β * ∑ g : γ, (C g).size + 2 * Fintype.card ι * Fintype.card α * Fintype.card β * Fintype.card γ

theorem Complexity.ExactFourier.TypedDAG.eval_weightedBlocks {α β γ ι : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype ι] (W : Matrix α (β × γ) ℂ) (C : γ → TypedDAG ι ι) (G : γ → Matrix ι ι ℂ) (hC : ∀ (g : γ) (x : ι → ℂ), (C g).eval x = (G g).mulVec x) (x : β × ι → ℂ) : (weightedBlocks W C).eval x = (blockMatrix W G).mulVec x

noncomputable def Complexity.ExactFourier.TypedDAG.addIdentity {ι : Type} [Fintype ι] (C : TypedDAG ι ι) : TypedDAG ι ι

Add the original input coordinatewise to the circuit's output.

Equations

• C.addIdentity = Complexity.ExactFourier.TypedDAG.addPair.comp (Complexity.ExactFourier.TypedDAG.identity.fanout C)

@[simp]

theorem Complexity.ExactFourier.TypedDAG.size_addIdentity {ι : Type} [Fintype ι] (C : TypedDAG ι ι) : C.addIdentity.size = C.size + Fintype.card ι

theorem Complexity.ExactFourier.TypedDAG.eval_addIdentity {ι : Type} [Fintype ι] [DecidableEq ι] (C : TypedDAG ι ι) (A : Matrix ι ι ℂ) (hC : ∀ (x : ι → ℂ), C.eval x = A.mulVec x) (x : ι → ℂ) : C.addIdentity.eval x = (1 + A).mulVec x

theorem Complexity.ExactFourier.Boundary.exists_tensor_coefficient_dag {α : Type} [Fintype α] (G : Matrix α α (Polynomial ℂ)) : ∃ (B : ℕ), ∀ (k j : ℕ), ∃ (C : TypedDAG (TensorAxis.Space α k) (TensorAxis.Space α k)), C.size ≤ B * (k + 1) ^ 2 * Fintype.card α ^ k ∧ ∀ (x : TensorAxis.Space α k → ℂ), C.eval x = (coefficientMatrix (TensorAxis.power G k) j).mulVec x

@[reducible, inline]

abbrev Complexity.ExactFourier.Boundary.Times (t d e : ℕ) : Type

The active boundary times among the first t coefficients.

Equations

• Complexity.ExactFourier.Boundary.Times t d e = { a : Fin t // Complexity.ExactFourier.Boundary.ActiveTime t d e ↑a }

theorem Complexity.ExactFourier.Boundary.card_times (t d e : ℕ) : Fintype.card (Times t d e) ≤ e + 2 * d

def Complexity.ExactFourier.Boundary.timeActiveSplit {ι : Type} (t d e : ℕ) : Times t d e × ι ⊕ { a : Fin t // ¬ActiveTime t d e ↑a } × ι ≃ Fin t × ι

Separate active and inactive times while retaining each spatial coordinate.

Equations

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

noncomputable def Complexity.ExactFourier.Boundary.activeMatrix {ι : Type} [Fintype ι] [DecidableEq ι] (t d e : ℕ) (η ℓ : Polynomial ℂ) (J G : Matrix ι ι (Polynomial ℂ)) : Matrix (Times t d e × ι) (Times t d e × ι) ℂ

The identity plus the correction restricted to active input and output times.

Equations

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

theorem Complexity.ExactFourier.Boundary.active_split {ι : Type} [Fintype ι] [DecidableEq ι] (t d e : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (ht : ℓ.natDegree = t) (hd : 0 < d) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) (hJ : ∀ (i j : ι), (J i j).natDegree ≤ e) : (1 + activeCorrection t d η ℓ J G).submatrix ⇑(timeActiveSplit t d e) ⇑(timeActiveSplit t d e) = Matrix.fromBlocks (activeMatrix t d e η ℓ J G) 0 0 1

theorem Complexity.ExactFourier.Boundary.active_price {ι : Type} [Fintype ι] [DecidableEq ι] (p : MatrixPrice) (t d e : ℕ) (η ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (J G : Matrix ι ι (Polynomial ℂ)) (ht : ℓ.natDegree = t) (hd : 0 < d) (hG : ∀ (i j : ι), (G i j).natDegree ≤ d) (hJ : ∀ (i j : ι), (J i j).natDegree ≤ e) (hu : IsUnit (1 + activeCorrection t d η ℓ J G)) : IsUnit (activeMatrix t d e η ℓ J G) ∧ p.value (1 + activeCorrection t d η ℓ J G) = p.value (activeMatrix t d e η ℓ J G)