ClearedCircuit.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

The O_K(k² n^k) evaluation DAG and O_K((k+1)³ n^k) coefficient DAG for the literal polynomial state correction, uniform in truncation length.

def OAI.ExactFourier.Cascade.clearedDAG line 14
theorem OAI.ExactFourier.Cascade.eval_clearedDAG line 20
theorem OAI.ExactFourier.Cascade.size_clearedDAG line 32
theorem OAI.ExactFourier.Cascade.exists_cleared_coeff_dag line 56
theorem OAI.ExactFourier.TypedDAG.circuit_eval_of_matrix line 107
theorem OAI.ExactFourier.TypedDAG.shear_price line 119
theorem OAI.ExactFourier.MatrixPrice.eliminate_top_right line 137
def OAI.ExactFourier.RadixTwo.evenIndex line 184
def OAI.ExactFourier.RadixTwo.oddIndex line 185
def OAI.ExactFourier.RadixTwo.parityEquiv line 187
theorem OAI.ExactFourier.RadixTwo.sum_even_odd line 203
def OAI.ExactFourier.RadixTwo.evalAt line 209
def OAI.ExactFourier.RadixTwo.eval line 212
theorem OAI.ExactFourier.RadixTwo.power_even line 215
theorem OAI.ExactFourier.RadixTwo.power_odd line 220
theorem OAI.ExactFourier.RadixTwo.evalAt_split line 225
theorem OAI.ExactFourier.RadixTwo.evalAt_periodic line 232
theorem OAI.ExactFourier.RadixTwo.square_period line 238

theorem OAI.ExactFourier.RadixTwo.eval_split line 243

Source documentation

First and second frequency halves are the sum and difference butterfly.

theorem eval_split (n : ℕ) (ω : ℂ) (hω : ω^n = -1) (x : Fin (n+n) → ℂ) :
    eval (n+n) ω x = Fin.addCases
      (fun i => eval n (ω^2) (x ∘ evenIndex n) i + ω^i.val * eval n (ω^2) (x ∘ oddIndex n) i)
      (fun i => eval n (ω^2) (x ∘ evenIndex n) i - ω^i.val * eval n (ω^2) (x ∘ oddIndex n) i) := by
…

Mentions: OAI.ExactFourier.RadixTwo.eval, OAI.ExactFourier.RadixTwo.evenIndex, OAI.ExactFourier.RadixTwo.oddIndex

theorem OAI.ExactFourier.RadixTwo.orthogonality line 257

Source documentation

Orthogonality of the exact n-th root evaluation matrix.

theorem orthogonality {n : ℕ} (hn : 0<n) (ω : ℂ) (hω : IsPrimitiveRoot ω n)
    (i k : Fin n) :
    (∑ j : Fin n, (ω⁻¹)^(i.val*j.val) * ω^(k.val*j.val)) =
      if i=k then (n : ℂ) else 0 := by
…

theorem OAI.ExactFourier.RadixTwo.eval_inverse line 286
Source documentation
The inverse FFT uses the inverse root and one scalar normalization.
```
theorem eval_inverse {n : ℕ} (hn : 0<n) (ω : ℂ) (hω : IsPrimitiveRoot ω n)
    (x : Fin n → ℂ) :
    eval n ω⁻¹ (eval n ω x) = fun i => (n : ℂ) * x i := by
…
```
Mentions: OAI.ExactFourier.RadixTwo.eval
theorem OAI.ExactFourier.RadixTwo.eval_ofFn line 303
Source documentation
Polynomial evaluation of the vector of coefficients is exactly the DFT.
```
theorem eval_ofFn (n : ℕ) (ω : ℂ) (x : Fin n → ℂ) (i : Fin n) :
    (Polynomial.ofFn n x).eval (ω^i.val) = eval n ω x i := by
…
```
Mentions: OAI.ExactFourier.RadixTwo.eval
theorem OAI.ExactFourier.RadixTwo.convolution_formula line 315
Source documentation
Transform, multiply by precomputed scalar evaluations, inverse transform. The only degree condition is that the product is represented by fewer than n coefficients, so there is no wraparound.
```
theorem convolution_formula {n : ℕ} (hn : 0<n) (ω : ℂ) (hω : IsPrimitiveRoot ω n)
    (f g : ℂ[X]) (hfg : (f*g).natDegree < n) :
    eval n ω⁻¹ (fun i => (n : ℂ)⁻¹ * f.eval (ω^i.val) * g.eval (ω^i.val)) =
      fun i => (f*g).coeff i.val := by
…
```
Mentions: OAI.ExactFourier.RadixTwo.eval