FFTCircuit.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The exact radix-two DAG needed by scalar convolution in the missing main proof. All multiplies by the roots and normalization scalars are charged.

theorem OAI.ExactFourier.RadixTwo.exists_fft_dag line 11
def OAI.ExactFourier.ScalarConvolution.padIndex line 61
def OAI.ExactFourier.ScalarConvolution.padded line 64
theorem OAI.ExactFourier.ScalarConvolution.eval_padding line 67
theorem OAI.ExactFourier.ScalarConvolution.ofFn_padded line 76
def OAI.ExactFourier.ScalarConvolution.diagonalDAG line 92
Source documentation
A fixed diagonal layer charges exactly one multiplication per coordinate.
```
def diagonalDAG {m : ℕ} (c : Fin m → ℂ) : LinearDAG m m :=
…
```
Mentions: OAI.ExactFourier.LinearDAG
theorem OAI.ExactFourier.ScalarConvolution.diagonalDAG_eval line 95

theorem OAI.ExactFourier.ScalarConvolution.convolution_dag_at_power line 102

Source documentation

Polynomial convolution on any containing radix-two length.

theorem convolution_dag_at_power (k t : ℕ) (ht : 0 < t) (htm : 2*t ≤ 2^k)
    (f : ℂ[X]) (hf : f.natDegree < t) :
    ∃ C : LinearDAG t t, C.size ≤ (6*k+1)*2^k ∧
      ∀ x i, C.eval x i = (f * Polynomial.ofFn t x).coeff i.val := by
…

Mentions: OAI.ExactFourier.LinearDAG

theorem OAI.ExactFourier.ScalarConvolution.exists_truncation_dag line 136
Source documentation
Uniform linear-DAG construction, with logarithmic cost independent of coefficients.
```
theorem exists_truncation_dag (t : ℕ) (ht : 0 < t) (f : PowerSeries ℂ) :
    ∃ C : LinearDAG t t, C.size ≤ 52 * t * (Nat.log 2 t + 1) ∧
      ∀ x, C.eval x = (truncMatrix t f).mulVec x := by
…
```
Mentions: OAI.ExactFourier.LinearDAG

theorem OAI.ExactFourier.ScalarConvolution.truncMatrix_inv line 177

Source documentation

Inversion commutes exactly with truncated scalar multiplication.

theorem truncMatrix_inv (t : ℕ) (f : PowerSeries ℂ)
    (hf : PowerSeries.constantCoeff f ≠ 0) :
    (truncMatrix t f)⁻¹ = truncMatrix t f⁻¹ := by
…

theorem OAI.ExactFourier.ScalarConvolution.price_truncation_nat line 183

theorem OAI.ExactFourier.ScalarConvolution.price_truncation line 201

Source documentation

The literal O(t log(2t)) estimate, with one absolute constant, uniform in f and t.

theorem price_truncation (p : MatrixPrice) (t : ℕ) (ht : 0 < t)
    (f : PowerSeries ℂ) (hf : PowerSeries.constantCoeff f ≠ 0) :
    p.value (truncMatrix t f) ≤ (627 / Real.log 2) * (t : ℝ) * Real.log (2*t) := by
…

Mentions: OAI.ExactFourier.MatrixPrice

theorem OAI.ExactFourier.CoefficientTime.blockTrunc_smul_one line 234
theorem OAI.ExactFourier.CoefficientTime.scalar_correction line 241
theorem OAI.ExactFourier.MatrixPrice.eliminate_series line 256
theorem OAI.ExactFourier.Cascade.q_constant line 289
theorem OAI.ExactFourier.Cascade.coefficients_eq_columns line 295
theorem OAI.ExactFourier.Cascade.uniform_bound line 301