OAI/Computability/FourierTransform/ConvolutionProgram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.polyOf line 11

   Source comment

   correspondence lemma for polynomials in dense coefficient representation

   def polyOf (n : ℕ) (x : Vec n) : Polynomial ℂ :=
   …

   Mentions: OAI.PowerSaving.Vec

2. lemma OAI.PowerSaving.polyOf_mul line 14
3. lemma OAI.PowerSaving.polyOf_coeff_exact line 36
4. lemma OAI.PowerSaving.RAM.Bench.crossT line 45
5. def OAI.PowerSaving.RAM.Bench.stretch line 56
6. lemma OAI.PowerSaving.RAM.Bench.stretch_pos line 58
7. lemma OAI.PowerSaving.RAM.Bench.fusing line 60