Exact Fourier circuits: pi tensor

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

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

def Complexity.ExactFourier.PiTensor.matrix {ι : Type} [Fintype ι] {D : ι → Type} (A : (i : ι) → Matrix (D i) (D i) ℂ) : Matrix ((i : ι) → D i) ((i : ι) → D i) ℂ

The tensor product of a dependent finite family of square matrices.

Equations

• Complexity.ExactFourier.PiTensor.matrix A x y = ∏ i : ι, A i (x i) (y i)

@[simp]

theorem Complexity.ExactFourier.PiTensor.one {ι : Type} [Fintype ι] {D : ι → Type} [(i : ι) → DecidableEq (D i)] : matrix 1 = 1

theorem Complexity.ExactFourier.PiTensor.mul {ι : Type} [Fintype ι] [DecidableEq ι] {D : ι → Type} [(i : ι) → Fintype (D i)] (A B : (i : ι) → Matrix (D i) (D i) ℂ) : matrix (A * B) = matrix A * matrix B

def Complexity.ExactFourier.PiTensor.hom {ι : Type} [Fintype ι] [DecidableEq ι] {D : ι → Type} [(i : ι) → Fintype (D i)] [(i : ι) → DecidableEq (D i)] : ((i : ι) → Matrix (D i) (D i) ℂ) →* Matrix ((i : ι) → D i) ((i : ι) → D i) ℂ

The dependent tensor product as a multiplicative homomorphism.

Equations

• Complexity.ExactFourier.PiTensor.hom = { toFun := Complexity.ExactFourier.PiTensor.matrix, map_one' := ⋯, map_mul' := ⋯ }

theorem Complexity.ExactFourier.PiTensor.unit {ι : Type} [Fintype ι] [DecidableEq ι] {D : ι → Type} [(i : ι) → Fintype (D i)] [(i : ι) → DecidableEq (D i)] (A : (i : ι) → Matrix (D i) (D i) ℂ) (hA : ∀ (i : ι), IsUnit (A i)) : IsUnit (matrix A)

def Complexity.ExactFourier.PiTensor.axisCoordinates {ι : Type} [DecidableEq ι] {D : ι → Type} (i : ι) : (_ : (j : { j : ι // j ≠ i }) → D ↑j) × D i ≃ ((j : ι) → D j)

Separate one coordinate axis from all the remaining dependent coordinates.

Equations

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

@[simp]

theorem Complexity.ExactFourier.PiTensor.axisCoordinates_symm {ι : Type} [DecidableEq ι] {D : ι → Type} (i : ι) (x : (j : ι) → D j) : (axisCoordinates i).symm x = ⟨fun (j : { j : ι // j ≠ i }) => x ↑j, x i⟩

theorem Complexity.ExactFourier.PiTensor.axis_matrix {ι : Type} [Fintype ι] [DecidableEq ι] {D : ι → Type} [(i : ι) → DecidableEq (D i)] (i : ι) (A : Matrix (D i) (D i) ℂ) : matrix (Function.update 1 i A) = (Matrix.reindex (axisCoordinates i) (axisCoordinates i)) (Matrix.blockDiagonal' fun (x : (j : { j : ι // j ≠ i }) → D ↑j) => A)

noncomputable def Complexity.ExactFourier.Packing.Word.axis {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] (i : ι) (W : Word D A (E i)) : Word D A ((i : ι) → E i)

Apply independent copies of a word along one axis of a product space.

Equations

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

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_axis {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] (i : ι) (W : Word D A (E i)) : (axis i W).matrix = PiTensor.matrix (Function.update 1 i W.matrix)

theorem Complexity.ExactFourier.Packing.Word.count_axis {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] [DecidableEq τ] (i : ι) (W : Word D A (E i)) (t : τ) : (axis i W).count t = Fintype.card ((j : { j : ι // j ≠ i }) → E ↑j) * W.count t

noncomputable def Complexity.ExactFourier.Packing.Word.tensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] (W : (i : ι) → Word D A (E i)) : Word D A ((i : ι) → E i)

Compose the axis words to realize their dependent tensor product.

Equations

• Complexity.ExactFourier.Packing.Word.tensor W = (List.map (fun (i : ι) => Complexity.ExactFourier.Packing.Word.axis i (W i)) Finset.univ.toList).flatten

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_tensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] (W : (i : ι) → Word D A (E i)) : (tensor W).matrix = PiTensor.matrix fun (i : ι) => (W i).matrix

theorem Complexity.ExactFourier.Packing.Word.count_tensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {ι : Type} [Fintype ι] [DecidableEq ι] {E : ι → Type} [(i : ι) → Fintype (E i)] [(i : ι) → DecidableEq (E i)] [DecidableEq τ] (W : (i : ι) → Word D A (E i)) (t : τ) : (tensor W).count t = ∑ i : ι, Fintype.card ((j : { j : ι // j ≠ i }) → E ↑j) * (W i).count t

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

Apply a word to the left coordinate of a product, fixing the right coordinate.

Equations

• W.leftTensor = Complexity.ExactFourier.Packing.Word.reindex ((Equiv.sigmaEquivProd β α).trans (Equiv.prodComm β α)) (Complexity.ExactFourier.Packing.Word.blockSum fun (x : β) => W)

noncomputable def Complexity.ExactFourier.Packing.Word.rightTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (V : Word D A β) : Word D A (α × β)

Apply a word to the right coordinate of a product, fixing the left coordinate.

Equations

• V.rightTensor = Complexity.ExactFourier.Packing.Word.reindex (Equiv.sigmaEquivProd α β) (Complexity.ExactFourier.Packing.Word.blockSum fun (x : α) => V)

theorem Complexity.ExactFourier.Packing.Word.matrix_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 α) : W.leftTensor.matrix = W.matrix.kronecker 1

theorem Complexity.ExactFourier.Packing.Word.matrix_rightTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (V : Word D A β) : V.rightTensor.matrix = Matrix.kronecker 1 V.matrix

theorem Complexity.ExactFourier.Packing.Word.count_leftTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] [DecidableEq τ] (W : Word D A α) (t : τ) : W.leftTensor.count t = Fintype.card β * W.count t

theorem Complexity.ExactFourier.Packing.Word.count_rightTensor {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] [DecidableEq τ] (V : Word D A β) (t : τ) : V.rightTensor.count t = Fintype.card α * V.count t

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

Realize the Kronecker product by concatenating the left-axis and right-axis words.

Equations

• W.kronecker V = W.leftTensor ++ V.rightTensor

@[simp]

theorem Complexity.ExactFourier.Packing.Word.matrix_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 β) : (W.kronecker V).matrix = W.matrix.kronecker V.matrix

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

def Complexity.ExactFourier.Packing.sectorCoordinates {σ : Type} {E : σ → Type} (k : σ → ℕ) : (p : σ × σ) × (Fin (k p.1) × Fin (k p.2)) × E p.1 × E p.2 ≃ ((s : σ) × Fin (k s) × E s) × (s : σ) × Fin (k s) × E s

The two tensor axes choose block-copy labels independently, even for repeated species.

Equations

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

def Complexity.ExactFourier.Packing.speciesInventory {σ : Type} [DecidableEq σ] {E : σ → Type} (k : σ → ℕ) (B : (s : σ) → Matrix (E s) (E s) ℂ) : Matrix ((s : σ) × Fin (k s) × E s) ((s : σ) × Fin (k s) × E s) ℂ

The direct sum of the specified number of copies of each species matrix.

Equations

• Complexity.ExactFourier.Packing.speciesInventory k B = Matrix.blockDiagonal' fun (s : σ) => Matrix.kronecker 1 (B s)

def Complexity.ExactFourier.Packing.sectorMatrix {σ : Type} [DecidableEq σ] {E : σ → Type} (k : σ → ℕ) (B : (s : σ) → Matrix (E s) (E s) ℂ) : Matrix ((p : σ × σ) × (Fin (k p.1) × Fin (k p.2)) × E p.1 × E p.2) ((p : σ × σ) × (Fin (k p.1) × Fin (k p.2)) × E p.1 × E p.2) ℂ

The tensor-square inventory regrouped into ordered pairs of species.

Equations

• Complexity.ExactFourier.Packing.sectorMatrix k B = Matrix.blockDiagonal' fun (p : σ × σ) => Matrix.kronecker 1 ((B p.1).kronecker (B p.2))

theorem Complexity.ExactFourier.Packing.inventory_tensor_sectors {σ : Type} [DecidableEq σ] {E : σ → Type} (k : σ → ℕ) (B : (s : σ) → Matrix (E s) (E s) ℂ) : (speciesInventory k B).kronecker (speciesInventory k B) = (Matrix.reindex (sectorCoordinates k) (sectorCoordinates k)) (sectorMatrix k B)

def Complexity.ExactFourier.Packing.colorEquiv {τ π ρ : Type} {D : τ → Type} (u : π → τ) (v : ρ → τ) (e : π ≃ ρ) (he : ∀ (p : π), u p = v (e p)) : (p : π) × D (u p) ≃ (r : ρ) × D (v r)

Transport dependent coordinates through a species-preserving equivalence of sites.

Equations

• Complexity.ExactFourier.Packing.colorEquiv u v e he = e.sigmaCongr fun (p : π) => Equiv.cast ⋯

@[simp]

theorem Complexity.ExactFourier.Packing.colorEquiv_fst {τ π ρ : Type} {D : τ → Type} (u : π → τ) (v : ρ → τ) (e : π ≃ ρ) (he : ∀ (p : π), u p = v (e p)) (x : (p : π) × D (u p)) : ((colorEquiv u v e he) x).fst = e x.fst

theorem Complexity.ExactFourier.Packing.color_cast_apply {τ : Type} {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} {i j : τ} (h : i = j) (a b : D i) : A j (cast ⋯ a) (cast ⋯ b) = A i a b

theorem Complexity.ExactFourier.Packing.coloredBlock_on {τ π ρ : Type} [DecidableEq π] [DecidableEq ρ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (u : π → τ) (v : ρ → τ) (e : π ≃ ρ) (he : ∀ (p : π), u p = v (e p)) (x y : (p : π) × D (u p)) : Matrix.blockDiagonal' (fun (r : ρ) => A (v r)) ((colorEquiv u v e he) x) ((colorEquiv u v e he) y) = Matrix.blockDiagonal' (fun (p : π) => A (u p)) x y

theorem Complexity.ExactFourier.Packing.coloredBlock_reindex {τ π ρ : Type} [DecidableEq π] [DecidableEq ρ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} (u : π → τ) (v : ρ → τ) (e : π ≃ ρ) (he : ∀ (p : π), u p = v (e p)) : (Matrix.reindex (colorEquiv u v e he) (colorEquiv u v e he)) (Matrix.blockDiagonal' fun (p : π) => A (u p)) = Matrix.blockDiagonal' fun (r : ρ) => A (v r)

theorem Complexity.ExactFourier.Packing.exists_colorEquiv {τ π ρ : Type} [Fintype π] [Fintype ρ] [DecidableEq τ] (u : π → τ) (v : ρ → τ) (h : ∀ (t : τ), Fintype.card { p : π // u p = t } = Fintype.card { r : ρ // v r = t }) : ∃ (e : π ≃ ρ), ∀ (p : π), u p = v (e p)

Equal multiplicities give an exact color-preserving matching of call blocks.

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.optionalDomain {τ : Type} (D : τ → Type) : Option τ → Type

The active coordinate type of an optional call, empty when there is no call.

Equations

• Complexity.ExactFourier.Packing.optionalDomain D none = Empty
• Complexity.ExactFourier.Packing.optionalDomain D (some t) = D t

@[instance_reducible]

instance Complexity.ExactFourier.Packing.optionalDomainFintype {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] (t : Option τ) : Fintype (optionalDomain D t)

Equations

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

@[instance_reducible]

instance Complexity.ExactFourier.Packing.optionalDomainDecidableEq {τ : Type} {D : τ → Type} [(t : τ) → DecidableEq (D t)] (t : Option τ) : DecidableEq (optionalDomain D t)

Equations

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

def Complexity.ExactFourier.Packing.optionalMatrix {τ : Type} {D : τ → Type} (A : (t : τ) → Matrix (D t) (D t) ℂ) (t : Option τ) : Matrix (optionalDomain D t) (optionalDomain D t) ℂ

The called matrix, or the identity on the empty domain of an inactive slot.

Equations

• Complexity.ExactFourier.Packing.optionalMatrix A none = 1
• Complexity.ExactFourier.Packing.optionalMatrix A (some t) = A t

def Complexity.ExactFourier.Packing.Step.activeTuple {τ : 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 α) : optionalDomain D s.kind ↪ α

The embedding of a step's active call coordinates into its ambient space.

Equations

• (Complexity.ExactFourier.Packing.Step.mono M hm).activeTuple = { toFun := Empty.elim, inj' := ⋯ }
• (Complexity.ExactFourier.Packing.Step.call t e).activeTuple = e

def Complexity.ExactFourier.Packing.Step.monoPart {τ : Type} {D : τ → Type} [(t : τ) → Fintype (D t)] [(t : τ) → DecidableEq (D t)] {A : (t : τ) → Matrix (D t) (D t) ℂ} {α : Type} [Fintype α] [DecidableEq α] : Step D A α → Matrix α α ℂ

The monomial part of a step, equal to the identity for a species call.

Equations

• (Complexity.ExactFourier.Packing.Step.mono M hm).monoPart = M
• (Complexity.ExactFourier.Packing.Step.call t e).monoPart = 1

theorem Complexity.ExactFourier.Packing.Step.monoPart_monomial {τ : 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 α) : MonomialMatrix s.monoPart

theorem Complexity.ExactFourier.Packing.Step.decompose {τ : 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 α) : s.matrix = s.monoPart * Embedded.matrix s.activeTuple (optionalMatrix A s.kind)

@[reducible, inline]

abbrev Complexity.ExactFourier.Packing.CallIndex {τ π : Type} (u : π → Option τ) : Type

Call sites grouped by their active species, excluding vacant sites.

Equations

• Complexity.ExactFourier.Packing.CallIndex u = ((t : τ) × { p : π // u p = some t })

def Complexity.ExactFourier.Packing.callSite {τ π : Type} (u : π → Option τ) : CallIndex u ↪ π

Forget the species witness and embed active call indices into all sites.

Equations

• Complexity.ExactFourier.Packing.callSite u = { toFun := fun (c : Complexity.ExactFourier.Packing.CallIndex u) => ↑c.snd, inj' := ⋯ }

def Complexity.ExactFourier.Packing.activeTo {τ : Type} {D : τ → Type} {π : Type} (u : π → Option τ) (x : (c : CallIndex u) × D c.fst) : (p : π) × optionalDomain D (u p)

Place species-grouped active coordinates back at their original call sites.

Equations

• Complexity.ExactFourier.Packing.activeTo u x = ⟨↑x.fst.snd, cast ⋯ x.snd⟩

theorem Complexity.ExactFourier.Packing.activeTo_injective {τ : Type} {D : τ → Type} {π : Type} (u : π → Option τ) : Function.Injective (activeTo u)

theorem Complexity.ExactFourier.Packing.activeTo_surjective {τ : Type} {D : τ → Type} {π : Type} (u : π → Option τ) : Function.Surjective (activeTo u)

noncomputable def Complexity.ExactFourier.Packing.activeEquiv {τ : Type} {D : τ → Type} {π : Type} (u : π → Option τ) : (c : CallIndex u) × D c.fst ≃ (p : π) × optionalDomain D (u p)

Identify active coordinates grouped by species with those grouped by call site.

Equations

• Complexity.ExactFourier.Packing.activeEquiv u = Equiv.ofBijective (Complexity.ExactFourier.Packing.activeTo u) ⋯

@[simp]

theorem Complexity.ExactFourier.Packing.activeEquiv_fst {τ : Type} {D : τ → Type} {π : Type} (u : π → Option τ) (x : (c : CallIndex u) × D c.fst) : ((activeEquiv u) x).fst = ↑x.fst.snd

theorem Complexity.ExactFourier.Packing.activeEquiv_on {τ : Type} [DecidableEq τ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [DecidableEq π] (u : π → Option τ) (x y : (c : CallIndex u) × D c.fst) : Matrix.blockDiagonal' (fun (p : π) => optionalMatrix A (u p)) ((activeEquiv u) x) ((activeEquiv u) y) = Matrix.blockDiagonal' (fun (c : CallIndex u) => A c.fst) x y

theorem Complexity.ExactFourier.Packing.activeEquiv_reindex {τ : Type} [DecidableEq τ] {D : τ → Type} {A : (t : τ) → Matrix (D t) (D t) ℂ} {π : Type} [DecidableEq π] (u : π → Option τ) : (Matrix.reindex (activeEquiv u) (activeEquiv u)) (Matrix.blockDiagonal' fun (c : CallIndex u) => A c.fst) = Matrix.blockDiagonal' fun (p : π) => optionalMatrix A (u p)