Exact Fourier circuits: finite separation

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/FiniteSeparation.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.finite_separator {ρ τ : Type} [Fintype ρ] [Fintype τ] (Δ : ρ → τ → ℝ) (hn : ¬∃ (lam : ρ → ℝ), (∀ (r : ρ), 0 ≤ lam r) ∧ ∀ (t : τ), 0 < ∑ r : ρ, lam r * Δ r t) : ∃ (v : τ → ℝ), (∀ (t : τ), 0 ≤ v t) ∧ (∃ (t : τ), 0 < v t) ∧ ∀ (r : ρ), ∑ t : τ, v t * Δ r t ≤ 0

Finite comparison alternative, exactly the separator needed for no-win prices.

theorem Complexity.ExactFourier.Packing.no_win_separator {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ρ : Type} [Fintype ρ] [DecidableEq ρ] (hno : ¬FiniteWinStatement) (hA : ∀ (t : τ), IsUnit (A t)) (u : τ) (hn : ¬MonomialMatrix (A u)) (c : ρ → PairComparison) : ∃ (v : τ → ℝ), (∀ (t : τ), 0 ≤ v t) ∧ (∃ (t : τ), 0 < v t) ∧ ∀ (r : ρ), pairPrice v (c r).pair ≤ Word.weight v (c r).word

theorem Complexity.ExactFourier.Packing.finite_prices {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ρ : Type} [Fintype ρ] [DecidableEq ρ] (hno : ¬FiniteWinStatement) (hA : ∀ (t : τ), IsUnit (A t)) (u : τ) (hn : ¬MonomialMatrix (A u)) (c : ρ → PairComparison) (C : τ → ℕ) (upper : (t : τ) → Word D A (D t)) (hu : ∀ (t : τ), (upper t).matrix = A t) (hcost : ∀ (t : τ) (p : τ → ℝ), Word.weight p (upper t) = ↑(C t) * p u) : ∃ (p : τ → ℝ), (∀ (t : τ), 0 ≤ p t ∧ p t ≤ ↑(C t)) ∧ p u = 1 ∧ ∀ (r : ρ), pairPrice p (c r).pair ≤ Word.weight p (c r).word

theorem Complexity.ExactFourier.Packing.finite_global_prices (hno : ¬FiniteWinStatement) (Q : Finset GlobalComparison) : ∃ (p : GMatrix → ℝ), (∀ (g : GMatrix), 0 ≤ p g ∧ p g ≤ ↑g.upperCost) ∧ p shearG = 1 ∧ ∀ c ∈ Q, c.holds p

theorem Complexity.ExactFourier.Packing.global_prices_exist (hno : ¬FiniteWinStatement) : ∃ (p : GMatrix → ℝ), (∀ (g : GMatrix), 0 ≤ p g ∧ p g ≤ ↑g.upperCost) ∧ p shearG = 1 ∧ GlobalConstraints p

theorem Complexity.ExactFourier.Packing.GlobalConstraints.reindex_le {p : GMatrix → ℝ} (hp : GlobalConstraints p) (a b : GMatrix) (e : a.domain ≃ b.domain) (he : (Matrix.reindex e e) a.mat = b.mat) : p b ≤ p a

theorem Complexity.ExactFourier.Packing.GlobalConstraints.reindex {p : GMatrix → ℝ} (hp : GlobalConstraints p) (a b : GMatrix) (e : a.domain ≃ b.domain) (he : (Matrix.reindex e e) a.mat = b.mat) : p b = p a

noncomputable def Complexity.ExactFourier.Packing.GMatrix.of {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : GMatrix

Enumerate an invertible matrix's finite coordinates to bundle its width and entries.

Equations

• Complexity.ExactFourier.Packing.GMatrix.of M hM = { width := Fintype.card α, mat := (Matrix.reindex (Fintype.equivFin α) (Fintype.equivFin α)) M, unit := ⋯ }

noncomputable def Complexity.ExactFourier.Packing.rawValue (p : GMatrix → ℝ) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) : ℝ

Evaluate a bundled price on an invertible matrix, assigning zero to singular matrices.

Equations

• Complexity.ExactFourier.Packing.rawValue p M = if h : IsUnit M then p (Complexity.ExactFourier.Packing.GMatrix.of M h) else 0

theorem Complexity.ExactFourier.Packing.rawValue_unit (p : GMatrix → ℝ) {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) (hM : IsUnit M) : rawValue p M = p (GMatrix.of M hM)

structure Complexity.ExactFourier.Packing.RawPrice : Type 1

Nonnegative matrix prices satisfying the pair-comparison inequalities.

• value {α : Type} [Fintype α] [DecidableEq α] : Matrix α α ℂ → ℝ

  The price assigned to each finite square complex matrix.

• nonneg {α : Type} [Fintype α] [DecidableEq α] (M : Matrix α α ℂ) : IsUnit M → 0 ≤ self.value M
• comparison {τ : Type} [Fintype τ] [DecidableEq τ] {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} : (∀ (t : τ), IsUnit (A t)) → ∀ (c : PairComparison), pairPrice (fun (t : τ) => self.value (A t)) c.pair ≤ Word.weight (fun (t : τ) => self.value (A t)) c.word
• normalized : self.value shearU = 1

theorem Complexity.ExactFourier.Packing.rawPrice_exists (hno : ¬FiniteWinStatement) : Nonempty RawPrice

theorem Complexity.ExactFourier.Embedded.matrix_inl {α β : Type} [DecidableEq α] [DecidableEq β] (M : Matrix α α ℂ) : matrix Function.Embedding.inl M = Matrix.fromBlocks M 0 0 1

theorem Complexity.ExactFourier.Embedded.matrix_inr {α β : Type} [DecidableEq α] [DecidableEq β] (M : Matrix β β ℂ) : matrix Function.Embedding.inr M = Matrix.fromBlocks 1 0 0 M

@[simp]

theorem Complexity.ExactFourier.Embedded.matrix_refl {α : Type} (M : Matrix α α ℂ) : matrix (Function.Embedding.refl α) M = M

noncomputable def Complexity.ExactFourier.Packing.Word.sum {τ : 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 β) : Word D A (α ⊕ β)

Run two words on disjoint coordinate blocks by embedding and concatenating them.

Equations

• W.sum V = Complexity.ExactFourier.Packing.Word.embed Function.Embedding.inl W ++ Complexity.ExactFourier.Packing.Word.embed Function.Embedding.inr V

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_sum {τ : 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 β) : (W.sum V).matrix = Matrix.fromBlocks W.matrix 0 0 V.matrix

@[simp]

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

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