Exact Fourier circuits: raw word bound

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

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

theorem Complexity.ExactFourier.Packing.RawPrice.word_le (p : RawPrice) {τ : Type} [Fintype τ] [DecidableEq τ] {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 α) : p.value W.matrix ≤ Word.weight (fun (t : τ) => p.value (A t)) W

theorem Complexity.ExactFourier.Packing.RawPrice.word_bound (p : RawPrice) {τ : Type} [Fintype τ] [DecidableEq τ] {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 α) (H : Matrix α α ℂ) (hW : W.matrix = H) : p.value H ≤ Word.weight (fun (t : τ) => p.value (A t)) W

theorem Complexity.ExactFourier.Packing.RawPrice.monomial_zero (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : MonomialMatrix M) : p.value M = 0

@[simp]

theorem Complexity.ExactFourier.Packing.RawPrice.one (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] : p.value 1 = 0

theorem Complexity.ExactFourier.Packing.RawPrice.reindex_le (p : RawPrice) {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (M : Matrix α α ℂ) (hM : IsUnit M) : p.value ((Matrix.reindex e e) M) ≤ p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.reindex (p : RawPrice) {α β : Type} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (e : α ≃ β) (M : Matrix α α ℂ) (hM : IsUnit M) : p.value ((Matrix.reindex e e) M) = p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.mul_le (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M N : Matrix α α ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (M * N) ≤ p.value M + p.value N

theorem Complexity.ExactFourier.Packing.RawPrice.monomial (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M L R : Matrix α α ℂ) (hM : IsUnit M) (hL : MonomialMatrix L) (hR : MonomialMatrix R) : p.value (L * M * R) = p.value M

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.BiDomain (α β : Type) : Bool → Type

The coordinate types of two matrix species indexed by Bool.

Equations

• Complexity.ExactFourier.Packing.BiDomain α β false = α
• Complexity.ExactFourier.Packing.BiDomain α β true = β

@[instance_reducible]

instance Complexity.ExactFourier.Packing.instFintypeBiDomain {α β : Type} [Fintype α] [Fintype β] (b : Bool) : Fintype (BiDomain α β b)

Equations

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

@[instance_reducible]

instance Complexity.ExactFourier.Packing.instDecidableEqBiDomain {α β : Type} [DecidableEq α] [DecidableEq β] (b : Bool) : DecidableEq (BiDomain α β b)

Equations

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

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.biMatrix {α β : Type} (M : Matrix α α ℂ) (N : Matrix β β ℂ) (b : Bool) : Matrix (BiDomain α β b) (BiDomain α β b) ℂ

The two matrices viewed as a Boolean-indexed species family.

Equations

• Complexity.ExactFourier.Packing.biMatrix M N false = M
• Complexity.ExactFourier.Packing.biMatrix M N true = N

theorem Complexity.ExactFourier.Packing.RawPrice.tensor_le (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) ≤ ↑(Fintype.card β) * p.value M + ↑(Fintype.card α) * p.value N

theorem Complexity.ExactFourier.Packing.RawPrice.tensor_ge (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : ↑(Fintype.card β) * p.value M + ↑(Fintype.card α) * p.value N ≤ p.value (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N)

theorem Complexity.ExactFourier.Packing.RawPrice.tensor (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N) = ↑(Fintype.card β) * p.value M + ↑(Fintype.card α) * p.value N

theorem Complexity.ExactFourier.Packing.RawPrice.directSum_le (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (Matrix.fromBlocks M 0 0 N) ≤ p.value M + p.value N

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

Every step is a species call, with no monomial steps.

Equations

• W.Pure = ∀ s ∈ W, s.kind ≠ none

@[simp]

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

@[simp]

theorem Complexity.ExactFourier.Packing.Word.pure_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 α) : Pure (s :: W) ↔ s.kind ≠ none ∧ W.Pure

@[simp]

theorem Complexity.ExactFourier.Packing.Word.pure_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).Pure ↔ W.Pure ∧ V.Pure

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

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

theorem Complexity.ExactFourier.Packing.Word.pure_blockSum {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [Fintype π] [DecidableEq π] {E : π → Type} [(t : π) → Fintype (E t)] [(t : π) → DecidableEq (E t)] (W : (t : π) → Word D A (E t)) (h : ∀ (t : π), (W t).Pure) : (blockSum W).Pure

theorem Complexity.ExactFourier.Packing.Word.Pure.leftTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {W : Word D A α} (h : W.Pure) : W.leftTensor.Pure

theorem Complexity.ExactFourier.Packing.Word.Pure.rightTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {W : Word D A β} (h : W.Pure) : W.rightTensor.Pure

theorem Complexity.ExactFourier.Packing.Word.Pure.kronecker {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {W : Word D A α} {V : Word D A β} (hW : W.Pure) (hV : V.Pure) : (W.kronecker V).Pure

@[simp]

theorem Complexity.ExactFourier.Packing.pure_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).Pure

theorem Complexity.ExactFourier.Packing.Word.Pure.length_eq_count {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {M : Matrix α α ℂ} {W : Word (fun (x : Unit) => α) (fun (x : Unit) => M) β} (hW : W.Pure) : List.length W = W.count ()

def Complexity.ExactFourier.Packing.purePower {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (k : ℕ) : Word (fun (x : Unit) => α) (fun (x : Unit) => M) (TensorAxis.Space α k)

A word using only calls to M that realizes its tensor power.

Equations

• Complexity.ExactFourier.Packing.purePower M 0 = []
• Complexity.ExactFourier.Packing.purePower M k.succ = (Complexity.ExactFourier.Packing.purePower M k).kronecker (Complexity.ExactFourier.Packing.callWord () (Function.Embedding.refl α))

@[simp]

theorem Complexity.ExactFourier.Packing.purePower_matrix {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (k : ℕ) : (purePower M k).matrix = TensorAxis.power M k

@[simp]

theorem Complexity.ExactFourier.Packing.purePower_pure {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (k : ℕ) : (purePower M k).Pure

theorem Complexity.ExactFourier.Packing.purePower_count {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (k : ℕ) : (purePower M k).count () = Fintype.card (TensorAxis.Fibers α k)

theorem Complexity.ExactFourier.Embedded.matrix_sumMap {α β γ δ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq δ] (e : α ↪ γ) (f : β ↪ δ) (M : Matrix α α ℂ) (N : Matrix β β ℂ) : matrix (e.sumMap f) (Matrix.fromBlocks M 0 0 N) = Matrix.fromBlocks (matrix e M) 0 0 (matrix f N)

theorem Complexity.ExactFourier.Packing.RawPrice.embedded_le (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ↪ β) (M : Matrix α α ℂ) (hM : IsUnit M) : p.value (Embedded.matrix e M) ≤ p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.paired_le (p : RawPrice) {α β γ δ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] [DecidableEq δ] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) (W : Word (fun (x : Unit) => α) (fun (x : Unit) => M) γ) (V : Word (fun (x : Unit) => β) (fun (x : Unit) => N) δ) (hW : W.Pure) (hV : V.Pure) (hlen : List.length W = List.length V) : p.value (Matrix.fromBlocks W.matrix 0 0 V.matrix) ≤ ↑(List.length W) * p.value (Matrix.fromBlocks M 0 0 N)

theorem Complexity.ExactFourier.Packing.RawPrice.sum_swap (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (Matrix.fromBlocks N 0 0 M) = p.value (Matrix.fromBlocks M 0 0 N)

theorem Complexity.ExactFourier.Packing.RawPrice.duplicate (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : p.value (Matrix.fromBlocks M 0 0 M) = 2 * p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.power (p : RawPrice) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) (k : ℕ) : p.value (TensorAxis.power M k) = ↑(Fintype.card (TensorAxis.Fibers α k)) * p.value M

theorem Complexity.ExactFourier.Packing.RawPrice.balanced_calls {α : Type} [Fintype α] (hα : 0 < Fintype.card α) : Fintype.card (TensorAxis.Fibers α (Fintype.card α)) = Fintype.card (TensorAxis.Space α (Fintype.card α))

theorem Complexity.ExactFourier.Packing.RawPrice.directSum_ge_nonempty (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) (hα : 0 < Fintype.card α) (hβ : 0 < Fintype.card β) : p.value M + p.value N ≤ p.value (Matrix.fromBlocks M 0 0 N)

theorem Complexity.ExactFourier.Packing.RawPrice.directSum (p : RawPrice) {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) (N : Matrix β β ℂ) (hM : IsUnit M) (hN : IsUnit N) : p.value (Matrix.fromBlocks M 0 0 N) = p.value M + p.value N