Exact Fourier circuits: sum framed #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/SumFramed.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.
@[reducible, inline]
Join two dependently indexed coordinate families over a sum of index types.
Equations
- Complexity.ExactFourier.Packing.SumDomain β γ (Sum.inl p) = β p
- Complexity.ExactFourier.Packing.SumDomain β γ (Sum.inr r) = γ r
Instances For
@[instance_reducible]
instance
Complexity.ExactFourier.Packing.sumDomainDecidableEq
{π ρ : Type}
{β : π → Type}
{γ : ρ → Type}
[(p : π) → DecidableEq (β p)]
[(r : ρ) → DecidableEq (γ r)]
(v : π ⊕ ρ)
:
DecidableEq (SumDomain β γ v)
Equations
- One or more equations did not get rendered due to their size.
def
Complexity.ExactFourier.Packing.sumFramed
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{π ρ : Type}
{β : π → Type}
{γ : ρ → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
[(r : ρ) → Fintype (γ r)]
[(r : ρ) → DecidableEq (γ r)]
(W : (p : π) → FramedWord D (β p))
(V : (r : ρ) → FramedWord D (γ r))
(v : π ⊕ ρ)
:
FramedWord D (SumDomain β γ v)
Join two indexed families of framed words without changing their individual programs.
Equations
- Complexity.ExactFourier.Packing.sumFramed W V (Sum.inl p) = W p
- Complexity.ExactFourier.Packing.sumFramed W V (Sum.inr r) = V r
Instances For
def
Complexity.ExactFourier.Packing.sumTime
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{π ρ : Type}
{β : π → Type}
{γ : ρ → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
[(r : ρ) → Fintype (γ r)]
[(r : ρ) → DecidableEq (γ r)]
(W : (p : π) → FramedWord D (β p))
(V : (r : ρ) → FramedWord D (γ r))
{T : ℕ}
(timeW : (p : π) → Fin (W p).frames.length → Fin T)
(timeV : (r : ρ) → Fin (V r).frames.length → Fin T)
(v : π ⊕ ρ)
:
Join the schedules of two families of framed words.
Equations
- Complexity.ExactFourier.Packing.sumTime W V timeW timeV (Sum.inl p) = timeW p
- Complexity.ExactFourier.Packing.sumTime W V timeW timeV (Sum.inr r) = timeV r
Instances For
theorem
Complexity.ExactFourier.Packing.sumTime_strict
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{π ρ : Type}
{β : π → Type}
{γ : ρ → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
[(r : ρ) → Fintype (γ r)]
[(r : ρ) → DecidableEq (γ r)]
(W : (p : π) → FramedWord D (β p))
(V : (r : ρ) → FramedWord D (γ r))
{T : ℕ}
(timeW : (p : π) → Fin (W p).frames.length → Fin T)
(timeV : (r : ρ) → Fin (V r).frames.length → Fin T)
(hW : ∀ (p : π), StrictMono (timeW p))
(hV : ∀ (r : ρ), StrictMono (timeV r))
(v : π ⊕ ρ)
:
StrictMono (sumTime W V timeW timeV v)
theorem
Complexity.ExactFourier.Packing.sum_slot_card
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π ρ : Type}
[Fintype π]
[Fintype ρ]
{β : π → Type}
{γ : ρ → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
[(r : ρ) → Fintype (γ r)]
[(r : ρ) → DecidableEq (γ r)]
(W : (p : π) → FramedWord D (β p))
(V : (r : ρ) → FramedWord D (γ r))
{T : ℕ}
(timeW : (p : π) → Fin (W p).frames.length → Fin T)
(timeV : (r : ρ) → Fin (V r).frames.length → Fin T)
(s : Fin T)
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.matrix_sumFramed
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π ρ : Type}
[DecidableEq π]
[DecidableEq ρ]
{β : π → Type}
{γ : ρ → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
[(r : ρ) → Fintype (γ r)]
[(r : ρ) → DecidableEq (γ r)]
(W : (p : π) → FramedWord D (β p))
(V : (r : ρ) → FramedWord D (γ r))
:
(Matrix.reindex (Equiv.sumSigmaDistrib (SumDomain β γ)) (Equiv.sumSigmaDistrib (SumDomain β γ)))
(Matrix.blockDiagonal' fun (v : π ⊕ ρ) => (sumFramed W V v).matrix) = Matrix.fromBlocks (Matrix.blockDiagonal' fun (p : π) => (W p).matrix) 0 0
(Matrix.blockDiagonal' fun (r : ρ) => (V r).matrix)
def
Complexity.ExactFourier.Packing.emptyFramed
{τ : Type}
(D : τ → Type)
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
(α : Type)
[Fintype α]
[DecidableEq α]
:
FramedWord D α
The empty framed word, with identity as its final monomial factor.
Equations
Instances For
@[simp]
theorem
Complexity.ExactFourier.Packing.emptyFramed_matrix
{τ : Type}
(D : τ → Type)
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(α : Type)
[Fintype α]
[DecidableEq α]
:
def
Complexity.ExactFourier.Packing.emptyTime
{τ : Type}
(D : τ → Type)
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
(α : Type)
[Fintype α]
[DecidableEq α]
(T : ℕ)
:
Fin (emptyFramed D α).frames.length → Fin T
The unique schedule for a word with no frames.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.emptyTime_strict
{τ : Type}
(D : τ → Type)
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
(α : Type)
[Fintype α]
[DecidableEq α]
(T : ℕ)
:
StrictMono (emptyTime D α T)
@[simp]
theorem
Complexity.ExactFourier.Packing.empty_slot_card
{τ : Type}
[DecidableEq τ]
(D : τ → Type)
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
(α : Type)
[Fintype α]
[DecidableEq α]
(T : ℕ)
(s : Fin T)
(t : τ)
:
Fintype.card { _unused : Unit // (slotCall (framedSlot (emptyFramed D α) (emptyTime D α T) s)).kind = some t } = 0
theorem
Complexity.ExactFourier.Packing.list_count_get
{τ : Type}
[DecidableEq τ]
(L : List τ)
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.list_card_get
{τ : Type}
[DecidableEq τ]
(L : List τ)
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.list_count_map_get
{α τ : Type}
[DecidableEq τ]
(L : List α)
(f : α → τ)
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.slot_card_sum
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
{T : ℕ}
(time : (p : π) → Fin (W p).frames.length → Fin T)
(ht : ∀ (p : π), Function.Injective (time p))
(s : Fin T)
(t : τ)
:
theorem
Complexity.ExactFourier.Packing.slot_card_total
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
{T : ℕ}
(time : (p : π) → Fin (W p).frames.length → Fin T)
(ht : ∀ (p : π), Function.Injective (time p))
(t : τ)
:
∑ s : Fin T, Fintype.card { p : π // (slotCall (framedSlot (W p) (time p) s)).kind = some t } = ∑ p : π, List.count t (W p).types
theorem
Complexity.ExactFourier.Packing.complete_and_pack
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{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)]
{ν : Type}
[Fintype ν]
[DecidableEq ν]
(k : τ → ℕ)
(W : (p : π) → FramedWord D (β p))
(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 : (p : π) → Fin (W p).frames.length → Fin T)
(htime : ∀ (p : π), StrictMono (time p))
(hload : ∀ (s : Fin T) (t : τ), Fintype.card { p : π // (slotCall (framedSlot (W p) (time p) s)).kind = some t } ≤ k t)
(d : τ → ℕ)
(hkd : ∀ (t : τ), k t < d t)
(hdef : ∀ (t : τ), k t * T - ∑ p : π, List.count t (W p).types = d t * (dummy t).frames.length)
(R : ℕ)
(hR : ∑ t : τ, d t * Fintype.card (D t) ≤ R)
(hw : Fintype.card (ActiveSpace D k ⊕ ν) ≤ Fintype.card ((p : π) × β p) + R)
:
∃ (V :
Word (fun (x : Unit) => ActiveSpace D k ⊕ ν) (fun (x : Unit) => inventoryWithIdentity k) ((p : π) × β p ⊕ Fin R)),
V.matrix = Matrix.fromBlocks (Matrix.blockDiagonal' fun (p : π) => (W p).matrix) 0 0 1 ∧ V.calls.length = T
def
Complexity.ExactFourier.Packing.cyclicTime
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{π : Type}
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
(m : π → ℕ)
(F L : ℕ)
(hF : 0 < F)
(hL : ∀ (p : π), (W p).frames.length ≤ L)
(v : (p : π) × Fin (m p))
:
Schedule each program copy at its cyclic start followed by consecutive frame times.
Equations
- Complexity.ExactFourier.Packing.cyclicTime W m F L hF hL v o = ⟨Complexity.ExactFourier.Packing.cyclicStart F v.snd + ↑o, ⋯⟩
Instances For
theorem
Complexity.ExactFourier.Packing.cyclicTime_strict
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{π : Type}
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
(m : π → ℕ)
(F L : ℕ)
(hF : 0 < F)
(hL : ∀ (p : π), (W p).frames.length ≤ L)
(v : (p : π) × Fin (m p))
:
StrictMono (cyclicTime W m F L hF hL v)
theorem
Complexity.ExactFourier.Packing.cyclic_slot_card
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
(m : π → ℕ)
(F L : ℕ)
(hF : 0 < F)
(hL : ∀ (p : π), (W p).frames.length ≤ L)
(s : Fin (F + L - 1))
(t : τ)
:
Fintype.card
{ v : (p : π) × Fin (m p) // (slotCall (framedSlot (W v.fst) (cyclicTime W m F L hF hL v) s)).kind = some t } = scheduledLoad (fun (p : π) => (W p).types) m F t ↑s
theorem
Complexity.ExactFourier.Packing.cyclic_slot_bound
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[Fintype π]
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
(m : π → ℕ)
(F L : ℕ)
(hF : 0 < F)
(hL : ∀ (p : π), (W p).frames.length ≤ L)
(s : Fin (F + L - 1))
(t : τ)
: