Exact Fourier circuits: live sectors #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/LiveSectors.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.
def
Complexity.ExactFourier.Packing.liveMatrix
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(k : τ → ℕ)
(I : ℕ)
:
The direct sum of all live pair matrices, repeated with their allocated multiplicities.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.live_matrix_on
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(k : τ → ℕ)
(I : ℕ)
(x y : LiveSpace D k I ⊕ Fin I × Fin I)
:
(speciesInventory (speciesCopies k I) speciesMatrix).kronecker (speciesInventory (speciesCopies k I) speciesMatrix)
((liveCoordinates k I) x) ((liveCoordinates k I) y) = Matrix.fromBlocks (liveMatrix k I) 0 0 1 x y
theorem
Complexity.ExactFourier.Packing.live_matrix_reindex
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(k : τ → ℕ)
(I : ℕ)
:
(Matrix.reindex (liveCoordinates k I) (liveCoordinates k I)) (Matrix.fromBlocks (liveMatrix k I) 0 0 1) = (speciesInventory (speciesCopies k I) speciesMatrix).kronecker (speciesInventory (speciesCopies k I) speciesMatrix)
theorem
Complexity.ExactFourier.Packing.copies_equiv
{σ π : Type}
[Fintype σ]
[DecidableEq σ]
[Fintype π]
[DecidableEq π]
{E : σ → Type}
{B : (s : σ) → Matrix (E s) (E s) ℂ}
{κ : σ → Type}
[(s : σ) → Fintype (κ s)]
[(s : σ) → DecidableEq (κ s)]
(key : π → σ)
(m : π → ℕ)
(h : ∀ (s : σ), (∑ p : π, if key p = s then m p else 0) = Fintype.card (κ s))
:
∃ (e : (v : (p : π) × Fin (m p)) × E (key v.fst) ≃ (v : (s : σ) × κ s) × E v.fst),
(Matrix.reindex e e) (Matrix.blockDiagonal' fun (v : (p : π) × Fin (m p)) => B (key v.fst)) = Matrix.blockDiagonal' fun (v : (s : σ) × κ s) => B v.fst
theorem
Complexity.ExactFourier.Packing.copyCoordinates_matrix
{σ : Type}
[DecidableEq σ]
{E : σ → Type}
{B : (s : σ) → Matrix (E s) (E s) ℂ}
(κ : σ → Type)
[(s : σ) → DecidableEq (κ s)]
:
(Matrix.reindex (copyCoordinates κ) (copyCoordinates κ)) (Matrix.blockDiagonal' fun (v : (s : σ) × κ s) => B v.fst) = Matrix.blockDiagonal' fun (s : σ) => Matrix.kronecker 1 (B s)
def
Complexity.ExactFourier.Packing.singleStepFin
{α : Type}
[Fintype α]
[DecidableEq α]
(e : α ≃ Fin (Fintype.card α))
(f : α × α ≃ Fin (Fintype.card α ^ 2))
(A : Matrix α α ℂ)
:
Step (fun (x : Unit) => α) (fun (x : Unit) => A) (α × α) → WordStep ((Matrix.reindex e e) A) (Fintype.card α ^ 2)
Convert a single-species packing step into the numbered finite-win word model.
Equations
- Complexity.ExactFourier.Packing.singleStepFin e f A (Complexity.ExactFourier.Packing.Step.mono M hM) = Complexity.ExactFourier.WordStep.monomial ((Matrix.reindex f f) M) ⋯
- Complexity.ExactFourier.Packing.singleStepFin e f A (Complexity.ExactFourier.Packing.Step.call t g) = Complexity.ExactFourier.WordStep.call (e.symm.toEmbedding.trans (g.trans f.toEmbedding))
Instances For
theorem
Complexity.ExactFourier.Packing.singleStepFin_matrix
{α : Type}
[Fintype α]
[DecidableEq α]
(e : α ≃ Fin (Fintype.card α))
(f : α × α ≃ Fin (Fintype.card α ^ 2))
(A : Matrix α α ℂ)
(s : Step (fun (x : Unit) => α) (fun (x : Unit) => A) (α × α))
:
noncomputable def
Complexity.ExactFourier.Packing.squareFinEquiv
{α : Type}
[Fintype α]
(e : α ≃ Fin (Fintype.card α))
:
Number pairs of coordinates using the tensor-square coordinate convention.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.ExactFourier.Packing.squareFinEquiv_tensor
{α : Type}
[Fintype α]
(e : α ≃ Fin (Fintype.card α))
(A : Matrix α α ℂ)
:
(Matrix.reindex (squareFinEquiv e) (squareFinEquiv e)) (A.kronecker A) = tensorPower ((Matrix.reindex e e) A) 2
theorem
Complexity.ExactFourier.Packing.square_win_implies_finite_win
{α : Type}
[Fintype α]
[DecidableEq α]
(A : Matrix α α ℂ)
(hA : IsUnit A)
(hna : ¬MonomialMatrix A)
(W : Word (fun (x : Unit) => α) (fun (x : Unit) => A) (α × α))
(hW : W.matrix = A.kronecker A)
(hc : W.calls.length < 2 * Fintype.card α)
:
theorem
Complexity.ExactFourier.Packing.family_square_win
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
[DecidableEq π]
(k : τ → ℕ)
(I : ℕ)
(key : π → LivePair τ)
(W : (p : π) → FramedWord D (PairDomain D (key p)))
(m : π → ℕ)
(hW : ∀ (p : π), (W p).matrix = pairMatrix (key p))
(hnum :
∀ (s : LivePair τ), (∑ p : π, if key p = s then m p else 0) = speciesCopies k I (↑s).1 * speciesCopies k I (↑s).2)
(dummy : (t : τ) → FramedWord D (D t))
(hdummy : ∀ (t : τ), (dummy t).matrix = 1)
(hdtype : ∀ (t : τ) (o : Fin (dummy t).frames.length), ((dummy t).frames.get o).type = t)
{T : ℕ}
(time : (v : (p : π) × Fin (m p)) → Fin (W v.fst).frames.length → Fin T)
(htime : ∀ (v : (p : π) × Fin (m p)), StrictMono (time v))
(hload :
∀ (s : Fin T) (t : τ),
Fintype.card { v : (p : π) × Fin (m p) // (slotCall (framedSlot (W v.fst) (time v) s)).kind = some t } ≤ k t)
(d : τ → ℕ)
(hkd : ∀ (t : τ), k t < d t)
(hdef : ∀ (t : τ), k t * T - ∑ p : π, m p * List.count t (W p).types = d t * (dummy t).frames.length)
(hR : ∑ t : τ, d t * Fintype.card (D t) ≤ I ^ 2)
(hJ : IsUnit (inventoryWithIdentity k))
(hnJ : ¬MonomialMatrix (inventoryWithIdentity k))
(hT : T < 2 * Fintype.card (ActiveSpace D k ⊕ Fin I))
:
theorem
Complexity.ExactFourier.Packing.square_schedule_margin
{K W G S u F L C : ℝ}
(hK : 1 ≤ K)
(hS : 2 * K ≤ S)
(hu : L + 2 * C * W ≤ u)
(hu0 : 0 ≤ u)
(hC : 0 ≤ C)
(hW : 0 ≤ W)
(hGF : G + S = 2 * K * W)
(hF : F = (2 * W - 1) * u + 1 - L)
(hFu : F ≤ 2 * W * u)
:
Quantitative slack for the deterministic cyclic schedule, using square sectors.