Exact Fourier circuits: word scheduling

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/WordScheduling.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.Packing.scheduledStep {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : Word D A α) {T : ℕ} (time : Fin (List.length W) → Fin T) : Fin T → Step D A α

Place each word step at its scheduled time and use identity steps in empty slots.

Equations

• Complexity.ExactFourier.Packing.scheduledStep W time = Function.extend time (List.get W) fun (x : Fin T) => Complexity.ExactFourier.Packing.Step.mono 1 ⋯

theorem Complexity.ExactFourier.Packing.scheduledStep_matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : Word D A α) {T : ℕ} (time : Fin (List.length W) → Fin T) (hinj : Function.Injective time) (t : Fin T) : (scheduledStep W time t).matrix = Function.extend time (fun (i : Fin (List.length W)) => (List.get W i).matrix) (fun (x : Fin T) => 1) t

theorem Complexity.ExactFourier.Packing.scheduledStep_product {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (W : Word D A α) {T : ℕ} (time : Fin (List.length W) → Fin T) (ht : StrictMono time) : (List.ofFn fun (t : Fin T) => (scheduledStep W time t).matrix).prod = W.matrix

noncomputable def Complexity.ExactFourier.Packing.scheduledLayer {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [DecidableEq π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] (W : (p : π) → Word D A (β p)) {T : ℕ} (time : (p : π) → Fin (List.length (W p)) → Fin T) (t : Fin T) : Matrix ((p : π) × β p) ((p : π) × β p) ℂ

The block diagonal matrix of all words' scheduled steps at one time.

Equations

• Complexity.ExactFourier.Packing.scheduledLayer W time t = Matrix.blockDiagonal' fun (p : π) => (Complexity.ExactFourier.Packing.scheduledStep (W p) (time p) t).matrix

theorem Complexity.ExactFourier.Packing.scheduledLayer_product {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] [DecidableEq π] {β : π → Type} [(p : π) → Fintype (β p)] [(p : π) → DecidableEq (β p)] (W : (p : π) → Word D A (β p)) {T : ℕ} (time : (p : π) → Fin (List.length (W p)) → Fin T) (ht : ∀ (p : π), StrictMono (time p)) : (List.ofFn (scheduledLayer W time)).prod = Matrix.blockDiagonal' fun (p : π) => (W p).matrix

Schedule correctness on fixed, disjoint physical supports, including every monomial.

def Complexity.ExactFourier.Packing.Word.substitute {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (V : (t : τ) → Word E B (D t)) : Word D A α → Word E B α

Replace every species call by its supplied realization, retaining monomial steps.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Packing.Word.substitute V [] = []

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_substitute {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (V : (t : τ) → Word E B (D t)) (hV : ∀ (t : τ), (V t).matrix = A t) (W : Word D A α) : (substitute V W).matrix = W.matrix

def Complexity.ExactFourier.Packing.Word.weight {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (p : τ → ℝ) (W : Word D A α) : ℝ

The total price of the word's species calls, with monomial steps uncharged.

Equations

• Complexity.ExactFourier.Packing.Word.weight p W = (List.map p W.calls).sum

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_nil {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (p : τ → ℝ) : weight p [] = 0

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_cons_mono {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (p : τ → ℝ) (M : Matrix α α ℂ) (h : MonomialMatrix M) (W : Word D A α) : weight p (Step.mono M h :: W) = weight p W

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_cons_call {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (p : τ → ℝ) (t : τ) (e : D t ↪ α) (W : Word D A α) : weight p (Step.call t e :: W) = p t + weight p W

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_append {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (p : τ → ℝ) (W V : Word D A α) : weight p (W ++ V) = weight p W + weight p V

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_embed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] {β : Type} [Fintype β] [DecidableEq β] (p : τ → ℝ) (e : α ↪ β) (W : Word D A α) : weight p (embed e W) = weight p W

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_reindex {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] {β : Type} [Fintype β] [DecidableEq β] (p : τ → ℝ) (e : α ≃ β) (W : Word D A α) : weight p (reindex e W) = weight p W

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_substitute {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (V : (t : τ) → Word E B (D t)) (p : σ → ℝ) (W : Word D A α) : weight p (substitute V W) = weight (fun (t : τ) => weight p (V t)) W

theorem Complexity.ExactFourier.Packing.Word.weight_count {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] [Fintype τ] [DecidableEq τ] (p : τ → ℝ) (W : Word D A α) : weight p W = ∑ t : τ, ↑(W.count t) * p t

theorem Complexity.ExactFourier.MonomialMatrix.inverse {α : Type} [Fintype α] [DecidableEq α] {A : Matrix α α ℂ} (hA : MonomialMatrix A) : MonomialMatrix A⁻¹

theorem Complexity.ExactFourier.MonomialMatrix.submatrix_unit {α : Type} [Fintype α] [DecidableEq α] {β : Type} [DecidableEq β] {B : Matrix β β ℂ} (hB : MonomialMatrix B) (e f : α ↪ β) (hA : IsUnit (B.submatrix ⇑e ⇑f)) : MonomialMatrix (B.submatrix ⇑e ⇑f)

A unit square submatrix of a monomial matrix is monomial.

theorem Complexity.ExactFourier.Packing.pattern_from_word {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (V : Word D A α) {H : Matrix α α ℂ} {h : ℕ} (hp : PositiveGeneration.Pattern V.matrix h H) : ∃ (W : Word D A α), W.matrix = H ∧ ∀ (p : τ → ℝ), Word.weight p W = ↑h * Word.weight p V

theorem Complexity.ExactFourier.Packing.word_generates {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (V : Word D A α) (hu : IsUnit V.matrix) (hn : ¬MonomialMatrix V.matrix) (H : Matrix α α ℂ) (hH : IsUnit H) : ∃ (h : ℕ), 0 < h ∧ ∃ (W : Word D A α), W.matrix = H ∧ ∀ (p : τ → ℝ), Word.weight p W = ↑h * Word.weight p V

theorem Complexity.ExactFourier.Packing.monomial_of_subsingleton {α : Type} [Fintype α] [DecidableEq α] [Subsingleton α] (H : Matrix α α ℂ) (hH : IsUnit H) : MonomialMatrix H

def Complexity.ExactFourier.Packing.shearU : Matrix (Fin 2) (Fin 2) ℂ

The elementary shear adding the first coordinate to the second.

Equations

• Complexity.ExactFourier.Packing.shearU = Matrix.transvection 1 0 1

theorem Complexity.ExactFourier.Packing.shearU_unit : IsUnit shearU

theorem Complexity.ExactFourier.Packing.shearU_not_monomial : ¬MonomialMatrix shearU

theorem Complexity.ExactFourier.Packing.shear_word_exists {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (u : τ) (eu : D u ≃ Fin 2) (hAu : (Matrix.reindex eu eu) (A u) = shearU) (H : Matrix α α ℂ) (hH : IsUnit H) : ∃ (C : ℕ) (W : Word D A α), W.matrix = H ∧ ∀ (p : τ → ℝ), Word.weight p W = ↑C * p u

theorem Complexity.ExactFourier.reindex_comp {α β γ : Type} (e : α ≃ β) (f : β ≃ γ) (M : Matrix α α ℂ) : (Matrix.reindex f f) ((Matrix.reindex e e) M) = (Matrix.reindex (e.trans f) (e.trans f)) M

theorem Complexity.ExactFourier.reindex_sum {α β γ δ : Type} (e : α ≃ β) (f : γ ≃ δ) (M : Matrix α α ℂ) (N : Matrix γ γ ℂ) : (Matrix.reindex (e.sumCongr f) (e.sumCongr f)) (Matrix.fromBlocks M 0 0 N) = Matrix.fromBlocks ((Matrix.reindex e e) M) 0 0 ((Matrix.reindex f f) N)

theorem Complexity.ExactFourier.reindex_tensor {α β γ δ : Type} (e : α ≃ β) (f : γ ≃ δ) (M : Matrix α α ℂ) (N : Matrix γ γ ℂ) : (Matrix.reindex (e.prodCongr f) (e.prodCongr f)) (M.kronecker N) = ((Matrix.reindex e e) M).kronecker ((Matrix.reindex f f) N)

theorem Complexity.ExactFourier.reindex_inverse {α β : Type} (e : α ≃ β) (M : Matrix α α ℂ) : (Matrix.reindex e.symm e.symm) ((Matrix.reindex e e) M) = M

theorem Complexity.ExactFourier.Embedded.matrix_domain {α β γ : Type} [Fintype α] [DecidableEq γ] (e : α ≃ β) (f : α ↪ γ) (M : Matrix α α ℂ) : matrix (e.symm.toEmbedding.trans f) ((Matrix.reindex e e) M) = matrix f M

def Complexity.ExactFourier.Packing.Step.rename {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : τ → σ) (e : (t : τ) → D t ≃ E (f t)) : Step D A α → Step E B α

Rename a step's species and transport its call coordinates through an equivalence.

Equations

• Complexity.ExactFourier.Packing.Step.rename f e (Complexity.ExactFourier.Packing.Step.mono M h) = Complexity.ExactFourier.Packing.Step.mono M h
• Complexity.ExactFourier.Packing.Step.rename f e (Complexity.ExactFourier.Packing.Step.call t a) = Complexity.ExactFourier.Packing.Step.call (f t) ((e t).symm.toEmbedding.trans a)

def Complexity.ExactFourier.Packing.Word.rename {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : τ → σ) (e : (t : τ) → D t ≃ E (f t)) (W : Word D A α) : Word E B α

Rename the species and coordinate types of every call in a word.

Equations

• Complexity.ExactFourier.Packing.Word.rename f e W = List.map (Complexity.ExactFourier.Packing.Step.rename f e) W

theorem Complexity.ExactFourier.Packing.Word.matrix_rename {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : τ → σ) (e : (t : τ) → D t ≃ E (f t)) (he : ∀ (t : τ), (Matrix.reindex (e t) (e t)) (A t) = B (f t)) (W : Word D A α) : (rename f e W).matrix = W.matrix

@[simp]

theorem Complexity.ExactFourier.Packing.Word.weight_rename {τ σ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {E : σ → Type} [(t : σ) → Fintype (E t)] [(t : σ) → DecidableEq (E t)] {B : (t : σ) → Matrix (E t) (E t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (f : τ → σ) (e : (t : τ) → D t ≃ E (f t)) (p : σ → ℝ) (W : Word D A α) : weight p (rename f e W) = weight (p ∘ f) W