Exact Fourier circuits: pair families

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

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

def Complexity.ExactFourier.PairFamily.sumEquiv {σ τ : Type} : (_ : σ ⊕ τ) × Fin 2 ≃ (_ : σ) × Fin 2 ⊕ (_ : τ) × Fin 2

Distribute the pair-coordinate sigma type over a sum of index types.

Equations

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

theorem Complexity.ExactFourier.PairFamily.sum_blocks {σ τ : Type} [DecidableEq σ] [DecidableEq τ] (H : σ → Matrix (Fin 2) (Fin 2) ℂ) (K : τ → Matrix (Fin 2) (Fin 2) ℂ) : (Matrix.reindex sumEquiv sumEquiv) (Matrix.blockDiagonal' (Sum.elim H K)) = Matrix.fromBlocks (Matrix.blockDiagonal' H) 0 0 (Matrix.blockDiagonal' K)

def Complexity.ExactFourier.PairFamily.subEmbedding {σ : Type} (S : Set σ) : (_ : ↑S) × Fin 2 ↪ (_ : σ) × Fin 2

Embed the pair coordinates indexed by a subset into the full family.

Equations

• Complexity.ExactFourier.PairFamily.subEmbedding S = { toFun := fun (i : (_ : ↑S) × Fin 2) => ⟨↑i.fst, i.snd⟩, inj' := ⋯ }

theorem Complexity.ExactFourier.PairFamily.sub_blocks {σ : Type} [DecidableEq σ] (S : Set σ) [DecidablePred fun (x : σ) => x ∈ S] (H : σ → Matrix (Fin 2) (Fin 2) ℂ) : Embedded.matrix (subEmbedding S) (Matrix.blockDiagonal' fun (i : ↑S) => H ↑i) = Matrix.blockDiagonal' fun (i : σ) => if i ∈ S then H i else 1

theorem Complexity.ExactFourier.PairFamily.split_blocks {σ : Type} [Fintype σ] [DecidableEq σ] (S : Set σ) [DecidablePred fun (x : σ) => x ∈ S] (H : σ → Matrix (Fin 2) (Fin 2) ℂ) : Matrix.blockDiagonal' H = Embedded.matrix (subEmbedding S) (Matrix.blockDiagonal' fun (i : ↑S) => H ↑i) * Embedded.matrix (subEmbedding Sᶜ) (Matrix.blockDiagonal' fun (i : ↑Sᶜ) => H ↑i)

structure Complexity.ExactFourier.PairFamily (α : Type) [Fintype α] [DecidableEq α] : Type 1

A simultaneous pair family retains its actual disjoint ordered coordinate tuples.

• index : Type

  The finite index type of disjoint two-coordinate operations.

• finite : Fintype self.index
• dec : DecidableEq self.index
• pairs : self.index → Matrix (Fin 2) (Fin 2) ℂ

  The invertible two-coordinate matrix assigned to each family index.

• unit (i : self.index) : IsUnit (self.pairs i)
• position : (_ : self.index) × Fin 2 ↪ α

  The embedding placing all pairs on disjoint ambient coordinates.

noncomputable def Complexity.ExactFourier.PairFamily.matrix {α : Type} [Fintype α] [DecidableEq α] (P : PairFamily α) : Matrix α α ℂ

Apply every pair matrix on its embedded block and fix the remaining coordinates.

Equations

• P.matrix = Complexity.ExactFourier.Embedded.matrix P.position (Matrix.blockDiagonal' P.pairs)

def Complexity.ExactFourier.PairFamily.empty {α : Type} [Fintype α] [DecidableEq α] : PairFamily α

The empty pair family, whose ambient action is the identity.

Equations

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

theorem Complexity.ExactFourier.PairFamily.empty_matrix {α : Type} [Fintype α] [DecidableEq α] : empty.matrix = 1

def Complexity.ExactFourier.PairFamily.pair (H : Matrix (Fin 2) (Fin 2) ℂ) (hu : IsUnit H) : PairFamily (Fin 2)

The family consisting of one invertible two-coordinate matrix.

Equations

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

theorem Complexity.ExactFourier.PairFamily.pair_matrix (H : Matrix (Fin 2) (Fin 2) ℂ) (hu : IsUnit H) : (pair H hu).matrix = H

def Complexity.ExactFourier.PairFamily.reindex {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (P : PairFamily α) (e : α ≃ β) : PairFamily β

Relabel the ambient coordinates of a disjoint pair family.

Equations

• P.reindex e = { index := P.index, finite := P.finite, dec := P.dec, pairs := P.pairs, unit := ⋯, position := P.position.trans e.toEmbedding }

theorem Complexity.ExactFourier.PairFamily.reindex_matrix {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (P : PairFamily α) (e : α ≃ β) : (P.reindex e).matrix = (Matrix.reindex e e) P.matrix

def Complexity.ExactFourier.PairFamily.sum {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (P : PairFamily α) (Q : PairFamily β) : PairFamily (α ⊕ β)

Combine pair families on the two disjoint blocks of a sum type.

Equations

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

theorem Complexity.ExactFourier.PairFamily.sum_matrix {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (P : PairFamily α) (Q : PairFamily β) : (P.sum Q).matrix = Matrix.fromBlocks P.matrix 0 0 Q.matrix

theorem Complexity.ExactFourier.PairFamily.card_le {α : Type} [Fintype α] [DecidableEq α] (P : PairFamily α) : 2 * Fintype.card P.index ≤ Fintype.card α

theorem Complexity.ExactFourier.Round.pair_rep {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} (h : Round M) : ∃ (P : PairFamily α) (Q : Matrix α α ℂ), MonomialMatrix Q ∧ M = P.matrix * Q

theorem Complexity.ExactFourier.AGenerated.blocks_fin {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (n : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] [(i : Fin n) → DecidableEq (D i)] (M : (i : Fin n) → Matrix (D i) (D i) ℂ) (d : ℕ) (hM : ∀ (i : Fin n), AGenerated A (M i) d) : AGenerated A (Matrix.blockDiagonal' M) d

theorem Complexity.ExactFourier.AGenerated.blocks {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {σ : Type} [Fintype σ] [DecidableEq σ] (D : σ → Type) [(i : σ) → Fintype (D i)] [(i : σ) → DecidableEq (D i)] (M : (i : σ) → Matrix (D i) (D i) ℂ) (d : ℕ) (hM : ∀ (i : σ), AGenerated A (M i) d) : AGenerated A (Matrix.blockDiagonal' M) d

theorem Complexity.ExactFourier.AGenerated.blockDiagonal {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α σ : Type} [Fintype α] [Fintype σ] [DecidableEq α] [DecidableEq σ] (M : σ → Matrix α α ℂ) (d : ℕ) (hM : ∀ (i : σ), AGenerated A (M i) d) : AGenerated A (Matrix.blockDiagonal M) d

theorem Complexity.ExactFourier.PairFamily.one_batch {q h : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {σ α : Type} [Fintype σ] [Fintype α] [DecidableEq σ] [DecidableEq α] (H : σ → Matrix (Fin 2) (Fin 2) ℂ) (hH : ∀ (i : σ), IsUnit (H i)) (e : (_ : σ) × Fin 2 ↪ α) (hc : q * Fintype.card σ ≤ Fintype.card α) : AGenerated A (Embedded.matrix e (Matrix.blockDiagonal' H)) (h + 1)

theorem Complexity.ExactFourier.PairFamily.batches {q h : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {σ α : Type} [Fintype σ] [Fintype α] [DecidableEq σ] [DecidableEq α] (b c : ℕ) (hc : q * c ≤ Fintype.card α) (H : σ → Matrix (Fin 2) (Fin 2) ℂ) (hH : ∀ (i : σ), IsUnit (H i)) (e : (_ : σ) × Fin 2 ↪ α) (hs : Fintype.card σ ≤ b * c) : AGenerated A (Embedded.matrix e (Matrix.blockDiagonal' H)) (b * (h + 1))

theorem Complexity.ExactFourier.PairFamily.generated {q h : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {α : Type} [Fintype α] [DecidableEq α] (P : PairFamily α) (hr : 2 * q ≤ Fintype.card α) : AGenerated A P.matrix (q * (h + 1))

theorem Complexity.ExactFourier.Round.generated {q h : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {M : Matrix α α ℂ} (hM : Round M) (hr : 2 * q ≤ Fintype.card α) : AGenerated A M (q * (h + 1) + 1)

theorem Complexity.ExactFourier.Layered.generated {q h : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) {M : Matrix α α ℂ} {d : ℕ} (hM : Layered M d) (hr : 2 * q ≤ Fintype.card α) : AGenerated A M (d * (q * (h + 1) + 1))

theorem Complexity.ExactFourier.AGenerated.zero {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} (h : AGenerated A M 0) : M = 1

theorem Complexity.ExactFourier.AGenerated.succ {q d : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {α : Type} [Fintype α] [DecidableEq α] {M : Matrix α α ℂ} (h : AGenerated A M (d + 1)) : ∃ (X : Matrix α α ℂ) (Y : Matrix α α ℂ), AFrame A X ∧ AGenerated A Y d ∧ M = X * Y

theorem Complexity.ExactFourier.ParallelTensorCost.frames_cost {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) (n : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] [(i : Fin n) → DecidableEq (D i)] (M : (i : Fin n) → Matrix (D i) (D i) ℂ) (hM : ∀ (i : Fin n), AFrame A (M i)) : ↑(CircuitCost.cost (PiTensor.matrix M)) ≤ C * ↑(Fintype.card ((i : Fin n) → D i)) * (↑n + 1) ^ a + ↑(Fintype.card ((i : Fin n) → D i))

theorem Complexity.ExactFourier.ParallelTensorCost.generated_cost {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) (n d : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] [(i : Fin n) → DecidableEq (D i)] (M : (i : Fin n) → Matrix (D i) (D i) ℂ) (hM : ∀ (i : Fin n), AGenerated A (M i) d) : ↑(CircuitCost.cost (PiTensor.matrix M)) ≤ ↑d * (C * ↑(Fintype.card ((i : Fin n) → D i)) * (↑n + 1) ^ a + ↑(Fintype.card ((i : Fin n) → D i)))

theorem Complexity.ExactFourier.ParallelTensorCost.layered_cost {q : ℕ} {A : Matrix (Fin q) (Fin q) ℂ} {a C : ℝ} (ha : 0 ≤ a) (hC : 0 ≤ C) (amp : ∀ (k : ℕ), ↑(CircuitCost.cost (TensorAxis.power A k)) ≤ C * ↑q ^ k * (↑k + 1) ^ a) {h : ℕ} (hq : 2 ≤ q) (gen : ∀ (M : Matrix (Fin q) (Fin q) ℂ), IsUnit M → PositiveGeneration.Pattern A h M) (n d : ℕ) (D : Fin n → Type) [(i : Fin n) → Fintype (D i)] [(i : Fin n) → DecidableEq (D i)] (M : (i : Fin n) → Matrix (D i) (D i) ℂ) (hM : ∀ (i : Fin n), Layered (M i) d) (hD : ∀ (i : Fin n), 2 * q ≤ Fintype.card (D i)) : ↑(CircuitCost.cost (PiTensor.matrix M)) ≤ ↑(d * (q * (h + 1) + 1)) * (C * ↑(Fintype.card ((i : Fin n) → D i)) * (↑n + 1) ^ a + ↑(Fintype.card ((i : Fin n) → D i)))