OAI/Computability/FourierTransform/LocalPreparation.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.RAM.Bench.Dry line 15
2. structure OAI.PowerSaving.RAM.Bench.Grain line 18
3. lemma OAI.PowerSaving.RAM.Bench.Moves.dry line 24
4. lemma OAI.PowerSaving.RAM.Bench.Moves.dunes line 26
5. lemma OAI.PowerSaving.RAM.Bench.Nick.grain line 28
6. lemma OAI.PowerSaving.RAM.Bench.Dry.congr line 34
7. lemma OAI.PowerSaving.RAM.Bench.Dry.pair line 36
8. lemma OAI.PowerSaving.RAM.Bench.Dry.fst line 38
9. lemma OAI.PowerSaving.RAM.Bench.Dry.snd line 40
10. lemma OAI.PowerSaving.RAM.Bench.Dry.wc line 42
11. lemma OAI.PowerSaving.RAM.Bench.Dry.one line 43
12. lemma OAI.PowerSaving.RAM.Bench.Dry.mul line 44
13. lemma OAI.PowerSaving.RAM.Bench.Dry.inv line 46
14. lemma OAI.PowerSaving.RAM.Bench.Dry.transfer line 48
15. lemma OAI.PowerSaving.RAM.Bench.Dry.together line 51
16. lemma OAI.PowerSaving.RAM.Bench.Dry.look line 53
17. lemma OAI.PowerSaving.RAM.Bench.Dry.pick line 55
18. lemma OAI.PowerSaving.RAM.Bench.Dry.testz line 59
19. lemma OAI.PowerSaving.RAM.Bench.Dry.branch line 63
20. lemma OAI.PowerSaving.RAM.Bench.Grain.wc line 74
21. lemma OAI.PowerSaving.RAM.Bench.Grain.add line 75
22. lemma OAI.PowerSaving.RAM.Bench.Grain.sub line 78
23. lemma OAI.PowerSaving.RAM.Bench.Grain.mul line 81
24. lemma OAI.PowerSaving.RAM.Bench.Grain.div line 84
25. lemma OAI.PowerSaving.RAM.Bench.Grain.residue line 87
26. lemma OAI.PowerSaving.RAM.Bench.Grain.cmp line 90
27. lemma OAI.PowerSaving.RAM.Bench.Grain.congr line 93
28. lemma OAI.PowerSaving.RAM.Bench.Grain.transfer line 95
29. lemma OAI.PowerSaving.RAM.Bench.Grain.logtwo line 98
30. lemma OAI.PowerSaving.RAM.Bench.strideG line 105
31. lemma OAI.PowerSaving.RAM.Bench.chopG line 109
32. lemma OAI.PowerSaving.RAM.Bench.Dry.token line 113
33. lemma OAI.PowerSaving.RAM.Bench.cycleG line 117
34. lemma OAI.PowerSaving.RAM.Bench.arrayG line 123
35. lemma OAI.PowerSaving.RAM.Bench.Grain.twoPow line 127