Exact Fourier circuits: toeplitz cross

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

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

def Complexity.ExactFourier.ToeplitzLayers.cross (s : ℕ) (h g : ℕ → ℂ) (i j : ℕ) : ℂ

The finite convolution sum describing the cross block of a truncated Toeplitz product.

Equations

• Complexity.ExactFourier.ToeplitzLayers.cross s h g i j = ∑ l ∈ Finset.range (s - j), h (i - j - l) * g l

theorem Complexity.ExactFourier.ToeplitzLayers.cross_succ (s : ℕ) (h g : ℕ → ℂ) (i j : ℕ) (hi : s ≤ i) (hj : j + 1 < s) : cross s h g (i + 1) (j + 1) = cross s h g i j - h (i + 1 - s) * g (s - (j + 1))

theorem Complexity.ExactFourier.ToeplitzLayers.sum_upper_shift (s j : ℕ) (hj : j ≤ s) (f g : ℕ → ℂ) : (∑ l ∈ Finset.range s, f l * if j ≤ l then g (l - j) else 0) = ∑ l ∈ Finset.range (s - j), f (j + l) * g l

def Complexity.ExactFourier.ToeplitzLayers.lowerCross (s a : ℕ) (h : ℕ → ℂ) : Matrix (Fin a) (Fin s) ℂ

The lower-left cross block obtained by splitting a Toeplitz matrix at time s.

Equations

• Complexity.ExactFourier.ToeplitzLayers.lowerCross s a h i j = h (s + ↑i - ↑j)

theorem Complexity.ExactFourier.ToeplitzLayers.cross_mul (s a : ℕ) (h g : PowerSeries ℂ) : (lowerCross s a fun (x : ℕ) => (PowerSeries.coeff x) h) * CoefficientTime.truncMatrix s g = fun (i : Fin a) (j : Fin s) => cross s (fun (x : ℕ) => (PowerSeries.coeff x) h) (fun (x : ℕ) => (PowerSeries.coeff x) g) (s + ↑i) ↑j

theorem Complexity.ExactFourier.ToeplitzLayers.cross_interior (s a e i₀ j₀ : ℕ) (h g : ℕ → ℂ) (hi : s ≤ i₀) (hj : j₀ + e ≤ s) (i j : ℕ) : i + 1 < a → j + 1 < e → cross s h g (i₀ + (i + 1)) (j₀ + (j + 1)) = cross s h g (i₀ + i) (j₀ + j) + -h (i₀ + (i + 1) - s) * g (s - (j₀ + (j + 1)))

theorem Complexity.ExactFourier.ToeplitzLayers.trunc_split (s a : ℕ) (f : PowerSeries ℂ) : (Matrix.reindex finSumFinEquiv.symm finSumFinEquiv.symm) (CoefficientTime.truncMatrix (s + a) f) = Matrix.fromBlocks (CoefficientTime.truncMatrix s f) 0 (lowerCross s a fun (x : ℕ) => (PowerSeries.coeff x) f) (CoefficientTime.truncMatrix a f)

theorem Complexity.ExactFourier.ToeplitzLayers.lower_shear {α β : Type} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {G : Matrix α β ℂ} {d : ℕ} (h : Layered (rectangularShear G) d) : Layered (Matrix.fromBlocks 1 0 G 1) d

theorem Complexity.ExactFourier.ToeplitzLayers.cross_layer (s a : ℕ) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : Layered (Matrix.fromBlocks 1 0 ((lowerCross s a fun (x : ℕ) => (PowerSeries.coeff x) f) * (CoefficientTime.truncMatrix s f)⁻¹) 1) (2097152 * (Nat.log 2 (a + s) + 1))

theorem Complexity.ExactFourier.ToeplitzLayers.recursion (s a d e : ℕ) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) (hs : Layered (CoefficientTime.truncMatrix s f) d) (ha : Layered (CoefficientTime.truncMatrix a f) e) : Layered (CoefficientTime.truncMatrix (s + a) f) (2097152 * (Nat.log 2 (a + s) + 1) + max d e)

theorem Complexity.ExactFourier.ToeplitzLayers.trunc_small (n : ℕ) (hn : n ≤ 1) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : Layered (CoefficientTime.truncMatrix n f) 1

theorem Complexity.ExactFourier.ToeplitzLayers.trunc_layers_pow (k n : ℕ) (hn : n ≤ 2 ^ k) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : Layered (CoefficientTime.truncMatrix n f) (4194304 * (k + 1) ^ 2)

theorem Complexity.ExactFourier.ToeplitzLayers.trunc_layers (n : ℕ) (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) : Layered (CoefficientTime.truncMatrix n f) (4194304 * (Nat.log 2 n + 2) ^ 2)

theorem Complexity.ExactFourier.Layered.symmetric_triangular {ι : Type} [Fintype ι] [LinearOrder ι] {F P N : Matrix ι ι ℂ} {d : ℕ} (hN : Layered N d) (hP : IsUnit P) (hU : P.IsUpperTriangular) (hL : N.IsLowerTriangular) (hFP : F * P = N) (hF : F.transpose = F) : Layered F (2 * d + 1)

Symmetric Gaussian factorization, avoiding an appeal to LDU uniqueness.

noncomputable def Complexity.ExactFourier.NewtonFourier.invH (ω : ℂ) : PowerSeries ℂ

The formal series of reciprocals of the Newton normalization products.

Equations

• Complexity.ExactFourier.NewtonFourier.invH ω = PowerSeries.mk fun (i : ℕ) => (Complexity.ExactFourier.NewtonFourier.H ω i)⁻¹

@[simp]

theorem Complexity.ExactFourier.NewtonFourier.invH_constant (ω : ℂ) : PowerSeries.constantCoeff (invH ω) = 1

theorem Complexity.ExactFourier.NewtonFourier.N_toeplitz {n : ℕ} {ω : ℂ} (hω : IsPrimitiveRoot ω n) : N n ω = (Matrix.diagonal fun (i : Fin n) => H ω ↑i) * CoefficientTime.truncMatrix n (invH ω) * Matrix.diagonal fun (i : Fin n) => scale ω ↑i

theorem Complexity.ExactFourier.NewtonFourier.P_unit (n : ℕ) (ω : ℂ) : IsUnit (P n ω)

theorem Complexity.ExactFourier.NewtonFourier.N_layers {n : ℕ} (hn : 0 < n) {ω : ℂ} (hω : IsPrimitiveRoot ω n) : Layered (N n ω) (4194304 * (Nat.log 2 n + 2) ^ 2 + 2)

theorem Complexity.ExactFourier.NewtonFourier.dft_layers {n : ℕ} (hn : 0 < n) {ω : ℂ} (hω : IsPrimitiveRoot ω n) : Layered (RadixTwo.dft n ω) (8388608 * (Nat.log 2 n + 2) ^ 2 + 5)

Exact-width Fourier layer theorem, with an absolute constant and a stronger quadratic logarithmic bound.

def Complexity.ExactFourier.FourierCRT.finZMod (n : ℕ) [NeZero n] : Fin n ≃ ZMod n

Identify indices below a positive modulus with its residue classes.

Equations

• Complexity.ExactFourier.FourierCRT.finZMod n = { toFun := fun (i : Fin n) => ↑↑i, invFun := fun (x : ZMod n) => ⟨x.val, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Complexity.ExactFourier.FourierCRT.char_nat {n : ℕ} (ψ : AddChar (ZMod n) ℂ) (k : ℕ) : ψ ↑k = ψ 1 ^ k

theorem Complexity.ExactFourier.FourierCRT.root_primitive {n : ℕ} (ψ : AddChar (ZMod n) ℂ) (hi : Function.Injective ⇑ψ) : IsPrimitiveRoot (ψ 1) n

def Complexity.ExactFourier.FourierCRT.singleAdd {ι : Type} [DecidableEq ι] (r : ι → ℕ) (i : ι) : ZMod (r i) →+ (j : ι) → ZMod (r j)

Embed one residue coordinate into a product of residue-class groups.

Equations

• Complexity.ExactFourier.FourierCRT.singleAdd r i = { toFun := fun (x : ZMod (r i)) => Function.update 0 i x, map_zero' := ⋯, map_add' := ⋯ }

theorem Complexity.ExactFourier.FourierCRT.singleAdd_injective {ι : Type} [DecidableEq ι] (r : ι → ℕ) (i : ι) : Function.Injective ⇑(singleAdd r i)

theorem Complexity.ExactFourier.FourierCRT.sum_singleAdd {ι : Type} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (x : (i : ι) → ZMod (r i)) : ∑ i : ι, (singleAdd r i) (x i) = x

theorem Complexity.ExactFourier.FourierCRT.char_sum {ι : Type} [Fintype ι] [DecidableEq ι] {R : Type} [AddCommMonoid R] (ψ : AddChar R ℂ) (x : ι → R) : ψ (∑ i : ι, x i) = ∏ i : ι, ψ (x i)

noncomputable def Complexity.ExactFourier.FourierCRT.component {ι : Type} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (hn : Pairwise fun (i j : ι) => (r i).Coprime (r j)) [NeZero (∏ i : ι, r i)] (i : ι) : AddChar (ZMod (r i)) ℂ

Restrict the product modulus's standard character to one Chinese-remainder component.

Equations

• Complexity.ExactFourier.FourierCRT.component r hn i = ZMod.stdAddChar.compAddMonoidHom ((ZMod.prodEquivPi r hn).symm.toAddMonoidHom.comp (Complexity.ExactFourier.FourierCRT.singleAdd r i))

theorem Complexity.ExactFourier.FourierCRT.component_injective {ι : Type} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (hn : Pairwise fun (i j : ι) => (r i).Coprime (r j)) [NeZero (∏ i : ι, r i)] (i : ι) : Function.Injective ⇑(component r hn i)

theorem Complexity.ExactFourier.FourierCRT.character_factor {ι : Type} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (hn : Pairwise fun (i j : ι) => (r i).Coprime (r j)) [NeZero (∏ i : ι, r i)] (x : (i : ι) → ZMod (r i)) : ZMod.stdAddChar ((ZMod.prodEquivPi r hn).symm x) = ∏ i : ι, (component r hn i) (x i)

theorem Complexity.ExactFourier.FourierCRT.standard_root (n : ℕ) [NeZero n] : ZMod.stdAddChar 1 = zeta n

theorem Complexity.ExactFourier.FourierCRT.factorization {ι : Type} [Fintype ι] [DecidableEq ι] (r : ι → ℕ) (hr : ∀ (i : ι), 0 < r i) (hn : Pairwise fun (i j : ι) => (r i).Coprime (r j)) : ∃ (ω : ι → ℂ), (∀ (i : ι), IsPrimitiveRoot (ω i) (r i)) ∧ ∃ (e : Fin (∏ i : ι, r i) ≃ ((i : ι) → Fin (r i))), (Matrix.reindex e e) (fourierMatrix (∏ i : ι, r i)) = PiTensor.matrix fun (i : ι) => RadixTwo.dft (r i) (ω i)