Exact Fourier circuits: multi word

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

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

inductive Complexity.ExactFourier.Packing.Step {τ : Type} (D : τ → Type) [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] (A : (t : τ) → Matrix (D t) (D t) ℂ) (α : Type) [Fintype α] [DecidableEq α] : Type

A monomial transformation or an embedded call to one matrix species.

• mono {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : Step D A α
• call {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (t : τ) (e : D t ↪ α) : Step D A α

noncomputable def Complexity.ExactFourier.Packing.Step.matrix {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] : Step D A α → Matrix α α ℂ

The ambient matrix represented by a monomial step or an embedded species call.

Equations

• (Complexity.ExactFourier.Packing.Step.mono M hm).matrix = M
• (Complexity.ExactFourier.Packing.Step.call t e).matrix = Complexity.ExactFourier.Embedded.matrix e (A t)

def Complexity.ExactFourier.Packing.Step.kind {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] : Step D A α → Option τ

The called species, with none for a monomial step.

Equations

• (Complexity.ExactFourier.Packing.Step.mono M hm).kind = none
• (Complexity.ExactFourier.Packing.Step.call t e).kind = some t

noncomputable def Complexity.ExactFourier.Packing.Step.embed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) : Step D A α → Step D A β

Embed a step in a larger coordinate set, fixing all new coordinates.

Equations

• Complexity.ExactFourier.Packing.Step.embed e (Complexity.ExactFourier.Packing.Step.mono M hm) = Complexity.ExactFourier.Packing.Step.mono (Complexity.ExactFourier.Embedded.matrix e M) ⋯
• Complexity.ExactFourier.Packing.Step.embed e (Complexity.ExactFourier.Packing.Step.call t e_1) = Complexity.ExactFourier.Packing.Step.call t (e_1.trans e)

@[simp]

theorem Complexity.ExactFourier.Packing.Step.matrix_embed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) (s : Step D A α) : (embed e s).matrix = Embedded.matrix e s.matrix

@[simp]

theorem Complexity.ExactFourier.Packing.Step.kind_embed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) (s : Step D A α) : (embed e s).kind = s.kind

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.Word {τ : Type} (D : τ → Type) [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] (A : (t : τ) → Matrix (D t) (D t) ℂ) (α : Type) [Fintype α] [DecidableEq α] : Type

A finite list of monomial steps and calls to the given matrix species.

Equations

• Complexity.ExactFourier.Packing.Word D A α = List (Complexity.ExactFourier.Packing.Step D A α)

noncomputable def Complexity.ExactFourier.Packing.Word.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 α) : Matrix α α ℂ

The ordered product of the matrices represented by the word's steps.

Equations

• W.matrix = (List.map Complexity.ExactFourier.Packing.Step.matrix W).prod

def Complexity.ExactFourier.Packing.Word.calls {τ : 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 α) : List τ

The sequence of called species after removing monomial steps.

Equations

• W.calls = List.filterMap Complexity.ExactFourier.Packing.Step.kind W

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

The number of times a word calls the specified species.

Equations

• W.count t = List.count t W.calls

noncomputable def Complexity.ExactFourier.Packing.Word.embed {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) (W : Word D A α) : Word D A β

Embed every step of a word into a larger coordinate set.

Equations

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

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_nil {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] : matrix [] = 1

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_cons {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (s : Step D A α) (W : Word D A α) : matrix (s :: W) = s.matrix * W.matrix

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Complexity.ExactFourier.Packing.Word.unit {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (hA : ∀ (t : τ), IsUnit (A t)) (W : Word D A α) : IsUnit W.matrix

def Complexity.ExactFourier.Packing.monoWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : Word D A α

A word consisting of one monomial transformation and no species calls.

Equations

• Complexity.ExactFourier.Packing.monoWord M hm = [Complexity.ExactFourier.Packing.Step.mono M hm]

def Complexity.ExactFourier.Packing.callWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (t : τ) (e : D t ↪ α) : Word D A α

A word consisting of one embedded call to the specified species.

Equations

• Complexity.ExactFourier.Packing.callWord t e = [Complexity.ExactFourier.Packing.Step.call t e]

@[simp]

theorem Complexity.ExactFourier.Packing.matrix_monoWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : (monoWord M hm).matrix = M

@[simp]

theorem Complexity.ExactFourier.Packing.matrix_callWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (t : τ) (e : D t ↪ α) : (callWord t e).matrix = Embedded.matrix e (A t)

@[simp]

theorem Complexity.ExactFourier.Packing.calls_monoWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hm : MonomialMatrix M) : (monoWord M hm).calls = []

@[simp]

theorem Complexity.ExactFourier.Packing.calls_callWord {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (t : τ) (e : D t ↪ α) : (callWord t e).calls = [t]

theorem Complexity.ExactFourier.Packing.pattern_word {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} (t : τ) {H : Matrix (D t) (D t) ℂ} {k : ℕ} (h : PositiveGeneration.Pattern (A t) k H) : ∃ (W : Word D A (D t)), W.matrix = H ∧ W.calls = List.replicate k t

def Complexity.ExactFourier.Embedded.sigmaIn {π : Type} {β : π → Type} (p : π) : β p ↪ (p : π) × β p

Embed one summand into a dependent sum of coordinate types.

Equations

• Complexity.ExactFourier.Embedded.sigmaIn p = { toFun := Sigma.mk p, inj' := ⋯ }

theorem Complexity.ExactFourier.Embedded.matrix_sigmaIn {π : Type} [DecidableEq π] {β : π → Type} [(i : π) → DecidableEq (β i)] (A : (p : π) → Matrix (β p) (β p) ℂ) (p : π) : matrix (sigmaIn p) (A p) = Matrix.blockDiagonal' (Function.update 1 p (A p))

theorem Complexity.ExactFourier.Embedded.list_update_prod {π : Type} [DecidableEq π] {R : π → Type} [(i : π) → Monoid (R i)] (A : (i : π) → R i) (L : List π) (hL : L.Nodup) (p : π) : (List.map (fun (i : π) => Function.update 1 i (A i)) L).prod p = if p ∈ L then A p else 1

theorem Complexity.ExactFourier.Embedded.blockDiagonal'_product {π : Type} [Fintype π] [DecidableEq π] {β : π → Type} [(i : π) → Fintype (β i)] [(i : π) → DecidableEq (β i)] (A : (p : π) → Matrix (β p) (β p) ℂ) : (List.map (fun (p : π) => matrix (sigmaIn p) (A p)) Finset.univ.toList).prod = Matrix.blockDiagonal' A

theorem Complexity.ExactFourier.Embedded.card_complement {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] (e : β ↪ α) : Fintype.card β + Fintype.card (complement e) = Fintype.card α

theorem Complexity.ExactFourier.Embedded.exists_completion {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq γ] (e : β ↪ α) (f : β ↪ γ) (hcard : Fintype.card α ≤ Fintype.card γ) : ∃ (g : α ↪ γ), e.trans g = f

Complete a prescribed active-tuple matching with untouched spectator wires.

theorem Complexity.ExactFourier.Embedded.realize_active {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq γ] (e : β ↪ α) (f : β ↪ γ) (A : Matrix β β ℂ) (hcard : Fintype.card α ≤ Fintype.card γ) : ∃ (g : α ↪ γ), matrix g (matrix e A) = matrix f A

def Complexity.ExactFourier.Embedded.sigmaEmbed {π : Type} {δ ε : π → Type} (e : (p : π) → δ p ↪ ε p) : (p : π) × δ p ↪ (p : π) × ε p

Combine a family of embeddings into an embedding of dependent sums.

Equations

• Complexity.ExactFourier.Embedded.sigmaEmbed e = { toFun := fun (i : (p : π) × δ p) => ⟨i.fst, (e i.fst) i.snd⟩, inj' := ⋯ }

theorem Complexity.ExactFourier.Embedded.matrix_sigmaEmbed {π : Type} [Fintype π] [DecidableEq π] {δ ε : π → Type} [(p : π) → Fintype (δ p)] [(p : π) → DecidableEq (ε p)] (e : (p : π) → δ p ↪ ε p) (A : (p : π) → Matrix (δ p) (δ p) ℂ) : matrix (sigmaEmbed e) (Matrix.blockDiagonal' A) = Matrix.blockDiagonal' fun (p : π) => matrix (e p) (A p)

theorem Complexity.ExactFourier.Packing.Word.matrix_flatten {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (L : List (Word D A α)) : matrix L.flatten = (List.map matrix L).prod

theorem Complexity.ExactFourier.Packing.Word.calls_flatten {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] (L : List (Word D A α)) : calls L.flatten = (List.map calls L).flatten

noncomputable def Complexity.ExactFourier.Packing.Word.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 β] (e : α ≃ β) (W : Word D A α) : Word D A β

Relabel a word's coordinates by an equivalence.

Equations

• Complexity.ExactFourier.Packing.Word.reindex e W = Complexity.ExactFourier.Packing.Word.embed e.toEmbedding W

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_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 β] (e : α ≃ β) (W : Word D A α) : (reindex e W).matrix = (Matrix.reindex e e) W.matrix

@[simp]

theorem Complexity.ExactFourier.Packing.Word.calls_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 β] (e : α ≃ β) (W : Word D A α) : (reindex e W).calls = W.calls

noncomputable def Complexity.ExactFourier.Packing.Word.blockSum {τ : 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)) : Word D A ((p : π) × β p)

Concatenate words embedded into their disjoint dependent coordinate blocks.

Equations

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

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_blockSum {τ : 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)) : (blockSum W).matrix = Matrix.blockDiagonal' fun (p : π) => (W p).matrix

@[simp]

theorem Complexity.ExactFourier.Packing.Word.calls_blockSum {τ : 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)) : (blockSum W).calls = (List.map (fun (p : π) => (W p).calls) Finset.univ.toList).flatten

theorem Complexity.ExactFourier.Packing.Word.count_blockSum {τ : 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)] [DecidableEq τ] (W : (p : π) → Word D A (β p)) (t : τ) : (blockSum W).count t = ∑ p : π, (W p).count t

theorem Complexity.ExactFourier.Packing.prod_filter_map {X : Type u_1} {M : Type u_2} [Monoid M] (L : List X) (p : X → Prop) [DecidablePred p] (f : X → M) (hf : ∀ x ∈ L, ¬p x → f x = 1) : (List.map f (List.filter (fun (b : X) => decide (p b)) L)).prod = (List.map f L).prod

Deleting only identity factors preserves a noncommutative product.

theorem Complexity.ExactFourier.Packing.ordered_padding {M : Type u_1} [Monoid M] {k T : ℕ} (time : Fin k → Fin T) (ht : StrictMono time) (f : Fin k → M) : (List.ofFn (Function.extend time f fun (x : Fin T) => 1)).prod = (List.ofFn f).prod

Physical slot padding retains every local program's exact multiplication order.