OAI/Computability/FourierTransform/PowerTables.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PowerSaving.RAM.Bench.Moves.branch line 16
2. lemma OAI.PowerSaving.RAM.Bench.Nick.branch line 27
3. lemma OAI.PowerSaving.RAM.Bench.tape_congr_sized line 31
4. lemma OAI.PowerSaving.RAM.Bench.pick_all line 35
5. def OAI.PowerSaving.RAM.Bench.tablePow line 40
6. lemma OAI.PowerSaving.RAM.Bench.unit_doubling line 43
7. lemma OAI.PowerSaving.RAM.Bench.pylon line 52
8. lemma OAI.PowerSaving.RAM.Bench.square_pow line 93

   Source comment

   index z^(j*j) for root z order d ≤ table length

   lemma square_pow (_h : Small b.size fun i => 2^k i)
       {z : ι→ℂ} {u : ι→ℕ}
       (g : b.Moves (fun _ => 0) (a sc) fun i => tablePow (z i) (k i)) (hk : b.Nick n)
       (hn : ∀ i,0<n i ∧ n i≤2^k i) (hz : ∀ i, z i^n i=1) (hu : b.Nick u) :
       b.Moves (fun _ => 0) sc fun i => epschirp (z i) (u i) :=
   …

   Mentions: OAI.PowerSaving.RAM.Small, OAI.PowerSaving.RAM.sc, OAI.PowerSaving.RAM.Bench.tablePow

9. lemma OAI.PowerSaving.RAM.Bench.padM line 105

   Source comment

   simple padded array

   lemma padM (_h : b.Nick n) (g : b.Nick k) {cl} {x : ι→Line}
       (hx : b.Moves (fun _ => 0) (a (c cl)) fun i => Tape.tab (n i) (x i)) :
       b.Moves k (a (c cl)) fun i => Tape.tab (k i) (padline (n i) (x i)) :=
   …

   Mentions: OAI.PowerSaving.Line, OAI.PowerSaving.Tape.tab