Exact Fourier circuits: tensor tools

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

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

theorem Complexity.ExactFourier.TensorTools.unit_reindex {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (A : Matrix ι ι ℂ) (hA : IsUnit A) : IsUnit ((Matrix.reindex e e) A)

theorem Complexity.ExactFourier.TensorTools.unit_tensor {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) (hA : IsUnit A) (hB : IsUnit B) : IsUnit (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)

def Complexity.ExactFourier.TensorTools.middleEquiv {ι κ τ : Type} : (ι ⊕ κ) ⊕ τ ≃ (ι ⊕ τ) ⊕ κ

Exchange the middle and final summands while retaining the first block.

Equations

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

theorem Complexity.ExactFourier.TensorTools.pad_middle {ι κ τ : Type} [DecidableEq τ] (A : Matrix ι ι ℂ) (E : Matrix ι κ ℂ) (Y : Matrix κ κ ℂ) : (Matrix.reindex middleEquiv middleEquiv) (Matrix.fromBlocks (Matrix.fromBlocks A E 0 Y) 0 0 1) = Matrix.fromBlocks (Matrix.fromBlocks A 0 0 1) (E.fromRows 0) 0 Y

theorem Complexity.ExactFourier.TensorTools.pad_front {ι κ τ : Type} [DecidableEq ι] (B : Matrix τ τ ℂ) (F : Matrix τ κ ℂ) (Z : Matrix κ κ ℂ) : (Matrix.reindex (Equiv.sumAssoc ι τ κ).symm (Equiv.sumAssoc ι τ κ).symm) (Matrix.fromBlocks 1 0 0 (Matrix.fromBlocks B F 0 Z)) = Matrix.fromBlocks (Matrix.fromBlocks 1 0 0 B) (Matrix.fromRows 0 F) 0 Z

theorem Complexity.ExactFourier.TensorTools.join_mul {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] [DecidableEq ι] [DecidableEq τ] (A : Matrix ι ι ℂ) (B : Matrix τ τ ℂ) (E : Matrix ι κ ℂ) (F : Matrix τ κ ℂ) (Y Z : Matrix κ κ ℂ) : Matrix.fromBlocks (Matrix.fromBlocks 1 0 0 B) (Matrix.fromRows 0 F) 0 Z * Matrix.fromBlocks (Matrix.fromBlocks A 0 0 1) (E.fromRows 0) 0 Y = Matrix.fromBlocks (Matrix.fromBlocks A 0 0 B) (E.fromRows (F * Y)) 0 (Z * Y)

theorem Complexity.ExactFourier.TensorTools.price_join {ι κ τ : Type} [Fintype ι] [Fintype κ] [Fintype τ] [DecidableEq ι] [DecidableEq κ] [DecidableEq τ] (p : MatrixPrice) (A : Matrix ι ι ℂ) (B : Matrix τ τ ℂ) (E : Matrix ι κ ℂ) (F : Matrix τ κ ℂ) (Y Z : Matrix κ κ ℂ) (hA : IsUnit A) (hB : IsUnit B) (hY : IsUnit Y) (hZ : IsUnit Z) : p.value (Matrix.fromBlocks (Matrix.fromBlocks A 0 0 B) (E.fromRows (F * Y)) 0 (Z * Y)) ≤ p.value (Matrix.fromBlocks A E 0 Y) + p.value (Matrix.fromBlocks B F 0 Z)

@[reducible, inline]

abbrev Complexity.ExactFourier.CellJoin.join {α β γ : Type} [Fintype β] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) : Matrix ((α ⊕ γ) ⊕ β) ((α ⊕ γ) ⊕ β) ℂ

Execute two cells with shared state and separate data blocks, retaining the final state.

Equations

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

theorem Complexity.ExactFourier.CellJoin.join_eq {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq γ] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) : join X Y = (Matrix.reindex (Equiv.sumAssoc α γ β).symm (Equiv.sumAssoc α γ β).symm) (Matrix.fromBlocks 1 0 0 Y) * (Matrix.reindex TensorTools.middleEquiv TensorTools.middleEquiv) (Matrix.fromBlocks X 0 0 1)

theorem Complexity.ExactFourier.CellJoin.unit {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : IsUnit (join X Y)

theorem Complexity.ExactFourier.CellJoin.price {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] [DecidableEq α] [DecidableEq β] [DecidableEq γ] (p : MatrixPrice) (X : Matrix (α ⊕ β) (α ⊕ β) ℂ) (Y : Matrix (γ ⊕ β) (γ ⊕ β) ℂ) (hX : IsUnit X) (hY : IsUnit Y) : p.value (join X Y) ≤ p.value X + p.value Y

def Complexity.ExactFourier.Triangular.swapLast {α β σ : Type} : (σ × α) × β ≃ (σ × β) × α

Exchange the last two factors of a three-coordinate product.

Equations

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

def Complexity.ExactFourier.Triangular.liftEquiv {α β σ κ : Type} : (σ × α ⊕ κ) × β ≃ (σ × β) × α ⊕ κ × β

Distribute a tensor lift across the triangular data and state blocks.

Equations

• Complexity.ExactFourier.Triangular.liftEquiv = (Equiv.sumProdDistrib (σ × α) κ β).trans (Complexity.ExactFourier.Triangular.swapLast.sumCongr (Equiv.refl (κ × β)))

def Complexity.ExactFourier.Triangular.oldE {α β σ κ : Type} [DecidableEq β] (E : Matrix (σ × α) κ ℂ) : Matrix ((σ × β) × α) (κ × β) ℂ

Lift the previous off-diagonal contribution with an identity on the new tensor factor.

Equations

• Complexity.ExactFourier.Triangular.oldE E i j = E (i.1.1, i.2) j.1 * 1 i.1.2 j.2

theorem Complexity.ExactFourier.Triangular.lift_identity {α β σ κ : Type} [DecidableEq β] [DecidableEq σ] (M : Matrix α α ℂ) (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) : (Matrix.reindex liftEquiv liftEquiv) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) E 0 Y) 1) = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) (oldE E) 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y 1)

theorem Complexity.ExactFourier.Triangular.new_identity {α β κ : Type} [DecidableEq κ] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) : (Matrix.reindex (Equiv.prodSumDistrib κ α β) (Equiv.prodSumDistrib κ α β)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 (Matrix.fromBlocks M C 0 D)) = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 C) 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 D)

def Complexity.ExactFourier.Triangular.nextE {α β σ κ : Type} [DecidableEq β] (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) (C : Matrix α β ℂ) : Matrix ((σ × β ⊕ κ) × α) (κ × β) ℂ

Combine the old lifted contribution with the new coupling contribution.

Equations

• Complexity.ExactFourier.Triangular.nextE E Y C i j = match i.1 with | Sum.inl s => E (s.1, i.2) j.1 * 1 s.2 j.2 | Sum.inr k => Y k j.1 * C i.2 j.2

def Complexity.ExactFourier.Triangular.mergeEquiv {α β σ κ : Type} : ((σ × β) × α ⊕ κ × α) ⊕ κ × β ≃ (σ × β ⊕ κ) × α ⊕ κ × β

Merge the old and new call coordinates into one product block.

Equations

• Complexity.ExactFourier.Triangular.mergeEquiv = (Equiv.sumProdDistrib (σ × β) κ α).symm.sumCongr (Equiv.refl (κ × β))

theorem Complexity.ExactFourier.Triangular.merge_identity {α β σ κ : Type} [Fintype β] [Fintype κ] [DecidableEq β] [DecidableEq σ] [DecidableEq κ] (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) : (Matrix.reindex mergeEquiv mergeEquiv) (Matrix.fromBlocks (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) 0 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M)) ((oldE E).fromRows (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 C * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y 1)) 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 D * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y 1)) = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) (nextE E Y C) 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y D)

theorem Complexity.ExactFourier.Triangular.next_price {α β σ κ : Type} [Fintype α] [Fintype β] [Fintype σ] [Fintype κ] [DecidableEq α] [DecidableEq β] [DecidableEq σ] [DecidableEq κ] (p : MatrixPrice) (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) (hM : IsUnit M) (hD : IsUnit D) (hY : IsUnit Y) : p.value (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) (nextE E Y C) 0 (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y D)) ≤ ↑(Fintype.card β) * p.value (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) E 0 Y) + ↑(Fintype.card κ) * p.value (Matrix.fromBlocks M C 0 D)

def Complexity.ExactFourier.RowCompression.splitEquiv {K : Type u_1} {E : Type u_2} {F : Type u_3} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] (f : E →ₗ[K] F) (s : F →ₗ[K] E) (hs : f ∘ₗ s = LinearMap.id) : E ≃ₗ[K] F × ↥f.ker

A chosen linear right inverse splits a surjection with its kernel.

Equations

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

@[simp]

theorem Complexity.ExactFourier.RowCompression.splitEquiv_fst {K : Type u_1} {E : Type u_2} {F : Type u_3} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] (f : E →ₗ[K] F) (s : F →ₗ[K] E) (hs : f ∘ₗ s = LinearMap.id) (x : E) : ((splitEquiv f s hs) x).1 = f x

theorem Complexity.ExactFourier.RowCompression.surjective_equiv {K : Type u_1} {E : Type u_2} {F : Type u_3} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] [FiniteDimensional K E] (f g : E →ₗ[K] F) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : ∃ (e : E ≃ₗ[K] E), ∀ (x : E), f (e x) = g x

Two surjections from the same finite-dimensional domain differ by an invertible change of domain. This is the block-copy coordinate change V.

theorem Complexity.ExactFourier.RowCompression.range_equiv {K : Type u_1} {E : Type u_2} {F : Type u_3} [Field K] [AddCommGroup E] [Module K E] [AddCommGroup F] [Module K F] [FiniteDimensional K E] (f g : E →ₗ[K] F) (hfg : f.range = g.range) : ∃ (e : E ≃ₗ[K] E), ∀ (x : E), f (e x) = g x

Equality of row spaces, not an assumption of full row rank, suffices.

theorem Complexity.ExactFourier.RowCompression.matrix_row_equiv {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Fintype α] [DecidableEq α] (R S : Matrix α β K) (hRS : Submodule.span K (Set.range R) = Submodule.span K (Set.range S)) : ∃ (V : Matrix α α K), IsUnit V ∧ V * R = S

The row-space equivalence as an actual invertible left multiplier.

theorem Complexity.ExactFourier.RowCompression.sparse_row_compression {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Fintype α] [DecidableEq α] {γ : Type u_4} [Fintype β] (R : Matrix α β K) (Q : γ → β → K) (hspan : Submodule.span K (Set.range R) = Submodule.span K (Set.range Q)) : ∃ (V : Matrix α α K), IsUnit V ∧ ∃ (I : Finset α), I.card ≤ Fintype.card β ∧ (∀ i ∉ I, (V * R) i = 0) ∧ ∀ i ∈ I, ∃ (g : γ), (V * R) i = Q g

Select a sparse spanning-family basis and perform the invertible compression on the whole row-block index. At most dim(β → K) rows remain.