OAI/Computability/FourierTransform/RootPreparation.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PowerSaving.RAM.Bench.clearP line 17

   Source comment

   check nondivisibility for j = 2 to n-1

   def clearP (n : ℕ) : ℕ→ℕ
     | 0 => 1
     | j+1 => if 1<j ∧ n%j=0 then 0 else clearP n j

2. lemma OAI.PowerSaving.RAM.Bench.clearP_eq line 21
3. lemma OAI.PowerSaving.RAM.Bench.Grain.isBar line 39
4. def OAI.PowerSaving.RAM.Bench.cartTy line 60
5. def OAI.PowerSaving.RAM.Bench.cartT line 61
6. structure OAI.PowerSaving.RAM.Bench.Lade line 63
7. lemma OAI.PowerSaving.RAM.Bench.Lade.emptyL line 72
8. lemma OAI.PowerSaving.RAM.Bench.Lade.dimL line 77
9. lemma OAI.PowerSaving.RAM.Bench.Lade.volL line 79
10. lemma OAI.PowerSaving.RAM.Bench.Lade.dataL line 81
11. lemma OAI.PowerSaving.RAM.Bench.Lade.push line 85
12. lemma OAI.PowerSaving.RAM.Bench.reapL line 105
13. lemma OAI.PowerSaving.RAM.Bench.fillerL line 131
14. structure OAI.PowerSaving.RAM.Bench.Neaps line 145
15. lemma OAI.PowerSaving.RAM.Bench.Neaps.transfer line 154
16. lemma OAI.PowerSaving.RAM.Bench.Neaps.stackPow line 158
17. lemma OAI.PowerSaving.RAM.Bench.Neaps.siloS line 161
18. lemma OAI.PowerSaving.RAM.Bench.Neaps.siloG line 164
19. lemma OAI.PowerSaving.RAM.Bench.Neaps.powOrderS line 168
20. lemma OAI.PowerSaving.RAM.Bench.Neaps.orderS line 171
21. lemma OAI.PowerSaving.RAM.Bench.Neaps.orderG line 173
22. lemma OAI.PowerSaving.RAM.Bench.Neaps.powOrderG line 175
23. lemma OAI.PowerSaving.RAM.Bench.Neaps.bedL line 178
24. lemma OAI.PowerSaving.RAM.Bench.Neaps.bargeL line 182
25. lemma OAI.PowerSaving.RAM.Bench.Neaps.expressG line 186
26. lemma OAI.PowerSaving.RAM.Bench.Neaps.portG line 190
27. lemma OAI.PowerSaving.RAM.Bench.Neaps.receiptG line 197
28. lemma OAI.PowerSaving.RAM.Bench.Nick.stackH line 204
29. lemma OAI.PowerSaving.RAM.Bench.Nick.planOrder line 214