Exact Fourier circuits: diagonal blocks

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

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

noncomputable def Complexity.ExactFourier.diagonalBlocks {α : Type} {t : ℕ} (A : Fin t → Matrix α α ℂ) : Matrix (Fin t × α) (Fin t × α) ℂ

Place the given square matrices on independent diagonal coordinate blocks.

Equations

• Complexity.ExactFourier.diagonalBlocks A i j = if i.1 = j.1 then A i.1 i.2 j.2 else 0

theorem Complexity.ExactFourier.MatrixPrice.diagonal_blocks {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (t : ℕ) (A : Fin t → Matrix α α ℂ) (hA : ∀ (i : Fin t), IsUnit (A i)) : IsUnit (diagonalBlocks A) ∧ p.value (diagonalBlocks A) = ∑ i : Fin t, p.value (A i)

noncomputable def Complexity.ExactFourier.RootEvaluation.fourier (t : ℕ) (ω : ℂ) : Matrix (Fin t) (Fin t) ℂ

The Fourier matrix formed from the first t powers of ω.

Equations

• Complexity.ExactFourier.RootEvaluation.fourier t ω i j = ω ^ (↑i * ↑j)

@[simp]

theorem Complexity.ExactFourier.RootEvaluation.fourier_mulVec (t : ℕ) (ω : ℂ) (x : Fin t → ℂ) : (fourier t ω).mulVec x = RadixTwo.eval t ω x

theorem Complexity.ExactFourier.RootEvaluation.fourier_unit (t : ℕ) (ht : 0 < t) (ω : ℂ) (hω : IsPrimitiveRoot ω t) : IsUnit (fourier t ω)

theorem Complexity.ExactFourier.RootEvaluation.fourier_price (p : MatrixPrice) (j : ℕ) (ω : ℂ) (hω : IsPrimitiveRoot ω (2 ^ j)) : p.value (fourier (2 ^ j) ω) ≤ 26 / Real.log 2 * 2 ^ j * Real.log (2 * 2 ^ j)

noncomputable def Complexity.ExactFourier.RootEvaluation.matrix (t : ℕ) (ω a : ℂ) : Matrix (Fin t) (Fin t) ℂ

The Vandermonde matrix of the scaled roots a * ω^i.

Equations

• Complexity.ExactFourier.RootEvaluation.matrix t ω a i j = (a * ω ^ ↑i) ^ ↑j

theorem Complexity.ExactFourier.RootEvaluation.matrix_eq (t : ℕ) (ω a : ℂ) : matrix t ω a = fourier t ω * Matrix.diagonal fun (j : Fin t) => a ^ ↑j

theorem Complexity.ExactFourier.RootEvaluation.matrix_unit (t : ℕ) (ht : 0 < t) (ω a : ℂ) (hω : IsPrimitiveRoot ω t) (ha : a ≠ 0) : IsUnit (matrix t ω a)

theorem Complexity.ExactFourier.RootEvaluation.matrix_price (p : MatrixPrice) (j : ℕ) (ω a : ℂ) (hω : IsPrimitiveRoot ω (2 ^ j)) (ha : a ≠ 0) : p.value (matrix (2 ^ j) ω a) ≤ 26 / Real.log 2 * 2 ^ j * Real.log (2 * 2 ^ j)

theorem Complexity.ExactFourier.RootEvaluation.coefficient_sum (t : ℕ) (ω a : ℂ) (f : Polynomial ℂ) (hf : f.natDegree < t) (i : Fin t) : Polynomial.eval (a * ω ^ ↑i) f = ∑ j : Fin t, matrix t ω a i j * f.coeff ↑j

theorem Complexity.ExactFourier.RootEvaluation.eval_remainder (ℓ f : Polynomial ℂ) (s : ℂ) (hs : Polynomial.eval s ℓ = 0) : Polynomial.eval s (f %ₘ ℓ) = Polynomial.eval s f

theorem Complexity.ExactFourier.RootEvaluation.intertwine {α : Type} [Fintype α] [DecidableEq α] (t : ℕ) (ht : 0 < t) (ω a : ℂ) (ℓ : Polynomial ℂ) (hℓ : ℓ.Monic) (hℓt : ℓ.natDegree = t) (hs : ∀ (i : Fin t), Polynomial.eval (a * ω ^ ↑i) ℓ = 0) (G : Matrix α α (Polynomial ℂ)) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (matrix t ω a) 1 * Boundary.modulusMatrix t ℓ G = (diagonalBlocks fun (i : Fin t) => G.map (Polynomial.eval (a * ω ^ ↑i))) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (matrix t ω a) 1

theorem Complexity.ExactFourier.RootEvaluation.root_modulus (t : ℕ) (ht : 0 < t) (ω a : ℂ) (hω : IsPrimitiveRoot ω t) (i : Fin t) : Polynomial.eval (a * ω ^ ↑i) (Polynomial.X ^ t - Polynomial.C (a ^ t)) = 0

theorem Complexity.ExactFourier.RootEvaluation.modulus_upper {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (j : ℕ) (ω a : ℂ) (hω : IsPrimitiveRoot ω (2 ^ j)) (ha : a ≠ 0) (G : Matrix α α (Polynomial ℂ)) (hG : ∀ (i : Fin (2 ^ j)), IsUnit (G.map (Polynomial.eval (a * ω ^ ↑i)))) : IsUnit (Boundary.modulusMatrix (2 ^ j) (Polynomial.X ^ 2 ^ j - Polynomial.C (a ^ 2 ^ j)) G) ∧ p.value (Boundary.modulusMatrix (2 ^ j) (Polynomial.X ^ 2 ^ j - Polynomial.C (a ^ 2 ^ j)) G) ≤ ∑ i : Fin (2 ^ j), p.value (G.map (Polynomial.eval (a * ω ^ ↑i))) + 2 * ↑(Fintype.card α) * (26 / Real.log 2) * 2 ^ j * Real.log (2 * 2 ^ j)

theorem Complexity.ExactFourier.RootEvaluation.exists_dilation (t : ℕ) (ω : ℂ) (hω : ω ≠ 0) (E : Finset ℂ) : ∃ (a : ℂ), a ≠ 0 ∧ ∀ (i : Fin t), a * ω ^ ↑i ∉ E

theorem Complexity.ExactFourier.exists_dyadic_between (b : ℕ) (hb : 0 < b) : ∃ (j : ℕ), b ≤ 2 ^ j ∧ 2 ^ j ≤ 2 * b

theorem Complexity.ExactFourier.fixed_price_of_dyadic_boundary (x y C : ℝ) (hC : 0 ≤ C) (h : ∀ (k j : ℕ), 0 < k → 2 ^ j * ↑k * (x - y) ≤ C * (2 ^ j * Real.log (2 * 2 ^ j) + (↑k + 1) ^ 6)) : x ≤ y

theorem Complexity.ExactFourier.MatrixPrice.specialize_polynomial_zero {α : Type} [Fintype α] [DecidableEq α] (p : MatrixPrice) (G : Matrix α α (Polynomial ℂ)) (hG0 : IsUnit (G.map (Polynomial.eval 0))) (E : Finset ℂ) (C0 : ℝ) (hG : ∀ s ∉ E, IsUnit (G.map (Polynomial.eval s)) ∧ p.value (G.map (Polynomial.eval s)) ≤ C0) : p.value (G.map (Polynomial.eval 0)) ≤ C0