OAI/Computability/FourierTransform/WordPrograms.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PowerSaving.RAM.Bench.Hue line 15
2. lemma OAI.PowerSaving.RAM.Bench.Hue.congr line 22
3. lemma OAI.PowerSaving.RAM.Bench.Hue.transfer line 24
4. lemma OAI.PowerSaving.RAM.Bench.Hue.zero line 27
5. lemma OAI.PowerSaving.RAM.Bench.Hue.one line 30
6. lemma OAI.PowerSaving.RAM.Bench.Hue.neg line 33
7. lemma OAI.PowerSaving.RAM.Bench.Hue.add line 36
8. lemma OAI.PowerSaving.RAM.Bench.Hue.sub line 39
9. lemma OAI.PowerSaving.RAM.Bench.Hue.mul line 42
10. lemma OAI.PowerSaving.RAM.Bench.Hue.inv line 45
11. lemma OAI.PowerSaving.RAM.Bench.Hue.div line 48
12. lemma OAI.PowerSaving.RAM.Bench.Hue.flip line 52
13. lemma OAI.PowerSaving.RAM.Bench.Hue.letterI line 56
14. lemma OAI.PowerSaving.RAM.Bench.Hue.casting line 59
15. lemma OAI.PowerSaving.RAM.Bench.Hue.numeral line 62
16. lemma OAI.PowerSaving.RAM.Bench.Hue.of_root line 64
17. lemma OAI.PowerSaving.RAM.Bench.Hue.exponent line 73
18. lemma OAI.PowerSaving.RAM.Bench.Hue.fork line 77
19. lemma OAI.PowerSaving.RAM.Bench.Hue.sum line 86
20. lemma OAI.PowerSaving.RAM.Bench.Hue.prod line 93
21. def OAI.PowerSaving.RAM.Bench.carried line 103

    Source comment

    easier lift over a scan on coordinates.

    def carried (p : ι→κ) (n : κ→ℕ) (i : During fun j => n (p j)) :
        During n := ⟨p i.i,i.j,i.hj⟩

    Mentions: OAI.PowerSaving.RAM.During

22. lemma OAI.PowerSaving.RAM.Bench.Feeds.carry line 106
23. def OAI.PowerSaving.RAM.Bench.Fabric line 111
24. lemma OAI.PowerSaving.RAM.Bench.Fabric.bright line 117
25. lemma OAI.PowerSaving.RAM.Bench.Fabric.dull line 119
26. lemma OAI.PowerSaving.RAM.Bench.Fabric.pick line 122
27. lemma OAI.PowerSaving.RAM.Bench.Fabric.transfer line 127
28. lemma OAI.PowerSaving.RAM.Bench.Fabric.congr line 131
29. lemma OAI.PowerSaving.RAM.Bench.Fabric.zero line 133
30. lemma OAI.PowerSaving.RAM.Bench.Fabric.one line 134
31. lemma OAI.PowerSaving.RAM.Bench.Fabric.flat line 135
32. lemma OAI.PowerSaving.RAM.Bench.Fabric.neg line 137
33. lemma OAI.PowerSaving.RAM.Bench.Fabric.add line 138
34. lemma OAI.PowerSaving.RAM.Bench.Fabric.sub line 140
35. lemma OAI.PowerSaving.RAM.Bench.Fabric.mul line 142
36. lemma OAI.PowerSaving.RAM.Bench.Fabric.inv line 144
37. lemma OAI.PowerSaving.RAM.Bench.Fabric.flip line 146
38. lemma OAI.PowerSaving.RAM.Bench.Fabric.supply line 149
39. lemma OAI.PowerSaving.RAM.Bench.Fabric.recover line 153