OAI/Computability/FourierTransform/WorkingPreparation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.RAM.Bench.shiftTy line 18

   Source comment

   count halving powers

   abbrev shiftTy := p w (p sc sc)

   Mentions: OAI.PowerSaving.RAM.sc

2. def OAI.PowerSaving.RAM.Bench.shiftP line 19
3. lemma OAI.PowerSaving.RAM.Bench.shiftP.stepP line 26
4. lemma OAI.PowerSaving.RAM.Bench.shiftP.real line 31
5. lemma OAI.PowerSaving.RAM.Bench.shiftP.countP line 47
6. lemma OAI.PowerSaving.RAM.Bench.shiftP.endP line 53
7. lemma OAI.PowerSaving.RAM.Bench.halveP line 58
8. lemma OAI.PowerSaving.RAM.Bench.Neaps.n_lt line 75
9. def OAI.PowerSaving.RAM.Bench.Neaps.layersP line 81
10. lemma OAI.PowerSaving.RAM.Bench.Neaps.layersG line 82
11. lemma OAI.PowerSaving.RAM.Bench.Neaps.layersS line 85
12. lemma OAI.PowerSaving.RAM.Bench.Neaps.layersBound line 87
13. lemma OAI.PowerSaving.RAM.Bench.Neaps.extractP line 98
14. lemma OAI.PowerSaving.RAM.Bench.Neaps.etaP line 109
15. lemma OAI.PowerSaving.RAM.Bench.Neaps.mediumP line 114
16. lemma OAI.PowerSaving.RAM.Bench.Neaps.ratioSq line 119
17. lemma OAI.PowerSaving.RAM.Bench.Neaps.ladeGrain line 130
18. lemma OAI.PowerSaving.RAM.Bench.Neaps.kilnP line 139
19. def OAI.PowerSaving.RAM.Bench.leg line 185
20. theorem OAI.PowerSaving.RAM.Bench.Neaps.streamP line 187