Exact Fourier circuits: sparse shear

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

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

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_add_le (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G H : Matrix ι κ ℂ) : p.value (rectangularShear (G + H)) ≤ p.value (rectangularShear G) + p.value (rectangularShear H)

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_single {ι κ : Type} [DecidableEq ι] [DecidableEq κ] (i : ι) (j : κ) (c : ℂ) : rectangularShear (Matrix.single i j c) = Matrix.transvection (Sum.inl i) (Sum.inr j) c

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_sum_le (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] {α : Type u_1} (s : Finset α) (G : α → Matrix ι κ ℂ) : p.value (rectangularShear (∑ i ∈ s, G i)) ≤ ∑ i ∈ s, p.value (rectangularShear (G i))

theorem Complexity.ExactFourier.MatrixPrice.rectangularShear_sparse (p : MatrixPrice) {ι κ : Type} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (G : Matrix ι κ ℂ) : p.value (rectangularShear G) ≤ ↑{ij : ι × κ | G ij.1 ij.2 ≠ 0}.card

A rectangular shear costs at most one per nonzero matrix entry.

def Complexity.ExactFourier.Triangular.flat {α σ κ : Type} (E : Matrix (σ × α) κ ℂ) : Matrix σ (α × κ) ℂ

Regroup matrix row and column indices to flatten a family of block rows.

Equations

• Complexity.ExactFourier.Triangular.flat E s j = E (s, j.1) j.2

def Complexity.ExactFourier.Triangular.liftRows {α β σ κ : Type} (R : Matrix σ (α × κ) ℂ) (H : Matrix β β ℂ) : Matrix (σ × β) (α × κ × β) ℂ

Tensor existing generator rows with the next state matrix and regroup coordinates.

Equations

• Complexity.ExactFourier.Triangular.liftRows R H i j = R i.1 (j.1, j.2.1) * H i.2 j.2.2

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

The new generator rows introduced by one additional triangular stage.

Equations

• Complexity.ExactFourier.Triangular.freshRows T i j = 1 i j.2.1 * T j.1 j.2.2

def Complexity.ExactFourier.Triangular.nextRows {α β σ κ : Type} [DecidableEq κ] (R : Matrix σ (α × κ) ℂ) (T : Matrix α β ℂ) (H : Matrix β β ℂ) : Matrix (σ × β ⊕ κ) (α × κ × β) ℂ

Stack the lifted old rows above the fresh rows of the next stage.

Equations

• Complexity.ExactFourier.Triangular.nextRows R T H = (Complexity.ExactFourier.Triangular.liftRows R H).fromRows (Complexity.ExactFourier.Triangular.freshRows T)

theorem Complexity.ExactFourier.Triangular.liftRows_mul {α β σ κ : Type} [Fintype β] [Fintype σ] (V : Matrix σ σ ℂ) (B : Matrix β β ℂ) (R : Matrix σ (α × κ) ℂ) (H : Matrix β β ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V B * liftRows R H = liftRows (V * R) (B * H)

theorem Complexity.ExactFourier.Triangular.nextRows_change {α β σ κ : Type} [Fintype β] [Fintype σ] [Fintype κ] [DecidableEq β] [DecidableEq κ] (V : Matrix σ σ ℂ) (D : Matrix β β ℂ) (R : Matrix σ (α × κ) ℂ) (T : Matrix α β ℂ) (hD : IsUnit D) : Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V D) 0 0 1 * nextRows R T D⁻¹ = nextRows (V * R) T 1

theorem Complexity.ExactFourier.Triangular.flat_next_normalized {α β σ κ : Type} [Fintype β] [Fintype κ] [DecidableEq β] [DecidableEq κ] (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (hY : IsUnit Y) : flat (nextE E Y C * (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) Y D)⁻¹) = nextRows (flat (E * Y⁻¹)) (C * D⁻¹) D⁻¹

theorem Complexity.ExactFourier.Triangular.span_rows_unit_mul {σ : Type} [Fintype σ] [DecidableEq σ] {δ : Type} (V : Matrix σ σ ℂ) (R : Matrix σ δ ℂ) (hV : IsUnit V) : Submodule.span ℂ (Set.range (V * R)) = Submodule.span ℂ (Set.range R)

Ordinary matrix row spaces are unchanged by an invertible row multiplier.

noncomputable def Complexity.ExactFourier.Triangular.nnz {δ : Type} [Fintype δ] (v : δ → ℂ) : ℕ

Number of supported scalar positions.

Equations

• Complexity.ExactFourier.Triangular.nnz v = {i : δ | v i ≠ 0}.card

theorem Complexity.ExactFourier.Triangular.nnz_lift_one {α β σ κ : Type} [Fintype α] [Fintype β] [Fintype κ] [DecidableEq β] (Q : Matrix σ (α × κ) ℂ) (s : σ) (b : β) : nnz (liftRows Q 1 (s, b)) ≤ nnz (Q s)

theorem Complexity.ExactFourier.Triangular.nnz_fresh {α β κ : Type} [Fintype α] [Fintype β] [Fintype κ] [DecidableEq κ] (T : Matrix α β ℂ) (i : κ) : nnz (freshRows T i) ≤ Fintype.card α * Fintype.card β

theorem Complexity.ExactFourier.Triangular.nnz_nextRows {α β σ κ : Type} [Fintype α] [Fintype β] [Fintype κ] [DecidableEq β] [DecidableEq κ] (Q : Matrix σ (α × κ) ℂ) (T : Matrix α β ℂ) (hQ : ∀ (s : σ), nnz (Q s) ≤ Fintype.card α * Fintype.card β) (s : σ × β ⊕ κ) : nnz (nextRows Q T 1 s) ≤ Fintype.card α * Fintype.card β

@[reducible, inline]

abbrev Complexity.ExactFourier.Triangular.Bottom (β : Type) : ℕ → Type

Recursive axis/fiber indexing; no extra workspace is introduced.

Equations

• Complexity.ExactFourier.Triangular.Bottom β 0 = PUnit.{1}
• Complexity.ExactFourier.Triangular.Bottom β k.succ = (Complexity.ExactFourier.Triangular.Bottom β k × β)

@[reducible, inline]

abbrev Complexity.ExactFourier.Triangular.Calls (β : Type) : ℕ → Type

The recursively accumulated call-coordinate type in the triangular tensor construction.

Equations

• Complexity.ExactFourier.Triangular.Calls β 0 = PEmpty.{1}
• Complexity.ExactFourier.Triangular.Calls β k.succ = (Complexity.ExactFourier.Triangular.Calls β k × β ⊕ Complexity.ExactFourier.Triangular.Bottom β k)

@[reducible]

noncomputable instance Complexity.ExactFourier.Triangular.bottomFintype (β : Type) [Fintype β] (k : ℕ) : Fintype (Bottom β k)

Equations

• Complexity.ExactFourier.Triangular.bottomFintype β 0 = { elems := {PUnit.unit}, complete := ⋯ }
• Complexity.ExactFourier.Triangular.bottomFintype β k.succ = { elems := Finset.univ ×ˢ Finset.univ, complete := ⋯ }

@[reducible]

noncomputable instance Complexity.ExactFourier.Triangular.callsFintype (β : Type) [Fintype β] (k : ℕ) : Fintype (Calls β k)

Equations

• Complexity.ExactFourier.Triangular.callsFintype β 0 = { elems := ∅, complete := ⋯ }
• Complexity.ExactFourier.Triangular.callsFintype β k.succ = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[reducible]

instance Complexity.ExactFourier.Triangular.bottomDecidableEq (β : Type) [DecidableEq β] (k : ℕ) : DecidableEq (Bottom β k)

Equations

• Complexity.ExactFourier.Triangular.bottomDecidableEq β 0 = instDecidableEqPUnit
• Complexity.ExactFourier.Triangular.bottomDecidableEq β k.succ = fun (a b : Complexity.ExactFourier.Triangular.Bottom β k × β) => instDecidableEqProd a b

@[reducible]

instance Complexity.ExactFourier.Triangular.callsDecidableEq (β : Type) [DecidableEq β] (k : ℕ) : DecidableEq (Calls β k)

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Triangular.callsDecidableEq β 0 = instDecidableEqPEmpty

theorem Complexity.ExactFourier.Triangular.bottom_card_zero {β : Type} : Fintype.card (Bottom β 0) = 1

theorem Complexity.ExactFourier.Triangular.calls_card_zero {β : Type} : Fintype.card (Calls β 0) = 0

theorem Complexity.ExactFourier.Triangular.bottom_card_succ {β : Type} [Fintype β] (k : ℕ) : Fintype.card (Bottom β (k + 1)) = Fintype.card (Bottom β k) * Fintype.card β

theorem Complexity.ExactFourier.Triangular.calls_card_succ {β : Type} [Fintype β] (k : ℕ) : Fintype.card (Calls β (k + 1)) = Fintype.card (Calls β k) * Fintype.card β + Fintype.card (Bottom β k)

theorem Complexity.ExactFourier.Triangular.calls_card_relation {β : Type} [Fintype β] (k : ℕ) : Fintype.card (Calls β k) * Fintype.card β = k * Fintype.card (Bottom β k)

theorem Complexity.ExactFourier.Triangular.bottom_card_pos {β : Type} [Fintype β] (hβ : 0 < Fintype.card β) (k : ℕ) : 0 < Fintype.card (Bottom β k)

noncomputable def Complexity.ExactFourier.Triangular.tensorPower {β : Type} (D : Matrix β β ℂ) (k : ℕ) : Matrix (Bottom β k) (Bottom β k) ℂ

Tensor powers indexed by the recursively defined bottom-coordinate type.

Equations

• Complexity.ExactFourier.Triangular.tensorPower D 0 = 1
• Complexity.ExactFourier.Triangular.tensorPower D k.succ = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Complexity.ExactFourier.Triangular.tensorPower D k) D

noncomputable def Complexity.ExactFourier.Triangular.contamination {α β : Type} [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (k : ℕ) : Matrix (Calls β k × α) (Bottom β k) ℂ

The accumulated off-diagonal contribution of the triangular tensor construction.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.ExactFourier.Triangular.contamination C D 0 = 0

noncomputable def Complexity.ExactFourier.Triangular.generators {α β : Type} [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (k : ℕ) : Matrix (Calls β k) (α × Bottom β k) ℂ

Recursive generator rows after normalizing the coupling by the state inverse.

Equations

• Complexity.ExactFourier.Triangular.generators C D 0 = 0
• Complexity.ExactFourier.Triangular.generators C D k.succ = Complexity.ExactFourier.Triangular.nextRows (Complexity.ExactFourier.Triangular.generators C D k) (C * D⁻¹) 1

noncomputable def Complexity.ExactFourier.Triangular.rowBasis {β : Type} [DecidableEq β] (D : Matrix β β ℂ) (k : ℕ) : Matrix (Calls β k) (Calls β k) ℂ

The recursive block change of basis on the accumulated call coordinates.

Equations

• Complexity.ExactFourier.Triangular.rowBasis D 0 = 1
• Complexity.ExactFourier.Triangular.rowBasis D k.succ = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Complexity.ExactFourier.Triangular.rowBasis D k) D) 0 0 1

theorem Complexity.ExactFourier.Triangular.tensorPower_unit {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) (hD : IsUnit D) (k : ℕ) : IsUnit (tensorPower D k)

theorem Complexity.ExactFourier.Triangular.rowBasis_unit {β : Type} [Fintype β] [DecidableEq β] (D : Matrix β β ℂ) (hD : IsUnit D) (k : ℕ) : IsUnit (rowBasis D k)

theorem Complexity.ExactFourier.Triangular.rowBasis_normalizes {α β : Type} [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (hD : IsUnit D) (k : ℕ) : rowBasis D k * flat (contamination C D k * (tensorPower D k)⁻¹) = generators C D k

theorem Complexity.ExactFourier.Triangular.generators_sparse {α β : Type} [Fintype α] [Fintype β] [DecidableEq β] (C : Matrix α β ℂ) (D : Matrix β β ℂ) (k : ℕ) (i : Calls β k) : nnz (generators C D k i) ≤ Fintype.card α * Fintype.card β

theorem Complexity.ExactFourier.Triangular.tensorPower_price {β : Type} [Fintype β] [DecidableEq β] (p : MatrixPrice) (D : Matrix β β ℂ) (hD : IsUnit D) (k : ℕ) : p.value (tensorPower D k) = ↑(Fintype.card (Calls β k)) * p.value D

theorem Complexity.ExactFourier.Triangular.experiment_price {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (p : MatrixPrice) (M : Matrix α α ℂ) (C : Matrix α β ℂ) (D : Matrix β β ℂ) (hM : IsUnit M) (hD : IsUnit D) (k : ℕ) : p.value (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) (contamination C D k) 0 (tensorPower D k)) ≤ ↑(Fintype.card (Calls β k)) * p.value (Matrix.fromBlocks M C 0 D)

theorem Complexity.ExactFourier.Triangular.flat_left {α σ κ : Type} [Fintype α] [Fintype σ] [DecidableEq α] (V : Matrix σ σ ℂ) (E : Matrix (σ × α) κ ℂ) : flat (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V 1 * E) = V * flat E

theorem Complexity.ExactFourier.Triangular.nnz_flat {α σ κ : Type} [Fintype α] [Fintype σ] [Fintype κ] (E : Matrix (σ × α) κ ℂ) : (nnz fun (ij : (σ × α) × κ) => E ij.1 ij.2) = ∑ s : σ, nnz (flat E s)

theorem Complexity.ExactFourier.Triangular.nnz_selected_le {σ : Type} [Fintype σ] {δ : Type} [Fintype δ] (R : Matrix σ δ ℂ) (I : Finset σ) (B : ℕ) (hzero : ∀ i ∉ I, R i = 0) (hB : ∀ i ∈ I, nnz (R i) ≤ B) : ∑ i : σ, nnz (R i) ≤ I.card * B

theorem Complexity.ExactFourier.Triangular.cancellation_identity {α σ κ : Type} [Fintype α] [Fintype σ] [Fintype κ] [DecidableEq α] [DecidableEq σ] [DecidableEq κ] (M : Matrix α α ℂ) (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) (V : Matrix σ σ ℂ) (hY : IsUnit Y) : rectangularShear (-(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V 1 * (E * Y⁻¹))) * Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V 1) 0 0 1 * Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) E 0 Y = Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V M) 0 0 Y

theorem Complexity.ExactFourier.Triangular.compressed_price {α σ κ : Type} [Fintype α] [Fintype σ] [Fintype κ] [DecidableEq α] [DecidableEq σ] [DecidableEq κ] (p : MatrixPrice) (M : Matrix α α ℂ) (E : Matrix (σ × α) κ ℂ) (Y : Matrix κ κ ℂ) (hM : IsUnit M) (hY : IsUnit Y) {γ : Type} (Q : γ → α × κ → ℂ) (hspan : Submodule.span ℂ (Set.range (flat (E * Y⁻¹))) = Submodule.span ℂ (Set.range Q)) (B : ℕ) (hQ : ∀ (g : γ), nnz (Q g) ≤ B) : ↑(Fintype.card σ) * p.value M + p.value Y ≤ p.value (Matrix.fromBlocks (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 M) E 0 Y) + ↑(Fintype.card α) * ↑(Fintype.card κ) * ↑B