Exact Fourier circuits: comparison rename #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/FourierCircuit/ComparisonRename.lean
Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.
@[reducible, inline]
abbrev
Complexity.ExactFourier.Packing.mapPair
{τ σ : Type}
(f : τ → σ)
(p : LivePair τ)
:
LivePair σ
Rename both species of a live pair while preserving its nonempty condition.
Equations
- Complexity.ExactFourier.Packing.mapPair f p = ⟨(Option.map f (↑p).1, Option.map f (↑p).2), ⋯⟩
Instances For
@[reducible, inline]
abbrev
Complexity.ExactFourier.Packing.pairEquiv
{τ σ : Type}
{D : τ → Type}
{E : σ → Type}
(f : τ → σ)
(e : (t : τ) → D t ≃ E (f t))
(p : LivePair τ)
:
Transport both coordinate factors of a renamed live pair.
Equations
- Complexity.ExactFourier.Packing.pairEquiv f e p = (Complexity.ExactFourier.Packing.speciesEquiv f e (↑p).1).prodCongr (Complexity.ExactFourier.Packing.speciesEquiv f e (↑p).2)
Instances For
theorem
Complexity.ExactFourier.Packing.speciesEquiv_matrix
{τ σ : Type}
{D : τ → Type}
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{E : σ → Type}
{B : (t : σ) → Matrix (E t) (E t) ℂ}
(f : τ → σ)
(e : (t : τ) → D t ≃ E (f t))
(he : ∀ (t : τ), (Matrix.reindex (e t) (e t)) (A t) = B (f t))
(s : Option τ)
:
(Matrix.reindex (speciesEquiv f e s) (speciesEquiv f e s)) (speciesMatrix s) = speciesMatrix (Option.map f s)
@[reducible, inline]
noncomputable abbrev
Complexity.ExactFourier.Packing.PairComparison.rename
{τ σ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{E : σ → Type}
[(t : σ) → Fintype (E t)]
[(t : σ) → DecidableEq (E t)]
{B : (t : σ) → Matrix (E t) (E t) ℂ}
(f : τ → σ)
(e : (t : τ) → D t ≃ E (f t))
(he : ∀ (t : τ), (Matrix.reindex (e t) (e t)) (A t) = B (f t))
(c : PairComparison)
:
Transport a pair comparison through compatible species and matrix renamings.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.ExactFourier.Packing.PairComparison.rename_ineq
{τ σ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{E : σ → Type}
[(t : σ) → Fintype (E t)]
[(t : σ) → DecidableEq (E t)]
{B : (t : σ) → Matrix (E t) (E t) ℂ}
(f : τ → σ)
(e : (t : τ) → D t ≃ E (f t))
(he : ∀ (t : τ), (Matrix.reindex (e t) (e t)) (A t) = B (f t))
(c : PairComparison)
(v : σ → ℝ)
:
An invertible complex matrix bundled with its finite width.
- width : ℕ
The number of rows and columns of the bundled matrix.
The invertible square matrix on the specified finite coordinate set.
Instances For
The elementary two-coordinate shear as a bundled invertible matrix.
Equations
- Complexity.ExactFourier.Packing.shearG = { width := 2, mat := Complexity.ExactFourier.Packing.shearU, unit := Complexity.ExactFourier.Packing.shearU_unit }
Instances For
@[reducible, inline]
The two-coordinate domain of the single shear species.
Equations
Instances For
@[reducible, inline]
The matrix assigned to the single shear species.
Instances For
A pair comparison bundled with a finite family of invertible matrices.
- num : ℕ
The number of species in the bundled comparison.
The invertible matrix assigned to each species.
- comparison : PairComparison
The word witnessing the comparison within the bundled family.
Instances For
def
Complexity.ExactFourier.Packing.GlobalComparison.holds
(c : GlobalComparison)
(p : GMatrix → ℝ)
:
The candidate prices satisfy this comparison's pair-versus-word inequality.
Equations
- c.holds p = (Complexity.ExactFourier.Packing.pairPrice (p ∘ c.family) c.comparison.pair ≤ Complexity.ExactFourier.Packing.Word.weight (p ∘ c.family) c.comparison.word)
Instances For
The candidate matrix prices satisfy every bundled pair comparison.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.Word.continuous_weight
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{α : Type}
[Fintype α]
[DecidableEq α]
(f : τ → GMatrix)
(W : Word D A α)
:
Continuous fun (p : GMatrix → ℝ) => weight (p ∘ f) W
theorem
Complexity.ExactFourier.Packing.family_cast_matrix
{τ : Type}
(f : τ → GMatrix)
{t u : τ}
(h : t = u)
:
@[reducible, inline]
noncomputable abbrev
Complexity.ExactFourier.Packing.toGlobalComparison
{τ : Type}
[Fintype τ]
(f : τ → GMatrix)
(c : PairComparison)
:
Enumerate a finite species family to obtain a bundled global comparison.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.ExactFourier.Packing.GlobalConstraints.apply
{τ : Type}
[Fintype τ]
(f : τ → GMatrix)
{p : GMatrix → ℝ}
(hp : GlobalConstraints p)
(c : PairComparison)
:
theorem
Complexity.ExactFourier.Packing.pair_baseline_sum
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
(k : τ → ℕ)
(I : ℕ)
(t : τ)
:
∑ p : LivePair τ, speciesCopies k I (↑p).1 * speciesCopies k I (↑p).2 * pairBaseline p t = 2 * k t * (∑ i : τ, k i * Fintype.card (D i) + I)
@[reducible, inline]
abbrev
Complexity.ExactFourier.Packing.familyKey
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
(c : ρ → PairComparison)
:
Associate each standard or replacement program with its target live pair.
Equations
Instances For
noncomputable def
Complexity.ExactFourier.Packing.familyProgram
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
(c : ρ → PairComparison)
(p : LivePair τ ⊕ ρ)
:
FramedWord D (PairDomain D (familyKey c p))
Choose the standard pair program or the supplied replacement comparison word.
Equations
Instances For
def
Complexity.ExactFourier.Packing.familyMultiplicity
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
(c : ρ → PairComparison)
(n : LivePair τ → ℕ)
(a : ρ → ℕ)
:
Allocate copies between standard pair programs and their replacements.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.familyProgram_matrix
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
(c : ρ → PairComparison)
(p : LivePair τ ⊕ ρ)
:
theorem
Complexity.ExactFourier.Packing.familyMultiplicity_key
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
(c : ρ → PairComparison)
(n : LivePair τ → ℕ)
(a : ρ → ℕ)
(h : ∀ (p : LivePair τ), (∑ r : ρ, if (c r).pair = p then a r else 0) ≤ n p)
(s : LivePair τ)
:
theorem
Complexity.ExactFourier.Packing.familyMultiplicity_scale
{τ : Type}
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
(c : ρ → PairComparison)
(n : LivePair τ → ℕ)
(a : ρ → ℕ)
(u : ℕ)
(p : LivePair τ ⊕ ρ)
:
familyMultiplicity c (fun (p : LivePair τ) => n p * u) (fun (r : ρ) => a r * u) p = familyMultiplicity c n a p * u
theorem
Complexity.ExactFourier.Packing.family_saving
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
(c : ρ → PairComparison)
(n : LivePair τ → ℕ)
(a : ρ → ℕ)
(h : ∀ (p : LivePair τ), (∑ r : ρ, if (c r).pair = p then a r else 0) ≤ n p)
(t : τ)
:
∑ p : LivePair τ, ↑(n p) * ↑(pairBaseline p t) - ∑ p : LivePair τ ⊕ ρ, ↑(familyMultiplicity c n a p) * ↑(List.count t (familyProgram c p).types) = ∑ r : ρ, ↑(a r) * (c r).delta t
theorem
Complexity.ExactFourier.Packing.family_total_scale
{τ : Type}
[Fintype τ]
[DecidableEq τ]
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{ρ : Type}
[Fintype ρ]
(c : ρ → PairComparison)
(n : LivePair τ → ℕ)
(a : ρ → ℕ)
(u : ℕ)
(t : τ)
:
∑ p : LivePair τ ⊕ ρ,
familyMultiplicity c (fun (p : LivePair τ) => n p * u) (fun (r : ρ) => a r * u) p * List.count t (familyProgram c p).types = (∑ p : LivePair τ ⊕ ρ, familyMultiplicity c n a p * List.count t (familyProgram c p).types) * u
noncomputable def
Complexity.ExactFourier.Packing.framedSlot
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{α : Type}
[Fintype α]
[DecidableEq α]
(W : FramedWord D α)
{T : ℕ}
(time : Fin W.frames.length → Fin T)
(t : Fin T)
:
The frame scheduled at a given time, or no frame at a vacant slot.
Equations
Instances For
def
Complexity.ExactFourier.Packing.slotCall
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{α : Type}
[Fintype α]
[DecidableEq α]
:
The call in an occupied slot, using an identity step for a vacant slot.
Equations
Instances For
def
Complexity.ExactFourier.Packing.slotMono
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{α : Type}
[Fintype α]
[DecidableEq α]
:
The monomial factor in a slot, or the identity when the slot is vacant.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.slotMono_monomial
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{α : Type}
[Fintype α]
[DecidableEq α]
(f : Option (Frame D α))
:
noncomputable def
Complexity.ExactFourier.Packing.slotMatrix
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{α : Type}
[Fintype α]
[DecidableEq α]
(f : Option (Frame D α))
:
The full matrix of a scheduled slot, including its monomial factor.
Equations
Instances For
theorem
Complexity.ExactFourier.Packing.slotMatrix_extend
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{α : Type}
[Fintype α]
[DecidableEq α]
(W : FramedWord D α)
{T : ℕ}
(time : Fin W.frames.length → Fin T)
(ht : Function.Injective time)
(t : Fin T)
:
slotMatrix (framedSlot W time t) = Function.extend time (fun (i : Fin W.frames.length) => (W.frames.get i).matrix) (fun (x : Fin T) => 1) t
theorem
Complexity.ExactFourier.Packing.slotMatrix_product
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{α : Type}
[Fintype α]
[DecidableEq α]
(W : FramedWord D α)
{T : ℕ}
(time : Fin W.frames.length → Fin T)
(ht : StrictMono time)
:
noncomputable def
Complexity.ExactFourier.Packing.framedLayer
{τ : Type}
{D : τ → Type}
[(t : τ) → Fintype (D t)]
[(t : τ) → DecidableEq (D t)]
{A : (t : τ) → Matrix (D t) (D t) ℂ}
{π : Type}
[DecidableEq π]
{β : π → Type}
[(p : π) → Fintype (β p)]
[(p : π) → DecidableEq (β p)]
(W : (p : π) → FramedWord D (β p))
{T : ℕ}
(time : (p : π) → Fin (W p).frames.length → Fin T)
(t : Fin T)
:
The block diagonal matrix of all programs' slots at one scheduled time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Complexity.ExactFourier.Packing.framedLayer_product
{τ : 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 : π) → FramedWord D (β p))
{T : ℕ}
(time : (p : π) → Fin (W p).frames.length → Fin T)
(ht : ∀ (p : π), StrictMono (time p))
:
((List.ofFn (framedLayer W time)).prod * Matrix.blockDiagonal' fun (p : π) => (W p).tail) = Matrix.blockDiagonal' fun (p : π) => (W p).matrix
theorem
Complexity.ExactFourier.Packing.gather_framed_slot
{τ : 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 : τ → ℕ)
(S : (p : π) → Option (Frame D (β p)))
(hc : ∀ (t : τ), Fintype.card { p : π // (slotCall (S p)).kind = some t } = k t)
(hw : Fintype.card (ActiveSpace D k ⊕ ν) ≤ Fintype.card ((p : π) × β p))
:
∃ (M : Matrix ((p : π) × β p) ((p : π) × β p) ℂ) (e : ActiveSpace D k ⊕ ν ↪ (p : π) × β p),
MonomialMatrix M ∧ (Matrix.blockDiagonal' fun (p : π) => slotMatrix (S p)) = M * Embedded.matrix e (inventoryWithIdentity k)